{-# 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 { Mk -> Int
mkPrec :: Int, Mk -> [Doc] -> Doc
mkPP :: [Doc] -> Doc
     , Mk -> [Value] -> Either ImportErrorMessage Value
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 :: Value -> [Frame] -> Importer
haveValue Value
v [Frame]
fs =
  case [Frame]
fs of
    [] -> Value -> Importer
Done Value
v
    Frame
f : [Frame]
more ->
      case Frame
f of
        Frame
NeedVal -> Value -> [Frame] -> Importer
haveValue Value
v [Frame]
more
        NeedDouble {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
AFloat ImportThing
AValue)
        NeedMany Mk
mk [Value]
vs [TValue]
ts ->
          let done :: [Eval (GenValue Concrete)]
done = Eval (GenValue Concrete)
Value
v Eval (GenValue Concrete)
-> [Eval (GenValue Concrete)] -> [Eval (GenValue Concrete)]
forall a. a -> [a] -> [a]
: [Eval (GenValue Concrete)]
[Value]
vs in
          case [TValue]
ts of
            [] -> case Mk -> [Value] -> Either ImportErrorMessage Value
mkVal Mk
mk ([Eval (GenValue Concrete)] -> [Eval (GenValue Concrete)]
forall a. [a] -> [a]
reverse [Eval (GenValue Concrete)]
done) of
                    Left ImportErrorMessage
err -> ImportErrorMessage -> Importer
Error ImportErrorMessage
err
                    Right Value
a  -> Value -> [Frame] -> Importer
haveValue Value
a [Frame]
more
            TValue
t : [TValue]
ts' -> TValue -> [Frame] -> Importer
needValue TValue
t (Mk -> [Value] -> [TValue] -> Frame
NeedMany Mk
mk [Eval (GenValue Concrete)]
[Value]
done [TValue]
ts' Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
more)
        NeedOneOf {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
ATag ImportThing
AValue)
        NeedSign {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
ASign ImportThing
AValue)

-- | Provide a constructor tag
haveTag :: Int -> [Frame] -> Importer
haveTag :: Int -> [Frame] -> Importer
haveTag Int
n [Frame]
fs0 =
  case [Frame]
fs0 of
    [] -> ImportErrorMessage -> Importer
Error ImportErrorMessage
UnexpectedData
    Frame
f : [Frame]
fs ->
      case Frame
f of
        Frame
NeedVal     -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
AValue ImportThing
ATag)
        NeedDouble {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
AFloat ImportThing
ATag)
        NeedMany {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
AValue ImportThing
ATag)
        NeedSign {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
ASign ImportThing
ATag)
        NeedOneOf Vector (ConInfo TValue)
opts ->
          case Vector (ConInfo TValue)
opts Vector (ConInfo TValue) -> Int -> Maybe (ConInfo TValue)
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
n of
            Maybe (ConInfo TValue)
Nothing -> ImportErrorMessage -> Importer
Error (Int -> ImportErrorMessage
TagOutOfBounds Int
n)
            Just ConInfo TValue
ci ->
              case Vector TValue -> [TValue]
forall a. Vector a -> [a]
Vector.toList (ConInfo TValue -> Vector TValue
forall a. ConInfo a -> Vector a
conFields ConInfo TValue
ci) of
                [] -> Value -> [Frame] -> Importer
haveValue ([Value] -> Value
mkV []) [Frame]
fs
                TValue
t : [TValue]
ts ->
                  TValue -> [Frame] -> Importer
needValue TValue
t (Mk -> [Value] -> [TValue] -> Frame
NeedMany (Int
-> ([Doc] -> Doc)
-> ([Value] -> Either ImportErrorMessage Value)
-> Mk
Mk Int
10 [Doc] -> Doc
ppV (Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right (Eval (GenValue Concrete)
 -> Either ImportErrorMessage (Eval (GenValue Concrete)))
-> ([Eval (GenValue Concrete)] -> Eval (GenValue Concrete))
-> [Eval (GenValue Concrete)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
[Value] -> Value
mkV)) [] [TValue]
ts Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
              where
              ppV :: [Doc] -> Doc
ppV [Doc]
xs = Ident -> Doc
forall a. PP a => a -> Doc
pp (ConInfo TValue -> Ident
forall a. ConInfo a -> Ident
conIdent ConInfo TValue
ci) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep [Doc]
xs

              mkV :: [Value] -> Value
              mkV :: [Value] -> Value
mkV [Value]
vs = GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger Concrete
-> IntMap (ConValue Concrete) -> GenValue Concrete
forall sym. SInteger sym -> IntMap (ConValue sym) -> GenValue sym
VEnum
                              (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)
                              (Int
-> ConInfo (Eval (GenValue Concrete))
-> IntMap (ConInfo (Eval (GenValue Concrete)))
forall a. Int -> a -> IntMap a
IntMap.singleton Int
n
                                  ConInfo TValue
ci { conFields = Vector.fromList vs }))


haveSign :: Bool -> [Frame] -> IO Importer
haveSign :: Bool -> [Frame] -> IO Importer
haveSign Bool
isPos [Frame]
fs0 =
  case [Frame]
fs0 of
    [] -> Importer -> IO Importer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImportErrorMessage -> Importer
Error ImportErrorMessage
UnexpectedData)
    Frame
f : [Frame]
fs ->
      case Frame
f of
        Frame
NeedVal -> ImportThing -> IO Importer
forall {f :: * -> *}. Applicative f => ImportThing -> f Importer
mismatch ImportThing
AValue
        NeedDouble {} -> ImportThing -> IO Importer
forall {f :: * -> *}. Applicative f => ImportThing -> f Importer
mismatch ImportThing
AValue
        NeedMany {} -> ImportThing -> IO Importer
forall {f :: * -> *}. Applicative f => ImportThing -> f Importer
mismatch ImportThing
AValue
        NeedOneOf {} -> ImportThing -> IO Importer
forall {f :: * -> *}. Applicative f => ImportThing -> f Importer
mismatch ImportThing
ATag
        NeedSign MutablePrimArray (PrimState IO) Word64
buf ->
          do PrimArray ByteArray#
fbuf <- MutablePrimArray (PrimState IO) Word64 -> IO (PrimArray Word64)
forall (m :: * -> *) a.
PrimMonad m =>
MutablePrimArray (PrimState m) a -> m (PrimArray a)
unsafeFreezePrimArray MutablePrimArray (PrimState IO) Word64
buf
             let i :: Integer
i = if Bool
isPos then ByteArray# -> Integer
bigNatToInteger ByteArray#
fbuf else ByteArray# -> Integer
bigNatToNegInteger ByteArray#
fbuf
             Integer
i Integer -> IO Importer -> IO Importer
forall a b. a -> b -> b
`seq` Importer -> IO Importer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> [Frame] -> Importer
haveValue (GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger Concrete -> GenValue Concrete
forall sym. SInteger sym -> GenValue sym
VInteger Integer
SInteger Concrete
i)) [Frame]
fs)
  where
  mismatch :: ImportThing -> f Importer
mismatch ImportThing
x = Importer -> f Importer
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
x ImportThing
ASign))

haveFloat :: Double -> [Frame] -> Importer
haveFloat :: Double -> [Frame] -> Importer
haveFloat Double
d [Frame]
fs0 =
  case [Frame]
fs0 of
    [] -> ImportErrorMessage -> Importer
Error ImportErrorMessage
UnexpectedData
    Frame
f : [Frame]
fs ->
      case Frame
f of
        NeedDouble Integer
e Integer
p -> Value -> [Frame] -> Importer
haveValue Eval (GenValue Concrete)
Value
v [Frame]
fs
          where v :: Value
v = GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SFloat Concrete -> GenValue Concrete
forall sym. SFloat sym -> GenValue sym
VFloat (Integer -> Integer -> BigFloat -> BF
BF Integer
e Integer
p (Double -> BigFloat
bfFromDouble Double
d))) :: Value
        Frame
NeedVal -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
AValue ImportThing
AFloat)
        NeedMany {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
AValue ImportThing
AFloat)
        NeedOneOf {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
ATag ImportThing
AFloat)
        NeedSign {} -> ImportErrorMessage -> Importer
Error (ImportThing -> ImportThing -> ImportErrorMessage
ProtocolMismatch ImportThing
ASign ImportThing
AFloat)


-- | Make a "hole" of the given type.
needValue :: TValue -> [Frame] -> Importer
needValue :: TValue -> [Frame] -> Importer
needValue TValue
tval [Frame]
fs =
  case TValue
tval of
    TValue
TVBit       -> [Frame] -> Importer
Building (Frame
NeedVal Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
    TValue
TVInteger   -> [Frame] -> Importer
Building (Frame
NeedVal Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
    TVIntMod Integer
_  -> [Frame] -> Importer
Building (Frame
NeedVal Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
    TVFloat Integer
e Integer
p -> [Frame] -> Importer
Building (Integer -> Integer -> Frame
NeedDouble Integer
e Integer
p Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)

    TValue
TVRational ->
      [Frame] -> Importer
Building (Frame
NeedVal Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: Mk -> [Value] -> [TValue] -> Frame
NeedMany (Int
-> ([Doc] -> Doc)
-> ([Value] -> Either ImportErrorMessage Value)
-> Mk
Mk Int
10 [Doc] -> Doc
ppV [Eval (GenValue Concrete)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
[Value] -> Either ImportErrorMessage Value
forall {sym}.
(SInteger sym ~ Integer) =>
[Eval (GenValue sym)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
mkV) [] [TValue
TVInteger] Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
        where
        ppV :: [Doc] -> Doc
ppV [Doc]
xs = Doc
"Rational" Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep [Doc]
xs
        mkV :: [Eval (GenValue sym)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
mkV [Eval (GenValue sym)]
xs =
          case [Eval (GenValue sym)]
xs of
            [Ready (VInteger SInteger sym
i), Ready (VInteger SInteger sym
j)] ->
              Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right (SRational Concrete -> GenValue Concrete
forall sym. SRational sym -> GenValue sym
VRational (SRational Concrete -> GenValue Concrete)
-> Eval (SRational Concrete) -> Eval (GenValue Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SRational Concrete)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio Concrete
Concrete SInteger sym
SInteger Concrete
i SInteger sym
SInteger Concrete
j)
            [Eval (GenValue sym)]
_ -> ImportErrorMessage
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. a -> Either a b
Left ImportErrorMessage
BadRationalValue

    TVSeq Integer
len TValue
elT ->
      case TValue
elT of
        TValue
TVBit -> [Frame] -> Importer
Building (Frame
NeedVal Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: Mk -> [Value] -> [TValue] -> Frame
NeedMany (Int
-> ([Doc] -> Doc)
-> ([Value] -> Either ImportErrorMessage Value)
-> Mk
Mk Int
10 [Doc] -> Doc
ppV [Eval (GenValue Concrete)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
[Value] -> Either ImportErrorMessage Value
forall {sym}.
(SInteger sym ~ Integer) =>
[Eval (GenValue sym)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
mkV) [] [] Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
          where
          ppV :: [Doc] -> Doc
ppV [Doc]
xs = Doc
"Word" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
len Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep [Doc]
xs
          mkV :: [Eval (GenValue sym)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
mkV [Eval (GenValue sym)]
xs =
            case [Eval (GenValue sym)]
xs of
              [Ready (VInteger SInteger sym
i)] -> Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right (Concrete -> Integer -> Integer -> Value
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (GenValue sym)
word Concrete
Concrete Integer
len Integer
SInteger sym
i)
              [Eval (GenValue sym)]
_ -> ImportErrorMessage
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. a -> Either a b
Left ImportErrorMessage
BadWordValue

        TValue
_ | Integer
len Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
1 -> Value -> [Frame] -> Importer
haveValue ([Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
mkV []) [Frame]
fs
          | Bool
otherwise ->
            TValue -> [Frame] -> Importer
needValue TValue
elT (Mk -> [Value] -> [TValue] -> Frame
NeedMany (Int
-> ([Doc] -> Doc)
-> ([Value] -> Either ImportErrorMessage Value)
-> Mk
Mk Int
0 [Doc] -> Doc
ppV (Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right (Eval (GenValue Concrete)
 -> Either ImportErrorMessage (Eval (GenValue Concrete)))
-> ([Eval (GenValue Concrete)] -> Eval (GenValue Concrete))
-> [Eval (GenValue Concrete)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
mkV)) [] [TValue]
ts Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
          where
          ppV :: [Doc] -> Doc
ppV [Doc]
xs = Doc -> Doc
brackets ([Doc] -> Doc
commaSep [Doc]
xs)
          mkV :: [Eval (GenValue Concrete)] -> Value
mkV [Eval (GenValue Concrete)]
xs = Concrete
-> Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Value
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq Concrete
Concrete (Integer -> Nat'
Nat Integer
len) TValue
elT (Concrete -> [Value] -> SeqMap Concrete (GenValue Concrete)
forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap Concrete
Concrete [Eval (GenValue Concrete)]
[Value]
xs)
          ts :: [TValue]
ts = Int -> TValue -> [TValue]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TValue
elT

    TVTuple [TValue]
tys ->
      case [TValue]
tys of
        [] -> Value -> [Frame] -> Importer
haveValue ([Value] -> Eval (GenValue Concrete)
forall {sym}. [SEval sym (GenValue sym)] -> Eval (GenValue sym)
mkV []) [Frame]
fs
        TValue
t : [TValue]
ts -> TValue -> [Frame] -> Importer
needValue TValue
t (Mk -> [Value] -> [TValue] -> Frame
NeedMany (Int
-> ([Doc] -> Doc)
-> ([Value] -> Either ImportErrorMessage Value)
-> Mk
Mk Int
0 [Doc] -> Doc
ppV (Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right (Eval (GenValue Concrete)
 -> Either ImportErrorMessage (Eval (GenValue Concrete)))
-> ([Eval (GenValue Concrete)] -> Eval (GenValue Concrete))
-> [Eval (GenValue Concrete)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
[Value] -> Eval (GenValue Concrete)
forall {sym}. [SEval sym (GenValue sym)] -> Eval (GenValue sym)
mkV)) [] [TValue]
ts Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
        where
        ppV :: [Doc] -> Doc
ppV [Doc]
xs = Doc -> Doc
parens ([Doc] -> Doc
commaSep [Doc]
xs)
        mkV :: [SEval sym (GenValue sym)] -> Eval (GenValue sym)
mkV = GenValue sym -> Eval (GenValue sym)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> Eval (GenValue sym))
-> ([SEval sym (GenValue sym)] -> GenValue sym)
-> [SEval sym (GenValue sym)]
-> Eval (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple

    TVRec RecordMap Ident TValue
rmp -> RecordMap Ident TValue -> Importer
doRec RecordMap Ident TValue
rmp

    TVNominal NominalType
_ [Either Nat' TValue]
_ TNominalTypeValue
nv ->
      case TNominalTypeValue
nv of
        TNominalTypeValue
TVAbstract -> ImportErrorMessage -> Importer
Error (Text -> ImportErrorMessage
Unsupported Text
"abstract")
        TVStruct RecordMap Ident TValue
rmp -> RecordMap Ident TValue -> Importer
doRec RecordMap Ident TValue
rmp
        TVEnum Vector (ConInfo TValue)
cons -> [Frame] -> Importer
Building (Vector (ConInfo TValue) -> Frame
NeedOneOf Vector (ConInfo TValue)
cons Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)

    TVFun {}    -> ImportErrorMessage -> Importer
Error (Text -> ImportErrorMessage
Unsupported Text
"function")
    TVStream {} -> ImportErrorMessage -> Importer
Error (Text -> ImportErrorMessage
Unsupported Text
"infinite stream")
    TVArray {}  -> ImportErrorMessage -> Importer
Error (Text -> ImportErrorMessage
Unsupported Text
"array")

  where
  doRec :: RecordMap Ident TValue -> Importer
doRec RecordMap Ident TValue
rmp =
    case [TValue]
ts of
      [] -> Value -> [Frame] -> Importer
haveValue ([Value] -> Eval (GenValue Concrete)
forall {f :: * -> *} {sym}.
Applicative f =>
[SEval sym (GenValue sym)] -> f (GenValue sym)
mkV []) [Frame]
fs
      TValue
t : [TValue]
ts' -> TValue -> [Frame] -> Importer
needValue TValue
t (Mk -> [Value] -> [TValue] -> Frame
NeedMany (Int
-> ([Doc] -> Doc)
-> ([Value] -> Either ImportErrorMessage Value)
-> Mk
Mk Int
0 [Doc] -> Doc
ppV (Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right (Eval (GenValue Concrete)
 -> Either ImportErrorMessage (Eval (GenValue Concrete)))
-> ([Eval (GenValue Concrete)] -> Eval (GenValue Concrete))
-> [Eval (GenValue Concrete)]
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
[Value] -> Eval (GenValue Concrete)
forall {f :: * -> *} {sym}.
Applicative f =>
[SEval sym (GenValue sym)] -> f (GenValue sym)
mkV)) [] [TValue]
ts' Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)
    where
    ([Ident]
ls,[TValue]
ts) = [(Ident, TValue)] -> ([Ident], [TValue])
forall a b. [(a, b)] -> ([a], [b])
unzip (RecordMap Ident TValue -> [(Ident, TValue)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
rmp)
    mkV :: [SEval sym (GenValue sym)] -> f (GenValue sym)
mkV [SEval sym (GenValue sym)]
vs = GenValue sym -> f (GenValue sym)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord ([(Ident, SEval sym (GenValue sym))]
-> RecordMap Ident (SEval sym (GenValue sym))
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([Ident]
-> [SEval sym (GenValue sym)]
-> [(Ident, SEval sym (GenValue sym))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ls [SEval sym (GenValue sym)]
vs)))
    ppV :: [Doc] -> Doc
ppV [Doc]
xs = Doc -> Doc
braces ([Doc] -> Doc
commaSep ((Ident -> Doc -> Doc) -> [Ident] -> [Doc] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Ident -> Doc -> Doc
forall {a}. PP a => a -> Doc -> Doc
ppF [Ident]
ls [Doc]
xs))
    ppF :: a -> Doc -> Doc
ppF a
x Doc
y = a -> Doc
forall a. PP a => a -> Doc
pp a
x Doc -> Doc -> Doc
<+> Doc
"_" Doc -> Doc -> Doc
<+> Doc
y


ppValPrec :: Int -> Value -> Doc
ppValPrec :: Int -> Value -> Doc
ppValPrec Int
p Value
v =
  case Concrete
-> PPOpts -> Int -> GenValue Concrete -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> Int -> GenValue sym -> SEval sym Doc
ppValuePrec Concrete
Concrete PPOpts
defaultPPOpts Int
p (GenValue Concrete -> Eval Doc)
-> Eval (GenValue Concrete) -> Eval Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue Concrete)
Value
v of
    Ready Doc
doc -> Doc
doc
    Eval Doc
_ -> Doc
"<thunk>"

instance PP Frame where
  ppPrec :: Int -> Frame -> Doc
ppPrec Int
_ Frame
f =
    case Frame
f of
      Frame
NeedVal -> Doc
"_"
      NeedDouble Integer
e Integer
p -> Doc -> Doc
parens (Doc
"_" Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Doc
"Float" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
e Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
p)
      NeedMany Mk
mk [Value]
vs [TValue]
ts ->
        let p :: Int
p = Mk -> Int
mkPrec Mk
mk
            args :: [Doc]
args = (Eval (GenValue Concrete) -> Doc)
-> [Eval (GenValue Concrete)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Value -> Doc
ppValPrec Int
p) [Eval (GenValue Concrete)]
[Value]
vs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
"_"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (TValue -> Doc) -> [TValue] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Type -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
p (Type -> Doc) -> (TValue -> Type) -> TValue -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> Type
tValTy) [TValue]
ts
        in Mk -> [Doc] -> Doc
mkPP Mk
mk [Doc]
args
      NeedOneOf Vector (ConInfo TValue)
vs ->
        [Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
intersperse Doc
"|" ((ConInfo TValue -> Doc) -> [ConInfo TValue] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Ident -> Doc
forall a. PP a => a -> Doc
pp (Ident -> Doc)
-> (ConInfo TValue -> Ident) -> ConInfo TValue -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConInfo TValue -> Ident
forall a. ConInfo a -> Ident
conIdent) (Vector (ConInfo TValue) -> [ConInfo TValue]
forall a. Vector a -> [a]
Vector.toList Vector (ConInfo TValue)
vs)))
      NeedSign {} -> Doc
"BigNum _"



--------------------------------------------------------------------------------

cryStartImport :: TValue -> IO (StablePtr (IORef Importer))
cryStartImport :: TValue -> IO (StablePtr (IORef Importer))
cryStartImport TValue
ty =
  do IORef Importer
ref <- Importer -> IO (IORef Importer)
forall a. a -> IO (IORef a)
newIORef (TValue -> [Frame] -> Importer
needValue TValue
ty [])
     IORef Importer -> IO (StablePtr (IORef Importer))
forall a. a -> IO (StablePtr a)
newStablePtr IORef Importer
ref

cryFinishImport ::
  StablePtr (IORef Importer) -> IO (Either ImportErrorMessage Value)
cryFinishImport :: StablePtr (IORef Importer) -> IO (Either ImportErrorMessage Value)
cryFinishImport StablePtr (IORef Importer)
ptr =
  do IORef Importer
ref <- StablePtr (IORef Importer) -> IO (IORef Importer)
forall a. StablePtr a -> IO a
deRefStablePtr StablePtr (IORef Importer)
ptr
     StablePtr (IORef Importer) -> IO ()
forall a. StablePtr a -> IO ()
freeStablePtr StablePtr (IORef Importer)
ptr
     Importer
builder <- IORef Importer -> IO Importer
forall a. IORef a -> IO a
readIORef IORef Importer
ref
     Either ImportErrorMessage (Eval (GenValue Concrete))
-> IO (Either ImportErrorMessage (Eval (GenValue Concrete)))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ImportErrorMessage (Eval (GenValue Concrete))
 -> IO (Either ImportErrorMessage (Eval (GenValue Concrete))))
-> Either ImportErrorMessage (Eval (GenValue Concrete))
-> IO (Either ImportErrorMessage (Eval (GenValue Concrete)))
forall a b. (a -> b) -> a -> b
$!
       case Importer
builder of
         Done Value
v -> Eval (GenValue Concrete)
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. b -> Either a b
Right Eval (GenValue Concrete)
Value
v
         Error ImportErrorMessage
e -> ImportErrorMessage
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. a -> Either a b
Left ImportErrorMessage
e
         Building [Frame]
_ -> ImportErrorMessage
-> Either ImportErrorMessage (Eval (GenValue Concrete))
forall a b. a -> Either a b
Left ImportErrorMessage
PartialValue


--------------------------------------------------------------------------------




modifyState :: ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState :: ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState [Frame] -> Importer
how Ptr ()
ptr =
  do IORef Importer
ref <- StablePtr (IORef Importer) -> IO (IORef Importer)
forall a. StablePtr a -> IO a
deRefStablePtr (Ptr () -> StablePtr (IORef Importer)
forall a. Ptr () -> StablePtr a
castPtrToStablePtr Ptr ()
ptr)
     IORef Importer -> (Importer -> Importer) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Importer
ref \case
       Error ImportErrorMessage
err    -> ImportErrorMessage -> Importer
Error ImportErrorMessage
err
       Done Value
_       -> ImportErrorMessage -> Importer
Error ImportErrorMessage
UnexpectedData
       Building [Frame]
fs  -> [Frame] -> Importer
how [Frame]
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 :: ([Frame] -> IO Importer) -> Ptr () -> IO ()
modifyStateIO [Frame] -> IO Importer
how Ptr ()
ptr =
  do IORef Importer
ref <- StablePtr (IORef Importer) -> IO (IORef Importer)
forall a. StablePtr a -> IO a
deRefStablePtr (Ptr () -> StablePtr (IORef Importer)
forall a. Ptr () -> StablePtr a
castPtrToStablePtr Ptr ()
ptr)
     Importer
builder <- IORef Importer -> IO Importer
forall a. IORef a -> IO a
readIORef IORef Importer
ref
     Importer
newS <- case Importer
builder of
               Error ImportErrorMessage
err    -> Importer -> IO Importer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImportErrorMessage -> Importer
Error ImportErrorMessage
err)
               Done Value
_       -> Importer -> IO Importer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImportErrorMessage -> Importer
Error ImportErrorMessage
UnexpectedData)
               Building [Frame]
fs  -> [Frame] -> IO Importer
how [Frame]
fs
     Importer
newS Importer -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IORef Importer -> Importer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Importer
ref Importer
newS



type Import a = Ptr () -> a -> IO ()

-- | Receive a bool value
cry_bool :: Import Word8
cry_bool :: Import Word8
cry_bool Ptr ()
self Word8
b = ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState (Eval (GenValue Concrete) -> [Frame] -> Importer
Value -> [Frame] -> Importer
haveValue (Eval (GenValue Concrete) -> [Frame] -> Importer)
-> Eval (GenValue Concrete) -> [Frame] -> Importer
forall a b. (a -> b) -> a -> b
$! Eval (GenValue Concrete)
v) Ptr ()
self
  where
  v :: Eval (GenValue Concrete)
v = if Word8
b Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0 then GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit Concrete -> GenValue Concrete
forall sym. SBit sym -> GenValue sym
VBit Bool
SBit Concrete
False) else GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit Concrete -> GenValue Concrete
forall sym. SBit sym -> GenValue sym
VBit Bool
SBit Concrete
True)

-- | Receive a double value
cry_double :: Import Double
cry_double :: Import Double
cry_double Ptr ()
self Double
b = ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState (Double -> [Frame] -> Importer
haveFloat (Double -> [Frame] -> Importer) -> Double -> [Frame] -> Importer
forall a b. (a -> b) -> a -> b
$! Double
b) Ptr ()
self

-- | Receive a small unsigned integer that fits in 64-bits
cry_small_uint :: Import Word64
cry_small_uint :: Import Word64
cry_small_uint Ptr ()
self Word64
i = ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState (Eval (GenValue Concrete) -> [Frame] -> Importer
Value -> [Frame] -> Importer
haveValue (Eval (GenValue Concrete) -> [Frame] -> Importer)
-> Eval (GenValue Concrete) -> [Frame] -> Importer
forall a b. (a -> b) -> a -> b
$! Eval (GenValue Concrete)
v) Ptr ()
self
  where
  v :: Eval (GenValue Concrete)
v = GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue Concrete -> Eval (GenValue Concrete))
-> GenValue Concrete -> Eval (GenValue Concrete)
forall a b. (a -> b) -> a -> b
$! Integer -> GenValue Concrete
SInteger Concrete -> GenValue Concrete
forall sym. SInteger sym -> GenValue sym
VInteger (Integer -> GenValue Concrete) -> Integer -> GenValue Concrete
forall a b. (a -> b) -> a -> b
$! Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger Word64
i

-- | Receive a small signed integer that fits in 64-bits
cry_small_sint :: Import Int64
cry_small_sint :: Import Int64
cry_small_sint Ptr ()
self Int64
i = ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState (Eval (GenValue Concrete) -> [Frame] -> Importer
Value -> [Frame] -> Importer
haveValue (Eval (GenValue Concrete) -> [Frame] -> Importer)
-> Eval (GenValue Concrete) -> [Frame] -> Importer
forall a b. (a -> b) -> a -> b
$! Eval (GenValue Concrete)
v) Ptr ()
self
  where
  v :: Eval (GenValue Concrete)
v = GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue Concrete -> Eval (GenValue Concrete))
-> GenValue Concrete -> Eval (GenValue Concrete)
forall a b. (a -> b) -> a -> b
$! Integer -> GenValue Concrete
SInteger Concrete -> GenValue Concrete
forall sym. SInteger sym -> GenValue sym
VInteger (Integer -> GenValue Concrete) -> Integer -> GenValue Concrete
forall a b. (a -> b) -> a -> b
$! Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
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 :: LargeIntFun
cry_large_int Ptr ()
ptr CSize
sz =
  do MutablePrimArray RealWorld Word64
arr <- Int -> IO (MutablePrimArray (PrimState IO) Word64)
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
Int -> m (MutablePrimArray (PrimState m) a)
newPinnedPrimArray (CSize -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral CSize
sz)
     ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState (\[Frame]
fs -> [Frame] -> Importer
Building (MutablePrimArray (PrimState IO) Word64 -> Frame
NeedSign MutablePrimArray RealWorld Word64
MutablePrimArray (PrimState IO) Word64
arr Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
fs)) Ptr ()
ptr
     Ptr Word64 -> IO (Ptr Word64)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MutablePrimArray RealWorld Word64 -> Ptr Word64
forall s a. MutablePrimArray s a -> Ptr a
mutablePrimArrayContents MutablePrimArray RealWorld Word64
arr)

-- | Finish building a large integer.
-- The argument is 1 for negative, 0 for non-negative.
cry_sign :: Import Word8
cry_sign :: Import Word8
cry_sign Ptr ()
self Word8
sign = ([Frame] -> IO Importer) -> Ptr () -> IO ()
modifyStateIO (Bool -> [Frame] -> IO Importer
haveSign (Word8
sign Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0)) Ptr ()
self

-- | Receive a tag for a sum type.
cry_tag :: Import CSize
cry_tag :: Import CSize
cry_tag Ptr ()
self CSize
c = ([Frame] -> Importer) -> Ptr () -> IO ()
modifyState (Int -> [Frame] -> Importer
haveTag (Int -> [Frame] -> Importer) -> Int -> [Frame] -> Importer
forall a b. (a -> b) -> a -> b
$! CSize -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral CSize
c) Ptr ()
self