git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/examples/interp.idr
71 lines 2.2 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
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 eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))
49 eEq = Lam (Lam (Op (==) (Var stop) (Var (pop stop))))
51 eDouble : Expr G (TyFun TyInt TyInt)
52 eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
54 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
55 app = \f, a => App f a
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
64unitTestFac : so (interp [] fact 4 == 24)
65unitTestFac = oh
67main : IO ()
68main = do putStr "Enter a number: "
69 x <- getLine
70 print (interp [] fact (cast x))