env.mli 3.26 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 43
  (** a function of type [read_channel] parses the given channel using
      its own syntax. The string argument indicates the origin of the stream
      (e.g. file name) to be used in error messages *)
44

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

50 51 52 53 54 55 56
exception NoFormat
exception UnknownExtension of string 
exception UnknownFormat of string (* format name *)

val read_channel : ?format:string -> read_channel
(** [read_channel ?format env f c] returns the map of theories
    in channel [c]. When given, [format] enforces the format, otherwise
57
    the format is chosen according to [f]'s extension. 
58
    Beware that nothing ensures that [c] corresponds to the contents of [f] 
59

MARCHE Claude's avatar
MARCHE Claude committed
60 61
    @raise NoFormat if [format] is not given and [f] has no extension
    @raise UnknownExtension [s] if the extension [s] is not known in 
62
      any registered parser
MARCHE Claude's avatar
MARCHE Claude committed
63
    @raise UnknownFormat [f] if the [format] is not registered
64
*)
65

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

71 72
val list_formats : unit -> (string * string list) list