git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/samples/interp.idr
92 lines 2.6 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 : HasType i G t -> Env G -> interpTy t
21 lookup stop (x :: xs) = x
22 lookup (pop k) (x :: xs) = lookup k xs
24 data Expr : Vect n Ty -> Ty -> Type 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 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
34 dsl expr
35 lambda = Lam
36 variable = Var
37 index_first = stop
38 index_next = pop
40 (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
41 (<$>) = \f, a => App f a
43 pure : Expr G a -> Expr G a
44 pure = id
46 syntax IF [x] THEN [t] ELSE [e] = If x t e
48 (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
49 (==) = Op (==)
51 (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
52 (<) = Op (<)
54 instance Num (Expr G TyInt) where
55 (+) x y = Op (+) x y
56 (-) x y = Op (-) x y
57 (*) x y = Op (*) x y
59 abs x = IF (x < 0) THEN (-x) ELSE x
61 fromInteger = Val . fromInteger
63 interp : Env G -> {static} Expr G t -> interpTy t
64 interp env (Var i) = lookup i env
65 interp env (Val x) = x
66 interp env (Lam sc) = \x => interp (x :: env) sc
67 interp env (App f s) = (interp env f) (interp env s)
68 interp env (Op op x y) = op (interp env x) (interp env y)
69 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)
70 interp env (Bind v f) = interp env (f (interp env v))
72 eId : Expr G (TyFun TyInt TyInt)
73 eId = expr (\x => x)
75 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
76 eTEST = expr (\x, y => y)
78 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
79 eAdd = expr (\x, y => Op (+) x y)
81 eDouble : Expr G (TyFun TyInt TyInt)
82 eDouble = expr (\x => App (App eAdd x) (Var stop))
84 eFac : Expr G (TyFun TyInt TyInt)
85 eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)
87testFac : Int
88testFac = interp [] eFac 4
90main : IO ()
91main = print testFac