Raffinement de l'algorithme d'inférence de type

-----------------------------------------------

- Les fonctions evar_define et real_clean font un travail plus fin :
  - S'il y a plusieurs manières d'inverser l'instance d'une evar, on
    retarde le choix au lieu de faire un choix arbitraire.
  - Si l'instance contient une evar et que cette evar n'est pas inversible,
    on essaie aussi d'inverser ou de restreindre (un sous-terme) de 
    l'evar qui était initialement à instancier.
  - Incidemment, real_clean est renommé en invert_instance, un nom qui
    reflète mieux la diversité du travail fait par ce fameux real_clean.
- La fonction solve_refl garde les problèmes qui contiennent encore de
  l'information.
- Changements secondaires :
  - Délégation de la gestion des variables modifiées et des problèmes à
    reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord
    au moment du define) (incidemment get_conv_pbs devient
    extract_conv_pbs)
  - Essai d'un mécanisme différent de restriction des evars : pour
    éviter des contextes mal formés (comme do_restrict pouvait a priori
    le faire), on utilise maintenant un contexte bien formé doublé d'un
    filtre signalant les instances interdites. C'est a priori plus
    souple (par ex : si une variable du contexte a un type dépendant
    d'une evar, on peut attendre de connaître cette evar avec de
    déterminer si cette variable du contexte, qui peut-être dépend via
    cette evar d'une autre variable interdite, doit être finalement
    interdite ou pas)
  - Nettoyages divers.
- Ce que evarutil ne fait toujours pas :
  - Utiliser l'inversion et/ou l'unification d'ordre supérieur (par
    exemple pour résoudre "?ev[S n]=n"); en particulier, la notion
    d'inversion unique ne prend pas en compte l'unification d'ordre
    supérieur et peut donc faire des choix irréversibles vis à vis de
    l'unif d'ordre supérieur.
  - Utiliser (systématiquement -- et précautionneusement) les types
    des solutions trouvées pour résoudre davantage de problèmes.



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

1 files changed, 13 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b65ad37b18..c4e3e6bdfc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -88,10 +88,9 @@ let evar_apprec env evd stack c =
   in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env evd c =
-  let (t,stack as s) = Reductionops.whd_stack c in
-  match kind_of_term t with
-    | (Case _ | Fix _) -> evar_apprec env evd [] c
-    | _ -> s
+  match kind_of_term (fst (Reductionops.whd_stack c)) with
+    | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
+    | _ -> c
 
 (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
    (t1 l1) = (t2 l2) into a problem
@@ -171,13 +170,8 @@ let ise_array2 evd f v1 v2 =
 
 let rec evar_conv_x env evd pbty term1 term2 = 
   let sigma = evars_of evd in
-  let term1 = whd_castappevar sigma term1 in
-  let term2 = whd_castappevar sigma term2 in
-(*
-  if eq_constr term1 term2 then 
-    true
-  else 
-*)
+  let term1 = apprec_nohdbeta env evd (whd_castappevar sigma term1) in
+  let term2 = apprec_nohdbeta env evd (whd_castappevar sigma term2) in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
@@ -188,10 +182,8 @@ let rec evar_conv_x env evd pbty term1 term2 =
     solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
   else if is_undefined_evar evd term2 then
     solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
-  else 
-    let (t1,l1) = apprec_nohdbeta env evd term1 in
-    let (t2,l2) = apprec_nohdbeta env evd term2 in
-    evar_eqappr_x env evd pbty (t1,l1) (t2,l2)
+  else
+    evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2)
 
 and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
@@ -522,12 +514,14 @@ let first_order_unification env evd pbty (term1,l1) (term2,l2) =
 	evar_conv_x env evd pbty (applist(term1,l1)) (applist(term2,l2))
 
 let consider_remaining_unif_problems env evd =
-  let (evd,pbs) = get_conv_pbs evd (fun _ -> true) in
+  let (evd,pbs) = extract_all_conv_pbs evd in
   List.fold_left
     (fun (evd,b as p) (pbty,env,t1,t2) ->
-      if b then first_order_unification env evd pbty 
-	(apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1))
-	(apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2))
+      if b then
+	let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in
+	let t2 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2) in
+	first_order_unification env evd pbty 
+	  (decompose_app t1) (decompose_app t2)
       else p)
     (evd,true)
     pbs