From 7ce2a046e9a9bee93fd5f63d3938ceedb85f19f2 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 17 Sep 2007 18:40:21 +0000 Subject: 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 --- test-suite/success/evars.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 26e62ae622..94daad3a59 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). -- cgit v1.2.3