| Age | Commit message (Collapse) | Author |
|---|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
|
|
We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.
|
|
Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.
In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.
Fixes #13896: cbn very slow.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
|
|
|
|
|
|
We compute earlier if "apply in" clears or not.
We inline prepare_naming into its only client prepare_intros_opt
(using the more general make_naming instead).
|
|
We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.
|
|
|
|
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.
|
|
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
We move bind_red_expr_occurrences from Tactics to Redexpr, where it
semantically belongs. We also hide it and seal the corresponding evaluated
types.
|
|
This was a source of slowdown observed in bedrock2.
|
|
incrementally.
The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
|
|
|
|
|
|
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
|
|
In case we give an empty list of occurrences to e_change_in_hyps, we
can return immediately. This saves the allocation of a dummy evar, and
a O(n) map over the context for "local" reduction functions.
Note that passing an empty list of hypotheses is the default for both
the "change" tactic and reduction tactics.
|
|
from initial evars
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
comment in #12944).
Ack-by: RalfJung
Ack-by: jashug
Reviewed-by: ppedrot
|
|
The test is refined to handle aliases: i.e. undefined evars coming from
restrictions and evar-evar unifications with an initial evar are not
considered fresh unresolved evars. To check this, we generalize the
restricted_evars set to an aliased_evars set in the evar map,
registering evars being solved by another evar due to restriction
or evar-evar unifications. This implements the proposal of PR #370
for testing the resolution status of evars independently of the evar-evar
orientation order.
This allows [apply] to refine an evar with a new one if it results from a
[clear] request or an evar-evar solution only, otherwise the new evar is
considered fresh and an error is raised.
Also fixes bugs #4095 and #4413.
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
|
|
Reviewed-by: herbelin
|
|
The code below checks that the term is an applied equality, so allowing
non-trivially quantified inductive types would trigger an error right after.
|
|
Fix #12944
|
|
The names computed in consume_pattern were lost when calling
intros_pattern_core. Moreover, the computation of names to avoid was
done several time. We compute it once for all.
|
|
No reason to have them there.
|
|
This is a footgun as it can refresh the name. Callers can still ignore
the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
|
|
|
|
|
|
|
|
|
|
|
|
This reduces the combinatorial complexity of the function, and the code size
as well.
|
|
|
|
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
All calls to this function are now factorized through Clenvtac.res_pf.
|
|
|
|
|
|
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.
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
|
