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