Ticket #2456: WouterTest2.hs

File WouterTest2.hs, 12.5 KB (added by ronwalf, 6 years ago)

Another file producing data derivation bug in GHC 6.9.20080730

Line 
1{-# OPTIONS
2 -fglasgow-exts
3 -fallow-overlapping-instances
4 -fallow-undecidable-instances
5  #-}
6module WouterTest2 where
7
8import Data.Generics hiding ((:+:), Inl, Inr)
9-- Thank you, Wouter Swierstra
10
11{-
12--------------------------------
13-- Records
14--------------------------------
15infixr 6 :@:
16data (f :@: g) e = Recb (f e) (g e) deriving Eq
17
18instance (Functor f, Functor g) => Functor (f :@: g) where
19    fmap f (Recb r1 r2) = Recb (fmap f r1) (fmap f r2)
20
21class (Functor sub, Functor sup) => sub :<@: sup where
22    rGet :: sup a -> sub a
23    rSet :: sub a -> sup a -> sup a
24
25instance Functor f => (:<@:) f f where
26    rGet = id
27    rSet x _ = x
28
29instance (Functor f, Functor g) => (:<@:) f (f :@: g) where
30    rGet (Recb x y) = x
31    rSet x (Recb _ y) = Recb x y
32
33instance (Functor f, Functor g, Functor h, (:<@:) f g) =>
34    (:<@:) f (h :@: g) where
35    rGet (Recb _ y) = rGet y
36    rSet x (Recb y z) = Recb y (rSet x z)
37
38
39data Record f = Rec (f (Record f))
40
41class Functor f => RecordField f where
42    dVal :: f a
43
44instance (RecordField f, RecordField g) =>
45    RecordField (f :@: g) where
46    dVal = Recb dVal dVal
47
48dRec :: RecordField f => Record f
49dRec = Rec dVal
50
51recGet (Rec r) = rGet r
52recSet v (Rec r) = Rec $ rSet v r
53-}
54
55--------------------------------
56-- Expressions
57--------------------------------
58
59infixr 6 :+:
60data (f :+: g) e = Inl (f e) | Inr (g e) deriving (Data, Eq)
61
62instance (Functor f, Functor g) => Functor (f :+: g) where
63    fmap f (Inl e1) = Inl (fmap f e1)
64    fmap f (Inr e2) = Inr (fmap f e2)
65
66instance (Typeable1 f, Typeable1 g) => Typeable1 (f :+: g) where
67    typeOf1 l = mkTyConApp (mkTyCon "WouterTest2.:+:") [typeOf1 x, typeOf1 y] where
68        Inl x = (Inl undefined) `asTypeOf` l
69        Inr y = (Inr undefined) `asTypeOf` l
70
71
72class (Functor sub, Functor sup) => sub :<: sup where
73    inj :: sub a -> sup a
74
75instance Functor f => (:<:) f f where
76    inj = id
77
78instance (Functor f, Functor g) => (:<:) f (f :+: g) where
79    inj = Inl
80
81instance (Functor f, Functor g, Functor h, (:<:) f g) => (:<:) f (h :+: g) where
82    inj = Inr . inj
83
84newtype Expr f = In (f (Expr f))
85instance Typeable1 f => Typeable (Expr f) where
86    typeOf e = mkTyConApp (mkTyCon "WouterTest2.Expr") [typeOf1 x]
87        where In x = (In undefined) `asTypeOf` e
88
89inject :: (g :<: f) => g (Expr f) -> Expr f
90inject = In . inj
91
92--------------------------------
93-- Utilities
94--------------------------------
95
96foldExpr :: Functor f => (f a -> a) -> Expr f -> a
97foldExpr f (In t) = f (fmap (foldExpr f) t)
98
99class Functor f => FuncEq f where
100    funcEq :: FuncEq g => f (Expr g) -> f (Expr g) -> Bool
101
102instance (FuncEq f, FuncEq g) => FuncEq (f :+: g) where
103    funcEq (Inl x) (Inl y) = funcEq x y
104    funcEq (Inr x) (Inr y) = funcEq x y
105    funcEq _ _ = False
106
107instance (FuncEq f) => Eq (Expr f) where
108    (In x) == (In y) = funcEq x y
109
110
111---------------------------------
112-- Term Holders
113---------------------------------
114data Const e = Const String deriving (Data, Eq)
115deriving instance Typeable1 Const
116instance Functor Const where
117    fmap f (Const x) = Const x
118instance FuncEq Const where
119    funcEq (Const x) (Const y) = x == y
120eConst x = inject (Const x)
121
122data Var e = Var String deriving (Data, Eq)
123deriving instance Typeable1 Var
124instance Functor Var where
125    fmap f (Var x) = Var x
126instance FuncEq Var where
127    funcEq (Var x) (Var y) = x == y
128eVar x = inject (Var x)
129
130data Function e = Function String [e] deriving (Data, Eq)
131deriving instance Typeable1 Function
132instance Functor Function where
133    fmap f (Function n tl) = Function n $ map f tl
134instance FuncEq Function where
135    funcEq (Function n1 tl1) (Function n2 tl2) = (n1 == n2) && (tl1 == tl2)
136eFunc n tl = inject (Function n tl)
137
138---------------------------------------
139-- Typing (commonly used to type Terms)
140---------------------------------------
141
142data Typed t e = Typed t (Expr Const) deriving (Data, Eq)
143deriving instance Typeable2 Typed
144instance Functor (Typed t) where
145    fmap f (Typed e t) = Typed e t
146instance Eq t => FuncEq (Typed t) where
147    funcEq (Typed e1 t1) (Typed e2 t2) = (e1 == e2) && (t1 == t2)
148eTyped e t = inject (Typed e t)
149type TypedConst = Typed (Expr Const)
150type TypedConstExpr = Expr (TypedConst :+: Const)
151type TypedVar = Typed (Expr Var)
152type TypedVarExpr = Expr (TypedVar :+: Var)
153type TypedFunc = Typed (Expr Function)
154type TypedFuncExpr = Expr (TypedFunc :+: Function :+: Var :+: TypedVar)
155
156class (Functor f, Functor g) => Untypeable g f where
157    untype :: f (Expr g) -> Expr g
158instance (Functor h, Untypeable h f, Untypeable h g) => Untypeable h (f :+: g) where
159    untype (Inl x) = untype x
160    untype (Inr y) = untype y
161instance (:<:) Const g => Untypeable g (Typed (Expr Const)) where
162    untype (Typed (In (Const c)) _) = eConst c
163instance (:<:) Var g => Untypeable g (Typed (Expr Var)) where
164    untype (Typed (In (Var v)) _ ) = eVar v
165instance (:<:) Const g => Untypeable g Const where
166    untype (Const c) = eConst c
167instance (:<:) Var g => Untypeable g Var where
168    untype (Var v) = eVar v
169
170removeType :: Untypeable g f => Expr f -> Expr g
171removeType = foldExpr untype
172
173
174
175--------------------------------------------------------
176-- Literals
177--------------------------------------------------------
178
179data Atomic t e = Atomic String [t] deriving (Data, Eq)
180deriving instance Typeable2 Atomic
181instance Functor (Atomic a) where
182    fmap f (Atomic p tl) = Atomic p tl
183instance (Eq t) => FuncEq (Atomic t) where
184    funcEq (Atomic p1 tl1) (Atomic p2 tl2) = (p1 == p2) && (tl1 == tl2)
185eAtomic p tl = inject (Atomic p tl)
186
187data Not e = Not e deriving (Data, Eq)
188deriving instance Typeable1 Not
189instance Functor Not where
190    fmap f (Not e) = Not $ f e
191instance FuncEq Not where
192    funcEq (Not x) (Not y) = x == y
193eNot e = inject (Not e)
194
195---------------------------------------
196-- First Order Logic Connectives
197---------------------------------------
198data And e = And [e] deriving (Data, Eq)
199deriving instance Typeable1 And
200instance Functor And where
201    fmap f (And el) = And $ map f el
202instance FuncEq And where
203    funcEq (And el1) (And el2) = el1 == el2
204eAnd [e] = e
205eAnd el = inject (And el)
206
207data Or e = Or [e] deriving (Data, Eq)
208deriving instance Typeable1 Or
209instance Functor Or where
210    fmap f (Or el) = Or $ map f el
211instance FuncEq Or where
212    funcEq (Or el1) (Or el2) = el1 == el2
213eOr [e] = e
214eOr el = inject (Or el)
215
216data Imply e = Imply e e deriving (Data, Eq)
217deriving instance Typeable1 Imply
218instance Functor Imply where
219    fmap f (Imply e1 e2) = Imply (f e1) (f e2)
220instance FuncEq Imply where
221    funcEq (Imply x1 y1) (Imply x2 y2) = (x1 == x2) && (y1 == y2)
222eImply e1 e2 = inject (Imply e1 e2)
223
224data ForAll v e = ForAll [v] e deriving (Data, Eq)
225deriving instance Typeable2 ForAll
226instance Functor (ForAll vl) where
227    fmap f (ForAll vl e) = ForAll vl $ f e
228instance Eq v => FuncEq (ForAll v) where
229    funcEq (ForAll vl1 e1) (ForAll vl2 e2) = (vl1 == vl2) && (e1 == e2)
230eForAll [] e = e
231eForAll vl e = inject (ForAll vl e)
232
233data Exists v e = Exists [v] e deriving (Data, Eq)
234deriving instance Typeable2 Exists
235instance Functor (Exists vl) where
236    fmap f (Exists vl e) = Exists vl $ f e
237instance Eq v => FuncEq (Exists v) where
238    funcEq (Exists vl1 e1) (Exists vl2 e2) = (vl1 == vl2) && (e1 == e2)
239eExists [] e = e
240eExists vl e = inject (Exists vl e)
241
242
243data When p e = When p e deriving (Data, Eq)
244deriving instance Typeable2 When
245instance Functor (When p) where
246    fmap f (When p e) = When p $ f e
247instance Eq p => FuncEq (When p) where
248    funcEq (When p1 e1) (When p2 e2) = (p1 == p2) && (e1 == e2)
249eWhen p e = inject (When p e)
250
251----------------------------------
252-- Preferences
253----------------------------------
254data Preference e = Preference (Maybe String) e deriving (Data, Eq)
255deriving instance Typeable1 Preference
256instance Functor Preference where
257    fmap f (Preference n e) = Preference n $ f e
258instance FuncEq Preference where
259    funcEq (Preference n1 e1) (Preference n2 e2) = (n1 == n2) && (e1 == e2)
260ePreference n e = inject (Preference n e)
261
262class Functor f => UnPreference g f where
263    unPreference :: f (Maybe g) -> Maybe g
264
265
266----------------------------------
267-- Timing
268----------------------------------
269data Start e = Start deriving (Data, Eq)
270deriving instance Typeable1 Start
271instance Functor Start where
272    fmap f Start = Start
273instance FuncEq Start where
274    funcEq _ _ = True
275eStart :: (:<:) Start f => Expr f
276eStart = inject Start
277
278data End e = End deriving (Data, Eq)
279deriving instance Typeable1 End
280instance Functor End where
281    fmap f End = End
282instance FuncEq End where
283    funcEq _ _ = True
284eEnd :: (:<:) End f => Expr f
285eEnd = inject End
286
287data All e = All deriving (Data, Eq)
288deriving instance Typeable1 All
289instance Functor All where
290    fmap f All = All
291instance FuncEq All where
292    funcEq _ _ = True
293eAll :: (:<:) All f => Expr f
294eAll = inject All
295
296
297data At t e = At t e deriving (Data, Eq)
298deriving instance Typeable2 At
299instance Functor (At t) where
300    fmap f (At t e) = At t $ f e
301instance Eq t => FuncEq (At t) where
302    funcEq (At t1 e1) (At t2 e2) = (t1 == t2) && (e1 == e2)
303eAt t e = inject (At t e)
304
305data Over t e = Over t e deriving (Data, Eq)
306deriving instance Typeable2 Over
307instance Functor (Over t) where
308    fmap f (Over t e) = Over t $ f e
309instance Eq t => FuncEq (Over t) where
310    funcEq (Over t1 e1) (Over t2 e2) = (t1 == t2) && (e1 == e2)
311eOver t e = inject (Over t e)
312
313data Always e = Always e deriving (Data, Eq)
314deriving instance Typeable1 Always
315instance Functor Always where
316    fmap f (Always e) = Always $ f e
317instance FuncEq Always where
318    funcEq (Always e1) (Always e2) = e1 == e2
319eAlways e = inject (Always e)
320
321data Sometime e = Sometime e deriving (Data, Eq)
322deriving instance Typeable1 Sometime
323instance Functor Sometime where
324    fmap f (Sometime e) = Sometime $ f e
325instance FuncEq Sometime where
326    funcEq (Sometime e1) (Sometime e2) = e1 == e2
327eSometime e = inject (Sometime e)
328
329data Within e = Within Double e deriving (Data, Eq)
330deriving instance Typeable1 Within
331instance Functor Within where
332    fmap f (Within n e) = Within n $ f e
333instance FuncEq Within where
334    funcEq (Within n1 e1) (Within n2 e2) = (n1 == n2) && (e1 == e2)
335eWithin d e = inject (Within d e)
336
337data AtMostOnce e = AtMostOnce e deriving (Data, Eq)
338deriving instance Typeable1 AtMostOnce
339instance Functor AtMostOnce where
340    fmap f (AtMostOnce e) = AtMostOnce $ f e
341instance FuncEq AtMostOnce where
342    funcEq (AtMostOnce e1) (AtMostOnce e2) = e1 == e2
343eAtMostOnce e = inject (AtMostOnce e)
344
345data SometimeAfter e = SometimeAfter e e deriving (Data, Eq)
346deriving instance Typeable1 SometimeAfter
347instance Functor SometimeAfter where
348    fmap f (SometimeAfter e1 e2) = SometimeAfter (f e1) (f e2)
349instance FuncEq SometimeAfter where
350    funcEq (SometimeAfter e11 e12 ) (SometimeAfter e21 e22) = (e11 == e21) && (e12 == e22)
351eSometimeAfter e1 e2 = inject (SometimeAfter e1 e2)
352
353data SometimeBefore e = SometimeBefore e e deriving (Data, Eq)
354deriving instance Typeable1 SometimeBefore
355instance Functor SometimeBefore where
356    fmap f (SometimeBefore e1 e2) = SometimeBefore (f e1) (f e2)
357instance FuncEq SometimeBefore where
358    funcEq (SometimeBefore e11 e12 ) (SometimeBefore e21 e22) = (e11 == e21) && (e12 == e22)
359eSometimeBefore e1 e2 = inject (SometimeBefore e1 e2)
360
361data AlwaysWithin e = AlwaysWithin Double e e deriving (Data, Eq)
362deriving instance Typeable1 AlwaysWithin
363instance Functor AlwaysWithin where
364    fmap f (AlwaysWithin d e1 e2) = AlwaysWithin d (f e1) (f e2)
365instance FuncEq AlwaysWithin where
366    funcEq (AlwaysWithin d1 e11 e12 ) (AlwaysWithin d2 e21 e22) = 
367        (d1 == d2) && (e11 == e21) && (e12 == e22)
368eAlwaysWithin d e1 e2 = inject (AlwaysWithin d e1 e2)
369
370data HoldDuring e = HoldDuring Double Double e deriving (Data, Eq)
371deriving instance Typeable1 HoldDuring
372instance Functor HoldDuring where
373    fmap f (HoldDuring b e p) = HoldDuring b e $ f p
374instance FuncEq HoldDuring where
375    funcEq (HoldDuring b1 e1 p1) (HoldDuring b2 e2 p2) = 
376        (b1 == b2) && (e1 == e2) && (p1 == p2)
377eHoldDuring b e p = inject (HoldDuring b e p)
378
379
380data HoldAfter e = HoldAfter Double e deriving (Data, Eq)
381deriving instance Typeable1 HoldAfter
382instance Functor HoldAfter where
383    fmap f (HoldAfter n e) = HoldAfter n $ f e
384instance FuncEq HoldAfter where
385    funcEq (HoldAfter n1 e1) (HoldAfter n2 e2) = (n1 == n2) && (e1 == e2)
386eHoldAfter d e = inject (HoldAfter d e)
387
388
389
390----------------------------------
391-- Data instance derivations
392----------------------------------
393deriving instance Data (Expr Const)
394deriving instance Data (Expr Var)
395deriving instance Data (Expr Function)
396deriving instance Data TypedConstExpr
397deriving instance Data TypedVarExpr
398deriving instance Data TypedFuncExpr
399deriving instance (Data f) => Data (Expr (Atomic f))