tests everywhere

src/Compiler/ES/ES.idr

@@ -20,14 +20,14 @@ addConstToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String
 addConstToPreamble name def =
   do
     s <- get ESs
+    let v = "const " ++ esName name ++ " = (" ++ def ++ ")"
     case lookup name (preamble s) of
       Nothing =>
         do
-          let v = "const " ++ esName name ++ " = (" ++ def ++ ")"
           put ESs (record { preamble = insert name v (preamble s) } s)
           pure $ esName name
       Just x =>
-        if x /= def then throw $ InternalError $ "two incompatible definitions for " ++ name
+        if x /= v then throw $ InternalError $ "two incompatible definitions for " ++ name ++ "<|" ++ x ++"|> <|"++ v ++ "|>"
                     else pure $ esName name
 
 
@@ -104,7 +104,7 @@ boundedIntOp bits o lhs rhs = boundedInt 63 (binOp o lhs rhs)
 
 
 boolOp : String -> String -> String -> String
-boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? 1 : 0)"
+boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? BigInt(1) : BigInt(0))"
 
 jsConstant : {auto c : Ref ESs ESSt} -> Constant -> Core String
 jsConstant (I i) = pure $ toBigInt $ show i

src/Compiler/ES/Imperative.idr

@@ -9,6 +9,10 @@ import Compiler.CompileExpr
 import public Core.Context
 import public Core.TT
 
+import Compiler.ES.RemoveUnused
+
+import Debug.Trace
+
 mutual
   public export
   data ImperativeExp = IEVar Name
@@ -272,6 +276,6 @@ compileToImperative c tm =
     let ndefs = namedDefs cdata
     let ctm = forget (mainExpr cdata)
     s <- newRef Imps (MkImpSt 0)
-    compdefs <- traverse getImp ndefs
+    compdefs <- traverse getImp (defsUsedByNamedCExp ctm ndefs)
     (s, main) <- impExp ctm
     pure $ concat compdefs <+> s <+> EvalExpStatement main

src/Compiler/ES/Node.idr

@@ -30,7 +30,8 @@ compileExpr : Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr c execDir tm outfile
     = do es <- compileToNode c tm
-         coreLift (writeFile outfile es)
+         Right () <- coreLift (writeFile outfile es)
+            | Left err => throw (FileErr outfile err)
          pure (Just outfile)
 
 ||| Node implementation of the `executeExpr` interface.

src/Compiler/ES/RemoveUnused.idr

@@ -0,0 +1,66 @@
+module Compiler.ES.RemoveUnused
+
+import Data.SortedSet
+import Data.SortedMap
+import Data.Vect
+import Data.List
+
+import Core.CompileExpr
+import Core.Name
+import Core.FC
+
+import Debug.Trace
+
+mutual
+  usedNames : NamedCExp -> SortedSet Name
+  usedNames (NmLocal fc n) = empty
+  usedNames (NmRef fc n) = insert n empty
+  usedNames (NmLam fc n e) = usedNames e
+  usedNames (NmApp fc x args) = usedNames x `union` concat (usedNames <$> args)
+  usedNames (NmPrimVal fc c) = empty
+  usedNames (NmOp fc op args) = concat $ usedNames <$> args
+  usedNames (NmConCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConAlt <$> alts)) `union` maybe empty usedNames def
+  usedNames (NmConstCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConstAlt <$> alts)) `union` maybe empty usedNames def
+  usedNames (NmExtPrim fc p args) = concat $ usedNames <$> args
+  usedNames (NmCon fc x t args) = concat $ usedNames <$> args
+  usedNames (NmDelay fc t) = usedNames t
+  usedNames (NmForce fc t) = usedNames t
+  usedNames (NmLet fc x val sc) = usedNames val `union` usedNames sc
+  usedNames (NmErased fc) = empty
+  usedNames (NmCrash fc msg) = empty
+
+  usedNamesConAlt : NamedConAlt -> SortedSet Name
+  usedNamesConAlt (MkNConAlt n t args exp) = usedNames exp
+
+  usedNamesConstAlt : NamedConstAlt -> SortedSet Name
+  usedNamesConstAlt (MkNConstAlt c exp) = usedNames exp
+
+usedNamesDef : NamedDef -> SortedSet Name
+usedNamesDef (MkNmFun args exp) = usedNames exp
+usedNamesDef (MkNmError exp) = usedNames exp
+usedNamesDef (MkNmForeign cs args ret) = empty
+usedNamesDef (MkNmCon _ _ _) = empty
+
+defsToUsedMap : List (Name, FC, NamedDef) -> SortedMap Name (SortedSet Name)
+defsToUsedMap defs =
+  fromList $ (\(n,_,d)=> (n, usedNamesDef d)) <$> defs
+
+calcUsed : SortedSet Name -> SortedMap Name (SortedSet Name) -> List Name -> SortedSet Name
+calcUsed done d [] = done
+calcUsed done d xs =
+  let used_in_xs = foldl f empty $ (\z => lookup z d) <$> xs
+      new_done   = union done (fromList xs)
+  in calcUsed (new_done) d (SortedSet.toList $ difference used_in_xs new_done)
+  where
+    f : SortedSet Name -> Maybe (SortedSet Name) -> SortedSet Name
+    f x Nothing = x
+    f x (Just y) = union x y
+
+calcUsedDefs : List Name -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef)
+calcUsedDefs names defs =
+  let usedNames = calcUsed empty (defsToUsedMap defs) names
+  in List.filter (\(n, fc, d) => contains n usedNames) defs
+
+export
+defsUsedByNamedCExp : NamedCExp -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef)
+defsUsedByNamedCExp exp defs = calcUsedDefs (SortedSet.toList $ usedNames exp) defs

tests/Main.idr

@@ -117,7 +117,11 @@ chezTests
 
 nodeTests : List String
 nodeTests
-  = ["node001"]
+  = [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
+    , "node011", "node012", "node013", "node014", "node015", "node017", "node018", "node019"
+    , "node020", "node021"
+    , "reg001"
+    ]
 
 ideModeTests : List String
 ideModeTests

tests/node/node002/Pythag.idr

@@ -0,0 +1,9 @@
+range : Integer -> Integer -> List Integer
+range bottom top
+    = if bottom > top then []
+         else bottom :: range (bottom + 1) top
+
+pythag : Integer -> List (Integer, Integer, Integer)
+pythag top
+   = [(x, y, z) | z <- range 1 top, y <- range 1 z, x <- range 1 y,
+                  x * x + y * y == z * z]

tests/node/node002/expected

@@ -0,0 +1,3 @@
+[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
+1/1: Building Pythag (Pythag.idr)
+Main> Main> Bye for now!

tests/node/node002/input

@@ -0,0 +1,2 @@
+:exec printLn (pythag 200)
+:q

tests/node/node002/run

@@ -0,0 +1,2 @@
+$1 --cg node --no-banner Pythag.idr < input
+rm -rf build

tests/node/node003/IORef.idr

@@ -0,0 +1,16 @@
+import Data.IORef
+
+main : IO ()
+main
+    = do x <- newIORef 42
+         let y = x
+         writeIORef y 94
+         val <- readIORef x
+         printLn val
+         val <- readIORef y
+         printLn val
+         modifyIORef x (* 2)
+         val <- readIORef x
+         printLn val
+         val <- readIORef y
+         printLn val

tests/node/node003/expected

@@ -0,0 +1,6 @@
+94
+94
+188
+188
+1/1: Building IORef (IORef.idr)
+Main> Main> Bye for now!

tests/node/node003/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node003/run

@@ -0,0 +1,2 @@
+$1 --cg node --no-banner IORef.idr < input
+rm -rf build

tests/node/node004/Buffer.idr

@@ -0,0 +1,54 @@
+import Data.Buffer
+import System.File
+
+main : IO ()
+main
+    = do Just buf <- newBuffer 100
+              | Nothing => putStrLn "Buffer creation failed"
+         s <- rawSize buf
+         printLn s
+
+         setInt32 buf 1 94
+         setString buf 5 "AAAA"
+         val <- getInt32 buf 1
+         printLn val
+
+         setDouble buf 10 94.42
+         val <- getDouble buf 10
+         printLn val
+
+         setString buf 20 "Hello there!"
+         val <- getString buf 20 5
+         printLn val
+
+         val <- getString buf 26 6
+         printLn val
+
+         setBits16 buf 32 65535
+         val <- getBits16 buf 32
+         printLn val
+
+         ds <- bufferData buf
+         printLn ds
+
+         Right _ <- writeBufferToFile "test.buf" buf 100
+             | Left err => putStrLn "Buffer write fail"
+         Right buf2 <- createBufferFromFile "test.buf"
+             | Left err => putStrLn "Buffer read fail"
+
+         ds <- bufferData buf2
+         printLn ds
+
+         freeBuffer buf
+         freeBuffer buf2
+
+-- Put back when the File API is moved to C and these can work again
+--          Right f <- openBinaryFile "test.buf" Read
+--              | Left err => putStrLn "File error on read"
+--          Just buf3 <- newBuffer 99
+--               | Nothing => putStrLn "Buffer creation failed"
+--          Right _ <- readBufferFromFile f buf3 100
+--              | Left err => do putStrLn "Buffer read fail"
+--                               closeFile f
+--          closeFile f
+

tests/node/node004/expected

@@ -0,0 +1,10 @@
+100
+94
+94.42
+"Hello"
+"there!"
+65535
+[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+1/1: Building Buffer (Buffer.idr)
+Main> Main> Bye for now!

tests/node/node004/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node004/run

@@ -0,0 +1,2 @@
+$1 --cg node --no-banner Buffer.idr < input
+rm -rf build test.buf

tests/node/node005/Filter.idr

@@ -0,0 +1,29 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+Show a => Show (Vect n a) where
+  show xs = "[" ++ showV xs ++ "]"
+    where
+      showV : forall n . Vect n a -> String
+      showV [] = ""
+      showV [x] = show x
+      showV (x :: xs) = show x ++ ", " ++ showV xs
+
+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
+filter pred [] = (_ ** [])
+filter pred (x :: xs)
+    = let (n ** xs') = filter pred xs in
+          if pred x
+             then (_ ** x :: xs')
+             else (_ ** xs')
+
+test : (x ** Vect x Nat)
+test = (_ ** [1,2])
+
+foo : String
+foo = show test
+
+even : Nat -> Bool
+even Z = True
+even (S k) = not (even k)

tests/node/node005/expected

@@ -0,0 +1,3 @@
+(3 ** [2, 4, 6])
+1/1: Building Filter (Filter.idr)
+Main> Main> Bye for now!

tests/node/node005/input

@@ -0,0 +1,2 @@
+:exec printLn (filter even [S Z,2,3,4,5,6])
+:q

tests/node/node005/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner Filter.idr < input
+
+rm -rf build

tests/node/node006/TypeCase.idr

@@ -0,0 +1,32 @@
+data Bar = MkBar
+data Baz = MkBaz
+
+foo : (x : Type) -> String
+foo Nat = "Nat"
+foo Bool = "Bool"
+foo (List x) = "List of " ++ foo x
+foo Int = "Int"
+foo Type = "Type"
+foo _ = "Something else"
+
+strangeId : {a : Type} -> a -> a
+strangeId {a=Integer} x = x+1
+strangeId x = x
+
+partial
+strangeId' : {a : Type} -> a -> a
+strangeId' {a=Integer} x = x+1
+
+main : IO ()
+main = do printLn (foo Nat)
+          printLn (foo (List Nat))
+          printLn (foo (List Bar))
+          printLn (foo (List Baz))
+          printLn (foo (List Bool))
+          printLn (foo Int)
+          printLn (foo String)
+          printLn (foo (List Type))
+          printLn (foo (List Int))
+          printLn (strangeId 42)
+          printLn (strangeId (the Int 42))
+

tests/node/node006/TypeCase2.idr

@@ -0,0 +1,14 @@
+data Bar = MkBar
+data Baz = MkBaz
+
+strangeId : a -> a
+strangeId {a=Nat} x = x+1
+strangeId x = x
+
+foo : (0 x : Type) -> String
+foo Nat = "Nat"
+foo Bool = "Bool"
+foo (List x) = "List of " ++ foo x
+foo Int = "Int"
+foo Type = "Type"
+foo _ = "Something else"

tests/node/node006/expected

@@ -0,0 +1,21 @@
+"Nat"
+"List of Nat"
+"List of Something else"
+"List of Something else"
+"List of Bool"
+"Int"
+"Something else"
+"List of Type"
+"List of Int"
+43
+42
+1/1: Building TypeCase (TypeCase.idr)
+Main> Main> Main.strangeId is total
+Main> Main.strangeId':
+strangeId' _
+Main> Bye for now!
+1/1: Building TypeCase2 (TypeCase2.idr)
+TypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:
+Can't match on Nat (Erased argument)
+TypeCase2.idr:9:5--9:9:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:
+Can't match on Nat (Erased argument)

tests/node/node006/input

@@ -0,0 +1,4 @@
+:exec main
+:total strangeId
+:missing strangeId'
+:q

tests/node/node006/run

@@ -0,0 +1,4 @@
+$1 --cg node --no-banner TypeCase.idr < input
+$1 --cg node --no-banner TypeCase2.idr --check
+
+rm -rf build

tests/node/node007/TypeCase.idr

@@ -0,0 +1,26 @@
+data Bar = MkBar
+data Baz = MkBaz
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+desc : Type -> String
+desc Int = "Int"
+desc Nat = "Nat"
+desc (Vect n a) = "Vector of " ++ show n ++ " " ++ desc a
+desc Type = "Type"
+desc _ = "Something else"
+
+descNat : Type -> String
+descNat t = "Function from Nat to " ++ desc t
+
+descFn : (x : Type) -> String
+descFn ((x : Nat) -> b) = descNat (b Z)
+descFn (a -> b) = "Function on " ++ desc a
+descFn x = desc x
+
+main : IO ()
+main = do printLn (descFn (Nat -> Nat))
+          printLn (descFn ((x : Nat) -> Vect x Int))
+          printLn (descFn (Type -> Int))

tests/node/node007/expected

@@ -0,0 +1,5 @@
+"Function from Nat to Nat"
+"Function from Nat to Vector of 0 Int"
+"Function on Type"
+1/1: Building TypeCase (TypeCase.idr)
+Main> Main> Bye for now!

tests/node/node007/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node007/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner TypeCase.idr < input
+
+rm -rf build

tests/node/node008/Nat.idr

@@ -0,0 +1,11 @@
+myS : Nat -> Nat
+myS n = S n
+
+myS_crash : Nat -> Nat
+myS_crash = S
+
+main : IO ()
+main = do
+  printLn (S Z)
+  printLn (myS Z)
+  printLn (myS_crash Z)

tests/node/node008/expected

@@ -0,0 +1,5 @@
+1
+1
+1
+1/1: Building Nat (Nat.idr)
+Main> Main> Bye for now!

tests/node/node008/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node008/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner Nat.idr < input
+
+rm -rf build

tests/node/node009/expected

@@ -0,0 +1,4 @@
+42
+ällo
+1/1: Building uni (uni.idr)
+Main> Main> Bye for now!

tests/node/node009/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node009/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner uni.idr < input
+
+rm -rf build

tests/node/node009/uni.idr

@@ -0,0 +1,9 @@
+foo : String
+foo = "ällo"
+
+ällo : Int
+ällo = 42
+
+main : IO ()
+main = do printLn ällo
+          putStrLn "ällo"

tests/node/node011/bangs.idr

@@ -0,0 +1,32 @@
+
+add : Int -> Int -> Int
+add = (+)
+
+-- lift to nearest binder
+addm1 : Maybe Int -> Maybe Int -> Maybe Int
+addm1 x y = let z = x in pure (add !z !y)
+
+-- lift to nearest binder
+addm2 : Maybe Int -> Maybe Int -> Maybe Int
+addm2 = \x, y => pure (!x + !y)
+
+getLen : String -> IO Nat
+getLen str = pure (length str)
+
+fakeGetLine : String -> IO String
+fakeGetLine str = pure str
+
+-- lift out innermost first
+printThing1 : IO ()
+printThing1 = printLn !(getLen !(fakeGetLine "line1"))
+
+-- lift out leftmost first
+printThing2 : IO ()
+printThing2 = printLn (!(fakeGetLine "1") ++ !(fakeGetLine "2"))
+
+-- don't lift out of if
+printBool : Bool -> IO ()
+printBool x
+    = if x
+         then putStrLn !(fakeGetLine "True")
+         else putStrLn !(fakeGetLine "False")

tests/node/node011/expected

@@ -0,0 +1,8 @@
+5
+"12"
+True
+False
+1/1: Building bangs (bangs.idr)
+Main> Just 7
+Main> Just 7
+Main> Main> Main> Main> Main> Bye for now!

tests/node/node011/input

@@ -0,0 +1,7 @@
+addm1 (Just 3) (Just 4)
+addm2 (Just 3) (Just 4)
+:exec printThing1
+:exec printThing2
+:exec printBool True
+:exec printBool False
+:q

tests/node/node011/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner bangs.idr < input
+
+rm -rf build

tests/node/node012/array.idr

@@ -0,0 +1,11 @@
+import Data.IOArray
+
+main : IO ()
+main
+    = do x <- newArray 20
+         writeArray x 10 "Hello"
+         writeArray x 11 "World"
+         printLn !(toList x)
+
+         y <- fromList (map Just [1,2,3,4,5])
+         printLn !(toList y)

tests/node/node012/expected

@@ -0,0 +1,4 @@
+[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
+[Just 1, Just 2, Just 3, Just 4, Just 5]
+1/1: Building array (array.idr)
+Main> Main> Bye for now!

tests/node/node012/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node012/run

@@ -0,0 +1,2 @@
+$1 --cg node --no-banner array.idr < input
+rm -rf build

tests/node/node014/Echo.idr

@@ -0,0 +1,57 @@
+module Main
+
+import System
+import System.Info
+import Network.Socket
+import Network.Socket.Data
+import Network.Socket.Raw
+
+runServer : IO (Either String (Port, ThreadID))
+runServer = do
+  Right sock <- socket AF_INET Stream 0
+        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
+  res <- bind sock (Just (Hostname "localhost")) 0
+  if res /= 0
+    then pure (Left $ "Failed to bind socket with error: " ++ show res)
+    else do
+      port <- getSockPort sock
+      res <- listen sock
+      if res /= 0
+        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
+        else do
+          forked <- fork (serve port sock)
+          pure $ Right (port, forked)
+
+  where
+    serve : Port -> Socket -> IO ()
+    serve port sock = do
+      Right (s, _) <- accept sock
+        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
+      Right  (str, _) <- recv s 1024
+        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
+      putStrLn ("Received: " ++ str)
+      Right n <- send s ("echo: " ++ str)
+        | Left err => putStrLn ("Server failed to send data with error: " ++ show err)
+      pure ()
+
+runClient : Port -> IO ()
+runClient serverPort = do
+  Right sock <- socket AF_INET Stream 0
+    | Left fail => putStrLn ("Failed to open socket: " ++ show fail)
+  res <- connect sock (Hostname "localhost") serverPort
+  if res /= 0
+    then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
+    else do
+      Right n <- send sock ("hello world!")
+        | Left err => putStrLn ("Client failed to send data with error: " ++ show err)
+      Right (str, _) <- recv sock 1024
+        | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
+      -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
+      -- to be printed after the server prints its own message
+      putStrLn ("Received: " ++ str)
+
+main : IO ()
+main = do
+  Right (serverPort, tid) <- runServer
+    | Left err => putStrLn $ "[server] " ++ err
+  runClient serverPort

tests/node/node014/expected

@@ -0,0 +1,4 @@
+Received: hello world!
+Received: echo: hello world!
+1/1: Building Echo (Echo.idr)
+Main> Main> Bye for now!

tests/node/node014/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node014/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner -p network Echo.idr < input
+
+rm -rf build

tests/node/node015/Numbers.idr

@@ -0,0 +1,36 @@
+module Main
+
+import Data.List
+
+%default partial
+
+large : (a: Type) -> a
+-- integer larger than 64 bits
+large Integer = 3518437212345678901234567890123
+-- int close to 2ˆ63
+-- we expect some operations will overflow
+large Int = 3518437212345678901234567890
+
+small : (a: Type) -> a
+small Integer = 437
+small Int = 377
+
+numOps : (Num a) => List ( a -> a -> a )
+numOps = [ (+), (*) ]
+
+negOps : (Neg a) => List (a -> a -> a)
+negOps = [ (-) ]
+
+integralOps : (Integral a) => List (a -> a -> a)
+integralOps = [ div, mod ]
+
+binOps : (Num a, Neg a, Integral a) => List (a -> a -> a)
+binOps = numOps ++ negOps ++ integralOps
+
+main : IO ()
+main = do
+  putStrLn $ show (results Integer)
+  putStrLn $ show (results Int)
+  where
+  results : (a:Type) -> (Num a, Neg a, Integral a) => List a
+  results a = map (\ op => large a  `op` small a) binOps

tests/node/node015/expected

@@ -0,0 +1,4 @@
+[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]
+[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
+1/1: Building Numbers (Numbers.idr)
+Main> Main> Bye for now!

tests/node/node015/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node015/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner Numbers.idr < input
+
+rm -rf build

tests/node/node017/.gitignore

@@ -0,0 +1,2 @@
+/expected
+

tests/node/node017/dir.idr

@@ -0,0 +1,15 @@
+import System.Directory
+
+main : IO ()
+main = do Right () <- createDir "testdir"
+               | Left err => printLn err
+          Left err <- createDir "testdir"
+               | _ => printLn "That wasn't supposed to work"
+          printLn err
+          ok <- changeDir "nosuchdir"
+          printLn ok
+          ok <- changeDir "testdir"
+          printLn ok
+          writeFile "test.txt" "hello\n"
+          printLn !currentDir
+

tests/node/node017/expected.in

@@ -0,0 +1,7 @@
+File Exists
+False
+True
+Just "__PWD__testdir"
+1/1: Building dir (dir.idr)
+Main> Main> Bye for now!
+hello

tests/node/node017/gen_expected.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env sh
+if [ $OS = "windows" ]; then
+    MY_PWD="$(cygpath -m $(pwd))\\\\" 
+else
+    MY_PWD=$(pwd)/
+fi
+
+sed -e "s|__PWD__|${MY_PWD}|g" expected.in > expected

tests/node/node017/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node017/run

@@ -0,0 +1,4 @@
+./gen_expected.sh
+$1 --cg node --no-banner dir.idr < input
+cat testdir/test.txt
+rm -rf build testdir

tests/node/node018/File.idr

@@ -0,0 +1,14 @@
+import System.File
+
+main : IO ()
+main
+    = do Right ok <- readFile "test.txt"
+               | Left err => printLn err
+         putStr ok
+         writeFile "testout.txt" "abc\ndef\n"
+         Right ok <- readFile "testout.txt"
+               | Left err => printLn err
+         putStr ok
+         Right ok <- readFile "notfound"
+               | Left err => printLn err
+         putStr ok

tests/node/node018/expected

@@ -0,0 +1,6 @@
+test test
+unfinished lineabc
+def
+File Not Found
+1/1: Building File (File.idr)
+Main> Main> Bye for now!

tests/node/node018/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node018/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner File.idr < input
+
+rm -rf build testout.txt

tests/node/node018/test.txt

@@ -0,0 +1,2 @@
+test test
+unfinished line

tests/node/node019/expected

@@ -0,0 +1,6 @@
+ERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1
+2
+ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1
+ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1
+1/1: Building partial (partial.idr)
+Main> Main> Main> Main> Main> Bye for now!

tests/node/node019/input

@@ -0,0 +1,5 @@
+:exec main
+:exec printLn $ lookup (FS FZ) [1,2,3,4]
+:exec printLn $ lookup' (FS FZ) [1,2,3,4]
+:exec printLn $ lookup'' (FS FZ) [1,2,3,4]
+:q

tests/node/node019/partial.idr

@@ -0,0 +1,26 @@
+%default partial
+
+foo : Maybe a -> a
+foo (Just x) = x
+
+data Vect : ? -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+data Fin : Nat -> Type where
+     FZ : Fin (S k)
+     FS : Fin k -> Fin (S k)
+
+lookup : Fin n -> Vect n a -> a
+lookup FZ (x :: xs) = x
+lookup (FS k) (x :: xs) = lookup k xs
+
+lookup' : Fin n -> Vect n a -> a
+lookup' (FS k) (x :: xs) = lookup' k xs
+
+lookup'' : Fin n -> Vect n a -> a
+lookup'' n xs = lookup' n xs
+
+main : IO ()
+main = do let x = foo Nothing
+          printLn (the Int x)

tests/node/node019/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner partial.idr < input
+
+rm -rf build testout.txt

tests/node/node020/Popen.idr

@@ -0,0 +1,29 @@
+import System
+import System.File
+import System.Info
+import Data.Strings
+
+windowsPath : String -> String
+windowsPath path =
+    let replaceSlashes : List Char -> List Char
+        replaceSlashes [] = []
+        replaceSlashes ('/' :: cs) = '\\' :: replaceSlashes cs
+        replaceSlashes (c :: cs) = c :: replaceSlashes cs
+    in
+        pack $ replaceSlashes (unpack path)
+
+main : IO ()
+main = do
+    Just cmd <- getEnv "POPEN_CMD"
+        | Nothing => putStrLn "POPEN_CMD env var not set"
+    let cmd = if isWindows then windowsPath cmd else cmd
+    Right fh <- popen cmd Read
+        | Left err => printLn err
+    putStrLn "opened"
+    Right output <- fGetLine fh
+        | Left err => printLn err
+    pclose fh
+    putStrLn "closed"
+    let [idris2, _] = split ((==) ',') output
+        | _ => printLn "Unexpected result"
+    putStrLn idris2

tests/node/node020/expected

@@ -0,0 +1,5 @@
+opened
+closed
+Idris 2
+1/1: Building Popen (Popen.idr)
+Main> Main> Bye for now!

tests/node/node020/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/node020/run

@@ -0,0 +1,3 @@
+POPEN_CMD="$1 --version" $1 --cg node --no-banner Popen.idr < input
+
+rm -rf build

tests/node/node021/Bits.idr

@@ -0,0 +1,43 @@
+t1 : Bits8
+t1 = 2
+
+t2 : Bits8
+t2 = 255
+
+t3 : Bits8
+t3 = 100
+
+tests8 : List String
+tests8 = map show [t1 + t2,
+                   t1 * t3,
+                   the Bits8 (fromInteger (-8)),
+                   the Bits8 257,
+                   the Bits8 (fromInteger (-1)),
+                   prim__shl_Bits8 t3 1,
+                   prim__shl_Bits8 t2 1]
+
+testsCmp : List String
+testsCmp = map show [t1 < t2, t3 < (t2 + t1)]
+
+testsMax : List String
+testsMax = [show (the Bits8 (fromInteger (-1))),
+            show (the Bits16 (fromInteger (-1))),
+            show (the Bits32 (fromInteger (-1))),
+            show (the Bits64 (fromInteger (-1)))]
+
+main : IO ()
+main
+    = do printLn (t1 + t2)
+         printLn (t1 * t3)
+         printLn (t1 < t2)
+         printLn (prim__shl_Bits8 t3 1)
+         printLn (prim__shl_Bits8 t2 1)
+         printLn (t3 < (t2 + t1))
+         printLn (the Bits8 (fromInteger (-8)))
+         printLn (the Bits8 257)
+         printLn (the Bits64 1234567890)
+         printLn (the Bits8 (fromInteger (-1)))
+         printLn (the Bits16 (fromInteger (-1)))
+         printLn (the Bits32 (fromInteger (-1)))
+         printLn (the Bits64 (fromInteger (-1)))
+

tests/node/node021/expected

@@ -0,0 +1,18 @@
+1
+200
+True
+200
+254
+False
+248
+1
+1234567890
+255
+65535
+4294967295
+18446744073709551615
+1/1: Building Bits (Bits.idr)
+Main> ["257", "200", "248", "1", "255", "200", "254"]
+Main> ["True", "True"]
+Main> ["255", "65535", "4294967295", "18446744073709551615"]
+Main> Main> Bye for now!

tests/node/node021/input

@@ -0,0 +1,5 @@
+tests8
+testsCmp
+testsMax
+:exec main
+:q

tests/node/node021/run

@@ -0,0 +1,3 @@
+$1 --cg node --no-banner Bits.idr < input
+
+rm -rf build

tests/node/reg001/expected

@@ -0,0 +1,10 @@
+3
+4.2
+"1.2"
+4
+1
+"2.7"
+5.9
+2
+2
+2

tests/node/reg001/numbers.idr

@@ -0,0 +1,21 @@
+-- the commented-out cases are still wrong,
+-- but fixing them as well would make other tests fail for mysterious reasons
+-- see https://github.com/edwinb/Idris2/pull/281
+main : IO ()
+main = do
+  printLn $ 3
+  printLn $ 4.2
+  printLn $ "1.2"
+
+  printLn $ cast {to = Int} 4.8
+  printLn $ cast {to = Integer} 1.2
+  printLn $ cast {to = String} 2.7
+
+  -- printLn $ cast {to = Int} "1.2"
+  -- printLn $ cast {to = Integer} "2.7"
+  printLn $ cast {to = Double} "5.9"
+
+  printLn $ (the Int 6 `div` the Int 3)
+  printLn $ (the Integer 6 `div` the Integer 3)
+  printLn $ (cast {to = Int} "6.6" `div` cast "3.9")
+  -- printLn $ (cast {to = Integer} "6.6" `div` cast "3.9")

tests/node/reg001/run

@@ -0,0 +1,3 @@
+$1 --cg node numbers.idr -x main
+
+rm -rf build