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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
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 {#Char},
instance toString Int, instance toString Char
import _SystemArray
// Evaluation utilities
instance eval Int Int where eval _ i _ = i
instance eval Var Int where eval _ v st = (toState 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 (a1 >= a2) st = eval m (a2 <= a1) st
eval m (a1 < a2) st = ltI (eval m a1 st) (eval m a2 st)
eval m (a1 > a2) st = eval m (a2 < a1) st
eval m (~ b) st = not (eval m b st)
eval m (b1 /\ b2) st = eval m b1 st && eval m b2 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 (toState st)) in st`
eval NS stm st = (tree stm (toState st)).result
// Natural Semantics
tree :: Stm st -> DerivTree | toState st
tree stm stv = tree` stm (toState stv)
where
tree` :: Stm State -> DerivTree
tree` stm=:Skip st = dTree stm st [] st
tree` stm=:(v:=a) st
= let e = eval NS a st in dTree stm st [] (\w->if (eqV v w) e (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 st -> DerivSeq | toState st
seq stm stv = let st = toState stv in case step stm st of
(Done st`) = [NDone stm 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 = let e = eval SOS a st in Done (\w->if (eqV v w) e (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
// State utilities
instance toState State where toState st = st
instance toState CharState where toState cst = \(Var v) -> cst v
instance toState (Var -> Int) where toState st = st
// String utilities
(<+) infixr 5 :: a b -> String | toString a & toString b
(<+) a b = toString a +++ toString b
instance toString ArithExpr
where
toString (a1 + a2) = a1 <+ "+" <+ a2
toString (a1 - a2) = a1 <+ "-" <+ a2
toString (a1 * a2) = "(" <+ a1 <+ "*" <+ a2 <+ ")"
instance toString Bool where toString True = "true"; toString False = "false"
instance toString BoolExpr
where
toString (a1 == a2) = a1 <+ "=" <+ a2
toString (a1 <= a2) = a1 <+ "<=" <+ a2
toString (a1 >= a2) = a1 <+ ">=" <+ a2
toString (a1 < a2) = a1 <+ "<" <+ a2
toString (a1 > a2) = a1 <+ ">" <+ a2
toString (~ b) = "~(" <+ toString b <+ ")"
toString (b1 /\ b2) = "(" <+ b1 <+ "/\\" <+ b2 <+ ")"
toString (b1 \/ b2) = "(" <+ b1 <+ "\\/" <+ b2 <+ ")"
instance toString Stm
where
toString Skip = "skip"
toString (s1 :. s2) = s1 <+ "; " <+ s2
toString (v := a) = v <+ ":=" <+ a
toString (While b s) = "while " <+ b <+ " do " <+ parens s
toString (If b s1 s2) = "if "<+b<+" then "<+parens s1<+" else "<+parens s2
parens :: Stm -> String
parens (s1 :. s2) = "(" <+ s1 <+ "; " <+ s2 <+ ")"
parens stm = toString stm
instance toString Var where toString (Var v) = {v}
instance toString DerivTree
where
toString t = toS 0 t
where
toS :: Int DerivTree -> String
toS i {stm,children=[]} = pad i <+ stm <+ "\n"
toS i {stm,children} = pad i <+ "(" <+ stm <+ "\n" <+
concat (map (toS (addI i 1)) children) <+ pad i <+ ")\n"
concat :: [a] -> String | toString a
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" [stm \\ (NDone stm _) <- seq]
where
join :: a [b] -> String | toString a & toString b
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
}
eqV :: !Var !Var -> Bool
eqV (Var a) (Var b) = eqC a b
|
