git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/misc/interp.idr
100 lines 2.8 kB history raw
1module Main
3import Data.Vect
5%language DSLNotation
7data Ty = TyInt | TyBool | TyFun Ty Ty
9interpTy : Ty -> Type
10interpTy TyInt = Int
11interpTy TyBool = Bool
12interpTy (TyFun s t) = interpTy s -> interpTy t
14using (G : Vect n Ty)
16 data Env : Vect n Ty -> Type where
17 Nil : Env Nil
18 (::) : interpTy a -> Env G -> Env (a :: G)
20 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
21 Stop : HasType FZ (t :: G) t
22 Pop : HasType k G t -> HasType (FS k) (u :: G) t
24 lookup : HasType i G t -> Env G -> interpTy t
25 lookup Stop (x :: xs) = x
26 lookup (Pop k) (x :: xs) = lookup k xs
28 data Expr : Vect n Ty -> Ty -> Type where
29 Var : HasType i G t -> Expr G t
30 Val : (x : Int) -> Expr G TyInt
31 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
32 App : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t
33 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
34 Expr G c
35 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
36 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
38 lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
39 lam_ _ = Lam
41 dsl expr
42 lambda = lam_
43 variable = Var
44 index_first = Stop
45 index_next = Pop
47 (<*>) : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t
48 (<*>) = \f, a => App f a
50 pure : Expr G a -> Expr G a
51 pure = id
53 syntax IF [x] THEN [t] ELSE [e] = If x t e
55 (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
56 (==) = Op (==)
58 (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
59 (<) = Op (<)
61 implementation Num (Expr G TyInt) where
62 (+) x y = Op (+) x y
63 (*) x y = Op (*) x y
65 fromInteger = Val . fromInteger
67 implementation Neg (Expr G TyInt) where
68 (-) x y = Op (-) x y
69 abs x = IF (x < 0) THEN (-x) ELSE x
70 negate x = Op (-) 0 x
72 interp : Env G -> Expr G t -> interpTy t
73 interp env (Var i) = lookup i env
74 interp env (Val x) = x
75 interp env (Lam sc) = \x => interp (x :: env) sc
76 interp env (App f s) = (interp env f) (interp env s)
77 interp env (Op op x y) = op (interp env x) (interp env y)
78 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)
79 interp env (Bind v f) = interp env (f (interp env v))
81 eId : Expr G (TyFun TyInt TyInt)
82 eId = expr (\x => x)
84 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
85 eTEST = expr (\x, y => y)
87 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
88 eAdd = expr (\x, y => Op (+) x y)
90 eDouble : Expr G (TyFun TyInt TyInt)
91 eDouble = expr (\x => App (App eAdd x) (Var Stop))
93 eFac : Expr G (TyFun TyInt TyInt)
94 eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)
96testFac : Int
97testFac = interp [] eFac 4
99main : IO ()
100main = printLn testFac