Ajout unification pattern dans l'algorithme d'unification des

tactiques (unification.ml) + renommages (evarconv.ml) + exemple (unification.v)


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

5 files changed, 55 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9af633b0ad..48da52bb25 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -231,7 +231,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
 	  if 
-	    is_unification_pattern ev1 l1 & 
+	    is_unification_pattern_evar ev1 l1 & 
 	    not (occur_evar (fst ev1) (applist (term2,l2)))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
@@ -261,7 +261,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
 	  if 
-	    is_unification_pattern ev2 l2 & 
+	    is_unification_pattern_evar ev2 l2 & 
 	    not (occur_evar (fst ev2) (applist (term1,l1)))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
@@ -318,7 +318,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, Rigid _ ->
 	if 
-	  is_unification_pattern ev1 l1 & 
+	  is_unification_pattern_evar ev1 l1 & 
 	  not (occur_evar (fst ev1) (applist (term2,l2)))
 	then
 	  (* Miller-Pfenning's patterns unification *)
@@ -344,7 +344,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Rigid _, Flexible ev2 ->
 	if 
-	  is_unification_pattern ev2 l2 & 
+	  is_unification_pattern_evar ev2 l2 & 
 	  not (occur_evar (fst ev2) (applist (term1,l1)))
 	then
 	  (* Miller-Pfenning's patterns unification *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 73cfa698db..47b10e6dd0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -493,9 +493,15 @@ let head_evar =
    that we don't care whether args itself contains Rel's or even Rel's
    distinct from the ones in l *)
 
-let is_unification_pattern (_,args) l =
+let is_unification_pattern_evar (_,args) l =
   let l' = Array.to_list args @ l in
-  List.for_all (fun a -> isRel a or isVar a) l' & list_uniquize l' = l'
+  List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l'
+
+let is_unification_pattern f l =
+  match kind_of_term f with
+    | Meta _ -> array_for_all isRel l & array_distinct l
+    | Evar ev -> is_unification_pattern_evar ev (Array.to_list l)
+    | _ -> false
 
 (* From a unification problem "?X l1 = term1 l2" such that l1 is made
    of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 5519b57c96..98db6174f6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -82,7 +82,8 @@ val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
 val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
 val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
-val is_unification_pattern : existential -> constr list -> bool
+val is_unification_pattern_evar : existential -> constr list -> bool
+val is_unification_pattern : constr -> constr array -> bool
 val solve_pattern_eqn : env -> constr list -> constr -> constr
 
 (***********************************************************)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f231c728b3..dab4b4f12f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -47,6 +47,9 @@ let abstract_list_all env sigma typ c l =
   with UserError _ ->
     raise (PretypeError (env,CannotGeneralize typ))
 
+(**)
+
+let solve_pattern_eqn_array env l c = solve_pattern_eqn env (Array.to_list l) c
 
 (*******************************)
 
@@ -72,7 +75,7 @@ let unify_0 env sigma cv_pb mod_delta m n =
   let trivial_unify pb substn m n =
     if (not(occur_meta m)) && (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) then substn
     else error_cannot_unify env sigma (m,n) in
-  let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
+  let rec unirec_rec env pb ((metasubst,evarsubst) as substn) m n =
     let cM = Evarutil.whd_castappevar sigma m
     and cN = Evarutil.whd_castappevar sigma n in 
     match (kind_of_term cM,kind_of_term cN) with
@@ -85,14 +88,25 @@ let unify_0 env sigma cv_pb mod_delta m n =
       | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
       | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
 
-      | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	  unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
-      | Prod (_,t1,c1), Prod (_,t2,c2) ->
-	  unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
-      | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
-      | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
+      | Lambda (na,t1,c1), Lambda (_,t2,c2) ->
+	  unirec_rec (push_rel_assum (na,t1) env) CONV 
+	    (unirec_rec env CONV substn t1 t2) c1 c2
+      | Prod (na,t1,c1), Prod (_,t2,c2) ->
+	  unirec_rec (push_rel_assum (na,t1) env) pb 
+	    (unirec_rec env CONV substn t1 t2) c1 c2
+      | LetIn (_,b,_,c), _ -> unirec_rec env pb substn (subst1 b c) cN
+      | _, LetIn (_,b,_,c) -> unirec_rec env pb substn cM (subst1 b c)
 
       | App (f1,l1), App (f2,l2) ->
+	  if is_unification_pattern f1 l1 & not (dependent f1 cN)
+	  then
+	    (destMeta f1,solve_pattern_eqn_array env l1 cN)::metasubst,
+	    evarsubst
+	  else if is_unification_pattern f2 l2 & not (dependent f2 cM)
+	  then
+	    (destMeta f2,solve_pattern_eqn_array env l2 cM)::metasubst,
+	    evarsubst
+	  else
 	  let len1 = Array.length l1
 	  and len2 = Array.length l2 in
           let (f1,l1,f2,l2) =
@@ -104,13 +118,13 @@ let unify_0 env sigma cv_pb mod_delta m n =
 	      let extras,restl1 = array_chop (len1-len2) l1 in 
               (appvect (f1,extras), restl1, f2, l2) in
           (try
-            array_fold_left2 (unirec_rec CONV)
-	      (unirec_rec CONV substn f1 f2) l1 l2
+            array_fold_left2 (unirec_rec env CONV)
+	      (unirec_rec env CONV substn f1 f2) l1 l2
 	  with ex when precatchable_exception ex ->
             trivial_unify pb substn cM cN)
       | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-          array_fold_left2 (unirec_rec CONV)
-	    (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
+          array_fold_left2 (unirec_rec env CONV)
+	    (unirec_rec env CONV (unirec_rec env CONV substn p1 p2) c1 c2) cl1 cl2
 
       | _ -> trivial_unify pb substn cM cN
 
@@ -120,7 +134,7 @@ let unify_0 env sigma cv_pb mod_delta m n =
   then 
     ([],[])
   else 
-    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
+    let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in
     ((*sort_eqns*) mc, (*sort_eqns*) ec)
 
 
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 60c03831a0..6886962156 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -48,3 +48,18 @@ Parameter t: L (unit + unit).
 Check (f (fun x : unit + unit =>
   sum_rec (fun _ : unit + unit => L unit)
     (fun y => c y) (fun y => c y) x) t).
+
+
+(* Test patterns unification in apply *)
+
+Require Import Arith.
+Parameter x y : nat.
+Parameter G:x=y->x=y->Prop.
+Parameter K:x<>y->x<>y->Prop.
+Lemma l3 : (forall f:x=y->Prop, forall g:x<>y->Prop,
+            match eq_nat_dec x y with left a => f a | right a => g a end)
+   -> match eq_nat_dec x y with left a => G a a | right a => K a a end.
+Proof.
+intros.
+apply H.
+Qed.