From d3ca360e7fe24ed01897ae824c9aaf25f3cacd3c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Jul 2019 10:49:54 -0700
Subject: [PATCH] feat(library/init/lean/parser): depArrow proof of concept

---
 library/init/lean/parser/parser.lean  | 16 ++++++++++++++++
 library/init/lean/parser/term.lean    | 10 +++++++---
 tests/playground/termparsertest1.lean |  7 ++++++-
 3 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index e932a7a612..126c960df3 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -806,6 +806,22 @@ let asciiSym := asciiSym.trim;
 { info := unicodeSymbolInfo sym asciiSym lbp,
   fn   := unicodeSymbolFn sym asciiSym }
 
+def unicodeSymbolCheckPrecFnAux (sym asciiSym : String) (lbp : Nat) (errorMsg : String) (precErrorMsg : String) : ParserFn leading :=
+fun (rbp : Nat) c s =>
+  if rbp > lbp then s.mkError precErrorMsg
+  else satisfySymbolFn (fun s => s == sym || s == asciiSym) errorMsg c s
+
+@[inline] def unicodeSymbolCheckPrecFn (sym asciiSym : String) (lbp : Nat) : ParserFn leading :=
+unicodeSymbolCheckPrecFnAux sym asciiSym lbp
+  ("expected '" ++ sym ++ "' or '" ++ asciiSym ++ "'")
+  ("found '" ++ sym ++ "' as expected, but brackets are needed") -- improve error message
+
+@[inline] def unicodeSymbolCheckPrec (sym asciiSym : String) (lbp : Nat) : Parser leading :=
+let sym := sym.trim;
+let asciiSym := asciiSym.trim;
+{ info := unicodeSymbolInfo sym asciiSym lbp,
+  fn   := unicodeSymbolCheckPrecFn sym asciiSym lbp }
+
 def mkAtomicInfo (k : String) : ParserInfo :=
 { firstTokens := FirstTokens.tokens [ { val := k } ] }
 
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 04376c9db2..2fad7542f4 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -45,7 +45,10 @@ 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
-@[inline] def parenSpecial : Parser := optional (", " >> sepBy termParser ", " <|> " : " >> termParser)
+def namedArgument  := parser! " := " >> termParser
+def typeAscription := parser! " : " >> termParser
+def tupleTail      := parser! ", " >> sepBy1 termParser ", "
+def parenSpecial : Parser := optional (tupleTail <|> typeAscription <|> namedArgument)
 @[builtinTermParser] def paren := parser! symbol "(" appPrec >> optional (termParser >> parenSpecial) >> ")"
 @[builtinTermParser] def anonymousCtor := parser! symbol "⟨" appPrec >> sepBy1 termParser ", " >> "⟩"
 @[inline] def optIdent : Parser := optional (try (ident >> " : "))
@@ -63,12 +66,13 @@ def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
 @[builtinTermParser] def subtype := parser! "{" >> ident >> optType >> " // " >> termParser >> "}"
 @[builtinTermParser] def list := parser! symbol "[" appPrec >> sepBy termParser "," true >> "]"
-def binderIdent := ident <|> hole
+-- def binderIdent := ident <|> hole
+@[builtinTermParser] def depArrow := parser! "{" >> many1 ident >> " : " >> termParser >> "}" >> unicodeSymbolCheckPrec " → " " -> " 25 >> termParser
 
 
 @[builtinTermParser] def app   := tparser! pushLeading >> termParser appPrec
 @[builtinTermParser] def proj  := tparser! pushLeading >> symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
-@[builtinTermParser] def arrow := tparser! unicodeInfixR "→" "->" 25
+@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
 @[builtinTermParser] def array := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]"
 
 @[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean
index 65c5b4cd6b..a118966936 100644
--- a/tests/playground/termparsertest1.lean
+++ b/tests/playground/termparsertest1.lean
@@ -51,5 +51,10 @@ test [
 "f [10, 20]",
 "g a[x+2]",
 "g f.a.1.2.bla x.1.a",
-"x+y*z < 10/3"
+"x+y*z < 10/3",
+"id (α := Nat) 10",
+"(x : a)",
+"a -> b",
+"f ((x : a) -> b)",
+"f ({x : a} -> b)"
 ]