git.iko.soy/Idris-dev
on master help sign in
Removed semicolons from tests
ead54e4Edwin Brady
test/test002/test002.idr+10−10
compare with master
unifiedsplit
@@ -1,17 +1,17 @@
1−myid : a -> a;
1+myid : a -> a
2−myid x = x;
2+myid x = x
3
3
4−idid : (a : Set) -> a -> a;
4+idid : (a : Set) -> a -> a
5−idid = myid ![myid];
5+idid = myid ![myid]
6
6
7−app : (a -> b) -> a -> b;
7+app : (a -> b) -> a -> b
8−app f x = f x;
8+app f x = f x
9
9
10−foo : a -> b -> c -> d -> e -> e;
10+foo : a -> b -> c -> d -> e -> e
11−foo a b c d e = e;
11+foo a b c d e = e
12
12
13−doapp : a -> a;
13+doapp : a -> a
14−doapp x = app myid x;
14+doapp x = app myid x
15
15
16{-
16{-
17
17
test/test003/test003.lidr+4−4
@@ -1,8 +1,8 @@
1−> module main;
1+> module main
2
2
3Import the literate module
3Import the literate module
4
4
5−> import lit;
5+> import lit
6
6
7−> main : IO ();
7+> main : IO ()
8−> main = lit.main;
8+> main = lit.main
test/test004/test004.idr+18−18
@@ -1,21 +1,21 @@
1−module main;
1+module main
2
2
3−dumpFile : String -> IO ();
3+dumpFile : String -> IO ()
4−dumpFile fn = do { h <- openFile fn Read;
4+dumpFile fn = do { h <- openFile fn Read
5− while (do { x <- feof h;
5+ while (do { x <- feof h
6− return (not x); })
6+ return (not x) })
7− (do { l <- fread h;
7+ (do { l <- fread h
8− putStr l; });
8+ putStr l })
9− closeFile h; };
9+ closeFile h }
10
10
11−main : IO ();
11+main : IO ()
12−main = do { h <- openFile "testfile" Write;
12+main = do { h <- openFile "testfile" Write
13− fwrite h "Hello!\nWorld!\n";
13+ fwrite h "Hello!\nWorld!\n"
14− closeFile h;
14+ closeFile h
15− putStrLn "Reading testfile";
15+ putStrLn "Reading testfile"
16− f <- readFile "testfile";
16+ f <- readFile "testfile"
17− putStrLn f;
17+ putStrLn f
18− putStrLn "---";
18+ putStrLn "---"
19− dumpFile "testfile";
19+ dumpFile "testfile"
20− };
20+ }
21
21
test/test005/test005.idr+13−13
@@ -1,16 +1,16 @@
1−module main;
1+module main
2
2
3−tstr : String;
3+tstr : String
4−tstr = "abc123";
4+tstr = "abc123"
5
5
6−tlist : List Int;
6+tlist : List Int
7−tlist = [1, 2, 3, 4, 5];
7+tlist = [1, 2, 3, 4, 5]
8
8
9−main : IO ();
9+main : IO ()
10−main = do { print (abs (-8));
10+main = do { print (abs (-8))
11− print (abs (S O));
11+ print (abs (S O))
12− print (span isAlpha tstr);
12+ print (span isAlpha tstr)
13− print (break isDigit tstr);
13+ print (break isDigit tstr)
14− print (span (\x => x < 3) tlist);
14+ print (span (\x => x < 3) tlist)
15− print (break (\x => x > 2) tlist);
15+ print (break (\x => x > 2) tlist)
16− };
16+ }
test/test006/test006.idr+13−13
@@ -1,27 +1,27 @@
1−module main;
1+module main
2
2
3data Parity : Nat -> Set where
3data Parity : Nat -> Set where
4 even : Parity (n + n)
4 even : Parity (n + n)
5− | odd : Parity (S (n + n));
5+ | odd : Parity (S (n + n))
6
6
7−parity : (n:Nat) -> Parity n;
7+parity : (n:Nat) -> Parity n
8−parity O = even {n=O};
8+parity O = even {n=O}
9−parity (S O) = odd {n=O};
9+parity (S O) = odd {n=O}
10parity (S (S k)) with parity k {
10parity (S (S k)) with parity k {
11− parity (S (S (j + j))) | even ?= even {n=S j};
11+ parity (S (S (j + j))) | even ?= even {n=S j}
12− parity (S (S (S (j + j)))) | odd ?= odd {n=S j};
12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
13}
13}
14
14
15
15
16−natToBin : Nat -> List Bool;
16+natToBin : Nat -> List Bool
17−natToBin O = Nil;
17+natToBin O = Nil
18natToBin k with parity k {
18natToBin k with parity k {
19− natToBin (j + j) | even = False :: natToBin j;
19+ natToBin (j + j) | even = False :: natToBin j
20− natToBin (S (j + j)) | odd = True :: natToBin j;
20+ natToBin (S (j + j)) | odd = True :: natToBin j
21}
21}
22
22
23−main : IO ();
23+main : IO ()
24−main = print (natToBin 42);
24+main = print (natToBin 42)
25
25
26---------- Proofs ----------
26---------- Proofs ----------
27
27
test/test007/test007.idr+27−27
@@ -1,57 +1,57 @@
1−module main;
1+module main
2
2
3instance Applicative Maybe where {
3instance Applicative Maybe where {
4− (Just f) <$> (Just a) = Just (f a);
4+ (Just f) <$> (Just a) = Just (f a)
5− Nothing <$> Nothing = Nothing;
5+ Nothing <$> Nothing = Nothing
6
6
7− pure x = Just x;
7+ pure x = Just x
8}
8}
9
9
10data Expr = Var String
10data Expr = Var String
11 | Val Int
11 | Val Int
12− | Add Expr Expr;
12+ | Add Expr Expr
13
13
14
14
15data Eval : Set -> Set where
15data Eval : Set -> Set where
16− MkEval : (List (String, Int) -> Maybe a) -> Eval a;
16+ MkEval : (List (String, Int) -> Maybe a) -> Eval a
17
17
18−fetch : String -> Eval Int;
18+fetch : String -> Eval Int
19fetch x = MkEval (\e => fetchVal e) where {
19fetch x = MkEval (\e => fetchVal e) where {
20− fetchVal : List (String, Int) -> Maybe Int;
20+ fetchVal : List (String, Int) -> Maybe Int
21− fetchVal [] = Nothing;
21+ fetchVal [] = Nothing
22− fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);
22+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
23}
23}
24
24
25instance Functor Eval where {
25instance Functor Eval where {
26− fmap f (MkEval g) = MkEval (\e => fmap f (g e));
26+ fmap f (MkEval g) = MkEval (\e => fmap f (g e))
27}
27}
28
28
29instance Applicative Eval where {
29instance Applicative Eval where {
30− pure x = MkEval (\e => Just x);
30+ pure x = MkEval (\e => Just x)
31
31
32 (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
32 (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
33− appAux : Maybe (a -> b) -> Maybe a -> Maybe b;
33+ appAux : Maybe (a -> b) -> Maybe a -> Maybe b
34− appAux (Just fx) (Just gx) = Just (fx gx);
34+ appAux (Just fx) (Just gx) = Just (fx gx)
35− appAux _ _ = Nothing;
35+ appAux _ _ = Nothing
36 }
36 }
37}
37}
38
38
39−eval : Expr -> Eval Int;
39+eval : Expr -> Eval Int
40−eval (Var x) = fetch x;
40+eval (Var x) = fetch x
41−eval (Val x) = [| x |];
41+eval (Val x) = [| x |]
42−eval (Add x y) = [| eval x + eval y |];
42+eval (Add x y) = [| eval x + eval y |]
43
43
44−runEval : List (String, Int) -> Expr -> Maybe Int;
44+runEval : List (String, Int) -> Expr -> Maybe Int
45runEval env e with eval e {
45runEval env e with eval e {
46− | MkEval envFn = envFn env;
46+ | MkEval envFn = envFn env
47}
47}
48
48
49−main : IO ();
49+main : IO ()
50−main = do { print [| (*2) (Just 4) |];
50+main = do { print [| (*2) (Just 4) |]
51− print [| plus (Just 4) (Just 5) |];
51+ print [| plus (Just 4) (Just 5) |]
52− print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))));
52+ print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
53− print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))));
53+ print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))
54− };
54+ }
55
55
56
56
57
57
test/test008/test008.idr+18−18
@@ -1,33 +1,33 @@
1−module main;
1+module main
2
2
3−testlist : List (String, Int);
3+testlist : List (String, Int)
4−testlist = [("foo", 1), ("bar", 2)];
4+testlist = [("foo", 1), ("bar", 2)]
5
5
6−getVal : String -> a -> List (String, a) -> a;
6+getVal : String -> a -> List (String, a) -> a
7getVal x b xs = case lookup x xs of {
7getVal x b xs = case lookup x xs of {
8 Just v => case lookup x xs of {
8 Just v => case lookup x xs of {
9 Just v' => v
9 Just v' => v
10 }
10 }
11 | Nothing => b
11 | Nothing => b
12− };
12+ }
13
13
14−foo : (Int, String);
14+foo : (Int, String)
15−foo = (4, "foo");
15+foo = (4, "foo")
16
16
17
17
18−ioVals : IO (String, String);
18+ioVals : IO (String, String)
19−ioVals = do { return ("First", "second"); };
19+ioVals = do { return ("First", "second") }
20
20
21−main : IO ();
21+main : IO ()
22−main = do { (a, b) <- ioVals;
22+main = do { (a, b) <- ioVals
23− putStr (show a ++ " and " ++ show b ++ "? ");
23+ putStr (show a ++ " and " ++ show b ++ "? ")
24− let x = "bar";
24+ let x = "bar"
25− putStrLn (show (getVal x 7 testlist));
25+ putStrLn (show (getVal x 7 testlist))
26− let ((y, z) :: _) = testlist;
26+ let ((y, z) :: _) = testlist
27− print z;
27+ print z
28 case lookup x testlist of {
28 case lookup x testlist of {
29 Just v => putStrLn (show v)
29 Just v => putStrLn (show v)
30 | Nothing => putStrLn "Not there!"
30 | Nothing => putStrLn "Not there!"
31− };
31+ }
32− };
32+ }
33
33
test/test009/test009.idr+5−5
@@ -1,9 +1,9 @@
1−module main;
1+module main
2
2
3−pythag : Int -> List (Int, Int, Int);
3+pythag : Int -> List (Int, Int, Int)
4pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
4pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
5− x*x + y*y == z*z ];
5+ x*x + y*y == z*z ]
6
6
7−main : IO ();
7+main : IO ()
8−main = print (pythag 50);
8+main = print (pythag 50)
9
9