sig
type cluster
val cluster :
id:string ->
?title:string ->
?position:Lexing.position -> unit -> Wp.Definitions.cluster
val axiomatic : Wp.LogicUsage.axiomatic -> Wp.Definitions.cluster
val section : Wp.LogicUsage.logic_section -> Wp.Definitions.cluster
val compinfo : Cil_types.compinfo -> Wp.Definitions.cluster
val matrix : Wp.Ctypes.c_object -> Wp.Definitions.cluster
val cluster_id : Wp.Definitions.cluster -> string
val cluster_title : Wp.Definitions.cluster -> string
val cluster_position : Wp.Definitions.cluster -> Lexing.position option
val cluster_age : Wp.Definitions.cluster -> int
val cluster_compare :
Wp.Definitions.cluster -> Wp.Definitions.cluster -> int
val pp_cluster : Format.formatter -> Wp.Definitions.cluster -> unit
val iter : (Wp.Definitions.cluster -> unit) -> unit
type trigger = (Wp.Lang.F.var, Wp.Lang.lfun) Qed.Engine.ftrigger
type typedef =
(Wp.Lang.F.tau, Wp.Lang.field, Wp.Lang.lfun) Qed.Engine.ftypedef
type dlemma = {
l_name : string;
l_cluster : Wp.Definitions.cluster;
l_assumed : bool;
l_types : int;
l_forall : Wp.Lang.F.var list;
l_triggers : Wp.Definitions.trigger list list;
l_lemma : Wp.Lang.F.pred;
}
type definition =
Logic of Wp.Lang.F.tau
| Value of Wp.Lang.F.tau * Wp.Definitions.recursion * Wp.Lang.F.term
| Predicate of Wp.Definitions.recursion * Wp.Lang.F.pred
| Inductive of Wp.Definitions.dlemma list
and recursion = Def | Rec
type dfun = {
d_lfun : Wp.Lang.lfun;
d_cluster : Wp.Definitions.cluster;
d_types : int;
d_params : Wp.Lang.F.var list;
d_definition : Wp.Definitions.definition;
}
module Trigger :
sig
val of_term : Wp.Lang.F.term -> Wp.Definitions.trigger
val of_pred : Wp.Lang.F.pred -> Wp.Definitions.trigger
val vars : Wp.Definitions.trigger -> Wp.Lang.F.Vars.t
end
val define_symbol : Wp.Definitions.dfun -> unit
val update_symbol : Wp.Definitions.dfun -> unit
val find_lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
val compile_lemma :
(Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma) ->
Wp.LogicUsage.logic_lemma -> unit
val define_lemma : Wp.Definitions.dlemma -> unit
val define_type :
Wp.Definitions.cluster -> Cil_types.logic_type_info -> unit
val call_fun :
Wp.Lang.lfun ->
(Wp.Lang.lfun -> Wp.Definitions.dfun) ->
Wp.Lang.F.term list -> Wp.Lang.F.term
val call_pred :
Wp.Lang.lfun ->
(Wp.Lang.lfun -> Wp.Definitions.dfun) ->
Wp.Lang.F.term list -> Wp.Lang.F.pred
type axioms = Wp.Definitions.cluster * Wp.LogicUsage.logic_lemma list
class virtual visitor :
Wp.Definitions.cluster ->
object
method do_local : Wp.Definitions.cluster -> bool
method virtual on_cluster : Wp.Definitions.cluster -> unit
method virtual on_comp :
Cil_types.compinfo -> (Wp.Lang.field * Wp.Lang.F.tau) list -> unit
method virtual on_dfun : Wp.Definitions.dfun -> unit
method virtual on_dlemma : Wp.Definitions.dlemma -> unit
method virtual on_library : string -> unit
method virtual on_type :
Cil_types.logic_type_info -> Wp.Definitions.typedef -> unit
method virtual section : string -> unit
method set_local : Wp.Definitions.cluster -> unit
method vadt : Wp.Lang.F.ADT.t -> unit
method vcluster : Wp.Definitions.cluster -> unit
method vcomp : Cil_types.compinfo -> unit
method vfield : Wp.Lang.F.Field.t -> unit
method vgoal : Wp.Definitions.axioms option -> Wp.Lang.F.pred -> unit
method vlemma : Wp.LogicUsage.logic_lemma -> unit
method vlibrary : string -> unit
method vparam : Wp.Lang.F.var -> unit
method vpred : Wp.Lang.F.pred -> unit
method vself : unit
method vsymbol : Wp.Lang.lfun -> unit
method vtau : Wp.Lang.F.tau -> unit
method vterm : Wp.Lang.F.term -> unit
method vtype : Cil_types.logic_type_info -> unit
end
end