Diverses modifications autour de l'unification modulo conversion:

- extension de l'unification au cas de motifs (au sens de Dale Miller)
  [appel de solve_pattern_eqn dans evar_conv_x],
- correction de bugs présumés dans real_clean et do_restrict_hyp
  (prise en compte de la taille courante du contexte de de Bruijn),
- ajout d'une heuristique de beta-reduction de tete dans real_clean
  (cf test-suite/success/unification.v),
- suppression de certains "try ... with _ => ...".


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

5 files changed, 185 insertions, 42 deletions

diff --git a/CHANGES b/CHANGES
index c1daeecbd..97c02e6c7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,9 @@
+Changes from V8.1beta to V8.1
+=============================
+
+- Support for Miller-Pfenning's patterns unification in type synthesis
+  (e.g. can infer P such that P x y = phi(x,y))
+
 Changes from V8.0 to V8.1
 =========================
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 923903bdb..c709a62b4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -8,12 +8,14 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Term
 open Closure
 open Reduction
 open Reductionops
+open Termops
 open Environ
 open Typing
 open Classops
@@ -83,7 +85,7 @@ let evar_apprec env isevars stack c =
       | Evar (n,_ as ev) when Evd.is_defined sigma n ->
 	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
-  in aux (c, append_stack (Array.of_list stack) empty_stack)
+  in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env isevars c =
   let (t,stack as s) = Reductionops.whd_stack c in
@@ -126,7 +128,6 @@ let check_conv_record (t1,l1) (t2,l2) =
   with _ -> 
     raise Not_found
 
-
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
@@ -229,7 +230,17 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
-          if List.length l1 <= List.length l2 then
+	  if 
+	    is_unification_pattern l1 & 
+	    not (occur_evar (fst ev1) (applist (term2,l2)))
+	  then
+	    (* Miller-Pfenning's patterns unification *)
+	    let t2 = solve_pattern_eqn env l1 (applist(term2,l2)) in
+	    solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	  else if
+            List.length l1 <= List.length l2
+	  then
+	  (* Try first-order unification *)
 	    let (deb2,rest2) =
               list_chop (List.length l2-List.length l1) l2 in
             ise_and i
@@ -248,7 +259,17 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
-       	  if List.length l2 <= List.length l1 then
+	  if 
+	    is_unification_pattern l2 & 
+	    not (occur_evar (fst ev2) (applist (term1,l1)))
+	  then
+	    (* Miller-Pfenning's patterns unification *)
+	    let t1 = solve_pattern_eqn env l2 (applist(term1,l1)) in
+	    solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	  else if
+       	    List.length l2 <= List.length l1
+	  then
+	    (* Try first-order unification *)
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
             (* First compare extra args for better failure message *)
@@ -273,8 +294,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (try conv_record env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
-(* TODO: remove this _ !!! *)
-           with _ -> (i,false))
+           with Not_found -> (i,false))
 	and f4 i =
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
@@ -295,7 +315,17 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	ise_try isevars [f2; f3; f4]
 
     | Flexible ev1, Rigid _ ->
-       	if (List.length l1 <= List.length l2) then
+	if 
+	  is_unification_pattern l1 & 
+	  not (occur_evar (fst ev1) (applist (term2,l2)))
+	then
+	  (* Miller-Pfenning's patterns unification *)
+	  let t2 = solve_pattern_eqn env l1 (applist(term2,l2)) in
+	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	else if
+       	  List.length l1 <= List.length l2
+	then
+	  (* Try first-order unification *)
        	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
           ise_and isevars
             (* First compare extra args for better failure message *)
@@ -308,8 +338,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	       else
 		 solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
         else (isevars,false)
+
     | Rigid _, Flexible ev2 ->
-        if List.length l2 <= List.length l1 then
+	if 
+	  is_unification_pattern l2 & 
+	  not (occur_evar (fst ev2) (applist (term1,l1)))
+	then
+	  (* Miller-Pfenning's patterns unification *)
+	  let t1 = solve_pattern_eqn env l2 (applist(term1,l1)) in
+	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	else if
+	  List.length l2 <= List.length l1
+	then
+	  (* Try first-order unification *)
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
           ise_and isevars
             (* First compare extra args for better failure message *)
@@ -326,7 +367,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | MaybeFlexible flex1, Rigid _ ->
 	let f3 i =
 	  (try conv_record env i (check_conv_record appr1 appr2)
-           with _ -> (i,false))
+           with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
@@ -337,8 +378,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	     
     | Rigid _ , MaybeFlexible flex2 -> 
 	let f3 i = 
-	  (try (conv_record env i (check_conv_record appr2 appr1))
-           with _ -> (i,false))
+	  (try conv_record env i (check_conv_record appr2 appr1)
+           with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
@@ -468,7 +509,7 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
          params1 params);
      (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
      (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
-    
+
 let the_conv_x     env t1 t2 isevars =
   match evar_conv_x env isevars CONV  t1 t2 with
       (evd',true) -> evd'
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 658bf407f..f803fd9d7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,13 +21,6 @@ open Evd
 open Reductionops
 open Pretype_errors
 
-
-let rec filter_unique = function
-  | [] -> []
-  | x::l ->
-      if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
-      else x::filter_unique l
-
 (* Expanding existential variables (pretyping.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 
@@ -310,29 +303,45 @@ let is_defined_equation env evd (ev,inst) rhs =
  * ?3 <-- ?1          no pb: env of ?3 is larger than ?1's
  * ?1 <-- (list ?2)   pb: ?2 may depend on x, but not ?1.
  * What we do is that ?2 is defined by a new evar ?4 whose context will be
- * a prefix of ?2's env, included in ?1's env. *)
+ * a prefix of ?2's env, included in ?1's env.
 
-let do_restrict_hyps evd ev args =
+ Concretely, the assumptions are "env |- ev : T" and "Gamma |-
+ ev[hyps:=args]" for some Gamma whose de Bruijn context has length k.
+ We create "env' |- ev' : T" for some env' <= env and define ev:=ev'
+*)
+
+let do_restrict_hyps env k evd ev args =
   let args = Array.to_list args in
   let evi = Evd.find (evars_of !evd) ev in
-  let env = evar_env evi in
   let hyps = evar_context evi in
-  let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
+  let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in
   (* No care is taken in case the evar type uses vars filtered out!
-     Is it important ? *)
-  let nc =
-    let env =
-      Sign.fold_named_context push_named sign ~init:(reset_context env) in
-    e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in
+     Assuming that the restriction comes from a well-typed Flex/Flex
+     unification problem (see real_clean), the type of the evar cannot
+     depend on variables that are not in the scope of the other evar,
+     since this other evar has the same type (up to unification).
+     Since moreover, the evar contexts uses names only, the
+     restriction raise no de Bruijn reallocation problem *)
+  let env' =
+    Sign.fold_named_context push_named hyps' ~init:(reset_context env) in
+  let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in
   evd := Evd.evar_define ev nc !evd;
   let (evn,_) = destEvar nc in
   mkEvar(evn,Array.of_list ncargs)
 
-
-let need_restriction isevars args = not (array_for_all closed0 args)
+let need_restriction k args = not (array_for_all (closedn k) args)
 
 (* We try to instantiate the evar assuming the body won't depend
- * on arguments that are not Rels or Vars, or appearing several times.
+ * on arguments that are not Rels or Vars, or appearing several times
+   (i.e. we tackle only Miller-Pfenning patterns unification) 
+
+  1) Let a unification problem "env |- ev[hyps:=args] = rhs"
+  2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
+     where only Rel's and Var's are relevant in subst
+  3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
+
+  Note: we don't assume rhs in normal form, it may fail while it would
+  have succeeded after some reductions
  *)
 (* Note: error_not_clean should not be an error: it simply means that the
  * conversion test that lead to the faulty call to [real_clean] should return
@@ -341,36 +350,52 @@ let need_restriction isevars args = not (array_for_all closed0 args)
 
 let real_clean env isevars ev evi args rhs =
   let evd = ref isevars in
-  let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
+  let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in
   let rec subs rigid k t =
     match kind_of_term t with
       | Rel i ->
  	 if i<=k then t
- 	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
+ 	 else
+	   (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *)
+	   (try List.assoc (mkRel (i-k)) subst 
+	    with Not_found -> if rigid then raise Exit else t)
       | Evar (ev,args) ->
           if Evd.is_defined_evar !evd (ev,args) then
             subs rigid k (existential_value (evars_of !evd) (ev,args))
           else
+	    (* Flex/Flex problem: restriction to a common scope *)
 	    let args' = Array.map (subs false k) args in
-	    if need_restriction !evd args' then
-              do_restrict_hyps evd ev args'
+	    if need_restriction k args' then
+              do_restrict_hyps (reset_context env) k evd ev args'
 	    else
 	      mkEvar (ev,args')
       | Var id ->
+	  (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *)
           (try List.assoc t subst
            with Not_found ->
              if
                not rigid 
+	     (* I don't understand this line: vars from evar_context evi
+		are private (especially some of them are freshly
+		generated in push_rel_context_to_named_context). They
+		have a priori nothing to do with the vars in env. I
+		remove the test [HH 25/8/06]
+
 		 or List.exists (fun (id',_,_) -> id=id') (evar_context evi)
+	     *)
              then t
-             else
-               error_not_clean env (evars_of !evd) ev rhs
-                 (evar_source ev !evd))
-      | _ -> map_constr_with_binders succ (subs rigid) k t
+             else raise Exit)
+               
+      | _ ->
+	  (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *)
+	  map_constr_with_binders succ (subs rigid) k t
   in
-  let body = subs true 0 (nf_evar (evars_of isevars) rhs) in
-  if not (closed0 body)
-  then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd);
+  let rhs = nf_evar (evars_of isevars) rhs in
+  let rhs = whd_beta rhs (* heuristic *) in
+  let body = 
+    try subs true 0 rhs
+    with Exit -> 
+      error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
   (!evd,body)
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
@@ -464,6 +489,24 @@ let head_evar =
   in 
   hrec 
 
+(* Check if an applied evar "?X[args] l" is a Miller's pattern; note
+   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 l =
+  List.for_all isRel l & list_uniquize l = l
+
+(* From a unification problem "?X l1 = term1 l2" such that l1 is made
+   of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
+
+let solve_pattern_eqn env l1 c =
+  let c' = List.fold_right (fun a c ->
+    let c' = subst_term (lift 1 a) (lift 1 c) in
+    let n = destRel a in 
+    let (na,_,t) = lookup_rel n env (* if na defined, do as if assumption *) in
+    (mkLambda (na,lift n t,c'))) l1 c in
+  whd_eta c'
+
 (* This code (i.e. solve_pb, etc.) takes a unification
  * problem, and tries to solve it. If it solves it, then it removes
  * all the conversion problems, and re-runs conversion on each one, in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 6ce30ff79..2aceece0b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -82,6 +82,9 @@ 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 : constr list -> bool
+val solve_pattern_eqn : env -> constr list -> constr -> constr
+
 (***********************************************************)
 (* Value/Type constraints *)
 
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
new file mode 100644
index 000000000..60c03831a
--- /dev/null
+++ b/test-suite/success/unification.v
@@ -0,0 +1,50 @@
+(* Test patterns unification *)
+
+Lemma l1 : (forall P, (exists x:nat, P x) -> False) 
+         -> forall P, (exists x:nat, P x /\ P x) -> False.
+Proof.
+intros; apply (H _ H0).
+Qed.
+
+Lemma l2 :  forall A:Set, forall Q:A->Set,
+           (forall (P: forall x:A, Q x -> Prop), 
+                   (exists x:A, exists y:Q x, P x y) -> False) 
+         -> forall (P: forall x:A, Q x -> Prop), 
+                   (exists x:A, exists y:Q x, P x y /\ P x y) -> False.
+Proof.
+intros; apply (H _ H0).
+Qed.
+
+
+(* Example submitted for Zenon *)
+
+Axiom zenon_noteq : forall T : Type, forall t : T, ((t <> t) -> False).
+Axiom zenon_notall : forall T : Type, forall P : T -> Prop,
+  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
+
+  (* Must infer "P := fun x => x=x" in zenon_notall *)
+Check (fun _h1 => (zenon_notall nat _ (fun _T_0 =>
+          (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)).
+
+
+(* Core of an example submitted by Ralph Matthes (#849)
+
+   It used to fail because of the K-variable x in the type of "sum_rec ..."
+   which was not in the scope of the evar ?B. Solved by a head
+   beta-reduction of the type "(fun _ : unit + unit => L unit) x" of
+   "sum_rec ...". Shall we used more reduction when solving evars (in
+   real_clean)?? Is there a risk of starting too long reductions?
+
+   Note that the example originally came from a non re-typable
+   pretty-printed term (the checked term is actually re-printed the
+   same form it is checked).  
+*)
+
+Set Implicit Arguments.
+Inductive L (A:Set) : Set := c : A -> L A.
+Parameter f: forall (A:Set)(B:Set), (A->B) -> L A -> L B.
+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).