From 39a5c25fbcc65d91b6e65f7d6f5489d8586c8ee9 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Fri, 2 Aug 2019 17:59:17 +0200 Subject: [PATCH] remove ide socket mode test because it's hard to make reliable --- tests/ideMode/ideMode002/Empty.idr | 1 - tests/ideMode/ideMode002/Vect.idr | 34 ------------------------------ tests/ideMode/ideMode002/expected | 3 --- tests/ideMode/ideMode002/input | 1 - tests/ideMode/ideMode002/run | 7 ------ 5 files changed, 46 deletions(-) delete mode 100644 tests/ideMode/ideMode002/Empty.idr delete mode 100644 tests/ideMode/ideMode002/Vect.idr delete mode 100644 tests/ideMode/ideMode002/expected delete mode 100644 tests/ideMode/ideMode002/input delete mode 100755 tests/ideMode/ideMode002/run diff --git a/tests/ideMode/ideMode002/Empty.idr b/tests/ideMode/ideMode002/Empty.idr deleted file mode 100644 index b052a4c..0000000 --- a/tests/ideMode/ideMode002/Empty.idr +++ /dev/null @@ -1 +0,0 @@ -module Empty diff --git a/tests/ideMode/ideMode002/Vect.idr b/tests/ideMode/ideMode002/Vect.idr deleted file mode 100644 index 300ac93..0000000 --- a/tests/ideMode/ideMode002/Vect.idr +++ /dev/null @@ -1,34 +0,0 @@ -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) diff --git a/tests/ideMode/ideMode002/expected b/tests/ideMode/ideMode002/expected deleted file mode 100644 index 0499bc6..0000000 --- a/tests/ideMode/ideMode002/expected +++ /dev/null @@ -1,3 +0,0 @@ -000018(:protocol-version 2 0) -000032(:write-string "1/1: Building Vect (Vect.idr)" 1) -000027(:return (:ok "Loaded Vect.idr" ()) 1) diff --git a/tests/ideMode/ideMode002/input b/tests/ideMode/ideMode002/input deleted file mode 100644 index fe64178..0000000 --- a/tests/ideMode/ideMode002/input +++ /dev/null @@ -1 +0,0 @@ -00001b((:load-file "Vect.idr") 1) diff --git a/tests/ideMode/ideMode002/run b/tests/ideMode/ideMode002/run deleted file mode 100755 index af96f74..0000000 --- a/tests/ideMode/ideMode002/run +++ /dev/null @@ -1,7 +0,0 @@ -$1 --no-prelude --ide-mode-socket 0.0.0.0:34567 Empty.idr > /dev/null & -sleep 2 - -nc -G 5 127.0.0.1 34567 < input - -kill %1 -rm -rf build