blob: 244045748748bed552f3296ae484f549523621bb (
plain) (
blame)
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
|
definition module While
from StdOverloaded import class toString
:: Semantics = NS // Natural Semantics
| SOS // Structural Operational Semantics
// evaluate @2 in state @3 according to @1
class eval a b :: Semantics a st -> b | toState st
instance eval Stm State
instance eval Int Int
instance eval Var Int
instance eval ArithExpr Int
instance eval Bool Bool
instance eval BoolExpr Bool
class toState a :: a -> State
instance toState State
instance toState CharState
instance toString ArithExpr
instance toString Bool
instance toString BoolExpr
instance toString Stm
instance toString Var
instance toString DerivTree
instance toString DerivSeq
// Syntax
:: Stm = Skip // Skip
| (:.) infixr 1 Stm Stm // Composition
| E.a: (:=) infix 2 Var a // Assignment
& eval a Int & toString a
| E.a: If a Stm Stm // If
& eval a Bool & toString a
| E.a: While a Stm // While
& eval a Bool & toString a
:: Var = Var Char // Variable
:: ArithExpr = E.a b: (+) infixl 6 a b // Addition
& eval a Int & toString a & eval b Int & toString b
| E.a b: (-) infixl 6 a b // Subtraction
& eval a Int & eval b Int & toString a & toString b
| E.a b: (*) infixl 7 a b // Multiplication
& eval a Int & toString a & eval b Int & toString b
:: BoolExpr = E.a b: (==) infix 4 a b // Equality on ArithExpr
& eval a Int & toString a & eval b Int & toString b
| E.a b: (<=) infix 4 a b // Ord
& eval a Int & toString a & eval b Int & toString b
| E.a b: (>=) infix 4 a b
& eval a Int & toString a & eval b Int & toString b
| E.a b: (<) infix 4 a b
& eval a Int & toString a & eval b Int & toString b
| E.a b: (>) infix 4 a b
& eval a Int & toString a & eval b Int & toString b
| E.a: ~ a // Negation
& eval a Bool & toString a
| E.a b: (\/) infixr 4 a b // Disjunction
& eval a Bool & toString a & eval b Bool & toString b
| E.a b: (/\) infixr 3 a b // Conjunction
& eval a Bool & toString a & eval b Bool & toString b
:: State :== Var -> Int
:: CharState :== Char -> Int
// Natural Semantics
:: DerivTree = { stm :: Stm
, state :: State
, children :: [DerivTree]
, result :: State
}
tree :: Stm st -> DerivTree | toState st // The deriv. tree for @1 in state @2
// Structural Operational Semantics
:: DerivSeqNode = Done State
| NDone Stm State
:: DerivSeq :== [DerivSeqNode]
seq :: Stm st -> DerivSeq | toState st // The deriv. seq. for @1 in state @2
|
