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