1 2 -- ==========================================================-- 3 -- === Find frontiers using Hunt's algorithm. ===-- 4 -- === Only works for functions whose result lattice ===-- 5 -- === does not contain any function spaces ===-- 6 -- === ("data functions"). ===-- 7 -- === ===-- 8 -- === FrontierDATAFN.hs ===-- 9 -- ==========================================================-- 10 11 module FrontierDATAFN2 where 12 import BaseDefs 13 import Utils 14 import MyUtils 15 import AbstractVals2 16 import SuccsAndPreds2 17 import AbstractMisc 18 import AbstractEval2 19 import AbsConc3 20 import FrontierMisc2 21 22 23 24 -- ==========================================================-- 25 -- 26 fdImprove :: (Route -> Route) -> -- coercion function 27 MemoList -> -- possibly useful info 28 [Domain] -> -- argument domains 29 Bool -> -- True == naive startup 30 [FrontierElem] -> -- max-0 superset 31 [FrontierElem] -> -- min-1 superset 32 ([FrontierElem], [FrontierElem]) 33 34 fdImprove coerce memo dss naive max0_super min1_super 35 = let 36 (zero_result_pairs, one_result_pairs) 37 = splitList (fdIsZero.coerce.second) memo 38 zero_nodes_max 39 = avMaxfrel (map (MkFrel . first) zero_result_pairs) 40 one_nodes_min 41 = avMinfrel (map (MkFrel . first) one_result_pairs) 42 new_max0 43 = (if naive then [MkFrel (map avTopR dss)] else max0_super) 44 `avLUBmax0frontier` 45 (spMax0FromMin1 dss one_nodes_min) 46 new_min1 47 = (if naive then [MkFrel (map avBottomR dss)] else min1_super) 48 `avGLBmin1frontier` 49 (spMin1FromMax0 dss zero_nodes_max) 50 in 51 (new_max0, new_min1) 52 53 54 -- ==========================================================-- 55 -- 56 fdFind :: ACMode -> 57 HExpr Naam -> -- tree of abstract function 58 Domain -> -- domain of function to be found 59 [Domain] -> -- small arg domains 60 [Domain] -> -- big arg domains 61 Rep -> -- bounding rep 62 (Route -> Route) -> -- the coercion function 63 Bool -> -- True == naive startup 64 [FrontierElem] -> -- inherited low factor's min-1-frontier 65 MemoList -> -- possibly useful information 66 (Rep, MemoList) 67 68 fdFind s_or_l hexpr (Func dss Two) small_argds big_argds 69 (RepTwo (Min1Max0 ar_prev min1_prev max0_prev)) 70 coerce naive min1_ilf memo 71 = let 72 (better_max0, better_min1) 73 = fdImprove coerce memo small_argds naive max0_prev min1_prev 74 (fr, new_memo_additions) 75 = fdFs2 s_or_l hexpr small_argds big_argds 76 ( {-min1_ilf `avGLBmin1frontier`-} better_min1) 77 better_max0 coerce 78 in 79 (RepTwo fr, 80 new_memo_additions) 81 82 83 fdFind s_or_l hexpr (Func dss (Lift1 dts)) small_argds big_argds 84 (Rep1 (Min1Max0 ar_prev min1_prev_lf max0_prev_lf) prev_hfs) 85 coerce naive min1_ilf memo 86 = let 87 (better_lf_max0, better_lf_min1) 88 = fdImprove (fdLo1.coerce) memo small_argds naive 89 max0_prev_lf min1_prev_lf 90 (lofact, lofact_memo_additions) 91 = fdFs2 s_or_l hexpr small_argds big_argds 92 ( {-min1_ilf `avGLBmin1frontier`-} better_lf_min1) 93 better_lf_max0 (fdLo1.coerce) 94 useful_lofact_memo 95 = filter (not.fdIsZero.fdLo1.coerce.second) 96 (lofact_memo_additions ++ memo) 97 98 min1_lofact 99 = case lofact of {Min1Max0 lf_ar lf_f1 lf_f0 -> lf_f1} 100 101 (hifacts, hifact_memo_additions) 102 = fdFind_aux s_or_l small_argds big_argds dts hexpr prev_hfs coerce 103 useful_lofact_memo False min1_lofact naive 104 in 105 (Rep1 lofact hifacts, 106 lofact_memo_additions ++ hifact_memo_additions) 107 108 109 fdFind s_or_l hexpr (Func dss (Lift2 dts)) small_argds big_argds 110 (Rep2 (Min1Max0 ar_prev_lf min1_prev_lf max0_prev_lf) 111 (Min1Max0 ar_prev_mf min1_prev_mf max0_prev_mf) prev_hfs) 112 coerce naive min1_ilf memo 113 = let 114 (better_lf_max0, better_lf_min1) 115 = fdImprove (fdLo2.coerce) memo small_argds naive 116 max0_prev_lf min1_prev_lf 117 (lofact, lofact_memo_additions) 118 = fdFs2 s_or_l hexpr small_argds big_argds 119 ( {-min1_ilf `avGLBmin1frontier`-} better_lf_min1) 120 better_lf_max0 (fdLo2.coerce) 121 useful_lofact_memo 122 = filter (not.fdIsZero.fdLo2.coerce.second) 123 (lofact_memo_additions ++ memo) 124 125 min1_lofact 126 = case lofact of {Min1Max0 lf_ar lf_f1 lf_f0 -> lf_f1} 127 128 (better_mf_max0, better_mf_min1) 129 = fdImprove (fdMid2.coerce) useful_lofact_memo small_argds naive 130 max0_prev_mf min1_prev_mf 131 (midfact, midfact_memo_additions) 132 = fdFs2 s_or_l hexpr small_argds big_argds 133 ( {-min1_lofact `avGLBmin1frontier`-} better_mf_min1) 134 better_mf_max0 (fdMid2.coerce) 135 useful_midfact_memo 136 = filter (not.fdIsZero.fdMid2.coerce.second) 137 (midfact_memo_additions ++ useful_lofact_memo) 138 139 min1_midfact 140 = case midfact of {Min1Max0 mf_ar mf_f1 mf_f0 -> mf_f1} 141 142 (hifacts, hifact_memo_additions) 143 = fdFind_aux s_or_l small_argds big_argds dts hexpr prev_hfs coerce 144 useful_midfact_memo True min1_midfact naive 145 in 146 (Rep2 lofact midfact hifacts, 147 lofact_memo_additions ++ 148 midfact_memo_additions ++ hifact_memo_additions) 149 150 151 -- ==========================================================-- 152 -- 153 fdFind_aux :: ACMode -> 154 [Domain] -> -- small argument domains 155 [Domain] -> -- big argument domains 156 [Domain] -> -- result domains 157 HExpr Naam -> -- the tree 158 [Rep] -> -- previous high factors 159 (Route -> Route) -> -- unlifted coercion function 160 MemoList -> -- the memo 161 Bool -> -- True => Lift2, False => Lift1 162 [FrontierElem] -> -- inherited low factor 163 Bool -> -- True => naive startup 164 ([Rep], MemoList) 165 166 167 fdFind_aux s_or_l small_argds big_argds dts hexpr prev_hfs coerce 168 initial_hf_memo double_lift min1_ilf naive 169 = let 170 high_coerce 171 = if double_lift then fdHi2 else fdHi1 172 small_hifact_domains 173 = map (avUncurry small_argds) dts 174 hifact_info_tuples 175 = myZipWith4 mkTuple (0 `myIntsFromTo` (length dts - 1)) 176 prev_hfs (map avBottomR dts) small_hifact_domains 177 mkTuple n hf_prev bottom small_hf_domain 178 = (small_hf_domain, (high_coerce bottom n . coerce), hf_prev) 179 180 (hf_memo_additions, hifacts) 181 = mapAccuml doOne [] hifact_info_tuples 182 183 doOne memo_adds_so_far (hf_dom, hf_coerce, hf_preev) 184 = let (rep, more_memo_additions) 185 = fdFind s_or_l hexpr hf_dom small_argds big_argds 186 hf_preev hf_coerce naive min1_ilf 187 (memo_adds_so_far ++ initial_hf_memo) 188 in (more_memo_additions ++ memo_adds_so_far, rep) 189 in 190 (hifacts, hf_memo_additions) 191 192 193 -- ==========================================================-- 194 -- 195 fdIdent :: Route -> Route 196 fdIdent p = p 197 198 fdLo1 :: Route -> Route 199 fdLo1 Stop1 = Zero 200 fdLo1 (Up1 rs) = One 201 202 fdHi1 :: Route -> Int -> Route -> Route 203 fdHi1 bottom n Stop1 = bottom 204 fdHi1 bottom n (Up1 rs) = rs ## n 205 206 fdLo2 :: Route -> Route 207 fdLo2 Stop2 = Zero 208 fdLo2 Up2 = One 209 fdLo2 (UpUp2 rs) = One 210 211 fdMid2 :: Route -> Route 212 fdMid2 Stop2 = Zero 213 fdMid2 Up2 = Zero 214 fdMid2 (UpUp2 rs) = One 215 216 fdHi2 :: Route -> Int -> Route -> Route 217 fdHi2 bottom n Stop2 = bottom 218 fdHi2 bottom n Up2 = bottom 219 fdHi2 bottom n (UpUp2 rs) = rs ## n 220 221 fdIsZero :: Route -> Bool 222 fdIsZero x = case x of {Zero -> True; One -> False} 223 224 225 -- ==========================================================-- 226 -- 227 fdFs2 :: ACMode -> 228 HExpr Naam -> -- the tree 229 [Domain] -> -- small arg domains 230 [Domain] -> -- big arg domains 231 [FrontierElem] -> -- min-1 superset (inherited low factor) 232 [FrontierElem] -> -- max-0 superset (previous value) 233 (Route -> Route) -> -- the coercion function 234 (Frontier, MemoList) 235 236 fdFs2 s_or_l hexpr small_argds big_argds min1_prev max0_prev coerce 237 = let initial_yy 238 = max0_prev 239 initial_xx 240 = min1_prev 241 (final_yy, final_xx, finalMemo) 242 = fdFs_aux s_or_l hexpr small_argds big_argds coerce 243 initial_yy initial_xx True [] (utRandomInts 1 2) 244 result 245 = Min1Max0 (length small_argds) final_xx final_yy 246 in 247 --if not (sane result small_argds) 248 --then panic (show (min1_prev, max0_prev, 249 -- fmSelect 2 initial_xx initial_yy False)) else 250 (result, finalMemo) 251 252 --sane (Min1Max0 ar f1 f0) dss 253 -- = f1 == spMin1FromMax0 dss f0 && 254 -- f0 == spMax0FromMin1 dss f1 255 256 257 -- ==========================================================-- 258 -- 259 fdFs_aux :: ACMode -> 260 HExpr Naam -> -- the tree 261 [Domain] -> -- small argument domains 262 [Domain] -> -- big argument domains 263 (Route -> Route) -> -- the coercion function 264 [FrontierElem] -> -- tentative max-0 frontier 265 [FrontierElem] -> -- tentative min-1 frontier 266 Bool -> -- True == take from top 267 MemoList -> -- memo list so far 268 [Int] -> 269 ([FrontierElem], [FrontierElem], MemoList) 270 271 fdFs_aux s_or_l hexpr small_argds big_argds 272 coerce trial_max_yy trial_min_xx fromTop memo rands 273 = let edgez 274 = fmSelect (head rands) trial_min_xx trial_max_yy fromTop 275 Just (MkFrel args) 276 = edgez 277 args_at_proper_sizes 278 = myZipWith3 (acConc s_or_l) big_argds small_argds args 279 evald_app 280 = aeEvalExact hexpr (map HPoint args_at_proper_sizes) 281 coerced_evald_app 282 = coerce evald_app 283 revised_max_yy 284 = fmReviseMaxYY small_argds trial_max_yy (MkFrel args) 285 revised_min_xx 286 = fmReviseMinXX small_argds trial_min_xx (MkFrel args) 287 new_memo 288 = (args, evald_app) : memo 289 in 290 if fmIsNothing edgez 291 then (sort trial_max_yy, sort trial_min_xx, memo) 292 else 293 if coerced_evald_app == One 294 then fdFs_aux s_or_l 295 hexpr small_argds big_argds coerce 296 revised_max_yy trial_min_xx False new_memo (tail rands) 297 else 298 if coerced_evald_app == Zero 299 then fdFs_aux s_or_l 300 hexpr small_argds big_argds coerce 301 trial_max_yy revised_min_xx True new_memo (tail rands) 302 else panic "fdFs_aux" 303 304 305 306 -- ==========================================================-- 307 -- === end FrontierDATAFN.hs ===-- 308 -- ==========================================================--