Make list, cons, nil predeclared builtins in jvt

src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs

@@ -65,17 +65,17 @@ runParserS'' parser sig bs fileName input_ =
 
 createBuiltinConstr ::
   Symbol ->
-  BuiltinDataTag ->
+  Tag ->
   Text ->
   Type ->
   Location ->
   ConstructorInfo
-createBuiltinConstr sym btag name ty i =
-  let n = builtinConstrArgsNum btag
+createBuiltinConstr sym tag name ty i =
+  let n = length (typeArgs ty)
    in ConstructorInfo
         { _constructorName = name,
           _constructorLocation = Just i,
-          _constructorTag = BuiltinTag btag,
+          _constructorTag = tag,
           _constructorType = ty,
           _constructorArgsNum = n,
           _constructorArgNames = replicate n Nothing,
@@ -84,22 +84,22 @@ createBuiltinConstr sym btag name ty i =
           _constructorFixity = Nothing
         }
 
-declareBuiltins :: forall t e r. (Members '[InfoTableBuilder' t e] r) => ParsecS r ()
-declareBuiltins = do
+declareInductiveBuiltins ::
+  forall t e r.
+  ((Member (InfoTableBuilder' t e)) r) =>
+  Text ->
+  [(Tag, Text, Type -> Type)] ->
+  ParsecS r ()
+declareInductiveBuiltins indName ctrs = do
   loc <- curLoc
   let i = mkInterval loc loc
   sym <- lift $ freshSymbol' @t @e
-  let tyio = mkTypeInductive sym
-      constrs =
-        [ createBuiltinConstr sym TagReturn "return" (mkTypeFun [TyDynamic] tyio) i,
-          createBuiltinConstr sym TagBind "bind" (mkTypeFun [tyio, mkTypeFun [TyDynamic] tyio] tyio) i,
-          createBuiltinConstr sym TagWrite "write" (mkTypeFun [TyDynamic] tyio) i,
-          createBuiltinConstr sym TagReadLn "readLn" tyio i
-        ]
+  let indTy = mkTypeInductive sym
+      constrs = map (builtinConstr i sym indTy) ctrs
   lift $
     registerInductive' @t @e
       ( InductiveInfo
-          { _inductiveName = "IO",
+          { _inductiveName = indName,
             _inductiveSymbol = sym,
             _inductiveLocation = Just i,
             _inductiveKind = TyDynamic,
@@ -108,6 +108,34 @@ declareBuiltins = do
           }
       )
   lift $ mapM_ (registerConstr' @t @e) constrs
+  where
+    builtinConstr :: Interval -> Symbol -> Type -> (Tag, Text, Type -> Type) -> ConstructorInfo
+    builtinConstr i sym indTy (tag, ctorName, ctorTyFn) = createBuiltinConstr sym tag ctorName (ctorTyFn indTy) i
+
+declareBuiltinIO :: forall t e r. (Members '[InfoTableBuilder' t e] r) => ParsecS r ()
+declareBuiltinIO =
+  declareInductiveBuiltins @t @e
+    "IO"
+    [ (BuiltinTag TagReturn, "return", mkTypeFun [TyDynamic]),
+      (BuiltinTag TagBind, "bind", \ty -> mkTypeFun [ty, mkTypeFun [TyDynamic] ty] ty),
+      (BuiltinTag TagWrite, "write", mkTypeFun [TyDynamic]),
+      (BuiltinTag TagReadLn, "readLn", id)
+    ]
+
+declareBuiltinList :: forall t e r. (Members '[InfoTableBuilder' t e] r) => ParsecS r ()
+declareBuiltinList = do
+  tagNil <- lift (freshTag' @t @e)
+  tagCons <- lift (freshTag' @t @e)
+  declareInductiveBuiltins @t @e
+    "list"
+    [ (tagNil, "nil", id),
+      (tagCons, "cons", \ty -> mkTypeFun [TyDynamic, ty] ty)
+    ]
+
+declareBuiltins :: forall t e r. (Members '[InfoTableBuilder' t e] r) => ParsecS r ()
+declareBuiltins = do
+  declareBuiltinIO @t @e
+  declareBuiltinList @t @e
 
 parseToplevel ::
   forall t e d.

tests/Tree/negative/test003.jvt

@@ -1,10 +1,5 @@
 -- case on non-data
 
-type list {
-  nil : list;
-  cons : * -> list -> list;
-}
-
 function main() : * {
   case[list](3) {
     nil: 0

tests/Tree/negative/test005.jvt

@@ -1,10 +1,5 @@
 -- no matching case branch
 
-type list {
-  nil : list;
-  cons : * -> list -> list;
-}
-
 function main() : * {
   case[list](alloc[nil]()) {
     cons: 1

tests/Tree/positive/test009.jvt

@@ -1,8 +1,3 @@
-type list {
-  nil : list;
-  cons : (*, list) → list;
-}
-
 function hd(list) : *;
 function tl(list) : list;
 function null(list) : bool;

tests/Tree/positive/test028.jvt

@@ -1,8 +1,3 @@
-type list {
-  nil : list;
-  cons : (*, list) → list;
-}
-
 function sum''(integer) : integer;
 function gt5(integer) : bool;
 function dec(integer) : integer;

tests/Tree/positive/test029.jvt

@@ -1,8 +1,3 @@
-type list {
-  nil : list;
-  cons : (*, list) → list;
-}
-
 function main() : *;
 
 function main() : * {

tests/Tree/positive/test035.jvt

@@ -1,8 +1,3 @@
-type list {
-  nil : list;
-  cons : (*, list) → list;
-}
-
 function mklst(integer) : list;
 function mklst2(integer) : list;
 function append(list, list) : list;

tests/Tree/positive/test036.jvt

@@ -1,5 +1,5 @@
 type stream {
-  cons : (integer, unit → stream) → stream;
+  scons : (integer, unit → stream) → stream;
 }
 
 function force(unit → stream) : stream;
@@ -17,24 +17,24 @@ function force(f : unit → stream) : stream {
 
 function filter(f : integer → bool, s : unit → stream, unit) : stream {
   save[s1](call[force](s)) {
-    br(call(f, s1.cons[0])) {
-      true: alloc[cons](s1.cons[0], calloc[filter](f, s1.cons[1]))
-      false: call[filter](f, s1.cons[1], unit)
+    br(call(f, s1.scons[0])) {
+      true: alloc[scons](s1.scons[0], calloc[filter](f, s1.scons[1]))
+      false: call[filter](f, s1.scons[1], unit)
     }
   }
 }
 
 function nth(n : integer, s : unit → stream) : integer {
   save[s1](call[force](s)) {
     br(eq(0, n)) {
-      true: s1.cons[0]
-      false: call[nth](sub(n, 1), s1.cons[1])
+      true: s1.scons[0]
+      false: call[nth](sub(n, 1), s1.scons[1])
     }
   }
 }
 
 function numbers(n : integer, unit) : stream {
-  alloc[cons](n, calloc[numbers](add(1, n)))
+  alloc[scons](n, calloc[numbers](add(1, n)))
 }
 
 function indivisible(n : integer, m : integer) : bool {
@@ -46,7 +46,7 @@ function indivisible(n : integer, m : integer) : bool {
 
 function eratostenes(s : unit → stream, unit) : stream {
   save[s1](call[force](s)) {
-    alloc[cons](s1.cons[0], calloc[eratostenes](calloc[filter](calloc[indivisible](s1.cons[0]), s1.cons[1])))
+    alloc[scons](s1.scons[0], calloc[eratostenes](calloc[filter](calloc[indivisible](s1.scons[0]), s1.scons[1])))
   }
 }