content: {-# Language OverloadedStrings, BangPatterns, MagicHash #-}
  module Cryptol.Eval.FFI.Abstract.Export
    ( ExportVal
    , ExporterErrorMessage(..)
    , Export
    , exportValue, exportValues, exportSizes
    , cryStartExport, cryEndExport
    , cry_recv_u8
    , cry_recv_u64
    , cry_recv_u64_digits
    , cry_recv_double
    ) where
  
  import Data.Text(Text)
  import qualified Data.Vector as Vector
  import qualified Data.IntMap as IntMap
  import Control.Exception(Exception,throw)
  import Data.IORef(IORef,newIORef,readIORef,writeIORef)
  import LibBF
  import Foreign
      ( Word8, Word32, Word64, StablePtr, Ptr, Storable(poke),
        newStablePtr, freeStablePtr, castPtrToStablePtr, deRefStablePtr )
  import GHC.Num ( Integer(IN, IS, IP) )
  import GHC.Base(Int(..))
  import Data.Primitive.PrimArray
      ( copyPrimArrayToPtr, sizeofPrimArray, PrimArray(..) )
  
  import Cryptol.Utils.RecordMap ( canonicalFields )
  import Cryptol.Eval.Value ( Backend(SWord, SEval), GenValue(..) )
  import Cryptol.Eval.Type(conFields)
  import Cryptol.Backend.FloatHelpers
  import Cryptol.Backend.Concrete ( BV(BV), Concrete(..) )
  import Cryptol.Backend.Monad(Eval)
  import Cryptol.Backend.SeqMap (enumerateSeqMap)
  import Cryptol.Backend(SRational(..))
  import Cryptol.Backend.WordValue(asWordVal)
  
  data ExportVal =
      EV8 !Word8              -- ^ Bit, integer sign
    | EV64 !Word64            -- ^ Buffer size, sum tag
    | EVDouble !Double        -- ^ A double
    | EVInteger !Integer      -- ^ Integer, Z, Word, components of Rational
  
  
  data ExporterErrorMessage =
      UnsupportedValue Text
    | MalformedSum
    deriving Show
  
  instance Exception ExporterErrorMessage
  
  type Value = SEval Concrete (GenValue Concrete)
  
  -- Serialize a value into its external representation.
  exportValue :: GenValue Concrete -> [ExportVal] -> Eval [ExportVal]
  exportValue v =
    case v of
      VRecord rmap -> doRec rmap
      VTuple vs    -> exportValues vs
      VSeq n sm    -> exportValues (enumerateSeqMap n sm)
  
      -- 1. tag, 2. constructor values
      VEnum tag mp
        | 0 <= tag && tag <= toInteger (maxBound :: Int)
        , let n = fromInteger tag
        , Just con <- IntMap.lookup n mp ->
          exportValues (Vector.toList (conFields con)) . (EV64 (fromIntegral n) :)
  
        | otherwise -> throw MalformedSum
  
      VBit b      -> pure . exportBit b
      VInteger i  -> pure . exportInteger i
      VRational r -> pure . exportRational r
      VFloat f
        |  bfExpWidth f == 8 && bfPrecWidth f == 24
        || bfExpWidth f == 11 && bfPrecWidth f == 53 ->
          pure . exportDouble (bfValue f)
        | otherwise -> throw (UnsupportedValue "non-standard float")
  
      VWord w   -> \start ->
        do wv <- asWordVal Concrete w
           pure (exportWord wv start)
  
  
      VStream {}  -> throw (UnsupportedValue "infinte stream")
      VFun {}     -> throw (UnsupportedValue "function")
      VPoly {}    -> throw (UnsupportedValue "polymorphic")
      VNumPoly {} -> throw (UnsupportedValue "polymorphic")
    where
    doRec rmap = exportValues (map snd (canonicalFields rmap))
  
  
  -- | Export some top-level sizes.
  -- Exported as `u64` if it is less than `2^64-1`.
  -- Otherwise exported as: `(2^64-1 : u64)` followed by an unsigned integer
  exportSizes :: [Integer] -> [ExportVal] -> [ExportVal]
  exportSizes xs =
    case xs of
      [] -> id
      x : more -> exportSizes more . exportSize x
  
  -- | Export a type-level size.
  -- Exported as `u64` if it is less than `2^64-1`.
  -- Otherwise exported as: `(2^64-1 : u64)` followed by an unsigned integer
  exportSize :: Integer -> [ExportVal] -> [ExportVal]
  exportSize n start
    | n < toInteger m = EV64 (fromInteger n) : start
    | otherwise = exportInteger n (EV64 m : start)
    where m = maxBound :: Word64
  
  exportDouble :: BigFloat -> [ExportVal] -> [ExportVal]
  exportDouble bf = (EVDouble d :)
    where
    (!d,_) = bfToDouble NearAway bf
  
  -- | Encoding of a bit: 0 or 1
  exportBit :: Bool -> [ExportVal] -> [ExportVal]
  exportBit b = (EV8 u8 :)
    where
    !u8 = if b then 1 else 0
  
  -- | Encoding for an integer: sign, buffer size, digits
  exportInteger :: Integer -> [ExportVal] -> [ExportVal]
  exportInteger i = \start -> EVInteger i : EV64 size : EV8 sign : start
    where
    !sign = if i < 0 then 1 else 0
    !size = integerSize i
  
  -- | Encoding of a rational: numerator, denominator; both are integers
  exportRational :: SRational Concrete -> [ExportVal] -> [ExportVal]
  exportRational r = exportInteger (sDenom r) . exportInteger (sNum r)
  
  -- | Encoding of a word: buffer size, digits
  exportWord :: SWord Concrete -> [ExportVal] -> [ExportVal]
  exportWord (BV sz i) = \start ->
    if sz <= 8 then EV8 (fromInteger i) : start else
    if sz <= 64 then EV64 (fromInteger i) : start else
    EVInteger i : EV64 size : start
    where
    !size = integerSize i
  
  -- | Export a sequence of values: tuples, records, sequences.
  -- Note that empty sequences don't have any representation.
  exportValues :: [Value] -> [ExportVal] -> Eval [ExportVal]
  exportValues vs done =
    case vs of
      mv : more ->
        do v <- mv
           exportValues more =<< exportValue v done
      [] -> pure done
  
  
  -- | How many Word64s do we need to represent this integer.
  integerSize :: Integer -> Word64
  integerSize i =
    case i of
      IS _ -> 1
      IP x -> getSize (PrimArray x)
      IN x -> getSize (PrimArray x)
    where
    getSize :: PrimArray Word64 -> Word64
    getSize x = fromIntegral (sizeofPrimArray x)
  
  
  
  cryStartExport ::
      [ExportVal] {-| REVERSED.  Send these to foreign. -} ->
      IO (StablePtr (IORef [ExportVal]))
  cryStartExport vs =
    do ref <- newIORef (reverse vs)
       newStablePtr ref
  
  -- | Get the next data item to export.
  -- We assume that this is the only place to manipulate the reference
  -- so there's not a race condition. Note that it is also important
  -- that we access these from the same thread, otherwise we may miss
  -- some of the writes etc.  This should be OK because FFI calls should
  -- all be happening on the same thread.
  cryExportNext ::
    StablePtr (IORef [ExportVal]) -> IO (Either Word32 ExportVal)
  cryExportNext ptr =
    do ref <- deRefStablePtr ptr
       xs  <- readIORef ref
       case xs of
         x : more -> writeIORef ref more >> pure (Right x)
         [] -> pure (Left maxBound)
  
  cryEndExport :: StablePtr (IORef [ExportVal]) -> IO ()
  cryEndExport = freeStablePtr
  
  
  type Export a = Ptr () -> Ptr a -> IO Word32
  
  -- | Get the next data item, which should be uint8_t
  cry_recv_u8 :: Export Word8
  cry_recv_u8 self out =
    do mb <- cryExportNext (castPtrToStablePtr self)
       case mb of
         Left err -> pure err
         Right d ->
           case d of
             EV8 w        -> poke out w >> pure 0
             EV64 {}      -> pure 2
             EVInteger {} -> pure 3
             EVDouble {}  -> pure 4
  
  
  -- | Get the next data item, which shoudl be uint64_t
  cry_recv_u64 :: Export Word64
  cry_recv_u64 self out =
    do mb <- cryExportNext (castPtrToStablePtr self)
       case mb of
         Left err -> pure err
         Right d ->
           case d of
             EV8 {}       -> pure 1
             EV64 w       -> poke out w >> pure 0
             EVInteger {} -> pure 3
             EVDouble {}  -> pure 4
  
  
  -- | Get the digits for an integer
  cry_recv_u64_digits :: Export Word64
  cry_recv_u64_digits self out =
    do mb <- cryExportNext (castPtrToStablePtr self)
       case mb of
         Left err -> pure err
         Right d ->
           case d of
             EV8 {}      -> pure 1
             EV64 {}     -> pure 2
             EVDouble {} -> pure 4
             EVInteger i ->
               do case i of
                    IS x -> poke out (fromIntegral (abs (I# x)))
                    IP x -> doCopy (PrimArray x)
                    IN x -> doCopy (PrimArray x)
                  pure 0
              where
              doCopy :: PrimArray Word64 -> IO ()
              doCopy x = copyPrimArrayToPtr out x 0 (sizeofPrimArray x)
  
  cry_recv_double :: Export Double
  cry_recv_double self out =
    do mb <- cryExportNext (castPtrToStablePtr self)
       case mb of
         Left err -> pure err
         Right d ->
           case d of
             EV8 {}       -> pure 1
             EV64 {}      -> pure 2
             EVInteger {} -> pure 3
             EVDouble dbl -> poke out dbl >> pure 0
  