@@ -1,5 +1,9 @@
11module Main
22
3+import Data.Vect
4+
5+%language DSLNotation
6+
37data Ty = TyInt | TyBool | TyFun Ty Ty
48
59interpTy : Ty -> Type
@@ -14,30 +18,33 @@ using (G : Vect n Ty)
1418 (::) : interpTy a -> Env G -> Env (a :: G)
1519
1620 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
21+ Stop : HasType FZ (t :: G) t
22+ Pop : HasType k G t -> HasType (FS k) (u :: G) t
1923
2024 lookup : HasType i G t -> Env G -> interpTy t
21− lookup stop (x :: xs) = x
22− lookup (pop k) (x :: xs) = lookup k xs
25+ lookup Stop (x :: xs) = x
26+ lookup (Pop k) (x :: xs) = lookup k xs
2327
2428 data Expr : Vect n Ty -> Ty -> Type where
2529 Var : HasType i G t -> Expr G t
2630 Val : (x : Int) -> Expr G TyInt
2731 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
28− App : Expr G (TyFun a t) -> Expr G a -> Expr G t
32+ App : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t
2933 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
3034 Expr G c
3135 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
3236 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
3337
38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
39+ lam_ _ = Lam
40+
3441 dsl expr
35− lambda = Lam
42+ lambda = lam_
3643 variable = Var
37− index_first = stop
38− index_next = pop
44+ index_first = Stop
45+ index_next = Pop
3946
40− (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
47+ (<*>) : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t
4148 (<*>) = \f, a => App f a
4249
4350 pure : Expr G a -> Expr G a
@@ -53,14 +60,16 @@ using (G : Vect n Ty)
5360
5461 implementation Num (Expr G TyInt) where
5562 (+) x y = Op (+) x y
56− (-) x y = Op (-) x y
5763 (*) x y = Op (*) x y
5864
59− abs x = IF (x < 0) THEN (-x) ELSE x
60−
6165 fromInteger = Val . fromInteger
66+
67+ implementation Neg (Expr G TyInt) where
68+ (-) x y = Op (-) x y
69+ abs x = IF (x < 0) THEN (-x) ELSE x
70+ negate x = Op (-) 0 x
6271
63− interp : Env G -> {static} Expr G t -> interpTy t
72+ interp : Env G -> Expr G t -> interpTy t
6473 interp env (Var i) = lookup i env
6574 interp env (Val x) = x
6675 interp env (Lam sc) = \x => interp (x :: env) sc
@@ -79,7 +88,7 @@ using (G : Vect n Ty)
7988 eAdd = expr (\x, y => Op (+) x y)
8089
8190 eDouble : Expr G (TyFun TyInt TyInt)
82− eDouble = expr (\x => App (App eAdd x) (Var stop))
91+ eDouble = expr (\x => App (App eAdd x) (Var Stop))
8392
8493 eFac : Expr G (TyFun TyInt TyInt)
8594 eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)