1 2 -- ==========================================================-- 3 -- === Computes inverses of function applications. ===-- 4 -- === Inverse.hs ===-- 5 -- ==========================================================-- 6 7 module Inverse where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 import AbstractVals2 12 import SuccsAndPreds2 13 import AbstractMisc 14 import Apply 15 16 17 -- ==========================================================-- 18 -- 19 inMinInverse :: Bool -> Domain -> Route -> Route -> [FrontierElem] 20 21 inMinInverse mindless fDomain (Rep f) res 22 | mindless = second (inMMI_mindless fDomain f res) 23 | otherwise = second (inMMI fDomain f res) 24 25 26 -- ==========================================================-- 27 -- 28 inMaxInverse :: Bool -> Domain -> Route -> Route -> [FrontierElem] 29 30 inMaxInverse mindless fDomain (Rep f) res 31 | mindless = first (inMMI_mindless fDomain f res) 32 | otherwise = first (inMMI fDomain f res) 33 34 35 -- ==========================================================-- 36 -- 37 inMMI_mindless :: Domain -> Rep -> Route -> ([FrontierElem], [FrontierElem]) 38 39 inMMI_mindless (Func dss dt) f a 40 = let totalInverseImage = inInverse_mindless dss f a 41 in (avMaxfrel totalInverseImage, avMinfrel totalInverseImage) 42 43 44 -- ==========================================================-- 45 -- 46 inNormalise :: [FrontierElem] -> 47 [FrontierElem] -> 48 ([FrontierElem], [FrontierElem]) 49 50 inNormalise max min 51 = let new_max = filter (`avAboveMin1frel` min) max 52 new_min = filter (`avBelowMax0frel` new_max) min 53 in 54 (new_max, new_min) 55 56 57 -- ==========================================================-- 58 -- 59 inIntersect :: ([FrontierElem], [FrontierElem]) -> 60 ([FrontierElem], [FrontierElem]) -> 61 ([FrontierElem], [FrontierElem]) 62 63 inIntersect (max1, min1) (max2, min2) 64 = let new_max = avMaxfrel [ x `avGLBfrel` y | x <- max1, y <- max2 ] 65 new_min = avMinfrel [ x `avLUBfrel` y | x <- min1, y <- min2 ] 66 in inNormalise new_max new_min 67 68 69 -- ==========================================================-- 70 -- 71 inMMI :: Domain -> Rep -> Route -> ([FrontierElem], [FrontierElem]) 72 73 inMMI (Func dss dt) (RepTwo (Min1Max0 ar f1 f0)) Zero 74 = (f0, 75 if null f0 then [] else [MkFrel (map avBottomR dss)]) 76 77 inMMI (Func dss Two) (RepTwo (Min1Max0 ar f1 f0)) One 78 = (if null f1 then [] else [MkFrel (map avTopR dss)], 79 f1) 80 81 inMMI (Func dss (Lift1 dts)) (Rep1 (Min1Max0 ar lf_f1 lf_f0) hfs) Stop1 82 = (lf_f0, 83 if null lf_f0 then [] else [MkFrel (map avBottomR dss)]) 84 85 -- special case because this happens extremely frequently 86 inMMI (Func dss (Lift1 [dt])) (Rep1 (Min1Max0 ar lf_f1 lf_f0) [hf]) (Up1 [r]) 87 = let (hf_maxI, hf_minI) = inMMI (avUncurry dss dt) hf r 88 min2 = avMinfrel [ x `avLUBfrel` y | x <- hf_minI, y <- lf_f1 ] 89 in inNormalise hf_maxI min2 90 91 inMMI (Func dss (Lift1 dts)) (Rep1 (Min1Max0 ar lf_f1 lf_f0) hfs) (Up1 rs) 92 = let hf_domains = map (avUncurry dss) dts 93 hf_MMIs = myZipWith3 inMMI hf_domains hfs rs 94 (hf_maxI, hf_minI) = foldr1 inIntersect hf_MMIs 95 min2 = avMinfrel [ x `avLUBfrel` y | x <- hf_minI, y <- lf_f1 ] 96 in inNormalise hf_maxI min2 97 98 -- cheat on this one, because I'm lazy 99 inMMI (Func dss (Lift2 dts)) (Rep2 lf mf hfs) a 100 = let isoD = Func dss (Lift1 [Lift1 dts]) 101 isoR = Rep1 lf [Rep1 mf hfs] 102 isoA Stop2 = Stop1 103 isoA Up2 = Up1 [Stop1] 104 isoA (UpUp2 rs) = Up1 [Up1 rs] 105 in 106 inMMI isoD isoR (isoA a) 107 108 --inMMI (DFunc dss (Cross dts), RFunc (RepCross reps)) 109 -- (Cross dts2, Split rs) 110 -- | dts == dts2 {-INVARIANT-} 111 -- = let doOne n 112 -- = inMMI (avUncurryDomain (DFunc dss (dts##n)), 113 -- RFunc (reps##n)) (dts##n, rs##n) 114 -- in foldr1 inIntersect (map doOne [0 .. length reps - 1]) 115 -- 116 ---- special case for partial applications of [... -> 2] 117 --inMMI f@(DFunc dssf Two, RFunc (RepTwo (Min1Max0 arf f1 f0))) 118 -- g@(DFunc dssg Two, RFunc (RepTwo (Min1Max0 arg g1 g0))) 119 -- | arf > arg && {-INVARIANT-} 120 -- dssg == drop (length dssf - length dssg) dssf {-INVARIANT-} 121 -- = let (g1Max, g1Min) = inMMI g (Two, One) 122 -- (g0Max, g0Min) = inMMI g (Two, Zero) 123 -- fMaxs = [inPapL f fels | MkFrel fels <- g1Min] 124 -- fMins = [inPapL f fels | MkFrel fels <- g0Max] 125 -- iMaxs = [inMMI fn (Two, One) | fn <- fMaxs] 126 -- iMins = [inMMI fn (Two, Zero) | fn <- fMins] 127 -- in foldr1 inIntersect (iMaxs ++ iMins) 128 -- 129 --inMMI f@(DFunc dssf (Lift dtf), RFunc (RepLift lff hff)) 130 -- g@(DFunc dssg (Lift dtg), RFunc (RepLift lfg hfg)) 131 -- | dtf == dtg && {-INVARIANT-} 132 -- dssg == drop (length dssf - length dssg) dssf {-INVARIANT-} 133 -- = let lofac_f = (DFunc dssf Two, RFunc (RepTwo lff)) 134 -- lofac_g = (DFunc dssg Two, RFunc (RepTwo lfg)) 135 -- hifac_f = (avUncurryDomain (DFunc dssf dtf), RFunc hff) 136 -- hifac_g = (avUncurryDomain (DFunc dssg dtg), RFunc hfg) 137 -- in inIntersect (inMMI lofac_f lofac_g) (inMMI hifac_f hifac_g) 138 -- 139 --inMMI f@(DFunc dssf (Cross dtfs), RFunc (RepCross repsf)) 140 -- g@(DFunc dssg (Cross dtgs), RFunc (RepCross repsg)) 141 -- = let doOne n 142 -- = inMMI (avUncurryDomain (DFunc dssf (dtfs##n)), RFunc (repsf##n)) 143 -- (avUncurryDomain (DFunc dssg (dtgs##n)), RFunc (repsg##n)) 144 -- in foldr1 inIntersect (map doOne [0 :: Int .. length repsf - 1]) 145 146 -- otherwise, give up and call the mindless method 147 inMMI dss f a 148 = inMMI_mindless dss f a 149 150 151 -- ==========================================================-- 152 ---- 153 --inPapL :: Point -> [Point] -> Point 154 -- 155 --inPapL (DFunc dss Two, RFunc (RepTwo (Min1Max0 ar f1 f0))) args 156 -- = let argCount = length args 157 -- argDomainAfter = revDrop argCount dss 158 -- revDrop n = reverse . drop n . reverse 159 -- revTake n = reverse . take n . reverse 160 -- newf1 = sort (avMinfrel [MkFrel (revDrop argCount fel) | 161 -- MkFrel fel <- f1, 162 -- and (myZipWith2 avBelowEQ 163 -- (revTake argCount fel) args)]) 164 -- newf0 = sort (avMaxfrel [MkFrel (revDrop argCount fel) | 165 -- MkFrel fel <- f0, 166 -- and (myZipWith2 avBelowEQ 167 -- args (revTake argCount fel))]) 168 -- in (DFunc argDomainAfter Two, 169 -- RFunc (RepTwo (Min1Max0 (ar-argCount) newf1 newf0))) 170 -- 171 172 -- ==========================================================-- 173 -- 174 inInverse_mindless :: [Domain] -> Rep -> Route -> [FrontierElem] 175 176 inInverse_mindless argDomains f a 177 = let isPartialApp 178 = case a of { Rep _ -> True; _ -> False } 179 aRep 180 = case a of { Rep r -> r } 181 actualArgDomains 182 = if isPartialApp 183 then take (amRepArity f - amRepArity aRep) argDomains 184 else argDomains 185 allArgs 186 = myCartesianProduct (map amAllRoutes actualArgDomains) 187 in 188 [MkFrel args | args <- allArgs, apApply (Rep f) args == a] 189 190 --inTrace :: Bool -> Bool 191 --inTrace x = x 192 193 -- ==========================================================-- 194 -- === end Inverse.hs ===-- 195 -- ==========================================================-- 196