git.iko.soy/Idris-dev
on master help sign in
Remove example directory

See http://github.com/edwinb/idris-demos instead

commit78c27e99d1e898d9db395cd6782d2d5c3336d925 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 10 Apr 2014, 14:09 (13 years ago) parent845e02a
16 files changed−392
compare with master
unifiedsplit
examples/binary.idr−62 examples/bmain.idr−8 examples/btree.idr−18 examples/classes.idr−10 examples/foo.idr−10 examples/hello.idr−5 examples/idiom.idr−38 examples/interp.idr−71 examples/letbind.idr−16 examples/prims.idr−14 examples/theorems.idr−57 examples/universe.idr−7 examples/usefultypes.idr−20 examples/vbroken.idr−5 examples/views.idr−37 examples/wheres.idr−14
examples/binary.idrdeleted−62
@@ -1,62 +0,0 @@
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−parity_lemma_1 = proof {
42− intros;
43− rewrite sym (plusSuccRightSucc j j);
44− trivial;
45−}
46−
47−natToBin_lemma_1 = proof {
48− intro;
49− intro;
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−
62−
examples/bmain.idrdeleted−8
@@ -1,8 +0,0 @@
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−
examples/btree.idrdeleted−18
@@ -1,18 +0,0 @@
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−
examples/classes.idrdeleted−10
@@ -1,10 +0,0 @@
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)
examples/foo.idrdeleted−10
@@ -1,10 +0,0 @@
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−
examples/hello.idrdeleted−5
@@ -1,5 +0,0 @@
1−module Main
2−
3−main : IO ()
4−main = putStrLn "Hello world"
5−
examples/idiom.idrdeleted−38
@@ -1,38 +0,0 @@
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−
examples/interp.idrdeleted−71
@@ -1,71 +0,0 @@
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 -> Expr G a -> Expr G a -> Expr G a
32−
33− interp : Env G -> {static} 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− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
55− app = \f, a => App f a
56−
57− fact : Expr G (TyFun TyInt TyInt)
58− fact = Lam (If (Op (==) (Var stop) (Val 0))
59− (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))
60−
61−testFac : Int
62−testFac = interp [] fact 4
63−
64−unitTestFac : so (interp [] fact 4 == 24)
65−unitTestFac = oh
66−
67−main : IO ()
68−main = do putStr "Enter a number: "
69− x <- getLine
70− print (interp [] fact (cast x))
71−
examples/letbind.idrdeleted−16
@@ -1,16 +0,0 @@
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−
examples/prims.idrdeleted−14
@@ -1,14 +0,0 @@
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−
examples/theorems.idrdeleted−57
@@ -1,57 +0,0 @@
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−
examples/universe.idrdeleted−7
@@ -1,7 +0,0 @@
1−myid : (a : Type) -> a -> a
2−myid _ x = x
3−
4−idid : (a : Type) -> a -> a
5−idid = myid _ myid
6−
7−
examples/usefultypes.idrdeleted−20
@@ -1,20 +0,0 @@
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−
examples/vbroken.idrdeleted−5
@@ -1,5 +0,0 @@
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−
examples/views.idrdeleted−37
@@ -1,37 +0,0 @@
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−
examples/wheres.idrdeleted−14
@@ -1,14 +0,0 @@
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−