40c303b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Since we can overload things, might as well use less ugly names ;)

commit40c303bd346d2c1867da4ba840357027aa61a4e1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 29 Nov 2011, 17:08 (15 years ago) parentddba413

3 files changed+21−21

compare with master

unifiedsplit

lib/prelude/vect.idr+11−11 samples/interp.idr+5−5 test/test001/test001.idr+5−5

lib/prelude/vect.idr+11−11

@@ -20,18 +20,18 @@ data Vect : Set -> Nat -> Set where

2020 Nil : Vect a O

2121 | (::) : a -> Vect a k -> Vect a (S k);

2222

23−vlookup : Fin n -> Vect a n -> a;

24−vlookup fO (x :: xs) = x;

25−vlookup (fS k) (x :: xs) = vlookup k xs;

23+lookup : Fin n -> Vect a n -> a;

24+lookup fO (x :: xs) = x;

25+lookup (fS k) (x :: xs) = lookup k xs;

2626

27−vapp : Vect a n -> Vect a m -> Vect a (n + m);

28−vapp [] ys = ys;

29−vapp (x :: xs) ys = x :: vapp xs ys;

30−

31−vfilter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

32−vfilter p [] = ( _ ** [] );

33−vfilter p (x :: xs) with (vfilter p xs) {

34− vfilter p (x :: xs) | ( _ ** xs' )

27+app : Vect a n -> Vect a m -> Vect a (n + m);

28+app [] ys = ys;

29+app (x :: xs) ys = x :: app xs ys;

30+

31+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

32+filter p [] = ( _ ** [] );

33+filter p (x :: xs) with (filter p xs) {

34+ filter p (x :: xs) | ( _ ** xs' )

3535 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

3636}

3737

samples/interp.idr+5−5

@@ -13,12 +13,12 @@ using (G : Vect Ty n) {

1313 Nil : Env Nil

1414 | (::) : interpTy a -> Env G -> Env (a :: G);

1515

16− envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);

17− envLookup fO (x :: xs) = x;

18− envLookup (fS i) (x :: xs) = envLookup i xs;

16+ lookup : (i : Fin n) -> Env G -> interpTy (lookup i G);

17+ lookup fO (x :: xs) = x;

18+ lookup (fS i) (x :: xs) = lookup i xs;

1919

2020 data Expr : Vect Ty n -> Ty -> Set where

21− Var : (i : Fin n) -> Expr G (vlookup i G)

21+ Var : (i : Fin n) -> Expr G (lookup i G)

2222 | Val : (x : Int) -> Expr G TyInt

2323 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

2424 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

@@ -30,7 +30,7 @@ using (G : Vect Ty n) {

3030 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

3131

3232 interp : Env G -> {static} Expr G t -> interpTy t;

33− interp env (Var i) = envLookup i env;

33+ interp env (Var i) = lookup i env;

3434 interp env (Val x) = x;

3535 interp env (Lam sc) = \x => interp (x :: env) sc;

3636 interp env (App f s) = (interp env f) (interp env s);

test/test001/test001.idr+5−5