From 2528aee72b518542d59ca044ead0a9158a36901c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 29 Aug 2018 15:12:27 -0700
Subject: [PATCH] refactor(library/init/lean/parser/reader): use different
 monad stacks for different parts of the reader

---
 library/init/lean/parser/reader/basic.lean  | 123 +++++++++++---------
 library/init/lean/parser/reader/module.lean |  68 ++++++-----
 library/init/lean/parser/reader/term.lean   |  22 ++--
 library/init/lean/parser/reader/token.lean  |  55 ++++-----
 src/frontends/lean/elaborator.cpp           |  35 +++---
 src/frontends/lean/elaborator.h             |   4 +-
 tests/lean/reader1.lean                     |   7 +-
 tests/lean/reader1.lean.expected.out        |  15 ---
 8 files changed, 175 insertions(+), 154 deletions(-)

diff --git a/library/init/lean/parser/reader/basic.lean b/library/init/lean/parser/reader/basic.lean
index c83b3cbc9b..505d51f1f5 100644
--- a/library/init/lean/parser/reader/basic.lean
+++ b/library/init/lean/parser/reader/basic.lean
@@ -19,20 +19,20 @@ namespace rec_t
 variables {m : Type → Type} {r α : Type} [monad m]
 local attribute [reducible] rec_t
 
-/-- Continue at the recursion point stored at `with_recurse`. -/
+/-- Continue at the recursion point stored at `run`. -/
 def recurse : rec_t r m r :=
 do x ← read,
    monad_lift x
 
 variables (base : m r) (rec : rec_t r m r)
-private def with_recurse_aux : nat → m r
+private def run_aux : nat → m r
 | 0     := base
-| (n+1) := rec.run (with_recurse_aux n)
+| (n+1) := rec.run (run_aux n)
 
 /-- Execute `rec`, re-executing it whenever `recurse` is called.
     After `max_rec` recursion steps, `base` is executed instead. -/
-def with_recurse (max_rec := 1000) : rec_t r m r :=
-⟨λ _, rec.run (with_recurse_aux base rec max_rec)⟩
+protected def run (max_rec := 1000) : m r :=
+rec.run (run_aux base rec max_rec)
 
 -- not clear how to auto-derive these given the additional constraints
 instance : monad (rec_t r m) := infer_instance
@@ -43,6 +43,16 @@ instance (μ) [alternative m] [lean.parser.monad_parsec μ m] : lean.parser.mona
 infer_instance
 end rec_t
 
+class monad_rec (r : out_param Type) (m : Type → Type) :=
+(recurse {} : m r)
+export monad_rec (recurse)
+
+instance monad_rec.base (r m) [monad m] : monad_rec r (rec_t r m) :=
+{ recurse := rec_t.recurse }
+
+instance monad_rec.trans (r m m') [has_monad_lift m m'] [monad_rec r m] [monad m] : monad_rec r m' :=
+{ recurse := monad_lift (recurse : m r) }
+
 namespace lean
 -- TODO: enhance massively
 abbreviation message := string
@@ -70,75 +80,76 @@ structure reader_state :=
 
 structure reader_config := mk
 
-section
-set_option class.instance_max_depth 37
 @[irreducible, derive monad alternative monad_reader monad_state monad_parsec monad_except]
-def read_m := rec_t syntax $ reader_t reader_config $ state_t reader_state $ parsec syntax
-end
+def read_t (m : Type → Type) [monad m] := reader_t reader_config $ state_t reader_state $ parsec_t syntax m
+abbreviation basic_read_m := read_t id
+abbreviation basic_reader := basic_read_m syntax
 
-abbreviation reader := read_m syntax
+ -- an arbitrary `reader` type; readers are usually some monad stack based on `basic_read_m` returning `syntax`
+variable {ρ : Type}
 
-class reader.has_tokens {ρ : Type} (r : ρ) := mk {} ::
+class reader.has_tokens (r : ρ) := mk {} ::
 (tokens : list token_config)
 
 open reader.has_tokens (tokens)
 
-instance list.nil.tokens (ρ) : reader.has_tokens ([] : list ρ) :=
+instance list.nil.tokens : reader.has_tokens ([] : list ρ) :=
 ⟨[]⟩
-instance list.cons.tokens (ρ) (r : ρ) (rs : list ρ) [reader.has_tokens r] [reader.has_tokens rs] :
+instance list.cons.tokens (r : ρ) (rs : list ρ) [reader.has_tokens r] [reader.has_tokens rs] :
   reader.has_tokens (r::rs) :=
 ⟨tokens r ++ tokens rs⟩
 
-class reader.has_view (r : reader) (α : out_param Type) :=
+class reader.has_view (r : ρ) (α : out_param Type) :=
 (view : syntax → option α)
 (review : α → syntax)
 
-instance reader.has_view.default (r : reader) : inhabited (reader.has_view r syntax) :=
+instance reader.has_view.default (r : ρ) : inhabited (reader.has_view r syntax) :=
 ⟨{ view := some, review := id }⟩
 
 class syntax_node_kind.has_view (k : syntax_node_kind) (α : out_param Type) :=
 (view : syntax → option α)
 (review : α → syntax)
 
-namespace read_m
-local attribute [reducible] read_m
-protected def run (cfg : reader_config) (st : reader_state) (s : string) (r : read_m syntax) :
-  syntax × list message :=
-match (((r.run (monad_parsec.error "no recursive parser at top level")).run cfg).run st).parse_with_eoi s with
-| except.ok (a, st) := (a, st.errors.reverse)
-| except.error msg  := (msg.custom, [to_string msg])
-
-def log_error (e : message) : read_m unit :=
-modify (λ st, {st with errors := to_string e :: st.errors})
-end read_m
+section
+local attribute [reducible] read_t
+protected def reader.run {m : Type → Type} [monad m] (cfg : reader_config) (st : reader_state) (s : string) (r : read_t m syntax) :
+  m (syntax × list message) :=
+do r ← ((r.run cfg).run st).parse_with_eoi s,
+   pure $ match r with
+   | except.ok (a, st) := (a, st.errors.reverse)
+   | except.error msg  := (msg.custom, [to_string msg])
+end
 
 namespace reader
 open monad_parsec
 open reader.has_view
-variable {α : Type}
+variables {α : Type} {m : Type → Type}
+local notation `reader` := m syntax
+
+def log_error [monad_state reader_state m] (e : message) : m unit :=
+modify (λ st, {st with errors := to_string e :: st.errors})
 
 def eoi : syntax_node_kind := ⟨`lean.parser.reader.eoi⟩
 
-protected def parse (cfg : reader_config) (s : string) (r : reader) [reader.has_tokens r] :
+protected def parse (cfg : reader_config) (s : string) (r : basic_reader) [reader.has_tokens r] :
   syntax × list message :=
 -- the only hardcoded tokens, because they are never directly mentioned by a `reader`
 let builtin_tokens : list token_config := [⟨"/-", none⟩, ⟨"--", none⟩] in
-do {
+reader.run cfg ⟨tokens r ++ builtin_tokens, [], s.mk_iterator⟩ s $ do
   stx ← catch r $ λ (msg : parsec.message _), do {
     modify $ λ st, {st with token_start := msg.it},
-    read_m.log_error (to_string msg),
+    reader.log_error (to_string msg),
     pure msg.custom
   },
   whitespace,
   -- add `eoi` node and store any residual input in its prefix
-  catch monad_parsec.eoi $ λ msg, read_m.log_error (to_string msg),
+  catch monad_parsec.eoi $ λ msg, reader.log_error (to_string msg),
   tk_start ← reader_state.token_start <$> get,
   let stop := tk_start.to_end in
   pure $ syntax.node ⟨none, [
     stx,
     syntax.node ⟨eoi, [syntax.atom ⟨some ⟨⟨tk_start, stop⟩, stop.offset, ⟨stop, stop⟩⟩, atomic_val.string ""⟩]⟩
   ]⟩
-}.run cfg ⟨tokens r ++ builtin_tokens, [], s.mk_iterator⟩ s
 
 structure parse.view_ty :=
 (root : syntax)
@@ -149,6 +160,8 @@ def parse.view : syntax → option parse.view_ty
 | _ := none
 
 namespace combinators
+variables [monad m] [monad_except (parsec.message syntax) m] [monad_parsec syntax m] [alternative m]
+
 def node' (k : option syntax_node_kind) (rs : list reader) : reader :=
 do (args, _) ← rs.mfoldl (λ (p : list syntax × nat) r, do
      (args, remaining) ← pure p,
@@ -160,13 +173,13 @@ do (args, _) ← rs.mfoldl (λ (p : list syntax × nat) r, do
    ) ([], rs.length),
    pure $ syntax.node ⟨k, args.reverse⟩
 
-@[reducible] def seq := node' none
-@[reducible] def node (k : syntax_node_kind) := node' k
+@[reducible] def seq : list reader → reader := node' none
+@[reducible] def node (k : syntax_node_kind) : list reader → reader := node' k
 
-instance node'.tokens (m rs) [reader.has_tokens rs] : reader.has_tokens (node' m rs) :=
+instance node'.tokens (k) (rs : list reader) [reader.has_tokens rs] : reader.has_tokens (node' k rs) :=
 ⟨tokens rs⟩
 
-instance node.view (k rs) [i : syntax_node_kind.has_view k α] : reader.has_view (node k rs) α :=
+instance node.view (k) (rs : list reader) [i : syntax_node_kind.has_view k α] : reader.has_view (node k rs) α :=
 { view := i.view, review := i.review }
 
 private def many1_aux (p : reader) : list syntax → nat → reader
@@ -179,10 +192,10 @@ private def many1_aux (p : reader) : list syntax → nat → reader
 def many1 (r : reader) : reader :=
 do rem ← remaining, many1_aux r [] (rem+1)
 
-instance many1.tokens (r) [reader.has_tokens r] : reader.has_tokens (many1 r) :=
+instance many1.tokens (r : reader) [reader.has_tokens r] : reader.has_tokens (many1 r) :=
 ⟨tokens r⟩
 
-instance many1.view (r) [reader.has_view r α] : reader.has_view (many1 r) (list α) :=
+instance many1.view (r : reader) [reader.has_view r α] : reader.has_view (many1 r) (list α) :=
 { view := λ stx, match stx with
     | syntax.missing := list.ret <$> view r syntax.missing
     | syntax.node ⟨none, stxs⟩ := stxs.mmap (view r)
@@ -192,10 +205,10 @@ instance many1.view (r) [reader.has_view r α] : reader.has_view (many1 r) (list
 def many (r : reader) : reader :=
 many1 r <|> pure (syntax.node ⟨none, []⟩)
 
-instance many.tokens (r) [reader.has_tokens r] : reader.has_tokens (many r) :=
+instance many.tokens (r : reader) [reader.has_tokens r] : reader.has_tokens (many r) :=
 ⟨tokens r⟩
 
-instance many.view (r) [has_view r α] : reader.has_view (many r) (list α) :=
+instance many.view (r : reader) [has_view r α] : reader.has_view (many r) (list α) :=
 {..many1.view r}
 
 def optional (r : reader) : reader :=
@@ -206,7 +219,7 @@ do r ← optional $
    | some r := syntax.node ⟨none, [r]⟩
    | none   := syntax.node ⟨none, []⟩
 
-instance optional.tokens (r) [reader.has_tokens r] : reader.has_tokens (optional r) :=
+instance optional.tokens (r : reader) [reader.has_tokens r] : reader.has_tokens (optional r) :=
 ⟨tokens r⟩
 
 inductive optional_view (α : Type)
@@ -222,7 +235,7 @@ instance : functor optional_view :=
   | missing := missing }
 end optional_view
 
-instance optional.view (r) [reader.has_view r α] : reader.has_view (optional r) (optional_view α) :=
+instance optional.view (r : reader) [reader.has_view r α] : reader.has_view (optional r) (optional_view α) :=
 { view := λ stx, match stx with
     | syntax.missing := pure optional_view.missing
     | syntax.node ⟨none, []⟩ := pure optional_view.none
@@ -241,10 +254,10 @@ match rs with
 | [] := error "any_of"
 | (r::rs) := rs.foldl (<|>) r
 
-instance any_of.tokens (rs) [reader.has_tokens rs] : reader.has_tokens (any_of rs) :=
+instance any_of.tokens (rs : list reader) [reader.has_tokens rs] : reader.has_tokens (any_of rs) :=
 ⟨tokens rs⟩
 
-instance any_of.view (rs) : reader.has_view (any_of rs) syntax := default _
+instance any_of.view (rs : list reader) : reader.has_view (any_of rs) syntax := default _
 
 /-- Parse a list `[p1, ..., pn]` of readers as `p1 <|> ... <|> pn`.
     The result will be wrapped in a node with the the index of the successful
@@ -255,7 +268,7 @@ rs.enum.foldr
   -- use `foldr` so that any other error is preferred over this one
   (error "choice: empty list")
 
-instance choice.tokens (rs) [reader.has_tokens rs] : reader.has_tokens (choice rs) :=
+instance choice.tokens (rs : list reader) [reader.has_tokens rs] : reader.has_tokens (choice rs) :=
 ⟨tokens rs⟩
 
 instance try.tokens (r : reader) [reader.has_tokens r] : reader.has_tokens (try r) :=
@@ -270,25 +283,21 @@ instance label.view (r : reader) (l) [i : reader.has_view r α] : reader.has_vie
 
 instance dbg.tokens (r : reader) (l) [reader.has_tokens r] : reader.has_tokens (dbg l r) :=
 ⟨tokens r⟩
-instance dbg.view (r l) [i : reader.has_view r α] : reader.has_view (dbg l r) α :=
+instance dbg.view (r  : reader) (l) [i : reader.has_view r α] : reader.has_view (dbg l r) α :=
 {..i}
 
-local attribute [reducible] read_m
-def recurse : reader :=
-rec_t.recurse
-
-instance recurse.tokens : reader.has_tokens recurse :=
+instance recurse.tokens (r m) [monad_rec r m] : reader.has_tokens (recurse : m r) :=
 ⟨[]⟩ -- recursive use should not contribute any new tokens
-instance recurse.view : reader.has_view recurse syntax := default _
+instance recurse.view (r m) [monad_rec r m] : reader.has_view (recurse : m r) syntax := default _
 
-def with_recurse (r : reader) : reader :=
-rec_t.with_recurse (error "recursion limit") r
+def with_recurse (r : rec_t syntax m syntax) : reader :=
+rec_t.run (error "recursion limit") r
 
-instance with_recurse.tokens (r : reader) [reader.has_tokens r] : reader.has_tokens (with_recurse r) :=
+instance with_recurse.tokens (r : rec_t syntax m syntax) [reader.has_tokens r] : reader.has_tokens (with_recurse r) :=
 ⟨tokens r⟩
-instance with_recurse.view (r) : reader.has_view (with_recurse r) syntax := default _
+instance with_recurse.view (r : rec_t syntax m syntax) : reader.has_view (with_recurse r) syntax := default _
 
 end combinators
-end reader
+end «reader»
 end parser
 end lean
diff --git a/library/init/lean/parser/reader/module.lean b/library/init/lean/parser/reader/module.lean
index 41674d3c2b..d140dc9e5d 100644
--- a/library/init/lean/parser/reader/module.lean
+++ b/library/init/lean/parser/reader/module.lean
@@ -14,27 +14,36 @@ open combinators monad_parsec
 open reader.has_tokens reader.has_view
 
 local postfix `?`:10000 := optional
-local postfix *:10000 := many
+local postfix *:10000 := combinators.many
 local postfix +:10000 := combinators.many1
 
+--TODO(Sebastian): add `coroutine`
+--@[irreducible, derive monad alternative monad_reader monad_state monad_parsec monad_except]
+abbreviation module_read_m := basic_read_m --rec_t syntax $ reader_t reader_config $ state_t reader_state $ parsec syntax
+abbreviation module_reader := module_read_m syntax
+
+instance module_read_m.lift_basic_read_m : has_monad_lift_t basic_read_m module_read_m :=
+--TODO(Sebastian): lift into coroutine
+{ monad_lift := λ α, id }
+
 @[derive reader.has_view reader.has_tokens]
-def prelude.reader :=
+def prelude.reader : module_reader :=
 node! «prelude» ["prelude"]
 
 @[derive reader.has_view reader.has_tokens]
-def import_path.reader :=
+def import_path.reader : module_reader :=
 -- use `raw_symbol` to ignore registered tokens like ".."
 node! import_path [
   dirups: (raw_symbol ".")*,
   module: ident]
 
 @[derive reader.has_view reader.has_tokens]
-def import.reader :=
+def import.reader : module_reader :=
 node! «import» ["import", imports: import_path.reader+]
 
-set_option class.instance_max_depth 66
+set_option class.instance_max_depth 300
 @[derive reader.has_view reader.has_tokens]
-def open_spec.reader : reader :=
+def open_spec.reader : command_reader :=
 node! open_spec [
  id: ident,
  as: node! open_spec.as ["as", id: ident]?,
@@ -44,15 +53,15 @@ node! open_spec [
 ]+
 
 @[derive reader.has_tokens]
-def open.reader :=
+def open.reader : command_reader :=
 node! «open» ["open", spec: open_spec.reader]
 
 @[derive reader.has_tokens]
-def section.reader :=
+def section.reader : command_reader :=
 node! «section» ["section", name: ident?, commands: recurse*, "end", end_name: ident?]
 
 @[derive reader.has_tokens]
-def universe.reader :=
+def universe.reader : command_reader :=
 any_of [
   -- local
   node! universe_variables [try ["universe", "variables"], ids: ident+],
@@ -63,9 +72,10 @@ any_of [
 
 namespace notation_spec
 @[derive reader.has_tokens reader.has_view]
-def precedence.reader := node! «precedence» [":", prec: number]/-TODO <|> expr-/
+def precedence.reader : command_reader :=
+node! «precedence» [":", prec: number]/-TODO <|> expr-/
 
-def quoted_symbol.reader : reader :=
+def quoted_symbol.reader : command_reader :=
 do (s, info) ← with_source_info $ take_until (= '`'),
    pure $ syntax.atom ⟨info, atomic_val.string s⟩
 
@@ -73,7 +83,7 @@ instance quoted_symbol.tokens : reader.has_tokens quoted_symbol.reader := ⟨[]
 instance quoted_symbol.view : reader.has_view quoted_symbol.reader syntax := default _
 
 @[derive reader.has_tokens reader.has_view]
-def symbol_quote.reader :=
+def symbol_quote.reader : command_reader :=
 node! notation_quoted_symbol [
   left_quote: raw_symbol "`",
   symbol: quoted_symbol.reader,
@@ -82,14 +92,14 @@ node! notation_quoted_symbol [
 
 --TODO(Sebastian): cannot be called `symbol` because of hygiene problems
 @[derive reader.has_tokens reader.has_view]
-def notation_symbol.reader :=
+def notation_symbol.reader : command_reader :=
 node_choice! notation_symbol {
   quoted: symbol_quote.reader
   --TODO, {read := do tk ← token, /- check if reserved token-/}
 }
 
 @[derive reader.has_tokens reader.has_view]
-def action.reader :=
+def action.reader : command_reader :=
 node! action [":", action: node_choice! action_kind {
   prec: number,
   "max",
@@ -102,7 +112,7 @@ node! action [":", action: node_choice! action_kind {
     notation_tk,-/}]
 
 @[derive reader.has_tokens reader.has_view]
-def transition.reader :=
+def transition.reader : command_reader :=
 node_choice! transition {
   binder: node! binder ["binder", prec: precedence.reader?],
   binders: node! binders ["binders", prec: precedence.reader?],
@@ -110,50 +120,50 @@ node_choice! transition {
 }
 
 @[derive reader.has_tokens reader.has_view]
-def rule.reader :=
+def rule.reader : command_reader :=
 node! rule [symbol: notation_symbol.reader, transition: transition.reader?]
 
 end notation_spec
 
 @[derive reader.has_tokens reader.has_view]
-def notation_spec.reader :=
+def notation_spec.reader : command_reader :=
 node_choice! notation_spec {
   number_literal: number,
   rules: node! notation_spec.rules [id: ident?, rules: notation_spec.rule.reader*]
 }
 
 @[derive reader.has_tokens reader.has_view]
-def notation.reader :=
+def notation.reader : command_reader :=
 node! «notation» ["notation", spec: notation_spec.reader, ":=", term: term.reader]
 
 @[derive reader.has_tokens reader.has_view]
-def reserve_notation.reader :=
+def reserve_notation.reader : command_reader :=
 node! «reserve_notation» [try ["reserve", "notation"], spec: notation_spec.reader]
 
 @[derive reader.has_tokens reader.has_view]
-def mixfix.kind.reader :=
+def mixfix.kind.reader : command_reader :=
 node_choice! mixfix.kind {"prefix", "infix", "infixl", "infixr", "postfix"}
 
 @[derive reader.has_tokens reader.has_view]
-def mixfix.reader :=
+def mixfix.reader : command_reader :=
 node! «mixfix» [
   kind: mixfix.kind.reader,
   symbol: notation_spec.notation_symbol.reader, ":=", term: term.reader]
 
 @[derive reader.has_tokens reader.has_view]
-def reserve_mixfix.reader :=
+def reserve_mixfix.reader : command_reader :=
 node! «reserve_mixfix» [
   try ["reserve", kind: mixfix.kind.reader],
   symbol: notation_spec.notation_symbol.reader]
 
 @[derive reader.has_tokens reader.has_view]
-def command.reader :=
+def command.reader : module_reader :=
 with_recurse $ any_of [open.reader, section.reader, universe.reader, notation.reader, reserve_notation.reader,
   mixfix.reader, reserve_mixfix.reader] <?> "command"
 
 /-- Read commands, recovering from errors inside commands (attach partial syntax tree)
     as well as unknown commands (skip input). -/
-private def commands_aux : bool → list syntax → nat → reader
+private def commands_aux : bool → list syntax → nat → module_reader
 | recovering cs 0            := error "unreachable"
 -- on end of input, return list of parsed commands
 | recovering cs (nat.succ n) := (monad_parsec.eoi *> pure (syntax.node ⟨none, cs.reverse⟩)) <|> do
@@ -164,7 +174,7 @@ private def commands_aux : bool → list syntax → nat → reader
       -- unknown command: try to skip token, or else single character
       when (¬ recovering) $ do {
         it ← left_over,
-        read_m.log_error $ to_string { parsec.message . expected := dlist.singleton "command", it := it, custom := () }
+        log_error $ to_string { parsec.message . expected := dlist.singleton "command", it := it, custom := () }
       },
       tk_start ← reader_state.token_start <$> get,
       -- since the output of the following parser is never captured in a syntax tree...
@@ -175,23 +185,23 @@ private def commands_aux : bool → list syntax → nat → reader
     }) $ λ msg, do {
       -- error inside command: log error, return partial syntax tree
       modify $ λ st, {st with token_start := msg.it},
-      read_m.log_error (to_string msg),
+      log_error (to_string msg),
       pure (tt, some msg.custom)
     },
   commands_aux recovering (c.to_monad++cs) n
 
-def commands.reader : reader :=
+def commands.reader : module_reader :=
 do { rem ← remaining, commands_aux ff [] rem.succ }
 
 instance commands.tokens : reader.has_tokens commands.reader :=
 ⟨tokens command.reader⟩
 
 -- custom reader requires custom instance
-instance commands.reader.has_view : commands.reader.has_view (list syntax) :=
+instance commands.reader.has_view : has_view commands.reader (list syntax) :=
 {..many.view command.reader}
 
 @[derive reader.has_tokens reader.has_view]
-def module.reader :=
+def module.reader : module_reader :=
 node! module [«prelude»: prelude.reader?, imports: import.reader*, commands: commands.reader]
 end reader
 
diff --git a/library/init/lean/parser/reader/term.lean b/library/init/lean/parser/reader/term.lean
index 68a3bb99d7..7bb8073ffa 100644
--- a/library/init/lean/parser/reader/term.lean
+++ b/library/init/lean/parser/reader/term.lean
@@ -10,17 +10,25 @@ import init.lean.parser.reader.token
 
 namespace lean.parser
 namespace reader
-open combinators
+open combinators reader.has_view
 
-@[pattern] def hole := {syntax_node_kind . name := `lean.parser.reader.hole}
+@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec]
+abbreviation command_read_m := rec_t syntax basic_read_m
+abbreviation command_reader := command_read_m syntax
 
-@[derive reader.has_tokens]
-def hole.reader : reader :=
-node hole [symbol "_"]
+@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec]
+abbreviation term_read_m := rec_t syntax command_read_m
+abbreviation term_reader := term_read_m syntax
 
 @[derive reader.has_tokens reader.has_view]
-def term.reader :=
-any_of [
+def hole.reader : term_reader :=
+node! hole [hole: symbol "_"]
+
+@[derive reader.has_tokens reader.has_view]
+-- While term.reader does not actually read a command, it does share the same effect set
+-- with command readers, introducing the term-level recursion effect only for nested readers
+def term.reader : command_reader :=
+with_recurse $ any_of [
   hole.reader
 ]
 
diff --git a/library/init/lean/parser/reader/token.lean b/library/init/lean/parser/reader/token.lean
index 603200f955..9608525bc6 100644
--- a/library/init/lean/parser/reader/token.lean
+++ b/library/init/lean/parser/reader/token.lean
@@ -20,7 +20,7 @@ namespace reader
 open lean.parser.monad_parsec
 open string
 
-def match_token : read_m (option token_config) :=
+def match_token : basic_read_m (option token_config) :=
 do st ← get,
    it ← left_over,
    -- the slowest longest prefix matcher on Earth
@@ -31,7 +31,7 @@ do st ← get,
        | none     := tk
      else acc) none
 
-private def finish_comment_block_aux : nat → nat → read_m unit
+private def finish_comment_block_aux : nat → nat → basic_read_m unit
 | nesting (n+1) :=
   str "/-" *> finish_comment_block_aux (nesting + 1) n <|>
   str "-/" *>
@@ -40,11 +40,11 @@ private def finish_comment_block_aux : nat → nat → read_m unit
   any *> finish_comment_block_aux nesting n
 | _ _ := error "unreachable"
 
-def finish_comment_block (nesting := 1) : read_m unit :=
+def finish_comment_block (nesting := 1) : basic_read_m unit :=
 do r ← remaining,
    finish_comment_block_aux nesting (r+1) <?> "end of comment block"
 
-private def whitespace_aux : nat → read_m unit
+private def whitespace_aux : nat → basic_read_m unit
 | (n+1) :=
 do tk ← whitespace *> match_token,
    (match tk with
@@ -53,47 +53,51 @@ do tk ← whitespace *> match_token,
     | _                 := pure ())
 | 0 := error "unreachable"
 
+variables {m : Type → Type} [has_monad_lift_t basic_read_m m]
+local notation `reader` := m syntax
+local notation `lift` := @monad_lift basic_read_m _ _ _
+
 /-- Skip whitespace and comments. -/
-def whitespace : read_m substring :=
+def whitespace : basic_read_m substring :=
 -- every `whitespace_aux` loop reads at least one char
 do start ← left_over,
    whitespace_aux (start.remaining+1),
    stop ← left_over,
    pure ⟨start, stop⟩
 
-def with_source_info {α : Type} (r : read_m α) : read_m (α × source_info) :=
+def with_source_info [monad m] [monad_state reader_state m] [monad_parsec syntax m] {α : Type} (r : m α) : m (α × source_info) :=
 do token_start ← reader_state.token_start <$> get,
-   whitespace,
+   lift whitespace,
    it ← left_over,
    a ← r,
    -- TODO(Sebastian): less greedy, more natural whitespace assignement
    -- E.g. only read up to the next line break
-   trailing ← whitespace,
+   trailing ← lift whitespace,
    it2 ← left_over,
    modify $ λ st, {st with token_start := it2},
    pure (a, ⟨⟨token_start, it⟩, it.offset, trailing⟩)
 
 /-- Match a string literally without consulting the token table. -/
 def raw_symbol (sym : string) : reader :=
-try $ do
+lift $ try $ do
   (_, info) ← with_source_info $ str sym,
   pure $ syntax.atom ⟨info, atomic_val.string sym⟩
 
-instance raw_symbol.tokens (s) : reader.has_tokens (raw_symbol s) := ⟨[]⟩
-instance raw_symbol.view (s) : reader.has_view (raw_symbol s) syntax := default _
+instance raw_symbol.tokens (s) : reader.has_tokens (raw_symbol s : reader) := ⟨[]⟩
+instance raw_symbol.view (s) : reader.has_view (raw_symbol s : reader) syntax := default _
 
 @[pattern] def base10_lit : syntax_node_kind := ⟨`lean.parser.reader.base10_lit⟩
 
 --TODO(Sebastian): other bases
-private def number' : read_m (source_info → syntax) :=
+private def number' : basic_read_m (source_info → syntax) :=
 do num ← take_while1 char.is_digit,
    pure $ λ i, syntax.node ⟨base10_lit, [syntax.atom ⟨i, atomic_val.string num⟩]⟩
 
-private def ident' : read_m (source_info → syntax) :=
+private def ident' : basic_read_m (source_info → syntax) :=
 do n ← identifier,
    pure $ λ i, syntax.ident ⟨i, n, none, none⟩
 
-private def symbol' : read_m (source_info → syntax) :=
+private def symbol' : basic_read_m (source_info → syntax) :=
 do tk ← match_token,
    match tk with
    -- constant-length token
@@ -104,7 +108,7 @@ do tk ← match_token,
    | some ⟨tk, some r⟩ := error "not implemented" --str tk *> monad_parsec.lift r
    | none              := error
 
-def token : read_m syntax :=
+def token : basic_read_m syntax :=
 do (r, i) ← with_source_info $ do {
      -- NOTE the order: if a token is both a symbol and a valid identifier (i.e. a keyword),
      -- we want it to be recognized as a symbol
@@ -115,35 +119,34 @@ do (r, i) ← with_source_info $ do {
 
 --TODO(Sebastian): error messages
 def symbol (sym : string) : reader :=
-try $ do
+lift $ try $ do
   it ← left_over,
   stx@(syntax.atom ⟨_, atomic_val.string sym'⟩) ← token | error "" (dlist.singleton (repr sym)) it,
   when (sym ≠ sym') $
     error "" (dlist.singleton (repr sym)) it,
   pure stx
 
-instance symbol.tokens (sym : string) : reader.has_tokens (symbol sym) :=
+instance symbol.tokens (sym : string) : reader.has_tokens (symbol sym : reader) :=
 ⟨[⟨sym, none⟩]⟩
-instance symbol.view (s) : reader.has_view (symbol s) syntax := default _
-instance symbol_coe : has_coe string reader := ⟨symbol⟩
+instance symbol.view (s) : reader.has_view (symbol s : reader) syntax := default _
 
 def number : reader :=
-try $ do
+lift $ try $ do
   it ← left_over,
   stx@(syntax.node ⟨base10_lit, _⟩) ← token | error "" (dlist.singleton "number") it,
   pure stx
 
-instance number.tokens : reader.has_tokens number := ⟨[]⟩
-instance number.view : reader.has_view number syntax := default _
+instance number.tokens : reader.has_tokens (number : reader) := ⟨[]⟩
+instance number.view : reader.has_view (number : reader) syntax := default _
 
 def ident : reader :=
-try $ do
+lift $ try $ do
   it ← left_over,
   stx@(syntax.ident _) ← token | error "" (dlist.singleton "identifier") it,
   pure stx
 
-instance ident.tokens : reader.has_tokens ident := ⟨[]⟩
-instance ident.view : reader.has_view ident syntax := default _
+instance ident.tokens : reader.has_tokens (ident : reader) := ⟨[]⟩
+instance ident.view : reader.has_view (ident : reader) syntax := default _
 
-end reader
+end «reader»
 end lean.parser
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 1a4d4d3222..3a8a941c56 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3259,12 +3259,15 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
     return visit(q, expected_type);
 }
 
-expr elaborator::visit_node_macro(expr const & e) {
+expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expected_type) {
     name macro = *get_name(mdata_data(e), "node!");
     name esc_macro = macro.is_atomic() ? "«" + macro.to_string() + "»" : macro;
     expr e2 = mdata_expr(e);
     expr macro_e = app_arg(app_fn(e2));
     name full_macro = const_name(macro_e);
+    if (!expected_type)
+        throw elaborator_exception(e, "node!: expected type must be known");
+    expr exp = expected_type.value();
     sstream struc, stx_pat, binds, mk_args, view_pat, reviews;
     unsigned i = 0;
     struc << "@[pattern] def " << esc_macro.to_string();
@@ -3277,9 +3280,9 @@ expr elaborator::visit_node_macro(expr const & e) {
         add_field = [&](expr r) {
             name fname = *get_name(mdata_data(r), "fname");
             r = mdata_expr(r);
+            r = visit(r, expected_type);
             auto m = mk_metavar(mk_Type(), r);
-            r = visit(r, some(mk_const({"lean", "parser", "reader"})));
-            auto inst = m_ctx.mk_class_instance(mk_app(mk_const(name{"lean", "parser", "reader", "has_view"}), r, m));
+            auto inst = m_ctx.mk_class_instance(mk_app(mk_const(name{"lean", "parser", "reader", "has_view"}), exp, r, m));
             if (!inst)
                 throw elaborator_exception(e, sstream() << "Could not infer instance of reader.has_view for '" << r
                                                         << "'");
@@ -3288,14 +3291,14 @@ expr elaborator::visit_node_macro(expr const & e) {
             if (i != 0)
                 stx_pat << ", ";
             stx_pat << "stx" << i;
-            binds << "a" << i << " <- view (" << pp(r) << ") stx" << i << ",\n";
+            binds << "a" << i << " <- view (" << pp(r) << " : " << pp(exp) << ") stx" << i << ",\n";
             mk_args << "a" << i << " ";
             if (i != 0)
                 view_pat << ", ";
             view_pat << "a" << i;
             if (i != 0)
                 reviews << ", ";
-            reviews << "review (" << pp(r) << ") a" << i;
+            reviews << "review (" << pp(r) << " : " << pp(exp) << ") a" << i;
             i++;
             return mk_as_is(r);
         };
@@ -3332,14 +3335,17 @@ expr elaborator::visit_node_macro(expr const & e) {
     m_env = p.env();
     m_ctx.set_env(m_env);
     return visit(mk_app(mk_const({"lean", "parser", "reader", "combinators", "node"}), mk_const(get_namespace(p.env()) + macro), mk_lean_list(new_args)),
-                 none_expr());
+                 expected_type);
 }
 
-expr elaborator::visit_node_choice_macro(expr const & e) {
+expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const & expected_type) {
     name macro = *get_name(mdata_data(e), "node_choice!");
     name esc_macro = macro.is_atomic() ? "«" + macro.to_string() + "»" : macro;
     expr args = mdata_expr(e);
     name full_macro = get_namespace(m_env) + macro;
+    if (!expected_type)
+        throw elaborator_exception(e, "node_choice!: expected type must be known");
+    expr exp = expected_type.value();
     sstream struc, view_cases, review_cases;
     unsigned i = 0;
     struc << "@[pattern] def " << esc_macro.to_string();
@@ -3351,17 +3357,18 @@ expr elaborator::visit_node_choice_macro(expr const & e) {
         name fname = *get_name(mdata_data(r), "fname");
         r = mdata_expr(r);
         auto m = mk_metavar(mk_Type(), r);
-        r = visit(r, some(mk_const({"lean", "parser", "reader"})));
-        auto inst = m_ctx.mk_class_instance(mk_app(mk_const(name{"lean", "parser", "reader", "has_view"}), r, m));
+        r = visit(r, expected_type);
+        auto inst = m_ctx.mk_class_instance(mk_app(mk_const(name{"lean", "parser", "reader", "has_view"}), exp, r, m));
         if (!inst)
             throw elaborator_exception(e, sstream() << "Could not infer instance of reader.has_view for '" << r
                                                     << "'");
         struc << "| «" << fname << "» : " << instantiate_mvars(m) << " -> " << macro.to_string() << ".view\n";
 
         view_cases << "| " << i << " := " << macro.to_string() << ".view." << fname << " <$> view  (" << pp(r)
-                   << ") stx\n";
+                << " : " << pp(exp) << ") stx\n";
         review_cases << "| " << macro.to_string() << ".view." << fname << " a := "
-                << "syntax.node (syntax_node.mk (some (syntax_node_kind.mk (name.mk_numeral name.anonymous " << i << "))) [review (" << pp(r) << ") a])\n";
+                << "syntax.node (syntax_node.mk (some (syntax_node_kind.mk (name.mk_numeral name.anonymous " << i << "))) "
+                << "[review (" << pp(r) << " : " << pp(exp) << ") a])\n";
         i++;
         new_args.push_back(mk_as_is(r));
     }
@@ -3390,7 +3397,7 @@ expr elaborator::visit_node_choice_macro(expr const & e) {
                         mk_app(mk_const({"list", "cons"}),
                                mk_app(mk_const({"lean", "parser", "reader", "combinators", "choice"}),
                                       mk_lean_list(new_args)),
-                               mk_const({"list", "nil"}))), none_expr());
+                               mk_const({"list", "nil"}))), expected_type);
 }
 
 expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
@@ -3438,9 +3445,9 @@ expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_typ
         lean_assert(!is_app_fn); // visit_convoy is used in this case
         return visit_equations(e);
     } else if (get_name(mdata_data(e), "node!")) {
-        return visit_node_macro(e);
+        return visit_node_macro(e, expected_type);
     } else if (get_name(mdata_data(e), "node_choice!")) {
-        return visit_node_choice_macro(e);
+        return visit_node_choice_macro(e, expected_type);
     } else {
         expr new_e = visit(mdata_expr(e), expected_type);
         return update_mdata(e, new_e);
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index e5c5043670..4a205454fc 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -229,8 +229,8 @@ private:
     expr visit_constant(expr const & e, optional<expr> const & expected_type);
     expr visit_lambda(expr const & e, optional<expr> const & expected_type);
     expr visit_pi(expr const & e);
-    expr visit_node_macro(expr const & e);
-    expr visit_node_choice_macro(expr const & e);
+    expr visit_node_macro(expr const & e, optional<expr> const & expected_type);
+    expr visit_node_choice_macro(expr const & e, optional<expr> const & expected_type);
     expr visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
     expr visit_app(expr const & e, optional<expr> const & expected_type);
     expr visit_let(expr const & e, optional<expr> const & expected_type);
diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean
index d6af17b449..9d717f91ac 100644
--- a/tests/lean/reader1.lean
+++ b/tests/lean/reader1.lean
@@ -2,8 +2,8 @@ import init.lean.parser.reader.module init.io
 open lean.parser
 open lean.parser.reader
 
-def show_result (p : lean.parser.reader) [has_tokens p] (s : string) : eio unit :=
-let (stx, errors) := p.parse ⟨⟩ s in
+def show_result (p : module_reader) [has_tokens p] (s : string) : eio unit :=
+let (stx, errors) := reader.parse ⟨⟩ s p in
 when (stx.reprint ≠ s) (
   io.println "reprint fail:" *>
   io.println stx.reprint
@@ -45,9 +45,8 @@ end b"
 
 #eval show_result module.reader "notation `Prop` := _"
 
-#eval show_result mixfix.reader "prefix `+`:10 := _"
 #eval (do {
-  let (stx, _) := mixfix.reader.parse ⟨⟩ "prefix `+`:10 := _",
+  let (stx, _) := reader.parse ⟨⟩ "prefix `+`:10 := _" $ combinators.with_recurse mixfix.reader,
   some {root := stx, ..} ← pure $ reader.parse.view stx,
   some stx ← pure $ mixfix.expand stx | throw "expand fail",
   io.println stx,
diff --git a/tests/lean/reader1.lean.expected.out b/tests/lean/reader1.lean.expected.out
index bcb8081816..7d738d4847 100644
--- a/tests/lean/reader1.lean.expected.out
+++ b/tests/lean/reader1.lean.expected.out
@@ -135,21 +135,6 @@ result:
     ":="
     (lean.parser.reader.hole "_"))])
  (lean.parser.reader.eoi "")]
-result: 
-[(lean.parser.reader.mixfix
-  (lean.parser.reader.mixfix.kind (0 "prefix"))
-  (lean.parser.reader.notation_spec.notation_symbol
-   (0
-    (lean.parser.reader.notation_spec.notation_quoted_symbol
-     "`"
-     "+"
-     "`"
-     [(lean.parser.reader.notation_spec.precedence
-       ":"
-       (lean.parser.reader.base10_lit "10"))])))
-  ":="
-  (lean.parser.reader.hole "_"))
- (lean.parser.reader.eoi "")]
 (lean.parser.reader.notation
  "notation"
  (lean.parser.reader.notation_spec