La notation with dependante + affichage dependante de moduels corrige

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

3 files changed, 75 insertions, 98 deletions

diff --git a/parsing/astmod.ml b/parsing/astmod.ml
index 9c0915a4f7..cbb19fa0bf 100644
--- a/parsing/astmod.ml
+++ b/parsing/astmod.ml
@@ -65,31 +65,13 @@ let lookup_qualid (modtype:bool) qid =
    and the basename. Searches Nametab otherwise.
 *)
 
-let lookup_module binders qid =
-  try
-    let dir,id = repr_qualid qid in
-      (* dirpath in natural order *)
-    let idl = List.rev (id::repr_dirpath dir) in
-    let top_mp = MPbound (fst (List.assoc (List.hd idl) binders)) in
-      make_mp top_mp (List.tl idl)
-  with 
-      Not_found -> Nametab.locate_module qid
+let lookup_module qid =
+  Nametab.locate_module qid
 	
-let lookup_modtype binders qid =
-  try
-    let dir,id = repr_qualid qid in
-      (* dirpath in natural order *)
-    match List.rev (repr_dirpath dir) with
-      | hd::tl ->
-	  let top_mp = MPbound (fst (List.assoc hd binders)) in
-	  let mp = make_mp top_mp tl in
-	    make_kn mp empty_dirpath (label_of_id id)
-      | [] -> raise Not_found 
-	  (* may-be a module, but not a module type!*)
-  with
-      Not_found -> Nametab.locate_modtype qid
+let lookup_modtype qid =
+  Nametab.locate_modtype qid
 
-let transl_with_decl binders = function 
+let transl_with_decl env = function 
   | Node(loc,"WITHMODULE",[id_ast;qid_ast]) ->
       let id = match id_ast with
 	  Nvar(_,id) -> id
@@ -100,22 +82,22 @@ let transl_with_decl binders = function
   	    interp_qualid astl
 	| _ -> anomaly "QUALID expected"
       in
-	With_Module (id,lookup_module binders qid)
+	With_Module (id,lookup_module qid)
   | Node(loc,"WITHDEFINITION",[id_ast;cast]) ->
       let id = match id_ast with
 	  Nvar(_,id) -> id
 	| _ -> anomaly "Identifier AST expected"
       in
-      let c = interp_constr Evd.empty (Global.env()) cast in
+      let c = interp_constr Evd.empty env cast in
 	With_Definition (id,c)
   | _ -> anomaly "Unexpected AST"
 
-let rec transl_modtype binders = function 
+let rec interp_modtype env = function 
   | Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with 
       | [Node (loc, "QUALID", astl)] -> 
   	  let qid = interp_qualid astl in begin
 	      try 
-	        MTEident (lookup_modtype binders qid)
+	        MTEident (lookup_modtype qid)
 	      with
 	        | Not_found -> 
 		    Modops.error_not_a_modtype (*loc*) (string_of_qualid qid)
@@ -123,32 +105,18 @@ let rec transl_modtype binders = function
       | _ -> anomaly "QUALID expected"
     end
   | Node(loc,"MODTYPEWITH",[mty_ast;decl_ast]) ->
-      let mty = transl_modtype binders mty_ast in
-      let decl = transl_with_decl binders decl_ast in
+      let mty = interp_modtype env mty_ast in
+      let decl = transl_with_decl env decl_ast in
 	MTEwith(mty,decl)
   | _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only"
  
 
-let transl_binder binders (idl,mty_ast) =
-  let mte = transl_modtype binders mty_ast in
-  let add_one binders id = 
-    if List.mem_assoc id binders then
-      error "Two identical module binders..."
-    else
-      let mbid = make_mbid (Lib.module_dp()) (string_of_id id) in
-	(id,(mbid,mte))::binders
-  in
-    List.fold_left add_one binders idl 
-
-let transl_binders = List.fold_left transl_binder
-
-
-let rec transl_modexpr binders = function 
+let rec interp_modexpr env = function 
   | Node(loc,"MODEXPRQID",qid_ast) -> begin match qid_ast with 
       | [Node (loc, "QUALID", astl)] -> 
 	  let qid = interp_qualid astl in begin
 	    try 
-	      MEident (lookup_module binders qid)
+	      MEident (lookup_module qid)
 	    with
 	      | Not_found -> 
 		 Modops.error_not_a_module (*loc*) (string_of_qualid qid)
@@ -156,17 +124,10 @@ let rec transl_modexpr binders = function
       | _ -> anomaly "QUALID expected"
     end
   | Node(_,"MODEXPRAPP",[ast1;ast2]) ->
-      let me1 = transl_modexpr binders ast1 in
-      let me2 = transl_modexpr binders ast2 in
+      let me1 = interp_modexpr env ast1 in
+      let me2 = interp_modexpr env ast2 in
 	MEapply(me1,me2)
   | Node(_,"MODEXPRAPP",_) -> 
       anomaly "transl_modexpr: MODEXPRAPP must have two arguments"
   | _ -> anomaly "transl_modexpr: I can handle MODEXPRQID or MODEXPRAPP only..."
 
-
-let interp_module_decl evd env args_ast mty_ast_o mexpr_ast_o = 
-  let binders = transl_binders [] args_ast in
-  let mty_o = option_app (transl_modtype binders) mty_ast_o in
-  let mexpr_o = option_app (transl_modexpr binders) mexpr_ast_o in
-    (List.rev binders, mty_o, mexpr_o)
-
diff --git a/parsing/astmod.mli b/parsing/astmod.mli
index 158f40e890..49e061a0be 100644
--- a/parsing/astmod.mli
+++ b/parsing/astmod.mli
@@ -19,12 +19,7 @@ open Evd
 (* Module expressions and module types are interpreted relatively to 
    eventual functor or funsig arguments. *)
 
-val interp_module_decl : evar_map -> env -> 
-  (identifier list * Coqast.t) list -> 
-  Coqast.t option ->
-  Coqast.t option
-    ->
-      (identifier * (mod_bound_id * module_type_entry)) list * 
-      module_type_entry option *
-      module_expr option
+val interp_modtype : env -> Coqast.t -> module_type_entry
+
+val interp_modexpr : env -> Coqast.t -> module_expr
 
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 075fdb03dc..2b75049b2a 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -13,44 +13,66 @@ open Declarations
 open Nameops
 open Libnames
 
-let print_modpath env mp = 
+let get_new_id locals id = 
+  let rec get_id l id = 
+    let dir = make_dirpath [id] in
+      if not (Nametab.exists_module dir) then
+	id
+      else
+	get_id (id::l) (Nameops.next_ident_away id l)
+  in
+    get_id (List.map snd locals) id
+
+let rec print_local_modpath locals = function
+  | MPbound mbid -> pr_id (List.assoc mbid locals)
+  | MPdot(mp,l) ->
+      print_local_modpath locals mp ++ str "." ++ pr_lab l
+  | MPself _ | MPfile _ -> raise Not_found
+
+let print_modpath locals mp = 
   try (* must be with let because streams are lazy! *)
-    let qid = Nametab.shortest_qualid_of_module mp in pr_qualid qid
+    let qid = Nametab.shortest_qualid_of_module mp in 
+      pr_qualid qid
   with
-    | Not_found as e -> 
-	match mp with 
-	  | MPbound mbid -> Nameops.pr_id (id_of_mbid mbid)
-	  | _ -> raise e
+    | Not_found -> print_local_modpath locals mp
 
-let print_kn env kn = 
-  let qid = Nametab.shortest_qualid_of_modtype kn in 
-    pr_qualid qid
+let print_kn locals kn = 
+  try
+    let qid = Nametab.shortest_qualid_of_modtype kn in 
+      pr_qualid qid
+  with
+      Not_found -> 
+	let (mp,_,l) = repr_kn kn in
+	  print_local_modpath locals mp ++ str"." ++ pr_lab l
 
 let rec flatten_app mexpr l = match mexpr with
   | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
   | mexpr -> mexpr::l
 
-let rec print_module name env with_body mb =
+let rec print_module name locals with_body mb =
   let body = match mb.mod_equiv, with_body, mb.mod_expr with 
     | None, false, _ 
     | None, true, None -> mt()
-    | None, true, Some mexpr -> str " := " ++ print_modexpr env mexpr
-    | Some mp, _, _ -> str " == " ++ print_modpath env mp
+    | None, true, Some mexpr -> 
+	spc () ++ str ":= " ++ print_modexpr locals mexpr
+    | Some mp, _, _ -> str " == " ++ print_modpath locals mp
   in
-  str "Module " ++ name ++ str" : " ++ print_modtype env mb.mod_type ++ body
+  hv 2 (str "Module " ++ name ++ spc () ++ str": " ++ 
+	print_modtype locals mb.mod_type ++ body)
 
-and print_modtype env mty = match mty with
-  | MTBident kn -> print_kn env kn
+and print_modtype locals mty = match mty with
+  | MTBident kn -> print_kn locals kn
   | MTBfunsig (mbid,mtb1,mtb2) ->
-(*      let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
-      in *)
+(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
+      in *) 
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
       hov 2 (str "Funsig" ++ spc () ++ str "(" ++ 
-        pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype env mtb1 ++ 
-      str ")" ++ spc() ++ print_modtype env mtb2)
+        pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype locals mtb1 ++ 
+      str ")" ++ spc() ++ print_modtype locals' mtb2)
   | MTBsig (msid,sign) -> 
-      hv 2 (str "Sig" ++ spc () ++ print_sig env msid sign ++ brk (1,-2) ++ str "End")
+      hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End")
 
-and print_sig env msid sign = 
+and print_sig locals msid sign = 
   let print_spec (l,spec) = (match spec with
     | SPBconst _ -> str "Definition "
     | SPBmind _ -> str "Inductive "
@@ -59,7 +81,7 @@ and print_sig env msid sign =
   in
     prlist_with_sep spc print_spec sign
 
-and print_struct env msid struc = 
+and print_struct locals msid struc = 
   let print_body (l,body) = (match body with
     | SEBconst _ -> str "Definition "
     | SEBmind _ -> str "Inductive "
@@ -68,29 +90,28 @@ and print_struct env msid struc =
   in
     prlist_with_sep spc print_body struc
 
-and print_modexpr env mexpr = match mexpr with 
-  | MEBident mp -> print_modpath env mp
+and print_modexpr locals mexpr = match mexpr with 
+  | MEBident mp -> print_modpath locals mp
   | MEBfunctor (mbid,mty,mexpr) ->
-(*      let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
+(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
       in *)
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
       hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ 
-	     str ":" ++ print_modtype env mty ++ 
-      str "]" ++ spc () ++ print_modexpr env mexpr)
+	     str ":" ++ print_modtype locals mty ++ 
+      str "]" ++ spc () ++ print_modexpr locals' mexpr)
   | MEBstruct (msid, struc) -> 
-      hv 2 (str "Struct" ++ spc () ++ print_struct env msid struc ++ brk (1,-2) ++ str "End")
+      hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
   | MEBapply (mexpr,marg,_) -> 
       let lapp = flatten_app mexpr [marg] in
-	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr env) lapp ++ str")")
+	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
 
 
 
 let print_module with_body mp = 
-  let env = Global.env() in
-  let name = print_modpath env mp in
-    print_module name env with_body (Environ.lookup_module mp env) ++ fnl ()
+  let name = print_modpath [] mp in
+    print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
 
 let print_modtype kn = 
-  let env = Global.env() in
-  let name = print_kn env kn in
-    str "Module Type " ++ name ++ str " = " ++
-    print_modtype env (Environ.lookup_modtype kn env) ++ fnl ()
+  let name = print_kn [] kn in
+    str "Module Type " ++ name ++ str " = " ++ 
+      print_modtype [] (Global.lookup_modtype kn) ++ fnl ()