Add syntax for builtin list

src/Juvix/Compiler/Asm/Translation/FromCore.hs

@@ -19,9 +19,9 @@ fromCore :: Core.InfoTable -> InfoTable
 fromCore tab =
   InfoTable
     { _infoMainFunction = tab ^. Core.infoMain,
-      _infoFunctions = fmap (genCode tab) (tab ^. Core.infoFunctions),
-      _infoInductives = fmap translateInductiveInfo (tab ^. Core.infoInductives),
-      _infoConstrs = fmap translateConstructorInfo (tab ^. Core.infoConstructors)
+      _infoFunctions = genCode tab <$> tab ^. Core.infoFunctions,
+      _infoInductives = translateInductiveInfo <$> tab ^. Core.infoInductives,
+      _infoConstrs = translateConstructorInfo <$> tab ^. Core.infoConstructors
     }
 
 -- Generate code for a single function.

src/Juvix/Compiler/Builtins.hs

@@ -4,6 +4,7 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.IO,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
+    module Juvix.Compiler.Builtins.List,
     module Juvix.Compiler.Builtins.String,
     module Juvix.Compiler.Builtins.Debug,
     module Juvix.Compiler.Builtins.Control,
@@ -16,5 +17,6 @@ import Juvix.Compiler.Builtins.Debug
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int
+import Juvix.Compiler.Builtins.List
 import Juvix.Compiler.Builtins.Nat
 import Juvix.Compiler.Builtins.String

src/Juvix/Compiler/Builtins/List.hs

@@ -0,0 +1,37 @@
+module Juvix.Compiler.Builtins.List where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Pretty
+import Juvix.Prelude
+
+registerListDef :: Member Builtins r => InductiveDef -> Sem r ()
+registerListDef d = do
+  unless (isSmallUniverse' (d ^. inductiveType)) (error "Lists should be in the small universe")
+  registerBuiltin BuiltinList (d ^. inductiveName)
+  case d ^. inductiveConstructors of
+    [c1, c2] -> registerNil param c1 >> registerCons param c2
+    _ -> error "List should have exactly two constructors"
+  where
+    param :: VarName
+    param = case d ^. inductiveParameters of
+      [v] -> v ^. inductiveParamName
+      _ -> error "List should have exactly one type parameter"
+
+registerNil :: Member Builtins r => VarName -> InductiveConstructorDef -> Sem r ()
+registerNil a d@InductiveConstructorDef {..} = do
+  let nil = _inductiveConstructorName
+      ty = _inductiveConstructorType
+  list_ <- getBuiltinName (getLoc d) BuiltinList
+  let nilty = list_ @@ a
+  unless (ty === nilty) (error $ "nil has the wrong type " <> ppTrace ty <> " | " <> ppTrace nilty)
+  registerBuiltin BuiltinListNil nil
+
+registerCons :: Member Builtins r => VarName -> InductiveConstructorDef -> Sem r ()
+registerCons a d@InductiveConstructorDef {..} = do
+  let cons_ = _inductiveConstructorName
+      ty = _inductiveConstructorType
+  list_ <- getBuiltinName (getLoc d) BuiltinList
+  let consty = a --> list_ @@ a --> list_ @@ a
+  unless (ty === consty) (error "cons has the wrong type")
+  registerBuiltin BuiltinListCons cons_

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -40,11 +40,13 @@ builtinConstructors = \case
   BuiltinNat -> [BuiltinNatZero, BuiltinNatSuc]
   BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse]
   BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc]
+  BuiltinList -> [BuiltinListNil, BuiltinListCons]
 
 data BuiltinInductive
   = BuiltinNat
   | BuiltinBool
   | BuiltinInt
+  | BuiltinList
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinInductive
@@ -54,6 +56,7 @@ instance Pretty BuiltinInductive where
     BuiltinNat -> Str.nat
     BuiltinBool -> Str.bool_
     BuiltinInt -> Str.int_
+    BuiltinList -> Str.list
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -62,6 +65,8 @@ data BuiltinConstructor
   | BuiltinBoolFalse
   | BuiltinIntOfNat
   | BuiltinIntNegSuc
+  | BuiltinListNil
+  | BuiltinListCons
   deriving stock (Show, Eq, Ord, Generic, Data)
 
 instance Hashable BuiltinConstructor

src/Juvix/Compiler/Concrete/Keywords.hs

@@ -22,6 +22,8 @@ import Juvix.Data.Keyword.All
     kwAssign,
     kwAt,
     kwAxiom,
+    kwBracketL,
+    kwBracketR,
     kwBuiltin,
     kwCase,
     kwColon,