From d15591a2d8d7a70b37c98fc396b8d6fc82a99b45 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 15 Feb 2017 01:41:05 +0100
Subject: [PATCH] feat(library,frontends/lean): expose parser to Lean and use
 for parsing tactic parameters

---
 library/init/algebra/functions.lean           |   2 +-
 library/init/category/alternative.lean        |  12 +-
 library/init/category/applicative.lean        |  24 +-
 library/init/data/list/basic.lean             |  18 +-
 library/init/data/list/instances.lean         |   9 -
 library/init/meta/async_tactic.lean           |   8 +-
 library/init/meta/expr.lean                   |  37 ++-
 library/init/meta/format.lean                 |  12 +-
 library/init/meta/interaction_monad.lean      |  86 ++++++
 library/init/meta/interactive.lean            | 153 ++++++-----
 library/init/meta/lean/parser.lean            |  69 +++++
 library/init/meta/quote.lean                  |  59 ++++
 library/init/meta/simp_tactic.lean            |   2 +-
 library/init/meta/smt/interactive.lean        |  56 ++--
 library/init/meta/smt/smt_tactic.lean         |  18 +-
 library/init/meta/tactic.lean                 | 153 ++---------
 library/tools/super/prover.lean               |   6 +-
 src/frontends/lean/builtin_exprs.cpp          |  19 +-
 src/frontends/lean/elaborator.cpp             |   3 +-
 src/frontends/lean/parser.cpp                 |  20 +-
 src/frontends/lean/parser.h                   |   5 +-
 src/frontends/lean/prenum.h                   |   1 +
 src/frontends/lean/tactic_evaluator.cpp       |  62 +----
 src/frontends/lean/tactic_evaluator.h         |  22 +-
 src/frontends/lean/tactic_notation.cpp        | 259 ++----------------
 src/frontends/lean/token_table.cpp            |   2 +-
 src/library/constants.cpp                     |  76 +----
 src/library/constants.h                       |  19 +-
 src/library/constants.txt                     |  19 +-
 src/library/io_state.h                        |   2 +-
 src/library/tactic/tactic_state.cpp           |  18 +-
 src/library/tactic/tactic_state.h             |   4 +
 src/library/vm/CMakeLists.txt                 |   2 +-
 src/library/vm/init_module.cpp                |   3 +
 src/library/vm/interaction_state.h            | 241 ++++++++++++++++
 src/library/vm/vm_expr.cpp                    |  18 ++
 src/library/vm/vm_parser.cpp                  |  88 ++++++
 src/library/vm/vm_parser.h                    |  16 ++
 tests/lean/bad_error5.lean.expected.out       |   2 +-
 tests/lean/elab3.lean.expected.out            |   3 +-
 .../elab_error_recovery.lean.expected.out     |   2 +-
 tests/lean/inline_issue.lean.expected.out     |   2 +-
 tests/lean/interactive/my_tac_class.lean      |   6 +-
 tests/lean/interactive/rb_map_ts.lean         |  10 +-
 tests/lean/run/isabelle.lean                  |   6 +-
 tests/lean/run/my_tac_class.lean              |   8 +-
 tests/lean/run/quote_bas.lean                 |   4 +
 tests/lean/tactic_state_pp.lean               |   4 +-
 48 files changed, 949 insertions(+), 721 deletions(-)
 create mode 100644 library/init/meta/interaction_monad.lean
 create mode 100644 library/init/meta/lean/parser.lean
 create mode 100644 library/init/meta/quote.lean
 create mode 100644 src/library/vm/interaction_state.h
 create mode 100644 src/library/vm/vm_parser.cpp
 create mode 100644 src/library/vm/vm_parser.h

diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean
index 26906410f0..4bff4c63cc 100644
--- a/library/init/algebra/functions.lean
+++ b/library/init/algebra/functions.lean
@@ -23,7 +23,7 @@ solve1 $ intros
 >> try `[apply le_refl]
 >> try `[apply le_of_not_le, assumption]
 
-meta def tactic.interactive.min_tac (a b : interactive.types.qexpr) : tactic unit :=
+meta def tactic.interactive.min_tac (a b : interactive.parse lean.parser.qexpr) : tactic unit :=
 `[apply @by_cases (%%a ≤ %%b), repeat {min_tac_step}]
 
 lemma min_le_left (a b : α) : min a b ≤ a :=
diff --git a/library/init/category/alternative.lean b/library/init/category/alternative.lean
index d42db96782..182266bee2 100644
--- a/library/init/category/alternative.lean
+++ b/library/init/category/alternative.lean
@@ -11,10 +11,13 @@ class alternative (f : Type u → Type v) extends applicative f : Type (max u+1
 (failure : Π {a : Type u}, f a)
 (orelse  : Π {a : Type u}, f a → f a → f a)
 
-@[inline] def failure {f : Type u → Type v} [alternative f] {a : Type u} : f a :=
+section
+variables {f : Type u → Type v} [alternative f] {a : Type u}
+
+@[inline] def failure : f a :=
 alternative.failure f
 
-@[inline] def orelse {f : Type u → Type v} [alternative f] {a : Type u} : f a → f a → f a :=
+@[inline] def orelse : f a → f a → f a :=
 alternative.orelse
 
 infixr ` <|> `:2 := orelse
@@ -27,3 +30,8 @@ if p then pure () else failure
 @[inline] def guardb {f : Type → Type v} [alternative f] : bool → f unit
 | tt := pure ()
 | ff := failure
+
+@[inline] def optional (x : f a) : f (option a) :=
+some <$> x <|> pure none
+
+end
diff --git a/library/init/category/applicative.lean b/library/init/category/applicative.lean
index 1c842491dd..4bf778dd52 100644
--- a/library/init/category/applicative.lean
+++ b/library/init/category/applicative.lean
@@ -5,16 +5,34 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.category.functor
+import init.function
+open function
 universes u v
 
 class applicative (f : Type u → Type v) extends functor f : Type (max u+1 v):=
 (pure : Π {a : Type u}, a → f a)
 (seq  : Π {a b : Type u}, f (a → b) → f a → f b)
 
-@[inline] def pure {f : Type u → Type v} [applicative f] {a : Type u} : a → f a :=
+section
+variables {a b : Type u} {f : Type u → Type v} [applicative f]
+
+@[inline] def pure : a → f a :=
 applicative.pure f
 
-@[inline] def seq_app {a b : Type u} {f : Type u → Type v} [applicative f] : f (a → b) → f a → f b :=
+@[inline] def seq_app : f (a → b) → f a → f b :=
 applicative.seq
 
-infixr ` <*> `:2 := seq_app
+infixl ` <*> `:2 := seq_app
+
+/-- Sequence actions, discarding the first value. -/
+def seq_left (x : f a) (y : f b) : f a :=
+pure (λ x y, x) <*> x <*> y
+
+/-- Sequence actions, discarding the second value. -/
+def seq_right (x : f a) (y : f b) : f b :=
+pure (λ x y, y) <*> x <*> y
+
+infixl ` <* `:2 := seq_left
+infixl ` *> `:2 := seq_right
+
+end
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index b19823cf98..56f5a15518 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.logic init.data.nat.basic
+import init.logic init.data.nat.basic init.category.monad
 open decidable list
 
 notation h :: t  := cons h t
@@ -179,4 +179,20 @@ def iota : ℕ → list ℕ :=
 def sum [has_add α] [has_zero α] : list α → α :=
 foldl add zero
 
+def intersperse (sep : α) : list α → list α
+| []      := []
+| [x]     := [x]
+| (x::xs) := x::sep::intersperse xs
+
+def intercalate (sep : list α) (xs : list (list α)) : list α :=
+join (intersperse sep xs)
+
+@[inline] def bind {α : Type u} {β : Type v} (a : list α) (b : α → list β) : list β :=
+join (map b a)
+
+@[inline] def ret {α : Type u} (a : α) : list α :=
+[a]
 end list
+
+instance : monad list :=
+{map := @list.map, ret := @list.ret, bind := @list.bind}
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index cf4dc52509..769fb46368 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -10,15 +10,6 @@ open list
 
 universes u v
 
-@[inline] def list.bind {α : Type u} {β : Type v} (a : list α) (b : α → list β) : list β :=
-join (map b a)
-
-@[inline] def list.ret {α : Type u} (a : α) : list α :=
-[a]
-
-instance : monad list :=
-{map := @map, ret := @list.ret, bind := @list.bind}
-
 instance : alternative list :=
 ⟨@map, @list.ret, @fapp _ _, @nil, @list.append⟩
 
diff --git a/library/init/meta/async_tactic.lean b/library/init/meta/async_tactic.lean
index 2fa6cf663a..0f86f1dfe1 100644
--- a/library/init/meta/async_tactic.lean
+++ b/library/init/meta/async_tactic.lean
@@ -16,15 +16,15 @@ private meta def report {α} (s : tactic_state) : option (unit → format) → 
 
 private meta def run_or_fail {α} (s : tactic_state) (tac : tactic α) : α :=
 match tac s with
-| (tactic_result.success a s) := a
-| (tactic_result.exception fmt _ s') := report s' fmt
+| (result.success a s) := a
+| (result.exception fmt _ s') := report s' fmt
 end
 
 meta def run_async {α : Type} (tac : tactic α) : tactic (task α) := do
 s ← read, return $ task.delay $ λ _,
   match tac s with
-  | (tactic_result.success a s) := a
-  | (tactic_result.exception fmt _ s') := report s' fmt
+  | (result.success a s) := a
+  | (result.exception fmt _ s') := report s' fmt
   end
 
 meta def prove_goal_async (tac : tactic unit) : tactic unit := do
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index aa5bd181f6..94c64174a8 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -9,6 +9,15 @@ import init.meta.level
 inductive binder_info
 | default | implicit | strict_implicit | inst_implicit | other
 
+instance : has_to_string binder_info :=
+⟨λ bi, match bi with
+| binder_info.default := "default"
+| binder_info.implicit := "implicit"
+| binder_info.strict_implicit := "strict_implicit"
+| binder_info.inst_implicit := "inst_implicit"
+| binder_info.other := "other"
+end⟩
+
 meta constant macro_def : Type
 
 /- Reflect a C++ expr object. The VM replaces it with the C++ implementation. -/
@@ -32,6 +41,9 @@ meta constant expr.macro_def_name (d : macro_def) : name
 meta def expr.mk_var (n : nat) : expr :=
 expr.var (unsigned.of_nat n)
 
+meta constant expr.mk_quote_macro : expr → expr
+meta constant expr.mk_prenum_macro : nat → expr
+meta constant expr.mk_string_macro : string → expr
 /- Choice macros are used to implement overloading. -/
 meta constant expr.is_choice_macro : expr → bool
 
@@ -43,7 +55,7 @@ attribute [instance] expr.has_decidable_eq
 meta constant expr.alpha_eqv : expr → expr → bool
 notation a ` =ₐ `:50 b:50 := expr.alpha_eqv a b = bool.tt
 
-meta constant expr.to_string : expr → string
+protected meta constant expr.to_string : expr → string
 
 meta instance : has_to_string expr :=
 has_to_string.mk expr.to_string
@@ -290,4 +302,27 @@ meta def pis : list expr → expr → expr
   pi pp info t (abstract_local (pis es f) uniq)
 | _ f := f
 
+open format
+
+private meta def p := λ xs, paren (format.join (list.intersperse " " xs))
+
+private meta def macro_args_to_list_aux (n : unsigned) (args : fin (unsigned.to_nat n) → expr) : Π (i : nat), i ≤ n^.to_nat → list expr
+| 0     _ := []
+| (i+1) h := args ⟨i, h⟩ :: macro_args_to_list_aux i (nat.le_trans (nat.le_succ _) h)
+
+meta def macro_args_to_list (n : unsigned) (args : fin (unsigned.to_nat n) → expr) : list expr :=
+macro_args_to_list_aux n args n^.to_nat (nat.le_refl _)
+
+meta def to_raw_fmt : expr → format
+| (var n) := p ["var", to_fmt n^.to_nat]
+| (sort l) := p ["sort", to_fmt l]
+| (const n ls) := p ["const", to_fmt n, to_fmt ls]
+| (mvar n t)   := p ["mvar", to_fmt n, to_raw_fmt t]
+| (local_const n m bi t) := p ["local_const", to_fmt n, to_fmt m, to_raw_fmt t]
+| (app e f) := p ["app", to_raw_fmt e, to_raw_fmt f]
+| (lam n bi e t) := p ["lam", to_fmt n, to_string bi, to_raw_fmt e, to_raw_fmt t]
+| (pi n bi e t) := p ["pi", to_fmt n, to_string bi, to_raw_fmt e, to_raw_fmt t]
+| (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f]
+| (macro d n args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: list.map to_raw_fmt (macro_args_to_list n args))))
+
 end expr
diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean
index bf0527dd09..d45ecaf204 100644
--- a/library/init/meta/format.lean
+++ b/library/init/meta/format.lean
@@ -60,6 +60,9 @@ meta def format.when {α : Type u} [has_to_format α] : bool → α → format
 | tt a := to_fmt a
 | ff a := nil
 
+meta def format.join (xs : list format) : format :=
+foldl compose (of_string "") xs
+
 meta instance : has_to_format options :=
 ⟨λ o, format.of_options o⟩
 
@@ -78,14 +81,9 @@ meta instance : has_to_format nat :=
 meta instance : has_to_format char :=
 ⟨λ c : char, format.of_string [c]⟩
 
-meta def list.to_format_aux {α : Type u} [has_to_format α] : bool → list α → format
-| b  []      := to_fmt ""
-| tt (x::xs) := to_fmt x ++ list.to_format_aux ff xs
-| ff (x::xs) := to_fmt "," ++ line ++ to_fmt x ++ list.to_format_aux ff xs
-
 meta def list.to_format {α : Type u} [has_to_format α] : list α → format
-| []      := to_fmt "[]"
-| (x::xs) := to_fmt "[" ++ group (nest 1 (list.to_format_aux tt (x::xs))) ++ to_fmt "]"
+| [] := to_fmt "[]"
+| xs := to_fmt "[" ++ group (nest 1 $ format.join $ list.intersperse ("," ++ line) $ xs^.for to_fmt) ++ to_fmt "]"
 
 meta instance {α : Type u} [has_to_format α] : has_to_format (list α) :=
 ⟨list.to_format⟩
diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean
new file mode 100644
index 0000000000..179f8fd1ab
--- /dev/null
+++ b/library/init/meta/interaction_monad.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import init.function init.data.option.basic init.util
+import init.category.combinators init.category.monad init.category.alternative init.category.monad_fail
+import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment
+import init.meta.pexpr init.data.to_string init.data.string.basic
+
+universes u v
+
+meta inductive interaction_monad.result (state : Type) (α : Type u)
+| success      : α → state → interaction_monad.result
+| exception {} : option (unit → format) → option expr → state → interaction_monad.result
+
+open interaction_monad.result
+
+section
+variables {state : Type} {α : Type u}
+variables [has_to_string α]
+
+meta def interaction_monad.result_to_string : result state α → string
+| (success a s)              := to_string a
+| (exception (some t) ref s) := "Exception: " ++ to_string (t ())
+| (exception none ref s)     := "[silent exception]"
+
+meta instance interaction_monad.result_has_string : has_to_string (result state α) :=
+⟨interaction_monad.result_to_string⟩
+end
+
+@[reducible] meta def interaction_monad (state : Type) (α : Type u) :=
+state → result state α
+
+section
+parameter {state : Type}
+variables {α : Type u} {β : Type v}
+local notation `m` := interaction_monad state
+
+
+@[inline] meta def interaction_monad_fmap (f : α → β) (t : m α) : m β :=
+λ s, interaction_monad.result.cases_on (t s)
+  (λ a s', success (f a) s')
+  (λ e s', exception e s')
+
+@[inline] meta def interaction_monad_bind (t₁ : m α) (t₂ : α → m β) : m β :=
+λ s,  interaction_monad.result.cases_on (t₁ s)
+  (λ a s', t₂ a s')
+  (λ e s', exception e s')
+
+@[inline] meta def interaction_monad_return (a : α) : m α :=
+λ s, success a s
+
+meta def interaction_monad_orelse {α : Type u} (t₁ t₂ : m α) : m α :=
+λ s, interaction_monad.result.cases_on (t₁ s)
+  success
+  (λ e₁ ref₁ s', interaction_monad.result.cases_on (t₂ s)
+     success
+     exception)
+
+@[inline] meta def interaction_monad_seq (t₁ : m α) (t₂ : m β) : m β :=
+interaction_monad_bind t₁ (λ a, t₂)
+
+meta instance interaction_monad.monad : monad m :=
+{map := @interaction_monad_fmap, ret := @interaction_monad_return, bind := @interaction_monad_bind}
+
+meta def interaction_monad.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : state) : result state α :=
+exception (some (λ _, to_fmt msg)) none s
+
+meta def interaction_monad.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : m α :=
+λ s, interaction_monad.mk_exception msg none s
+
+meta def interaction_monad.silent_fail {α : Type u} : m α :=
+λ s, exception none none s
+
+meta def interaction_monad.failed {α : Type u} : m α :=
+interaction_monad.fail "failed"
+
+meta instance interaction_monad.monad_fail : monad_fail m :=
+{ interaction_monad.monad with fail := λ α s, interaction_monad.fail (to_fmt s) }
+
+-- TODO: unify `parser` and `tactic` behavior?
+-- meta instance interaction_monad.alternative : alternative m :=
+-- ⟨@interaction_monad_fmap, (λ α a s, success a s), (@fapp _ _), @interaction_monad.failed, @interaction_monad_orelse⟩
+end
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index fab5897011..a80026a5b3 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -6,16 +6,19 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
 import init.meta.smt.congruence_closure init.category.combinators
+import init.meta.lean.parser init.meta.quote
+
+open lean
+open lean.parser
 
 namespace interactive
+@[reducible] meta def parse {α : Type} [has_quote α] (p : parser α) : Type := α
+
 namespace types
 /- The parser treats constants in the tactic.interactive namespace specially.
    The following argument types have special parser support when interactive tactics
    are used inside `begin ... end` blocks.
 
-   - ident : make sure the next token is an identifier, and
-             produce the quoted name `t, where t is the next identifier.
-
    - opt_ident : parse (identifier)?
 
    - using_ident
@@ -70,23 +73,37 @@ namespace types
             and produce a list of quoted expressions with position information
 
 -/
-def pos : Type := nat × nat
-def ident : Type := name
-def opt_ident : Type := option ident
-def using_ident : Type := option ident
-def raw_ident_list : Type := list ident
-def with_ident_list : Type := list ident
-def without_ident_list : Type := list ident
-def location : Type := list ident
-@[reducible] meta def qexpr : Type := pexpr
-@[reducible] meta def qexpr0 : Type := pexpr
-meta def qexpr_list : Type := list qexpr
-meta def qexpr_list_with_pos : Type := list (qexpr × pos)
-meta def opt_qexpr_list : Type := list qexpr
-meta def qexpr_list_or_qexpr0 : Type := list qexpr
-meta def qexpr_list_or_qexpr0_with_pos : Type := list (qexpr × pos)
-meta def assign_tk : Type := unit
-meta def colon_tk : Type := unit
+
+variables {α β : Type}
+
+local postfix ?:100 := optional
+local notation p ` ?: `:100 d := (λ o, option.get_or_else o d) <$> p?
+local postfix * := many
+
+meta def list_of (p : parser α) := tk "[" *> sep_by "," p <* tk "]"
+
+/- legacy definitions. remove some? -/
+
+/- Remark: rbp for '<|>' is 2, ';' is 1, and ',' is 0
+   qexpr0 shoud use rbp 2.
+
+   TODO(Leo): rename qexpr0 to something else -/
+meta def qexpr0 := qexpr 2
+meta def opt_ident := ident?
+meta def using_ident := (tk "using" *> ident)?
+meta def raw_ident_list := ident*
+meta def with_ident_list := (tk "with" *> ident*) ?: []
+meta def without_ident_list := (tk "without" *> ident*) ?: []
+meta def location := (tk "at" *> ident*) ?: []
+meta def qexpr_list := list_of qexpr0
+meta def qexpr_with_pos (rbp : nat := nat.of_num std.prec.max) : parser (pexpr × pos) :=
+(λ p e, (e,p)) <$> cur_pos <*> qexpr rbp
+meta def qexpr_list_with_pos := list_of (qexpr_with_pos 0)
+meta def opt_qexpr_list := qexpr_list ?: []
+meta def qexpr_list_or_qexpr0 := qexpr_list <|> return <$> qexpr0
+meta def qexpr_list_or_qexpr0_with_pos := list_of (qexpr_with_pos 0) <|> (λ x, [x]) <$> qexpr_with_pos 0
+meta def assign_tk := tk ":="
+meta def colon_tk := tk ":"
 end types
 end interactive
 
@@ -105,7 +122,7 @@ meta def i_to_expr_strict (q : pexpr) : tactic expr :=
 to_expr q ff tt
 
 namespace interactive
-open interactive.types expr
+open interactive interactive.types expr
 
 /-
 itactic: parse a nested "interactive" tactic. That is, parse
@@ -118,7 +135,7 @@ tactic unit
 irtactic: parse a nested "interactive" tactic. That is, parse
   `(` tactic `)`
 It is similar to itactic, but the interactive mode will report errors
-when any of the nested tactics fail. This is good for tactics such as asynch and abstact.
+when any of the nested tactics fail. This is good for tactics such as async and abstract.
 -/
 meta def irtactic : Type :=
 tactic unit
@@ -133,7 +150,7 @@ If the goal is an arrow `T → U`, then it puts in the local context either `h:T
 If the goal is neither a Pi/forall nor starting with a let definition,
 the tactic `intro` applies the tactic `whnf` until the tactic `intro` can be applied or the goal is not `head-reducible`.
 -/
-meta def intro : opt_ident → tactic unit
+meta def intro : parse opt_ident → tactic unit
 | none     := intro1 >> skip
 | (some h) := tactic.intro h >> skip
 
@@ -141,14 +158,14 @@ meta def intro : opt_ident → tactic unit
 Similar to `intro` tactic. The tactic `intros` will keep introducing new hypotheses until the goal target is not a Pi/forall or let binder.
 The variant `intros h_1 ... h_n` introduces `n` new hypotheses using the given identifiers to name them.
 -/
-meta def intros : raw_ident_list → tactic unit
+meta def intros : parse raw_ident_list → tactic unit
 | [] := tactic.intros >> skip
 | hs := intro_lst hs >> skip
 
 /--
 The tactic `rename h₁ h₂` renames hypothesis `h₁` into `h₂` in the current local context.
 -/
-meta def rename : ident → ident → tactic unit :=
+meta def rename : parse ident → parse ident → tactic unit :=
 tactic.rename
 
 /--
@@ -161,14 +178,14 @@ that have not been fixed by type inference or type class resolution.
 The tactic `apply` uses higher-order pattern matching, type class resolution, and
 first-order unification with dependent types.
 -/
-meta def apply (q : qexpr0) : tactic unit :=
+meta def apply (q : parse qexpr0) : tactic unit :=
 i_to_expr q >>= tactic.apply
 
 /--
 Similar to the `apply` tactic, but it also creates subgoals for dependent premises
 that have not been fixed by type inference or type class resolution.
 -/
-meta def fapply (q : qexpr0) : tactic unit :=
+meta def fapply (q : parse qexpr0) : tactic unit :=
 i_to_expr q >>= tactic.fapply
 
 /--
@@ -186,7 +203,7 @@ Note that some holes may be implicit.
 The type of holes must be either synthesized by the system or declared by
 an explicit type ascription like (e.g., `(_ : nat → Prop)`).
 -/
-meta def refine (q : qexpr0) : tactic unit :=
+meta def refine (q : parse qexpr0) : tactic unit :=
 tactic.refine q tt
 
 /--
@@ -201,7 +218,7 @@ This tactic applies to any goal. `change U` replaces the main goal target `T` wi
 providing that `U` is well-formed with respect to the main goal local context,
 and `T` and `U` are definitionally equal.
 -/
-meta def change (q : qexpr0) : tactic unit :=
+meta def change (q : parse qexpr0) : tactic unit :=
 i_to_expr q >>= tactic.change
 
 /--
@@ -209,7 +226,7 @@ This tactic applies to any goal. It gives directly the exact proof
 term of the goal. Let `T` be our goal, let `p` be a term of type `U` then
 `exact p` succeeds iff `T` and `U` are definitionally equal.
 -/
-meta def exact (q : qexpr0) : tactic unit :=
+meta def exact (q : parse qexpr0) : tactic unit :=
 do tgt : expr ← target,
    i_to_expr_strict `(%%q : %%tgt) >>= tactic.exact
 
@@ -222,7 +239,7 @@ private meta def get_locals : list name → tactic (list expr)
 It moves the hypotheses and its dependencies to the goal target.
 This tactic is the inverse of `intro`.
 -/
-meta def revert (ids : raw_ident_list) : tactic unit :=
+meta def revert (ids : parse raw_ident_list) : tactic unit :=
 do hs ← get_locals ids, revert_lst hs, skip
 
 /- Return (some a) iff p is of the form (- a) -/
@@ -279,27 +296,27 @@ private meta def rw_hyps : transparency → list (bool × expr × pos) → list
 | m es  []      := return ()
 | m es  (h::hs) := rw_hyp m es h >> rw_hyps m es hs
 
-private meta def rw_core (m : transparency) (hs : qexpr_list_or_qexpr0_with_pos) (loc : location) : tactic unit :=
+private meta def rw_core (m : transparency) (hs : parse qexpr_list_or_qexpr0_with_pos) (loc : parse location) : tactic unit :=
 do hlist ← to_symm_expr_list hs,
    match loc with
    | [] := rw_goal m hlist >> try (reflexivity reducible)
    | hs := rw_hyps m hlist hs >> try (reflexivity reducible)
    end
 
-meta def rewrite : qexpr_list_or_qexpr0_with_pos → location → tactic unit :=
+meta def rewrite : parse qexpr_list_or_qexpr0_with_pos → parse location → tactic unit :=
 rw_core reducible
 
-meta def rw : qexpr_list_or_qexpr0_with_pos → location → tactic unit :=
+meta def rw : parse qexpr_list_or_qexpr0_with_pos → parse location → tactic unit :=
 rewrite
 
 /- rewrite followed by assumption -/
-meta def rwa (q : qexpr_list_or_qexpr0_with_pos) (l : location) : tactic unit :=
+meta def rwa (q : parse qexpr_list_or_qexpr0_with_pos) (l : parse location) : tactic unit :=
 rewrite q l >> try assumption
 
-meta def erewrite : qexpr_list_or_qexpr0_with_pos → location → tactic unit :=
+meta def erewrite : parse qexpr_list_or_qexpr0_with_pos → parse location → tactic unit :=
 rw_core semireducible
 
-meta def erw : qexpr_list_or_qexpr0_with_pos → location → tactic unit :=
+meta def erw : parse qexpr_list_or_qexpr0_with_pos → parse location → tactic unit :=
 erewrite
 
 private meta def get_type_name (e : expr) : tactic name :=
@@ -307,7 +324,7 @@ do e_type ← infer_type e >>= whnf,
    (const I ls) ← return $ get_app_fn e_type,
    return I
 
-meta def induction (p : qexpr0) (rec_name : using_ident) (ids : with_ident_list) : tactic unit :=
+meta def induction (p : parse qexpr0) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit :=
 do e ← i_to_expr p,
    match rec_name with
    | some n := tactic.induction e n ids
@@ -315,14 +332,14 @@ do e ← i_to_expr p,
    end,
    return ()
 
-meta def cases (p : qexpr0) (ids : with_ident_list) : tactic unit :=
+meta def cases (p : parse qexpr0) (ids : parse with_ident_list) : tactic unit :=
 do e ← i_to_expr p,
    tactic.cases e ids
 
-meta def destruct (p : qexpr0) : tactic unit :=
+meta def destruct (p : parse qexpr0) : tactic unit :=
 i_to_expr p >>= tactic.destruct
 
-meta def generalize (p : qexpr) (x : ident) : tactic unit :=
+meta def generalize (p : parse qexpr) (x : parse ident) : tactic unit :=
 do e ← i_to_expr p,
    tactic.generalize e x
 
@@ -349,7 +366,7 @@ tactic.try
 meta def solve1 : itactic → tactic unit :=
 tactic.solve1
 
-meta def abstract (id : opt_ident) (tac : irtactic) : tactic unit :=
+meta def abstract (id : parse opt_ident) (tac : irtactic) : tactic unit :=
 tactic.abstract tac id
 
 meta def all_goals : itactic → tactic unit :=
@@ -365,32 +382,32 @@ tactic.focus [tac]
 This tactic applies to any goal. `assert h : T` adds a new hypothesis of name `h` and type `T` to the current goal and opens a new subgoal with target `T`.
 The new subgoal becomes the main goal.
 -/
-meta def assert (h : ident) (c : colon_tk) (q : qexpr0) : tactic unit :=
+meta def assert (h : parse ident) (c : parse colon_tk) (q : parse qexpr0) : tactic unit :=
 do e ← i_to_expr_strict q,
    tactic.assert h e
 
-meta def define (h : ident) (c : colon_tk) (q : qexpr0) : tactic unit :=
+meta def define (h : parse ident) (c : parse colon_tk) (q : parse qexpr0) : tactic unit :=
 do e ← i_to_expr_strict q,
    tactic.define h e
 
 /--
 This tactic applies to any goal. `assertv h : T := p` adds a new hypothesis of name `h` and type `T` to the current goal if `p` a term of type `T`.
 -/
-meta def assertv (h : ident) (c : colon_tk) (q₁ : qexpr0) (a : assign_tk) (q₂ : qexpr0) : tactic unit :=
+meta def assertv (h : parse ident) (c : parse colon_tk) (q₁ : parse qexpr0) (a : parse assign_tk) (q₂ : parse qexpr0) : tactic unit :=
 do t ← i_to_expr_strict q₁,
    v ← i_to_expr_strict `(%%q₂ : %%t),
    tactic.assertv h t v
 
-meta def definev (h : ident) (c : colon_tk) (q₁ : qexpr0) (a : assign_tk) (q₂ : qexpr0) : tactic unit :=
+meta def definev (h : parse ident) (c : parse colon_tk) (q₁ : parse qexpr0) (a : parse assign_tk) (q₂ : parse qexpr0) : tactic unit :=
 do t ← i_to_expr_strict q₁,
    v ← i_to_expr_strict `(%%q₂ : %%t),
    tactic.definev h t v
 
-meta def note (h : ident) (a : assign_tk) (q : qexpr0) : tactic unit :=
+meta def note (h : parse ident) (a : parse assign_tk) (q : parse qexpr0) : tactic unit :=
 do p ← i_to_expr_strict q,
    tactic.note h p
 
-meta def pose (h : ident) (a : assign_tk) (q : qexpr0) : tactic unit :=
+meta def pose (h : parse ident) (a : parse assign_tk) (q : parse qexpr0) : tactic unit :=
 do p ← i_to_expr_strict q,
    tactic.pose h p
 
@@ -406,7 +423,7 @@ tactic.trace_state
 meta def trace {α : Type} [has_to_tactic_format α] (a : α) : tactic unit :=
 tactic.trace a
 
-meta def existsi (e : qexpr0) : tactic unit :=
+meta def existsi (e : parse qexpr0) : tactic unit :=
 i_to_expr e >>= tactic.existsi
 
 /--
@@ -442,7 +459,7 @@ Given `h : a::b = c::d`, the tactic `injection h` adds to new hypothesis with ty
 to the main goal. The tactic `injection h with h₁ h₂` uses the names `h₁` an `h₂` to name the new
 hypotheses.
 -/
-meta def injection (q : qexpr0) (hs : with_ident_list) : tactic unit :=
+meta def injection (q : parse qexpr0) (hs : parse with_ident_list) : tactic unit :=
 do e ← i_to_expr q, tactic.injection_with e hs
 
 private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas
@@ -480,7 +497,7 @@ private meta def simp_lemmas.append_pexprs : simp_lemmas → list pexpr → tact
 | s []      := return s
 | s (l::ls) := do new_s ← simp_lemmas.add_pexpr s l, simp_lemmas.append_pexprs new_s ls
 
-private meta def mk_simp_set (attr_names : list name) (hs : list qexpr) (ex : list name) : tactic simp_lemmas :=
+private meta def mk_simp_set (attr_names : list name) (hs : list pexpr) (ex : list name) : tactic simp_lemmas :=
 do s₀ ← join_user_simp_lemmas attr_names,
    s₁ ← simp_lemmas.append_pexprs s₀ hs,
    return $ simp_lemmas.erase s₁ ex
@@ -500,11 +517,11 @@ do h     ← get_local h_name,
    mk_eq_mp eqpr h >>= tactic.exact,
    try $ tactic.clear h
 
-private meta def simp_hyps (cfg : simplify_config) : simp_lemmas → location → tactic unit
+private meta def simp_hyps (cfg : simplify_config) : simp_lemmas → list name → tactic unit
 | s []      := skip
 | s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs
 
-private meta def simp_core (cfg : simplify_config) (ctx : list expr) (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
+private meta def simp_core (cfg : simplify_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (loc : list name) : tactic unit :=
 do s ← mk_simp_set attr_names hs ids,
    s ← s^.append ctx,
    match loc : _ → tactic unit with
@@ -530,28 +547,28 @@ It has many variants.
 
 - `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.
 -/
-meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
+meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) : tactic unit :=
 simp_core {} [] hs attr_names ids loc
 
 /--
 Similar to the `simp` tactic, but uses contextual simplification. For example, when simplifying `t = s → p`,
 the equation `t = s` is automatically added to the set of simplification rules when simplifying `p`.
 -/
-meta def ctx_simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
+meta def ctx_simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) : tactic unit :=
 simp_core {contextual := tt} [] hs attr_names ids loc
 
 /--
 Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules.
 -/
-meta def simp_using_hs (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : tactic unit :=
+meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : tactic unit :=
 do ctx ← collect_ctx_simps,
    simp_core {} ctx hs attr_names ids []
 
-private meta def dsimp_hyps (s : simp_lemmas) : location → tactic unit
+private meta def dsimp_hyps (s : simp_lemmas) : list name → tactic unit
 | []      := skip
 | (h::hs) := get_local h >>= dsimp_at_core s
 
-meta def dsimp (es : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : location → tactic unit
+meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : parse location → tactic unit
 | [] := do s ← mk_simp_set attr_names es ids, tactic.dsimp_core s
 | hs := do s ← mk_simp_set attr_names es ids, dsimp_hyps s hs
 
@@ -584,10 +601,10 @@ tactic.ac_refl
 meta def cc : tactic unit :=
 tactic.cc
 
-meta def subst (q : qexpr0) : tactic unit :=
+meta def subst (q : parse qexpr0) : tactic unit :=
 i_to_expr q >>= tactic.subst >> try (tactic.reflexivity reducible)
 
-meta def clear : raw_ident_list → tactic unit :=
+meta def clear : parse raw_ident_list → tactic unit :=
 tactic.clear_lst
 
 private meta def to_qualified_name_core : name → list name → tactic name
@@ -609,35 +626,35 @@ private meta def to_qualified_names : list name → tactic (list name)
 | []      := return []
 | (c::cs) := do new_c ← to_qualified_name c, new_cs ← to_qualified_names cs, return (new_c::new_cs)
 
-private meta def dunfold_hyps : list name → location → tactic unit
+private meta def dunfold_hyps : list name → list name → tactic unit
 | cs []      := skip
 | cs (h::hs) := get_local h >>= dunfold_at cs >> dunfold_hyps cs hs
 
-meta def dunfold : raw_ident_list → location → tactic unit
+meta def dunfold : parse raw_ident_list → parse location → tactic unit
 | cs [] := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs
 | cs hs := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs hs
 
 /- TODO(Leo): add support for non-refl lemmas -/
-meta def unfold : raw_ident_list → location → tactic unit :=
+meta def unfold : parse raw_ident_list → parse location → tactic unit :=
 dunfold
 
-private meta def dunfold_hyps_occs : name → occurrences → location → tactic unit
+private meta def dunfold_hyps_occs : name → occurrences → list name → tactic unit
 | c occs []  := skip
 | c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs
 
-meta def dunfold_occs : ident → list nat → location → tactic unit
+meta def dunfold_occs : parse ident → list nat → parse location → tactic unit
 | c ps [] := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
 | c ps hs := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
 
 /- TODO(Leo): add support for non-refl lemmas -/
-meta def unfold_occs : ident → list nat → location → tactic unit :=
+meta def unfold_occs : parse ident → list nat → parse location → tactic unit :=
 dunfold_occs
 
-private meta def delta_hyps : list name → location → tactic unit
+private meta def delta_hyps : list name → list name → tactic unit
 | cs []      := skip
 | cs (h::hs) := get_local h >>= delta_at cs >> dunfold_hyps cs hs
 
-meta def delta : raw_ident_list → location → tactic unit
+meta def delta : parse raw_ident_list → parse location → tactic unit
 | cs [] := do new_cs ← to_qualified_names cs, tactic.delta new_cs
 | cs hs := do new_cs ← to_qualified_names cs, delta_hyps new_cs hs
 
diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean
new file mode 100644
index 0000000000..020b218808
--- /dev/null
+++ b/library/init/meta/lean/parser.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import init.data.option.basic init.category.monad init.category.alternative
+import init.meta.pexpr init.meta.interaction_monad
+
+namespace lean
+
+@[reducible] def pos := nat × nat
+
+-- TODO: make inspectable (and pure)
+meta constant parser_state : Type
+meta constant parser_state.cur_pos : parser_state → pos
+
+@[reducible] meta def parser := interaction_monad parser_state
+@[reducible] meta def parser_result := interaction_monad.result parser_state
+
+open interaction_monad
+open interaction_monad.result
+
+namespace parser
+
+/-- Make sure the next token is an identifier, consume it, and
+    produce the quoted name `t, where t is the identifier. -/
+meta constant ident : parser name
+/-- Check that the next token is `tk` and consume it. `tk` must be a registered token. -/
+meta constant tk (tk : string) : parser unit
+/-- Parse an unelaborated expression using the given right-binding power. The expression
+    may contain antiquotations (`%%e`). -/
+meta constant qexpr (rbp := nat.of_num std.prec.max) : parser pexpr
+
+/-- 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 α :=
+λ s,
+let pos₁ := parser_state.cur_pos s in
+result.cases_on (p₁ s)
+  success
+  (λ e₁ ref₁ s',
+    let pos₂ := parser_state.cur_pos s' in
+    if pos₁ ≠ pos₂ then
+      exception e₁ ref₁ s'
+    else result.cases_on (p₂ s)
+     success
+     exception)
+
+meta instance : alternative parser :=
+⟨@interaction_monad_fmap parser_state, (λ α a s, success a s), (@fapp _ _), @interaction_monad.failed parser_state, @parser_orelse⟩
+
+
+-- TODO: move
+meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type u} : f a → f (list a)
+| x := (do y ← x,
+           ys ← many x,
+           return $ y::ys) <|> pure list.nil
+
+local postfix ?:100 := optional
+local notation p ` ?: `:100 d := (λ o, option.get_or_else o d) <$> p?
+local postfix * := many
+
+meta def sep_by {α : Type} : string → parser α → parser (list α)
+| s p := (list.cons <$> p <*> (tk s *> p)*) ?: []
+
+end parser
+end lean
diff --git a/library/init/meta/quote.lean b/library/init/meta/quote.lean
new file mode 100644
index 0000000000..139300371c
--- /dev/null
+++ b/library/init/meta/quote.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import init.meta.tactic
+
+open tactic
+
+meta class has_quote (α : Type) :=
+(quote : α → pexpr)
+
+@[inline] meta def quote {α : Type} [has_quote α] : α → pexpr :=
+has_quote.quote
+
+meta instance : has_quote nat := ⟨pexpr.of_raw_expr ∘ expr.mk_prenum_macro⟩
+
+meta instance : has_quote char :=
+⟨λ ⟨n, pr⟩, ``(char.of_nat %%(quote n))⟩
+
+@[priority std.priority.default + 1]
+meta instance : has_quote string := ⟨pexpr.of_raw_expr ∘ expr.mk_string_macro⟩
+
+meta instance : has_quote unsigned :=
+⟨λ ⟨n, pr⟩, ``(unsigned.of_nat %%(quote n))⟩
+
+meta def name.quote : name → pexpr
+| name.anonymous        := ``(name.anonymous)
+| (name.mk_string s n)  := ``(name.mk_string  %%(quote s) %%(name.quote n))
+| (name.mk_numeral i n) := ``(name.mk_numeral %%(quote i) %%(name.quote n))
+
+meta instance : has_quote name := ⟨name.quote⟩
+
+--meta instance : has_quote expr  := ⟨expr.mk_quote_macro⟩
+meta instance : has_quote pexpr := ⟨pexpr.of_raw_expr ∘ expr.mk_quote_macro ∘ pexpr.to_raw_expr⟩
+
+private meta def list.quote {α : Type} [has_quote α] : list α → pexpr
+| []     := ``([])
+| (h::t) := ``(%%(quote h) :: %%(list.quote t))
+
+meta instance {α : Type} [has_quote α] : has_quote (list α) := ⟨list.quote⟩
+
+meta instance {α : Type} [has_quote α] : has_quote (option α) :=
+⟨λ opt, match opt with
+| some x := ``(option.some %%(quote x))
+| none   := ``(option.none)
+end⟩
+
+meta instance : has_quote unit := ⟨λ _, ``(unit.star)⟩
+
+meta instance {α β : Type} [has_quote α] [has_quote β] : has_quote (α × β) :=
+⟨λ ⟨x, y⟩, ``((%%(quote x), %%(quote y)))⟩
+
+meta def nat.to_expr : nat → tactic expr := λ n, to_expr $ quote n
+meta def char.to_expr : char → tactic expr := λ n, to_expr $ quote n
+meta def unsigned.to_expr : unsigned → tactic expr := λ n, to_expr $ quote n
+meta def name.to_expr : name → tactic expr := λ n, to_expr $ quote n
+meta def list_name.to_expr : list name → tactic expr := λ n, to_expr $ quote n
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index f805a3c7ed..cccff782e0 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.tactic init.meta.attribute init.meta.constructor_tactic
-import init.meta.relation_tactics init.meta.occurrences
+import init.meta.relation_tactics init.meta.occurrences init.meta.quote
 
 open tactic
 
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index a1d453fa3c..25df1632bd 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -24,8 +24,8 @@ meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_
 λ 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, tactic_result.cases_on (istep line col tac ss ts)
-  (λ ⟨a, new_ss⟩ new_ts, tactic_result.success ((), new_ss) new_ts)
+λ 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)
 
 meta def execute (tac : smt_tactic unit) : tactic unit :=
@@ -35,6 +35,8 @@ meta def execute_with (cfg : smt_config) (tac : smt_tactic unit) : tactic unit :
 using_smt tac cfg
 
 namespace interactive
+open lean.parser
+open interactive -- ?
 open interactive.types
 
 meta def itactic : Type :=
@@ -43,7 +45,7 @@ smt_tactic unit
 meta def irtactic : Type :=
 smt_tactic unit
 
-meta def intros : raw_ident_list → smt_tactic unit
+meta def intros : parse raw_ident_list → smt_tactic unit
 | [] := smt_tactic.intros
 | hs := smt_tactic.intro_lst hs
 
@@ -65,48 +67,48 @@ smt_tactic.close
 meta def ematch : smt_tactic unit :=
 smt_tactic.ematch
 
-meta def apply (q : qexpr0) : smt_tactic unit :=
+meta def apply (q : parse qexpr0) : smt_tactic unit :=
 tactic.interactive.apply q
 
-meta def fapply (q : qexpr0) : smt_tactic unit :=
+meta def fapply (q : parse qexpr0) : smt_tactic unit :=
 tactic.interactive.fapply q
 
 meta def apply_instance : smt_tactic unit :=
 tactic.apply_instance
 
-meta def change (q : qexpr0) : smt_tactic unit :=
+meta def change (q : parse qexpr0) : smt_tactic unit :=
 tactic.interactive.change q
 
-meta def exact (q : qexpr0) : smt_tactic unit :=
+meta def exact (q : parse qexpr0) : smt_tactic unit :=
 tactic.interactive.exact q
 
-meta def assert (h : ident) (c : colon_tk) (q : qexpr0) : smt_tactic unit :=
+meta def assert (h : parse ident) (c : parse colon_tk) (q : parse qexpr0) : smt_tactic unit :=
 do e ← tactic.to_expr_strict q,
    smt_tactic.assert h e
 
-meta def define (h : ident) (c : colon_tk) (q : qexpr0) : smt_tactic unit :=
+meta def define (h : parse ident) (c : parse colon_tk) (q : parse qexpr0) : smt_tactic unit :=
 do e ← tactic.to_expr_strict q,
    smt_tactic.define h e
 
-meta def assertv (h : ident) (c : colon_tk) (q₁ : qexpr0) (a : assign_tk) (q₂ : qexpr0) : smt_tactic unit :=
+meta def assertv (h : parse ident) (c : parse colon_tk) (q₁ : parse qexpr0) (a : parse assign_tk) (q₂ : parse qexpr0) : smt_tactic unit :=
 do t ← tactic.to_expr_strict q₁,
    v ← tactic.to_expr_strict `(%%q₂ : %%t),
    smt_tactic.assertv h t v
 
-meta def definev (h : ident) (c : colon_tk) (q₁ : qexpr0) (a : assign_tk) (q₂ : qexpr0) : smt_tactic unit :=
+meta def definev (h : parse ident) (c : parse colon_tk) (q₁ : parse qexpr0) (a : parse assign_tk) (q₂ : parse qexpr0) : smt_tactic unit :=
 do t ← tactic.to_expr_strict q₁,
    v ← tactic.to_expr_strict `(%%q₂ : %%t),
    smt_tactic.definev h t v
 
-meta def note (h : ident) (a : assign_tk) (q : qexpr0) : smt_tactic unit :=
+meta def note (h : parse ident) (a : parse assign_tk) (q : parse qexpr0) : smt_tactic unit :=
 do p ← tactic.to_expr_strict q,
    smt_tactic.note h p
 
-meta def pose (h : ident) (a : assign_tk) (q : qexpr0) : smt_tactic unit :=
+meta def pose (h : parse ident) (a : parse assign_tk) (q : parse qexpr0) : smt_tactic unit :=
 do p ← tactic.to_expr_strict q,
    smt_tactic.pose h p
 
-meta def add_fact (q : qexpr0) : smt_tactic unit :=
+meta def add_fact (q : parse qexpr0) : smt_tactic unit :=
 do h ← tactic.get_unused_name `h none,
    p ← tactic.to_expr_strict q,
    smt_tactic.note h p
@@ -117,11 +119,11 @@ smt_tactic.trace_state
 meta def trace {α : Type} [has_to_tactic_format α] (a : α) : smt_tactic unit :=
 tactic.trace a
 
-meta def destruct (q : qexpr0) : smt_tactic unit :=
+meta def destruct (q : parse qexpr0) : smt_tactic unit :=
 do p ← tactic.to_expr_strict q,
    smt_tactic.destruct p
 
-meta def by_cases (q : qexpr0) : smt_tactic unit :=
+meta def by_cases (q : parse qexpr0) : smt_tactic unit :=
 do p ← tactic.to_expr_strict q,
    smt_tactic.by_cases p
 
@@ -157,10 +159,10 @@ private meta def add_lemma_pexprs (md : transparency) (lhs_lemma : bool) : list
 | []      := return ()
 | (p::ps) := add_lemma_pexpr md lhs_lemma p >> add_lemma_pexprs ps
 
-meta def add_lemma (l : qexpr_list_or_qexpr0) : smt_tactic unit :=
+meta def add_lemma (l : parse qexpr_list_or_qexpr0) : smt_tactic unit :=
 add_lemma_pexprs reducible ff l
 
-meta def add_lhs_lemma (l : qexpr_list_or_qexpr0) : smt_tactic unit :=
+meta def add_lhs_lemma (l : parse qexpr_list_or_qexpr0) : smt_tactic unit :=
 add_lemma_pexprs reducible tt l
 
 private meta def add_eqn_lemmas_for_core (md : transparency) : list name → smt_tactic unit
@@ -172,10 +174,10 @@ private meta def add_eqn_lemmas_for_core (md : transparency) : list name → smt
   | _                        := fail $ "'" ++ to_string c ++ "' is not a constant"
   end
 
-meta def add_eqn_lemmas_for (ids : raw_ident_list) : smt_tactic unit :=
+meta def add_eqn_lemmas_for (ids : parse raw_ident_list) : smt_tactic unit :=
 add_eqn_lemmas_for_core reducible ids
 
-meta def add_eqn_lemmas (ids : raw_ident_list) : smt_tactic unit :=
+meta def add_eqn_lemmas (ids : parse raw_ident_list) : smt_tactic unit :=
 add_eqn_lemmas_for ids
 
 private meta def add_hinst_lemma_from_name (md : transparency) (lhs_lemma : bool) (n : name) (hs : hinst_lemmas) (ref : expr) : smt_tactic hinst_lemmas :=
@@ -206,7 +208,7 @@ private meta def add_hinst_lemmas_from_pexprs (md : transparency) (lhs_lemma : b
 | []      hs := return hs
 | (p::ps) hs := do hs₁ ← add_hinst_lemma_from_pexpr md lhs_lemma p hs, add_hinst_lemmas_from_pexprs ps hs₁
 
-meta def ematch_using (l : qexpr_list_or_qexpr0) : smt_tactic unit :=
+meta def ematch_using (l : parse qexpr_list_or_qexpr0) : smt_tactic unit :=
 do hs ← add_hinst_lemmas_from_pexprs reducible ff l hinst_lemmas.mk,
    smt_tactic.ematch_using hs
 
@@ -222,21 +224,21 @@ smt_tactic.repeat t
 meta def all_goals (t : itactic) : smt_tactic unit :=
 smt_tactic.all_goals t
 
-meta def induction (p : qexpr0) (rec_name : using_ident) (ids : with_ident_list) : smt_tactic unit :=
+meta def induction (p : parse qexpr0) (rec_name : parse using_ident) (ids : parse with_ident_list) : smt_tactic unit :=
 slift (tactic.interactive.induction p rec_name ids)
 
 /-- Simplify the target type of the main goal. -/
-meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : smt_tactic unit :=
+meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
 tactic.interactive.simp hs attr_names ids []
 
-meta def ctx_simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : smt_tactic unit :=
+meta def ctx_simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
 tactic.interactive.ctx_simp hs attr_names ids []
 
 /-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/
-meta def simp_using_hs (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : smt_tactic unit :=
+meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
 tactic.interactive.simp_using_hs hs attr_names ids
 
-meta def dsimp (es : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) : smt_tactic unit :=
+meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
 tactic.interactive.dsimp es attr_names ids []
 
 /-- Keep applying heuristic instantiation until the current goal is solved, or it fails. -/
@@ -244,7 +246,7 @@ meta def eblast : smt_tactic unit :=
 smt_tactic.eblast
 
 /-- Keep applying heuristic instantiation using the given lemmas until the current goal is solved, or it fails. -/
-meta def eblast_using (l : qexpr_list_or_qexpr0) : smt_tactic unit :=
+meta def eblast_using (l : parse qexpr_list_or_qexpr0) : smt_tactic unit :=
 do hs ← add_hinst_lemmas_from_pexprs reducible ff l hinst_lemmas.mk,
    smt_tactic.repeat (smt_tactic.ematch_using hs >> smt_tactic.try smt_tactic.close)
 
diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index 32e39e40c1..491537a74e 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -72,11 +72,11 @@ meta instance (α : Type) : has_coe (tactic α) (smt_tactic α) :=
 ⟨monad.monad_lift⟩
 
 meta def smt_tactic_orelse {α : Type} (t₁ t₂ : smt_tactic α) : smt_tactic α :=
-λ ss ts, tactic_result.cases_on (t₁ ss ts)
-  tactic_result.success
-  (λ e₁ ref₁ s', tactic_result.cases_on (t₂ ss ts)
-     tactic_result.success
-     tactic_result.exception)
+λ ss ts, result.cases_on (t₁ ss ts)
+  result.success
+  (λ e₁ ref₁ s', result.cases_on (t₂ ss ts)
+     result.success
+     result.exception)
 
 meta instance : monad_fail smt_tactic :=
 { smt_tactic.monad with fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α) }
@@ -152,9 +152,9 @@ meta def fail {α : Type} {β : Type u} [has_to_format β] (msg : β) : tactic 
 tactic.fail msg
 
 meta def try {α : Type} (t : smt_tactic α) : smt_tactic unit :=
-λ ss ts, tactic_result.cases_on (t ss ts)
- (λ ⟨a, new_ss⟩, tactic_result.success ((), new_ss))
- (λ e ref s', tactic_result.success ((), ss) ts)
+λ ss ts, result.cases_on (t ss ts)
+ (λ ⟨a, new_ss⟩, result.success ((), new_ss))
+ (λ e ref s', result.success ((), ss) ts)
 
 /- (repeat_at_most n t): repeat the given tactic at most n times or until t fails -/
 meta def repeat_at_most : nat → smt_tactic unit → smt_tactic unit
@@ -180,7 +180,7 @@ do s₁ ← state_t.read,
    return (s₁, s₂)
 
 protected meta def write : smt_state × tactic_state → smt_tactic unit :=
-λ ⟨ss, ts⟩ _ _, tactic_result.success ((), ss) ts
+λ ⟨ss, ts⟩ _ _, result.success ((), ss) ts
 
 private meta def mk_smt_goals_for (cfg : smt_config) : list expr → list smt_goal → list expr
                                   → tactic (list smt_goal × list expr)
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index eda041b9a1..6cc73a360c 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -7,7 +7,8 @@ prelude
 import init.function init.data.option.basic init.util
 import init.category.combinators init.category.monad init.category.alternative init.category.monad_fail
 import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment
-import init.meta.pexpr init.data.to_string init.data.string.basic
+import init.meta.pexpr init.data.to_string init.data.string.basic init.meta.interaction_monad
+
 meta constant tactic_state : Type
 
 universes u v
@@ -26,79 +27,28 @@ end tactic_state
 meta instance : has_to_format tactic_state :=
 ⟨tactic_state.to_format⟩
 
-meta inductive tactic_result (α : Type u)
-| success      : α → tactic_state → tactic_result
-| exception {} : option (unit → format) → option expr → tactic_state → tactic_result
+@[reducible] meta def tactic := interaction_monad tactic_state
+@[reducible] meta def tactic_result := interaction_monad.result tactic_state
 
+namespace tactic
+  export interaction_monad (hiding failed fail)
+  meta def failed {α : Type} : tactic α := interaction_monad.failed
+  meta def fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : tactic α :=
+  interaction_monad.fail msg
+end tactic
+
+namespace tactic_result
+  export interaction_monad.result
+end tactic_result
+
+open tactic
 open tactic_result
 
-section
-variables {α : Type u}
-variables [has_to_string α]
-
-meta def tactic_result_to_string : tactic_result α → string
-| (success a s)              := to_string a
-| (exception (some t) ref s) := "Exception: " ++ to_string (t ())
-| (exception none ref s)     := "[silent exception]"
-
-meta instance : has_to_string (tactic_result α) :=
-⟨tactic_result_to_string⟩
-end
-
-attribute [reducible]
-meta def tactic (α : Type u) :=
-tactic_state → tactic_result α
-
-section
-variables {α : Type u} {β : Type v}
-
-@[inline] meta def tactic_fmap (f : α → β) (t : tactic α) : tactic β :=
-λ s, tactic_result.cases_on (t s)
-  (λ a s', success (f a) s')
-  (λ e s', exception e s')
-
-@[inline] meta def tactic_bind (t₁ : tactic α) (t₂ : α → tactic β) : tactic β :=
-λ s,  tactic_result.cases_on (t₁ s)
-  (λ a s', t₂ a s')
-  (λ e s', exception e s')
-
-@[inline] meta def tactic_return (a : α) : tactic α :=
-λ s, success a s
-
-meta def tactic_orelse {α : Type u} (t₁ t₂ : tactic α) : tactic α :=
-λ s, tactic_result.cases_on (t₁ s)
-  success
-  (λ e₁ ref₁ s', tactic_result.cases_on (t₂ s)
-     success
-     exception)
-
-@[inline] meta def tactic_seq (t₁ : tactic α) (t₂ : tactic β) : tactic β :=
-tactic_bind t₁ (λ a, t₂)
-
-infixl ` >>=[tactic] `:2 := tactic_bind
-infixl ` >>[tactic] `:2  := tactic_seq
-end
-
-meta instance : monad tactic :=
-{map := @tactic_fmap, ret := @tactic_return, bind := @tactic_bind}
-
-meta def tactic.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : tactic_state) : tactic_result α :=
-exception (some (λ _, to_fmt msg)) none s
-
-meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : tactic α :=
-λ s, tactic.mk_exception msg none s
-
-meta def tactic.silent_fail {α : Type u} : tactic α :=
-λ s, exception none none s
-
-meta def tactic.failed {α : Type u} : tactic α :=
-tactic.fail "failed"
-
-meta instance : monad_fail tactic :=
-{ tactic.monad with fail := λ α s, tactic.fail (to_fmt s) }
+infixl ` >>=[tactic] `:2 := interaction_monad_bind
+infixl ` >>[tactic] `:2  := interaction_monad_seq
 
 meta instance : alternative tactic :=
-⟨@tactic_fmap, (λ α a s, success a s), (@fapp _ _), @tactic.failed, @tactic_orelse⟩
+⟨@interaction_monad_fmap tactic_state, (λ α a s, success a s), (@fapp _ _), @interaction_monad.failed tactic_state, @interaction_monad_orelse tactic_state⟩
 
 meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.{u₁} α) :=
 λ s, match t s with
@@ -116,7 +66,7 @@ namespace tactic
 variables {α : Type u}
 
 meta def try_core (t : tactic α) : tactic (option α) :=
-λ s, tactic_result.cases_on (t s)
+λ s, result.cases_on (t s)
  (λ a, success (some a))
  (λ e ref s', success none s)
 
@@ -127,7 +77,7 @@ meta def try (t : tactic α) : tactic unit :=
 try_core t >>[tactic] skip
 
 meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
-λ s, tactic_result.cases_on (t s)
+λ s, result.cases_on (t s)
  (λ a s, mk_exception "fail_if_success combinator failed, given tactic succeeded" none s)
  (λ e ref s', success () s)
 
@@ -156,7 +106,7 @@ meta instance opt_to_tac : has_coe (option α) (tactic α) :=
 
 /- Decorate t's exceptions with msg -/
 meta def decorate_ex (msg : format) (t : tactic α) : tactic α :=
-λ s, tactic_result.cases_on (t s)
+λ s, result.cases_on (t s)
   success
   (λ opt_thunk,
      match opt_thunk with
@@ -211,30 +161,13 @@ has_to_tactic_format.to_tactic_format
 
 open tactic format
 
-meta def list_to_tactic_format_aux {α : Type u} [has_to_tactic_format α] : bool → list α → tactic format
-| b  []     := return $ to_fmt ""
-| b (x::xs) := do
-  f₁ ← pp x,
-  f₂ ← list_to_tactic_format_aux ff xs,
-  return $ (if ¬ b then to_fmt "," ++ line else nil) ++ f₁ ++ f₂
-
-meta def list_to_tactic_format {α : Type u} [has_to_tactic_format α] : list α → tactic format
-| []      := return $ to_fmt "[]"
-| (x::xs) := do
-  f ← list_to_tactic_format_aux tt (x::xs),
-  return $ to_fmt "[" ++ group (nest 1 f) ++ to_fmt "]"
-
 meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (list α) :=
-⟨list_to_tactic_format⟩
-
-meta def pair_to_tactic_format_aux {α : Type u} {β : Type v} [has_to_tactic_format α] [has_to_tactic_format β] :
-         α × β → tactic format
-| (a, b) := do
-  fa ← pp a, fb ← pp b,
-  return $ to_fmt "(" ++ fa ++ ", " ++ fb ++ ")"
+⟨fmap to_fmt ∘ monad.mapm pp⟩
 
 meta instance (α : Type u) (β : Type v) [has_to_tactic_format α] [has_to_tactic_format β] :
- has_to_tactic_format (α × β) := ⟨pair_to_tactic_format_aux⟩
+ has_to_tactic_format (α × β) :=
+⟨λ ⟨a, b⟩, to_fmt <$> (prod.mk <$> pp a <*> pp b)⟩
+
 
 meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] : option α → tactic format
 | (some a) := do fa ← pp a, return (to_fmt "(some " ++ fa ++ ")")
@@ -526,8 +459,8 @@ meta def report_exception {α : Type} (line col : nat) : option (unit → format
 /- 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, tactic_result.cases_on (istep line col t s)
-  (λ a new_s, tactic_result.success () new_s)
+λ 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 is_prop (e : expr) : tactic bool :=
@@ -996,36 +929,6 @@ end
 
 end tactic
 
-open tactic
-
-meta def nat.to_expr : nat → tactic expr
-| n :=
-  if n = 0 then to_expr `(0)
-  else if n = 1 then to_expr `(1)
-  else do
-    r : expr ← nat.to_expr (n / 2),
-    if n % 2 = 0 then to_expr `(bit0 %%r)
-    else to_expr `(bit1 %%r)
-
-meta def char.to_expr : char → tactic expr
-| ⟨n, pr⟩ := do e ← n^.to_expr, to_expr `(char.of_nat %%e)
-
-meta def string.to_expr : string → tactic expr
-| []      := to_expr `(string.empty)
-| (c::cs) := do e ← c^.to_expr, es ← string.to_expr cs, to_expr `(string.str %%e %%es)
-
-meta def unsigned.to_expr : unsigned → tactic expr
-| ⟨n, pr⟩ := do e ← n^.to_expr, to_expr `(unsigned.of_nat %%e)
-
-meta def name.to_expr : name → tactic expr
-| name.anonymous        := to_expr `(name.anonymous)
-| (name.mk_string s n)  := do es ← s^.to_expr, en ← name.to_expr n, to_expr `(name.mk_string %%es %%en)
-| (name.mk_numeral i n) := do is ← i^.to_expr, en ← name.to_expr n, to_expr `(name.mk_string %%is %%en)
-
-meta def list_name.to_expr : list name → tactic expr
-| []     := to_expr `([] : list name)
-| (h::t) := do eh ← h^.to_expr, et ← list_name.to_expr t, to_expr `(%%eh :: %%et)
-
 notation [parsing_only] `command`:max := tactic unit
 
 open tactic
diff --git a/library/tools/super/prover.lean b/library/tools/super/prover.lean
index d1f2610715..4d36e2cae5 100644
--- a/library/tools/super/prover.lean
+++ b/library/tools/super/prover.lean
@@ -110,14 +110,14 @@ end
 namespace tactic.interactive
 open interactive
 
-meta def with_lemmas (ls : types.raw_ident_list) : tactic unit := monad.for' ls $ λl, do
+meta def with_lemmas (ls : parse types.raw_ident_list) : tactic unit := monad.for' ls $ λl, do
 p ← mk_const l,
 t ← infer_type p,
 n ← get_unused_name p^.get_app_fn^.const_name none,
 tactic.assertv n t p
 
-meta def super (extra_clause_names : types.raw_ident_list)
-               (extra_lemma_names : types.with_ident_list) : tactic unit := do
+meta def super (extra_clause_names : parse types.raw_ident_list)
+               (extra_lemma_names : parse types.with_ident_list) : tactic unit := do
 with_lemmas extra_clause_names,
 extra_lemmas ← monad.for extra_lemma_names mk_const,
 _root_.super extra_lemmas
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 49df683a17..5bb373216c 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -618,7 +618,7 @@ static expr parse_do(parser_state & p, unsigned, expr const *, pos_info const &)
     return r;
 }
 
-static expr parse_quoted_expr(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+static expr parse_lazy_quoted_expr(parser_state & p, unsigned, expr const *, pos_info const & pos) {
     if (p.in_quote())
         throw parser_error("invalid nested quoted expression", pos);
     parser_state::quote_scope scope(p, true);
@@ -632,6 +632,20 @@ static expr parse_quoted_expr(parser_state & p, unsigned, expr const *, pos_info
     return p.save_pos(mk_quote(e), pos);
 }
 
+static expr parse_quoted_expr(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+    if (p.in_quote())
+        throw parser_error("invalid nested quoted expression", pos);
+    parser_state::quote_scope scope(p, true, id_behavior::ErrorIfUndef);
+    expr e = p.parse_expr();
+    if (p.curr_is_token(get_colon_tk())) {
+        p.next();
+        expr t = p.parse_expr();
+        e = mk_typed_expr_distrib_choice(p, t, e, pos);
+    }
+    p.check_token_next(get_rparen_tk(), "invalid quoted expression, `)` expected");
+    return p.save_pos(mk_quote(e), pos);
+}
+
 static expr parse_antiquote_expr(parser_state & p, unsigned, expr const *, pos_info const & pos) {
     if (!p.in_quote())
         throw parser_error("invalid antiquotation, occurs outside of quoted expressions", pos);
@@ -791,7 +805,8 @@ parse_table init_nud_table() {
     r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);
     r = r.add({transition("⟨", mk_ext_action(parse_constructor))}, x0);
     r = r.add({transition("{", mk_ext_action(parse_curly_bracket))}, x0);
-    r = r.add({transition("`(", mk_ext_action(parse_quoted_expr))}, x0);
+    r = r.add({transition("`(", mk_ext_action(parse_lazy_quoted_expr))}, x0);
+    r = r.add({transition("``(", mk_ext_action(parse_quoted_expr))}, x0);
     r = r.add({transition("`[", mk_ext_action(parse_auto_quote_tactic_block))}, x0);
     r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0);
     r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0);
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 062887de51..ee2a54a562 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2944,7 +2944,8 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
     tactic_state s       = mk_tactic_state_for(mvar);
 
     try {
-        if (optional<tactic_state> new_s = tactic_evaluator(m_ctx, m_opts)(s, tactic, ref)) {
+        vm_obj r = tactic_evaluator(m_ctx, m_opts, ref)(tactic, s);
+        if (auto new_s = is_tactic_success(r)) {
             metavar_context mctx = new_s->mctx();
             expr val = mctx.instantiate_mvars(new_s->main());
             if (has_expr_metavar(val)) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index aa11af9b4d..0bf2789714 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -109,19 +109,17 @@ parser::local_scope::~local_scope() {
     m_p.m_env = m_env;
 }
 
-parser::quote_scope::quote_scope(parser & p, bool q):
-    m_p(p), m_id_behavior(m_p.m_id_behavior), m_in_quote(q),
+parser::quote_scope::quote_scope(parser & p, bool q, id_behavior i):
+    m_p(p), m_id_behavior(m_p.m_id_behavior), m_old_in_quote(m_p.m_in_quote), m_in_quote(q),
     m_saved_in_pattern(p.m_in_pattern) {
     m_p.m_in_pattern = false;
-    if (q) {
-        lean_assert(!m_p.m_in_quote);
-        m_p.m_id_behavior = id_behavior::AssumeLocalIfNotLocal;
+    if (m_in_quote && !m_old_in_quote) {
+        m_p.m_id_behavior = i;
         m_p.m_in_quote = true;
         m_p.push_local_scope(false);
         m_p.m_quote_stack = cons(m_p.mk_parser_scope(), m_p.m_quote_stack);
         m_p.clear_expr_locals();
-    } else {
-        lean_assert(m_p.m_in_quote);
+    } else if (!m_in_quote && m_old_in_quote) {
         lean_assert(m_p.m_quote_stack);
         m_p.m_id_behavior = id_behavior::ErrorIfUndef;
         m_p.push_local_scope(false);
@@ -132,12 +130,12 @@ parser::quote_scope::quote_scope(parser & p, bool q):
 
 parser::quote_scope::~quote_scope() {
     m_p.m_in_pattern = m_saved_in_pattern;
-    if (m_in_quote) {
+    if (m_in_quote && !m_old_in_quote) {
         lean_assert(m_p.m_in_quote);
         m_p.m_in_quote = false;
         m_p.pop_local_scope();
         m_p.m_quote_stack = tail(m_p.m_quote_stack);
-    } else {
+    } else if (!m_in_quote && m_old_in_quote) {
         lean_assert(!m_p.m_in_quote);
         m_p.m_in_quote = true;
         m_p.pop_local_scope();
@@ -2071,10 +2069,6 @@ expr parser::parse_expr_with_env(local_environment const & lenv, unsigned rbp) {
     return parse_expr(rbp);
 }
 
-expr parser::parse_tactic(unsigned) {
-    lean_unreachable();
-}
-
 /** \brief Helper class for creating type context only if needed */
 class lazy_type_context : public abstract_type_context {
     environment m_env;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 8d5e208f80..b3cfc333cd 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -393,8 +393,6 @@ public:
     expr parse_scoped_expr(buffer<expr> const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
     expr parse_expr_with_env(local_environment const & lenv, unsigned rbp = 0);
 
-    expr parse_tactic(unsigned rbp = 0);
-
     void parse_imports(unsigned & fingerprint, std::vector<module_name> &);
 
     struct local_scope {
@@ -408,9 +406,10 @@ public:
     struct quote_scope {
         parser &    m_p;
         id_behavior m_id_behavior;
+        bool        m_old_in_quote;
         bool        m_in_quote;
         bool        m_saved_in_pattern;
-        quote_scope(parser & p, bool q);
+        quote_scope(parser & p, bool q, id_behavior i = id_behavior::AssumeLocalIfNotLocal);
         ~quote_scope();
     };
 
diff --git a/src/frontends/lean/prenum.h b/src/frontends/lean/prenum.h
index a6ee91a9a5..47c2474247 100644
--- a/src/frontends/lean/prenum.h
+++ b/src/frontends/lean/prenum.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/expr.h"
+#include "util/numerics/mpz.h"
 
 namespace lean {
 /** \brief Create a pre-numeral. We create pre-numerals at parsing time. The elaborator is responsible for
diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp
index ac635eaa10..6a7b045860 100644
--- a/src/frontends/lean/tactic_evaluator.cpp
+++ b/src/frontends/lean/tactic_evaluator.cpp
@@ -36,33 +36,7 @@ elaborator_exception unsolved_tactic_state(tactic_state const & ts, char const *
     throw_unsolved_tactic_state(ts, format(msg), ref);
 }
 
-/* Compile tactic into bytecode */
-environment tactic_evaluator::compile_tactic(name const & tactic_name, expr const & tactic) {
-    pos_info_provider * provider = get_pos_info_provider();
-    expr tactic_type     = m_ctx.infer(tactic);
-    environment new_env  = m_ctx.env();
-    bool use_conv_opt    = true;
-    bool is_trusted      = false;
-    auto cd = check(new_env, mk_definition(new_env, tactic_name, {}, tactic_type, tactic, use_conv_opt, is_trusted));
-    new_env = new_env.add(cd);
-    if (auto pos = provider->get_pos_info(tactic))
-        new_env = add_transient_decl_pos_info(new_env, tactic_name, *pos);
-    try {
-        return vm_compile(new_env, new_env.get(tactic_name));
-    } catch (exception & ex) {
-        throw elaborator_exception(tactic, ex.what());
-    }
-}
-
-vm_obj tactic_evaluator::invoke_tactic(vm_state & S, name const & tactic_name, std::initializer_list<vm_obj> const & args) {
-    vm_state::profiler prof(S, m_opts);
-    vm_obj r = S.invoke(tactic_name, args);
-    if (prof.enabled())
-        prof.get_snapshots().display(get_global_ios().get_regular_stream());
-    return r;
-}
-
-static void process_failure(vm_state & S, vm_obj const & r, expr const & ref) {
+void tactic_evaluator::process_failure(vm_state & S, vm_obj const & r) {
     pos_info_provider * provider = get_pos_info_provider();
     if (optional<tactic_exception_info> ex = is_tactic_exception(S, r)) {
         format fmt          = std::get<0>(*ex);
@@ -71,37 +45,17 @@ static void process_failure(vm_state & S, vm_obj const & r, expr const & ref) {
         if (ref1 && provider && provider->get_pos_info(*ref1))
             throw elaborator_exception(*ref1, fmt);
         else
-            throw_unsolved_tactic_state(s1, fmt, ref);
+            throw_unsolved_tactic_state(s1, fmt, m_ref);
     }
     /* Do nothing if it is a silent failure */
     lean_assert(is_tactic_silent_exception(r));
 }
 
-optional<tactic_state> tactic_evaluator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
-    name tactic_name("_tactic");
-    environment new_env = compile_tactic(tactic_name, tactic);
-    vm_state S(new_env, m_opts);
-    vm_obj r = invoke_tactic(S, tactic_name, {to_obj(s)});
-
-    if (optional<tactic_state> new_s = is_tactic_success(r)) {
-        return new_s;
-    }
-    process_failure(S, r, ref);
-    return optional<tactic_state>();
-}
-
-optional<tactic_state> tactic_evaluator::execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref) {
-    optional<tactic_state> new_s = execute_tactic(tactic, s, ref);
-    if (new_s && new_s->goals())
-        throw_unsolved_tactic_state(*new_s, "tactic failed, there are unsolved goals", ref);
-    return new_s;
-}
-
-optional<tactic_state> tactic_evaluator::operator()(tactic_state const & s, expr const & tactic, expr const & ref) {
-    return execute_atomic(s, tactic, ref);
-}
-
-tactic_evaluator::tactic_evaluator(type_context & ctx, options const & opts):
-    m_ctx(ctx), m_opts(opts) {
+vm_obj tactic_evaluator::operator()(expr const & tactic, tactic_state const & s) {
+    vm_obj r = tactic::evaluator::operator()(tactic, s);
+    if (auto s = is_tactic_success(r))
+        if (s->goals())
+            throw_unsolved_tactic_state(*s, "tactic failed, there are unsolved goals", m_ref);
+    return r;
 }
 }
diff --git a/src/frontends/lean/tactic_evaluator.h b/src/frontends/lean/tactic_evaluator.h
index 36efd9689c..71cf781355 100644
--- a/src/frontends/lean/tactic_evaluator.h
+++ b/src/frontends/lean/tactic_evaluator.h
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "library/tactic/tactic_state.h"
+#include "library/tactic/elaborator_exception.h"
+#include "library/vm/interaction_state.h"
 #include "frontends/lean/info_manager.h"
 
 namespace lean {
@@ -14,18 +16,14 @@ elaborator_exception unsolved_tactic_state(tactic_state const & ts, char const *
 [[noreturn]] void throw_unsolved_tactic_state(tactic_state const & ts, format const & fmt, expr const & ref);
 [[noreturn]] void throw_unsolved_tactic_state(tactic_state const & ts, char const * msg, expr const & ref);
 
-class tactic_evaluator {
-    type_context &  m_ctx;
-    options const & m_opts;
-
-    environment compile_tactic(name const & tactic_name, expr const & tactic);
-    vm_obj invoke_tactic(vm_state & S, name const & tactic_name, std::initializer_list<vm_obj> const & args);
-
-    optional<tactic_state> execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref);
-    optional<tactic_state> execute_atomic(tactic_state const & s, expr const & tactic, expr const & ref);
+class tactic_evaluator : public tactic::evaluator {
+private:
+    expr m_ref;
+protected:
+    virtual void process_failure(vm_state & S, vm_obj const & r) override;
 public:
-    tactic_evaluator(type_context & ctx, options const & opts);
-
-    optional<tactic_state> operator()(tactic_state const & s, expr const & tactic, expr const & ref);
+    tactic_evaluator(type_context & ctx, options const & opts, expr const & ref):
+            tactic::evaluator(ctx, opts), m_ref(ref) {}
+    virtual vm_obj operator()(expr const & tactic, tactic_state const & s) override;
 };
 }
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 1a4713e0f3..8d5ca2c41d 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -14,15 +14,18 @@ Author: Leonardo de Moura
 #include "library/typed_expr.h"
 #include "library/placeholder.h"
 #include "library/scope_pos_info_provider.h"
-#include "library/io_state.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_format.h"
+#include "library/vm/vm_expr.h"
+#include "library/vm/vm_parser.h"
 #include "library/tactic/elaborate.h"
-#include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/tactic_notation.h"
+#include "frontends/lean/tactic_evaluator.h"
+#include "frontends/lean/elaborator.h"
+#include "frontends/lean/pp.h"
 
 /* The auto quotation currently supports two classes of tactics: tactic and smt_tactic.
    To add a new class Tac, we have to
@@ -119,200 +122,12 @@ static optional<name> is_auto_quote_tactic(parser & p, name const & tac_class) {
         return optional<name>();
 }
 
-static expr mk_lean_list(buffer<expr> const & es) {
-    expr r = mk_constant(get_list_nil_name());
-    unsigned i = es.size();
-    while (i > 0) {
-        --i;
-        r = mk_app(mk_constant(get_list_cons_name()), es[i], r);
-    }
-    return r;
-}
-
-static expr mk_lean_none() {
-    return mk_constant(get_option_none_name());
-}
-
-static expr mk_lean_some(expr const & e) {
-    return mk_app(mk_constant(get_option_some_name()), e);
-}
-
-static expr parse_quoted_ident(parser & p, name const & decl_name) {
-    if (!p.curr_is_identifier())
-        throw parser_error(sstream() << "invalid auto-quote tactic '" << decl_name  << "', identifier expected", p.pos());
-    auto pos = p.pos();
-    name id  = p.get_name_val();
-    p.next();
-    return p.save_pos(quote_name(id), pos);
-}
-
-static expr parse_optional_quoted_ident(parser & p, name const & decl_name) {
-    auto pos = p.pos();
-    if (p.curr_is_identifier())
-        return p.save_pos(mk_lean_some(parse_quoted_ident(p, decl_name)), pos);
-    else
-        return p.save_pos(mk_lean_none(), pos);
-}
-
-
-static expr parse_using_id(parser & p, name const & decl_name) {
-    auto pos = p.pos();
-    if (p.curr_is_token(get_using_tk())) {
-        p.next();
-        return p.save_pos(mk_lean_some(parse_quoted_ident(p, decl_name)), pos);
-    } else {
-        return p.save_pos(mk_lean_none(), pos);
-    }
-}
-
-/* Remark: rbp for '<|>' is 2, ';' is 1, and ',' is 0
-   qexpr0 shoud use rbp 2.
-
-   TODO(Leo): rename qexpr0 to something else */
-static expr parse_qexpr(parser & p, unsigned rbp = 2) {
-    auto pos = p.pos();
-    expr e;
-    /* TODO(Leo): avoid p.in_quote by improving
-       parser::quote_scope constructor */
-    if (p.in_quote()) {
-        e = p.parse_expr(rbp);
-    } else {
-        parser::quote_scope scope(p, true);
-        e = p.parse_expr(rbp);
-    }
-    return p.save_pos(mk_quote(e), pos);
-}
-
-static expr parse_qexpr_list(parser & p) {
-    buffer<expr> result;
-    p.check_token_next(get_lbracket_tk(), "invalid auto-quote tactic argument, '[' expected");
-    while (!p.curr_is_token(get_rbracket_tk())) {
-        result.push_back(parse_qexpr(p));
-        if (!p.curr_is_token(get_comma_tk())) break;
-        p.next();
-    }
-    p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic argument, ']' expected");
-    return mk_lean_list(result);
-}
-
-static expr parse_opt_qexpr_list(parser & p) {
-    if (p.curr_is_token(get_lbracket_tk()))
-        return parse_qexpr_list(p);
-    else
-        return mk_constant(get_list_nil_name());
-}
-
-static expr parse_qexpr_list_or_qexpr0(parser & p) {
-    if (p.curr_is_token(get_lbracket_tk())) {
-        return parse_qexpr_list(p);
-    } else {
-        buffer<expr> args;
-        args.push_back(parse_qexpr(p));
-        /* Remark: We do not save position information for list.cons and list.nil.
-           Reason: consider the tactic
-              rw add_zero a
-           Now, assume we use the position immediately before add_zero for list.cons.
-           Then, info_manager::add_type_inf will store the type of list.cons and
-           the type of add_zero for this position, and the lean server may incorrectly report
-           the type of list.cons when we hover over add_zero. */
-        return mk_lean_list(args);
-    }
-}
-
-static expr mk_pair(expr const & e1, expr const & e2) {
-    return mk_app(mk_constant(get_prod_mk_name()), e1, e2);
-}
-
-/* Convert given position into an expression of type (prod nat nat) */
-static expr to_expr_pos(pos_info const & pos) {
-    return mk_pair(mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second)));
-}
-
 // small 'info' tweak: for `,`, report tactic state at following token instead
 static void info_tweak(parser & p) {
     if (!p.get_complete() && p.get_break_at_pos() == some(p.pos()))
         p.set_break_at_pos({p.pos().first, p.pos().second + 1});
 }
 
-static expr parse_qexpr_list_with_pos(parser & p) {
-    buffer<expr> result;
-    p.check_token_next(get_lbracket_tk(), "invalid auto-quote tactic argument, '[' expected");
-    while (!p.curr_is_token(get_rbracket_tk())) {
-        auto pos = p.pos();
-        try {
-            expr pos_expr = to_expr_pos(pos);
-            expr tac      = parse_qexpr(p, 0);
-            result.push_back(mk_pair(tac, pos_expr));
-            if (!p.curr_is_token(get_comma_tk())) break;
-            info_tweak(p);
-            p.next();
-        } catch (break_at_pos_exception & ex) {
-            ex.report_goal_pos(pos);
-            throw ex;
-        }
-    }
-    info_tweak(p);
-    p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic argument, ']' expected");
-    return mk_lean_list(result);
-}
-
-static expr parse_qexpr_list_or_qexpr0_with_pos(parser & p) {
-    if (p.curr_is_token(get_lbracket_tk())) {
-        return parse_qexpr_list_with_pos(p);
-    } else {
-        buffer<expr> args;
-        expr pos = to_expr_pos(p.pos());
-        expr tac = parse_qexpr(p);
-        args.push_back(mk_pair(tac, pos));
-        /* Remark: We do not save position information for list.cons and list.nil.
-           Reason: consider the tactic
-              rw add_zero a
-           Now, assume we use the position immediately before add_zero for list.cons.
-           Then, info_manager::add_type_inf will store the type of list.cons and
-           the type of add_zero for this position, and the lean server may incorrectly report
-           the type of list.cons when we hover over add_zero. */
-        return mk_lean_list(args);
-    }
-}
-
-static expr parse_raw_id_list(parser & p) {
-    buffer<expr> result;
-    while (p.curr_is_identifier()) {
-        auto id_pos = p.pos();
-        name id = p.get_name_val();
-        p.next();
-        result.push_back(p.save_pos(quote_name(id), id_pos));
-    }
-    return mk_lean_list(result);
-}
-
-static expr parse_with_id_list(parser & p) {
-    if (p.curr_is_token(get_with_tk())) {
-        p.next();
-        return parse_raw_id_list(p);
-    } else {
-        return mk_constant(get_list_nil_name());
-    }
-}
-
-static expr parse_without_id_list(parser & p) {
-    if (p.curr_is_token(get_without_tk())) {
-        p.next();
-        return parse_raw_id_list(p);
-    } else {
-        return mk_constant(get_list_nil_name());
-    }
-}
-
-static expr parse_location(parser & p) {
-    if (p.curr_is_token(get_at_tk())) {
-        p.next();
-        return parse_raw_id_list(p);
-    } else {
-        return mk_constant(get_list_nil_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_nested_auto_quote_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) {
@@ -326,6 +141,17 @@ static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class, b
     }
 }
 
+static expr parse_interactive_param(parser & p, expr const & ty, expr const & quote_inst, expr const & lean_parser) {
+    vm_obj vm_parsed = run_parser(p, lean_parser);
+    type_context ctx(p.env());
+    name n("_quote_inst");
+    tactic_evaluator eval(ctx, p.get_options(), ty);
+    auto env = eval.compile(n, quote_inst);
+    vm_state S(env, p.get_options());
+    auto vm_res = S.invoke(n, vm_parsed);
+    return to_expr(vm_res);
+}
+
 static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_rstep, bool report_error) {
     auto pos = p.pos();
     p.next();
@@ -336,43 +162,11 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
     while (is_pi(type)) {
         if (is_explicit(binding_info(type))) {
             expr arg_type = binding_domain(type);
-            if (is_constant(arg_type, get_interactive_types_qexpr_name())) {
-                args.push_back(parse_qexpr(p, get_max_prec()));
-            } else if (is_constant(arg_type, get_interactive_types_qexpr0_name())) {
-                args.push_back(parse_qexpr(p));
-            } else if (is_constant(arg_type, get_interactive_types_qexpr_list_name())) {
-                args.push_back(parse_qexpr_list(p));
-            } else if (is_constant(arg_type, get_interactive_types_qexpr_list_with_pos_name())) {
-                args.push_back(parse_qexpr_list_with_pos(p));
-            } else if (is_constant(arg_type, get_interactive_types_opt_qexpr_list_name())) {
-                args.push_back(parse_opt_qexpr_list(p));
-            } else if (is_constant(arg_type, get_interactive_types_qexpr_list_or_qexpr0_name())) {
-                args.push_back(parse_qexpr_list_or_qexpr0(p));
-            } else if (is_constant(arg_type, get_interactive_types_qexpr_list_or_qexpr0_with_pos_name())) {
-                args.push_back(parse_qexpr_list_or_qexpr0_with_pos(p));
-            } else if (is_constant(arg_type, get_interactive_types_ident_name())) {
-                args.push_back(parse_quoted_ident(p, decl_name));
-            } else if (is_constant(arg_type, get_interactive_types_opt_ident_name())) {
-                args.push_back(parse_optional_quoted_ident(p, decl_name));
-            } else if (is_constant(arg_type, get_interactive_types_raw_ident_list_name())) {
-                args.push_back(parse_raw_id_list(p));
-            } else if (is_constant(arg_type, get_interactive_types_with_ident_list_name())) {
-                args.push_back(parse_with_id_list(p));
-            } else if (is_constant(arg_type, get_interactive_types_without_ident_list_name())) {
-                args.push_back(parse_without_id_list(p));
-            } else if (is_constant(arg_type, get_interactive_types_using_ident_name())) {
-                args.push_back(parse_using_id(p, decl_name));
-            } else if (is_constant(arg_type, get_interactive_types_location_name())) {
-                args.push_back(parse_location(p));
-            } else if (is_constant(arg_type, get_interactive_types_colon_tk_name())) {
-                p.check_token_next(get_colon_tk(), "invalid auto-quote tactic, ':' expected");
-                args.push_back(mk_constant(get_unit_star_name()));
-            } else if (is_constant(arg_type, get_interactive_types_assign_tk_name())) {
-                p.check_token_next(get_assign_tk(), "invalid auto-quote tactic, ':=' expected");
-                args.push_back(mk_constant(get_unit_star_name()));
-            } else if (is_constant(arg_type, get_interactive_types_comma_tk_name())) {
-                p.check_token_next(get_comma_tk(), "invalid auto-quote tactic, ',' expected");
-                args.push_back(mk_constant(get_unit_star_name()));
+            if (is_app_of(arg_type, get_interactive_parse_name())) {
+                buffer<expr> arg_args;
+                get_app_args(arg_type, arg_args);
+                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_auto_quote_tactic(p, tac_class, use_rstep, report_error));
@@ -418,6 +212,13 @@ struct parse_tactic_fn {
         return m_p.save_pos(mk_app(mk_constant(get_orelse_name()), tac1, tac2), pos);
     }
 
+    expr parse_qexpr(unsigned rbp = 0) {
+        auto p = m_p.pos();
+        parser::quote_scope scope(m_p, true);
+        expr e = m_p.parse_expr(rbp);
+        return m_p.save_pos(mk_quote(e), p);
+    }
+
     expr parse_elem_core(bool save_info) {
         try {
             m_p.check_break_before();
@@ -433,7 +234,7 @@ struct parse_tactic_fn {
         if (auto dname = is_auto_quote_tactic(m_p, m_tac_class)) {
             r = parse_auto_quote_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error);
         } else if (is_curr_exact_shortcut(m_p)) {
-            expr arg = parse_qexpr(m_p);
+            expr arg = parse_qexpr();
             r = m_p.mk_app(m_p.save_pos(mk_constant(m_tac_class + name({"interactive", "exact"})), pos), arg, pos);
             if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error);
         } else {
@@ -579,7 +380,7 @@ struct parse_begin_end_block_fn {
 
     expr mk_save_info() {
         expr r = mk_tactic_save_info(m_p, {m_p.pos().first, m_p.pos().second+1}, m_tac_class);
-        info_tweak(m_p);
+       info_tweak(m_p);
         return r;
     }
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 942b2577cc..abeeceec29 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -81,7 +81,7 @@ void init_token_table(token_table & t) {
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0},
          {"have", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
          {"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
-         {"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
+         {"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"``(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
          {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index dcfb3dc0f4..0e01f61b79 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -173,6 +173,7 @@ name const * g_int_ne_neg_of_pos = nullptr;
 name const * g_int_neg_ne_zero_of_ne = nullptr;
 name const * g_int_zero_ne_neg_of_ne = nullptr;
 name const * g_int_decidable_linear_ordered_comm_group = nullptr;
+name const * g_interactive_parse = nullptr;
 name const * g_inv = nullptr;
 name const * g_io = nullptr;
 name const * g_io_functor = nullptr;
@@ -447,24 +448,6 @@ name const * g_tactic_triv = nullptr;
 name const * g_tactic_interactive = nullptr;
 name const * g_tactic_interactive_exact = nullptr;
 name const * g_trivial = nullptr;
-name const * g_interactive_types_ident = nullptr;
-name const * g_interactive_types_opt_ident = nullptr;
-name const * g_interactive_types_using_ident = nullptr;
-name const * g_interactive_types_ident_list = nullptr;
-name const * g_interactive_types_raw_ident_list = nullptr;
-name const * g_interactive_types_with_ident_list = nullptr;
-name const * g_interactive_types_without_ident_list = nullptr;
-name const * g_interactive_types_location = nullptr;
-name const * g_interactive_types_qexpr = nullptr;
-name const * g_interactive_types_qexpr0 = nullptr;
-name const * g_interactive_types_qexpr_list = nullptr;
-name const * g_interactive_types_qexpr_list_with_pos = nullptr;
-name const * g_interactive_types_opt_qexpr_list = nullptr;
-name const * g_interactive_types_qexpr_list_or_qexpr0 = nullptr;
-name const * g_interactive_types_qexpr_list_or_qexpr0_with_pos = nullptr;
-name const * g_interactive_types_colon_tk = nullptr;
-name const * g_interactive_types_assign_tk = nullptr;
-name const * g_interactive_types_comma_tk = nullptr;
 name const * g_thunk = nullptr;
 name const * g_to_fmt = nullptr;
 name const * g_to_int = nullptr;
@@ -661,6 +644,7 @@ void initialize_constants() {
     g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"};
     g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"};
     g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"};
+    g_interactive_parse = new name{"interactive", "parse"};
     g_inv = new name{"inv"};
     g_io = new name{"io"};
     g_io_functor = new name{"io", "functor"};
@@ -935,24 +919,6 @@ void initialize_constants() {
     g_tactic_interactive = new name{"tactic", "interactive"};
     g_tactic_interactive_exact = new name{"tactic", "interactive", "exact"};
     g_trivial = new name{"trivial"};
-    g_interactive_types_ident = new name{"interactive", "types", "ident"};
-    g_interactive_types_opt_ident = new name{"interactive", "types", "opt_ident"};
-    g_interactive_types_using_ident = new name{"interactive", "types", "using_ident"};
-    g_interactive_types_ident_list = new name{"interactive", "types", "ident_list"};
-    g_interactive_types_raw_ident_list = new name{"interactive", "types", "raw_ident_list"};
-    g_interactive_types_with_ident_list = new name{"interactive", "types", "with_ident_list"};
-    g_interactive_types_without_ident_list = new name{"interactive", "types", "without_ident_list"};
-    g_interactive_types_location = new name{"interactive", "types", "location"};
-    g_interactive_types_qexpr = new name{"interactive", "types", "qexpr"};
-    g_interactive_types_qexpr0 = new name{"interactive", "types", "qexpr0"};
-    g_interactive_types_qexpr_list = new name{"interactive", "types", "qexpr_list"};
-    g_interactive_types_qexpr_list_with_pos = new name{"interactive", "types", "qexpr_list_with_pos"};
-    g_interactive_types_opt_qexpr_list = new name{"interactive", "types", "opt_qexpr_list"};
-    g_interactive_types_qexpr_list_or_qexpr0 = new name{"interactive", "types", "qexpr_list_or_qexpr0"};
-    g_interactive_types_qexpr_list_or_qexpr0_with_pos = new name{"interactive", "types", "qexpr_list_or_qexpr0_with_pos"};
-    g_interactive_types_colon_tk = new name{"interactive", "types", "colon_tk"};
-    g_interactive_types_assign_tk = new name{"interactive", "types", "assign_tk"};
-    g_interactive_types_comma_tk = new name{"interactive", "types", "comma_tk"};
     g_thunk = new name{"thunk"};
     g_to_fmt = new name{"to_fmt"};
     g_to_int = new name{"to_int"};
@@ -1150,6 +1116,7 @@ void finalize_constants() {
     delete g_int_neg_ne_zero_of_ne;
     delete g_int_zero_ne_neg_of_ne;
     delete g_int_decidable_linear_ordered_comm_group;
+    delete g_interactive_parse;
     delete g_inv;
     delete g_io;
     delete g_io_functor;
@@ -1424,24 +1391,6 @@ void finalize_constants() {
     delete g_tactic_interactive;
     delete g_tactic_interactive_exact;
     delete g_trivial;
-    delete g_interactive_types_ident;
-    delete g_interactive_types_opt_ident;
-    delete g_interactive_types_using_ident;
-    delete g_interactive_types_ident_list;
-    delete g_interactive_types_raw_ident_list;
-    delete g_interactive_types_with_ident_list;
-    delete g_interactive_types_without_ident_list;
-    delete g_interactive_types_location;
-    delete g_interactive_types_qexpr;
-    delete g_interactive_types_qexpr0;
-    delete g_interactive_types_qexpr_list;
-    delete g_interactive_types_qexpr_list_with_pos;
-    delete g_interactive_types_opt_qexpr_list;
-    delete g_interactive_types_qexpr_list_or_qexpr0;
-    delete g_interactive_types_qexpr_list_or_qexpr0_with_pos;
-    delete g_interactive_types_colon_tk;
-    delete g_interactive_types_assign_tk;
-    delete g_interactive_types_comma_tk;
     delete g_thunk;
     delete g_to_fmt;
     delete g_to_int;
@@ -1638,6 +1587,7 @@ name const & get_int_ne_neg_of_pos_name() { return *g_int_ne_neg_of_pos; }
 name const & get_int_neg_ne_zero_of_ne_name() { return *g_int_neg_ne_zero_of_ne; }
 name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne; }
 name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; }
+name const & get_interactive_parse_name() { return *g_interactive_parse; }
 name const & get_inv_name() { return *g_inv; }
 name const & get_io_name() { return *g_io; }
 name const & get_io_functor_name() { return *g_io_functor; }
@@ -1912,24 +1862,6 @@ name const & get_tactic_triv_name() { return *g_tactic_triv; }
 name const & get_tactic_interactive_name() { return *g_tactic_interactive; }
 name const & get_tactic_interactive_exact_name() { return *g_tactic_interactive_exact; }
 name const & get_trivial_name() { return *g_trivial; }
-name const & get_interactive_types_ident_name() { return *g_interactive_types_ident; }
-name const & get_interactive_types_opt_ident_name() { return *g_interactive_types_opt_ident; }
-name const & get_interactive_types_using_ident_name() { return *g_interactive_types_using_ident; }
-name const & get_interactive_types_ident_list_name() { return *g_interactive_types_ident_list; }
-name const & get_interactive_types_raw_ident_list_name() { return *g_interactive_types_raw_ident_list; }
-name const & get_interactive_types_with_ident_list_name() { return *g_interactive_types_with_ident_list; }
-name const & get_interactive_types_without_ident_list_name() { return *g_interactive_types_without_ident_list; }
-name const & get_interactive_types_location_name() { return *g_interactive_types_location; }
-name const & get_interactive_types_qexpr_name() { return *g_interactive_types_qexpr; }
-name const & get_interactive_types_qexpr0_name() { return *g_interactive_types_qexpr0; }
-name const & get_interactive_types_qexpr_list_name() { return *g_interactive_types_qexpr_list; }
-name const & get_interactive_types_qexpr_list_with_pos_name() { return *g_interactive_types_qexpr_list_with_pos; }
-name const & get_interactive_types_opt_qexpr_list_name() { return *g_interactive_types_opt_qexpr_list; }
-name const & get_interactive_types_qexpr_list_or_qexpr0_name() { return *g_interactive_types_qexpr_list_or_qexpr0; }
-name const & get_interactive_types_qexpr_list_or_qexpr0_with_pos_name() { return *g_interactive_types_qexpr_list_or_qexpr0_with_pos; }
-name const & get_interactive_types_colon_tk_name() { return *g_interactive_types_colon_tk; }
-name const & get_interactive_types_assign_tk_name() { return *g_interactive_types_assign_tk; }
-name const & get_interactive_types_comma_tk_name() { return *g_interactive_types_comma_tk; }
 name const & get_thunk_name() { return *g_thunk; }
 name const & get_to_fmt_name() { return *g_to_fmt; }
 name const & get_to_int_name() { return *g_to_int; }
diff --git a/src/library/constants.h b/src/library/constants.h
index fc56ee53c8..492c3b4043 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -175,6 +175,7 @@ name const & get_int_ne_neg_of_pos_name();
 name const & get_int_neg_ne_zero_of_ne_name();
 name const & get_int_zero_ne_neg_of_ne_name();
 name const & get_int_decidable_linear_ordered_comm_group_name();
+name const & get_interactive_parse_name();
 name const & get_inv_name();
 name const & get_io_name();
 name const & get_io_functor_name();
@@ -449,24 +450,6 @@ name const & get_tactic_triv_name();
 name const & get_tactic_interactive_name();
 name const & get_tactic_interactive_exact_name();
 name const & get_trivial_name();
-name const & get_interactive_types_ident_name();
-name const & get_interactive_types_opt_ident_name();
-name const & get_interactive_types_using_ident_name();
-name const & get_interactive_types_ident_list_name();
-name const & get_interactive_types_raw_ident_list_name();
-name const & get_interactive_types_with_ident_list_name();
-name const & get_interactive_types_without_ident_list_name();
-name const & get_interactive_types_location_name();
-name const & get_interactive_types_qexpr_name();
-name const & get_interactive_types_qexpr0_name();
-name const & get_interactive_types_qexpr_list_name();
-name const & get_interactive_types_qexpr_list_with_pos_name();
-name const & get_interactive_types_opt_qexpr_list_name();
-name const & get_interactive_types_qexpr_list_or_qexpr0_name();
-name const & get_interactive_types_qexpr_list_or_qexpr0_with_pos_name();
-name const & get_interactive_types_colon_tk_name();
-name const & get_interactive_types_assign_tk_name();
-name const & get_interactive_types_comma_tk_name();
 name const & get_thunk_name();
 name const & get_to_fmt_name();
 name const & get_to_int_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 9f05741510..239b000f35 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -168,6 +168,7 @@ int.ne_neg_of_pos
 int.neg_ne_zero_of_ne
 int.zero_ne_neg_of_ne
 int_decidable_linear_ordered_comm_group
+interactive.parse
 inv
 io
 io.functor
@@ -442,24 +443,6 @@ tactic.triv
 tactic.interactive
 tactic.interactive.exact
 trivial
-interactive.types.ident
-interactive.types.opt_ident
-interactive.types.using_ident
-interactive.types.ident_list
-interactive.types.raw_ident_list
-interactive.types.with_ident_list
-interactive.types.without_ident_list
-interactive.types.location
-interactive.types.qexpr
-interactive.types.qexpr0
-interactive.types.qexpr_list
-interactive.types.qexpr_list_with_pos
-interactive.types.opt_qexpr_list
-interactive.types.qexpr_list_or_qexpr0
-interactive.types.qexpr_list_or_qexpr0_with_pos
-interactive.types.colon_tk
-interactive.types.assign_tk
-interactive.types.comma_tk
 thunk
 to_fmt
 to_int
diff --git a/src/library/io_state.h b/src/library/io_state.h
index 636dc579bb..0d4a7fc8b9 100644
--- a/src/library/io_state.h
+++ b/src/library/io_state.h
@@ -60,9 +60,9 @@ class formatted_exception : public exception {
 protected:
     optional<expr> m_expr;
     format         m_fmt;
-    formatted_exception(optional<expr> const & e, format const & fmt):m_expr(e), m_fmt(fmt) {}
 public:
     explicit formatted_exception(format const & fmt):m_fmt(fmt) {}
+    formatted_exception(optional<expr> const & e, format const & fmt):m_expr(e), m_fmt(fmt) {}
     formatted_exception(expr const & e, format const & fmt):m_expr(e), m_fmt(fmt) {}
     virtual ~formatted_exception() noexcept {}
     virtual char const * what() const noexcept;
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index b7ca687906..78b05f14fe 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -199,28 +199,16 @@ format tactic_state::pp_goal(expr const & g) const {
     return pp_goal(fmtf, g);
 }
 
-struct vm_tactic_state : public vm_external {
-    tactic_state m_val;
-    vm_tactic_state(tactic_state const & v):m_val(v) {}
-    virtual ~vm_tactic_state() {}
-    virtual void dealloc() override {
-        this->~vm_tactic_state(); get_vm_allocator().deallocate(sizeof(vm_tactic_state), this);
-    }
-    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_tactic_state(m_val); }
-    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_tactic_state))) vm_tactic_state(m_val); }
-};
-
 bool is_tactic_state(vm_obj const & o) {
-    return is_external(o) && dynamic_cast<vm_tactic_state*>(to_external(o));
+    return tactic::is_State(o);
 }
 
 tactic_state const & to_tactic_state(vm_obj const & o) {
-    lean_vm_check(dynamic_cast<vm_tactic_state*>(to_external(o)));
-    return static_cast<vm_tactic_state*>(to_external(o))->m_val;
+    return tactic::to_State(o);
 }
 
 vm_obj to_obj(tactic_state const & s) {
-    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_tactic_state))) vm_tactic_state(s));
+    return tactic::to_obj(s);
 }
 
 transparency_mode to_transparency_mode(vm_obj const & o) {
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index b04d24ab90..c80174c0d5 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/defeq_canonizer.h"
 #include "library/vm/vm.h"
+#include "library/vm/interaction_state.h"
 
 namespace lean {
 typedef defeq_canonizer::state defeq_can_state;
@@ -121,6 +122,9 @@ template<typename T> tactic_state update_option_if_undef(tactic_state const & s,
     return set_options(s, s.get_options().update_if_undef(n, v));
 }
 
+template class interaction_monad<tactic_state>;
+typedef interaction_monad<tactic_state> tactic;
+
 bool is_tactic_state(vm_obj const & o);
 tactic_state const & to_tactic_state(vm_obj const & o);
 vm_obj to_obj(tactic_state const & s);
diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt
index a2416dd6c8..5ddd14db34 100644
--- a/src/library/vm/CMakeLists.txt
+++ b/src/library/vm/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
   vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
   vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp
-  vm_native.cpp vm_int.cpp init_module.cpp)
+  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp)
diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp
index 84b0149e2a..4c08bb8458 100644
--- a/src/library/vm/init_module.cpp
+++ b/src/library/vm/init_module.cpp
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_declaration.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_task.h"
+#include "library/vm/vm_parser.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -43,8 +44,10 @@ void initialize_vm_core_module() {
     initialize_vm_task();
     initialize_vm_declaration();
     initialize_vm_environment();
+    initialize_vm_parser();
 }
 void finalize_vm_core_module() {
+    finalize_vm_parser();
     finalize_vm_environment();
     finalize_vm_declaration();
     finalize_vm_task();
diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h
new file mode 100644
index 0000000000..97ed9d4907
--- /dev/null
+++ b/src/library/vm/interaction_state.h
@@ -0,0 +1,241 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura, Sebastian Ullrich
+*/
+#pragma once
+#include <algorithm>
+#include "util/sstream.h"
+#include "kernel/environment.h"
+#include "library/metavar_context.h"
+#include "library/type_context.h"
+#include "library/defeq_canonizer.h"
+#include "library/scope_pos_info_provider.h"
+#include "util/fresh_name.h"
+#include "util/sexpr/option_declarations.h"
+#include "kernel/type_checker.h"
+#include "kernel/instantiate.h"
+#include "library/constants.h"
+#include "library/pp_options.h"
+#include "library/trace.h"
+#include "library/util.h"
+#include "library/cache_helper.h"
+#include "library/module.h"
+#include "library/documentation.h"
+#include "library/scoped_ext.h"
+#include "library/aux_definition.h"
+#include "library/unfold_macros.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_environment.h"
+#include "library/vm/vm_exceptional.h"
+#include "library/vm/vm_format.h"
+#include "library/vm/vm_string.h"
+#include "library/vm/vm_options.h"
+#include "library/vm/vm_name.h"
+#include "library/vm/vm_nat.h"
+#include "library/vm/vm_level.h"
+#include "library/vm/vm_declaration.h"
+#include "library/vm/vm_expr.h"
+#include "library/vm/vm_list.h"
+#include "library/vm/vm_option.h"
+#include "library/compiler/vm_compiler.h"
+
+namespace lean {
+
+template <class State>
+struct interaction_monad {
+    struct vm_State : public vm_external {
+        State m_val;
+
+        vm_State(State const & v) : m_val(v) {}
+
+        virtual ~vm_State() {}
+
+        virtual void dealloc() override {
+            this->~vm_State();
+            get_vm_allocator().deallocate(sizeof(vm_State), this);
+        }
+
+        virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_State(m_val); }
+
+        virtual vm_external * clone(vm_clone_fn const &) override {
+            return new(get_vm_allocator().allocate(sizeof(vm_State))) vm_State(m_val);
+        }
+    };
+
+    static bool is_State(vm_obj const & o) {
+        return is_external(o) && dynamic_cast<vm_State *>(to_external(o));
+    }
+
+    static State const & to_State(vm_obj const & o) {
+        lean_vm_check(dynamic_cast<vm_State*>(to_external(o)));
+        return static_cast<vm_State *>(to_external(o))->m_val;
+    }
+
+    static vm_obj to_obj(State const & s) {
+        return mk_vm_external(new(get_vm_allocator().allocate(sizeof(vm_State))) vm_State(s));
+    }
+
+    static bool is_success(vm_obj const & o) {
+        return is_constructor(o) && cidx(o) == 0;
+    }
+
+    typedef std::tuple<format, optional<expr>, State> exception_info;
+
+    static optional<exception_info> is_exception(vm_state & S, vm_obj const & ex) {
+        if (is_constructor(ex) && cidx(ex) == 1 && !is_none(cfield(ex, 0))) {
+            vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit());
+            optional<expr> ref;
+            if (!is_none(cfield(ex, 1)))
+                ref = to_expr(get_some_value(cfield(ex, 1)));
+            return optional<exception_info>(to_format(fmt), ref, to_State(cfield(ex, 2)));
+        } else {
+            return optional<exception_info>();
+        }
+    }
+
+    static bool is_silent_exception(vm_obj const & ex) {
+        return is_constructor(ex) && cidx(ex) == 1 && is_none(cfield(ex, 0));
+    }
+
+    static vm_obj mk_result(vm_obj const & a, vm_obj const & s) {
+        lean_assert(is_State(s));
+        return mk_vm_constructor(0, a, s);
+    }
+
+    static bool is_result_exception(vm_obj const & r) {
+        return is_constructor(r) && cidx(r) == 1;
+    }
+
+    static bool is_result_success(vm_obj const & r) {
+        return is_constructor(r) && cidx(r) == 0;
+    }
+
+    static vm_obj get_result_value(vm_obj const & r) {
+        lean_assert(is_result_success(r));
+        return cfield(r, 0);
+    }
+
+    static vm_obj get_result_state(vm_obj const & r) {
+        lean_assert(is_result_success(r));
+        return cfield(r, 1);
+    }
+
+    static vm_obj mk_success(vm_obj const & a, State const & s) {
+        return mk_vm_constructor(0, a, to_obj(s));
+    }
+
+    static vm_obj mk_success(State const & s) {
+        return mk_success(mk_vm_unit(), s);
+    }
+
+    static vm_obj mk_exception(vm_obj const & fn, State const & s) {
+        return mk_vm_constructor(1, mk_vm_some(fn), mk_vm_none(), to_obj(s));
+    }
+
+    static vm_obj mk_silent_exception(State const & s) {
+        return mk_vm_constructor(1, mk_vm_none(), mk_vm_none(), to_obj(s));
+    }
+
+    static vm_obj mk_exception(vm_obj const & fn, vm_obj const & ref, State const & s) {
+        return mk_vm_constructor(1, mk_vm_some(fn), ref, to_obj(s));
+    }
+
+    static vm_obj mk_exception(throwable const & ex, State const & s) {
+        vm_obj _ex = lean::to_obj(ex);
+        vm_obj fn = mk_vm_closure(get_throwable_to_format_fun_idx(), 1, &_ex);
+        optional<expr> ref;
+        if (auto kex = dynamic_cast<ext_exception const *>(&ex))
+            ref = kex->get_main_expr();
+        else if (auto fex = dynamic_cast<formatted_exception const *>(&ex))
+            ref = fex->get_main_expr();
+        vm_obj _ref = ref ? mk_vm_some(lean::to_obj(*ref)) : mk_vm_none();
+        return mk_exception(fn, _ref, s);
+    }
+
+    static vm_obj mk_exception(format const & fmt, State const & s) {
+        vm_state const & S = get_vm_state();
+        if (optional<vm_decl> K = S.get_decl(get_combinator_K_name())) {
+            return mk_exception(mk_vm_closure(K->get_idx(), lean::to_obj(fmt), mk_vm_unit(), mk_vm_unit()), s);
+        } else {
+            throw exception("failed to create tactic exceptional result, combinator.K is not in the environment, "
+                                    "this can happen when users are hacking the init folder");
+        }
+    }
+
+    static vm_obj mk_exception(char const * msg, State const & s) {
+        return mk_exception(format(msg), s);
+    }
+
+    static vm_obj mk_exception(sstream const & strm, State const & s) {
+        return mk_exception(strm.str().c_str(), s);
+    }
+
+    static vm_obj mk_exception(std::function<format()> const & thunk, State const & s) {
+        return mk_exception(mk_vm_format_thunk(thunk), s);
+    }
+
+    static void report_exception(vm_state & S, vm_obj const & r) {
+        if (optional<exception_info> ex = is_exception(S, r)) {
+            format fmt = std::get<0>(*ex);
+            optional<expr> ref1 = std::get<1>(*ex);
+            throw formatted_exception(ref1, fmt);
+        }
+    }
+
+    class evaluator {
+        type_context & m_ctx;
+        options const & m_opts;
+
+    protected:
+        virtual void process_failure(vm_state & S, vm_obj const & r) {
+            report_exception(S, r);
+            /* Do nothing if it is a silent failure */
+            lean_assert(is_silent_exception(r));
+        }
+
+    public:
+        environment compile(name const & interaction_name, expr const & interaction) {
+            pos_info_provider * provider = get_pos_info_provider();
+            expr interaction_type = m_ctx.infer(interaction);
+            environment new_env = m_ctx.env();
+            bool use_conv_opt = true;
+            bool is_trusted = false;
+            auto cd = check(new_env,
+                            mk_definition(new_env, interaction_name, {}, interaction_type, interaction, use_conv_opt,
+                                          is_trusted));
+            new_env = new_env.add(cd);
+            if (auto pos = provider->get_pos_info(interaction))
+                new_env = add_transient_decl_pos_info(new_env, interaction_name, *pos);
+            try {
+                return vm_compile(new_env, new_env.get(interaction_name));
+            } catch (exception & ex) {
+                throw formatted_exception(interaction, format(ex.what()));
+            }
+        }
+
+        vm_obj invoke(vm_state & S, name const & interaction_name, std::initializer_list<vm_obj> const & args) {
+            vm_state::profiler prof(S, m_opts);
+            vm_obj r = S.invoke(interaction_name, args);
+            if (prof.enabled())
+                prof.get_snapshots().display(get_global_ios().get_regular_stream());
+            return r;
+        }
+
+        evaluator(type_context & ctx, options const & opts) : m_ctx(ctx), m_opts(opts) {}
+
+        virtual vm_obj operator()(expr const & interaction, State const & s) {
+            name interaction_name("_interaction");
+            environment new_env = compile(interaction_name, interaction);
+            vm_state S(new_env, m_opts);
+            vm_obj r = invoke(S, interaction_name, {to_obj(s)});
+
+            if (!is_success(r))
+                process_failure(S, r);
+            return r;
+        }
+    };
+};
+
+}
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index b35c3f38ec..24519096e7 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -6,6 +6,9 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <iostream>
+#include <library/quote.h>
+#include <frontends/lean/prenum.h>
+#include <library/string.h>
 #include "kernel/expr.h"
 #include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
@@ -418,6 +421,18 @@ vm_obj expr_is_choice_macro(vm_obj const & e) {
     return mk_vm_bool(is_choice(to_expr(e)));
 }
 
+vm_obj expr_mk_quote_macro(vm_obj const & e) {
+    return to_obj(mk_quote(to_expr(e)));
+}
+
+vm_obj expr_mk_prenum_macro(vm_obj const & n) {
+    return to_obj(mk_prenum(is_simple(n) ? mpz{cidx(n)} : to_mpz(n)));
+}
+
+vm_obj expr_mk_string_macro(vm_obj const & s) {
+    return to_obj(from_string(to_string(s)));
+}
+
 vm_obj expr_mk_sorry(vm_obj const & t) {
     return to_obj(mk_sorry(to_expr(t)));
 }
@@ -477,6 +492,9 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name("mk_int_val_ne_proof"),        vm_mk_int_val_ne_proof);
 
     DECLARE_VM_BUILTIN(name("expr", "is_choice_macro"),    expr_is_choice_macro);
+    DECLARE_VM_BUILTIN(name("expr", "mk_quote_macro"),     expr_mk_quote_macro);
+    DECLARE_VM_BUILTIN(name("expr", "mk_prenum_macro"),    expr_mk_prenum_macro);
+    DECLARE_VM_BUILTIN(name("expr", "mk_string_macro"),    expr_mk_string_macro);
 
     DECLARE_VM_BUILTIN(name("expr", "mk_sorry"), expr_mk_sorry);
     DECLARE_VM_BUILTIN(name("expr", "is_sorry"), expr_is_sorry);
diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp
new file mode 100644
index 0000000000..a808c3e599
--- /dev/null
+++ b/src/library/vm/vm_parser.cpp
@@ -0,0 +1,88 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#include "library/vm/vm_parser.h"
+#include <string>
+#include <iostream>
+#include <vector>
+#include <library/num.h>
+#include <library/quote.h>
+#include "frontends/lean/parser.h"
+#include "library/trace.h"
+#include "library/type_context.h"
+#include "frontends/lean/info_manager.h"
+#include "frontends/lean/elaborator.h"
+#include "library/tactic/elaborate.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_string.h"
+#include "library/vm/vm_expr.h"
+#include "library/vm/vm_nat.h"
+#include "library/vm/interaction_state.h"
+#include "util/task_queue.h"
+
+namespace lean {
+
+struct lean_parser_state {
+    parser * m_p;
+};
+
+template class interaction_monad<lean_parser_state>;
+typedef interaction_monad<lean_parser_state> lean_parser;
+
+#define TRY try {
+#define CATCH } catch (exception const & ex) { return lean_parser::mk_exception(ex, s); }
+
+vm_obj run_parser(parser & p, expr const & spec) {
+    type_context ctx(p.env(), p.get_options());
+    return lean_parser::get_result_value(lean_parser::evaluator(ctx, p.get_options())(spec, lean_parser_state {&p}));
+}
+
+vm_obj vm_parser_state_cur_pos(vm_obj const & o) {
+    auto const & s = lean_parser::to_State(o);
+    auto pos = s.m_p->pos();
+    return mk_vm_pair(mk_vm_nat(pos.first), mk_vm_nat(pos.second));
+}
+
+vm_obj vm_parser_ident(vm_obj const & o) {
+    auto const & s = lean_parser::to_State(o);
+    TRY;
+        name ident = s.m_p->check_id_next("identifier expected");
+        return lean_parser::mk_success(to_obj(ident), s);
+    CATCH;
+}
+
+vm_obj vm_parser_tk(vm_obj const & vm_tk, vm_obj const & o) {
+    auto const & s = lean_parser::to_State(o);
+    TRY;
+        name tk = to_string(vm_tk);
+        if (!s.m_p->curr_is_token(tk))
+            throw parser_error(sstream() << "'" << tk << "' expected", s.m_p->pos());
+        s.m_p->next();
+        return lean_parser::mk_success(s);
+    CATCH;
+}
+
+vm_obj vm_parser_qexpr(vm_obj const & vm_rbp, vm_obj const & o) {
+    auto const & s = lean_parser::to_State(o);
+    TRY;
+        auto rbp = to_unsigned(vm_rbp);
+        parser::quote_scope scope(*s.m_p, true);
+        expr e = s.m_p->parse_expr(rbp);
+        return lean_parser::mk_success(to_obj(e), s);
+    CATCH;
+}
+
+void initialize_vm_parser() {
+    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(name({"lean", "parser", "tk"}), vm_parser_tk);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),  vm_parser_qexpr);
+}
+
+void finalize_vm_parser() {
+}
+
+}
diff --git a/src/library/vm/vm_parser.h b/src/library/vm/vm_parser.h
new file mode 100644
index 0000000000..70cf408b9e
--- /dev/null
+++ b/src/library/vm/vm_parser.h
@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#pragma once
+#include "library/vm/vm.h"
+#include "frontends/lean/parser.h"
+
+namespace lean {
+vm_obj run_parser(parser & p, expr const & spec);
+void initialize_vm_parser();
+void finalize_vm_parser();
+}
+
diff --git a/tests/lean/bad_error5.lean.expected.out b/tests/lean/bad_error5.lean.expected.out
index 275ed4cd97..56451cb2cc 100644
--- a/tests/lean/bad_error5.lean.expected.out
+++ b/tests/lean/bad_error5.lean.expected.out
@@ -2,7 +2,7 @@ bad_error5.lean:13:10: error: don't know how to synthesize placeholder
 context:
 c : S
 ⊢ Type ?
-bad_error5.lean:13:10: error: failed to add declaration '_tactic' to environment, value has metavariables
+bad_error5.lean:13:10: error: failed to add declaration '_interaction' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   …
 bad_error5.lean:9:11: warning: declaration 'V' uses sorry
diff --git a/tests/lean/elab3.lean.expected.out b/tests/lean/elab3.lean.expected.out
index 18480348c2..cd1c0321ec 100644
--- a/tests/lean/elab3.lean.expected.out
+++ b/tests/lean/elab3.lean.expected.out
@@ -1,4 +1,5 @@
-@pre_monad.and_then.{0 0} unit unit tactic.{0} (@monad.to_pre_monad.{0 0} tactic.{0} tactic.monad.{0})
+@pre_monad.and_then.{0 0} unit unit tactic.{0}
+  (@monad.to_pre_monad.{0 0} tactic.{0} (@interaction_monad.monad.{0} tactic_state))
   tactic.trace_state
   tactic.trace_state :
   tactic.{0} unit
diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out
index 2c019f186b..9b5539d3e2 100644
--- a/tests/lean/elab_error_recovery.lean.expected.out
+++ b/tests/lean/elab_error_recovery.lean.expected.out
@@ -16,7 +16,7 @@ elab_error_recovery.lean:10:11: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
 ⊢ Type ?
-elab_error_recovery.lean:10:11: error: failed to add declaration '_tactic' to environment, value has metavariables
+elab_error_recovery.lean:10:11: error: failed to add declaration '_interaction' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   …
 elab_error_recovery.lean:12:20: error: invalid type ascription, expression has type
diff --git a/tests/lean/inline_issue.lean.expected.out b/tests/lean/inline_issue.lean.expected.out
index a409049c12..9ac1101429 100644
--- a/tests/lean/inline_issue.lean.expected.out
+++ b/tests/lean/inline_issue.lean.expected.out
@@ -1,6 +1,6 @@
 world
 hello
 ------------
-_tactic
+_interaction
 g
 f
diff --git a/tests/lean/interactive/my_tac_class.lean b/tests/lean/interactive/my_tac_class.lean
index 36ab1c99d5..057712882f 100644
--- a/tests/lean/interactive/my_tac_class.lean
+++ b/tests/lean/interactive/my_tac_class.lean
@@ -16,11 +16,11 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
 t >> return ()
 
 meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
-λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
-  (λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
+λ 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 >> tactic.silent_fail) new_s | none := tactic.silent_fail new_s end)
+        (tactic.report_error line col msg >> interaction_monad.silent_fail) 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/rb_map_ts.lean b/tests/lean/interactive/rb_map_ts.lean
index 19cecc1fe7..886afae221 100644
--- a/tests/lean/interactive/rb_map_ts.lean
+++ b/tests/lean/interactive/rb_map_ts.lean
@@ -16,11 +16,11 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
 t >> return ()
 
 meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
-λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
-  (λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
+λ 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 >> tactic.silent_fail) new_s | none := tactic.silent_fail new_s end)
+        (tactic.report_error line col msg >> interaction_monad.silent_fail) new_s | none := interaction_monad.silent_fail new_s end)
 
 meta def execute (tac : mytac unit) : tactic unit :=
 tac (name_map.mk nat) >> return ()
@@ -45,9 +45,11 @@ tactic.trace s
 meta def assumption : mytac unit :=
 tactic.assumption
 
+open lean.parser
+open interactive
 open interactive.types
 
-meta def add (n : ident) (v : nat) : mytac unit :=
+meta def add (n : parse ident) (v : nat) : mytac unit :=
 do m ← state_t.read, state_t.write (m^.insert n v)
 
 end interactive
diff --git a/tests/lean/run/isabelle.lean b/tests/lean/run/isabelle.lean
index 57f10a99b1..7a6125d692 100644
--- a/tests/lean/run/isabelle.lean
+++ b/tests/lean/run/isabelle.lean
@@ -13,8 +13,8 @@ open lazy_list
 
 meta def of_tactic {α : Type u} (t : tactic α) : lazy_tactic α :=
 λ s, match t s with
-| tactic_result.success a new_s    := lazy_list.singleton (a, new_s)
-| tactic_result.exception f e s := lazy_list.nil
+| result.success a new_s    := lazy_list.singleton (a, new_s)
+| result.exception f e s := lazy_list.nil
 end
 
 meta instance {α : Type} : has_coe (tactic α) (lazy_tactic α) :=
@@ -54,7 +54,7 @@ meta def choose {α} (xs : list α) : lazy_tactic α :=
 meta def run {α} (t : lazy_tactic α) : tactic α :=
 λ s, match t s with
 | nil                := tactic.failed s
-| cons (a, new_s) ss := tactic_result.success a new_s
+| cons (a, new_s) ss := result.success a new_s
 end
 
 open tactic
diff --git a/tests/lean/run/my_tac_class.lean b/tests/lean/run/my_tac_class.lean
index 90b1206fe0..222bb1eacc 100644
--- a/tests/lean/run/my_tac_class.lean
+++ b/tests/lean/run/my_tac_class.lean
@@ -16,14 +16,14 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
 t >> return ()
 
 meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit :=
-λ v s, tactic_result.cases_on (@scope_trace _ line col (t v s))
-  (λ ⟨a, v⟩ new_s, tactic_result.success ((), v) new_s)
+λ 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 >> tactic.silent_fail) new_s
-    | none := tactic.silent_fail new_s
+          (tactic.report_error line col msg >> interaction_monad.silent_fail) new_s
+    | none := interaction_monad.silent_fail new_s
     end)
 
 meta def execute (tac : mytac unit) : tactic unit :=
diff --git a/tests/lean/run/quote_bas.lean b/tests/lean/run/quote_bas.lean
index 5411a09843..7ec2db38cc 100644
--- a/tests/lean/run/quote_bas.lean
+++ b/tests/lean/run/quote_bas.lean
@@ -1,5 +1,7 @@
 universes u v w
 
+namespace quote_bas
+
 inductive Expr (V : Type u)
 | One {}            : Expr
 | Var (v : V)       : Expr
@@ -75,3 +77,5 @@ instance quote_mul {V : Type u} (v : Env V) n {V' : Type v} (v' : Env V') m {V''
                    Quote v (n * m) (merge v' v'') :=
 { quote      := Mult (map_var sum_assoc (map_var inl (quote n))) (map_var sum_assoc (quote m)),
   eval_quote := by simp }
+
+end quote_bas
diff --git a/tests/lean/tactic_state_pp.lean b/tests/lean/tactic_state_pp.lean
index 8bc0f0b051..f2ee7bbd6f 100644
--- a/tests/lean/tactic_state_pp.lean
+++ b/tests/lean/tactic_state_pp.lean
@@ -16,8 +16,8 @@ do t     ← target,
 
 meta def pp_state (s : tactic_state) : format :=
 match pp_state_core s with
-| tactic_result.success r _     := r
-| tactic_result.exception _ _ _ := "failed to pretty print"
+| result.success r _     := r
+| result.exception _ _ _ := "failed to pretty print"
 end
 
 meta instance i2 : has_to_format tactic_state :=