-- |
-- Module      :  Cryptol.TypeCheck.Solver.Numeric.Interval
-- Copyright   :  (c) 2015-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- An interval interpretation of types.

{-# 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)


-- | Only meaningful for numeric types
typeInterval :: Map TVar Interval -> Type -> Interval
typeInterval :: Map TVar Interval -> Type -> Interval
typeInterval Map TVar Interval
varInfo = Type -> Interval
go
  where
  go :: Type -> Interval
go Type
ty =
    case Type
ty of
      TUser Name
_ [Type]
_ Type
t -> Type -> Interval
go Type
t
      TCon TCon
tc [Type]
ts ->
        case (TCon
tc, [Type]
ts) of
          (TC TC
TCInf, [])      -> Nat' -> Interval
iConst Nat'
Inf
          (TC (TCNum Integer
n), [])  -> Nat' -> Interval
iConst (Integer -> Nat'
Nat Integer
n)
          (TF TFun
TCAdd, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iAdd (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCSub, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iSub (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCMul, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iMul (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCDiv, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iDiv (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCMod, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iMod (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCExp, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iExp (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCWidth, [Type
x])   -> Interval -> Interval
iWidth (Type -> Interval
go Type
x)
          (TF TFun
TCMin, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iMin (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCMax, [Type
x,Type
y])   -> Interval -> Interval -> Interval
iMax (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)

          (TF TFun
TCCeilDiv, [Type
x,Type
y]) -> Interval -> Interval -> Interval
iCeilDiv (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)
          (TF TFun
TCCeilMod, [Type
x,Type
y]) -> Interval -> Interval -> Interval
iCeilMod (Type -> Interval
go Type
x) (Type -> Interval
go Type
y)

          (TF TFun
TCLenFromThenTo, [Type
x,Type
y,Type
z]) ->
            Interval -> Interval -> Interval -> Interval
iLenFromThenTo (Type -> Interval
go Type
x) (Type -> Interval
go Type
y) (Type -> Interval
go Type
z)
          (TCon, [Type])
_ -> Interval
iAny

      TVar TVar
x -> Map TVar Interval -> TVar -> Interval
tvarInterval Map TVar Interval
varInfo TVar
x

      Type
_ -> Interval
iAny

tvarInterval :: Map TVar Interval -> TVar -> Interval
tvarInterval :: Map TVar Interval -> TVar -> Interval
tvarInterval Map TVar Interval
varInfo 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 (TVar
x,Interval
int) 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 Interval
int' ->
      case Interval -> Interval -> Maybe Interval
iIntersect Interval
int Interval
int' of
        Just 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
        Maybe Interval
Nothing                -> TVar -> IntervalUpdate
InvalidInterval TVar
x

    Maybe Interval
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 Map TVar Interval
ints [Type]
ps0 = Int -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
forall t.
(Ord t, Num t) =>
t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go (Int
3 :: Int) Bool
False Map TVar Interval
ints [Type]
ps0
  where
  go :: t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go !t
_n Bool
False Map TVar Interval
_ [] = IntervalUpdate
NoChange

  go !t
n Bool
True  Map TVar Interval
is []
    | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
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
-t
1) Bool
False Map TVar Interval
is [Type]
ps0)
    | Bool
otherwise = Map TVar Interval -> IntervalUpdate
NewIntervals Map TVar Interval
is

  go !t
n Bool
new   Map TVar Interval
is (Type
p:[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 TVar
i -> TVar -> IntervalUpdate
InvalidInterval TVar
i
      NewIntervals Map TVar Interval
is'  -> t -> Bool -> Map TVar Interval -> [Type] -> IntervalUpdate
go t
n Bool
True Map TVar Interval
is' [Type]
ps
      IntervalUpdate
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 Bool
ch [] Map TVar Interval
int = if Bool
ch then Map TVar Interval -> IntervalUpdate
NewIntervals Map TVar Interval
int else IntervalUpdate
NoChange
  add Bool
ch ((TVar, Interval)
i:[(TVar, Interval)]
is) Map TVar Interval
int = case (TVar, Interval) -> Map TVar Interval -> IntervalUpdate
updateInterval (TVar, Interval)
i Map TVar Interval
int of
                        InvalidInterval TVar
j -> TVar -> IntervalUpdate
InvalidInterval TVar
j
                        IntervalUpdate
NoChange          -> Bool -> [(TVar, Interval)] -> Map TVar Interval -> IntervalUpdate
add Bool
ch [(TVar, Interval)]
is Map TVar Interval
int
                        NewIntervals 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 Map TVar Interval
a IntervalUpdate
x = case IntervalUpdate
x of
                  IntervalUpdate
NoChange -> Map TVar Interval -> IntervalUpdate
NewIntervals Map TVar Interval
a
                  IntervalUpdate
r        -> IntervalUpdate
r


-- | What we learn about variables from a single prop.
propInterval :: Map TVar Interval -> Prop -> [(TVar,Interval)]
propInterval :: Map TVar Interval -> Type -> [(TVar, Interval)]
propInterval Map TVar Interval
varInts 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 (Type
l,Type
r) <- Type -> Maybe (Type, Type)
pIsEqual 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 (Type
l,Type
r) <- Type -> Maybe (Type, Type)
pIsEqual 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 (Type
l,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 (Type
l,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 Integer
0 })

    -- k >= width x
  , do (Type
l,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
           -- record the exact upper bound when it produces values within 128
           -- bits
       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 Integer
val) | Integer
val Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
128 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat (Integer
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
- Integer
1))
                                 | Bool
otherwise -> Maybe Nat'
forall a. Maybe a
Nothing
                  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 Integer
0, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
ub })

    , do (Type
e,Type
_) <- Type -> Maybe (Type, Type)
pIsValidFloat Type
prop
         TVar
x <- Type -> Maybe TVar
tIsVar Type
e
         (TVar, Interval) -> Maybe (TVar, Interval)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TVar
x, Interval
iAnyFin)

    , do (Type
_,Type
p) <- Type -> Maybe (Type, Type)
pIsValidFloat Type
prop
         TVar
x <- Type -> Maybe TVar
tIsVar Type
p
         (TVar, Interval) -> Maybe (TVar, Interval)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TVar
x, Interval
iAnyFin)

  ]


--------------------------------------------------------------------------------

data Interval = Interval
  { Interval -> Nat'
iLower :: Nat'          -- ^ lower bound (inclusive)
  , Interval -> Maybe Nat'
iUpper :: Maybe Nat'    -- ^ upper bound (inclusive)
                            -- If there is no upper bound,
                            -- then all *natural* numbers.
  } 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 (a
var,Interval
i) = a -> Doc
forall a. PP a => a -> Doc
pp a
var Doc -> Doc -> Doc
<.> Char -> Doc
char Char
':' Doc -> Doc -> Doc
<+> Interval -> Doc
ppInterval Interval
i

ppInterval :: Interval -> Doc
ppInterval :: Interval -> Doc
ppInterval Interval
x = Doc -> Doc
brackets ([Doc] -> Doc
hsep [ Nat' -> Doc
ppr (Interval -> Nat'
iLower Interval
x)
                              , String -> Doc
text String
".."
                              , Doc -> (Nat' -> Doc) -> Maybe Nat' -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Doc
text String
"fin") Nat' -> Doc
ppr (Interval -> Maybe Nat'
iUpper Interval
x)])
  where
  ppr :: Nat' -> Doc
ppr Nat'
a = case Nat'
a of
           Nat Integer
n -> Integer -> Doc
integer Integer
n
           Nat'
Inf   -> String -> Doc
text String
"inf"


iIsExact :: Interval -> Maybe Nat'
iIsExact :: Interval -> Maybe Nat'
iIsExact 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 Interval
i = case Interval -> Maybe Nat'
iUpper Interval
i of
             Just Nat'
Inf -> Bool
False
             Maybe Nat'
_        -> Bool
True

-- | Finite positive number. @[1 ..  inf)@.
iIsPosFin :: Interval -> Bool
iIsPosFin :: Interval -> Bool
iIsPosFin Interval
i = Interval -> Nat'
iLower Interval
i Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat Integer
1 Bool -> Bool -> Bool
&& Interval -> Bool
iIsFin Interval
i


-- | Returns 'True' when the intervals definitely overlap, and 'False'
-- otherwise.
iOverlap :: Interval -> Interval -> Bool
iOverlap :: Interval -> Interval -> Bool
iOverlap
  (Interval (Nat Integer
l1) (Just (Nat Integer
h1)))
  (Interval (Nat Integer
l2) (Just (Nat 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 Interval
_ Interval
_ = Bool
False


-- | Intersect two intervals, yielding a new one that describes the space where
-- they overlap.  If the two intervals are disjoint, the result will be
-- 'Nothing'.
iIntersect :: Interval -> Interval -> Maybe Interval
iIntersect :: Interval -> Interval -> Maybe Interval
iIntersect Interval
i Interval
j =
  case (Nat'
lower,Maybe Nat'
upper) of
    (Nat Integer
l, Just (Nat Integer
u)) | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
u -> Maybe Interval
ok
    (Nat Integer
_, Just  Nat'
Inf)             -> Maybe Interval
ok
    (Nat Integer
_, Maybe Nat'
Nothing)               -> Maybe Interval
ok
    (Nat'
Inf,   Just Nat'
Inf)              -> Maybe Interval
ok
    (Nat', Maybe Nat')
_                              -> 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 Nat'
a, Just Nat'
b)            -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMin Nat'
a Nat'
b)
            (Maybe Nat'
Nothing,Maybe Nat'
Nothing)           -> Maybe Nat'
forall a. Maybe a
Nothing
            (Just Nat'
l,Maybe Nat'
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
            (Maybe Nat'
Nothing,Just 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', Maybe Nat')
_                           -> Maybe Nat'
forall a. Maybe a
Nothing


-- | Any value
iAny :: Interval
iAny :: Interval
iAny = Nat' -> Maybe Nat' -> Interval
Interval (Integer -> Nat'
Nat Integer
0) (Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf)

-- | Any finite value
iAnyFin :: Interval
iAnyFin :: Interval
iAnyFin = Nat' -> Maybe Nat' -> Interval
Interval (Integer -> Nat'
Nat Integer
0) Maybe Nat'
forall a. Maybe a
Nothing

-- | Exactly this value
iConst :: Nat' -> Interval
iConst :: Nat' -> Interval
iConst 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 Interval
i 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
                                 (Maybe Nat'
Nothing, Maybe Nat'
Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
x, Just Nat'
y)   -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nAdd Nat'
x Nat'
y)
                                 (Maybe Nat'
Nothing, Just Nat'
y)  -> Nat' -> Maybe Nat'
upper Nat'
y
                                 (Just Nat'
x, Maybe Nat'
Nothing)  -> Nat' -> Maybe Nat'
upper Nat'
x
                    }
  where
  upper :: Nat' -> Maybe Nat'
upper Nat'
x = case Nat'
x of
              Nat'
Inf -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
              Nat'
_   -> Maybe Nat'
forall a. Maybe a
Nothing

iMul :: Interval -> Interval -> Interval
iMul :: Interval -> Interval -> Interval
iMul Interval
i 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
                                 (Maybe Nat'
Nothing, Maybe Nat'
Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
x, Just Nat'
y)   -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMul Nat'
x Nat'
y)
                                 (Maybe Nat'
Nothing, Just Nat'
y)  -> Nat' -> Maybe Nat'
upper Nat'
y
                                 (Just Nat'
x, Maybe Nat'
Nothing)  -> Nat' -> Maybe Nat'
upper Nat'
x
                    }
  where
  upper :: Nat' -> Maybe Nat'
upper Nat'
x = case Nat'
x of
              Nat'
Inf   -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
              Nat Integer
0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat Integer
0)
              Nat'
_     -> Maybe Nat'
forall a. Maybe a
Nothing

iExp :: Interval -> Interval -> Interval
iExp :: Interval -> Interval -> Interval
iExp Interval
i 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
                                 (Maybe Nat'
Nothing, Maybe Nat'
Nothing) -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
x, Just Nat'
y)   -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nExp Nat'
x Nat'
y)
                                 (Maybe Nat'
Nothing, Just Nat'
y)  -> Nat' -> Maybe Nat'
upperR Nat'
y
                                 (Just Nat'
x, Maybe Nat'
Nothing)  -> Nat' -> Maybe Nat'
upperL Nat'
x
                    }
  where
  upperL :: Nat' -> Maybe Nat'
upperL Nat'
x = case Nat'
x of
               Nat'
Inf   -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
               Nat Integer
0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat Integer
0)
               Nat Integer
1 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat Integer
1)
               Nat'
_     -> Maybe Nat'
forall a. Maybe a
Nothing

  upperR :: Nat' -> Maybe Nat'
upperR Nat'
x = case Nat'
x of
               Nat'
Inf   -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
               Nat Integer
0 -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat Integer
1)
               Nat'
_     -> Maybe Nat'
forall a. Maybe a
Nothing

iMin :: Interval -> Interval -> Interval
iMin :: Interval -> Interval -> Interval
iMin Interval
i 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
                                 (Maybe Nat'
Nothing, Maybe Nat'
Nothing)   -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
x, Just Nat'
y)     -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMin Nat'
x Nat'
y)
                                 (Maybe Nat'
Nothing, Just Nat'
Inf)  -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Maybe Nat'
Nothing, Just Nat'
y)    -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y
                                 (Just Nat'
Inf, Maybe Nat'
Nothing)  -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
x, Maybe Nat'
Nothing)    -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
x
                    }

iMax :: Interval -> Interval -> Interval
iMax :: Interval -> Interval -> Interval
iMax Interval
i 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
                                 (Maybe Nat'
Nothing, Maybe Nat'
Nothing)   -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
x, Just Nat'
y)     -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Nat' -> Nat' -> Nat'
nMax Nat'
x Nat'
y)
                                 (Maybe Nat'
Nothing, Just Nat'
Inf)  -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
                                 (Maybe Nat'
Nothing, Just Nat'
_)    -> Maybe Nat'
forall a. Maybe a
Nothing
                                 (Just Nat'
Inf, Maybe Nat'
Nothing)  -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
                                 (Just Nat'
_, Maybe Nat'
Nothing)    -> Maybe Nat'
forall a. Maybe a
Nothing
                    }

iSub :: Interval -> Interval -> Interval
iSub :: Interval -> Interval -> Interval
iSub Interval
i 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
            Maybe Nat'
Nothing -> Integer -> Nat'
Nat Integer
0
            Just Nat'
x  -> case Nat' -> Nat' -> Maybe Nat'
nSub (Interval -> Nat'
iLower Interval
i) Nat'
x of
                         Maybe Nat'
Nothing -> Integer -> Nat'
Nat Integer
0
                         Just Nat'
y  -> Nat'
y


  upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
i of
            Maybe Nat'
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
            Just Nat'
x  -> case Nat' -> Nat' -> Maybe Nat'
nSub Nat'
x (Interval -> Nat'
iLower Interval
j) of
                         Maybe Nat'
Nothing -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf {- malformed subtraction -}
                         Just Nat'
y  -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y


iDiv :: Interval -> Interval -> Interval
iDiv :: Interval -> Interval -> Interval
iDiv Interval
i 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
            Maybe Nat'
Nothing -> Integer -> Nat'
Nat Integer
0
            Just Nat'
x  -> case Nat' -> Nat' -> Maybe Nat'
nDiv (Interval -> Nat'
iLower Interval
i) Nat'
x of
                         Maybe Nat'
Nothing -> Integer -> Nat'
Nat Integer
0   -- malformed division
                         Just Nat'
y  -> Nat'
y

  upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
i of
            Maybe Nat'
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
            Just Nat'
x  -> case Nat' -> Nat' -> Maybe Nat'
nDiv Nat'
x (Nat' -> Nat' -> Nat'
nMax (Interval -> Nat'
iLower Interval
i) (Integer -> Nat'
Nat Integer
1)) of
                         Maybe Nat'
Nothing -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
                         Just Nat'
y  -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
y


iMod :: Interval -> Interval -> Interval
iMod :: Interval -> Interval -> Interval
iMod Interval
_ Interval
j = Interval :: Nat' -> Maybe Nat' -> Interval
Interval { iLower :: Nat'
iLower = Integer -> Nat'
Nat Integer
0, iUpper :: Maybe Nat'
iUpper = Maybe Nat'
upper }
  where
  upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
j of
            Just (Nat Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
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
- Integer
1))
            Maybe Nat'
_                    -> Maybe Nat'
forall a. Maybe a
Nothing


iCeilDiv :: Interval -> Interval -> Interval
iCeilDiv :: Interval -> Interval -> Interval
iCeilDiv Interval
i 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
            Maybe Nat'
Nothing -> if Interval -> Nat'
iLower Interval
i Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Nat'
Nat Integer
0 then Integer -> Nat'
Nat Integer
0 else Integer -> Nat'
Nat Integer
1
            Just Nat'
x  -> case Nat' -> Nat' -> Maybe Nat'
nCeilDiv (Interval -> Nat'
iLower Interval
i) Nat'
x of
                         Maybe Nat'
Nothing -> Integer -> Nat'
Nat Integer
0   -- malformed division
                         Just Nat'
y  -> Nat'
y

  upper :: Maybe Nat'
upper = case Interval -> Maybe Nat'
iUpper Interval
i of
            Maybe Nat'
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
            Just Nat'
x  -> case Nat' -> Nat' -> Maybe Nat'
nCeilDiv Nat'
x (Nat' -> Nat' -> Nat'
nMax (Interval -> Nat'
iLower Interval
i) (Integer -> Nat'
Nat Integer
1)) of
                         Maybe Nat'
Nothing -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
                         Just 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 -- bounds are the same as for Mod

iWidth :: Interval -> Interval
iWidth :: Interval -> Interval
iWidth 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
                                 Maybe Nat'
Nothing -> Maybe Nat'
forall a. Maybe a
Nothing
                                 Just 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 Interval
i Interval
j Interval
k
  | Just Nat'
x <- Interval -> Maybe Nat'
iIsExact Interval
i, Just Nat'
y <- Interval -> Maybe Nat'
iIsExact Interval
j, Just Nat'
z <- Interval -> Maybe Nat'
iIsExact Interval
k
  , Just Nat'
r <- Nat' -> Nat' -> Nat' -> Maybe Nat'
nLenFromThenTo Nat'
x Nat'
y Nat'
z = Nat' -> Interval
iConst Nat'
r
  | Bool
otherwise = Interval
iAnyFin