{-# 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)
testEquality IndexLit tp
x IndexLit tp
y)

instance TestEquality IndexLit where
  testEquality :: 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 :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
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
    w :~: w
Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
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 BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
BV w
y then (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality IndexLit a
_ IndexLit b
_ =
    Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF IndexLit where
  compareF :: 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 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 :: Int -> IndexLit idx -> 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 :: 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