content: {-# Language OverloadedStrings #-}
  {-# Language BlockArguments #-}
  {-# Language LambdaCase #-}
  -- | Export builders for Cryptol values
  module Cryptol.Eval.FFI.Abstract.Import (
    cryStartImport,
    cryFinishImport,
    cry_bool,
    cry_small_uint,
    cry_small_sint,
    cry_large_int,
    cry_sign,
    cry_tag,
    cry_double,
    Value,
    Import,
    LargeIntFun,
    ImportErrorMessage(..)
    )where
  
  import qualified Data.IntMap as IntMap
  import Data.List(intersperse)
  import Data.Vector(Vector)
  import qualified Data.Vector as Vector
  import Data.IORef
  import LibBF(bfFromDouble)
  import Foreign
  import Foreign.C.Types(CSize(..) )
  import Control.Monad.Primitive(PrimState)
  import GHC.Num.Compat(bigNatToInteger, bigNatToNegInteger)
  import Data.Primitive.PrimArray(MutablePrimArray(..), PrimArray(..),
          mutablePrimArrayContents, newPinnedPrimArray, unsafeFreezePrimArray)
  
  import Cryptol.Utils.PP
  import Cryptol.Backend.FloatHelpers
  import Cryptol.Utils.RecordMap
  import Cryptol.TypeCheck.Solver.InfNat
  import Cryptol.Eval.Type
  import Cryptol.Eval.Value
  import Cryptol.Backend.Monad
  import Cryptol.Backend.Concrete
  import Cryptol.Backend.SeqMap
  
  import Cryptol.Backend
  
  
  type Value = SEval Concrete (GenValue Concrete)
  
  -- | Imported Cryptol values (aka \"context\")
  data Importer =
      Building [Frame]    -- ^ A partial value
    | Done Value          -- ^ Fully built value
    | Error ImportErrorMessage
      -- ^ Something went wrong
      -- XXX: It'd be nice to store the [Frame] here as well,
      -- but that's a bit of a pain because of missing `Show` instances...
  
  data Mk =
    Mk { mkPrec :: Int, mkPP :: [Doc] -> Doc
       , mkVal :: [Value] -> Either ImportErrorMessage Value
       }
  
  -- | Describes what we are missing
  data Frame =
      NeedVal
      -- ^ A primitive value
  
    | NeedDouble Integer Integer
      -- ^ We are expecting a double to make the given floating point number
  
    | NeedSign (MutablePrimArray (PrimState IO) Word64)
      -- ^ This is a step of making a BigInt.
      -- We've allocated a buffer and are waiting for it to be filled with the
      -- base-64 digits of of a big int (least significant first),
      -- and to be told what the sign should be.
  
    | NeedMany Mk [Value] [TValue]
      -- ^ A compound value, fields are like this:
      --  * Constructor for the value
      --  * Parts of the value we have
      --  * Types of the parts of the values we still need,
      --    not counting the hole.
  
    | NeedOneOf (Vector (ConInfo TValue))
      -- ^ Sum type value, which needs a constructor tag to proceed.
  
  -- | Fill the "hole" with the given value.
  haveValue :: Value -> [Frame] -> Importer
  haveValue v fs =
    case fs of
      [] -> Done v
      f : more ->
        case f of
          NeedVal -> haveValue v more
          NeedDouble {} -> Error (ProtocolMismatch AFloat AValue)
          NeedMany mk vs ts ->
            let done = v : vs in
            case ts of
              [] -> case mkVal mk (reverse done) of
                      Left err -> Error err
                      Right a  -> haveValue a more
              t : ts' -> needValue t (NeedMany mk done ts' : more)
          NeedOneOf {} -> Error (ProtocolMismatch ATag AValue)
          NeedSign {} -> Error (ProtocolMismatch ASign AValue)
  
  -- | Provide a constructor tag
  haveTag :: Int -> [Frame] -> Importer
  haveTag n fs0 =
    case fs0 of
      [] -> Error UnexpectedData
      f : fs ->
        case f of
          NeedVal     -> Error (ProtocolMismatch AValue ATag)
          NeedDouble {} -> Error (ProtocolMismatch AFloat ATag)
          NeedMany {} -> Error (ProtocolMismatch AValue ATag)
          NeedSign {} -> Error (ProtocolMismatch ASign ATag)
          NeedOneOf opts ->
            case opts Vector.!? n of
              Nothing -> Error (TagOutOfBounds n)
              Just ci ->
                case Vector.toList (conFields ci) of
                  [] -> haveValue (mkV []) fs
                  t : ts ->
                    needValue t (NeedMany (Mk 10 ppV (Right . mkV)) [] ts : fs)
                where
                ppV xs = pp (conIdent ci) <+> hsep xs
  
                mkV :: [Value] -> Value
                mkV vs = pure (VEnum
                                (toInteger n)
                                (IntMap.singleton n
                                    ci { conFields = Vector.fromList vs }))
  
  
  haveSign :: Bool -> [Frame] -> IO Importer
  haveSign isPos fs0 =
    case fs0 of
      [] -> pure (Error UnexpectedData)
      f : fs ->
        case f of
          NeedVal -> mismatch AValue
          NeedDouble {} -> mismatch AValue
          NeedMany {} -> mismatch AValue
          NeedOneOf {} -> mismatch ATag
          NeedSign buf ->
            do PrimArray fbuf <- unsafeFreezePrimArray buf
               let i = if isPos then bigNatToInteger fbuf else bigNatToNegInteger fbuf
               i `seq` pure (haveValue (pure (VInteger i)) fs)
    where
    mismatch x = pure (Error (ProtocolMismatch x ASign))
  
  haveFloat :: Double -> [Frame] -> Importer
  haveFloat d fs0 =
    case fs0 of
      [] -> Error UnexpectedData
      f : fs ->
        case f of
          NeedDouble e p -> haveValue v fs
            where v = pure (VFloat (BF e p (bfFromDouble d))) :: Value
          NeedVal -> Error (ProtocolMismatch AValue AFloat)
          NeedMany {} -> Error (ProtocolMismatch AValue AFloat)
          NeedOneOf {} -> Error (ProtocolMismatch ATag AFloat)
          NeedSign {} -> Error (ProtocolMismatch ASign AFloat)
  
  
  -- | Make a "hole" of the given type.
  needValue :: TValue -> [Frame] -> Importer
  needValue tval fs =
    case tval of
      TVBit       -> Building (NeedVal : fs)
      TVInteger   -> Building (NeedVal : fs)
      TVIntMod _  -> Building (NeedVal : fs)
      TVFloat e p -> Building (NeedDouble e p : fs)
  
      TVRational ->
        Building (NeedVal : NeedMany (Mk 10 ppV mkV) [] [TVInteger] : fs)
          where
          ppV xs = "Rational" <+> hsep xs
          mkV xs =
            case xs of
              [Ready (VInteger i), Ready (VInteger j)] ->
                Right (VRational <$> ratio Concrete i j)
              _ -> Left BadRationalValue
  
      TVSeq len elT ->
        case elT of
          TVBit -> Building (NeedVal : NeedMany (Mk 10 ppV mkV) [] [] : fs)
            where
            ppV xs = "Word" <+> integer len <+> hsep xs
            mkV xs =
              case xs of
                [Ready (VInteger i)] -> Right (word Concrete len i)
                _ -> Left BadWordValue
  
          _ | len < 1 -> haveValue (mkV []) fs
            | otherwise ->
              needValue elT (NeedMany (Mk 0 ppV (Right . mkV)) [] ts : fs)
            where
            ppV xs = brackets (commaSep xs)
            mkV xs = mkSeq Concrete (Nat len) elT (finiteSeqMap Concrete xs)
            ts = replicate (fromInteger len - 1) elT
  
      TVTuple tys ->
        case tys of
          [] -> haveValue (mkV []) fs
          t : ts -> needValue t (NeedMany (Mk 0 ppV (Right . mkV)) [] ts : fs)
          where
          ppV xs = parens (commaSep xs)
          mkV = pure . VTuple
  
      TVRec rmp -> doRec rmp
  
      TVNominal _ _ nv ->
        case nv of
          TVAbstract -> Error (Unsupported "abstract")
          TVStruct rmp -> doRec rmp
          TVEnum cons -> Building (NeedOneOf cons : fs)
  
      TVFun {}    -> Error (Unsupported "function")
      TVStream {} -> Error (Unsupported "infinite stream")
      TVArray {}  -> Error (Unsupported "array")
  
    where
    doRec rmp =
      case ts of
        [] -> haveValue (mkV []) fs
        t : ts' -> needValue t (NeedMany (Mk 0 ppV (Right . mkV)) [] ts' : fs)
      where
      (ls,ts) = unzip (canonicalFields rmp)
      mkV vs = pure (VRecord (recordFromFields (zip ls vs)))
      ppV xs = braces (commaSep (zipWith ppF ls xs))
      ppF x y = pp x <+> "_" <+> y
  
  
  ppValPrec :: Int -> Value -> Doc
  ppValPrec p v =
    case ppValuePrec Concrete defaultPPOpts p =<< v of
      Ready doc -> doc
      _ -> "<thunk>"
  
  instance PP Frame where
    ppPrec _ f =
      case f of
        NeedVal -> "_"
        NeedDouble e p -> parens ("_" <+> ":" <+> "Float" <+> integer e <+> integer p)
        NeedMany mk vs ts ->
          let p = mkPrec mk
              args = map (ppValPrec p) vs ++ ["_"] ++ map (ppPrec p . tValTy) ts
          in mkPP mk args
        NeedOneOf vs ->
          hsep (intersperse "|" (map (pp . conIdent) (Vector.toList vs)))
        NeedSign {} -> "BigNum _"
  
  
  
  --------------------------------------------------------------------------------
  
  cryStartImport :: TValue -> IO (StablePtr (IORef Importer))
  cryStartImport ty =
    do ref <- newIORef (needValue ty [])
       newStablePtr ref
  
  cryFinishImport ::
    StablePtr (IORef Importer) -> IO (Either ImportErrorMessage Value)
  cryFinishImport ptr =
    do ref <- deRefStablePtr ptr
       freeStablePtr ptr
       builder <- readIORef ref
       pure $!
         case builder of
           Done v -> Right v
           Error e -> Left e
           Building _ -> Left PartialValue
  
  
  --------------------------------------------------------------------------------
  
  
  
  
  modifyState :: ([Frame] -> Importer) -> Ptr () -> IO ()
  modifyState how ptr =
    do ref <- deRefStablePtr (castPtrToStablePtr ptr)
       modifyIORef' ref \case
         Error err    -> Error err
         Done _       -> Error UnexpectedData
         Building fs  -> how fs
  
  
  -- | This function assumes that we are the only ones modifying the
  -- builder state, so we don't need to worry about race conditions.
  modifyStateIO :: ([Frame] -> IO Importer) -> Ptr () -> IO ()
  modifyStateIO how ptr =
    do ref <- deRefStablePtr (castPtrToStablePtr ptr)
       builder <- readIORef ref
       newS <- case builder of
                 Error err    -> pure (Error err)
                 Done _       -> pure (Error UnexpectedData)
                 Building fs  -> how fs
       newS `seq` writeIORef ref newS
  
  
  
  type Import a = Ptr () -> a -> IO ()
  
  -- | Receive a bool value
  cry_bool :: Import Word8
  cry_bool self b = modifyState (haveValue $! v) self
    where
    v = if b == 0 then pure (VBit False) else pure (VBit True)
  
  -- | Receive a double value
  cry_double :: Import Double
  cry_double self b = modifyState (haveFloat $! b) self
  
  -- | Receive a small unsigned integer that fits in 64-bits
  cry_small_uint :: Import Word64
  cry_small_uint self i = modifyState (haveValue $! v) self
    where
    v = pure $! VInteger $! toInteger i
  
  -- | Receive a small signed integer that fits in 64-bits
  cry_small_sint :: Import Int64
  cry_small_sint self i = modifyState (haveValue $! v) self
    where
    v = pure $! VInteger $! toInteger i
  
  
  -- | Receive an integer that's larger than 64-bits.
  -- This is part 1 of a 2 step process.
  type LargeIntFun = Ptr () -> CSize -> IO (Ptr Word64)
  cry_large_int :: LargeIntFun
  cry_large_int ptr sz =
    do arr <- newPinnedPrimArray (fromIntegral sz)
       modifyState (\fs -> Building (NeedSign arr : fs)) ptr
       pure (mutablePrimArrayContents arr)
  
  -- | Finish building a large integer.
  -- The argument is 1 for negative, 0 for non-negative.
  cry_sign :: Import Word8
  cry_sign self sign = modifyStateIO (haveSign (sign == 0)) self
  
  -- | Receive a tag for a sum type.
  cry_tag :: Import CSize
  cry_tag self c = modifyState (haveTag $! fromIntegral c) self
  