-- ==========================================================--
-- === Revised domain operations for HO analysis ===--
-- === AbstractVals2.hs ===--
-- ==========================================================--
module AbstractVals2 where
import BaseDefs
import Utils
import MyUtils
infix 9 << -- Below-or-equal for Routes
infix 9 /\ -- Binary GLB for routes
infix 9 \/ -- Binary LUB for routes
-- ==========================================================--
-- === ===--
-- === Top and bottom points of domains. ===--
-- === ===--
-- ==========================================================--
-- ==========================================================--
--
avUncurry :: [Domain] -> Domain -> Domain
avUncurry dss (Func dss2 dt) = Func (dss++dss2) dt
avUncurry dss non_func_dom = Func dss non_func_dom
-- ==========================================================--
--
avTopR :: Domain -> Route
avTopR Two = One
avTopR (Lift1 ds) = Up1 (map avTopR ds)
avTopR (Lift2 ds) = UpUp2 (map avTopR ds)
avTopR d@(Func dss dt) = Rep (avTopR_aux d)
-- ==========================================================--
--
avTopR_aux_2 :: [Domain] -> Frontier
avTopR_aux_2 dss
= Min1Max0 (length dss) [MkFrel (map avBottomR dss)] []
-- ==========================================================--
--
avTopR_aux :: Domain -> Rep
avTopR_aux (Func dss Two)
= RepTwo (avTopR_aux_2 dss)
avTopR_aux (Func dss (Lift1 dts))
= let lf = avTopR_aux_2 dss
hf_domains = map (avUncurry dss) dts
hfs = map avTopR_aux hf_domains
in
Rep1 lf hfs
avTopR_aux (Func dss (Lift2 dts))
= let lf = avTopR_aux_2 dss
hf_domains = map (avUncurry dss) dts
hfs = map avTopR_aux hf_domains
in
Rep2 lf lf hfs
-- ==========================================================--
--
avBottomR :: Domain -> Route
avBottomR Two = Zero
avBottomR (Lift1 ds) = Stop1
avBottomR (Lift2 ds) = Stop2
avBottomR d@(Func dss dt) = Rep (avBottomR_aux d)
-- ==========================================================--
--
avBottomR_aux_2 :: [Domain] -> Frontier
avBottomR_aux_2 dss
= Min1Max0 (length dss) [] [MkFrel (map avTopR dss)]
-- ==========================================================--
--
avBottomR_aux :: Domain -> Rep
avBottomR_aux (Func dss Two)
= RepTwo (avBottomR_aux_2 dss)
avBottomR_aux (Func dss (Lift1 dts))
= let lf = avBottomR_aux_2 dss
hf_domains = map (avUncurry dss) dts
hfs = map avBottomR_aux hf_domains
in
Rep1 lf hfs
avBottomR_aux (Func dss (Lift2 dts))
= let lf = avBottomR_aux_2 dss
hf_domains = map (avUncurry dss) dts
hfs = map avBottomR_aux hf_domains
in
Rep2 lf lf hfs
-- ==========================================================--
--
avIsBottomR :: Route -> Bool
avIsBottomR Zero = True
avIsBottomR Stop1 = True
avIsBottomR Stop2 = True
avIsBottomR One = False
avIsBottomR (Up1 _) = False
avIsBottomR Up2 = False
avIsBottomR (UpUp2 _) = False
avIsBottomR (Rep r) = avIsBottomRep r
-- ==========================================================--
--
avIsBottomRep :: Rep -> Bool
avIsBottomRep (RepTwo (Min1Max0 ar f1 f0))
= null f1
avIsBottomRep (Rep1 (Min1Max0 lf_ar lf_f1 lf_f0) hfs)
= null lf_f1
avIsBottomRep (Rep2 (Min1Max0 lf_ar lf_f1 lf_f0) mf hfs)
= null lf_f1
-- ==========================================================--
-- Is this correct? I think so.
--
avIsTopR :: Route -> Bool
avIsTopR Zero = False
avIsTopR One = True
avIsTopR Stop1 = False
avIsTopR (Up1 rs) = myAll avIsTopR rs
avIsTopR Stop2 = False
avIsTopR Up2 = False
avIsTopR (UpUp2 rs) = myAll avIsTopR rs
avIsTopR (Rep r) = avIsTopRep r
-- ==========================================================--
--
avIsTopRep :: Rep -> Bool
avIsTopRep (RepTwo (Min1Max0 ar f1 f0))
= null f0
avIsTopRep (Rep1 lf hfs)
= myAll avIsTopRep hfs
avIsTopRep (Rep2 lf mf hfs)
= myAll avIsTopRep hfs
-- ==========================================================--
-- === ===--
-- === Partial ordering predicates for points in domains. ===--
-- === ===--
-- ==========================================================--
-- ==========================================================--
--
(<<) :: Route -> Route -> Bool
Zero << _ = True
One << One = True
One << Zero = False
Stop1 << _ = True
Up1 rs1 << Up1 rs2 = avLEQR_list rs1 rs2
Up1 rs1 << _ = False
Stop2 << _ = True
Up2 << Stop2 = False
Up2 << _ = True
UpUp2 rs1 << UpUp2 rs2 = avLEQR_list rs1 rs2
UpUp2 rs1 << _ = False
Rep rep1 << Rep rep2 = avBelowEQrep rep1 rep2
-- ==========================================================--
-- A little bit of Cordy-style loop unrolling
-- although not actually tail-strict :-)
--
avLEQR_list :: [Route] -> [Route] -> Bool
avLEQR_list [] []
= True
avLEQR_list (a1:[]) (b1:[])
= a1 << b1
avLEQR_list (a1:a2:[]) (b1:b2:[])
= if a1 << b1
then a2 << b2
else False
avLEQR_list (a1:a2:a3:[]) (b1:b2:b3:[])
= if a1 << b1
then if a2 << b2
then a3 << b3
else False
else False
avLEQR_list (a1:a2:a3:a4:[]) (b1:b2:b3:b4:[])
= if a1 << b1
then if a2 << b2
then if a3 << b3
then a4 << b4
else False
else False
else False
-- OLD: avLEQR_list (a1:a2:a3:a4:as) (b1:b2:b3:b4:bs)
avLEQR_list (a1:a2:a3:a4:as@(_:_)) (b1:b2:b3:b4:bs@(_:_))
= if a1 << b1
then if a2 << b2
then if a3 << b3
then if a4 << b4
then avLEQR_list as bs
else False
else False
else False
else False
--avLEQR_list (a:as) (b:bs) = if a << b then avLEQR_list as bs else False
avLEQR_list _ _ = panic "avLEQR_list: unequal lists"
-- ==========================================================--
--
avBelowEQfrel :: FrontierElem -> FrontierElem -> Bool
avBelowEQfrel (MkFrel rs1) (MkFrel rs2)
= avLEQR_list rs1 rs2
-- ==========================================================--
--
avBelowEQfrontier :: Frontier -> Frontier -> Bool
avBelowEQfrontier (Min1Max0 ar1 f1a f0a) (Min1Max0 ar2 f1b f0b)
--
-- | ar1 == ar2 {-INVARIANT-}
--
-- = myAnd [myOr [q `avBelowEQfrel` p | q <- f1b] | p <- f1a]
--
-- Tail recursive special
--
= let outer [] = True
outer (x:xs) = if inner x f1b then outer xs else False
inner y [] = False
inner y (z:zs) = if z `avBelowEQfrel` y then True else inner y zs
in
outer f1a
-- ==========================================================--
--
avBelowEQrep :: Rep -> Rep -> Bool
avBelowEQrep (RepTwo fr1) (RepTwo fr2)
= avBelowEQfrontier fr1 fr2
avBelowEQrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2)
= avBelowEQfrontier lf1 lf2 &&
myAndWith2 avBelowEQrep hfs1 hfs2
avBelowEQrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2)
= avBelowEQfrontier lf1 lf2 &&
avBelowEQfrontier mf1 mf2 &&
myAndWith2 avBelowEQrep hfs1 hfs2
-- ==========================================================--
-- === ===--
-- === LUB and GLB operations for Points. ===--
-- === ===--
-- ==========================================================--
-- ==========================================================--
--
(\/) :: Route -> Route -> Route
p@ Zero \/ q = q
p@ One \/ q = p
p@ Stop1 \/ q = q
p@(Up1 rs1) \/ Stop1 = p
p@(Up1 rs1) \/ Up1 rs2 = Up1 (myZipWith2 (\/) rs1 rs2)
p@ Stop2 \/ q = q
p@ Up2 \/ Stop2 = p
p@ Up2 \/ q = q
p@(UpUp2 rs1) \/ UpUp2 rs2 = UpUp2 (myZipWith2 (\/) rs1 rs2)
p@(UpUp2 rs1) \/ q = p
p@(Rep rep1) \/ q@(Rep rep2) = Rep (avLUBrep rep1 rep2)
-- ==========================================================--
--
avLUBfrel :: FrontierElem -> FrontierElem -> FrontierElem
avLUBfrel (MkFrel rs1) (MkFrel rs2)
= MkFrel (myZipWith2 (\/) rs1 rs2)
-- ==========================================================--
--
avLUBfrontier :: Frontier -> Frontier -> Frontier
avLUBfrontier (Min1Max0 ar1 f1a f0a) (Min1Max0 ar2 f1b f0b)
-- | ar1 == ar2 {-INVARIANT-}
= Min1Max0 ar1 (avLUBmin1frontier f1a f1b) (avLUBmax0frontier f0a f0b)
-- ==========================================================--
--
avLUBrep :: Rep -> Rep -> Rep
avLUBrep (RepTwo fr1) (RepTwo fr2)
= RepTwo (avLUBfrontier fr1 fr2)
avLUBrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2)
= Rep1 (avLUBfrontier lf1 lf2) (myZipWith2 avLUBrep hfs1 hfs2)
avLUBrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2)
= Rep2 (avLUBfrontier lf1 lf2) (avLUBfrontier mf1 mf2)
(myZipWith2 avLUBrep hfs1 hfs2)
-- ==========================================================--
--
avLUBmin1frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem]
avLUBmin1frontier f1a f1b
= sort (foldr avMinAddPtfrel f1a f1b) {-OPTIMISE-}
-- ==========================================================--
--
avLUBmax0frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem]
avLUBmax0frontier f0a f0b
= sort (avMaxfrel [ x `avGLBfrel` y | x <- f0a, y <- f0b ])
-- ==========================================================--
--
(/\) :: Route -> Route -> Route
p@ Zero /\ q = p
p@ One /\ q = q
p@ Stop1 /\ q = p
p@(Up1 rs1) /\ (Up1 rs2) = Up1 (myZipWith2 (/\) rs1 rs2)
p@(Up1 rs1) /\ q = q
p@ Stop2 /\ q = p
p@ Up2 /\ q@ Stop2 = q
p@ Up2 /\ q = p
p@(UpUp2 rs1) /\ q@(UpUp2 rs2) = UpUp2 (myZipWith2 (/\) rs1 rs2)
p@(UpUp2 rs1) /\ q = q
p@(Rep rep1) /\ q@(Rep rep2) = Rep (avGLBrep rep1 rep2)
-- ==========================================================--
--
avGLBfrel :: FrontierElem -> FrontierElem -> FrontierElem
avGLBfrel (MkFrel rs1) (MkFrel rs2)
= MkFrel (myZipWith2 (/\) rs1 rs2)
-- ==========================================================--
--
avGLBfrontier :: Frontier -> Frontier -> Frontier
avGLBfrontier (Min1Max0 ar1 f1a f0a) (Min1Max0 ar2 f1b f0b)
-- | ar1 == ar2 {-INVARIANT-}
= Min1Max0 ar1 (avGLBmin1frontier f1a f1b) (avGLBmax0frontier f0a f0b)
-- ==========================================================--
--
avGLBrep :: Rep -> Rep -> Rep
avGLBrep (RepTwo fr1) (RepTwo fr2)
= RepTwo (avGLBfrontier fr1 fr2)
avGLBrep (Rep1 lf1 hfs1) (Rep1 lf2 hfs2)
= Rep1 (avGLBfrontier lf1 lf2) (myZipWith2 avGLBrep hfs1 hfs2)
avGLBrep (Rep2 lf1 mf1 hfs1) (Rep2 lf2 mf2 hfs2)
= Rep2 (avGLBfrontier lf1 lf2) (avGLBfrontier mf1 mf2)
(myZipWith2 avGLBrep hfs1 hfs2)
-- ==========================================================--
--
avGLBmax0frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem]
avGLBmax0frontier f0a f0b
= sort (foldr avMaxAddPtfrel f0a f0b) {-OPTIMISE-}
-- ==========================================================--
--
avGLBmin1frontier :: [FrontierElem] -> [FrontierElem] -> [FrontierElem]
avGLBmin1frontier f1a f1b
= sort (avMinfrel [ x `avLUBfrel` y | x <- f1a, y <- f1b ])
-- ==========================================================--
-- === ===--
-- === Min and Max operations for frontiers. ===--
-- === Note avBelowMax0/avAboveMin1 expect Frel's to be ===--
-- === of the same length. ===--
-- === ===--
-- ==========================================================--
pt `avBelowMax0frel` f = myAny (pt `avBelowEQfrel`) f
pt `avAboveMin1frel` f = myAny (`avBelowEQfrel` pt) f
avMinAddPtfrel x ys
| x `avAboveMin1frel` ys = ys
| otherwise = x:[y | y <- ys, not (x `avBelowEQfrel` y)]
avMaxAddPtfrel x ys
| x `avBelowMax0frel` ys = ys
| otherwise = x:[y | y <- ys, not (y `avBelowEQfrel` x)]
avMinfrel = foldr avMinAddPtfrel []
avMaxfrel = foldr avMaxAddPtfrel []
-- ==========================================================--
-- === ===--
-- === Min and Max operations for Routes ===--
-- === ===--
-- ==========================================================--
pt `avBelowMax0R` f = myAny (pt <<) f
pt `avAboveMin1R` f = myAny (<< pt) f
avMinAddPtR x ys
| x `avAboveMin1R` ys = ys
| otherwise = x:[y | y <- ys, not (x << y)]
avMaxAddPtR x ys
| x `avBelowMax0R` ys = ys
| otherwise = x:[y | y <- ys, not (y << x)]
avMinR = foldr avMinAddPtR []
avMaxR = foldr avMaxAddPtR []
-- ==========================================================--
-- === ===--
-- === Min and Max operations for Reps ===--
-- === ===--
-- ==========================================================--
pt `avBelowMax0rep` f = myAny (pt `avBelowEQrep`) f
pt `avAboveMin1rep` f = myAny (`avBelowEQrep` pt) f
avMinAddPtrep x ys
| x `avAboveMin1rep` ys = ys
| otherwise = x:[y | y <- ys, not (x `avBelowEQrep` y)]
avMaxAddPtrep x ys
| x `avBelowMax0rep` ys = ys
| otherwise = x:[y | y <- ys, not (y `avBelowEQrep` x)]
avMinrep = foldr avMinAddPtrep []
avMaxrep = foldr avMaxAddPtrep []
-- ==========================================================--
-- === end AbstractVals2.hs ===--
-- ==========================================================--
|
