env.mli 5.45 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Theory
14

15 16 17 18 19
(** Local type aliases and exceptions *)

type fformat = string (* format name *)
type filename = string (* file name *)
type extension = string (* file extension *)
20
type pathname = string list (* library path *)
21 22 23 24 25

exception KnownFormat of fformat
exception UnknownFormat of fformat
exception UnknownExtension of extension
exception UnspecifiedFormat
26
exception LibFileNotFound of pathname
27 28
exception TheoryNotFound of pathname * string

29
(** Library environment *)
30

31 32
type env

33
val env_tag : env -> Weakhtbl.tag
34

35
module Wenv : Weakhtbl.S with type key = env
36

37 38 39
val create_env : filename list -> env
(** creates an environment from a "loadpath", a list of directories
    containing loadable Why3/WhyML/etc files *)
40

41 42
val get_loadpath : env -> filename list
(** returns the loadpath of a given environment *)
43

44
val read_channel :
45
  ?format:fformat -> env -> filename -> in_channel -> theory Mstr.t
46
(** [read_channel ?format env path file ch] returns the theories in [ch].
47 48
    When given, [format] enforces the format, otherwise we choose
    the format according to [file]'s extension. Nothing ensures
49
    that [ch] corresponds to the contents of [file].
50

51 52 53 54 55
    @raise UnknownFormat [format] if the format is not registered
    @raise UnknownExtension [s] if the extension [s] is not known
      to any registered parser
    @raise UnspecifiedFormat if format is not given and [file]
      has no extension *)
56

57
val read_file : ?format:fformat -> env -> filename -> theory Mstr.t
58 59 60
(** [read_file ?format env file] returns the theories in [file].
    When given, [format] enforces the format, otherwise we choose
    the format according to [file]'s extension. *)
61

62 63
val read_theory : format:fformat -> env -> pathname -> string -> theory
(** [read_theory ~format env path th] returns the theory [path.th]
64
    from the library. The parameter [format] specifies the format
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
    of the library file to look for.

    @raise UnknownFormat [format] if the format is not registered
    @raise LibFileNotFound [path] if the library file was not found
    @raise TheoryNotFound if the theory was not found in the file *)

val find_theory : env -> pathname -> string -> theory
(** the same as [read_theory ~format:"why"]

    This function is left for compatibility purposes and may be
    removed in future versions of Why3. *)

(** Input formats *)

type 'a library
(** part of the environment restricted to a particular format *)

type 'a read_format =
  'a library -> pathname -> filename -> in_channel -> 'a * theory Mstr.t
(** [(fn : 'a read_format) lib path file ch] parses the channel [ch]
    and returns the format-specific contents of type ['a] and a set of
    logical theories. References to the library files of the same format
    are resolved via [lib]. If the parsed file is itself a part of
    the library, the argument [path] contains the fully qualified
    library name of the file, which can be put in the identifiers.
    The string argument [file] indicates the origin of the stream
    (e.g. file name) to be used in error messages. *)

val register_format :
94
  desc:Pp.formatted ->
95 96 97 98 99 100 101 102 103 104 105 106
  fformat -> extension list -> 'a read_format -> (env -> 'a library)
(** [register_format fname exts read] registers a new format [fname]
    for files with extensions from the string list [exts] (without
    the separating dot); [read] is the function to perform parsing.
    Returns a function that maps an environment to a format-specific
    library inside it.

    @raise KnownFormat [name] if the format is already registered *)

val env_of_library : 'a library -> env
(** [env_of_library lib] returns the environment of [lib] *)

107
val list_formats : unit -> (fformat * extension list * Pp.formatted) list
108
(** [list_formats ()] returns the list of registered formats *)
109

110
val read_lib_file : 'a library -> pathname -> 'a * theory Mstr.t
111
(** [read_lib_file lib path] retrieves the contents of a library file
112

113
    @raise LibFileNotFound [path] if the library file was not found *)
114

115 116 117 118 119
val read_lib_theory : 'a library -> pathname -> string -> theory
(** [read_lib_theory lib path th] returns the theory [path.th]
    from the library. This is the same as [read_theory] above,
    but the format is determined by [lib] and not by the extra
    [format] parameter.
120

121 122
    @raise LibFileNotFound [path] if the library file was not found
    @raise TheoryNotFound if the theory was not found in the file *)
123

124 125 126
val locate_lib_file : env -> fformat -> pathname -> filename
(** [locate_lib_file env format path] finds a library file in a given
    environment, knowing its format and its library path
127

128 129
    This is a low-level function that allows to accees a library file
    without parsing it. Do not use it without a good reason to do.
130

131 132
    @raise LibFileNotFound [path] if the library file was not found
    @raise UnknownFormat [format] if the format is not registered *)
133