programs (.mlw files) are now searched for in loadpath

parent 4294d89f
...@@ -22,7 +22,7 @@ open Theory ...@@ -22,7 +22,7 @@ open Theory
(** Environment *) (** Environment *)
type retrieve_channel = string list -> in_channel type retrieve_channel = string list -> string * in_channel
type env = { type env = {
env_ret_chan : retrieve_channel; env_ret_chan : retrieve_channel;
......
...@@ -27,7 +27,9 @@ val env_tag : env -> Hashweak.tag ...@@ -27,7 +27,9 @@ val env_tag : env -> Hashweak.tag
module Wenv : Hashweak.S with type key = env 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 type retrieve_theory = env -> string list -> theory Mnm.t
...@@ -39,7 +41,7 @@ val find_theory : env -> string list -> string -> theory ...@@ -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] (** [find_theory e p n] finds the theory named [p.n] in environment [e]
@raise TheoryNotFound if theory not present in env [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 *) (** Parsers *)
......
...@@ -282,7 +282,8 @@ and string = parse ...@@ -282,7 +282,8 @@ and string = parse
let create_env lp = let create_env lp =
let ret_chan sl = let ret_chan sl =
let f = List.fold_left Filename.concat "" sl in 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 in
let retrieve env sl = let retrieve env sl =
let f = List.fold_left Filename.concat "" sl ^ ".why" in let f = List.fold_left Filename.concat "" sl ^ ".why" in
......
...@@ -8,7 +8,7 @@ type t = { ...@@ -8,7 +8,7 @@ type t = {
memo : (string list, Pgm_module.t Mnm.t) Hashtbl.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 let get_env penv = penv.env
...@@ -29,8 +29,8 @@ let find_library penv sl = ...@@ -29,8 +29,8 @@ let find_library penv sl =
try Hashtbl.find penv.memo sl try Hashtbl.find penv.memo sl
with Not_found -> with Not_found ->
Hashtbl.add penv.memo sl Mnm.empty; Hashtbl.add penv.memo sl Mnm.empty;
let c = Env.find_channel penv.env (add_suffix sl) in let file, c = Env.find_channel penv.env (add_suffix sl) in
let m = penv.retrieve penv c in let m = penv.retrieve penv file c in
close_in c; close_in c;
Hashtbl.replace penv.memo sl m; Hashtbl.replace penv.memo sl m;
m m
......
...@@ -6,7 +6,7 @@ type t ...@@ -6,7 +6,7 @@ type t
val get_env : t -> Env.env 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 val create : Env.env -> retrieve_module -> t
......
...@@ -33,10 +33,18 @@ let add_module ?(type_only=false) env penv lmod m = ...@@ -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 = 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 uc = List.fold_left (Pgm_typing.decl ~wp env penv lmod) uc m.mod_decl in
let m = close_module uc in let m = close_module uc in
Mstr.add id.id m lmod Mnm.add id.id m lmod
let retrieve penv c = let retrieve penv file c =
assert false (*TODO*) 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 pgm_env_of_env =
let h = Env.Wenv.create 17 in let h = Env.Wenv.create 17 in
...@@ -49,19 +57,11 @@ let pgm_env_of_env = ...@@ -49,19 +57,11 @@ let pgm_env_of_env =
penv penv
let read_channel env file c = let read_channel env file c =
let lb = Lexing.from_channel c in let penv = pgm_env_of_env env in
Loc.set_file file lb; let mm = retrieve penv file c in
let ml = Pgm_lexer.parse_file lb in Mnm.fold
if Debug.test_flag Typing.debug_parse_only then (fun _ m tm -> Theory.Mnm.add m.m_name.id_string m.m_th tm)
Theory.Mnm.empty mm 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 () = Env.register_format "whyml" ["mlw"] read_channel let () = Env.register_format "whyml" ["mlw"] read_channel
......
...@@ -133,6 +133,7 @@ let specialize_global loc x uc = ...@@ -133,6 +133,7 @@ let specialize_global loc x uc =
let p = ns_find_pr (namespace uc) x in let p = ns_find_pr (namespace uc) x in
p.p_ls, specialize_type_v ~loc (Htv.create 17) p.p_tv 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_qualids = print_list dot pp_print_string
let print_qualid fmt q = let print_qualid fmt q =
print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q) print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q)
...@@ -140,7 +141,7 @@ let print_qualid fmt q = ...@@ -140,7 +141,7 @@ let print_qualid fmt q =
let specialize_exception loc x uc = let specialize_exception loc x uc =
let s = let s =
try ns_find_ex (namespace uc) x 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 in
match Denv.specialize_lsymbol ~loc s with match Denv.specialize_lsymbol ~loc s with
| tyl, Some ty -> s, tyl, ty | tyl, Some ty -> s, tyl, ty
...@@ -1307,7 +1308,7 @@ let cannot_be_generalized gl = function ...@@ -1307,7 +1308,7 @@ let cannot_be_generalized gl = function
let find_module penv lmod q id = match q with let find_module penv lmod q id = match q with
| [] -> | [] ->
(* local module *) (* local module *)
Mstr.find id lmod Mnm.find id lmod
| _ :: _ -> | _ :: _ ->
(* theory in file f *) (* theory in file f *)
Pgm_env.find_module penv q id Pgm_env.find_module penv q id
...@@ -1364,8 +1365,8 @@ let rec decl ~wp env penv lmod uc = function ...@@ -1364,8 +1365,8 @@ let rec decl ~wp env penv lmod uc = function
let m = let m =
try try
find_module penv lmod q id find_module penv lmod q id
with Not_found -> with Not_found | Pgm_env.ModuleNotFound _ ->
errorm ~loc "unbound module %a" print_qualid qid errorm ~loc "@[unbound module %a@]" print_qualid qid
in in
let n = match use_as with let n = match use_as with
| None -> Some (m.m_name.id_string) | None -> Some (m.m_name.id_string)
......
...@@ -23,7 +23,7 @@ open Util ...@@ -23,7 +23,7 @@ open Util
val debug : Debug.flag val debug : Debug.flag
val decl : 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 Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc
val print_post : Format.formatter -> Pgm_ttree.post -> unit val print_post : Format.formatter -> Pgm_ttree.post -> unit
......
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 module P
{ use import programs.Prelude } { use import programs.Prelude }
use module R use module import pervasives.Ref
let test () = let test () =
{ true } { true }
let r = R.ref 0 in let r = ref 0 in
R.set r 1; set r 1;
!r !r
{ result > 0 } { result > 0 }
......
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
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment