content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE UndecidableInstances #-}
  --
  -- Array.hs --- Bit data array types.
  --
  -- Copyright (C) 2013, Galois, Inc.
  -- All Rights Reserved.
  --
  
  module Ivory.Language.BitData.Array where
  
  import Ivory.Language.Bits
  import Ivory.Language.Proxy
  
  import Ivory.Language.BitData.Bits
  import Ivory.Language.BitData.BitData
  
  import GHC.TypeLits(Nat)
  
  -- NOTE: This type family is used to calculate the total size of a bit
  -- array by multiplying "n" by the size of "a" in bits.  Once we have
  -- the type-nats solver in place, we should no longer need this.
  --
  -- The quasiquoter may generate multiple instances of "ArraySize" with
  -- the same "n", "a" and result, which is allowed by the type family
  -- overlapping rules.  It does seem like a bit of a hack though.
  type family ArraySize (n :: Nat) (a :: *) :: Nat
  
  -- | An array of "n" bit data elements of type "a".
  data BitArray (n :: Nat) a = BitArray { unArray :: Bits (ArraySize n a) }
  
  -- | Return the number of elements in a "BitArray".
  bitLength :: forall a n. ANat n => BitArray n a -> Int
  bitLength _ = fromIntegral (fromTypeNat (aNat :: NatType n))
  
  instance (ANat n,
            ANat (ArraySize n a),
            BitData a,
            IvoryRep (BitRep (ArraySize n a)))
      => BitData (BitArray n a) where
    type BitType (BitArray n a) = Bits (ArraySize n a)
    toBits = unArray
    fromBits = BitArray
  
  -- | Return the "n"th element of a "BitArray".
  (#!) :: forall a n.
          (BitData a,
           ANat n,
           ANat (BitSize a),
           ANat (ArraySize n a),
           BitCast (BitRep (ArraySize n a)) (BitDataRep a),
           IvoryRep (BitRep (ArraySize n a)))
       => BitArray n a -> Int -> a
  BitArray bits #! i =
    if (i < 0) || (i >= n')
      then error "bit array index out of bounds"
      else bits #. field
    where
      n'       = fromIntegral (fromTypeNat (aNat :: NatType n)) :: Int
      elemSize = fromIntegral (fromTypeNat (aNat :: NatType (BitSize a))) :: Int
      field    = BitDataField (i * elemSize) elemSize ixname
      ixname = "[" ++ show i ++ "]"
  
  -- | Return a "BitDataField" that accesses the "n"th element of a
  -- "BitArray".  This can be composed with other field accessors using
  -- "#>".
  bitIx :: forall a n.
           (BitData a,
            ANat n,
            ANat (BitSize a),
            ANat (ArraySize n a))
        => Int -> BitDataField (BitArray n a) a
  bitIx i = BitDataField (i * elemSize) elemSize ixname
    where
      ixname = "[" ++ show i ++ "]"
      elemSize = fromIntegral (fromTypeNat (aNat :: NatType (BitSize a))) :: Int
  