1 2 -- ==========================================================-- 3 -- === Successors and predecessors of a point in a ===-- 4 -- === finite lattice. SuccsAndPreds2.hs ===-- 5 -- ==========================================================-- 6 7 module SuccsAndPreds2 where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 import AbstractVals2 12 13 14 -- ==========================================================-- 15 -- === ===-- 16 -- === "succs" and "preds" of a point, where: ===-- 17 -- === ===-- 18 -- === succs(x) = Min (complement (downclose (x))) ===-- 19 -- === preds(x) = Max (complement (upclose (x))) ===-- 20 -- === ===-- 21 -- ==========================================================-- 22 23 -- ==========================================================-- 24 -- 25 spSuccs :: Point -> [Point] 26 27 spSuccs (d1, r1) = [(d1, r) | r <- spSuccsR d1 r1] 28 29 30 -- ==========================================================-- 31 -- 32 spSuccsR :: Domain -> Route -> [Route] 33 34 spSuccsR Two Zero = [One] 35 spSuccsR Two One = [] 36 37 spSuccsR (Lift1 ds) Stop1 38 = [Up1 (map avBottomR ds)] 39 spSuccsR (Lift1 [d]) (Up1 [r]) 40 = map (\rs -> Up1 [rs]) (spSuccsR d r) {-OPTIONAL-} 41 spSuccsR (Lift1 ds) (Up1 rs) 42 = map Up1 (myListVariants (map avBottomR ds) (myZipWith2 spSuccsR ds rs)) 43 44 spSuccsR (Lift2 ds) Stop2 45 = [Up2] 46 spSuccsR (Lift2 ds) Up2 47 = [UpUp2 (map avBottomR ds)] 48 spSuccsR (Lift2 [d]) (UpUp2 [r]) 49 = map (\rs -> UpUp2 [rs]) (spSuccsR d r) {-OPTIONAL-} 50 spSuccsR (Lift2 ds) (UpUp2 rs) 51 = map UpUp2 (myListVariants (map avBottomR ds) (myZipWith2 spSuccsR ds rs)) 52 53 spSuccsR d@(Func _ _) (Rep r) 54 = map Rep (spSuccsRep d r) 55 56 57 -- ==========================================================-- 58 -- 59 spSuccsRep :: Domain -> Rep -> [Rep] 60 61 spSuccsRep (Func dss Two) (RepTwo (Min1Max0 ar f1 f0)) 62 = [RepTwo (Min1Max0 ar [x] (sort (spPredsFrel dss x))) | x <- f0] 63 64 spSuccsRep (Func dss (Lift1 dts)) (Rep1 lf hfs) 65 = let hfDomains = map (avUncurry dss) dts 66 hfBottoms = map avBottomR_aux hfDomains 67 initTops = map avTopR dss 68 s1 = [spLEmb hfBottoms h 69 | RepTwo h <- spSuccsRep (Func dss Two) (RepTwo lf)] 70 s2 = [spLLift initTops dss hfDomains hfs2 71 | hfs2 <- myListVariants hfBottoms 72 (myZipWith2 spSuccsRep hfDomains hfs)] 73 in 74 avMinrep (s1 ++ s2) 75 76 spSuccsRep (Func dss (Lift2 dts)) (Rep2 lf mf hfs) 77 = let isoDomain = Func dss (Lift1 [Lift1 dts]) 78 isoRoute = Rep1 lf [Rep1 mf hfs] 79 isoSuccs = spSuccsRep isoDomain isoRoute 80 isoRouteInv (Rep1 lfi [Rep1 mfi hfsi]) 81 = Rep2 lfi mfi hfsi 82 in 83 map isoRouteInv isoSuccs 84 85 86 -- ==========================================================-- 87 -- 88 spSuccsFrel :: [Domain] -> FrontierElem -> [FrontierElem] 89 90 spSuccsFrel [d] (MkFrel [r]) 91 = map (\rs -> MkFrel [rs]) (spSuccsR d r) {-OPTIONAL-} 92 93 spSuccsFrel ds (MkFrel rs) 94 = map MkFrel (myListVariants (map avBottomR ds) (myZipWith2 spSuccsR ds rs)) 95 96 97 -- ==========================================================-- 98 -- 99 spLEmb :: [Rep] -> Frontier -> Rep 100 101 spLEmb hfBottoms h 102 = Rep1 h hfBottoms 103 104 105 -- ==========================================================-- 106 -- 107 spLLift :: [Route] -> [Domain] -> [Domain] -> [Rep] -> Rep 108 109 spLLift initTops initDss hfDomains hfs_reps 110 = let lf_arity = length initTops 111 zapped_hfs = myZipWith2 (spLLift_aux lf_arity initTops initDss) 112 hfDomains hfs_reps 113 new_lf = case foldr1 avLUBrep zapped_hfs of 114 RepTwo fr -> fr 115 in 116 Rep1 new_lf hfs_reps 117 118 119 -- ==========================================================-- 120 -- 121 spLLift_aux :: Int -> [Route] -> [Domain] -> Domain -> Rep -> Rep 122 123 spLLift_aux des_arity initTops initDss (Func dss Two) fr 124 = spLLift_reduce_arity_as_top des_arity initTops initDss fr 125 spLLift_aux des_arity initTops initDss (Func dss (Lift1 dts)) (Rep1 lf hfs) 126 = spLLift_reduce_arity_as_top des_arity initTops initDss (RepTwo lf) 127 spLLift_aux des_arity initTops initDss (Func dss (Lift2 dts)) (Rep2 lf mf hfs) 128 = spLLift_reduce_arity_as_top des_arity initTops initDss (RepTwo lf) 129 130 131 -- ==========================================================-- 132 -- 133 spLLift_reduce_arity_as_top :: Int -> [Route] -> [Domain] -> Rep -> Rep 134 135 spLLift_reduce_arity_as_top des_arity initTops initDss 136 f@(RepTwo (Min1Max0 ar f1 f0)) 137 | ar == des_arity 138 = f 139 | ar > des_arity 140 = let shorten (MkFrel rs) = MkFrel (take des_arity rs) 141 new_f1 = map shorten f1 142 new_f0 = spMax0FromMin1_aux initTops initDss new_f1 143 in 144 RepTwo (Min1Max0 des_arity new_f1 new_f0) 145 146 147 -- ==========================================================-- 148 -- 149 spPreds :: Point -> [Point] 150 151 spPreds (d1, r1) = [(d1, r) | r <- spPredsR d1 r1] 152 153 154 -- ==========================================================-- 155 -- 156 spPredsR :: Domain -> Route -> [Route] 157 158 spPredsR Two Zero = [] 159 spPredsR Two One = [Zero] 160 161 spPredsR (Lift1 ds) Stop1 162 = [] 163 spPredsR (Lift1 [d]) (Up1 [r]) 164 = if avIsBottomR r 165 then [Stop1] 166 else map (\rp -> Up1 [rp]) (spPredsR d r) {-OPTIONAL-} 167 spPredsR (Lift1 ds) (Up1 rs) 168 = if myAll avIsBottomR rs 169 then [Stop1] 170 else map Up1 (myListVariants (map avTopR ds) (myZipWith2 spPredsR ds rs)) 171 172 spPredsR (Lift2 ds) Stop2 173 = [] 174 spPredsR (Lift2 ds) Up2 175 = [Stop2] 176 spPredsR (Lift2 [d]) (UpUp2 [r]) 177 = if avIsBottomR r 178 then [Up2] 179 else map (\rp -> UpUp2 [rp]) (spPredsR d r) {-OPTIONAL-} 180 spPredsR (Lift2 ds) (UpUp2 rs) 181 = if myAll avIsBottomR rs 182 then [Up2] 183 else map UpUp2 (myListVariants (map avTopR ds) (myZipWith2 spPredsR ds rs)) 184 185 spPredsR d@(Func _ _) (Rep r) 186 = map Rep (spPredsRep d r) 187 188 189 -- ==========================================================-- 190 -- 191 spPredsRep :: Domain -> Rep -> [Rep] 192 193 spPredsRep (Func dss Two) (RepTwo (Min1Max0 ar f1 f0)) 194 = [RepTwo (Min1Max0 ar (sort (spSuccsFrel dss x)) [x]) | x <- f1] 195 196 spPredsRep (Func dss (Lift1 dts)) (Rep1 lf hfs) 197 = let hfDomains = map (avUncurry dss) dts 198 hfTops = map avTopR_aux hfDomains 199 lfDomain = Func dss Two 200 lfTop = avTopR_aux_2 dss 201 p1 = [spGEmb h dts 202 | RepTwo h <- spPredsRep lfDomain (RepTwo lf)] 203 p2 = [spGLift lfTop hfs2 204 | hfs2 <- myListVariants hfTops 205 (myZipWith2 spPredsRep hfDomains hfs)] 206 in 207 avMaxrep (p1 ++ p2) 208 209 spPredsRep (Func dss (Lift2 dts)) (Rep2 lf mf hfs) 210 = let isoDomain = Func dss (Lift1 [Lift1 dts]) 211 isoRoute = Rep1 lf [Rep1 mf hfs] 212 isoPreds = spPredsRep isoDomain isoRoute 213 isoRouteInv (Rep1 lfi [Rep1 mfi hfsi]) 214 = Rep2 lfi mfi hfsi 215 in 216 map isoRouteInv isoPreds 217 218 219 -- ==========================================================-- 220 -- 221 spPredsFrel :: [Domain] -> FrontierElem -> [FrontierElem] 222 223 spPredsFrel [d] (MkFrel [r]) 224 = map (\rp -> MkFrel [rp]) (spPredsR d r) {-OPTIONAL-} 225 226 spPredsFrel ds (MkFrel rs) 227 = map MkFrel (myListVariants (map avTopR ds) (myZipWith2 spPredsR ds rs)) 228 229 230 -- ==========================================================-- 231 -- 232 spGLift :: Frontier -> [Rep] -> Rep 233 234 spGLift lfTop hfs2 = Rep1 lfTop hfs2 235 236 237 -- ==========================================================-- 238 -- 239 spGEmb :: Frontier -> [Domain] -> Rep 240 241 spGEmb lf hfTargDs = Rep1 lf (map (spGEmb_aux lf) hfTargDs) 242 243 244 -- ==========================================================-- 245 -- 246 spGEmb_aux :: Frontier -> Domain -> Rep 247 248 spGEmb_aux lf Two 249 = RepTwo lf 250 251 spGEmb_aux lf (Lift1 dss) 252 = Rep1 lf (map (spGEmb_aux lf) dss) 253 254 spGEmb_aux lf (Lift2 dss) 255 = Rep2 lf lf (map (spGEmb_aux lf) dss) 256 257 spGEmb_aux lf (Func dss dt) 258 = spGEmb_aux 259 (case spGEmb_increase_arity_ignore lf dss of 260 RepTwo re -> re) 261 dt 262 263 264 -- ==========================================================-- 265 -- 266 spGEmb_increase_arity_ignore :: Frontier -> [Domain] -> Rep 267 268 spGEmb_increase_arity_ignore f [] 269 = RepTwo f {-OPTIONAL-} 270 271 spGEmb_increase_arity_ignore (Min1Max0 ar f1 f0) dss 272 = let tops = map avTopR dss 273 bottoms = map avBottomR dss 274 extend_top (MkFrel rs) = MkFrel (rs++tops) 275 extend_bottom (MkFrel rs) = MkFrel (rs++bottoms) 276 new_f1 = map extend_bottom f1 277 new_f0 = map extend_top f0 278 in 279 RepTwo (Min1Max0 (ar + length dss) new_f1 new_f0) 280 281 282 -- ==========================================================-- 283 -- 284 spMax0FromMin1 :: [Domain] -> [FrontierElem] -> [FrontierElem] 285 286 spMax0FromMin1 dss f1 287 = spMax0FromMin1_aux (map avTopR dss) dss f1 288 289 spMax0FromMin1_aux tops dss f1 290 = sort (foldr avLUBmax0frontier [MkFrel tops] 291 (map (spPredsFrel dss) f1)) 292 293 294 -- ==========================================================-- 295 -- 296 spMin1FromMax0 :: [Domain] -> [FrontierElem] -> [FrontierElem] 297 298 spMin1FromMax0 dss f0 299 = spMin1FromMax0_aux (map avBottomR dss) dss f0 300 301 spMin1FromMax0_aux bottoms dss f0 302 = sort (foldr avGLBmin1frontier [MkFrel bottoms] 303 (map (spSuccsFrel dss) f0)) 304 305 306 -- ==========================================================-- 307 -- === end SuccsAndPreds2.hs ===-- 308 -- ==========================================================--