Ajout notation c.(f) en v8 pour les projections de Record

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

7 files changed, 45 insertions, 24 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 83f4cad58..397189271 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -274,10 +274,11 @@ let subst_constr_expr a loc subs =
       let na = name_app (subst_id subs) na in
       CLetIn (loc,(loc,na),subst b,subst c)
   | CArrow (_,a,b) -> CArrow (loc,subst a,subst b)
-  | CAppExpl (_,Ident (_,id),l) ->
-      CAppExpl (loc,subst_ref loc subs id,List.map subst l) 
+  | CAppExpl (_,(p,Ident (_,id)),l) ->
+      CAppExpl (loc,(p,subst_ref loc subs id),List.map subst l) 
   | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) 
-  | CApp (_,a,l) -> CApp (loc,subst a,List.map (fun (a,i) -> (subst a,i)) l)
+  | CApp (_,(p,a),l) ->
+      CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l)
   | CCast (_,a,b) -> CCast (loc,subst a,subst b)
   | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l)
   | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 367fd5e0e..be9e00c58 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -23,7 +23,7 @@ let constr_kw =
     ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!";
     "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/";
     "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-";
-    "~"; "'"; "<<"; ">>"; "<>";
+    "~"; "'"; "<<"; ">>"; "<>"; ".("
   ]
 let _ = List.iter (fun s -> Lexer.add_token ("",s)) constr_kw
 (* "let" is not a keyword because #Core#let.cci would not parse.
@@ -127,12 +127,12 @@ GEXTEND Gram
   operconstr:
     [ "10" RIGHTA
       [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") ->
-          CAppExpl (loc, f, args)
+          CAppExpl (loc, (false,f), args)
 (*
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
 *)
-      | f = operconstr; args = LIST1 constr91 -> CApp (loc, f, args) ]
+      | f = operconstr; args = LIST1 constr91 -> CApp (loc, (false,f), args) ]
     | "9" RIGHTA
       [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ]
     | "8" RIGHTA
@@ -196,7 +196,7 @@ GEXTEND Gram
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
 	  (match lc1 with
 	    | CPatVar (loc2,(false,n)) -> 
-                CApp (loc,CPatVar (loc2, (true,n)), List.map (fun c -> c, None) cl)
+                CApp (loc,(false,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl)
 	    | _ ->
 	    Util.error "Second-order pattern-matching expects a head metavariable")
       | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" ->
@@ -208,7 +208,7 @@ GEXTEND Gram
       | s = sort -> CSort (loc, s)
       | v = global -> CRef v
       | n = bigint -> CNumeral (loc,n)
-      | "!"; f = global -> CAppExpl (loc,f,[])
+      | "!"; f = global -> CAppExpl (loc,(false,f),[])
       | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> 
           CDelimiters (loc,key,c) ] ]
   ;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 88d108fdd..1876863d4 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -142,11 +142,15 @@ GEXTEND Gram
     | "40L" LEFTA
       [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
     | "10L" LEFTA
-      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,f,args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,f,args) ]
+      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(false,f),args)
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(false,f),args) ]
     | "9" [ ]
     | "1L" LEFTA
-      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
+      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c)
+      |	c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
+	  CApp(loc,(true,CRef f),args@[c,None])
+      | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT ->
+	  CAppExpl(loc,(false,f),args@[c]) ]
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 7fba1f279..5acc694aa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -117,10 +117,12 @@ GEXTEND Gram
   hints:
     [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
          (dbnames, 
-	  HintsResolve (List.map (fun qid -> (None, CAppExpl(loc,qid,[]))) l))
+	  HintsResolve
+	    (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l))
       | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, 
-	 HintsImmediate (List.map (fun qid-> (None, CAppExpl (loc,qid,[]))) l))
+	 HintsImmediate
+	   (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l))
       | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
     ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 629c20177..0d431ea93 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -422,7 +422,7 @@ GEXTEND Gram
 	   let c = match n with
 	     | Some n ->
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
-		 CApp (loc,c,l)
+		 CApp (loc,(false,c),l)
 	     | None -> c in
 	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 72a693012..361e24647 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -213,6 +213,19 @@ let pr_cases pr po tml eqns =
       prlist_with_sep (fun () -> str "| ") (pr_eqn pr) eqns ++
       str "end"))
 
+let pr_proj pr pr_app a f l =
+  hov 0 (pr (latom,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+
+let pr_explapp pr f l =
+  hov 0 (
+    str "!" ++ pr_reference f ++ 
+    prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l)
+
+let pr_app pr a l =
+  hov 0 (
+    pr (lapp,L) a ++ 
+    prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l)
+
 let rec pr inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
@@ -234,14 +247,15 @@ let rec pr inherited a =
       hv 1 (
 	hv 1 (str "[" ++ pr_let_binder pr (snd x) a ++ bll ++ str "]") ++
 	brk (0,1) ++ b), lletin
-  | CAppExpl (_,f,l) ->
-      hov 0 (
-	str "!" ++ pr_reference f ++
-	prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l), lapp
-  | CApp (_,a,l) ->
-      hov 0 (
-	pr (lapp,L) a ++ 
-	prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp
+  | CAppExpl (_,(true,f),l) ->
+      let a,l = list_sep_last l in
+      pr_proj pr pr_explapp a f l, lapp
+  | CAppExpl (_,(false,f),l) -> pr_explapp pr f l, lapp
+  | CApp (_,(true,a),l) ->
+      let c,l = list_sep_last l in
+      assert (snd c = None);
+      pr_proj pr pr_app (fst c) a l, lapp
+  | CApp (_,(false,a),l) -> pr_app pr a l, lapp
   | CCases (_,po,tml,eqns) ->
       pr_cases pr po tml eqns, lcases
   | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a42465572..cf59d9a97 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -194,8 +194,8 @@ let rec mlexpr_of_constr = function
   | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
+  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
+  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>