git.iko.soy/Idris-dev
on master help sign in
Migrated tutorial examples into samples.
commitbd6199a309feec513cafeb8abc31b1e9dc46f3ad authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateThu 16 Apr 2015, 09:57 (12 years ago) parentff46849
19 files changed+436
compare with master
unifiedsplit
samples/tutorial/Makefile+11 samples/tutorial/binary.idr+61 samples/tutorial/bmain.idr+8 samples/tutorial/btree.idr+18 samples/tutorial/btreemod.idr+20 samples/tutorial/classes.idr+10 samples/tutorial/foo.idr+10 samples/tutorial/hello.idr+5 samples/tutorial/idiom.idr+38 samples/tutorial/interp.idr+68 samples/tutorial/letbind.idr+16 samples/tutorial/prims.idr+14 samples/tutorial/theorems.idr+57 samples/tutorial/universe.idr+7 samples/tutorial/usefultypes.idr+20 samples/tutorial/vbroken.idr+10 samples/tutorial/views.idr+37 samples/tutorial/viewsbroken.idr+12 samples/tutorial/wheres.idr+14
samples/tutorial/Makefilenew file+11
@@ -0,0 +1,11 @@
1+check: .PHONY
2+ rm -f *.ibc
3+ for x in *.idr ; do \
4+ echo "Checking $$x"; \
5+ idris --check $$x; \
6+ done
7+
8+clean:
9+ rm -f *.ibc
10+
11+.PHONY:
samples/tutorial/binary.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+
samples/tutorial/bmain.idrnew file+8
@@ -0,0 +1,8 @@
1+module Main
2+
3+import btree
4+
5+main : IO ()
6+main = do let t = toTree [1,8,2,7,9,3]
7+ print (btree.toList t)
8+
samples/tutorial/btree.idrnew file+18
@@ -0,0 +1,18 @@
1+module btree
2+
3+data BTree a = Leaf
4+ | Node (BTree a) a (BTree a)
5+
6+insert : Ord a => a -> BTree a -> BTree a
7+insert x Leaf = Node Leaf x Leaf
8+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
9+ else (Node l v (insert x r))
10+
11+toList : BTree a -> List a
12+toList Leaf = []
13+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
14+
15+toTree : Ord a => List a -> BTree a
16+toTree [] = Leaf
17+toTree (x :: xs) = insert x (toTree xs)
18+
samples/tutorial/btreemod.idrnew file+20
@@ -0,0 +1,20 @@
1+module btree
2+
3+abstract data BTree a = Leaf
4+ | Node (BTree a) a (BTree a)
5+
6+abstract
7+insert : Ord a => a -> BTree a -> BTree a
8+insert x Leaf = Node Leaf x Leaf
9+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
10+ else (Node l v (insert x r))
11+
12+abstract
13+toList : BTree a -> List a
14+toList Leaf = []
15+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
16+
17+abstract
18+toTree : Ord a => List a -> BTree a
19+toTree [] = Leaf
20+toTree (x :: xs) = insert x (toTree xs)
samples/tutorial/classes.idrnew file+10
@@ -0,0 +1,10 @@
1+m_add : Maybe Int -> Maybe Int -> Maybe Int
2+m_add x y = do x' <- x -- Extract value from x
3+ y' <- y -- Extract value from y
4+ return (x' + y') -- Add them
5+
6+m_add' : Maybe Int -> Maybe Int -> Maybe Int
7+m_add' x y = [ x' + y' | x' <- x, y' <- y ]
8+
9+sortAndShow : (Ord a, Show a) => List a -> String
10+sortAndShow xs = show (sort xs)
samples/tutorial/foo.idrnew file+10
@@ -0,0 +1,10 @@
1+module foo
2+
3+namespace x
4+ test : Int -> Int
5+ test x = x * 2
6+
7+namespace y
8+ test : String -> String
9+ test x = x ++ x
10+
samples/tutorial/hello.idrnew file+5
@@ -0,0 +1,5 @@
1+module Main
2+
3+main : IO ()
4+main = putStrLn "Hello world"
5+
samples/tutorial/idiom.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 fetchVal 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+
samples/tutorial/interp.idrnew file+68
@@ -0,0 +1,68 @@
1+module Main
2+
3+data Ty = TyInt | TyBool| TyFun Ty Ty
4+
5+interpTy : Ty -> Type
6+interpTy TyInt = Int
7+interpTy TyBool = Bool
8+interpTy (TyFun s t) = interpTy s -> interpTy t
9+
10+using (G : Vect n Ty)
11+
12+ data Env : Vect n Ty -> Type where
13+ Nil : Env Nil
14+ (::) : interpTy a -> Env G -> Env (a :: G)
15+
16+ data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17+ Stop : HasType FZ (t :: G) t
18+ Pop : HasType k G t -> HasType (FS k) (u :: G) t
19+
20+ lookup : HasType i G t -> Env G -> interpTy t
21+ lookup Stop (x :: xs) = x
22+ lookup (Pop k) (x :: xs) = lookup k xs
23+
24+ data Expr : Vect n Ty -> Ty -> Type where
25+ Var : HasType i G t -> Expr G t
26+ Val : (x : Int) -> Expr G TyInt
27+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)
28+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t
29+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
30+ Expr G c
31+ If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a
32+
33+ interp : Env G -> [static] (e : Expr G t) -> interpTy t
34+ interp env (Var i) = lookup i env
35+ interp env (Val x) = x
36+ interp env (Lam sc) = \x => interp (x :: env) sc
37+ interp env (App f s) = interp env f (interp env s)
38+ interp env (Op op x y) = op (interp env x) (interp env y)
39+ interp env (If x t e) = if interp env x then interp env t
40+ else interp env e
41+
42+ eId : Expr G (TyFun TyInt TyInt)
43+ eId = Lam (Var Stop)
44+
45+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
46+ eAdd = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
47+
48+ eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))
49+ eEq = Lam (Lam (Op (==) (Var Stop) (Var (Pop Stop))))
50+
51+ eDouble : Expr G (TyFun TyInt TyInt)
52+ eDouble = Lam (App (App eAdd (Var Stop)) (Var Stop))
53+
54+ fact : Expr G (TyFun TyInt TyInt)
55+ fact = Lam (If (Op (==) (Var Stop) (Val 0))
56+ (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1))) (Var Stop)))
57+
58+testFac : Int
59+testFac = interp [] fact 4
60+
61+-- unitTestFac : so (interp [] fact 4 == 24)
62+-- unitTestFac = oh
63+
64+main : IO ()
65+main = do putStr "Enter a number: "
66+ x <- getLine
67+ print (interp [] fact (cast x))
68+
samples/tutorial/letbind.idrnew file+16
@@ -0,0 +1,16 @@
1+module letbind
2+
3+mirror : List a -> List a
4+mirror xs = let xs' = reverse xs in
5+ xs ++ xs'
6+
7+data Person = MkPerson String Int
8+
9+showPerson : Person -> String
10+showPerson p = let MkPerson name age = p in
11+ name ++ " is " ++ show age ++ " years old"
12+
13+splitAt : Char -> String -> (String, String)
14+splitAt c x = case break (== c) x of
15+ (x, y) => (x, strTail y)
16+
samples/tutorial/prims.idrnew file+14
@@ -0,0 +1,14 @@
1+module prims
2+
3+x : Int
4+x = 42
5+
6+foo : String
7+foo = "Sausage machine"
8+
9+bar : Char
10+bar = 'Z'
11+
12+quux : Bool
13+quux = False
14+
samples/tutorial/theorems.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 -> Void
9+disjoint n p = replace {P = disjointTy} p ()
10+ where
11+ disjointTy : Nat -> Type
12+ disjointTy Z = ()
13+ disjointTy (S k) = Void
14+
15+total acyclic : (n : Nat) -> n = S n -> Void
16+acyclic Z p = disjoint _ p
17+acyclic (S k) p = acyclic k (succInjective _ _ p)
18+
19+empty1 : Void
20+empty1 = hd [] where
21+ hd : List a -> a
22+ hd (x :: xs) = x
23+
24+empty2 : Void
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+
samples/tutorial/universe.idrnew file+7
@@ -0,0 +1,7 @@
1+myid : (a : Type) -> a -> a
2+myid _ x = x
3+
4+idid : (a : Type) -> a -> a
5+idid = myid _ myid
6+
7+
samples/tutorial/usefultypes.idrnew file+20
@@ -0,0 +1,20 @@
1+
2+intVec : Vect 5 Int
3+intVec = [1, 2, 3, 4, 5]
4+
5+double : Int -> Int
6+double x = x * 2
7+
8+vec : (n ** Vect n Int)
9+vec = (_ ** [3, 4])
10+
11+list_lookup : Nat -> List a -> Maybe a
12+list_lookup _ Nil = Nothing
13+list_lookup Z (x :: xs) = Just x
14+list_lookup (S k) (x :: xs) = list_lookup k xs
15+
16+lookup_default : Nat -> List a -> a -> a
17+lookup_default i xs def = case list_lookup i xs of
18+ Nothing => def
19+ Just x => x
20+
samples/tutorial/vbroken.idrnew file+10
@@ -0,0 +1,10 @@
1+module Vect
2+
3+data Vect : Nat -> Type -> Type where
4+ Nil : Vect Z a
5+ (::) : a -> Vect k a -> Vect (S k) a
6+
7+(++) : Vect n a -> Vect m a -> Vect (n + m) a
8+(++) Nil ys = ys
9+(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN
10+
samples/tutorial/views.idrnew file+37
@@ -0,0 +1,37 @@
1+module views
2+
3+data Parity : Nat -> Type where
4+ Even : Parity (n + n)
5+ Odd : Parity (S (n + n))
6+
7+parity : (n:Nat) -> Parity n
8+parity Z = Even {n=Z}
9+parity (S Z) = Odd {n=Z}
10+parity (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}
13+
14+natToBin : Nat -> List Bool
15+natToBin Z = Nil
16+natToBin k with (parity k)
17+ natToBin (j + j) | Even = False :: natToBin j
18+ natToBin (S (j + j)) | Odd = True :: natToBin j
19+
20+
21+---------- Proofs ----------
22+
23+views.parity_lemma_2 = proof {
24+ intro;
25+ intro;
26+ rewrite sym (plusSuccRightSucc j j);
27+ trivial;
28+}
29+
30+views.parity_lemma_1 = proof {
31+ intro;
32+ intro;
33+ rewrite sym (plusSuccRightSucc j j);
34+ trivial;
35+}
36+
37+
samples/tutorial/viewsbroken.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+
samples/tutorial/wheres.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+