-- |
-- 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 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


-- | What we learn about variables from a single prop.
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 })

    -- k >= width x
  , 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
           -- 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 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'          -- ^ 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 (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

-- | Finite positive number. @[1 ..  inf)@.
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


-- | Returns 'True' when the intervals definitely overlap, and 'False'
-- otherwise.
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


-- | 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 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


-- | Any value
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)

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

-- | Exactly this value
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 {- malformed subtraction -}
                         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   -- malformed division
                         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   -- malformed division
                         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 -- bounds are the same as for Mod

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