sig
type library = string
type 'a infoprover = { altergo : 'a; why3 : 'a; coq : 'a; }
val infoprover : 'a -> 'a Wp.Lang.infoprover
val comp_id : Cil_types.compinfo -> string
val field_id : Cil_types.fieldinfo -> string
val type_id : Cil_types.logic_type_info -> string
val logic_id : Cil_types.logic_info -> string
val lemma_id : string -> string
type adt = private
Mtype of Wp.Lang.mdt
| Mrecord of Wp.Lang.mdt * Wp.Lang.fields
| Atype of Cil_types.logic_type_info
| Comp of Cil_types.compinfo
and mdt = string Wp.Lang.extern
and 'a extern = {
ext_id : int;
ext_link : 'a Wp.Lang.infoprover;
ext_library : Wp.Lang.library;
ext_debug : string;
}
and fields = { mutable fields : Wp.Lang.field list; }
and field =
Mfield of Wp.Lang.mdt * Wp.Lang.fields * string * Wp.Lang.tau
| Cfield of Cil_types.fieldinfo
and tau = (Wp.Lang.field, Wp.Lang.adt) Qed.Logic.datatype
type lfun =
ACSL of Cil_types.logic_info
| CTOR of Cil_types.logic_ctor_info
| Model of Wp.Lang.model
and model = {
m_category : Wp.Lang.lfun Qed.Logic.category;
m_params : Qed.Logic.sort list;
m_result : Qed.Logic.sort;
m_typeof : Wp.Lang.tau option list -> Wp.Lang.tau;
m_source : Wp.Lang.source;
}
and source = Generated of string | Extern of Qed.Engine.link Wp.Lang.extern
val mem_builtin_type : name:string -> bool
val set_builtin_type :
name:string -> link:string Wp.Lang.infoprover -> library:string -> unit
val get_builtin_type :
name:string ->
link:string Wp.Lang.infoprover -> library:string -> Wp.Lang.adt
val is_builtin : Cil_types.logic_type_info -> bool
val is_builtin_type : name:string -> Wp.Lang.tau -> bool
val datatype : library:string -> string -> Wp.Lang.adt
val record :
link:string Wp.Lang.infoprover ->
library:string -> (string * Wp.Lang.tau) list -> Wp.Lang.adt
val atype : Cil_types.logic_type_info -> Wp.Lang.adt
val comp : Cil_types.compinfo -> Wp.Lang.adt
val field : Wp.Lang.adt -> string -> Wp.Lang.field
val fields_of_adt : Wp.Lang.adt -> Wp.Lang.field list
val fields_of_tau : Wp.Lang.tau -> Wp.Lang.field list
val fields_of_field : Wp.Lang.field -> Wp.Lang.field list
type balance = Nary | Left | Right
val extern_s :
library:Wp.Lang.library ->
?link:Qed.Engine.link Wp.Lang.infoprover ->
?category:Wp.Lang.lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:Wp.Lang.tau ->
?typecheck:(Wp.Lang.tau option list -> Wp.Lang.tau) ->
string -> Wp.Lang.lfun
val extern_f :
library:Wp.Lang.library ->
?link:Qed.Engine.link Wp.Lang.infoprover ->
?balance:Wp.Lang.balance ->
?category:Wp.Lang.lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:Wp.Lang.tau ->
?typecheck:(Wp.Lang.tau option list -> Wp.Lang.tau) ->
('a, Stdlib.Format.formatter, unit, Wp.Lang.lfun) Stdlib.format4 -> 'a
val extern_p :
library:Wp.Lang.library ->
?bool:string ->
?prop:string ->
?link:Qed.Engine.link Wp.Lang.infoprover ->
?params:Qed.Logic.sort list -> unit -> Wp.Lang.lfun
val extern_fp :
library:Wp.Lang.library ->
?params:Qed.Logic.sort list ->
?link:string Wp.Lang.infoprover -> string -> Wp.Lang.lfun
val generated_f :
?category:Wp.Lang.lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:Wp.Lang.tau ->
('a, Stdlib.Format.formatter, unit, Wp.Lang.lfun) Stdlib.format4 -> 'a
val generated_p : string -> Wp.Lang.lfun
val tau_of_comp : Cil_types.compinfo -> Wp.Lang.tau
val tau_of_object : Wp.Ctypes.c_object -> Wp.Lang.tau
val tau_of_ctype : Cil_types.typ -> Wp.Lang.tau
val tau_of_ltype : Cil_types.logic_type -> Wp.Lang.tau
val tau_of_return : Cil_types.logic_info -> Wp.Lang.tau
val tau_of_lfun : Wp.Lang.lfun -> Wp.Lang.tau option list -> Wp.Lang.tau
val tau_of_field : Wp.Lang.field -> Wp.Lang.tau
val tau_of_record : Wp.Lang.field -> Wp.Lang.tau
val t_int : Wp.Lang.tau
val t_real : Wp.Lang.tau
val t_bool : Wp.Lang.tau
val t_prop : Wp.Lang.tau
val t_addr : unit -> Wp.Lang.tau
val t_array : Wp.Lang.tau -> Wp.Lang.tau
val t_farray : Wp.Lang.tau -> Wp.Lang.tau -> Wp.Lang.tau
val t_datatype : Wp.Lang.adt -> Wp.Lang.tau list -> Wp.Lang.tau
val pointer : (Cil_types.typ -> Wp.Lang.tau) Wp.Context.value
val floats : (Wp.Ctypes.c_float -> Wp.Lang.tau) Wp.Context.value
val poly : string list Wp.Context.value
val parameters : (Wp.Lang.lfun -> Qed.Logic.sort list) -> unit
val name_of_lfun : Wp.Lang.lfun -> string
val name_of_field : Wp.Lang.field -> string
module ADT :
sig
type t = adt
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
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 = lfun
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
class virtual idprinting :
object
method datatype : Wp.Lang.ADT.t -> string
method field : Wp.Lang.Field.t -> string
method virtual infoprover : 'a Wp.Lang.infoprover -> 'a
method link : Wp.Lang.Fun.t -> Qed.Engine.link
method virtual sanitize : string -> string
method sanitize_field : string -> string
method sanitize_fun : string -> string
method sanitize_type : string -> string
end
module F :
sig
module QED :
sig
module ADT :
sig
type t = adt
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
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 = lfun
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 : Qed.Logic.Variable
type term
type bind
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
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
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 iter2 :
(key -> 'a option -> 'b option -> unit) ->
'a t -> 'b t -> unit
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
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
module STset :
sig
type elt = term
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
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 map : (elt -> elt) -> t -> t
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 min_elt : t -> elt
val min_elt_opt : t -> elt option
val max_elt : t -> elt
val max_elt_opt : t -> elt option
val choose : t -> elt
val choose_opt : t -> elt option
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val find_opt : elt -> t -> elt option
val find_first : (elt -> bool) -> t -> elt
val find_first_opt : (elt -> bool) -> t -> elt option
val find_last : (elt -> bool) -> t -> elt
val find_last_opt : (elt -> bool) -> t -> elt option
val of_list : elt list -> t
val to_seq_from : elt -> t -> elt Seq.t
val to_seq : t -> elt Seq.t
val add_seq : elt Seq.t -> t -> t
val of_seq : elt Seq.t -> t
end
module STmap :
sig
type key = term
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val union :
(key -> 'a -> 'a -> 'a option) -> 'a t -> '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 fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val min_binding_opt : 'a t -> (key * 'a) option
val max_binding : 'a t -> key * 'a
val max_binding_opt : 'a t -> (key * 'a) option
val choose : 'a t -> key * 'a
val choose_opt : 'a t -> (key * 'a) option
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_first : (key -> bool) -> 'a t -> key * 'a
val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
val find_last : (key -> bool) -> 'a t -> key * 'a
val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
val of_seq : (key * 'a) Seq.t -> 'a t
end
type var = Var.t
type tau = (Field.t, ADT.t) Qed.Logic.datatype
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
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
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 iter2 :
(key -> 'a option -> 'b option -> unit) ->
'a t -> 'b t -> unit
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
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
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 =
(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_float : float -> 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 -> 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
val sigma : unit -> sigma
val sigma_add : sigma -> term Tmap.t -> unit
val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
val e_subst_var : var -> term -> term -> term
val lc_bind : var -> term -> bind
val lc_open : var -> bind -> term
val lc_open_term : term -> 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 binders : term -> Qed.Logic.binder list
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 typeof :
?field:(Field.t -> tau) ->
?record:(Field.t -> tau) ->
?call:(Fun.t -> tau option list -> tau) -> term -> tau
val set_builtin : Fun.t -> (term list -> term) -> unit
val set_builtin_map : Fun.t -> (term list -> term list) -> unit
val set_builtin_get : Fun.t -> (term list -> term -> term) -> unit
val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
val consequence : term -> term -> term
val literal : term -> bool * term
val affine : term -> 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 debug : Format.formatter -> t -> unit
val pp_id : Format.formatter -> t -> unit
val pp_rid : Format.formatter -> t -> unit
val pp_repr : Format.formatter -> repr -> unit
val is_subterm : term -> term -> bool
val shared :
?shared:(term -> bool) ->
?shareable:(term -> bool) ->
?subterms:((term -> unit) -> term -> unit) ->
term list -> term list
type marks
val marks :
?shared:(term -> bool) ->
?shareable:(term -> bool) ->
?subterms:((term -> unit) -> term -> unit) -> unit -> marks
val mark : marks -> term -> unit
val share : marks -> term -> unit
val defs : marks -> term list
end
type var = Wp.Lang.F.QED.var
type tau = Wp.Lang.F.QED.tau
type pool = Wp.Lang.F.QED.pool
module Tau = QED.Tau
module Var = QED.Var
module Vars :
sig
type elt = var
type 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
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 iter2 :
(key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
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 pool : ?copy:Wp.Lang.F.pool -> unit -> Wp.Lang.F.pool
val fresh :
Wp.Lang.F.pool -> ?basename:string -> Wp.Lang.F.tau -> Wp.Lang.F.var
val add_var : Wp.Lang.F.pool -> Wp.Lang.F.var -> unit
val add_vars : Wp.Lang.F.pool -> Wp.Lang.F.Vars.t -> unit
val tau_of_var : Wp.Lang.F.var -> Wp.Lang.F.tau
type term = Wp.Lang.F.QED.term
type record = (Wp.Lang.field * Wp.Lang.F.term) list
val hash : Wp.Lang.F.term -> int
val equal : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val compare : Wp.Lang.F.term -> Wp.Lang.F.term -> int
module Tset :
sig
type elt = term
type 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
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 iter2 :
(key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
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 unop = Wp.Lang.F.term -> Wp.Lang.F.term
type binop = Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_zero : Wp.Lang.F.term
val e_one : Wp.Lang.F.term
val e_minus_one : Wp.Lang.F.term
val e_minus_one_real : Wp.Lang.F.term
val e_one_real : Wp.Lang.F.term
val e_zero_real : Wp.Lang.F.term
val constant : Wp.Lang.F.term -> Wp.Lang.F.term
val e_fact : int -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_int64 : int64 -> Wp.Lang.F.term
val e_bigint : Integer.t -> Wp.Lang.F.term
val e_float : float -> Wp.Lang.F.term
val e_setfield :
Wp.Lang.F.term -> Wp.Lang.field -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_range : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val is_zero : Wp.Lang.F.term -> bool
val e_true : Wp.Lang.F.term
val e_false : Wp.Lang.F.term
val e_bool : bool -> Wp.Lang.F.term
val e_literal : bool -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_int : int -> Wp.Lang.F.term
val e_zint : Z.t -> Wp.Lang.F.term
val e_real : Q.t -> Wp.Lang.F.term
val e_var : Wp.Lang.F.var -> Wp.Lang.F.term
val e_opp : Wp.Lang.F.term -> Wp.Lang.F.term
val e_times : Z.t -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_sum : Wp.Lang.F.term list -> Wp.Lang.F.term
val e_prod : Wp.Lang.F.term list -> Wp.Lang.F.term
val e_add : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_sub : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_mul : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_div : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_mod : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_eq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_neq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_leq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_lt : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_imply : Wp.Lang.F.term list -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_equiv : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_and : Wp.Lang.F.term list -> Wp.Lang.F.term
val e_or : Wp.Lang.F.term list -> Wp.Lang.F.term
val e_not : Wp.Lang.F.term -> Wp.Lang.F.term
val e_if :
Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_const : Wp.Lang.F.tau -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_get : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_set :
Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val e_getfield : Wp.Lang.F.term -> Wp.Lang.Field.t -> Wp.Lang.F.term
val e_record : Wp.Lang.F.record -> Wp.Lang.F.term
val e_fun : Wp.Lang.Fun.t -> Wp.Lang.F.term list -> Wp.Lang.F.term
val e_bind :
Qed.Logic.binder -> Wp.Lang.F.var -> Wp.Lang.F.term -> Wp.Lang.F.term
type pred
type cmp = Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
type operator = Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
module Pmap :
sig
type key = pred
type 'a 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 iter2 :
(key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
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
module Pset :
sig
type elt = pred
type 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
val p_true : Wp.Lang.F.pred
val p_false : Wp.Lang.F.pred
val p_equal : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
val p_equals :
(Wp.Lang.F.term * Wp.Lang.F.term) list -> Wp.Lang.F.pred list
val p_neq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
val p_leq : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
val p_lt : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.pred
val p_positive : Wp.Lang.F.term -> Wp.Lang.F.pred
val is_ptrue : Wp.Lang.F.pred -> Qed.Logic.maybe
val is_pfalse : Wp.Lang.F.pred -> Qed.Logic.maybe
val is_equal : Wp.Lang.F.term -> Wp.Lang.F.term -> Qed.Logic.maybe
val eqp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
val comparep : Wp.Lang.F.pred -> Wp.Lang.F.pred -> int
val p_bool : Wp.Lang.F.term -> Wp.Lang.F.pred
val e_prop : Wp.Lang.F.pred -> Wp.Lang.F.term
val p_bools : Wp.Lang.F.term list -> Wp.Lang.F.pred list
val e_props : Wp.Lang.F.pred list -> Wp.Lang.F.term list
val lift :
(Wp.Lang.F.term -> Wp.Lang.F.term) ->
Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_not : Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_and : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_or : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_imply : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_equiv : Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_hyps : Wp.Lang.F.pred list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_if :
Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_conj : Wp.Lang.F.pred list -> Wp.Lang.F.pred
val p_disj : Wp.Lang.F.pred list -> Wp.Lang.F.pred
val p_any : ('a -> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred
val p_all : ('a -> Wp.Lang.F.pred) -> 'a list -> Wp.Lang.F.pred
val p_call : Wp.Lang.lfun -> Wp.Lang.F.term list -> Wp.Lang.F.pred
val p_forall : Wp.Lang.F.var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_exists : Wp.Lang.F.var list -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_bind :
Qed.Logic.binder -> Wp.Lang.F.var -> Wp.Lang.F.pred -> Wp.Lang.F.pred
type sigma = Wp.Lang.F.QED.sigma
val sigma : unit -> Wp.Lang.F.sigma
val e_subst :
?sigma:Wp.Lang.F.sigma ->
(Wp.Lang.F.term -> Wp.Lang.F.term) ->
Wp.Lang.F.term -> Wp.Lang.F.term
val p_subst :
?sigma:Wp.Lang.F.sigma ->
(Wp.Lang.F.term -> Wp.Lang.F.term) ->
Wp.Lang.F.pred -> Wp.Lang.F.pred
val p_apply :
Wp.Lang.F.var -> Wp.Lang.F.term -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val e_vars : Wp.Lang.F.term -> Wp.Lang.F.var list
val p_vars : Wp.Lang.F.pred -> Wp.Lang.F.var list
val p_close : Wp.Lang.F.pred -> Wp.Lang.F.pred
val pp_tau : Stdlib.Format.formatter -> Wp.Lang.F.tau -> unit
val pp_var : Stdlib.Format.formatter -> Wp.Lang.F.var -> unit
val pp_vars : Stdlib.Format.formatter -> Wp.Lang.F.Vars.t -> unit
val pp_term : Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
val pp_pred : Stdlib.Format.formatter -> Wp.Lang.F.pred -> unit
val debugp : Stdlib.Format.formatter -> Wp.Lang.F.pred -> unit
type env
val context_pp : Wp.Lang.F.env Wp.Context.value
type marks = Wp.Lang.F.QED.marks
val env : Wp.Lang.F.Vars.t -> Wp.Lang.F.env
val marker : Wp.Lang.F.env -> Wp.Lang.F.marks
val mark_e : Wp.Lang.F.marks -> Wp.Lang.F.term -> unit
val mark_p : Wp.Lang.F.marks -> Wp.Lang.F.pred -> unit
val defs : Wp.Lang.F.marks -> Wp.Lang.F.term list
val define :
(Wp.Lang.F.env -> string -> Wp.Lang.F.term -> unit) ->
Wp.Lang.F.env -> Wp.Lang.F.marks -> Wp.Lang.F.env
val pp_eterm :
Wp.Lang.F.env -> Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
val pp_epred :
Wp.Lang.F.env -> Stdlib.Format.formatter -> Wp.Lang.F.pred -> unit
val p_expr : Wp.Lang.F.pred -> Wp.Lang.F.pred Wp.Lang.F.QED.expression
val e_expr : Wp.Lang.F.pred -> Wp.Lang.F.term Wp.Lang.F.QED.expression
val p_iter :
(Wp.Lang.F.pred -> unit) ->
(Wp.Lang.F.term -> unit) -> Wp.Lang.F.pred -> unit
val lc_closed : Wp.Lang.F.term -> bool
val lc_iter : (Wp.Lang.F.term -> unit) -> Wp.Lang.F.term -> unit
val lc_map :
(Wp.Lang.F.term -> Wp.Lang.F.term) ->
Wp.Lang.F.term -> Wp.Lang.F.term
val decide : Wp.Lang.F.term -> bool
val basename : Wp.Lang.F.term -> string
val is_true : Wp.Lang.F.term -> Qed.Logic.maybe
val is_false : Wp.Lang.F.term -> Qed.Logic.maybe
val is_prop : Wp.Lang.F.term -> bool
val is_int : Wp.Lang.F.term -> bool
val is_real : Wp.Lang.F.term -> bool
val is_arith : Wp.Lang.F.term -> bool
val is_closed : Wp.Lang.F.term -> bool
val is_simple : Wp.Lang.F.term -> bool
val is_atomic : Wp.Lang.F.term -> bool
val is_primitive : Wp.Lang.F.term -> bool
val is_neutral : Wp.Lang.Fun.t -> Wp.Lang.F.term -> bool
val is_absorbant : Wp.Lang.Fun.t -> Wp.Lang.F.term -> bool
val record_with :
Wp.Lang.F.record -> (Wp.Lang.F.term * Wp.Lang.F.record) option
val are_equal : Wp.Lang.F.term -> Wp.Lang.F.term -> Qed.Logic.maybe
val eval_eq : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val eval_neq : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val eval_lt : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val eval_leq : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val repr : Wp.Lang.F.term -> Wp.Lang.F.QED.repr
val sort : Wp.Lang.F.term -> Qed.Logic.sort
val vars : Wp.Lang.F.term -> Wp.Lang.F.Vars.t
val varsp : Wp.Lang.F.pred -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> Wp.Lang.F.term -> bool
val occursp : Wp.Lang.F.var -> Wp.Lang.F.pred -> bool
val intersect : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val intersectp : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
val is_subterm : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val typeof :
?field:(Wp.Lang.Field.t -> Wp.Lang.F.tau) ->
?record:(Wp.Lang.Field.t -> Wp.Lang.F.tau) ->
?call:(Wp.Lang.Fun.t -> Wp.Lang.F.tau option list -> Wp.Lang.F.tau) ->
Wp.Lang.F.term -> Wp.Lang.F.tau
val set_builtin :
Wp.Lang.lfun -> (Wp.Lang.F.term list -> Wp.Lang.F.term) -> unit
val set_builtin_get :
Wp.Lang.lfun ->
(Wp.Lang.F.term list -> Wp.Lang.F.term -> Wp.Lang.F.term) -> unit
val set_builtin_1 : Wp.Lang.lfun -> Wp.Lang.F.unop -> unit
val set_builtin_2 : Wp.Lang.lfun -> Wp.Lang.F.binop -> unit
val set_builtin_eq : Wp.Lang.lfun -> Wp.Lang.F.binop -> unit
val set_builtin_leq : Wp.Lang.lfun -> Wp.Lang.F.binop -> unit
val set_builtin_eqp : Wp.Lang.lfun -> Wp.Lang.F.cmp -> unit
val release : unit -> unit
module Check :
sig
val reset : unit -> unit
val set : string -> unit
val is_set : unit -> bool
val iter :
(qed:Wp.Lang.F.term ->
raw:Wp.Lang.F.term -> goal:Wp.Lang.F.pred -> unit) ->
unit
end
end
module N :
sig
val ( + ) : Wp.Lang.F.binop
val ( - ) : Wp.Lang.F.binop
val ( ~- ) : Wp.Lang.F.unop
val ( * ) : Wp.Lang.F.binop
val ( / ) : Wp.Lang.F.binop
val ( mod ) : Wp.Lang.F.binop
val ( = ) : Wp.Lang.F.cmp
val ( < ) : Wp.Lang.F.cmp
val ( > ) : Wp.Lang.F.cmp
val ( <= ) : Wp.Lang.F.cmp
val ( >= ) : Wp.Lang.F.cmp
val ( <> ) : Wp.Lang.F.cmp
val ( && ) : Wp.Lang.F.operator
val ( || ) : Wp.Lang.F.operator
val not : Wp.Lang.F.pred -> Wp.Lang.F.pred
val ( $ ) : Wp.Lang.lfun -> Wp.Lang.F.term list -> Wp.Lang.F.term
val ( $$ ) : Wp.Lang.lfun -> Wp.Lang.F.term list -> Wp.Lang.F.pred
end
type gamma
val new_pool :
?copy:Wp.Lang.F.pool -> ?vars:Wp.Lang.F.Vars.t -> unit -> Wp.Lang.F.pool
val new_gamma : ?copy:Wp.Lang.gamma -> unit -> Wp.Lang.gamma
val local :
?pool:Wp.Lang.F.pool ->
?vars:Wp.Lang.F.Vars.t -> ?gamma:Wp.Lang.gamma -> ('a -> 'b) -> 'a -> 'b
val freshvar : ?basename:string -> Wp.Lang.F.tau -> Wp.Lang.F.var
val freshen : Wp.Lang.F.var -> Wp.Lang.F.var
val assume : Wp.Lang.F.pred -> unit
val without_assume : ('a -> 'b) -> 'a -> 'b
val epsilon :
?basename:string ->
Wp.Lang.F.tau -> (Wp.Lang.F.term -> Wp.Lang.F.pred) -> Wp.Lang.F.term
val hypotheses : Wp.Lang.gamma -> Wp.Lang.F.pred list
val variables : Wp.Lang.gamma -> Wp.Lang.F.var list
val get_pool : unit -> Wp.Lang.F.pool
val get_gamma : unit -> Wp.Lang.gamma
val has_gamma : unit -> bool
val get_hypotheses : unit -> Wp.Lang.F.pred list
val get_variables : unit -> Wp.Lang.F.var list
module Alpha :
sig
type t
val create : unit -> Wp.Lang.Alpha.t
val get : Wp.Lang.Alpha.t -> Wp.Lang.F.var -> Wp.Lang.F.var
val iter :
(Wp.Lang.F.var -> Wp.Lang.F.var -> unit) -> Wp.Lang.Alpha.t -> unit
val convert : Wp.Lang.Alpha.t -> Wp.Lang.F.term -> Wp.Lang.F.term
val convertp : Wp.Lang.Alpha.t -> Wp.Lang.F.pred -> Wp.Lang.F.pred
end
module Subst :
sig
type sigma
val sigma :
Wp.Lang.F.var list -> Wp.Lang.F.term list -> Wp.Lang.Subst.sigma
val e_apply : Wp.Lang.Subst.sigma -> Wp.Lang.F.term -> Wp.Lang.F.term
val p_apply : Wp.Lang.Subst.sigma -> Wp.Lang.F.pred -> Wp.Lang.F.pred
end
exception Contradiction
class type simplifier =
object
method assume : Wp.Lang.F.pred -> unit
method copy : Wp.Lang.simplifier
method fixpoint : unit
method infer : Wp.Lang.F.pred list
method name : string
method simplify_branch : Wp.Lang.F.pred -> Wp.Lang.F.pred
method simplify_exp : Wp.Lang.F.term -> Wp.Lang.F.term
method simplify_goal : Wp.Lang.F.pred -> Wp.Lang.F.pred
method simplify_hyp : Wp.Lang.F.pred -> Wp.Lang.F.pred
method target : Wp.Lang.F.pred -> unit
end
end