-
Notifications
You must be signed in to change notification settings - Fork 0
/
expr2.idr
50 lines (42 loc) · 1.48 KB
/
expr2.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
data Expr num = Val num
| Add (Expr num) (Expr num)
| Sub (Expr num) (Expr num)
| Mul (Expr num) (Expr num)
| Div (Expr num) (Expr num)
| Abs (Expr num)
eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)
Num ty => Num (Expr ty) where
(+) = Add
(*) = Mul
fromInteger = Val . fromInteger
Neg ty => Neg (Expr ty) where
negate x = 0 - x
(-) = Sub
abs = Abs
(Integral ty, Neg ty, Eq ty ) => Eq (Expr ty) where
(==) x y = eval x == eval y
Show ty => Show (Expr ty) where
show (Val x) = show x
show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"
show (Div x y) = "(" ++ show x ++ " / " ++ show y ++ ")"
show (Abs x) = "|" ++ show x ++ "|"
--https://github.com/idris-lang/Idris-dev/issues/3479
Cast ty ty where
cast = id
(Integral ty, Neg ty, Cast ty num) => Cast (Expr ty) num where
cast expr = cast (eval expr)
Functor Expr where
map func (Val x) = Val (func x)
map func (Add x y) = Add (map func x) (map func y)
map func (Sub x y) = Sub (map func x) (map func y)
map func (Mul x y) = Mul (map func x) (map func y)
map func (Div x y) = Div (map func x) (map func y)
map func (Abs x) = Abs (map func x)