From ea4d7af66d4f4d4c237ab42cf9cc5cb7c5063cd2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 17 Sep 2018 15:21:43 -0700 Subject: [PATCH] refactor(library/init/lean/parser/command): move out notations --- library/init/lean/parser/command.lean | 96 ++------------------- library/init/lean/parser/notation.lean | 112 +++++++++++++++++++++++++ tests/lean/parser1.lean | 2 +- 3 files changed, 122 insertions(+), 88 deletions(-) create mode 100644 library/init/lean/parser/notation.lean diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index 77018f162a..d4e4673840 100644 --- a/library/init/lean/parser/command.lean +++ b/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 diff --git a/library/init/lean/parser/notation.lean b/library/init/lean/parser/notation.lean new file mode 100644 index 0000000000..b1a5361244 --- /dev/null +++ b/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 diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index db08f0df5d..9f1134707c 100644 --- a/tests/lean/parser1.lean +++ b/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)