dolmen

A parser library for automated deduction
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.std
Module Dolmen_std . Expr . Subst
type ('a, 'b) t

The type of substitutions from values of type 'a to values of type 'b.

val empty : ( 'a, 'b ) t

The empty substitution

val is_empty : ( 'a, 'b ) t -> bool

Test wether a substitution is empty

val iter : ( 'a -> 'b -> unit ) -> ( 'a, 'b ) t -> unit

Iterates over the bindings of the substitution.

val map : ( 'b -> 'c ) -> ( 'a, 'b ) t -> ( 'a, 'c ) t

Maps the given function over bound values

val fold : ( 'a -> 'b -> 'c -> 'c ) -> ( 'a, 'b ) t -> 'c -> 'c

Fold over the elements

val merge : ( 'a -> 'b option -> 'c option -> 'd option ) -> ( 'a, 'b ) t -> ( 'a, 'c ) t -> ( 'a, 'd ) t

Merge two substitutions

val filter : ( 'a -> 'b -> bool ) -> ( 'a, 'b ) t -> ( 'a, 'b ) t

Filter bindings base on a predicate.

val bindings : ( 'a, 'b ) t -> ('a * 'b) list

Returns the list of bindings ofa substitution.

val exists : ( 'a -> 'b -> bool ) -> ( 'a, 'b ) t -> bool

Tests wether the predicate holds for at least one binding.

val for_all : ( 'a -> 'b -> bool ) -> ( 'a, 'b ) t -> bool

Tests wether the predicate holds for all bindings.

val hash : ( 'b -> int ) -> ( 'a, 'b ) t -> int
val compare : ( 'b -> 'b -> int ) -> ( 'a, 'b ) t -> ( 'a, 'b ) t -> int
val equal : ( 'b -> 'b -> bool ) -> ( 'a, 'b ) t -> ( 'a, 'b ) t -> bool

Comparison and hash functions, with a comparison/hash function on values as parameter

val print : ( Stdlib.Format.formatter -> 'a -> unit ) -> ( Stdlib.Format.formatter -> 'b -> unit ) -> Stdlib.Format.formatter -> ( 'a, 'b ) t -> unit

Prints the substitution, using the given functions to print keys and values.

val debug : ( Stdlib.Format.formatter -> 'a -> unit ) -> ( Stdlib.Format.formatter -> 'b -> unit ) -> Stdlib.Format.formatter -> ( 'a, 'b ) t -> unit

Prints the substitution, using the given functions to print keys and values, includign some debug info.

val choose : ( 'a, 'b ) t -> 'a * 'b

Return one binding of the given substitution, or raise Not_found if the substitution is empty.

module type S = sig ... end
module Var : S with type 'a key = 'a id