sig
module ZInteger :
sig
type t = Integer.t
val equal : t -> t -> bool
val compare : t -> t -> int
val le : t -> t -> bool
val ge : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val native_div : t -> t -> t
val rem : t -> t -> t
val pos_div : t -> t -> t
val divexact : t -> t -> t
val c_div : t -> t -> t
val c_rem : t -> t -> t
val div_rem : t -> t -> t * t
val cast : size:t -> signed:bool -> value:t -> t
val abs : t -> t
val one : t
val two : t
val four : t
val onethousand : t
val minus_one : t
val is_zero : t -> bool
val is_one : t -> bool
val pgcd : t -> t -> t
val ppcm : t -> t -> t
val min : t -> t -> t
val max : t -> t -> t
val length : t -> t -> t
val of_int : int -> t
val of_int64 : Int64.t -> t
val of_int32 : Int32.t -> t
val to_int64 : t -> int64
val to_int : t -> int
val to_float : t -> float
val neg : t -> t
val succ : t -> t
val pred : t -> t
val round_up_to_r : min:t -> r:t -> modu:t -> t
val round_down_to_r : max:t -> r:t -> modu:t -> t
val pos_rem : t -> t -> t
val shift_left : t -> t -> t
val shift_right : t -> t -> t
val logand : t -> t -> t
val logor : t -> t -> t
val logxor : t -> t -> t
val lognot : t -> t
val two_power : t -> t
val two_power_of_int : int -> t
val extract_bits : start:t -> stop:t -> t -> t
val small_nums : t array
val zero : t
val eight : t
val sixteen : t
val thirtytwo : t
val div : t -> t -> t
val billion_one : t
val hash : t -> int
val shift_right_logical : t -> t -> t
val two_power_64 : t
val max_int64 : t
val min_int64 : t
val of_string : string -> t
val to_string : t -> string
val add_2_64 : t -> t
val add_2_32 : t -> t
val is_even : t -> bool
val round_down_to_zero : t -> t -> t
val power_int_positive_int : int -> int -> t
val to_num : t -> Num.num
val popcount : t -> int
val pretty : ?hexa:bool -> t Pretty_utils.formatter
val leq : Integer.t -> Integer.t -> bool
end
module T :
sig
module Z :
sig
type t = ZInteger.t
val zero : t
val one : t
val minus_one : t
val succ : t -> t
val pred : t -> t
val neg : t -> t
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val equal : t -> t -> bool
val leq : t -> t -> bool
val lt : t -> t -> bool
val of_int : int -> t
val of_string : string -> t
val to_string : t -> string
val hash : t -> int
val compare : t -> t -> int
end
module ADT :
sig
type t = ADT.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val basename : t -> string
end
module Field :
sig
type t = Field.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val sort : t -> Qed.Logic.sort
end
module Fun :
sig
type t = Fun.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val category : t -> t Qed.Logic.category
val params : t -> Qed.Logic.sort list
val sort : t -> Qed.Logic.sort
end
module Var :
sig
type t = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Var.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val sort : t -> Qed.Logic.sort
val basename : t -> string
val dummy : t
end
type term = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).term
type bind = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).bind
type var = Var.t
type tau = (Field.t, ADT.t) Qed.Logic.datatype
type signature = (Field.t, ADT.t) Qed.Logic.funtype
module Tau :
sig
type t = tau
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val basename : t -> string
end
module Vars :
sig
type elt = var
type t = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Vars.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module Vmap :
sig
type key = var
type 'a t = 'a Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Vmap.t
val is_empty : 'a t -> bool
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val remove : key -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) ->
key -> 'b -> 'a t -> 'a t
end
type pool = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).pool
val pool : ?copy:pool -> unit -> pool
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
val add_term : pool -> term -> unit
val fresh : pool -> ?basename:string -> tau -> var
val alpha : pool -> var -> var
val tau_of_var : var -> tau
val sort_of_var : var -> Qed.Logic.sort
val base_of_var : var -> string
type 'a expression =
(Z.t, Field.t, ADT.t, Fun.t, var, bind, 'a) Qed.Logic.term_repr
type repr = term expression
type path = int list
type record = (Field.t * term) list
val decide : term -> bool
val is_true : term -> Qed.Logic.maybe
val is_false : term -> Qed.Logic.maybe
val is_prop : term -> bool
val is_int : term -> bool
val is_real : term -> bool
val is_arith : term -> bool
val are_equal : term -> term -> Qed.Logic.maybe
val eval_eq : term -> term -> bool
val eval_neq : term -> term -> bool
val eval_lt : term -> term -> bool
val eval_leq : term -> term -> bool
val repr : term -> repr
val sort : term -> Qed.Logic.sort
val vars : term -> Vars.t
val subterm : term -> path -> term
val change_subterm : term -> path -> term -> term
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 : Qed.R.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_get : term -> term -> term
val e_set : term -> term -> term -> term
val e_getfield : term -> Field.t -> term
val e_record : record -> term
val e_fun : Fun.t -> term list -> term
val e_repr : repr -> term
val e_forall : var list -> term -> term
val e_exists : var list -> term -> term
val e_lambda : var list -> term -> term
val e_bind : Qed.Logic.binder -> var -> term -> term
val e_apply : term -> term list -> term
type sigma = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).sigma
val sigma : unit -> sigma
val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
val lc_bind : var -> term -> bind
val lc_open : var -> bind -> term
val lc_closed : term -> bool
val lc_closed_at : int -> term -> bool
val lc_vars : term -> Qed.Bvars.t
val lc_repr : bind -> term
val e_map : pool -> (term -> term) -> term -> term
val e_iter : pool -> (term -> unit) -> term -> unit
val f_map : (int -> term -> term) -> int -> term -> term
val f_iter : (int -> term -> unit) -> int -> term -> unit
val lc_map : (term -> term) -> term -> term
val lc_iter : (term -> unit) -> term -> unit
val set_builtin : Fun.t -> (term list -> term) -> unit
val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
val literal : term -> bool * term
val congruence_eq : term -> term -> (term * term) list option
val congruence_neq : term -> term -> (term * term) list option
val flattenable : term -> bool
val flattens : term -> term -> bool
val flatten : term -> term list
val affine : term -> (Z.t, term) Qed.Logic.affine
val record_with : record -> (term * record) option
type t = term
val id : t -> int
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val weigth : t -> int
val is_closed : t -> bool
val is_simple : t -> bool
val is_atomic : t -> bool
val is_primitive : t -> bool
val is_neutral : Fun.t -> t -> bool
val is_absorbant : Fun.t -> t -> bool
val size : t -> int
val basename : t -> string
val pp_id : Format.formatter -> t -> unit
val pp_rid : Format.formatter -> t -> unit
val pp_repr : Format.formatter -> repr -> unit
module Term :
sig
type t = term
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
end
module Tset :
sig
type elt = term
type t = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Tset.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module Tmap :
sig
type key = term
type 'a t = 'a Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Tmap.t
val is_empty : 'a t -> bool
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val remove : key -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) ->
key -> 'b -> 'a t -> 'a t
end
val shared :
?shared:(term -> bool) ->
?shareable:(term -> bool) -> term list -> term list
type marks = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).marks
val marks :
?shared:(term -> bool) -> ?shareable:(term -> bool) -> unit -> marks
val mark : marks -> term -> unit
val defs : marks -> term list
val debug : Format.formatter -> term -> unit
type state = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).state
val create : unit -> state
val get_state : unit -> state
val set_state : state -> unit
val clr_state : state -> unit
val constant : term -> term
val check : repr -> term -> term
val check_unit : qed:term -> raw:term -> term
val iter_checks : (qed:term -> raw:term -> unit) -> unit
val release : unit -> unit
end
module TT = T
module DATA :
sig
type t = T.state
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module STATE :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype :
sig
type t = DATA.t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
end
module Pretty :
sig
type env = Qed.Pretty.Make(T).env
val empty : env
val marks : env -> T.marks
val known : env -> T.Vars.t -> env
val fresh : env -> T.term -> string * env
val bind : string -> T.term -> env -> env
val pp_tau : Format.formatter -> T.tau -> unit
val pp_term : env -> Format.formatter -> T.term -> unit
val pp_def : env -> Format.formatter -> T.term -> unit
end
module Z :
sig
type t = ZInteger.t
val zero : t
val one : t
val minus_one : t
val succ : t -> t
val pred : t -> t
val neg : t -> t
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val equal : t -> t -> bool
val leq : t -> t -> bool
val lt : t -> t -> bool
val of_int : int -> t
val of_string : string -> t
val to_string : t -> string
val hash : t -> int
val compare : t -> t -> int
end
module ADT :
sig
type t = ADT.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val basename : t -> string
end
module Field :
sig
type t = Field.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val sort : t -> Qed.Logic.sort
end
module Fun :
sig
type t = Fun.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val category : t -> t Qed.Logic.category
val params : t -> Qed.Logic.sort list
val sort : t -> Qed.Logic.sort
end
module Var :
sig
type t = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Var.t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val sort : t -> Qed.Logic.sort
val basename : t -> string
val dummy : t
end
type term = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).term
type bind = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).bind
type var = Var.t
type tau = (Field.t, ADT.t) Qed.Logic.datatype
type signature = (Field.t, ADT.t) Qed.Logic.funtype
module Tau :
sig
type t = tau
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
val basename : t -> string
end
module Vars :
sig
type elt = var
type t = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Vars.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module Vmap :
sig
type key = var
type 'a t = 'a Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Vmap.t
val is_empty : 'a t -> bool
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val remove : key -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) -> key -> 'b -> 'a t -> 'a t
end
type pool = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).pool
val pool : ?copy:pool -> unit -> pool
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
val add_term : pool -> term -> unit
val fresh : pool -> ?basename:string -> tau -> var
val alpha : pool -> var -> var
val tau_of_var : var -> tau
val sort_of_var : var -> Qed.Logic.sort
val base_of_var : var -> string
type 'a expression =
(Z.t, Field.t, ADT.t, Fun.t, var, bind, 'a) Qed.Logic.term_repr
type repr = term expression
type path = int list
type record = (Field.t * term) list
val decide : term -> bool
val is_true : term -> Qed.Logic.maybe
val is_false : term -> Qed.Logic.maybe
val is_prop : term -> bool
val is_int : term -> bool
val is_real : term -> bool
val is_arith : term -> bool
val are_equal : term -> term -> Qed.Logic.maybe
val eval_eq : term -> term -> bool
val eval_neq : term -> term -> bool
val eval_lt : term -> term -> bool
val eval_leq : term -> term -> bool
val repr : term -> repr
val sort : term -> Qed.Logic.sort
val vars : term -> Vars.t
val subterm : term -> path -> term
val change_subterm : term -> path -> term -> term
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 : Qed.R.t -> term
val e_var : var -> term
val e_prod : term list -> 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_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_get : term -> term -> term
val e_set : term -> term -> term -> term
val e_getfield : term -> Field.t -> term
val e_record : record -> term
val e_repr : repr -> term
val e_forall : var list -> term -> term
val e_exists : var list -> term -> term
val e_lambda : var list -> term -> term
val e_bind : Qed.Logic.binder -> var -> term -> term
val e_apply : term -> term list -> term
type sigma = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).sigma
val sigma : unit -> sigma
val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
val lc_bind : var -> term -> bind
val lc_open : var -> bind -> term
val lc_closed : term -> bool
val lc_closed_at : int -> term -> bool
val lc_vars : term -> Qed.Bvars.t
val lc_repr : bind -> term
val e_map : pool -> (term -> term) -> term -> term
val e_iter : pool -> (term -> unit) -> term -> unit
val f_map : (int -> term -> term) -> int -> term -> term
val f_iter : (int -> term -> unit) -> int -> term -> unit
val lc_map : (term -> term) -> term -> term
val lc_iter : (term -> unit) -> term -> unit
val set_builtin : Fun.t -> (term list -> term) -> unit
val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
val literal : term -> bool * term
val congruence_eq : term -> term -> (term * term) list option
val congruence_neq : term -> term -> (term * term) list option
val flattenable : term -> bool
val flattens : term -> term -> bool
val flatten : term -> term list
val affine : term -> (Z.t, term) Qed.Logic.affine
val record_with : record -> (term * record) option
type t = term
val id : t -> int
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val weigth : t -> int
val is_closed : t -> bool
val is_simple : t -> bool
val is_atomic : t -> bool
val is_primitive : t -> bool
val is_neutral : Fun.t -> t -> bool
val is_absorbant : Fun.t -> t -> bool
val size : t -> int
val basename : t -> string
val pp_id : Format.formatter -> t -> unit
val pp_rid : Format.formatter -> t -> unit
val pp_repr : Format.formatter -> repr -> unit
module Term :
sig
type t = term
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val debug : t -> string
end
module Tset :
sig
type elt = term
type t = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Tset.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module Tmap :
sig
type key = term
type 'a t = 'a Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).Tmap.t
val is_empty : 'a t -> bool
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val remove : key -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) -> key -> 'b -> 'a t -> 'a t
end
val shared :
?shared:(term -> bool) ->
?shareable:(term -> bool) -> term list -> term list
type marks = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).marks
val marks :
?shared:(term -> bool) -> ?shareable:(term -> bool) -> unit -> marks
val mark : marks -> term -> unit
val defs : marks -> term list
val debug : Format.formatter -> term -> unit
type state = Qed.Term.Make(ZInteger)(ADT)(Field)(Fun).state
val create : unit -> state
val get_state : unit -> state
val set_state : state -> unit
val clr_state : state -> unit
val constant : term -> term
val check : repr -> term -> term
val check_unit : qed:term -> raw:term -> term
val release : unit -> unit
val do_checks : bool Pervasives.ref
val iter_checks :
(qed:Lang.F.T.term -> raw:Lang.F.T.term -> goal:Lang.F.T.term -> unit) ->
unit
val e_add : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val e_sum : Lang.F.T.term list -> Lang.F.T.term
val e_times : Lang.F.T.Z.t -> Lang.F.T.term -> Lang.F.T.term
val e_opp : Lang.F.T.term -> Lang.F.T.term
val e_leq : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val e_lt : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val e_eq : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val e_neq : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val e_fun : Lang.F.T.Fun.t -> Lang.F.T.term list -> Lang.F.T.term
type unop = term -> term
type binop = term -> term -> term
val e_zero : Lang.F.T.term
val e_one : Lang.F.T.term
val e_minus_one : Lang.F.T.term
val e_one_real : Lang.F.T.term
val e_zero_real : Lang.F.T.term
val hex_of_float : float -> string
val e_int64 : int64 -> term
val e_fact : int -> Lang.F.T.term -> Lang.F.T.term
val e_bigint : Integer.t -> term
val e_range : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val e_mthfloat : float -> Lang.F.T.term
val e_hexfloat : float -> Lang.F.T.term
val e_setfield : term -> Lang.Field.t -> term -> term
type pred = term
type cmp = term -> term -> Lang.F.pred
val p_bool : 'a -> 'a
val e_prop : 'a -> 'a
val p_bools : 'a -> 'a
val e_props : 'a -> 'a
val lift : ('a -> 'b) -> 'a -> 'b
val is_zero : Lang.F.T.term -> bool
val eqp : t -> t -> bool
val comparep : t -> t -> int
val is_ptrue : term -> Qed.Logic.maybe
val is_pfalse : term -> Qed.Logic.maybe
val is_equal : Lang.F.T.term -> Lang.F.T.term -> Qed.Logic.maybe
val p_equal : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val p_neq : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val p_leq : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val p_lt : Lang.F.T.term -> Lang.F.T.term -> Lang.F.T.term
val p_positive : Lang.F.T.term -> Lang.F.T.term
val p_true : term
val p_false : term
val p_not : term -> term
val p_bind : Qed.Logic.binder -> var -> term -> term
val p_forall : var list -> term -> term
val p_exists : var list -> term -> term
val p_subst : ?sigma:sigma -> (term -> term) -> term -> term
val p_and : term -> term -> term
val p_or : term -> term -> term
val p_imply : term -> term -> term
val p_hyps : term list -> term -> term
val p_equiv : term -> term -> term
val p_if : term -> term -> term -> term
val p_conj : term list -> term
val p_disj : term list -> term
val p_all : ('a -> term) -> 'a list -> term
val p_any : ('a -> term) -> 'a list -> term
val p_call : Lang.F.T.Fun.t -> Lang.F.T.term list -> Lang.F.T.term
val p_close : term -> term
val occurs : Vars.elt -> term -> bool
val intersect : term -> term -> bool
val occursp : Vars.elt -> term -> bool
val intersectp : term -> term -> bool
val varsp : term -> Vars.t
val pred : term -> repr
val idp : t -> int
val pp_term : Format.formatter -> Lang.F.T.term -> unit
val pp_pred : Format.formatter -> Lang.F.T.term -> unit
val pp_var : Format.formatter -> var -> unit
val pp_vars : Format.formatter -> Vars.t -> unit
val debugp : Format.formatter -> Lang.F.T.term -> unit
type env = Lang.F.Pretty.env
val env : Lang.F.T.Vars.t -> Lang.F.Pretty.env
val marker : Lang.F.Pretty.env -> Lang.F.T.marks
val mark_vars : Lang.F.Pretty.env -> Lang.F.T.Vars.t -> Lang.F.Pretty.env
val mark_e : Lang.F.T.marks -> Lang.F.T.term -> unit
val mark_p : Lang.F.T.marks -> Lang.F.T.term -> unit
val define :
(Lang.F.Pretty.env -> string -> Lang.F.T.term -> 'a) ->
Lang.F.Pretty.env -> Lang.F.T.marks -> Lang.F.Pretty.env
val pp_eterm :
Lang.F.Pretty.env -> Format.formatter -> Lang.F.T.term -> unit
val pp_epred :
Lang.F.Pretty.env -> Format.formatter -> Lang.F.T.term -> unit
module Pmap = Tmap
module Pset = Tset
val set_builtin_1 : Lang.Fun.t -> (term -> term) -> unit
val set_builtin_2 : Lang.Fun.t -> (term -> term -> term) -> unit
val set_builtin_eqp : Lang.Fun.t -> (term -> term -> term) -> unit
end