{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE Safe #-}
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
toFFIFunType :: Schema -> Either FFITypeError ([Prop], FFIFunType)
toFFIFunType :: Schema -> Either FFITypeError ([Prop], FFIFunType)
toFFIFunType (Forall [TParam]
params [Prop]
_ Prop
t) =
case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
go forall a b. (a -> b) -> a -> b
$ Bool -> Prop -> Prop
tRebuild' Bool
False Prop
t of
Just (Right ([Prop]
props, FFIFunType
fft)) -> forall a b. b -> Either a b
Right
(forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Prop -> Prop
fin forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Prop
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound) [TParam]
params forall a. [a] -> [a] -> [a]
++ [Prop]
props, FFIFunType
fft)
Just (Left [FFITypeError]
errs) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t forall a b. (a -> b) -> a -> b
$ [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes [FFITypeError]
errs
Maybe (Either [FFITypeError] ([Prop], FFIFunType))
Nothing -> forall a b. a -> Either a b
Left 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]) = 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)) -> forall a b. b -> Either a b
Right
( [Prop]
ps forall a. [a] -> [a] -> [a]
++ [Prop]
ps'
, FFIFunType
ffiFunType
{ ffiArgTypes :: [FFIType]
ffiArgTypes = FFIType
ffiArgType forall a. a -> [a] -> [a]
: FFIFunType -> [FFIType]
ffiArgTypes FFIFunType
ffiFunType } )
Just (Left [FFITypeError]
errs) -> 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) -> forall a b. b -> Either a b
Right
( [Prop]
ps 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 -> forall a b. a -> Either a b
Left [FFITypeError
err]
Left FFITypeError
err -> 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 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
_ = forall a. Maybe a
Nothing
toFFIType :: Type -> Either FFITypeError ([Prop], FFIType)
toFFIType :: Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType Prop
t =
case Prop
t of
TCon (TC TC
TCBit) [] -> 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)) 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) -> (forall a b. (a -> b) -> [a] -> [b]
map Prop -> Prop
fin [Prop]
szs, [Prop] -> FFIBasicType -> FFIType
FFIArray [Prop]
szs FFIBasicType
fbt)) 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 -> forall a b. b -> Either a b
Right ([], FFIBasicType
fbt)
Left FFITypeError
err -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t forall a b. (a -> b) -> a -> b
$ [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes [FFITypeError
err]
go (TCon (TC TC
TCSeq) [Prop
sz, Prop
ty]) = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Prop
szforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> Either FFITypeError ([Prop], FFIBasicType)
go Prop
ty
go Prop
_ = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadArrayType
TCon (TC (TCTuple Int
_)) [Prop]
ts ->
case forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType [Prop]
ts of
([], forall a b. [(a, b)] -> ([a], [b])
unzip -> ([[Prop]]
pss, [FFIType]
fts)) -> forall a b. b -> Either a b
Right (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Prop]]
pss, [FFIType] -> FFIType
FFITuple [FFIType]
fts)
([FFITypeError]
errs, [([Prop], FFIType)]
_) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t forall a b. (a -> b) -> a -> b
$ [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes [FFITypeError]
errs
TRec RecordMap Ident Prop
tMap ->
case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence RecordMap Ident (Either FFITypeError ([Prop], FFIType))
resMap of
Right RecordMap Ident ([Prop], FFIType)
resMap' -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ RecordMap Ident FFIType -> FFIType
FFIRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
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' forall a. [a] -> [a] -> [a]
++ [Prop]
ps, FFIType
ft)) [] RecordMap Ident ([Prop], FFIType)
resMap'
Left FFITypeError
_ -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t forall a b. (a -> b) -> a -> b
$
[FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [a]
lefts forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Either FFITypeError ([Prop], FFIType)
toFFIType RecordMap Ident Prop
tMap
Prop
_ -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadType
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 forall a. Ord a => a -> a -> Bool
<= Integer
8 -> forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord8
| Integer
n forall a. Ord a => a -> a -> Bool
<= Integer
16 -> forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord16
| Integer
n forall a. Ord a => a -> a -> Bool
<= Integer
32 -> forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord32
| Integer
n forall a. Ord a => a -> a -> Bool
<= Integer
64 -> forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
word FFIWordSize
FFIWord64
| Bool
otherwise -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadWordSize
where word :: FFIWordSize -> Maybe (Either a FFIBasicType)
word = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicValType -> FFIBasicType
FFIBasicVal 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) forall a. Eq a => a -> a -> Bool
== (Integer, Integer)
float32ExpPrec -> forall {a}. FFIFloatSize -> Maybe (Either a FFIBasicType)
float FFIFloatSize
FFIFloat32
| (Integer
e, Integer
p) forall a. Eq a => a -> a -> Bool
== (Integer, Integer)
float64ExpPrec -> forall {a}. FFIFloatSize -> Maybe (Either a FFIBasicType)
float FFIFloatSize
FFIFloat64
| Bool
otherwise -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Prop -> FFITypeErrorReason -> FFITypeError
FFITypeError Prop
t FFITypeErrorReason
FFIBadFloatSize
where float :: FFIFloatSize -> Maybe (Either a FFIBasicType)
float = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicValType -> FFIBasicType
FFIBasicVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> FFIFloatSize -> FFIBasicValType
FFIFloat Integer
e Integer
p
TCon (TC TC
TCInteger) [] -> forall {a}. Maybe Prop -> Maybe (Either a FFIBasicType)
integer forall a. Maybe a
Nothing
TCon (TC TC
TCIntMod) [Prop
n] -> forall {a}. Maybe Prop -> Maybe (Either a FFIBasicType)
integer forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Prop
n
TCon (TC TC
TCRational) [] -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ FFIBasicRefType -> FFIBasicType
FFIBasicRef FFIBasicRefType
FFIRational
Prop
_ -> forall a. Maybe a
Nothing
where integer :: Maybe Prop -> Maybe (Either a FFIBasicType)
integer = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFIBasicRefType -> FFIBasicType
FFIBasicRef 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]