From c6ec659bf55efd885693fa5529c98ba38d029c97 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Sep 2016 13:30:17 -0700 Subject: [PATCH] feat(frontends/lean): improve 'begin...end' blocks --- library/init/meta/interactive.lean | 160 +++++++++++++++++++++++-- library/init/meta/pexpr.lean | 8 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/begin_end_block.cpp | 133 ++++++++++++++++++-- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 8 ++ src/frontends/lean/tokens.h | 2 + src/frontends/lean/tokens.txt | 2 + src/library/constants.cpp | 60 +++++++++- src/library/constants.h | 15 ++- src/library/constants.txt | 15 ++- src/library/vm/vm_pexpr.cpp | 10 ++ tests/lean/run/auto_quote1.lean | 48 +++++++- 13 files changed, 435 insertions(+), 30 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 9a1e9f1860..887da4e0e8 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -4,26 +4,172 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.meta.tactic +import init.meta.tactic init.meta.rewrite_tactic namespace tactic namespace interactive +namespace types +/- The parser treats constants in the tactic.interactice namespace specially. + The following argument types have special parser support when interactive tactics + are used inside `begin ... end` blocks. -meta def intro (h : name) : tactic unit := -tactic.intro h >> skip + - ident : make sure the next token is an identifier, and + produce the quoted name `t, where t is the next identifier. -meta def apply (q : pexpr) : tactic unit := + - opt_ident : parse (identifier)? + + - using_ident + + - raw_ident_list : parse identifier* and produce a list of quoted identifiers. + + Example: + a b c + produces + [`a, `b, `c] + + - with_ident_list : parse + (`with` identifier+)? + and produce a list of quoted identifiers + - comma_tk : parse the token `,` and produce the unit () + + - location : parse + (`at` identifier+)? + and produce a list of quoted identifiers + + - qexpr : parse an expression e and produce the quoted expression `e + + - qexpr_list : parse + `[` (expr (`,` expr)*)? `]` + + and produce a list of quoted expressions. + + - qexpr0 : parse an expression e using 0 as the right-binding-power, + and produce the quoted expression `e + + - qexpr_list_or_qexpr0 : parse + `[` (expr (`,` expr)*)? `]` + or + expr + + and produce a list of quoted expressions + + - itactic: parse a nested "interactive" tactic -/ +def ident : Type := name +def opt_ident : Type := option ident +def using_ident : Type := option ident +def raw_ident_list : Type := list ident +def with_ident_list : Type := list ident +def location : Type := list ident +@[reducible] meta def qexpr : Type := pexpr +@[reducible] meta def qexpr0 : Type := pexpr +meta def qexpr_list : Type := list qexpr +meta def qexpr_list_or_qexpr0 : Type := list qexpr +meta def itactic : Type := tactic unit +end types + +open types expr + +meta def intro : opt_ident → tactic unit +| none := intro1 >> skip +| (some h) := tactic.intro h >> skip + +meta def intros : raw_ident_list → tactic unit +| [] := tactic.intros >> skip +| hs := intro_lst hs >> skip + +meta def apply (q : qexpr0) : tactic unit := to_expr q >>= tactic.apply -meta def refine : pexpr → tactic unit := +meta def refine : qexpr0 → tactic unit := tactic.refine meta def assumption : tactic unit := tactic.assumption -meta def exact (e : pexpr) : tactic unit := +meta def change (q : qexpr0) : tactic unit := +to_expr_strict q >>= tactic.change + +meta def exact (q : qexpr0) : tactic unit := do tgt : expr ← target, - to_expr_strict `((%%e : %%tgt)) >>= exact + to_expr_strict `((%%q : %%tgt)) >>= tactic.exact + +private meta def get_locals : list name → tactic (list expr) +| [] := return [] +| (n::ns) := do h ← get_local n, hs ← get_locals ns, return (h::hs) + +meta def revert (ids : raw_ident_list) : tactic unit := +do hs ← get_locals ids, revert_lst hs, skip + +/- Return (some a) iff p is of the form (- a) -/ +private meta def is_neg (p : pexpr) : option pexpr := +/- Remark: we use the low-level to_raw_expr and of_raw_expr to be able to + pattern match pre-terms. This is a low-level trick (aka hack). -/ +match pexpr.to_raw_expr p with +| (app (const c []) arg) := if c = `neg then some (pexpr.of_raw_expr arg) else none +| _ := none +end + +private meta def to_symm_expr_list : list pexpr → tactic (list (bool × expr)) +| [] := return [] +| (p::ps) := + match is_neg p with + | some a := do r ← to_expr a, rs ← to_symm_expr_list ps, return ((tt, r) :: rs) + | none := do r ← to_expr p, rs ← to_symm_expr_list ps, return ((ff, r) :: rs) + end + +private meta def rw_goal : list (bool × expr) → tactic unit +| [] := return () +| ((symm, e)::es) := rewrite_core reducible tt occurrences.all symm e >> rw_goal es + +private meta def rw_hyp : list (bool × expr) → name → tactic unit +| [] hname := return () +| ((symm, e)::es) hname := + do h ← get_local hname, + rewrite_at_core reducible tt occurrences.all symm e h, + rw_hyp es hname + +private meta def rw_hyps : list (bool × expr) → list name → tactic unit +| es [] := return () +| es (h::hs) := rw_hyp es h >> rw_hyps es hs + +meta def rewrite (hs : qexpr_list_or_qexpr0) (loc : location) : tactic unit := +do hlist ← to_symm_expr_list hs, + match loc with + | [] := rw_goal hlist >> try reflexivity + | hs := rw_hyps hlist hs >> try reflexivity + end + +meta def rw : qexpr_list_or_qexpr0 → location → tactic unit := +rewrite + +private meta def get_type_name (e : expr) : tactic name := +do e_type ← infer_type e >>= whnf, + (const I ls) ← return $ get_app_fn e_type | failed, + return I + +meta def induction (p : qexpr0) (rec_name : using_ident) (ids : with_ident_list) : tactic unit := +do e ← to_expr p, + match rec_name with + | some n := induction_core semireducible e n ids + | none := do I ← get_type_name e, induction_core semireducible e (I <.> "rec") ids + end + +meta def cases (p : qexpr0) (ids : with_ident_list) : tactic unit := +do e ← to_expr p, + cases_core semireducible e ids + +meta def generalize (p : qexpr) (x : ident) : tactic unit := +do e ← to_expr p, + tactic.generalize e x + +meta def trivial : tactic unit := +tactic.triv <|> tactic.reflexivity <|> tactic.contradiction + +meta def contradiction : tactic unit := +tactic.contradiction + +meta def repeat : itactic → tactic unit := +tactic.repeat end interactive end tactic diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean index 869dfcfcdc..e4e6addce9 100644 --- a/library/init/meta/pexpr.lean +++ b/library/init/meta/pexpr.lean @@ -9,8 +9,12 @@ universe variables u /- Quoted expressions. They can be converted into expressions by using a tactic. -/ meta constant pexpr : Type -protected meta constant pexpr.of_expr : expr → pexpr -protected meta constant pexpr.subst : pexpr → pexpr → pexpr +protected meta constant pexpr.of_expr : expr → pexpr +protected meta constant pexpr.subst : pexpr → pexpr → pexpr + +/- Low level primitives for accessing internal representation. -/ +protected meta constant pexpr.to_raw_expr : pexpr → expr +protected meta constant pexpr.of_raw_expr : expr → pexpr meta constant pexpr.to_string : pexpr → string meta instance : has_to_string pexpr := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index abfae2cb64..a416a70353 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -16,7 +16,7 @@ "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence" "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance" "eval" "vm_eval" "check" "end" "reveal" "this" "suppose" - "using_well_founded" "namespace" "section" "fields" + "using" "using_well_founded" "namespace" "section" "fields" "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class" "instances" "coercions" "attributes" "raw" "replacing" "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun" diff --git a/src/frontends/lean/begin_end_block.cpp b/src/frontends/lean/begin_end_block.cpp index 3c3969f0f8..3ec7f26878 100644 --- a/src/frontends/lean/begin_end_block.cpp +++ b/src/frontends/lean/begin_end_block.cpp @@ -68,32 +68,141 @@ static optional is_tactic_interactive(parser & p) { return optional(); } -static expr parse_auto_quoted_expr(parser & p, unsigned rbp) { +static expr mk_lean_list(buffer const & es) { + expr r = mk_constant(get_list_nil_name()); + unsigned i = es.size(); + while (i > 0) { + --i; + r = mk_app(mk_constant(get_list_cons_name()), es[i], r); + } + return r; +} + +static expr mk_lean_none() { + return mk_constant(get_option_none_name()); +} + +static expr mk_lean_some(expr const & e) { + return mk_app(mk_constant(get_option_some_name()), e); +} + +static expr parse_quoted_ident(parser & p, name const & decl_name) { + if (!p.curr_is_identifier()) + throw parser_error(sstream() << "invalid tactic '" << decl_name << "', identifier expected", p.pos()); + auto pos = p.pos(); + name id = p.get_name_val(); + p.next(); + return p.save_pos(quote_name(id), pos); +} + +static expr parse_optional_quoted_ident(parser & p, name const & decl_name) { + auto pos = p.pos(); + if (p.curr_is_identifier()) + return p.save_pos(mk_lean_some(parse_quoted_ident(p, decl_name)), pos); + else + return p.save_pos(mk_lean_none(), pos); +} + + +static expr parse_using_id(parser & p, name const & decl_name) { + auto pos = p.pos(); + if (p.curr_is_token(get_using_tk())) { + p.next(); + return p.save_pos(mk_lean_some(parse_quoted_ident(p, decl_name)), pos); + } else { + return p.save_pos(mk_lean_none(), pos); + } +} + +static expr parse_qexpr(parser & p, unsigned rbp) { auto pos = p.pos(); parser::quote_scope scope(p, true); expr e = p.parse_expr(rbp); return p.save_pos(mk_quote(e), pos); } +static expr parse_qexpr_list(parser & p) { + buffer result; + auto pos = p.pos(); + p.check_token_next(get_lbracket_tk(), "invalid tactic argument, '[' expected"); + while (!p.curr_is_token(get_rbracket_tk())) { + result.push_back(parse_qexpr(p, 0)); + if (!p.curr_is_token(get_comma_tk())) break; + p.next(); + } + p.check_token_next(get_rbracket_tk(), "invalid tactic argument, ']' expected"); + return p.rec_save_pos(mk_lean_list(result), pos); +} + +static expr parse_qexpr_list_or_qexpr0(parser & p) { + if (p.curr_is_token(get_lbracket_tk())) { + return parse_qexpr_list(p); + } else { + auto pos = p.pos(); + buffer args; + args.push_back(parse_qexpr(p, 0)); + return p.rec_save_pos(mk_lean_list(args), pos); + } +} + +static expr parse_raw_id_list(parser & p) { + auto pos = p.pos(); + buffer result; + while (p.curr_is_identifier()) { + auto id_pos = p.pos(); + name id = p.get_name_val(); + p.next(); + result.push_back(p.save_pos(quote_name(id), id_pos)); + } + return p.rec_save_pos(mk_lean_list(result), pos); +} + +static expr parse_with_id_list(parser & p) { + if (p.curr_is_token(get_with_tk())) { + p.next(); + return parse_raw_id_list(p); + } else { + return p.save_pos(mk_constant(get_list_nil_name()), p.pos()); + } +} + +static expr parse_location(parser & p) { + if (p.curr_is_token(get_at_tk())) { + p.next(); + return parse_raw_id_list(p); + } else { + return p.save_pos(mk_constant(get_list_nil_name()), p.pos()); + } +} + static expr parse_tactic_interactive(parser & p, name const & decl_name) { auto pos = p.pos(); p.next(); expr type = p.env().get(decl_name).get_type(); - unsigned arity = get_arity(type); buffer args; while (is_pi(type)) { if (is_explicit(binding_info(type))) { expr arg_type = binding_domain(type); - if (is_constant(arg_type, get_pexpr_name())) { - /* auto quote expressions */ - expr arg = parse_auto_quoted_expr(p, arity == 1 ? 0 : get_max_prec()); - args.push_back(arg); - } else if (is_constant(arg_type, get_name_name())) { - if (!p.curr_is_identifier()) - throw parser_error(sstream() << "invalid tactic '" << decl_name << "', identifier expected", p.pos()); - name id = p.get_name_val(); - p.next(); - args.push_back(quote_name(id)); + if (is_constant(arg_type, get_tactic_interactive_types_qexpr_name())) { + args.push_back(parse_qexpr(p, get_max_prec())); + } else if (is_constant(arg_type, get_tactic_interactive_types_qexpr0_name())) { + args.push_back(parse_qexpr(p, 0)); + } else if (is_constant(arg_type, get_tactic_interactive_types_qexpr_list_name())) { + args.push_back(parse_qexpr_list(p)); + } else if (is_constant(arg_type, get_tactic_interactive_types_qexpr_list_or_qexpr0_name())) { + args.push_back(parse_qexpr_list_or_qexpr0(p)); + } else if (is_constant(arg_type, get_tactic_interactive_types_ident_name())) { + args.push_back(parse_quoted_ident(p, decl_name)); + } else if (is_constant(arg_type, get_tactic_interactive_types_opt_ident_name())) { + args.push_back(parse_optional_quoted_ident(p, decl_name)); + } else if (is_constant(arg_type, get_tactic_interactive_types_raw_ident_list_name())) { + args.push_back(parse_raw_id_list(p)); + } else if (is_constant(arg_type, get_tactic_interactive_types_with_ident_list_name())) { + args.push_back(parse_with_id_list(p)); + } else if (is_constant(arg_type, get_tactic_interactive_types_using_ident_name())) { + args.push_back(parse_using_id(p, decl_name)); + } else if (is_constant(arg_type, get_tactic_interactive_types_location_name())) { + args.push_back(parse_location(p)); } else { args.push_back(p.parse_expr(get_max_prec())); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 685b03c99f..e56b87bf96 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -89,7 +89,7 @@ void init_token_table(token_table & t) { {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, - {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, + {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"using", 0}, {"@@", g_max_prec}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index a226d38e12..f846e31153 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -39,6 +39,7 @@ static name const * g_turnstile_tk = nullptr; static name const * g_membership_tk = nullptr; static name const * g_explicit_tk = nullptr; static name const * g_partial_explicit_tk = nullptr; +static name const * g_at_tk = nullptr; static name const * g_max_tk = nullptr; static name const * g_imax_tk = nullptr; static name const * g_import_tk = nullptr; @@ -117,6 +118,7 @@ static name const * g_this_tk = nullptr; static name const * g_noncomputable_tk = nullptr; static name const * g_theory_tk = nullptr; static name const * g_key_equivalences_tk = nullptr; +static name const * g_using_tk = nullptr; static name const * g_using_well_founded_tk = nullptr; void initialize_tokens() { g_aliases_tk = new name{"aliases"}; @@ -155,6 +157,7 @@ void initialize_tokens() { g_membership_tk = new name{"∈"}; g_explicit_tk = new name{"@"}; g_partial_explicit_tk = new name{"@@"}; + g_at_tk = new name{"at"}; g_max_tk = new name{"max"}; g_imax_tk = new name{"imax"}; g_import_tk = new name{"import"}; @@ -233,6 +236,7 @@ void initialize_tokens() { g_noncomputable_tk = new name{"noncomputable"}; g_theory_tk = new name{"theory"}; g_key_equivalences_tk = new name{"key_equivalences"}; + g_using_tk = new name{"using"}; g_using_well_founded_tk = new name{"using_well_founded"}; } void finalize_tokens() { @@ -272,6 +276,7 @@ void finalize_tokens() { delete g_membership_tk; delete g_explicit_tk; delete g_partial_explicit_tk; + delete g_at_tk; delete g_max_tk; delete g_imax_tk; delete g_import_tk; @@ -350,6 +355,7 @@ void finalize_tokens() { delete g_noncomputable_tk; delete g_theory_tk; delete g_key_equivalences_tk; + delete g_using_tk; delete g_using_well_founded_tk; } name const & get_aliases_tk() { return *g_aliases_tk; } @@ -388,6 +394,7 @@ name const & get_turnstile_tk() { return *g_turnstile_tk; } name const & get_membership_tk() { return *g_membership_tk; } name const & get_explicit_tk() { return *g_explicit_tk; } name const & get_partial_explicit_tk() { return *g_partial_explicit_tk; } +name const & get_at_tk() { return *g_at_tk; } name const & get_max_tk() { return *g_max_tk; } name const & get_imax_tk() { return *g_imax_tk; } name const & get_import_tk() { return *g_import_tk; } @@ -466,5 +473,6 @@ name const & get_this_tk() { return *g_this_tk; } name const & get_noncomputable_tk() { return *g_noncomputable_tk; } name const & get_theory_tk() { return *g_theory_tk; } name const & get_key_equivalences_tk() { return *g_key_equivalences_tk; } +name const & get_using_tk() { return *g_using_tk; } name const & get_using_well_founded_tk() { return *g_using_well_founded_tk; } } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 3c335a6109..e33f24eb0e 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -41,6 +41,7 @@ name const & get_turnstile_tk(); name const & get_membership_tk(); name const & get_explicit_tk(); name const & get_partial_explicit_tk(); +name const & get_at_tk(); name const & get_max_tk(); name const & get_imax_tk(); name const & get_import_tk(); @@ -119,5 +120,6 @@ name const & get_this_tk(); name const & get_noncomputable_tk(); name const & get_theory_tk(); name const & get_key_equivalences_tk(); +name const & get_using_tk(); name const & get_using_well_founded_tk(); } diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index fb0b41e807..17798833c8 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -34,6 +34,7 @@ turnstile ⊢ membership ∈ explicit @ partial_explicit @@ +at at max max imax imax import import @@ -112,4 +113,5 @@ this this noncomputable noncomputable theory theory key_equivalences key_equivalences +using using using_well_founded using_well_founded diff --git a/src/library/constants.cpp b/src/library/constants.cpp index ddab2fa150..00d9fd7bd5 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -339,11 +339,24 @@ name const * g_sum_inl = nullptr; name const * g_sum_inr = nullptr; name const * g_tactic = nullptr; name const * g_tactic_constructor = nullptr; -name const * g_tactic_interactive = nullptr; name const * g_tactic_step = nullptr; name const * g_tactic_to_expr = nullptr; name const * g_tactic_skip = nullptr; name const * g_tactic_try = nullptr; +name const * g_tactic_interactive = nullptr; +name const * g_tactic_interactive_types_ident = nullptr; +name const * g_tactic_interactive_types_opt_ident = nullptr; +name const * g_tactic_interactive_types_using_ident = nullptr; +name const * g_tactic_interactive_types_ident_list = nullptr; +name const * g_tactic_interactive_types_raw_ident_list = nullptr; +name const * g_tactic_interactive_types_with_ident_list = nullptr; +name const * g_tactic_interactive_types_location = nullptr; +name const * g_tactic_interactive_types_comma_tk = nullptr; +name const * g_tactic_interactive_types_qexpr = nullptr; +name const * g_tactic_interactive_types_qexpr0 = nullptr; +name const * g_tactic_interactive_types_qexpr_list = nullptr; +name const * g_tactic_interactive_types_qexpr_list_or_qexpr0 = nullptr; +name const * g_tactic_interactive_types_itactic = nullptr; name const * g_to_string = nullptr; name const * g_to_int = nullptr; name const * g_to_real = nullptr; @@ -703,11 +716,24 @@ void initialize_constants() { g_sum_inr = new name{"sum", "inr"}; g_tactic = new name{"tactic"}; g_tactic_constructor = new name{"tactic", "constructor"}; - g_tactic_interactive = new name{"tactic", "interactive"}; g_tactic_step = new name{"tactic", "step"}; g_tactic_to_expr = new name{"tactic", "to_expr"}; g_tactic_skip = new name{"tactic", "skip"}; g_tactic_try = new name{"tactic", "try"}; + g_tactic_interactive = new name{"tactic", "interactive"}; + g_tactic_interactive_types_ident = new name{"tactic", "interactive", "types", "ident"}; + g_tactic_interactive_types_opt_ident = new name{"tactic", "interactive", "types", "opt_ident"}; + g_tactic_interactive_types_using_ident = new name{"tactic", "interactive", "types", "using_ident"}; + g_tactic_interactive_types_ident_list = new name{"tactic", "interactive", "types", "ident_list"}; + g_tactic_interactive_types_raw_ident_list = new name{"tactic", "interactive", "types", "raw_ident_list"}; + g_tactic_interactive_types_with_ident_list = new name{"tactic", "interactive", "types", "with_ident_list"}; + g_tactic_interactive_types_location = new name{"tactic", "interactive", "types", "location"}; + g_tactic_interactive_types_comma_tk = new name{"tactic", "interactive", "types", "comma_tk"}; + g_tactic_interactive_types_qexpr = new name{"tactic", "interactive", "types", "qexpr"}; + g_tactic_interactive_types_qexpr0 = new name{"tactic", "interactive", "types", "qexpr0"}; + g_tactic_interactive_types_qexpr_list = new name{"tactic", "interactive", "types", "qexpr_list"}; + g_tactic_interactive_types_qexpr_list_or_qexpr0 = new name{"tactic", "interactive", "types", "qexpr_list_or_qexpr0"}; + g_tactic_interactive_types_itactic = new name{"tactic", "interactive", "types", "itactic"}; g_to_string = new name{"to_string"}; g_to_int = new name{"to_int"}; g_to_real = new name{"to_real"}; @@ -1068,11 +1094,24 @@ void finalize_constants() { delete g_sum_inr; delete g_tactic; delete g_tactic_constructor; - delete g_tactic_interactive; delete g_tactic_step; delete g_tactic_to_expr; delete g_tactic_skip; delete g_tactic_try; + delete g_tactic_interactive; + delete g_tactic_interactive_types_ident; + delete g_tactic_interactive_types_opt_ident; + delete g_tactic_interactive_types_using_ident; + delete g_tactic_interactive_types_ident_list; + delete g_tactic_interactive_types_raw_ident_list; + delete g_tactic_interactive_types_with_ident_list; + delete g_tactic_interactive_types_location; + delete g_tactic_interactive_types_comma_tk; + delete g_tactic_interactive_types_qexpr; + delete g_tactic_interactive_types_qexpr0; + delete g_tactic_interactive_types_qexpr_list; + delete g_tactic_interactive_types_qexpr_list_or_qexpr0; + delete g_tactic_interactive_types_itactic; delete g_to_string; delete g_to_int; delete g_to_real; @@ -1432,11 +1471,24 @@ name const & get_sum_inl_name() { return *g_sum_inl; } name const & get_sum_inr_name() { return *g_sum_inr; } name const & get_tactic_name() { return *g_tactic; } name const & get_tactic_constructor_name() { return *g_tactic_constructor; } -name const & get_tactic_interactive_name() { return *g_tactic_interactive; } name const & get_tactic_step_name() { return *g_tactic_step; } name const & get_tactic_to_expr_name() { return *g_tactic_to_expr; } name const & get_tactic_skip_name() { return *g_tactic_skip; } name const & get_tactic_try_name() { return *g_tactic_try; } +name const & get_tactic_interactive_name() { return *g_tactic_interactive; } +name const & get_tactic_interactive_types_ident_name() { return *g_tactic_interactive_types_ident; } +name const & get_tactic_interactive_types_opt_ident_name() { return *g_tactic_interactive_types_opt_ident; } +name const & get_tactic_interactive_types_using_ident_name() { return *g_tactic_interactive_types_using_ident; } +name const & get_tactic_interactive_types_ident_list_name() { return *g_tactic_interactive_types_ident_list; } +name const & get_tactic_interactive_types_raw_ident_list_name() { return *g_tactic_interactive_types_raw_ident_list; } +name const & get_tactic_interactive_types_with_ident_list_name() { return *g_tactic_interactive_types_with_ident_list; } +name const & get_tactic_interactive_types_location_name() { return *g_tactic_interactive_types_location; } +name const & get_tactic_interactive_types_comma_tk_name() { return *g_tactic_interactive_types_comma_tk; } +name const & get_tactic_interactive_types_qexpr_name() { return *g_tactic_interactive_types_qexpr; } +name const & get_tactic_interactive_types_qexpr0_name() { return *g_tactic_interactive_types_qexpr0; } +name const & get_tactic_interactive_types_qexpr_list_name() { return *g_tactic_interactive_types_qexpr_list; } +name const & get_tactic_interactive_types_qexpr_list_or_qexpr0_name() { return *g_tactic_interactive_types_qexpr_list_or_qexpr0; } +name const & get_tactic_interactive_types_itactic_name() { return *g_tactic_interactive_types_itactic; } name const & get_to_string_name() { return *g_to_string; } name const & get_to_int_name() { return *g_to_int; } name const & get_to_real_name() { return *g_to_real; } diff --git a/src/library/constants.h b/src/library/constants.h index 8cceea200b..076a719f03 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -341,11 +341,24 @@ name const & get_sum_inl_name(); name const & get_sum_inr_name(); name const & get_tactic_name(); name const & get_tactic_constructor_name(); -name const & get_tactic_interactive_name(); name const & get_tactic_step_name(); name const & get_tactic_to_expr_name(); name const & get_tactic_skip_name(); name const & get_tactic_try_name(); +name const & get_tactic_interactive_name(); +name const & get_tactic_interactive_types_ident_name(); +name const & get_tactic_interactive_types_opt_ident_name(); +name const & get_tactic_interactive_types_using_ident_name(); +name const & get_tactic_interactive_types_ident_list_name(); +name const & get_tactic_interactive_types_raw_ident_list_name(); +name const & get_tactic_interactive_types_with_ident_list_name(); +name const & get_tactic_interactive_types_location_name(); +name const & get_tactic_interactive_types_comma_tk_name(); +name const & get_tactic_interactive_types_qexpr_name(); +name const & get_tactic_interactive_types_qexpr0_name(); +name const & get_tactic_interactive_types_qexpr_list_name(); +name const & get_tactic_interactive_types_qexpr_list_or_qexpr0_name(); +name const & get_tactic_interactive_types_itactic_name(); name const & get_to_string_name(); name const & get_to_int_name(); name const & get_to_real_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 2db019ebfc..c126af1578 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -334,11 +334,24 @@ sum.inl sum.inr tactic tactic.constructor -tactic.interactive tactic.step tactic.to_expr tactic.skip tactic.try +tactic.interactive +tactic.interactive.types.ident +tactic.interactive.types.opt_ident +tactic.interactive.types.using_ident +tactic.interactive.types.ident_list +tactic.interactive.types.raw_ident_list +tactic.interactive.types.with_ident_list +tactic.interactive.types.location +tactic.interactive.types.comma_tk +tactic.interactive.types.qexpr +tactic.interactive.types.qexpr0 +tactic.interactive.types.qexpr_list +tactic.interactive.types.qexpr_list_or_qexpr0 +tactic.interactive.types.itactic to_string to_int to_real diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp index 969dda080f..84c1245ff8 100644 --- a/src/library/vm/vm_pexpr.cpp +++ b/src/library/vm/vm_pexpr.cpp @@ -30,10 +30,20 @@ vm_obj pexpr_to_string(vm_obj const & e) { return expr_to_string(e); } +vm_obj pexpr_to_raw_expr(vm_obj const & e) { + return e; +} + +vm_obj pexpr_of_raw_expr(vm_obj const & e) { + return e; +} + void initialize_vm_pexpr() { DECLARE_VM_BUILTIN(name({"pexpr", "subst"}), pexpr_subst); DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}), pexpr_of_expr); DECLARE_VM_BUILTIN(name({"pexpr", "to_string"}), pexpr_to_string); + DECLARE_VM_BUILTIN(name({"pexpr", "of_raw_expr"}), pexpr_of_raw_expr); + DECLARE_VM_BUILTIN(name({"pexpr", "to_raw_expr"}), pexpr_to_raw_expr); } void finalize_vm_pexpr() { diff --git a/tests/lean/run/auto_quote1.lean b/tests/lean/run/auto_quote1.lean index 6b2ab1db87..f03fa2a5ab 100644 --- a/tests/lean/run/auto_quote1.lean +++ b/tests/lean/run/auto_quote1.lean @@ -1,6 +1,6 @@ example (a b c : nat) : a = b → b = c → c = a := begin - tactic.intros, + intros, apply eq.symm, apply eq.trans, assumption, @@ -14,3 +14,49 @@ begin refine eq.symm (eq.trans h1 _), exact h2 end + +example (a b c : nat) : a = b → b = c → c = a := +begin + intros h1 h2, -- we can optionally provide the names + refine eq.symm (eq.trans h1 _), + exact h2 +end + +example (a b c : nat) : a = b → b = c → c = a := +begin + intro h1, + intro, -- optional argument + refine eq.symm (eq.trans h1 _), + assumption +end + +constant add_comm {a b : nat} : a + b = b + a +constant add_assoc {a b c : nat} : (a + b) + c = a + (b + c) +constant zero_add (a : nat) : 0 + a = a + +example (a b c : nat) : b = 0 → 0 + a + b + c = c + a := +begin + intro h, + rewrite h, -- single rewrite + rewrite [zero_add, @add_comm a 0, zero_add, add_comm] -- sequence of rewrites +end + +example (a b c : nat) : 0 = b → 0 + a + b + c = c + a := +begin + intro h, + rewrite -h, -- single rewrite using symmetry + rw [zero_add, @add_comm a 0, zero_add, add_comm] -- rw is shorthand for rewrite +end + +open nat + +example : ∀ n m : ℕ, n + m = m + n := +begin + intros n m, + induction m with m' ih, + { -- Remark: Used change here to make sure nat.zero is replaced with polymorphic zero. + -- dsimp tactic should fix that in the future. + change n + 0 = 0 + n, rw zero_add n }, + { change succ (n + m') = succ m' + n, + rw [succ_add, ih] } +end