sig
type fformat = string
type filename = string
type extension = string
type pathname = string list
type env
val env_tag : Env.env -> Weakhtbl.tag
module Wenv :
sig
type key = env
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val copy : 'a t -> 'a t
val find : 'a t -> key -> 'a
val mem : 'a t -> key -> bool
val set : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val length : 'a t -> int
val memoize : int -> (key -> 'a) -> key -> 'a
val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
val memoize_option : int -> (key option -> 'a) -> key option -> 'a
end
val create_env : Env.filename list -> Env.env
val get_loadpath : Env.env -> Env.filename list
type 'a language
val base_language : Theory.theory Wstdlib.Mstr.t Env.language
val register_language : 'a Env.language -> ('b -> 'a) -> 'b Env.language
val add_builtin : 'a Env.language -> (Env.pathname -> 'a) -> unit
val base_language_builtin : Env.pathname -> Theory.theory Wstdlib.Mstr.t
type 'a format_parser =
Env.env -> Env.pathname -> Env.filename -> Stdlib.in_channel -> 'a
exception KnownFormat of Env.fformat
val register_format :
desc:Pp.formatted ->
'a Env.language ->
Env.fformat -> Env.extension list -> 'a Env.format_parser -> unit
val list_formats :
'a Env.language -> (Env.fformat * Env.extension list * Pp.formatted) list
val get_format : ?format:Env.fformat -> string -> Env.fformat
exception InvalidFormat of Env.fformat
exception UnknownFormat of Env.fformat
exception UnknownExtension of Env.extension
exception UnspecifiedFormat
val read_channel :
?format:Env.fformat ->
'a Env.language -> Env.env -> Env.filename -> Stdlib.in_channel -> 'a
val read_file :
?format:Env.fformat ->
'a Env.language -> Env.env -> Env.filename -> 'a * Env.fformat
exception LibraryNotFound of Env.pathname
exception LibraryConflict of Env.pathname
exception AmbiguousPath of Env.filename * Env.filename
val read_library : 'a Env.language -> Env.env -> Env.pathname -> 'a
val locate_library : Env.env -> Env.pathname -> Env.filename
exception TheoryNotFound of Env.pathname * string
val read_theory : Env.env -> Env.pathname -> string -> Theory.theory
end