Added automatic expansion on the left of recursive notations

(currently only one expansion but could be virtually made user-parametrizable).
Also fixed a bug in recursive notations happening with multiple-tokens
separators (see Notations.v in test-suite).

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

7 files changed, 137 insertions, 66 deletions

diff --git a/CHANGES b/CHANGES
index 6a75ba64f..845f8d785 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,8 @@ Notations
   incompatibilities generally solvable by changing such abbreviations from
   e.g. "Notation foo' := (foo x)" to "Notation foo' y := (foo x (y:=y))").
 - The "where" clause now supports multiple notations per defined object.
+- Recursive notations automatically expand one step on the left for better
+  factorization; recursion notations inner separators now ensured being tokens.
 
 Vernacular commands
 
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 927ac74e0..023ec0f3c 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -59,62 +59,90 @@ let cases_pattern_expr_of_name (loc,na) = match na with
 type grammar_constr_prod_item =
   | GramConstrTerminal of Token.pattern
   | GramConstrNonTerminal of constr_prod_entry_key * identifier option
+  | GramConstrListMark of int * bool
+    (* tells action rule to make a list of the n previous parsed items; 
+       concat with last parsed list if true *)
 
 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,envlist as fullenv : constr_expr action_env) = function
-    | [] ->
-	Gramext.action (fun loc -> f loc fullenv)
-    | None :: tl -> (* parse a non-binding item *)
-        Gramext.action (fun _ -> make fullenv tl)
-    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
+  | [] ->
+      Gramext.action (fun loc -> f loc fullenv)
+  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
+      (* parse a non-binding item *)
+      Gramext.action (fun _ -> make fullenv tl)
+  | GramConstrNonTerminal (typ, Some _) :: tl ->
+      (* parse a binding non-terminal *)
+    (match typ with
+    | (ETConstr _| ETOther _) ->
         Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
-    | Some (p, ETReference) :: tl -> (* non-terminal *)
+    | ETReference ->
         Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
-    | Some (p, ETName) :: tl -> (* non-terminal *)
+    | ETName ->
         Gramext.action (fun (na:name located) ->
 	  make (constr_expr_of_name na :: env, envlist) tl)
-    | Some (p, ETBigint) :: tl -> (* non-terminal *)
+    | ETBigint ->
         Gramext.action (fun (v:Bigint.bigint) ->
 	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
-    | Some (p, ETConstrList _) :: 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
+    | ETConstrList (_,n) ->
+	Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
+    | ETPattern ->
+	failwith "Unexpected entry of type cases pattern")
+  | GramConstrListMark (n,b) :: tl ->
+      (* Rebuild expansions of ConstrList *)
+      let heads,env = list_chop n env in
+      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
+      else make (env,heads::envlist) tl
+  in
   make ([],[]) (List.rev pil)
 
 let make_cases_pattern_action
   (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
   let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
-    | [] ->
-	Gramext.action (fun loc -> f loc fullenv)
-    | None :: tl -> (* parse a non-binding item *)
-        Gramext.action (fun _ -> make fullenv tl)
-    | Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
+  | [] ->
+      Gramext.action (fun loc -> f loc fullenv)
+  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
+      (* parse a non-binding item *)
+      Gramext.action (fun _ -> make fullenv tl)
+  | GramConstrNonTerminal (typ, Some _) :: tl ->
+      (* parse a binding non-terminal *)
+    (match typ with
+    | ETConstr _ -> (* pattern non-terminal *)
         Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
-    | Some (p, ETReference) :: tl -> (* non-terminal *)
+    | ETReference ->
         Gramext.action (fun (v:reference) ->
 	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
-    | Some (p, ETName) :: tl -> (* non-terminal *)
+    | ETName ->
         Gramext.action (fun (na:name located) ->
 	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
-    | Some (p, ETBigint) :: tl -> (* non-terminal *)
+    | ETBigint ->
         Gramext.action (fun (v:Bigint.bigint) ->
 	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
-    | Some (p, ETConstrList _) :: tl ->
-        Gramext.action (fun (v:cases_pattern_expr list) ->
-	  make (env, v :: envlist) tl)
-    | Some (p, (ETPattern | ETOther _)) :: tl ->
-	failwith "Unexpected entry of type cases pattern or other" in
+    | ETConstrList (_,_) ->
+        Gramext.action  (fun (vl:cases_pattern_expr list) ->
+	  make (env, vl :: envlist) tl)
+    | (ETPattern | ETOther _) ->
+	failwith "Unexpected entry of type cases pattern or other")
+  | GramConstrListMark (n,b) :: tl ->
+      (* Rebuild expansions of ConstrList *)
+      let heads,env = list_chop n env in
+      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
+      else make (env,heads::envlist) tl
+  in
   make ([],[]) (List.rev pil)
 
-let make_constr_prod_item univ assoc from forpat = function
-  | GramConstrTerminal tok -> (Gramext.Stoken tok, None)
-  | GramConstrNonTerminal (nt, ovar) ->
-      let eobj = symbol_of_constr_prod_entry_key assoc from forpat nt in
-      (eobj, Option.map (fun x -> (x,nt)) ovar)
+let rec make_constr_prod_item assoc from forpat = function
+  | GramConstrTerminal tok :: l ->
+      Gramext.Stoken tok :: make_constr_prod_item assoc from forpat l
+  | GramConstrNonTerminal (nt, ovar) :: l ->
+      symbol_of_constr_prod_entry_key assoc from forpat nt
+      :: make_constr_prod_item assoc from forpat l
+  | GramConstrListMark _ :: l ->
+      make_constr_prod_item assoc from forpat l
+  | [] ->
+      []
 
 let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
   let entry = 
@@ -129,26 +157,25 @@ let pure_sublevels level symbs =
   | _ ->
       failwith "") symbs
 
-let extend_constr (entry,level) (n,assoc) mkact forpat pt =
-  let univ = get_univ "constr" in
-  let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
-  let (symbs,ntl) = List.split pil in
+let extend_constr (entry,level) (n,assoc) mkact forpat rules =
+  List.iter (fun pt ->
+  let symbs = make_constr_prod_item assoc n forpat pt in
   let pure_sublevels = pure_sublevels level symbs in
   let needed_levels = register_empty_levels forpat pure_sublevels in
   let pos,p4assoc,name,reinit = find_position forpat assoc level in
   List.iter (prepare_empty_levels forpat) needed_levels;
-  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
+  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]) rules
 
-let extend_constr_notation (n,assoc,ntn,rule) =
+let extend_constr_notation (n,assoc,ntn,rules) =
   (* Add the notation in constr *)
   let mkact loc env = CNotation (loc,ntn,env) in
   let e = interp_constr_entry_key false (ETConstr (n,())) in
-  extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
+  extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules;
   (* Add the notation in cases_pattern *)
   let mkact loc env = CPatNotation (loc,ntn,env) in
   let e = interp_constr_entry_key true (ETConstr (n,())) in
   extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
-    true rule
+    true rules
 
 (**********************************************************************)
 (** Making generic actions in type generic_argument                   *)
@@ -241,7 +268,7 @@ let add_tactic_entry (key,lev,prods,tac) =
 (** State of the grammar extensions                                   *)
 
 type notation_grammar =
-    int * Gramext.g_assoc option * notation * grammar_constr_prod_item list
+    int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
 
 type all_grammar_command =
   | Notation of (precedence * tolerability list) * notation_grammar
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 14e4cfd37..1228b40cf 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -31,9 +31,12 @@ open Mod_subst
 type grammar_constr_prod_item =
   | GramConstrTerminal of Token.pattern
   | GramConstrNonTerminal of constr_prod_entry_key * identifier option
+  | GramConstrListMark of int * bool
+    (* tells action rule to make a list of the n previous parsed items; 
+       concat with last parsed list if true *)
 
 type notation_grammar =
-    int * Gramext.g_assoc option * notation * grammar_constr_prod_item list
+    int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
 
 (* For tactic and vernac notations *)
 
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 2121671a8..7643120f3 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -50,9 +50,14 @@ type ('lev,'pos) constr_entry_key_gen =
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Token.pattern list
 
-type constr_prod_entry_key =
-    (production_level,production_position) constr_entry_key_gen
+(* Entries level (left-hand-side of grammar rules) *)
 type constr_entry_key =
     (int,unit) constr_entry_key_gen
+
+(* Entries used in productions (in right-hand-side of grammar rules) *)
+type constr_prod_entry_key =
+    (production_level,production_position) constr_entry_key_gen
+
+(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
 type simple_constr_prod_entry_key =
     (production_level,unit) constr_entry_key_gen
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 0ca073956..7643120f3 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -50,10 +50,14 @@ type ('lev,'pos) constr_entry_key_gen =
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Token.pattern list
 
-type constr_prod_entry_key =
-    (production_level,production_position) constr_entry_key_gen
+(* Entries level (left-hand-side of grammar rules) *)
 type constr_entry_key =
     (int,unit) constr_entry_key_gen
+
+(* Entries used in productions (in right-hand-side of grammar rules) *)
+type constr_prod_entry_key =
+    (production_level,production_position) constr_entry_key_gen
+
+(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
 type simple_constr_prod_entry_key =
     (production_level,unit) constr_entry_key_gen
-
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 7ddb6146d..661a8757a 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -53,3 +53,9 @@ Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat
 
 Notation R x := (@pair _ _ x).
 Check (fun x:nat*nat => match x with R x y => (x,y) end).
+
+(* Check multi-tokens recursive notations *)
+
+Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
+Check [ 0 ].
+Check [ 0 # ; 1 ].
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6fdfb5732..a75ee2a7d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -25,6 +25,7 @@ open Libnames
 open Lexer
 open Egrammar
 open Notation
+open Nameops
 
 (**********************************************************************)
 (* Tokens                                                             *)
@@ -269,24 +270,29 @@ let split_notation_string str =
 
 (* Interpret notations with a recursive component *)
 
-let rec find_pattern xl = function
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let rec find_pattern nt xl = function
   | Break n as x :: l, Break n' :: l' when n=n' ->
-      find_pattern (x::xl) (l,l')
+      find_pattern nt (x::xl) (l,l')
   | Terminal s as x :: l, Terminal s' :: l' when s = s' ->
-      find_pattern (x::xl) (l,l')
-  | [NonTerminal x], NonTerminal x' :: l' ->
-      (x,x',xl),l'
-  | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+      find_pattern nt (x::xl) (l,l')
+  | [], NonTerminal x' :: l' ->
+      (out_nt nt,x',List.rev xl),l'
+  | _, Terminal s :: _ | Terminal s :: _, _ ->
       error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
-  | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+  | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
-  | ((SProdList _ | NonTerminal _) :: _ | []), _ ->
+  | _, [] ->
       error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
+  | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
+      anomaly "Only Terminal or Break expected on left, non-SProdList on right"
 
 let rec interp_list_parser hd = function
   | [] -> [], [], List.rev hd
   | NonTerminal id :: tl when id = ldots_var ->
-      let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+      let hd = List.rev hd in
+      let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let yl,xl,tl'' = interp_list_parser [] tl' in
       (* We remember each pair of variable denoting a recursive part to *)
       (* remove the second copy of it afterwards *)
@@ -302,6 +308,7 @@ let rec interp_list_parser hd = function
       yl, xl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
+
 (* Find non-terminal tokens of notation *)
 
 let is_normal_token str =
@@ -576,7 +583,7 @@ let is_not_small_constr = function
   | _ -> false
 
 let rec define_keywords_aux = function
-    GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",k) :: l
+  | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",k) :: l
       when is_not_small_constr e ->
       message ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
@@ -584,37 +591,54 @@ let rec define_keywords_aux = function
   | n :: l -> n :: define_keywords_aux l
   | [] -> []
 
+  (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
-    GramConstrTerminal("IDENT",k)::l ->
+  | GramConstrTerminal("IDENT",k)::l ->
       message ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
       GramConstrTerminal("",k) :: define_keywords_aux l
   | l -> define_keywords_aux l
 
+let distribute a ll = List.map (fun l -> a @ l) ll
+
+  (* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep)
+     as many times as expected in [n] argument *)
+let rec expand_list_rule typ tkl x n i hds ll =
+  if i = n then
+    let hds =
+      GramConstrListMark (n,true) :: hds
+      @	[GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in
+    distribute hds ll
+  else
+    let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in
+    let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in
+    let tks = List.map (fun x -> GramConstrTerminal x) tkl in
+    distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @
+      expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll
+
 let make_production etyps symbols =
   let prod =
     List.fold_right
-      (fun t l -> match t with
+      (fun t ll -> match t with
         | NonTerminal m ->
 	    let typ = List.assoc m etyps in
-	    GramConstrNonTerminal (typ, Some m) :: l
+	    distribute [GramConstrNonTerminal (typ, Some m)] ll
         | Terminal s ->
-	    GramConstrTerminal (terminal s) :: l
+	    distribute [GramConstrTerminal (terminal s)] ll
         | Break _ ->
-            l
+            ll
         | SProdList (x,sl) ->
-            let sl = List.flatten
+            let tkl = List.flatten
               (List.map (function Terminal s -> [terminal s]
                 | Break _ -> []
                 | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
-	    let y = match List.assoc x etyps with
+	    let typ = match List.assoc x etyps with
               | ETConstr x -> x
               | _ ->
                   error "Component of recursive patterns in notation must be constr." in
-            let typ = ETConstrList (y,sl) in
-            GramConstrNonTerminal (typ, Some x) :: l)
-      symbols [] in
-  define_keywords prod
+	    expand_list_rule typ tkl x 1 0 [] ll)
+      symbols [[]] in
+  List.map define_keywords prod
 
 let rec find_symbols c_current c_next c_last = function
   | [] -> []