1 2 -- ==========================================================-- 3 -- === Implementation of Gebreselassie Baraki's ===-- 4 -- === polymorphism stuff BarakiConc.hs ===-- 5 -- ==========================================================-- 6 7 module BarakiConc3 where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 import AbstractVals2 12 import SuccsAndPreds2 13 import AbstractMisc 14 import DomainExpr 15 import AbsConc3 16 import BarakiMeet 17 18 19 -- ==================================================-- 20 -- === Application of a embedding functor (e-app) ===-- 21 -- === to a point. ===-- 22 -- ==================================================-- 23 24 -- ==========================================================-- 25 -- 26 bcEApp_d :: DRRSubst -> DExpr -> Domain 27 28 bcEApp_d rho DXTwo 29 = Two 30 bcEApp_d rho (DXLift1 dxs) 31 = Lift1 (map (bcEApp_d rho) dxs) 32 bcEApp_d rho (DXLift2 dxs) 33 = Lift2 (map (bcEApp_d rho) dxs) 34 bcEApp_d rho (DXFunc dss dt) 35 = Func (map (bcEApp_d rho) dss) (bcEApp_d rho dt) 36 bcEApp_d rho (DXVar alpha) 37 = bcGetD (utSureLookup rho "bcEApp_d" alpha) 38 39 40 -- ==========================================================-- 41 -- 42 bcEApp :: DRRSubst -> DExpr -> Route -> Route 43 44 bcEApp rho DXTwo Zero 45 = Zero 46 bcEApp rho DXTwo One 47 = One 48 49 bcEApp rho (DXLift1 dxs) Stop1 50 = Stop1 51 bcEApp rho (DXLift1 dxs) (Up1 rs) 52 = Up1 (myZipWith2 (bcEApp rho) dxs rs) 53 54 bcEApp rho (DXLift2 dxs) Stop2 55 = Stop2 56 bcEApp rho (DXLift2 dxs) Up2 57 = Up2 58 bcEApp rho (DXLift2 dxs) (UpUp2 rs) 59 = UpUp2 (myZipWith2 (bcEApp rho) dxs rs) 60 61 bcEApp rho (DXVar alpha) Zero 62 = bcGetR (utSureLookup rho "bcEApp(1)" alpha) 63 bcEApp rho (DXVar alpha) One 64 = bcGetT (utSureLookup rho "bcEApp(2)" alpha) 65 66 bcEApp rho (DXFunc dxss dxt) (Rep rep) 67 = let repDomain = dxApplyDSubst_2 (DXFunc dxss dxt) 68 in 69 bcEdotFdotC rho dxt repDomain rep dxss 70 71 72 -- =============================================-- 73 -- === Composition of an embedding functor e ===-- 74 -- === with a function f, hence: e.f ===-- 75 -- =============================================-- 76 77 -- ==========================================================-- 78 -- 79 bcEdotF :: DRRSubst -> -- binds domain variables to Points 80 DExpr -> -- the embedding functor "e" 81 Domain -> -- domain of some function "f" 82 Rep -> -- representation of "f" 83 Rep -- representation of "e.f" 84 85 86 bcEdotF 87 rho 88 DXTwo 89 d@(Func _ Two) 90 f@(RepTwo _) 91 = f 92 93 94 bcEdotF 95 rho 96 (DXLift1 dxs) 97 d@(Func dss (Lift1 dts)) 98 f@(Rep1 lf hfs) 99 = let hf_domains = map (avUncurry dss) dts 100 new_hfs = myZipWith3 (bcEdotF rho) dxs hf_domains hfs 101 in 102 Rep1 lf new_hfs 103 104 105 bcEdotF 106 rho 107 (DXLift2 dxs) 108 d@(Func dss (Lift2 dts)) 109 f@(Rep2 lf mf hfs) 110 = let hf_domains = map (avUncurry dss) dts 111 new_hfs = myZipWith3 (bcEdotF rho) dxs hf_domains hfs 112 in 113 Rep2 lf mf new_hfs 114 115 116 bcEdotF 117 rho 118 (DXVar alpha) 119 d@(Func ds2 Two) 120 f@(RepTwo f1f0) 121 = let f_top = avTopR_aux_2 ds2 122 f_top_rep = RepTwo f_top 123 124 evb Two = f 125 evb (Lift1 es) = Rep1 f1f0 (map evb es) 126 evb (Lift2 es) = Rep2 f1f0 f1f0 (map evb es) 127 128 ev Two Zero = f 129 ev Two One = f_top_rep 130 131 ev (Lift1 es) Stop1 = Rep1 f1f0 (map evb es) 132 ev (Lift1 es) (Up1 rs) = Rep1 f_top (myZipWith2 ev es rs) 133 134 ev (Lift2 es) Stop2 = Rep2 f1f0 f1f0 (map evb es) 135 ev (Lift2 es) Up2 = Rep2 f_top f1f0 (map evb es) 136 ev (Lift2 es) (UpUp2 rs) = Rep2 f_top f_top (myZipWith2 ev es rs) 137 138 evLookup = utSureLookup rho "bcEdotF" alpha 139 evD = bcGetD evLookup 140 evR = bcGetR evLookup 141 in 142 ev evD evR 143 144 145 146 -- =============================================-- 147 -- === Composition of a function f with a ===-- 148 -- === list of closure functors [c1 ... cn], ===-- 149 -- === hence: "f.[c1 ... cn]" ===-- 150 -- =============================================-- 151 152 -- ==========================================================-- 153 -- 154 bcFdotC :: DRRSubst -> -- binds domain variables to Points 155 [DExpr] -> -- the closure functor "[c1 ... cn]" 156 [Domain] -> -- ???????????????????????? 157 Domain -> -- domain of some function "f" 158 Rep -> -- representation of "f" 159 Rep -- representation of "f.[c1 ... cn]" 160 161 bcFdotC rho dxs newDs (Func dss dt) rep 162 = let new_rep = bcApplyF0 eapp_pt newDs rep 163 eapp_pt (MkFrel fels) 164 = MkFrel (myZipWith2 (bcEApp rho) dxs fels) 165 in 166 new_rep 167 168 169 -- ==========================================================-- 170 -- apply some function to the max0 frontiers of a function 171 -- and recalculate the corresponding min1 frontiers. 172 -- 173 bcApplyF0 :: (FrontierElem -> 174 FrontierElem) -> -- what to apply to min1 points 175 [Domain] -> -- source domains of abstract function 176 Rep -> -- abstract function 177 Rep -- resulting abstract function 178 179 bcApplyF0 f dss (RepTwo fr) 180 = RepTwo (bcApplyF0_2 f dss fr) 181 182 bcApplyF0 f dss (Rep1 lf hfs) 183 = let new_lf = bcApplyF0_2 f dss lf 184 new_hfs = map (bcApplyF0 f dss) hfs 185 in 186 Rep1 new_lf new_hfs 187 188 bcApplyF0 f dss (Rep2 lf mf hfs) 189 = let new_lf = bcApplyF0_2 f dss lf 190 new_mf = bcApplyF0_2 f dss mf 191 new_hfs = map (bcApplyF0 f dss) hfs 192 in 193 Rep2 new_lf new_mf new_hfs 194 195 196 -- ==========================================================-- 197 -- 198 bcApplyF0_2 :: (FrontierElem -> FrontierElem) -> 199 [Domain] -> 200 Frontier -> 201 Frontier 202 203 bcApplyF0_2 f dss fr@(Min1Max0 ar f1 f0) 204 = let new_f0 = map f f0 205 new_f1 = [] 206 in 207 Min1Max0 ar new_f1 new_f0 208 209 210 -- =================================================-- 211 -- === Given embedding functor "e", function "f" ===-- 212 -- === and closure functor "c", computes ===-- 213 -- === "e.f.c" (ie "Ge.f2.Fc", in accordance ===-- 214 -- === with Baraki's theory). ===-- 215 -- =================================================-- 216 217 -- ==========================================================-- 218 -- 219 bcEdotFdotC :: DRRSubst -> -- binds domain variables to Points 220 DExpr -> -- target domain functor, "Ge" 221 Domain -> -- domain of "f2" 222 Rep -> -- the function "f2" 223 [DExpr] -> -- source domain functors, "F[c1 ... cn]" 224 Route 225 226 bcEdotFdotC rho g_e fDomain@(Func fds fdt) f f_cs 227 = let f_dot_c = bcFdotC rho f_cs newDs fDomain f 228 newDs = map (bcEApp_d rho) f_cs 229 fd_dot_c = Func newDs fdt 230 e_dot_f_dot_c = bcEdotF rho g_e fd_dot_c f_dot_c 231 in 232 Rep e_dot_f_dot_c 233 234 235 -- ==========================================================-- 236 -- 237 bcGetR (d, r, t) = r 238 bcGetD (d, r, t) = d 239 bcGetT (d, r, t) = t 240 241 242 -- =========================================================-- 243 -- === Do Baraki-style concretisation of function points ===-- 244 -- =========================================================-- 245 246 -- ==========================================================-- 247 -- 248 bcMakeInstance :: 249 Bool -> -- True if use Baraki, False if use Conc 250 Int -> -- How hard to work (for Baraki) 251 ACMode -> -- Mode for Conc (IRRELEVANT) 252 DExpr -> -- simplest instance domain of point (DXFunc _ _) 253 DSubst -> -- binds domain vars to required instances 254 Route -> -- simplest instance of function 255 Route -- function at desired instance 256 257 ------------------------------------------------------------------- 258 -- Function-valued objects case. -- 259 ------------------------------------------------------------------- 260 -- Constraints, assumptions, &c. -- 261 ------------------------------------------------------------------- 262 -- 1. The function in question must be first-order. -- 263 -- 2. The domain variables in the DExpr correspond exactly with -- 264 -- those supplied in the DSubst. -- 265 -- 3. The DExpr is of the form (DXFunc _ _) and correspondingly -- 266 -- the supplied Point is of the form (DFunc _ _, RFunc _), -- 267 -- and that the DFunc's args and DXFunc's args are -- 268 -- appropriately related. -- 269 ------------------------------------------------------------------- 270 bcMakeInstance 271 use_baraki 272 threshold 273 s_or_l 274 simplest_dirty@(DXFunc args_f_functors_dirty result_g_functor_dirty) 275 rho_d 276 f@(Rep fRep) 277 = let 278 --------------------------- 279 -- Clean up the functors -- 280 --------------------------- 281 282 simplest@(DXFunc args_f_functors result_g_functor) 283 = bcClean simplest_dirty 284 285 ----------------------------------------- 286 -- The domain of the simplest instance -- 287 ----------------------------------------- 288 289 simplestD = dxApplyDSubst_2 simplest 290 291 ----------------------------------------------- 292 -- the domain variables in the instantiation -- 293 ----------------------------------------------- 294 295 domainVarNames = map first rho_d 296 297 -------------------------------------------------- 298 -- the domains corresponding to those variables -- 299 -------------------------------------------------- 300 301 bigInstanceDomains = map second rho_d 302 303 ----------------------------------------------------- 304 -- Find out if we actually need to do anything. -- 305 -- baseInstance will also be True if this is -- 306 -- f is non-polymorphic, since rho_d will be empty -- 307 ----------------------------------------------------- 308 309 baseInstance = myAll (==Two) bigInstanceDomains 310 311 ------------------------------------------------------- 312 -- find out if we can actually use Baraki's stuff. -- 313 -- No function spaces in instantiations, and -- 314 -- no non-top-level function spaces in the function. -- 315 ------------------------------------------------------- 316 317 barakiApplicable 318 = myAll (not.amContainsFunctionSpace) bigInstanceDomains && 319 (not.dxContainsFnSpace) result_g_functor && 320 myAll (not.dxContainsSubsidiaryFnSpace) args_f_functors 321 322 ----------------------------------------------------- 323 -- Find out if we can use Baraki's first order -- 324 -- optimisations. This requires first order -- 325 -- instantiations of a first order function. -- 326 -- The former condition is true anyway if we're -- 327 -- using Baraki's method. -- 328 ----------------------------------------------------- 329 330 canUseOpt 331 = all (not.dxContainsFnSpace) args_f_functors 332 333 ----------------------------------------------------------- 334 -- the set of points over which we have to take the meet -- 335 ----------------------------------------------------------- 336 337 bigInstancePoints 338 = let 339 individualIndices 340 = if canUseOpt 341 then map amMeetIRoutes bigInstanceDomains 342 else map amAllRoutesMinusTopJONES bigInstanceDomains 343 allIndices 344 = myCartesianProduct individualIndices 345 in 346 take (max 1 threshold) allIndices 347 348 -------------------------------------- 349 -- The tops of the instance domains -- 350 -------------------------------------- 351 352 instanceTops = map avTopR bigInstanceDomains 353 354 ------------------------------------------------------------- 355 -- all the bindings of domain variables to relevant points -- 356 ------------------------------------------------------------- 357 358 allRhos 359 = let makeOneRho rs 360 = myZipWith4 (\n d r t -> (n, (d, r, t))) 361 domainVarNames bigInstanceDomains rs instanceTops 362 in 363 map makeOneRho bigInstancePoints 364 365 --------------------------------------------- 366 -- all of the e.f.[c1 ... cn] compositions -- 367 --------------------------------------------- 368 369 all_edotfdotc 370 = let makeOneEdotFdotC rho 371 = bcEdotFdotC rho result_g_functor simplestD 372 fRep args_f_functors 373 in 374 map makeOneEdotFdotC allRhos 375 376 ---------------------------------------------------- 377 -- the domain of the function after instantiation -- 378 ---------------------------------------------------- 379 380 big_function_domain = dxApplyDSubst rho_d simplest 381 382 in 383 if baseInstance 384 then f 385 else if not use_baraki || not barakiApplicable 386 then acMakeInstance s_or_l simplest rho_d f 387 else bmNorm big_function_domain (foldl1 bmGLB all_edotfdotc) 388 389 390 ---------------------------------------- 391 -- Non-function valued objects case. -- 392 -- Just use Conc. In principle could -- 393 -- use Baraki but I don't think this -- 394 -- is really worth bothering with. -- 395 ---------------------------------------- 396 bcMakeInstance 397 use_baraki 398 threshold 399 s_or_l 400 simplest 401 rho_d 402 f 403 = acMakeInstance s_or_l simplest rho_d f 404 405 406 -- ==========================================================-- 407 -- 408 bcClean :: DExpr -> DExpr 409 410 bcClean DXTwo = DXTwo 411 bcClean (DXLift1 []) = DXTwo 412 bcClean (DXLift2 []) = DXLift1 [DXTwo] 413 bcClean (DXLift1 dxs) = DXLift1 (map bcClean dxs) 414 bcClean (DXLift2 dxs) = DXLift2 (map bcClean dxs) 415 bcClean (DXVar v) = DXVar v 416 bcClean (DXFunc dxss dxt) = DXFunc (map bcClean dxss) (bcClean dxt) 417 418 -- ==========================================================-- 419 -- === end BarakiConc.hs ===-- 420 -- ==========================================================--