Module Expr.TermSource

Signature required by terms for typing first-order polymorphic terms.

Sourcetype t = term

The type of terms and term variables.

Sourcetype ty = Ty.t
Sourcetype ty_var = Ty.Var.t
Sourcetype ty_const = Ty.Const.t

The representation of term types, type variables, and type constants.

Sourcetype subst = (term_var, term) Subst.t

The type of substitutions over terms.

Sourcetype 'a tag = 'a Tag.t

The type of tags used to annotate arbitrary terms.

Sourceval hash : t -> int

Hash function.

Sourceval equal : t -> t -> bool

Equality function.

Sourceval compare : t -> t -> int

Comparison function.

Sourceval print : Format.formatter -> t -> unit

Printing function.

Sourceval ty : t -> ty

Returns the type of a term.

Sourceval get_tag : t -> 'a Tag.t -> 'a option

Get the value bound to a tag.

Sourceval get_tag_list : t -> 'a list Tag.t -> 'a list

Get the list of values bound to a list tag, returning the empty list if no value is bound.

Sourceval get_tag_last : t -> 'a list Tag.t -> 'a option

Get the last value bound to a list tag.

Sourceval set_tag : t -> 'a Tag.t -> 'a -> unit

Set the value bound to the tag.

Sourceval add_tag : t -> 'a list Tag.t -> 'a -> unit

Bind an additional value to a list tag.

Sourceval add_tag_opt : t -> 'a list Tag.t -> 'a option -> unit

Optionally bind an additional value to a list tag.

Sourceval add_tag_list : t -> 'a list Tag.t -> 'a list -> unit

Bind a list of additional values to a list tag.

Sourceval unset_tag : t -> _ Tag.t -> unit

Remove the binding to the given tag.

Sourcemodule Var : sig ... end

A module for variables that occur in terms.

Sourcemodule Const : sig ... end

A module for constant symbols that occur in terms.

Sourcemodule Cstr : sig ... end

A module for Algebraic datatype constructors.

Sourcemodule Field : sig ... end

A module for Record fields.

Sourceval define_record : ty_const -> ty_var list -> (Path.t * ty) list -> Ty.def * Field.t list

Define a new record type.

Sourceval define_adt : ty_const -> ty_var list -> (Path.t * (ty * Path.t option) list) list -> Ty.def * (Cstr.t * (ty * Const.t option) list) list

define_aft t vars cstrs defines the type constant t, parametrised over the type variables ty_vars as defining an algebraic datatypes with constructors cstrs. cstrs is a list where each elements of the form (name, l) defines a new constructor for the algebraic datatype, with the given name. The list l defines the arguments to said constructor, each element of the list giving the type ty of the argument expected by the constructor (which may contain any of the type variables in vars), as well as an optional destructor name. If the construcotr name is Some s, then the ADT definition also defines a function that acts as destructor for that particular field. This polymorphic function is expected to takes as arguments as many types as there are variables in vars, an element of the algebraic datatype being defined, and returns a value for the given field. For instance, consider the following definition for polymorphic lists: define_adt list [ty_var_a] [ "nil", []; "const", [ (Ty.of_var ty_var_a , Some "hd"); (ty_list_a , Some "tl"); ]; ] This definition defines the usual type of polymorphic linked lists, as well as two destructors "hd" and "tl". "hd" would have type forall alpha. alpha list -> a, and be the partial function returning the head of the list.

Sourceexception Wrong_type of t * ty

Exception raised in case of typing error during term construction. Wrong_type (t, ty) should be raised by term constructor functions when some term t is expected to have type ty, but does not have that type.

Sourceexception Wrong_sum_type of Cstr.t * ty

Raised when some constructor was expected to belong to some type but does not belong to the given type.

Sourceexception Wrong_record_type of Field.t * ty_const

Exception raised in case of typing error during term construction. This should be raised when the returned field was expected to be a field for the returned record type constant, but it was of another record type.

Sourceexception Field_repeated of Field.t

Field repeated in a record expression.

Sourceexception Field_missing of Field.t

Field missing in a record expression.

Sourceexception Field_expected of term_cst

A field was expected but the returned term constant is not a record field.

Sourceexception Pattern_expected of t

Raised when trying to create a pattern matching, but a non-pattern term was provided where a pattern was expected.

Sourceexception Empty_pattern_matching

Raise when creating a pattern matching but an empty list of branches was provided

Sourceexception Partial_pattern_match of t list

Raised when a partial pattern matching was created. A list of terms not covered by the patterns is provided.

Sourceexception Constructor_expected of Cstr.t

Raised when trying to access the tester of an ADT constructor, but the constant provided was not a constructor.

Sourceexception Over_application of t list

Raised when an application was provided too many term arguments. The extraneous arguments are returned by the exception.

Sourceexception Bad_poly_arity of ty_var list * ty list

Raised when a polymorphic application does not have an adequate number of arguments.

Sourceval ensure : t -> ty -> t

Ensure a term has the given type.

Sourceval of_var : Var.t -> t

Create a term from a variable

Sourceval of_cst : Const.t -> t

Create a term from a constant.

Sourceval apply : t -> ty list -> t list -> t

Polymorphic application.

Sourceval apply_cst : term_cst -> ty list -> t list -> t

Polymorphic application of a constructor.

Sourceval apply_cstr : Cstr.t -> ty list -> t list -> t

Polymorphic application of a constructor.

Sourceval apply_field : Field.t -> t -> t

Field access for a record.

Sourceval cstr_tester : Cstr.t -> t -> t

Test expression for a constructor.

Sourceval pattern_match : ?redundant:(pattern -> unit) -> t -> (pattern * t) list -> t

Create a pattern match.

Sourceval void : t

The only inhabitant of type unit.

Sourceval _true : t
Sourceval _false : t

Some usual formulas.

Sourceval int : string -> t
Sourceval rat : string -> t
Sourceval real : string -> t

Real literals

Sourceval record : (Field.t * t) list -> t

Create a record

Sourceval record_with : t -> (Field.t * t) list -> t

Record udpate

Sourceval eq : t -> t -> t

Build the equality of two terms.

Sourceval eqs : t list -> t

Build equalities with arbitrary arities.

Sourceval neq : t -> t -> t

Disequality

Sourceval distinct : t list -> t

Distinct constraints on terms.

Sourceval neg : t -> t

Negation.

Sourceval _and : t list -> t

Conjunction of formulas

Sourceval _or : t list -> t

Disjunction of formulas

Sourceval nand : t -> t -> t

Negated conjunction.

Sourceval nor : t -> t -> t

Negated disjunction.

Sourceval xor : t -> t -> t

Exclusive disjunction.

Sourceval imply : t -> t -> t

Implication

Sourceval implied : t -> t -> t

Reverse Implication

Sourceval equiv : t -> t -> t

Equivalence

Sourceval lam : (ty_var list * Var.t list) -> t -> t

Create a local function. The first pair of arguments are the variables that are free in the resulting quantified formula, and the second pair are the variables bound.

Sourceval all : (ty_var list * Var.t list) -> t -> t

Universally quantify the given formula over the type and terms variables. The first pair of arguments are the variables that are free in the resulting quantified formula, and the second pair are the variables bound.

Sourceval ex : (ty_var list * Var.t list) -> t -> t

Existencially quantify the given formula over the type and terms variables. The first pair of arguments are the variables that are free in the resulting quantified formula, and the second pair are the variables bound.

Sourceval bind : Var.t -> t -> t

Tag the given variable with the term, to mark it has been let-bound. Views might use that information to transparently replace a let-bound variable with its defining term.

Sourceval letin : (Var.t * t) list -> t -> t

Sequential let-binding. Variables can be bound to either terms or formulas.

Sourceval letand : (Var.t * t) list -> t -> t

Parrallel let-binding. Variables can be bound to either terms or formulas.

Sourceval ite : t -> t -> t -> t

ite condition then_t else_t creates a conditional branch.

Sourceval fv : t -> ty_var list * Var.t list

Returns the list of free variables in the formula.

Sourceval subst : ?fix:bool -> Ty.subst -> subst -> t -> t

Substitution over terms.

Sourceval multi_trigger : t list -> t

Create a multi trigger from a list of arbtirary terms.

Sourceval semantic_trigger : t -> t

Semantic triggers.

Sourceval maps_to : Var.t -> t -> t

Variable mapping to term.

Sourcemodule Array : sig ... end
Sourcemodule Bitv : sig ... end
Sourcemodule Float : sig ... end
Sourcemodule Int : sig ... end

Integer operations.

Sourcemodule Rat : sig ... end

Rational operations

Sourcemodule Real : sig ... end

Real operations

Sourcemodule String : sig ... end

String operations