env.mli 7.39 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
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

14
(** Local type aliases *)
15 16 17 18

type fformat = string (* format name *)
type filename = string (* file name *)
type extension = string (* file extension *)
19
type pathname = string list (* library path *)
20

21
(** Library environment *)
22

23 24
type env

25
val env_tag : env -> Weakhtbl.tag
26

27
module Wenv : Weakhtbl.S with type key = env
28

29 30 31
val create_env : filename list -> env
(** creates an environment from a "loadpath", a list of directories
    containing loadable Why3/WhyML/etc files *)
32

33 34
val get_loadpath : env -> filename list
(** returns the loadpath of a given environment *)
35

36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
(** Input languages *)

type 'a language

val base_language : Theory.theory Mstr.t language
(** [base_language] is the root of the tree of supported languages.
    Any input language must be translatable into pure theories for
    the purposes of verification. *)

val register_language : 'a language -> ('b -> 'a) -> 'b language
(** [register_language parent convert] adds a leaf to the language tree.
    The [convert] function provides translation from the new language to
    [parent]. *)

val add_builtin : 'a language -> (pathname -> 'a) -> unit
(** [add_builtin lang builtin] adds new builtin libraries to [lang].
    The [builtin] function is called by [read_library] (below) for any
    library path that starts with "why3" (this prefix is not passed to
    [builtin]). For all library paths not covered by [builtin] it must
    raise [Not_found].

    By convention, every builtin theory of the base language is placed
    under a separate pathname that ends with the name of the theory.
    For example, the full qualified name of the [Builtin] theory is
    [why3.Builtin.Builtin]. The name of the theory is duplicated in
    the library path to ensure that every builtin theory is obtained
    from a separate call to [builtin], which permits to generate
    builtin theories on demand.

    If there are several definitions of a builtin library for a given
    language and path, they must be physically identical, otherwise
    [LibraryConflict] is raised. For example, if an offspring language
    provides extended definitions of builtin theories, they must be
    [convert]'ed into exactly the same singleton [theory Mstr.t] maps
    as stored for the base language. *)

type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a
(** [(fn : 'a format_parser) env path file ch] parses the in_channel [ch]
    and returns the language-specific contents of type ['a]. References
    to libraries in the input file are resolved via [env]. If the parsed
    file is itself a library file, the argument [path] contains the fully
    qualified library path of the file, which can be put in the identifiers.
    The string argument [file] indicates the origin of the stream (file name)
    to be used in error messages. *)
80

81 82
exception KnownFormat of fformat
exception KnownExtension of extension * fformat
83

84 85 86 87 88 89
val register_format :
  desc:Pp.formatted ->
  fformat -> extension list -> 'a language -> 'a format_parser -> unit
(** [register_format ~desc format_name exts lang parser] registers a new
    format [fname] for files with extensions from the string list [exts]
    (without the separating dot).
90

91 92 93
    @raise KnownFormat [name] if the format is already registered
    @raise KnownExtension [ext,name] if a parser for [ext] is already
      registered for format [name] *)
94

95 96 97 98 99
val list_formats :
  'a language -> (fformat * extension list * Pp.formatted) list
(** [list_formats lang] returns the list of registered formats that can
    be translated to [lang]. Use [list_formats base_language] to obtain
    the list of all registered formats. *)
100

101
(** Language-specific parsers *)
102

103 104 105 106
exception InvalidFormat of fformat
exception UnknownFormat of fformat
exception UnknownExtension of extension
exception UnspecifiedFormat
107

108 109 110 111 112 113
val read_channel :
  ?format:fformat -> 'a language -> env -> filename -> in_channel -> 'a
(** [read_channel ?format lang env file ch] returns the contents of [ch]
    in language [lang]. When given, [format] enforces the format, otherwise
    we choose the parser according to [file]'s extension. Nothing ensures
    that [ch] corresponds to the contents of [file].
114

115 116 117 118 119 120 121
    @raise InvalidFormat [format] if the format, given in the parameter
      or determined from the file's extension, does not translate to [lang]
    @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 *)
122

123 124
val read_file : ?format:fformat -> 'a language -> env -> filename -> 'a
(** an open-close wrapper around [read_channel] *)
125

126 127 128
exception LibraryNotFound of pathname
exception LibraryConflict of pathname
exception AmbiguousPath of filename * filename
129

130 131 132 133 134
val read_library : 'a language -> env -> pathname -> 'a
(** [read_lib_file lang env path] returns the contents of the library
    file specified by [path]. If [path] starts with ["why3"] then the
    [builtin] functions of the language are called on [List.tl path].
    If [path] is empty, [builtin] are called on the empty path.
135

136 137 138 139 140 141 142
    @raise InvalidFormat [format] if the format of the library file,
      determined from the file's extension, does not translate to [lang]
    @raise LibraryNotFound [path] if the library file was not found
    @raise LibraryConflict [path] if a bultin library has several
      non-physically-equal definitions
    @raise AmbiguousPath [(file1,file2)] if [env] contains two library
      files corresponding to [path] *)
143

144 145 146
val locate_library : env -> pathname -> filename
(** [locate_lib_file env path] returns the location of the library
    file specified by [path].
147

148 149
    This is a low-level function that allows to accees a library file
    without parsing it. Do not use it without a good reason.
150

151 152 153 154 155
    @raise LibraryNotFound [path] if the library file was not found
    @raise AmbiguousPath [(file1,file2)] if [env] contains two library
      files corresponding to [path]
    @raise InvalidArgument if the library path starts with "why3" or
      is empty. *)
156

157
exception TheoryNotFound of pathname * string
158

159 160 161 162 163 164 165 166 167 168 169
val read_theory : env -> pathname -> string -> Theory.theory
(** [read_theory env path th] returns the theory [path.th] from
    the library. If [path] is empty, it is assumed to be ["why3".th],
    that is, [read_theory env [] "Bool"] will look for the builtin
    theory [why3.Bool.Bool] (see [register_language]).

    @raise LibraryNotFound [path] if the library file was not found
    @raise LibraryConflict [path] if a bultin library has several
      non-physically-equal definitions
    @raise AmbiguousPath [(file1,file2)] if [env] contains two library
      files corresponding to [path]
170
    @raise TheoryNotFound if the theory was not found in the file *)