-- ==========================================================-- -- === Implementation of Gebreselassie Baraki's ===-- -- === polymorphism stuff BarakiConc.hs ===-- -- ==========================================================-- module BarakiConc3 where import BaseDefs import Utils import MyUtils import AbstractVals2 import SuccsAndPreds2 import AbstractMisc import DomainExpr import AbsConc3 import BarakiMeet -- ==================================================-- -- === Application of a embedding functor (e-app) ===-- -- === to a point. ===-- -- ==================================================-- -- ==========================================================-- -- bcEApp_d :: DRRSubst -> DExpr -> Domain bcEApp_d rho DXTwo = Two bcEApp_d rho (DXLift1 dxs) = Lift1 (map (bcEApp_d rho) dxs) bcEApp_d rho (DXLift2 dxs) = Lift2 (map (bcEApp_d rho) dxs) bcEApp_d rho (DXFunc dss dt) = Func (map (bcEApp_d rho) dss) (bcEApp_d rho dt) bcEApp_d rho (DXVar alpha) = bcGetD (utSureLookup rho "bcEApp_d" alpha) -- ==========================================================-- -- bcEApp :: DRRSubst -> DExpr -> Route -> Route bcEApp rho DXTwo Zero = Zero bcEApp rho DXTwo One = One bcEApp rho (DXLift1 dxs) Stop1 = Stop1 bcEApp rho (DXLift1 dxs) (Up1 rs) = Up1 (myZipWith2 (bcEApp rho) dxs rs) bcEApp rho (DXLift2 dxs) Stop2 = Stop2 bcEApp rho (DXLift2 dxs) Up2 = Up2 bcEApp rho (DXLift2 dxs) (UpUp2 rs) = UpUp2 (myZipWith2 (bcEApp rho) dxs rs) bcEApp rho (DXVar alpha) Zero = bcGetR (utSureLookup rho "bcEApp(1)" alpha) bcEApp rho (DXVar alpha) One = bcGetT (utSureLookup rho "bcEApp(2)" alpha) bcEApp rho (DXFunc dxss dxt) (Rep rep) = let repDomain = dxApplyDSubst_2 (DXFunc dxss dxt) in bcEdotFdotC rho dxt repDomain rep dxss -- =============================================-- -- === Composition of an embedding functor e ===-- -- === with a function f, hence: e.f ===-- -- =============================================-- -- ==========================================================-- -- bcEdotF :: DRRSubst -> -- binds domain variables to Points DExpr -> -- the embedding functor "e" Domain -> -- domain of some function "f" Rep -> -- representation of "f" Rep -- representation of "e.f" bcEdotF rho DXTwo d@(Func _ Two) f@(RepTwo _) = f bcEdotF rho (DXLift1 dxs) d@(Func dss (Lift1 dts)) f@(Rep1 lf hfs) = let hf_domains = map (avUncurry dss) dts new_hfs = myZipWith3 (bcEdotF rho) dxs hf_domains hfs in Rep1 lf new_hfs bcEdotF rho (DXLift2 dxs) d@(Func dss (Lift2 dts)) f@(Rep2 lf mf hfs) = let hf_domains = map (avUncurry dss) dts new_hfs = myZipWith3 (bcEdotF rho) dxs hf_domains hfs in Rep2 lf mf new_hfs bcEdotF rho (DXVar alpha) d@(Func ds2 Two) f@(RepTwo f1f0) = let f_top = avTopR_aux_2 ds2 f_top_rep = RepTwo f_top evb Two = f evb (Lift1 es) = Rep1 f1f0 (map evb es) evb (Lift2 es) = Rep2 f1f0 f1f0 (map evb es) ev Two Zero = f ev Two One = f_top_rep ev (Lift1 es) Stop1 = Rep1 f1f0 (map evb es) ev (Lift1 es) (Up1 rs) = Rep1 f_top (myZipWith2 ev es rs) ev (Lift2 es) Stop2 = Rep2 f1f0 f1f0 (map evb es) ev (Lift2 es) Up2 = Rep2 f_top f1f0 (map evb es) ev (Lift2 es) (UpUp2 rs) = Rep2 f_top f_top (myZipWith2 ev es rs) evLookup = utSureLookup rho "bcEdotF" alpha evD = bcGetD evLookup evR = bcGetR evLookup in ev evD evR -- =============================================-- -- === Composition of a function f with a ===-- -- === list of closure functors [c1 ... cn], ===-- -- === hence: "f.[c1 ... cn]" ===-- -- =============================================-- -- ==========================================================-- -- bcFdotC :: DRRSubst -> -- binds domain variables to Points [DExpr] -> -- the closure functor "[c1 ... cn]" [Domain] -> -- ???????????????????????? Domain -> -- domain of some function "f" Rep -> -- representation of "f" Rep -- representation of "f.[c1 ... cn]" bcFdotC rho dxs newDs (Func dss dt) rep = let new_rep = bcApplyF0 eapp_pt newDs rep eapp_pt (MkFrel fels) = MkFrel (myZipWith2 (bcEApp rho) dxs fels) in new_rep -- ==========================================================-- -- apply some function to the max0 frontiers of a function -- and recalculate the corresponding min1 frontiers. -- bcApplyF0 :: (FrontierElem -> FrontierElem) -> -- what to apply to min1 points [Domain] -> -- source domains of abstract function Rep -> -- abstract function Rep -- resulting abstract function bcApplyF0 f dss (RepTwo fr) = RepTwo (bcApplyF0_2 f dss fr) bcApplyF0 f dss (Rep1 lf hfs) = let new_lf = bcApplyF0_2 f dss lf new_hfs = map (bcApplyF0 f dss) hfs in Rep1 new_lf new_hfs bcApplyF0 f dss (Rep2 lf mf hfs) = let new_lf = bcApplyF0_2 f dss lf new_mf = bcApplyF0_2 f dss mf new_hfs = map (bcApplyF0 f dss) hfs in Rep2 new_lf new_mf new_hfs -- ==========================================================-- -- bcApplyF0_2 :: (FrontierElem -> FrontierElem) -> [Domain] -> Frontier -> Frontier bcApplyF0_2 f dss fr@(Min1Max0 ar f1 f0) = let new_f0 = map f f0 new_f1 = [] in Min1Max0 ar new_f1 new_f0 -- =================================================-- -- === Given embedding functor "e", function "f" ===-- -- === and closure functor "c", computes ===-- -- === "e.f.c" (ie "Ge.f2.Fc", in accordance ===-- -- === with Baraki's theory). ===-- -- =================================================-- -- ==========================================================-- -- bcEdotFdotC :: DRRSubst -> -- binds domain variables to Points DExpr -> -- target domain functor, "Ge" Domain -> -- domain of "f2" Rep -> -- the function "f2" [DExpr] -> -- source domain functors, "F[c1 ... cn]" Route bcEdotFdotC rho g_e fDomain@(Func fds fdt) f f_cs = let f_dot_c = bcFdotC rho f_cs newDs fDomain f newDs = map (bcEApp_d rho) f_cs fd_dot_c = Func newDs fdt e_dot_f_dot_c = bcEdotF rho g_e fd_dot_c f_dot_c in Rep e_dot_f_dot_c -- ==========================================================-- -- bcGetR (d, r, t) = r bcGetD (d, r, t) = d bcGetT (d, r, t) = t -- =========================================================-- -- === Do Baraki-style concretisation of function points ===-- -- =========================================================-- -- ==========================================================-- -- bcMakeInstance :: Bool -> -- True if use Baraki, False if use Conc Int -> -- How hard to work (for Baraki) ACMode -> -- Mode for Conc (IRRELEVANT) DExpr -> -- simplest instance domain of point (DXFunc _ _) DSubst -> -- binds domain vars to required instances Route -> -- simplest instance of function Route -- function at desired instance ------------------------------------------------------------------- -- Function-valued objects case. -- ------------------------------------------------------------------- -- Constraints, assumptions, &c. -- ------------------------------------------------------------------- -- 1. The function in question must be first-order. -- -- 2. The domain variables in the DExpr correspond exactly with -- -- those supplied in the DSubst. -- -- 3. The DExpr is of the form (DXFunc _ _) and correspondingly -- -- the supplied Point is of the form (DFunc _ _, RFunc _), -- -- and that the DFunc's args and DXFunc's args are -- -- appropriately related. -- ------------------------------------------------------------------- bcMakeInstance use_baraki threshold s_or_l simplest_dirty@(DXFunc args_f_functors_dirty result_g_functor_dirty) rho_d f@(Rep fRep) = let --------------------------- -- Clean up the functors -- --------------------------- simplest@(DXFunc args_f_functors result_g_functor) = bcClean simplest_dirty ----------------------------------------- -- The domain of the simplest instance -- ----------------------------------------- simplestD = dxApplyDSubst_2 simplest ----------------------------------------------- -- the domain variables in the instantiation -- ----------------------------------------------- domainVarNames = map first rho_d -------------------------------------------------- -- the domains corresponding to those variables -- -------------------------------------------------- bigInstanceDomains = map second rho_d ----------------------------------------------------- -- Find out if we actually need to do anything. -- -- baseInstance will also be True if this is -- -- f is non-polymorphic, since rho_d will be empty -- ----------------------------------------------------- baseInstance = myAll (==Two) bigInstanceDomains ------------------------------------------------------- -- find out if we can actually use Baraki's stuff. -- -- No function spaces in instantiations, and -- -- no non-top-level function spaces in the function. -- ------------------------------------------------------- barakiApplicable = myAll (not.amContainsFunctionSpace) bigInstanceDomains && (not.dxContainsFnSpace) result_g_functor && myAll (not.dxContainsSubsidiaryFnSpace) args_f_functors ----------------------------------------------------- -- Find out if we can use Baraki's first order -- -- optimisations. This requires first order -- -- instantiations of a first order function. -- -- The former condition is true anyway if we're -- -- using Baraki's method. -- ----------------------------------------------------- canUseOpt = all (not.dxContainsFnSpace) args_f_functors ----------------------------------------------------------- -- the set of points over which we have to take the meet -- ----------------------------------------------------------- bigInstancePoints = let individualIndices = if canUseOpt then map amMeetIRoutes bigInstanceDomains else map amAllRoutesMinusTopJONES bigInstanceDomains allIndices = myCartesianProduct individualIndices in take (max 1 threshold) allIndices -------------------------------------- -- The tops of the instance domains -- -------------------------------------- instanceTops = map avTopR bigInstanceDomains ------------------------------------------------------------- -- all the bindings of domain variables to relevant points -- ------------------------------------------------------------- allRhos = let makeOneRho rs = myZipWith4 (\n d r t -> (n, (d, r, t))) domainVarNames bigInstanceDomains rs instanceTops in map makeOneRho bigInstancePoints --------------------------------------------- -- all of the e.f.[c1 ... cn] compositions -- --------------------------------------------- all_edotfdotc = let makeOneEdotFdotC rho = bcEdotFdotC rho result_g_functor simplestD fRep args_f_functors in map makeOneEdotFdotC allRhos ---------------------------------------------------- -- the domain of the function after instantiation -- ---------------------------------------------------- big_function_domain = dxApplyDSubst rho_d simplest in if baseInstance then f else if not use_baraki || not barakiApplicable then acMakeInstance s_or_l simplest rho_d f else bmNorm big_function_domain (foldl1 bmGLB all_edotfdotc) ---------------------------------------- -- Non-function valued objects case. -- -- Just use Conc. In principle could -- -- use Baraki but I don't think this -- -- is really worth bothering with. -- ---------------------------------------- bcMakeInstance use_baraki threshold s_or_l simplest rho_d f = acMakeInstance s_or_l simplest rho_d f -- ==========================================================-- -- bcClean :: DExpr -> DExpr bcClean DXTwo = DXTwo bcClean (DXLift1 []) = DXTwo bcClean (DXLift2 []) = DXLift1 [DXTwo] bcClean (DXLift1 dxs) = DXLift1 (map bcClean dxs) bcClean (DXLift2 dxs) = DXLift2 (map bcClean dxs) bcClean (DXVar v) = DXVar v bcClean (DXFunc dxss dxt) = DXFunc (map bcClean dxss) (bcClean dxt) -- ==========================================================-- -- === end BarakiConc.hs ===-- -- ==========================================================--