{-| Module : MinMaxAffine Description : Lattice completion of our Affine type Copyright : (c) David Janin, 2016 License : see the LICENSE file in the distribution Maintainer : janin@labri.fr Stability : experimental Lattice complemention of the affine type with explicit min and max when non reducible. -} {-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-} {-# LANGUAGE TypeSynonymInstances , MultiParamTypeClasses , FlexibleInstances #-} module Duration.MinMaxAffine where import Duration.Affine import Duration.Lattice import Duration.MinMax --------------------------------------------------------------- -- * --------------------------------------------------------------- -- | Duration over a numeric type d and unknown indices i type MinMaxAffine d i = MinMax (Affine d i) --------------------------------------------------------------- -- * Primitive setters --------------------------------------------------------------- -- | Creates a duration from variable index i varDur :: (Num d) => i -> MinMaxAffine d i varDur i = Min [Max [affineFromID i]] -- | Creates a duration from a duration constant d constDur :: d -> MinMaxAffine d i constDur d = Min [Max [affineFromConst d]] --------------------------------------------------------------- -- * Partial order --------------------------------------------------------------- -- | Compares two durations compareMinMaxAffine :: (Ord d, Num d, Ord i) => MinMaxAffine d i -> MinMaxAffine d i -> Maybe Ordering compareMinMaxAffine = partialCompare -- | Takes the min of two durations meetD :: (Num d, Ord d, Ord i) => [MinMaxAffine d i] -> MinMaxAffine d i meetD = meet -- | Takes the max of two durations joinD :: (Num d, Ord d, Ord i) => [MinMaxAffine d i] -> MinMaxAffine d i joinD = join --------------------------------------------------------------- -- * Checks constant value and extracts if possible. --------------------------------------------------------------- -- | Checks if the arguement is actually a defined constant of type d, and send it back if true. getConstDurMaybe :: (Num d, Ord d, Ord i) => MinMaxAffine d i -> Maybe d getConstDurMaybe x = getMaybeMin getNextKnownDelay x {- getConstDurMaybe (Min []) = Nothing getConstDurMaybe d = case d1 of Min [Max [Affine c []]] -> Just c _ -> Nothing where d1 = getConstDurMinMax d getConstDurMinMax :: (Num d, Ord d, Ord i) => MinMax (Affine d i) -> MinMax (Affine d i) getConstDurMinMax (Min ml) = reduceMin (Min [Max [d] | Max [d] <- (fmap getConstDurMax ml)]) getConstDurMax:: (Num d, Ord d, Ord i) => Max (Affine d i) -> Max (Affine d i) getConstDurMax (Max ml) = reduceMax (Max [(Affine d []) | (Affine d _) <- ml]) -} getMaybeMin :: Ord e => (d -> Maybe e) -> MinMax d -> Maybe e getMaybeMin f (Min l) = let ld = [d | Just d <- map (getMaybeMax f) l] in case ld of [] -> Nothing _ -> Just $ minimum ld getMaybeMax :: Ord e => (d -> Maybe e) -> Max d -> Maybe e getMaybeMax f (Max l) = let ld = [d | Just d <- map f l] in case ld of [] -> Nothing _ -> Just $ maximum ld {- (Min (x:xs)) = let ms = getConstDurMaybe (Min xs) m = getConstDurMaybeMax x getConstDurMaybeMax (Max []) = Nothing getConstDurMaybeMax (Max (Affine d []:xs)) = let max = getConstDurMaybeMax (Max xs) in case max of Just d1 -> Just $ maximum [d,d1] Nothing -> Just d getConstDurMaybeMax (Max (Affine d _:xs)) = getConstDurMaybeMax (Max xs) in case (m,ms) of (Nothing, Just d) -> Just d (Just d, Nothing) -> Just d (Just d1, Just d2) -> Just $ minimum [d1,d2] _ -> Nothing -} --------------------------------------------------------------- -- * Related boolean queries --------------------------------------------------------------- -- | True when provably positive or null isPosDur :: (Num d, Ord d, Ord i) => MinMaxAffine d i -> Bool isPosDur d = case compareMinMaxAffine 0 d of Just LT -> True Just EQ -> True _ -> False -- | True when provably negative or null isNegDur :: (Num d, Ord d, Ord i) => MinMaxAffine d i -> Bool isNegDur d = case compareMinMaxAffine d 0 of Just LT -> True Just EQ -> True _ -> False -- | True when provably zero isZeroDur :: (Eq d, Num d, Ord d, Ord i) => MinMaxAffine d i -> Bool isZeroDur d = d == 0 --------------------------------------------------------------- -- * Update queries --------------------------------------------------------------- -- | Replaces every unknown X by X + d updateMinMaxOnDelay :: (Num d, Ord d, Ord i) => d -> MinMax (Affine d i) -> MinMax (Affine d i) updateMinMaxOnDelay d = fmap1MinMax (shiftAffine d) -- | Replaces every unknown Xi by 0 for specified indices. updateMinMaxOnVariable :: (Num d, Ord i, Ord d) => [i] -> MinMax (Affine d i) -> MinMax (Affine d i) updateMinMaxOnVariable li = fmap1MinMax (setToZeroAffine li) -- * Basic functions for tests -- | An inspiring examples. Observe that 0 == d - d will fail unless -- some more (LP based) advanced polytopes comparison are put in practice. -- -- @ -- d = meetM [varDur 1, varDur 2] -- @ d :: MinMax (Affine Integer Integer) d = meetM [varDur 1, varDur 2] evalMinMaxAffine :: (Ord d, Num d, Ord i) => d -> MinMax (Affine d i) -> MinMax (Affine d i) evalMinMaxAffine d (Min l) = reduceMin $ Min (map (evalMaxAffine d) l) evalMaxAffine :: (Ord d, Num d, Ord i) => d -> Max (Affine d i) -> Max (Affine d i) evalMaxAffine d (Max l) = reduceMax $ Max (map (evalAffine d) l)