module Model: sig
.. end
Model Registration
module S: Datatype.S_with_collections
type
t = S.t
type
model = S.t
type
tuning = unit -> unit
type
separation = Kernel_function.t -> Wp.Separation.clause list
val repr : model
val register : id:string ->
?descr:string ->
?tuning:tuning list ->
?separation:separation -> unit -> model
val get_id : model -> string
val get_descr : model -> string
val get_emitter : model -> Emitter.t
val get_separation : model -> separation
val find : id:string -> model
val iter : (model -> unit) -> unit
val with_model : model -> ('a -> 'b) -> 'a -> 'b
val on_model : model -> (unit -> unit) -> unit
val get_model : unit -> model
Current model
val is_model_defined : unit -> bool
type
scope = Kernel_function.t option
val on_scope : scope -> ('a -> 'b) -> 'a -> 'b
val on_kf : Kernel_function.t -> (unit -> unit) -> unit
on_scope (Some kf)
val on_global : (unit -> unit) -> unit
on_scope None
val get_scope : unit -> scope
val directory : unit -> string
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 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
val run_once_for_each_ast : name:string -> (unit -> unit) -> unit -> unit
run the function once for each ast