@@ -1,13 +1,13 @@
1data Nat = O | S Nat;
1data Nat = O | S Nat;
3plus : Nat -> Nat -> Nat;
3plus : Nat -> Nat -> Nat;
4−plus O y = y;
4+plus O y = y;
5plus (S k) y = S (plus k y);
5plus (S k) y = S (plus k y);
7data Ty = TyNat | TyFun Ty Ty;
7data Ty = TyNat | TyFun Ty Ty;
9interpTy : Ty -> Set;
9interpTy : Ty -> Set;
10−interpTy TyNat = Nat;
10+interpTy TyNat = Nat;
11interpTy (TyFun s t) = interpTy s -> interpTy t;
11interpTy (TyFun s t) = interpTy s -> interpTy t;
13data Fin : Nat -> Set where
13data Fin : Nat -> Set where
@@ -21,8 +21,9 @@ data Vect : Set -> Nat -> Set where
21 | (::) : a -> Vect a k -> Vect a (S k);
21 | (::) : a -> Vect a k -> Vect a (S k);
23data Env : Vect Ty n -> Set where
23data Env : Vect Ty n -> Set where
24− Empty : Env VNil
24+ Empty : Env VNil
25+ | Extend : {xs : Vect Ty n} ->
25− | Extend : {xs : Vect Ty n} -> interpTy a -> Env xs -> Env (a :: xs);
26+ interpTy a -> Env xs -> Env (a :: xs);
27lookup : (i : Fin n) -> Vect a n -> a;
28lookup : (i : Fin n) -> Vect a n -> a;
28lookup fO (x :: xs) = x;
29lookup fO (x :: xs) = x;
@@ -43,15 +44,18 @@ data Expr : Vect Ty n -> Ty -> Set where
43 | App : {G : Vect Ty n} ->
44 | App : {G : Vect Ty n} ->
44 Expr G (TyFun a t) -> Expr G a -> Expr G t
45 Expr G (TyFun a t) -> Expr G a -> Expr G t
45 | Add : {G : Vect Ty n} ->
46 | Add : {G : Vect Ty n} ->
46− Expr G TyNat -> Expr G TyNat -> Expr G TyNat;
47+ Expr G TyNat -> Expr G TyNat -> Expr G TyNat
48+ | Bind : {G : Vect Ty n} ->
49+ Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
48interp : {G : Vect Ty n} ->
51interp : {G : Vect Ty n} ->
49 Env G -> Expr G t -> interpTy t;
52 Env G -> Expr G t -> interpTy t;
50−interp env (Var i) = envLookup i env;
53+interp env (Var i) = envLookup i env;
51−interp env (Val x) = x;
54+interp env (Val x) = x;
52−interp env (Lam sc) = \x => interp (Extend x env) sc;
55+interp env (Lam sc) = \x => interp (Extend x env) sc;
53−interp env (App f s) = (interp env f) (interp env s);
56+interp env (App f s) = (interp env f) (interp env s);
54−interp env (Add x y) = plus (interp env x) (interp env y);
57+interp env (Add x y) = plus (interp env x) (interp env y);
58+interp env (Bind v f) = interp env (f (interp env v));
56eAdd : {G : Vect Ty n} ->
60eAdd : {G : Vect Ty n} ->
57 Expr G (TyFun TyNat (TyFun TyNat TyNat));
61 Expr G (TyFun TyNat (TyFun TyNat TyNat));
@@ -65,5 +69,12 @@ eDouble' : {G : Vect Ty n} ->
65 Expr G (TyFun TyNat TyNat);
69 Expr G (TyFun TyNat TyNat);
66eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
70eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
72+eProg : {G : Vect Ty n} -> Expr G (TyFun TyNat TyNat);
73+eProg = Lam (Bind (App eDouble (Var fO))
74+ (\x => Bind (App eDouble (Var fO))
75+ (\y => Bind (App eDouble (Val x))
76+ (\z => App (App eAdd (Val y)) (Val z)))));
68test : Nat;
78test : Nat;
69test = interp Empty eAdd (S (S O)) (S (S O));
79test = interp Empty eAdd (S (S O)) (S (S O));