From 9936e2ba36e1d16dcee047d34b0c4caf8c377726 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 23 Sep 2006 07:39:28 +0000
Subject: - Correction filtrage des notations impliquant un "match" : la
 présence   des localisations empêchait toute unification des pattern de
 filtrage   de réussir. - Ajout au passage d'unification des pattern modulo
 alpha. - Exemples dans Notations.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 06a8ec9d02..c613bf0dbe 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -394,6 +394,15 @@ 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 =
+  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)
+	(match_names metas acc na1 na2) patl1 patl2
+  | _ -> raise No_match
+
 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
@@ -462,10 +471,12 @@ 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
 
-and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
-  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
-    match_ alp metas sigma rhs1 rhs2
-  else raise No_match
+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
+  match_ alp metas sigma rhs1 rhs2
 
 type scope_name = string
 
-- 
cgit v1.2.3