| Age | Commit message (Collapse) | Author |
|---|
|
This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial
changes in the other files, the real changes are in the parent commit.
|
|
|
|
Was PR#366: Univs: fix bug 5208
|
|
|
|
In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.
|
|
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
|
|
|
Was PR#339: Documenting type class options, typeclasses eauto
|
|
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
|
|
|
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
|
We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.
|
|
Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
|
|
|
|
(May it fell in the case mentioned in the inner comment of Exninfo.info?)
|
|
Was PR#337: Fix arguments
|
|
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
|
|
|
Was PR#233: Fix a bug in error printing of unif constraints
|
|
|
|
This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
|
|
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
|
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
|
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
|
|
Adds a compatibility flag so that the behavior of 8.5 can be obtained too.
Original commit:
unification.ml: fix for bug #4763, unif regression
Do not force all remaining conversions problems to be solved after
the _first_ solution of an evar. This was hell to track down, thanks
for the help of Maxime. contribs pass and HoTT too.
|
|
|
|
This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.
A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
|
|
If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.
If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
|
|
When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.
|
|
|
|
|
|
The commit which caused the regression (5ea2539d4a) looks reasonable.
However, it happens that this commit made that unification started in
the #4955 example to follow a path with problems of the form
"proj ?x == ?x" which clearly are unsolvable (both ?x have the same
instance).
We hack the corresponding very permissive occur-check function so that
it is a bit less permissive.
One day, this occur-check function would have to be rewritten in a
more stricter way.
----------------------------------------------------------------------
Extra comments:
I could list several functions for occur check of evars.
Four of them are too strict in the sense that they do not take into
account occurrences of evars which may disappear by reduction, nor
evars which have instances made in such a way that the occur-check is
solvable (as in "fst ?x[y:=(0,0)] = ?x[y:=0]"). These are:
- Termops.occur_evar for clenv, evar_refiner, tactic unification
- syntactic check without any normalization, even on defined evars
- Evarutil.occur_evar_upto for refine and the V82 compatibility mode
- syntactic check without any normalization but inlining of defined evars
- Evarsolve.occur_evar_upto_types for evar_define
- syntactic check without any normalization but inlining of defined evars
- occur-check in the type of evars met
- optimization for not visiting several time the same evar
- Evarsolve.noccur_evar for pattern unification and for inversion of
substitution (evar/evar or evar/term problems)
- syntactic check without any normalization but inlining of defined evars
- occur-check in the type of evars met in arguments of projections
- occur-check in the type of variables met in arguments of projections
- optimization for not visiting several time the same evar
- optimization for not visiting several time the type of the same variable
- note: to go this way, it seems to me that it should check also in
all types which are a cut-formula in the expression
One is much too lax:
- Evarconv.occur_rigidly
- no recursive check except on the types of "forall" and sometimes
in the arguments of an application
- note: there is obviously a large room for refinements without
loosing solutions
|
|
The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
|
|
|
|
|
|
Revert "Inference of return clause: giving uniformly priority to "small inversion"."
This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87.
|
|
|
|
The move to systematically trying small inversion first bumps
sometimes as feared to the weakness of unification (see #5107).
----
Revert "Posssible abstractions over goal variables when inferring match return clause."
This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94.
Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given."
This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548.
Revert "Trying a no-inversion no-dependency heuristic for match return clause."
This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
|
|
|
|
|
|
|
|
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
|
|
Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
|
|
This change exposed bug #4763
|
|
Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
|
|
|
|
Also getting rid of a global side-effect.
|
|
Was PR#263: Fast lookup in named contexts
|
|
|
|
This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
