dolmen_type

A typechecker for automated deduction languages
IN THIS PACKAGE
val empty : Type.T.t

The empty regular language.

val all : Type.T.t

The language that contains all strings

val allchar : Type.T.t

The language that contains all strings of length 1

val of_string : Type.T.t -> Type.T.t

Singleton language containing a single string.

val range : Type.T.t -> Type.T.t -> Type.T.t

range s1 s2 is the language containing all singleton strings (i.e. string of length 1) that are lexicographically beetween s1 and s2, **assuming s1 and s2 are singleton strings**. Else it is the empty language.

val concat : Type.T.t -> Type.T.t -> Type.T.t

Language concatenation.

val union : Type.T.t -> Type.T.t -> Type.T.t

Language union.

val inter : Type.T.t -> Type.T.t -> Type.T.t

language intersection.

val star : Type.T.t -> Type.T.t

Kleene closure.

val cross : Type.T.t -> Type.T.t

Kleene cross. cross e abreviates concat e (star e)

val complement : Type.T.t -> Type.T.t

Complement.

val diff : Type.T.t -> Type.T.t -> Type.T.t

Difference

val option : Type.T.t -> Type.T.t

Option. option e abbreviates union e (of_string "")

val power : int -> Type.T.t -> Type.T.t

power n e is n-th power of e.

val loop : int -> int -> Type.T.t -> Type.T.t

Loop. See SMTLIb documentation.