| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
I think the usage looks cleaner this way.
|
|
|
|
Also extend evarconv to handle frozen evars and flags for delta and
betaiota reduction.
- Make evar_conv unification take a record of flags
- Adds an imitate_defs option to evarsolve, deactivated in first-order unification
- Add a way to call back conv_algo differently on types
- We distinguish comparison of terms and types which might be different
w.r.t. delta reductions allowed (everything for types, controlled for
terms). We keep the with_cs flag even for types, to avoid
incompatibilities (in HoTT's theories/Spaces/No.v, the refine in
No_encode_le_lt would diverge due to trying a default canonical
structure during type verification).
- In evarsolve, do_project_effects checks evar instances now
- Solve evar-evar unification using miller patterns if possible.
- FO heuristic in evarconv
- Do not catch critical exceptions in evarconv
- Force HO matching to abstract toplevel evar args,
This disallows K on them, more compatible with w_unify_to_subterm.
- occur_rigidly improvement, better approx of occur-check.
- K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into
account in apply_on_subterm and evar_conv_x.
This allow implementing a unification without reduction, e.g. for the
fast path of rewrite subterm selection.
- second_order_matching works up-to cumulativity
- pretyping/coercion: now take unification flags as argument
- pretyping/unification: default_occurrence_test takes a frozen_evars set
export elim_flags_evars to compute frozen evars before elim
- evarsolve: fix evar_define doing check in the wrong order,
as conv_algo can trigger the definition of the evar itself,
define it first in the evd.
- w_unify: disallow HO in consider_remaining. Only used in rewrite now
- use evar_abstraction info
- catch second_order_matching NoOccurrence exception in second_order_matching_with_args
- unify_with_heuristics in API
- second_order_matching: thin evars after abstraction to put in the
right env or fail.
|
|
Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.
|
|
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
for the determination of evars that can be turned into obligations.
|
|
This avoids all the side effects associated with the manipulation of an
unresolvable flag. In the new design:
- The evar_map stores a set of evars that are candidates for typeclass
resolution, which can be retrieved and set.
We maintain the invariant that it always contains only undefined
evars.
- At the creation time of an evar (new_evar), we classify it as a
potential candidate of resolution.
- This uses a hook to test if the conclusion ends in a typeclass
application. (hook set in typeclasses.ml)
- This is an approximation if the conclusion is an existential (i.e.
not yet determined). In that case we register the evar as
potentially a typeclass instance, and later phases must consider
that case, dropping the evar if it is not a typeclass.
- One can pass the ~typeclass_candidate:false flag to new_evar to
prevent classification entirely. Typically this is for new goals
which should not ever be considered to be typeclass resolution
candidates.
- One can mark a subset of evars unresolvable later if
needed. Typically for clausenv, and marking future goals as
unresolvable even if they are typeclass goals. For clausenv for
example, after turing metas into evars we first (optionally) try a
typeclass resolution on the newly created evars and only then mark
the remaining newly created evars as subgoals. The intent of the
code looks clearer now.
This should prevent keeping testing if undefined evars are classes
all the time and crawling large sets when no typeclasses are present.
- Typeclass candidate evars stay candidates through
restriction/evar-evar solutions.
- Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new
evar is a candidate. There's a deficiency in the API, in most use
cases of Evd.add we should rather use a:
`Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info)
-> evar_map`
Usually it is only about nf_evar'ing the evar_info's contents, which
doesn't change the evar candidate status.
- Typeclass resolution can now handle the set of candidates
functionally: it always starts from the set of candidates (and not the
whole undefined_map) and a filter on it, potentially splitting it in
connected components, does proof search for each component in an
evar_map with an empty set of typeclass evars (allowing clean
reentrancy), then reinstates the potential remaining unsolved
components and filtered out typeclass evars at the end of
resolution.
This means no more marking of resolvability/unresolvability
everywhere, and hopefully a more efficient implementation in general.
- This is on top of the cleanup of evar_info's currently but can
be made independent.
[typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates
Solve bug in inheritance of flags in evar-evar solutions.
Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook
|
|
|
|
More precisely: the lambda-let-expanded canonical form of branches and
return predicate is considered as part of the structure of a "match"
and is preserved.
|
|
|
|
(Universes and Evd)
|
|
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
|
|
|
|
|
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
|
When restricting an evar with candidates, raise an exception if this
restriction would leave the evar without candidates, i.e. unsolvable.
- evarutil: mark restricted evars as "cleared"
They would otherwise escape being catched by the [advance] function
of clenv, and result in dangling evars not being registered to the shelf.
- engine: restrict_evar marks it cleared, update the future goals
We make the new evar a future goal and remove the old one.
If we did nothing, [unshelve tac] would work correctly as it
uses [Proofview.advance] to find the shelved goals, going through
the cleared evar. But [Unshelve] would fail as it expects only
undefined evars on the shelf and throws away the defined ones.
|
|
Avoid adding the same unification problem twice, module evar instantiation.
|
|
|
|
|
|
This API is a bit strange, I expect it will change at some point.
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
|
|
Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.
This fixes #6313.
Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
|
|
|
|
|
|
|
|
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
|
|
|
|
|
|
|
|
|
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
|
|
|
|
|
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
|
|
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
|
|
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
|
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
|
|
|
Before sometimes there were lists and strings.
|
|
|
