Réparation bug d'affichage et affichage des instanciations par des {...}

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

5 files changed, 62 insertions, 31 deletions

diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index c5be89d926..ef9b4feecc 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -17,13 +17,20 @@ open Extend
 
 type key =
   | Cst of string list (* keys for global constants rules *)
+  | Ind of string list * int 
+  | Cstr of (string list * int) * int
   | Nod of string      (* keys for other constructed asts rules *)
   | Oth                (* key for other syntax rules *)
   | All     (* key for catch-all rules (i.e. with a pattern such as $x .. *)
 
 let ast_keys = function
-  | Node(_,"APPLIST",(Node(_,"CONST",(Path (_,sl,_))::_))::_) ->
+  | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl,_)]) ::_) ->
       [Cst sl; Nod "APPLIST"; All]
+  | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl,_); Num (_,tyi)]) ::_) ->
+      [Ind (sl,tyi); Nod "APPLIST"; All]
+  | Node(_,"APPLIST", Node(_,"MUTCONSTRUCT",
+			   [Path (_,sl,_); Num (_,tyi); Num (_,i)]) ::_) ->
+      [Cstr ((sl,tyi),i); Nod "APPLIST"; All]
   | Node(_,s,_) -> [Nod s; All]
   | _ -> [Oth; All]
 
@@ -31,8 +38,19 @@ let spat_key astp =
   match astp with
     | Pnode("APPLIST",
             Pcons(Pnode("CONST",
-                        Pcons(Pquote(Path (_,sl,s)),_)),
-                  _)) -> Cst sl
+                        Pcons(Pquote(Path (_,sl,s)),_)), _))
+      -> Cst sl
+    | Pnode("APPLIST",
+            Pcons(Pnode("MUTIND",
+                        Pcons(Pquote(Path (_,sl,s)),
+			      Pcons(Pquote(Num (_,tyi)),_))), _))
+      -> Ind (sl,tyi)
+    | Pnode("APPLIST",
+            Pcons(Pnode("MUTCONSTRUCT",
+                        Pcons(Pquote(Path (_,sl,s)),
+			      Pcons(Pquote(Num (_,tyi)),
+				    Pcons(Pquote(Num (_,i)),_)))), _))
+      -> Cstr ((sl,tyi),i)
     | Pnode(na,_) -> Nod na
     | Pquote ast -> List.hd (ast_keys ast)
     | Pmeta _ -> All
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 5fa57bd39e..bad9c38667 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -16,23 +16,37 @@ let emacs_str s = if !Options.print_emacs then s else ""
 
 let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >];;
 
-(*
 let section_path sl s =
   let sl = List.rev sl in
   make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)
 
+(*
 let pr_global k oper =
   let id = id_of_global oper in
   [< 'sTR (string_of_id id) >]
 *)
 
+let pr_qualified_path sp id =
+  if Nametab.sp_of_id (kind_of_path sp) id = sp then [<'sTR(string_of_id id)>]
+  else [<'sTR(string_of_path (make_path (dirpath sp) id (kind_of_path sp)))>]
+
 let globpr gt = match gt with
   | Nvar(_,s) -> [< 'sTR s >]
+  | Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
+  | Node(_,"CONST",[Path(_,sl,s)]) ->
+      let sp = section_path sl s in
+      pr_qualified_path sp (basename (section_path sl s))
+  | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
+      let sp = section_path sl s in
+      pr_qualified_path sp (Global.id_of_global (MutInd (sp,tyi)))
+  | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
+      let sp = section_path sl s in
+      pr_qualified_path sp (Global.id_of_global (MutConstruct ((sp,tyi),i)))
 (*
   | Node(_,"EVAR", (Num (_,ev))::_) ->
       if !print_arguments then dfltpr gt
       else pr_existential (ev,[])
-  | Node(_,"CONST",(Path(_,sl,s))::_) ->
+  | Node(_,"CONST"),(Path(_,sl,s))::_) ->
       if !print_arguments then dfltpr gt
       else pr_constant (section_path sl s,[])
   | Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index f92f9cef42..f4b7071932 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -24,6 +24,9 @@ open Pattern
 (* This governs printing of local context of references *)
 let print_arguments = ref false
 
+(* If true, prints local context of evars, whatever print_arguments *)
+let print_evar_arguments = ref false
+
 (* This forces printing of cast nodes *)
 let print_casts = ref false
 
@@ -83,44 +86,32 @@ let stringopt_of_name = function
   | Name id -> Some (string_of_id id)
   | Anonymous -> None
 
-let ast_of_qualified sp id =
-  if Nametab.sp_of_id (kind_of_path sp) id = sp then nvar (string_of_id id)
-  else nvar (string_of_path sp)
-
 let ast_of_constant_ref (sp,ids) =
-  if !print_arguments then
-    ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident ids))
-  else
-    try ast_of_qualified sp (basename sp)
-    with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
+  let a = ope("CONST", [path_section dummy_loc sp]) in
+  if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids))
+  else a
 
 let ast_of_constant (ev,ids) = ast_of_constant_ref (ev,ids_of_ctxt ids)
 
 let ast_of_existential_ref (ev,ids) =
-  if !print_arguments then
-      ope("EVAR", (num ev)::(List.map ast_of_ident ids))
-  else nvar ("?" ^ string_of_int ev)
+  let a = ope("EVAR", [num ev]) in
+  if !print_arguments or !print_evar_arguments then
+    ope("INSTANCE",a::(List.map ast_of_ident ids))
+  else a
 
 let ast_of_existential (ev,ids) = ast_of_existential_ref (ev,ids_of_ctxt ids)
 
 let ast_of_constructor_ref (((sp,tyi),n) as cstr_sp,ids) =
-  if !print_arguments then
-    ope("MUTCONSTRUCT",
-	(path_section dummy_loc sp)::(num tyi)::(num n)
-	::(List.map ast_of_ident ids))
-  else 
-    try ast_of_qualified sp (Global.id_of_global (MutConstruct cstr_sp))
-    with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
+  let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in
+  if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids))
+  else a
 
 let ast_of_constructor (ev,ids) = ast_of_constructor_ref (ev,ids_of_ctxt ids)
 
 let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) =
-  if !print_arguments then
-    ope("MUTIND",
-	(path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids))
-  else
-    try ast_of_qualified sp (Global.id_of_global (MutInd ind_sp))
-    with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
+  let a = ope("MUTIND",	[path_section dummy_loc sp; num tyi]) in
+  if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids))
+  else a
 
 let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt)
 
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 064dc8c25b..e0b8069d93 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -34,6 +34,7 @@ val ast_of_inductive    : inductive -> Coqast.t
 val print_implicits : bool ref
 val print_casts : bool ref
 val print_arguments : bool ref
+val print_evar_arguments : bool ref
 val print_coercions : bool ref
 
 val with_casts : ('a -> 'b) -> 'a -> 'b
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 4980afd587..ad74cd462e 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -35,12 +35,19 @@ Syntax constr
   | type [(TYPE)] -> ["Type"]
   | type_sp [(TYPE ($PATH $sp) ($NUM $n))] -> ["Type"]
 (* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
-   typing/printer to deal with the duality CCI/FW *)
+   Printer to know if they must be qualified or not (and previously to
+   deal with the duality CCI/FW) *)
 
   | evar [<< ? >>] -> ["?"]
   | meta [(META ($NUM $n))] -> [ "?" $n ]
   | implicit [(IMPLICIT)] -> ["<Implicit>"]
   | indice [(REL ($NUM $n))] -> ["<Unbound ref: " $n ">"]
+  | instantiation [(INSTANCE $a ($LIST $l))] ->
+	 [ $a "{" (CONTEXT ($LIST $l)) "}"]
+  | instantiation_nil [(CONTEXT)] -> [ ]
+  | instantiation_one [(CONTEXT $a)] -> [ $a ]
+  | instantiation_many [(CONTEXT $a $b ($LIST $l))] ->
+	 [ (CONTEXT $b ($LIST $l)) ";" $a ]
   ;
 
 (* Things parsed in command1 *)