blob: be11a6f51784e7566470a0223cf812982f214ec5 (
plain)
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
180
181
182
183
|
module Bit where
import LogFun
import Signal
data Bit = Bot | WeakZero | WeakOne | Zero | One | Top
deriving (Eq,Show{-was:Text-})
instance Static Bit where
intToSig = intToSigBit
sigToInt = sigToIntBit
showStaticSig = showBit
instance Lattice Bit where
bot = Bot
top = Top
weakZero = WeakZero
weakOne = WeakOne
lub = lubBit
pass = passBit
instance Signal Bit where
showSig = showBit
initial = Zero
zerO = Zero
one = One
tt1 = tt1Bit
tt2 = tt2Bit
instance Log Bit where
dumLog = Zero
tt1Bit :: TT1 -> Bit -> Bit
tt1Bit (a,b) =
let p = intBit a
q = intBit b
f x = case x of
Bot -> Bot
Zero -> p
One -> q
Top -> Top
in f
tt2Bit :: TT2 -> Bit -> Bit -> Bit
tt2Bit (a,b,c,d) = f
where p = intBit a
q = intBit b
r = intBit c
s = intBit d
f x y = case x of
Bot -> case y of
Bot -> Bot
WeakZero -> Bot
WeakOne -> Bot
Zero -> Bot
One -> Bot
Top -> Top
WeakZero -> case y of
Bot -> Bot
WeakZero -> p
WeakOne -> q
Zero -> p
One -> q
Top -> Top
WeakOne -> case y of
Bot -> Bot
WeakZero -> r
WeakOne -> s
Zero -> r
One -> s
Top -> Top
Zero -> case y of
Bot -> Bot
WeakZero -> p
WeakOne -> q
Zero -> p
One -> q
Top -> Top
One -> case y of
Bot -> Bot
WeakZero -> r
WeakOne -> s
Zero -> r
One -> s
Top -> Top
Top -> case y of
Bot -> Top
WeakZero -> Top
WeakOne -> Top
Zero -> Top
One -> Top
Top -> Top
lubBit :: Bit -> Bit -> Bit
lubBit a b =
case a of
Bot -> case b of
Bot -> Bot
WeakZero -> WeakZero
WeakOne -> WeakOne
Zero -> Zero
One -> One
Top -> Top
WeakZero -> case b of
Bot -> Zero
WeakZero -> WeakZero
WeakOne -> Top
Zero -> Zero
One -> One
Top -> Top
WeakOne -> case b of
Bot -> WeakOne
WeakZero -> Top
WeakOne -> WeakOne
Zero -> Zero
One -> One
Top -> Top
Zero -> case b of
Bot -> Zero
WeakZero -> Zero
WeakOne -> Zero
Zero -> Zero
One -> Top
Top -> Top
One -> case b of
Bot -> One
WeakZero -> One
WeakOne -> One
Zero -> Top
One -> One
Top -> Top
Top -> case b of
Bot -> Top
WeakZero -> Top
WeakOne -> Top
Zero -> Top
One -> Top
Top -> Top
showBit :: Bit -> String
showBit Bot = "v"
showBit WeakZero = "z"
showBit WeakOne = "o"
showBit Zero = "0"
showBit One = "1"
showBit Top = "^"
intBit :: Int -> Bit
intBit 0 = Zero
intBit 1 = One
intBit x =
error ("\nintBit received bad Int " ++ show x ++ ".\n")
intToSigBit :: Int -> Bit
intToSigBit i
| i==0 = Zero
| i==1 = One
| i==8 = Bot
| i==9 = Top
sigToIntBit :: Bit -> Int
sigToIntBit Zero = 0
sigToIntBit One = 1
sigToIntBit Bot = 8
sigToIntBit Top = 9
passBit :: Bit -> Bit -> Bit
passBit c a =
case c of
Bot -> Bot
Zero -> Bot
One -> a
Top -> Top
instance Num Bit where
(+) = or2
(*) = and2
a - b = xor a b
negate = inv
abs = error "abs not defined for Signals"
signum = error "signum not defined for Signals"
fromInteger = error "fromInteger not defined for Signals"
|
