refactor(library/init/lean/parser/command): move out notations

library/init/lean/parser/command.lean

@@ -6,10 +6,11 @@ Author: Sebastian Ullrich
 Command parsers
 -/
 prelude
-import init.lean.parser.term
+import init.lean.parser.notation
 
 namespace lean
 namespace parser
+
 open combinators monad_parsec
 open parser.has_tokens parser.has_view
 
@@ -20,6 +21,8 @@ local postfix +:10000 := combinators.many1
 @[derive parser.has_view parser.has_tokens]
 def command_parser.recurse : command_parser := recurse ()
 
+namespace «command»
+
 set_option class.instance_max_depth 200
 @[derive parser.has_view parser.has_tokens]
 def open_spec.parser : command_parser :=
@@ -49,95 +52,12 @@ any_of [
   node! «universe» ["universe", id: ident]
 ]
 
-namespace notation_spec
-@[derive parser.has_tokens parser.has_view]
-def precedence.parser : command_parser :=
-node! «precedence» [":", prec: number]/-TODO <|> expr-/
-
-def quoted_symbol.parser : command_parser :=
-do (s, info) ← with_source_info $ take_until (= '`'),
-   pure $ syntax.atom ⟨info, s⟩
-
-instance quoted_symbol.tokens : parser.has_tokens quoted_symbol.parser := ⟨[]⟩
-instance quoted_symbol.view : parser.has_view quoted_symbol.parser syntax := default _
-
-@[derive parser.has_tokens parser.has_view]
-def symbol_quote.parser : command_parser :=
-node! notation_quoted_symbol [
-  left_quote: raw $ ch '`',
-  symbol: quoted_symbol.parser,
-  right_quote: raw (ch '`') tt, -- consume trailing ws
-  prec: precedence.parser?]
-
---TODO(Sebastian): cannot be called `symbol` because of hygiene problems
-@[derive parser.has_tokens parser.has_view]
-def notation_symbol.parser : command_parser :=
-node_choice! notation_symbol {
-  quoted: symbol_quote.parser
-  --TODO, {read := do tk ← token, /- check if reserved token-/}
-}
-
-@[derive parser.has_tokens parser.has_view]
-def action.parser : command_parser :=
-node! action [":", action: node_choice! action_kind {
-  prec: number,
-  max: symbol_or_ident "max",
-  prev: symbol_or_ident "prev",
-  scoped: symbol_or_ident "scoped"
-  /-TODO seq [
-    "(",
-    any_of ["foldl", "foldr"],
-    optional prec,
-    notation_tk,-/}]
-
-@[derive parser.has_tokens parser.has_view]
-def transition.parser : command_parser :=
-node_choice! transition {
-  binder: node! binder ["binder", prec: precedence.parser?],
-  binders: node! binders ["binders", prec: precedence.parser?],
-  arg: node! argument [id: ident, action: action.parser?]
-}
-
-@[derive parser.has_tokens parser.has_view]
-def rule.parser : command_parser :=
-node! rule [symbol: notation_symbol.parser, transition: transition.parser?]
-
-end notation_spec
-
-@[derive parser.has_tokens parser.has_view]
-def notation_spec.parser : command_parser :=
-node_choice! notation_spec {
-  number_literal: number,
-  rules: node! notation_spec.rules [id: ident?, rules: notation_spec.rule.parser*]
-}
-
-@[derive parser.has_tokens parser.has_view]
-def notation.parser : command_parser :=
-node! «notation» ["notation", spec: notation_spec.parser, ":=", term: term.parser]
-
-@[derive parser.has_tokens parser.has_view]
-def reserve_notation.parser : command_parser :=
-node! «reserve_notation» [try ["reserve", "notation"], spec: notation_spec.parser]
-
-@[derive parser.has_tokens parser.has_view]
-def mixfix.kind.parser : command_parser :=
-node_choice! mixfix.kind {"prefix", "infix", "infixl", "infixr", "postfix"}
-
-@[derive parser.has_tokens parser.has_view]
-def mixfix.parser : command_parser :=
-node! «mixfix» [
-  kind: mixfix.kind.parser,
-  symbol: notation_spec.notation_symbol.parser, ":=", term: term.parser]
-
-@[derive parser.has_tokens parser.has_view]
-def reserve_mixfix.parser : command_parser :=
-node! «reserve_mixfix» [
-  try ["reserve", kind: mixfix.kind.parser],
-  symbol: notation_spec.notation_symbol.parser]
-
 @[derive parser.has_tokens parser.has_view]
 def check.parser : command_parser :=
 node! check ["#check", term: term.parser]
+end «command»
+
+open «command»
 
 @[derive parser.has_tokens parser.has_view]
 def command.parser : command_parser :=
@@ -147,6 +67,7 @@ any_of [open.parser, section.parser, universe.parser, notation.parser, reserve_n
 end parser
 
 namespace parser
+namespace «command»
 open syntax_node_kind.has_view combinators notation_spec
 
 -- example macro
@@ -168,5 +89,6 @@ do v ← view mixfix stx,
      | _ := sorry,
    pure $ review «notation» ⟨"notation", spec, ":=", v.term⟩
 
+end «command»
 end parser
 end lean

library/init/lean/parser/notation.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sebastian Ullrich
+
+Notation parsers
+-/
+prelude
+import init.lean.parser.term
+
+namespace lean
+namespace parser
+namespace «command»
+
+open combinators monad_parsec
+open parser.has_tokens parser.has_view
+
+local postfix `?`:10000 := optional
+local postfix *:10000 := combinators.many
+local postfix +:10000 := combinators.many1
+
+set_option class.instance_max_depth 100
+
+namespace notation_spec
+@[derive parser.has_tokens parser.has_view]
+def precedence.parser : command_parser :=
+node! «precedence» [":", prec: number]/-TODO <|> expr-/
+
+def quoted_symbol.parser : command_parser :=
+do (s, info) ← with_source_info $ take_until (= '`'),
+   pure $ syntax.atom ⟨info, s⟩
+
+instance quoted_symbol.tokens : parser.has_tokens quoted_symbol.parser := ⟨[]⟩
+instance quoted_symbol.view : parser.has_view quoted_symbol.parser syntax := default _
+
+@[derive parser.has_tokens parser.has_view]
+def symbol_quote.parser : command_parser :=
+node! notation_quoted_symbol [
+  left_quote: raw $ ch '`',
+  symbol: quoted_symbol.parser,
+  right_quote: raw (ch '`') tt, -- consume trailing ws
+  prec: precedence.parser?]
+
+--TODO(Sebastian): cannot be called `symbol` because of hygiene problems
+@[derive parser.has_tokens parser.has_view]
+def notation_symbol.parser : command_parser :=
+node_choice! notation_symbol {
+  quoted: symbol_quote.parser
+  --TODO, {read := do tk ← token, /- check if reserved token-/}
+}
+
+@[derive parser.has_tokens parser.has_view]
+def action.parser : command_parser :=
+node! action [":", action: node_choice! action_kind {
+  prec: number,
+  max: symbol_or_ident "max",
+  prev: symbol_or_ident "prev",
+  scoped: symbol_or_ident "scoped"
+  /-TODO seq [
+    "(",
+    any_of ["foldl", "foldr"],
+    optional prec,
+    notation_tk,-/}]
+
+@[derive parser.has_tokens parser.has_view]
+def transition.parser : command_parser :=
+node_choice! transition {
+  binder: node! binder ["binder", prec: precedence.parser?],
+  binders: node! binders ["binders", prec: precedence.parser?],
+  arg: node! argument [id: ident, action: action.parser?]
+}
+
+@[derive parser.has_tokens parser.has_view]
+def rule.parser : command_parser :=
+node! rule [symbol: notation_symbol.parser, transition: transition.parser?]
+
+end notation_spec
+
+@[derive parser.has_tokens parser.has_view]
+def notation_spec.parser : command_parser :=
+node_choice! notation_spec {
+  number_literal: number,
+  rules: node! notation_spec.rules [id: ident?, rules: notation_spec.rule.parser*]
+}
+
+@[derive parser.has_tokens parser.has_view]
+def notation.parser : command_parser :=
+node! «notation» ["notation", spec: notation_spec.parser, ":=", term: term.parser]
+
+@[derive parser.has_tokens parser.has_view]
+def reserve_notation.parser : command_parser :=
+node! «reserve_notation» [try ["reserve", "notation"], spec: notation_spec.parser]
+
+@[derive parser.has_tokens parser.has_view]
+def mixfix.kind.parser : command_parser :=
+node_choice! mixfix.kind {"prefix", "infix", "infixl", "infixr", "postfix"}
+
+@[derive parser.has_tokens parser.has_view]
+def mixfix.parser : command_parser :=
+node! «mixfix» [
+  kind: mixfix.kind.parser,
+  symbol: notation_spec.notation_symbol.parser, ":=", term: term.parser]
+
+@[derive parser.has_tokens parser.has_view]
+def reserve_mixfix.parser : command_parser :=
+node! «reserve_mixfix» [
+  try ["reserve", kind: mixfix.kind.parser],
+  symbol: notation_spec.notation_symbol.parser]
+
+end «command»
+end parser
+end lean

tests/lean/parser1.lean

@@ -60,7 +60,7 @@ universes u v
   (stx, ⟨[]⟩) ← pure $ parse_module "prefix `+`:10 := _",
   some {root := stx, ..} ← pure $ parser.parse.view stx,
   some {commands := [stx], ..} ← pure $ view module stx,
-  some stx ← pure $ mixfix.expand stx | throw "expand fail",
+  some stx ← pure $ command.mixfix.expand stx | throw "expand fail",
   io.println stx,
   io.println stx.reprint
 } : except_t string io unit)