From d2e5af8f88125f81be94a3a915a5e2c66ec6d870 Mon Sep 17 00:00:00 2001
From: Alex Humphreys <alex.humphreys@here.com>
Date: Tue, 2 Jun 2020 10:54:23 +0200
Subject: [PATCH] Add List type

Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
---
 Idrall/Check.idr  | 18 ++++++++++++++++++
 Idrall/Expr.idr   |  3 +++
 Idrall/Parser.idr |  7 ++++++-
 tests/Test.idr    |  2 +-
 4 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/Idrall/Check.idr b/Idrall/Check.idr
index a9e7feb..99891fe 100644
--- a/Idrall/Check.idr
+++ b/Idrall/Check.idr
@@ -52,6 +52,8 @@ mutual
       aEquivHelper i ns2 y ns2 z
   aEquivHelper i ns1 (EAssert x) ns2 (EAssert y)
     = aEquivHelper i ns1 x ns2 y
+  aEquivHelper i ns1 (EList x) ns2 (EList y)
+    = aEquivHelper i ns1 x ns2 y
   aEquivHelper _ _ _ _ _ = False
   -- TODO check if assert/equivalent should be in here
 
@@ -121,6 +123,7 @@ mutual
     | VBoolLit Bool
     | VNatural
     | VNaturalLit Nat
+    | VList Ty
     | VNeutral Ty Neutral
 
   export
@@ -130,6 +133,7 @@ mutual
     | NEquivalent Neutral Normal
     | NAssert Neutral
     | NApp Neutral Normal
+    | NList Neutral
     | NBoolAnd Neutral Normal
 
   Show Value where
@@ -142,6 +146,7 @@ mutual
     show (VBoolLit x) = "(VBoolLit" ++ show x ++ ")"
     show VNatural = "VNatural"
     show (VNaturalLit k) = "(VNaturalLit" ++ show k ++ ")"
+    show (VList a) = "(VList" ++ show a ++ ")"
     show (VNeutral x y) = "(VNeutral " ++ show x ++ " " ++ show y ++ ")"
 
   Show Neutral where
@@ -150,6 +155,7 @@ mutual
     show (NEquivalent x y) = "(NEquivalent " ++ show x ++ " " ++ show y ++ ")"
     show (NAssert x) = "(NEquivalent " ++ show x ++ ")"
     show (NApp x y) = "(NApp " ++ show x ++ " " ++ show y ++ ")"
+    show (NList x) = "(NList " ++ show x ++ ")"
     show (NBoolAnd x y) = "(NBoolAnd " ++ show x ++ " " ++ show y ++ ")"
 
 extendEnv : Env -> Name -> Value -> Env
@@ -266,6 +272,9 @@ mutual
          doBoolAnd x' y'
   eval env ENatural = Right VNatural
   eval env (ENaturalLit k) = Right (VNaturalLit k)
+  eval env (EList a) = do
+    a' <- eval env a
+    Right (VList a')
   eval env (ENaturalIsZero x)
     = do x' <- eval env x
          doNaturalIsZero x'
@@ -333,6 +342,9 @@ mutual
   readBackNeutral ctx (NAssert x) = do
     x' <- readBackNeutral ctx x
     Right (EAssert x')
+  readBackNeutral ctx (NList a) = do
+    a' <- readBackNeutral ctx a
+    Right (EList a')
 
   partial
   readBackTyped : Ctx -> Ty -> Value -> Either Error Expr
@@ -364,6 +376,9 @@ mutual
        b' <- evalClosure bT (VNeutral aT (NVar x))
        b <- readBackTyped (extendCtx ctx x aT) (VConst CType) b'
        Right (EPi x a b)
+  readBackTyped ctx (VConst CType) (VList a) = do
+    a' <- readBackTyped ctx (VConst CType) a
+    Right (EList a')
   readBackTyped _ t v = Left (ReadBackError ("error reading back: " ++ (show v) ++ " of type: " ++ (show v)))
 
   export
@@ -525,4 +540,7 @@ mutual
     case aEquiv xRb yRb of -- TODO should eventually use CBOR to check
           False => Left (AssertError ("Not equivalent: " ++ show x ++ " : " ++ show y ++ ")"))
           True => Right (VEquivalent x' y')
+  synth ctx (EList x) = do
+    check ctx x (VConst CType)
+    Right (VConst CType)
   synth ctx (EAssert other) = Left (AssertError ("Can't assert for expr: " ++ show other))
diff --git a/Idrall/Expr.idr b/Idrall/Expr.idr
index 433b6d7..5afe9e1 100644
--- a/Idrall/Expr.idr
+++ b/Idrall/Expr.idr
@@ -55,6 +55,8 @@ data Expr
   | ENaturalLit Nat
   -- | > NaturalIsZero ~ Natural/isZero
   | ENaturalIsZero Expr
+  -- | > EList a ~ List a
+  | EList Expr
 
 export
 Show Expr where
@@ -74,3 +76,4 @@ Show Expr where
   show ENatural = "ENatural"
   show (ENaturalLit k) = "(ENaturalLit " ++ show k ++ ")"
   show (ENaturalIsZero x) = "(ENaturalIsZero " ++ show x ++ ")"
+  show (EList x) = "(EList " ++ show x ++ ")"
diff --git a/Idrall/Parser.idr b/Idrall/Parser.idr
index 127c055..c57a913 100644
--- a/Idrall/Parser.idr
+++ b/Idrall/Parser.idr
@@ -9,9 +9,14 @@ import Idrall.BuildExprParser
 fNaturalIsZero : Expr
 fNaturalIsZero = ELam "naturalIsZeroParam1" ENatural (ENaturalIsZero (EVar "naturalIsZeroParam1"))
 
+fList : Expr
+fList = ELam "listArg1" (EConst CType) (EList (EVar "listArg1"))
+
 %access export
 builtin : Parser Expr
-builtin = string "Natural/isZero" *> pure fNaturalIsZero
+builtin =
+  (string "Natural/isZero" *> pure fNaturalIsZero) <|>
+  (string "List" *> pure fList)
 
 true : Parser Expr
 true = token "True" *> pure (EBoolLit True)
diff --git a/tests/Test.idr b/tests/Test.idr
index 436a4a2..47a5357 100644
--- a/tests/Test.idr
+++ b/tests/Test.idr
@@ -79,7 +79,7 @@ testAll = do
       putStrLn "done"
 
 expectPass : List String
-expectPass = ["AssertTrivial", "Bool", "Function", "Natural", "True", "NaturalIsZero", "NaturalLiteral", "Let", "FunctionTypeTermTerm", "FunctionApplication", "Equivalence", "FunctionDependentType1"]
+expectPass = ["AssertTrivial", "Bool", "Function", "Natural", "True", "NaturalIsZero", "NaturalLiteral", "Let", "FunctionTypeTermTerm", "FunctionApplication", "Equivalence", "FunctionDependentType1", "List"]
 
 testGood : IO ()
 testGood