feat(library/init/lean/parser/reader/basic): first has_view prototype, plus prefix ~> notation expansion based on it

library/init/lean/parser/reader/basic.lean

@@ -77,6 +77,18 @@ structure reader :=
 (read : read_m syntax)
 (tokens : list token_config := [])
 
+class reader.has_view (r : reader) (α : out_param Type) :=
+(view : syntax → option α)
+(review : α → syntax)
+
+@[priority 0] instance reader.has_view.default (r) : reader.has_view r syntax :=
+{ view := some,
+  review := id }
+
+class macro.has_view (m : macro) (α : 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) :
@@ -91,6 +103,8 @@ end read_m
 
 namespace reader
 open monad_parsec
+open reader.has_view
+variable {α : Type}
 
 protected def parse (cfg : reader_config) (s : string) (r : reader) :
   syntax × list message :=
@@ -113,6 +127,14 @@ do {
   ]⟩
 }.run cfg ⟨r.tokens ++ tokens, [], s.mk_iterator⟩ s
 
+structure parse.view_ty :=
+(root : syntax)
+(eoi  : syntax)
+
+def parse.view : syntax → option parse.view_ty
+| (syntax.node ⟨name.anonymous, [root, eoi]⟩) := some ⟨root, eoi⟩
+| _ := none
+
 namespace combinators
 def node' (m : name) (rs : list reader) : reader :=
 { read := do {
@@ -128,8 +150,30 @@ def node' (m : name) (rs : list reader) : reader :=
   },
   tokens := rs.bind reader.tokens }
 
-def seq := node' name.anonymous
-def node (m : macro) := node' m.name
+@[reducible] def seq := node' name.anonymous
+@[reducible] def node (m : macro) := node' m.name
+
+instance node'.view_cons (β m r rs) [reader.has_view r α] [reader.has_view (node' m rs) β] : reader.has_view (node' m (r::rs)) (α × β) :=
+{ view := λ stx, do {
+    syntax.node ⟨m', (stx::stxs)⟩ ← pure stx | failure,
+    guard (m' = m),
+    a ← view r stx,
+    b ← view (node' m rs) $ syntax.node ⟨m, stxs⟩,
+    pure (a, b)
+  },
+  review := λ ⟨a, b⟩, match review (node' m rs) b with
+    | syntax.node ⟨_, stxs⟩ := syntax.node ⟨m, review r a::stxs⟩
+    | _ := syntax.missing /- unreachable -/ }
+
+instance node'.view_nil (m r) [reader.has_view r α] : reader.has_view (node' m [r]) α :=
+{ view := λ stx, do {
+    syntax.node ⟨m', [stx]⟩ ← pure stx | failure,
+    guard (m' = m),
+    a ← view r stx,
+    pure a
+  },
+  review := λ a, syntax.node ⟨m, [review r a]⟩ }
+
 
 private def many1_aux (p : read_m syntax) : list syntax → nat → read_m syntax
 | as 0     := error "unreachable"
@@ -141,9 +185,27 @@ private def many1_aux (p : read_m syntax) : list syntax → nat → read_m synta
 def many1 (r : reader) : reader :=
 { r with read := do rem ← remaining, many1_aux r.read [] (rem+1) }
 
+/-
+instance many1.view (r) [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 ⟨name.anonymous, stxs⟩ := stxs.mmap (view r)
+    | _ := failure,
+  review := λ as, syntax.node ⟨name.anonymous, as.map (review r)⟩ }
+-/
+instance many1.view (r) : reader.has_view (many1 r) (list syntax) :=
+{ view := λ stx, match stx with
+    | syntax.missing := [syntax.missing]
+    | syntax.node ⟨name.anonymous, stxs⟩ := stxs
+    | _ := failure,
+  review := λ stxs, syntax.node ⟨name.anonymous, stxs⟩ }
+
 def many (r : reader) : reader :=
 { r with read := (many1 r).read <|> pure (syntax.node ⟨name.anonymous, []⟩) }
 
+instance many.view (r) : reader.has_view (many r) (list syntax) :=
+{..many1.view r}
+
 def optional (r : reader) : reader :=
 { r with read := do
     r ← optional $
@@ -153,6 +215,22 @@ def optional (r : reader) : reader :=
     | some r := syntax.node ⟨name.anonymous, [r]⟩
     | none   := syntax.node ⟨name.anonymous, []⟩ }
 
+inductive optional_view (α : Type)
+| some (a : α) : optional_view
+| none {} : optional_view
+| missing {} : optional_view
+
+instance optional.view (r) [reader.has_view r α] : reader.has_view (optional r) (optional_view α) :=
+{ view := λ stx, match stx with
+    | syntax.missing := pure optional_view.missing
+    | syntax.node ⟨name.anonymous, []⟩ := pure optional_view.none
+    | syntax.node ⟨name.anonymous, [stx]⟩ := optional_view.some <$> view r stx
+    | _ := failure,
+  review := λ a, match a with
+    | optional_view.some a  := syntax.node ⟨name.anonymous, [review r a]⟩
+    | optional_view.none    := syntax.node ⟨name.anonymous, []⟩
+    | optional_view.missing := syntax.missing }
+
 /-- Parse a list `[p1, ..., pn]` of readers as `p1 <|> ... <|> pn`.
     Note that there is NO explicit encoding of which reader was chosen;
     readers should instead produce distinct node names for disambiguation. -/
@@ -165,14 +243,23 @@ def any_of (rs : list reader) : reader :=
 def try (r : reader) : reader :=
 { r with read := try r.read }
 
+instance try.view (r) [i : reader.has_view r α] : reader.has_view (try r) α :=
+{..i}
+
 def label (r : reader) (l : string) : reader :=
 { r with read := label r.read l }
 
+instance label.view (r l) [i : reader.has_view r α] : reader.has_view (label r l) α :=
+{..i}
+
 infixr <?> := label
 
 def dbg (label : string) (r : reader) : reader :=
 { r with read := dbg label r.read }
 
+instance dbg.view (r l) [i : reader.has_view r α] : reader.has_view (dbg l r) α :=
+{..i}
+
 local attribute [reducible] read_m
 def recurse : reader :=
 { read   := rec_t.recurse,

library/init/lean/parser/reader/module.lean

@@ -11,6 +11,7 @@ import init.lean.parser.reader.token init.lean.parser.reader.term init.data.list
 namespace lean.parser
 namespace reader
 open combinators monad_parsec
+open reader.has_view
 
 def symbol_coe : has_coe string reader := ⟨symbol⟩
 def seq_coe : has_coe_t (list reader) reader := ⟨seq⟩
@@ -19,6 +20,8 @@ local attribute [instance] symbol_coe seq_coe
 -- coerce all list literals to `list reader`
 local notation `[` l:(foldr `, ` (h t, @list.cons reader h t) list.nil `]`) := l
 
+instance (r rs α) [i : reader.has_view (seq (r::rs)) α] : reader.has_view (r::rs : list reader) α := i
+
 local postfix `?`:10000 := optional
 local postfix *:10000 := many
 local postfix +:10000 := many1
@@ -30,15 +33,33 @@ node «prelude» ["prelude"]
 
 def import_path := {macro . name := `import_path}
 
+@[derive reader.has_view]
 def import_path.reader : reader :=
 -- use `raw_symbol` to ignore registered tokens like ".."
 node import_path [(raw_symbol ".")*, ident]
 
+structure import_path.view :=
+(dirups : list syntax)
+(ident  : syntax)
+
+instance import_path.has_view : import_path.has_view import_path.view :=
+{ view := λ stx, function.uncurry import_path.view.mk <$> view import_path.reader stx,
+  review := λ ⟨a, b⟩, review import_path.reader (a, b) }
+
 def «import» := {macro . name := `import}
 
+@[derive reader.has_view]
 def import.reader : reader :=
 node «import» ["import", import_path.reader+]
 
+structure import.view :=
+(«import» : syntax)
+(paths : list syntax)
+
+instance import.has_view : import.has_view import.view :=
+{ view := λ stx, function.uncurry import.view.mk <$> view import.reader stx,
+  review := λ ⟨a, b⟩, review import.reader (a, b) }
+
 section commands
 
 def «open» := {macro . name := `open}
@@ -71,18 +92,37 @@ node «universe» [any_of [
 
 def «notation» := {macro . name := `notation}
 
+@[derive reader.has_view]
 def prec : reader := [":", number]/-TODO <|> expr-/
 
 def quoted_symbol : read_m syntax :=
 do (s, info) ← with_source_info $ take_until (= '`'),
    pure $ syntax.atom ⟨info, atomic_val.string s⟩
 
-def notation_symbol :=
+def notation_quoted_symbol := {macro . name := `notation_symbol}
+
+@[derive reader.has_view]
+def notation_quoted_symbol.reader : reader :=
+[raw_symbol "`", {read := quoted_symbol}, raw_symbol "`", prec?]
+
+structure notation_quoted_symbol.view :=
+(left_quote : syntax)
+(symbol : syntax)
+(right_quote : syntax)
+(prec : optional_view (syntax × syntax))
+
+instance notation_quoted_symbol.has_view : notation_quoted_symbol.has_view notation_quoted_symbol.view :=
+{ view := λ stx, do { (a, b, c, d) ← view notation_quoted_symbol.reader stx, pure $ notation_quoted_symbol.view.mk a b c d },
+  review := λ ⟨a, b, c, d⟩, review notation_quoted_symbol.reader (a, b, c, d) }
+
+@[derive reader.has_view]
+def notation_symbol : reader :=
 any_of [
-  [raw_symbol "`", {read := quoted_symbol}, raw_symbol "`", prec?]
+  notation_quoted_symbol.reader
   --TODO, {read := do tk ← token, /- check if reserved token-/}
 ]
 
+@[derive reader.has_view]
 def action : reader :=
 [":", any_of [
   number,
@@ -95,35 +135,70 @@ def action : reader :=
     optional prec,
     notation_tk,-/]]
 
-def notation_reader : reader :=
+@[derive reader.has_view]
+def arg_transition : reader :=
+[ident, action?]
+
+@[derive reader.has_view]
+def transition :=
 any_of [
-  number,
-  [ident?,
-   [notation_symbol,
-    (any_of [
-      ["binder", prec?],
-      ["binders", prec?],
-      [ident, action?]
-    ])?
-   ]*
-  ]
+ ["binder", prec?],
+ ["binders", prec?],
+ arg_transition
 ]
 
+@[derive reader.has_view]
+def rule : reader :=
+[notation_symbol, transition?]
+
+@[derive reader.has_view]
+def rules : reader :=
+[ident?, rule*]
+
+@[derive reader.has_view]
+def notation_spec : reader :=
+any_of [
+  number,
+  rules
+]
+
+@[derive has_view]
 def notation.reader : reader :=
-node «notation» ["notation", notation_reader, ":=", term.reader]
+node «notation» ["notation", notation_spec, ":=", term.reader]
+
+structure notation.view :=
+(«notation» : syntax)
+(spec : syntax)
+(assign : syntax)
+(term : syntax)
+
+instance notation.has_view : notation.has_view notation.view :=
+{ view := λ stx, do { (a, b, c, d) ← view notation.reader stx, pure $ notation.view.mk a b c d },
+  review := λ ⟨a, b, c, d⟩, review notation.reader (a, b, c, d) }
 
 def reserve_notation : macro := {macro . name := `reserve_notation}
 
 def reserve_notation.reader : reader :=
-node «reserve_notation» [try ["reserve", "notation"], notation_reader]
+node «reserve_notation» [try ["reserve", "notation"], notation_spec]
 
 def mixfix : macro := {macro . name := `mixfix}
 
+@[derive has_view]
 def mixfix.reader : reader :=
 node «mixfix» [
   any_of ["prefix", "infix", "infixl", "infixr", "postfix"],
   notation_symbol, ":=", term.reader]
 
+structure mixfix.view :=
+(kind : syntax)
+(notation_symbol : syntax)
+(assign : syntax)
+(term : syntax)
+
+instance mixfix.has_view : mixfix.has_view mixfix.view :=
+{ view := λ stx, do { (a, b, c, d) ← view mixfix.reader stx, pure $ mixfix.view.mk a b c d },
+  review := λ ⟨a, b, c, d⟩, review mixfix.reader (a, b, c, d) }
+
 def reserve_mixfix : macro := {macro . name := `reserve_mixfix}
 
 def reserve_mixfix.reader : reader :=
@@ -168,12 +243,50 @@ def commands.reader : reader :=
 { read := do { rem ← remaining, commands_aux ff [] rem.succ },
   tokens := command.reader.tokens }
 
+-- custom reader requires custom instance
+instance commands.reader.has_view : commands.reader.has_view (list syntax) :=
+{..many.view command.reader}
+
 end commands
 
 def module := {macro . name := `module}
 
+@[derive reader.has_view]
 def module.reader : reader :=
 node module [prelude.reader?, import.reader*, commands.reader]
 
+structure module.view :=
+(«prelude» : optional_view syntax)
+(imports   : list syntax)
+(commands  : list syntax)
+
+instance module.has_view : module.has_view module.view :=
+{ view := λ stx, do { (a, b, c) ← view module.reader stx, pure $ module.view.mk a b c },
+  review := λ ⟨a, b, c⟩, review module.reader (a, b, c) }
+
+end reader
+
+namespace reader
+open macro.has_view combinators
+
+instance string_syntax_coe : has_coe string syntax :=
+⟨λ s, syntax.atom ⟨none, atomic_val.string s⟩⟩
+
+instance name_syntax_coe : has_coe name syntax :=
+⟨λ n, syntax.ident ⟨none, n, none, none⟩⟩
+
+def mixfix.expand (stx : syntax) : option syntax :=
+do v ← view mixfix stx,
+   syntax.atom ⟨_, atomic_val.string kind⟩ ← pure v.kind | failure,
+   -- TODO: reserved token case
+   prec ← notation_quoted_symbol.view.prec <$> view notation_quoted_symbol v.notation_symbol,
+   let spec := reader.has_view.review notation_spec $ match kind with
+     | "prefix" := reader.has_view.review rules (optional_view.none, [
+         reader.has_view.review rule (v.notation_symbol, optional_view.some $
+           reader.has_view.review arg_transition (`b, prec))
+       ])
+     | _ := sorry,
+   pure $ review «notation» (⟨"notation", spec, ":=", v.term⟩ : notation.view)
+
 end reader
 end lean.parser

tests/lean/reader1.lean

@@ -45,6 +45,15 @@ 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 := _",
+  some {root := stx, ..} ← pure $ reader.parse.view stx,
+  some stx ← pure $ mixfix.expand stx | io.fail "expand fail",
+  io.print_ln stx,
+  io.print_ln stx.reprint
+} : io unit)
+
 -- slowly progressing...
 #eval do
   s ← io.fs.read_file "../../library/init/core.lean",

tests/lean/reader1.lean.expected.out

@@ -79,6 +79,15 @@ result:
   []
   [(notation "notation" [[] [[["`" "Prop" "`" []] []]]] ":=" (hole "_"))])
  (eoi "")]
+result: 
+[(mixfix "prefix" ["`" "+" "`" [[":" (base10_lit "10")]]] ":=" (hole "_"))
+ (eoi "")]
+(notation
+ "notation"
+ [[] [[["`" "+" "`" [[":" (base10_lit "10")]]] [[b [[":" (base10_lit "10")]]]]]]]
+ ":="
+ (hole "_"))
+notation`+`:10 b:10 :=_
 error at line 10, column 19:
 expected "_"
 error at line 11, column 26: