{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE BangPatterns #-}
module Cryptol.TypeCheck.Solver.Numeric.Interval where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.PP hiding (int)
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Maybe (catMaybes)
typeInterval :: Map TVar Interval -> Type -> Interval
typeInterval :: Map TVar Interval -> Type -> Interval
typeInterval varInfo :: Map TVar Interval
varInfo = Type -> Interval
go
where
go :: Type -> Interval
go ty :: Type
ty =
case Type
ty of
TUser _ _ t :: Type
t -> Type -> Interval
go Type
t
TCon tc :: TCon
tc ts :: [Type]
ts ->
case (TCon
tc, [Type]
ts) of
(TC TCInf, []) -> Nat' -> Interval
iConst Nat'
Inf
(TC (TCNum n :: Integer
n), []) -> Nat' -> Interval
iConst (Integer -> Nat'
Nat Integer
n)
(TF TCAdd, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iAdd (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCSub, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iSub (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCMul, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iMul (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCDiv, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iDiv (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCMod, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iMod (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCExp, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iExp (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCWidth, [x :: Type
x]) -> Interval -> Interval
iWidth (Type -> Interval
go Type
x)
(TF TCMin, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iMin (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCMax, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iMax (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCCeilDiv, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iCeilDiv (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCCeilMod, [x :: Type
x,y :: Type
y]) -> Interval -> Interval -> Interval
iCeilMod (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
(TF TCLenFromThenTo, [x :: Type
x,y :: Type
y,z :: Type
z]) ->
Interval -> Interval -> Interval -> Interval
iLenFromThenTo (Type -> Interval
go Type
x) (Type -> Interval
go Type
y) (Type -> Interval
go Type
z)
_ -> Interval
iAny
TVar x :: TVar
x -> Map TVar Interval -> TVar -> Interval
tvarInterval Map TVar Interval
varInfo TVar
x
_ -> Interval
iAny
tvarInterval :: Map TVar Interval -> TVar -> Interval
tvarInterval :: Map TVar Interval -> TVar -> Interval
tvarInterval varInfo :: Map TVar Interval
varInfo x :: TVar
x = Interval -> TVar -> Map TVar Interval -> Interval
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Interval
iAny TVar
x Map TVar Interval
varInfo
data IntervalUpdate = NoChange
| InvalidInterval TVar
| NewIntervals (Map TVar Interval)
deriving (Int -> IntervalUpdate -> ShowS
[IntervalUpdate] -> ShowS
IntervalUpdate -> String
(Int -> IntervalUpdate -> ShowS)
-> (IntervalUpdate -> String)
-> ([IntervalUpdate] -> ShowS)
-> Show IntervalUpdate
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IntervalUpdate] -> ShowS
$cshowList :: [IntervalUpdate] -> ShowS
show :: IntervalUpdate -> String
$cshow :: IntervalUpdate -> String
showsPrec :: Int -> IntervalUpdate -> ShowS
$cshowsPrec :: Int -> IntervalUpdate -> ShowS
Show)
updateInterval :: (TVar,Interval) -> Map TVar Interval -> IntervalUpdate
updateInterval :: (TVar, Interval) -> Map TVar Interval -> IntervalUpdate
updateInterval (x :: TVar
x,int :: Interval
int) varInts :: Map TVar Interval
varInts =
case TVar -> Map TVar Interval -> Maybe Interval
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
x Map TVar Interval
varInts of
Just int' :: Interval
int' ->
case Interval -> Interval -> Maybe Interval
iIntersect Interval
int Interval
int' of
Just val :: Interval
val | Interval
int' Interval -> Interval -> Bool
forall a. Eq a => a -> a -> Bool
/= Interval
val -> Map TVar Interval -> IntervalUpdate
NewIntervals (TVar -> Interval -> Map TVar Interval -> Map TVar Interval
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
x Interval
val Map TVar Interval
varInts)
| Bool
otherwise -> IntervalUpdate
NoChange
Nothing -> TVar -> IntervalUpdate
InvalidInterval TVar
x
Nothing -> Map TVar Interval -> IntervalUpdate
NewIntervals (TVar -> Interval -> Map TVar Interval -> Map TVar Interval
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
x Interval
int Map TVar Interval
varInts)
computePropIntervals :: Map TVar Interval -> [Prop] -> IntervalUpdate
computePropIntervals :: Map TVar Interval -> [Type] -> IntervalUpdate
computePropIntervals ints :: Map TVar Interval
ints ps0 :: [Type]
ps0 = Int -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
forall t.
(Ord t, Num t) =>
t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go (3 :: Int) Bool
False Map TVar Interval
ints [Type]
ps0
where
go :: t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go !t
_n False _ [] = IntervalUpdate
NoChange
go !t
n True is :: Map TVar Interval
is []
| t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = Map TVar Interval -> IntervalUpdate -> IntervalUpdate
changed Map TVar Interval
is (t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go (t
nt -> t -> t
forall a. Num a => a -> a -> a
-1) Bool
False Map TVar Interval
is [Type]
ps0)
| Bool
otherwise = Map TVar Interval -> IntervalUpdate
NewIntervals Map TVar Interval
is
go !t
n new :: Bool
new is :: Map TVar Interval
is (p :: Type
p:ps :: [Type]
ps) =
case Bool -> [(TVar, Interval)] -> Map TVar Interval -> IntervalUpdate
add Bool
False (Map TVar Interval -> Type -> [(TVar, Interval)]
propInterval Map TVar Interval
is Type
p) Map TVar Interval
is of
InvalidInterval i :: TVar
i -> TVar -> IntervalUpdate
InvalidInterval TVar
i
NewIntervals is' :: Map TVar Interval
is' -> t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go t
n Bool
True Map TVar Interval
is' [Type]
ps
NoChange -> t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go t
n Bool
new Map TVar Interval
is [Type]
ps
add :: Bool -> [(TVar, Interval)] -> Map TVar Interval -> IntervalUpdate
add ch :: Bool
ch [] int :: Map TVar Interval
int = if Bool
ch then Map TVar Interval -> IntervalUpdate
NewIntervals Map TVar Interval
int else IntervalUpdate
NoChange
add ch :: Bool
ch (i :: (TVar, Interval)
i:is :: [(TVar, Interval)]
is) int :: Map TVar Interval
int = case (TVar, Interval) -> Map TVar Interval -> IntervalUpdate
updateInterval (TVar, Interval)
i Map TVar Interval
int of
InvalidInterval j :: TVar
j -> TVar -> IntervalUpdate
InvalidInterval TVar
j
NoChange -> Bool -> [(TVar, Interval)] -> Map TVar Interval -> IntervalUpdate
add Bool
ch [(TVar, Interval)]
is Map TVar Interval
int
NewIntervals is' :: Map TVar Interval
is' -> Bool -> [(TVar, Interval)] -> Map TVar Interval -> IntervalUpdate
add Bool
True [(TVar, Interval)]
is Map TVar Interval
is'
changed :: Map TVar Interval -> IntervalUpdate -> IntervalUpdate
changed a :: Map TVar Interval
a x :: IntervalUpdate
x = case IntervalUpdate
x of
NoChange -> Map TVar Interval -> IntervalUpdate
NewIntervals Map TVar Interval
a
r :: IntervalUpdate
r -> IntervalUpdate
r
propInterval :: Map TVar Interval -> Prop -> [(TVar,Interval)]
propInterval :: Map TVar Interval -> Type -> [(TVar, Interval)]
propInterval varInts :: Map TVar Interval
varInts prop :: Type
prop = [Maybe (TVar, Interval)] -> [(TVar, Interval)]
forall a. [Maybe a] -> [a]
catMaybes
[ do Type
ty <- Type -> Maybe Type
pIsFin Type
prop
TVar
x <- Type -> Maybe TVar
tIsVar Type
ty
(TVar, Interval) -> Maybe (TVar, Interval)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x,Interval
iAnyFin)
, do (l :: Type
l,r :: Type
r) <- Type -> Maybe (Type, Type)
pIsEq Type
prop
TVar
x <- Type -> Maybe TVar
tIsVar Type
l
(TVar, Interval) -> Maybe (TVar, Interval)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x,Map TVar Interval -> Type -> Interval
typeInterval Map TVar Interval
varInts Type
r)
, do (l :: Type
l,r :: Type
r) <- Type -> Maybe (Type, Type)
pIsEq Type
prop
TVar
x <- Type -> Maybe TVar
tIsVar Type
r
(TVar, Interval) -> Maybe (TVar, Interval)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x,Map TVar Interval -> Type -> Interval
typeInterval Map TVar Interval
varInts Type
l)
, do (l :: Type
l,r :: Type
r) <- Type -> Maybe (Type, Type)
pIsGeq Type
prop
TVar
x <- Type -> Maybe TVar
tIsVar Type
l
let int :: Interval
int = Map TVar Interval -> Type -> Interval
typeInterval Map TVar Interval
varInts Type
r
(TVar, Interval) -> Maybe (TVar, Interval)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x,Interval
int { iUpper :: Maybe Nat'
iUpper = Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf })
, do (l :: Type
l,r :: Type
r) <- Type -> Maybe (Type, Type)
pIsGeq Type
prop
TVar
x <- Type -> Maybe TVar
tIsVar Type
r
let int :: Interval
int = Map TVar Interval -> Type -> Interval
typeInterval Map TVar Interval
varInts Type
l
(TVar, Interval) -> Maybe (TVar, Interval)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x,Interval
int { iLower :: Nat'
iLower = Integer -> Nat'
Nat 0 })
, do (l :: Type
l,r :: Type
r) <- Type -> Maybe (Type, Type)
pIsGeq Type
prop
TVar
x <- Type -> Maybe TVar
tIsVar (Type -> Maybe TVar) -> Maybe Type -> Maybe TVar
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Maybe Type
pIsWidth Type
r
let ub :: Maybe Nat'
ub = case Interval -> Maybe Nat'
iIsExact (Map TVar Interval -> Type -> Interval
typeInterval Map TVar Interval
varInts Type
l) of
Just (Nat val :: Integer
val) | Integer
val Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 128 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat (2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1))
| Bool
otherwise -> Maybe Nat'
forall a. Maybe a
Nothing
upper :: Maybe Nat'
upper -> Maybe Nat'
upper
(TVar, Interval) -> Maybe (TVar, Interval)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x, Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Integer -> Nat'
Nat 0, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
ub })
]
data Interval = Interval
{ Interval -> Nat'
iLower :: Nat'
, Interval -> Maybe Nat'
iUpper :: Maybe Nat'
} deriving (Interval -> Interval -> Bool
(Interval -> Interval -> Bool)
-> (Interval -> Interval -> Bool) -> Eq Interval
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Interval -> Interval -> Bool
$c/= :: Interval -> Interval -> Bool
== :: Interval -> Interval -> Bool
$c== :: Interval -> Interval -> Bool
Eq,Int -> Interval -> ShowS
[Interval] -> ShowS
Interval -> String
(Int -> Interval -> ShowS)
-> (Interval -> String) -> ([Interval] -> ShowS) -> Show Interval
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Interval] -> ShowS
$cshowList :: [Interval] -> ShowS
show :: Interval -> String
$cshow :: Interval -> String
showsPrec :: Int -> Interval -> ShowS
$cshowsPrec :: Int -> Interval -> ShowS
Show)
ppIntervals :: Map TVar Interval -> Doc
ppIntervals :: Map TVar Interval -> Doc
ppIntervals = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (Map TVar Interval -> [Doc]) -> Map TVar Interval -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TVar, Interval) -> Doc) -> [(TVar, Interval)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Interval) -> Doc
forall a. PP a => (a, Interval) -> Doc
ppr ([(TVar, Interval)] -> [Doc])
-> (Map TVar Interval -> [(TVar, Interval)])
-> Map TVar Interval
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TVar Interval -> [(TVar, Interval)]
forall k a. Map k a -> [(k, a)]
Map.toList
where
ppr :: (a, Interval) -> Doc
ppr (var :: a
var,i :: Interval
i) = a -> Doc
forall a. PP a => a -> Doc
pp a
var Doc -> Doc -> Doc
<.> Char -> Doc
char ':' Doc -> Doc -> Doc
<+> Interval -> Doc
ppInterval Interval
i
ppInterval :: Interval -> Doc
ppInterval :: Interval -> Doc
ppInterval x :: Interval
x = Doc -> Doc
brackets ([Doc] -> Doc
hsep [ Nat' -> Doc
ppr (Interval -> Nat'
iLower Interval
x)
, String -> Doc
text ".."
, Doc -> (Nat' -> Doc) -> Maybe Nat' -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Doc
text "fin") Nat' -> Doc
ppr (Interval -> Maybe Nat'
iUpper Interval
x)])
where
ppr :: Nat' -> Doc
ppr a :: Nat'
a = case Nat'
a of
Nat n :: Integer
n -> Integer -> Doc
integer Integer
n
Inf -> String -> Doc
text "inf"
iIsExact :: Interval -> Maybe Nat'
iIsExact :: Interval -> Maybe Nat'
iIsExact i :: Interval
i = if Interval -> Maybe Nat'
iUpper Interval
i Maybe Nat' -> Maybe Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Interval -> Nat'
iLower Interval
i) then Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Interval -> Nat'
iLower Interval
i) else Maybe Nat'
forall a. Maybe a
Nothing
iIsFin :: Interval -> Bool
iIsFin :: Interval -> Bool
iIsFin i :: Interval
i = case Interval -> Maybe Nat'
iUpper Interval
i of
Just Inf -> Bool
False
_ -> Bool
True
iIsPosFin :: Interval -> Bool
iIsPosFin :: Interval -> Bool
iIsPosFin i :: Interval
i = Interval -> Nat'
iLower Interval
i Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 1 Bool -> Bool -> Bool
&& Interval -> Bool
iIsFin Interval
i
iOverlap :: Interval -> Interval -> Bool
iOverlap :: Interval -> Interval -> Bool
iOverlap
(Interval (Nat l1 :: Integer
l1) (Just (Nat h1 :: Integer
h1)))
(Interval (Nat l2 :: Integer
l2) (Just (Nat h2 :: Integer
h2))) =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Integer
h1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
l2 Bool -> Bool -> Bool
&& Integer
h1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
h2, Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
l2 Bool -> Bool -> Bool
&& Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
h2 ]
iOverlap _ _ = Bool
False
iIntersect :: Interval -> Interval -> Maybe Interval
iIntersect :: Interval -> Interval -> Maybe Interval
iIntersect i :: Interval
i j :: Interval
j =
case (Nat'
lower,Maybe Nat'
upper) of
(Nat l :: Integer
l, Just (Nat u :: Integer
u)) | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
u -> Maybe Interval
ok
(Nat _, Just Inf) -> Maybe Interval
ok
(Nat _, Nothing) -> Maybe Interval
ok
(Inf, Just Inf) -> Maybe Interval
ok
_ -> Maybe Interval
forall a. Maybe a
Nothing
where
ok :: Maybe Interval
ok = Interval -> Maybe Interval
forall a. a -> Maybe a
Just (Nat' -> Maybe Nat' -> Interval
Interval Nat'
lower Maybe Nat'
upper)
lower :: Nat'
lower = Nat' -> Nat' -> Nat'
nMax (Interval -> Nat'
iLower Interval
i) (Interval -> Nat'
iLower Interval
j)
upper :: Maybe Nat'
upper = case (Interval -> Maybe Nat'
iUpper Interval
i, Interval -> Maybe Nat'
iUpper Interval
j) of
(Just a :: Nat'
a, Just b :: Nat'
b) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMin Nat'
a Nat'
b)
(Nothing,Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just l :: Nat'
l,Nothing) | Nat'
l Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
/= Nat'
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
l
(Nothing,Just r :: Nat'
r) | Nat'
r Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
/= Nat'
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
r
_ -> Maybe Nat'
forall a. Maybe a
Nothing
iAny :: Interval
iAny :: Interval
iAny = Nat' -> Maybe Nat' -> Interval
Interval (Integer -> Nat'
Nat 0) (Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf)
iAnyFin :: Interval
iAnyFin :: Interval
iAnyFin = Nat' -> Maybe Nat' -> Interval
Interval (Integer -> Nat'
Nat 0) Maybe Nat'
forall a. Maybe a
Nothing
iConst :: Nat' -> Interval
iConst :: Nat' -> Interval
iConst x :: Nat'
x = Nat' -> Maybe Nat' -> Interval
Interval Nat'
x (Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
x)
iAdd :: Interval -> Interval -> Interval
iAdd :: Interval -> Interval -> Interval
iAdd i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat' -> Nat' -> Nat'
nAdd (Interval -> Nat'
iLower Interval
i) (Interval -> Nat'
iLower Interval
j)
, iUpper :: Maybe Nat'
iUpper = case (Interval -> Maybe Nat'
iUpper Interval
i, Interval -> Maybe Nat'
iUpper Interval
j) of
(Nothing, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just x :: Nat'
x, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nAdd Nat'
x Nat'
y)
(Nothing, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
upper Nat'
y
(Just x :: Nat'
x, Nothing) -> Nat' -> Maybe Nat'
upper Nat'
x
}
where
upper :: Nat' -> Maybe Nat'
upper x :: Nat'
x = case Nat'
x of
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
_ -> Maybe Nat'
forall a. Maybe a
Nothing
iMul :: Interval -> Interval -> Interval
iMul :: Interval -> Interval -> Interval
iMul i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat' -> Nat' -> Nat'
nMul (Interval -> Nat'
iLower Interval
i) (Interval -> Nat'
iLower Interval
j)
, iUpper :: Maybe Nat'
iUpper = case (Interval -> Maybe Nat'
iUpper Interval
i, Interval -> Maybe Nat'
iUpper Interval
j) of
(Nothing, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just x :: Nat'
x, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMul Nat'
x Nat'
y)
(Nothing, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
upper Nat'
y
(Just x :: Nat'
x, Nothing) -> Nat' -> Maybe Nat'
upper Nat'
x
}
where
upper :: Nat' -> Maybe Nat'
upper x :: Nat'
x = case Nat'
x of
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
Nat 0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat 0)
_ -> Maybe Nat'
forall a. Maybe a
Nothing
iExp :: Interval -> Interval -> Interval
iExp :: Interval -> Interval -> Interval
iExp i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat' -> Nat' -> Nat'
nExp (Interval -> Nat'
iLower Interval
i) (Interval -> Nat'
iLower Interval
j)
, iUpper :: Maybe Nat'
iUpper = case (Interval -> Maybe Nat'
iUpper Interval
i, Interval -> Maybe Nat'
iUpper Interval
j) of
(Nothing, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just x :: Nat'
x, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nExp Nat'
x Nat'
y)
(Nothing, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
upperR Nat'
y
(Just x :: Nat'
x, Nothing) -> Nat' -> Maybe Nat'
upperL Nat'
x
}
where
upperL :: Nat' -> Maybe Nat'
upperL x :: Nat'
x = case Nat'
x of
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
Nat 0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat 0)
Nat 1 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat 1)
_ -> Maybe Nat'
forall a. Maybe a
Nothing
upperR :: Nat' -> Maybe Nat'
upperR x :: Nat'
x = case Nat'
x of
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
Nat 0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat 1)
_ -> Maybe Nat'
forall a. Maybe a
Nothing
iMin :: Interval -> Interval -> Interval
iMin :: Interval -> Interval -> Interval
iMin i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat' -> Nat' -> Nat'
nMin (Interval -> Nat'
iLower Interval
i) (Interval -> Nat'
iLower Interval
j)
, iUpper :: Maybe Nat'
iUpper = case (Interval -> Maybe Nat'
iUpper Interval
i, Interval -> Maybe Nat'
iUpper Interval
j) of
(Nothing, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just x :: Nat'
x, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMin Nat'
x Nat'
y)
(Nothing, Just Inf) -> Maybe Nat'
forall a. Maybe a
Nothing
(Nothing, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y
(Just Inf, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just x :: Nat'
x, Nothing) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
x
}
iMax :: Interval -> Interval -> Interval
iMax :: Interval -> Interval -> Interval
iMax i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat' -> Nat' -> Nat'
nMax (Interval -> Nat'
iLower Interval
i) (Interval -> Nat'
iLower Interval
j)
, iUpper :: Maybe Nat'
iUpper = case (Interval -> Maybe Nat'
iUpper Interval
i, Interval -> Maybe Nat'
iUpper Interval
j) of
(Nothing, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just x :: Nat'
x, Just y :: Nat'
y) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMax Nat'
x Nat'
y)
(Nothing, Just Inf) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
(Nothing, Just _) -> Maybe Nat'
forall a. Maybe a
Nothing
(Just Inf, Nothing) -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
(Just _, Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
}
iSub :: Interval -> Interval -> Interval
iSub :: Interval -> Interval -> Interval
iSub i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat'
lower, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
upper }
where
lower :: Nat'
lower = case Interval -> Maybe Nat'
iUpper Interval
j of
Nothing -> Integer -> Nat'
Nat 0
Just x :: Nat'
x -> case Nat' -> Nat' -> Maybe Nat'
nSub (Interval -> Nat'
iLower Interval
i) Nat'
x of
Nothing -> Integer -> Nat'
Nat 0
Just y :: Nat'
y -> Nat'
y
upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
i of
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
Just x :: Nat'
x -> case Nat' -> Nat' -> Maybe Nat'
nSub Nat'
x (Interval -> Nat'
iLower Interval
j) of
Nothing -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
Just y :: Nat'
y -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y
iDiv :: Interval -> Interval -> Interval
iDiv :: Interval -> Interval -> Interval
iDiv i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat'
lower, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
upper }
where
lower :: Nat'
lower = case Interval -> Maybe Nat'
iUpper Interval
j of
Nothing -> Integer -> Nat'
Nat 0
Just x :: Nat'
x -> case Nat' -> Nat' -> Maybe Nat'
nDiv (Interval -> Nat'
iLower Interval
i) Nat'
x of
Nothing -> Integer -> Nat'
Nat 0
Just y :: Nat'
y -> Nat'
y
upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
i of
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
Just x :: Nat'
x -> case Nat' -> Nat' -> Maybe Nat'
nDiv Nat'
x (Nat' -> Nat' -> Nat'
nMax (Interval -> Nat'
iLower Interval
i) (Integer -> Nat'
Nat 1)) of
Nothing -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
Just y :: Nat'
y -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y
iMod :: Interval -> Interval -> Interval
iMod :: Interval -> Interval -> Interval
iMod _ j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Integer -> Nat'
Nat 0, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
upper }
where
upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
j of
Just (Nat n :: Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1))
_ -> Maybe Nat'
forall a. Maybe a
Nothing
iCeilDiv :: Interval -> Interval -> Interval
iCeilDiv :: Interval -> Interval -> Interval
iCeilDiv i :: Interval
i j :: Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat'
lower, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
upper }
where
lower :: Nat'
lower = case Interval -> Maybe Nat'
iUpper Interval
j of
Nothing -> if Interval -> Nat'
iLower Interval
i Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Nat'
Nat 0 then Integer -> Nat'
Nat 0 else Integer -> Nat'
Nat 1
Just x :: Nat'
x -> case Nat' -> Nat' -> Maybe Nat'
nCeilDiv (Interval -> Nat'
iLower Interval
i) Nat'
x of
Nothing -> Integer -> Nat'
Nat 0
Just y :: Nat'
y -> Nat'
y
upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
i of
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
Just x :: Nat'
x -> case Nat' -> Nat' -> Maybe Nat'
nCeilDiv Nat'
x (Nat' -> Nat' -> Nat'
nMax (Interval -> Nat'
iLower Interval
i) (Integer -> Nat'
Nat 1)) of
Nothing -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
Just y :: Nat'
y -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y
iCeilMod :: Interval -> Interval -> Interval
iCeilMod :: Interval -> Interval -> Interval
iCeilMod = Interval -> Interval -> Interval
iMod
iWidth :: Interval -> Interval
iWidth :: Interval -> Interval
iWidth i :: Interval
i = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Nat' -> Nat'
nWidth (Interval -> Nat'
iLower Interval
i)
, iUpper :: Maybe Nat'
iUpper = case Interval -> Maybe Nat'
iUpper Interval
i of
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
Just n :: Nat'
n -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat'
nWidth Nat'
n)
}
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
iLenFromThenTo i :: Interval
i j :: Interval
j k :: Interval
k
| Just x :: Nat'
x <- Interval -> Maybe Nat'
iIsExact Interval
i, Just y :: Nat'
y <- Interval -> Maybe Nat'
iIsExact Interval
j, Just z :: Nat'
z <- Interval -> Maybe Nat'
iIsExact Interval
k
, Just r :: Nat'
r <- Nat' -> Nat' -> Nat' -> Maybe Nat'
nLenFromThenTo Nat'
x Nat'
y Nat'
z = Nat' -> Interval
iConst Nat'
r
| Bool
otherwise = Interval
iAnyFin