{-# LANGUAGE BlockArguments  #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ViewPatterns    #-}
{-# LANGUAGE Safe    #-}

-- | Checking and conversion of 'Type's to 'FFIType's.
module Cryptol.TypeCheck.FFI
  ( toFFIFunType
  ) where

import  Data.Bifunctor
import  Data.Containers.ListUtils
import  Data.Either

import Cryptol.Utils.Panic(panic)
import Cryptol.Parser.AST(ForeignMode(..))
import Cryptol.TypeCheck.FFI.Error
import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.TypeCheck.SimpType
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.AST(FFI(..))
import Cryptol.TypeCheck.Subst
import Cryptol.Utils.RecordMap
import Cryptol.Utils.Types


-- | Convert a 'Schema' to a 'FFIFunType', along with any 'Prop's that must be
-- satisfied for the 'FFIFunType' to be valid.
toFFIFunType :: ForeignMode -> Schema -> Either FFITypeError ([Prop], FFI)
toFFIFunType :: ForeignMode -> Schema -> Either FFITypeError ([Prop], FFI)
toFFIFunType ForeignMode
how (Forall [TParam]
params [Prop]
_ Prop
t) =

  case ForeignMode
how of
    ForeignMode
ForeignAbstract -> [TParam] -> Prop -> Either FFITypeError ([Prop], FFI)
checkForeignAbstract [TParam]
params Prop
t
    ForeignMode
ForeignC ->
       -- Remove all type synonyms and simplify the type before processing it
       case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
go (Prop
 -> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType)))
-> Prop
-> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
forall a b. (a -> b) -> a -> b
$ Bool -> Prop -> Prop
tRebuild' Bool
False Prop
t of
         Just (Right ([Prop]
props, FFIFunType FFIType
fft)) -> ([Prop], FFI) -> Either FFITypeError ([Prop], FFI)
forall a b. b -> Either a b
Right
           -- Remove duplicate constraints
           ([Prop] -> [Prop]
forall a. Ord a => [a] -> [a]
nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ (TParam -> Prop) -> [TParam] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Prop -> Prop
fin (Prop -> Prop) -> (TParam -> Prop) -> TParam -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Prop
TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound) [TParam]
params [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
props, FFIFunType FFIType -> FFI
CallC FFIFunType FFIType
fft)
         Just (Left [FFITypeError]
errs) -> FFITypeError -> Either FFITypeError ([Prop], FFI)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFI))
-> FFITypeError -> Either FFITypeError ([Prop], FFI)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t (FFITypeErrorReason -> FFITypeError)
-> FFITypeErrorReason -> FFITypeError
forall a b. (a -> b) -> a -> b
$ [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes [FFITypeError]
errs
         Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
Nothing -> FFITypeError -> Either FFITypeError ([Prop], FFI)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFI))
-> FFITypeError -> Either FFITypeError ([Prop], FFI)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFINotFunction
  where go :: Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
go (TCon (TC TC
TCFun) [Prop
argType, Prop
retType]) = Either [FFITypeError] ([Prop], FFIFunType FFIType)
-> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
forall a. a -> Maybe a
Just
          case Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType Prop
argType of
            Right ([Prop]
ps, FFIType
ffiArgType) ->
              case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
go Prop
retType of
                Just (Right ([Prop]
ps', FFIFunType FFIType
ffiFunType)) -> ([Prop], FFIFunType FFIType)
-> Either [FFITypeError] ([Prop], FFIFunType FFIType)
forall a b. b -> Either a b
Right
                  ( [Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ps'
                  , FFIFunType FFIType
ffiFunType
                      { ffiArgTypes = ffiArgType : ffiArgTypes ffiFunType } )
                Just (Left [FFITypeError]
errs) -> [FFITypeError]
-> Either [FFITypeError] ([Prop], FFIFunType FFIType)
forall a b. a -> Either a b
Left [FFITypeError]
errs
                Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
Nothing ->
                  case Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType Prop
retType of
                    Right ([Prop]
ps', FFIType
ffiRetType) -> ([Prop], FFIFunType FFIType)
-> Either [FFITypeError] ([Prop], FFIFunType FFIType)
forall a b. b -> Either a b
Right
                      ( [Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ps'
                      , FFIFunType
                          { ffiTParams :: [TParam]
ffiTParams = [TParam]
params
                          , ffiArgTypes :: [FFIType]
ffiArgTypes = [FFIType
ffiArgType], FFIType
ffiRetType :: FFIType
ffiRetType :: FFIType
.. } )
                    Left FFITypeError
err -> [FFITypeError]
-> Either [FFITypeError] ([Prop], FFIFunType FFIType)
forall a b. a -> Either a b
Left [FFITypeError
err]
            Left FFITypeError
err -> [FFITypeError]
-> Either [FFITypeError] ([Prop], FFIFunType FFIType)
forall a b. a -> Either a b
Left
              case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
go Prop
retType of
                Just (Right ([Prop], FFIFunType FFIType)
_) -> [FFITypeError
err]
                Just (Left [FFITypeError]
errs) -> FFITypeError
err FFITypeError -> [FFITypeError] -> [FFITypeError]
forall a. a -> [a] -> [a]
: [FFITypeError]
errs
                Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
Nothing ->
                  case Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType Prop
retType of
                    Right ([Prop], FFIType)
_   -> [FFITypeError
err]
                    Left FFITypeError
err' -> [FFITypeError
err, FFITypeError
err']
        go Prop
_ = Maybe (Either [FFITypeError] ([Prop], FFIFunType FFIType))
forall a. Maybe a
Nothing

-- | Convert a 'Type' to a 'FFIType', along with any 'Prop's that must be
-- satisfied for the 'FFIType' to be valid.
toFFIType :: Type -> Either FFITypeError ([Prop], FFIType)
toFFIType :: Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType Prop
t =
  case Prop
t of
    TCon (TC TC
TCBit) [] -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
forall a b. b -> Either a b
Right ([], FFIType
FFIBool)
    (Prop -> Maybe (Either FFITypeError FFIBasicType)
toFFIBasicType -> Just Either FFITypeError FFIBasicType
r) -> (\FFIBasicType
fbt -> ([], FFIBasicType -> FFIType
FFIBasic FFIBasicType
fbt)) (FFIBasicType -> ([Prop], FFIType))
-> Either FFITypeError FFIBasicType
-> Either FFITypeError ([Prop], FFIType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either FFITypeError FFIBasicType
r
    TCon (TC TC
TCSeq) [Prop]
_ ->
      (\([Prop]
szs, FFIBasicType
fbt) -> ((Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Prop
fin [Prop]
szs, [Prop] -> FFIBasicType -> FFIType
FFIArray [Prop]
szs FFIBasicType
fbt)) (([Prop], FFIBasicType) -> ([Prop], FFIType))
-> Either FFITypeError ([Prop], FFIBasicType)
-> Either FFITypeError ([Prop], FFIType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> Either FFITypeError ([Prop], FFIBasicType)
go Prop
t
      where go :: Prop -> Either FFITypeError ([Prop], FFIBasicType)
go (Prop -> Maybe (Either FFITypeError FFIBasicType)
toFFIBasicType -> Just Either FFITypeError FFIBasicType
r) =
              case Either FFITypeError FFIBasicType
r of
                Right FFIBasicType
fbt -> ([Prop], FFIBasicType)
-> Either FFITypeError ([Prop], FFIBasicType)
forall a b. b -> Either a b
Right ([], FFIBasicType
fbt)
                Left FFITypeError
err  -> FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIBasicType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t (FFITypeErrorReason -> FFITypeError)
-> FFITypeErrorReason -> FFITypeError
forall a b. (a -> b) -> a -> b
$ [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes [FFITypeError
err]
            go (TCon (TC TC
TCSeq) [Prop
sz, Prop
ty]) = ([Prop] -> [Prop])
-> ([Prop], FFIBasicType) -> ([Prop], FFIBasicType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Prop
szProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:) (([Prop], FFIBasicType) -> ([Prop], FFIBasicType))
-> Either FFITypeError ([Prop], FFIBasicType)
-> Either FFITypeError ([Prop], FFIBasicType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> Either FFITypeError ([Prop], FFIBasicType)
go Prop
ty
            go Prop
_ = FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIBasicType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadArrayType
    TCon (TC (TCTuple Int
_)) [Prop]
ts ->
      case [Either FFITypeError ([Prop], FFIType)]
-> ([FFITypeError], [([Prop], FFIType)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either FFITypeError ([Prop], FFIType)]
 -> ([FFITypeError], [([Prop], FFIType)]))
-> [Either FFITypeError ([Prop], FFIType)]
-> ([FFITypeError], [([Prop], FFIType)])
forall a b. (a -> b) -> a -> b
$ (Prop -> Either FFITypeError ([Prop], FFIType))
-> [Prop] -> [Either FFITypeError ([Prop], FFIType)]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType [Prop]
ts of
        ([], [([Prop], FFIType)] -> ([[Prop]], [FFIType])
forall a b. [(a, b)] -> ([a], [b])
unzip -> ([[Prop]]
pss, [FFIType]
fts)) -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
forall a b. b -> Either a b
Right ([[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Prop]]
pss, [FFIType] -> FFIType
FFITuple [FFIType]
fts)
        ([FFITypeError]
errs, [([Prop], FFIType)]
_) -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIType)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t (FFITypeErrorReason -> FFITypeError)
-> FFITypeErrorReason -> FFITypeError
forall a b. (a -> b) -> a -> b
$ [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes [FFITypeError]
errs
    TRec RecordMap Ident Prop
tMap ->
      case RecordMap Ident (Either FFITypeError ([Prop], FFIType))
-> Either FFITypeError (RecordMap Ident ([Prop], FFIType))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Monad m =>
RecordMap Ident (m a) -> m (RecordMap Ident a)
sequence RecordMap Ident (Either FFITypeError ([Prop], FFIType))
resMap of
        Right RecordMap Ident ([Prop], FFIType)
resMap' -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
forall a b. b -> Either a b
Right (([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType))
-> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
forall a b. (a -> b) -> a -> b
$ RecordMap Ident FFIType -> FFIType
FFIRecord (RecordMap Ident FFIType -> FFIType)
-> ([Prop], RecordMap Ident FFIType) -> ([Prop], FFIType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          ([Prop] -> ([Prop], FFIType) -> ([Prop], FFIType))
-> [Prop]
-> RecordMap Ident ([Prop], FFIType)
-> ([Prop], RecordMap Ident FFIType)
forall a b c k.
(a -> b -> (a, c)) -> a -> RecordMap k b -> (a, RecordMap k c)
recordMapAccum (\[Prop]
ps ([Prop]
ps', FFIType
ft) -> ([Prop]
ps' [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ps, FFIType
ft)) [] RecordMap Ident ([Prop], FFIType)
resMap'
        Left FFITypeError
_ -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIType)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t (FFITypeErrorReason -> FFITypeError)
-> FFITypeErrorReason -> FFITypeError
forall a b. (a -> b) -> a -> b
$
          [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes ([FFITypeError] -> FFITypeErrorReason)
-> [FFITypeError] -> FFITypeErrorReason
forall a b. (a -> b) -> a -> b
$ [Either FFITypeError ([Prop], FFIType)] -> [FFITypeError]
forall a b. [Either a b] -> [a]
lefts ([Either FFITypeError ([Prop], FFIType)] -> [FFITypeError])
-> [Either FFITypeError ([Prop], FFIType)] -> [FFITypeError]
forall a b. (a -> b) -> a -> b
$ RecordMap Ident (Either FFITypeError ([Prop], FFIType))
-> [Either FFITypeError ([Prop], FFIType)]
forall a b. (Show a, Ord a) => RecordMap a b -> [b]
displayElements RecordMap Ident (Either FFITypeError ([Prop], FFIType))
resMap
      where resMap :: RecordMap Ident (Either FFITypeError ([Prop], FFIType))
resMap = (Prop -> Either FFITypeError ([Prop], FFIType))
-> RecordMap Ident Prop
-> RecordMap Ident (Either FFITypeError ([Prop], FFIType))
forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType RecordMap Ident Prop
tMap
    Prop
_ -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIType)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadType

-- | Convert a 'Type' to a 'FFIBasicType', returning 'Nothing' if it isn't a
-- basic type and 'Left' if it is but there was some other issue with it.
toFFIBasicType :: Type -> Maybe (Either FFITypeError FFIBasicType)
toFFIBasicType :: Prop -> Maybe (Either FFITypeError FFIBasicType)
toFFIBasicType Prop
t =
  case Prop
t of
    TCon (TC TC
TCSeq) [TCon (TC (TCNum Integer
n)) [], TCon (TC TC
TCBit) []]
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
8 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord8
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
16 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord16
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
32 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord32
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
64 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord64
      | Bool
otherwise -> Either FFITypeError FFIBasicType
-> Maybe (Either FFITypeError FFIBasicType)
forall a. a -> Maybe a
Just (Either FFITypeError FFIBasicType
 -> Maybe (Either FFITypeError FFIBasicType))
-> Either FFITypeError FFIBasicType
-> Maybe (Either FFITypeError FFIBasicType)
forall a b. (a -> b) -> a -> b
$ FFITypeError -> Either FFITypeError FFIBasicType
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError FFIBasicType)
-> FFITypeError -> Either FFITypeError FFIBasicType
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadWordSize
      where word :: FFIWordSize -> Maybe (Either a FFIBasicType)
word = Either a FFIBasicType -> Maybe (Either a FFIBasicType)
forall a. a -> Maybe a
Just (Either a FFIBasicType -> Maybe (Either a FFIBasicType))
-> (FFIWordSize -> Either a FFIBasicType)
-> FFIWordSize
-> Maybe (Either a FFIBasicType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicType -> Either a FFIBasicType
forall a b. b -> Either a b
Right (FFIBasicType -> Either a FFIBasicType)
-> (FFIWordSize -> FFIBasicType)
-> FFIWordSize
-> Either a FFIBasicType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicValType -> FFIBasicType
FFIBasicVal (FFIBasicValType -> FFIBasicType)
-> (FFIWordSize -> FFIBasicValType) -> FFIWordSize -> FFIBasicType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> FFIWordSize -> FFIBasicValType
FFIWord Integer
n
    TCon (TC TC
TCFloat) [TCon (TC (TCNum Integer
e)) [], TCon (TC (TCNum Integer
p)) []]
      | (Integer
e, Integer
p) (Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer, Integer)
float32ExpPrec -> FFIFloatSize -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. FFIFloatSize -> Maybe (Either a FFIBasicType)
float FFIFloatSize
FFIFloat32
      | (Integer
e, Integer
p) (Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer, Integer)
float64ExpPrec -> FFIFloatSize -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. FFIFloatSize -> Maybe (Either a FFIBasicType)
float FFIFloatSize
FFIFloat64
      | Bool
otherwise -> Either FFITypeError FFIBasicType
-> Maybe (Either FFITypeError FFIBasicType)
forall a. a -> Maybe a
Just (Either FFITypeError FFIBasicType
 -> Maybe (Either FFITypeError FFIBasicType))
-> Either FFITypeError FFIBasicType
-> Maybe (Either FFITypeError FFIBasicType)
forall a b. (a -> b) -> a -> b
$ FFITypeError -> Either FFITypeError FFIBasicType
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError FFIBasicType)
-> FFITypeError -> Either FFITypeError FFIBasicType
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadFloatSize
      where float :: FFIFloatSize -> Maybe (Either a FFIBasicType)
float = Either a FFIBasicType -> Maybe (Either a FFIBasicType)
forall a. a -> Maybe a
Just (Either a FFIBasicType -> Maybe (Either a FFIBasicType))
-> (FFIFloatSize -> Either a FFIBasicType)
-> FFIFloatSize
-> Maybe (Either a FFIBasicType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicType -> Either a FFIBasicType
forall a b. b -> Either a b
Right (FFIBasicType -> Either a FFIBasicType)
-> (FFIFloatSize -> FFIBasicType)
-> FFIFloatSize
-> Either a FFIBasicType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicValType -> FFIBasicType
FFIBasicVal (FFIBasicValType -> FFIBasicType)
-> (FFIFloatSize -> FFIBasicValType)
-> FFIFloatSize
-> FFIBasicType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> FFIFloatSize -> FFIBasicValType
FFIFloat Integer
e Integer
p
    TCon (TC TC
TCInteger) [] -> Maybe Prop -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. Maybe Prop -> Maybe (Either a FFIBasicType)
integer Maybe Prop
forall a. Maybe a
Nothing
    TCon (TC TC
TCIntMod) [Prop
n] -> Maybe Prop -> Maybe (Either FFITypeError FFIBasicType)
forall {a}. Maybe Prop -> Maybe (Either a FFIBasicType)
integer (Maybe Prop -> Maybe (Either FFITypeError FFIBasicType))
-> Maybe Prop -> Maybe (Either FFITypeError FFIBasicType)
forall a b. (a -> b) -> a -> b
$ Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
n
    TCon (TC TC
TCRational) [] -> Either FFITypeError FFIBasicType
-> Maybe (Either FFITypeError FFIBasicType)
forall a. a -> Maybe a
Just (Either FFITypeError FFIBasicType
 -> Maybe (Either FFITypeError FFIBasicType))
-> Either FFITypeError FFIBasicType
-> Maybe (Either FFITypeError FFIBasicType)
forall a b. (a -> b) -> a -> b
$ FFIBasicType -> Either FFITypeError FFIBasicType
forall a b. b -> Either a b
Right (FFIBasicType -> Either FFITypeError FFIBasicType)
-> FFIBasicType -> Either FFITypeError FFIBasicType
forall a b. (a -> b) -> a -> b
$ FFIBasicRefType -> FFIBasicType
FFIBasicRef FFIBasicRefType
FFIRational
    Prop
_ -> Maybe (Either FFITypeError FFIBasicType)
forall a. Maybe a
Nothing
  where integer :: Maybe Prop -> Maybe (Either a FFIBasicType)
integer = Either a FFIBasicType -> Maybe (Either a FFIBasicType)
forall a. a -> Maybe a
Just (Either a FFIBasicType -> Maybe (Either a FFIBasicType))
-> (Maybe Prop -> Either a FFIBasicType)
-> Maybe Prop
-> Maybe (Either a FFIBasicType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicType -> Either a FFIBasicType
forall a b. b -> Either a b
Right (FFIBasicType -> Either a FFIBasicType)
-> (Maybe Prop -> FFIBasicType)
-> Maybe Prop
-> Either a FFIBasicType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicRefType -> FFIBasicType
FFIBasicRef (FFIBasicRefType -> FFIBasicType)
-> (Maybe Prop -> FFIBasicRefType) -> Maybe Prop -> FFIBasicType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Prop -> FFIBasicRefType
FFIInteger

fin :: Type -> Prop
fin :: Prop -> Prop
fin Prop
t = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PFin) [Prop
t]


-- XXX: eliminate stuff we know will not work at runtime
checkForeignAbstract :: [TParam] -> Type -> Either FFITypeError ([Prop], FFI)
checkForeignAbstract :: [TParam] -> Prop -> Either FFITypeError ([Prop], FFI)
checkForeignAbstract [TParam]
params Prop
t =
  do [Prop]
fromArgs <- [Prop] -> Either FFITypeError [Prop]
forall (t :: * -> *).
Traversable t =>
t Prop -> Either FFITypeError [Prop]
validForeignAbstractTypes [Prop]
args
     [Prop]
fromRes <- Prop -> Either FFITypeError [Prop]
validForeignAbstractType Prop
res
     ([Prop], FFI) -> Either FFITypeError ([Prop], FFI)
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [Prop]
fromRes [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
fromArgs
          , FFIFunType Prop -> FFI
CallAbstract
              FFIFunType { ffiTParams :: [TParam]
ffiTParams = [TParam]
params
                         , ffiArgTypes :: [Prop]
ffiArgTypes = [Prop]
args
                         , ffiRetType :: Prop
ffiRetType = Prop
res }
          )
  where
  ([Prop]
args,Prop
res) = Prop -> ([Prop], Prop)
go Prop
t
  go :: Prop -> ([Prop], Prop)
go Prop
ty =
    case Prop -> Maybe (Prop, Prop)
tIsFun Prop
ty of
      Just (Prop
a,Prop
r) ->
        let ([Prop]
bs,Prop
r1) = Prop -> ([Prop], Prop)
go Prop
r
        in (Prop
aProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop]
bs,Prop
r1)
      Maybe (Prop, Prop)
Nothing -> ([],Prop
ty)



validForeignAbstractTypes ::
 Traversable t => t Type -> Either FFITypeError [Prop]
validForeignAbstractTypes :: forall (t :: * -> *).
Traversable t =>
t Prop -> Either FFITypeError [Prop]
validForeignAbstractTypes t Prop
ts = t [Prop] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (t [Prop] -> [Prop])
-> Either FFITypeError (t [Prop]) -> Either FFITypeError [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Prop -> Either FFITypeError [Prop])
-> t Prop -> Either FFITypeError (t [Prop])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
traverse Prop -> Either FFITypeError [Prop]
validForeignAbstractType t Prop
ts

validForeignAbstractType :: Type -> Either FFITypeError [Prop]
validForeignAbstractType :: Prop -> Either FFITypeError [Prop]
validForeignAbstractType Prop
t =
  let nope :: FFITypeErrorReason -> Either FFITypeError b
nope = FFITypeError -> Either FFITypeError b
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError b)
-> (FFITypeErrorReason -> FFITypeError)
-> FFITypeErrorReason
-> Either FFITypeError b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t
  in
  case Prop
t of
    TCon TCon
c [Prop]
ts ->
      case TCon
c of
        PC {} -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"PC"
        TF {} -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"TF"
        TError {} -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"TError"
        TC TC
tc ->
         case TC
tc of
           TCNum {} -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"TCNum"
           TCInf {} -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"TCInf"
           TC
TCBit    -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []   
           TC
TCInteger -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] 
           TC
TCFloat ->
             case [Prop]
ts of
               [Prop
e',Prop
p'] ->
                 case (Prop -> Maybe Integer
tIsNum Prop
e', Prop -> Maybe Integer
tIsNum Prop
p') of
                   (Just Integer
e, Just Integer
p)
                     | (Integer
e, Integer
p) (Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer, Integer)
float32ExpPrec -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                     | (Integer
e, Integer
p) (Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer, Integer)
float64ExpPrec -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                   (Maybe Integer, Maybe Integer)
_ -> FFITypeErrorReason -> Either FFITypeError [Prop]
forall {b}. FFITypeErrorReason -> Either FFITypeError b
nope FFITypeErrorReason
FFIBadFloatSize
               [Prop]
_ -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"TCFloat"
           TC
TCIntMod -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
           TC
TCRational -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []    
           TC
TCArray -> FFITypeErrorReason -> Either FFITypeError [Prop]
forall {b}. FFITypeErrorReason -> Either FFITypeError b
nope FFITypeErrorReason
FFIBadType
           TC
TCSeq ->
             case [Prop]
ts of
               [Prop
len,Prop
el] ->
                  do [Prop]
ps <- Prop -> Either FFITypeError [Prop]
validForeignAbstractType Prop
el
                     let prop :: Prop
prop = Prop -> Prop
pFin Prop
len
                     case Prop -> Maybe Prop
tIsError Prop
prop of
                       Just Prop
err -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop
err Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
ps)
                       Maybe Prop
Nothing -> [Prop] -> Either FFITypeError [Prop]
forall a. a -> Either FFITypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop
prop Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
ps)
               [Prop]
_ -> String -> Either FFITypeError [Prop]
forall {a}. String -> a
bad String
"TCSeq"
           TC
TCFun -> FFITypeErrorReason -> Either FFITypeError [Prop]
forall {b}. FFITypeErrorReason -> Either FFITypeError b
nope FFITypeErrorReason
FFIBadType
           TCTuple {} -> [Prop] -> Either FFITypeError [Prop]
forall (t :: * -> *).
Traversable t =>
t Prop -> Either FFITypeError [Prop]
validForeignAbstractTypes [Prop]
ts
           
    TVar {} -> FFITypeErrorReason -> Either FFITypeError [Prop]
forall {b}. FFITypeErrorReason -> Either FFITypeError b
nope FFITypeErrorReason
FFIBadType
    TUser Name
_ [Prop]
_ Prop
t1 -> Prop -> Either FFITypeError [Prop]
validForeignAbstractType Prop
t1
    TRec RecordMap Ident Prop
rs -> RecordMap Ident Prop -> Either FFITypeError [Prop]
forall (t :: * -> *).
Traversable t =>
t Prop -> Either FFITypeError [Prop]
validForeignAbstractTypes RecordMap Ident Prop
rs
    TNominal NominalType
nm [Prop]
ts ->
      let su :: Subst
su = [(TParam, Prop)] -> Subst
listParamSubst (NominalType -> [TParam]
ntParams NominalType
nm [TParam] -> [Prop] -> [(TParam, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Prop]
ts) in
      Prop -> Subst -> NominalTypeDef -> Either FFITypeError [Prop]
validForeignAbstractNominalType Prop
t Subst
su (NominalType -> NominalTypeDef
ntDef NominalType
nm)
  where
  bad :: String -> a
bad String
msg = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"validOfreignAbstactType" [String
msg]

validForeignAbstractNominalType ::
  Type -> Subst -> NominalTypeDef -> Either FFITypeError[Prop]
validForeignAbstractNominalType :: Prop -> Subst -> NominalTypeDef -> Either FFITypeError [Prop]
validForeignAbstractNominalType Prop
ty Subst
su NominalTypeDef
def =
  case NominalTypeDef
def of
    Struct StructCon
sc -> [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Prop]] -> [Prop])
-> Either FFITypeError [[Prop]] -> Either FFITypeError [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Prop -> Either FFITypeError [Prop])
-> [Prop] -> Either FFITypeError [[Prop]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Prop -> Either FFITypeError [Prop]
validT (RecordMap Ident Prop -> [Prop]
forall a b. RecordMap a b -> [b]
recordElements (StructCon -> RecordMap Ident Prop
ntFields StructCon
sc))
    Enum [EnumCon]
cs -> [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Prop]] -> [Prop])
-> Either FFITypeError [[Prop]] -> Either FFITypeError [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EnumCon -> Either FFITypeError [Prop])
-> [EnumCon] -> Either FFITypeError [[Prop]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse EnumCon -> Either FFITypeError [Prop]
validCon [EnumCon]
cs
    NominalTypeDef
Abstract -> FFITypeError -> Either FFITypeError [Prop]
forall a b. a -> Either a b
Left (Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
ty FFITypeErrorReason
FFIBadType)
  where
  validT :: Prop -> Either FFITypeError [Prop]
validT Prop
t = Prop -> Either FFITypeError [Prop]
validForeignAbstractType (Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
t)
  validCon :: EnumCon -> Either FFITypeError [Prop]
validCon EnumCon
c = [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Prop]] -> [Prop])
-> Either FFITypeError [[Prop]] -> Either FFITypeError [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Prop -> Either FFITypeError [Prop])
-> [Prop] -> Either FFITypeError [[Prop]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Prop -> Either FFITypeError [Prop]
validT (EnumCon -> [Prop]
ecFields EnumCon
c)