| Age | Commit message (Collapse) | Author |
|---|
|
|
|
By separating the libobject for create db and other hints we can unify
handling of local/superglobal.
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
|
|
|
|
The prepare_hint function was trying to requantify over all undefined evars,
but actually this should not happen when defining generic terms as hints through
some Hint vernacular command.
|
|
|
|
|
|
We know statically that only global references are passed to make_resolves.
|
|
It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
|
|
We move the "verbose" case to the only point it is actually used.
It is a bit unfortunate since it implies a bit of code duplication, but
this should not affect runtime since the replaying only happens in case
of a user-facing warning.
|
|
We know statically that it is going to be the one provided at the time of
lookup, so we simply fetch it from there.
|
|
|
|
The two implementations are essentially the same except for potential
interleaving of let-bindings and pattern-matchings. The only place
the removed function was called probably does not rely on this difference
of behaviour.
|
|
Instead of having to go through the pattern translation, we compute the
pattern directly from the term.
|
|
|
|
Due to the way transparency is handled in hint databases, every time it is
changed, all dnets are recomputed from scratch. This is very expensive, and
a bench showed that it was sometimes contributing significantly to the whole
compilation time of hint-heavy libraries. This patch makes this computation
lazy, so that the dnet is computed only the first time a hint lookup is
performed.
The implementation is functionally equivalent to wrapping the sentry_bnet
field in a Lazy.t, but because dnets are stored in the summary and thus
marshalled, I had to manually perform a defunctionalization.
A (maybe cleaner?) alternative would be to track the set of constants a
hint depend on, in order to only refresh those touched by the change of
transparency. Yet, this would be a much more invasive change.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.
|
|
|
|
|
|
The old API was taking a function to decompose constr patterns into dnet
patterns, but it was applying it in an eager way. So there is not point in
exposing such a complex interface. Instead, we make explicit the dnet pattern
type, export a function that turns a constr pattern into a dnet pattern, and
make the add and remove dnet functions take a dnet pattern instead.
This only affects pattern-consuming functions. The lookup function, which
operates on kernel terms instead of constr patterns, is still relying on HO
primitives.
|
|
|
|
It is only used for this kind of hints, never for Extern / Unfold.
|
|
|
|
The only use was seemingly a bug introduced in 0aec9033a by an accidental
variable capture. There is indeed no reason that the set of variables of a
hint corresponds to the one of the current environment.
|
|
|
|
|
|
They are always the same.
|
|
This allows to remove internal API from the mli as well.
|
|
Current backtraces for tactics leave a bit to desire, for example
given the program:
```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```
the backtrace stops at:
```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.
The backtrace for the failed rewrite is now:
```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
which IMO is much better.
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
