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