@@ -36,6 +36,14 @@ using (G : Vect Ty n)
3636 variable = Var
3737 index_first = stop
3838 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
3947
4048 interp : Env G -> {static} Expr G t -> interpTy t
4149 interp env (Var i) = lookup i env
@@ -55,36 +63,17 @@ using (G : Vect Ty n)
5563 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
5664 eAdd = expr (\x, y => Op (+) x y)
5765
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−
6166 eDouble : Expr G (TyFun TyInt TyInt)
6267 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
6668
6769 eFac : Expr G (TyFun TyInt TyInt)
68− eFac = expr (\x => If (Op (==) x (Val 0))
69− (Val 1)
70− (Op (*) (app 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
70+ eFac = expr (\x => IF Op (==) x (Val 0)
71+ THEN Val 1
72+ ELSE Op (*) [| eFac (Op (-) x (Val 1)) |] x)
8373
8474testFac : Int
8575testFac = interp [] eFac 4
8676
8777main : IO ()
88−main = do print test
89− print testFac
78+main = print testFac
9079