Module Definitions

module Definitions: sig .. end
return type of an abstract function

Unique


type trigger = (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger 
type typedef = (Lang.F.tau, Lang.field, Lang.lfun) Qed.Engine.ftypedef 
type cluster = {
   c_id : string;
   c_title : string;
   c_position : Lexing.position option;
   mutable c_age : int;
   mutable c_records : Cil_types.compinfo list;
   mutable c_types : Cil_types.logic_type_info list;
   mutable c_symbols : dfun list;
   mutable c_lemmas : dlemma list;
}
type dlemma = {
   l_name : string;
   l_cluster : cluster;
   l_assumed : bool;
   l_types : int;
   l_forall : Lang.F.var list;
   l_triggers : trigger list list; (*OR of AND-triggers*)
   l_lemma : Lang.F.pred;
}
type dfun = {
   d_lfun : Lang.lfun;
   d_cluster : cluster;
   d_types : int;
   d_params : Lang.F.var list;
   d_definition : definition;
}
type definition = 
| Logic of Lang.F.tau (*return type of an abstract function*)
| Value of Lang.F.tau * recursion * Lang.F.term
| Predicate of recursion * Lang.F.pred
| Inductive of dlemma list
type recursion = 
| Def
| Rec
module Trigger: sig .. end
module Cluster: Model.Index(sig
type key = string 
type data = Definitions.cluster 
val name : string
val compare : String.t -> String.t -> int
val pretty : Format.formatter -> string -> unit
end)
module Symbol: Model.Index(sig
type key = Lang.lfun 
type data = Definitions.dfun 
val name : string
val compare : Lang.Fun.t -> Lang.Fun.t -> int
val pretty : Format.formatter -> Lang.Fun.t -> unit
end)
module Lemma: Model.Index(sig
type key = string 
type data = Definitions.dlemma 
val name : string
val compare : String.t -> String.t -> int
val pretty : Format.formatter -> string -> unit
end)
val touch : cluster -> unit
val compare_symbol : dfun -> dfun -> int
val compare_lemma : dlemma -> dlemma -> int
val define_symbol : Symbol.data -> unit
val update_symbol : Symbol.data -> unit
val find_lemma : LogicUsage.logic_lemma -> Lemma.data
val compile_lemma : (LogicUsage.logic_lemma -> Lemma.data) ->
LogicUsage.logic_lemma -> unit
val define_lemma : Lemma.data -> unit
val define_type : cluster -> Cil_types.logic_type_info -> unit
val cluster_id : cluster -> string
Unique
val cluster_title : cluster -> string
val cluster_position : cluster -> Lexing.position option
val cluster_age : cluster -> int
val cluster_compare : cluster -> cluster -> int
val pp_cluster : Format.formatter -> cluster -> unit
val newcluster : id:string ->
?title:string -> ?position:Lexing.position -> unit -> cluster
val cluster : id:Cluster.key ->
?title:Cluster.key ->
?position:Lexing.position -> unit -> Cluster.data
val axiomatic : LogicUsage.axiomatic -> Cluster.data
val section : LogicUsage.logic_section -> Cluster.data
val compinfo : Cil_types.compinfo -> Cluster.data
val matrix : Ctypes.c_object -> Cluster.data
val call_fun : Symbol.key ->
(Symbol.key -> Symbol.data) ->
Lang.F.term list -> Lang.F.term
val call_pred : Symbol.key ->
(Symbol.key -> Symbol.data) ->
Lang.F.term list -> Lang.F.pred
module DT: Cil_datatype.Logic_type_info.Set
module DR: Cil_datatype.Compinfo.Set
module DS: Datatype.String.Set
module DF: FCSet.Make(Lang.Fun)
module DC: FCSet.Make(sig
type t = Definitions.cluster 
val compare : Definitions.cluster -> Definitions.cluster -> int
end)
type axioms = cluster * LogicUsage.logic_lemma list 
class virtual visitor : DC.elt -> object .. end