    {-|
    Module      : What4.Utils.AbstractDomains
    Description : Abstract domains for term simplification
    Copyright   : (c) Galois Inc, 2015-2020
    License     : BSD3
    Maintainer  : jhendrix@galois.com

    This module declares a set of abstract domains used by the solver.
    These are mostly interval domains on numeric types.

    Since these abstract domains are baked directly into the term
    representation, we want to get as much bang-for-buck as possible.
    Thus, we prioritize compact representations and simple algorithms over
    precision.
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE ViewPatterns #-}

    module What4.Utils.AbstractDomains
      ( ValueBound(..)
      , minValueBound
      , maxValueBound
        -- * ValueRange
      , ValueRange(..)
      , pattern MultiRange
      , unboundedRange
      , mapRange
      , rangeLowBound
      , rangeHiBound
      , singleRange
      , concreteRange
      , valueRange
      , addRange
      , negateRange
      , rangeScalarMul
      , mulRange
      , joinRange
      , asSingleRange
      , rangeCheckEq
      , rangeCheckLe
      , rangeMin
      , rangeMax
        -- * integer range operations
      , intAbsRange
      , intDivRange
      , intModRange
        -- * Boolean abstract value
      , absAnd
      , absOr

        -- * RealAbstractValue
      , RealAbstractValue(..)
      , ravUnbounded
      , ravSingle
      , ravConcreteRange
      , ravJoin
      , ravAdd
      , ravScalarMul
      , ravMul
      , ravCheckEq
      , ravCheckLe
        -- * StringAbstractValue
      , StringAbstractValue(..)
      , stringAbsJoin
      , stringAbsTop
      , stringAbsSingle
      , stringAbsOverlap
      , stringAbsLength
      , stringAbsConcat
      , stringAbsSubstring
      , stringAbsContains
      , stringAbsIsPrefixOf
      , stringAbsIsSuffixOf
      , stringAbsIndexOf
      , stringAbsEmpty

        -- * Abstractable
      , avTop
      , avSingle
      , avContains
      , AbstractValue
      , ConcreteValue
      , Abstractable(..)
      , withAbstractable
      , AbstractValueWrapper(..)
      , ConcreteValueWrapper(..)
      , HasAbsValue(..)
      ) where

    import           Control.Exception (assert)
    import           Data.Kind
    import           Data.Parameterized.Context as Ctx
    import           Data.Parameterized.NatRepr
    import           Data.Parameterized.TraversableFC
    import           Data.Ratio (denominator)

    import           What4.BaseTypes
    import           What4.Utils.BVDomain (BVDomain)
    import qualified What4.Utils.BVDomain as BVD
    import           What4.Utils.Complex
    import           What4.Utils.StringLiteral

    ctxZipWith3 :: (forall (x::k) . a x -> b x -> c x -> d x)
                -> Ctx.Assignment a (ctx::Ctx.Ctx k)
                -> Ctx.Assignment b ctx
                -> Ctx.Assignment c ctx
                -> Ctx.Assignment d ctx
    ctxZipWith3 :: forall k (a :: k -> Type) (b :: k -> Type) (c :: k -> Type)
           (d :: k -> Type) (ctx :: Ctx k).
    (forall (x :: k). a x -> b x -> c x -> d x)
    -> Assignment a ctx
    -> Assignment b ctx
    -> Assignment c ctx
    -> Assignment d ctx
    ctxZipWith3 forall (x :: k). a x -> b x -> c x -> d x
    f Assignment a ctx
    a Assignment b ctx
    b Assignment c ctx
    c =
      Size ctx
    -> (forall (tp :: k). Index ctx tp -> d tp) -> Assignment d ctx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    Size ctx
    -> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
    Ctx.generate (Assignment a ctx -> Size ctx
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    Ctx.size Assignment a ctx
    a) ((forall (tp :: k). Index ctx tp -> d tp) -> Assignment d ctx)
    -> (forall (tp :: k). Index ctx tp -> d tp) -> Assignment d ctx
    forall a b. (a -> b) -> a -> b
    $ \Index ctx tp
    i ->
        a tp -> b tp -> c tp -> d tp
    forall (x :: k). a x -> b x -> c x -> d x
    f (Assignment a ctx
    a Assignment a ctx -> Index ctx tp -> a tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i) (Assignment b ctx
    b Assignment b ctx -> Index ctx tp -> b tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i) (Assignment c ctx
    c Assignment c ctx -> Index ctx tp -> c tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i)

    ------------------------------------------------------------------------
    -- ValueBound

    -- | A lower or upper bound on a value.
    data ValueBound tp
       = Unbounded
       | Inclusive !tp
      deriving ((forall a b. (a -> b) -> ValueBound a -> ValueBound b)
    -> (forall a b. a -> ValueBound b -> ValueBound a)
    -> Functor ValueBound
    forall a b. a -> ValueBound b -> ValueBound a
    forall a b. (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> ValueBound a -> ValueBound b
    fmap :: forall a b. (a -> b) -> ValueBound a -> ValueBound b
    $c<$ :: forall a b. a -> ValueBound b -> ValueBound a
    <$ :: forall a b. a -> ValueBound b -> ValueBound a
    Functor, Int -> ValueBound tp -> ShowS
    [ValueBound tp] -> ShowS
    ValueBound tp -> String
    (Int -> ValueBound tp -> ShowS)
    -> (ValueBound tp -> String)
    -> ([ValueBound tp] -> ShowS)
    -> Show (ValueBound tp)
    forall tp. Show tp => Int -> ValueBound tp -> ShowS
    forall tp. Show tp => [ValueBound tp] -> ShowS
    forall tp. Show tp => ValueBound tp -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall tp. Show tp => Int -> ValueBound tp -> ShowS
    showsPrec :: Int -> ValueBound tp -> ShowS
    $cshow :: forall tp. Show tp => ValueBound tp -> String
    show :: ValueBound tp -> String
    $cshowList :: forall tp. Show tp => [ValueBound tp] -> ShowS
    showList :: [ValueBound tp] -> ShowS
    Show, ValueBound tp -> ValueBound tp -> Bool
    (ValueBound tp -> ValueBound tp -> Bool)
    -> (ValueBound tp -> ValueBound tp -> Bool) -> Eq (ValueBound tp)
    forall tp. Eq tp => ValueBound tp -> ValueBound tp -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall tp. Eq tp => ValueBound tp -> ValueBound tp -> Bool
    == :: ValueBound tp -> ValueBound tp -> Bool
    $c/= :: forall tp. Eq tp => ValueBound tp -> ValueBound tp -> Bool
    /= :: ValueBound tp -> ValueBound tp -> Bool
    Eq, Eq (ValueBound tp)
    Eq (ValueBound tp) =>
    (ValueBound tp -> ValueBound tp -> Ordering)
    -> (ValueBound tp -> ValueBound tp -> Bool)
    -> (ValueBound tp -> ValueBound tp -> Bool)
    -> (ValueBound tp -> ValueBound tp -> Bool)
    -> (ValueBound tp -> ValueBound tp -> Bool)
    -> (ValueBound tp -> ValueBound tp -> ValueBound tp)
    -> (ValueBound tp -> ValueBound tp -> ValueBound tp)
    -> Ord (ValueBound tp)
    ValueBound tp -> ValueBound tp -> Bool
    ValueBound tp -> ValueBound tp -> Ordering
    ValueBound tp -> ValueBound tp -> ValueBound tp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall tp. Ord tp => Eq (ValueBound tp)
    forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
    forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Ordering
    forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    $ccompare :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Ordering
    compare :: ValueBound tp -> ValueBound tp -> Ordering
    $c< :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
    < :: ValueBound tp -> ValueBound tp -> Bool
    $c<= :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
    <= :: ValueBound tp -> ValueBound tp -> Bool
    $c> :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
    > :: ValueBound tp -> ValueBound tp -> Bool
    $c>= :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
    >= :: ValueBound tp -> ValueBound tp -> Bool
    $cmax :: forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    max :: ValueBound tp -> ValueBound tp -> ValueBound tp
    $cmin :: forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    min :: ValueBound tp -> ValueBound tp -> ValueBound tp
    Ord)

    instance Applicative ValueBound where
      pure :: forall a. a -> ValueBound a
    pure = a -> ValueBound a
    forall a. a -> ValueBound a
    Inclusive
      ValueBound (a -> b)
    Unbounded <*> :: forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    <*> ValueBound a
    _ = ValueBound b
    forall tp. ValueBound tp
    Unbounded
      ValueBound (a -> b)
    _ <*> ValueBound a
    Unbounded = ValueBound b
    forall tp. ValueBound tp
    Unbounded
      Inclusive a -> b
    f <*> Inclusive a
    v = b -> ValueBound b
    forall a. a -> ValueBound a
    Inclusive (a -> b
    f a
    v)

    instance Monad ValueBound where
      return :: forall a. a -> ValueBound a
    return = a -> ValueBound a
    forall a. a -> ValueBound a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure
      ValueBound a
    Unbounded >>= :: forall a b. ValueBound a -> (a -> ValueBound b) -> ValueBound b
    >>= a -> ValueBound b
    _ = ValueBound b
    forall tp. ValueBound tp
    Unbounded
      Inclusive a
    v >>= a -> ValueBound b
    f = a -> ValueBound b
    f a
    v

    minValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
    minValueBound :: forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    minValueBound ValueBound tp
    x ValueBound tp
    y = tp -> tp -> tp
    forall a. Ord a => a -> a -> a
    min (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    x ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    y

    maxValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
    maxValueBound :: forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    maxValueBound ValueBound tp
    x ValueBound tp
    y = tp -> tp -> tp
    forall a. Ord a => a -> a -> a
    max (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    x ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    y

    lowerBoundIsNegative :: (Ord tp, Num tp) => ValueBound tp -> Bool
    lowerBoundIsNegative :: forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
    lowerBoundIsNegative ValueBound tp
    Unbounded = Bool
    True
    lowerBoundIsNegative (Inclusive tp
    y) = tp
    y tp -> tp -> Bool
    forall a. Ord a => a -> a -> Bool
    <= tp
    0

    upperBoundIsNonNeg :: (Ord tp, Num tp) => ValueBound tp -> Bool
    upperBoundIsNonNeg :: forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
    upperBoundIsNonNeg ValueBound tp
    Unbounded = Bool
    True
    upperBoundIsNonNeg (Inclusive tp
    y) = tp
    y tp -> tp -> Bool
    forall a. Ord a => a -> a -> Bool
    >= tp
    0

    ------------------------------------------------------------------------
    -- ValueRange support classes.

    -- | Describes a range of values in a totally ordered set.
    data ValueRange tp
      = SingleRange !tp
        -- ^ Indicates that range denotes a single value
      | UnboundedRange
        -- ^ The number is unconstrained.
      | MinRange !tp
        -- ^ The number is greater than or equal to the given lower bound.
      | MaxRange !tp
        -- ^ The number is less than or equal to the given upper bound.
      | IntervalRange !tp !tp
        -- ^ The number is between the given lower and upper bounds.

    asMultiRange :: ValueRange tp -> Maybe (ValueBound tp, ValueBound tp)
    asMultiRange :: forall tp. ValueRange tp -> Maybe (ValueBound tp, ValueBound tp)
    asMultiRange ValueRange tp
    r =
      case ValueRange tp
    r of
        SingleRange tp
    _ -> Maybe (ValueBound tp, ValueBound tp)
    forall a. Maybe a
    Nothing
        ValueRange tp
    UnboundedRange -> (ValueBound tp, ValueBound tp)
    -> Maybe (ValueBound tp, ValueBound tp)
    forall a. a -> Maybe a
    Just (ValueBound tp
    forall tp. ValueBound tp
    Unbounded, ValueBound tp
    forall tp. ValueBound tp
    Unbounded)
        MinRange tp
    lo -> (ValueBound tp, ValueBound tp)
    -> Maybe (ValueBound tp, ValueBound tp)
    forall a. a -> Maybe a
    Just (tp -> ValueBound tp
    forall a. a -> ValueBound a
    Inclusive tp
    lo, ValueBound tp
    forall tp. ValueBound tp
    Unbounded)
        MaxRange tp
    hi -> (ValueBound tp, ValueBound tp)
    -> Maybe (ValueBound tp, ValueBound tp)
    forall a. a -> Maybe a
    Just (ValueBound tp
    forall tp. ValueBound tp
    Unbounded, tp -> ValueBound tp
    forall a. a -> ValueBound a
    Inclusive tp
    hi)
        IntervalRange tp
    lo tp
    hi -> (ValueBound tp, ValueBound tp)
    -> Maybe (ValueBound tp, ValueBound tp)
    forall a. a -> Maybe a
    Just (tp -> ValueBound tp
    forall a. a -> ValueBound a
    Inclusive tp
    lo, tp -> ValueBound tp
    forall a. a -> ValueBound a
    Inclusive tp
    hi)

    multiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp
    multiRange :: forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    multiRange ValueBound tp
    Unbounded ValueBound tp
    Unbounded = ValueRange tp
    forall tp. ValueRange tp
    UnboundedRange
    multiRange ValueBound tp
    Unbounded (Inclusive tp
    hi) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MaxRange tp
    hi
    multiRange (Inclusive tp
    lo) ValueBound tp
    Unbounded = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MinRange tp
    lo
    multiRange (Inclusive tp
    lo) (Inclusive tp
    hi) = tp -> tp -> ValueRange tp
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange tp
    lo tp
    hi

    -- | Indicates that the number is somewhere between the given upper and lower bound.
    pattern MultiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp
    pattern $mMultiRange :: forall {r} {tp}.
    ValueRange tp
    -> (ValueBound tp -> ValueBound tp -> r) -> ((# #) -> r) -> r
    $bMultiRange :: forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange lo hi <- (asMultiRange -> Just (lo, hi)) where
      MultiRange ValueBound tp
    lo ValueBound tp
    hi = ValueBound tp -> ValueBound tp -> ValueRange tp
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    multiRange ValueBound tp
    lo ValueBound tp
    hi

    {-# COMPLETE SingleRange, MultiRange #-}

    intAbsRange :: ValueRange Integer -> ValueRange Integer
    intAbsRange :: ValueRange Integer -> ValueRange Integer
    intAbsRange ValueRange Integer
    r =
      case ValueRange Integer
    r of
        SingleRange Integer
    x -> Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    SingleRange (Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    x)
        ValueRange Integer
    UnboundedRange -> Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    MinRange Integer
    0
        MinRange Integer
    lo
          | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    lo -> ValueRange Integer
    r
          | Bool
    otherwise -> Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    MinRange Integer
    0
        MaxRange Integer
    hi
          | Integer
    hi Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    0 -> Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    MinRange (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    hi)
          | Bool
    otherwise -> Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    MinRange Integer
    0
        IntervalRange Integer
    lo Integer
    hi
          | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    lo -> ValueRange Integer
    r
          | Integer
    hi Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    0 -> Integer -> Integer -> ValueRange Integer
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    hi) (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    lo)
          | Bool
    otherwise -> Integer -> Integer -> ValueRange Integer
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange Integer
    0 (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max (Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    lo) (Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    hi))

    -- | Compute an abstract range for integer division.  We are using the SMTLib
    --   division operation, where the division is floor when the divisor is positive
    --   and ceiling when the divisor is negative.  We compute the ranges assuming
    --   that division by 0 doesn't happen, and we are allowed to return nonsense
    --   ranges for these cases.
    intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    intDivRange (SingleRange Integer
    x) (SingleRange Integer
    y)
      | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0  = Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    SingleRange (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    y)
      | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0  = Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    SingleRange (Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    y))
    intDivRange (MultiRange ValueBound Integer
    lo ValueBound Integer
    hi) (SingleRange Integer
    y)
      | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >  Integer
    0 = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange
                       ((\Integer
    x -> Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound Integer
    lo)
                       ((\Integer
    x -> Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound Integer
    hi)
      | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <  Integer
    0 = ValueRange Integer -> ValueRange Integer
    forall tp. Num tp => ValueRange tp -> ValueRange tp
    negateRange (ValueRange Integer -> ValueRange Integer)
    -> ValueRange Integer -> ValueRange Integer
    forall a b. (a -> b) -> a -> b
    $ ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange
                        ((\Integer
    x -> Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound Integer
    lo)
                        ((\Integer
    x -> Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound Integer
    hi)

    intDivRange ValueRange Integer
    x (MultiRange (Inclusive Integer
    lo) ValueBound Integer
    hi)
      | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    lo = ValueRange Integer
    -> Integer -> ValueBound Integer -> ValueRange Integer
    intDivAux ValueRange Integer
    x Integer
    lo ValueBound Integer
    hi

    intDivRange ValueRange Integer
    x (MultiRange ValueBound Integer
    lo (Inclusive Integer
    hi))
      | Integer
    hi Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 = ValueRange Integer -> ValueRange Integer
    forall tp. Num tp => ValueRange tp -> ValueRange tp
    negateRange (ValueRange Integer
    -> Integer -> ValueBound Integer -> ValueRange Integer
    intDivAux ValueRange Integer
    x (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    hi) (Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound Integer
    lo))

    -- The divisor interval contains 0, so we learn nothing
    intDivRange ValueRange Integer
    _ ValueRange Integer
    _ = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound Integer
    forall tp. ValueBound tp
    Unbounded ValueBound Integer
    forall tp. ValueBound tp
    Unbounded

    -- Here we get to assume 'lo' and 'hi' are strictly positive
    intDivAux ::
      ValueRange Integer ->
      Integer -> ValueBound Integer ->
      ValueRange Integer
    intDivAux :: ValueRange Integer
    -> Integer -> ValueBound Integer -> ValueRange Integer
    intDivAux ValueRange Integer
    x Integer
    lo ValueBound Integer
    Unbounded = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound Integer
    lo' ValueBound Integer
    hi'
      where
      lo' :: ValueBound Integer
    lo' = case ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange Integer
    x of
               ValueBound Integer
    Unbounded -> ValueBound Integer
    forall tp. ValueBound tp
    Unbounded
               Inclusive Integer
    z -> Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    0 (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    z Integer
    lo))

      hi' :: ValueBound Integer
    hi' = case ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange Integer
    x of
               ValueBound Integer
    Unbounded   -> ValueBound Integer
    forall tp. ValueBound tp
    Unbounded
               Inclusive Integer
    z -> Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max (-Integer
    1) (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    z Integer
    lo))

    intDivAux ValueRange Integer
    x Integer
    lo (Inclusive Integer
    hi) = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound Integer
    lo' ValueBound Integer
    hi'
      where
      lo' :: ValueBound Integer
    lo' = case ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange Integer
    x of
               ValueBound Integer
    Unbounded -> ValueBound Integer
    forall tp. ValueBound tp
    Unbounded
               Inclusive Integer
    z -> Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    z Integer
    hi) (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    z Integer
    lo))

      hi' :: ValueBound Integer
    hi' = case ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange Integer
    x of
               ValueBound Integer
    Unbounded   -> ValueBound Integer
    forall tp. ValueBound tp
    Unbounded
               Inclusive Integer
    z -> Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    z Integer
    hi) (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    z Integer
    lo))

    intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    intModRange ValueRange Integer
    _ (SingleRange Integer
    y) | Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound Integer
    forall tp. ValueBound tp
    Unbounded ValueBound Integer
    forall tp. ValueBound tp
    Unbounded
    intModRange (SingleRange Integer
    x) (SingleRange Integer
    y) = Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    SingleRange (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    y)
    intModRange (MultiRange (Inclusive Integer
    lo) (Inclusive Integer
    hi)) (SingleRange Integer
    y)
       | Integer
    hi' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    lo' Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    hi Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    lo = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange (Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive Integer
    lo') (Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive Integer
    hi')
      where
      lo' :: Integer
    lo' = Integer
    lo Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    y
      hi' :: Integer
    hi' = Integer
    hi Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    y
    intModRange ValueRange Integer
    _ ValueRange Integer
    y
      | Inclusive Integer
    lo <- ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange Integer
    yabs, Integer
    lo Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0
      = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange (Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive Integer
    0) (Integer -> Integer
    forall a. Enum a => a -> a
    pred (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange Integer
    yabs)
      | Bool
    otherwise
      = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound Integer
    forall tp. ValueBound tp
    Unbounded ValueBound Integer
    forall tp. ValueBound tp
    Unbounded
     where
     yabs :: ValueRange Integer
    yabs = ValueRange Integer -> ValueRange Integer
    intAbsRange ValueRange Integer
    y

    addRange :: Num tp => ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange :: forall tp.
    Num tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange (SingleRange tp
    x) ValueRange tp
    y = (tp -> tp) -> ValueRange tp -> ValueRange tp
    forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapRange (tp
    xtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +) ValueRange tp
    y
    addRange ValueRange tp
    x (SingleRange tp
    y) = (tp -> tp) -> ValueRange tp -> ValueRange tp
    forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapRange (tp
    ytp -> tp -> tp
    forall a. Num a => a -> a -> a
    +) ValueRange tp
    x
    addRange ValueRange tp
    UnboundedRange ValueRange tp
    _ = ValueRange tp
    forall tp. ValueRange tp
    UnboundedRange
    addRange ValueRange tp
    _ ValueRange tp
    UnboundedRange = ValueRange tp
    forall tp. ValueRange tp
    UnboundedRange
    addRange (MinRange tp
    _) (MaxRange tp
    _) = ValueRange tp
    forall tp. ValueRange tp
    UnboundedRange
    addRange (MaxRange tp
    _) (MinRange tp
    _) = ValueRange tp
    forall tp. ValueRange tp
    UnboundedRange
    addRange (MinRange tp
    lx) (MinRange tp
    ly) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MinRange (tp
    lxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    ly)
    addRange (MaxRange tp
    ux) (MaxRange tp
    uy) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MaxRange (tp
    uxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    uy)
    addRange (MinRange tp
    lx) (IntervalRange tp
    ly tp
    _) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MinRange (tp
    lxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    ly)
    addRange (IntervalRange tp
    lx tp
    _) (MinRange tp
    ly) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MinRange (tp
    lxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    ly)
    addRange (MaxRange tp
    ux) (IntervalRange tp
    _ tp
    uy) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MaxRange (tp
    uxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    uy)
    addRange (IntervalRange tp
    _ tp
    ux) (MaxRange tp
    uy) = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    MaxRange (tp
    uxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    uy)
    addRange (IntervalRange tp
    lx tp
    ux) (IntervalRange tp
    ly tp
    uy) = tp -> tp -> ValueRange tp
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange (tp
    lxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    ly) (tp
    uxtp -> tp -> tp
    forall a. Num a => a -> a -> a
    +tp
    uy)

    -- | Return 'Just True if the range only contains an integer, 'Just False' if it
    -- contains no integers, and 'Nothing' if the range contains both integers and
    -- non-integers.
    rangeIsInteger :: ValueRange Rational -> Maybe Bool
    rangeIsInteger :: ValueRange Rational -> Maybe Bool
    rangeIsInteger (SingleRange Rational
    x) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1)
    rangeIsInteger (MultiRange (Inclusive Rational
    l) (Inclusive Rational
    u))
      | Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    floor Rational
    l Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= (Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    ceiling Rational
    u :: Integer)
      , Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    l Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    1
      , Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    u Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    1 = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    rangeIsInteger ValueRange Rational
    _ = Maybe Bool
    forall a. Maybe a
    Nothing

    -- | Multiply a range by a scalar value
    rangeScalarMul :: (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
    rangeScalarMul :: forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
    rangeScalarMul tp
    x ValueRange tp
    r =
      case tp -> tp -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare tp
    x tp
    0 of
        Ordering
    LT -> (tp -> tp) -> ValueRange tp -> ValueRange tp
    forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapAntiRange (tp
    x tp -> tp -> tp
    forall a. Num a => a -> a -> a
    *) ValueRange tp
    r
        Ordering
    EQ -> tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    SingleRange tp
    0
        Ordering
    GT -> (tp -> tp) -> ValueRange tp -> ValueRange tp
    forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapRange (tp
    x tp -> tp -> tp
    forall a. Num a => a -> a -> a
    *) ValueRange tp
    r

    negateRange :: (Num tp) => ValueRange tp -> ValueRange tp
    negateRange :: forall tp. Num tp => ValueRange tp -> ValueRange tp
    negateRange = (tp -> tp) -> ValueRange tp -> ValueRange tp
    forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapAntiRange tp -> tp
    forall a. Num a => a -> a
    negate

    -- | Multiply two ranges together.
    mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp
    mulRange :: forall tp.
    (Ord tp, Num tp) =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    mulRange (SingleRange tp
    x) ValueRange tp
    y = tp -> ValueRange tp -> ValueRange tp
    forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
    rangeScalarMul tp
    x ValueRange tp
    y
    mulRange ValueRange tp
    x (SingleRange tp
    y) = tp -> ValueRange tp -> ValueRange tp
    forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
    rangeScalarMul tp
    y ValueRange tp
    x
    mulRange (MultiRange ValueBound tp
    lx ValueBound tp
    ux) (MultiRange ValueBound tp
    ly ValueBound tp
    uy) = ValueBound tp -> ValueBound tp -> ValueRange tp
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound tp
    lz ValueBound tp
    uz
      where x_neg :: Bool
    x_neg = ValueBound tp -> Bool
    forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
    lowerBoundIsNegative ValueBound tp
    lx
            x_pos :: Bool
    x_pos = ValueBound tp -> Bool
    forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
    upperBoundIsNonNeg ValueBound tp
    ux
            y_neg :: Bool
    y_neg = ValueBound tp -> Bool
    forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
    lowerBoundIsNegative ValueBound tp
    ly
            y_pos :: Bool
    y_pos = ValueBound tp -> Bool
    forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
    upperBoundIsNonNeg ValueBound tp
    uy
                 -- X can be negative and y can be positive, and also
                 -- x can be positive and y can be negative.
            lz :: ValueBound tp
    lz | Bool
    x_neg Bool -> Bool -> Bool
    && Bool
    y_pos Bool -> Bool -> Bool
    && Bool
    x_pos Bool -> Bool -> Bool
    && Bool
    y_neg =
                   ValueBound tp -> ValueBound tp -> ValueBound tp
    forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    minValueBound (tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    uy)
                                 (tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    ly)
                 -- X can be negative and Y can be positive, but
                 -- either x must be negative (!x_pos) or y cannot be
                 -- negative (!y_neg).
               | Bool
    x_neg Bool -> Bool -> Bool
    && Bool
    y_pos = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    uy
                 -- X can be positive and Y can be negative, but
                 -- either x must be positive (!x_neg) or y cannot be
                 -- positive (!y_pos).
               | Bool
    x_pos Bool -> Bool -> Bool
    && Bool
    y_neg = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    ly
                 -- Both x and y must be negative.
               | Bool
    x_neg = Bool -> ValueBound tp -> ValueBound tp
    forall a. (?callStack::CallStack) => Bool -> a -> a
    assert (Bool -> Bool
    not Bool
    x_pos Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    y_pos) (ValueBound tp -> ValueBound tp) -> ValueBound tp -> ValueBound tp
    forall a b. (a -> b) -> a -> b
    $ tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    uy
                 -- Both x and y must be positive.
               | Bool
    otherwise = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    ly
            uz :: ValueBound tp
    uz | Bool
    x_neg Bool -> Bool -> Bool
    && Bool
    y_neg Bool -> Bool -> Bool
    && Bool
    x_pos Bool -> Bool -> Bool
    && Bool
    y_pos =
                 ValueBound tp -> ValueBound tp -> ValueBound tp
    forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    maxValueBound (tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    ly)
                               (tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    uy)
                 -- Both x and y can be negative, but they both can't be positive.
               | Bool
    x_neg Bool -> Bool -> Bool
    && Bool
    y_neg = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    ly
                 -- Both x and y can be positive, but they both can't be negative.
               | Bool
    x_pos Bool -> Bool -> Bool
    && Bool
    y_pos = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    uy
                 -- x must be positive and y must be negative.
               | Bool
    x_pos = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    uy
                 -- x must be negative and y must be positive.
               | Bool
    otherwise = tp -> tp -> tp
    forall a. Num a => a -> a -> a
    (*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ValueBound tp
    ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
    forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> ValueBound tp
    ly

    -- | Return lower bound of range.
    rangeLowBound :: ValueRange tp -> ValueBound tp
    rangeLowBound :: forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound (SingleRange tp
    x) = tp -> ValueBound tp
    forall a. a -> ValueBound a
    Inclusive tp
    x
    rangeLowBound (MultiRange ValueBound tp
    l ValueBound tp
    _) = ValueBound tp
    l

    -- | Return upper bound of range.
    rangeHiBound :: ValueRange tp -> ValueBound tp
    rangeHiBound :: forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound (SingleRange tp
    x) = tp -> ValueBound tp
    forall a. a -> ValueBound a
    Inclusive tp
    x
    rangeHiBound (MultiRange ValueBound tp
    _ ValueBound tp
    u) = ValueBound tp
    u

    -- | Compute the smallest range containing both ranges.
    joinRange :: Ord tp => ValueRange tp -> ValueRange tp -> ValueRange tp
    joinRange :: forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    joinRange (SingleRange tp
    x) (SingleRange tp
    y)
      | tp
    x tp -> tp -> Bool
    forall a. Eq a => a -> a -> Bool
    == tp
    y = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    SingleRange tp
    x
    joinRange ValueRange tp
    x ValueRange tp
    y = ValueBound tp -> ValueBound tp -> ValueRange tp
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange (ValueBound tp -> ValueBound tp -> ValueBound tp
    forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    minValueBound ValueBound tp
    lx ValueBound tp
    ly) (ValueBound tp -> ValueBound tp -> ValueBound tp
    forall tp.
    Ord tp =>
    ValueBound tp -> ValueBound tp -> ValueBound tp
    maxValueBound ValueBound tp
    ux ValueBound tp
    uy)
      where lx :: ValueBound tp
    lx = ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange tp
    x
            ux :: ValueBound tp
    ux = ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange tp
    x
            ly :: ValueBound tp
    ly = ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange tp
    y
            uy :: ValueBound tp
    uy = ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange tp
    y

    -- | Return true if value ranges overlap.
    rangeOverlap :: Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap :: forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap ValueRange tp
    x ValueRange tp
    y
       -- first range is before second.
      | Inclusive tp
    ux <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange tp
    x
      , Inclusive tp
    ly <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange tp
    y
      , tp
    ux tp -> tp -> Bool
    forall a. Ord a => a -> a -> Bool
    < tp
    ly = Bool
    False

      -- second range is before first.
      | Inclusive tp
    lx <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange tp
    x
      , Inclusive tp
    uy <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange tp
    y
      , tp
    uy tp -> tp -> Bool
    forall a. Ord a => a -> a -> Bool
    < tp
    lx = Bool
    False

      -- Ranges share some elements.
      | Bool
    otherwise = Bool
    True

    -- | Return maybe Boolean if range is equal, is not equal, or indeterminant.
    rangeCheckEq :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckEq :: forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckEq ValueRange tp
    x ValueRange tp
    y
        -- If ranges do not overlap return false.
      | Bool -> Bool
    not (ValueRange tp -> ValueRange tp -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap ValueRange tp
    x ValueRange tp
    y) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
        -- If they are both single values, then result can be determined.
      | Just tp
    cx <- ValueRange tp -> Maybe tp
    forall tp. ValueRange tp -> Maybe tp
    asSingleRange ValueRange tp
    x
      , Just tp
    cy <- ValueRange tp -> Maybe tp
    forall tp. ValueRange tp -> Maybe tp
    asSingleRange ValueRange tp
    y
      = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (tp
    cx tp -> tp -> Bool
    forall a. Eq a => a -> a -> Bool
    == tp
    cy)
        -- Otherwise result is indeterminant.
      | Bool
    otherwise = Maybe Bool
    forall a. Maybe a
    Nothing

    rangeCheckLe :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe :: forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe ValueRange tp
    x ValueRange tp
    y
        -- First range upper bound is below lower bound of second.
      | Inclusive tp
    ux <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange tp
    x
      , Inclusive tp
    ly <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange tp
    y
      , tp
    ux tp -> tp -> Bool
    forall a. Ord a => a -> a -> Bool
    <= tp
    ly = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True

        -- First range lower bound is above upper bound of second.
      | Inclusive tp
    lx <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange tp
    x
      , Inclusive tp
    uy <- ValueRange tp -> ValueBound tp
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange tp
    y
      , tp
    uy tp -> tp -> Bool
    forall a. Ord a => a -> a -> Bool
    <  tp
    lx = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False

      | Bool
    otherwise = Maybe Bool
    forall a. Maybe a
    Nothing

    -- | Defines a unbounded value range.
    unboundedRange :: ValueRange tp
    unboundedRange :: forall tp. ValueRange tp
    unboundedRange = ValueRange tp
    forall tp. ValueRange tp
    UnboundedRange

    -- | Defines a unbounded value range.
    concreteRange :: Eq tp => tp -> tp -> ValueRange tp
    concreteRange :: forall tp. Eq tp => tp -> tp -> ValueRange tp
    concreteRange tp
    x tp
    y
      | tp
    x tp -> tp -> Bool
    forall a. Eq a => a -> a -> Bool
    == tp
    y = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    SingleRange tp
    x
      | Bool
    otherwise = tp -> tp -> ValueRange tp
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange tp
    x tp
    y

    -- | Defines a value range containing a single element.
    singleRange :: tp -> ValueRange tp
    singleRange :: forall tp. tp -> ValueRange tp
    singleRange tp
    v = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    SingleRange tp
    v

    -- | Define a value range with the given bounds
    valueRange :: Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
    valueRange :: forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
    valueRange (Inclusive tp
    x) (Inclusive tp
    y)
      | tp
    x tp -> tp -> Bool
    forall a. Eq a => a -> a -> Bool
    == tp
    y = tp -> ValueRange tp
    forall tp. tp -> ValueRange tp
    SingleRange tp
    x
    valueRange ValueBound tp
    x ValueBound tp
    y = ValueBound tp -> ValueBound tp -> ValueRange tp
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange ValueBound tp
    x ValueBound tp
    y

    -- | Check if range is just a single element.
    asSingleRange :: ValueRange tp -> Maybe tp
    asSingleRange :: forall tp. ValueRange tp -> Maybe tp
    asSingleRange (SingleRange tp
    x) = tp -> Maybe tp
    forall a. a -> Maybe a
    Just tp
    x
    asSingleRange ValueRange tp
    _ = Maybe tp
    forall a. Maybe a
    Nothing

    -- | Map a monotonic function over a range.
    mapRange :: (a -> b) -> ValueRange a -> ValueRange b
    mapRange :: forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapRange a -> b
    f ValueRange a
    r =
      case ValueRange a
    r of
        SingleRange a
    x -> b -> ValueRange b
    forall tp. tp -> ValueRange tp
    SingleRange (a -> b
    f a
    x)
        ValueRange a
    UnboundedRange -> ValueRange b
    forall tp. ValueRange tp
    UnboundedRange
        MinRange a
    l -> b -> ValueRange b
    forall tp. tp -> ValueRange tp
    MinRange (a -> b
    f a
    l)
        MaxRange a
    h -> b -> ValueRange b
    forall tp. tp -> ValueRange tp
    MaxRange (a -> b
    f a
    h)
        IntervalRange a
    l a
    h -> b -> b -> ValueRange b
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange (a -> b
    f a
    l) (a -> b
    f a
    h)

    -- | Map an anti-monotonic function over a range.
    mapAntiRange :: (a -> b) -> ValueRange a -> ValueRange b
    mapAntiRange :: forall a b. (a -> b) -> ValueRange a -> ValueRange b
    mapAntiRange a -> b
    f ValueRange a
    r =
      case ValueRange a
    r of
        SingleRange a
    x -> b -> ValueRange b
    forall tp. tp -> ValueRange tp
    SingleRange (a -> b
    f a
    x)
        ValueRange a
    UnboundedRange -> ValueRange b
    forall tp. ValueRange tp
    UnboundedRange
        MinRange a
    l -> b -> ValueRange b
    forall tp. tp -> ValueRange tp
    MaxRange (a -> b
    f a
    l)
        MaxRange a
    h -> b -> ValueRange b
    forall tp. tp -> ValueRange tp
    MinRange (a -> b
    f a
    h)
        IntervalRange a
    l a
    h -> b -> b -> ValueRange b
    forall tp. tp -> tp -> ValueRange tp
    IntervalRange (a -> b
    f a
    h) (a -> b
    f a
    l)

    ------------------------------------------------------------------------
    -- AbstractValue definition.

    -- Contains range for rational and whether value must be an integer.
    data RealAbstractValue = RAV { RealAbstractValue -> ValueRange Rational
    ravRange :: !(ValueRange Rational)
                                 , RealAbstractValue -> Maybe Bool
    ravIsInteger :: !(Maybe Bool)
                                 }

    ravUnbounded :: RealAbstractValue
    ravUnbounded :: RealAbstractValue
    ravUnbounded = (ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV ValueRange Rational
    forall tp. ValueRange tp
    unboundedRange Maybe Bool
    forall a. Maybe a
    Nothing)

    ravSingle :: Rational -> RealAbstractValue
    ravSingle :: Rational -> RealAbstractValue
    ravSingle Rational
    x = ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV (Rational -> ValueRange Rational
    forall tp. tp -> ValueRange tp
    singleRange Rational
    x) (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
    forall a b. (a -> b) -> a -> b
    $! Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1)

    -- | Range accepting everything between lower and upper bound.
    ravConcreteRange :: Rational -- ^ Lower bound
                     -> Rational -- ^ Upper bound
                     -> RealAbstractValue
    ravConcreteRange :: Rational -> Rational -> RealAbstractValue
    ravConcreteRange Rational
    l Rational
    h = ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV (Rational -> Rational -> ValueRange Rational
    forall tp. Eq tp => tp -> tp -> ValueRange tp
    concreteRange Rational
    l Rational
    h) (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
    forall a b. (a -> b) -> a -> b
    $! Bool
    b)
      where -- Return true if this is a singleton.
            b :: Bool
    b = Rational
    l Rational -> Rational -> Bool
    forall a. Eq a => a -> a -> Bool
    == Rational
    h Bool -> Bool -> Bool
    && Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    l Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1

    -- | Add two real abstract values.
    ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravAdd (RAV ValueRange Rational
    xr Maybe Bool
    xi) (RAV ValueRange Rational
    yr Maybe Bool
    yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV ValueRange Rational
    zr Maybe Bool
    zi
      where zr :: ValueRange Rational
    zr = ValueRange Rational -> ValueRange Rational -> ValueRange Rational
    forall tp.
    Num tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange ValueRange Rational
    xr ValueRange Rational
    yr
            zi :: Maybe Bool
    zi | (Maybe Bool
    xi,Maybe Bool
    yi) (Maybe Bool, Maybe Bool) -> (Maybe Bool, Maybe Bool) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True, Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
               | Bool
    otherwise = ValueRange Rational -> Maybe Bool
    rangeIsInteger ValueRange Rational
    zr

    ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue
    ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue
    ravScalarMul Rational
    x (RAV ValueRange Rational
    yr Maybe Bool
    yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV ValueRange Rational
    zr Maybe Bool
    zi
      where zr :: ValueRange Rational
    zr = Rational -> ValueRange Rational -> ValueRange Rational
    forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
    rangeScalarMul Rational
    x ValueRange Rational
    yr
            zi :: Maybe Bool
    zi | Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1 Bool -> Bool -> Bool
    && Maybe Bool
    yi Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
               | Bool
    otherwise = ValueRange Rational -> Maybe Bool
    rangeIsInteger ValueRange Rational
    zr

    ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravMul (RAV ValueRange Rational
    xr Maybe Bool
    xi) (RAV ValueRange Rational
    yr Maybe Bool
    yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV ValueRange Rational
    zr Maybe Bool
    zi
      where zr :: ValueRange Rational
    zr = ValueRange Rational -> ValueRange Rational -> ValueRange Rational
    forall tp.
    (Ord tp, Num tp) =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    mulRange ValueRange Rational
    xr ValueRange Rational
    yr
            zi :: Maybe Bool
    zi | (Maybe Bool
    xi,Maybe Bool
    yi) (Maybe Bool, Maybe Bool) -> (Maybe Bool, Maybe Bool) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True, Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
               | Bool
    otherwise = ValueRange Rational -> Maybe Bool
    rangeIsInteger ValueRange Rational
    zr

    ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravJoin (RAV ValueRange Rational
    xr Maybe Bool
    xi) (RAV ValueRange Rational
    yr Maybe Bool
    yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
    RAV (ValueRange Rational -> ValueRange Rational -> ValueRange Rational
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    joinRange ValueRange Rational
    xr ValueRange Rational
    yr) Maybe Bool
    zi
      where zi :: Maybe Bool
    zi | Maybe Bool
    xi Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe Bool
    yi = Maybe Bool
    xi
               | Bool
    otherwise = Maybe Bool
    forall a. Maybe a
    Nothing

    ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
    ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
    ravCheckEq (RAV ValueRange Rational
    xr Maybe Bool
    _) (RAV ValueRange Rational
    yr Maybe Bool
    _) = ValueRange Rational -> ValueRange Rational -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckEq ValueRange Rational
    xr ValueRange Rational
    yr

    ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
    ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
    ravCheckLe (RAV ValueRange Rational
    xr Maybe Bool
    _) (RAV ValueRange Rational
    yr Maybe Bool
    _) = ValueRange Rational -> ValueRange Rational -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe ValueRange Rational
    xr ValueRange Rational
    yr

    -- Computing AbstractValue

    absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool
    absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool
    absAnd (Just Bool
    False) Maybe Bool
    _ = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    absAnd (Just Bool
    True) Maybe Bool
    y = Maybe Bool
    y
    absAnd Maybe Bool
    _ (Just Bool
    False) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    absAnd Maybe Bool
    x (Just Bool
    True) = Maybe Bool
    x
    absAnd Maybe Bool
    Nothing Maybe Bool
    Nothing = Maybe Bool
    forall a. Maybe a
    Nothing

    absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool
    absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool
    absOr (Just Bool
    False) Maybe Bool
    y = Maybe Bool
    y
    absOr (Just Bool
    True)  Maybe Bool
    _ = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
    absOr Maybe Bool
    x (Just Bool
    False) = Maybe Bool
    x
    absOr Maybe Bool
    _ (Just Bool
    True)  = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
    absOr Maybe Bool
    Nothing Maybe Bool
    Nothing = Maybe Bool
    forall a. Maybe a
    Nothing

    rangeMax :: Ord a => ValueRange a -> ValueRange a -> ValueRange a
    rangeMax :: forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMax ValueRange a
    x ValueRange a
    y = ValueBound a -> ValueBound a -> ValueRange a
    forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
    valueRange ValueBound a
    lo ValueBound a
    hi
     where
     lo :: ValueBound a
    lo = case (ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange a
    x, ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange a
    y) of
            (ValueBound a
    Unbounded, ValueBound a
    b) -> ValueBound a
    b
            (ValueBound a
    a, ValueBound a
    Unbounded) -> ValueBound a
    a
            (Inclusive a
    a, Inclusive a
    b) -> a -> ValueBound a
    forall a. a -> ValueBound a
    Inclusive (a -> a -> a
    forall a. Ord a => a -> a -> a
    max a
    a a
    b)

     hi :: ValueBound a
    hi = case (ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange a
    x, ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange a
    y) of
             (ValueBound a
    Unbounded, ValueBound a
    _) -> ValueBound a
    forall tp. ValueBound tp
    Unbounded
             (ValueBound a
    _, ValueBound a
    Unbounded) -> ValueBound a
    forall tp. ValueBound tp
    Unbounded
             (Inclusive a
    a, Inclusive a
    b) -> a -> ValueBound a
    forall a. a -> ValueBound a
    Inclusive (a -> a -> a
    forall a. Ord a => a -> a -> a
    max a
    a a
    b)

    rangeMin :: Ord a => ValueRange a -> ValueRange a -> ValueRange a
    rangeMin :: forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMin ValueRange a
    x ValueRange a
    y = ValueBound a -> ValueBound a -> ValueRange a
    forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
    valueRange ValueBound a
    lo ValueBound a
    hi
     where
     lo :: ValueBound a
    lo = case (ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange a
    x, ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeLowBound ValueRange a
    y) of
            (ValueBound a
    Unbounded, ValueBound a
    _) -> ValueBound a
    forall tp. ValueBound tp
    Unbounded
            (ValueBound a
    _, ValueBound a
    Unbounded) -> ValueBound a
    forall tp. ValueBound tp
    Unbounded
            (Inclusive a
    a, Inclusive a
    b) -> a -> ValueBound a
    forall a. a -> ValueBound a
    Inclusive (a -> a -> a
    forall a. Ord a => a -> a -> a
    min a
    a a
    b)

     hi :: ValueBound a
    hi = case (ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange a
    x, ValueRange a -> ValueBound a
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange a
    y) of
             (ValueBound a
    Unbounded, ValueBound a
    b) -> ValueBound a
    b
             (ValueBound a
    a, ValueBound a
    Unbounded) -> ValueBound a
    a
             (Inclusive a
    a, Inclusive a
    b) -> a -> ValueBound a
    forall a. a -> ValueBound a
    Inclusive (a -> a -> a
    forall a. Ord a => a -> a -> a
    min a
    a a
    b)

    ------------------------------------------------------
    -- String abstract domain

    -- | The string abstract domain tracks an interval
    --   range for the length of the string.
    newtype StringAbstractValue =
      StringAbs
      { StringAbstractValue -> ValueRange Integer
    _stringAbsLength :: ValueRange Integer
         -- ^ The length of the string falls in this range
      }

    stringAbsTop :: StringAbstractValue
    stringAbsTop :: StringAbstractValue
    stringAbsTop = ValueRange Integer -> StringAbstractValue
    StringAbs (ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange (Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive Integer
    0) ValueBound Integer
    forall tp. ValueBound tp
    Unbounded)

    stringAbsEmpty :: StringAbstractValue
    stringAbsEmpty :: StringAbstractValue
    stringAbsEmpty = ValueRange Integer -> StringAbstractValue
    StringAbs (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0)

    stringAbsJoin :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
    stringAbsJoin :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
    stringAbsJoin (StringAbs ValueRange Integer
    lenx) (StringAbs ValueRange Integer
    leny) = ValueRange Integer -> StringAbstractValue
    StringAbs (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    joinRange ValueRange Integer
    lenx ValueRange Integer
    leny)

    stringAbsSingle :: StringLiteral si -> StringAbstractValue
    stringAbsSingle :: forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
    stringAbsSingle StringLiteral si
    lit = ValueRange Integer -> StringAbstractValue
    StringAbs (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange (Integer -> Integer
    forall a. Integral a => a -> Integer
    toInteger (StringLiteral si -> Integer
    forall (si :: StringInfo). StringLiteral si -> Integer
    stringLitLength StringLiteral si
    lit)))

    stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool
    stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool
    stringAbsOverlap (StringAbs ValueRange Integer
    lenx) (StringAbs ValueRange Integer
    leny) = ValueRange Integer -> ValueRange Integer -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap ValueRange Integer
    lenx ValueRange Integer
    leny

    stringAbsCheckEq :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsCheckEq :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsCheckEq (StringAbs ValueRange Integer
    lenx) (StringAbs ValueRange Integer
    leny)
      | Just Integer
    0 <- ValueRange Integer -> Maybe Integer
    forall tp. ValueRange tp -> Maybe tp
    asSingleRange ValueRange Integer
    lenx
      , Just Integer
    0 <- ValueRange Integer -> Maybe Integer
    forall tp. ValueRange tp -> Maybe tp
    asSingleRange ValueRange Integer
    leny
      = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True

      | Bool -> Bool
    not (ValueRange Integer -> ValueRange Integer -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap ValueRange Integer
    lenx ValueRange Integer
    leny)
      = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False

      | Bool
    otherwise
      = Maybe Bool
    forall a. Maybe a
    Nothing

    stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
    stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
    stringAbsConcat (StringAbs ValueRange Integer
    lenx) (StringAbs ValueRange Integer
    leny) = ValueRange Integer -> StringAbstractValue
    StringAbs (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Num tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange ValueRange Integer
    lenx ValueRange Integer
    leny)

    stringAbsSubstring :: StringAbstractValue -> ValueRange Integer -> ValueRange Integer -> StringAbstractValue
    stringAbsSubstring :: StringAbstractValue
    -> ValueRange Integer -> ValueRange Integer -> StringAbstractValue
    stringAbsSubstring (StringAbs ValueRange Integer
    s) ValueRange Integer
    off ValueRange Integer
    len
      -- empty string if len is negative
      | Just Bool
    False <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) ValueRange Integer
    len = ValueRange Integer -> StringAbstractValue
    StringAbs (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0)
      -- empty string if off is negative
      | Just Bool
    False <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) ValueRange Integer
    off = ValueRange Integer -> StringAbstractValue
    StringAbs (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0)
      -- empty string if off is out of bounds
      | Just Bool
    True <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe ValueRange Integer
    s ValueRange Integer
    off = ValueRange Integer -> StringAbstractValue
    StringAbs (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0)

      | Bool
    otherwise =
          let -- clamp off at 0
              off' :: ValueRange Integer
    off' = ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMax (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) ValueRange Integer
    off
              -- clamp len at 0
              len' :: ValueRange Integer
    len' = ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMax (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) ValueRange Integer
    len
              -- subtract off' from the length of s, clamp to 0
              s' :: ValueRange Integer
    s'   = ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMax (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Num tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange ValueRange Integer
    s (ValueRange Integer -> ValueRange Integer
    forall tp. Num tp => ValueRange tp -> ValueRange tp
    negateRange ValueRange Integer
    off'))
              -- result is the minimum of the length requested and the length
              -- of the string after removing the prefix
           in ValueRange Integer -> StringAbstractValue
    StringAbs (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMin ValueRange Integer
    len' ValueRange Integer
    s')

    stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsContains = StringAbstractValue -> StringAbstractValue -> Maybe Bool
    couldContain

    stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsIsPrefixOf = (StringAbstractValue -> StringAbstractValue -> Maybe Bool)
    -> StringAbstractValue -> StringAbstractValue -> Maybe Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StringAbstractValue -> StringAbstractValue -> Maybe Bool
    couldContain

    stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsIsSuffixOf = (StringAbstractValue -> StringAbstractValue -> Maybe Bool)
    -> StringAbstractValue -> StringAbstractValue -> Maybe Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StringAbstractValue -> StringAbstractValue -> Maybe Bool
    couldContain

    couldContain :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    couldContain :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
    couldContain (StringAbs ValueRange Integer
    lenx) (StringAbs ValueRange Integer
    leny)
      | Just Bool
    False <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe ValueRange Integer
    leny ValueRange Integer
    lenx = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
      | Bool
    otherwise = Maybe Bool
    forall a. Maybe a
    Nothing

    stringAbsIndexOf :: StringAbstractValue -> StringAbstractValue -> ValueRange Integer -> ValueRange Integer
    stringAbsIndexOf :: StringAbstractValue
    -> StringAbstractValue -> ValueRange Integer -> ValueRange Integer
    stringAbsIndexOf (StringAbs ValueRange Integer
    lenx) (StringAbs ValueRange Integer
    leny) ValueRange Integer
    k
      | Just Bool
    False <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) ValueRange Integer
    k = Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    SingleRange (-Integer
    1)
      | Just Bool
    False <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckLe (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Num tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange ValueRange Integer
    leny ValueRange Integer
    k) ValueRange Integer
    lenx = Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    SingleRange (-Integer
    1)
      | Bool
    otherwise = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
    forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
    MultiRange (Integer -> ValueBound Integer
    forall a. a -> ValueBound a
    Inclusive (-Integer
    1)) (ValueRange Integer -> ValueBound Integer
    forall tp. ValueRange tp -> ValueBound tp
    rangeHiBound ValueRange Integer
    rng)

      where
      -- possible values that the final offset could have if the substring exists anywhere
      rng :: ValueRange Integer
    rng = ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    rangeMax (Integer -> ValueRange Integer
    forall tp. tp -> ValueRange tp
    singleRange Integer
    0) (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Num tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    addRange ValueRange Integer
    lenx (ValueRange Integer -> ValueRange Integer
    forall tp. Num tp => ValueRange tp -> ValueRange tp
    negateRange ValueRange Integer
    leny))

    stringAbsLength :: StringAbstractValue -> ValueRange Integer
    stringAbsLength :: StringAbstractValue -> ValueRange Integer
    stringAbsLength (StringAbs ValueRange Integer
    len) = ValueRange Integer
    len

    -- | An abstract value represents a disjoint st of values.
    type family AbstractValue (tp::BaseType) :: Type where
      AbstractValue BaseBoolType = Maybe Bool
      AbstractValue BaseIntegerType = ValueRange Integer
      AbstractValue BaseRealType = RealAbstractValue
      AbstractValue (BaseStringType si) = StringAbstractValue
      AbstractValue (BaseBVType w) = BVDomain w
      AbstractValue (BaseFloatType _) = ()
      AbstractValue BaseComplexType = Complex RealAbstractValue
      AbstractValue (BaseArrayType idx b) = AbstractValue b
      AbstractValue (BaseStructType ctx) = Ctx.Assignment AbstractValueWrapper ctx

    -- | A utility class for values that contain abstract values
    class HasAbsValue f where
      getAbsValue :: f tp -> AbstractValue tp

    newtype AbstractValueWrapper tp
          = AbstractValueWrapper { forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV :: AbstractValue tp }

    type family ConcreteValue (tp::BaseType) :: Type where
      ConcreteValue BaseBoolType = Bool
      ConcreteValue BaseIntegerType = Integer
      ConcreteValue BaseRealType = Rational
      ConcreteValue (BaseStringType si) = StringLiteral si
      ConcreteValue (BaseBVType w) = Integer
      ConcreteValue (BaseFloatType _) = ()
      ConcreteValue BaseComplexType = Complex Rational
      ConcreteValue (BaseArrayType idx b) = ()
      ConcreteValue (BaseStructType ctx) = Ctx.Assignment ConcreteValueWrapper ctx

    newtype ConcreteValueWrapper tp
          = ConcreteValueWrapper { forall (tp :: BaseType).
    ConcreteValueWrapper tp -> ConcreteValue tp
    unwrapCV :: ConcreteValue tp }

    -- | Create an abstract value that contains every concrete value.
    avTop :: BaseTypeRepr tp -> AbstractValue tp
    avTop :: forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
    avTop BaseTypeRepr tp
    tp =
      case BaseTypeRepr tp
    tp of
        BaseTypeRepr tp
    BaseBoolRepr    -> Maybe Bool
    AbstractValue tp
    forall a. Maybe a
    Nothing
        BaseTypeRepr tp
    BaseIntegerRepr -> AbstractValue tp
    ValueRange Integer
    forall tp. ValueRange tp
    unboundedRange
        BaseTypeRepr tp
    BaseRealRepr    -> AbstractValue tp
    RealAbstractValue
    ravUnbounded
        BaseTypeRepr tp
    BaseComplexRepr -> RealAbstractValue
    ravUnbounded RealAbstractValue -> RealAbstractValue -> Complex RealAbstractValue
    forall a. a -> a -> Complex a
    :+ RealAbstractValue
    ravUnbounded
        BaseStringRepr StringInfoRepr si
    _ -> AbstractValue tp
    StringAbstractValue
    stringAbsTop
        BaseBVRepr NatRepr w
    w    -> NatRepr w -> BVDomain w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BVDomain w
    BVD.any NatRepr w
    w
        BaseFloatRepr{} -> ()
        BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _a BaseTypeRepr xs
    b -> BaseTypeRepr xs -> AbstractValue xs
    forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
    avTop BaseTypeRepr xs
    b
        BaseStructRepr Assignment BaseTypeRepr ctx
    flds -> (forall (x :: BaseType). BaseTypeRepr x -> AbstractValueWrapper x)
    -> forall (x :: Ctx BaseType).
       Assignment BaseTypeRepr x -> Assignment AbstractValueWrapper x
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
           (g :: k -> Type).
    FunctorFC t =>
    (forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
    forall (f :: BaseType -> Type) (g :: BaseType -> Type).
    (forall (x :: BaseType). f x -> g x)
    -> forall (x :: Ctx BaseType). Assignment f x -> Assignment g x
    fmapFC (\BaseTypeRepr x
    etp -> AbstractValue x -> AbstractValueWrapper x
    forall (tp :: BaseType).
    AbstractValue tp -> AbstractValueWrapper tp
    AbstractValueWrapper (BaseTypeRepr x -> AbstractValue x
    forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
    avTop BaseTypeRepr x
    etp)) Assignment BaseTypeRepr ctx
    flds

    -- | Create an abstract value that contains the given concrete value.
    avSingle :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
    avSingle :: forall (tp :: BaseType).
    BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
    avSingle BaseTypeRepr tp
    tp =
      case BaseTypeRepr tp
    tp of
        BaseTypeRepr tp
    BaseBoolRepr -> Bool -> Maybe Bool
    ConcreteValue tp -> AbstractValue tp
    forall a. a -> Maybe a
    Just
        BaseTypeRepr tp
    BaseIntegerRepr -> Integer -> ValueRange Integer
    ConcreteValue tp -> AbstractValue tp
    forall tp. tp -> ValueRange tp
    singleRange
        BaseTypeRepr tp
    BaseRealRepr -> Rational -> RealAbstractValue
    ConcreteValue tp -> AbstractValue tp
    ravSingle
        BaseStringRepr StringInfoRepr si
    _ -> StringLiteral si -> StringAbstractValue
    ConcreteValue tp -> AbstractValue tp
    forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
    stringAbsSingle
        BaseTypeRepr tp
    BaseComplexRepr -> (Rational -> RealAbstractValue)
    -> Complex Rational -> Complex RealAbstractValue
    forall a b. (a -> b) -> Complex a -> Complex b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Rational -> RealAbstractValue
    ravSingle
        BaseBVRepr NatRepr w
    w -> NatRepr w -> Integer -> BVDomain w
    forall (w :: Natural).
    (?callStack::CallStack, 1 <= w) =>
    NatRepr w -> Integer -> BVDomain w
    BVD.singleton NatRepr w
    w
        BaseFloatRepr FloatPrecisionRepr fpp
    _ -> \ConcreteValue tp
    _ -> ()
        BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _a BaseTypeRepr xs
    b -> \ConcreteValue tp
    _ -> BaseTypeRepr xs -> AbstractValue xs
    forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
    avTop BaseTypeRepr xs
    b
        BaseStructRepr Assignment BaseTypeRepr ctx
    flds -> \ConcreteValue tp
    vals ->
          (forall (x :: BaseType).
     BaseTypeRepr x -> ConcreteValueWrapper x -> AbstractValueWrapper x)
    -> Assignment BaseTypeRepr ctx
    -> Assignment ConcreteValueWrapper ctx
    -> Assignment AbstractValueWrapper ctx
    forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
           (a :: Ctx k).
    (forall (x :: k). f x -> g x -> h x)
    -> Assignment f a -> Assignment g a -> Assignment h a
    Ctx.zipWith
            (\BaseTypeRepr x
    ftp ConcreteValueWrapper x
    v -> AbstractValue x -> AbstractValueWrapper x
    forall (tp :: BaseType).
    AbstractValue tp -> AbstractValueWrapper tp
    AbstractValueWrapper (BaseTypeRepr x -> ConcreteValue x -> AbstractValue x
    forall (tp :: BaseType).
    BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
    avSingle BaseTypeRepr x
    ftp (ConcreteValueWrapper x -> ConcreteValue x
    forall (tp :: BaseType).
    ConcreteValueWrapper tp -> ConcreteValue tp
    unwrapCV ConcreteValueWrapper x
    v)))
            Assignment BaseTypeRepr ctx
    flds
            Assignment ConcreteValueWrapper ctx
    ConcreteValue tp
    vals

    ------------------------------------------------------------------------
    -- Abstractable

    class Abstractable (tp::BaseType) where

      -- | Take the union of the two abstract values.
      avJoin     :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp

      -- | Returns true if the abstract values could contain a common concrete
      -- value.
      avOverlap  :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool

      -- | Check equality on two abstract values.  Return true or false if we can definitively
      --   determine the equality of the two elements, and nothing otherwise.
      avCheckEq :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Maybe Bool

    avJoin' :: BaseTypeRepr tp
            -> AbstractValueWrapper tp
            -> AbstractValueWrapper tp
            -> AbstractValueWrapper tp
    avJoin' :: forall (tp :: BaseType).
    BaseTypeRepr tp
    -> AbstractValueWrapper tp
    -> AbstractValueWrapper tp
    -> AbstractValueWrapper tp
    avJoin' BaseTypeRepr tp
    tp AbstractValueWrapper tp
    x AbstractValueWrapper tp
    y = BaseTypeRepr tp
    -> (Abstractable tp => AbstractValueWrapper tp)
    -> AbstractValueWrapper tp
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr tp
    tp ((Abstractable tp => AbstractValueWrapper tp)
     -> AbstractValueWrapper tp)
    -> (Abstractable tp => AbstractValueWrapper tp)
    -> AbstractValueWrapper tp
    forall a b. (a -> b) -> a -> b
    $
      AbstractValue tp -> AbstractValueWrapper tp
    forall (tp :: BaseType).
    AbstractValue tp -> AbstractValueWrapper tp
    AbstractValueWrapper (AbstractValue tp -> AbstractValueWrapper tp)
    -> AbstractValue tp -> AbstractValueWrapper tp
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
    avJoin BaseTypeRepr tp
    tp (AbstractValueWrapper tp -> AbstractValue tp
    forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV AbstractValueWrapper tp
    x) (AbstractValueWrapper tp -> AbstractValue tp
    forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV AbstractValueWrapper tp
    y)

    -- Abstraction captures whether Boolean is constant true or false or Nothing
    instance Abstractable BaseBoolType where
      avJoin :: BaseTypeRepr 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    avJoin BaseTypeRepr 'BaseBoolType
    _ AbstractValue 'BaseBoolType
    x AbstractValue 'BaseBoolType
    y | Maybe Bool
    AbstractValue 'BaseBoolType
    x Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe Bool
    AbstractValue 'BaseBoolType
    y = AbstractValue 'BaseBoolType
    x
                   | Bool
    otherwise = Maybe Bool
    AbstractValue 'BaseBoolType
    forall a. Maybe a
    Nothing

      avOverlap :: BaseTypeRepr 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    -> Bool
    avOverlap BaseTypeRepr 'BaseBoolType
    _ (Just Bool
    x) (Just Bool
    y) | Bool
    x Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Bool
    y = Bool
    False
      avOverlap BaseTypeRepr 'BaseBoolType
    _ AbstractValue 'BaseBoolType
    _ AbstractValue 'BaseBoolType
    _ = Bool
    True

      avCheckEq :: BaseTypeRepr 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    -> AbstractValue 'BaseBoolType
    -> Maybe Bool
    avCheckEq BaseTypeRepr 'BaseBoolType
    _ (Just Bool
    x) (Just Bool
    y) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (Bool
    x Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    y)
      avCheckEq BaseTypeRepr 'BaseBoolType
    _ AbstractValue 'BaseBoolType
    _ AbstractValue 'BaseBoolType
    _ = Maybe Bool
    forall a. Maybe a
    Nothing

    instance Abstractable (BaseStringType si) where
      avJoin :: BaseTypeRepr (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    avJoin BaseTypeRepr (BaseStringType si)
    _     = AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    StringAbstractValue -> StringAbstractValue -> StringAbstractValue
    stringAbsJoin
      avOverlap :: BaseTypeRepr (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> Bool
    avOverlap BaseTypeRepr (BaseStringType si)
    _  = AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si) -> Bool
    StringAbstractValue -> StringAbstractValue -> Bool
    stringAbsOverlap
      avCheckEq :: BaseTypeRepr (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si)
    -> Maybe Bool
    avCheckEq BaseTypeRepr (BaseStringType si)
    _  = AbstractValue (BaseStringType si)
    -> AbstractValue (BaseStringType si) -> Maybe Bool
    StringAbstractValue -> StringAbstractValue -> Maybe Bool
    stringAbsCheckEq

    -- Integers have a lower and upper bound associated with them.
    instance Abstractable BaseIntegerType where
      avJoin :: BaseTypeRepr 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    avJoin BaseTypeRepr 'BaseIntegerType
    _ = AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType -> AbstractValue 'BaseIntegerType
    ValueRange Integer -> ValueRange Integer -> ValueRange Integer
    forall tp.
    Ord tp =>
    ValueRange tp -> ValueRange tp -> ValueRange tp
    joinRange
      avOverlap :: BaseTypeRepr 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    -> Bool
    avOverlap BaseTypeRepr 'BaseIntegerType
    _ = AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType -> Bool
    ValueRange Integer -> ValueRange Integer -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap
      avCheckEq :: BaseTypeRepr 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType
    -> Maybe Bool
    avCheckEq BaseTypeRepr 'BaseIntegerType
    _ = AbstractValue 'BaseIntegerType
    -> AbstractValue 'BaseIntegerType -> Maybe Bool
    ValueRange Integer -> ValueRange Integer -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckEq

    -- Real numbers  have a lower and upper bound associated with them.
    instance Abstractable BaseRealType where
      avJoin :: BaseTypeRepr 'BaseRealType
    -> AbstractValue 'BaseRealType
    -> AbstractValue 'BaseRealType
    -> AbstractValue 'BaseRealType
    avJoin BaseTypeRepr 'BaseRealType
    _ = AbstractValue 'BaseRealType
    -> AbstractValue 'BaseRealType -> AbstractValue 'BaseRealType
    RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravJoin
      avOverlap :: BaseTypeRepr 'BaseRealType
    -> AbstractValue 'BaseRealType
    -> AbstractValue 'BaseRealType
    -> Bool
    avOverlap BaseTypeRepr 'BaseRealType
    _ AbstractValue 'BaseRealType
    x AbstractValue 'BaseRealType
    y = ValueRange Rational -> ValueRange Rational -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap (RealAbstractValue -> ValueRange Rational
    ravRange AbstractValue 'BaseRealType
    RealAbstractValue
    x) (RealAbstractValue -> ValueRange Rational
    ravRange AbstractValue 'BaseRealType
    RealAbstractValue
    y)
      avCheckEq :: BaseTypeRepr 'BaseRealType
    -> AbstractValue 'BaseRealType
    -> AbstractValue 'BaseRealType
    -> Maybe Bool
    avCheckEq BaseTypeRepr 'BaseRealType
    _ = AbstractValue 'BaseRealType
    -> AbstractValue 'BaseRealType -> Maybe Bool
    RealAbstractValue -> RealAbstractValue -> Maybe Bool
    ravCheckEq

    -- Bitvectors always have a lower and upper bound (represented as unsigned numbers)
    instance (1 <= w) => Abstractable (BaseBVType w) where
      avJoin :: BaseTypeRepr (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    avJoin (BaseBVRepr NatRepr w
    _) = BVDomain w -> BVDomain w -> BVDomain w
    AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w) -> AbstractValue (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    BVDomain w -> BVDomain w -> BVDomain w
    BVD.union
      avOverlap :: BaseTypeRepr (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    -> Bool
    avOverlap BaseTypeRepr (BaseBVType w)
    _ = BVDomain w -> BVDomain w -> Bool
    AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w) -> Bool
    forall (w :: Natural). BVDomain w -> BVDomain w -> Bool
    BVD.domainsOverlap
      avCheckEq :: BaseTypeRepr (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w)
    -> Maybe Bool
    avCheckEq BaseTypeRepr (BaseBVType w)
    _ = BVDomain w -> BVDomain w -> Maybe Bool
    AbstractValue (BaseBVType w)
    -> AbstractValue (BaseBVType w) -> Maybe Bool
    forall (w :: Natural). BVDomain w -> BVDomain w -> Maybe Bool
    BVD.eq

    instance Abstractable (BaseFloatType fpp) where
      avJoin :: BaseTypeRepr (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    avJoin BaseTypeRepr (BaseFloatType fpp)
    _ AbstractValue (BaseFloatType fpp)
    _ AbstractValue (BaseFloatType fpp)
    _ = ()
      avOverlap :: BaseTypeRepr (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    -> Bool
    avOverlap BaseTypeRepr (BaseFloatType fpp)
    _ AbstractValue (BaseFloatType fpp)
    _ AbstractValue (BaseFloatType fpp)
    _ = Bool
    True
      avCheckEq :: BaseTypeRepr (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    -> AbstractValue (BaseFloatType fpp)
    -> Maybe Bool
    avCheckEq BaseTypeRepr (BaseFloatType fpp)
    _ AbstractValue (BaseFloatType fpp)
    _ AbstractValue (BaseFloatType fpp)
    _ = Maybe Bool
    forall a. Maybe a
    Nothing

    instance Abstractable BaseComplexType where
      avJoin :: BaseTypeRepr 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    avJoin BaseTypeRepr 'BaseComplexType
    _ (RealAbstractValue
    r1 :+ RealAbstractValue
    i1) (RealAbstractValue
    r2 :+ RealAbstractValue
    i2) = (RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravJoin RealAbstractValue
    r1 RealAbstractValue
    r2) RealAbstractValue -> RealAbstractValue -> Complex RealAbstractValue
    forall a. a -> a -> Complex a
    :+ (RealAbstractValue -> RealAbstractValue -> RealAbstractValue
    ravJoin RealAbstractValue
    i1 RealAbstractValue
    i2)
      avOverlap :: BaseTypeRepr 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    -> Bool
    avOverlap BaseTypeRepr 'BaseComplexType
    _ (RealAbstractValue
    r1 :+ RealAbstractValue
    i1) (RealAbstractValue
    r2 :+ RealAbstractValue
    i2) = ValueRange Rational -> ValueRange Rational -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    r1) (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    r2)
                                       Bool -> Bool -> Bool
    && ValueRange Rational -> ValueRange Rational -> Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
    rangeOverlap (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    i1) (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    i2)
      avCheckEq :: BaseTypeRepr 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    -> AbstractValue 'BaseComplexType
    -> Maybe Bool
    avCheckEq BaseTypeRepr 'BaseComplexType
    _ (RealAbstractValue
    r1 :+ RealAbstractValue
    i1) (RealAbstractValue
    r2 :+ RealAbstractValue
    i2)
        = Maybe Bool -> Maybe Bool -> Maybe Bool
    combineEqCheck
            (ValueRange Rational -> ValueRange Rational -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckEq (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    r1) (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    r2))
            (ValueRange Rational -> ValueRange Rational -> Maybe Bool
    forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
    rangeCheckEq (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    i1) (RealAbstractValue -> ValueRange Rational
    ravRange RealAbstractValue
    i2))

    instance Abstractable (BaseArrayType idx b) where
      avJoin :: BaseTypeRepr (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    avJoin (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _ BaseTypeRepr xs
    b) AbstractValue (BaseArrayType idx b)
    x AbstractValue (BaseArrayType idx b)
    y = BaseTypeRepr xs
    -> (Abstractable xs => AbstractValue (BaseArrayType idx b))
    -> AbstractValue (BaseArrayType idx b)
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr xs
    b ((Abstractable xs => AbstractValue (BaseArrayType idx b))
     -> AbstractValue (BaseArrayType idx b))
    -> (Abstractable xs => AbstractValue (BaseArrayType idx b))
    -> AbstractValue (BaseArrayType idx b)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr xs
    -> AbstractValue xs -> AbstractValue xs -> AbstractValue xs
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
    avJoin BaseTypeRepr xs
    b AbstractValue xs
    AbstractValue (BaseArrayType idx b)
    x AbstractValue xs
    AbstractValue (BaseArrayType idx b)
    y
      avOverlap :: BaseTypeRepr (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    -> Bool
    avOverlap (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _ BaseTypeRepr xs
    b) AbstractValue (BaseArrayType idx b)
    x AbstractValue (BaseArrayType idx b)
    y = BaseTypeRepr xs -> (Abstractable xs => Bool) -> Bool
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr xs
    b ((Abstractable xs => Bool) -> Bool)
    -> (Abstractable xs => Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr xs -> AbstractValue xs -> AbstractValue xs -> Bool
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
    avOverlap BaseTypeRepr xs
    b AbstractValue xs
    AbstractValue (BaseArrayType idx b)
    x AbstractValue xs
    AbstractValue (BaseArrayType idx b)
    y
      avCheckEq :: BaseTypeRepr (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    -> AbstractValue (BaseArrayType idx b)
    -> Maybe Bool
    avCheckEq (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _ BaseTypeRepr xs
    b) AbstractValue (BaseArrayType idx b)
    x AbstractValue (BaseArrayType idx b)
    y = BaseTypeRepr xs -> (Abstractable xs => Maybe Bool) -> Maybe Bool
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr xs
    b ((Abstractable xs => Maybe Bool) -> Maybe Bool)
    -> (Abstractable xs => Maybe Bool) -> Maybe Bool
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr xs
    -> AbstractValue xs -> AbstractValue xs -> Maybe Bool
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> Maybe Bool
    avCheckEq BaseTypeRepr xs
    b AbstractValue xs
    AbstractValue (BaseArrayType idx b)
    x AbstractValue xs
    AbstractValue (BaseArrayType idx b)
    y

    combineEqCheck :: Maybe Bool -> Maybe Bool -> Maybe Bool
    combineEqCheck :: Maybe Bool -> Maybe Bool -> Maybe Bool
    combineEqCheck (Just Bool
    False) Maybe Bool
    _ = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    combineEqCheck (Just Bool
    True)  Maybe Bool
    y = Maybe Bool
    y
    combineEqCheck Maybe Bool
    _ (Just Bool
    False) = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
    combineEqCheck Maybe Bool
    x (Just Bool
    True)  = Maybe Bool
    x
    combineEqCheck Maybe Bool
    _ Maybe Bool
    _            = Maybe Bool
    forall a. Maybe a
    Nothing

    instance Abstractable (BaseStructType ctx) where
      avJoin :: BaseTypeRepr (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    avJoin (BaseStructRepr Assignment BaseTypeRepr ctx
    flds) AbstractValue (BaseStructType ctx)
    x AbstractValue (BaseStructType ctx)
    y = (forall (tp :: BaseType).
     BaseTypeRepr tp
     -> AbstractValueWrapper tp
     -> AbstractValueWrapper tp
     -> AbstractValueWrapper tp)
    -> Assignment BaseTypeRepr ctx
    -> Assignment AbstractValueWrapper ctx
    -> Assignment AbstractValueWrapper ctx
    -> Assignment AbstractValueWrapper ctx
    forall k (a :: k -> Type) (b :: k -> Type) (c :: k -> Type)
           (d :: k -> Type) (ctx :: Ctx k).
    (forall (x :: k). a x -> b x -> c x -> d x)
    -> Assignment a ctx
    -> Assignment b ctx
    -> Assignment c ctx
    -> Assignment d ctx
    ctxZipWith3 BaseTypeRepr x
    -> AbstractValueWrapper x
    -> AbstractValueWrapper x
    -> AbstractValueWrapper x
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> AbstractValueWrapper tp
    -> AbstractValueWrapper tp
    -> AbstractValueWrapper tp
    avJoin' Assignment BaseTypeRepr ctx
    flds Assignment AbstractValueWrapper ctx
    AbstractValue (BaseStructType ctx)
    x Assignment AbstractValueWrapper ctx
    AbstractValue (BaseStructType ctx)
    y
      avOverlap :: BaseTypeRepr (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    -> Bool
    avOverlap (BaseStructRepr Assignment BaseTypeRepr ctx
    flds) AbstractValue (BaseStructType ctx)
    x AbstractValue (BaseStructType ctx)
    y = Size ctx
    -> (forall (tp :: BaseType). Bool -> Index ctx tp -> Bool)
    -> Bool
    -> Bool
    forall {k} (ctx :: Ctx k) r.
    Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
    Ctx.forIndex (Assignment BaseTypeRepr ctx -> Size ctx
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    Ctx.size Assignment BaseTypeRepr ctx
    flds) Bool -> Index ctx tp -> Bool
    Bool -> Index ctx tp -> Bool
    forall (tp :: BaseType). Bool -> Index ctx tp -> Bool
    forall (tp :: BaseType). Bool -> Index ctx tp -> Bool
    f Bool
    True
        where f :: Bool -> Ctx.Index ctx tp -> Bool
              f :: forall (tp :: BaseType). Bool -> Index ctx tp -> Bool
    f Bool
    b Index ctx tp
    i = BaseTypeRepr tp -> (Abstractable tp => Bool) -> Bool
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr tp
    tp (BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
    avOverlap BaseTypeRepr tp
    tp (AbstractValueWrapper tp -> AbstractValue tp
    forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV AbstractValueWrapper tp
    u) (AbstractValueWrapper tp -> AbstractValue tp
    forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV AbstractValueWrapper tp
    v)) Bool -> Bool -> Bool
    && Bool
    b
                where tp :: BaseTypeRepr tp
    tp = Assignment BaseTypeRepr ctx
    flds Assignment BaseTypeRepr ctx -> Index ctx tp -> BaseTypeRepr tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    Index ctx tp
    i
                      u :: AbstractValueWrapper tp
    u  = Assignment AbstractValueWrapper ctx
    AbstractValue (BaseStructType ctx)
    x Assignment AbstractValueWrapper ctx
    -> Index ctx tp -> AbstractValueWrapper tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i
                      v :: AbstractValueWrapper tp
    v  = Assignment AbstractValueWrapper ctx
    AbstractValue (BaseStructType ctx)
    y Assignment AbstractValueWrapper ctx
    -> Index ctx tp -> AbstractValueWrapper tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i

      avCheckEq :: BaseTypeRepr (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    -> AbstractValue (BaseStructType ctx)
    -> Maybe Bool
    avCheckEq (BaseStructRepr Assignment BaseTypeRepr ctx
    flds) AbstractValue (BaseStructType ctx)
    x AbstractValue (BaseStructType ctx)
    y = Size ctx
    -> (forall (tp :: BaseType).
        Maybe Bool -> Index ctx tp -> Maybe Bool)
    -> Maybe Bool
    -> Maybe Bool
    forall {k} (ctx :: Ctx k) r.
    Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
    Ctx.forIndex (Assignment BaseTypeRepr ctx -> Size ctx
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    Ctx.size Assignment BaseTypeRepr ctx
    flds) Maybe Bool -> Index ctx tp -> Maybe Bool
    Maybe Bool -> Index ctx tp -> Maybe Bool
    forall (tp :: BaseType). Maybe Bool -> Index ctx tp -> Maybe Bool
    forall (tp :: BaseType). Maybe Bool -> Index ctx tp -> Maybe Bool
    f (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True)
        where f :: Maybe Bool -> Ctx.Index ctx tp -> Maybe Bool
              f :: forall (tp :: BaseType). Maybe Bool -> Index ctx tp -> Maybe Bool
    f Maybe Bool
    b Index ctx tp
    i = Maybe Bool -> Maybe Bool -> Maybe Bool
    combineEqCheck Maybe Bool
    b (BaseTypeRepr tp -> (Abstractable tp => Maybe Bool) -> Maybe Bool
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr tp
    tp (BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> Maybe Bool
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp
    -> AbstractValue tp -> AbstractValue tp -> Maybe Bool
    avCheckEq BaseTypeRepr tp
    tp (AbstractValueWrapper tp -> AbstractValue tp
    forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV AbstractValueWrapper tp
    u) (AbstractValueWrapper tp -> AbstractValue tp
    forall (tp :: BaseType).
    AbstractValueWrapper tp -> AbstractValue tp
    unwrapAV AbstractValueWrapper tp
    v)))
                where tp :: BaseTypeRepr tp
    tp = Assignment BaseTypeRepr ctx
    flds Assignment BaseTypeRepr ctx -> Index ctx tp -> BaseTypeRepr tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    Index ctx tp
    i
                      u :: AbstractValueWrapper tp
    u  = Assignment AbstractValueWrapper ctx
    AbstractValue (BaseStructType ctx)
    x Assignment AbstractValueWrapper ctx
    -> Index ctx tp -> AbstractValueWrapper tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i
                      v :: AbstractValueWrapper tp
    v  = Assignment AbstractValueWrapper ctx
    AbstractValue (BaseStructType ctx)
    y Assignment AbstractValueWrapper ctx
    -> Index ctx tp -> AbstractValueWrapper tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i

    withAbstractable
       :: BaseTypeRepr bt
       -> (Abstractable bt => a)
       -> a
    withAbstractable :: forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr bt
    bt Abstractable bt => a
    k =
      case BaseTypeRepr bt
    bt of
        BaseTypeRepr bt
    BaseBoolRepr -> a
    Abstractable bt => a
    k
        BaseBVRepr NatRepr w
    _w -> a
    Abstractable bt => a
    k
        BaseTypeRepr bt
    BaseIntegerRepr -> a
    Abstractable bt => a
    k
        BaseStringRepr StringInfoRepr si
    _ -> a
    Abstractable bt => a
    k
        BaseTypeRepr bt
    BaseRealRepr -> a
    Abstractable bt => a
    k
        BaseTypeRepr bt
    BaseComplexRepr -> a
    Abstractable bt => a
    k
        BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _a BaseTypeRepr xs
    _b -> a
    Abstractable bt => a
    k
        BaseStructRepr Assignment BaseTypeRepr ctx
    _flds -> a
    Abstractable bt => a
    k
        BaseFloatRepr FloatPrecisionRepr fpp
    _fpp -> a
    Abstractable bt => a
    k

    -- | Returns true if the concrete value is a member of the set represented
    -- by the abstract value.
    avContains :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool
    avContains :: forall (tp :: BaseType).
    BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool
    avContains BaseTypeRepr tp
    tp = BaseTypeRepr tp
    -> (Abstractable tp =>
        ConcreteValue tp -> AbstractValue tp -> Bool)
    -> ConcreteValue tp
    -> AbstractValue tp
    -> Bool
    forall (bt :: BaseType) a.
    BaseTypeRepr bt -> (Abstractable bt => a) -> a
    withAbstractable BaseTypeRepr tp
    tp ((Abstractable tp => ConcreteValue tp -> AbstractValue tp -> Bool)
     -> ConcreteValue tp -> AbstractValue tp -> Bool)
    -> (Abstractable tp =>
        ConcreteValue tp -> AbstractValue tp -> Bool)
    -> ConcreteValue tp
    -> AbstractValue tp
    -> Bool
    forall a b. (a -> b) -> a -> b
    $ \ConcreteValue tp
    x AbstractValue tp
    y -> BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
    forall (tp :: BaseType).
    Abstractable tp =>
    BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
    avOverlap BaseTypeRepr tp
    tp (BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
    forall (tp :: BaseType).
    BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
    avSingle BaseTypeRepr tp
    tp ConcreteValue tp
    x) AbstractValue tp
    y