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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
implementation module While
from StdBool import not, &&, ||
from StdList import hd, last, map, take
from StdMisc import abort
from StdOverloaded import class +++(..), class toString(..)
from StdString import instance +++ {#Char},
instance toString Int, instance toString Bool, instance toString Char
import _SystemArray
// Evaluation utilities
instance eval Int Int where eval _ i _ = i
instance eval Var Int where eval _ v st = st v
instance eval ArithExpr Int
where
eval m (a1 + a2) st = addI (eval m a1 st) (eval m a2 st)
eval m (a1 - a2) st = subI (eval m a1 st) (eval m a2 st)
eval m (a1 * a2) st = mulI (eval m a1 st) (eval m a2 st)
instance eval Bool Bool where eval _ b _ = b
instance eval BoolExpr Bool
where
eval m (a1 == a2) st = eqI (eval m a1 st) (eval m a2 st)
eval m (a1 <= a2) st = ltI (eval m a1 st) (eval m a2 st)
|| eqI (eval m a1 st) (eval m a2 st)
eval m (~ b) st = not (eval m b st)
eval m (b1 /\ b2) st = eval m b1 st && eval m b2 st
instance eval Stm State
where
eval SOS stm st = let (Done st`) = last (seq stm st) in st`
eval NS stm st = (tree stm st).result
// Natural Semantics
tree :: Stm State -> DerivTree
tree stm=:Skip st = dTree stm st [] st
tree stm=:(v:=a) st = dTree stm st [] (\w->if (eqC v w) (eval NS a st) (st w))
tree stm=:(s1 :. s2) st = dTree stm st [t1,t2] t2.result
where t1 = tree s1 st; t2 = tree s2 t1.result
tree stm=:(If b s1 s2) st = dTree stm st [t] t.result
where t = tree (if (eval NS b st) s1 s2) st
tree stm=:(While b s) st
| eval NS b st = dTree stm st [t1,t2] t2.result
| otherwise = dTree stm st [] st
where t1 = tree s st; t2 = tree stm t1.result
// Records are too much typing
dTree :: Stm State [DerivTree] State -> DerivTree
dTree stm st ts r = {stm=stm, state=st, children=ts, result=r}
// Structural Operational Semantics
seq :: Stm State -> DerivSeq
seq stm st = case step stm st of (Done st) = [Done st]
(NDone stm st) = [NDone stm st : seq stm st]
where
step :: Stm State -> DerivSeqNode
step Skip st = Done st
step (v := a) st = Done (\w->if (eqC v w) (eval SOS a st) (st w))
step (s1 :. s2) st = case step s1 st of
seqe=:(NDone s1` st`) = NDone (s1` :. s2) st`
(Done st`) = NDone s2 st`
step (If b s1 s2) st = NDone (if (eval SOS b st) s1 s2) st
step stm=:(While b s) st = NDone (If b (s:.stm) Skip) st
// String utilities
instance toString ArithExpr
where
toString (a1 + a2) = toString a1 +++ "+" +++ toString a2
toString (a1 - a2) = toString a1 +++ "-" +++ toString a2
toString (a1 * a2) = toString a1 +++ "*" +++ toString a2
instance toString BoolExpr
where
toString (a1 == a2) = toString a1 +++ "=" +++ toString a2
toString (a1 <= a2) = toString a1 +++ "<=" +++ toString a2
toString (~ b) = "~" +++ toString b
toString (b1 /\ b2) = toString b1 +++ "/\\" +++ toString b2
instance toString Stm
where
toString Skip = "skip"
toString (s1 :. s2) = toString s1 +++ "; " +++ toString s2
toString (v := a) = {v} +++ ":=" +++ toString a
toString (If b s1 s2) = "if " +++ toString b +++ " then " +++ toString s1 +++ " else " +++ toString s2
toString (While b s) = "while " +++ toString b +++ " do " +++ toString s +++ " done"
instance toString DerivTree
where
toString t = toS 0 t
where
toS :: Int DerivTree -> String
toS i {stm,children=[]} = pad i +++ toString stm +++ "\n"
toS i {stm,children} = pad i +++ "(" +++ toString stm +++ "\n" +++
concat (map (toS (addI i 1)) children) +++ pad i +++ ")\n"
concat :: [String] -> String
concat [] = ""
concat [s:ss] = s +++ concat ss
pad :: Int -> String
pad 0 = ""
pad i = pad (subI i 1) +++ " "
instance toString DerivSeq
where
toString seq = join "\n" (map toString [stm \\ (NDone stm _) <- seq])
where
join :: String [String] -> String
join _ [] = ""
join g [s:ss] = s +++ g +++ join g ss
// Low end
addI :: !Int !Int -> Int
addI a b = code inline {
addI
}
subI :: !Int !Int -> Int
subI a b = code inline {
subI
}
mulI :: !Int !Int -> Int
mulI a b = code inline {
mulI
}
eqI :: !Int !Int -> Bool
eqI a b = code inline {
eqI
}
ltI :: !Int !Int -> Bool
ltI a b = code inline {
ltI
}
eqC :: !Char !Char -> Bool
eqC a b = code inline {
eqC
}
|
