Commit a810c7c4 authored by Andrei Paskevich's avatar Andrei Paskevich

store the current qualifier prefix in theory_uc/module_uc

parent 0970675c
......@@ -578,9 +578,9 @@ let typedecl denv env impl loc s (tvl,(el,e)) =
let flush_impl ~strict env uc impl =
let update_th _ e uc = match e with
| Suse th ->
let uc = open_namespace uc in
let uc = open_namespace uc th.th_name.id_string in
let uc = use_export uc th in
close_namespace uc false th.th_name.id_string
close_namespace uc false
| _ -> uc
in
let update s e (env,uc) = match e with
......
......@@ -261,6 +261,7 @@ type theory_uc = {
uc_name : ident;
uc_path : string list;
uc_decls : tdecl list;
uc_prefix : string list;
uc_import : namespace list;
uc_export : namespace list;
uc_known : known_map;
......@@ -275,6 +276,7 @@ let empty_theory n p = {
uc_name = id_register n;
uc_path = p;
uc_decls = [];
uc_prefix = [];
uc_import = [empty_ns];
uc_export = [empty_ns];
uc_known = Mid.empty;
......@@ -294,25 +296,27 @@ 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 = match uc.uc_import with
let open_namespace uc s = match uc.uc_import with
| ns :: _ -> { uc with
uc_prefix = s :: uc.uc_prefix;
uc_import = ns :: uc.uc_import;
uc_export = empty_ns :: uc.uc_export; }
| [] -> assert false
let close_namespace uc import s =
match uc.uc_import, uc.uc_export with
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let close_namespace uc import =
match uc.uc_prefix, uc.uc_import, uc.uc_export with
| s :: prf, _ :: 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 = 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
{ uc with uc_prefix = prf; uc_import = i1::sti; uc_export = e1::ste; }
| [], [_], [_] -> raise NoOpenedNamespace
| _ -> assert false
(* Base constructors *)
......@@ -843,4 +847,3 @@ let () = Exn_printer.register
m.meta_name print_meta_arg_type t1 print_meta_arg_type t2
| _ -> raise exn
end
......@@ -129,11 +129,11 @@ type theory_uc (* a theory under construction *)
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 -> theory_uc
(* the Boolean indicates [import]; the string indicates [as T] *)
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
......
......@@ -27,8 +27,8 @@ module Incremental = struct
let close_theory () = (Stack.top stack).Ptree.close_theory ()
let open_module id = (Stack.top stack).Ptree.open_module id
let close_module () = (Stack.top stack).Ptree.close_module ()
let open_namespace () = (Stack.top stack).Ptree.open_namespace ()
let close_namespace l b n = (Stack.top stack).Ptree.close_namespace l b n
let open_namespace n = (Stack.top stack).Ptree.open_namespace n
let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
......@@ -283,12 +283,13 @@ new_decl:
{ Incremental.new_decl (floc ()) $1 }
| use_clone
{ Incremental.use_clone (floc ()) $1 }
| namespace_head namespace_import uident list0_decl END
{ Incremental.close_namespace (floc_ij 1 3) $2 $3.id }
| namespace_head list0_decl END
{ Incremental.close_namespace (floc_i 1) $1 }
;
namespace_head:
| NAMESPACE { Incremental.open_namespace () }
| NAMESPACE namespace_import uident
{ Incremental.open_namespace $3.id; $2 }
;
namespace_import:
......
......@@ -267,8 +267,8 @@ type incremental = {
close_theory : unit -> unit;
open_module : ident -> unit;
close_module : unit -> unit;
open_namespace : unit -> unit;
close_namespace : loc -> bool (*import:*) -> string -> unit;
open_namespace : string -> unit;
close_namespace : loc -> bool (*import:*) -> unit;
new_decl : loc -> decl -> unit;
new_pdecl : loc -> pdecl -> unit;
use_clone : loc -> use_clone -> unit;
......
......@@ -1184,9 +1184,9 @@ let add_use_clone env lenv th loc (use, subst) =
let use_or_clone th = match use.use_imp_exp with
| Some imp ->
(* use T = namespace T use_export T end *)
let th = open_namespace th in
let th = open_namespace th use.use_as in
let th = use_or_clone th in
close_namespace th imp use.use_as
close_namespace th imp
| None ->
use_or_clone th
in
......@@ -1200,8 +1200,8 @@ let close_theory lenv th =
if Mstr.mem id lenv then error ?loc (ClashTheory id);
Mstr.add id th lenv
let close_namespace loc import id th =
Loc.try3 loc close_namespace th import id
let close_namespace loc import th =
Loc.try2 loc close_namespace th import
(* incremental parsing *)
......@@ -1214,10 +1214,10 @@ let open_file, close_file =
Stack.push (Theory.create_theory ~path (Denv.create_user_id id)) uc in
let close_theory () =
Stack.push (close_theory (Stack.pop lenv) (Stack.pop uc)) lenv in
let open_namespace () =
Stack.push (Theory.open_namespace (Stack.pop uc)) uc in
let close_namespace loc imp name =
Stack.push (close_namespace loc imp name (Stack.pop uc)) uc in
let open_namespace name =
Stack.push (Theory.open_namespace (Stack.pop uc) name) uc in
let close_namespace loc imp =
Stack.push (close_namespace loc imp (Stack.pop uc)) uc in
let new_decl loc d =
Stack.push (add_decl loc (Stack.pop uc) d) uc in
let use_clone loc use =
......
......@@ -37,7 +37,7 @@ val add_use_clone :
Loc.position -> Ptree.use_clone -> theory_uc
val close_namespace :
Loc.position -> bool -> string -> theory_uc -> theory_uc
Loc.position -> bool -> theory_uc -> theory_uc
val close_theory : theory Mstr.t -> theory_uc -> theory Mstr.t
......
......@@ -62,9 +62,9 @@ let add_theory env path lenv m =
| Pgm_typing.PDuseclone d ->
Typing.add_use_clone env lenv th loc d
| Pgm_typing.PDnamespace (name, import, dl) ->
let th = Theory.open_namespace th in
let th = Theory.open_namespace th name in
let th = List.fold_left add_decl th dl in
Typing.close_namespace loc import name th
Typing.close_namespace loc import th
| Pgm_typing.PDpdecl _ | Pgm_typing.PDuse _ -> assert false
in
let th = List.fold_left add_decl th m.pth_decl in
......@@ -94,6 +94,7 @@ open Pgm_typing
let open_file, close_file =
let ids = Stack.create () in
let muc = Stack.create () in
let prf = Stack.create () in
let lenv = Stack.create () in
let open_file () =
Stack.push [] lenv;
......@@ -107,8 +108,10 @@ let open_file, close_file =
let mast = { mod_name = Stack.pop ids;
mod_decl = List.rev (Stack.pop muc) } in
Stack.push (Pmodule mast :: Stack.pop lenv) lenv in
let open_namespace () = Stack.push [] muc in
let close_namespace loc imp name =
let open_namespace s =
Stack.push s prf; Stack.push [] muc in
let close_namespace loc imp =
let name = Stack.pop prf in
let decl = List.rev (Stack.pop muc) in
Stack.push ((loc, PDnamespace (name,imp,decl)) :: Stack.pop muc) muc in
let new_decl loc d =
......
......@@ -85,6 +85,7 @@ type uc = {
uc_effect : theory_uc; (* the theory used for typing effects *)
uc_pure : theory_uc; (* the logic theory used to type annotations *)
uc_decls : decl list; (* the program declarations *)
uc_prefix : string list;
uc_import : namespace list;
uc_export : namespace list;
}
......@@ -102,30 +103,32 @@ let add_pervasives uc =
in
add_ty_decl uc ts
let open_namespace uc = match uc.uc_import with
let open_namespace uc s = match uc.uc_import with
| ns :: _ -> { uc with
uc_impure = Theory.open_namespace uc.uc_impure;
uc_effect = Theory.open_namespace uc.uc_effect;
uc_pure = Theory.open_namespace uc.uc_pure;
uc_impure = Theory.open_namespace uc.uc_impure s;
uc_effect = Theory.open_namespace uc.uc_effect s;
uc_pure = Theory.open_namespace uc.uc_pure s;
uc_prefix = s :: uc.uc_prefix;
uc_import = ns :: uc.uc_import;
uc_export = empty_ns :: uc.uc_export; }
| [] -> assert false
exception NoOpenedNamespace
let close_namespace uc import s =
match uc.uc_import, uc.uc_export with
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let close_namespace uc import =
match uc.uc_prefix, uc.uc_import, uc.uc_export with
| s :: prf, _ :: 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 = 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
let ith = Theory.close_namespace uc.uc_impure import in
let eth = Theory.close_namespace uc.uc_effect import in
let pth = Theory.close_namespace uc.uc_pure import in
{ uc with uc_impure = ith; uc_effect = eth; uc_pure = pth;
uc_import = i1 :: sti; uc_export = e1 :: ste; }
| [_], [_] -> raise NoOpenedNamespace
uc_import = i1 :: sti; uc_export = e1 :: ste;
uc_prefix = prf; }
| [], [_], [_] -> raise NoOpenedNamespace
| _ -> assert false
(** Insertion of new declarations *)
......@@ -201,6 +204,7 @@ let empty_module path n =
uc_effect = Theory.create_theory ~path n;
uc_pure = Theory.create_theory ~path n;
uc_decls = [];
uc_prefix = [];
uc_import = [empty_ns];
uc_export = [empty_ns]; }
in
......
......@@ -56,8 +56,8 @@ type t = private {
val create_module : ?path:string list -> preid -> uc
val close_module : uc -> t
val open_namespace : uc -> uc
val close_namespace : uc -> bool -> string -> uc
val open_namespace : uc -> string -> uc
val close_namespace : uc -> bool -> uc
val use_export : uc -> t -> uc
val use_export_theory : uc -> Theory.theory -> uc
......
......@@ -2408,18 +2408,18 @@ let rec decl ~wp env ltm lmod uc (loc,dcl) = match dcl with
begin try match imp_exp with
| Some imp ->
(* use T = namespace T use_export T end *)
let uc = open_namespace uc in
let uc = open_namespace uc use_as in
let uc = use_export uc m in
close_namespace uc imp use_as
close_namespace uc imp
| None ->
use_export uc m
with ClashSymbol s ->
errorm ~loc "clash with previous symbol %s" s
end
| PDnamespace (id, import, dl) ->
let uc = open_namespace uc in
let uc = open_namespace uc id in
let uc = List.fold_left (decl ~wp env ltm lmod) uc dl in
begin try close_namespace uc import id
begin try close_namespace uc import
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
| PDdecl (Ptree.TypeDecl d) ->
add_types loc uc d
......
......@@ -135,6 +135,7 @@ type modul = {
type module_uc = {
muc_theory : theory_uc;
muc_decls : pdecl list;
muc_prefix : string list;
muc_import : namespace list;
muc_export : namespace list;
muc_known : known_map;
......@@ -146,6 +147,7 @@ type module_uc = {
let empty_module env n p = {
muc_theory = create_theory ~path:p n;
muc_decls = [];
muc_prefix = [];
muc_import = [empty_ns];
muc_export = [empty_ns];
muc_known = Mid.empty;
......@@ -165,25 +167,28 @@ 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 = match uc.muc_import with
let open_namespace uc s = match uc.muc_import with
| ns :: _ -> { uc with
muc_theory = Theory.open_namespace uc.muc_theory;
muc_theory = Theory.open_namespace uc.muc_theory s;
muc_prefix = s :: uc.muc_prefix;
muc_import = ns :: uc.muc_import;
muc_export = empty_ns :: uc.muc_export; }
| [] -> assert false
let close_namespace uc import s =
let th = Theory.close_namespace uc.muc_theory import s in (* catches errors *)
match uc.muc_import, uc.muc_export with
| _ :: i1 :: sti, e0 :: e1 :: ste ->
let close_namespace uc import =
let th = Theory.close_namespace uc.muc_theory import in (* catches errors *)
match uc.muc_prefix, uc.muc_import, uc.muc_export with
| s :: prf, _ :: 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 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
{ uc with
muc_theory = th;
muc_prefix = prf;
muc_import = i1 :: sti;
muc_export = e1 :: ste; }
| _ ->
......
......@@ -69,11 +69,12 @@ type module_uc (* a module under construction *)
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 -> module_uc
val open_namespace : module_uc -> string -> module_uc
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
(** Use and clone *)
......
......@@ -1642,7 +1642,8 @@ let use_clone_pure lib mth uc loc (use,inst) =
let path, s = Typing.split_qualid use.use_theory in
let th = find_theory loc lib mth path s in
(* open namespace, if any *)
let uc = if use.use_imp_exp <> None then Theory.open_namespace uc else uc in
let uc = if use.use_imp_exp = None then uc
else Theory.open_namespace uc use.use_as in
(* use or clone *)
let uc = match inst with
| None -> Theory.use_export uc th
......@@ -1650,7 +1651,7 @@ let use_clone_pure lib mth uc loc (use,inst) =
(* close namespace, if any *)
match use.use_imp_exp with
| None -> uc
| Some imp -> Theory.close_namespace uc imp use.use_as
| Some imp -> Theory.close_namespace uc imp
let use_clone_pure lib mth uc loc use =
if Debug.test_flag Typing.debug_parse_only then uc else
......@@ -1661,7 +1662,8 @@ let use_clone lib mmd mth uc loc (use,inst) =
let path, s = Typing.split_qualid use.use_theory in
let mth = find_module loc lib mmd mth path s in
(* open namespace, if any *)
let uc = if use.use_imp_exp <> None then open_namespace uc else uc in
let uc = if use.use_imp_exp = None then uc
else open_namespace uc use.use_as in
(* use or clone *)
let uc = match mth, inst with
| Module m, None -> use_export uc m
......@@ -1673,7 +1675,7 @@ let use_clone lib mmd mth uc loc (use,inst) =
(* close namespace, if any *)
match use.use_imp_exp with
| None -> uc
| Some imp -> close_namespace uc imp use.use_as
| Some imp -> close_namespace uc imp
let use_clone lib mmd mth uc loc use =
if Debug.test_flag Typing.debug_parse_only then uc else
......@@ -1684,7 +1686,8 @@ let use_module lib mmd mth uc loc use =
let path, s = Typing.split_qualid use.use_theory in
let mth = find_module loc lib mmd mth path s in
(* open namespace, if any *)
let uc = if use.use_imp_exp <> None then open_namespace uc else uc in
let uc = if use.use_imp_exp = None then uc
else open_namespace uc use.use_as in
(* use or clone *)
let uc = match mth with
| Theory _ ->
......@@ -1693,7 +1696,7 @@ let use_module lib mmd mth uc loc use =
(* close namespace, if any *)
match use.use_imp_exp with
| None -> uc
| Some imp -> close_namespace uc imp use.use_as
| Some imp -> close_namespace uc imp
let use_module lib mmd mth uc loc use =
if Debug.test_flag Typing.debug_parse_only then uc else
......@@ -1734,12 +1737,12 @@ let open_file, close_file =
Stack.push (close_theory (Stack.pop lenv) (Stack.pop tuc)) lenv in
let close_module () = ignore (Stack.pop inm);
Stack.push (close_module (Stack.pop lenv) (Stack.pop muc)) lenv in
let open_namespace () = if Stack.top inm
then Stack.push (Mlw_module.open_namespace (Stack.pop muc)) muc
else Stack.push (Theory.open_namespace (Stack.pop tuc)) tuc in
let close_namespace imp name = if Stack.top inm
then Stack.push (Mlw_module.close_namespace (Stack.pop muc) imp name) muc
else Stack.push (Theory.close_namespace (Stack.pop tuc) imp name) tuc in
let open_namespace name = if Stack.top inm
then Stack.push (Mlw_module.open_namespace (Stack.pop muc) name) muc
else Stack.push (Theory.open_namespace (Stack.pop tuc) name) tuc in
let close_namespace imp = if Stack.top inm
then Stack.push (Mlw_module.close_namespace (Stack.pop muc) imp) muc
else Stack.push (Theory.close_namespace (Stack.pop tuc) imp) tuc in
let new_decl loc d = if Stack.top inm
then Stack.push (add_decl ~wp loc (Stack.pop muc) d) muc
else Stack.push (Typing.add_decl loc (Stack.pop tuc) d) tuc in
......@@ -1755,7 +1758,7 @@ let open_file, close_file =
open_module = open_module;
close_module = close_module;
open_namespace = open_namespace;
close_namespace = (fun loc -> Loc.try2 loc close_namespace);
close_namespace = (fun loc -> Loc.try1 loc close_namespace);
new_decl = new_decl;
new_pdecl = new_pdecl;
use_clone = use_clone;
......
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