Encore quelques rangements dans Nametab + petits trucs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 314 insertions, 200 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 4169fa56fe..397104d7b5 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -344,6 +344,7 @@ let classify_modtype (_,(_,substobjs)) =
 let (in_modtype,out_modtype) =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
+      open_function = open_modtype;
       load_function = load_modtype;
       subst_function = subst_modtype;
       classify_function = classify_modtype;
diff --git a/library/nametab.ml b/library/nametab.ml
index 9bd42b388f..c0812c2d2d 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -91,80 +91,79 @@ struct
 
   let empty = Idmap.empty
 		
-  (* [push_many] is used to register [Until vis] visibility and 
-     [push_one] to [Exactly vis] and [push_tree] chooses the right one*)
-
-  let push_many vis tab dir uname o = 
-    let rec push level (current,dirmap) = function
-      | modid :: path as dir ->
-	  let mc = 
-	    try ModIdmap.find modid dirmap
-	    with Not_found -> (Nothing, ModIdmap.empty)
-	  in
-	  let this =
-            if level >= vis then
-	      match current with
-		| Absolute (n,_) -> 
-		    (* This is an absolute name, we must keep it otherwise it may
-		       become unaccessible forever *)
-		    warning ("Trying to mask the absolute name \"" 
-			     ^ U.to_string n ^ "\"!"); 
-		    current
-		| Nothing
-		| Relative _ -> Relative (uname,o)
-            else current 
-	  in
-	    (this, ModIdmap.add modid (push (level+1) mc path) dirmap)
-      | [] -> 
-	  match current with
-	    | Absolute (n,_) -> 
-		(* This is an absolute name, we must keep it otherwise it may
-		   become unaccessible forever *)
-		(* But ours is also absolute! This is an error! *)
-		error ("Trying to mask an absolute name \""
-  		       ^ U.to_string n ^ "\"!")
-	    | Nothing
-	    | Relative _ -> Absolute (uname,o), dirmap
-    in
-      push 0 tab dir
-
-let push_one vis tab dir uname o =
-  let rec push level (current,dirmap) = function
+  (* [push_until] is used to register [Until vis] visibility and 
+     [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
+
+  let rec push_until uname o level (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (Nothing, ModIdmap.empty)
 	in
-          if level = vis then
-	    let this =
-	      match current with
-		| Absolute _ -> 
-	(* This is an absolute name, we must keep it otherwise it may
-           become unaccessible forever *)
-		    error "Trying to mask an absolute name!"
-		| Nothing
-		| Relative _ -> Relative (uname,o)
-	    in
-	      (this, dirmap)
-	  else
-	    (current, ModIdmap.add modid (push (level+1) mc path) dirmap)
-    | [] -> anomaly "We should never come to this point"
-  in
-    push 0 tab dir
-
-
-let push_tree = function 
-  | Until i -> push_many (i-1)
-  | Exactly i -> push_one (i-1)
+	let this =
+          if level <= 0 then
+	    match current with
+	      | Absolute (n,_) -> 
+		  (* This is an absolute name, we must keep it 
+		     otherwise it may become unaccessible forever *)
+		  warning ("Trying to mask the absolute name \"" 
+			   ^ U.to_string n ^ "\"!"); 
+		  current
+	      | Nothing
+	      | Relative _ -> Relative (uname,o)
+          else current 
+	in
+	let ptab' = push_until uname o (level-1) mc path in
+	  (this, ModIdmap.add modid ptab' dirmap)
+    | [] -> 
+	match current with
+	  | Absolute (n,_) -> 
+	      (* This is an absolute name, we must keep it otherwise it may
+		 become unaccessible forever *)
+	      (* But ours is also absolute! This is an error! *)
+	      error ("Cannot mask an absolute name \""
+  		     ^ U.to_string n ^ "\"!")
+	  | Nothing
+	  | Relative _ -> Absolute (uname,o), dirmap
+
+
+let rec push_exactly uname o level (current,dirmap) = function
+  | modid :: path as dir ->
+      let mc = 
+	try ModIdmap.find modid dirmap
+	with Not_found -> (Nothing, ModIdmap.empty)
+      in
+        if level = 0 then
+	  let this =
+	    match current with
+	      | Absolute (n,_) -> 
+		  (* This is an absolute name, we must keep it 
+		     otherwise it may become unaccessible forever *)
+		  warning ("Trying to mask an absolute name \""
+  			   ^ U.to_string n ^ "\"!");
+		  current
+	      | Nothing
+	      | Relative _ -> Relative (uname,o)
+	  in
+	    (this, dirmap)
+	else (* not right level *)
+	  let ptab' = push_exactly uname o (level-1) mc path in
+	    (current, ModIdmap.add modid ptab' dirmap)
+  | [] -> 
+      anomaly "Prefix longer than path! Impossible!"
 
 
 let push visibility uname o tab =
   let id,dir = U.repr uname in
-  let modtab =
+  let ptab =
     try Idmap.find id tab
     with Not_found -> (Nothing, ModIdmap.empty) 
   in
-    Idmap.add id (push_tree visibility modtab dir uname o) tab
+  let ptab' = match visibility with
+    | Until i -> push_until uname o (i-1) ptab dir
+    | Exactly i -> push_exactly uname o (i-1) ptab dir
+  in
+    Idmap.add id ptab' tab
 
 
 let rec search (current,modidtab) = function
diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
index 9773bc6f4e..61966c7c8b 100644
--- a/test-suite/modules/Nametab.v
+++ b/test-suite/modules/Nametab.v
@@ -1,128 +1,48 @@
 Module Q.
-Module N.
-Module K.
-Definition id:=Set.
-End K.
-End N.
+  Module N.
+    Module K.
+      Definition id:=Set.
+    End K.
+  End N.
 End Q.
 
-Locate id.
-Locate K.id.
-Locate N.K.id.
-Locate Q.N.K.id.
-Locate Top.Q.N.K.id.
-Locate K.
-Locate N.K.
-Locate Q.N.K.
-Locate Top.Q.N.K.
-Locate N.
-Locate Q.N.
-Locate Top.Q.N.
-Locate Q.
-Locate Top.Q.
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
 
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
 
-Module Type SIG.
-End SIG.
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
 
-Module Type FSIG[X:SIG].
-End FSIG.
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
 
-Module F[X:SIG].
-End F.
 
-(*
-#trace Nametab.push;;
-#trace Nametab.push_short_name;;
-#trace Nametab.freeze;;
-#trace Nametab.unfreeze;;
-#trace Nametab.exists_cci;;
-*)
 
-Module M.
-Reset M.
-Module M[X:SIG].
-Reset M.
-Module M[X,Y:SIG].
-Reset M.
-Module M[X:SIG;Y:SIG].
-Reset M.
-Module M[X,Y:SIG;Z1,Z:SIG].
-Reset M.
-Module M[X:SIG][Y:SIG].
-Reset M.
-Module M[X,Y:SIG][Z1,Z:SIG].
-Reset M.
-Module M:SIG.
-Reset M.
-Module M[X:SIG]:SIG.
-Reset M.
-Module M[X,Y:SIG]:SIG.
-Reset M.
-Module M[X:SIG;Y:SIG]:SIG.
-Reset M.
-Module M[X,Y:SIG;Z1,Z:SIG]:SIG.
-Reset M.
-Module M[X:SIG][Y:SIG]:SIG.
-Reset M.
-Module M[X,Y:SIG][Z1,Z:SIG]:SIG.
-Reset M.
-Module M:=(F Q).
-Reset M.
-Module M[X:FSIG]:=(X Q).
-Reset M.
-Module M[X,Y:FSIG]:=(X Q).
-Reset M.
-Module M[X:FSIG;Y:SIG]:=(X Y).
-Reset M.
-Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z).
-Reset M.
-Module M[X:FSIG][Y:SIG]:=(X Y).
-Reset M.
-Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z).
-Reset M.
-Module M:SIG:=(F Q).
-Reset M.
-Module M[X:FSIG]:SIG:=(X Q).
-Reset M.
-Module M[X,Y:FSIG]:SIG:=(X Q).
-Reset M.
-Module M[X:FSIG;Y:SIG]:SIG:=(X Y).
-Reset M.
-Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z).
-Reset M.
-Module M[X:FSIG][Y:SIG]:SIG:=(X Y).
-Reset M.
-Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z).
-Reset M.
+Import Q.N.
 
 
-Module Type ELEM.
-  Parameter A:Set.
-  Parameter x:A.
-End ELEM.
+(* Bad *) Locate id.
+(* OK  *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
 
-Module Nat.
-    Definition A:=nat.
-    Definition x:=O.
-End Nat. 
+(* OK  *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
 
-Module List[X:ELEM].
-  Inductive list : Set := nil : list 
-		       | cons : X.A -> list -> list.
- 
-  Definition head := 
-     [l:list]Cases l of 
-	  nil => X.x 
-	| (cons x _) => x
-     end.
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
 
-  Definition singl := [x:X.A] (cons x nil).
-  
-  Lemma head_singl : (x:X.A)(head (singl x))=x.
-  Auto.
-  Qed.
-
-End List.
-
-Module N:=(List Nat).
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
new file mode 100644
index 0000000000..13c2841812
--- /dev/null
+++ b/test-suite/modules/Tescik.v
@@ -0,0 +1,30 @@
+
+Module Type ELEM.
+  Parameter A:Set.
+  Parameter x:A.
+End ELEM.
+
+Module Nat.
+    Definition A:=nat.
+    Definition x:=O.
+End Nat. 
+
+Module List[X:ELEM].
+  Inductive list : Set := nil : list 
+		       | cons : X.A -> list -> list.
+ 
+  Definition head := 
+     [l:list]Cases l of 
+	  nil => X.x 
+	| (cons x _) => x
+     end.
+
+  Definition singl := [x:X.A] (cons x nil).
+  
+  Lemma head_singl : (x:X.A)(head (singl x))=x.
+  Auto.
+  Qed.
+
+End List.
+
+Module N:=(List Nat).
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
new file mode 100644
index 0000000000..505821d7eb
--- /dev/null
+++ b/test-suite/output/Nametab.out
@@ -0,0 +1,28 @@
+id is not a defined object
+K.id is not a defined object
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+K is not a defined object
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
+id is not a defined object
+Constant Top.Q.N.K.id
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+Module Top.Q.N.K
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v
new file mode 100644
index 0000000000..61966c7c8b
--- /dev/null
+++ b/test-suite/output/Nametab.v
@@ -0,0 +1,48 @@
+Module Q.
+  Module N.
+    Module K.
+      Definition id:=Set.
+    End K.
+  End N.
+End Q.
+
+(* Bad *) Locate id.
+(* Bad *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
+
+(* Bad *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
+
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
+
+
+
+Import Q.N.
+
+
+(* Bad *) Locate id.
+(* OK  *) Locate K.id.
+(* Bad *) Locate N.K.id.
+(* OK  *) Locate Q.N.K.id.
+(* OK  *) Locate Top.Q.N.K.id.
+
+(* OK  *) Locate K.
+(* Bad *) Locate N.K.
+(* OK  *) Locate Q.N.K.
+(* OK  *) Locate Top.Q.N.K.
+
+(* Bad *) Locate N.
+(* OK  *) Locate Q.N.
+(* OK  *) Locate Top.Q.N.
+
+(* OK  *) Locate Q.
+(* OK  *) Locate Top.Q.
diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v
new file mode 100644
index 0000000000..098de3cfbf
--- /dev/null
+++ b/test-suite/success/Mod_params.v
@@ -0,0 +1,78 @@
+(* Syntax test - all possible kinds of module parameters *)
+
+Module Type SIG.
+End SIG.
+
+Module Type FSIG[X:SIG].
+End FSIG.
+
+Module F[X:SIG].
+End F.
+
+Module Q.
+End Q.
+
+(*
+#trace Nametab.push;;
+#trace Nametab.push_short_name;;
+#trace Nametab.freeze;;
+#trace Nametab.unfreeze;;
+#trace Nametab.exists_cci;;
+*)
+
+Module M.
+Reset M.
+Module M[X:SIG].
+Reset M.
+Module M[X,Y:SIG].
+Reset M.
+Module M[X:SIG;Y:SIG].
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG].
+Reset M.
+Module M[X:SIG][Y:SIG].
+Reset M.
+Module M[X,Y:SIG][Z1,Z:SIG].
+Reset M.
+Module M:SIG.
+Reset M.
+Module M[X:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG]:SIG.
+Reset M.
+Module M[X:SIG;Y:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG;Z1,Z:SIG]:SIG.
+Reset M.
+Module M[X:SIG][Y:SIG]:SIG.
+Reset M.
+Module M[X,Y:SIG][Z1,Z:SIG]:SIG.
+Reset M.
+Module M:=(F Q).
+Reset M.
+Module M[X:FSIG]:=(X Q).
+Reset M.
+Module M[X,Y:FSIG]:=(X Q).
+Reset M.
+Module M[X:FSIG;Y:SIG]:=(X Y).
+Reset M.
+Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z).
+Reset M.
+Module M[X:FSIG][Y:SIG]:=(X Y).
+Reset M.
+Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z).
+Reset M.
+Module M:SIG:=(F Q).
+Reset M.
+Module M[X:FSIG]:SIG:=(X Q).
+Reset M.
+Module M[X,Y:FSIG]:SIG:=(X Q).
+Reset M.
+Module M[X:FSIG;Y:SIG]:SIG:=(X Y).
+Reset M.
+Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z).
+Reset M.
+Module M[X:FSIG][Y:SIG]:SIG:=(X Y).
+Reset M.
+Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z).
+Reset M.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb6c930c16..d7a4307b22 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -211,30 +211,40 @@ let locate_file f =
 		  str"on loadpath"))
 
 let print_located_qualid (_,qid) =
-  try
-    let sp = Nametab.sp_of_global None (Nametab.locate qid) in
-    msgnl (pr_sp sp)
-  with Not_found -> 
-  try
-    let kn = Nametab.locate_syntactic_definition qid in
-    let sp = Nametab.sp_of_syntactic_definition kn in
-    msgnl (pr_sp sp)
-  with Not_found ->
-  try
-    let dir = match Nametab.locate_dir qid with
-      | DirOpenModule (dir,_)
-      | DirOpenModtype (dir,_)
-      | DirOpenSection (dir,_)
-      | DirModule (dir,_)
-      | DirClosedSection dir -> dir
-    in
-    msgnl (pr_dirpath dir)
-  with Not_found ->
-  try
-    let sp = Nametab.full_name_modtype qid in
-    msgnl (pr_sp sp)
-  with Not_found ->
-    msgnl (pr_qualid qid ++ str " is not a defined object")
+  let msg = 
+    try
+      let ref = Nametab.locate qid in
+      let ref_str = match ref with
+	  ConstRef _ -> "Constant"
+	| IndRef _ -> "Inductive"
+	| ConstructRef _ -> "Constructor"
+	| VarRef _ -> "Variable"
+      in
+      let sp = Nametab.sp_of_global None ref in
+	str ref_str ++ spc () ++ pr_sp sp
+    with Not_found -> 
+      try
+	let kn = Nametab.locate_syntactic_definition qid in
+	let sp = Nametab.sp_of_syntactic_definition kn in
+	  str "Syntactic Definition" ++ spc () ++ pr_sp sp
+      with Not_found ->
+	try
+	  let s,dir = match Nametab.locate_dir qid with
+	    | DirOpenModule (dir,_) -> "Open Module", dir
+	    | DirOpenModtype (dir,_) -> "Open Module Type", dir
+	    | DirOpenSection (dir,_) -> "Open Section", dir
+	    | DirModule (dir,_) -> "Module", dir
+	    | DirClosedSection dir -> "Closed Section", dir
+	  in
+	    str s ++ spc () ++ pr_dirpath dir
+	with Not_found ->
+	  try
+	    let sp = Nametab.full_name_modtype qid in
+	      str "Module Type" ++ spc () ++ pr_sp sp
+	  with Not_found ->
+	    pr_qualid qid ++ str " is not a defined object"
+  in
+    msgnl (hov 0 msg)
 
 (*let print_path_entry (s,l) =
   (str s ++ tbrk (0,2) ++ str (string_of_dirpath l))