1 2 -- ==========================================================-- 3 -- === Miscellaneous operations in the Abstract value ===-- 4 -- === world. AbstractMisc.hs ===-- 5 -- ==========================================================-- 6 7 module AbstractMisc where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 import AbstractVals2 12 import SuccsAndPreds2 13 14 import List(nub) -- 1.3 15 16 -- ==========================================================-- 17 -- 18 amIAboves :: Domain -> Route -> [Route] 19 20 amIAboves d r = map (r \/) (spSuccsR d r) 21 22 23 -- ==========================================================-- 24 -- 25 amIBelows :: Domain -> Route -> [Route] 26 27 amIBelows d r = map (r /\) (spPredsR d r) 28 29 30 -- ==========================================================-- 31 -- 32 amPushUpFF :: Domain -> [Route] -> [Route] 33 34 amPushUpFF d [] = [] 35 amPushUpFF d xs = nub (concat (map (amIAboves d) xs)) 36 37 38 -- ==========================================================-- 39 -- 40 amPushDownFF :: Domain -> [Route] -> [Route] 41 42 amPushDownFF d [] = [] 43 amPushDownFF d xs = nub (concat (map (amIBelows d) xs)) 44 45 46 -- ==========================================================-- 47 -- 48 amAllUpSlices :: Domain -> [[Route]] 49 50 amAllUpSlices d 51 = takeWhile (not.null) (iterate (amPushUpFF d) [avBottomR d]) 52 53 54 -- ==========================================================-- 55 -- 56 amAllDownSlices :: Domain -> [[Route]] 57 58 amAllDownSlices d 59 = takeWhile (not.null) (iterate (amPushDownFF d) [avTopR d]) 60 61 62 -- ==========================================================-- 63 -- 64 amAllRoutes :: Domain -> [Route] 65 66 amAllRoutes Two 67 = [Zero, One] 68 69 amAllRoutes (Lift1 dss) 70 = Stop1 : map Up1 (myCartesianProduct (map amAllRoutes dss)) 71 72 amAllRoutes (Lift2 dss) 73 = Stop2 : Up2 : map UpUp2 (myCartesianProduct (map amAllRoutes dss)) 74 75 amAllRoutes (Func dss dt) 76 = concat (amAllUpSlices (Func dss dt)) 77 78 79 -- ==========================================================-- 80 -- 81 amUpCloseOfMinf :: Domain -> [Route] -> [Route] 82 83 amUpCloseOfMinf d [] 84 = [] 85 amUpCloseOfMinf d q@(x:_) 86 = x : (amUpCloseOfMinf d 87 (avMinR [ y \/ z | y <- q, z <- spSuccsR d x ])) 88 89 90 -- ==========================================================-- 91 -- 92 amDownCloseOfMaxf :: Domain -> [Route] -> [Route] 93 94 amDownCloseOfMaxf d [] 95 = [] 96 amDownCloseOfMaxf d q@(x:_) 97 = x : (amDownCloseOfMaxf d 98 (avMaxR [ y /\ z | y <- q, z <- spPredsR d x ])) 99 100 101 -- ==========================================================-- 102 -- 103 amAllRoutesMinusTopJONES :: Domain -> [Route] 104 105 amAllRoutesMinusTopJONES d 106 = amDownCloseOfMaxf d (spPredsR d (avTopR d)) 107 108 109 -- ==========================================================-- 110 -- 111 --amAllRoutesMinusTopMINE :: Domain -> [Route] 112 -- 113 --amAllRoutesMinusTopMINE d 114 -- = let sliceJustBelowTop 115 -- = spPredsR d (avTopR d) 116 -- allSlices 117 -- = takeWhile (not.null) 118 -- (iterate (amPushDownFF d) sliceJustBelowTop) 119 -- in 120 -- concat allSlices 121 122 123 -- ==========================================================-- 124 -- 125 amEqualPoints :: Point -> Point -> Bool 126 127 amEqualPoints (d1, r1) (d2, r2) 128 = if d1 == d2 129 then r1 == r2 130 else panic "Comparing points in different domains." 131 132 133 -- ==========================================================-- 134 -- 135 amIsaHOF :: Domain -> Bool 136 137 amIsaHOF (Func dss dt) 138 = amContainsFunctionSpace dt || 139 myAny amContainsFunctionSpace dss 140 141 142 -- ==========================================================-- 143 -- 144 amContainsFunctionSpace :: Domain -> Bool 145 146 amContainsFunctionSpace Two = False 147 amContainsFunctionSpace (Lift1 dss) = myAny amContainsFunctionSpace dss 148 amContainsFunctionSpace (Lift2 dss) = myAny amContainsFunctionSpace dss 149 amContainsFunctionSpace (Func _ _) = True 150 151 152 -- ==========================================================-- 153 -- 154 amIsDataFn :: Domain -> Bool 155 156 amIsDataFn (Func _ dt) = not (amContainsFunctionSpace dt) 157 158 159 -- ==========================================================-- 160 -- 161 amRepArity :: Rep -> Int 162 163 amRepArity (RepTwo (Min1Max0 ar f1 f0)) = ar 164 amRepArity (Rep1 (Min1Max0 lf_ar lf_f1 lf_f0) hfs) = lf_ar 165 amRepArity (Rep2 (Min1Max0 lf_ar lf_f1 lf_f0) mf hfs) = lf_ar 166 167 168 -- ==========================================================-- 169 -- 170 amStrongNormalise :: Domain -> Domain 171 172 amStrongNormalise Two 173 = Two 174 175 amStrongNormalise (Lift1 ds) 176 = Lift1 (map amStrongNormalise ds) 177 178 amStrongNormalise (Lift2 ds) 179 = Lift2 (map amStrongNormalise ds) 180 181 amStrongNormalise (Func dss (Func dss2 dt)) 182 = amStrongNormalise (Func (dss++dss2) dt) 183 184 amStrongNormalise (Func dss non_func_res) 185 = Func (map amStrongNormalise dss) (amStrongNormalise non_func_res) 186 187 188 -- ==========================================================-- 189 -- 190 amMeetIRoutes :: Domain -> [Route] 191 192 amMeetIRoutes Two 193 = [Zero] 194 amMeetIRoutes (Lift1 ds) 195 = Stop1 : 196 map Up1 (myListVariants (map avTopR ds) (map amMeetIRoutes ds)) 197 amMeetIRoutes (Lift2 ds) 198 = Stop2 : 199 Up2 : 200 map UpUp2 (myListVariants (map avTopR ds) (map amMeetIRoutes ds)) 201 202 203 -- ==========================================================-- 204 -- === end AbstractMisc.hs ===-- 205 -- ==========================================================-- 206