ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

Removed semicolons from tests

Browse Source
This commit is contained in:
Edwin Brady 2012-01-06 23:05:34 +00:00
parent bd61594868
commit ead54e4e70
8 changed files with 108 additions and 108 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
test/test002/test002.idr
View File

@ -1,17 +1,17 @@
myid : a -> a;
myid x = x;
myid : a -> a
myid x = x
idid : (a : Set) -> a -> a;
idid = myid ![myid];
idid : (a : Set) -> a -> a
idid = myid ![myid]
app : (a -> b) -> a -> b;
app f x = f x;
app : (a -> b) -> a -> b
app f x = f x
foo : a -> b -> c -> d -> e -> e;
foo a b c d e = e;
foo : a -> b -> c -> d -> e -> e
foo a b c d e = e
doapp : a -> a;
doapp x = app myid x;
doapp : a -> a
doapp x = app myid x
{-

8
test/test003/test003.lidr
View File

@ -1,8 +1,8 @@
> module main;
> module main
Import the literate module
> import lit;
> import lit
> main : IO ();
> main = lit.main;
> main : IO ()
> main = lit.main

36
test/test004/test004.idr
View File

@ -1,21 +1,21 @@
module main;
module main
dumpFile : String -> IO ();
dumpFile fn = do { h <- openFile fn Read;
while (do { x <- feof h;
return (not x); })
(do { l <- fread h;
putStr l; });
closeFile h; };
dumpFile : String -> IO ()
dumpFile fn = do { h <- openFile fn Read
while (do { x <- feof h
return (not x) })
(do { l <- fread h
putStr l })
closeFile h }
main : IO ();
main = do { h <- openFile "testfile" Write;
fwrite h "Hello!\nWorld!\n";
closeFile h;
putStrLn "Reading testfile";
f <- readFile "testfile";
putStrLn f;
putStrLn "---";
dumpFile "testfile";
};
main : IO ()
main = do { h <- openFile "testfile" Write
fwrite h "Hello!\nWorld!\n"
closeFile h
putStrLn "Reading testfile"
f <- readFile "testfile"
putStrLn f
putStrLn "---"
dumpFile "testfile"
}

26
test/test005/test005.idr
View File

@ -1,16 +1,16 @@
module main;
module main
tstr : String;
tstr = "abc123";
tstr : String
tstr = "abc123"
tlist : List Int;
tlist = [1, 2, 3, 4, 5];
tlist : List Int
tlist = [1, 2, 3, 4, 5]
main : IO ();
main = do { print (abs (-8));
print (abs (S O));
print (span isAlpha tstr);
print (break isDigit tstr);
print (span (\x => x < 3) tlist);
print (break (\x => x > 2) tlist);
};
main : IO ()
main = do { print (abs (-8))
print (abs (S O))
print (span isAlpha tstr)
print (break isDigit tstr)
print (span (\x => x < 3) tlist)
print (break (\x => x > 2) tlist)
}

26
test/test006/test006.idr
View File

@ -1,27 +1,27 @@
module main;
module main
data Parity : Nat -> Set where
even : Parity (n + n)
| odd : Parity (S (n + n));
| odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n;
parity O = even {n=O};
parity (S O) = odd {n=O};
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity (S (S k)) with parity k {
parity (S (S (j + j))) | even ?= even {n=S j};
parity (S (S (S (j + j)))) | odd ?= odd {n=S j};
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
}
natToBin : Nat -> List Bool;
natToBin O = Nil;
natToBin : Nat -> List Bool
natToBin O = Nil
natToBin k with parity k {
natToBin (j + j) | even = False :: natToBin j;
natToBin (S (j + j)) | odd = True :: natToBin j;
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j
}
main : IO ();
main = print (natToBin 42);
main : IO ()
main = print (natToBin 42)
---------- Proofs ----------

54
test/test007/test007.idr
View File

@ -1,57 +1,57 @@
module main;
module main
instance Applicative Maybe where {
(Just f) <$> (Just a) = Just (f a);
Nothing <$> Nothing = Nothing;
(Just f) <$> (Just a) = Just (f a)
Nothing <$> Nothing = Nothing
pure x = Just x;
pure x = Just x
}
data Expr = Var String
| Val Int
| Add Expr Expr;
| Add Expr Expr
data Eval : Set -> Set where
MkEval : (List (String, Int) -> Maybe a) -> Eval a;
MkEval : (List (String, Int) -> Maybe a) -> Eval a
fetch : String -> Eval Int;
fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where {
fetchVal : List (String, Int) -> Maybe Int;
fetchVal [] = Nothing;
fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);
fetchVal : List (String, Int) -> Maybe Int
fetchVal [] = Nothing
fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
}
instance Functor Eval where {
fmap f (MkEval g) = MkEval (\e => fmap f (g e));
fmap f (MkEval g) = MkEval (\e => fmap f (g e))
}
instance Applicative Eval where {
pure x = MkEval (\e => Just x);
pure x = MkEval (\e => Just x)
(<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
appAux : Maybe (a -> b) -> Maybe a -> Maybe b;
appAux (Just fx) (Just gx) = Just (fx gx);
appAux _ _ = Nothing;
appAux : Maybe (a -> b) -> Maybe a -> Maybe b
appAux (Just fx) (Just gx) = Just (fx gx)
appAux _ _ = Nothing
}
}
eval : Expr -> Eval Int;
eval (Var x) = fetch x;
eval (Val x) = [| x |];
eval (Add x y) = [| eval x + eval y |];
eval : Expr -> Eval Int
eval (Var x) = fetch x
eval (Val x) = [| x |]
eval (Add x y) = [| eval x + eval y |]
runEval : List (String, Int) -> Expr -> Maybe Int;
runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e with eval e {
| MkEval envFn = envFn env;
| MkEval envFn = envFn env
}
main : IO ();
main = do { print [| (*2) (Just 4) |];
print [| plus (Just 4) (Just 5) |];
print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))));
print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))));
};
main : IO ()
main = do { print [| (*2) (Just 4) |]
print [| plus (Just 4) (Just 5) |]
print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))
print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))
}

36
test/test008/test008.idr
View File

@ -1,33 +1,33 @@
module main;
module main
testlist : List (String, Int);
testlist = [("foo", 1), ("bar", 2)];
testlist : List (String, Int)
testlist = [("foo", 1), ("bar", 2)]
getVal : String -> a -> List (String, a) -> a;
getVal : String -> a -> List (String, a) -> a
getVal x b xs = case lookup x xs of {
Just v => case lookup x xs of {
Just v' => v
}
| Nothing => b
};
}
foo : (Int, String);
foo = (4, "foo");
foo : (Int, String)
foo = (4, "foo")
ioVals : IO (String, String);
ioVals = do { return ("First", "second"); };
ioVals : IO (String, String)
ioVals = do { return ("First", "second") }
main : IO ();
main = do { (a, b) <- ioVals;
putStr (show a ++ " and " ++ show b ++ "? ");
let x = "bar";
putStrLn (show (getVal x 7 testlist));
let ((y, z) :: _) = testlist;
print z;
main : IO ()
main = do { (a, b) <- ioVals
putStr (show a ++ " and " ++ show b ++ "? ")
let x = "bar"
putStrLn (show (getVal x 7 testlist))
let ((y, z) :: _) = testlist
print z
case lookup x testlist of {
Just v => putStrLn (show v)
| Nothing => putStrLn "Not there!"
};
};
}
}

10
test/test009/test009.idr
View File

@ -1,9 +1,9 @@
module main;
module main
pythag : Int -> List (Int, Int, Int);
pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
x*x + y*y == z*z ];
x*x + y*y == z*z ]
main : IO ();
main = print (pythag 50);
main : IO ()
main = print (pythag 50)