From 8fe9613c02d877556407850ba148b6ff4981e9eb Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 23 Oct 2024 21:41:36 -0700
Subject: [PATCH] additional syntactic sugar

- allow multiple names in infix, typesig, and dcon defs
- align fixities with Idris
---
 aoc2023/Day1.newt        |  2 +-
 aoc2023/Day2.newt        |  4 ++--
 aoc2023/Lib.newt         | 18 ++++++++----------
 src/Lib/Parser.idr       | 10 +++++-----
 src/Lib/ProcessDecl.idr  | 31 +++++++++++++++----------------
 src/Lib/Syntax.idr       | 10 +++++-----
 tests/black/Oper.newt    |  8 +++-----
 tests/black/Prelude.newt |  2 +-
 8 files changed, 40 insertions(+), 45 deletions(-)

diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt
index d678bf0..2f81ce4 100644
--- a/aoc2023/Day1.newt
+++ b/aoc2023/Day1.newt
@@ -51,7 +51,7 @@ part1 text digits =
   let nums = map combine $ map digits lines in
   foldl _+_ 0 nums
 
-infixl 3 _>>_
+infixl 1 _>>_
 
 _>>_ : {A B : U} -> A -> B -> B
 a >> b = b
diff --git a/aoc2023/Day2.newt b/aoc2023/Day2.newt
index dc4adbd..0f00e8d 100644
--- a/aoc2023/Day2.newt
+++ b/aoc2023/Day2.newt
@@ -12,7 +12,7 @@ data Game : U where
 -- Add, Sub, Mul, Neg
 
 -- NB this is not lazy!
-infixl 2 _&&_
+infixl 5 _&&_
 
 _&&_ : Bool -> Bool -> Bool
 a && b = case a of
@@ -68,7 +68,7 @@ parseGame line =
       _ => Left "No Game"
     _ => Left $ "No colon in " ++ line
 
-infixl 3 _>>_
+infixl 1 _>>_
 
 _>>_ : {A B : U} -> A -> B -> B
 a >> b = b
diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt
index ca90881..09b4465 100644
--- a/aoc2023/Lib.newt
+++ b/aoc2023/Lib.newt
@@ -21,7 +21,7 @@ data Either : U -> U -> U where
   Right : {a b : U} -> b -> Either a b
 
 
-infixr 4 _::_
+infixr 7 _::_
 data List : U -> U where
   Nil : {a : U} -> List a
   _::_ : {a : U} -> a -> List a -> List a
@@ -41,11 +41,12 @@ length : {a : U} -> List a -> Nat
 length Nil = Z
 length (x :: xs) = S (length xs)
 
-infixr 2 _,_
+infixr 0 _,_
 
 data Pair : U -> U -> U where
   _,_ : {a b : U} -> a -> b -> Pair a b
 
+-- Idris says it special cases to deal with unification issues
 infixr 0 _$_
 
 _$_ : {a b : U} -> (a -> b) -> a -> b
@@ -104,13 +105,10 @@ pfunc _+_ : Int -> Int -> Int := "(x,y) => x + y"
 pfunc _-_ : Int -> Int -> Int := "(x,y) => x - y"
 pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
 pfunc _/_ : Int -> Int -> Int := "(x,y) => x / y"
-infix 3 _<_
-infix 3 _<=_
-infixl 4 _-_
-infixl 4 _+_
-infixl 5 _*_
-infixl 5 _/_
 
+infix 6 _<_ _<=_
+infixl 8 _+_ _-_
+infixl 9 _*_ _/_
 
 -- Ideally we'd have newt write the arrows for us to keep things correct
 -- We'd still have difficulty with callbacks...
@@ -134,7 +132,7 @@ pfunc slen : String -> Int := "s => s.length"
 pfunc sindex : String -> Int -> Char := "(s,i) => s[i]"
 
 
-infixl 4 _++_
+infixl 7 _++_
 pfunc _++_ : String -> String -> String := "(a,b) => a + b"
 
 
@@ -159,6 +157,6 @@ map f Nil = Nil
 map f (x :: xs) = f x :: map f xs
 
 
-infixl 7 _._
+infixl 9 _._
 _._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
 (f . g) x = f ( g x)
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 1e496b1..06963a1 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -244,13 +244,13 @@ typeExpr = binders
 
 export
 parseSig : Parser Decl
-parseSig = TypeSig <$> getPos <*> (ident <|> uident) <* keyword ":" <*> typeExpr
+parseSig = TypeSig <$> getPos <*> some (ident <|> uident) <* keyword ":" <*> typeExpr
 
 parseImport : Parser Import
 parseImport = MkImport <$> getPos <* keyword "import" <*> uident
 
 -- Do we do pattern stuff now? or just name = lambda?
-
+-- TODO multiple names
 parseMixfix : Parser Decl
 parseMixfix = do
   fc <- getPos
@@ -258,9 +258,9 @@ parseMixfix = do
      <|> InfixR <$ keyword "infixr"
      <|> Infix <$ keyword "infix"
   prec <- token Number
-  op <- token MixFix
-  addOp op (cast prec) fix
-  pure $ PMixFix fc op (cast prec) fix
+  ops <- some $ token MixFix
+  for_ ops $ \ op => addOp op (cast prec) fix
+  pure $ PMixFix fc ops (cast prec) fix
 
 getName : Raw -> Parser String
 getName (RVar x nm) = pure nm
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 987f0cc..1ea9495 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -1,6 +1,7 @@
 module Lib.ProcessDecl
 
 import Data.IORef
+import Data.String
 
 import Lib.Elab
 import Lib.Parser
@@ -30,20 +31,23 @@ collectDecl (x :: xs) = x :: collectDecl xs
 export
 processDecl : Decl -> M ()
 
+-- REVIEW I supposed I could have updated top here instead of the dance with the parser...
 processDecl (PMixFix{})  = pure ()
 
-processDecl (TypeSig fc nm tm) = do
+processDecl (TypeSig fc names tm) = do
   top <- get
-  let Nothing := lookup nm top
-    | _ => error fc "\{show nm} is already defined"
+  for_ names $ \nm => do
+    let Nothing := lookup nm top
+      | _ => error fc "\{show nm} is already defined"
+    pure ()
   putStrLn "-----"
-  putStrLn "TypeSig \{nm} \{show tm}"
+  putStrLn "TypeSig \{unwords names} : \{show tm}"
   ty <- check (mkCtx top.metas fc) tm (VU fc)
   putStrLn "got \{pprint [] ty}"
   -- I was doing this previously, but I don't want to over-expand VRefs
   -- ty' <- nf [] ty
   -- putStrLn "nf \{pprint [] ty'}"
-  modify $ setDef nm ty Axiom
+  for_ names $ \nm => modify $ setDef nm ty Axiom
 
 processDecl (PType fc nm ty) = do
   ctx <- get
@@ -114,11 +118,10 @@ processDecl (Data fc nm ty cons) = do
   modify $ setDef nm tyty Axiom
   ctx <- get
   cnames <- for cons $ \x => case x of
-      -- expecting tm to be a Pi type
-      (TypeSig fc nm' tm) => do
+      (TypeSig fc names tm) => do
           ctx <- get
           dty <- check (mkCtx ctx.metas fc) tm (VU fc)
-          debug "dty \{nm'} is \{pprint [] dty}"
+          debug "dty \{show names} is \{pprint [] dty}"
 
           -- We only check that codomain uses the right type constructor
           -- We know it's in U because it's part of a checked Pi type
@@ -130,15 +133,11 @@ processDecl (Data fc nm ty cons) = do
           when (hn /= nm) $
             error (getFC codomain) "Constructor codomain is \{pprint tnames codomain} rather than \{nm}"
 
-          modify $ setDef nm' dty (DCon (getArity dty) nm)
-          pure nm'
+          for_ names $ \ nm' => modify $ setDef nm' dty (DCon (getArity dty) nm)
+          pure names
       _ => throwError $ E (0,0) "expected constructor declaration"
-  -- TODO check tm is VU or Pi ending in VU
-  -- Maybe a pi -> binders function
-  -- TODO we're putting in axioms, we need constructors
-  -- for each constructor, check and add
-  putStrLn "setDef \{nm}  TCon \{show cnames}"
-  modify $ setDef nm tyty (TCon cnames)
+  putStrLn "setDef \{nm}  TCon \{show $ join cnames}"
+  modify $ setDef nm tyty (TCon (join cnames))
   pure ()
   where
     checkDeclType : Tm -> M ()
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index e4c640e..134d28c 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -100,13 +100,13 @@ data Import = MkImport FC Name
 -- FIXME - I think I don't want "where" here, but the parser has an issue
 public export
 data Decl
-  = TypeSig FC Name Raw
+  = TypeSig FC (List Name) Raw
   | Def FC Name (List (Raw,Raw)) -- (List Clause)
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
   | PType FC Name (Maybe Raw)
   | PFunc FC Name Raw String
-  | PMixFix FC Name Nat Fixity
+  | PMixFix FC (List Name) Nat Fixity
 
 
 public export
@@ -148,7 +148,7 @@ Show Decl where
   show (DCheck _ x y) = foo ["DCheck", show x, show y]
   show (PType _ name ty) = foo ["PType", name, show ty]
   show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src]
-  show (PMixFix _ nm prec fix) = foo ["PMixFix", nm, show prec, show fix]
+  show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
 
 export covering
 Show Module where
@@ -246,11 +246,11 @@ Pretty Module where
         doImport (MkImport _ nm) = text "import" <+> text nm ++ line
 
         doDecl : Decl -> Doc
-        doDecl (TypeSig _ nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
+        doDecl (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
         doDecl (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> "=" <+> pretty b) clauses
         -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
         doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
         doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
         doDecl (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
         doDecl (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
-        doDecl (PMixFix _ _ _ fix) = text (show fix)
+        doDecl (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
diff --git a/tests/black/Oper.newt b/tests/black/Oper.newt
index 2a32747..a0350c7 100644
--- a/tests/black/Oper.newt
+++ b/tests/black/Oper.newt
@@ -11,10 +11,8 @@ module Oper
 -- long term, I might want TopContext in the parser, and parse a top-level
 -- declaration at a time (for incremental updates), but much longer term.
 
-infixl 4 _+_
-infixl 4 _-_
-infixl 5 _*_
-infixl 5 _/_
+infixl 8 _+_ _-_
+infixl 9 _*_ _/_
 
 ptype Int
 ptype String
@@ -33,7 +31,7 @@ _+_ x y = plus x y
 test : Int -> Int
 test x = 42 + x * 3 + 2
 
-infixr 2 _,_
+infixr 0 _,_
 data Pair : U -> U -> U where
   _,_ : {A B : U} -> A -> B -> Pair A B
 
diff --git a/tests/black/Prelude.newt b/tests/black/Prelude.newt
index 070e670..c3b1858 100644
--- a/tests/black/Prelude.newt
+++ b/tests/black/Prelude.newt
@@ -18,7 +18,7 @@ data List : U -> U where
 
 -- Currently if I say _::_ = Cons, it gets curried
 
-infixr 4 _::_
+infixr 7 _::_
 _::_ : {a : U} -> a -> List a -> List a
 _::_ x xs = Cons x xs