env.mli 3.55 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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
module Wenv : Hashweak.S with type key = env

30
type retrieve_channel = string list -> string * in_channel
31
  (** retrieves a channel from a given path; a filename is also returned,
32
      for printing purposes only *)
33

34 35 36
type retrieve_theory  = env -> string list -> theory Mnm.t

val create_env : retrieve_channel -> retrieve_theory -> env
37

38 39
exception TheoryNotFound of string list * string

40
val find_theory : env -> string list -> string -> theory
41
  (** [find_theory e p n] finds the theory named [p.n] in environment [e]
Francois Bobot's avatar
Francois Bobot committed
42
      @raise TheoryNotFound if theory not present in env [e] *)
43

44
val find_channel : env -> string list -> string * in_channel
45

46 47
(** Parsers *)

48
type read_channel = env -> string -> in_channel -> theory Mnm.t
49 50 51
  (** 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 *)
52

53
val register_format : string -> string list -> read_channel -> unit
54
  (** [register_format name extensions f] registers a new format
55
      under name [name], for files with extensions in list [extensions];
56
      [f] is the function to perform parsing *)
57

58
exception NoFormat
59
exception UnknownExtension of string
60 61 62 63 64
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
65 66
    the format is chosen according to [f]'s extension.
    Beware that nothing ensures that [c] corresponds to the contents of [f]
67

MARCHE Claude's avatar
MARCHE Claude committed
68
    @raise NoFormat if [format] is not given and [f] has no extension
69
    @raise UnknownExtension [s] if the extension [s] is not known in
70
      any registered parser
MARCHE Claude's avatar
MARCHE Claude committed
71
    @raise UnknownFormat [f] if the [format] is not registered
72
*)
73

74
val read_file : ?format:string -> env -> string -> theory Mnm.t
75 76 77
(** [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. *)
78

79 80
val list_formats : unit -> (string * string list) list