Module Lang.F

module F: sig .. end

module QED: Logic.Term  with module ADT = ADT
                           and module Field = Field
                           and module Fun = Fun

Types and Variables

type var = QED.var

type tau = QED.tau

type pool = 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

Expressions

type term = QED.term

type record = (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

type unop = term -> term

type binop = 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 -> 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 -> Lang.Field.t -> term

val e_record : record -> term

val e_fun : ?result:tau -> 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

Predicates

type pred

type cmp = term -> term -> pred

type operator = 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 e_lift : (term -> term) -> pred -> pred

val p_lift : (pred -> pred) -> term -> term

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 : 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 Context.value

Context used by pp_term, pp_pred, pp_var, ppvars for printing the term. Allows to keep the same disambiguation.

type marks = 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

Binders

val lc_closed : term -> bool

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

Utilities

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 : Lang.Fun.t -> term -> bool

val is_absorbant : 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:(Lang.Field.t -> tau) ->
       ?record:(Lang.Field.t -> tau) ->
       ?call:(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.

Raises Not_found if no type is found.

field : type of a field value

record : type of the record containing a field

call : type of the values returned by the function

Builtins

The 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 : Lang.lfun -> (term list -> term) -> unit

val set_builtin_get : Lang.lfun ->
       (term list -> tau option -> term -> term) -> unit

val set_builtin_1 : Lang.lfun -> unop -> unit

val set_builtin_2 : Lang.lfun -> binop -> unit

val set_builtin_2' : Lang.lfun ->
       (term -> term -> tau option -> term) -> unit

val set_builtin_eq : Lang.lfun -> binop -> unit

val set_builtin_leq : Lang.lfun -> binop -> unit

val set_builtin_eqp : Lang.lfun -> cmp -> unit

val release : unit -> unit

Empty local caches