module F:sig
..end
module QED:Logic.Term
with module ADT = ADT and module Field = Field and module Fun = Fun
typevar =
QED.var
typetau =
QED.tau
typepool =
QED.pool
module Tau: QED.Tau
module Var: QED.Var
module Vars:Qed.Idxset.S
with type elt = var
module Vmap:Qed.Idxmap.S
with type key = var
val pool : ?copy:pool -> unit -> pool
val fresh : pool -> ?basename:string -> tau -> var
val alpha : pool -> var -> var
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
val tau_of_var : var -> tau
typeterm =
QED.term
typerecord =
(Wp.Lang.field * term) list
val hash : term -> int
Constant time
val equal : term -> term -> bool
Same as ==
val compare : term -> term -> int
module Tset:Qed.Idxset.S
with type elt = term
module Tmap:Qed.Idxmap.S
with type key = term
typeunop =
term -> term
typebinop =
term -> term -> term
val e_zero : term
val e_one : term
val e_minus_one : term
val e_minus_one_real : term
val e_one_real : term
val e_zero_real : term
val constant : term -> term
val e_fact : int -> term -> term
val e_int64 : int64 -> term
val e_bigint : Integer.t -> term
val e_float : float -> term
val e_setfield : term -> Wp.Lang.field -> term -> term
val e_range : term -> term -> term
e_range a b = b+1-a
val is_zero : term -> bool
val e_true : term
val e_false : term
val e_bool : bool -> term
val e_literal : bool -> term -> term
val e_int : int -> term
val e_zint : Z.t -> term
val e_real : Q.t -> term
val e_var : var -> term
val e_opp : term -> term
val e_times : Z.t -> term -> term
val e_sum : term list -> term
val e_prod : term list -> term
val e_add : term -> term -> term
val e_sub : term -> term -> term
val e_mul : term -> term -> term
val e_div : term -> term -> term
val e_mod : term -> term -> term
val e_eq : term -> term -> term
val e_neq : term -> term -> term
val e_leq : term -> term -> term
val e_lt : term -> term -> term
val e_imply : term list -> term -> term
val e_equiv : term -> term -> term
val e_and : term list -> term
val e_or : term list -> term
val e_not : term -> term
val e_if : term -> term -> term -> term
val e_const : tau -> term -> term
val e_get : term -> term -> term
val e_set : term -> term -> term -> term
val e_getfield : term -> Wp.Lang.Field.t -> term
val e_record : record -> term
val e_fun : ?result:tau ->
Wp.Lang.Fun.t -> term list -> term
val e_bind : Qed.Logic.binder -> var -> term -> term
val 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.
val e_close : (Qed.Logic.binder * var) list -> term -> term
Closes all specified binders
type
pred
typecmp =
term -> term -> pred
typeoperator =
pred -> pred -> pred
module Pmap:Qed.Idxmap.S
with type key = pred
module Pset:Qed.Idxset.S
with type elt = pred
val p_true : pred
val p_false : pred
val p_equal : term -> term -> pred
val p_equals : (term * term) list -> pred list
val p_neq : term -> term -> pred
val p_leq : term -> term -> pred
val p_lt : term -> term -> pred
val p_positive : term -> pred
val is_ptrue : pred -> Qed.Logic.maybe
val is_pfalse : pred -> Qed.Logic.maybe
val is_equal : term -> term -> Qed.Logic.maybe
val eqp : pred -> pred -> bool
val comparep : pred -> pred -> int
val p_bool : term -> pred
val e_prop : pred -> term
val p_bools : term list -> pred list
val e_props : pred list -> term list
val lift : (term -> term) -> pred -> pred
val p_not : pred -> pred
val p_and : pred -> pred -> pred
val p_or : pred -> pred -> pred
val p_imply : pred -> pred -> pred
val p_equiv : pred -> pred -> pred
val p_hyps : pred list -> pred -> pred
val p_if : pred -> pred -> pred -> pred
val p_conj : pred list -> pred
val p_disj : pred list -> pred
val p_any : ('a -> pred) -> 'a list -> pred
val p_all : ('a -> pred) -> 'a list -> pred
val p_call : Wp.Lang.lfun -> term list -> pred
val p_forall : var list -> pred -> pred
val p_exists : var list -> pred -> pred
val p_bind : Qed.Logic.binder -> var -> pred -> pred
type
sigma
module Subst:sig
..end
val e_subst : sigma -> term -> term
val p_subst : sigma -> pred -> pred
val p_subst_var : var -> term -> pred -> pred
val e_vars : term -> var list
Sorted
val p_vars : pred -> var list
Sorted
val p_close : pred -> pred
Quantify over (sorted) free variables
val pp_tau : Stdlib.Format.formatter -> tau -> unit
val pp_var : Stdlib.Format.formatter -> var -> unit
val pp_vars : Stdlib.Format.formatter -> Vars.t -> unit
val pp_term : Stdlib.Format.formatter -> term -> unit
val pp_pred : Stdlib.Format.formatter -> pred -> unit
val debugp : Stdlib.Format.formatter -> pred -> unit
type
env
val context_pp : env Wp.Context.value
Context used by pp_term, pp_pred, pp_var, ppvars for printing the term. Allows to keep the same disambiguation.
typemarks =
QED.marks
val env : Vars.t -> env
val marker : env -> marks
val mark_e : marks -> term -> unit
val mark_p : marks -> pred -> unit
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.
val defs : marks -> term list
val define : (env -> string -> term -> unit) ->
env -> marks -> env
val pp_eterm : env -> Stdlib.Format.formatter -> term -> unit
val pp_epred : env -> Stdlib.Format.formatter -> pred -> unit
val p_expr : pred -> pred QED.expression
val e_expr : pred -> term QED.expression
val lc_closed : term -> bool
val lc_iter : (term -> unit) -> term -> unit
val decide : term -> bool
Return true
if and only the term is e_true
. Constant time.
val basename : term -> string
val is_true : term -> Qed.Logic.maybe
Constant time.
val is_false : term -> Qed.Logic.maybe
Constant time.
val is_prop : term -> bool
Boolean or Property
val is_int : term -> bool
Integer sort
val is_real : term -> bool
Real sort
val is_arith : term -> bool
Integer or Real sort
val is_closed : term -> bool
No bound variables
val is_simple : term -> bool
Constants, variables, functions of arity 0
val is_atomic : term -> bool
Constants and variables
val is_primitive : term -> bool
Constants only
val is_neutral : Wp.Lang.Fun.t -> term -> bool
val is_absorbant : Wp.Lang.Fun.t -> term -> bool
val record_with : record -> (term * record) option
val are_equal : term -> term -> Qed.Logic.maybe
Computes equality
val eval_eq : term -> term -> bool
Same as are_equal
is Yes
val eval_neq : term -> term -> bool
Same as are_equal
is No
val eval_lt : term -> term -> bool
Same as e_lt
is e_true
val eval_leq : term -> term -> bool
Same as e_leq
is e_true
val repr : term -> QED.repr
Constant time
val sort : term -> Qed.Logic.sort
Constant time
val vars : term -> Vars.t
Constant time
val varsp : pred -> Vars.t
Constant time
val occurs : var -> term -> bool
val occursp : var -> pred -> bool
val intersect : term -> term -> bool
val intersectp : pred -> pred -> bool
val is_subterm : term -> term -> bool
val typeof : ?field:(Wp.Lang.Field.t -> tau) ->
?record:(Wp.Lang.Field.t -> tau) ->
?call:(Wp.Lang.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.
Not_found
if no type is found.field
: type of a field valuerecord
: type of the record containing a fieldcall
: type of the values returned by the functionThe functions below register simplifiers 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.
val set_builtin : Wp.Lang.lfun -> (term list -> term) -> unit
val set_builtin_get : Wp.Lang.lfun ->
(term list ->
tau option -> term -> term) ->
unit
val set_builtin_1 : Wp.Lang.lfun -> unop -> unit
val set_builtin_2 : Wp.Lang.lfun -> binop -> unit
val set_builtin_2' : Wp.Lang.lfun ->
(term -> term -> tau option -> term) ->
unit
val set_builtin_eq : Wp.Lang.lfun -> binop -> unit
val set_builtin_leq : Wp.Lang.lfun -> binop -> unit
val set_builtin_eqp : Wp.Lang.lfun -> cmp -> unit
val release : unit -> unit
Empty local caches