env.mli 2.79 KB
Newer Older
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 *)
21

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

type env

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

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

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

val read_channel : ?name:string -> read_channel
48 49 50 51 52 53 54 55 56 57
(** [read_channel ?name env f c] returns the map of theories
    in channel [c]. When given, [name] enforces the format, otherwise
    the format is chosen according to [f]'s extension. 
    Beware that it cannot be checked that [c] corresponds 
    to the contents of [f] *)

val read_file : ?name:string -> env -> string -> theory Mnm.t 
(** [read_file ?name env f] returns the map of theories
    in file [f]. When given, [name] enforces the format, otherwise
    the format is chosen according to [f]'s extension. *)
58

59
exception UnknownFormat of string (* format name *)
60

61 62
val list_formats : unit -> (string * string list) list