| Age | Commit message (Collapse) | Author |
|---|
|
de plusieurs bugs d'indice, de List.rev, d'oubli d'application de
whd_evar + code plus concis pour l'argument optionnel "filter").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10145 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-----------------------------------------------
- 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
|
|
evdref si evar_defs ref)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
l'unification sur les types (qui nécessite le coûteux hnf_constr pour
la compatibilité) que si le type contient encore des méta (et pour
cela on attend le dernier moment) ou si une coercion est
potentiellement à insérer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau
type d'evar EvarGoal pour raffinement du message d'erreur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
métas permettant de savoir si une instance de méta vient d'un
with-binding ou d'une unification, et si elle a déjà été typée ou pas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
apply afin de reculer au plus tard les décisions irréversibles et en
particulier de pouvoir typer les with-bindings modulo coercions :
- l'unification des types des métas données en with-bindings est
retardé à après l'unification (unify_0) de telle sorte que les
instances trouvées par unify_0 soient prioritaires et que la
décision d'insérer éventuellement des coercions autour des valeurs
données en with-bindings se fasse au dernier moment;
- toujours pour permettre d'insérer ultimement des coercions,
l'instantiation des with-bindings ne se fait plus
l'appel unify_0 (cf clenv_unique_resolver);
- pour permettre ce retardement sans limiter le test de conversion
que unify_0 fait sur les termes clos, on transmet à unify_0 les
métas données en with-bindings (ainsi l'instantiation de ces métas
peut être faite dynamiquement au moment du test de clôture);
- parce que les métas données en with-bindings qui sont en position
de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent
simplifier le problème d'unification (et elles ne sont pas de
toutes façons pas réinférables au premier ordre), on continue à
les substituer avant l'appel à unify_0 (cf meta_reducible_instance);
- pour l'unification du second-ordre, on continue d'instancier les
with-bindings et d'unifier les types des with-bindings avant
unification;
- reste à régler un problème de compatibilité lorsque le résultat de
l'unification des types des with-bindings est utilisé pour rendre
un terme clos et pour permettre à unify_0 d'utiliser la conversion.
+ meilleure compatibilité de apply, split, left, right pour le code
qui l'utilise avec des bindings clos
+ nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
lemme n'est pas un lemme d'induction (plus précisément si la tête de
la conclusion n'est pas une variable), alors on n'instancie pas les
with-bindings pour que les unifications venant du filtrage de la
conclusion du lemme avec le but soient prioritaires (en effet
l'utilisation des types des with-bindings pour inférer des instances
-- portion du commit r9842 -- ne produit pas des solutions exactes
mais seulement des sous-types de solutions exactes alors que
l'unification avec le but produit des solutions exactes qui doivent
donc être considérées en priorité). Toutefois, dans certains cas, du
fait que unify_0 travaille modulo conversion uniquement sur les termes
clos, il faut quand même donner crédit aux instances données en
with-bindings pour que la conversion puisse être prise en compte et
ainsi retrouver un comportement au moins identique au précédent.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de résoudre des buts comme celui-ci :
Record nat_retract : Type :=
{f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
Goal nat_retract.
exists (fun x => x) (fun x => x).
- Nouvelle tentative d'utilisation des types des metas/evars pour
inférer de nouvelles instances de metas/evars; permet par exemple
d'utiliser f_equal sans option with, mais aussi, avec la modif
précédente, de résoudre des buts tels que
Goal exists f:bool->Prop, f true = True.
exists (fun x => True).
[Les expériences passées avaient montré qu'en prenant en compte les
types dans l'unification, on peut unifier trop tôt une evars à une
mauvaise sorte; à défaut de mécanisme de prise en compte des problème
d'unification avec sous-typage, on s'est interdit ici d'unifier des
types qui sont des arités.]
- Tout les constr de tactic_expr deviennent des open_constr (même si seul
with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
obligations (even an opaque one).
Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- ajouts des opérations clear_evar_hyps_in_evar,
clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui
permettent de supprimer des hypothèses dans le contexte des evars,
en créant une nouvelle evar avec un contexte restreint;
- adaptation de clear_hyps dans Logic pour qu'elle mette à jour le
contexte des evars;
- adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié;
- déplacement de la tactique Change_evars dans prim_rule.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
degrés de liberté concernant les instances de méta (cumulativité et
possibilité d'éta-expansion) de telle sorte que la fusion d'équations
se fasse modulo ces degrés de liberté.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9140 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7640 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7121 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
notion de variable de sortes (mais pas encore utilise...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6811 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the new module kernel/mod_subst.ml.
MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- reduction du noyau (variables existentielles, fonctions auxiliaires
pour inventer des noms, etc. deplacees hors de kernel/)
- changement de noms de constructeurs des constr (suppression de "Is" et
"Mut")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
