| Age | Commit message (Collapse) | Author |
|---|
|
(it is a priori optimized but also able to reason modulo equality of
names and modulo alpha-conversion).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes
declared in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
be unified with a (truly) rigid term would need to be able to project
non-atomic arguments of evars what is not done (consider e.g.
"Check (fun m n (H:m+n=n) => ((f_equal _ H) : S (m+n) = S n)).").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13894 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
be unified with a (truly) rigid term.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Made a distinction between truly rigid constructions (Rigid) and
possibly flexible constructions (match/fix/meta, now called
PseudoRigid) that are currently assimilated to rigid by lack of
appropriate study of their flexibility. One day, the flexibility of
these pseudo-rigid constructions will have to considered seriously.
- Removed useless Cast/Cast cases in Rigid/Rigid block (Cast
are removed in advance and LetIn are not considered Rigid).
- Moved LetIn into the MaybeFlexible class.
- Moved the Lambda/Lambda case upwards to factorize the rules for
eta-expansion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13882 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
governed in the latter case by a flag since (useful e.g. for setoid
rewriting which otherwise loops as it is implemented).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).
Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.
Removed obsolete printer mod_self_id from dev/db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Evars of source "ImpossibleCase" that remain undefined at the end of
case analysis are now defined to ID (forall A : Type, A -> A).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evar_map into a map for defined evars and a map for undefined evars.
Even before Spiwack's new proof engine, some Evd.fold were very
costly, e.g. in check_evars or progress_evar_map. With the new proof
engine, undefined evars traversals are apparently even more common (at
least, it improves significantly the complexity of some calls to omega
in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained
by removal of evar_merge in clenv_fchain in commit 13007, arriving to
figures comparable to the 8.3 ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to rawconstr
Also cleaned a bit typing.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12902 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
informative exception if some constraints do not unify.
All calls except one used to raise a less informative exception when the
constraints weren't solved.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1- Management of the name-space in a modular development / sharing of non-logical objects.
2- Performance of atomic module operations (adding a module to the environment, subtyping ...).
1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P
Module M := P.
Module M.
Include P.
...
End M.
Declare Module K : S with Module M := P.
In this 3 cases we don't want to be bothered by the duplication of names.
Of course, M.foo delta reduce to P.foo but many non-logical features of coq
do not work modulo conversion (they use eq_constr or constr_pat object).
To engender a transparent name-space (ie using P.foo or M.foo is the same thing)
we quotient the name-space by the equivalence relation on names induced by the
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo).
So:
*************************************************************************************
* Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values *
*************************************************************************************
Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free
(also for a posteriori declaration of them, ex: a notation on M.foo will be
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.
2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate
several functors then we have bigger vo.
Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inference (see file failure/evar1.v) + fix of some CUMUL problems that
were in the wrong direction. We assume for the fix that ill-typed
unification problems come from subtyping where we don't know yet if a
coercion has to be inserted or not, and hence are of the CUMUL
form. More on suspending problems of the form ?n <= Type or Prop <= ?n
has to be done yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
structures)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
major changes in [w_unify] and the conversion functions used by it to
handle the sort constraints correctly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[base_sort_conv] and revert change in [unify_type].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12153 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[set_eq_sort_variable] for cases where two universes should be equal,
fix [evars_reset_evd] to keep sort constraints and use [whd_sort_var]
directly in [whd_evar].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12149 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort
constraints are thrown away at the end of unification for the moment,
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12120 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Choose one of the possible instances of an evar when considering
remaining unification constraints: otherwise we just do nothing and
some evars remain uninstantiated.
- Normalise the goal w.r.t. evars before subst, to avoid a double vision
problem: the substituted variable appears only in an instance of an evar
and when we try the rewrite it has been substituted making the dependency
disappear.
- Hack to correcly handle let-in annotations which are internalized as
casts: they're really typing constraints. Shouldn't we just change the
AST to have the type at rawconstr let-in nodes?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par Evd). Ça s'accompagne de quelques autres modifications de
l'interface (certaines fonctions étaient des doublons, ou des
conversions entre evar_map et evar_defs).
J'ai modifié un peu la structure de evd.ml aussi, pour éviter des
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai
introduit des sous-modules pour les différentes couches.
Il y a à l'heure actuelle une pénalité en performance assez sévère (due
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique
est correct). Mais fera l'objet de plusieurs optimisations dans les
commits à venir.
Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour
l'instant incapable de comprendre ce qui cause cette erreur. J'espère
qu'on pourra le déterminer rapidement.
Ce commit est le tout premier commit dans le trunk en rapport avec les
évolution futures de la machine de preuve, en vue en particulier
d'obtenir un "vrai refine".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by user) and #2017 (unification pattern test too crude leading to
regression wrt to 8.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
declaring additional conversion problems when unifying the type of an
evar instance and the evar's declared type. Fix the corresponding
conversion heuristic which failed due to (misplaced?) assertions when
faced with general conversion problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un
terme applicatif au moment de tester f u1 .. un = g v1 .. vn au
premier ordre : on revient sur l'algo tel qu'il était avant le
commit 11187.
- Bug #1887 (format récursif cassé à cause de la vérification des idents).
- Nouveau choix de formattage du message "Tactic Failure".
- Nettoyage vocabulaire "match context" -> "match goal" au passage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
canonique que si elle contribue vraiment à une équation canonique,
c'est-à-dire si son argument principal est une evar; sinon on
répercute le comportement historique qui est de préférer le dépliage
du côté droit d'une équation constante/constante.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
majuscule - si pas un ident ou un terme - et se terminent par un point).
Restent quelques utilisations de "error" qui sont liées à des usages internes,
ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(report de 11190 de v8.2 vers trunk). Le code fautif n'était en fait
plus utilisé car les contraintes de la forme ?n[..,x,..,x,..] := x que
ce code analysait sont finalement résolues par une heuristique de
consider_remaining_univ_constraints consistant à reproduire le
comportement de la 8.1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11192 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
canoniques lors d'une unification constante/constante s'apprêtant à
déplier l'une des deux constantes (suggestion des utilisateurs de
structures canoniques), ceci afin de préserver des possibilités
ultérieures de résolution d'evars par équipement en structure
canonique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(résolution entre autres des bugs 1882, 1883, 1884).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
les alias avant de déclarer qu'une evar n'était appliquée qu'à des
variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10956 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
problèmes de filtrage au nivau de consider_remaining_unif_problems
(résoud en particulier le "bug" #1851).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10927 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
du filtrage. Cela permet de détecter les cas impossibles et de simuler
les contraintes d'inversion exprimables sous la forme d'un assignement
des arguments du constructeurs (cf le cas de Vtail dans Bvector.v).
Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi)
avec vi composé uniquement de constructeurs, et que le résultat final
est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on
construit le prédicat
Q:=fun x1 .. xn y =>
match x1 .. xn y with
| v1(z) .. vn(z) t => P(z)
| _ .. _ _ => ?evar-speciale-cas-impossible
end
qui vérifiera bien que Q u1 .. un = P(w1,..,wp).
En raison de limitations de l'unification (on aurait besoin d'eta
conversion pour résoudre des problèmes du genre
"terme rigide == match x with _ => ?evar end", et besoin d'instanciation par
constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"),
je n'ai pas réussi à traiter le cas général.
Aussi, on adopte une stratégie pragmatique consistant à tester
plusieurs prédicats possibles :
- si un type final est donné, on essaie d'abord l'algorithme de
Matthieu et sinon le nouvel algorithme (permet par exemple de traiter
certains cas d'élimination dépendante de Bvector.v),
- s'il n'y a pas de type final, on essaie d'abord le nouvel algo et
sinon, on essaie avec un prédicat sans dépendance (permet de traiter
des cas compliqués comme celui de par cas sur I' dans le fichier
Case13.v de la test-suite).
Dans la pratique, il y a beaucoup de changement dans le code de compile_case.
- Par exemple, la compilation est maintenant toujours appelé avec un
prédicat (là où l'on pouvait avoir None, on a maintenant toujours au
moins une evar).
- En revanche, le membre droit des clauses est maintenant
optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une
branche impossible au moment du calcul du prédicat de retour.
- Aussi, on renonce aux PrLetIn et PrProd dans l'expression du
predicat de retour mais il faut savoir que c'est maintenant la liste
des tomatchs qui spécifie le contexte exact dans lequel le prédicat
de retour est bien typé.
- Et d'autres...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des théorèmes prouvés par récursion ou corécursion mutuelle.
Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
is_fconv et le test d'équations simples (on admettra que is_fconv est
a priori plus efficace pour réduire que nohdbeta -- et de fait, sur
Stalmarck/algoRun, apprec_nohdbeta part en vrille alors que if_fconv
réussit vite).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
