Affichage des notations récursives:

- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives 
  sous forme de terme par une représentation directe (permet notamment
  de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml



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

5 files changed, 56 insertions, 60 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index bd688bcdd..585d7ab82 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -52,58 +52,56 @@ type prod_item =
   | NonTerm of constr_production_entry * 
       (Names.identifier * constr_production_entry) option
 
-type 'a action_env = (identifier * 'a) list
+type 'a action_env = 'a list * 'a list list
 
 let make_constr_action
   (f : loc -> constr_expr action_env -> constr_expr) pil =
-  let rec make (env : constr_expr action_env) = function
+  let rec make (env,envlist as fullenv : constr_expr action_env) = function
     | [] ->
-	Gramext.action (fun loc -> f loc env)
+	Gramext.action (fun loc -> f loc fullenv)
     | None :: tl -> (* parse a non-binding item *)
-        Gramext.action (fun _ -> make env tl)
+        Gramext.action (fun _ -> make fullenv tl)
     | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
-        Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
+        Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
-        Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
+        Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
     | Some (p, ETIdent) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:identifier) ->
-	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+	  make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
+	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
     | Some (p, ETConstrList _) :: tl ->
-        Gramext.action (fun (v:constr_expr list) ->
-          let dummyid = Ident (dummy_loc,id_of_string "_") in
-	  make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
+        Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
     | Some (p, ETPattern) :: tl -> 
 	failwith "Unexpected entry of type cases pattern" in
-  make [] (List.rev pil)
+  make ([],[]) (List.rev pil)
 
 let make_cases_pattern_action
   (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
-  let rec make (env : cases_pattern_expr action_env) = function
+  let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
     | [] ->
-	Gramext.action (fun loc -> f loc env)
+	Gramext.action (fun loc -> f loc fullenv)
     | None :: tl -> (* parse a non-binding item *)
-        Gramext.action (fun _ -> make env tl)
+        Gramext.action (fun _ -> make fullenv tl)
     | Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
-        Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl)
+        Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:reference) ->
-	  make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
+	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
     | Some (p, ETIdent) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:identifier) ->
-	  make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
+	  make 
+	    (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
+	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:cases_pattern_expr list) ->
-          let dummyid = Ident (dummy_loc,id_of_string "_") in
-	  make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
+	  make (env, v :: envlist) tl)
     | Some (p, (ETPattern | ETOther _)) :: tl -> 
 	failwith "Unexpected entry of type cases pattern or other" in
-  make [] (List.rev pil)
+  make ([],[]) (List.rev pil)
 
 let make_constr_prod_item univ assoc from forpat = function
   | Term tok -> (Gramext.Stoken tok, None)
@@ -133,11 +131,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt =
 
 let extend_constr_notation (n,assoc,ntn,rule) =
   (* Add the notation in constr *)
-  let mkact loc env = CNotation (loc,ntn,List.map snd env) in
+  let mkact loc env = CNotation (loc,ntn,env) in
   let e = get_constr_entry false (ETConstr (n,())) in
   extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
   (* Add the notation in cases_pattern *)
-  let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
+  let mkact loc env = CPatNotation (loc,ntn,env) in
   let e = get_constr_entry true (ETConstr (n,())) in
   extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
     true rule
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b8dcf8e99..740ba0b34 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -202,7 +202,7 @@ GEXTEND Gram
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CNotation(loc,"( _ )",[c])
+                CNotation(loc,"( _ )",([c],[]))
             | _ -> c) ] ]
   ;
   forall: 
@@ -337,7 +337,7 @@ GEXTEND Gram
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
               CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CPatNotation(loc,"( _ )",[p])
+                CPatNotation(loc,"( _ )",([p],[]))
             | _ -> p)
       | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
       | s = string -> CPatPrim (loc, String s) ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4f266f5ca..e906fb398 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -62,36 +62,32 @@ let prec_of_prim_token = function
   | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
   | String _ -> latom
 
-let env_assoc_value v env =
-  try List.nth env (v-1)
-  with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
-
-let decode_constrlist_value = function
-  | CAppExpl (_,_,l) -> l
-  | CApp (_,_,l) -> List.map fst l
-  | _ -> anomaly "Ill-formed list argument of notation"
-
-let decode_patlist_value = function
-  | CPatCstr (_,_,l) -> l
-  | _ -> anomaly "Ill-formed list argument of notation"
-
 open Notation
 
-let rec print_hunk n decode pr env = function
-  | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
-  | UnpListMetaVar (e,prec,sl) -> 
-      prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
-      (pr (n,prec)) (decode (env_assoc_value e env))
-  | UnpTerminal s -> str s
-  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
-  | UnpCut cut -> ppcmd_of_cut cut
-
-let pr_notation_gen decode pr s env =
+let print_hunks n pr (env,envlist) unp =
+  let env = ref env and envlist = ref envlist in
+  let pop r = let a = List.hd !r in r := List.tl !r; a in
+  let rec aux = function
+  | [] -> mt ()
+  | UnpMetaVar (_,prec) :: l ->
+      let c = pop env in pr (n,prec) c ++ aux l
+  | UnpListMetaVar (_,prec,sl) :: l ->
+      let cl = pop envlist in
+      let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+      let pp2 = aux l in
+      pp1 ++ pp2
+  | UnpTerminal s :: l -> str s ++ aux l
+  | UnpBox (b,sub) :: l ->
+      (* Keep order: side-effects *)
+      let pp1 = ppcmd_of_box b (aux sub) in
+      let pp2 = aux l in
+      pp1 ++ pp2
+  | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
+  aux unp
+
+let pr_notation pr s env =
   let unpl, level = find_notation_printing_rule s in
-  prlist (print_hunk level decode pr env) unpl, level
-
-let pr_notation = pr_notation_gen decode_constrlist_value
-let pr_patnotation = pr_notation_gen decode_patlist_value
+  print_hunks level pr env unpl, level
 
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
@@ -179,9 +175,9 @@ let rec pr_patt sep inh p =
   | CPatAtom (_,Some r) -> pr_reference r, latom
   | CPatOr (_,pl) ->
       hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
-  | CPatNotation (_,"( _ )",[p]) ->
+  | CPatNotation (_,"( _ )",([p],[])) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
-  | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
+  | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
   | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
@@ -592,7 +588,7 @@ let rec pr sep inherited a =
   | CCast (_,a,CastCoerce) ->
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
       lcast
-  | CNotation (_,"( _ )",[t]) ->
+  | CNotation (_,"( _ )",([t],[])) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation (pr mt) s env
   | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f779f53fb..2233bbd6a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -539,11 +539,11 @@ let rec pr_vernac = function
   | VernacStartTheoremProof (ki,l,_,_) ->
       let pr_statement head (id,(bl,c)) =
         hov 0
-          (head ++ spc () ++ pr_opt pr_lident id ++ spc() ++
+          (head ++ pr_opt pr_lident id ++ spc() ++
               (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
               str":" ++ pr_spc_lconstr c) in
       hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
-             prlist (pr_statement (str "with ")) (List.tl l))
+             prlist (pr_statement (spc () ++ str "with")) (List.tl l))
 
   | VernacEndProof Admitted -> str"Admitted"
   | VernacEndProof (Proved (opac,o)) -> (match o with
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 37350af08..8407211f1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -159,9 +159,11 @@ let rec mlexpr_of_constr = function
   | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
   | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
-  | Topconstr.CNotation(_,ntn,l) ->
+  | Topconstr.CNotation(_,ntn,subst) ->
       <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
-                $mlexpr_of_list mlexpr_of_constr l$ >>
+              $mlexpr_of_pair 
+                (mlexpr_of_list mlexpr_of_constr)
+                (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >>
   | Topconstr.CPatVar (loc,n) -> 
       <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"