max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/elaborator): bug at @@ annotation

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-15 17:03:59 -07:00
parent f8fbc95e29
commit f60de96d98
3 changed files with 20 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/elaborator.cpp
View file

@ -1000,7 +1000,7 @@ expr elaborator::visit_default_app_core(expr const & _fn, arg_mask amask, buffer
if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size())
break;
if ((amask == arg_mask::Default && !is_explicit(bi)) ||
(amask == arg_mask::Simple && !bi.is_inst_implicit() && !is_first_order(d))) {
(amask == arg_mask::InstHoExplicit && !is_explicit(bi) && !bi.is_inst_implicit() && !is_pi(d))) {
// implicit argument
if (bi.is_inst_implicit())
new_arg = mk_instance(d, ref);
@ -1191,7 +1191,7 @@ expr elaborator::visit_no_confusion(expr const & fn, buffer<expr> const & args,
new_args.push_back(copy_tag(args[0], mk_as_is(Heq)));
for (unsigned i = 1; i < args.size(); i++)
new_args.push_back(args[i]);
return visit_default_app_core(fn, arg_mask::All, new_args, false, expected_type, ref);
return visit_default_app_core(fn, arg_mask::AllExplicit, new_args, false, expected_type, ref);
}
expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type,
@ -1199,10 +1199,10 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
arg_mask amask = arg_mask::Default;
if (is_explicit(fn)) {
fn = get_explicit_arg(fn);
amask = arg_mask::All;
amask = arg_mask::AllExplicit;
} else if (is_partial_explicit(fn)) {
fn = get_partial_explicit_arg(fn);
amask = arg_mask::Simple;
amask = arg_mask::InstHoExplicit;
}
bool has_args = !args.empty();

4
src/frontends/lean/elaborator.h
View file

@ -25,8 +25,8 @@ public:
private:
typedef std::vector<pair<expr, expr>> to_check_sorts;
enum class arg_mask {
All /* @ annotation */,
Simple /* @@ annotation */,
AllExplicit /* @ annotation */,
InstHoExplicit, /* @@ annotation (i.e., instance implicit and higher-order arguments are explicit */
Default /* default behavior */
};
environment m_env;

14
tests/lean/run/at_at_bug.lean Normal file
View file

@ -0,0 +1,14 @@
set_option new_elaborator true
example (a b : nat) (p : nat → nat → Prop) (h₁ : p a b) (h₂ : a = b) : p b b :=
@@eq.subst (λ x, p x b) h₂ h₁
set_option pp.all true
variable my_has_add : has_add nat
check @@add my_has_add 0 1
local notation h1 `▸[` m `]` h2 := @@eq.subst m h1 h2
example (a b : nat) (p : nat → nat → Prop) (h₁ : p a b) (h₂ : a = b) : p b b :=
h₂ ▸[λ x, p x b] h₁