1 2 -- ==========================================================-- 3 -- === Revised domain operations for HO analysis ===-- 4 -- === AbstractVals2.hs ===-- 5 -- ==========================================================-- 6 7 module AbstractVals2 where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 12 13 infix 9 << -- Below-or-equal for Routes 14 infix 9 /\ -- Binary GLB for routes 15 infix 9 \/ -- Binary LUB for routes 16 17 18 -- ==========================================================-- 19 -- === ===-- 20 -- === Top and bottom points of domains. ===-- 21 -- === ===-- 22 -- ==========================================================-- 23 24 -- ==========================================================-- 25 -- 26 avUncurry :: [Domain] -> Domain -> Domain 27 28 avUncurry dss (Func dss2 dt) = Func (dss++dss2) dt 29 avUncurry dss non_func_dom = Func dss non_func_dom 30 31 32 -- ==========================================================-- 33 -- 34 avTopR :: Domain -> Route 35 36 avTopR Two = One 37 avTopR (Lift1 ds) = Up1 (map avTopR ds) 38 avTopR (Lift2 ds) = UpUp2 (map avTopR ds) 39 avTopR d@(Func dss dt) = Rep (avTopR_aux d) 40 41 42 -- ==========================================================-- 43 -- 44 avTopR_aux_2 :: [Domain] -> Frontier 45 46 avTopR_aux_2 dss 47 = Min1Max0 (length dss) [MkFrel (map avBottomR dss)] [] 48 49 50 -- ==========================================================-- 51 -- 52 avTopR_aux :: Domain -> Rep 53 54 avTopR_aux (Func dss Two) 55 = RepTwo (avTopR_aux_2 dss) 56 57 avTopR_aux (Func dss (Lift1 dts)) 58 = let lf = avTopR_aux_2 dss 59 hf_domains = map (avUncurry dss) dts 60 hfs = map avTopR_aux hf_domains 61 in 62 Rep1 lf hfs 63 64 avTopR_aux (Func dss (Lift2 dts)) 65 = let lf = avTopR_aux_2 dss 66 hf_domains = map (avUncurry dss) dts 67 hfs = map avTopR_aux hf_domains 68 in 69 Rep2 lf lf hfs 70 71 72 -- ==========================================================-- 73 -- 74 avBottomR :: Domain -> Route 75 76 avBottomR Two = Zero 77 avBottomR (Lift1 ds) = Stop1 78 avBottomR (Lift2 ds) = Stop2 79 avBottomR d@(Func dss dt) = Rep (avBottomR_aux d) 80 81 82 -- ==========================================================-- 83 -- 84 avBottomR_aux_2 :: [Domain] -> Frontier 85 86 avBottomR_aux_2 dss 87 = Min1Max0 (length dss) [] [MkFrel (map avTopR dss)] 88 89 90 -- ==========================================================-- 91 -- 92 avBottomR_aux :: Domain -> Rep 93 94 avBottomR_aux (Func dss Two) 95 = RepTwo (avBottomR_aux_2 dss) 96 97 avBottomR_aux (Func dss (Lift1 dts)) 98 = let lf = avBottomR_aux_2 dss 99 hf_domains = map (avUncurry dss) dts 100 hfs = map avBottomR_aux hf_domains 101 in 102 Rep1 lf hfs 103 104 avBottomR_aux (Func dss (Lift2 dts)) 105 = let lf = avBottomR_aux_2 dss 106 hf_domains = map (avUncurry dss) dts 107 hfs = map avBottomR_aux hf_domains 108 in 109 Rep2 lf lf hfs 110 111 112 -- ==========================================================-- 113 -- 114 avIsBottomR :: Route -> Bool 115 116 avIsBottomR Zero = True 117 avIsBottomR Stop1 = True 118 avIsBottomR Stop2 = True 119 avIsBottomR One = False 120 avIsBottomR (Up1 _) = False 121 avIsBottomR Up2 = False 122 avIsBottomR (UpUp2 _) = False 123 avIsBottomR (Rep r) = avIsBottomRep r 124 125 126 -- ==========================================================-- 127 -- 128 avIsBottomRep :: Rep -> Bool 129 130 avIsBottomRep (RepTwo (Min1Max0 ar f1 f0)) 131 = null f1 132 avIsBottomRep (Rep1 (Min1Max0 lf_ar lf_f1 lf_f0) hfs) 133 = null lf_f1 134 avIsBottomRep (Rep2 (Min1Max0 lf_ar lf_f1 lf_f0) mf hfs) 135 = null lf_f1 136 137 138 -- ==========================================================-- 139 -- Is this correct? I think so. 140 -- 141 avIsTopR :: Route -> Bool 142 143 avIsTopR Zero = False 144 avIsTopR One = True 145 avIsTopR Stop1 = False 146 avIsTopR (Up1 rs) = myAll avIsTopR rs 147 avIsTopR Stop2 = False 148 avIsTopR Up2 = False 149 avIsTopR (UpUp2 rs) = myAll avIsTopR rs 150 avIsTopR (Rep r) = avIsTopRep r 151 152 153 -- ==========================================================-- 154 -- 155 avIsTopRep :: Rep -> Bool 156 157 avIsTopRep (RepTwo (Min1Max0 ar f1 f0)) 158 = null f0 159 avIsTopRep (Rep1 lf hfs) 160 = myAll avIsTopRep hfs 161 avIsTopRep (Rep2 lf mf hfs) 162 = myAll avIsTopRep hfs 163 164 165 -- ==========================================================-- 166 -- === ===-- 167 -- === Partial ordering predicates for points in domains. ===-- 168 -- === ===-- 169 -- ==========================================================-- 170 171 -- ==========================================================-- 172 -- 173 (<<) :: Route -> Route -> Bool 174 175 Zero << _ = True 176 One << One = True 177 One << Zero = False 178 179 Stop1 << _ = True 180 Up1 rs1 << Up1 rs2 = avLEQR_list rs1 rs2 181 Up1 rs1 << _ = False 182 183 Stop2 << _ = True 184 Up2 << Stop2 = False 185 Up2 << _ = True 186 UpUp2 rs1 << UpUp2 rs2 = avLEQR_list rs1 rs2 187 UpUp2 rs1 << _ = False 188 189 Rep rep1 << Rep rep2 = avBelowEQrep rep1 rep2 190 191 192 -- ==========================================================-- 193 -- A little bit of Cordy-style loop unrolling 194 -- although not actually tail-strict :-) 195 -- 196 avLEQR_list :: [Route] -> [Route] -> Bool 197 198 avLEQR_list [] [] 199 = True 200 201 avLEQR_list (a1:[]) (b1:[]) 202 = a1 << b1 203 204 avLEQR_list (a1:a2:[]) (b1:b2:[]) 205 = if a1 << b1 206 then a2 << b2 207 else False 208 209 avLEQR_list (a1:a2:a3:[]) (b1:b2:b3:[]) 210 = if a1 << b1 211 then if a2 << b2 212 then a3 << b3 213 else False 214 else False 215 216 avLEQR_list (a1:a2:a3:a4:[]) (b1:b2:b3:b4:[]) 217 = if a1 << b1 218 then if a2 << b2 219 then if a3 << b3 220 then a4 << b4 221 else False 222 else False 223 else False 224 225 -- OLD: avLEQR_list (a1:a2:a3:a4:as) (b1:b2:b3:b4:bs) 226 avLEQR_list (a1:a2:a3:a4:as@(_:_)) (b1:b2:b3:b4:bs@(_:_)) 227 = if a1 << b1 228 then if a2 << b2 229 then if a3 << b3 230 then if a4 << b4 231 then avLEQR_list as bs 232 else False 233 else False 234 else False 235 else False 236 237 238 --avLEQR_list (a:as) (b:bs) = if a << b then avLEQR_list as bs else False 239 avLEQR_list _ _ = panic "avLEQR_list: unequal lists" 240 241 242 -- ==========================================================-- 243 -- 244 avBelowEQfrel :: FrontierElem -> FrontierElem -> Bool 245 246 avBelowEQfrel (MkFrel rs1) (MkFrel rs2) 247 = avLEQR_list rs1 rs2 248 249 250 -- ==========================================================-- 251 -- 252 avBelowEQfrontier :: Frontier -> Frontier -> Bool 253 254 avBelowEQfrontier (Min1Max0 ar1 f1a f0a) (Min1Max0 ar2 f1b f0b) 255 -- 256 -- | ar1 == ar2 {-INVARIANT-} 257 -- 258 -- = myAnd [myOr [q `avBelowEQfrel` p | q <- f1b] | p <- f1a] 259 -- 260 -- Tail recursive special 261 -- 262 = let outer [] = True 263 outer (x:xs) = if inner x f1b then outer xs else False 264 inner y [] = False 265 inner y (z:zs) = if z `avBelowEQfrel` y then True else inner y zs 266 in 267 outer f1a 268 269 270 271 -- ==========================================================-- 272 -- 273 avBelowEQrep :: Rep -> Rep -> Bool 274 275 avBelowEQrep (RepTwo fr1) (RepTwo fr2) 276 = avBelowEQfrontier fr1 fr2 277 278 avBelowEQrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2) 279 = avBelowEQfrontier lf1 lf2 && 280 myAndWith2 avBelowEQrep hfs1 hfs2 281 282 avBelowEQrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2) 283 = avBelowEQfrontier lf1 lf2 && 284 avBelowEQfrontier mf1 mf2 && 285 myAndWith2 avBelowEQrep hfs1 hfs2 286 287 288 -- ==========================================================-- 289 -- === ===-- 290 -- === LUB and GLB operations for Points. ===-- 291 -- === ===-- 292 -- ==========================================================-- 293 294 -- ==========================================================-- 295 -- 296 (\/) :: Route -> Route -> Route 297 298 p@ Zero \/ q = q 299 p@ One \/ q = p 300 301 p@ Stop1 \/ q = q 302 p@(Up1 rs1) \/ Stop1 = p 303 p@(Up1 rs1) \/ Up1 rs2 = Up1 (myZipWith2 (\/) rs1 rs2) 304 305 p@ Stop2 \/ q = q 306 p@ Up2 \/ Stop2 = p 307 p@ Up2 \/ q = q 308 p@(UpUp2 rs1) \/ UpUp2 rs2 = UpUp2 (myZipWith2 (\/) rs1 rs2) 309 p@(UpUp2 rs1) \/ q = p 310 311 p@(Rep rep1) \/ q@(Rep rep2) = Rep (avLUBrep rep1 rep2) 312 313 314 -- ==========================================================-- 315 -- 316 avLUBfrel :: FrontierElem -> FrontierElem -> FrontierElem 317 318 avLUBfrel (MkFrel rs1) (MkFrel rs2) 319 = MkFrel (myZipWith2 (\/) rs1 rs2) 320 321 322 -- ==========================================================-- 323 -- 324 avLUBfrontier :: Frontier -> Frontier -> Frontier 325 326 avLUBfrontier (Min1Max0 ar1 f1a f0a) (Min1Max0 ar2 f1b f0b) 327 -- | ar1 == ar2 {-INVARIANT-} 328 = Min1Max0 ar1 (avLUBmin1frontier f1a f1b) (avLUBmax0frontier f0a f0b) 329 330 331 -- ==========================================================-- 332 -- 333 avLUBrep :: Rep -> Rep -> Rep 334 335 avLUBrep (RepTwo fr1) (RepTwo fr2) 336 = RepTwo (avLUBfrontier fr1 fr2) 337 avLUBrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2) 338 = Rep1 (avLUBfrontier lf1 lf2) (myZipWith2 avLUBrep hfs1 hfs2) 339 avLUBrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2) 340 = Rep2 (avLUBfrontier lf1 lf2) (avLUBfrontier mf1 mf2) 341 (myZipWith2 avLUBrep hfs1 hfs2) 342 343 344 -- ==========================================================-- 345 -- 346 avLUBmin1frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem] 347 348 avLUBmin1frontier f1a f1b 349 = sort (foldr avMinAddPtfrel f1a f1b) {-OPTIMISE-} 350 351 352 -- ==========================================================-- 353 -- 354 avLUBmax0frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem] 355 356 avLUBmax0frontier f0a f0b 357 = sort (avMaxfrel [ x `avGLBfrel` y | x <- f0a, y <- f0b ]) 358 359 360 -- ==========================================================-- 361 -- 362 (/\) :: Route -> Route -> Route 363 364 p@ Zero /\ q = p 365 p@ One /\ q = q 366 367 p@ Stop1 /\ q = p 368 p@(Up1 rs1) /\ (Up1 rs2) = Up1 (myZipWith2 (/\) rs1 rs2) 369 p@(Up1 rs1) /\ q = q 370 371 p@ Stop2 /\ q = p 372 p@ Up2 /\ q@ Stop2 = q 373 p@ Up2 /\ q = p 374 p@(UpUp2 rs1) /\ q@(UpUp2 rs2) = UpUp2 (myZipWith2 (/\) rs1 rs2) 375 p@(UpUp2 rs1) /\ q = q 376 377 p@(Rep rep1) /\ q@(Rep rep2) = Rep (avGLBrep rep1 rep2) 378 379 380 -- ==========================================================-- 381 -- 382 avGLBfrel :: FrontierElem -> FrontierElem -> FrontierElem 383 384 avGLBfrel (MkFrel rs1) (MkFrel rs2) 385 = MkFrel (myZipWith2 (/\) rs1 rs2) 386 387 388 -- ==========================================================-- 389 -- 390 avGLBfrontier :: Frontier -> Frontier -> Frontier 391 392 avGLBfrontier (Min1Max0 ar1 f1a f0a) (Min1Max0 ar2 f1b f0b) 393 -- | ar1 == ar2 {-INVARIANT-} 394 = Min1Max0 ar1 (avGLBmin1frontier f1a f1b) (avGLBmax0frontier f0a f0b) 395 396 397 -- ==========================================================-- 398 -- 399 avGLBrep :: Rep -> Rep -> Rep 400 401 avGLBrep (RepTwo fr1) (RepTwo fr2) 402 = RepTwo (avGLBfrontier fr1 fr2) 403 avGLBrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2) 404 = Rep1 (avGLBfrontier lf1 lf2) (myZipWith2 avGLBrep hfs1 hfs2) 405 avGLBrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2) 406 = Rep2 (avGLBfrontier lf1 lf2) (avGLBfrontier mf1 mf2) 407 (myZipWith2 avGLBrep hfs1 hfs2) 408 409 410 -- ==========================================================-- 411 -- 412 avGLBmax0frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem] 413 414 avGLBmax0frontier f0a f0b 415 = sort (foldr avMaxAddPtfrel f0a f0b) {-OPTIMISE-} 416 417 418 -- ==========================================================-- 419 -- 420 avGLBmin1frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem] 421 422 avGLBmin1frontier f1a f1b 423 = sort (avMinfrel [ x `avLUBfrel` y | x <- f1a, y <- f1b ]) 424 425 426 -- ==========================================================-- 427 -- === ===-- 428 -- === Min and Max operations for frontiers. ===-- 429 -- === Note avBelowMax0/avAboveMin1 expect Frel's to be ===-- 430 -- === of the same length. ===-- 431 -- === ===-- 432 -- ==========================================================-- 433 434 pt `avBelowMax0frel` f = myAny (pt `avBelowEQfrel`) f 435 436 pt `avAboveMin1frel` f = myAny (`avBelowEQfrel` pt) f 437 438 avMinAddPtfrel x ys 439 | x `avAboveMin1frel` ys = ys 440 | otherwise = x:[y | y <- ys, not (x `avBelowEQfrel` y)] 441 442 avMaxAddPtfrel x ys 443 | x `avBelowMax0frel` ys = ys 444 | otherwise = x:[y | y <- ys, not (y `avBelowEQfrel` x)] 445 446 avMinfrel = foldr avMinAddPtfrel [] 447 448 avMaxfrel = foldr avMaxAddPtfrel [] 449 450 451 -- ==========================================================-- 452 -- === ===-- 453 -- === Min and Max operations for Routes ===-- 454 -- === ===-- 455 -- ==========================================================-- 456 457 pt `avBelowMax0R` f = myAny (pt <<) f 458 459 pt `avAboveMin1R` f = myAny (<< pt) f 460 461 avMinAddPtR x ys 462 | x `avAboveMin1R` ys = ys 463 | otherwise = x:[y | y <- ys, not (x << y)] 464 465 avMaxAddPtR x ys 466 | x `avBelowMax0R` ys = ys 467 | otherwise = x:[y | y <- ys, not (y << x)] 468 469 avMinR = foldr avMinAddPtR [] 470 471 avMaxR = foldr avMaxAddPtR [] 472 473 474 -- ==========================================================-- 475 -- === ===-- 476 -- === Min and Max operations for Reps ===-- 477 -- === ===-- 478 -- ==========================================================-- 479 480 pt `avBelowMax0rep` f = myAny (pt `avBelowEQrep`) f 481 482 pt `avAboveMin1rep` f = myAny (`avBelowEQrep` pt) f 483 484 avMinAddPtrep x ys 485 | x `avAboveMin1rep` ys = ys 486 | otherwise = x:[y | y <- ys, not (x `avBelowEQrep` y)] 487 488 avMaxAddPtrep x ys 489 | x `avBelowMax0rep` ys = ys 490 | otherwise = x:[y | y <- ys, not (y `avBelowEQrep` x)] 491 492 avMinrep = foldr avMinAddPtrep [] 493 494 avMaxrep = foldr avMaxAddPtrep [] 495 496 497 -- ==========================================================-- 498 -- === end AbstractVals2.hs ===-- 499 -- ==========================================================--