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, 37 insertions, 0 deletions

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 26e62ae62..94daad3a5 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -68,6 +68,7 @@ Proof. trivial. Qed.
 Hint Resolve contradiction.
 Goal False.
 eauto.
+Abort.
 
 (* This used to fail in V8.1beta because first-order unification was
    used before using type information *)
@@ -86,3 +87,39 @@ Let Output := bool.
 Parameter Out : STATE -> Output.
 Check fun (s : STATE) (reg : Input) => reg = Out s.
 End A.
+
+(* An example extracted from FMapAVL which (may) test restriction on
+   evars problems of the form ?n[args1]=?n[args2] with distinct args1
+   and args2 *)
+
+Set Implicit Arguments.
+Parameter t:Set->Set.
+Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'.
+Parameter avl: forall elt : Set, t elt -> Prop.
+Parameter bst: forall elt : Set, t elt -> Prop.
+Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   avl m -> avl (map f m).
+Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   bst m -> bst (map f m).
+Record bbst (elt:Set) : Set := 
+  Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}.
+Definition t' := bbst.
+Section B.
+Variables elt elt': Set.
+Definition map' f (m:t' elt) : t' elt' := 
+  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
+End B.
+
+(* An example from Lexicographic_Exponentiation that tests the 
+   contraction of reducible fixpoints in type inference *)
+
+Require Import List.
+Check (fun (A:Set) (a b x:A) (l:list A) 
+  (H : l ++ cons x nil = cons b (cons a nil)) =>
+  app_inj_tail l (cons b nil) _ _ H).
+
+(* An example from NMake (simplified), that uses restriction in solve_refl *)
+
+Parameter g:(nat->nat)->(nat->nat).
+Fixpoint G p cont {struct p} :=
+  g (fun n => match p with O => cont | S p => G p cont end n).