feat(library/init/lean/parser/token): give number a view

library/init/lean/parser/level.lean

@@ -38,7 +38,7 @@ node_choice! leading {
   imax: symbol_or_ident "imax",
   hole: symbol "_" max_prec,
   paren: paren.parser,
-  lit: number,
+  lit: number.parser,
   var: ident.parser
 }
 
@@ -48,7 +48,7 @@ node! app [fn: get_leading, arg: recurse max_prec]
 
 @[derive parser.has_tokens parser.has_view]
 def add_lit.parser : trailing_level_parser :=
-node! add_lit [lhs: get_leading, "+", rhs: number]
+node! add_lit [lhs: get_leading, "+", rhs: number.parser]
 
 @[derive parser.has_tokens parser.has_view]
 def trailing.parser : trailing_level_parser :=

library/init/lean/parser/notation.lean

@@ -24,7 +24,7 @@ set_option class.instance_max_depth 100
 namespace notation_spec
 @[derive parser.has_tokens parser.has_view]
 def precedence.parser : term_parser :=
-node! «precedence» [":", prec: number]/-TODO <|> expr-/
+node! «precedence» [":", prec: number.parser]/-TODO <|> expr-/
 
 def quoted_symbol.parser : term_parser :=
 do (s, info) ← with_source_info $ take_until (= '`'),
@@ -52,7 +52,7 @@ node_choice! notation_symbol {
 @[derive parser.has_tokens parser.has_view]
 def action.parser : term_parser :=
 node! action [":", action: node_choice! action_kind {
-  prec: number,
+  prec: number.parser,
   max: symbol_or_ident "max",
   prev: symbol_or_ident "prev",
   scoped: symbol_or_ident "scoped"
@@ -79,7 +79,7 @@ end notation_spec
 @[derive parser.has_tokens parser.has_view]
 def notation_spec.parser : term_parser :=
 node_choice! notation_spec {
-  number_literal: number,
+  number_literal: number.parser,
   rules: node! notation_spec.rules [id: ident.parser?, rules: notation_spec.rule.parser*]
 }
 

library/init/lean/parser/pratt.lean

@@ -25,8 +25,8 @@ do st ← get,
      st ← get,
      some ⟨_, tk_cfg⟩ ← pure (st.tokens.match_prefix sym.mk_iterator) | error "curr_lbp: unreachable",
      pure tk_cfg.lbp
-   | syntax.node ⟨base10_lit, _⟩ := pure max_prec
-   | syntax.node ⟨id, _⟩ := pure max_prec
+   | syntax.node ⟨@number, _⟩ := pure max_prec
+   | syntax.node ⟨@ident, _⟩ := pure max_prec
    | _ := error "curr_lbp: unknown token kind"
 
 private def trailing_loop (trailing : reader_t syntax m syntax) (rbp : nat) : nat → syntax → parser

library/init/lean/parser/syntax.lean

@@ -26,7 +26,7 @@ structure source_info :=
 (trailing : substring)
 
 structure syntax_atom :=
-(info : option source_info) (val : string)
+(info : option source_info := none) (val : string)
 
 /-- A simple wrapper that should remind you to use the static declaration instead
     of hard-coding the node name. -/

library/init/lean/parser/term.lean

@@ -154,7 +154,7 @@ node! explicit [
 def leading.parser :=
 any_of [
   term.ident.parser,
-  number,
+  number.parser,
   paren.parser,
   hole.parser,
   sort.parser,
@@ -186,7 +186,7 @@ node! projection [
   ".":max_prec.succ,
   proj: node_choice! projection_spec {
     id: parser.ident.parser,
-    num: number,
+    num: number.parser,
   },
 ]
 

library/init/lean/parser/token.lean

@@ -89,13 +89,6 @@ instance raw.view {α} (p : m α) (t) : parser.has_view (raw p t : parser) synta
 
 end
 
-@[pattern] def base10_lit : syntax_node_kind := ⟨`lean.parser.base10_lit⟩
-
---TODO(Sebastian): other bases
-private def number' : basic_parser_m (source_info → syntax) :=
-do num ← take_while1 char.is_digit,
-   pure $ λ i, syntax.node ⟨base10_lit, [syntax.atom ⟨i, num⟩]⟩
-
 set_option class.instance_max_depth 200
 
 @[derive has_tokens has_view]
@@ -140,6 +133,13 @@ do tk ← match_token,
    | some ⟨tk, _, some r⟩ := error "symbol': not implemented" --str tk *> monad_parsec.lift r
    | none                 := monad_parsec.eoi *> error "end of file" <|> error "token"
 
+--TODO(Sebastian): other bases
+def number' : basic_parser_m (source_info → syntax) :=
+do stx ← (node_choice! number {
+     base10: raw (take_while1 char.is_digit),
+   } : basic_parser),
+   pure $ λ info, update_trailing info.trailing stx
+
 def token : basic_parser_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),
@@ -170,15 +170,24 @@ instance symbol.view (sym lbp) : parser.has_view (symbol sym lbp : parser) (opti
 instance symbol.view_default (sym lbp) : parser.has_view_default (symbol sym lbp : parser) _
   (some {info := none, val := sym}) := ⟨⟩
 
-def number : parser :=
+def number.parser : parser :=
 lift $ try $ do {
   it ← left_over,
-  stx@(syntax.node ⟨base10_lit, _⟩) ← token | error "" (dlist.singleton "number") it,
+  stx ← token,
+  some _ ← pure $ try_view number stx | error "" (dlist.singleton "number") it,
   pure stx
 } <?> "number"
 
-instance number.tokens : parser.has_tokens (number : parser) := default _
-instance number.view : parser.has_view (number : parser) syntax := default _
+instance number.parser.tokens : parser.has_tokens (number.parser : parser) := default _
+instance number.parser.view : parser.has_view (number.parser : parser) number.view :=
+{..number.has_view}
+
+def number.view.to_nat : number.view → nat
+| (number.view.base10 (syntax.atom a)) := a.val.to_nat
+| _ := 1138 -- should never happen, but let's still choose a grep-able number
+
+def number.view.of_nat (n : nat) : number.view :=
+number.view.base10 (syntax.atom {val := to_string n})
 
 def ident.parser : parser :=
 lift $ try $ do {