Module type Term.Tff

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

type t

The type of terms and term variables.

type path

The type of patsh to constants.

type ty
type ty_var
type ty_const

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

type 'a tag

The type of tags used to annotate arbitrary terms.

val ty : t -> ty

Returns the type of a term.

module Var : sig ... end

A module for variables that occur in terms.

module Const : sig ... end

A module for constant symbols that occur in terms.

module Cstr : sig ... end

A module for Algebraic datatype constructors.

module Field : sig ... end
val define_adt : ty_const -> ty_var list -> (path * (ty * path option) list) list -> (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.

val define_record : ty_const -> ty_var list -> (path * ty) list -> Field.t list

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

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

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

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

exception Field_repeated of Field.t

Field repeated in a record expression.

exception Field_missing of Field.t

Field missing in a record expression.

exception Pattern_expected of t

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

exception Empty_pattern_matching

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

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

exception Over_application of t list

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

exception Bad_poly_arity of ty_var list * ty list

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

val ensure : t -> ty -> t

Ensure that a given term has the given type.

val of_var : Var.t -> t

Create a term from a variable

val apply_cst : Const.t -> ty list -> t list -> t

Polymorphic application of a constant.

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

Polymorphic application of a constructor.

val apply_field : Field.t -> t -> t

Apply a field to a record.

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

Create a record.

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

Create an updated record

val cstr_tester : Cstr.t -> t -> t

Given a constructor c and a term t, returns a terms that evaluates to true iff t has c as head constructor.

val _and : t list -> t

Conjunction of formulas

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

Create a local function.

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

Universally quantify the given formula over the type and terms variables.

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

Existencially quantify the given formula over the type and terms variables.

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

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

Create a sequential let-binding.

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

Create a parrallel let-binding.

val pattern_match : ?redundant:( t -> unit ) -> 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)

val set_tag : t -> 'a tag -> 'a -> unit

Annotate the given formula wiht the tag and value.

val add_tag : t -> 'a list tag -> 'a -> unit

Add a value to the list of values bound to a tag.

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

Returns the list of free variables in the formula.