diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean index 06c3c2e137..72ffe87855 100644 --- a/library/init/meta/interaction_monad.lean +++ b/library/init/meta/interaction_monad.lean @@ -30,6 +30,11 @@ meta instance interaction_monad.result_has_string : has_to_string (result state ⟨interaction_monad.result_to_string⟩ end +meta def interaction_monad.result.clamp_pos {state : Type} {α : Type u} (line col : ℕ) : result state α → result state α +| (success a s) := success a s +| (exception msg (some pos) s) := exception msg (some $ if pos^.line < line then ⟨line, col⟩ else pos) s +| (exception msg none s) := exception msg (some ⟨line, col⟩) s + @[reducible] meta def interaction_monad (state : Type) (α : Type u) := state → result state α diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 58118cc673..a5758edcde 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -22,12 +22,7 @@ meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit := tac >> solve_goals meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit := -λ ss ts, @scope_trace _ line col ((tac >> solve_goals) ss ts) - -meta def rstep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit := -λ ss ts, result.cases_on (istep line col tac ss ts) - (λ ⟨a, new_ss⟩ new_ts, result.success ((), new_ss) new_ts) - (λ msg_thunk e, tactic.report_exception line col msg_thunk) +λ ss ts, (@scope_trace _ line col ((tac >> solve_goals) ss ts))^.clamp_pos line col meta def execute (tac : smt_tactic unit) : tactic unit := using_smt tac diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index f8a512b619..e492ef6959 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -435,7 +435,6 @@ meta constant decl_name : tactic name /- (save_type_info e ref) save (typeof e) at position associated with ref -/ meta constant save_type_info : expr → expr → tactic unit meta constant save_info_thunk : pos → (unit → format) → tactic unit -meta constant report_error : nat → nat → format → tactic unit /-- Return list of currently open namespaces -/ meta constant open_namespaces : tactic (list name) /-- Return tt iff `t` "occurs" in `e`. The occurrence checking is performed using @@ -461,21 +460,8 @@ get_goals >>= set_goals meta def step {α : Type u} (t : tactic α) : tactic unit := t >>[tactic] cleanup -meta def istep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit := -λ s, @scope_trace _ line col ((t >>[tactic] cleanup) s) - -meta def report_exception {α : Type} (line col : nat) : option (unit → format) → tactic α -| (some msg_thunk) := λ s, - let msg := msg_thunk () ++ format.line ++ to_fmt "state:" ++ format.line ++ s^.to_format in - (tactic.report_error line col msg >> silent_fail) s -| none := silent_fail - -/- Auxiliary definition used to implement begin ... end blocks. - It is similar to step, but it reports an error at the given line/col if the tactic t fails. -/ -meta def rstep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic unit := -λ s, result.cases_on (istep line col t s) - (λ a new_s, result.success () new_s) - (λ msg_thunk e, report_exception line col msg_thunk) +meta def istep {α : Type u} (line col : ℕ) (t : tactic α) : tactic unit := +λ s, (@scope_trace _ line col (step t s))^.clamp_pos line col meta def is_prop (e : expr) : tactic bool := do t ← infer_type e, diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp index b837fa8490..878e287949 100644 --- a/src/frontends/lean/tactic_evaluator.cpp +++ b/src/frontends/lean/tactic_evaluator.cpp @@ -18,9 +18,12 @@ Author: Leonardo de Moura #include "frontends/lean/tactic_notation.h" namespace lean { +static format mk_tactic_error_msg(tactic_state const & ts, format const & fmt) { + return fmt + line() + format("state:") + line() + ts.pp(); +} + elaborator_exception unsolved_tactic_state(tactic_state const & ts, format const & fmt, expr const & ref) { - format msg = fmt + line() + format("state:") + line() + ts.pp(); - return elaborator_exception(ref, msg); + return elaborator_exception(ref, mk_tactic_error_msg(ts, fmt)); } elaborator_exception unsolved_tactic_state(tactic_state const & ts, char const * msg, expr const & ref) { @@ -37,13 +40,12 @@ elaborator_exception unsolved_tactic_state(tactic_state const & ts, char const * void tactic_evaluator::process_failure(vm_state & S, vm_obj const & r) { if (optional ex = tactic::is_exception(S, r)) { - format fmt = std::get<0>(*ex); - optional pos = std::get<1>(*ex); - tactic_state s1 = std::get<2>(*ex); - if (pos) - throw elaborator_exception(pos, fmt); - else - throw_unsolved_tactic_state(s1, fmt, m_ref); + auto msg = mk_tactic_error_msg(std::get<2>(*ex), std::get<0>(*ex)); + if (optional pos = std::get<1>(*ex)) { + throw elaborator_exception(pos, msg); + } else { + throw elaborator_exception(m_ref, msg); + } } /* Do nothing if it is a silent failure */ lean_assert(tactic::is_silent_exception(r)); diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 580145192c..38875e2661 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -39,10 +39,7 @@ Author: Leonardo de Moura 4) (Optional) Tac.istep {α : Type} (line : nat) (col : nat) (tac : Tac α) : Tac unit Similar to step but it should scope trace messages at the given line/col, - - 5) (Optional) Tac.rstep {α : Type} (line : nat) (col : nat) (tac : Tac α) (r : bool) : Tac unit - Extended step. It should scope trace messages at the given line/col, - and report error at line/col if r is tt. + and ensure that the exception position is after (line, col) 6) There is a definition Tac.save_info (line col : nat) : Tac unit @@ -64,27 +61,20 @@ static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name cons return p.save_pos(mk_app(mk_constant(step_name), tac), pos); } -static expr mk_tactic_rstep(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool report_error) { +static expr mk_tactic_istep(parser &p, expr tac, pos_info const &pos, name const &tac_class) { if (p.in_notation()) return mk_tactic_step(p, tac, pos, tac_class); if (tac.get_tag() == nulltag) tac = p.save_pos(tac, pos); - name c; - if (report_error) { - c = name(tac_class, "rstep"); - if (!p.env().find(c)) - c = name(tac_class, "istep"); - } else { - c = name(tac_class, "istep"); - } + name c(tac_class, "istep"); if (!p.env().find(c)) return mk_tactic_step(p, tac, pos, tac_class); return p.save_pos(mk_app(mk_constant(c), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second)), tac), pos); } -static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) { - if (use_rstep) - return mk_tactic_rstep(p, tac, pos, tac_class, report_error); +static expr mk_tactic_step(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_istep) { + if (use_istep) + return mk_tactic_istep(p, tac, pos, tac_class); else return mk_tactic_step(p, tac, pos, tac_class); } @@ -100,7 +90,7 @@ static expr mk_tactic_save_info(parser & p, pos_info const & pos, name const & t return p.save_pos(mk_app(mk_constant(save_info_name), pos_e), pos); } -static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) { +static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_istep) { if (tac.get_tag() == nulltag) tac = p.save_pos(tac, pos); name solve1_name(tac_class, "solve1"); @@ -108,8 +98,8 @@ static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name co throw parser_error(sstream() << "invalid tactic class '" << tac_class << "', '" << tac_class << ".solve1' has not been defined", pos); expr r = p.save_pos(mk_app(mk_constant(solve1_name), tac), pos); - if (use_rstep) - r = mk_tactic_rstep(p, r, pos, tac_class, report_error); + if (use_istep) + r = mk_tactic_istep(p, r, pos, tac_class); return r; } @@ -130,14 +120,14 @@ static optional is_interactive_tactic(parser & p, name const & tac_class) return optional(); } -static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error); +static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_istep); -static expr parse_nested_interactive_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) { +static expr parse_nested_interactive_tactic(parser & p, name const & tac_class, bool use_istep) { auto pos = p.pos(); if (p.curr_is_token(get_lcurly_tk())) { - return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_rstep, report_error); + return parse_begin_end_block(p, pos, get_rcurly_tk(), tac_class, use_istep); } else if (p.curr_is_token(get_begin_tk())) { - return parse_begin_end_block(p, pos, get_end_tk(), tac_class, use_rstep, report_error); + return parse_begin_end_block(p, pos, get_end_tk(), tac_class, use_istep); } else { throw parser_error("invalid nested auto-quote tactic, '{' or 'begin' expected", pos); } @@ -154,7 +144,7 @@ static expr parse_interactive_param(parser & p, expr const & ty, expr const & qu return to_expr(vm_res); } -static expr parse_interactive_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) { +static expr parse_interactive_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_istep) { auto pos = p.pos(); expr type = p.env().get(decl_name).get_type(); name itactic = get_interactive_tactic_full_name(tac_class, "itactic"); @@ -173,10 +163,9 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co lean_assert(arg_args.size() == 3); args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2])); } else if (is_constant(arg_type, itactic)) { - bool report_error = false; - args.push_back(parse_nested_interactive_tactic(p, tac_class, use_rstep, report_error)); + args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep)); } else if (is_constant(arg_type, irtactic)) { - args.push_back(parse_nested_interactive_tactic(p, tac_class, use_rstep, report_error)); + args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep)); } else { break; } @@ -199,7 +188,7 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co throw; } expr r = p.mk_app(p.save_pos(mk_constant(decl_name), pos), args, pos); - return mk_tactic_step(p, r, pos, tac_class, use_rstep, report_error); + return mk_tactic_step(p, r, pos, tac_class, use_istep); } static bool is_curr_exact_shortcut(parser & p) { @@ -214,11 +203,10 @@ static bool is_curr_exact_shortcut(parser & p) { struct parse_tactic_fn { parser & m_p; name m_tac_class; - bool m_use_rstep; - bool m_report_error; + bool m_use_istep; - parse_tactic_fn(parser & p, name tac_class, bool use_rstep, bool report_error): - m_p(p), m_tac_class(tac_class), m_use_rstep(use_rstep), m_report_error(report_error) {} + parse_tactic_fn(parser & p, name tac_class, bool use_istep): + m_p(p), m_tac_class(tac_class), m_use_istep(use_istep) {} expr concat(expr const & tac1, expr const & tac2, pos_info const & pos) { return ::lean::concat(m_p, tac1, tac2, pos); @@ -253,7 +241,7 @@ struct parse_tactic_fn { auto pos = m_p.pos(); if (auto dname = is_interactive_tactic(m_p, m_tac_class)) { try { - r = parse_interactive_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error); + r = parse_interactive_tactic(m_p, *dname, m_tac_class, m_use_istep); } catch (break_at_pos_exception & e) { if (!m_p.get_complete() && (!e.m_token_info.m_token.size() || @@ -268,10 +256,10 @@ struct parse_tactic_fn { } else if (is_curr_exact_shortcut(m_p)) { expr arg = parse_qexpr(); r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "exact")), pos), arg, pos); - if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error); + if (m_use_istep) r = mk_tactic_istep(m_p, r, pos, m_tac_class); } else { r = m_p.parse_expr(); - if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error); + if (m_use_istep) r = mk_tactic_istep(m_p, r, pos, m_tac_class); } if (save_info) return concat(mk_tactic_save_info(m_p, pos, m_tac_class), r, pos); @@ -280,7 +268,7 @@ struct parse_tactic_fn { } expr parse_block(pos_info const & pos, name const & end_tk) { - return ::lean::parse_begin_end_block(m_p, pos, end_tk, m_tac_class, m_use_rstep, m_report_error); + return ::lean::parse_begin_end_block(m_p, pos, end_tk, m_tac_class, m_use_istep); } expr parse_elem(bool save_info) { @@ -290,7 +278,7 @@ struct parse_tactic_fn { name const & end_tk = m_p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk(); expr next_tac = parse_block(pos, end_tk); auto block_pos = m_p.pos_of(next_tac); - next_tac = mk_tactic_solve1(m_p, next_tac, block_pos, m_tac_class, m_use_rstep && save_info, m_report_error && save_info); + next_tac = mk_tactic_solve1(m_p, next_tac, block_pos, m_tac_class, m_use_istep && save_info); if (save_info) { expr info_tac = mk_tactic_save_info(m_p, pos, m_tac_class); return concat(info_tac, next_tac, pos); @@ -337,16 +325,16 @@ struct parse_tactic_fn { } }; -static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep, bool report_error) { - return parse_tactic_fn(p, tac_class, use_rstep, report_error)(); +static expr parse_tactic_core(parser & p, name const & tac_class, bool use_istep) { + return parse_tactic_fn(p, tac_class, use_istep)(); } -static expr parse_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) { +static expr parse_tactic(parser & p, name const & tac_class, bool use_istep) { if (p.in_quote()) { parser::quote_scope _(p, false); - return parse_tactic_core(p, tac_class, use_rstep, report_error); + return parse_tactic_core(p, tac_class, use_istep); } else { - return parse_tactic_core(p, tac_class, use_rstep, report_error); + return parse_tactic_core(p, tac_class, use_istep); } } @@ -384,11 +372,10 @@ static name parse_tactic_class(parser & p, name tac_class) { struct parse_begin_end_block_fn { parser & m_p; name m_tac_class; - bool m_use_rstep; - bool m_report_error; + bool m_use_istep; - parse_begin_end_block_fn(parser & p, name tac_class, bool use_rstep, bool report_error): - m_p(p), m_tac_class(tac_class), m_use_rstep(use_rstep), m_report_error(report_error) {} + parse_begin_end_block_fn(parser & p, name tac_class, bool use_istep): + m_p(p), m_tac_class(tac_class), m_use_istep(use_istep) {} expr concat(expr const & tac1, expr const & tac2, pos_info const & pos) { return ::lean::concat(m_p, tac1, tac2, pos); @@ -416,7 +403,7 @@ struct parse_begin_end_block_fn { } expr parse_tactic() { - return ::lean::parse_tactic(m_p, m_tac_class, m_use_rstep, m_report_error); + return ::lean::parse_tactic(m_p, m_tac_class, m_use_istep); } expr operator()(pos_info const & start_pos, name const & end_token) { @@ -474,16 +461,15 @@ struct parse_begin_end_block_fn { } }; -static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error) { - return parse_begin_end_block_fn(p, tac_class, use_rstep, report_error)(start_pos, end_token); +static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_istep) { + return parse_begin_end_block_fn(p, tac_class, use_istep)(start_pos, end_token); } expr parse_begin_end_expr_core(parser & p, pos_info const & pos, name const & end_token) { parser::local_scope _(p); p.clear_expr_locals(); - bool use_rstep = true; - bool report_error = true; - expr tac = parse_begin_end_block(p, pos, end_token, get_tactic_name(), use_rstep, report_error); + bool use_istep = true; + expr tac = parse_begin_end_block(p, pos, end_token, get_tactic_name(), use_istep); return copy_tag(tac, mk_by(tac)); } @@ -505,9 +491,8 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { p.clear_expr_locals(); auto tac_pos = p.pos(); try { - bool use_rstep = true; - bool report_error = true; - expr tac = parse_tactic(p, get_tactic_name(), use_rstep, report_error); + bool use_istep = true; + expr tac = parse_tactic(p, get_tactic_name(), use_istep); expr type = mk_tactic_unit(get_tactic_name()); expr r = p.save_pos(mk_typed_expr(type, tac), tac_pos); return p.save_pos(mk_by(r), pos); @@ -544,13 +529,12 @@ static void erase_quoted_terms_pos_info(parser & p, expr const & e) { expr parse_interactive_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) { name const & tac_class = get_tactic_name(); - bool use_rstep = false; - bool report_error = false; - expr r = parse_tactic(p, tac_class, use_rstep, report_error); + bool use_istep = false; + expr r = parse_tactic(p, tac_class, use_istep); erase_quoted_terms_pos_info(p, r); while (p.curr_is_token(get_comma_tk())) { p.next(); - expr next = parse_tactic(p, tac_class, use_rstep, report_error); + expr next = parse_tactic(p, tac_class, use_istep); erase_quoted_terms_pos_info(p, next); r = p.mk_app({p.save_pos(mk_constant(get_has_bind_and_then_name()), pos), r, next}, pos); } @@ -558,21 +542,7 @@ expr parse_interactive_tactic_block(parser & p, unsigned, expr const *, pos_info return r; } -vm_obj tactic_report_error(vm_obj const & line, vm_obj const & col, vm_obj const & fmt, vm_obj const & _s) { - tactic_state s = tactic::to_state(_s); - pos_info pos(force_to_unsigned(line), force_to_unsigned(col)); - pos_info_provider * pip = get_pos_info_provider(); - if (pip) { - std::shared_ptr tc = std::make_shared(mk_type_context_for(s)); - message_builder out(tc, s.env(), get_global_ios(), pip->get_file_name(), pos, ERROR); - out << mk_pair(to_format(fmt), s.get_options()); - out.report(); - } - return tactic::mk_success(s); -} - void initialize_tactic_notation() { - DECLARE_VM_BUILTIN(name({"tactic", "report_error"}), tactic_report_error); } void finalize_tactic_notation() { diff --git a/tests/lean/interactive/my_tac_class.lean b/tests/lean/interactive/my_tac_class.lean index e07297042b..f20d9f7faa 100644 --- a/tests/lean/interactive/my_tac_class.lean +++ b/tests/lean/interactive/my_tac_class.lean @@ -15,12 +15,15 @@ namespace mytac meta def step {α : Type} (t : mytac α) : mytac unit := t >> return () -meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit := +meta def istep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit := λ v s, result.cases_on (@scope_trace _ line col (t v s)) (λ ⟨a, v⟩ new_s, result.success ((), v) new_s) (λ opt_msg_thunk e new_s, match opt_msg_thunk with - | some msg_thunk := let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in - (tactic.report_error line col msg >> interaction_monad.silent_fail) new_s | none := interaction_monad.silent_fail new_s end) + | some msg_thunk := + let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in + interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s + | none := interaction_monad.silent_fail new_s + end) meta def execute (tac : mytac unit) : tactic unit := tac 0 >> return () diff --git a/tests/lean/interactive/my_tac_class.lean.expected.out b/tests/lean/interactive/my_tac_class.lean.expected.out index 029ee811f7..b01c94545a 100644 --- a/tests/lean/interactive/my_tac_class.lean.expected.out +++ b/tests/lean/interactive/my_tac_class.lean.expected.out @@ -1,3 +1,3 @@ -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":58,"severity":"information","text":"test\n"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":61,"severity":"information","text":"test\n"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"source":,"state":"Custom state: 2\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":62} +{"record":{"source":,"state":"Custom state: 2\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":65} diff --git a/tests/lean/interactive/rb_map_ts.lean b/tests/lean/interactive/rb_map_ts.lean index c012256e68..a5b9fca9f1 100644 --- a/tests/lean/interactive/rb_map_ts.lean +++ b/tests/lean/interactive/rb_map_ts.lean @@ -15,12 +15,16 @@ namespace mytac meta def step {α : Type} (t : mytac α) : mytac unit := t >> return () -meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit := +meta def istep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit := λ v s, result.cases_on (@scope_trace _ line col (t v s)) (λ ⟨a, v⟩ new_s, result.success ((), v) new_s) - (λ opt_msg_thunk e new_s, match opt_msg_thunk with - | some msg_thunk := let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in - (tactic.report_error line col msg >> interaction_monad.silent_fail) new_s | none := interaction_monad.silent_fail new_s end) + (λ opt_msg_thunk e new_s, + match opt_msg_thunk with + | some msg_thunk := + let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in + interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s + | none := interaction_monad.silent_fail new_s + end) meta def execute (tac : mytac unit) : tactic unit := tac (name_map.mk nat) >> return () diff --git a/tests/lean/interactive/rb_map_ts.lean.expected.out b/tests/lean/interactive/rb_map_ts.lean.expected.out index 15193b785f..38d644e504 100644 --- a/tests/lean/interactive/rb_map_ts.lean.expected.out +++ b/tests/lean/interactive/rb_map_ts.lean.expected.out @@ -1,8 +1,8 @@ -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":85,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":63} -{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":67} -{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":81} +{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":67} +{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":71} +{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":85} diff --git a/tests/lean/run/my_tac_class.lean b/tests/lean/run/my_tac_class.lean index f20974ca5e..5deecd3b79 100644 --- a/tests/lean/run/my_tac_class.lean +++ b/tests/lean/run/my_tac_class.lean @@ -15,14 +15,14 @@ namespace mytac meta def step {α : Type} (t : mytac α) : mytac unit := t >> return () -meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit := +meta def istep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit := λ v s, result.cases_on (@scope_trace _ line col (t v s)) (λ ⟨a, v⟩ new_s, result.success ((), v) new_s) (λ opt_msg_thunk e new_s, match opt_msg_thunk with | some msg_thunk := - let msg := msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in - (tactic.report_error line col msg >> interaction_monad.silent_fail) new_s + let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in + interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s | none := interaction_monad.silent_fail new_s end)