module Cryptol.TypeCheck.Solver.Interval
( Interval(..)
, anything
, iConst
, iAdd, iMul, iExp
, iMin, iMax
, iLg2, iWidth
, iSub, iDiv, iMod
, iLenFromThen, iLenFromTo, iLenFromThenTo
, iLeq, iLt, iDisjoint
) where
import Cryptol.TypeCheck.Solver.InfNat
data Interval = Interval
{ lowerBound :: Nat'
, upperBound :: Nat'
, isFinite :: Bool
} deriving Show
anything :: Interval
anything = Interval { lowerBound = Nat 0
, upperBound = Inf
, isFinite = False
}
anyFinite :: Interval
anyFinite = anything { isFinite = True }
iConst :: Nat' -> Interval
iConst x = Interval { lowerBound = x, upperBound = x, isFinite = x < Inf }
iAdd :: Interval -> Interval -> Interval
iAdd = liftMono2 nAdd (&&)
iMul :: Interval -> Interval -> Interval
iMul = liftMono2 nMul (&&)
iMin :: Interval -> Interval -> Interval
iMin = liftMono2 nMin (||)
iMax :: Interval -> Interval -> Interval
iMax = liftMono2 nMax (&&)
iLg2 :: Interval -> Interval
iLg2 = liftMono1 nLg2
iWidth :: Interval -> Interval
iWidth = liftMono1 nWidth
iExp :: Interval -> Interval -> Interval
iExp i1 i2 = fixUp (liftMono2 nExp (&&) i1 i2)
where
fixUp i3
| lowerBound i1 == Nat 0 &&
lowerBound i2 == Nat 0 &&
upperBound i2 >= Nat 1 =
Interval { lowerBound = Nat 0
, upperBound = nMax (Nat 1) (upperBound i3)
, isFinite = isFinite i3
}
fixUp i3 = i3
iSub :: Interval -> Interval -> Interval
iSub = liftPosNeg nSub
iDiv :: Interval -> Interval -> Interval
iDiv = liftPosNeg nDiv
iMod :: Interval -> Interval -> Interval
iMod _ i2 = Interval { lowerBound = Nat 0
, upperBound = case upperBound i2 of
Inf -> Inf
Nat n -> Nat (n 1)
, isFinite = True
}
iLenFromThen :: Interval -> Interval -> Interval -> Interval
iLenFromThen _ _ _ = anyFinite
iLenFromTo :: Interval -> Interval -> Interval
iLenFromTo _ _ = anyFinite
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
iLenFromThenTo _ _ _ = anyFinite
iLeq :: Interval -> Interval -> Bool
iLeq i1 i2 = upperBound i1 <= lowerBound i2
iLt :: Interval -> Interval -> Bool
iLt i1 i2 = upperBound i1 < lowerBound i2
|| (isFinite i1 && lowerBound i2 == Inf)
iDisjoint :: Interval -> Interval -> Bool
iDisjoint i1 i2 = iLt i1 i2 || iLt i2 i1
liftMono1 :: (Nat' -> Nat')
-> Interval -> Interval
liftMono1 f i =
let u = f (upperBound i)
in Interval { lowerBound = f (lowerBound i)
, upperBound = u
, isFinite = mkFin (isFinite i) u
}
liftMono2 :: (Nat' -> Nat' -> Nat')
-> (Bool -> Bool -> Bool)
-> Interval -> Interval -> Interval
liftMono2 f isF i1 i2 =
let u = f (upperBound i1) (upperBound i2)
in Interval { lowerBound = f (lowerBound i1) (lowerBound i2)
, upperBound = u
, isFinite = mkFin (isF (isFinite i1) (isFinite i2)) u
}
liftPosNeg :: (Nat' -> Nat' -> Maybe Nat')
-> Interval -> Interval -> Interval
liftPosNeg f i1 i2 =
Interval { lowerBound = case f (lowerBound i1) (upperBound i2) of
Nothing -> Nat 0
Just n -> n
, upperBound = case f (upperBound i1) (lowerBound i2) of
Just n -> n
Nothing -> upperBound i1
, isFinite = isFinite i1
}
mkFin :: Bool -> Nat' -> Bool
mkFin ifInf ub = case ub of
Nat _ -> True
Inf -> ifInf