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

4 files changed, 40 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9af633b0a..48da52bb2 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 73cfa698d..47b10e6dd 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 5519b57c9..98db6174f 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 f231c728b..dab4b4f12 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)