From d2fbd15b4a8d611ce63944db0637ca35eafa4e6e Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Tue, 25 Jun 2024 13:53:15 -0700
Subject: [PATCH] sugar on binders

---
 eg/ex.newt         |  2 +-
 src/Lib/Parser.idr | 37 +++++++++++++++++++------------------
 2 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/eg/ex.newt b/eg/ex.newt
index 94431b5..9d15bba 100644
--- a/eg/ex.newt
+++ b/eg/ex.newt
@@ -12,7 +12,7 @@ List : U -> U
 List = \ A => (L : U) -> L -> (A -> L -> L) -> L
 
 -- need more sugar for lambdas
-nil : (A : U) -> (L : U) -> L -> (A -> L -> L) -> L
+nil : (A L : U) -> L -> (A -> L -> L) -> L
 nil = \ A => \ L => \ n => \ f => n
 
 Bool : U
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index d0fc676..1bd7735 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -176,36 +176,37 @@ term =  caseExpr
     <|> lamExpr
     <|> parseOp
 
-expBinder : Parser Raw
-expBinder = do
+
+ebind : Parser (List (String, Icit, Raw))
+ebind = do
   sym "("
-  name <- ident
+  names <- some ident
   sym ":"
   ty <- typeExpr
   sym ")"
-  sym "->"
-  scope <- typeExpr
-  pure $ RPi (Just name) Explicit ty scope
+  pure $ map (\name => (name, Explicit, ty)) names
 
-impBinder : Parser Raw
-impBinder = do
+ibind : Parser (List (String, Icit, Raw))
+ibind = do
   sym "{"
-  name <- ident
+  names <- some ident
   sym ":"
   ty <- typeExpr
   sym "}"
+  pure $ map (\name => (name, Explicit, ty)) names
+
+-- Collect a bunch of binders (A : U) {y : A} -> ...
+binders : Parser Raw
+binders = do  
+  binds <- many (ibind <|> ebind)
   sym "->"
   scope <- typeExpr
-  pure $ RPi (Just name) Implicit ty scope
+  pure $ foldr mkBind scope (join binds)
+  where
+    mkBind : (String, Icit, Raw) -> Raw -> Raw
+    mkBind (name, icit, ty) scope = RPi (Just name) icit ty scope
 
--- something binder looking
--- todo sepby space or whatever
-export
-binder : Parser Raw
-binder = expBinder <|> impBinder
-
-
-typeExpr = binder
+typeExpr = binders
   <|> do
         exp <- term
         scope <- optional (sym "->" *> mustWork typeExpr)