sig
type model
type scope = Global | Kf of Kernel_function.t
type tuning = unit -> unit
type hypotheses = unit -> Wp.MemoryContext.clause list
val register :
id:string ->
?descr:string ->
?tuning:Wp.WpContext.tuning list ->
?hypotheses:Wp.WpContext.hypotheses -> unit -> Wp.WpContext.model
val get_descr : Wp.WpContext.model -> string
val get_emitter : Wp.WpContext.model -> Emitter.t
val compute_hypotheses :
Wp.WpContext.model -> Kernel_function.t -> Wp.MemoryContext.clause list
type context = Wp.WpContext.model * Wp.WpContext.scope
type t = Wp.WpContext.context
module S :
sig
type t = Wp.WpContext.context
val id : Wp.WpContext.S.t -> string
val hash : Wp.WpContext.S.t -> int
val equal : Wp.WpContext.S.t -> Wp.WpContext.S.t -> bool
val compare : Wp.WpContext.S.t -> Wp.WpContext.S.t -> int
end
module MODEL :
sig
type t = Wp.WpContext.model
val id : Wp.WpContext.MODEL.t -> string
val descr : Wp.WpContext.MODEL.t -> string
val hash : Wp.WpContext.MODEL.t -> int
val equal : Wp.WpContext.MODEL.t -> Wp.WpContext.MODEL.t -> bool
val compare : Wp.WpContext.MODEL.t -> Wp.WpContext.MODEL.t -> int
val repr : Wp.WpContext.MODEL.t
end
module SCOPE :
sig
type t = Wp.WpContext.scope
val id : Wp.WpContext.SCOPE.t -> string
val hash : Wp.WpContext.SCOPE.t -> int
val equal : Wp.WpContext.SCOPE.t -> Wp.WpContext.SCOPE.t -> bool
val compare : Wp.WpContext.SCOPE.t -> Wp.WpContext.SCOPE.t -> int
end
val is_defined : unit -> bool
val on_context : Wp.WpContext.context -> ('a -> 'b) -> 'a -> 'b
val get_model : unit -> Wp.WpContext.model
val get_scope : unit -> Wp.WpContext.scope
val get_context : unit -> Wp.WpContext.context
val directory : unit -> string
module type Entries =
sig
type key
type data
val name : string
val compare :
Wp.WpContext.Entries.key -> Wp.WpContext.Entries.key -> int
val pretty : Format.formatter -> Wp.WpContext.Entries.key -> unit
end
module type Registry =
sig
module E : Entries
type key = E.key
type data = E.data
val id : basename:string -> Wp.WpContext.Registry.key -> string
val mem : Wp.WpContext.Registry.key -> bool
val find : Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data
val get :
Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data option
val clear : unit -> unit
val remove : Wp.WpContext.Registry.key -> unit
val define :
Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data -> unit
val update :
Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data -> unit
val memoize :
(Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data) ->
Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data
val compile :
(Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data) ->
Wp.WpContext.Registry.key -> unit
val callback :
(Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data -> unit) ->
unit
val iter :
(Wp.WpContext.Registry.key -> Wp.WpContext.Registry.data -> unit) ->
unit
val iter_sorted :
(Wp.WpContext.Registry.key -> Wp.WpContext.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 id : basename:string -> key -> string
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 id : basename:string -> key -> string
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.WpContext.Key.t -> Wp.WpContext.Key.t -> int
val pretty : Format.formatter -> Wp.WpContext.Key.t -> unit
end
module type Data =
sig
type key
type data
val name : string
val compile : Wp.WpContext.Data.key -> Wp.WpContext.Data.data
end
module type IData =
sig
type key
type data
val name : string
val basename : Wp.WpContext.IData.key -> string
val compile :
Wp.WpContext.IData.key -> string -> Wp.WpContext.IData.data
end
module type Generator =
sig
type key
type data
val get : Wp.WpContext.Generator.key -> Wp.WpContext.Generator.data
val mem : Wp.WpContext.Generator.key -> bool
val clear : unit -> unit
val remove : Wp.WpContext.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
module GeneratorID :
functor
(K : Key) (D : sig
type key = K.t
type data
val name : string
val basename : key -> string
val compile : key -> string -> 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 StaticGeneratorID :
functor
(K : Key) (D : sig
type key = K.t
type data
val name : string
val basename : key -> string
val compile : key -> string -> 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