598aca4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Update interp example and test001 to use namespaces and overloading names

commit598aca471d50bcecd0946fba90ea5dcfa3ac301e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 29 Nov 2011, 11:06 (15 years ago) parent9f65713

2 files changed+22−14

compare with master

unifiedsplit

samples/interp.idr+11−7 test/test001/test001.idr+11−7

samples/interp.idr+11−7

@@ -1,3 +1,5 @@

1+namespace main {

13data Ty = TyInt | TyBool| TyFun Ty Ty;

35interpTy : Ty -> Set;

@@ -8,12 +10,12 @@ interpTy (TyFun s t) = interpTy s -> interpTy t;

810using (G : Vect Ty n) {

911

1012 data Env : Vect Ty n -> Set where

11− Empty : Env VNil

12− | Extend : interpTy a -> Env G -> Env (a :: G);

13+ Nil : Env Nil

14+ | (::) : interpTy a -> Env G -> Env (a :: G);

1315

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

15− envLookup fO (Extend x xs) = x;

16− envLookup (fS i) (Extend x xs) = envLookup i xs;

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

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

1719

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

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

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

3032 interp : Env G -> [static] Expr G t -> interpTy t;

3133 interp env (Var i) = envLookup i env;

3234 interp env (Val x) = x;

33− interp env (Lam sc) = \x => interp (Extend x env) sc;

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

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

3537 interp env (Op op x y) = op (interp env x) (interp env y);

3638 interp env (Op' op x y) = op (interp env x) (interp env y);

@@ -67,10 +69,12 @@ using (G : Vect Ty n) {

6769}

6870

6971test : Int;

70−test = interp Empty eProg 2 2;

72+test = interp Nil eProg 2 2;

7173

7274testFac : Int;

73−testFac = interp Empty eFac 4;

75+testFac = interp Nil eFac 4;

76+

77+}

7478

7579main : IO ();

7680main = print testFac;

test/test001/test001.idr+11−7