pgm_env.ml 2.24 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20

open Why
21
open Pgm_module
22

23 24 25 26
type t = {
  env      : Env.env;
  retrieve : retrieve_module;
  memo     : (string list, Pgm_module.t Mnm.t) Hashtbl.t;
27 28
}

29
and retrieve_module = t -> string -> in_channel -> Pgm_module.t Mnm.t
30

31
let get_env penv = penv.env
32

33 34 35 36
let create env retrieve = {
  env = env;
  retrieve = retrieve;
  memo = Hashtbl.create 17;
37
}
38

39 40 41 42 43 44 45 46 47 48 49
exception ModuleNotFound of string list * string

let rec add_suffix = function
  | [] -> assert false
  | [f] -> [f ^ ".mlw"]
  | p :: f -> p :: add_suffix f

let find_library penv sl =
  try Hashtbl.find penv.memo sl
  with Not_found ->
    Hashtbl.add penv.memo sl Mnm.empty;
50 51
    let file, c = Env.find_channel penv.env (add_suffix sl) in
    let m = penv.retrieve penv file c in
52 53 54 55 56 57 58
    close_in c;
    Hashtbl.replace penv.memo sl m;
    m

let find_module penv sl s =
  try Mnm.find s (find_library penv sl)
  with Not_found -> raise (ModuleNotFound (sl, s))