diff --git a/src/core/env.ml b/src/core/env.ml index 57ec4f1465a2966970504a736bd99682fe249920..14665fe3066cc6e2ef32646593f3bf53a7a5b696 100644 --- a/src/core/env.ml +++ b/src/core/env.ml @@ -22,7 +22,7 @@ open Theory (** Environment *) -type retrieve_channel = string list -> in_channel +type retrieve_channel = string list -> string * in_channel type env = { env_ret_chan : retrieve_channel; diff --git a/src/core/env.mli b/src/core/env.mli index c4d7099c99bf8fc829479faba5aecc9ce2e2f5a9..973120458fab4ed8cf282f4f03e8ffcc4d7bcd8b 100644 --- a/src/core/env.mli +++ b/src/core/env.mli @@ -27,7 +27,9 @@ val env_tag : env -> Hashweak.tag module Wenv : Hashweak.S with type key = env -type retrieve_channel = string list -> in_channel +type retrieve_channel = string list -> string * in_channel + (** retrieves a channel from a given path; a filename is also returned, + for printing purposes only *) type retrieve_theory = env -> string list -> theory Mnm.t @@ -39,7 +41,7 @@ val find_theory : env -> string list -> string -> theory (** [find_theory e p n] finds the theory named [p.n] in environment [e] @raise TheoryNotFound if theory not present in env [e] *) -val find_channel : env -> string list -> in_channel +val find_channel : env -> string list -> string * in_channel (** Parsers *) diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll index 1ec4b7bfa786fd104ac14795a1e0945eded98208..7324f2326ba2dd180b7a1c5e008b2a394c493c97 100644 --- a/src/parser/lexer.mll +++ b/src/parser/lexer.mll @@ -282,7 +282,8 @@ and string = parse let create_env lp = let ret_chan sl = let f = List.fold_left Filename.concat "" sl in - open_in (locate_file lp f) + let file = locate_file lp f in + file, open_in file in let retrieve env sl = let f = List.fold_left Filename.concat "" sl ^ ".why" in diff --git a/src/programs/pgm_env.ml b/src/programs/pgm_env.ml index 028924bd9733463a6818dc6a1d45bb594bb48838..1daeef87688a40b21b8b6572263075eee4c60b70 100644 --- a/src/programs/pgm_env.ml +++ b/src/programs/pgm_env.ml @@ -8,7 +8,7 @@ type t = { memo : (string list, Pgm_module.t Mnm.t) Hashtbl.t; } -and retrieve_module = t -> in_channel -> Pgm_module.t Mnm.t +and retrieve_module = t -> string -> in_channel -> Pgm_module.t Mnm.t let get_env penv = penv.env @@ -29,8 +29,8 @@ let find_library penv sl = try Hashtbl.find penv.memo sl with Not_found -> Hashtbl.add penv.memo sl Mnm.empty; - let c = Env.find_channel penv.env (add_suffix sl) in - let m = penv.retrieve penv c in + let file, c = Env.find_channel penv.env (add_suffix sl) in + let m = penv.retrieve penv file c in close_in c; Hashtbl.replace penv.memo sl m; m diff --git a/src/programs/pgm_env.mli b/src/programs/pgm_env.mli index b97b4242025f73165c62165fbb318a0dc145ca65..2bf62d907bff54e94a96efa40e797c50aedde888 100644 --- a/src/programs/pgm_env.mli +++ b/src/programs/pgm_env.mli @@ -6,7 +6,7 @@ type t val get_env : t -> Env.env -type retrieve_module = t -> in_channel -> Pgm_module.t Mnm.t +type retrieve_module = t -> string -> in_channel -> Pgm_module.t Mnm.t val create : Env.env -> retrieve_module -> t diff --git a/src/programs/pgm_main.ml b/src/programs/pgm_main.ml index 92e71c19d6ae2355f1cdcd8984a746da08b9ac95..0f313dbe9cb7b84a0f68f43c9977ed4425e2f37c 100644 --- a/src/programs/pgm_main.ml +++ b/src/programs/pgm_main.ml @@ -33,10 +33,18 @@ let add_module ?(type_only=false) env penv lmod m = let uc = create_module (Ident.id_user id.id id.id_loc) in let uc = List.fold_left (Pgm_typing.decl ~wp env penv lmod) uc m.mod_decl in let m = close_module uc in - Mstr.add id.id m lmod + Mnm.add id.id m lmod -let retrieve penv c = - assert false (*TODO*) +let retrieve penv file c = + let lb = Lexing.from_channel c in + Loc.set_file file lb; + let ml = Pgm_lexer.parse_file lb in + if Debug.test_flag Typing.debug_parse_only then + Mnm.empty + else + let type_only = Debug.test_flag Typing.debug_type_only in + let env = Pgm_env.get_env penv in + List.fold_left (add_module ~type_only env penv) Mnm.empty ml let pgm_env_of_env = let h = Env.Wenv.create 17 in @@ -49,19 +57,11 @@ let pgm_env_of_env = penv let read_channel env file c = - let lb = Lexing.from_channel c in - Loc.set_file file lb; - let ml = Pgm_lexer.parse_file lb in - if Debug.test_flag Typing.debug_parse_only then - Theory.Mnm.empty - else begin - let type_only = Debug.test_flag Typing.debug_type_only in - let penv = pgm_env_of_env env in - let mm = List.fold_left (add_module ~type_only env penv) Mstr.empty ml in - Mstr.fold - (fun _ m tm -> Theory.Mnm.add m.m_name.id_string m.m_th tm) - mm Theory.Mnm.empty - end + let penv = pgm_env_of_env env in + let mm = retrieve penv file c in + Mnm.fold + (fun _ m tm -> Theory.Mnm.add m.m_name.id_string m.m_th tm) + mm Theory.Mnm.empty let () = Env.register_format "whyml" ["mlw"] read_channel diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index 60fd721d1598cb05c80fade3f3d282cca18e38c4..e7d0aa180708e3550906aef4fbc052c11a35491b 100644 --- a/src/programs/pgm_typing.ml +++ b/src/programs/pgm_typing.ml @@ -133,6 +133,7 @@ let specialize_global loc x uc = let p = ns_find_pr (namespace uc) x in p.p_ls, specialize_type_v ~loc (Htv.create 17) p.p_tv +let dot fmt () = pp_print_string fmt "." let print_qualids = print_list dot pp_print_string let print_qualid fmt q = print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q) @@ -140,7 +141,7 @@ let print_qualid fmt q = let specialize_exception loc x uc = let s = try ns_find_ex (namespace uc) x - with Not_found -> errorm ~loc "unbound exception %a" print_qualids x + with Not_found -> errorm ~loc "@[unbound exception %a@]" print_qualids x in match Denv.specialize_lsymbol ~loc s with | tyl, Some ty -> s, tyl, ty @@ -1307,7 +1308,7 @@ let cannot_be_generalized gl = function let find_module penv lmod q id = match q with | [] -> (* local module *) - Mstr.find id lmod + Mnm.find id lmod | _ :: _ -> (* theory in file f *) Pgm_env.find_module penv q id @@ -1364,8 +1365,8 @@ let rec decl ~wp env penv lmod uc = function let m = try find_module penv lmod q id - with Not_found -> - errorm ~loc "unbound module %a" print_qualid qid + with Not_found | Pgm_env.ModuleNotFound _ -> + errorm ~loc "@[unbound module %a@]" print_qualid qid in let n = match use_as with | None -> Some (m.m_name.id_string) diff --git a/src/programs/pgm_typing.mli b/src/programs/pgm_typing.mli index 68cfebd9f77fccd79919f7f0033bbd588f9779f7..ea5db93ee1ed5e4a24f103c85596f95d2ae9d1c1 100644 --- a/src/programs/pgm_typing.mli +++ b/src/programs/pgm_typing.mli @@ -23,7 +23,7 @@ open Util val debug : Debug.flag val decl : - wp:bool -> Env.env -> Pgm_env.t -> Pgm_module.t Mstr.t -> + wp:bool -> Env.env -> Pgm_env.t -> Pgm_module.t Pgm_module.Mnm.t -> Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc val print_post : Format.formatter -> Pgm_ttree.post -> unit diff --git a/tests/test-pgm-jcf.mlw b/tests/test-pgm-jcf.mlw index 9ec5562c4973396455e0f8c2e1fe93fb56a1eaa6..a09b247dcf8c266771122bacd8aeb80ba946d9ae 100644 --- a/tests/test-pgm-jcf.mlw +++ b/tests/test-pgm-jcf.mlw @@ -1,24 +1,14 @@ -module R - - { use import programs.Prelude } - - parameter ref : v:'a -> {} ref 'a { !result = v } - - parameter set : r:ref 'a -> v:'a -> {} unit writes r { !r = v } - -end - module P { use import programs.Prelude } - use module R + use module import pervasives.Ref let test () = { true } - let r = R.ref 0 in - R.set r 1; + let r = ref 0 in + set r 1; !r { result > 0 } diff --git a/theories/pervasives.mlw b/theories/pervasives.mlw new file mode 100644 index 0000000000000000000000000000000000000000..d44174b8ece49a2d30b8bdc0a0ea112f969203e3 --- /dev/null +++ b/theories/pervasives.mlw @@ -0,0 +1,10 @@ +module Ref + + { use import programs.Prelude } + + parameter ref : v:'a -> {} ref 'a { !result = v } + + parameter set : r:ref 'a -> v:'a -> {} unit writes r { !r = v } + +end +