env.ml 8.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
Andrei Paskevich's avatar
Andrei Paskevich committed
11

12
open Stdlib
Andrei Paskevich's avatar
Andrei Paskevich committed
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
(** Library environment *)
Andrei Paskevich's avatar
Andrei Paskevich committed
15

Andrei Paskevich's avatar
Andrei Paskevich committed
16 17 18
type fformat = string (* format name *)
type filename = string (* file name *)
type extension = string (* file extension *)
Andrei Paskevich's avatar
Andrei Paskevich committed
19
type pathname = string list (* library path *)
Andrei Paskevich's avatar
Andrei Paskevich committed
20 21 22

exception KnownFormat of fformat
exception UnknownFormat of fformat
23
exception InvalidFormat of fformat
Andrei Paskevich's avatar
Andrei Paskevich committed
24
exception UnspecifiedFormat
25 26 27
exception UnknownExtension of extension

exception LibraryNotFound of pathname
Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30
exception TheoryNotFound of pathname * string
exception AmbiguousPath of filename * filename

Andrei Paskevich's avatar
Andrei Paskevich committed
31
type env = {
32
  env_path : Sstr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
33
  env_tag  : Weakhtbl.tag;
Andrei Paskevich's avatar
Andrei Paskevich committed
34 35
}

Andrei Paskevich's avatar
Andrei Paskevich committed
36
let env_tag env = env.env_tag
Andrei Paskevich's avatar
Andrei Paskevich committed
37

Andrei Paskevich's avatar
Andrei Paskevich committed
38
module Wenv = Weakhtbl.Make(struct type t = env let tag = env_tag end)
39

Andrei Paskevich's avatar
Andrei Paskevich committed
40
(** Environment construction and utilisation *)
Andrei Paskevich's avatar
Andrei Paskevich committed
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42
let create_env = let c = ref (-1) in fun lp -> {
43
  env_path = Sstr.of_list lp;
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  env_tag  = (incr c; Weakhtbl.create_tag !c)
Andrei Paskevich's avatar
Andrei Paskevich committed
45
}
Andrei Paskevich's avatar
Andrei Paskevich committed
46

47
let get_loadpath env = Sstr.elements env.env_path
48

49 50 51 52
(** Input languages *)

type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a

53 54
type format_info = fformat * extension list * Pp.formatted

55 56 57 58 59 60 61
module Hpath = Hashtbl.Make(struct
  type t = pathname
  let hash = Hashtbl.hash
  let equal = (=)
end)

type 'a language = {
62 63
  memo : 'a Hpath.t Wenv.t;
  push : env -> pathname -> 'a -> unit;
64
  regf : format_info -> unit format_parser -> unit;
65
  regb : (env -> pathname -> unit) -> unit;
66
  mutable fmts : unit format_parser Mstr.t;
67
  mutable bins : (env -> pathname -> unit) list;
68
  mutable info : format_info list;
69 70 71
}

let base_language = {
72 73
  memo = Wenv.create 3;
  push = (fun _ _ _ -> ());
74 75 76 77 78
  regf = (fun _ _ -> ());
  regb = (fun _ -> ());
  fmts = Mstr.empty;
  bins = [];
  info = [];
79 80 81 82
}

exception LibraryConflict of pathname

83 84 85 86
let store lang env path c =
  let ht = try Wenv.find lang.memo env with Not_found ->
    let ht = Hpath.create 17 in Wenv.set lang.memo env ht; ht in
  match path with
87 88
  | "why3" :: _ ->
      begin try
89 90
        if Hpath.find ht path != c then raise (LibraryConflict path)
      with Not_found -> lang.push env path c; Hpath.add ht path c end
91
  | _ ->
92 93
      assert (path = [] || not (Hpath.mem ht path));
      lang.push env path c; Hpath.add ht path c
94 95 96 97 98

let register_format lang (ff,_,_ as inf) fp =
  lang.regf inf fp;
  lang.fmts <- Mstr.add_new (KnownFormat ff) ff fp lang.fmts;
  lang.info <- inf :: lang.info
99

100 101 102
let add_builtin lang bp =
  lang.regb bp;
  lang.bins <- bp :: lang.bins
103 104

let register_language parent convert = {
105 106
  memo = Wenv.create 3;
  push = (fun env path c -> store parent env path (convert c));
107 108 109 110 111
  regf = (fun inf fp -> register_format parent inf fp);
  regb = (fun bp -> add_builtin parent bp);
  fmts = Mstr.empty;
  bins = [];
  info = [];
112 113 114
}

let extension_table = ref Mstr.empty
115

116
let register_format ~desc lang ff extl fp =
117
  let fp env path fn ch = store lang env path (fp env path fn ch) in
118 119 120
  register_format lang (ff,extl,desc) fp;
  let add_ext m e = Mstr.add e ff m in
  extension_table := List.fold_left add_ext !extension_table extl
121 122

let add_builtin lang bp =
123
  let bp env path = store lang env ("why3" :: path) (bp path) in
124
  add_builtin lang bp
125

126 127 128 129 130
let list_formats lang =
  let filter_ext (ff,extl,desc) =
    let filt e = Mstr.find e !extension_table = ff in
    ff, List.filter filt extl, desc in
  List.rev_map filter_ext lang.info
131 132

(** Input file parsing *)
Andrei Paskevich's avatar
Andrei Paskevich committed
133

Andrei Paskevich's avatar
Andrei Paskevich committed
134 135 136
let get_extension file =
  let s = try Filename.chop_extension file
    with Invalid_argument _ -> raise UnspecifiedFormat in
Andrei Paskevich's avatar
Andrei Paskevich committed
137
  let n = String.length s + 1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
138
  String.sub file n (String.length file - n)
Andrei Paskevich's avatar
Andrei Paskevich committed
139

140 141
let get_format ?format file = match format with
  | Some ff -> ff
142 143 144
  | None ->
      let ext = get_extension file in
      Mstr.find_exn (UnknownExtension ext) ext !extension_table
145

146 147 148 149 150 151
let get_parser lang ff =
  try Mstr.find ff lang.fmts
  with Not_found ->
    if Mstr.mem ff base_language.fmts
      then raise (InvalidFormat ff)
      else raise (UnknownFormat ff)
152

153 154
let read_channel ?format lang env file ch =
  let ff = get_format ?format file in
155 156
  get_parser lang ff env [] file ch;
  Hpath.find (Wenv.find lang.memo env) []
157

158
let read_lib_file ?format lang env path file =
159
  let ff = get_format ?format file in
160
  let fp = get_parser lang ff in
161
  let ch = open_in file in
162 163
  try fp env path file ch; close_in ch
  with exn -> close_in ch; raise exn
164

165
let read_file ?format lang env file =
166
  read_lib_file ?format lang env [] file;
167
  Hpath.find (Wenv.find lang.memo env) []
168

169
(** Library file parsing *)
170

171 172 173 174 175 176 177 178
let locate_library env path =
  if path = [] || path = ["why3"]
    then invalid_arg "Env.locate_library";
  let check_qualifier s =
    if (s = Filename.parent_dir_name ||
        s = Filename.current_dir_name ||
        Filename.basename s <> s)
    then invalid_arg "Env.locate_library" in
Andrei Paskevich's avatar
Andrei Paskevich committed
179
  List.iter check_qualifier path;
180
  let file = List.fold_left Filename.concat "" path in
Andrei Paskevich's avatar
Andrei Paskevich committed
181
  let add_ext ext = file ^ "." ^ ext in
182 183
  let fl = List.map add_ext (Mstr.keys !extension_table) in
  if fl = [] then failwith "Env.locate_library (no formats)";
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  let add_dir dir = List.map (Filename.concat dir) fl in
185
  let fl = List.concat (List.map add_dir (get_loadpath env)) in
186
  if fl = [] then failwith "Env.locate_library (empty loadpath)";
Andrei Paskevich's avatar
Andrei Paskevich committed
187
  match List.filter Sys.file_exists fl with
188
  | [] -> raise (LibraryNotFound path)
Andrei Paskevich's avatar
Andrei Paskevich committed
189 190 191
  | [file] -> file
  | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))

Andrei Paskevich's avatar
Andrei Paskevich committed
192 193
exception CircularDependency of pathname

194 195
let read_library lang env = function
  | "why3" :: path ->
196
      let read bp = try bp env path with Not_found -> () in
197 198 199 200
      List.iter read lang.bins
  | path ->
      let file = locate_library env path in
      read_lib_file lang env path file
Andrei Paskevich's avatar
Andrei Paskevich committed
201

202
let libstack = Hpath.create 17
203

204 205 206
let read_library lang env path =
  if Hpath.mem libstack path then
    raise (CircularDependency path);
Andrei Paskevich's avatar
Andrei Paskevich committed
207
  try
208 209 210 211
    Hpath.add libstack path ();
    read_library lang env path;
    Hpath.remove libstack path
  with exn ->
212
    Hpath.remove libstack path;
213
    raise exn
214 215 216

let read_library lang env path =
  let path = if path = [] then ["why3"] else path in
217
  try Hpath.find (Wenv.find lang.memo env) path with Not_found ->
218
  read_library lang env path;
219
  try Hpath.find (Wenv.find lang.memo env) path with Not_found ->
220
  raise (LibraryNotFound path)
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246

let read_theory env path s =
  let path = if path = [] then ["why3"; s] else path in
  let mt = read_library base_language env path in
  Mstr.find_exn (TheoryNotFound (path,s)) s mt

(* Builtin theories *)

open Ident
open Theory

let base_builtin path =
  let builtin s =
    if s = builtin_theory.th_name.id_string then builtin_theory else
    if s = highord_theory.th_name.id_string then highord_theory else
    if s = bool_theory.th_name.id_string then bool_theory else
    if s = unit_theory.th_name.id_string then unit_theory else
    match tuple_theory_name s with
    | Some n -> tuple_theory n
    | None -> raise Not_found
  in
  match path with
  | [s] -> Mstr.singleton s (builtin s)
  | _   -> raise Not_found

let () = add_builtin base_language base_builtin
247

248
(* Exception reporting *)
249

Andrei Paskevich's avatar
Andrei Paskevich committed
250 251 252
let print_path fmt sl =
  Pp.print_list (Pp.constant_string ".") Format.pp_print_string fmt sl

253
let () = Exn_printer.register
254
  begin fun fmt exn -> match exn with
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
  | CircularDependency sl -> Format.fprintf fmt
      "Circular dependency in %a" print_path sl
  | LibraryNotFound sl -> Format.fprintf fmt
      "Library file not found: %a" print_path sl
  | TheoryNotFound (sl,s) -> Format.fprintf fmt
      "Theory %s not found in library %a" s print_path sl
  | KnownFormat s -> Format.fprintf fmt
      "Format %s is already registered" s
  | UnknownFormat s -> Format.fprintf fmt
      "Unknown input format: %s" s
  | UnknownExtension s -> Format.fprintf fmt
      "Unknown file extension: `%s'" s
  | UnspecifiedFormat -> Format.fprintf fmt
      "Format not specified"
  | AmbiguousPath (f1,f2) -> Format.fprintf fmt
      "Ambiguous path:@ both %s@ and %s@ match" f1 f2
  | InvalidFormat f -> Format.fprintf fmt
272
      "Input format `%s' is unsuitable for the desired content" f
273
  | LibraryConflict sl -> Format.fprintf fmt
274
      "Conflicting definitions for builtin library %a" print_path sl
275 276
  | _ -> raise exn
  end