refactor(library/init/meta): remove tactic_state.mk_empty

The tactic_state object will contain a name_generator for creating fresh
names. `tactic_state.mk_empty` is bad because it does not have sufficient
information to create this name_generator.
Moreover `tactic_state.mk_empty` was only being used to convert
`tactic A` into a `parser A`.
We implement this primitive now in C++. In C++, we will be able
to use the parser name generator to initialize a fresh `tactic_state`.

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

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,

src/library/tactic/tactic_state.cpp

@@ -271,11 +271,6 @@ vm_obj to_obj(transparency_mode m) {
     return mk_vm_simple(static_cast<unsigned>(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);

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<format()> 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<State> is_success(vm_obj const & r);
     static optional<exception_info> is_exception(vm_state & S, vm_obj const & ex);

src/library/vm/interaction_state_imp.h

@@ -131,6 +131,12 @@ vm_obj interaction_monad<State>::mk_exception(vm_obj const & fn, vm_obj const &
     return mk_vm_constructor(1, mk_vm_some(fn), pos, to_obj(s));
 }
 
+template<typename State>
+vm_obj interaction_monad<State>::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<typename State>
 vm_obj interaction_monad<State>::mk_exception(throwable const & ex, State const & s) {
     vm_obj _ex = lean::to_obj(ex);

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