Module Dolmen_std.TermSource

Standard implementation of terms

Type definitions

Sourcetype location = Loc.t
Sourcetype builtin =
  1. | Wildcard
    (*

    Wildcard symbol, i.e placeholder for an expression to be inferred, typically during type-checking.

    *)
  2. | Ttype
    (*

    Builtin symbol for the type of Types.

    *)
  3. | Unit
    (*

    Unit type.

    *)
  4. | Void
    (*

    Only inhabitant of the unit type.

    *)
  5. | Prop
    (*

    Builtin symbol for the type of propositions.

    *)
  6. | Bool
    (*

    The boolean type.

    *)
  7. | True
    (*

    The true propositional constant.

    *)
  8. | False
    (*

    The false propositional constant.

    *)
  9. | Eq
    (*

    Should all arguments be pariwise equal ?

    *)
  10. | Distinct
    (*

    Should all arguments be pairwise distinct ?

    *)
  11. | Ite
    (*

    Condional, usually applied to 3 terms (the condition, the then branch and the else branch).

    *)
  12. | Sequent
    (*

    Sequent as term, usually takes two argument (left side, and right side of the sequent), which are respectively a conjunction and a disjunction of propositional formulas.

    *)
  13. | Int
    (*

    Builtin integer type. Currently specific to Zipperposition and alt-ergo format; other languages might use constants with pre-defined name, such as tptp's "$int".

    *)
  14. | Real
    (*

    Builtin real type. Currently specific to Alt-ergo format; other languages might use constants with pre-defined name, such as smtlib's "real".

    *)
  15. | Minus
    (*

    Arithmetic unary minus.

    *)
  16. | Add
    (*

    Arithmetic addition.

    *)
  17. | Sub
    (*

    Arithmetic substraction.

    *)
  18. | Mult
    (*

    Arithmetic multiplication.

    *)
  19. | Div
    (*

    Arithmetic division quotient

    *)
  20. | Mod
    (*

    Arithmetic division modulo

    *)
  21. | Int_pow
    (*

    Integer exponentiation.

    *)
  22. | Real_pow
    (*

    Real exponentiation.

    *)
  23. | Lt
    (*

    Arithmetic "less than" comparison (strict).

    *)
  24. | Leq
    (*

    Arithmetic "lesser or equal" comparison.

    *)
  25. | Gt
    (*

    Arithmetic "greater than" comparison.

    *)
  26. | Geq
    (*

    Arithmetic "greater or equal" comparison.

    *)
  27. | Subtype
    (*

    Subtyping relation

    *)
  28. | Product
    (*

    Product type constructor

    *)
  29. | Union
    (*

    Union type constructor

    *)
  30. | Pi
    (*

    Pi: higher-order encoding of the forall quantifier as a constant.

    *)
  31. | Sigma
    (*

    Sigma: higher-order envoding of the exists quantifier of a constant.

    *)
  32. | Not
    (*

    Propositional negation

    *)
  33. | And
    (*

    Propositional conjunction

    *)
  34. | Or
    (*

    Propositional disjunction

    *)
  35. | Nand
    (*

    Propositional not-and connective

    *)
  36. | Xor
    (*

    Propositional exclusive disjunction

    *)
  37. | Nor
    (*

    Propositional not-or

    *)
  38. | Imply
    (*

    Propositional implication

    *)
  39. | Implied
    (*

    Propositional left implication (i.e implication with reversed arguments).

    *)
  40. | Equiv
    (*

    Propositional equivalence

    *)
  41. | Bitv of int
    (*

    Bitvector type (with given length)

    *)
  42. | Bitv_extract of int * int
    (*

    Bitvector extraction

    *)
  43. | Bitv_concat
    (*

    Bitvector concatenation

    *)
  44. | Array_get
    (*

    Array getter.

    *)
  45. | Array_set
    (*

    Array setter.

    *)
  46. | Adt_check
    (*

    Algebraic datatype head constructore checker.

    *)
  47. | Adt_project
    (*

    Algebraic datatype projection.

    *)
  48. | Record
    (*

    Record creation

    *)
  49. | Record_with
    (*

    Record "with" creation

    *)
  50. | Record_access
    (*

    Record field access

    *)
  51. | Multi_trigger
  52. | Maps_to
    (*

    Mapping; used in Alt-ergo triggers.

    *)
  53. | In_interval of bool * bool
    (*

    Interval check; used in Alt-ergo triggers

    *)
  54. | Check
    (*

    Similar to cut, but does not introduce the proved term into the axioms.

    *)
  55. | Cut
    (*

    Insert a cut of the given term.

    *)
  56. | Sexpr
    (*

    Head symbol for s-exprs in smtlib.

    *)

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.

Sourcetype binder =
  1. | All
    (*

    Universal quantification. Each term in the list of quantified terms should represent a variable (optionnally typed using the Colon constructor.

    *)
  2. | Ex
    (*

    Existencial quantification Each term in the list of quantified terms should represent a variable (optionnally typed using the Colon constructor.

    *)
  3. | Pi
    (*

    Polymorphic type quantification in function type Each term in the list of quantified terms should represent a variable (optionnally typed using the Colon constructor.

    *)
  4. | Arrow
    (*

    The arrow binder, for function types. Allows for curified types, if wanted.

    *)
  5. | 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:

    • an equality (using the builtin Eq) between a variable (optionnally typed using the Colon constructor), and a term (e.g. in tptp)
    • an equivalence (using the builtin Equiv) between a variable (optionnally typed using the Colon constructor), and a term/proposition (e.g. in tptp)
    • a variable and a term juxtaposed using the Colon constructor (e.g. in smtlib)
    *)
  6. | Let_par
    (*

    Similar to Let_seq; except that the list of bindings should be considered all bound at the same time/level/scope. More precisely, for Let_seq, the list of bindings is to be understood sequentially (i.e. Let_seq (b1 :: b2 ...) is semantically the same as Let_seq b1 (Let_seq b2 (..)). For Let_par, the list of bindings all happen at the same time: the defining expressions of each binding cannot refer to other bindings in the same parralel let-binding.

    *)
  7. | Fun
    (*

    Lambda, i.e function abstraction binder. Bound terms are the variables bound by the lambda, optionnally typed using the Colon constructor.

    *)
  8. | Choice
    (*

    Indefinite description, or epsilon terms. Likely to have its usual shape change following tptp's recent changes.

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

Sourcetype descr =
  1. | Symbol of Id.t
    (*

    Constants, variables, etc... any string-identified non-builtin atomic term.

    *)
  2. | Builtin of builtin
    (*

    Predefined builtins, i.e constants with lexical or syntaxic defintion in the source language.

    *)
  3. | Colon of t * t
    (*

    Juxtaposition of terms, usually used to annotate a term with its type (for quantified variables, functions arguments, etc...).

    *)
  4. | App of t * t list
    (*

    Higher-order application

    *)
  5. | Binder of binder * t list * t
    (*

    Binder (quantifiers, local functions, ...), see the binder type for more information.

    *)
  6. | Match of t * (t * t) list
    (*

    Pattern matching, the list contains tuples of the form (pattern,branch).

    *)

The AST for terms

Sourceand t = {
  1. term : descr;
  2. attr : t list;
  3. loc : location;
}

The type of terms. A record containing an optional location, and a description of the term.

Standard functions

Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int

Equality and comparison

Sourceval print : Format.formatter -> t -> unit
Sourceval print_builtin : 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

Sourceval eq_t : ?loc:location -> unit -> t
Sourceval neq_t : ?loc:location -> unit -> t

The terms representing equality and disequality, respectively.

Sourceval wildcard : ?loc:location -> 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.

Sourceval tType : ?loc:location -> 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.

Sourceval prop : ?loc:location -> 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).

Sourceval bool : ?loc:location -> 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.

Sourceval ty_unit : ?loc:location -> 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.

Sourceval ty_int : ?loc:location -> 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") .

Sourceval ty_real : ?loc:location -> 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") .

Sourceval ty_bitv : ?loc:location -> 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") .

Sourceval void : ?loc:location -> unit -> t

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

Sourceval true_ : ?loc:location -> unit -> t
Sourceval false_ : ?loc:location -> 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).

Sourceval not_t : ?loc:location -> unit -> t
Sourceval or_t : ?loc:location -> unit -> t
Sourceval and_t : ?loc:location -> unit -> t
Sourceval xor_t : ?loc:location -> unit -> t
Sourceval nor_t : ?loc:location -> unit -> t
Sourceval nand_t : ?loc:location -> unit -> t
Sourceval equiv_t : ?loc:location -> unit -> t
Sourceval implied_t : ?loc:location -> unit -> t
Sourceval implies_t : ?loc:location -> unit -> t
Sourceval pi_t : ?loc:location -> unit -> t
Sourceval sigma_t : ?loc:location -> 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".

Sourceval data_t : ?loc:location -> 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

Sourceval var : ?loc:location -> Id.t -> t
Sourceval const : ?loc:location -> Id.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.

Sourceval atom : ?loc:location -> 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.

Sourceval distinct : ?loc:location -> Id.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\""

Sourceval str : ?loc:location -> string -> t
Sourceval int : ?loc:location -> string -> t
Sourceval rat : ?loc:location -> string -> t
Sourceval real : ?loc:location -> string -> t
Sourceval hexa : ?loc:location -> string -> t
Sourceval binary : ?loc:location -> 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.

Sourceval bitv : ?loc:location -> string -> t

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

Term constructors

Sourceval colon : ?loc:location -> 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.

Sourceval eq : ?loc:location -> t -> t -> t
Sourceval neq : ?loc:location -> t list -> t

Equality and dis-equality of terms.

Sourceval not_ : ?loc:location -> t -> t
Sourceval or_ : ?loc:location -> t list -> t
Sourceval and_ : ?loc:location -> t list -> t
Sourceval xor : ?loc:location -> t -> t -> t
Sourceval imply : ?loc:location -> t -> t -> t
Sourceval equiv : ?loc:location -> 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).

Sourceval apply : ?loc:location -> 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.

Sourceval ite : ?loc:location -> t -> t -> t -> t

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

Sourceval match_ : ?loc:location -> 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.

Sourceval pi : ?loc:location -> t list -> t -> t
Sourceval par : ?loc:location -> t list -> t -> t
Sourceval letin : ?loc:location -> t list -> t -> t
Sourceval letand : ?loc:location -> t list -> t -> t
Sourceval forall : ?loc:location -> t list -> t -> t
Sourceval exists : ?loc:location -> t list -> t -> t
Sourceval lambda : ?loc:location -> t list -> t -> t
Sourceval choice : ?loc:location -> t list -> t -> t
Sourceval description : ?loc:location -> 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

Sourceval arrow : ?loc:location -> 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).

Sourceval product : ?loc:location -> t -> t -> t

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

Sourceval union : ?loc:location -> t -> t -> t

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

Sourceval subtype : ?loc:location -> t -> t -> t

Subtype relation for types.

Record constructors

Sourceval record : ?loc:location -> t list -> t

Create a record expression.

Sourceval record_with : ?loc:location -> t -> t list -> t

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

Sourceval record_access : ?loc:location -> t -> Id.t -> t

Field record access.

Algebraic datatypes

Sourceval adt_check : ?loc:location -> t -> Id.t -> t

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

Sourceval adt_project : ?loc:location -> t -> Id.t -> t

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

Array constructors

Sourceval array_get : ?loc:location -> t -> t -> t

Array getter.

Sourceval array_set : ?loc:location -> t -> t -> t -> t

Array setter.

Bitvector constructors

Sourceval bitv_extract : ?loc:location -> t -> int -> int -> t

Bitvector extraction.

Sourceval bitv_concat : ?loc:location -> t -> t -> t

Bitvector concatenation.

Arithmetic constructors

Sourceval uminus : ?loc:location -> t -> t

Arithmetic unary minus.

Sourceval add : ?loc:location -> t -> t -> t

Arithmetic addition.

Sourceval sub : ?loc:location -> t -> t -> t

Arithmetic substraction.

Sourceval mult : ?loc:location -> t -> t -> t

Arithmetic multiplication.

Sourceval div : ?loc:location -> t -> t -> t

Arithmetic division quotient.

Sourceval mod_ : ?loc:location -> t -> t -> t

Arithmetic modulo (aka division reminder).

Sourceval int_pow : ?loc:location -> t -> t -> t

Integer power.

Sourceval real_pow : ?loc:location -> t -> t -> t

Real power.

Sourceval lt : ?loc:location -> t -> t -> t

Arithmetic "lesser than" comparison (strict).

Sourceval leq : ?loc:location -> t -> t -> t

Arithmetic "lesser or equal" comparison.

Sourceval gt : ?loc:location -> t -> t -> t

Arithmetic "greater than" comparison (strict).

Sourceval geq : ?loc:location -> t -> t -> t

Arithmetic "greater or equal" comparison.

Triggers

Sourceval in_interval : ?loc:location -> 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).

Sourceval maps_to : ?loc:location -> Id.t -> t -> t

Id mapping (see alt-ergo).

Sourceval trigger : ?loc:location -> t list -> t

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

Sourceval triggers : ?loc:location -> t -> t list -> t

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

Sourceval filters : ?loc:location -> t -> t list -> t

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

Special constructions

Sourceval tracked : ?loc:location -> Id.t -> t -> t

Name a term for tracking purposes.

Sourceval quoted : ?loc:location -> string -> t

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

Sourceval sequent : ?loc:location -> t list -> t list -> t

Sequents as terms

Sourceval check : ?loc:location -> t -> t

Check a term (see alt-ergo).

Sourceval cut : ?loc:location -> t -> t

Create a cut (see alt-ergo).

Sourceval annot : ?loc:location -> 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.

Sourceval sexpr : ?loc:location -> t list -> t

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

Term constructor not in implemented interfaces

Sourceval ite_t : ?loc:location -> unit -> t

The standalone term corresponding to the if-then-else builtin construction.

Term inspection

Sourcemodule S : Set.S with type elt = Id.t

Sets of Ids

Sourceval free_ids : test:(Id.t -> bool) -> S.t -> t -> S.t

Returns the set of identifiers that respect the test:predicate function, and occurs free in the term (i.e. not bound by a binder).

Sourceval fv : t -> Id.t list

Return the list of free variables (i.e currently, Ids that are in the Var namespace).

Additional functions

Sourceval builtin : builtin -> ?loc:location -> unit -> t

Make a builtin.

Sourceval fun_ty : ?loc:location -> t list -> t -> t

Multi-arguments function type constructor.

Sourceval add_attr : t -> t -> t

add_attr attr term rturns a term t equal to term, but with attr added to the list of attributes.

Sourceval add_attrs : t list -> t -> t

Same as add_attr but adds a list of attributes.

Sourceval set_attrs : t list -> t -> t

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 leave all other untouched. In these cases, it is useful to override the identity mapper, redefining only the fields needed.

Sourcetype 'a mapper = {
  1. symbol : 'a mapper -> attr:t list -> loc:location -> Id.t -> 'a;
  2. builtin : 'a mapper -> attr:t list -> loc:location -> builtin -> 'a;
  3. colon : 'a mapper -> attr:t list -> loc:location -> t -> t -> 'a;
  4. app : 'a mapper -> attr:t list -> loc:location -> t -> t list -> 'a;
  5. binder : 'a mapper -> attr:t list -> loc:location -> binder -> t list -> t -> 'a;
  6. pmatch : 'a mapper -> attr:t list -> loc:location -> t -> (t * t) list -> 'a;
}

The type of a mapper on terms.

Sourceval id_mapper : t mapper

The identity mapper: maps any term to itself.

Sourceval unit_mapper : unit mapper

The unit mapper, i.e. an iterator.

Sourceval map : 'a mapper -> t -> 'a

Apply a mapper to a term.