1 2 -- ==========================================================-- 3 -- === Concretisation of function points. ===-- 4 -- === AbsConc3.hs ===-- 5 -- ==========================================================-- 6 7 module AbsConc3 where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 import AbstractVals2 12 import SuccsAndPreds2 13 import AbstractMisc 14 import DomainExpr 15 16 17 -- ==========================================================-- 18 -- 19 acUncurryWRT :: Domain -> Domain -> Domain 20 -- small big 21 -- 22 acUncurryWRT Two anyThing 23 = anyThing 24 25 acUncurryWRT (Lift1 ds1) (Lift1 ds2) 26 = Lift1 (myZipWith2 acUncurryWRT ds1 ds2) 27 28 acUncurryWRT (Lift2 ds1) (Lift2 ds2) 29 = Lift2 (myZipWith2 acUncurryWRT ds1 ds2) 30 31 acUncurryWRT (Func ds_s dt_s) (Func ds_b dt_b) 32 = let small_arity = length ds_s 33 big_arity = length ds_b 34 fixed_at_outer_level 35 = if small_arity == big_arity 36 then Func ds_b dt_b 37 else 38 if small_arity < big_arity 39 then Func (take small_arity ds_b) 40 (Func (drop small_arity ds_b) dt_b) 41 else panic "acUncurryWRT" 42 totally_fixed 43 = case fixed_at_outer_level of 44 Func ds_ol dt_ol 45 -> Func (myZipWith2 acUncurryWRT ds_s ds_ol) 46 (acUncurryWRT dt_s dt_ol) 47 in 48 totally_fixed 49 50 51 -- ==========================================================-- 52 -- 53 acNormAndCurried :: Domain -> Domain -> (Domain, Domain) 54 55 acNormAndCurried small_d big_d 56 = let big_d_u = amStrongNormalise big_d 57 in (big_d_u, acUncurryWRT small_d big_d_u) 58 59 60 -- ==========================================================-- 61 -- big domain smaller domain 62 acCompatible :: Domain -> Domain -> Bool 63 -- 64 -- In the (DFunc _ _) (DFunc _ _) case, note that 65 -- the big domain is 66 -- assumed to be curried, so its apparent arity is 67 -- the same as that of the small domain. 68 -- 69 acCompatible _ Two 70 = True 71 72 acCompatible (Lift1 ds1) (Lift1 ds2) 73 = myAndWith2 acCompatible ds1 ds2 74 75 acCompatible (Lift2 ds1) (Lift2 ds2) 76 = myAndWith2 acCompatible ds1 ds2 77 78 acCompatible (Func big_ss big_t) (Func smaller_ss smaller_t) 79 = acCompatible big_t smaller_t && 80 myAndWith2 acCompatible big_ss smaller_ss 81 82 acCompatible _ _ 83 = False 84 85 86 -- ==========================================================-- 87 -- 88 acConc :: ACMode -> Domain -> Domain -> Route -> Route 89 90 acConc s_or_l big_d small_d small_r 91 = let isFn = case small_d of { Func _ _ -> True; _ -> False } 92 (big_d_u, big_d_c) 93 = if isFn then acNormAndCurried small_d big_d else (big_d, big_d) 94 isOk = acCompatible big_d_c small_d 95 small_rep = case small_r of Rep rep -> rep 96 in 97 if big_d == small_d 98 then small_r 99 else 100 if not isOk 101 then panic "acConc: incompatible domains\n\n" 102 else 103 if isFn 104 then Rep (acConcRep s_or_l big_d_c big_d_u small_d small_rep) 105 else acConcData s_or_l big_d_u small_d small_r 106 107 108 -- ==========================================================-- 109 -- big small 110 -- 111 acConcData :: ACMode -> Domain -> Domain -> Route -> Route 112 113 acConcData s_or_l db Two One 114 = avTopR db 115 acConcData s_or_l db Two Zero 116 = avBottomR db 117 118 acConcData s_or_l (Lift1 dbs) (Lift1 dss) Stop1 119 = Stop1 120 acConcData s_or_l (Lift1 dbs) (Lift1 dss) (Up1 rs) 121 = Up1 (myZipWith3 (acConc s_or_l) dbs dss rs) 122 123 acConcData s_or_l (Lift2 dbs) (Lift2 dss) Stop2 124 = Stop2 125 acConcData s_or_l (Lift2 dbs) (Lift2 dss) Up2 126 = Up2 127 acConcData s_or_l (Lift2 dbs) (Lift2 dss) (UpUp2 rs) 128 = UpUp2 (myZipWith3 (acConc s_or_l) dbs dss rs) 129 130 131 -- ==========================================================-- 132 -- big_c big_u small 133 acConcRep :: ACMode -> Domain -> Domain -> Domain -> Rep -> Rep 134 135 acConcRep s_or_l big_d_c@(Func dss_b_c dt_b_c) 136 big_d_u@(Func dss_b_u dt_b_u) 137 small_d@(Func dss_s_c dt_s_c) 138 rep 139 = let concd_source 140 = acConcSource s_or_l big_d_u small_d rep 141 concd_source_d 142 = amStrongNormalise (acConcSourceD big_d_c small_d) 143 concd_all 144 = acConcTarget s_or_l dt_b_c concd_source_d concd_source 145 in 146 concd_all 147 148 149 -- ==========================================================-- 150 -- Concretise target domain of a function. 151 -- target_big rep_current 152 acConcTarget :: ACMode -> Domain -> Domain -> Rep -> Rep 153 -- target_big may be a function space, derived from 154 -- *curried* final desired domain. 155 -- 156 acConcTarget 157 s_or_l 158 Two 159 c@(Func dsc Two) 160 f@(RepTwo _) 161 = f 162 163 164 acConcTarget 165 s_or_l 166 (Lift1 dts) 167 c@(Func dsc Two) 168 f@(RepTwo fr) 169 = let doOne dt = acConcTarget s_or_l dt c f 170 in 171 Rep1 fr (map doOne dts) 172 173 174 acConcTarget 175 s_or_l 176 (Lift2 dts) 177 c@(Func dsc Two) 178 f@(RepTwo fr) 179 = let doOne dt = acConcTarget s_or_l dt c f 180 in 181 Rep2 fr fr (map doOne dts) 182 183 184 acConcTarget 185 s_or_l 186 (Func es g) 187 c@(Func dsc Two) 188 f@(RepTwo fr) 189 = let arity_increase = length es 190 new_c = Func (dsc++es) Two 191 increased_arity 192 = case s_or_l of 193 Safe -> ac_increase_arity_safe arity_increase dsc es fr 194 Live -> ac_increase_arity_live arity_increase dsc es fr 195 in 196 acConcTarget s_or_l g new_c increased_arity 197 198 199 acConcTarget 200 s_or_l 201 (Lift1 dts_b) 202 c@(Func dss (Lift1 dts_s)) 203 f@(Rep1 lf hfs) 204 = let hfds_small = map (avUncurry dss) dts_s 205 hfds_big = map (avUncurry dss) dts_b 206 hfds_targ = myZipWith2 doOne hfds_small hfds_big 207 doOne (Func xxss_s xxt_s) (Func xxss_b xxt_b) 208 = let xxss_fin = drop (length xxss_s) xxss_b 209 in 210 if null xxss_fin 211 then xxt_b 212 else Func xxss_fin xxt_b 213 hfs_big = myZipWith3 (acConcTarget s_or_l) hfds_targ hfds_small hfs 214 in 215 Rep1 lf hfs_big 216 217 218 acConcTarget 219 s_or_l 220 (Lift2 dts_b) 221 c@(Func dss (Lift2 dts_s)) 222 f@(Rep2 lf mf hfs) 223 = let hfds_small = map (avUncurry dss) dts_s 224 hfds_big = map (avUncurry dss) dts_b 225 hfds_targ = myZipWith2 doOne hfds_small hfds_big 226 doOne (Func xxss_s xxt_s) (Func xxss_b xxt_b) 227 = let xxss_fin = drop (length xxss_s) xxss_b 228 in 229 if null xxss_fin 230 then xxt_b 231 else Func xxss_fin xxt_b 232 hfs_big = myZipWith3 (acConcTarget s_or_l) hfds_targ hfds_small hfs 233 in 234 Rep2 lf mf hfs_big 235 236 237 238 -- ==========================================================-- 239 -- 240 ac_increase_arity_safe :: Int -> -- arity increase 241 [Domain] -> -- existing arg domains 242 [Domain] -> -- new arg domains 243 Frontier -> -- the function 244 Rep 245 246 ac_increase_arity_safe arity_increase argds new_argds fr 247 = let special_case = avIsBottomRep (RepTwo fr) 248 final_argds = argds ++ new_argds 249 new_bottoms = map avBottomR new_argds 250 special_fix = avBottomR_aux (Func final_argds Two) 251 in 252 if special_case 253 then special_fix 254 else ac_ia_aux Safe arity_increase new_bottoms final_argds fr 255 256 257 258 -- ==========================================================-- 259 -- 260 ac_increase_arity_live :: Int -> -- arity increase 261 [Domain] -> -- existing arg domains 262 [Domain] -> -- new arg domains 263 Frontier -> -- the function 264 Rep 265 266 ac_increase_arity_live arity_increase argds new_argds fr 267 = let special_case = avIsTopRep (RepTwo fr) 268 final_argds = argds ++ new_argds 269 new_tops = map avTopR new_argds 270 special_fix = avTopR_aux (Func final_argds Two) 271 in 272 if special_case 273 then special_fix 274 else ac_ia_aux Live arity_increase new_tops final_argds fr 275 276 277 278 -- ==========================================================-- 279 -- 280 ac_ia_aux :: ACMode -> -- mode 281 Int -> -- arity increase 282 [Route] -> -- top/bottom routes for new args 283 [Domain] -> -- arg domains **after** arity increase 284 Frontier -> -- the function 285 Rep 286 287 ac_ia_aux 288 s_or_l 289 ai 290 new_points 291 final_argds 292 (Min1Max0 ar f1 f0) 293 = let (new_f1, new_f0) = ac_extend_fr s_or_l final_argds f1 f0 new_points 294 in 295 RepTwo (Min1Max0 (ar+ai) new_f1 new_f0) 296 297 298 299 -- ==========================================================-- 300 -- 301 ac_extend_fr :: ACMode -> 302 [Domain] -> 303 [FrontierElem] -> 304 [FrontierElem] -> 305 [Route] -> 306 ([FrontierElem], [FrontierElem]) 307 308 ac_extend_fr s_or_l final_argds f1 f0 new_points 309 = let new_f0_safe = [MkFrel (frel++new_points) | MkFrel frel <- f0] 310 new_f1_safe = spMin1FromMax0 final_argds new_f0_safe 311 new_f1_live = [MkFrel (frel++new_points) | MkFrel frel <- f1] 312 new_f0_live = spMax0FromMin1 final_argds new_f1_live 313 in 314 case s_or_l of 315 Safe -> (new_f1_safe, new_f0_safe) 316 Live -> (new_f1_live, new_f0_live) 317 318 319 -- ==========================================================-- 320 -- big_args small_args 321 acConcSource_aux :: ACMode -> [Domain] -> [Domain] -> Frontier -> Frontier 322 323 acConcSource_aux Safe dbs dss (Min1Max0 ar f1 f0) 324 = let dbs_used = take ar dbs 325 new_f0 = map ( \(MkFrel pts) -> 326 MkFrel (myZipWith3 (acConc Safe) dbs_used dss pts)) f0 327 new_f1 = spMin1FromMax0 dbs_used new_f0 328 in 329 Min1Max0 ar new_f1 new_f0 330 331 acConcSource_aux Live dbs dss (Min1Max0 ar f1 f0) 332 = let dbs_used = take ar dbs 333 new_f1 = map ( \(MkFrel pts) -> 334 MkFrel (myZipWith3 (acConc Live) dbs_used dss pts)) f1 335 new_f0 = spMax0FromMin1 dbs_used new_f1 336 in 337 Min1Max0 ar new_f1 new_f0 338 339 340 -- ==========================================================-- 341 -- Concretise source domain of a function 342 -- big small 343 acConcSource :: ACMode -> Domain -> Domain -> Rep -> Rep 344 -- 345 -- we pass in the *entire* desired final domain of the 346 -- function, in *curried* form. This is preserved by 347 -- subsequent calls. In general 348 -- there may be more "dss" than components of each frontier 349 -- point. This is OK: only as many "dss" as are relevant 350 -- are actually concretised. "acConcTarget" 351 -- sticks on those "dss" components ignored here. 352 -- 353 354 acConcSource s_or_l (Func dss_b dt_b) 355 (Func dss_s Two) 356 (RepTwo fr) 357 = RepTwo (acConcSource_aux s_or_l dss_b dss_s fr) 358 359 360 acConcSource s_or_l (Func dss_b (Lift1 dts_b)) 361 (Func dss_s (Lift1 dts_s)) 362 (Rep1 lf hfs) 363 = let new_lf = acConcSource_aux s_or_l dss_b dss_s lf 364 hf_big_domains = map (avUncurry dss_b) dts_b 365 hf_small_domains = map (avUncurry dss_s) dts_s 366 new_hfs 367 = myZipWith3 (acConcSource s_or_l) hf_big_domains hf_small_domains hfs 368 in 369 Rep1 new_lf new_hfs 370 371 372 acConcSource s_or_l (Func dss_b (Lift2 dts_b)) 373 (Func dss_s (Lift2 dts_s)) 374 (Rep2 lf mf hfs) 375 = let new_lf = acConcSource_aux s_or_l dss_b dss_s lf 376 new_mf = acConcSource_aux s_or_l dss_b dss_s mf 377 hf_big_domains = map (avUncurry dss_b) dts_b 378 hf_small_domains = map (avUncurry dss_s) dts_s 379 new_hfs 380 = myZipWith3 (acConcSource s_or_l) hf_big_domains hf_small_domains hfs 381 in 382 Rep2 new_lf new_mf new_hfs 383 384 385 -- ==========================================================-- 386 -- Figure out the domain of the thing created by acConcSource. 387 -- big small 388 acConcSourceD :: Domain -> Domain -> Domain 389 390 acConcSourceD (Func dss_b dt_b) (Func dss_s Two) 391 = Func dss_b Two 392 393 acConcSourceD (Func dss_b (Lift1 dts_b)) (Func dss_s (Lift1 dts_s)) 394 = let low_fac_arity = length dss_s 395 hf_big_ds = map (avUncurry dss_b) dts_s {- XXXXXX -} 396 hf_small_ds = map (avUncurry dss_s) dts_s 397 hf_resultants = myZipWith2 acConcSourceD hf_big_ds hf_small_ds 398 hf_res2 = map drop_lf_ar hf_resultants 399 drop_lf_ar (Func ess et) 400 = let ess2 = drop low_fac_arity ess 401 in if null ess2 402 then et 403 else Func ess2 et 404 in 405 Func dss_b (Lift1 hf_res2) 406 407 acConcSourceD (Func dss_b (Lift2 dts_b)) (Func dss_s (Lift2 dts_s)) 408 = case 409 acConcSourceD (Func dss_b (Lift1 dts_b)) (Func dss_s (Lift1 dts_s)) 410 of 411 Func dss_res (Lift1 dts_res) -> Func dss_res (Lift2 dts_res) 412 413 414 -- ==========================================================-- 415 -- 416 acMakeInstance :: ACMode -> -- should be Safe for real applications 417 DExpr -> -- simplest instance domain of point (DXFunc _ _) 418 DSubst -> -- binds domain vars to required instances 419 Route -> -- simplest instance of function 420 Route -- function at desired instance 421 {- Constraints, assumptions, &c. 422 1. The domain variables in the DExpr correspond exactly with 423 those supplied in the DSubst. 424 2. The DExpr is of the form (DXFunc _ _) and correspondingly 425 the supplied Point is of the form (DFunc _ _, RFunc _), 426 and that the DFunc's args and DXFunc's args are 427 appropriately related. 428 -} 429 acMakeInstance s_or_l 430 simplest_dx 431 rho_d 432 f_simplest 433 = let 434 finalDomain = amStrongNormalise (dxApplyDSubst rho_d simplest_dx) 435 basicDomain = (dxApplyDSubst_2 simplest_dx) 436 in 437 acConc s_or_l finalDomain basicDomain f_simplest 438 439 440 -- ==========================================================-- 441 -- === end AbsConc3.hs ===-- 442 -- ==========================================================--