max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/lean/parser/reader): use different monad stacks for different parts of the reader

Browse source
This commit is contained in:
Sebastian Ullrich 2018-08-29 15:12:27 -07:00
parent 3bdc0db397
commit 2528aee72b
8 changed files with 175 additions and 154 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

123
library/init/lean/parser/reader/basic.lean
View file

@ -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

68
library/init/lean/parser/reader/module.lean
View file

@ -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

22
library/init/lean/parser/reader/term.lean
View file

@ -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
]

55
library/init/lean/parser/reader/token.lean
View file

@ -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

35
src/frontends/lean/elaborator.cpp
View file

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

4
src/frontends/lean/elaborator.h
View file

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

7
tests/lean/reader1.lean
View file

@ -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,

15
tests/lean/reader1.lean.expected.out
View file

@ -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