Module F.QEDSource

Sourcemodule ADT = ADT
Sourcemodule Field = Field
Sourcemodule Fun = Fun
Sourcetype term
Sourcetype lc_term

Loosely closed terms.

Sourcemodule Term : Qed.Logic.Symbol with type t = term
Sourcemodule Tset : Qed.Idxset.S with type elt = term

Non-structural, machine dependent, but fast comparison and efficient merges

Sourcemodule Tmap : Qed.Idxmap.S with type key = term

Non-structural, machine dependent, but fast comparison and efficient merges

Sourcemodule STset : Set.S with type elt = term

Structuraly ordered, but less efficient access and non-linear merges

Sourcemodule STmap : Map.S with type key = term

Structuraly ordered, but less efficient access and non-linear merges

Variables

Sourcetype var = Var.t
Sourcemodule Tau : Qed.Logic.Data with type t = tau
Sourcemodule Vars : Qed.Idxset.S with type elt = var
Sourcemodule Vmap : Qed.Idxmap.S with type key = var
Sourcetype pool
Sourceval pool : ?copy:pool -> unit -> pool
Sourceval add_var : pool -> var -> unit
Sourceval add_vars : pool -> Vars.t -> unit
Sourceval add_term : pool -> term -> unit
Sourceval fresh : pool -> ?basename:string -> tau -> var
Sourceval alpha : pool -> var -> var
Sourceval tau_of_var : var -> tau
Sourceval sort_of_var : var -> Qed.Logic.sort
Sourceval base_of_var : var -> string

Terms

Sourcetype 'a expression = (Field.t, ADT.t, Fun.t, var, lc_term, 'a) Qed.Logic.term_repr
Sourcetype record = (Field.t * term) list
Sourceval decide : term -> bool

Return true if and only the term is e_true. Constant time.

Sourceval is_true : term -> Qed.Logic.maybe

Constant time.

Sourceval is_false : term -> Qed.Logic.maybe

Constant time.

Sourceval is_prop : term -> bool

Boolean or Property

Sourceval is_int : term -> bool

Integer sort

Sourceval is_real : term -> bool

Real sort

Sourceval is_arith : term -> bool

Integer or Real sort

Sourceval are_equal : term -> term -> Qed.Logic.maybe

Computes equality

Sourceval eval_eq : term -> term -> bool

Same as are_equal is Yes

Sourceval eval_neq : term -> term -> bool

Same as are_equal is No

Sourceval eval_lt : term -> term -> bool

Same as e_lt is e_true

Sourceval eval_leq : term -> term -> bool

Same as e_leq is e_true

Sourceval repr : term -> repr

Constant time

Constant time

Sourceval vars : term -> Vars.t

Constant time

Path-positioning access

This part of the API is DEPRECATED

Sourcetype path = int list

position of a subterm in a term.

Basic constructors

Sourceval e_true : term
Sourceval e_false : term
Sourceval e_bool : bool -> term
Sourceval e_literal : bool -> term -> term
Sourceval e_int : int -> term
Sourceval e_float : float -> term
Sourceval e_zint : Z.t -> term
Sourceval e_real : Q.t -> term
Sourceval e_var : var -> term
Sourceval e_opp : term -> term
Sourceval e_times : Z.t -> term -> term
Sourceval e_sum : term list -> term
Sourceval e_prod : term list -> term
Sourceval e_add : term -> term -> term
Sourceval e_sub : term -> term -> term
Sourceval e_mul : term -> term -> term
Sourceval e_div : term -> term -> term
Sourceval e_mod : term -> term -> term
Sourceval e_eq : term -> term -> term
Sourceval e_neq : term -> term -> term
Sourceval e_leq : term -> term -> term
Sourceval e_lt : term -> term -> term
Sourceval e_imply : term list -> term -> term
Sourceval e_equiv : term -> term -> term
Sourceval e_and : term list -> term
Sourceval e_or : term list -> term
Sourceval e_not : term -> term
Sourceval e_if : term -> term -> term -> term
Sourceval e_const : tau -> term -> term
Sourceval e_get : term -> term -> term
Sourceval e_set : term -> term -> term -> term
Sourceval e_getfield : term -> Field.t -> term
Sourceval e_record : record -> term
Sourceval e_fun : ?result:tau -> Fun.t -> term list -> term
Sourceval e_repr : ?result:tau -> repr -> term

Quantifiers and Binding

Sourceval e_forall : var list -> term -> term
Sourceval e_exists : var list -> term -> term
Sourceval e_lambda : var list -> term -> term
Sourceval e_close_forall : term -> term
Sourceval e_close_exists : term -> term
Sourceval e_close_lambda : term -> term
Sourceval e_apply : term -> term list -> term
Sourceval e_bind : Qed.Logic.binder -> var -> term -> term

Bind the given variable if it appears free in the term, or return the term unchanged.

Sourceval e_unbind : var -> lc_term -> term

Opens the top-most bound variable with a (fresh) variable. Can be only applied on top-most lc-term from `Bind(_,_,_)`, thanks to typing.

Sourceval e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> term -> (Qed.Logic.binder * var) list * term

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default). The pool must contain all free variables of the term.

Sourceval e_close : (Qed.Logic.binder * var) list -> term -> term

Closes all specified binders

Generalized Substitutions

Sourcetype sigma
Sourceval sigma : ?pool:pool -> unit -> sigma
Sourcemodule Subst : sig ... end
Sourceval e_subst : sigma -> term -> term

The environment sigma must be prepared with the desired substitution. Its pool of fresh variables must covers the entire domain and co-domain of the substitution, and the transformed values.

Sourceval e_subst_var : var -> term -> term -> term

Locally Nameless Representation

These functions can be unsafe because they might expose terms that contains non-bound b-vars. Never use such terms to build substitutions (sigma).

Sourceval lc_vars : term -> Qed.Bvars.t
Sourceval lc_closed : term -> bool

All bound variables are under their binder

Sourceval lc_repr : lc_term -> term

Calling this function is unsafe unless the term is lc_closed

Sourceval lc_iter : (term -> unit) -> term -> unit

Similar to f_iter but exposes non-closed sub-terms of `Bind` as regular term values instead of lc_term ones.

Iteration Scheme

Sourceval f_map : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> (term -> term) -> term -> term

Pass and open binders, maps its direct sub-terms and then close then opened binders Raises Invalid_argument in case of a bind-term without pool. The optional pool must contain all free variables of the term.

Sourceval f_iter : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> (term -> unit) -> term -> unit

Iterates over its direct sub-terms (pass and open binders) Raises Invalid_argument in case of a bind-term without pool. The optional pool must contain all free variables of the term.

Partial Typing

Sourceval typeof : ?field:(Field.t -> tau) -> ?record:(Field.t -> tau) -> ?call:(Fun.t -> tau option list -> tau) -> term -> tau

Try to extract a type of term. Parameterized by optional extractors for field and functions. Extractors may raise Not_found ; however, they are only used when the provided kinds for fields and functions are not precise enough.

  • parameter field

    type of a field value

  • parameter record

    type of the record containing a field

  • parameter call

    type of the values returned by the function

Support for Builtins

Sourceval set_builtin : ?force:bool -> Fun.t -> (term list -> term) -> unit

Register a simplifier for function f. The computation code may raise Not_found, in which case the symbol is not interpreted.

If f is an operator with algebraic rules (see type operator), the children are normalized before builtin call.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

Sourceval set_builtin' : ?force:bool -> Fun.t -> (term list -> tau option -> term) -> unit
Sourceval set_builtin_map : ?force:bool -> Fun.t -> (term list -> term list) -> unit

Register a builtin for rewriting f a1..an into f b1..bm.

This is short cut for set_builtin, where the head application of f avoids to run into an infinite loop.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

Sourceval set_builtin_get : ?force:bool -> Fun.t -> (term list -> term list -> term) -> unit

set_builtin_get f rewrite register a builtin for rewriting (f a1..an)[k1]..[km] into rewrite (a1..an) (k1..km).

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

  • before 28.0-Nickel

    one-dimensional access only

Sourceval set_builtin_field : ?force:bool -> Fun.t -> Field.t -> (term list -> term) -> unit

Register a builtin for simplifying (f eā€¦).fd expressions. Must only use recursive comparison for strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • since 28.0-Nickel
Sourceval set_builtin_eq : ?force:bool -> Fun.t -> (term -> term -> term) -> unit

Register a builtin equality for comparing any term with head-symbol. Must only use recursive comparison for strictly smaller terms. The recognized term with head function symbol is passed first.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

Sourceval set_builtin_leq : ?force:bool -> Fun.t -> (term -> term -> term) -> unit

Register a builtin for comparing any term with head-symbol. Must only use recursive comparison for strictly smaller terms. The recognized term with head function symbol can be on both sides. Strict comparison is automatically derived from the non-strict one.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

  • before 22.0-Titanium

    the optional force parameter does not exist

Specific Patterns

Sourceval consequence : term -> term -> term

Knowing h, consequence h a returns b such that h -> (a<->b)

Sourceval literal : term -> bool * term
Sourceval record_with : record -> (term * record) option

Symbol

Sourcetype t = term
Sourceval id : t -> int

unique identifier (stored in t)

Sourceval hash : t -> int

constant access (stored in t)

Sourceval equal : t -> t -> bool

physical equality

Sourceval compare : t -> t -> int

atoms are lower than complex terms ; otherwise, sorted by id.

Sourceval pretty : Format.formatter -> t -> unit
Sourceval weigth : t -> int

Informal size

Utilities

Sourceval is_closed : t -> bool

No bound variables

Sourceval is_simple : t -> bool

Constants, variables, functions of arity 0

Sourceval is_atomic : t -> bool

Constants and variables

Sourceval is_primitive : t -> bool

Constants only

Sourceval is_neutral : Fun.t -> t -> bool
Sourceval is_absorbant : Fun.t -> t -> bool
Sourceval size : t -> int
Sourceval basename : t -> string
Sourceval debug : Format.formatter -> t -> unit
Sourceval pp_id : Format.formatter -> t -> unit

internal id

Sourceval pp_rid : Format.formatter -> t -> unit

head symbol with children id's

Sourceval pp_repr : Format.formatter -> repr -> unit

head symbol with children id's

Shared sub-terms

Sourceval is_subterm : term -> term -> bool

Occurrence check. is_subterm a b returns true iff a is a subterm of b. Optimized wrt shared subterms, term size, and term variables.

Sourceval shared : ?shared:(term -> bool) -> ?shareable:(term -> bool) -> ?subterms:((term -> unit) -> term -> unit) -> term list -> term list

Computes the sub-terms that appear several times. shared marked linked e returns the shared subterms of e.

The list of shared subterms is consistent with order of definition: each trailing terms only depend on heading ones.

The traversal is controlled by two optional arguments:

  • shared those terms are not traversed (considered as atomic, default to none)
  • shareable those terms (is_simple excepted) that can be shared (default to all)
  • subterms those sub-terms a term to be considered during traversal (lc_iter by default)

Low-level shared primitives: shared is actually a combination of building marks, marking terms, and extracting definitions:

 let share ?... e =
     let m = marks ?... () in
     List.iter (mark m) es ;
     defs m
Sourcetype marks

Create a marking accumulator. Same defaults than shared.

Sourceval marks : ?shared:(term -> bool) -> ?shareable:(term -> bool) -> ?subterms:((term -> unit) -> term -> unit) -> unit -> marks
Sourceval mark : marks -> term -> unit

Mark a term to be printed

Sourceval share : marks -> term -> unit

Mark a term to be explicitly shared

Sourceval defs : marks -> term list

Returns a list of terms to be shared among all shared or marked subterms. The order of terms is consistent with definition order: head terms might be used in tail ones.