git.iko.soy/Idris-dev
on df49a2a help sign in
Idris-dev/samples/interp.idr
77 lines 2.7 kB history raw
1data Ty = TyInt | TyBool| TyFun Ty Ty;
3interpTy : Ty -> Set;
4interpTy TyInt = Int;
5interpTy TyBool = Bool;
6interpTy (TyFun s t) = interpTy s -> interpTy t;
8using (G : Vect Ty n) {
10 data Env : Vect Ty n -> Set where
11 Empty : Env VNil
12 | Extend : interpTy a -> Env G -> Env (a :: G);
14 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;
18 data Expr : Vect Ty n -> Ty -> Set where
19 Var : (i : Fin n) -> Expr G (vlookup i G)
20 | Val : (x : Int) -> Expr G TyInt
21 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
22 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
23 | Op : (Int -> Int -> interpTy c) ->
24 Expr G TyInt -> Expr G TyInt -> Expr G c
25 | Op' : (interpTy a -> interpTy b -> interpTy c) ->
26 Expr G a -> Expr G b -> Expr G c
27 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
28 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
30 interp : Env G -> [static] Expr G t -> interpTy t;
31 interp env (Var i) = envLookup i env;
32 interp env (Val x) = x;
33 interp env (Lam sc) = \x => interp (Extend x env) sc;
34 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);
36 interp env (Op' op x y) = op (interp env x) (interp env y);
37 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
38 interp env (Bind v f) = interp env (f (interp env v));
40 eId : Expr G (TyFun TyInt TyInt);
41 eId = Lam (Var fO);
43 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
44 eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));
46-- eDouble : Expr G (TyFun TyInt TyInt);
47-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
49 eDouble : Expr G (TyFun TyInt TyInt);
50 eDouble = Lam (App (App eAdd (Var fO)) (Var fO));
52 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
53 app = \f, a => App f a;
55 eFac : Expr G (TyFun TyInt TyInt);
56 eFac = Lam (If (Op (==) (Var fO) (Val 0))
57 (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));
59 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
61 eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
62 eProg = Lam (Lam
63 (Bind (App eDouble (Var (fS fO)))
64 (\x => Bind (App eDouble (Var fO))
65 (\y => Bind (App eDouble (Val x))
66 (\z => App (App eAdd (Val y)) (Val z))))));
69test : Int;
70test = interp Empty eProg 2 2;
72testFac : Int;
73testFac = interp Empty eFac 4;
75main : IO ();
76main = print testFac;