sig
  type model
  type scope = Global | Kf of Kernel_function.t
  type rollback = unit -> unit
  type hypotheses = unit -> Wp.MemoryContext.clause list
  val register :
    id:string ->
    ?descr:string ->
    configure:(unit -> Wp.WpContext.rollback) ->
    ?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 -> ('-> 'b) -> '-> '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 -> Datatype.Filepath.t
  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