Module Wp.WpContext

module WpContext: sig .. end


Model Registration
type model 
type scope = 
| Global
| Kf of Kernel_function.t
type rollback = unit -> unit 
type hypotheses = unit -> Wp.MemoryContext.clause list 
val register : id:string ->
?descr:string ->
configure:(unit -> rollback) ->
?hypotheses:hypotheses -> unit -> model
Model registration. The model is identified by id and described by descr (that defaults to id). The configure function is called on WpContext.on_context call, it must prepare and set the different Context.values related to the model. It must return the function that allows to rollback on the original state. The hypotheses function must return the hypotheses made by the model.
val get_descr : model -> string
val get_emitter : model -> Emitter.t
val compute_hypotheses : model -> Kernel_function.t -> Wp.MemoryContext.clause list
type context = model * scope 
type t = context 
module S: sig .. end
module MODEL: sig .. end
module SCOPE: sig .. end
val is_defined : unit -> bool
val on_context : context -> ('a -> 'b) -> 'a -> 'b
val get_model : unit -> model
val get_scope : unit -> scope
val get_context : unit -> context
val directory : unit -> Datatype.Filepath.t
Current model in "-wp-out" directory
module type Entries = sig .. end
module type Registry = sig .. end
module Index: 
functor (E : Entries-> Registry with module E = E
projectified, depend on the model, not serialized
module Static: 
functor (E : Entries-> Registry with module E = E
projectified, independent from the model, not serialized
module type Key = sig .. end
module type Data = sig .. end
module type IData = sig .. end
module type Generator = sig .. end
module Generator: 
functor (K : Key-> 
functor (D : Data with type key = K.t-> Generator with type key = D.key and type data = D.data
projectified, depend on the model, not serialized
module StaticGenerator: 
functor (K : Key-> 
functor (D : Data with type key = K.t-> Generator with type key = D.key and type data = D.data
projectified, independent from the model, not serialized
module GeneratorID: 
functor (K : Key-> 
functor (D : IData with type key = K.t-> Generator with type key = D.key and type data = D.data
projectified, depend on the model, not serialized
module StaticGeneratorID: 
functor (K : Key-> 
functor (D : IData with type key = K.t-> Generator with type key = D.key and type data = D.data
projectified, independent from the model, not serialized