module WpContext:sig
..end
Model Registration
type
model
type
scope =
| |
Global |
| |
Kf of |
typerollback =
unit -> unit
typehypotheses =
Wp.MemoryContext.partition -> Wp.MemoryContext.partition
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.partition
typecontext =
model * scope
typet =
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:
projectified, depend on the model, not serialized
module Static:
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:
projectified, depend on the model, not serialized
module StaticGenerator:
projectified, independent from the model, not serialized
module GeneratorID:
projectified, depend on the model, not serialized
module StaticGeneratorID:
projectified, independent from the model, not serialized