Report de l'heuristique d'unification premier ordre flexible/rigide

en dernière étape de la procédure d'unification
- Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution
  de l'unification premier ordre flexible/rigide
- Déplacement check_evars dans Evarutil
Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
(cf exemples d'application dans test-suite/success/evars.v)


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

6 files changed, 89 insertions, 75 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 48da52bb25..34f5a3c14f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -191,12 +191,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   else 
     let (t1,l1) = apprec_nohdbeta env isevars term1 in
     let (t2,l2) = apprec_nohdbeta env isevars term2 in
-    if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
-      or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
-    then 
-      (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true)
-    else 
-      evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+    evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
 
 and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
@@ -235,13 +230,15 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    not (occur_evar (fst ev1) (applist (term2,l2)))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
+	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
 	    let t2 = solve_pattern_eqn env l1 t2 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 *)
+	    (* Try first-order unification *)
+	    (* (heuristic that gives acceptable results in practice) *)
 	    let (deb2,rest2) =
               list_chop (List.length l2-List.length l1) l2 in
             ise_and i
@@ -265,6 +262,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    not (occur_evar (fst ev2) (applist (term1,l1)))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
+	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
 	    solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
@@ -272,6 +270,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
        	    List.length l2 <= List.length l1
 	  then
 	    (* Try first-order unification *)
+	    (* (heuristic that gives acceptable results in practice) *)
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
             (* First compare extra args for better failure message *)
@@ -322,25 +321,14 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  not (occur_evar (fst ev1) (applist (term2,l2)))
 	then
 	  (* Miller-Pfenning's patterns unification *)
+	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
 	  let t2 = solve_pattern_eqn env l1 t2 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 *)
-            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2);
-             (fun i ->
-               (* Then instantiate evar unless already done by unifying args *)
-	       let t2 = applist(term2,deb2) in
-	       if is_defined_evar i ev1 then
-		 evar_conv_x env i pbty (mkEvar ev1) t2
-	       else
-		 solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
-        else (isevars,false)
+	else
+	  (* Postpone the use of an heuristic *)
+	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  true
 
     | Rigid _, Flexible ev2 ->
 	if 
@@ -348,25 +336,14 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  not (occur_evar (fst ev2) (applist (term1,l1)))
 	then
 	  (* Miller-Pfenning's patterns unification *)
+	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
 	  let t1 = solve_pattern_eqn env l2 t1 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 *)
-            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
-	     (fun i ->
-               (* Then instantiate evar unless already done by unifying args *)
-	       let t1 = applist(term1,deb1) in
-	       if is_defined_evar i ev2 then
-		 evar_conv_x env i pbty t1 (mkEvar ev2)
-	       else
-		 solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
-        else (isevars,false)
+	else
+	  (* Postpone the use of an heuristic *)
+	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  true
 
     | MaybeFlexible flex1, Rigid _ ->
 	let f3 i =
@@ -514,6 +491,50 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
      (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 first_order_unification env isevars pbty (term1,l1) (term2,l2) =
+  match kind_of_term term1, kind_of_term term2 with
+    | Evar ev1,_ when List.length l1 <= List.length l2 ->
+	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+	ise_and isevars
+          (* First compare extra args for better failure message *)
+        [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+	(fun i ->
+          (* Then instantiate evar unless already done by unifying args *)
+	  let t2 = applist(term2,deb2) in
+	  if is_defined_evar i ev1 then
+	    evar_conv_x env i pbty t2 (mkEvar ev1)
+	  else
+	    solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
+    | _,Evar ev2 when List.length l2 <= List.length l1 ->
+	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+	ise_and isevars
+          (* First compare extra args for better failure message *)
+        [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
+	(fun i ->
+          (* Then instantiate evar unless already done by unifying args *)
+	  let t1 = applist(term1,deb1) in
+	  if is_defined_evar i ev2 then
+	    evar_conv_x env i pbty t1 (mkEvar ev2)
+	  else
+	    solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
+    | _ -> 
+	(* Some head evar have been instantiated *)
+	evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2))
+
+let consider_remaining_unif_problems env isevars =
+  let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
+  List.fold_left
+    (fun (isevars,b as p) (pbty,t1,t2) ->
+      (* Pas le bon env pour le problème... *)
+      if b then first_order_unification env isevars pbty 
+	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
+	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
+      else p)
+    (isevars,true)
+    pbs
+
+(* Main entry points *)
+
 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/evarconv.mli b/pretyping/evarconv.mli
index 41b5e05fa1..538ac29b9e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -33,3 +33,5 @@ val evar_eqappr_x :
     conv_pb -> constr * constr list -> constr * constr list ->
       evar_defs * bool
 (*i*)
+
+val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 47b10e6dd0..262214c3a7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -603,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
       (fun (isevars,b as p) (pbty,t1,t2) ->
-        if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
     (isevars,false)
 
+
+(* [check_evars] fails if some unresolved evar remains *)
+(* it assumes that the defined existentials have already been substituted *)
+
+let check_evars env initial_sigma isevars c =
+  let sigma = evars_of isevars in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (ev,args) ->
+          assert (Evd.mem sigma ev);
+	  if not (Evd.mem initial_sigma ev) then
+            let (loc,k) = evar_source ev isevars in
+	    error_unsolvable_implicit loc env sigma k
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 98db6174f6..670b742707 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -78,6 +78,10 @@ val solve_simple_eqn :
   -> env ->  evar_defs -> conv_pb * existential * constr ->
     evar_defs * bool
 
+(* [check_evars env initial_sigma extended_sigma c] fails if some
+   new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_defs -> constr -> unit
+
 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
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 738a951470..bb973b71ee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -114,8 +114,6 @@ sig
 
   val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
-  val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit
-
   (*i*)
   (* Internal of Pretyping...
    * Unused outside, but useful for debugging
@@ -634,35 +632,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
       nf_evar (evars_of !isevars) c'
 
-  (* [check_evars] fails if some unresolved evar remains *)
-  (* it assumes that the defined existentials have already been substituted
-     (should be done in unsafe_infer and unsafe_infer_type) *)
-
-  let check_evars env initial_sigma isevars c =
-    let sigma = evars_of !isevars in
-    let rec proc_rec c =
-      match kind_of_term c with
-	| Evar (ev,args) ->
-            assert (Evd.mem sigma ev);
-	    if not (Evd.mem initial_sigma ev) then
-              let (loc,k) = evar_source ev !isevars in
-		error_unsolvable_implicit loc env sigma k
-	| _ -> iter_constr proc_rec c
-    in
-      proc_rec c(*;
-		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-		  if pbs <> [] then begin
-		  pperrnl
-		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-		  prlist_with_sep fnl
-		  (fun  (pb,c1,c2) ->
-		  Termops.print_constr c1 ++
-		  (if pb=Reduction.CUMUL then str " <="++ spc()
-		  else str" =="++spc()) ++
-		  Termops.print_constr c2)
-		  pbs ++ fnl())
-		  end*)
-
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -671,7 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let isevars = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env isevars ([],[]) c in
-    let j = j_nf_evar (evars_of !isevars) j in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let j = j_nf_evar (evars_of isevars) j in
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
@@ -688,8 +658,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let c = nf_evar (evars_of isevars) c in
       if fail_evar then check_evars env sigma isevars c;
-      !isevars, c
+      isevars, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 06b290b1da..0b9b47b7a7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -78,8 +78,6 @@ sig
   (* Idem but do not fail on unresolved evars *)
   val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
-  val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit
-       
   (*i*)
   (* Internal of Pretyping...
    *)