{-# 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.TypeCheck.FFI.Error
import           Cryptol.TypeCheck.FFI.FFIType
import           Cryptol.TypeCheck.SimpType
import           Cryptol.TypeCheck.Type
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 :: Schema -> Either FFITypeError ([Prop], FFIFunType)
toFFIFunType :: Schema -> Either FFITypeError ([Prop], FFIFunType)
toFFIFunType (Forall [TParam]
params [Prop]
_ Prop
t) =
  -- Remove all type synonyms and simplify the type before processing it
  case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
go (Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType)))
-> Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
forall a b. (a -> b) -> a -> b
$ Bool -> Prop -> Prop
tRebuild' Bool
False Prop
t of
    Just (Right ([Prop]
props, FFIFunType
fft)) -> ([Prop], FFIFunType) -> Either FFITypeError ([Prop], FFIFunType)
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
fft)
    Just (Left [FFITypeError]
errs) -> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIFunType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
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))
Nothing -> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
forall a b. a -> Either a b
Left (FFITypeError -> Either FFITypeError ([Prop], FFIFunType))
-> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFINotFunction
  where go :: Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
go (TCon (TC TC
TCFun) [Prop
argType, Prop
retType]) = Either [FFITypeError] ([Prop], FFIFunType)
-> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
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))
go Prop
retType of
                Just (Right ([Prop]
ps', FFIFunType
ffiFunType)) -> ([Prop], FFIFunType) -> Either [FFITypeError] ([Prop], FFIFunType)
forall a b. b -> Either a b
Right
                  ( [Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ps'
                  , FFIFunType
ffiFunType
                      { ffiArgTypes = ffiArgType : ffiArgTypes ffiFunType } )
                Just (Left [FFITypeError]
errs) -> [FFITypeError] -> Either [FFITypeError] ([Prop], FFIFunType)
forall a b. a -> Either a b
Left [FFITypeError]
errs
                Maybe (Either [FFITypeError] ([Prop], FFIFunType))
Nothing ->
                  case Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType Prop
retType of
                    Right ([Prop]
ps', FFIType
ffiRetType) -> ([Prop], FFIFunType) -> Either [FFITypeError] ([Prop], FFIFunType)
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)
forall a b. a -> Either a b
Left [FFITypeError
err]
            Left FFITypeError
err -> [FFITypeError] -> Either [FFITypeError] ([Prop], FFIFunType)
forall a b. a -> Either a b
Left
              case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
go Prop
retType of
                Just (Right ([Prop], FFIFunType)
_) -> [FFITypeError
err]
                Just (Left [FFITypeError]
errs) -> FFITypeError
err FFITypeError -> [FFITypeError] -> [FFITypeError]
forall a. a -> [a] -> [a]
: [FFITypeError]
errs
                Maybe (Either [FFITypeError] ([Prop], FFIFunType))
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))
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]