git.iko.soy/Idris-dev
on master help sign in
Since we can overload things, might as well use less ugly names ;)
40c303bEdwin Brady
lib/prelude/vect.idr+11−11
compare with master
unifiedsplit
@@ -20,18 +20,18 @@ data Vect : Set -> Nat -> Set where
20 Nil : Vect a O
20 Nil : Vect a O
21 | (::) : a -> Vect a k -> Vect a (S k);
21 | (::) : a -> Vect a k -> Vect a (S k);
22
22
23−vlookup : Fin n -> Vect a n -> a;
23+lookup : Fin n -> Vect a n -> a;
24−vlookup fO (x :: xs) = x;
24+lookup fO (x :: xs) = x;
25−vlookup (fS k) (x :: xs) = vlookup k xs;
25+lookup (fS k) (x :: xs) = lookup k xs;
26
26
27−vapp : Vect a n -> Vect a m -> Vect a (n + m);
27+app : Vect a n -> Vect a m -> Vect a (n + m);
28−vapp [] ys = ys;
28+app [] ys = ys;
29−vapp (x :: xs) ys = x :: vapp xs ys;
29+app (x :: xs) ys = x :: app xs ys;
30−
30+
31−vfilter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
31+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
32−vfilter p [] = ( _ ** [] );
32+filter p [] = ( _ ** [] );
33−vfilter p (x :: xs) with (vfilter p xs) {
33+filter p (x :: xs) with (filter p xs) {
34− vfilter p (x :: xs) | ( _ ** xs' )
34+ filter p (x :: xs) | ( _ ** xs' )
35 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
35 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
36}
36}
37
37
samples/interp.idr+5−5
@@ -13,12 +13,12 @@ using (G : Vect Ty n) {
13 Nil : Env Nil
13 Nil : Env Nil
14 | (::) : interpTy a -> Env G -> Env (a :: G);
14 | (::) : interpTy a -> Env G -> Env (a :: G);
15
15
16− envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);
16+ lookup : (i : Fin n) -> Env G -> interpTy (lookup i G);
17− envLookup fO (x :: xs) = x;
17+ lookup fO (x :: xs) = x;
18− envLookup (fS i) (x :: xs) = envLookup i xs;
18+ lookup (fS i) (x :: xs) = lookup i xs;
19
19
20 data Expr : Vect Ty n -> Ty -> Set where
20 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)
22 | Val : (x : Int) -> Expr G TyInt
22 | Val : (x : Int) -> Expr G TyInt
23 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
23 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
24 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
24 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
@@ -30,7 +30,7 @@ using (G : Vect Ty n) {
30 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
30 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
31
31
32 interp : Env G -> {static} Expr G t -> interpTy t;
32 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;
34 interp env (Val x) = x;
34 interp env (Val x) = x;
35 interp env (Lam sc) = \x => interp (x :: env) sc;
35 interp env (Lam sc) = \x => interp (x :: env) sc;
36 interp env (App f s) = (interp env f) (interp env s);
36 interp env (App f s) = (interp env f) (interp env s);
test/test001/test001.idr+5−5
@@ -13,12 +13,12 @@ using (G : Vect Ty n) {
13 Nil : Env Nil
13 Nil : Env Nil
14 | (::) : interpTy a -> Env G -> Env (a :: G);
14 | (::) : interpTy a -> Env G -> Env (a :: G);
15
15
16− envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);
16+ lookup : (i : Fin n) -> Env G -> interpTy (lookup i G);
17− envLookup fO (x :: xs) = x;
17+ lookup fO (x :: xs) = x;
18− envLookup (fS i) (x :: xs) = envLookup i xs;
18+ lookup (fS i) (x :: xs) = lookup i xs;
19
19
20 data Expr : Vect Ty n -> Ty -> Set where
20 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)
22 | Val : (x : Int) -> Expr G TyInt
22 | Val : (x : Int) -> Expr G TyInt
23 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
23 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
24 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
24 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
@@ -30,7 +30,7 @@ using (G : Vect Ty n) {
30 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
30 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
31
31
32 interp : Env G -> {static} Expr G t -> interpTy t;
32 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;
34 interp env (Val x) = x;
34 interp env (Val x) = x;
35 interp env (Lam sc) = \x => interp (x :: env) sc;
35 interp env (Lam sc) = \x => interp (x :: env) sc;
36 interp env (App f s) = (interp env f) (interp env s);
36 interp env (App f s) = (interp env f) (interp env s);