git.iko.soy/Idris-dev
on master help sign in
Tidy up interpreter sample
fb3160eEdwin Brady
samples/interp.idr+12−23
compare with master
unifiedsplit
@@ -36,6 +36,14 @@ using (G : Vect Ty n)
36 variable = Var
36 variable = Var
37 index_first = stop
37 index_first = stop
38 index_next = pop
38 index_next = pop
39+
40+ (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
41+ (<$>) = \f, a => App f a
42+
43+ pure : Expr G a -> Expr G a
44+ pure = id
45+
46+ syntax IF [x] THEN [t] ELSE [e] = If x t e
39
47
40 interp : Env G -> {static} Expr G t -> interpTy t
48 interp : Env G -> {static} Expr G t -> interpTy t
41 interp env (Var i) = lookup i env
49 interp env (Var i) = lookup i env
@@ -55,36 +63,17 @@ using (G : Vect Ty n)
55 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
63 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
56 eAdd = expr (\x, y => Op (+) x y)
64 eAdd = expr (\x, y => Op (+) x y)
57
65
58−-- eDouble : Expr G (TyFun TyInt TyInt)
59−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
60−
61 eDouble : Expr G (TyFun TyInt TyInt)
66 eDouble : Expr G (TyFun TyInt TyInt)
62 eDouble = expr (\x => App (App eAdd x) (Var stop))
67 eDouble = expr (\x => App (App eAdd x) (Var stop))
63−
64− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
65− app = \f, a => App f a
66
68
67 eFac : Expr G (TyFun TyInt TyInt)
69 eFac : Expr G (TyFun TyInt TyInt)
68− eFac = expr (\x => If (Op (==) x (Val 0))
70+ eFac = expr (\x => IF Op (==) x (Val 0)
69− (Val 1)
71+ THEN Val 1
70− (Op (*) (app eFac (Op (-) x (Val 1))) x))
72+ ELSE Op (*) [| eFac (Op (-) x (Val 1)) |] x)
71−
72− -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
73−
74− eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
75− eProg = Lam (Lam (Bind (App eDouble (Var (pop stop)))
76− (\x => Bind (App eDouble (Var stop))
77− (\y => Bind (App eDouble (Val x))
78− (\z => App (App eAdd (Val y)) (Val z))))))
79−
80−
81−test : Int
82−test = interp [] eProg 2 2
83
73
84testFac : Int
74testFac : Int
85testFac = interp [] eFac 4
75testFac = interp [] eFac 4
86
76
87main : IO ()
77main : IO ()
88−main = do print test
89− print testFac
78+main = print testFac
90
79