{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.FFI.Error where
import Control.DeepSeq
import GHC.Generics
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.Type
data FFITypeError = FFITypeError Type FFITypeErrorReason
deriving (Int -> FFITypeError -> ShowS
[FFITypeError] -> ShowS
FFITypeError -> String
(Int -> FFITypeError -> ShowS)
-> (FFITypeError -> String)
-> ([FFITypeError] -> ShowS)
-> Show FFITypeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FFITypeError -> ShowS
showsPrec :: Int -> FFITypeError -> ShowS
$cshow :: FFITypeError -> String
show :: FFITypeError -> String
$cshowList :: [FFITypeError] -> ShowS
showList :: [FFITypeError] -> ShowS
Show, (forall x. FFITypeError -> Rep FFITypeError x)
-> (forall x. Rep FFITypeError x -> FFITypeError)
-> Generic FFITypeError
forall x. Rep FFITypeError x -> FFITypeError
forall x. FFITypeError -> Rep FFITypeError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FFITypeError -> Rep FFITypeError x
from :: forall x. FFITypeError -> Rep FFITypeError x
$cto :: forall x. Rep FFITypeError x -> FFITypeError
to :: forall x. Rep FFITypeError x -> FFITypeError
Generic, FFITypeError -> ()
(FFITypeError -> ()) -> NFData FFITypeError
forall a. (a -> ()) -> NFData a
$crnf :: FFITypeError -> ()
rnf :: FFITypeError -> ()
NFData)
data FFITypeErrorReason
= FFIBadWordSize
| FFIBadFloatSize
| FFIBadArrayType
| FFIBadComponentTypes [FFITypeError]
| FFIBadType
| FFINotFunction
deriving (Int -> FFITypeErrorReason -> ShowS
[FFITypeErrorReason] -> ShowS
FFITypeErrorReason -> String
(Int -> FFITypeErrorReason -> ShowS)
-> (FFITypeErrorReason -> String)
-> ([FFITypeErrorReason] -> ShowS)
-> Show FFITypeErrorReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FFITypeErrorReason -> ShowS
showsPrec :: Int -> FFITypeErrorReason -> ShowS
$cshow :: FFITypeErrorReason -> String
show :: FFITypeErrorReason -> String
$cshowList :: [FFITypeErrorReason] -> ShowS
showList :: [FFITypeErrorReason] -> ShowS
Show, (forall x. FFITypeErrorReason -> Rep FFITypeErrorReason x)
-> (forall x. Rep FFITypeErrorReason x -> FFITypeErrorReason)
-> Generic FFITypeErrorReason
forall x. Rep FFITypeErrorReason x -> FFITypeErrorReason
forall x. FFITypeErrorReason -> Rep FFITypeErrorReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FFITypeErrorReason -> Rep FFITypeErrorReason x
from :: forall x. FFITypeErrorReason -> Rep FFITypeErrorReason x
$cto :: forall x. Rep FFITypeErrorReason x -> FFITypeErrorReason
to :: forall x. Rep FFITypeErrorReason x -> FFITypeErrorReason
Generic, FFITypeErrorReason -> ()
(FFITypeErrorReason -> ()) -> NFData FFITypeErrorReason
forall a. (a -> ()) -> NFData a
$crnf :: FFITypeErrorReason -> ()
rnf :: FFITypeErrorReason -> ()
NFData)
instance TVars FFITypeError where
apSubst :: Subst -> FFITypeError -> FFITypeError
apSubst Subst
su (FFITypeError Type
t FFITypeErrorReason
r) = Type -> FFITypeErrorReason -> FFITypeError
FFITypeError (Type -> FFITypeErrorReason -> FFITypeError)
-> Type -> FFITypeErrorReason -> FFITypeError
forall a b. (a -> b) -> a -> b
!$ Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t (FFITypeErrorReason -> FFITypeError)
-> FFITypeErrorReason -> FFITypeError
forall a b. (a -> b) -> a -> b
!$ Subst -> FFITypeErrorReason -> FFITypeErrorReason
forall t. TVars t => Subst -> t -> t
apSubst Subst
su FFITypeErrorReason
r
instance TVars FFITypeErrorReason where
apSubst :: Subst -> FFITypeErrorReason -> FFITypeErrorReason
apSubst Subst
su FFITypeErrorReason
r =
case FFITypeErrorReason
r of
FFITypeErrorReason
FFIBadWordSize -> FFITypeErrorReason
r
FFITypeErrorReason
FFIBadFloatSize -> FFITypeErrorReason
r
FFITypeErrorReason
FFIBadArrayType -> FFITypeErrorReason
r
FFIBadComponentTypes [FFITypeError]
errs -> [FFITypeError] -> FFITypeErrorReason
FFIBadComponentTypes ([FFITypeError] -> FFITypeErrorReason)
-> [FFITypeError] -> FFITypeErrorReason
forall a b. (a -> b) -> a -> b
!$ Subst -> [FFITypeError] -> [FFITypeError]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [FFITypeError]
errs
FFITypeErrorReason
FFIBadType -> FFITypeErrorReason
r
FFITypeErrorReason
FFINotFunction -> FFITypeErrorReason
r
instance FVS FFITypeError where
fvs :: FFITypeError -> Set TVar
fvs (FFITypeError Type
t FFITypeErrorReason
r) = (Type, FFITypeErrorReason) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type
t, FFITypeErrorReason
r)
instance FVS FFITypeErrorReason where
fvs :: FFITypeErrorReason -> Set TVar
fvs FFITypeErrorReason
r =
case FFITypeErrorReason
r of
FFITypeErrorReason
FFIBadWordSize -> Set TVar
forall a. Monoid a => a
mempty
FFITypeErrorReason
FFIBadFloatSize -> Set TVar
forall a. Monoid a => a
mempty
FFITypeErrorReason
FFIBadArrayType -> Set TVar
forall a. Monoid a => a
mempty
FFIBadComponentTypes [FFITypeError]
errs -> [FFITypeError] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [FFITypeError]
errs
FFITypeErrorReason
FFIBadType -> Set TVar
forall a. Monoid a => a
mempty
FFITypeErrorReason
FFINotFunction -> Set TVar
forall a. Monoid a => a
mempty
instance PP (WithNames FFITypeError) where
ppPrec :: Int -> WithNames FFITypeError -> Doc
ppPrec Int
_ (WithNames (FFITypeError Type
t FFITypeErrorReason
r) NameMap
names) =
Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Type unsupported for FFI:" Doc -> Doc -> Doc
$$
[Doc] -> Doc
vcat
[ NameMap -> Type -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t
, Doc
"Due to:"
, NameMap -> FFITypeErrorReason -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names FFITypeErrorReason
r ]
instance PP (WithNames FFITypeErrorReason) where
ppPrec :: Int -> WithNames FFITypeErrorReason -> Doc
ppPrec Int
_ (WithNames FFITypeErrorReason
r NameMap
names) =
case FFITypeErrorReason
r of
FFITypeErrorReason
FFIBadWordSize -> [Doc] -> Doc
vcat
[ Doc
"Unsupported word size"
, Doc
"Only words of up to 64 bits are supported" ]
FFITypeErrorReason
FFIBadFloatSize -> [Doc] -> Doc
vcat
[ Doc
"Unsupported Float format"
, Doc
"Only Float32 and Float64 are supported" ]
FFITypeErrorReason
FFIBadArrayType -> [Doc] -> Doc
vcat
[ Doc
"Unsupported sequence element type"
, Doc
"Only words or floats are supported as the element type of"
, Doc
"(possibly multidimensional) sequences"
]
FFIBadComponentTypes [FFITypeError]
errs ->
Int -> Doc -> Doc
indent Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (FFITypeError -> Doc) -> [FFITypeError] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> FFITypeError -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names) [FFITypeError]
errs
FFITypeErrorReason
FFIBadType -> [Doc] -> Doc
vcat
[ Doc
"Only Bit, words, floats, Integer, Z, Rational, sequences, or structs"
, Doc
"or tuples of the above are supported as FFI argument or return types"
]
FFITypeErrorReason
FFINotFunction -> Doc
"FFI binding must be a function"