git.iko.soy/Idris-dev
on master help sign in
Add tests for tutorial examples
commit7cea99530632ee1da7c7150239337d2864ee6b6d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 23 Mar 2014, 15:21 (13 years ago) parent678fc86
17 files changed+241
compare with master
unifiedsplit
idris.cabal+15 test/tutorial002/expected test/tutorial002/run+3 test/tutorial002/tutorial002.idr+61 test/tutorial003/expected test/tutorial003/run+3 test/tutorial003/tutorial003.idr+38 test/tutorial004/expected test/tutorial004/run+3 test/tutorial004/tutorial004.idr+57 test/tutorial005/expected test/tutorial005/run+3 test/tutorial005/tutorial005.idr+14 test/tutorial006/expected+23 test/tutorial006/run+4 test/tutorial006/tutorial006a.idr+5 test/tutorial006/tutorial006b.idr+12
idris.cabal+15
@@ -391,6 +391,21 @@ Extra-source-files:
391391 test/tutorial001/run
392392 test/tutorial001/*.idr
393393 test/tutorial001/expected
394+ test/tutorial002/run
395+ test/tutorial002/*.idr
396+ test/tutorial002/expected
397+ test/tutorial003/run
398+ test/tutorial003/*.idr
399+ test/tutorial003/expected
400+ test/tutorial004/run
401+ test/tutorial004/*.idr
402+ test/tutorial004/expected
403+ test/tutorial005/run
404+ test/tutorial005/*.idr
405+ test/tutorial005/expected
406+ test/tutorial006/run
407+ test/tutorial006/*.idr
408+ test/tutorial006/expected
394409
395410source-repository head
396411 type: git
test/tutorial002/expectednew file

No changes to the content.

test/tutorial002/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ tutorial002.idr --check
3+rm -f *.ibc
test/tutorial002/tutorial002.idrnew file+61
@@ -0,0 +1,61 @@
1+module Main
2+
3+data Binary : Nat -> Type where
4+ bEnd : Binary Z
5+ bO : Binary n -> Binary (n + n)
6+ bI : Binary n -> Binary (S (n + n))
7+
8+instance Show (Binary n) where
9+ show (bO x) = show x ++ "0"
10+ show (bI x) = show x ++ "1"
11+ show bEnd = ""
12+
13+data Parity : Nat -> Type where
14+ even : Parity (n + n)
15+ odd : Parity (S (n + n))
16+
17+parity : (n:Nat) -> Parity n
18+parity Z = even {n=Z}
19+parity (S Z) = odd {n=Z}
20+parity (S (S k)) with (parity k)
21+ parity (S (S (j + j))) | even ?= even {n=S j}
22+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
23+
24+natToBin : (n:Nat) -> Binary n
25+natToBin Z = bEnd
26+natToBin (S k) with (parity k)
27+ natToBin (S (j + j)) | even = bI (natToBin j)
28+ natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
29+
30+intToNat : Int -> Nat
31+intToNat 0 = Z
32+intToNat x = if (x>0) then (S (intToNat (x-1))) else Z
33+
34+main : IO ()
35+main = do putStr "Enter a number: "
36+ x <- getLine
37+ print (natToBin (fromInteger (cast x)))
38+
39+---------- Proofs ----------
40+
41+Main.natToBin_lemma_1 = proof
42+ intros
43+ rewrite plusSuccRightSucc j j
44+ rewrite sym (plusSuccRightSucc j j)
45+ trivial
46+
47+
48+parity_lemma_1 = proof
49+ intros
50+ rewrite sym (plusSuccRightSucc j j)
51+ trivial
52+
53+
54+parity_lemma_2 = proof {
55+ intro;
56+ intro;
57+ rewrite sym (plusSuccRightSucc j j);
58+ trivial;
59+}
60+
61+
test/tutorial003/expectednew file

No changes to the content.

test/tutorial003/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ tutorial003.idr --check
3+rm -f *.ibc
test/tutorial003/tutorial003.idrnew file+38
@@ -0,0 +1,38 @@
1+module idiom
2+
3+data Expr = Var String
4+ | Val Int
5+ | Add Expr Expr
6+
7+data Eval : Type -> Type where
8+ MkEval : (List (String, Int) -> Maybe a) -> Eval a
9+
10+fetch : String -> Eval Int
11+fetch x = MkEval (\e => fetchVal e) where
12+ fetchVal : List (String, Int) -> Maybe Int
13+ fetchVal [] = Nothing
14+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
15+
16+instance Functor Eval where
17+ map f (MkEval g) = MkEval (\e => map f (g e))
18+
19+instance Applicative Eval where
20+ pure x = MkEval (\e => Just x)
21+
22+ (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
23+ app : Maybe (a -> b) -> Maybe a -> Maybe b
24+ app (Just fx) (Just gx) = Just (fx gx)
25+ app _ _ = Nothing
26+
27+eval : Expr -> Eval Int
28+eval (Var x) = fetch x
29+eval (Val x) = [| x |]
30+eval (Add x y) = [| eval x + eval y |]
31+
32+runEval : List (String, Int) -> Expr -> Maybe Int
33+runEval env e = case eval e of
34+ MkEval envFn => envFn env
35+
36+m_add' : Maybe Int -> Maybe Int -> Maybe Int
37+m_add' x y = [| x + y |]
38+
test/tutorial004/expectednew file

No changes to the content.

test/tutorial004/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ tutorial004.idr --check
3+rm -f *.ibc
test/tutorial004/tutorial004.idrnew file+57
@@ -0,0 +1,57 @@
1+
2+fiveIsFive : 5 = 5
3+fiveIsFive = refl
4+
5+twoPlusTwo : 2 + 2 = 4
6+twoPlusTwo = refl
7+
8+total disjoint : (n : Nat) -> Z = S n -> _|_
9+disjoint n p = replace {P = disjointTy} p ()
10+ where
11+ disjointTy : Nat -> Type
12+ disjointTy Z = ()
13+ disjointTy (S k) = _|_
14+
15+total acyclic : (n : Nat) -> n = S n -> _|_
16+acyclic Z p = disjoint _ p
17+acyclic (S k) p = acyclic k (succInjective _ _ p)
18+
19+empty1 : _|_
20+empty1 = hd [] where
21+ hd : List a -> a
22+ hd (x :: xs) = x
23+
24+empty2 : _|_
25+empty2 = empty2
26+
27+plusReduces : (n:Nat) -> plus Z n = n
28+plusReduces n = refl
29+
30+plusReducesZ : (n:Nat) -> n = plus n Z
31+plusReducesZ Z = refl
32+plusReducesZ (S k) = cong (plusReducesZ k)
33+
34+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
35+plusReducesS Z m = refl
36+plusReducesS (S k) m = cong (plusReducesS k m)
37+
38+plusReducesZ' : (n:Nat) -> n = plus n Z
39+plusReducesZ' Z = ?plusredZ_Z
40+plusReducesZ' (S k) = let ih = plusReducesZ' k in
41+ ?plusredZ_S
42+
43+
44+---------- Proofs ----------
45+
46+plusredZ_S = proof {
47+ intro;
48+ intro;
49+ rewrite ih;
50+ trivial;
51+}
52+
53+plusredZ_Z = proof {
54+ compute;
55+ trivial;
56+}
57+
test/tutorial005/expectednew file

No changes to the content.

test/tutorial005/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ tutorial005.idr --check
3+rm -f *.ibc
test/tutorial005/tutorial005.idrnew file+14
@@ -0,0 +1,14 @@
1+module wheres
2+
3+even : Nat -> Bool
4+even Z = True
5+even (S k) = odd k where
6+ odd Z = False
7+ odd (S k) = even k
8+
9+test : List Nat
10+test = [c (S 1), c Z, d (S Z)]
11+ where c x = 42 + x
12+ d y = c (y + 1 + z y)
13+ where z w = y + w
14+
test/tutorial006/expectednew file+23
@@ -0,0 +1,23 @@
1+tutorial006a.idr:3:23:When elaborating right hand side of vapp:
2+When elaborating argument xs to constructor Prelude.Vect.:::
3+ Can't unify
4+ Vect (n + m) a
5+ with
6+ Vect (plus n m) a
7+
8+ Specifically:
9+ Can't unify
10+ plus n m
11+ with
12+ plus n m
13+tutorial006b.idr:10:10:When elaborating right hand side of Main.parity:
14+Can't unify
15+ Parity (plus (S j) (S j))
16+with
17+ Parity (S (S (plus j j)))
18+
19+Specifically:
20+ Can't unify
21+ plus (S j) (S j)
22+ with
23+ S (S (plus j j))
test/tutorial006/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ tutorial006a.idr --check
3+idris $@ tutorial006b.idr --check
4+rm -f *.ibc
test/tutorial006/tutorial006a.idrnew file+5
@@ -0,0 +1,5 @@
1+vapp : Vect n a -> Vect m a -> Vect (n + m) a
2+vapp Nil ys = ys
3+vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
4+
5+
test/tutorial006/tutorial006b.idrnew file+12
@@ -0,0 +1,12 @@
1+
2+data Parity : Nat -> Type where
3+ even : Parity (n + n)
4+ odd : Parity (S (n + n))
5+
6+parity : (n:Nat) -> Parity n
7+parity Z = even {n=Z}
8+parity (S Z) = odd {n=Z}
9+parity (S (S k)) with (parity k)
10+ parity (S (S (j + j))) | even = even {n=S j}
11+ parity (S (S (S (j + j)))) | odd = odd {n=S j}
12+