git.iko.soy/Idris-dev
on 496cf41 help sign in
Idris-dev/tutorial/examples/interp.idr
68 lines 2.1 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 Ty n)
12 data Env : Vect Ty n -> Type where
13 Nil : Env Nil
14 (::) : interpTy a -> Env G -> Env (a :: G)
16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
17 stop : HasType fO (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 Ty n -> 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
33 interp : Env G -> {static} Expr G t -> interpTy t
34 interp env (Var i) = lookup i env
35 interp env (Val x) = x
36 interp env (Lam sc) = \x => interp (x :: env) sc
37 interp env (App f s) = interp env f (interp env s)
38 interp env (Op op x y) = op (interp env x) (interp env y)
39 interp env (If x t e) = if interp env x then interp env t
40 else interp env e
42 eId : Expr G (TyFun TyInt TyInt)
43 eId = Lam (Var stop)
45 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
46 eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
48 eDouble : Expr G (TyFun TyInt TyInt)
49 eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
51 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
52 app = \f, a => App f a
54 fact : Expr G (TyFun TyInt TyInt)
55 fact = Lam (If (Op (==) (Var stop) (Val 0))
56 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))
58testFac : Int
59testFac = interp [] fact 4
61unitTestFac : so (interp [] fact 4 == 24)
62unitTestFac = oh
64main : IO ()
65main = do putStr "Enter a number: "
66 x <- getLine
67 print (interp [] fact (cast x))