dolmen
Library
Module
Module type
Parameter
Class
Class type
Type definitions
type location = Loc.t
type builtin =
The type of builtins symbols for terms. Some languages have specific syntax for logical connectives (tptp's'&&' or '' for isntance) whereas some (smtlib for instance) don't and treat them as constants.
type binder =
 All  (* Universal quantification. Each term in the list of quantified terms should represent a variable (optionnally typed using the 
 Ex  (* Existencial quantification Each term in the list of quantified terms should represent a variable (optionnally typed using the 
 Pi  (* Polymorphic type quantification in function type Each term in the list of quantified terms should represent a variable (optionnally typed using the 
 Arrow  (* The arrow binder, for function types. Allows for curified types, if wanted. *) 
 Let_seq  (* Let bindings (either propositional or for terms). Term bound by a let can have many forms depending on the language, but usual shapes are:

 Let_par  (* Similar to 
 Fun  (* Lambda, i.e function abstraction binder. Bound terms are the variables bound by the lambda, optionnally typed using the 
 Choice  (* Indefinite description, or epsilon terms. Likely to have its usual shape change following tptp's recent changes. *) 
 Description  (* Definite description. Likely to have its usual shape change following tptp's recent changes. *) 
The type of binders, these are pretty much always builtin in all languages.
type descr =
 Symbol of Id.t  (* Constants, variables, etc... any stringidentified nonbuiltin atomic term. *) 
 Builtin of builtin  (* Predefined builtins, i.e constants with lexical or syntaxic defintion in the source language. *) 
 Colon of t * t  (* Juxtaposition of terms, usually used to annotate a term with its type (for quantified variables, functions arguments, etc...). *) 
 App of t * t list  (* Higherorder application *) 
 Binder of binder * t list * t  (* Binder (quantifiers, local functions, ...), see the 
 Match of t * (t * t) list  (* Pattern matching, the list contains tuples of the form 
The AST for terms
The type of terms. A record containing an optional location, and a description of the term.
Standard functions
val print : Stdlib.Format.formatter > t > unit
val print_builtin : Stdlib.Format.formatter > builtin > unit
Printing functionson buffer and formatters.
Implemented interfaces
Include the Logic interface. This interface defines almost all term building functions that you may want to use.
include Dolmen_intf.Term.Logic
with type t := t
and type id := Id.t
and type location := location
Predefined terms
The terms representing equality and disequality, respectively.
The wildcard term, usually used in place of type arguments to explicit polymorphic functions to not explicit types that can be inferred by the typechecker.
The type of types, defined as specific token by the Zipperposition format; in other languages, will be represented as a constant (the "$tType" constant in tptp for instance). Used to define new types, or quantify type variables in languages that support polymorphism.
The type of propositions. Also defined as a lexical token by the Zipperposition format. Will be defined as a constant in most other languages (for instance, "$o" in tptp).
The type of boolean, defined as a specific token by the Altergo format; in other languages, it might be represented as a constant with a specific name.
The type unit, defined as a specific token by the Altergo format; in other languages, it might be represented as a constant with a specific name.
The type of integers, defined as a specific token by the Zipperposition and Altergo formats; in other languages, it might be represented as a constant with a specific name (for isntance, tptp's "$int") .
The type of integers, defined as a specific token by the Altergo format; in other languages, it might be represented as a constant with a specific name (for isntance, tptp's "$int") .
The type of bitvectors of the given constant length, defined as a specifi token by the Altergo format; in other languages, it might be represented as a constant with a specific name (for isntance, smtlib(s "bitv") .
The only value of type unit, defined as a specific token by the Altergo format.
The constants for the true and false propositional constants. Again defined as lexical token in the Zipperposition format, while treated as a constant in other languages ("$true" in tptp).
Standard logical connectives viewed as terms. implies_t
is usual right implication, i.e apply implies_t [p; q]
is "p implies q", while apply implied_t [p; q ]
means "p is implied by q" or "q implies p".
Term without semantic meaning, used for creating "data" terms. Used in tptp's annotations, and with similar meaning as smtlib's sexpressions (as used in the sexpr
function defined later).
Terms leaf constructors
Variable and constant constructors. While in some languages they can distinguished at the lexical level (in tptp for instance), in most languages, it is an issue dependant on scoping rules, so terms parsed from an smtlib file will have all variables parsed as constants.
Atoms are used for dimacs cnf parsing. Positive integers denotes variables, and negative integers denote the negation of the variable corresponding to their absolute value.
Used in tptp to specify constants different from other constants, for instance the 'distinct' "Apple" should be syntactically different from the "Apple" constant. Can be safely aliased to the const
function as the distinct
function is always given strings already enclosed with quotes, so in the example above, const
would be called with "Apple"
as string argument, while distinct
would be called with the string "\"Apple\""
Constructors for words defined as numeric or string formats by the languages specifications. These also can be safely aliased to const
, but then the provenance information is lost, which might complicate the task of a typechecker.
Bitvetor litteral, defined as a specific token in Altergo; Expects a decimal integer in the string to be extended as a bitvector.
Term constructors
Represents juxtaposition of two terms, usually denoted "t : t'" in most languages, and mainly used to annotated terms with their supposed, or defined, type.
Proposition construction functions. The conjunction and disjunction are nary instead of binary mostly because they are in smtlib (and that is subsumes the binary case).
Application constructor, seen as higher order application rather than firstorder application for the following reasons: being able to parse tptp's THF, having location attached to function symbols.
Conditional constructor, both for firstorder terms and propositions. Used in the following schema: ite condition then_branch else_branch
.
Pattern matching. The first term is the term to match, and each tuple in the list is a match case, which is a pair of a pattern and a match branch.
Binders for variables. Takes a list of terms as first argument for simplicity, the lists will almost always be a list of variables, optionally typed using the colon
term constructor.
 Pi is the polymorphic type quantification, for instance the polymorphic identity function has type: "Pi alpha. alpha > alpha"
 Letin is local binding, takes a list of equality of equivalences whose left handside is a variable. Letand is the parrallel version of Letin.
 Forall is universal quantification
 Par is universal quantification over type variables specifically (i.e. the same as forall, but only for a list of type variables, which thus may omit the
colon
annotations in the arguments).  Exists is existential quantification
 Lambda is used for function construction
 Choice is the choice operator, also called indefinite description, or also epsilon terms, i.e "Choice x. p(x)" is one "x" such that "p(x)" is true.
 Description is the definite description, i.e "Description x. p(x)" is the only "x" that satisfies p.
Type constructors
Function type constructor, for curryfied functions. Functions that takes multiple arguments in firstorder terms might take a product as only argument (see the following product
function) in some languages (e.g. tptp), or be curryfied using this constructor in other languages (e.g. altergo).
Product type constructor, used for instance in the types of functions that takes multiple arguments in a noncurry way.
Union type constructor, currently used in tptp's THF format.
Record constructors
Algebraic datatypes
Check whether some expression matches a given adt constructor (in head position).
Project a field of an adt constructor (usually unsafe except when guarded by an adt_check function).
Array constructors
Bitvector constructors
Arithmetic constructors
Triggers
Create a predicate for whether a term is within the given bounds (each bound is represented by a term which is tis value and a boolean which specifies whether it is strict or not).
Create a multitrigger (i.e. all terms in the lsit must match to trigger).
triggers ~loc f l
annotates formula/term f
with a list of triggers.
filters ~loc f l
annotates formula/term f
with a list of filters.
Special constructions
Attach a list of attributes (also called annotations) to a term. Attributes have no logical meaning (they can be safely ignored), but may serve to give hints or metainformation.
Term constructor not in implemented interfaces
The standalone term corresponding to the ifthenelse builtin construction.
Term inspection
Return the list of free variables (i.e currently, Ids that are in the Var
namespace).
Additional functions
add_attr attr term
rturns a term t
equal to term
, but with attr
added to the list of attributes.
Set the given list of terms as th attributes of the given term. Will fail (with an assertion) if the given term already have some assertion. In such cases, use add_attr instead.
Term mapping
The main use of terms mapper is to map fuctions over some terms. Traditionally, a mapping will usually only care about a few syntax cases and leav all other untouched. In these cases, it is useful to override the identity mapper, redefining only the fields needed.
type 'a mapper = {
symbol : 'a mapper > attr:t list > loc:location > Id.t > 'a; 
builtin : 'a mapper > attr:t list > loc:location > builtin > 'a; 
colon : 'a mapper > attr:t list > loc:location > t > t > 'a; 
app : 'a mapper > attr:t list > loc:location > t > t list > 'a; 
binder : 'a mapper >
attr:t list >
loc:location >
binder >
t list >
t >
'a; 
pmatch : 'a mapper > attr:t list > loc:location > t > (t * t) list > 'a; 
}
The type of a mapper on terms.
val unit_mapper : unit mapper
The unit mapper, i.e. an iterator.