Add list sugar

src/Lib/Elab.newt

@@ -80,6 +80,18 @@ lookupDef ctx name = go 0 ctx.types ctx.env
     go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs
     go ix _ _ = Nothing
 
+expandList : FC → Maybe Raw → Raw
+expandList fc Nothing = RVar fc "Nil"
+expandList fc (Just t) = go fc t
+  where
+    cons : FC → Raw → Raw → Raw
+    cons fc t u = RApp fc (RApp fc (RVar fc "_::_") t Explicit) u Explicit
+
+    go : FC → Raw → Raw
+    go fc (RApp fc' (RApp fc'' (RVar fc "_,_") t Explicit) u Explicit) =
+      cons fc t $ go fc u
+    go fc t = cons fc t (RVar fc "Nil")
+
 forceMeta : Val -> M Val
 forceMeta (VMeta fc ix sp) = do
   meta <- lookupMeta ix
@@ -977,6 +989,7 @@ mkPat (RAs fc as tm, icit) = do
     (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
     (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}"
     t => error fc "Can't put as on non-constructor \{show tm}"
+mkPat (RList fc mt, icit) = mkPat (expandList fc mt, icit)
 mkPat (tm, icit) = do
   top <- getTop
   case splitArgs tm Nil of
@@ -1538,6 +1551,8 @@ infer ctx (RVar fc nm) = go 0 ctx.types
     go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty)
       else go (i + 1) xs
 
+infer ctx (RList fc mt) = infer ctx $ expandList fc mt
+
 infer ctx (RApp fc t u icit) = do
   -- If the app is explicit, add any necessary metas
   (icit, t, tty) <- case icit of

src/Lib/Parser.newt

@@ -110,6 +110,14 @@ asAtom = do
 
 recordUpdate : Parser Raw
 
+listTypeExp : Parser Raw
+listTypeExp = do
+  fc <- getPos
+  symbol "["
+  tm <- optional typeExpr
+  symbol "]"
+  pure $ RList fc tm
+
 parenTypeExp : Parser Raw
 parenTypeExp = do
   fc <- getPos
@@ -134,6 +142,7 @@ atom = do
     <|> lit
     <|> RImplicit <$> getPos <* keyword "_"
     <|> RHole <$> getPos <* keyword "?"
+    <|> listTypeExp
     <|> parenTypeExp
 
 updateClause : Parser UpdateClause

src/Lib/Syntax.newt

@@ -60,6 +60,7 @@ data Raw : U where
   -- has to be applied or we have to know its type as Foo → Foo to elaborate.
   -- I can bake the arg in here, or require an app in elab.
   RUpdateRec : (fc : FC) → List UpdateClause → Maybe Raw → Raw
+  RList : (fc : FC) → Maybe Raw → Raw
 
 instance HasFC Raw where
   getFC (RVar fc nm) = fc
@@ -78,6 +79,7 @@ instance HasFC Raw where
   getFC (RAs fc _ _) = fc
   getFC (RUpdateRec fc _ _) = fc
   getFC (RImpossible fc) = fc
+  getFC (RList fc _) = fc
 
 data Import = MkImport FC (FC × Name)
 
@@ -189,6 +191,8 @@ instance Pretty Raw where
     asDoc p (RWhere _ dd b) = text "TODO pretty RWhere"
     asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")"
     asDoc p (RUpdateRec _ clauses tm) = text "{" <+> text "TODO RUpdateRec" <+> text "}"
+    asDoc p (RList _ (Just t)) = text "[" <+> asDoc p t <+> text "]"
+    asDoc p (RList _ Nothing) = text "[]"
 
 prettyBind : (BindInfo × Raw) -> Doc
 prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty)
@@ -246,6 +250,8 @@ substRaw ss t = case t of
   (RWhere fc ds body) => RWhere fc (map substDecl ds) (substRaw ss body)
   (RDo fc stmts) => RDo fc (substStmts ss stmts)
   (RCase fc scrut mdef alts) => RCase fc (substRaw ss scrut) (map (substRaw ss) mdef) (map substAlt alts)
+  (RList fc (Just t)) => RList fc (Just $ substRaw ss t)
+  (RList fc Nothing) => RList fc Nothing
   -- Enumerate to force consideration of new cases
   t@(RImpossible _) => t
   t@(RU _) => t

tests/ListSugar.newt

@@ -0,0 +1,19 @@
+module ListSugar
+
+import Prelude
+
+
+blah : List Int
+blah = [ 1, 2, 3]
+
+bar : List Int → Int
+bar [ ] = 0
+bar [x] = 1
+bar _ = 42
+
+main : IO Unit
+main = do
+  printLn blah
+  printLn $ bar []
+  printLn $ bar [ 42 ]
+  printLn $ bar blah

tests/ListSugar.newt.golden

@@ -0,0 +1,4 @@
+[1, 2, 3]
+0
+1
+42