The dependent eliminator for an inductive predicate C is called C.drec
TODO: construct dcases_on and drec_on using C.drec
We need this recursor for implementing dependent elimination for
inductive predicates.
We don't need to define acc.drec and eq.drec in the standard library anymore.
The peformance problem was affecting theorems that contain many `intro`
tactic applications.
@gebner After this optimization, the GAPT benchmark elaboration time went from
1.6 secs to 0.6 secs.
We cannot assume both source and target are binding expressions.
The source has already been elaborated, and it may be a `sorry` because
of error recovery code.
This is a hard coded extra case. It is not an instance of has_coe.
Even if we change has_coe to accomodate this case, it will not be a
satisfactory solution because this coercion depends on the element and
not the type, and the element usually contains metavariables.
We should eventually write a tactic for synthesizing coercions.
Summary:
We minimize the number of "'sorry' used warning messages". We also
re-target the error to the main declaration. Example: foo._main ==> foo
We do not report for auxiliary declarations such as "_example" and
"foo.equations._eqn_1"
Get rid of the redundant error message "error : failed" for tactics.
We added "silent failures" in the tactic framework.
We do not store line/col information for tactics nested in notation
declarations. Before this commit, we would have tactics such
as (tactic.save_info line col) nested inside of notation declarations.
Fixes#1363
After error recovery has been implemented in the elaborator, a few
assumptions made in the type context are not valid anymore since we may
be recovering from errors, and the local and metavariable contexts may
be invalid.
I used the approach used in the class environment.
- find* methods return optional<...>
- get* methods throw exception for unknown elements
Remarks:
I preserved code patterns such as
optional<local_decl> d = lctx.find_local_decl(...)
lean_assert(d)
and did not convert them into
local_decl d = lctx.get_local_decl(...)
Reason: the intention is clear that the local must be defined there.
If it is not we should analyze the problem and decide whether we should
throw an exception or not.
However, I converted code patterns such as
local_decl d = *lctx.find_local_decl(...)
into
local_decl d = lctx.get_local_decl(...)
Disclaimer: this change fixes issue #1363, but it may obfuscate other bugs.
@johoelzl We now produce a better message for your example:
inductive R : ℕ → Prop
| pos : ∀p n, R (p + n)
lemma R_id : ∀n, R n → R n
| (.p + .n) (R.pos p n) := R.pos p n
The new error is:
file.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
.p + .n
For example, the following definition did not work before this commit:
protected meta def map {α β} (f : α → β) : lazy_tactic α → lazy_tactic β
| t s := (t s)^.for (λ ⟨a, new_s⟩, (f a, new_s))
(Type u) is the old (Type (u+1))
(PType u) is the old (Type u)
Type* is the old (Type (_+1))
PType* is the old Type*
The stdlib can be compiled, but we still have > 70 broken tests
See discussion at #1341
After this commit, new interactice tactic classes can be added without
writing C++ code (see example: tests/lean/run/my_tac_class.lean).
The tactic_evaluator was simplified, and all the complexity has been
moved to tactic_notation, and lean code.
We can now inspect the intermediate states produced by the rewrite
tactic.
The function (@scope_trace _ line col thunk) can be used to position trace
messages produced by thunk. If line/col are not provided (i.e., we
just write (scope_trace thunk)), then line/col are filled with the
position of this term by the elaborator.
We can visualize the intermediate tactic states inside nested blocks
such as (try { ... })
The new infrastructure can be used to implement custom tactic_state
pretty printers.
@semorrison this commit improves the bad error message you have
reported at lean-user. It is not perfect since the user has to
remember the position of the structure field in the constructor.
