-
Notifications
You must be signed in to change notification settings - Fork 0
/
ArithEval.lhs
49 lines (34 loc) · 1.47 KB
/
ArithEval.lhs
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
> module ArithEval where
> import Terms
Homework 3 Derick Falk
isNumerical
> isNumerical :: Term t -> Bool
> isNumerical t = case t of
> Z -> True
> Succ(t) -> isNumerical t
> _ -> False
isVal
> isVal :: Term t -> Bool
> isVal t = case t of
> T -> True
> F -> True
> t -> isNumerical t
> eval1 :: Term t -> Maybe (Term t)
> eval1 (If t1 t2 t3) | t1 == T = Just t2
> | t1 == F = Just t3
> | (eval1 t1) == Nothing = Nothing
> | otherwise = let Just t1' = eval1 t1 in (Just (If t1' t2 t3))
> eval1 (Succ t) | t == Z = Nothing
> | (eval1 t) == Nothing = Nothing
> | otherwise = let Just t' = eval1 t in Just (Succ t')
> eval1 (Prd t) = case t of
> Z -> Just Z
> (Succ t) -> if (isNumerical t) then Just t else Nothing
> t -> let Just t' = eval1 t in (Just (Prd t'))
> eval1 (IsZ t) | t == Z = Just T
> | t == Succ(t) = if (isNumerical t) then Just F else Nothing
> | (eval1 t) == Nothing = Nothing
> | otherwise = let Just t' = eval1 t in Just (IsZ t')
> eval1 _ = Nothing
Big step style
> eval t = let t1 = eval1 t in if t1 == Nothing then t else let Just t2 = t1 in eval t2