git.iko.soy/Idris-dev
on master help sign in
Fix 'interp' sample
55a8e1fEdwin Brady
samples/misc/interp.idr+23−14
compare with master
unifiedsplit
@@ -1,5 +1,9 @@
1module Main
1module Main
2
2
3+import Data.Vect
4+
5+%language DSLNotation
6+
3data Ty = TyInt | TyBool | TyFun Ty Ty
7data Ty = TyInt | TyBool | TyFun Ty Ty
4
8
5interpTy : Ty -> Type
9interpTy : Ty -> Type
@@ -14,30 +18,33 @@ using (G : Vect n Ty)
14 (::) : interpTy a -> Env G -> Env (a :: G)
18 (::) : interpTy a -> Env G -> Env (a :: G)
15
19
16 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
20 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17− stop : HasType FZ (t :: G) t
21+ Stop : HasType FZ (t :: G) t
18− pop : HasType k G t -> HasType (FS k) (u :: G) t
22+ Pop : HasType k G t -> HasType (FS k) (u :: G) t
19
23
20 lookup : HasType i G t -> Env G -> interpTy t
24 lookup : HasType i G t -> Env G -> interpTy t
21− lookup stop (x :: xs) = x
25+ lookup Stop (x :: xs) = x
22− lookup (pop k) (x :: xs) = lookup k xs
26+ lookup (Pop k) (x :: xs) = lookup k xs
23
27
24 data Expr : Vect n Ty -> Ty -> Type where
28 data Expr : Vect n Ty -> Ty -> Type where
25 Var : HasType i G t -> Expr G t
29 Var : HasType i G t -> Expr G t
26 Val : (x : Int) -> Expr G TyInt
30 Val : (x : Int) -> Expr G TyInt
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
31 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
29 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
33 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
30 Expr G c
34 Expr G c
31 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
35 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
32 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
36 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
33
37
38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
39+ lam_ _ = Lam
40+
34 dsl expr
41 dsl expr
35− lambda = Lam
42+ lambda = lam_
36 variable = Var
43 variable = Var
37− index_first = stop
44+ index_first = Stop
38− index_next = pop
45+ index_next = Pop
39
46
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
41 (<*>) = \f, a => App f a
48 (<*>) = \f, a => App f a
42
49
43 pure : Expr G a -> Expr G a
50 pure : Expr G a -> Expr G a
@@ -53,14 +60,16 @@ using (G : Vect n Ty)
53
60
54 implementation Num (Expr G TyInt) where
61 implementation Num (Expr G TyInt) where
55 (+) x y = Op (+) x y
62 (+) x y = Op (+) x y
56− (-) x y = Op (-) x y
57 (*) x y = Op (*) x y
63 (*) x y = Op (*) x y
58
64
59− abs x = IF (x < 0) THEN (-x) ELSE x
60−
61 fromInteger = Val . fromInteger
65 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
62
71
63− interp : Env G -> {static} Expr G t -> interpTy t
72+ interp : Env G -> Expr G t -> interpTy t
64 interp env (Var i) = lookup i env
73 interp env (Var i) = lookup i env
65 interp env (Val x) = x
74 interp env (Val x) = x
66 interp env (Lam sc) = \x => interp (x :: env) sc
75 interp env (Lam sc) = \x => interp (x :: env) sc
@@ -79,7 +88,7 @@ using (G : Vect n Ty)
79 eAdd = expr (\x, y => Op (+) x y)
88 eAdd = expr (\x, y => Op (+) x y)
80
89
81 eDouble : Expr G (TyFun TyInt TyInt)
90 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))
83
92
84 eFac : Expr G (TyFun TyInt TyInt)
93 eFac : Expr G (TyFun TyInt TyInt)
85 eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)
94 eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)