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

refactor(init/meta/interaction_monad): replace rstep by istep

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-15 18:08:59 +01:00
parent 7f1569535b
commit c8fff9f4ff
10 changed files with 88 additions and 123 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/meta/interaction_monad.lean
View file

@ -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 α

7
library/init/meta/smt/interactive.lean
View file

@ -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

18
library/init/meta/tactic.lean
View file

@ -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,

20
src/frontends/lean/tactic_evaluator.cpp
View file

@ -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<tactic::exception_info> ex = tactic::is_exception(S, r)) {
format fmt = std::get<0>(*ex);
optional<pos_info> 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_info> 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));

116
src/frontends/lean/tactic_notation.cpp
View file

@ -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<name> is_interactive_tactic(parser & p, name const & tac_class)
return optional<name>();
}
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<abstract_type_context> tc = std::make_shared<type_context>(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() {

9
tests/lean/interactive/my_tac_class.lean
View file

@ -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 ()

4
tests/lean/interactive/my_tac_class.lean.expected.out
View file

@ -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}

12
tests/lean/interactive/rb_map_ts.lean
View file

@ -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 ()

14
tests/lean/interactive/rb_map_ts.lean.expected.out
View file

@ -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}

6
tests/lean/run/my_tac_class.lean
View file

@ -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)