git.iko.soy/Idris-dev
on master help sign in
Removed semicolons from tests
commitead54e4e70e8544d34a1cb0c27880c6525124c2b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 23:05 (15 years ago) parentbd61594
8 files changed+108−108
compare with master
unifiedsplit
test/test002/test002.idr+10−10 test/test003/test003.lidr+4−4 test/test004/test004.idr+18−18 test/test005/test005.idr+13−13 test/test006/test006.idr+13−13 test/test007/test007.idr+27−27 test/test008/test008.idr+18−18 test/test009/test009.idr+5−5
test/test002/test002.idr+10−10
@@ -1,17 +1,17 @@
1−myid : a -> a;
2−myid x = x;
1+myid : a -> a
2+myid x = x
33
4−idid : (a : Set) -> a -> a;
5−idid = myid ![myid];
4+idid : (a : Set) -> a -> a
5+idid = myid ![myid]
66
7−app : (a -> b) -> a -> b;
8−app f x = f x;
7+app : (a -> b) -> a -> b
8+app f x = f x
99
10−foo : a -> b -> c -> d -> e -> e;
11−foo a b c d e = e;
10+foo : a -> b -> c -> d -> e -> e
11+foo a b c d e = e
1212
13−doapp : a -> a;
14−doapp x = app myid x;
13+doapp : a -> a
14+doapp x = app myid x
1515
1616{-
1717
test/test003/test003.lidr+4−4
@@ -1,8 +1,8 @@
1−> module main;
1+> module main
22
33Import the literate module
44
5−> import lit;
5+> import lit
66
7−> main : IO ();
8−> main = lit.main;
7+> main : IO ()
8+> main = lit.main
test/test004/test004.idr+18−18
@@ -1,21 +1,21 @@
1−module main;
1+module main
22
3−dumpFile : String -> IO ();
4−dumpFile fn = do { h <- openFile fn Read;
5− while (do { x <- feof h;
6− return (not x); })
7− (do { l <- fread h;
8− putStr l; });
9− closeFile h; };
3+dumpFile : String -> IO ()
4+dumpFile fn = do { h <- openFile fn Read
5+ while (do { x <- feof h
6+ return (not x) })
7+ (do { l <- fread h
8+ putStr l })
9+ closeFile h }
1010
11−main : IO ();
12−main = do { h <- openFile "testfile" Write;
13− fwrite h "Hello!\nWorld!\n";
14− closeFile h;
15− putStrLn "Reading testfile";
16− f <- readFile "testfile";
17− putStrLn f;
18− putStrLn "---";
19− dumpFile "testfile";
20− };
11+main : IO ()
12+main = do { h <- openFile "testfile" Write
13+ fwrite h "Hello!\nWorld!\n"
14+ closeFile h
15+ putStrLn "Reading testfile"
16+ f <- readFile "testfile"
17+ putStrLn f
18+ putStrLn "---"
19+ dumpFile "testfile"
20+ }
2121
test/test005/test005.idr+13−13
@@ -1,16 +1,16 @@
1−module main;
1+module main
22
3−tstr : String;
4−tstr = "abc123";
3+tstr : String
4+tstr = "abc123"
55
6−tlist : List Int;
7−tlist = [1, 2, 3, 4, 5];
6+tlist : List Int
7+tlist = [1, 2, 3, 4, 5]
88
9−main : IO ();
10−main = do { print (abs (-8));
11− print (abs (S O));
12− print (span isAlpha tstr);
13− print (break isDigit tstr);
14− print (span (\x => x < 3) tlist);
15− print (break (\x => x > 2) tlist);
16− };
9+main : IO ()
10+main = do { print (abs (-8))
11+ print (abs (S O))
12+ print (span isAlpha tstr)
13+ print (break isDigit tstr)
14+ print (span (\x => x < 3) tlist)
15+ print (break (\x => x > 2) tlist)
16+ }
test/test006/test006.idr+13−13
@@ -1,27 +1,27 @@
1−module main;
1+module main
22
33data Parity : Nat -> Set where
44 even : Parity (n + n)
5− | odd : Parity (S (n + n));
5+ | odd : Parity (S (n + n))
66
7−parity : (n:Nat) -> Parity n;
8−parity O = even {n=O};
9−parity (S O) = odd {n=O};
7+parity : (n:Nat) -> Parity n
8+parity O = even {n=O}
9+parity (S O) = odd {n=O}
1010parity (S (S k)) with parity k {
11− parity (S (S (j + j))) | even ?= even {n=S j};
12− parity (S (S (S (j + j)))) | odd ?= odd {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}
1313}
1414
1515
16−natToBin : Nat -> List Bool;
17−natToBin O = Nil;
16+natToBin : Nat -> List Bool
17+natToBin O = Nil
1818natToBin k with parity k {
19− natToBin (j + j) | even = False :: natToBin j;
20− natToBin (S (j + j)) | odd = True :: natToBin j;
19+ natToBin (j + j) | even = False :: natToBin j
20+ natToBin (S (j + j)) | odd = True :: natToBin j
2121}
2222
23−main : IO ();
24−main = print (natToBin 42);
23+main : IO ()
24+main = print (natToBin 42)
2525
2626---------- Proofs ----------
2727
test/test007/test007.idr+27−27
@@ -1,57 +1,57 @@
1−module main;
1+module main
22
33instance Applicative Maybe where {
4− (Just f) <$> (Just a) = Just (f a);
5− Nothing <$> Nothing = Nothing;
4+ (Just f) <$> (Just a) = Just (f a)
5+ Nothing <$> Nothing = Nothing
66
7− pure x = Just x;
7+ pure x = Just x
88}
99
1010data Expr = Var String
1111 | Val Int
12− | Add Expr Expr;
12+ | Add Expr Expr
1313
1414
1515data Eval : Set -> Set where
16− MkEval : (List (String, Int) -> Maybe a) -> Eval a;
16+ MkEval : (List (String, Int) -> Maybe a) -> Eval a
1717
18−fetch : String -> Eval Int;
18+fetch : String -> Eval Int
1919fetch x = MkEval (\e => fetchVal e) where {
20− fetchVal : List (String, Int) -> Maybe Int;
21− fetchVal [] = Nothing;
22− fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);
20+ fetchVal : List (String, Int) -> Maybe Int
21+ fetchVal [] = Nothing
22+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
2323}
2424
2525instance 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))
2727}
2828
2929instance Applicative Eval where {
30− pure x = MkEval (\e => Just x);
30+ pure x = MkEval (\e => Just x)
3131
3232 (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
33− appAux : Maybe (a -> b) -> Maybe a -> Maybe b;
34− appAux (Just fx) (Just gx) = Just (fx gx);
35− appAux _ _ = Nothing;
33+ appAux : Maybe (a -> b) -> Maybe a -> Maybe b
34+ appAux (Just fx) (Just gx) = Just (fx gx)
35+ appAux _ _ = Nothing
3636 }
3737}
3838
39−eval : Expr -> Eval Int;
40−eval (Var x) = fetch x;
41−eval (Val x) = [| x |];
42−eval (Add x y) = [| eval x + eval y |];
39+eval : Expr -> Eval Int
40+eval (Var x) = fetch x
41+eval (Val x) = [| x |]
42+eval (Add x y) = [| eval x + eval y |]
4343
44−runEval : List (String, Int) -> Expr -> Maybe Int;
44+runEval : List (String, Int) -> Expr -> Maybe Int
4545runEval env e with eval e {
46− | MkEval envFn = envFn env;
46+ | MkEval envFn = envFn env
4747}
4848
49−main : IO ();
50−main = do { print [| (*2) (Just 4) |];
51− print [| plus (Just 4) (Just 5) |];
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"))));
54− };
49+main : IO ()
50+main = do { print [| (*2) (Just 4) |]
51+ print [| plus (Just 4) (Just 5) |]
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"))))
54+ }
5555
5656
5757
test/test008/test008.idr+18−18
@@ -1,33 +1,33 @@
1−module main;
1+module main
22
3−testlist : List (String, Int);
4−testlist = [("foo", 1), ("bar", 2)];
3+testlist : List (String, Int)
4+testlist = [("foo", 1), ("bar", 2)]
55
6−getVal : String -> a -> List (String, a) -> a;
6+getVal : String -> a -> List (String, a) -> a
77getVal x b xs = case lookup x xs of {
88 Just v => case lookup x xs of {
99 Just v' => v
1010 }
1111 | Nothing => b
12− };
12+ }
1313
14−foo : (Int, String);
15−foo = (4, "foo");
14+foo : (Int, String)
15+foo = (4, "foo")
1616
1717
18−ioVals : IO (String, String);
19−ioVals = do { return ("First", "second"); };
18+ioVals : IO (String, String)
19+ioVals = do { return ("First", "second") }
2020
21−main : IO ();
22−main = do { (a, b) <- ioVals;
23− putStr (show a ++ " and " ++ show b ++ "? ");
24− let x = "bar";
25− putStrLn (show (getVal x 7 testlist));
26− let ((y, z) :: _) = testlist;
27− print z;
21+main : IO ()
22+main = do { (a, b) <- ioVals
23+ putStr (show a ++ " and " ++ show b ++ "? ")
24+ let x = "bar"
25+ putStrLn (show (getVal x 7 testlist))
26+ let ((y, z) :: _) = testlist
27+ print z
2828 case lookup x testlist of {
2929 Just v => putStrLn (show v)
3030 | Nothing => putStrLn "Not there!"
31− };
32− };
31+ }
32+ }
3333
test/test009/test009.idr+5−5
@@ -1,9 +1,9 @@
1−module main;
1+module main
22
3−pythag : Int -> List (Int, Int, Int);
3+pythag : Int -> List (Int, Int, Int)
44pythag 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 ]
66
7−main : IO ();
8−main = print (pythag 50);
7+main : IO ()
8+main = print (pythag 50)
99