@@ -0,0 +1,68 @@
1+module main;
2+
3+data Ty = TyInt | TyBool| TyFun Ty Ty;
4+
5+interpTy : Ty -> Set;
6+interpTy TyInt = Int;
7+interpTy TyBool = Bool;
8+interpTy (TyFun s t) = interpTy s -> interpTy t;
9+
10+using (G : Vect Ty n) {
11+
12+ data Env : Vect Ty n -> Set where
13+ Nil : Env Nil
14+ | (::) : interpTy a -> Env G -> Env (a :: G);
15+
16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
17+ stop : HasType fO (t :: G) t
18+ | pop : HasType k G t -> HasType (fS k) (u :: G) t;
19+
20+ lookup : HasType i G t -> Env G -> interpTy t;
21+ lookup stop (x :: xs) = x;
22+ lookup (pop k) (x :: xs) = lookup k xs;
23+
24+ data Expr : Vect Ty n -> Ty -> Set where
25+ Var : HasType i G t -> Expr G t
26+ | Val : (x : Int) -> Expr G TyInt
27+ | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
28+ | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
29+ | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
30+ Expr G c
31+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;
32+
33+ interp : Env G -> {static} Expr G t -> interpTy t;
34+ interp env (Var i) = lookup i env;
35+ interp env (Val x) = x;
36+ interp env (Lam sc) = \x => interp (x :: env) sc;
37+ interp env (App f s) = (interp env f) (interp env s);
38+ interp env (Op op x y) = op (interp env x) (interp env y);
39+ interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
40+
41+ eId : Expr G (TyFun TyInt TyInt);
42+ eId = Lam (Var stop);
43+
44+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
45+ eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))));
46+
47+ eDouble : Expr G (TyFun TyInt TyInt);
48+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
49+
50+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
51+ app = \f, a => App f a;
52+
53+ fact : Expr G (TyFun TyInt TyInt);
54+ fact = Lam (If (Op (==) (Var stop) (Val 0))
55+ (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)));
56+
57+}
58+
59+testFac : Int;
60+testFac = interp [] fact 4;
61+
62+main : IO ();
63+main = do { putStr "Enter a number: ";
64+ x <- getLine;
65+ print (interp [] fact (prim__strToInt x));
66+ };
67+
68+