| Age | Commit message (Collapse) | Author |
|---|
|
- Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml
so as to ease the comparison between these files. Application of a
change that cannot do harm: j_nf_evar now called after getting evd
from consider_remaining_unif_problems in
Subtac_pretyping_F.understand_judgment. Four differences remain
(is it the sign of a problem?):
1) understand_type fails in Pretyping if evars remain but does not fail in
Subtac_pretyping_F
2) resolve_typeclasses (when called) is called with ~onlyargs:false and
~fail:true in Pretyping.understand, Pretyping.understand_gen and
Pretyping.understand_type but with true and false in these same
functions in Subtac_pretyping_F
3) understand_ltac does not call typeclasses in Pretyping but it
does call it in Subtac_pretyping_F
4) understand_judgment does call typeclasses in Pretyping but not in
Subtac_pretyping_F
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Axiom f: (nat->nat)->Prop.
Eval compute in let _ := f(fun _ => mult 1000 1000) in 0.
function was strongly evaluated when applied to f
(based on examples provided by Damien Pous)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
correctly.
- Fix the new autorewrite to implement the (unstated) invariant that the
last declared rules are applied first, which makes a difference for
non-confluent rewrite rules. Some scripts in CoLoR rely on that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to be generalized as they may appear in other arguments or their types.
Try to keep the original names around as well, using the ones found in
the goal. This only requires that interning a pattern [forall x, _]
properly declares [x] as a metavariable, binding instances are already
part of the substitutions computed by [extended_matches].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Type instead of sort variables for unknown levels in unification).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12075 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This commit concerns about the first half of the useless code
mentionned by Oug for coqtop (without plugins). For the moment,
Oug is used in a mode where any elements mentionned in a .mli
is considered to be precious. This already allows to detect and
remove about 600 lines, and more is still to come.
Among the interesting points, the type Entries.specification_entry
and its constructors SPExxx were never used. Large parts of cases.ml
(and hence subtac_cases.ml) were also useless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
it does not cause a time penalty.
- Removing of get_type_of_with_meta made possible by the
evar_defs/evar_map merge.
- Adding unfolding of Meta in reductionops (this assumes that reduction does
not move Metas across binders...)
- Renaming newly created fold_map_rel_context into map_rel_context_in_env.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12061 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Not_found bug in Theorem with) from V8.2 to trunk.
- Improving indentation in presence of tabulation and utf-8 when
reporting error messages with "^^^^^^".
- Updating a few svn:ignore properties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments.
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of new support for dependent "destruct" over terms in dependent types
(r11944): dependencies in evars are not considered to be a cause of
dependent "destruct".
This solves one of the incompatibilities revealed in contribs. The
other one comes from a "destruct_call" on a truly dependent
goal. Fortunately, dependent destruct makes that destruct_call now
works better and the corresponding script can be shortened
(FSetAVL_prog).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12006 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 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
|
|
L'expérience prouve que ce n'est pas franchement concluant.
On peut se risquer à une explication :
- nf_evar, version mémoïsée n'est pas tail recursive
- On retarde la substitution des hypothèses de l'evar en échange de
faire moins de substitutions d'evars. Intuitivement c'est intéressant
seulement si il y a plus de substitutions d'evar dupliquées que
d'hypothèses dupliquées. Ce qui ne doit pas être le cas (ne serait-ce
que parce que dupliquer une evar duplique aussi ses variables libres).
This reverts commit 066a564021788e995eb166ad6ed6e55611d6f593.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11958 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
=20[whd=5Fevar]=20:=20les
=20evar=5Fdefs=20gardent=20un=20cache=20des=20appels=20pr=C3=A9c=C3=A9dents.=20Le=20d=C3=A9faut=20de=20la
=20m=C3=A9thodologie=20est=20que=20=C3=A7a=20int=C3=A9ragit=20assez=20mal=20avec=20la=20substitution=20des
=20hypoth=C3=A8ses=20de=20l'evar=20(qui=20n'est=20pas=20mise=20en=20cache).=20En=20particulier=20les
=20deux=20fonctions=20ne=20sont=20plus=20r=C3=A9cursives=20terminales.=20De=20plus=20un=20appel=20=C3=A0
=20l'une=20des=20deux=20fera=20n=C3=A9cessairement=20un=20parcours=20du=20terme=20pour=20appliquer
=20la=20substitution.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
D'un point de vue de l'effet observer, ça a un effet assez léger sur le
trunk, je suis curieux de voir les effets sur les contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11950 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
d'entiers à ensemble d'entier. A première vue l'optimisation a un effet
négligeable.
Mais vu l'utilisation qui est fait des des last_mods (des mem à
répétition). C'est plus raisonnable ainsi.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11942 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
L'optimisation semble significative.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11941 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
|
|
- commit 11871 (Miller's pattern detection bug) + a corresponding test
- commit 11883 (.ml4 to .cmxs in coq_makefile)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11884 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactics, an unchanged map may have a different adress. Part of the fix
for making Ynot work in 8.2.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11818 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evar-evar problems).
- Fixing target "make programs".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
==========
This big patch is commited here with a HUGE experimental tag on it. It
is probably not a finished job. The aim of committing it now, as
agreed with Hugo, is to get some feedback from potential users to
identify more clearly the directions the implementation could take. So
please feel free to mail me any remarks, bug reports or advices at
<puech@cs.unibo.it>.
Here are the changes induced by it :
For the user
============
* Search tools have been reimplemented to be faster and more
general. Affected are [SearchPattern], [SearchRewrite] and [Search]
(not [SearchAbout] yet). Changes are:
- All of them accept general constructions, and previous syntactical
limitations are abolished. In particular, one can for example
[SearchPattern (nat -> Prop)], which will find [isSucc], but also
[le], [gt] etc.
- Patterns are typed. This means that you cannot search mistyped
expressions anymore. I'm not sure if it's a good or a bad thing
though (especially regarding coercions)...
* New tool to automatically infer (some) Record/Typeclasses instances.
Usage : [Record/Class *Infer* X := ...] flags a record/class as
subject to instance search. There is also an option to
activate/deactivate the search [Set/Unset Autoinstance]. It works
by finding combinations of definitions (actually all kinds of
objects) which forms a record instance, possibly parameterized. It
is activated at two moments:
- A complete search is done when defining a new record, to find all
possible instances that could have been formed with past
definitions. Example:
Require Import List.
Record Infer Monoid A (op:A->A->A) e :=
{ assoc : forall x y z, op x (op y z) = op (op x y) z;
idl : forall x, x = op x e ;
idr : forall x, x = op e x }.
new instance Monoid_autoinstance_1 : (Monoid nat plus 0)
[...]
- At each new declaration (Definition, Axiom, Inductive), a search
is made to find instances involving the new object. Example:
Parameter app_nil_beg : forall A (l:list A), l = nil ++ l.
new instance Build_Monoid_autoinstance_12 :
(forall H : Type, Monoid (list H) app nil) :=
(fun H : Type =>
Build_Monoid (list H) app nil ass_app (app_nil_beg H)
(app_nil_end H))
For the developper
==================
* New yet-to-be-named datastructure in [lib/dnet.ml]. Should do
efficient one-to-many or many-to-one non-linear first-order
filtering, faster than traditional methods like discrimination nets
(so yes, the name of the file should probably be changed).
* Comes with its application to Coq's terms
[pretyping/term_dnet.ml]. Terms are represented so that you can
search for patterns under products as fast as you would do not under
products, and facilities are provided to express other kind of
searches (head of application, under equality, whatever you need
that can be expressed as a pattern)
* A global repository of all objects defined and imported is
maintained [toplevel/libtypes.ml], with all search facilities
described before.
* A certain kind of proof search in [toplevel/autoinstance.ml]. For
the moment it is specialized on finding instances, but it should be
generalizable and reusable (more on this in a few months :-).
The bad news
============
* Compile time should increase by 0 to 15% (depending on the size of
the Requires done). This could be optimized greatly by not
performing substitutions on modules which are not functors I
think. There may also be some inefficiency sources left in my code
though...
* Vo's also gain a little bit of weight (20%). That's inevitable if I
wanted to store the big datastructure of objects, but could also be
optimized some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11792 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Really unify with types of metas when they contain metas
_or_ evars (why not always?) (fixes bug #2027).
- Better handling of evars in rewrite lemmas when using setoid_rewrite
through rewrite (reported by Ralf Hinze).
- Use retyping with metas when possible (check?) and improve an
obscure error message in retyping.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11776 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(detection of Miller's pattern)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11748 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
|
|
- matching_subterm was activating partial_app to true in matches_core even
when no partial_app was expected,
- "match goal" (hence "extended_matches") was called with partial_app
in 8.2 (currently "matches" but not in trunk; what to do with
(legacy) "matches" remains unclear.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11733 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
the naming of hypotheses (especially when doing "case H" with H of
type "{x|P<->Q}" since not unfolding will eventually introduce a name
"i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
of names manipulating type constr_pattern, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inductive types was not taken into account).
- Virtually extended tauto to
- support arbitrary-length disjunctions and conjunctions,
- support arbitrary complex forms of disjunctions and
conjunctions when in the contravariant of an implicative hypothesis,
- stick with the purely propositional fragment and not apply reflexivity.
This is virtual in the sense that it is not activated since it breaks
compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a
way that is closer to the intuitive meaning (forbid dependencies
between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
definition; modified tauto.ml4 so that it works with the current and
the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
automation.
- Permitted to use evars in the intermediate steps of "apply in" (as expected
in the test file apply.v).
- Back on the systematic use of eq_rect (r11697) for implementing
rewriting (some proofs, especially lemma DistOoVv in
Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in
Sophia-Antipolis/Semantics/example2.v are explicitly refering
to the name of the lemmas used for rewriting).
- Fixed at the same time a bug in get_sort_of (predicativity of Set was not
taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unused methods object. Matthieu please review this change (after
monday), I might have introduced a bug in rebuild_instance.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11659 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11655 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixed a virtual bug of unification (ever occurs if w_unify called with
a non-empty context of rel's, which is a priori uncommon).
- Fixed Notation.out test.
- Add better coqide error message in case editor is called on an unnamed file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
<<
Axiom A : nat -> bool.
Definition foo :=
match A 0 with
| true => true
| k => k
end.
Print foo.
>>
[A 0] is duplicated in the [k => k] branch!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11640 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
closed w.r.t. dependencies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 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
|
|
11585)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11590 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk
revision 11300).
- Improved various error messages related to inversion, evars and case
analysis (including the removal of the obsolete dependent/non dependent
distinction).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11560 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
help the type _checking_ anymore (they don't become typing constraints)
but they permit to coerce a subterm in a type. In particular, when
using a VM cast we avoid unneeded, unexpected conversions using the
default machine (oops!). Also remove the corresponding comment in
pretyping and fix the wrong use of casts in toplevel/command: accept
the trouble of using evars. This has the somewhat adverse effect that
when typing casted object we now have no typing constraints (see
e.g. examples in Cases.v)!
Probably, this will be backtracked partially tomorrow as many contribs
can rely on it and the change could make some unifications fail (in
particular with deep coercions). Let's try anyway!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
|
