@@ -1,13 +1,13 @@
11data Nat = O | S Nat;
22
33plus : Nat -> Nat -> Nat;
4−plus O y = y;
4+plus O y = y;
55plus (S k) y = S (plus k y);
66
77data Ty = TyNat | TyFun Ty Ty;
88
99interpTy : Ty -> Set;
10−interpTy TyNat = Nat;
10+interpTy TyNat = Nat;
1111interpTy (TyFun s t) = interpTy s -> interpTy t;
1212
1313data Fin : Nat -> Set where
@@ -21,8 +21,9 @@ data Vect : Set -> Nat -> Set where
2121 | (::) : a -> Vect a k -> Vect a (S k);
2222
2323data Env : Vect Ty n -> Set where
24− Empty : Env VNil
25− | Extend : {xs : Vect Ty n} -> interpTy a -> Env xs -> Env (a :: xs);
24+ Empty : Env VNil
25+ | Extend : {xs : Vect Ty n} ->
26+ interpTy a -> Env xs -> Env (a :: xs);
2627
2728lookup : (i : Fin n) -> Vect a n -> a;
2829lookup fO (x :: xs) = x;
@@ -43,15 +44,18 @@ data Expr : Vect Ty n -> Ty -> Set where
4344 | App : {G : Vect Ty n} ->
4445 Expr G (TyFun a t) -> Expr G a -> Expr G t
4546 | 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;
4750
4851interp : {G : Vect Ty n} ->
4952 Env G -> Expr G t -> interpTy t;
50−interp env (Var i) = envLookup i env;
51−interp env (Val x) = x;
52−interp env (Lam sc) = \x => interp (Extend x env) sc;
53−interp env (App f s) = (interp env f) (interp env s);
54−interp env (Add x y) = plus (interp env x) (interp env y);
53+interp env (Var i) = envLookup i env;
54+interp env (Val x) = x;
55+interp env (Lam sc) = \x => interp (Extend x env) sc;
56+interp env (App f s) = (interp env f) (interp env s);
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));
5559
5660eAdd : {G : Vect Ty n} ->
5761 Expr G (TyFun TyNat (TyFun TyNat TyNat));
@@ -65,5 +69,12 @@ eDouble' : {G : Vect Ty n} ->
6569 Expr G (TyFun TyNat TyNat);
6670eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
6771
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)))));
77+
6878test : Nat;
6979test = interp Empty eAdd (S (S O)) (S (S O));
80+