Ticket #5439: Bug.hs

File Bug.hs, 7.9 KB (added by mikhail.vorozhtsov, 3 years ago)
Line 
1{-# LANGUAGE UnicodeSyntax #-}
2{-# LANGUAGE DeriveDataTypeable #-}
3{-# LANGUAGE EmptyDataDecls #-}
4{-# LANGUAGE TypeOperators #-}
5{-# LANGUAGE ScopedTypeVariables #-}
6{-# LANGUAGE Rank2Types #-}
7{-# LANGUAGE GADTs #-}
8{-# LANGUAGE TypeFamilies #-}
9{-# LANGUAGE MultiParamTypeClasses #-}
10{-# LANGUAGE FlexibleContexts #-}
11{-# LANGUAGE FlexibleInstances #-}
12{-# LANGUAGE OverlappingInstances #-}
13{-# LANGUAGE UndecidableInstances #-}
14
15module Main where
16
17import Data.Typeable
18import Control.Exception
19
20data Attempt α = Success α
21               |  e . Exception e  Failure e
22
23data Inject f α =  β . Inject (f β) (α  β)
24
25class Completable f where
26  complete  f α  α  IO Bool
27
28instance Completable f  Completable (Inject f) where
29  complete (Inject f inj) = complete f . inj
30
31class WaitOp op where
32  type WaitOpResult op
33  registerWaitOp  Completable f
34                  op  f (Attempt (WaitOpResult op))  IO Bool
35
36data WaitOps rs where
37  WaitOp  WaitOp op  op  WaitOps (HSingle (WaitOpResult op))
38  (:?)    (WaitOp op, HNonEmpty rs)
39          op  WaitOps rs  WaitOps (WaitOpResult op :* rs)
40
41waitOpsNonEmpty   rs . WaitOps rs  HNonEmptyInst rs
42waitOpsNonEmpty (WaitOp _) = HNonEmptyInst
43waitOpsNonEmpty (_ :? _)   = HNonEmptyInst
44
45infixr 7 .?
46infix  8 .?.
47
48(.?)  WaitOp op  op  WaitOps rs  WaitOps (WaitOpResult op :* rs)
49op .? ops = case waitOpsNonEmpty ops of
50  HNonEmptyInst  op :? ops
51
52(.?.)  (WaitOp op1, WaitOp op2)  op1  op2
53       WaitOps (WaitOpResult op1 :*: WaitOpResult op2)
54op1 .?. op2 = op1 .? WaitOp op2
55
56data NthException n e = NthException (Peano n) e deriving (Typeable, Show)
57
58instance (Typeable n, Exception e)  Exception (NthException n e)
59
60instance WaitOp (WaitOps rs) where
61  type WaitOpResult (WaitOps rs) = HElemOf rs
62  registerWaitOp ops ev = do
63    let register   n . HDropClass n rs
64                  Bool  Peano n  WaitOps (HDrop n rs)  IO Bool
65        register first n (WaitOp op) = do
66          let inj n (Success r) = Success (HNth n r)
67              inj n (Failure e) = Failure (NthException n e)
68          t  try $ registerWaitOp op (Inject ev $ inj n)
69          r  case t of
70            Right r  return r
71            Left e   complete ev $ inj n $ Failure (e  SomeException)
72          return $ r || not first
73        register first n (op :? ops') = do
74          let inj n (Success r) = Success (HNth n r)
75              inj n (Failure e) = Failure (NthException n e)
76          t  try $ registerWaitOp op (Inject ev $ inj n)
77          case t of
78            Right True  case waitOpsNonEmpty ops' of
79              HNonEmptyInst  case hTailDropComm  HTailDropComm n rs of
80                HTailDropComm  register False (PSucc n) ops'
81            Right False  return $ not first
82            Left e  do
83              c  complete ev $ inj $ Failure (e  SomeException)
84              return $ c || not first
85    case waitOpsNonEmpty ops of
86      HNonEmptyInst  register True PZero ops
87
88main = return ()
89
90data PZero deriving Typeable
91data PSucc p deriving Typeable
92
93data Peano n where
94  PZero  Peano PZero
95  PSucc  IsPeano p  Peano p  Peano (PSucc p)
96
97instance Show (Peano n) where
98  show n = show (peanoNum n  Int)
99
100peanoNum  Num n  Peano p  n
101peanoNum PZero     = 0
102peanoNum (PSucc p) = 1 + peanoNum p
103
104class Typeable n  IsPeano n where
105  peano  Peano n
106
107instance IsPeano PZero where
108  peano = PZero
109
110instance IsPeano p  IsPeano (PSucc p) where
111  peano = PSucc peano
112
113class (n ~ PSucc (PPred n))  PHasPred n where
114  type PPred n
115
116instance PHasPred (PSucc p) where
117  type PPred (PSucc p) = p
118
119pPred  Peano (PSucc p)  Peano p
120pPred (PSucc p) = p
121
122infixr 7 :*, .*
123infix  8 :*:, .*.
124
125data HNil
126data h :* t
127type HSingle α = α :* HNil
128type α :*: β = α :* β :* HNil
129
130data HList l where
131  HNil  HList HNil
132  (:*)  HListClass t  h  HList t  HList (h :* t)
133
134instance Show (HList HNil) where
135  show _ = "HNil"
136
137instance (Show h, Show (HList t))  Show (HList (h :* t)) where
138  showsPrec d (h :* t) = showParen (d > 7) $
139    showsPrec 8 h . showString " .* " . showsPrec 7 t
140
141(.*)  HListClass t  h  HList t  HList (h :* t)
142(.*) = (:*)
143
144(.*.)  α  β  HList (α :*: β)
145a .*. b = a .* b .* HNil
146
147data HListWitness l where
148  HNilList   HListWitness HNil
149  HConsList  HListClass t  HListWitness (h :* t)
150
151class HListClass l where
152  hListWitness  HListWitness l
153
154instance HListClass HNil where
155  hListWitness = HNilList
156
157instance HListClass t  HListClass (h :* t) where
158  hListWitness = HConsList
159
160data HListInst l where
161  HListInst  HListClass l  HListInst l
162
163hListInst  HList l  HListInst l
164hListInst HNil     = HListInst
165hListInst (_ :* _) = HListInst
166
167class (l ~ (HHead l :* HTail l), HListClass (HTail l))  HNonEmpty l where
168  type HHead l
169  type HTail l
170
171instance HListClass t  HNonEmpty (h :* t) where
172  type HHead (h :* t) = h
173  type HTail (h :* t) = t
174
175hHead  HList (h :* t)  h
176hHead (h :* _) = h
177
178hTail  HList (h :* t)  HList t
179hTail (_ :* t) = t
180
181data HNonEmptyInst l where
182  HNonEmptyInst  HListClass t  HNonEmptyInst (h :* t)
183
184data HDropWitness n l where
185  HDropZero  HListClass l  HDropWitness PZero l
186  HDropSucc  HDropClass p t  HDropWitness (PSucc p) (h :* t)
187
188class (IsPeano n, HListClass l, HListClass (HDrop n l))  HDropClass n l where
189  type HDrop n l
190  hDropWitness  HDropWitness n l
191
192instance HListClass l  HDropClass PZero l where
193  type HDrop PZero l = l
194  hDropWitness = HDropZero
195
196instance HDropClass p t  HDropClass (PSucc p) (h :* t) where
197  type HDrop (PSucc p) (h :* t) = HDrop p t
198  hDropWitness = case hDropWitness  HDropWitness p t of
199    HDropZero  HDropSucc
200    HDropSucc  HDropSucc
201
202data HDropInst n l where
203  HDropInst  HDropClass n l  HDropInst n l
204
205hDrop   n l . HDropClass n l  Peano n  HList l  HList (HDrop n l)
206hDrop n l = case hDropWitness  HDropWitness n l of
207  HDropZero  l
208  HDropSucc  hDrop (pPred n) (hTail l)
209
210data HNonEmptyDropInst n l where
211  HNonEmptyDropInst  (HDropClass n l, HNonEmpty l,
212                       HDropClass (PSucc n) l, HNonEmpty (HDrop n l))
213                     HNonEmptyDropInst n l
214
215pPrevDropInst   n l . HDropClass (PSucc n) l  HNonEmptyDropInst n l
216pPrevDropInst = case hDropWitness  HDropWitness (PSucc n) l of
217  HDropSucc  case hDropWitness  HDropWitness n (HTail l) of
218    HDropZero  HNonEmptyDropInst
219    HDropSucc  case pPrevDropInst  HNonEmptyDropInst (PPred n) (HTail l) of
220      HNonEmptyDropInst  HNonEmptyDropInst
221
222hNextDropInst   n l . (HDropClass n l, HNonEmpty (HDrop n l))
223               HNonEmptyDropInst n l
224hNextDropInst = case hDropWitness  HDropWitness n l of
225  HDropZero  HNonEmptyDropInst
226  HDropSucc  case hNextDropInst  HNonEmptyDropInst (PPred n) (HTail l) of
227    HNonEmptyDropInst  HNonEmptyDropInst
228
229data HTailDropComm n l where
230  HTailDropComm  (HNonEmpty l, HDropClass n l,
231                   HNonEmpty (HDrop n l), HDropClass n (HTail l),
232                   HDropClass (PSucc n) l,
233                   HTail (HDrop n l) ~ HDrop n (HTail l),
234                   HDrop (PSucc n) l ~ HTail (HDrop n l),
235                   HDrop (PSucc n) l ~ HDrop n (HTail l))
236                 HTailDropComm n l
237
238hTailDropComm'   n l . (HDropClass (PSucc n) l)
239                HTailDropComm n l
240hTailDropComm' = case pPrevDropInst  HNonEmptyDropInst n l of
241  HNonEmptyDropInst  hTailDropComm
242
243hTailDropComm   n l . (HDropClass n l, HNonEmpty (HDrop n l))
244                HTailDropComm n l
245hTailDropComm = case hDropWitness  HDropWitness n l of
246  HDropZero  HTailDropComm
247  HDropSucc   case hTailDropComm  HTailDropComm (PPred n) (HTail l) of
248    HTailDropComm  HTailDropComm
249
250type HNth n l = HHead (HDrop n l)
251
252data HElemOf l where
253  HNth  (HDropClass n l, HNonEmpty (HDrop n l))
254        Peano n  HNth n l  HElemOf l
255