sig
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 : Wp.Model.model
val register :
id:string ->
?descr:string ->
?tuning:Wp.Model.tuning list ->
?separation:Wp.Model.separation -> unit -> Wp.Model.model
val get_id : Wp.Model.model -> string
val get_descr : Wp.Model.model -> string
val get_emitter : Wp.Model.model -> Emitter.t
val get_separation : Wp.Model.model -> Wp.Model.separation
val find : id:string -> Wp.Model.model
val iter : (Wp.Model.model -> unit) -> unit
val with_model : Wp.Model.model -> ('a -> 'b) -> 'a -> 'b
val on_model : Wp.Model.model -> (unit -> unit) -> unit
val get_model : unit -> Wp.Model.model
val is_model_defined : unit -> bool
type scope = Kernel_function.t option
val on_scope : Wp.Model.scope -> ('a -> 'b) -> 'a -> 'b
val on_kf : Kernel_function.t -> (unit -> unit) -> unit
val on_global : (unit -> unit) -> unit
val get_scope : unit -> Wp.Model.scope
val directory : unit -> string
module type Entries =
sig
type key
type data
val name : string
val compare : Wp.Model.Entries.key -> Wp.Model.Entries.key -> int
val pretty : Format.formatter -> Wp.Model.Entries.key -> unit
end
module type Registry =
sig
module E : Entries
type key = E.key
type data = E.data
val mem : Wp.Model.Registry.key -> bool
val find : Wp.Model.Registry.key -> Wp.Model.Registry.data
val get : Wp.Model.Registry.key -> Wp.Model.Registry.data option
val clear : unit -> unit
val remove : Wp.Model.Registry.key -> unit
val define : Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit
val update : Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit
val memoize :
(Wp.Model.Registry.key -> Wp.Model.Registry.data) ->
Wp.Model.Registry.key -> Wp.Model.Registry.data
val compile :
(Wp.Model.Registry.key -> Wp.Model.Registry.data) ->
Wp.Model.Registry.key -> unit
val callback :
(Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit) -> unit
val iter :
(Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit) -> unit
val iter_sorted :
(Wp.Model.Registry.key -> Wp.Model.Registry.data -> unit) -> unit
end
module Index :
functor (E : Entries) ->
sig
module E :
sig
type key = E.key
type data = E.data
val name : string
val compare : key -> key -> int
val pretty : Format.formatter -> key -> unit
end
type key = E.key
type data = E.data
val mem : key -> bool
val find : key -> data
val get : key -> data option
val clear : unit -> unit
val remove : key -> unit
val define : key -> data -> unit
val update : key -> data -> unit
val memoize : (key -> data) -> key -> data
val compile : (key -> data) -> key -> unit
val callback : (key -> data -> unit) -> unit
val iter : (key -> data -> unit) -> unit
val iter_sorted : (key -> data -> unit) -> unit
end
module Static :
functor (E : Entries) ->
sig
module E :
sig
type key = E.key
type data = E.data
val name : string
val compare : key -> key -> int
val pretty : Format.formatter -> key -> unit
end
type key = E.key
type data = E.data
val mem : key -> bool
val find : key -> data
val get : key -> data option
val clear : unit -> unit
val remove : key -> unit
val define : key -> data -> unit
val update : key -> data -> unit
val memoize : (key -> data) -> key -> data
val compile : (key -> data) -> key -> unit
val callback : (key -> data -> unit) -> unit
val iter : (key -> data -> unit) -> unit
val iter_sorted : (key -> data -> unit) -> unit
end
module type Key =
sig
type t
val compare : Wp.Model.Key.t -> Wp.Model.Key.t -> int
val pretty : Format.formatter -> Wp.Model.Key.t -> unit
end
module type Data =
sig
type key
type data
val name : string
val compile : Wp.Model.Data.key -> Wp.Model.Data.data
end
module type Generator =
sig
type key
type data
val get : Wp.Model.Generator.key -> Wp.Model.Generator.data
val mem : Wp.Model.Generator.key -> bool
val clear : unit -> unit
val remove : Wp.Model.Generator.key -> unit
end
module Generator :
functor
(K : Key) (D : sig
type key = K.t
type data
val name : string
val compile : key -> data
end) ->
sig
type key = D.key
type data = D.data
val get : key -> data
val mem : key -> bool
val clear : unit -> unit
val remove : key -> unit
end
module StaticGenerator :
functor
(K : Key) (D : sig
type key = K.t
type data
val name : string
val compile : key -> data
end) ->
sig
type key = D.key
type data = D.data
val get : key -> data
val mem : key -> bool
val clear : unit -> unit
val remove : key -> unit
end
end