{-# 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 = forall a. Maybe a -> Bool
isJust (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 :: forall (a :: BaseType) (b :: BaseType).
IndexLit a -> IndexLit b -> Maybe (a :~: b)
testEquality (IntIndexLit Integer
x) (IntIndexLit Integer
y) =
    if Integer
x forall a. Eq a => a -> a -> Bool
== Integer
y then
     forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
     else
     forall a. Maybe a
Nothing
  testEquality (BVIndexLit NatRepr w
wx BV w
x) (BVIndexLit NatRepr w
wy BV w
y) = do
    w :~: w
Refl <- 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 forall a. Eq a => a -> a -> Bool
== BV w
y then forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl else forall a. Maybe a
Nothing
  testEquality IndexLit a
_ IndexLit 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) = forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y)
  compareF IntIndexLit{} IndexLit y
_ = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF IndexLit x
_ IntIndexLit{} = 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 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 -> forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      OrderingF w w
GTF -> forall {k} (x :: k) (y :: k). OrderingF x y
GTF
      OrderingF w w
EQF -> forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (forall a. Ord a => a -> a -> Ordering
compare BV w
x BV w
y)

instance Hashable (IndexLit tp) where
  hashWithSalt :: Int -> IndexLit tp -> Int
hashWithSalt = 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 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0::Int)
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Integer
i
Int
s `hashIndexLit` (BVIndexLit NatRepr w
w BV w
i) =
    Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1::Int)
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` NatRepr w
w
      forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BV w
i

instance HashableF IndexLit where
  hashWithSaltF :: forall (tp :: BaseType). Int -> IndexLit tp -> Int
hashWithSaltF = 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 = 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 = forall a. Show a => Int -> a -> ShowS
showsPrec Int
p BV w
i (String
"::[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ShowS
shows NatRepr w
w (Char
']' forall a. a -> [a] -> [a]
: String
s))

instance ShowF IndexLit