additional syntactic sugar

- allow multiple names in infix, typesig, and dcon defs
- align fixities with Idris

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

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 ()

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)