public
Fork of hst/hst
Description: An open-source refinement checker for the CSP process algebra
Homepage: http://hst.github.com/
Clone URL: git://github.com/dcreager/hst.git
Flattening the Expression type

Before, we had separate datatypes for each “class” of expression; for
instance, a Number type for any expression that always evaluates to a
number.  The Expression type was then defined as a sum type across all
of these subtypes.

This patch flattens things so that there's only a single Expression
type.  This simplifies things by removing a level of indirection in
the type definitions, and also will make it easier to define “bound
expressions” as we implement static-scoped environments.

Lighthouse: [#11]
Douglas Creager (author)
Sat Aug 30 13:47:18 -0700 2008
commit  37739ef6e867fa53cb039c707bf15d4e1affd1ba
tree    bd66e4392f5dfff3c5111189e23ac2cde766155b
parent  2a3f31e387e7b41c1856ff79a47ad5bfebdea5cc
...
14
15
16
 
17
18
19
...
14
15
16
17
18
19
20
0
@@ -14,6 +14,7 @@ Library
0
   Other-Modules:    HST.CSPM.Environments,
0
                     HST.CSPM.Evaluate,
0
                     HST.CSPM.Expressions,
0
+                    HST.CSPM.Utils,
0
                     HST.CSPM.Values
0
 
0
 Executable tests
...
24
25
26
 
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
...
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
 
 
 
 
...
24
25
26
27
28
29
30
 
 
 
 
 
 
 
 
 
 
 
 
 
 
31
32
33
...
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
0
@@ -24,23 +24,10 @@ module HST.CSPM.Evaluate where
0
 
0
 import Data.List
0
 
0
+import HST.CSPM.Utils
0
 import HST.CSPM.Expressions
0
 import HST.CSPM.Values
0
 
0
-eval :: Expression -> Value
0
-
0
-eval EBottom             = VBottom
0
-eval (ENumber id)        = VNumber (evalNumber id)
0
-eval (ESequence s)       = VSequence (evalSequence s)
0
-eval (ESet a)            = VSet (evalSet a)
0
-eval (EBoolean b)        = VBoolean (evalBoolean b)
0
-eval (ETuple t)          = VTuple (evalTuple t)
0
-eval (QHead s)           = head (evalAsSequence s)
0
-eval (EIfThenElse b x y) = if (evalAsBoolean b) then
0
-                               eval x
0
-                           else
0
-                               eval y
0
-
0
 evalAsNumber :: Expression -> Int
0
 evalAsNumber = coerceNumber . eval
0
 
0
@@ -56,86 +43,79 @@ evalAsBoolean = coerceBoolean . eval
0
 evalAsTuple :: Expression -> [Value]
0
 evalAsTuple = coerceTuple . eval
0
 
0
+eval :: Expression -> Value
0
+
0
+eval EBottom = VBottom
0
+
0
+-- Expressions that evaluate to a number
0
+
0
+eval (ENLit i)         = VNumber $ i
0
+eval (ENNeg m)         = VNumber $ -(evalAsNumber m)
0
+eval (ENSum m n)       = VNumber $ (evalAsNumber m) + (evalAsNumber n)
0
+eval (ENDiff m n)      = VNumber $ (evalAsNumber m) - (evalAsNumber n)
0
+eval (ENProd m n)      = VNumber $ (evalAsNumber m) * (evalAsNumber n)
0
+eval (ENQuot m n)      = VNumber $ (evalAsNumber m) `quot` (evalAsNumber n)
0
+eval (ENRem m n)       = VNumber $ (evalAsNumber m) `rem` (evalAsNumber n)
0
+eval (EQLength s)      = VNumber $ length (evalAsSequence s)
0
+eval (ESCardinality a) = VNumber $ length (evalAsSet a)
0
+
0
+-- Expressions that evaluate to a sequence
0
+
0
+eval (EQLit xs)          = VSequence $ map eval xs
0
+eval (EQClosedRange m n) = VSequence $
0
+                           map VNumber
0
+                           [evalAsNumber m .. evalAsNumber n]
0
+eval (EQOpenRange m)     = VSequence $
0
+                           map VNumber
0
+                           [evalAsNumber m .. ]
0
+eval (EQConcat s t)      = VSequence $
0
+                           (evalAsSequence s) ++ (evalAsSequence t)
0
+eval (EQTail s)          = VSequence $ tail (evalAsSequence s)
0
+
0
+-- Expressions that evaluate to a set
0
+
0
+eval (ESLit xs)              = VSet $ nub (map eval xs)
0
+eval (ESClosedRange m n)     = VSet $ map VNumber
0
+                               [evalAsNumber m .. evalAsNumber n]
0
+eval (ESOpenRange m)         = VSet $ map VNumber [evalAsNumber m ..]
0
+eval (ESUnion a b)           = VSet $ (evalAsSet a) `union` (evalAsSet b)
0
+eval (ESIntersection a b)    = VSet $ (evalAsSet a) `intersect` (evalAsSet b)
0
+eval (ESDifference a b)      = VSet $ (evalAsSet a) \\ (evalAsSet b)
0
+eval (ESDistUnion aa)        = VSet $ distUnion
0
+                               (map coerceSet (evalAsSet aa))
0
+eval (ESDistIntersection aa) = VSet $ distIntersect
0
+                               (map coerceSet (evalAsSet aa))
0
+eval (EQSet s)               = VSet $ nub (evalAsSequence s)
0
+eval (ESPowerset a)          = VSet $ map VSet (powerset (evalAsSet a))
0
+eval (ESSequenceset a)       = VSet $ map VSequence (sequenceset (evalAsSet a))
0
+
0
+-- Expressions that evaluate to a boolean
0
+
0
+eval EBTrue          = VBoolean $ True
0
+eval EBFalse         = VBoolean $ False
0
+eval (EBAnd b1 b2)   = VBoolean $ (evalAsBoolean b1) && (evalAsBoolean b2)
0
+eval (EBOr b1 b2)    = VBoolean $ (evalAsBoolean b1) || (evalAsBoolean b2)
0
+eval (EBNot b)       = VBoolean $ not (evalAsBoolean b)
0
+eval (EEqual x y)    = VBoolean $ (eval x) == (eval y)
0
+eval (ENotEqual x y) = VBoolean $ (eval x) /= (eval y)
0
+eval (ELT x y)       = VBoolean $ (eval x) < (eval y)
0
+eval (EGT x y)       = VBoolean $ (eval x) > (eval y)
0
+eval (ELTE x y)      = VBoolean $ (eval x) <= (eval y)
0
+eval (EGTE x y)      = VBoolean $ (eval x) >= (eval y)
0
+eval (EQEmpty s)     = VBoolean $ null (evalAsSequence s)
0
+eval (EQIn x s)      = VBoolean $ (eval x) `elem` (evalAsSequence s)
0
+eval (ESIn x a)      = VBoolean $ (eval x) `elem` (evalAsSet a)
0
+eval (ESEmpty a)     = VBoolean $ null (evalAsSet a)
0
+
0
+-- Expressions that evaluate to a tuple
0
+
0
+eval (ETLit xs) = VTuple $ map eval xs
0
+
0
+-- Expressions that can evaluate to anything
0
+
0
+eval (EQHead s) = head (evalAsSequence s)
0
 
0
-evalNumber :: Number -> Int
0
-
0
-evalNumber (NLit i)         = i
0
-evalNumber (NNeg m)         = -(evalAsNumber m)
0
-evalNumber (NSum m n)       = (evalAsNumber m) + (evalAsNumber n)
0
-evalNumber (NDiff m n)      = (evalAsNumber m) - (evalAsNumber n)
0
-evalNumber (NProd m n)      = (evalAsNumber m) * (evalAsNumber n)
0
-evalNumber (NQuot m n)      = (evalAsNumber m) `quot` (evalAsNumber n)
0
-evalNumber (NRem m n)       = (evalAsNumber m) `rem` (evalAsNumber n)
0
-evalNumber (QLength s)      = length (evalAsSequence s)
0
-evalNumber (SCardinality a) = length (evalAsSet a)
0
-
0
-
0
-evalSequence :: Sequence -> [Value]
0
-
0
-evalSequence (QLit xs)          = map eval xs
0
-evalSequence (QClosedRange m n) = map VNumber
0
-                                      [evalAsNumber m .. evalAsNumber n]
0
-evalSequence (QOpenRange m)     = map VNumber
0
-                                      [evalAsNumber m .. ]
0
-evalSequence (QConcat s t)      = (evalAsSequence s) ++ (evalAsSequence t)
0
-evalSequence (QTail s)          = tail (evalAsSequence s)
0
-
0
-
0
-distUnion :: Eq a => [[a]] -> [a]
0
-distUnion xss = foldr union [] xss
0
-
0
-distIntersect :: Eq a => [[a]] -> [a]
0
-distIntersect []  = []
0
-distIntersect xss = foldr1 intersect xss
0
-
0
-powerset :: [a] -> [[a]]
0
-
0
-powerset []     = [[]]
0
-powerset (x:xs) = ps ++ map (x:) ps
0
-                  where
0
-                    ps = powerset xs
0
-
0
-sequenceset :: [a] -> [[a]]
0
-sequenceset as = [[]] ++
0
-                 concat (map (\xs -> (map (:xs) as)) (sequenceset as))
0
-
0
-evalSet :: Set -> [Value]
0
-
0
-evalSet (SLit xs)              = nub (map eval xs)
0
-evalSet (SClosedRange m n)     = map VNumber
0
-                                 [evalAsNumber m .. evalAsNumber n]
0
-evalSet (SOpenRange m)         = map VNumber [evalAsNumber m ..]
0
-evalSet (SUnion a b)           = (evalAsSet a) `union` (evalAsSet b)
0
-evalSet (SIntersection a b)    = (evalAsSet a) `intersect` (evalAsSet b)
0
-evalSet (SDifference a b)      = (evalAsSet a) \\ (evalAsSet b)
0
-evalSet (SDistUnion aa)        = distUnion
0
-                                 (map coerceSet (evalAsSet aa))
0
-evalSet (SDistIntersection aa) = distIntersect
0
-                                 (map coerceSet (evalAsSet aa))
0
-evalSet (QSet s)               = nub (evalAsSequence s)
0
-evalSet (SPowerset a)          = map VSet (powerset (evalAsSet a))
0
-evalSet (SSequenceset a)       = map VSequence (sequenceset (evalAsSet a))
0
-
0
-
0
-evalBoolean :: Boolean -> Bool
0
-
0
-evalBoolean BTrue           = True
0
-evalBoolean BFalse          = False
0
-evalBoolean (BAnd b1 b2)    = (evalAsBoolean b1) && (evalAsBoolean b2)
0
-evalBoolean (BOr b1 b2)     = (evalAsBoolean b1) || (evalAsBoolean b2)
0
-evalBoolean (BNot b)        = not (evalAsBoolean b)
0
-evalBoolean (EEqual x y)    = (eval x) == (eval y)
0
-evalBoolean (ENotEqual x y) = (eval x) /= (eval y)
0
-evalBoolean (ELT x y)       = (eval x) < (eval y)
0
-evalBoolean (EGT x y)       = (eval x) > (eval y)
0
-evalBoolean (ELTE x y)      = (eval x) <= (eval y)
0
-evalBoolean (EGTE x y)      = (eval x) >= (eval y)
0
-evalBoolean (QEmpty s)      = null (evalAsSequence s)
0
-evalBoolean (QIn x s)       = (eval x) `elem` (evalAsSequence s)
0
-evalBoolean (SIn x a)       = (eval x) `elem` (evalAsSet a)
0
-evalBoolean (SEmpty a)      = null (evalAsSet a)
0
-
0
-
0
-evalTuple :: Tuple -> [Value]
0
-
0
-evalTuple (TLit xs) = map eval xs
0
+eval (EIfThenElse b x y) = if (evalAsBoolean b) then
0
+                               eval x
0
+                           else
0
+                               eval y
...
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
180
181
182
183
184
 
 
 
 
 
 
185
186
 
 
 
187
188
189
190
 
 
 
 
 
 
 
 
 
 
...
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
0
@@ -42,149 +42,126 @@ instance Show Binding where
0
 
0
 data Expression
0
     = EBottom
0
-    | ENumber Number
0
-    | ESequence Sequence
0
-    | ESet Set
0
-    | EBoolean Boolean
0
-    | ETuple Tuple
0
-    | QHead Expression
0
-    | EIfThenElse Expression Expression Expression
0
-    deriving (Eq, Ord)
0
 
0
-instance Show Expression where
0
-    show EBottom = "Bottom"
0
-    show (ENumber n) = show n
0
-    show (ESequence s) = show s
0
-    show (ESet a) = show a
0
-    show (EBoolean b) = show b
0
-    show (ETuple t) = show t
0
-    show (QHead x) = "head(" ++ show x ++ ")"
0
-    show (EIfThenElse b x y) = "if (" ++ show b ++ ") then " ++
0
-                               show x ++ " else " ++ show y
0
-
0
-    -- We don't want to show the [] brackets when showing a list of
0
-    -- expressions, since we're going to use different brackets
0
-    -- depending on whether the list represents a sequence, set, or
0
-    -- tuple literal.
0
-
0
-    showList []     = showString ""
0
-    showList (x:xs) = shows x . showl xs
0
-                      where
0
-                        showl []     = id
0
-                        showl (x:xs) = showChar ',' . shows x . showl xs
0
-
0
--- Numbers
0
-
0
-data Number
0
-    = NLit Int
0
-    | NNeg Expression
0
-    | NSum Expression Expression
0
-    | NDiff Expression Expression
0
-    | NProd Expression Expression
0
-    | NQuot Expression Expression
0
-    | NRem Expression Expression
0
-    | QLength Expression
0
-    | SCardinality Expression
0
-    deriving (Eq, Ord)
0
-
0
-instance Show Number where
0
-    show (NLit i)         = show i
0
-    show (NNeg m)         = "(-" ++ show m ++ ")"
0
-    show (NSum m n)       = "(" ++ show m ++ " + " ++ show n ++ ")"
0
-    show (NDiff m n)      = "(" ++ show m ++ " - " ++ show n ++ ")"
0
-    show (NProd m n)      = "(" ++ show m ++ " * " ++ show n ++ ")"
0
-    show (NQuot m n)      = "(" ++ show m ++ " / " ++ show n ++ ")"
0
-    show (NRem m n)       = "(" ++ show m ++ " % " ++ show n ++ ")"
0
-    show (QLength s)      = "(#" ++ show s ++ ")"
0
-    show (SCardinality a) = "(#" ++ show a ++ ")"
0
-
0
--- Sequences
0
-
0
-data Sequence
0
-    = QLit [Expression]
0
-    | QClosedRange Expression Expression
0
-    | QOpenRange Expression
0
-    | QConcat Expression Expression
0
-    | QTail Expression
0
+    -- Expressions which evaluate to a number
0
+    | ENLit Int
0
+    | ENNeg Expression
0
+    | ENSum Expression Expression
0
+    | ENDiff Expression Expression
0
+    | ENProd Expression Expression
0
+    | ENQuot Expression Expression
0
+    | ENRem Expression Expression
0
+    | EQLength Expression
0
+    | ESCardinality Expression
0
+
0
+    -- Expressions which evaluate to a sequence
0
+    | EQLit [Expression]
0
+    | EQClosedRange Expression Expression
0
+    | EQOpenRange Expression
0
+    | EQConcat Expression Expression
0
+    | EQTail Expression
0
     -- TODO: sequence comprehension
0
-    deriving (Eq, Ord)
0
 
0
-instance Show Sequence where
0
-    show (QLit xs)          = "<" ++ show xs ++ ">"
0
-    show (QClosedRange m n) = "<" ++ show m ++ ".." ++ show n ++ ">"
0
-    show (QOpenRange m)     = "<" ++ show m ++ "..>"
0
-    show (QConcat s t)      = "concat(" ++ show s ++ ", " ++ show t ++ ")"
0
-    show (QTail s)          = "tail(" ++ show s ++ ")"
0
-
0
--- Sets
0
-
0
-data Set
0
-    = SLit [Expression]
0
-    | SClosedRange Expression Expression
0
-    | SOpenRange Expression
0
-    | SUnion Expression Expression
0
-    | SIntersection Expression Expression
0
-    | SDifference Expression Expression
0
-    | SDistUnion Expression
0
-    | SDistIntersection Expression
0
-    | QSet Expression
0
-    | SPowerset Expression
0
-    | SSequenceset Expression
0
+    -- Expressions which evaluate to a set
0
+    | ESLit [Expression]
0
+    | ESClosedRange Expression Expression
0
+    | ESOpenRange Expression
0
+    | ESUnion Expression Expression
0
+    | ESIntersection Expression Expression
0
+    | ESDifference Expression Expression
0
+    | ESDistUnion Expression
0
+    | ESDistIntersection Expression
0
+    | EQSet Expression
0
+    | ESPowerset Expression
0
+    | ESSequenceset Expression
0
     -- TODO: set comprehension
0
-    deriving (Eq, Ord)
0
 
0
-instance Show Set where
0
-    show (SLit xs)              = "{" ++ show xs ++ "}"
0
-    show (SClosedRange m n)     = "{" ++ show m ++ ".." ++ show n ++ "}"
0
-    show (SOpenRange m)         = "{" ++ show m ++ "..}"
0
-    show (SUnion s1 s2)         = "union(" ++ show s1 ++ ", " ++ show s2 ++ "}"
0
-    show (SIntersection s1 s2)  = "inter(" ++ show s1 ++ ", " ++ show s2 ++ "}"
0
-    show (SDifference s1 s2)    = "diff(" ++ show s1 ++ ", " ++ show s2 ++ "}"
0
-    show (SDistUnion s1)        = "Union(" ++ show s1 ++ ")"
0
-    show (SDistIntersection s1) = "Inter(" ++ show s1 ++ ")"
0
-    show (QSet q0)              = "set(" ++ show q0 ++ ")"
0
-    show (SPowerset s1)         = "Set(" ++ show s1 ++ ")"
0
-    show (SSequenceset s1)      = "Seq(" ++ show s1 ++ ")"
0
-
0
--- Booleans
0
-
0
-data Boolean
0
-    = BTrue
0
-    | BFalse
0
-    | BAnd Expression Expression
0
-    | BOr Expression Expression
0
-    | BNot Expression
0
+    -- Expressions which evaluate to a boolean
0
+    | EBTrue
0
+    | EBFalse
0
+    | EBAnd Expression Expression
0
+    | EBOr Expression Expression
0
+    | EBNot Expression
0
     | EEqual Expression Expression
0
     | ENotEqual Expression Expression
0
     | ELT Expression Expression
0
     | EGT Expression Expression
0
     | ELTE Expression Expression
0
     | EGTE Expression Expression
0
-    | QEmpty Expression
0
-    | QIn Expression Expression
0
-    | SIn Expression Expression
0
-    | SEmpty Expression
0
+    | EQEmpty Expression
0
+    | EQIn Expression Expression
0
+    | ESIn Expression Expression
0
+    | ESEmpty Expression
0
+
0
+    -- Expressions which evaluate to a tuple
0
+    | ETLit [Expression]
0
+
0
+    -- Expressions which can evaluate to anything
0
+    | EQHead Expression
0
+    | EIfThenElse Expression Expression Expression
0
+
0
     deriving (Eq, Ord)
0
 
0
-instance Show Boolean where
0
-    show BTrue             = "true"
0
-    show BFalse            = "false"
0
-    show (BAnd b1 b2)      = "(" ++ show b1 ++ " && " ++ show b2 ++ ")"
0
-    show (BOr b1 b2)       = "(" ++ show b1 ++ " || " ++ show b2 ++ ")"
0
-    show (BNot b1)         = "(!" ++ show b1 ++ ")"
0
+instance Show Expression where
0
+    show EBottom = "Bottom"
0
+
0
+    show (ENLit i)         = show i
0
+    show (ENNeg m)         = "(-" ++ show m ++ ")"
0
+    show (ENSum m n)       = "(" ++ show m ++ " + " ++ show n ++ ")"
0
+    show (ENDiff m n)      = "(" ++ show m ++ " - " ++ show n ++ ")"
0
+    show (ENProd m n)      = "(" ++ show m ++ " * " ++ show n ++ ")"
0
+    show (ENQuot m n)      = "(" ++ show m ++ " / " ++ show n ++ ")"
0
+    show (ENRem m n)       = "(" ++ show m ++ " % " ++ show n ++ ")"
0
+    show (EQLength s)      = "(#" ++ show s ++ ")"
0
+    show (ESCardinality a) = "(#" ++ show a ++ ")"
0
+
0
+    show (EQLit xs)          = "<" ++ show xs ++ ">"
0
+    show (EQClosedRange m n) = "<" ++ show m ++ ".." ++ show n ++ ">"
0
+    show (EQOpenRange m)     = "<" ++ show m ++ "..>"
0
+    show (EQConcat s t)      = "concat(" ++ show s ++ ", " ++ show t ++ ")"
0
+    show (EQTail s)          = "tail(" ++ show s ++ ")"
0
+
0
+    show (ESLit xs)              = "{" ++ show xs ++ "}"
0
+    show (ESClosedRange m n)     = "{" ++ show m ++ ".." ++ show n ++ "}"
0
+    show (ESOpenRange m)         = "{" ++ show m ++ "..}"
0
+    show (ESUnion s1 s2)         = "union(" ++ show s1 ++ ", " ++ show s2 ++ "}"
0
+    show (ESIntersection s1 s2)  = "inter(" ++ show s1 ++ ", " ++ show s2 ++ "}"
0
+    show (ESDifference s1 s2)    = "diff(" ++ show s1 ++ ", " ++ show s2 ++ "}"
0
+    show (ESDistUnion s1)        = "Union(" ++ show s1 ++ ")"
0
+    show (ESDistIntersection s1) = "Inter(" ++ show s1 ++ ")"
0
+    show (EQSet q0)              = "set(" ++ show q0 ++ ")"
0
+    show (ESPowerset s1)         = "Set(" ++ show s1 ++ ")"
0
+    show (ESSequenceset s1)      = "Seq(" ++ show s1 ++ ")"
0
+
0
+    show EBTrue            = "true"
0
+    show EBFalse           = "false"
0
+    show (EBAnd b1 b2)     = "(" ++ show b1 ++ " && " ++ show b2 ++ ")"
0
+    show (EBOr b1 b2)      = "(" ++ show b1 ++ " || " ++ show b2 ++ ")"
0
+    show (EBNot b1)        = "(!" ++ show b1 ++ ")"
0
     show (EEqual e1 e2)    = "(" ++ show e1 ++ " == " ++ show e2 ++ ")"
0
     show (ENotEqual e1 e2) = "(" ++ show e1 ++ " != " ++ show e2 ++ ")"
0
     show (ELT e1 e2)       = "(" ++ show e1 ++ " < " ++ show e2 ++ ")"
0
     show (EGT e1 e2)       = "(" ++ show e1 ++ " > " ++ show e2 ++ ")"
0
     show (ELTE e1 e2)      = "(" ++ show e1 ++ " <= " ++ show e2 ++ ")"
0
     show (EGTE e1 e2)      = "(" ++ show e1 ++ " >= " ++ show e2 ++ ")"
0
-    show (QEmpty q0)       = "null(" ++ show q0 ++ ")"
0
-    show (QIn x q0)        = "elem(" ++ show x ++ ", " ++ show q0 ++ ")"
0
-    show (SIn x s0)        = "member(" ++ show x ++ ", " ++ show s0 ++ ")"
0
-    show (SEmpty s0)       = "empty(" ++ show s0 ++ ")"
0
+    show (EQEmpty q0)      = "null(" ++ show q0 ++ ")"
0
+    show (EQIn x q0)       = "elem(" ++ show x ++ ", " ++ show q0 ++ ")"
0
+    show (ESIn x s0)       = "member(" ++ show x ++ ", " ++ show s0 ++ ")"
0
+    show (ESEmpty s0)      = "empty(" ++ show s0 ++ ")"
0
+
0
+    show (ETLit xs) = "(" ++ show xs ++ ")"
0
 
0
--- Tuples
0
+    show (EQHead x) = "head(" ++ show x ++ ")"
0
+    show (EIfThenElse b x y) = "if (" ++ show b ++ ") then " ++
0
+                               show x ++ " else " ++ show y
0
 
0
-data Tuple
0
-    = TLit [Expression]
0
-    deriving (Eq, Ord, Show)
0
+    -- We don't want to show the [] brackets when showing a list of
0
+    -- expressions, since we're going to use different brackets
0
+    -- depending on whether the list represents a sequence, set, or
0
+    -- tuple literal.
0
+
0
+    showList []     = showString ""
0
+    showList (x:xs) = shows x . showl xs
0
+                      where
0
+                        showl []     = id
0
+                        showl (x:xs) = showChar ',' . shows x . showl xs
...
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
 
 
 
...
39
40
41
 
 
 
 
 
42
43
44
45
46
47
48
49
50
 
 
 
 
 
51
52
53
54
55
56
57
58
59
 
 
 
 
60
61
62
0
@@ -39,29 +39,24 @@ prop_BoolAnd = forAll (two eboolean) tester
0
     where
0
       tester (eb1, eb2) = v0 == v12
0
           where
0
-            v0 = eval (EBoolean (BAnd eb1 eb2))
0
-            v1 = eval eb1
0
-            v2 = eval eb2
0
-            VBoolean b1 = v1
0
-            VBoolean b2 = v2
0
+            v0 = eval (EBAnd eb1 eb2)
0
+            b1 = evalAsBoolean eb1
0
+            b2 = evalAsBoolean eb2
0
             v12 = VBoolean (b1 && b2)
0
 
0
 prop_BoolOr = forAll (two eboolean) tester
0
     where
0
       tester (eb1, eb2) = v0 == v12
0
           where
0
-            v0 = eval (EBoolean (BOr eb1 eb2))
0
-            v1 = eval eb1
0
-            v2 = eval eb2
0
-            VBoolean b1 = v1
0
-            VBoolean b2 = v2
0
+            v0 = eval (EBOr eb1 eb2)
0
+            b1 = evalAsBoolean eb1
0
+            b2 = evalAsBoolean eb2
0
             v12 = VBoolean (b1 || b2)
0
 
0
 prop_BoolNot = forAll eboolean tester
0
     where
0
       tester eb1 = v0 == v1
0
           where
0
-            v0 = eval (EBoolean (BNot eb1))
0
-            v1' = eval eb1
0
-            VBoolean b1' = v1'
0
-            v1 = VBoolean (not b1')
0
+            v0 = eval (EBNot eb1)
0
+            b1 = evalAsBoolean eb1
0
+            v1 = VBoolean (not b1)
...
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
...
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
 
 
 
0
@@ -30,48 +30,45 @@ import HST.CSPM
0
 checkAll checker props =
0
     foldl (>>) (return ()) $ map checker props
0
 
0
-number :: Gen Number
0
-number = sized number'
0
-    where
0
-      number' 0         = liftM NLit arbitrary
0
-      number' n | n > 0 = oneof [liftM  NLit arbitrary,
0
-                                 liftM  NNeg subnum,
0
-                                 liftM2 NSum subnum subnum,
0
-                                 liftM2 NDiff subnum subnum,
0
-                                 liftM2 NProd subnum subnum
0
-                                 --liftM2 NQuot subnum subnum,
0
-                                 --liftM2 NRem subnum subnum
0
-                                ]
0
-                where
0
-                  subnum = liftM ENumber $ number' (n `div` 2)
0
-
0
-enumber :: Gen Expression
0
-enumber = liftM ENumber number
0
 
0
 listOf :: Gen a -> Gen [a]
0
 listOf g = sized listOf'
0
     where
0
       listOf' n = sequence [g | i <- [1..n]]
0
 
0
-qsequence = listOf enumber
0
-esequence = liftM (ESequence . QLit) qsequence
0
+pair :: Gen a -> Gen b -> Gen (a, b)
0
+pair = liftM2 (curry id)
0
+
0
 
0
-boolean :: Gen Boolean
0
-boolean = sized boolean'
0
+enumber :: Gen Expression
0
+enumber = sized number'
0
     where
0
-      boolean' 0         = oneof [return BTrue, return BFalse]
0
-      boolean' n | n > 0 = oneof [liftM2 BAnd subbool subbool,
0
-                                  liftM2 BOr subbool subbool,
0
-                                  liftM  BNot subbool
0
+      number' 0         = liftM ENLit arbitrary
0
+      number' n | n > 0 = oneof [liftM  ENLit arbitrary,
0
+                                 liftM  ENNeg subnum,
0
+                                 liftM2 ENSum subnum subnum,
0
+                                 liftM2 ENDiff subnum subnum,
0
+                                 liftM2 ENProd subnum subnum
0
+                                 --liftM2 ENQuot subnum subnum,
0
+                                 --liftM2 ENRem subnum subnum
0
+                                ]
0
+                where
0
+                  subnum = number' (n `div` 2)
0
+
0
+
0
+esequence = liftM EQLit $ listOf enumber
0
+
0
+eboolean :: Gen Expression
0
+eboolean = sized boolean'
0
+    where
0
+      boolean' 0         = oneof [return EBTrue, return EBFalse]
0
+      boolean' n | n > 0 = oneof [liftM2 EBAnd subbool subbool,
0
+                                  liftM2 EBOr subbool subbool,
0
+                                  liftM  EBNot subbool
0
                                  ]
0
                  where
0
-                   subbool = liftM EBoolean $ boolean' (n `div` 2)
0
-
0
-eboolean = liftM EBoolean boolean
0
+                   subbool = boolean' (n `div` 2)
0
 
0
 expression = oneof [enumber, esequence, eboolean]
0
 
0
 identifier = elements $ map (Identifier . (:[])) ['a'..'z']
0
-
0
-pair :: Gen a -> Gen b -> Gen (a, b)
0
-pair = liftM2 (curry id)
...
49
50
51
52
 
53
54
55
...
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
 
 
 
...
49
50
51
 
52
53
54
55
...
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
0
@@ -49,7 +49,7 @@ testAll = do
0
 
0
 prop_NumLiteral i = v1 == v2
0
     where
0
-      v1 = eval (ENumber (NLit i))
0
+      v1 = eval (ENLit i)
0
       v2 = VNumber i
0
       types = i :: Int
0
 
0
@@ -57,65 +57,61 @@ prop_NumNeg = forAll enumber tester
0
     where
0
       tester n = i0 == negate i1
0
           where
0
-            VNumber i0 = eval (ENumber (NNeg n))
0
-            VNumber i1 = eval n
0
+            i0 = evalAsNumber (ENNeg n)
0
+            i1 = evalAsNumber n
0
 
0
 prop_NumSum = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = i0 == i1 + i2
0
           where
0
-            VNumber i0 = eval (ENumber (NSum n1 n2))
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            i0 = evalAsNumber (ENSum n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
 prop_NumDiff = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = i0 == i1 - i2
0
           where
0
-            VNumber i0 = eval (ENumber (NDiff n1 n2))
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            i0 = evalAsNumber (ENDiff n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
 prop_NumProd = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = i0 == i1 * i2
0
           where
0
-            VNumber i0 = eval (ENumber (NProd n1 n2))
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            i0 = evalAsNumber (ENProd n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
 prop_NumLT = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = b0 == (i1 < i2)
0
           where
0
-            v0 = eval (EBoolean (ELT n1 n2))
0
-            VBoolean b0 = v0
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            b0 = evalAsBoolean (ELT n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
 prop_NumGT = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = b0 == (i1 > i2)
0
           where
0
-            v0 = eval (EBoolean (EGT n1 n2))
0
-            VBoolean b0 = v0
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            b0 = evalAsBoolean (EGT n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
 prop_NumLTE = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = b0 == (i1 <= i2)
0
           where
0
-            v0 = eval (EBoolean (ELTE n1 n2))
0
-            VBoolean b0 = v0
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            b0 = evalAsBoolean (ELTE n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
 prop_NumGTE = forAll (two enumber) tester
0
     where
0
       tester (n1, n2) = b0 == (i1 >= i2)
0
           where
0
-            v0 = eval (EBoolean (EGTE n1 n2))
0
-            VBoolean b0 = v0
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            b0 = evalAsBoolean (EGTE n1 n2)
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
...
41
42
43
44
 
45
46
47
...
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
 
 
 
 
 
 
...
41
42
43
 
44
45
46
47
...
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
0
@@ -41,7 +41,7 @@ prop_SeqLiteral = forAll (listOf enumber) tester
0
     where
0
       tester ns = q0 == q1
0
           where
0
-            q0 = eval (ESequence (QLit ns))
0
+            q0 = eval (EQLit ns)
0
             q1 = VSequence (map eval ns)
0
 
0
 prop_SeqClosedRange = forAll (two enumber) tester
0
@@ -53,31 +53,27 @@ prop_SeqClosedRange = forAll (two enumber) tester
0
       -- equality.
0
       tester (n1, n2) = (i2 - i1 <= 1000) ==> q0 == q1
0
           where
0
-            q0 = eval (ESequence (QClosedRange n1 n2))
0
+            q0 = eval (EQClosedRange n1 n2)
0
             q1 = VSequence (map VNumber [i1 .. i2])
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2
0
 
0
-prop_SeqConcat = forAll (two qsequence) tester
0
+prop_SeqConcat = forAll (two esequence) tester
0
     where
0
-      tester (ns1, ns2) = v0 == v12
0
+      tester (eq1, eq2) = v0 == v12
0
           where
0
-            eq1 = ESequence (QLit ns1)
0
-            eq2 = ESequence (QLit ns2)
0
-            v0 = eval (ESequence (QConcat eq1 eq2))
0
-            v1 = eval eq1
0
-            v2 = eval eq2
0
-            VSequence q1 = v1
0
-            VSequence q2 = v2
0
+            v0 = eval (EQConcat eq1 eq2)
0
+            q1 = evalAsSequence eq1
0
+            q2 = evalAsSequence eq2
0
             v12 = VSequence (q1 ++ q2)
0
 
0
-prop_SeqTail = forAll qsequence tester
0
+prop_SeqTail = forAll esequence tester
0
     where
0
-      tester ns = (length ns > 0) ==> v0 == v1
0
+      tester eq = (length ns > 0) ==> v0 == v1
0
           where
0
-            eq0 = ESequence (QTail eq1)
0
-            eq1 = ESequence (QLit ns)
0
-            v0 = eval eq0
0
-            v1' = eval eq1
0
-            VSequence q1' = v1'
0
-            v1 = VSequence (tail q1')
0
\ No newline at end of file
0
+            eq0 = EQTail eq
0
+            v0  = eval eq0
0
+
0
+            EQLit ns = eq
0
+            eq1      = EQLit (tail ns)
0
+            v1       = eval eq1
...
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
 
48
49
50
...
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
 
 
...
33
34
35
 
 
 
 
 
 
36
37
38
39
40
 
41
42
43
44
...
50
51
52
 
53
54
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
55
56
0
@@ -33,18 +33,12 @@ testAll = do
0
   quickCheck prop_SetLiteral
0
   putStr "SetClosedRange: "
0
   quickCheck prop_SetClosedRange
0
-{-
0
-  putStr "SetConcat: "
0
-  quickCheck prop_SetConcat
0
-  putStr "SetTail: "
0
-  quickCheck prop_SetTail
0
--}
0
 
0
 prop_SetLiteral = forAll (listOf enumber) tester
0
     where
0
       tester ns = s0 == s1
0
           where
0
-            s0 = eval (ESet (SLit ns))
0
+            s0 = eval (ESLit ns)
0
             s1 = VSet (nub (map eval ns))
0
 
0
 prop_SetClosedRange = forAll (two enumber) tester
0
@@ -56,33 +50,7 @@ prop_SetClosedRange = forAll (two enumber) tester
0
       -- equality.
0
       tester (n1, n2) = (i2 - i1 <= 1000) ==> s0 == s1
0
           where
0
-            s0 = eval (ESet (SClosedRange n1 n2))
0
+            s0 = eval (ESClosedRange n1 n2)
0
             s1 = VSet (map VNumber [i1 .. i2])
0
-            VNumber i1 = eval n1
0
-            VNumber i2 = eval n2
0
-
0
-{-
0
-prop_SetConcat = forAll (two esequence) tester
0
-    where
0
-      tester (ns1, ns2) = v0 == v12
0
-          where
0
-            eq1 = ESet (QLit ns1)
0
-            eq2 = ESet (QLit ns2)
0
-            v0 = eval (ESet (QConcat eq1 eq2))
0
-            v1 = eval eq1
0
-            v2 = eval eq2
0
-            VSet q1 = v1
0
-            VSet q2 = v2
0
-            v12 = VSet (q1 ++ q2)
0
-
0
-prop_SetTail = forAll esequence tester
0
-    where
0
-      tester ns = (length ns > 0) ==> v0 == v1
0
-          where
0
-            eq0 = ESet (QTail eq1)
0
-            eq1 = ESet (QLit ns)
0
-            v0 = eval eq0
0
-            v1' = eval eq1
0
-            VSet q1' = v1'
0
-            v1 = VSet (tail q1')
0
--}
0
+            i1 = evalAsNumber n1
0
+            i2 = evalAsNumber n2

Comments