store the full name of idents declared in theories and modules

The full name includes the library path to the theory/module (if any),
and the qualifier prefix of the ident in the theory/module.

src/core/theory.ml

@@ -296,9 +296,7 @@ let close_theory uc = match uc.uc_export with
   | _ -> raise CloseTheory
 
 let get_namespace uc = List.hd uc.uc_import
-let get_prefix uc = List.rev uc.uc_prefix
 let get_known uc = uc.uc_known
-
 let get_rev_decls uc = uc.uc_decls
 
 let open_namespace uc s = match uc.uc_import with
@@ -353,7 +351,19 @@ let add_tdecl uc td = match td.td_node with
 
 (** Declarations *)
 
+let store_path, restore_path =
+  let id_to_path = Wid.create 17 in
+  let store_path uc path id =
+    (* this symbol already belongs to some theory *)
+    if Wid.mem id_to_path id then () else
+    let prefix = List.rev (id.id_string :: path @ uc.uc_prefix) in
+    Wid.set id_to_path id (uc.uc_path, uc.uc_name.id_string, prefix)
+  in
+  let restore_path id = Wid.find id_to_path id in
+  store_path, restore_path
+
 let add_symbol add id v uc =
+  store_path uc [] id;
   match uc.uc_import, uc.uc_export with
   | i0 :: sti, e0 :: ste -> { uc with
       uc_import = add false id.id_string v i0 :: sti;
@@ -648,17 +658,23 @@ let clone_export uc th inst =
   let g_ts _ ts = not (Mts.mem ts inst.inst_ts) in
   let g_ls _ ls = not (Mls.mem ls inst.inst_ls) in
 
-  let f_ts ts = Mts.find_def ts ts cl.ts_table in
-  let f_ls ls = Mls.find_def ls ls cl.ls_table in
-  let f_pr pr = Mpr.find_def pr pr cl.pr_table in
-
-  let rec f_ns ns = {
-    ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.ns_ts);
-    ns_ls = Mstr.map f_ls (Mstr.filter g_ls ns.ns_ls);
-    ns_pr = Mstr.map f_pr ns.ns_pr;
-    ns_ns = Mstr.map f_ns ns.ns_ns; } in
-
-  let ns = f_ns th.th_export in
+  let f_ts p ts =
+    try let ts = Mts.find ts cl.ts_table in store_path uc p ts.ts_name; ts
+    with Not_found -> ts in
+  let f_ls p ls =
+    try let ls = Mls.find ls cl.ls_table in store_path uc p ls.ls_name; ls
+    with Not_found -> ls in
+  let f_pr p pr =
+    try let pr = Mpr.find pr cl.pr_table in store_path uc p pr.pr_name; pr
+    with Not_found -> pr in
+
+  let rec f_ns p ns = {
+    ns_ts = Mstr.map (f_ts p) (Mstr.filter g_ts ns.ns_ts);
+    ns_ls = Mstr.map (f_ls p) (Mstr.filter g_ls ns.ns_ls);
+    ns_pr = Mstr.map (f_pr p) ns.ns_pr;
+    ns_ns = Mstr.mapi (fun n -> f_ns (n::p)) ns.ns_ns; } in
+
+  let ns = f_ns [] th.th_export in
 
   match uc.uc_import, uc.uc_export with
     | i0 :: sti, e0 :: ste -> { uc with

src/core/theory.mli

@@ -133,11 +133,16 @@ val open_namespace  : theory_uc -> string -> theory_uc
 val close_namespace : theory_uc -> bool (* import *) -> theory_uc
 
 val get_namespace : theory_uc -> namespace
-val get_prefix : theory_uc -> string list
 val get_known : theory_uc -> known_map
-
 val get_rev_decls : theory_uc -> tdecl list
 
+val restore_path : ident -> string list * string * string list
+(* [restore_path id] returns the triple (library path, theory,
+   qualified symbol name) if the ident was ever introduced in
+   a theory declaration. If the ident was declared in several
+   different theories, the first association is retained.
+   Raises Not_found if the ident was never declared in a theory. *)
+
 (** Declaration constructors *)
 
 val create_decl : decl -> tdecl

src/whyml/mlw_module.ml

@@ -134,6 +134,8 @@ type modul = {
 
 type module_uc = {
   muc_theory : theory_uc;
+  muc_name   : string;
+  muc_path   : string list;
   muc_decls  : pdecl list;
   muc_prefix : string list;
   muc_import : namespace list;
@@ -143,9 +145,13 @@ type module_uc = {
   muc_used   : Sid.t;
   muc_env    : Env.env;
 }
+(* FIXME? We wouldn't need to store muc_name, muc_path,
+   and muc_prefix if theory_uc was exported *)
 
 let empty_module env n p = {
   muc_theory = create_theory ~path:p n;
+  muc_name   = Ident.preid_name n;
+  muc_path   = p;
   muc_decls  = [];
   muc_prefix = [];
   muc_import = [empty_ns];
@@ -167,7 +173,6 @@ let close_module uc =
 
 let get_theory uc = uc.muc_theory
 let get_namespace uc = List.hd uc.muc_import
-let get_prefix uc = List.rev uc.muc_prefix
 let get_known uc = uc.muc_known
 
 let open_namespace uc s = match uc.muc_import with
@@ -218,7 +223,19 @@ let use_export uc m =
 
 let add_to_theory f uc x = { uc with muc_theory = f uc.muc_theory x }
 
+let store_path, restore_path =
+  let id_to_path = Wid.create 17 in
+  let store_path uc path id =
+    (* this symbol already belongs to some theory *)
+    if Wid.mem id_to_path id then () else
+    let prefix = List.rev (id.id_string :: path @ uc.muc_prefix) in
+    Wid.set id_to_path id (uc.muc_path, uc.muc_name, prefix)
+  in
+  let restore_path id = Wid.find id_to_path id in
+  store_path, restore_path
+
 let add_symbol add id v uc =
+  store_path uc [] id;
   match uc.muc_import, uc.muc_export with
   | i0 :: sti, e0 :: ste -> { uc with
       muc_import = add false id.id_string v i0 :: sti;
@@ -254,14 +271,18 @@ let clone_export_theory uc th inst =
     | _ -> assert false in
   let g_ts _ ts = not (Mts.mem ts inst.inst_ts) in
   let g_ls _ ls = not (Mls.mem ls inst.inst_ls) in
-  let f_ts ts = TS (Mts.find_def ts ts sm.sm_ts) in
-  let f_ls ls = LS (Mls.find_def ls ls sm.sm_ls) in
-  let rec f_ns ns = {
-    ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.Theory.ns_ts);
-    ns_ps = Mstr.map f_ls (Mstr.filter g_ls ns.Theory.ns_ls);
-    ns_ns = Mstr.map f_ns ns.Theory.ns_ns; }
+  let f_ts p ts =
+    try let ts = Mts.find ts sm.sm_ts in store_path uc p ts.ts_name; TS ts
+    with Not_found -> TS ts in
+  let f_ls p ls =
+    try let ls = Mls.find ls sm.sm_ls in store_path uc p ls.ls_name; LS ls
+    with Not_found -> LS ls in
+  let rec f_ns p ns = {
+    ns_ts = Mstr.map (f_ts p) (Mstr.filter g_ts ns.Theory.ns_ts);
+    ns_ps = Mstr.map (f_ls p) (Mstr.filter g_ls ns.Theory.ns_ls);
+    ns_ns = Mstr.mapi (fun n -> f_ns (n::p)) ns.Theory.ns_ns; }
   in
-  add_to_module uc nth (f_ns th.th_export)
+  add_to_module uc nth (f_ns [] th.th_export)
 
 let add_meta uc m al =
   { uc with muc_theory = Theory.add_meta uc.muc_theory m al }
@@ -406,7 +427,6 @@ let clone_export uc m inst =
   let conv_pv pv =
     create_pvsymbol (id_clone pv.pv_vs.vs_name) (conv_vtv pv.pv_vtv) in
   let psh = Hid.create 3 in
-  let find_ps def id = try Hid.find psh id with Not_found -> def in
   let conv_xs xs = try match Hid.find psh xs.xs_name with
     | XS xs -> xs | _ -> assert false with Not_found -> xs in
   let conv_eff eff =
@@ -513,17 +533,36 @@ let clone_export uc m inst =
   let g_ps _ = function
     | LS ls -> not (Mls.mem ls inst.inst_ls)
     | _ -> true in
-  let f_ts = function
-    | TS ts -> TS (Mts.find_def ts ts sm.Theory.sm_ts)
-    | PT pt -> PT (Mits.find_def pt pt psm.sm_its) in
-  let f_ps prs = match prs with
-    | LS ls -> LS (Mls.find_def ls ls sm.Theory.sm_ls)
-    | PL pl -> PL (Mls.find_def pl pl.pl_ls psm.sm_pls)
-    | PV pv -> find_ps prs pv.pv_vs.vs_name
-    | PS ps -> find_ps prs ps.ps_name
-    | XS xs -> find_ps prs xs.xs_name in
-  let rec f_ns ns = {
-    ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.ns_ts);
-    ns_ps = Mstr.map f_ps (Mstr.filter g_ps ns.ns_ps);
-    ns_ns = Mstr.map f_ns ns.ns_ns; } in
-  add_to_module uc nth (f_ns m.mod_export)
+  let f_ts p = function
+    | TS ts ->
+        begin try let ts = Mts.find ts sm.Theory.sm_ts in
+          store_path uc p ts.ts_name; TS ts
+        with Not_found -> TS ts end
+    | PT pt ->
+        begin try let pt = Mits.find pt psm.sm_its in
+          store_path uc p pt.its_pure.ts_name; PT pt
+        with Not_found -> PT pt end in
+  let find_prs p def id =
+    try let s = Hid.find psh id in match s with
+      | PV pv -> store_path uc p pv.pv_vs.vs_name; s
+      | PS ps -> store_path uc p ps.ps_name; s
+      | XS xs -> store_path uc p xs.xs_name; s
+      | LS _ | PL _ -> assert false
+    with Not_found -> def in
+  let f_ps p prs = match prs with
+    | LS ls ->
+        begin try let ls = Mls.find ls sm.Theory.sm_ls in
+          store_path uc p ls.ls_name; LS ls
+        with Not_found -> LS ls end
+    | PL pl ->
+        begin try let pl = Mls.find pl.pl_ls psm.sm_pls in
+          store_path uc p pl.pl_ls.ls_name; PL pl
+        with Not_found -> PL pl end
+    | PV pv -> find_prs p prs pv.pv_vs.vs_name
+    | PS ps -> find_prs p prs ps.ps_name
+    | XS xs -> find_prs p prs xs.xs_name in
+  let rec f_ns p ns = {
+    ns_ts = Mstr.map (f_ts p) (Mstr.filter g_ts ns.ns_ts);
+    ns_ps = Mstr.map (f_ps p) (Mstr.filter g_ps ns.ns_ps);
+    ns_ns = Mstr.mapi (fun n -> f_ns (n::p)) ns.ns_ns; } in
+  add_to_module uc nth (f_ns [] m.mod_export)

src/whyml/mlw_module.mli

@@ -74,9 +74,15 @@ val close_namespace : module_uc -> bool -> module_uc
 
 val get_theory : module_uc -> theory_uc
 val get_namespace : module_uc -> namespace
-val get_prefix : module_uc -> string list
 val get_known : module_uc -> known_map
 
+val restore_path : ident -> string list * string * string list
+(* [restore_path id] returns the triple (library path, module,
+   qualified symbol name) if the ident was ever introduced in
+   a module declaration. If the ident was declared in several
+   different modules, the first association is retained.
+   Raises Not_found if the ident was never declared in a module. *)
+
 (** Use and clone *)
 
 val use_export : module_uc -> modul -> module_uc