    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE TypeOperators #-}

    module What4.IndexLit where

    import qualified Data.BitVector.Sized as BV
    import Data.Parameterized.Classes

    import What4.BaseTypes

    ------------------------------------------------------------------------
    -- IndexLit

    -- | This represents a concrete index value, and is used for creating
    -- arrays.
    data IndexLit idx where
      IntIndexLit :: !Integer -> IndexLit BaseIntegerType
      BVIndexLit :: (1 <= w) => !(NatRepr w) -> !(BV.BV w) ->  IndexLit (BaseBVType w)

    instance Eq (IndexLit tp) where
      IndexLit tp
    x == :: IndexLit tp -> IndexLit tp -> Bool
    == IndexLit tp
    y = Maybe (tp :~: tp) -> Bool
    forall a. Maybe a -> Bool
    isJust (IndexLit tp -> IndexLit tp -> Maybe (tp :~: tp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    IndexLit a -> IndexLit b -> Maybe (a :~: b)
    testEquality IndexLit tp
    x IndexLit tp
    y)

    instance TestEquality IndexLit where
      testEquality :: forall (a :: BaseType) (b :: BaseType).
    IndexLit a -> IndexLit b -> Maybe (a :~: b)
    testEquality (IntIndexLit Integer
    x) (IntIndexLit Integer
    y) =
        if Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    y then
         (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
         else
         Maybe (a :~: b)
    forall a. Maybe a
    Nothing
      testEquality (BVIndexLit NatRepr w
    wx BV w
    x) (BVIndexLit NatRepr w
    wy BV w
    y) = do
        Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
    forall (a :: Natural) (b :: Natural).
    NatRepr a -> NatRepr b -> Maybe (a :~: b)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality NatRepr w
    wx NatRepr w
    wy
        if x == y then Just Refl else Nothing
      testEquality IndexLit a
    _ IndexLit b
    _ =
        Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance OrdF IndexLit where
      compareF :: forall (x :: BaseType) (y :: BaseType).
    IndexLit x -> IndexLit y -> OrderingF x y
    compareF (IntIndexLit Integer
    x) (IntIndexLit Integer
    y) = Ordering -> OrderingF x x
    forall {k} (x :: k). Ordering -> OrderingF x x
    fromOrdering (Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    x Integer
    y)
      compareF IntIndexLit{} IndexLit y
    _ = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
      compareF IndexLit x
    _ IntIndexLit{} = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
      compareF (BVIndexLit NatRepr w
    wx BV w
    x) (BVIndexLit NatRepr w
    wy BV w
    y) =
        case NatRepr w -> NatRepr w -> OrderingF w w
    forall (x :: Natural) (y :: Natural).
    NatRepr x -> NatRepr y -> OrderingF x y
    forall k (ktp :: k -> Type) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF NatRepr w
    wx NatRepr w
    wy of
          OrderingF w w
    LTF -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
          OrderingF w w
    GTF -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
          OrderingF w w
    EQF -> Ordering -> OrderingF x x
    forall {k} (x :: k). Ordering -> OrderingF x x
    fromOrdering (BV w -> BV w -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare BV w
    x BV w
    BV w
    y)

    instance Hashable (IndexLit tp) where
      hashWithSalt :: Int -> IndexLit tp -> Int
    hashWithSalt = Int -> IndexLit tp -> Int
    forall (tp :: BaseType). Int -> IndexLit tp -> Int
    hashIndexLit
      {-# INLINE hashWithSalt #-}

    hashIndexLit :: Int -> IndexLit idx -> Int
    Int
    s hashIndexLit :: forall (tp :: BaseType). Int -> IndexLit tp -> Int
    `hashIndexLit` (IntIndexLit Integer
    i) =
        Int
    s Int -> Int -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` (Int
    0::Int)
          Int -> Integer -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` Integer
    i
    Int
    s `hashIndexLit` (BVIndexLit NatRepr w
    w BV w
    i) =
        Int
    s Int -> Int -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` (Int
    1::Int)
          Int -> NatRepr w -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` NatRepr w
    w
          Int -> BV w -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` BV w
    i

    instance HashableF IndexLit where
      hashWithSaltF :: forall (tp :: BaseType). Int -> IndexLit tp -> Int
    hashWithSaltF = Int -> IndexLit tp -> Int
    forall (tp :: BaseType). Int -> IndexLit tp -> Int
    hashIndexLit

    instance Show (IndexLit tp) where
      showsPrec :: Int -> IndexLit tp -> ShowS
    showsPrec Int
    p (IntIndexLit Integer
    i) String
    s = Int -> Integer -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p Integer
    i String
    s
      showsPrec Int
    p (BVIndexLit NatRepr w
    w BV w
    i) String
    s = Int -> BV w -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p BV w
    i (String
    "::[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> ShowS
    forall a. Show a => a -> ShowS
    shows NatRepr w
    w (Char
    ']' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s))

    instance ShowF IndexLit