Added printing of recursive notations in cases pattern (supported by wish 2248).

Note that the code is no longer in constrextern.ml but in topconstr.ml where
the code for reversing notations of term already was.

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

3 files changed, 81 insertions, 69 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fec00c65a..28cd12fbd 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -338,48 +338,6 @@ let make_pat_notation loc ntn l =
     (fun (loc,p) -> CPatPrim (loc,p))
     destPatPrim l
 
-let bind_env (sigma,sigmalist as fullsigma) var v =
-  try
-    let vvar = List.assoc var sigma in
-    if v=vvar then fullsigma else raise No_match
-  with Not_found ->
-    (* TODO: handle the case of multiple occs in different scopes *)
-    (var,v)::sigma,sigmalist
-
-let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
-  | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
-  | PatVar (_,Anonymous), AHole _ -> sigma
-  | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
-      let nparams =
-	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
-      let l2 =
-        match a2 with
-	  | ARef (ConstructRef r2) when r1 = r2 -> []
-	  | AApp (ARef (ConstructRef r2),l2)  when r1 = r2 -> l2
-          | _ -> raise No_match in
-      if List.length l2 <> nparams + List.length args1
-      then
-	(* TODO: revert partially applied notations of the form 
-           "Notation P x := (@pair _ _ x)." *)
-	raise No_match
-      else
-        let (p2,args2) = list_chop nparams l2 in
-        (* All parameters must be _ *)
-        List.iter (function AHole _ -> () | _ -> raise No_match) p2;
-	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
-  (* TODO: use recursive notations *)
-  | _ -> raise No_match
-
-let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
-  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
-  let subst,substlist = match_cases_pattern vars ([],[]) c pat in
-  (* Reorder canonically the substitution *)
-  let find x subst =
-    try List.assoc x subst
-    with Not_found -> anomaly "match_aconstr_cases_pattern" in
-  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
-  List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
-
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e9a81f09c..0aa4339dd 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -467,12 +467,12 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
-let rec match_cases_pattern metas acc pat1 pat2 =
+let rec match_cases_pattern_binders metas acc pat1 pat2 =
   match (pat1,pat2) with
   | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2
   | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2)
       when c1 = c2 & List.length patl1 = List.length patl2 ->
-      List.fold_left2 (match_cases_pattern metas)
+      List.fold_left2 (match_cases_pattern_binders metas)
 	(match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
@@ -480,6 +480,29 @@ let adjust_application_n n loc f l =
   let l1,l2 = list_chop (List.length l - n) l in
   if l1 = [] then f,l else RApp (loc,f,l1), l2
 
+let match_alist match_fun metas sigma l1 l2 x iter termin lassoc =
+  (* match the iterator at least once *)
+  let sigmavar,sigmalist =
+    List.fold_left2 (match_fun (ldots_var::metas)) sigma l1 l2 in
+  (* Recover the recursive position *)
+  let rest = List.assoc ldots_var sigmavar in
+  (* Recover the first element *)
+  let t1 = List.assoc x sigmavar in
+  let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
+  (* try to find the remaining elements or the terminator *)
+  let rec match_alist_tail metas sigma acc rest =
+    try
+      let sigmavar,sigmalist = match_fun (ldots_var::metas) sigma rest iter in
+      let rest = List.assoc ldots_var sigmavar in
+      let t = List.assoc x sigmavar in
+      let sigmavar =
+	List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
+      match_alist_tail metas (sigmavar,sigmalist) (t::acc) rest
+    with No_match ->
+      List.rev acc, match_fun metas (sigmavar,sigmalist) rest termin in
+  let tl,(sigmavar,sigmalist) = match_alist_tail metas sigma [t1] rest in
+  (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
+
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
@@ -497,7 +520,8 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
       when List.length l1 >= List.length l2 ->
       let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in
-      match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
+      match_alist (match_ alp)
+	metas sigma (f1::l1) (f2::l2) x iter termin lassoc
   | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
@@ -550,29 +574,6 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | (RDynamic _ | RRec _ | REvar _), _
   | _,_ -> raise No_match
 
-and match_alist alp metas sigma l1 l2 x iter termin lassoc =
-  (* match the iterator at least once *)
-  let sigmavar,sigmalist =
-    List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
-  (* Recover the recursive position *)
-  let rest = List.assoc ldots_var sigmavar in
-  (* Recover the first element *)
-  let t1 = List.assoc x sigmavar in
-  let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
-  (* try to find the remaining elements or the terminator *)
-  let rec match_alist_tail alp metas sigma acc rest =
-    try
-      let sigmavar,sigmalist = match_ alp (ldots_var::metas) sigma rest iter in
-      let rest = List.assoc ldots_var sigmavar in
-      let t = List.assoc x sigmavar in
-      let sigmavar =
-	List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
-      match_alist_tail alp metas (sigmavar,sigmalist) (t::acc) rest
-    with No_match ->
-      List.rev acc, match_ alp metas (sigmavar,sigmalist) rest termin in
-  let tl,(sigmavar,sigmalist) = match_alist_tail alp metas sigma [t1] rest in
-  (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
-
 and match_binders alp metas na1 na2 sigma b1 b2 =
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
   match_ alp metas sigma b1 b2
@@ -581,7 +582,8 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
   let (alp,sigma) =
-    List.fold_left2 (match_cases_pattern metas) (alp,sigma) patl1 patl2 in
+    List.fold_left2 (match_cases_pattern_binders metas)
+      (alp,sigma) patl1 patl2 in
   match_ alp metas sigma rhs1 rhs2
 
 type scope_name = string
@@ -607,6 +609,55 @@ let match_aconstr c ((metas_scl,metaslist_scl),pat) =
   List.map (fun (x,scl) -> (find x,scl)) metas_scl,
   List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
 
+(* Matching cases pattern *)
+
+let bind_env_cases_pattern (sigma,sigmalist as fullsigma) var v =
+  try
+    let vvar = List.assoc var sigma in
+    if v=vvar then fullsigma else raise No_match
+  with Not_found ->
+    (* TODO: handle the case of multiple occs in different scopes *)
+    (var,v)::sigma,sigmalist
+
+let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
+  | r1, AVar id2 when List.mem id2 metas -> bind_env_cases_pattern sigma id2 r1
+  | PatVar (_,Anonymous), AHole _ -> sigma
+  | PatCstr (loc,(ind,_ as r1),[],_), ARef (ConstructRef r2) when r1 = r2 ->
+      sigma
+  | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2)
+      when r1 = r2 ->
+      let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
+      if List.length l2 <> nparams + List.length args1
+      then
+	(* TODO: revert partially applied notations of the form
+           "Notation P := (@pair)." *)
+	raise No_match
+      else
+        let (p2,args2) = list_chop nparams l2 in
+        (* All parameters must be _ *)
+        List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+  | PatCstr (loc,(ind,_ as r1),args1,_),
+    AList (x,_,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc)
+      when r1 = r2 ->
+      let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
+      assert (List.length args1 + nparams = List.length l2);
+      let (p2,args2) = list_chop nparams l2 in
+      List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+      match_alist match_cases_pattern
+	metas sigma args1 args2 x iter termin lassoc
+  | _ -> raise No_match
+
+let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
+  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+  let subst,substlist = match_cases_pattern vars ([],[]) c pat in
+  (* Reorder canonically the substitution *)
+  let find x subst =
+    try List.assoc x subst
+    with Not_found -> anomaly "match_aconstr_cases_pattern" in
+  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
+  List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
+
 (**********************************************************************)
 (*s Concrete syntax for terms *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a30c14966..b288fe8b5 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -82,6 +82,9 @@ type interpretation =
 val match_aconstr : rawconstr -> interpretation ->
       (rawconstr * subscopes) list * (rawconstr list * subscopes) list
 
+val match_aconstr_cases_pattern :  cases_pattern -> interpretation ->
+      (cases_pattern * subscopes) list * (cases_pattern list * subscopes) list
+
 (** Substitution of kernel names in interpretation data                *)
 
 val subst_interpretation : substitution -> interpretation -> interpretation