(hopefully) fix ide-mode-socket test

for some reason running idris2 _without_ an input file fails which
throws this test in a spin. We start the interpreter in ide mode on a
socket loading an empty module without prelude and then request
loading a file that does not require Prelude.

tests/ideMode/ideMode002/Empty.idr

@@ -0,0 +1 @@
+module Empty

tests/ideMode/ideMode002/LocType.idr

@@ -1,7 +0,0 @@
-data Vect : Nat -> Type -> Type where
-     Nil : Vect Z a
-     (::) : a -> Vect k a -> Vect (S k) a
-
-append : Vect n a -> Vect m a -> Vect (n + m) a
-append [] ys = ys
-append (x :: xs) ys = x :: append xs ys

tests/ideMode/ideMode002/Vect.idr

@@ -0,0 +1,34 @@
+data Nat = Z | S Nat
+
+plus : Nat -> Nat -> Nat
+plus Z     y = y
+plus (S k) y = S (plus k y)
+
+data Vect : Nat -> Type -> Type where
+     Nil  : Vect Z a
+     Cons : a -> Vect k a -> Vect (S k) a
+
+foldl : (0 b : Nat -> Type) ->
+        ({k : Nat} -> b k -> a -> b (S k)) ->
+        b Z ->
+        Vect n a -> b n
+foldl b g z Nil = z
+foldl b g z (Cons x xs) = foldl (\i => b (S i)) g (g z x) xs
+
+reverse : Vect n a -> Vect n a
+reverse
+    = foldl (\m => Vect m a)
+            (\rev => \x => Cons x rev) Nil
+
+append : Vect n a -> Vect m a -> Vect (plus n m) a
+append Nil ys = ys
+append (Cons x xs) ys = Cons x (append xs ys)
+
+vlength : (n : Nat) -> Vect n a -> Nat
+vlength Z Nil = Z
+vlength n@_ (Cons x xs) = n -- (vlength _ xs);
+
+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
+zipWith f Nil Nil = Nil
+-- zipWith f (Cons x xs) Nil impossible
+zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)

tests/ideMode/ideMode002/expected

@@ -1,3 +1,3 @@
 000018(:protocol-version 2 0)
-000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
-00002a(:return (:ok "Loaded LocType.idr" ()) 1)
+000032(:write-string "1/1: Building Vect (Vect.idr)" 1)
+000027(:return (:ok "Loaded Vect.idr" ()) 1)

tests/ideMode/ideMode002/input

@@ -1 +1 @@
-00001e((:load-file "LocType.idr") 1)
+00001b((:load-file "Vect.idr") 1)

tests/ideMode/ideMode002/run

@@ -1,6 +1,7 @@
-$1 --ide-mode-socket 0.0.0.0:34567 > /dev/null &
+$1 --no-prelude --ide-mode-socket 0.0.0.0:34567 Empty.idr > /dev/null &
 sleep 2
-nc localhost 34567 < input
+
+nc -G 5 127.0.0.1 34567 < input
 
 kill %1
 rm -rf build