Extension of the recursive notations mechanism

- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation

Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).

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

1 files changed, 36 insertions, 22 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index a32bfdec4..db28c866f 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -62,44 +62,53 @@ type grammar_constr_prod_item =
     (* 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
+  (f : loc -> constr_notation_substitution -> constr_expr) pil =
+  let rec make (constrs,constrlists,binders as fullsubst) = function
   | [] ->
-      Gram.action (fun loc -> f loc fullenv)
+      Gram.action (fun loc -> f loc fullsubst)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullenv tl)
+      Gram.action (fun _ -> make fullsubst tl)
   | GramConstrNonTerminal (typ, Some _) :: tl ->
       (* parse a binding non-terminal *)
     (match typ with
     | (ETConstr _| ETOther _) ->
-        Gram.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
+	Gram.action (fun (v:constr_expr) ->
+	  make (v :: constrs, constrlists, binders) tl)
     | ETReference ->
-        Gram.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
+        Gram.action (fun (v:reference) ->
+	  make (CRef v :: constrs, constrlists, binders) tl)
     | ETName ->
         Gram.action (fun (na:name located) ->
-	  make (constr_expr_of_name na :: env, envlist) tl)
+	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl)
     | ETConstrList (_,n) ->
-	Gram.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
+	Gram.action (fun (v:constr_expr list) ->
+	  make (constrs, v::constrlists, binders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gram.action (fun (v:local_binder list) ->
+	  make (constrs, constrlists, v::binders) tl)
+    | ETBinderList (false,_) ->
+	Gram.action (fun (v:local_binder list list) ->
+	  make (constrs, constrlists, List.flatten v::binders) 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
+      let heads,constrs = list_chop n constrs in
+      let constrlists =
+	if b then (heads@List.hd constrlists)::List.tl constrlists
+	else heads::constrlists
+      in make (constrs, constrlists, binders) tl
   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,envlist as fullenv : cases_pattern_expr action_env) = function
+  (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
+  let rec make (env,envlist as fullenv) = function
   | [] ->
       Gram.action (fun loc -> f loc fullenv)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
@@ -122,7 +131,7 @@ let make_cases_pattern_action
     | ETConstrList (_,_) ->
         Gram.action  (fun (vl:cases_pattern_expr list) ->
 	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETOther _) ->
+    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
 	failwith "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
@@ -273,7 +282,10 @@ type notation_grammar =
     int * gram_assoc option * notation * grammar_constr_prod_item list list
 
 type all_grammar_command =
-  | Notation of (precedence * tolerability list) * notation_grammar
+  | Notation of
+	 (precedence * tolerability list) *
+	  notation_var_internalization_type list *
+	  notation_grammar
   | TacticGrammar of
       (string * int * grammar_prod_item list *
          (dir_path * Tacexpr.glob_tactic_expr))
@@ -282,14 +294,16 @@ let (grammar_state : all_grammar_command list ref) = ref []
 
 let extend_grammar gram =
   (match gram with
-  | Notation (_,a) -> extend_constr_notation a
+  | Notation (_,_,a) -> extend_constr_notation a
   | TacticGrammar g -> add_tactic_entry g);
   grammar_state := gram :: !grammar_state
 
 let recover_notation_grammar ntn prec =
   let l = map_succeed (function
-    | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x
-    | _ -> failwith "") !grammar_state in
+    | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+	 vars, x
+    | _ ->
+	 failwith "") !grammar_state in
   assert (List.length l = 1);
   List.hd l