Module Definitions

module Definitions: sig .. end
Unique

type cluster 
val cluster : id:string ->
?title:string -> ?position:Lexing.position -> unit -> cluster
val axiomatic : LogicUsage.axiomatic -> cluster
val section : LogicUsage.logic_section -> cluster
val compinfo : Cil_types.compinfo -> cluster
val matrix : Ctypes.c_object -> cluster
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 iter : (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 : 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 definition = 
| Logic of Lang.F.tau
| Value of Lang.F.tau * recursion * Lang.F.term
| Predicate of recursion * Lang.F.pred
| Inductive of dlemma list
type recursion = 
| Def
| Rec
type dfun = {
   d_lfun : Lang.lfun;
   d_cluster : cluster;
   d_types : int;
   d_params : Lang.F.var list;
   d_definition : definition;
}
module Trigger: sig .. end
val define_symbol : dfun -> unit
val update_symbol : dfun -> unit
val find_lemma : LogicUsage.logic_lemma -> dlemma
raises Not_found
val compile_lemma : (LogicUsage.logic_lemma -> dlemma) ->
LogicUsage.logic_lemma -> unit
val define_lemma : dlemma -> unit
val define_type : cluster -> Cil_types.logic_type_info -> unit
val call_fun : Lang.lfun ->
(Lang.lfun -> dfun) -> Lang.F.term list -> Lang.F.term
val call_pred : Lang.lfun ->
(Lang.lfun -> dfun) -> Lang.F.term list -> Lang.F.pred
type axioms = cluster * LogicUsage.logic_lemma list 
class virtual visitor : cluster -> object .. end