env.mli 2.28 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

MARCHE Claude's avatar
MARCHE Claude committed
20
(** Access to Environment, Load Path *)
Andrei Paskevich's avatar
Andrei Paskevich committed
21

MARCHE Claude's avatar
MARCHE Claude committed
22
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
23 24 25

type env

Andrei Paskevich's avatar
Andrei Paskevich committed
26
val env_tag : env -> Hashweak.tag
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30 31
type retrieve_theory = env -> string list -> theory Mnm.t

val create_env : retrieve_theory -> env

32 33
exception TheoryNotFound of string list * string

Andrei Paskevich's avatar
Andrei Paskevich committed
34
val find_theory : env -> string list -> string -> theory
35
  (** [find_theory e p n] finds the theory named [p.n] in environment [e]
Francois Bobot's avatar
Francois Bobot committed
36
      @raise TheoryNotFound if theory not present in env [e] *)
37 38 39

(** Parsers *)

40
type read_channel = env -> string -> in_channel -> theory Mnm.t
41

42
val register_format : string -> string list -> read_channel -> unit
43
  (** [register_format name extensions f1 f2] registers a new format
44
      under name [name], for files with extensions in list [extensions];
45
      [f1] is the function to perform parsing *)
46 47 48

val read_channel : ?name:string -> read_channel

49
exception UnknownFormat of string (* format name *)
50

51 52
val list_formats : unit -> (string * string list) list