package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type t = term

The type of terms and term variables.

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

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

type subst = (term_var, term) Subst.t

The type of substitutions over terms.

type 'a tag = 'a Tag.t

The type of tags used to annotate arbitrary terms.

val hash : t -> int

Hash function.

val equal : t -> t -> bool

Equality function.

val compare : t -> t -> int

Comparison function.

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

Printing function.

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

A module for Record fields.

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

Define a new record type.

val define_adt : ty_const -> ty_var list -> (string * (ty * string 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.

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 Field_expected of term_const

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

val ensure : t -> ty -> t

Ensure a term has the given type.

val of_var : Var.t -> t

Create a term from a variable

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

Polymorphic application.

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

Polymorphic application of a constructor.

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

Field access for a record.

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

Test expression for a constructor.

val pattern_match : t -> (pattern * t) list -> t

Create a pattern match.

val void : t

The only inhabitant of type unit.

val _true : t
val _false : t

Some usual formulas.

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

Real literals

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

Create a record

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

Record udpate

val eq : t -> t -> t

Build the equality of two terms.

val eqs : t list -> t

Build equalities with arbitrary arities.

val distinct : t list -> t

Distinct constraints on terms.

val neg : t -> t

Negation.

val _and : t list -> t

Conjunction of formulas

val _or : t list -> t

Disjunction of formulas

val nand : t -> t -> t

Negated conjunction.

val nor : t -> t -> t

Negated disjunction.

val xor : t -> t -> t

Exclusive disjunction.

val imply : t -> t -> t

Implication

val equiv : t -> t -> t

Equivalence

val select : t -> t -> t

Array selection.

val store : t -> t -> t -> t

Array store

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

val ex : (ty_var list * Var.t list) -> (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.

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

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

Let-binding. Variabels can be bound to either terms or formulas.

val ite : t -> t -> t -> t

ite condition then_t else_t creates a conditional branch.

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

Annotate the given formula wiht the tag and value.

val get_tag : t -> 'a tag -> 'a list

Return the list of values associated to the tag.

val get_tag_last : t -> 'a tag -> 'a option

Return the last value associated to the tag (if any).

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

Returns the list of free variables in the formula.

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

Substitution over terms.

module Bitv : sig ... end
module Float : sig ... end
module Int : sig ... end

Integer operations.

module Rat : sig ... end

Rational operations

module Real : sig ... end

Real operations

module String : sig ... end

String operations

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct