git.iko.soy/Idris-dev
on bbefa33 help sign in
Idris-dev/samples/tutorial/Interp.idr
71 lines 2.2 kB history raw
1module Main
3import Data.Vect
4import Data.Fin
6data Ty = TyInt | TyBool| TyFun Ty Ty
8interpTy : Ty -> Type
9interpTy TyInt = Int
10interpTy TyBool = Bool
11interpTy (TyFun s t) = interpTy s -> interpTy t
13using (G : Vect n Ty)
15 data Env : Vect n Ty -> Type where
16 Nil : Env Nil
17 (::) : interpTy a -> Env G -> Env (a :: G)
19 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
20 Stop : HasType FZ (t :: G) t
21 Pop : HasType k G t -> HasType (FS k) (u :: G) t
23 lookup : HasType i G t -> Env G -> interpTy t
24 lookup Stop (x :: xs) = x
25 lookup (Pop k) (x :: xs) = lookup k xs
27 data Expr : Vect n Ty -> Ty -> Type where
28 Var : HasType i G t -> Expr G t
29 Val : (x : Int) -> Expr G TyInt
30 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
31 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
32 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
33 Expr G c
34 If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a
36 interp : Env G -> (e : Expr G t) -> interpTy t
37 interp env (Var i) = lookup i env
38 interp env (Val x) = x
39 interp env (Lam sc) = \x => interp (x :: env) sc
40 interp env (App f s) = interp env f (interp env s)
41 interp env (Op op x y) = op (interp env x) (interp env y)
42 interp env (If x t e) = if interp env x then interp env t
43 else interp env e
45 eId : Expr G (TyFun TyInt TyInt)
46 eId = Lam (Var Stop)
48 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
49 eAdd = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
51 eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))
52 eEq = Lam (Lam (Op (==) (Var Stop) (Var (Pop Stop))))
54 eDouble : Expr G (TyFun TyInt TyInt)
55 eDouble = Lam (App (App eAdd (Var Stop)) (Var Stop))
57 fact : Expr G (TyFun TyInt TyInt)
58 fact = Lam (If (Op (==) (Var Stop) (Val 0))
59 (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1))) (Var Stop)))
61testFac : Int
62testFac = interp [] fact 4
64-- unitTestFac : so (interp [] fact 4 == 24)
65-- unitTestFac = oh
67main : IO ()
68main = do putStr "Enter a number: "
69 x <- getLine
70 printLn (interp [] fact (cast x))