module WpContext: sig
.. end
Model Registration
type
model
type
scope =
| |
Global |
| |
Kf of Kernel_function.t |
type
rollback = unit -> unit
type
hypotheses = unit -> 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 -> 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:
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: 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