diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean index a1e305ddfd..e4c31c45a2 100644 --- a/library/init/meta/lean/parser.lean +++ b/library/init/meta/lean/parser.lean @@ -80,14 +80,10 @@ local postfix `*`:100 := many meta def sep_by : parser unit → parser α → parser (list α) | s p := (list.cons <$> p <*> (s *> p)*) <|> return [] -meta def tactic_to_parser : tactic α → parser α := -λ t s, match t (tactic_state.mk_empty s.env s.options) with - | success x ts := (set_env ts.env >> pure x) s - | exception f p _ := exception f p s - end +meta constant of_tactic : tactic α → parser α meta instance : has_coe (tactic α) (parser α) := -⟨tactic_to_parser⟩ +⟨of_tactic⟩ end parser end lean diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index b956fe99c8..c75e3c9d29 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -14,8 +14,6 @@ meta constant tactic_state : Type universes u v namespace tactic_state -/-- Create a tactic state with an empty local context and a dummy goal. -/ -meta constant mk_empty : environment → options → tactic_state meta constant env : tactic_state → environment /-- Format the given tactic state. If `target_lhs_only` is true and the target is of the form `lhs ~ rhs`, where `~` is a simplification relation, diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index ebae8252a6..101cb693a7 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -271,11 +271,6 @@ vm_obj to_obj(transparency_mode m) { return mk_vm_simple(static_cast(m)); } - -vm_obj tactic_state_mk_empty(vm_obj const & vm_env, vm_obj const & vm_opts) { - return to_obj(mk_tactic_state_for(to_env(vm_env), to_options(vm_opts), "_mk_empty", local_context(), mk_true())); -} - vm_obj tactic_state_env(vm_obj const & s) { return to_obj(tactic::to_state(s).env()); } @@ -1021,7 +1016,6 @@ vm_obj tactic_frozen_local_instances(vm_obj const & s0) { } void initialize_tactic_state() { - DECLARE_VM_BUILTIN(name({"tactic_state", "mk_empty"}), tactic_state_mk_empty); DECLARE_VM_BUILTIN(name({"tactic_state", "env"}), tactic_state_env); DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr); DECLARE_VM_BUILTIN(name({"tactic_state", "to_format"}), tactic_state_to_format); diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h index 31d88eae3f..56e960272b 100644 --- a/src/library/vm/interaction_state.h +++ b/src/library/vm/interaction_state.h @@ -52,6 +52,7 @@ struct interaction_monad { static vm_obj mk_exception(char const * msg, State const & s); static vm_obj mk_exception(sstream const & strm, State const & s); static vm_obj mk_exception(std::function const & thunk, State const & s); + static vm_obj update_exception_state(vm_obj const & ex, State const & s); static void report_exception(vm_state & S, vm_obj const & r); static optional is_success(vm_obj const & r); static optional is_exception(vm_state & S, vm_obj const & ex); diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index 16a9746542..a6781ab0f0 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -131,6 +131,12 @@ vm_obj interaction_monad::mk_exception(vm_obj const & fn, vm_obj const & return mk_vm_constructor(1, mk_vm_some(fn), pos, to_obj(s)); } +template +vm_obj interaction_monad::update_exception_state(vm_obj const & ex, State const & s) { + lean_assert(!is_success(ex)); + return mk_vm_constructor(1, cfield(ex, 0), cfield(ex, 1), to_obj(s)); +} + template vm_obj interaction_monad::mk_exception(throwable const & ex, State const & s) { vm_obj _ex = lean::to_obj(ex); diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 46634536a4..c62b996da7 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -314,6 +314,27 @@ static vm_obj interactive_parse_binders(vm_obj const & vm_rbp, vm_obj const & vm CATCH; } +static vm_obj vm_parser_of_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & vm_s) { + auto s = lean_parser::to_state(vm_s); + tactic_state ts = mk_tactic_state_for(s.m_p->env(), s.m_p->get_options(), name("_parser_of_tactic"), + metavar_context(), local_context(), mk_true()); + try { + vm_obj r = invoke(tac, to_obj(ts)); + if (tactic::is_result_success(r)) { + vm_obj a = tactic::get_result_value(r); + tactic_state new_ts = tactic::to_state(tactic::get_result_state(r)); + s.m_p->set_env(new_ts.env()); + return lean_parser::mk_success(a, s); + } else { + /* Remark: the following command relies on the fact that + `tactic` and `parser` are both implemented using interaction_monad */ + return lean_parser::update_exception_state(r, s); + } + } catch (exception & ex) { + return lean_parser::mk_exception(ex, s); + } +} + void initialize_vm_parser() { DECLARE_VM_BUILTIN(name({"lean", "parser_state", "env"}), vm_parser_state_env); DECLARE_VM_BUILTIN(name({"lean", "parser_state", "options"}), vm_parser_state_options); @@ -327,7 +348,7 @@ void initialize_vm_parser() { DECLARE_VM_BUILTIN(name({"lean", "parser", "skip_info"}), vm_parser_skip_info); DECLARE_VM_BUILTIN(name({"lean", "parser", "set_goal_info_pos"}), vm_parser_set_goal_info_pos); DECLARE_VM_BUILTIN(name({"lean", "parser", "with_input"}), vm_parser_with_input); - + DECLARE_VM_BUILTIN(name({"lean", "parser", "of_tactic"}), vm_parser_of_tactic); DECLARE_VM_BUILTIN(name({"interactive", "decl_attributes", "apply"}), interactive_decl_attributes_apply); DECLARE_VM_BUILTIN(name({"interactive", "inductive_decl", "parse"}), interactive_inductive_decl_parse); DECLARE_VM_BUILTIN(name({"interactive", "parse_binders"}), interactive_parse_binders);