env.mli 4.48 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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.                  *)
(*                                                                        *)
(**************************************************************************)

20
(** Library environment *)
21 22 23

type env

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

26 27
module Wenv : Hashweak.S with type key = env

28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
(** Local type aliases and exceptions *)

type fformat = string (* format name *)
type filename = string (* file name *)
type extension = string (* file extension *)
type pathname = string list (* path in an environment *)

exception KnownFormat of fformat
exception UnknownFormat of fformat
exception UnknownExtension of extension
exception UnspecifiedFormat

exception ChannelNotFound of pathname
exception TheoryNotFound of pathname * string

(** Input formats *)

open Theory

47 48
type read_channel =
  env -> pathname -> filename -> in_channel -> theory Util.Mstr.t
49 50 51
(** a function of type [read_channel] parses a 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 54 55 56 57
val register_format : fformat -> extension list -> read_channel -> unit
(** [register_format name extensions fn] registers a new format
    called [name], for files with extensions in the string list
    [extensions] (separating dot not included);
    [fn] is the function to perform parsing.
58

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

61 62 63
val read_channel :
  ?format:fformat -> env -> filename -> in_channel -> theory Util.Mstr.t
(** [read_channel ?format env path file ch] returns the theories in [ch].
64 65 66
    When given, [format] enforces the format, otherwise we choose
    the format according to [file]'s extension. Nothing ensures
    that [ch] corresponds to the contents of [f].
67

68 69 70 71 72
    @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 *)
73

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

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

81
(** Environment construction and utilisation *)
82

83 84 85
val create_env : filename list -> env
(** creates an environment from a "loadpath", a list of directories
    containing loadable Why3/WhyML/etc files *)
86

87
val create_env_of_loadpath : filename list -> env
88 89 90 91
(** the same as [create_env], will be removed in some future version *)

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

93 94 95 96
val find_channel : env -> fformat -> pathname -> filename * in_channel
(** finds an input channel in a given environment, knowing its format
    and its name (presented as a list of strings); a filename is also
    returned, to be used in logs or error messages.
97

98 99
    @raise ChannelNotFound [sl] if the channel [sl] was not found
    @raise UnknownFormat [f] if the format is not registered *)
100

101 102 103
val find_theory : env -> pathname -> string -> theory
(** a special case of [find_channel] that returns a particular theory,
    using the format ["why"]
104

105
    @raise TheoryNotFound if the theory was not found in a channel *)