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 -> ('-> 'b) -> '-> '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 -> ('-> 'b) -> '-> '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 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 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 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
    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 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 end
end