env.mli 6.06 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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.                  *)
(*                                                                        *)
(**************************************************************************)

Andrei Paskevich's avatar
Andrei Paskevich committed
20 21
open Util
open Theory
22

Andrei Paskevich's avatar
Andrei Paskevich committed
23 24 25 26 27
(** Local type aliases and exceptions *)

type fformat = string (* format name *)
type filename = string (* file name *)
type extension = string (* file extension *)
Andrei Paskevich's avatar
Andrei Paskevich committed
28
type pathname = string list (* library path *)
Andrei Paskevich's avatar
Andrei Paskevich committed
29 30 31 32 33

exception KnownFormat of fformat
exception UnknownFormat of fformat
exception UnknownExtension of extension
exception UnspecifiedFormat
Andrei Paskevich's avatar
Andrei Paskevich committed
34
exception LibFileNotFound of pathname
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36
exception TheoryNotFound of pathname * string

Andrei Paskevich's avatar
Andrei Paskevich committed
37
(** Library environment *)
Andrei Paskevich's avatar
Andrei Paskevich committed
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39 40 41
type env

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

Andrei Paskevich's avatar
Andrei Paskevich committed
43
module Wenv : Hashweak.S with type key = env
Andrei Paskevich's avatar
Andrei Paskevich committed
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45 46 47
val create_env : filename list -> env
(** creates an environment from a "loadpath", a list of directories
    containing loadable Why3/WhyML/etc files *)
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49 50
val get_loadpath : env -> filename list
(** returns the loadpath of a given environment *)
Andrei Paskevich's avatar
Andrei Paskevich committed
51

52
val read_channel :
Andrei Paskevich's avatar
Andrei Paskevich committed
53
  ?format:fformat -> env -> filename -> in_channel -> theory Mstr.t
54
(** [read_channel ?format env path file ch] returns the theories in [ch].
Andrei Paskevich's avatar
Andrei Paskevich committed
55 56
    When given, [format] enforces the format, otherwise we choose
    the format according to [file]'s extension. Nothing ensures
Andrei Paskevich's avatar
Andrei Paskevich committed
57
    that [ch] corresponds to the contents of [file].
58

Andrei Paskevich's avatar
Andrei Paskevich committed
59 60 61 62 63
    @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 *)
64

Andrei Paskevich's avatar
Andrei Paskevich committed
65
val read_file : ?format:fformat -> env -> filename -> theory Mstr.t
Andrei Paskevich's avatar
Andrei Paskevich committed
66 67 68
(** [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. *)
69

Andrei Paskevich's avatar
Andrei Paskevich committed
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
val read_theory : format:fformat -> env -> pathname -> string -> theory
(** [read_theory ~format env path th] returns the theory [path.th]
    from the library. The parameter [format] speicifies the format
    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 :
  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] *)

Andrei Paskevich's avatar
Andrei Paskevich committed
114
val list_formats : unit -> (fformat * extension list) list
Andrei Paskevich's avatar
Andrei Paskevich committed
115
(** [list_formats ()] returns the list of registered formats *)
116

Andrei Paskevich's avatar
Andrei Paskevich committed
117 118
val read_lib_file : 'a library -> pathname -> 'a
(** [read_lib_file lib path] retrieves the contents of a library file
119

Andrei Paskevich's avatar
Andrei Paskevich committed
120
    @raise LibFileNotFound [path] if the library file was not found *)
121

Andrei Paskevich's avatar
Andrei Paskevich committed
122 123 124 125 126
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.
127

Andrei Paskevich's avatar
Andrei Paskevich committed
128 129
    @raise LibFileNotFound [path] if the library file was not found
    @raise TheoryNotFound if the theory was not found in the file *)
130

Andrei Paskevich's avatar
Andrei Paskevich committed
131 132 133
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
134

Andrei Paskevich's avatar
Andrei Paskevich committed
135 136
    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.
137

Andrei Paskevich's avatar
Andrei Paskevich committed
138 139
    @raise LibFileNotFound [path] if the library file was not found
    @raise UnknownFormat [format] if the format is not registered *)
140