1 2 -- ==========================================================-- 3 -- === Specialised meet to speed up calculation of meets ===-- 4 -- === in Gebre's polymorphic generalisation system ===-- 5 -- === ===-- 6 -- === BarakiMeet.hs ===-- 7 -- ==========================================================-- 8 9 10 module BarakiMeet where 11 import BaseDefs 12 import MyUtils 13 import Utils 14 import AbstractVals2 15 import SuccsAndPreds2 16 17 18 infix 9 %% 19 20 21 -- ==========================================================-- 22 -- 23 bmNorm :: Domain -> Route -> Route 24 25 bmNorm Two r = r 26 bmNorm (Lift1 ds) r@ Stop1 = r 27 bmNorm (Lift1 ds) (Up1 rs) = Up1 (myZipWith2 bmNorm ds rs) 28 bmNorm (Lift2 ds) r@ Stop2 = r 29 bmNorm (Lift2 ds) r@ Up2 = r 30 bmNorm (Lift2 ds) (UpUp2 rs) = UpUp2 (myZipWith2 bmNorm ds rs) 31 bmNorm d (Rep rep) = Rep (bmNorm_rep d rep) 32 33 34 bmNorm_rep (Func dss Two) (RepTwo fr) 35 = RepTwo (bmNorm_2 dss fr) 36 37 bmNorm_rep (Func dss (Lift1 dts)) (Rep1 lf hfs) 38 = let hf_domains = map (avUncurry dss) dts 39 in 40 Rep1 (bmNorm_2 dss lf) 41 (myZipWith2 bmNorm_rep hf_domains hfs) 42 43 bmNorm_rep (Func dss (Lift2 dts)) (Rep2 lf mf hfs) 44 = let hf_domains = map (avUncurry dss) dts 45 in 46 Rep2 (bmNorm_2 dss lf) (bmNorm_2 dss mf) 47 (myZipWith2 bmNorm_rep hf_domains hfs) 48 49 50 bmNorm_2 dss (Min1Max0 ar f1 f0) 51 = let norm_f0 = sort (map (bmNorm_frel dss) f0) 52 norm_f1 = spMin1FromMax0 dss f0 53 in 54 Min1Max0 ar norm_f1 norm_f0 55 56 bmNorm_frel dss (MkFrel fels) 57 = MkFrel (myZipWith2 bmNorm dss fels) 58 59 60 -- ==========================================================-- 61 -- 62 bmGLB :: Route -> Route -> Route 63 64 bmGLB (Rep rep1) (Rep rep2) = Rep (bmGLBrep rep1 rep2) 65 66 67 -- ==========================================================-- 68 -- 69 bmGLBrep :: Rep -> Rep -> Rep 70 71 bmGLBrep (RepTwo fr1) (RepTwo fr2) 72 = RepTwo (bmGLBfrontier fr1 fr2) 73 bmGLBrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2) 74 = Rep1 (bmGLBfrontier lf1 lf2) (myZipWith2 bmGLBrep hfs1 hfs2) 75 bmGLBrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2) 76 = Rep2 (bmGLBfrontier lf1 lf2) (bmGLBfrontier mf1 mf2) 77 (myZipWith2 bmGLBrep hfs1 hfs2) 78 79 80 -- ==========================================================-- 81 -- 82 bmGLBfrontier :: Frontier -> Frontier -> Frontier 83 84 bmGLBfrontier (Min1Max0 ar1 _ f0a) (Min1Max0 ar2 _ f0b) 85 -- 86 -- | ar1 == ar2 {-INVARIANT-} 87 -- 88 = Min1Max0 ar1 [] (bmGLBmax0frontier f0a f0b) 89 90 91 -- ==========================================================-- 92 -- 93 bmGLBmax0frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem] 94 95 bmGLBmax0frontier f0a f0b 96 = {-sort-} (foldr bmMaxAddPtfrel f0a f0b) {-OPTIMISE-} 97 98 bmMaxAddPtfrel x ys 99 | x `bmBelowMax0frel` ys = ys 100 | otherwise = x:[y | y <- ys, not (y `bmBelowEQfrel` x)] 101 102 pt `bmBelowMax0frel` f = myAny (pt `bmBelowEQfrel`) f 103 104 105 -- ==========================================================-- 106 -- 107 bmBelowEQfrel :: FrontierElem -> FrontierElem -> Bool 108 109 bmBelowEQfrel (MkFrel rs1) (MkFrel rs2) 110 = myAndWith2 (%%) rs1 rs2 111 112 113 -- ==========================================================-- 114 -- 115 (%%) :: Route -> Route -> Bool 116 117 Zero %% _ = True 118 One %% One = True 119 One %% Zero = False 120 121 Stop1 %% _ = True 122 Up1 rs1 %% Up1 rs2 = myAndWith2 (%%) rs1 rs2 123 Up1 rs1 %% _ = False 124 125 Stop2 %% _ = True 126 Up2 %% Stop2 = False 127 Up2 %% _ = True 128 UpUp2 rs1 %% UpUp2 rs2 = myAndWith2 (%%) rs1 rs2 129 UpUp2 rs1 %% _ = False 130 131 Rep rep1 %% Rep rep2 = bmBelowEQrep rep1 rep2 132 133 134 -- ==========================================================-- 135 -- 136 bmBelowEQrep :: Rep -> Rep -> Bool 137 138 bmBelowEQrep (RepTwo fr1) (RepTwo fr2) 139 = bmBelowEQfrontier fr1 fr2 140 141 bmBelowEQrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2) 142 = bmBelowEQfrontier lf1 lf2 && 143 myAndWith2 bmBelowEQrep hfs1 hfs2 144 145 bmBelowEQrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2) 146 = bmBelowEQfrontier lf1 lf2 && 147 bmBelowEQfrontier mf1 mf2 && 148 myAndWith2 bmBelowEQrep hfs1 hfs2 149 150 151 -- ==========================================================-- 152 -- 153 bmBelowEQfrontier :: Frontier -> Frontier -> Bool 154 155 bmBelowEQfrontier (Min1Max0 ar1 _ f0a) (Min1Max0 ar2 _ f0b) 156 -- 157 -- | ar1 == ar2 {-INVARIANT-} 158 -- = myAnd [myOr [p `bmBelowEQfrel` q | q <- f0a] | p <- f0b] 159 -- 160 -- Tail recursive special 161 -- 162 = let outer [] = True 163 outer (x:xs) = if inner x f0a then outer xs else False 164 inner y [] = False 165 inner y (z:zs) = if y `bmBelowEQfrel` z then True else inner y zs 166 in 167 outer f0b 168 169 -- ==========================================================-- 170 -- === end BarakiMeet.hs ===-- 171 -- ==========================================================--