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

git.iko.soy/Idris-dev

on master help sign in

Update interp example and test001 to use namespaces and overloading names

598aca4Edwin Brady15 years ago

samples/interp.idr+11−7

compare with master

unifiedsplit

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

1+namespace main {

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

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

3interpTy : Ty -> Set;

5interpTy : Ty -> Set;

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

8using (G : Vect Ty n) {

10using (G : Vect Ty n) {

10 data Env : Vect Ty n -> Set where

12 data Env : Vect Ty n -> Set where

11− Empty : Env VNil

13+ Nil : Env Nil

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

32 interp env (Val x) = x;

34 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;

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

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

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

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

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

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

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

67}

69}

69test : Int;

71test : Int;

70−test = interp Empty eProg 2 2;

72+test = interp Nil eProg 2 2;

72testFac : Int;

74testFac : Int;

73−testFac = interp Empty eFac 4;

75+testFac = interp Nil eFac 4;

76+

77+}

75main : IO ();

79main : IO ();

76main = print testFac;

80main = print testFac;

test/test001/test001.idr+11−7