Module WpContext

module WpContext: sig .. end

Model Registration

type model

type scope =

`\|`	`Global`
`\|`	`Kf of Kernel_function.t`

type rollback = unit -> unit

type hypotheses = MemoryContext.partition -> 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 -> MemoryContext.partition

type context = model * scope

type t = context

module S: sig .. end

module MODEL: sig .. end

module SCOPE: sig .. end

module MINDEX: Hashtbl.S  with type key = model

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