Mise en place de motifs récursifs dans Notation; quelques simplifications au passage

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

6 files changed, 64 insertions, 26 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c8f167eb3b..20cec7a959 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -94,6 +94,10 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bignat.bigint) ->
 	  make ((p,CNumeral (dummy_loc,v)) :: env) 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)
     | Some (p, ETPattern) :: tl -> 
 	failwith "Unexpected entry of type cases pattern" in
   make [] (List.rev pil)
@@ -116,11 +120,16 @@ let make_act_in_cases_pattern (* For Notations *)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bignat.bigint) ->
 	  make ((p,CPatNumeral (dummy_loc,v)) :: env) 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)
     | Some (p, (ETPattern | ETOther _)) :: tl -> 
 	failwith "Unexpected entry of type cases pattern or other" in
   make [] (List.rev pil)
 
-let make_cases_pattern_act (* For Grammar *)
+(* For V7 Grammar only *)
+let make_cases_pattern_act
   (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
   let rec make (env : cases_pattern_expr action_env) = function
     | [] ->
@@ -134,7 +143,7 @@ let make_cases_pattern_act (* For Grammar *)
 	  tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
 	Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl)
-    | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
+    | Some (p, (ETConstrList _ | ETIdent | ETConstr _ | ETOther _)) :: tl ->
 	error "ident and constr entry not admitted in patterns cases syntax extensions" in
   make [] (List.rev pil)
 
@@ -145,16 +154,10 @@ let make_cases_pattern_act (* For Grammar *)
  * annotations are added when type-checking the command, function
  * Extend.of_ast) *)
 
-let rec build_prod_item univ assoc fromlevel pat = function
-  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc fromlevel pat s)
-  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc fromlevel pat s)
-  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc fromlevel pat s)
-  | ProdPrimitive typ -> symbol_of_production assoc fromlevel pat typ
-
 let symbol_of_prod_item univ assoc from forpat = function
   | Term tok -> (Gramext.Stoken tok, None)
   | NonTerm (nt, ovar) ->
-      let eobj = build_prod_item univ assoc from forpat nt in
+      let eobj = symbol_of_production assoc from forpat nt in
       (eobj, ovar)
 
 let coerce_to_id = function
@@ -252,7 +255,9 @@ let subst_constr_expr a loc subs =
          subst t,subst d)) dl)
   in subst a
 
+(* For V7 Grammar only *)
 let make_rule univ assoc etyp rule =
+  if not !Options.v7 then anomaly "No Grammar in new syntax";
   let pil = List.map (symbol_of_prod_item univ assoc etyp false) rule.gr_production in
   let (symbs,ntl) = List.split pil in
   let act = match etyp with
@@ -264,13 +269,14 @@ let make_rule univ assoc etyp rule =
 	      CPatDelimiters (loc,s,a)
           | _ -> error "Unable to handle this grammar extension of pattern" in
 	make_cases_pattern_act f ntl
-    | ETIdent | ETBigint | ETReference -> error "Cannot extend"
+    | ETConstrList _ | ETIdent | ETBigint | ETReference -> error "Cannot extend"
     | ETConstr _ | ETOther _ -> 
 	make_act (subst_constr_expr rule.gr_action) ntl in
   (symbs, act)
 
 (* Rules of a level are entered in reverse order, so that the first rules
    are applied before the last ones *)
+(* For V7 Grammar only *)
 let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
   let rules = List.rev (List.map (make_rule univ ass etyp) rls) in
   grammar_extend te pos [(name, p4ass, rules)]
@@ -282,6 +288,7 @@ let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} =
   (e,typ,pos,name,ass,p4ass,rls)
 
 (* Add a bunch of grammar rules. Does not check if it is well formed *)
+(* For V7 Grammar only *)
 let extend_grammar_rules gram =
   let univ = get_univ gram.gc_univ in
   let tl = List.map (define_entry univ) gram.gc_entries in
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 89a3da95f1..0fd620e3c3 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -33,6 +33,7 @@ type ('lev,'pos) constr_entry_key =
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
+  | ETConstrList of ('lev * 'pos) * Token.pattern list
 
 type constr_production_entry =
     (production_level,production_position) constr_entry_key
@@ -41,14 +42,14 @@ type simple_constr_production_entry = (production_level,unit) constr_entry_key
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
-  | ProdList1 of nonterm_prod
+  | ProdList1 of nonterm_prod * Token.pattern list
   | ProdOpt of nonterm_prod
   | ProdPrimitive of constr_production_entry
 
 type prod_item =
   | Term of Token.pattern
-  | NonTerm of
-      nonterm_prod * (Names.identifier * constr_production_entry) option
+  | NonTerm of constr_production_entry *
+      (Names.identifier * constr_production_entry) option
 
 type grammar_rule = {
   gr_name : string; 
@@ -236,10 +237,10 @@ let prod_item univ env = function
   | VTerm s -> env, Term (terminal s)
   | VNonTerm (loc, nt, Some p) ->
      let typ = nterm loc univ nt in
-      (p :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
+      (p :: env, NonTerm (typ, Some (p,typ)))
   | VNonTerm (loc, nt, None) ->
       let typ = nterm loc univ nt in 
-      env, NonTerm (ProdPrimitive typ, None)
+      env, NonTerm (typ, None)
 
 let rec prod_item_list univ penv pil current_pos =
   match pil with
@@ -256,7 +257,7 @@ let gram_rule univ (name,pil,act) =
   { gr_name = name; gr_production = pilc; gr_action = a }
 
 let border = function
-  | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a
+  | NonTerm (ETConstr(_,BorderProd (_,a)),_) :: _ -> a
   | _ -> None
 
 let clever_assoc ass g =
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 4aae3e3094..a95f1134b0 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -34,6 +34,7 @@ type ('lev,'pos) constr_entry_key =
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
+  | ETConstrList of ('lev * 'pos) * Token.pattern list
 
 type constr_production_entry =
     (production_level,production_position) constr_entry_key
@@ -42,14 +43,14 @@ type simple_constr_production_entry = (production_level,unit) constr_entry_key
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
-  | ProdList1 of nonterm_prod
+  | ProdList1 of nonterm_prod * Token.pattern list
   | ProdOpt of nonterm_prod
   | ProdPrimitive of constr_production_entry
 
 type prod_item =
   | Term of Token.pattern
-  | NonTerm of
-      nonterm_prod * (Names.identifier * constr_production_entry) option
+  | NonTerm of constr_production_entry * 
+      (Names.identifier * constr_production_entry) option
 
 type grammar_rule = {
   gr_name : string; 
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 606949e5f9..bf4c3372ef 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -180,7 +180,9 @@ GEXTEND Gram
     | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
-    | "9" [ ]
+    | "9"
+        [ ".."; ".."; c = operconstr LEVEL "0"; ".."; ".." ->
+          CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5ef39419c6..5e48e5edac 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -722,6 +722,7 @@ let compute_entry allow_create adjust forpat = function
   | ETPattern -> weaken_entry Constr.pattern, None, false
   | ETOther ("constr","annot") -> 
       weaken_entry Constr.annot, None, false
+  | ETConstrList _ -> error "List of entries cannot be registered"
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
@@ -776,12 +777,23 @@ let is_binder_level from e =
       ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7
     | _ -> false
 
-let symbol_of_production assoc from forpat typ =
+let rec symbol_of_production assoc from forpat typ =
   if is_binder_level from typ then
     let eobj = snd (get_entry (get_univ "constr") "operconstr") in
     Gramext.Snterml (Gram.Entry.obj eobj,"200")
   else if is_self from typ then Gramext.Sself
   else
+    match typ with
+    | ETConstrList (typ',[]) ->
+        Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ'))
+    | ETConstrList (typ',tkl) ->
+        Gramext.Slist1sep
+          (symbol_of_production assoc from forpat (ETConstr typ'),
+           Gramext.srules
+             [List.map (fun x -> Gramext.Stoken x) tkl,
+              List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
+                (Gramext.action (fun loc -> ()))])
+    | _ ->
     match get_constr_production_entry assoc from forpat typ with
       | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
       | (eobj,Some None,_) -> Gramext.Snext
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 335d3b7964..f30ac61cb9 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -45,17 +45,32 @@ 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 Symbols
 
-let rec print_hunk n pr env = function
+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 pr env) sub)
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
   | UnpCut cut -> ppcmd_of_cut cut
 
-let pr_notation pr s env =
+let pr_notation_gen decode pr s env =
   let unpl, level = find_notation_printing_rule s in
-  prlist (print_hunk level pr env) unpl, level
+  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
 
 let pr_delimiters key strm =
   let left = "'"^key^":" and right = "'" in
@@ -206,7 +221,7 @@ let rec pr_cases_pattern _inh = function
   | CPatAtom (_,None) -> str "_"
   | CPatNotation (_,"( _ )",[p]) ->
       str"("++ pr_cases_pattern _inh p ++ str")"
-  | CPatNotation (_,s,env) -> fst (pr_notation pr_cases_pattern s env)
+  | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env)
   | CPatNumeral (_,n) -> Bignat.pr_bigint n
   | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern _inh p)