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

4 files changed, 36 insertions, 6 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index da417f44df..1ae4d96fa0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1032,7 +1032,7 @@ let rec generalize_problem names pb = function
 	  tomatch = Abstract d :: tomatch;
           pred = generalize_predicate names i d pb.tomatch pb'.pred  }
 
-(* No more patterns: typing the right-hand-side of equations *)
+(* No more patterns: typing the right-hand side of equations *)
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
@@ -1669,7 +1669,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
 
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
 
-  (* We build the matrix of patterns and right-hand-side *)
+  (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env tomatchl eqns in
 
   (* We build the vector of terms to match consistently with the *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9113efd559..01d1b8b006 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -362,6 +362,8 @@ let detype_sort = function
   | Prop c -> RProp c
   | Type u -> RType (Some u)
 
+type binder_kind = BProd | BLambda | BLetIn
+
 (**********************************************************************)
 (* Main detyping function                                             *)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index fb6bf8545c..6dbaebc46a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -32,8 +32,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -183,6 +181,36 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
 
+let fold_rawconstr f acc =
+  let rec fold acc = function
+  | RVar _ -> acc
+  | RApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) ->
+      fold (fold acc b) c
+  | RCases (_,_,rtntypopt,tml,pl) ->
+      List.fold_left fold_pattern
+	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
+	pl
+    | RLetTuple (_,_,rtntyp,b,c) ->
+	fold (fold (fold_return_type acc rtntyp) b) c
+    | RIf (_,c,rtntyp,b1,b2) ->
+	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
+    | RRec (_,_,_,bl,tyl,bv) ->
+	let acc = Array.fold_left
+	  (List.fold_left (fun acc (na,k,bbd,bty) ->
+	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
+	Array.fold_left fold (Array.fold_left fold acc tyl) bv
+    | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc
+
+  and fold_pattern acc (_,idl,p,c) = fold acc c
+
+  and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt
+
+  in fold acc
+
+let iter_rawconstr f = fold_rawconstr (fun () -> f) ()
+
 let occur_rawconstr id =
   let rec occur = function
     | RVar (loc,id') -> id = id'
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2498af7b53..242244bd65 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -33,8 +33,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -105,6 +103,8 @@ val map_rawconstr_with_binders_loc : loc ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
 *)
 
+val fold_rawconstr : ('a -> rawconstr -> 'a) -> 'a -> rawconstr -> 'a
+val iter_rawconstr : (rawconstr -> unit) -> rawconstr -> unit
 val occur_rawconstr : identifier -> rawconstr -> bool
 val free_rawvars : rawconstr -> identifier list
 val loc_of_rawconstr : rawconstr -> loc