Module Wp.Definitions

module Definitions: sig .. end

type cluster 
val cluster : id:string ->
?title:string ->
?position:Filepath.position -> unit -> cluster
val axiomatic : Wp.LogicUsage.axiomatic -> cluster
val section : Wp.LogicUsage.logic_section -> cluster
val compinfo : Cil_types.compinfo -> cluster
val matrix : Wp.Ctypes.c_object -> cluster
val cluster_id : cluster -> string

Unique

val cluster_title : cluster -> string
val cluster_position : cluster -> Filepath.position option
val cluster_age : cluster -> int
val cluster_compare : cluster -> cluster -> int
val pp_cluster : Stdlib.Format.formatter -> cluster -> unit
val iter : (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 : cluster;
   l_assumed : bool;
   l_types : int;
   l_forall : Wp.Lang.F.var list;
   l_triggers : trigger list list; (*

OR of AND-triggers

*)
   l_lemma : Wp.Lang.F.pred;
}
type definition = 
| Logic of Wp.Lang.F.tau
| Function of Wp.Lang.F.tau * recursion * Wp.Lang.F.term
| Predicate of recursion * Wp.Lang.F.pred
| Inductive of dlemma list
type recursion = 
| Def
| Rec
type dfun = {
   d_lfun : Wp.Lang.lfun;
   d_cluster : cluster;
   d_types : int;
   d_params : Wp.Lang.F.var list;
   d_definition : definition;
}
module Trigger: sig .. end
val find_symbol : Wp.Lang.lfun -> dfun
val define_symbol : dfun -> unit
val update_symbol : dfun -> unit
val find_name : string -> dlemma
val find_lemma : Wp.LogicUsage.logic_lemma -> dlemma
val compile_lemma : (Wp.LogicUsage.logic_lemma -> dlemma) ->
Wp.LogicUsage.logic_lemma -> unit
val define_lemma : dlemma -> unit
val define_type : cluster -> Cil_types.logic_type_info -> unit
val call_fun : Wp.Lang.lfun ->
(Wp.Lang.lfun -> dfun) ->
Wp.Lang.F.term list -> Wp.Lang.F.term
val call_pred : Wp.Lang.lfun ->
(Wp.Lang.lfun -> dfun) ->
Wp.Lang.F.term list -> Wp.Lang.F.pred
type axioms = cluster * Wp.LogicUsage.logic_lemma list 
class virtual visitor : cluster -> object .. end