dolmen 0.7 · OCaml Package

Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Mainly used to parse first-order terms, it is also used to parse tptp's THF language, which uses higher order terms, so some first-order constructs such as conjunction, equality, etc... also need to be represented by standalone terms.

type t

The type of terms.

Predefined terms

val eq_t : ?loc:L.t -> unit -> t

val neq_t : ?loc:L.t -> unit -> t

The terms representing equality and disequality, respectively.

val wildcard : ?loc:L.t -> unit -> t

The wildcard term, usually used in place of type arguments to explicit polymorphic functions to not explicit types that can be inferred by the type-checker.

val tType : ?loc:L.t -> unit -> t

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.

val prop : ?loc:L.t -> unit -> t

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

val bool : ?loc:L.t -> unit -> t

The type of boolean, defined as a specific token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name.

val ty_unit : ?loc:L.t -> unit -> t

The type unit, defined as a specific token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name.

val ty_int : ?loc:L.t -> unit -> t

The type of integers, defined as a specific token by the Zipperposition and Alt-ergo formats; in other languages, it might be represented as a constant with a specific name (for isntance, tptp's "$int") .

val ty_real : ?loc:L.t -> unit -> t

The type of integers, defined as a specific token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name (for isntance, tptp's "$int") .

val ty_bitv : ?loc:L.t -> int -> t

The type of bitvectors of the given constant length, defined as a specifi token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name (for isntance, smtlib(s "bitv") .

val void : ?loc:L.t -> unit -> t

The only value of type unit, defined as a specific token by the Alt-ergo format.

val true_ : ?loc:L.t -> unit -> t

val false_ : ?loc:L.t -> unit -> t

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

val not_t : ?loc:L.t -> unit -> t

val or_t : ?loc:L.t -> unit -> t

val and_t : ?loc:L.t -> unit -> t

val xor_t : ?loc:L.t -> unit -> t

val nor_t : ?loc:L.t -> unit -> t

val nand_t : ?loc:L.t -> unit -> t

val equiv_t : ?loc:L.t -> unit -> t

val implied_t : ?loc:L.t -> unit -> t

val implies_t : ?loc:L.t -> unit -> t

val pi_t : ?loc:L.t -> unit -> t

val sigma_t : ?loc:L.t -> unit -> t

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

val data_t : ?loc:L.t -> unit -> t

Term without semantic meaning, used for creating "data" terms. Used in tptp's annotations, and with similar meaning as smtlib's s-expressions (as used in the sexpr function defined later).

Terms leaf constructors

val var : ?loc:L.t -> I.t -> t

val const : ?loc:L.t -> I.t -> t

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.

val atom : ?loc:L.t -> int -> t

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.

val distinct : ?loc:L.t -> I.t -> t

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\""

val str : ?loc:L.t -> string -> t

val int : ?loc:L.t -> string -> t

val rat : ?loc:L.t -> string -> t

val real : ?loc:L.t -> string -> t

val hexa : ?loc:L.t -> string -> t

val binary : ?loc:L.t -> string -> t

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 type-checker.

val bitv : ?loc:L.t -> string -> t

Bitvetor litteral, defined as a specific token in Alt-ergo; Expects a decimal integer in the string to be extended as a bitvector.

Term constructors

val colon : ?loc:L.t -> t -> t -> t

Represents juxtaposition of two terms, usually denoted "t : t'" in most languages, and mainly used to annotated terms with their supposed, or defined, type.

val eq : ?loc:L.t -> t -> t -> t

val neq : ?loc:L.t -> t list -> t

Equality and dis-equality of terms.

val not_ : ?loc:L.t -> t -> t

val or_ : ?loc:L.t -> t list -> t

val and_ : ?loc:L.t -> t list -> t

val xor : ?loc:L.t -> t -> t -> t

val imply : ?loc:L.t -> t -> t -> t

val equiv : ?loc:L.t -> t -> t -> t

Proposition construction functions. The conjunction and disjunction are n-ary instead of binary mostly because they are in smtlib (and that is subsumes the binary case).

val apply : ?loc:L.t -> t -> t list -> t

Application constructor, seen as higher order application rather than first-order application for the following reasons: being able to parse tptp's THF, having location attached to function symbols.

val ite : ?loc:L.t -> t -> t -> t -> t

Conditional constructor, both for first-order terms and propositions. Used in the following schema: ite condition then_branch else_branch.

val match_ : ?loc:L.t -> t -> (t * t) list -> t

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.

val pi : ?loc:L.t -> t list -> t -> t

val par : ?loc:L.t -> t list -> t -> t

val letin : ?loc:L.t -> t list -> t -> t

val letand : ?loc:L.t -> t list -> t -> t

val forall : ?loc:L.t -> t list -> t -> t

val exists : ?loc:L.t -> t list -> t -> t

val lambda : ?loc:L.t -> t list -> t -> t

val choice : ?loc:L.t -> t list -> t -> t

val description : ?loc:L.t -> t list -> t -> t

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 hand-side 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

val arrow : ?loc:L.t -> t -> t -> t

Function type constructor, for curryfied functions. Functions that takes multiple arguments in first-order 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. alt-ergo).

val product : ?loc:L.t -> t -> t -> t

Product type constructor, used for instance in the types of functions that takes multiple arguments in a non-curry way.

val union : ?loc:L.t -> t -> t -> t

Union type constructor, currently used in tptp's THF format.

val subtype : ?loc:L.t -> t -> t -> t

Subtype relation for types.

Record constructors

val record : ?loc:L.t -> t list -> t

Create a record expression.

val record_with : ?loc:L.t -> t -> t list -> t

Record "with" update (e.g. " r with ....").

val record_access : ?loc:L.t -> t -> I.t -> t

Field record access.

Algebraic datatypes

val adt_check : ?loc:L.t -> t -> I.t -> t

Check whether some expression matches a given adt constructor (in head position).

val adt_project : ?loc:L.t -> t -> I.t -> t

Project a field of an adt constructor (usually unsafe except when guarded by an adt_check function).

Array constructors

val array_get : ?loc:L.t -> t -> t -> t

Array getter.

val array_set : ?loc:L.t -> t -> t -> t -> t

Array setter.

Bitvector constructors

val bitv_extract : ?loc:L.t -> t -> int -> int -> t

Bitvector extraction.

val bitv_concat : ?loc:L.t -> t -> t -> t

Bitvector concatenation.

Arithmetic constructors

val uminus : ?loc:L.t -> t -> t

Arithmetic unary minus.

val add : ?loc:L.t -> t -> t -> t

Arithmetic addition.

val sub : ?loc:L.t -> t -> t -> t

Arithmetic substraction.

val mult : ?loc:L.t -> t -> t -> t

Arithmetic multiplication.

val div : ?loc:L.t -> t -> t -> t

Arithmetic division quotient.

val mod_ : ?loc:L.t -> t -> t -> t

Arithmetic modulo (aka division reminder).

val int_pow : ?loc:L.t -> t -> t -> t

Integer power.

val real_pow : ?loc:L.t -> t -> t -> t

Real power.

val lt : ?loc:L.t -> t -> t -> t

Arithmetic "lesser than" comparison (strict).

val leq : ?loc:L.t -> t -> t -> t

Arithmetic "lesser or equal" comparison.

val gt : ?loc:L.t -> t -> t -> t

Arithmetic "greater than" comparison (strict).

val geq : ?loc:L.t -> t -> t -> t

Arithmetic "greater or equal" comparison.

Triggers

val in_interval : ?loc:L.t -> t -> (t * bool) -> (t * bool) -> t

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

val maps_to : ?loc:L.t -> I.t -> t -> t

Id mapping (see alt-ergo).

val trigger : ?loc:L.t -> t list -> t

Create a multi-trigger (i.e. all terms in the lsit must match to trigger).

val triggers : ?loc:L.t -> t -> t list -> t

triggers ~loc f l annotates formula/term f with a list of triggers.

val filters : ?loc:L.t -> t -> t list -> t

filters ~loc f l annotates formula/term f with a list of filters.

Special constructions

val tracked : ?loc:L.t -> I.t -> t -> t

Name a term for tracking purposes.

val quoted : ?loc:L.t -> string -> t

Create an attribute from a quoted string (in Zf).

val sequent : ?loc:L.t -> t list -> t list -> t

Sequents as terms

val check : ?loc:L.t -> t -> t

Check a term (see alt-ergo).

val cut : ?loc:L.t -> t -> t

Create a cut (see alt-ergo).

val annot : ?loc:L.t -> t -> t list -> t

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 meta-information.

val sexpr : ?loc:L.t -> t list -> t

S-expressions (for smtlib attributes), should probably be related to the data_t term.

package dolmen