Commit 0970675c authored by Andrei Paskevich's avatar Andrei Paskevich

remove anonymous namespaces

For realization, code extraction, metas-in-sessions, etc, we need
absolute names for identifiers. To that purpose it is better to
have and store the qualified path to every ident.
parent 5ae69cd3
......@@ -580,7 +580,7 @@ let flush_impl ~strict env uc impl =
| Suse th ->
let uc = open_namespace uc in
let uc = use_export uc th in
close_namespace uc false None
close_namespace uc false th.th_name.id_string
| _ -> uc
in
let update s e (env,uc) = match e with
......
......@@ -309,8 +309,8 @@ let close_namespace uc import s =
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
let e1 = match s with Some s -> add_ns true s e0 e1 | _ -> e1 in
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
{ uc with uc_import = i1 :: sti; uc_export = e1 :: ste; }
| [_], [_] -> raise NoOpenedNamespace
| _ -> assert false
......
......@@ -130,8 +130,8 @@ val create_theory : ?path:string list -> preid -> theory_uc
val close_theory : theory_uc -> theory
val open_namespace : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
(* the Boolean indicates [import]; the string option indicates [as T] *)
val close_namespace : theory_uc -> bool -> string -> theory_uc
(* the Boolean indicates [import]; the string indicates [as T] *)
val get_namespace : theory_uc -> namespace
val get_known : theory_uc -> known_map
......
......@@ -283,8 +283,8 @@ new_decl:
{ Incremental.new_decl (floc ()) $1 }
| use_clone
{ Incremental.use_clone (floc ()) $1 }
| namespace_head namespace_import namespace_name list0_decl END
{ Incremental.close_namespace (floc_ij 1 3) $2 $3 }
| namespace_head namespace_import uident list0_decl END
{ Incremental.close_namespace (floc_ij 1 3) $2 $3.id }
;
namespace_head:
......@@ -296,11 +296,6 @@ namespace_import:
| IMPORT { true }
;
namespace_name:
| uident { Some $1.id }
| UNDERSCORE { None }
;
/* Declaration */
decl:
......@@ -340,11 +335,9 @@ use_clone:
use:
| imp_exp tqualid
{ { use_theory = $2; use_as = Some (qualid_last $2); use_imp_exp = $1 } }
{ { use_theory = $2; use_as = qualid_last $2; use_imp_exp = $1 } }
| imp_exp tqualid AS uident
{ { use_theory = $2; use_as = Some $4.id; use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
{ { use_theory = $2; use_as = None; use_imp_exp = $1 } }
{ { use_theory = $2; use_as = $4.id; use_imp_exp = $1 } }
;
imp_exp:
......@@ -1001,11 +994,9 @@ new_pdecl:
use_module:
| imp_exp MODULE tqualid
{ { use_theory = $3; use_as = Some (qualid_last $3); use_imp_exp = $1 } }
{ { use_theory = $3; use_as = qualid_last $3; use_imp_exp = $1 } }
| imp_exp MODULE tqualid AS uident
{ { use_theory = $3; use_as = Some $5.id; use_imp_exp = $1 } }
| imp_exp MODULE tqualid AS UNDERSCORE
{ { use_theory = $3; use_as = None; use_imp_exp = $1 } }
{ { use_theory = $3; use_as = $5.id; use_imp_exp = $1 } }
;
pdecl:
......
......@@ -97,8 +97,7 @@ type plogic_type =
type use = {
use_theory : qualid;
use_as : string option;
(* None = as _, Some id = as id *)
use_as : string;
use_imp_exp : bool option;
(* None = export, Some false = default, Some true = import *)
}
......@@ -269,7 +268,7 @@ type incremental = {
open_module : ident -> unit;
close_module : unit -> unit;
open_namespace : unit -> unit;
close_namespace : loc -> bool (*import:*) -> string option -> unit;
close_namespace : loc -> bool (*import:*) -> string -> unit;
new_decl : loc -> decl -> unit;
new_pdecl : loc -> pdecl -> unit;
use_clone : loc -> use_clone -> unit;
......
......@@ -37,7 +37,7 @@ val add_use_clone :
Loc.position -> Ptree.use_clone -> theory_uc
val close_namespace :
Loc.position -> bool -> string option -> theory_uc -> theory_uc
Loc.position -> bool -> string -> theory_uc -> theory_uc
val close_theory : theory Mstr.t -> theory_uc -> theory Mstr.t
......
......@@ -118,8 +118,8 @@ let close_namespace uc import s =
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
let e1 = match s with Some s -> add_ns true s e0 e1 | _ -> e1 in
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
let ith = Theory.close_namespace uc.uc_impure import s in
let eth = Theory.close_namespace uc.uc_effect import s in
let pth = Theory.close_namespace uc.uc_pure import s in
......
......@@ -57,7 +57,7 @@ val create_module : ?path:string list -> preid -> uc
val close_module : uc -> t
val open_namespace : uc -> uc
val close_namespace : uc -> bool -> string option -> uc
val close_namespace : uc -> bool -> string -> uc
val use_export : uc -> t -> uc
val use_export_theory : uc -> Theory.theory -> uc
......
......@@ -2318,7 +2318,7 @@ type program_decl =
| PDpdecl of Ptree.pdecl
| PDuseclone of Ptree.use_clone
| PDuse of Ptree.use
| PDnamespace of string option * bool * (Ptree.loc * program_decl) list
| PDnamespace of string * bool * (Ptree.loc * program_decl) list
(* env = to retrieve theories and modules from the loadpath
lmod = local modules *)
......
......@@ -27,7 +27,7 @@ type program_decl =
| PDpdecl of Ptree.pdecl
| PDuseclone of Ptree.use_clone
| PDuse of Ptree.use
| PDnamespace of string option * bool * (Ptree.loc * program_decl) list
| PDnamespace of string * bool * (Ptree.loc * program_decl) list
val decl :
wp:bool -> Pgm_module.t Util.Mstr.t Env.library ->
......
......@@ -180,8 +180,8 @@ let close_namespace uc import s =
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
let e1 = match s with Some s -> add_ns true s e0 e1 | _ -> e1 in
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
{ uc with
muc_theory = th;
muc_import = i1 :: sti;
......
......@@ -70,7 +70,7 @@ val create_module : Env.env -> ?path:string list -> preid -> module_uc
val close_module : module_uc -> modul
val open_namespace : module_uc -> module_uc
val close_namespace : module_uc -> bool -> string option -> module_uc
val close_namespace : module_uc -> bool -> string -> module_uc
val get_theory : module_uc -> theory_uc
val get_namespace : module_uc -> namespace
......
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