feat(init/meta): tactic -> parser coercion

library/init/meta/lean/parser.lean

@@ -10,6 +10,8 @@ namespace lean
 
 -- TODO: make inspectable (and pure)
 meta constant parser_state : Type
+meta constant parser_state.env     : parser_state → environment
+meta constant parser_state.options : parser_state → options
 meta constant parser_state.cur_pos : parser_state → pos
 
 @[reducible] meta def parser := interaction_monad parser_state
@@ -19,6 +21,7 @@ open interaction_monad
 open interaction_monad.result
 
 namespace parser
+variable {α : Type}
 
 /-- Make sure the next token is an identifier, consume it, and
     produce the quoted name `t, where t is the identifier. -/
@@ -32,14 +35,14 @@ protected meta constant pexpr (rbp := std.prec.max) : parser pexpr
 meta constant qexpr (rbp := std.prec.max) : parser pexpr
 
 /-- Do not report info from content parsed by `p`. -/
-meta constant skip_info {α : Type} (p : parser α) : parser α
+meta constant skip_info (p : parser α) : parser α
 /-- Set goal info position of content parsed by `p` to current position. Nested calls take precedence. -/
-meta constant set_goal_info_pos {α : Type} (p : parser α) : parser α
+meta constant set_goal_info_pos (p : parser α) : parser α
 
 /-- Return the current parser position without consuming any input. -/
 meta def cur_pos : parser pos := λ s, success (parser_state.cur_pos s) s
 
-meta def parser_orelse {α : Type} (p₁ p₂ : parser α) : parser α :=
+meta def parser_orelse (p₁ p₂ : parser α) : parser α :=
 λ s,
 let pos₁ := parser_state.cur_pos s in
 result.cases_on (p₁ s)
@@ -67,8 +70,14 @@ meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type
 local postfix `?`:100 := optional
 local postfix `*`:100 := many
 
-meta def sep_by {α : Type} : parser unit → parser α → parser (list α)
+meta def sep_by : parser unit → parser α → parser (list α)
 | s p := (list.cons <$> p <*> (s *> p)*) <|> return []
 
+meta instance tactic_to_parser : has_coe (tactic α) (parser α) :=
+⟨λ t s, match t (tactic_state.mk_empty s.env s.options) with
+ | success x _     := success x s
+ | exception f p _ := exception f p s
+ end⟩
+
 end parser
 end lean

library/init/meta/tactic.lean

@@ -14,6 +14,8 @@ 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
 meta constant to_format   : tactic_state → format
 /- Format expression with respect to the main goal in the tactic state.

src/library/tactic/tactic_state.cpp

@@ -226,6 +226,10 @@ vm_obj to_obj(transparency_mode 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());
 }
@@ -842,6 +846,7 @@ vm_obj tactic_sleep(vm_obj const & msecs, 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/vm_parser.cpp

@@ -70,6 +70,16 @@ expr parse_interactive_param(parser & p, expr const & param_ty) {
     }
 }
 
+vm_obj vm_parser_state_env(vm_obj const & o) {
+    auto const & s = lean_parser::to_state(o);
+    return to_obj(s.m_p->env());
+}
+
+vm_obj vm_parser_state_options(vm_obj const & o) {
+    auto const & s = lean_parser::to_state(o);
+    return to_obj(s.m_p->get_options());
+}
+
 vm_obj vm_parser_state_cur_pos(vm_obj const & o) {
     auto const & s = lean_parser::to_state(o);
     return to_obj(s.m_p->pos());
@@ -139,6 +149,8 @@ vm_obj vm_parser_set_goal_info_pos(vm_obj const &, vm_obj const & vm_p, vm_obj c
 }
 
 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);
     DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}),     vm_parser_state_cur_pos);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),             vm_parser_ident);
     DECLARE_VM_BUILTIN(get_lean_parser_tk_name(),                     vm_parser_tk);