| Age | Commit message (Collapse) | Author |
|---|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
|
|
universes are declared correctly in the enclosing proofs evar_map's.
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
Let merge_context_set be lenient when merging the context of side
effects of an entry from solve_by_tac.
|
|
- Fix union of universe contexts to keep declarations
- Fix side-effect handling to register new global universes
in the graph.
|
|
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
Evars already had their own extensible state, but adding it globally allows
to write out extensible state-passing code in e.g. plugins. The additional
data is hopefully transparently preserved by the code out there. Trespassers
ought to be prosecuted.
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
|
|
progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
|
|
Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.
|
|
to display by default (see bc8a5357889 - 17 Oct 2014):
- not printing instances for let-in anymore even when expanded (since
they are canonical up to conversion)
- still printing x:=x in [x:=x;x':=x] when x is directly an instance
of another var, but not in [x:=x;x':=S x]
This can be discussed, but if ever this is to be changed, it should
not be printed in [x:=x;x:=?n] with ?n implicitly depending on x
(otherwise said, variables which are not displayed in instances of
internal evars should not contribute to the decision of writing
x:=x in the instance).
|
|
|
|
printing functions touched in the kernel).
|
|
|
|
types: we downcast the evar in the higher type to the lower type.
Then, we have the freedom to choose the order of instantiation
according to the instances of the evars (e.g. choosing the
instantiation for which pattern-unification is possible, if ever it is
possible in only one way - as shown by an example in contribution
Paco).
This still does not preserve compatibility because it happens that
type classes resolution is crucially dependent on the order of
presentation of the ?n=?p problems. Consider e.g. an example taken
from Containers. Both now and before e2fa65fccb9, one has this asymmetry:
Context `{Helt : OrderedType elt}.
Check forall x y r l h, @Equivalence.equiv _ _ _ x y -> In x (Node l x r h).
--> @Equivalence.equiv QArith_base.Q QArith_base.Qeq QArith_base.Q_Setoid x y
Context `{Helt : OrderedType elt}.
Check forall x y r l h, In x (Node l x r h) -> @Equivalence.equiv _ _ _ x y.
--> @Equivalence.equiv elt (@_eq elt Helt) (@OT_Equivalence elt Helt)
Then, embedding this example within a bigger one which relies on the
?n=?n' resolution order, one can get two incompatible resolution of
the same problem.
To be continued...
|
|
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
|
|
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
|
eager meta substition in w_unify, so as to preserve compatibility
after PMP's move of (setoid) rewrite clauses from metas to
evars (fbbe491cfa).
Hoping it is compatible for non-rewrite uses of the eager meta flag,
and that it is not too costly.
|
|
|
|
|
|
Its semantics was dubious, and it was not used anymore anyway.
|
|
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
|
|
In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.
|
|
See previous commit for more discussion.
Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.
|
|
That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct.
It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though.
Following a suggestion by Hugo.
|
|
another one.
|
|
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
|
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
|
|
with existing ML code.
|
|
|
|
equality of universes, along with a few other functions in evd.
|
|
|
|
|
|
in instances.
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
for typeclass errors.
|
|
of the universe context in the obligations, it gets gradually fixed
globally by each one of them.
Fixes bug found in Misc/Overloading.
|
|
variable
as algebraic so it can disappear from the proof (it always gets substituted away from
the term). This means less spurious universes remaining in proof terms.
|
|
for helping fixing this).
Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
|
|
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|
|
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
|
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
|
|
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
|
|
evar_map
in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).
|
