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
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
|
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
-- Supplied by Henrik Nilsson, showed up a bug in GADTs
module Nilsson where
data Event a = NoEvent | Event a
fromEvent :: Event a -> a
fromEvent = undefined
usrErr :: String -> String -> String -> a
usrErr = undefined
type DTime = Double -- [s]
data SF a b = SF {sfTF :: a -> Transition a b}
data SF' a b where
SFArr :: (DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
SFAcc :: (DTime -> Event a -> Transition (Event a) b)
-> (c -> a -> (c, b)) -> c -> b
-> SF' (Event a) b
SFCpAXA :: (DTime -> a -> Transition a d)
-> FunDesc a b -> SF' b c -> FunDesc c d
-> SF' a d
SF' :: (DTime -> a -> Transition a b) -> SF' a b
-- A transition is a pair of the next state (in the form of a signal
-- function) and the output at the present time step.
type Transition a b = (SF' a b, b)
sfTF' :: SF' a b -> (DTime -> a -> Transition a b)
sfTF' (SFArr tf _) = tf
sfTF' (SFAcc tf _ _ _) = tf
-- sfTF' (SFSScan ...)
sfTF' (SFCpAXA tf _ _ _) = tf
sfTF' (SF' tf) = tf
-- "Smart" constructors. The corresponding "raw" constructors should not
-- be used directly for construction.
sfArr :: FunDesc a b -> SF' a b
sfArr FDI = sfId
sfArr (FDC b) = sfConst b
sfArr (FDE f fne) = sfArrE f fne
sfArr (FDG f) = sfArrG f
sfId :: SF' a a
sfId = sf
where
sf = SFArr (\_ a -> (sf, a)) FDI
sfConst :: b -> SF' a b
sfConst b = sf
where
sf = SFArr (\_ _ -> (sf, b)) (FDC b)
sfNever :: SF' a (Event b)
sfNever = sfConst NoEvent
-- Assumption: fne = f NoEvent
sfArrE :: (Event a -> b) -> b -> SF' (Event a) b
sfArrE f fne = sf
where
sf = SFArr (\_ ea -> (sf, case ea of NoEvent -> fne ; _ -> f ea))
(FDE f fne)
sfArrG :: (a -> b) -> SF' a b
sfArrG f = sf
where
sf = SFArr (\_ a -> (sf, f a)) (FDG f)
sfAcc :: (c -> a -> (c, b)) -> c -> b -> SF' (Event a) b
sfAcc f c bne = sf
where
sf = SFAcc (\dt ea -> case ea of
NoEvent -> (sf, bne)
Event a -> let
(c', b) = f c a
in
(sfAcc f c' bne, b))
f
c
bne
-- sfAccHld would be very similar. The only difference is that
-- what's now called "bne" would be updated at each event.
--
-- So maybe one could use the SAME constructor, just different
-- transition functions? It really depends on what assumptions
-- one need to make when optimizing.
-- Motivation for event-processing function type
-- (alternative would be function of type a->b plus ensuring that it
-- only ever gets invoked on events):
-- * Now we need to be consistent with other kinds of arrows.
-- * We still want to be able to get hold of the original function.
data FunDesc a b where
FDI :: FunDesc a a -- Identity function
FDC :: b -> FunDesc a b -- Constant function
FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun
FDG :: (a -> b) -> FunDesc a b -- General function
fdFun :: FunDesc a b -> (a -> b)
fdFun FDI = id
fdFun (FDC b) = const b
fdFun (FDE f _) = f
fdFun (FDG f) = f
fdComp :: FunDesc a b -> FunDesc b c -> FunDesc a c
fdComp FDI fd2 = fd2
fdComp fd1 FDI = fd1
fdComp (FDC b) fd2 = FDC ((fdFun fd2) b)
fdComp _ (FDC c) = FDC c
fdComp (FDE f1 f1ne) fd2 = FDE (f2 . f1) (f2 f1ne)
where
f2 = fdFun fd2
fdComp (FDG f1) (FDE f2 f2ne) = FDG f
where
f a = case f1 a of
NoEvent -> f2ne
f1a -> f2 f1a
fdComp (FDG f1) fd2 = FDG (fdFun fd2 . f1)
-- Verifies that the first argument is NoEvent. Returns the value of the
-- second argument that is the case. Raises an error otherwise.
-- Used to check that functions on events do not map NoEvent to Event
-- wherever that assumption is exploited.
vfyNoEv :: Event a -> b -> b
vfyNoEv NoEvent b = b
vfyNoEv _ _ = usrErr "AFRP" "vfyNoEv"
"Assertion failed: Functions on events must not \
\map NoEvent to Event."
compPrim :: SF a b -> SF b c -> SF a c
compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
where
tf0 a0 = (cpXX sf1 sf2, c0)
where
(sf1, b0) = tf10 a0
(sf2, c0) = tf20 b0
-- Naming convention: cp<X><Y> where <X> and <Y> is one of:
-- X - arbitrary signal function
-- A - arbitrary pure arrow
-- C - constant arrow
-- E - event-processing arrow
-- G - arrow known not to be identity, constant (C) or
-- event-processing (E).
cpXX :: SF' a b -> SF' b c -> SF' a c
cpXX (SFArr _ fd1) sf2 = cpAX fd1 sf2
cpXX sf1 (SFArr _ fd2) = cpXA sf1 fd2
cpXX (SFAcc _ f1 s1 bne) (SFAcc _ f2 s2 cne) =
sfAcc f (s1, s2) (vfyNoEv bne cne)
where
f (s1, s2) a =
case f1 s1 a of
(s1', NoEvent) -> ((s1', s2), cne)
(s1', Event b) ->
let (s2', c) = f2 s2 b in ((s1', s2'), c)
cpXX (SFCpAXA _ fd11 sf12 fd13) (SFCpAXA _ fd21 sf22 fd23) =
cpAXA fd11 (cpXX (cpXA sf12 (fdComp fd13 fd21)) sf22) fd23
cpXX sf1 sf2 = SF' tf
where
tf dt a = (cpXX sf1' sf2', c)
where
(sf1', b) = (sfTF' sf1) dt a
(sf2', c) = (sfTF' sf2) dt b
cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
cpAXA FDI sf2 fd3 = cpXA sf2 fd3
cpAXA fd1 sf2 FDI = cpAX fd1 sf2
cpAXA (FDC b) sf2 fd3 = cpCXA b sf2 fd3
cpAXA fd1 sf2 (FDC d) = sfConst d
cpAXA fd1 (SFArr _ fd2) fd3 = sfArr (fdComp (fdComp fd1 fd2) fd3)
cpAX :: FunDesc a b -> SF' b c -> SF' a c
cpAX FDI sf2 = sf2
cpAX (FDC b) sf2 = cpCX b sf2
cpAX (FDE f1 f1ne) sf2 = cpEX f1 f1ne sf2
cpAX (FDG f1) sf2 = cpGX f1 sf2
cpXA :: SF' a b -> FunDesc b c -> SF' a c
cpXA sf1 FDI = sf1
cpXA sf1 (FDC c) = sfConst c
cpXA sf1 (FDE f2 f2ne) = cpXE sf1 f2 f2ne
cpXA sf1 (FDG f2) = cpXG sf1 f2
cpCX :: b -> SF' b c -> SF' a c
cpCX b (SFArr _ fd2) = sfConst ((fdFun fd2) b)
cpCX b (SFAcc _ _ _ cne) = sfConst (vfyNoEv b cne)
cpCX b (SFCpAXA _ fd21 sf22 fd23) =
cpCXA ((fdFun fd21) b) sf22 fd23
cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI
where
tf dt _ = (cpCX b sf2', c)
where
(sf2', c) = (sfTF' sf2) dt b
-- For SPJ: The following version did not work.
-- The commented out one below did work, by lambda-lifting cpCXAux
cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA b sf2 FDI = cpCX b sf2
cpCXA _ _ (FDC c) = sfConst c
cpCXA b (sf2 :: SF' b c) (fd3 :: FunDesc c d) = cpCXAAux sf2
where
f3 = fdFun fd3
cpCXAAux :: SF' b c -> SF' a d
cpCXAAux (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b))
cpCXAAux (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne))
cpCXAAux (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3)
{- -- For SPJ: This version works
cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
cpCXA b sf2 FDI = cpCX b sf2
cpCXA _ _ (FDC c) = sfConst c
cpCXA b sf2 fd3 = cpCXAAux b fd3 (fdFun fd3) sf2
where
-- f3 = fdFun fd3
-- Really something like: cpCXAAux :: SF' b c -> SF' a d
cpCXAAux :: b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
cpCXAAux b fd3 f3 (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b))
cpCXAAux b fd3 f3 (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne))
cpCXAAux b fd3 f3 (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3)
-}
cpGX :: (a -> b) -> SF' b c -> SF' a c
cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2)
cpGX f1 (SFCpAXA _ fd21 sf22 fd23) =
cpAXA (fdComp (FDG f1) fd21) sf22 fd23
cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI
where
tf dt a = (cpGX f1 sf2', c)
where
(sf2', c) = (sfTF' sf2) dt (f1 a)
cpXG :: SF' a b -> (b -> c) -> SF' a c
cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2))
cpXG (SFAcc _ f1 s bne) f2 = sfAcc f s (f2 bne)
where
f s a = let (s', b) = f1 s a in (s', f2 b)
cpXG (SFCpAXA _ fd11 sf12 fd22) f2 =
cpAXA fd11 sf12 (fdComp fd22 (FDG f2))
cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2)
where
tf dt a = (cpXG sf1' f2, f2 b)
where
(sf1', b) = (sfTF' sf1) dt a
cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2)
cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne)
where
f s a = f2 s (fromEvent (f1 (Event a)))
cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) =
cpAXA (fdComp (FDE f1 f1ne) fd21) sf22 fd23
cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI
where
tf dt ea = (cpEX f1 f1ne sf2', c)
where
(sf2', c) = case ea of
NoEvent -> (sfTF' sf2) dt f1ne
_ -> (sfTF' sf2) dt (f1 ea)
cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
cpXE (SFArr _ fd1) f2 f2ne = sfArr (fdComp fd1 (FDE f2 f2ne))
cpXE (SFAcc _ f1 s bne) f2 f2ne = sfAcc f s (vfyNoEv bne f2ne)
where
f s a = let (s', eb) = f1 s a
in
case eb of NoEvent -> (s', f2ne); _ -> (s', f2 eb)
cpXE (SFCpAXA _ fd11 sf12 fd13) f2 f2ne =
cpAXA fd11 sf12 (fdComp fd13 (FDE f2 f2ne))
cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne)
where
tf dt a = (cpXE sf1' f2 f2ne,
case eb of NoEvent -> f2ne; _ -> f2 eb)
where
(sf1', eb) = (sfTF' sf1) dt a
|
