package dolmen_loop

  1. Overview
  2. Docs

Module T.TSource

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

The type of terms and term variables.

Sourceval ty : t -> Ty.t

Returns the type of a term.

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
Sourceval define_adt : Ty.Const.t -> Ty.Var.t list -> (string * (Ty.t * string option) list) list -> (Cstr.t * (Ty.t * 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.

Sourceval define_record : Ty.Const.t -> Ty.Var.t list -> (string * Ty.t) list -> Field.t list

Define a (previously abstract) type to be a record type, with the given fields.

Sourceexception Wrong_type of t * Ty.t

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.t

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.t

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.

Sourceval ensure : t -> Ty.t -> t

Ensure that a given term has the given type.

Sourceval of_var : Var.t -> t

Create a term from a variable

Sourceval apply : Const.t -> Ty.t list -> t list -> t

Polymorphic application.

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

Polymorphic application of a constructor.

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

Apply a field to a record.

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

Create a record.

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

Create an updated record

Sourceval _true : t
Sourceval _false : t

Some usual formulas.

Sourceval eq : t -> t -> t

Build the equality of two terms.

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

Not-and

Sourceval nor : t -> t -> t

Not-or

Sourceval imply : t -> t -> t

Implication

Sourceval equiv : t -> t -> t

Equivalence

Sourceval xor : t -> t -> t

Exclusive disjunction.

Sourceval all : (Ty.Var.t list * Var.t list) -> (Ty.Var.t 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.t list * Var.t list) -> (Ty.Var.t 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

Bind a variable to an expressions. This function is called when typing a let-binding, before the body of the let-binding is typed. The returned expressions is used to replace the variable everywhere in the body of the let-binding being typed.

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

Create a let-binding. This function is called after the body of the let-binding has been typed.

Sourceval pattern_match : t -> (t * t) list -> t

pattern_match scrutinee branches creates a pattern match expression on the scrutinee with the given branches, each of the form (pattern, body)

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

ite condition then_t else_t creates a conditional branch.

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

Annotate the given formula wiht the tag and value.

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

Returns the list of free variables in the formula.