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

refactor(frontends/lean/user_notation): use parser instead of tactic monad

Browse source
This commit is contained in:
Sebastian Ullrich 2017-06-01 18:22:58 +02:00 • committed by Leonardo de Moura
parent 2bb93aa4f9
commit c49f6f7873
2 changed files with 11 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/user_notation.cpp
View file

@ -46,24 +46,21 @@ static environment add_user_notation(environment const & env, name const & d, un
return add_notation(env, notation_entry(is_nud, {notation::transition(tk, notation::mk_ext_action(
[=](parser & p, unsigned num, expr const * args, pos_info const &) -> expr {
lean_assert(num == (is_nud ? 0 : 1));
expr tactic = mk_constant(d);
expr parser = mk_constant(d);
if (!is_nud)
tactic = mk_app(tactic, mk_pexpr_quote(args[0]));
parser = mk_app(parser, mk_pexpr_quote(args[0]));
// `parse (tk c)` arg
tactic = mk_app(tactic, mk_constant(get_unit_star_name()));
parser = mk_app(parser, mk_constant(get_unit_star_name()));
for (expr t = type; is_pi(t); t = binding_body(t)) {
expr arg_type = binding_domain(t);
if (is_app_of(arg_type, get_interactive_parse_name())) {
tactic = mk_app(tactic, parse_interactive_param(p, arg_type));
parser = mk_app(parser, parse_interactive_param(p, arg_type));
} else {
tactic = mk_app(tactic, p.parse_expr(get_max_prec()));
parser = mk_app(parser, p.parse_expr(get_max_prec()));
}
}
tactic = p.elaborate("_user_notation", {}, tactic).first;
tactic_state s = mk_tactic_state_for(p.env(), p.get_options(), "_user_notation", local_context(), dummy);
type_context ctx(p.env());
auto result = tactic::evaluator(ctx, p.get_options())(tactic, s);
return to_expr(tactic::get_result_value(result));
parser = p.elaborate("_user_notation", {}, parser).first;
return to_expr(run_parser(p, parser));
}))}, Var(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true));
}

7
tests/lean/user_notation.lean
View file

@ -1,11 +1,12 @@
open lean (parser)
open lean.parser
open interactive
open tactic
reserve prefix `unquote! `:100
@[user_notation]
to_expr e >>= eval_expr pexpr
meta def unquote_macro (_ : parse $ tk "unquote!") (e : parse lean.parser.pexpr) : parser pexpr :=
↑(to_expr e >>= eval_expr pexpr)
#eval unquote! ``(1 + 1)
@ -19,17 +20,17 @@ private meta def parse_format : string → string → ℕ × pexpr
reserve prefix `format! `:100
@[user_notation]
meta def format_macro (_ : parse $ tk "format!") (s : string) : tactic pexpr :=
let (n, f) := parse_format "" s.reverse in
pure $ n.repeat (λ _ e, expr.lam `_ binder_info.default pexpr.mk_placeholder e) f
meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr :=
#eval format! "a{}c" "b"
-- #eval format! "{} {}" "a" "bla" -- TODO: delayed abstractions issue
reserve infix ` +⋯+ `:65
@[user_notation]
do n₁ ← to_expr e₁ >>= eval_expr nat,
meta def upto_notation (e₁ : parse lean.parser.pexpr) (_ : parse $ tk "+⋯+") (n₂ : ℕ) : parser pexpr :=
do n₁ ← ↑(to_expr e₁ >>= eval_expr nat),
pure $ (n₂+1-n₁).repeat (λ i e, ``(%%e + %%(reflect $ n₁ + i))) ``(0)
#check 1 +⋯+ 10