Modify a couple of error messages slightly
[ghc.git] / testsuite / tests / gadt / Nilsson.hs
1 {-# LANGUAGE GADTs, ScopedTypeVariables #-}
2
3 -- Supplied by Henrik Nilsson, showed up a bug in GADTs
4
5 module Nilsson where
6
7 data Event a = NoEvent | Event a
8
9 fromEvent :: Event a -> a
10 fromEvent = undefined
11
12 usrErr :: String -> String -> String -> a
13 usrErr = undefined
14
15 type DTime = Double -- [s]
16
17 data SF a b = SF {sfTF :: a -> Transition a b}
18
19 data SF' a b where
20 SFArr :: (DTime -> a -> Transition a b) -> FunDesc a b -> SF' a b
21
22 SFAcc :: (DTime -> Event a -> Transition (Event a) b)
23 -> (c -> a -> (c, b)) -> c -> b
24 -> SF' (Event a) b
25 SFCpAXA :: (DTime -> a -> Transition a d)
26 -> FunDesc a b -> SF' b c -> FunDesc c d
27 -> SF' a d
28 SF' :: (DTime -> a -> Transition a b) -> SF' a b
29
30 -- A transition is a pair of the next state (in the form of a signal
31 -- function) and the output at the present time step.
32
33 type Transition a b = (SF' a b, b)
34
35
36 sfTF' :: SF' a b -> (DTime -> a -> Transition a b)
37 sfTF' (SFArr tf _) = tf
38 sfTF' (SFAcc tf _ _ _) = tf
39 -- sfTF' (SFSScan ...)
40 sfTF' (SFCpAXA tf _ _ _) = tf
41 sfTF' (SF' tf) = tf
42
43 -- "Smart" constructors. The corresponding "raw" constructors should not
44 -- be used directly for construction.
45
46 sfArr :: FunDesc a b -> SF' a b
47 sfArr FDI = sfId
48 sfArr (FDC b) = sfConst b
49 sfArr (FDE f fne) = sfArrE f fne
50 sfArr (FDG f) = sfArrG f
51
52
53 sfId :: SF' a a
54 sfId = sf
55 where
56 sf = SFArr (\_ a -> (sf, a)) FDI
57
58
59 sfConst :: b -> SF' a b
60 sfConst b = sf
61 where
62 sf = SFArr (\_ _ -> (sf, b)) (FDC b)
63
64
65 sfNever :: SF' a (Event b)
66 sfNever = sfConst NoEvent
67
68
69 -- Assumption: fne = f NoEvent
70 sfArrE :: (Event a -> b) -> b -> SF' (Event a) b
71 sfArrE f fne = sf
72 where
73 sf = SFArr (\_ ea -> (sf, case ea of NoEvent -> fne ; _ -> f ea))
74 (FDE f fne)
75
76 sfArrG :: (a -> b) -> SF' a b
77 sfArrG f = sf
78 where
79 sf = SFArr (\_ a -> (sf, f a)) (FDG f)
80
81
82 sfAcc :: (c -> a -> (c, b)) -> c -> b -> SF' (Event a) b
83 sfAcc f c bne = sf
84 where
85 sf = SFAcc (\dt ea -> case ea of
86 NoEvent -> (sf, bne)
87 Event a -> let
88 (c', b) = f c a
89 in
90 (sfAcc f c' bne, b))
91 f
92 c
93 bne
94
95 -- sfAccHld would be very similar. The only difference is that
96 -- what's now called "bne" would be updated at each event.
97 --
98 -- So maybe one could use the SAME constructor, just different
99 -- transition functions? It really depends on what assumptions
100 -- one need to make when optimizing.
101
102
103 -- Motivation for event-processing function type
104 -- (alternative would be function of type a->b plus ensuring that it
105 -- only ever gets invoked on events):
106 -- * Now we need to be consistent with other kinds of arrows.
107 -- * We still want to be able to get hold of the original function.
108
109 data FunDesc a b where
110 FDI :: FunDesc a a -- Identity function
111 FDC :: b -> FunDesc a b -- Constant function
112 FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun
113 FDG :: (a -> b) -> FunDesc a b -- General function
114
115 fdFun :: FunDesc a b -> (a -> b)
116 fdFun FDI = id
117 fdFun (FDC b) = const b
118 fdFun (FDE f _) = f
119 fdFun (FDG f) = f
120
121 fdComp :: FunDesc a b -> FunDesc b c -> FunDesc a c
122 fdComp FDI fd2 = fd2
123 fdComp fd1 FDI = fd1
124 fdComp (FDC b) fd2 = FDC ((fdFun fd2) b)
125 fdComp _ (FDC c) = FDC c
126 fdComp (FDE f1 f1ne) fd2 = FDE (f2 . f1) (f2 f1ne)
127 where
128 f2 = fdFun fd2
129 fdComp (FDG f1) (FDE f2 f2ne) = FDG f
130 where
131 f a = case f1 a of
132 NoEvent -> f2ne
133 f1a -> f2 f1a
134 fdComp (FDG f1) fd2 = FDG (fdFun fd2 . f1)
135
136
137 -- Verifies that the first argument is NoEvent. Returns the value of the
138 -- second argument that is the case. Raises an error otherwise.
139 -- Used to check that functions on events do not map NoEvent to Event
140 -- wherever that assumption is exploited.
141 vfyNoEv :: Event a -> b -> b
142 vfyNoEv NoEvent b = b
143 vfyNoEv _ _ = usrErr "AFRP" "vfyNoEv"
144 "Assertion failed: Functions on events must not \
145 \map NoEvent to Event."
146
147 compPrim :: SF a b -> SF b c -> SF a c
148 compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0}
149 where
150 tf0 a0 = (cpXX sf1 sf2, c0)
151 where
152 (sf1, b0) = tf10 a0
153 (sf2, c0) = tf20 b0
154
155 -- Naming convention: cp<X><Y> where <X> and <Y> is one of:
156 -- X - arbitrary signal function
157 -- A - arbitrary pure arrow
158 -- C - constant arrow
159 -- E - event-processing arrow
160 -- G - arrow known not to be identity, constant (C) or
161 -- event-processing (E).
162
163 cpXX :: SF' a b -> SF' b c -> SF' a c
164 cpXX (SFArr _ fd1) sf2 = cpAX fd1 sf2
165 cpXX sf1 (SFArr _ fd2) = cpXA sf1 fd2
166 cpXX (SFAcc _ f1 s1 bne) (SFAcc _ f2 s2 cne) =
167 sfAcc f (s1, s2) (vfyNoEv bne cne)
168 where
169 f (s1, s2) a =
170 case f1 s1 a of
171 (s1', NoEvent) -> ((s1', s2), cne)
172 (s1', Event b) ->
173 let (s2', c) = f2 s2 b in ((s1', s2'), c)
174 cpXX (SFCpAXA _ fd11 sf12 fd13) (SFCpAXA _ fd21 sf22 fd23) =
175 cpAXA fd11 (cpXX (cpXA sf12 (fdComp fd13 fd21)) sf22) fd23
176 cpXX sf1 sf2 = SF' tf
177 where
178 tf dt a = (cpXX sf1' sf2', c)
179 where
180 (sf1', b) = (sfTF' sf1) dt a
181 (sf2', c) = (sfTF' sf2) dt b
182
183 cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d
184 cpAXA FDI sf2 fd3 = cpXA sf2 fd3
185 cpAXA fd1 sf2 FDI = cpAX fd1 sf2
186 cpAXA (FDC b) sf2 fd3 = cpCXA b sf2 fd3
187 cpAXA fd1 sf2 (FDC d) = sfConst d
188 cpAXA fd1 (SFArr _ fd2) fd3 = sfArr (fdComp (fdComp fd1 fd2) fd3)
189
190 cpAX :: FunDesc a b -> SF' b c -> SF' a c
191 cpAX FDI sf2 = sf2
192 cpAX (FDC b) sf2 = cpCX b sf2
193 cpAX (FDE f1 f1ne) sf2 = cpEX f1 f1ne sf2
194 cpAX (FDG f1) sf2 = cpGX f1 sf2
195
196 cpXA :: SF' a b -> FunDesc b c -> SF' a c
197 cpXA sf1 FDI = sf1
198 cpXA sf1 (FDC c) = sfConst c
199 cpXA sf1 (FDE f2 f2ne) = cpXE sf1 f2 f2ne
200 cpXA sf1 (FDG f2) = cpXG sf1 f2
201
202 cpCX :: b -> SF' b c -> SF' a c
203 cpCX b (SFArr _ fd2) = sfConst ((fdFun fd2) b)
204 cpCX b (SFAcc _ _ _ cne) = sfConst (vfyNoEv b cne)
205 cpCX b (SFCpAXA _ fd21 sf22 fd23) =
206 cpCXA ((fdFun fd21) b) sf22 fd23
207 cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI
208 where
209 tf dt _ = (cpCX b sf2', c)
210 where
211 (sf2', c) = (sfTF' sf2) dt b
212
213 -- For SPJ: The following version did not work.
214 -- The commented out one below did work, by lambda-lifting cpCXAux
215 cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
216 cpCXA b sf2 FDI = cpCX b sf2
217 cpCXA _ _ (FDC c) = sfConst c
218 cpCXA b (sf2 :: SF' b c) (fd3 :: FunDesc c d) = cpCXAAux sf2
219 where
220 f3 = fdFun fd3
221
222 cpCXAAux :: SF' b c -> SF' a d
223 cpCXAAux (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b))
224 cpCXAAux (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne))
225 cpCXAAux (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3)
226
227 {- -- For SPJ: This version works
228 cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d
229 cpCXA b sf2 FDI = cpCX b sf2
230 cpCXA _ _ (FDC c) = sfConst c
231 cpCXA b sf2 fd3 = cpCXAAux b fd3 (fdFun fd3) sf2
232 where
233 -- f3 = fdFun fd3
234 -- Really something like: cpCXAAux :: SF' b c -> SF' a d
235 cpCXAAux :: b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d
236 cpCXAAux b fd3 f3 (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b))
237 cpCXAAux b fd3 f3 (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne))
238 cpCXAAux b fd3 f3 (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3)
239 -}
240
241 cpGX :: (a -> b) -> SF' b c -> SF' a c
242 cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2)
243 cpGX f1 (SFCpAXA _ fd21 sf22 fd23) =
244 cpAXA (fdComp (FDG f1) fd21) sf22 fd23
245 cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI
246 where
247 tf dt a = (cpGX f1 sf2', c)
248 where
249 (sf2', c) = (sfTF' sf2) dt (f1 a)
250
251 cpXG :: SF' a b -> (b -> c) -> SF' a c
252 cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2))
253 cpXG (SFAcc _ f1 s bne) f2 = sfAcc f s (f2 bne)
254 where
255 f s a = let (s', b) = f1 s a in (s', f2 b)
256 cpXG (SFCpAXA _ fd11 sf12 fd22) f2 =
257 cpAXA fd11 sf12 (fdComp fd22 (FDG f2))
258 cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2)
259 where
260 tf dt a = (cpXG sf1' f2, f2 b)
261 where
262 (sf1', b) = (sfTF' sf1) dt a
263
264 cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c
265 cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2)
266 cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne)
267 where
268 f s a = f2 s (fromEvent (f1 (Event a)))
269 cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) =
270 cpAXA (fdComp (FDE f1 f1ne) fd21) sf22 fd23
271 cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI
272 where
273 tf dt ea = (cpEX f1 f1ne sf2', c)
274 where
275 (sf2', c) = case ea of
276 NoEvent -> (sfTF' sf2) dt f1ne
277 _ -> (sfTF' sf2) dt (f1 ea)
278
279 cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c
280 cpXE (SFArr _ fd1) f2 f2ne = sfArr (fdComp fd1 (FDE f2 f2ne))
281 cpXE (SFAcc _ f1 s bne) f2 f2ne = sfAcc f s (vfyNoEv bne f2ne)
282 where
283 f s a = let (s', eb) = f1 s a
284 in
285 case eb of NoEvent -> (s', f2ne); _ -> (s', f2 eb)
286 cpXE (SFCpAXA _ fd11 sf12 fd13) f2 f2ne =
287 cpAXA fd11 sf12 (fdComp fd13 (FDE f2 f2ne))
288 cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne)
289 where
290 tf dt a = (cpXE sf1' f2 f2ne,
291 case eb of NoEvent -> f2ne; _ -> f2 eb)
292 where
293 (sf1', eb) = (sfTF' sf1) dt a