git.iko.soy/Idris-dev
on master help sign in
Add tests for interactively adding a missing clause
b9bad2dMatthias Heinzel
test/TestData.hs+3−1
compare with master
unifiedsplit
@@ -155,7 +155,9 @@ testFamiliesData = [
155 ( 11, ANY ),
155 ( 11, ANY ),
156 ( 12, ANY ),
156 ( 12, ANY ),
157 ( 13, ANY ),
157 ( 13, ANY ),
158− ( 14, C_CG )]),
158+ ( 14, C_CG ),
159+ ( 15, ANY ),
160+ ( 16, ANY )]),
159 ("interfaces", "Interfaces",
161 ("interfaces", "Interfaces",
160 [ ( 1, ANY ),
162 [ ( 1, ANY ),
161 ( 2, ANY ),
163 ( 2, ANY ),
test/interactive015/expectednew file+6
@@ -0,0 +1,6 @@
1+test (Just x) = ?Nothing_rhs_1
2+
3+test : Maybe a -> Bool
4+test Nothing = False
5+test (Just x) = ?Nothing_rhs_1
6+
test/interactive015/inputnew file+2
@@ -0,0 +1,2 @@
1+:addmissing 3 Nothing
2+:addmissing! 3 Nothing
test/interactive015/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+cp src/interactive015.idr .
4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input
5+
6+cat interactive015.idr
7+
8+rm -f *.ibc interactive015.idr
test/interactive015/src/interactive015.idrnew file+4
@@ -0,0 +1,4 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+
test/interactive016/expectednew file+7
@@ -0,0 +1,7 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+test (Just x) = True
5+
6+other : Int
7+other = 3
test/interactive016/inputnew file+2
@@ -0,0 +1,2 @@
1+:addmissing 3 Nothing
2+:addmissing! 3 Nothing
test/interactive016/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+cp src/interactive016.idr .
4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input
5+
6+cat interactive016.idr
7+
8+rm -f *.ibc interactive016.idr
test/interactive016/src/interactive016.idrnew file+7
@@ -0,0 +1,7 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+test (Just x) = True
5+
6+other : Int
7+other = 3