summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/Nilsson.hs
blob: 50dd3c58fcf528eda809251613f3f7b5114c334e (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
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