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

fix(library/init/lean/parser/term): allow namedArgument notation in applications only

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-08 13:43:12 -07:00
parent 769e5fc8b1
commit 846ec9578d
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/parser/term.lean
View file

@ -45,10 +45,9 @@ pushLeading >> symbol sym lbp >> termParser lbp
@[builtinTermParser] def hole := parser! symbol "_" appPrec
@[builtinTermParser] def «sorry» := parser! symbol "sorry" appPrec
@[builtinTermParser] def cdot := parser! symbol "·" appPrec
def namedArgument := parser! " := " >> termParser
def typeAscription := parser! " : " >> termParser
def tupleTail := parser! ", " >> sepBy1 termParser ", "
def parenSpecial : Parser := optional (tupleTail <|> typeAscription <|> namedArgument)
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
@[builtinTermParser] def paren := parser! symbol "(" appPrec >> optional (termParser >> parenSpecial) >> ")"
@[builtinTermParser] def anonymousCtor := parser! symbol "⟨" appPrec >> sepBy1 termParser ", " >> "⟩"
@[inline] def optIdent : Parser := optional (try (ident >> " : "))
@ -79,7 +78,8 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl
def simpleBinder := parser! many1 binderIdent
@[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser
@[builtinTermParser] def app := tparser! pushLeading >> termParser appPrec
def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! pushLeading >> (namedArgument <|> termParser appPrec)
@[builtinTermParser] def proj := tparser! pushLeading >> symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
@[builtinTermParser] def array := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]"

5
tests/playground/termparsertest1.lean
View file

@ -19,7 +19,7 @@ do
env ← mkEmptyEnvironment;
termPTables ← builtinTermParsingTable.get;
match runParser env termPTables input "<input>" "expr" with
| Except.ok _ => throw "unexpected success"
| Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx))
| Except.error msg => IO.println ("failed as expected, error: " ++ msg)
def testFailures (is : List String) : IO Unit :=
@ -77,5 +77,6 @@ test [
"∀ x y (z : Nat), x > y -> x > y - z"
];
testFailures [
"f {x : a} -> b"
"f {x : a} -> b",
"(x := 20)"
]