anonymous namespaces + "namespace import"

src/core/theory.ml

@@ -798,13 +798,13 @@ module Theory = struct
     | [] ->
         assert false
 
-  let close_namespace uc s ~import =
+  let close_namespace uc import s =
     match uc.uc_import, uc.uc_export with
     | _ :: 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 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
         { uc with uc_import = i1 :: sti; uc_export = e1 :: ste; }
     | [_], [_] ->
         raise NoOpenedNamespace

src/core/theory.mli

@@ -184,7 +184,7 @@ module Theory : sig
   val add_decl : theory_uc -> decl -> theory_uc
 
   val open_namespace  : theory_uc -> theory_uc
-  val close_namespace : theory_uc -> string -> import:bool -> theory_uc
+  val close_namespace : theory_uc -> bool -> string option -> theory_uc
 
   val use_export   : theory_uc -> theory -> theory_uc
   val clone_export : theory_uc -> theory -> th_inst -> theory_uc

src/parser/parser.mly

@@ -311,15 +311,30 @@ list1_inductive_decl:
 ;
 
 decl:
-| list1_type_decl                 { TypeDecl $1 }
-| list1_logic_decl                { LogicDecl $1 }
-| list1_inductive_decl            { IndDecl $1 }
-| AXIOM uident COLON lexpr        { PropDecl (loc (), Kaxiom, $2, $4) }
-| LEMMA uident COLON lexpr        { PropDecl (loc (), Klemma, $2, $4) }
-| GOAL uident COLON lexpr         { PropDecl (loc (), Kgoal, $2, $4) }
-| USE use                         { UseClone (loc (), $2, None) }
-| CLONE use clone_subst           { UseClone (loc (), $2, Some $3) }
-| NAMESPACE uident list0_decl END { Namespace (loc (), $2, $3) }
+| list1_type_decl
+    { TypeDecl $1 }
+| list1_logic_decl
+    { LogicDecl $1 }
+| list1_inductive_decl
+    { IndDecl $1 }
+| AXIOM uident COLON lexpr
+    { PropDecl (loc (), Kaxiom, $2, $4) }
+| LEMMA uident COLON lexpr
+    { PropDecl (loc (), Klemma, $2, $4) }
+| GOAL uident COLON lexpr
+    { PropDecl (loc (), Kgoal, $2, $4) }
+| USE use
+    { UseClone (loc (), $2, None) }
+| CLONE use clone_subst
+    { UseClone (loc (), $2, Some $3) }
+| NAMESPACE uident list0_decl END
+    { Namespace (loc (), false, Some $2, $3) }
+| NAMESPACE UNDERSCORE list0_decl END
+    { Namespace (loc (), false, None, $3) }
+| NAMESPACE IMPORT uident list0_decl END
+    { Namespace (loc (), false, Some $3, $4) }
+| NAMESPACE IMPORT UNDERSCORE list0_decl END
+    { Namespace (loc (), false, None, $4) }
 ;
 
 list1_theory:
@@ -524,7 +539,9 @@ use:
 | imp_exp tqualid              
     { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
 | imp_exp tqualid AS uident
-    { { use_theory = $2; use_as = Some $4; use_imp_exp = $1 } }
+    { { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
+| imp_exp tqualid AS UNDERSCORE
+    { { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
 ;
 
 imp_exp:

src/parser/ptree.mli

@@ -87,7 +87,7 @@ type imp_exp =
 
 type use = {
   use_theory  : qualid;
-  use_as      : ident option;
+  use_as      : ident option option;
   use_imp_exp : imp_exp;
 }
 
@@ -135,7 +135,7 @@ type decl =
   | IndDecl of ind_decl list
   | PropDecl of loc * prop_kind * ident * lexpr
   | UseClone of loc * use * clone_subst list option
-  | Namespace of loc * ident * decl list
+  | Namespace of loc * bool * ident option * decl list
 
 type theory = {
   pt_loc  : loc;

src/parser/typing.ml

@@ -1153,31 +1153,38 @@ and add_decl env th = function
 	    clone_export th t s
       in
       let n = match use.use_as with 
-	| None -> t.th_name.id_short
-	| Some x -> x.id
+	| None -> Some t.th_name.id_short
+	| Some (Some x) -> Some x.id
+	| Some None -> None
       in
       begin try match use.use_imp_exp with
 	| Nothing ->
 	    (* use T = namespace T use_export T end *)
 	    let th = open_namespace th in
 	    let th = use_or_clone th in
-	    close_namespace th n ~import:false
+	    close_namespace th false n
 	| Import ->
 	    (* use import T = namespace T use_export T end import T *)
 	    let th = open_namespace th in
 	    let th = use_or_clone th in
-	    close_namespace th n ~import:true
+	    close_namespace th true n
 	| Export ->
 	    use_or_clone th 
       with Theory.ClashSymbol s ->
 	error ~loc (Clash s)
       end
-  | Namespace (_, {id=id; id_loc=loc}, dl) ->
+  | Namespace (_, import, name, dl) ->
       let ns = get_namespace th in
-      if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
+      let id = match name with
+        | Some { id=id; id_loc=loc } ->
+            if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
+            Some id
+        | None ->
+            None
+      in
       let th = open_namespace th in
       let th = add_decls env th dl in
-      close_namespace th id ~import:false
+      close_namespace th import id
 
 and add_theory env pt =
   let id = pt.pt_name in