git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/samples/interp-alt.idr
81 lines 2.7 kB history raw
1module main
3data Ty = TyInt | TyBool| TyFun Ty Ty
5interpTy : Ty -> Type
6interpTy TyInt = Int
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
10using (G : Vect n Ty)
12 data Env : Vect n Ty -> Type where
13 Nil : Env Nil
14 (::) : interpTy a -> Env G -> Env (a :: G)
16-- data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17-- stop : HasType FZ (t :: G) t
18-- pop : HasType k G t -> HasType (FS k) (u :: G) t
20 lookup : (i:Fin n) -> Env G -> interpTy (index i G)
21 lookup FZ (x :: xs) = x
22 lookup (FS i) (x :: xs) = lookup i xs
24 data Expr : Vect n Ty -> Ty -> Type where
25 Var : (i : Fin n) -> Expr G (index i G)
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 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
34 interp : Env G -> {static} Expr G t -> interpTy t
35 interp env (Var i) = lookup i env
36 interp env (Val x) = x
37 interp env (Lam sc) = \x => interp (x :: env) sc
38 interp env (App f s) = (interp env f) (interp env s)
39 interp env (Op op x y) = op (interp env x) (interp env y)
40 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)
41 interp env (Bind v f) = interp env (f (interp env v))
43 eId : Expr G (TyFun TyInt TyInt)
44 eId = Lam (Var FZ)
46 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
47 eTEST = Lam (Lam (Var (FS FZ)))
49 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
50 eAdd = Lam (Lam (Op prim__addInt (Var FZ) (Var (FS FZ))))
52-- eDouble : Expr G (TyFun TyInt TyInt)
53-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var FZ) (Var (FS FZ))))) (Var FZ)) (Var FZ))
55 eDouble : Expr G (TyFun TyInt TyInt)
56 eDouble = Lam (App (App eAdd (Var FZ)) (Var FZ))
58 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
59 app = \f, a => App f a
61 eFac : Expr G (TyFun TyInt TyInt)
62 eFac = Lam (If (Op (==) (Var FZ) (Val 0))
63 (Val 1) (Op (*) (app eFac (Op (-) (Var FZ) (Val 1))) (Var FZ)))
65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
67 eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
68 eProg = Lam (Lam (Bind (App eDouble (Var (FS FZ)))
69 (\x => Bind (App eDouble (Var FZ))
70 (\y => Bind (App eDouble (Val x))
71 (\z => App (App eAdd (Val y)) (Val z))))))
73test : Int
74test = interp [] eProg 2 2
76testFac : Int
77testFac = interp [] eFac 4
79main : IO ()
80main = do printLn test
81 printLn testFac