{-# Language GADTs, DataKinds, TypeOperators #-}
{-# Language ScopedTypeVariables #-}
{-# Language Rank2Types #-}
module Lang.Crucible.Vector
  ( module Data.Parameterized.Vector

    -- ** Bit-vectors
  , fromBV
  , toBV
  , joinVecBV
  , splitVecBV

  ) where

import Prelude hiding (length,zipWith)

import Data.Coerce
import Data.Proxy

import Data.Parameterized.NatRepr
import Data.Parameterized.Vector
import Data.Parameterized.Utils.Endian

import Lang.Crucible.Types
import Lang.Crucible.Syntax (IsExpr(..))
import Lang.Crucible.CFG.Expr ( App( BVConcat, BVSelect ) )

{- | Join the bit-vectors in a vector into a single large bit-vector.
The "Endian" parameter indicates which way to join the elemnts:
"LittleEndian" indicates that low vector indexes are less significant. -}
toBV :: forall f n w.  (1 <= w, IsExpr f) =>
  Endian ->
  NatRepr w ->
  Vector n (f (BVType w)) -> f (BVType (n * w))
toBV :: forall (f :: CrucibleType -> Type) (n :: Natural) (w :: Natural).
(1 <= w, IsExpr f) =>
Endian
-> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w))
toBV Endian
endian NatRepr w
w Vector n (f (BVType w))
xs = f (BVType (n * w))
ys
  where
  xs' :: Vector n (Bits f w)
xs' = Vector n (f (BVType w)) -> Vector n (Bits f w)
forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec Vector n (f (BVType w))
xs

  jn :: (1 <= b) => NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
  jn :: forall (b :: Natural).
(1 <= b) =>
NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
jn  = case Endian
endian of
          Endian
LittleEndian -> NatRepr w -> NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnLittle NatRepr w
w
          Endian
BigEndian    -> NatRepr w -> NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnBig NatRepr w
w

  Bits f (BVType (n * w))
ys = (forall (b :: Natural).
 (1 <= b) =>
 NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b))
-> NatRepr w -> Vector n (Bits f w) -> Bits f (n * w)
forall (f :: Natural -> Type) (n :: Natural) (w :: Natural).
(1 <= w) =>
(forall (l :: Natural).
 (1 <= l) =>
 NatRepr l -> f w -> f l -> f (w + l))
-> NatRepr w -> Vector n (f w) -> f (n * w)
joinWith NatRepr l -> Bits f w -> Bits f l -> Bits f (w + l)
forall (b :: Natural).
(1 <= b) =>
NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
jn NatRepr w
w Vector n (Bits f w)
xs'
{-# Inline toBV #-}

coerceVec :: Coercible a b => Vector n a -> Vector n b
coerceVec :: forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec = Vector n a -> Vector n b
forall a b. Coercible a b => a -> b
coerce

newtype Bits f n = Bits (f (BVType n))


-- | Earlier indexes are more signficant.
jnBig :: (IsExpr f, 1 <= a, 1 <= b) =>
         NatRepr a -> NatRepr b ->
         Bits f a -> Bits f b -> Bits f (a + b)
jnBig :: forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnBig NatRepr a
la NatRepr b
lb (Bits f (BVType a)
a) (Bits f (BVType b)
b) =
  case LeqProof 1 a -> NatRepr b -> LeqProof 1 (a + b)
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (Proxy 1 -> NatRepr a -> LeqProof 1 a
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1) NatRepr a
la) NatRepr b
lb of { LeqProof 1 (a + b)
LeqProof ->
    f (BVType (a + b)) -> Bits f (a + b)
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits (App (ExprExt f) f (BVType (a + b)) -> f (BVType (a + b))
forall (tp :: CrucibleType). App (ExprExt f) f tp -> f tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (NatRepr a
-> NatRepr b
-> f (BVType a)
-> f (BVType b)
-> App (ExprExt f) f (BVType (a + b))
forall (u :: Natural) (v :: Natural) (f :: CrucibleType -> Type)
       ext.
(1 <= u, 1 <= v, 1 <= (u + v)) =>
NatRepr u
-> NatRepr v
-> f (BVType u)
-> f (BVType v)
-> App ext f ('BaseToType (BaseBVType (u + v)))
BVConcat NatRepr a
la NatRepr b
lb f (BVType a)
a f (BVType b)
b)) }
{-# Inline jnBig #-}

-- | Earlier indexes are less signficant.
jnLittle :: (IsExpr f, 1 <= a, 1 <= b) =>
            NatRepr a -> NatRepr b ->
            Bits f a -> Bits f b -> Bits f (a + b)
jnLittle :: forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnLittle NatRepr a
la NatRepr b
lb (Bits f (BVType a)
a) (Bits f (BVType b)
b) =
  case LeqProof 1 b -> NatRepr a -> LeqProof 1 (b + a)
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (Proxy 1 -> NatRepr b -> LeqProof 1 b
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1) NatRepr b
lb) NatRepr a
la of { LeqProof 1 (b + a)
LeqProof ->
  case NatRepr b -> NatRepr a -> (b + a) :~: (a + b)
forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr b
lb NatRepr a
la                             of { (b + a) :~: (a + b)
Refl     ->
    f (BVType (b + a)) -> Bits f (b + a)
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits (App (ExprExt f) f (BVType (b + a)) -> f (BVType (b + a))
forall (tp :: CrucibleType). App (ExprExt f) f tp -> f tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (NatRepr b
-> NatRepr a
-> f (BVType b)
-> f (BVType a)
-> App (ExprExt f) f (BVType (b + a))
forall (u :: Natural) (v :: Natural) (f :: CrucibleType -> Type)
       ext.
(1 <= u, 1 <= v, 1 <= (u + v)) =>
NatRepr u
-> NatRepr v
-> f (BVType u)
-> f (BVType v)
-> App ext f ('BaseToType (BaseBVType (u + v)))
BVConcat NatRepr b
lb NatRepr a
la f (BVType b)
b f (BVType a)
a)) }}
{-# Inline jnLittle #-}

-- | Split a bit-vector into a vector of bit-vectors.
fromBV :: forall f w n.
  (1 <= w, 1 <= n, IsExpr f) =>
  Endian ->
  NatRepr n -> NatRepr w -> f (BVType (n * w)) -> Vector n (f (BVType w))

fromBV :: forall (f :: CrucibleType -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n, IsExpr f) =>
Endian
-> NatRepr n
-> NatRepr w
-> f (BVType (n * w))
-> Vector n (f (BVType w))
fromBV Endian
e NatRepr n
n NatRepr w
w f (BVType (n * w))
xs = Vector n (Bits f w) -> Vector n (f (BVType w))
forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec (Endian
-> (forall (i :: Natural).
    ((i + w) <= (n * w)) =>
    NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w)
-> NatRepr n
-> NatRepr w
-> Bits f (n * w)
-> Vector n (Bits f w)
forall (f :: Natural -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Natural).
    ((i + w) <= (n * w)) =>
    NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
-> NatRepr n
-> NatRepr w
-> f (n * w)
-> Vector n (f w)
splitWith Endian
e NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
sel NatRepr n
n NatRepr w
w (f (BVType (n * w)) -> Bits f (n * w)
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits f (BVType (n * w))
xs))
  where
  sel :: (i + w <= n * w) =>
          NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
  sel :: forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
sel NatRepr (n * w)
totL NatRepr i
i (Bits f (BVType (n * w))
val) =
    case NatRepr n -> NatRepr w -> LeqProof 1 (n * w)
forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos NatRepr n
n NatRepr w
w of { LeqProof 1 (n * w)
LeqProof ->
      f (BVType w) -> Bits f w
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits (App (ExprExt f) f (BVType w) -> f (BVType w)
forall (tp :: CrucibleType). App (ExprExt f) f tp -> f tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (NatRepr i
-> NatRepr w
-> NatRepr (n * w)
-> f (BVType (n * w))
-> App (ExprExt f) f (BVType w)
forall (w :: Natural) (len :: Natural) (idx :: Natural)
       (f :: CrucibleType -> Type) ext.
(1 <= w, 1 <= len, (idx + len) <= w) =>
NatRepr idx
-> NatRepr len
-> NatRepr w
-> f (BVType w)
-> App ext f ('BaseToType (BaseBVType len))
BVSelect NatRepr i
i NatRepr w
w NatRepr (n * w)
totL f (BVType (n * w))
val)) }
{-# Inline fromBV #-}

-- | Turn a vector of bit-vectors,
-- into a shorter vector of longer bit-vectors.
joinVecBV :: (IsExpr f, 1 <= i, 1 <= w, 1 <= n) =>
  Endian              {- ^ How to append bit-vectors -} ->
  NatRepr w           {- ^ Width of bit-vectors in input -} ->
  NatRepr i           {- ^ Number of bit-vectors to join togeter -} ->
  Vector (n * i) (f (BVType w)) ->
  Vector n (f (BVType (i * w)))
joinVecBV :: forall (f :: CrucibleType -> Type) (i :: Natural) (w :: Natural)
       (n :: Natural).
(IsExpr f, 1 <= i, 1 <= w, 1 <= n) =>
Endian
-> NatRepr w
-> NatRepr i
-> Vector (n * i) (f (BVType w))
-> Vector n (f (BVType (i * w)))
joinVecBV Endian
e NatRepr w
w NatRepr i
i Vector (n * i) (f (BVType w))
xs = Endian
-> NatRepr w -> Vector i (f (BVType w)) -> f (BVType (i * w))
forall (f :: CrucibleType -> Type) (n :: Natural) (w :: Natural).
(1 <= w, IsExpr f) =>
Endian
-> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w))
toBV Endian
e NatRepr w
w (Vector i (f (BVType w)) -> f (BVType (i * w)))
-> Vector n (Vector i (f (BVType w)))
-> Vector n (f (BVType (i * w)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr n
-> NatRepr i
-> Vector (n * i) (f (BVType w))
-> Vector n (Vector i (f (BVType w)))
forall (w :: Natural) (n :: Natural) a.
(1 <= w, 1 <= n) =>
NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
split (NatRepr (n * i) -> NatRepr i -> NatRepr n
forall (n :: Natural) (m :: Natural).
(1 <= n) =>
NatRepr (m * n) -> NatRepr n -> NatRepr m
divNat (Vector (n * i) (f (BVType w)) -> NatRepr (n * i)
forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector (n * i) (f (BVType w))
xs) NatRepr i
i) NatRepr i
i Vector (n * i) (f (BVType w))
xs
{-# Inline joinVecBV #-}


-- | Turn a vector of large bit-vectors,
-- into a longer vector of shorter bit-vectors.
splitVecBV :: (IsExpr f, 1 <= i, 1 <= w) =>
  Endian ->
  NatRepr i {- ^ Split bit-vectors in this many parts -} ->
  NatRepr w {- ^ Length of bit-vectors in the result -} ->
  Vector n (f (BVType (i * w))) -> Vector (n*i) (f (BVType w))
splitVecBV :: forall (f :: CrucibleType -> Type) (i :: Natural) (w :: Natural)
       (n :: Natural).
(IsExpr f, 1 <= i, 1 <= w) =>
Endian
-> NatRepr i
-> NatRepr w
-> Vector n (f (BVType (i * w)))
-> Vector (n * i) (f (BVType w))
splitVecBV Endian
e NatRepr i
i NatRepr w
w Vector n (f (BVType (i * w)))
xs = NatRepr i
-> Vector n (Vector i (f (BVType w)))
-> Vector (n * i) (f (BVType w))
forall (w :: Natural) (n :: Natural) a.
(1 <= w) =>
NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
join NatRepr i
i (Endian
-> NatRepr i
-> NatRepr w
-> f (BVType (i * w))
-> Vector i (f (BVType w))
forall (f :: CrucibleType -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n, IsExpr f) =>
Endian
-> NatRepr n
-> NatRepr w
-> f (BVType (n * w))
-> Vector n (f (BVType w))
fromBV Endian
e NatRepr i
i NatRepr w
w (f (BVType (i * w)) -> Vector i (f (BVType w)))
-> Vector n (f (BVType (i * w)))
-> Vector n (Vector i (f (BVType w)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector n (f (BVType (i * w)))
xs)
{-# Inline splitVecBV #-}