{-# 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FFITypeError] -> ShowS
$cshowList :: [FFITypeError] -> ShowS
show :: FFITypeError -> String
$cshow :: FFITypeError -> String
showsPrec :: Int -> FFITypeError -> ShowS
$cshowsPrec :: Int -> FFITypeError -> ShowS
Show, 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
$cto :: forall x. Rep FFITypeError x -> FFITypeError
$cfrom :: forall x. FFITypeError -> Rep FFITypeError x
Generic, FFITypeError -> ()
forall a. (a -> ()) -> NFData a
rnf :: FFITypeError -> ()
$crnf :: FFITypeError -> ()
NFData)
data FFITypeErrorReason
= FFIBadWordSize
| FFIBadFloatSize
| FFIBadArrayType
| FFIBadComponentTypes [FFITypeError]
| FFIBadType
| FFINotFunction
deriving (Int -> FFITypeErrorReason -> ShowS
[FFITypeErrorReason] -> ShowS
FFITypeErrorReason -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FFITypeErrorReason] -> ShowS
$cshowList :: [FFITypeErrorReason] -> ShowS
show :: FFITypeErrorReason -> String
$cshow :: FFITypeErrorReason -> String
showsPrec :: Int -> FFITypeErrorReason -> ShowS
$cshowsPrec :: Int -> FFITypeErrorReason -> ShowS
Show, 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
$cto :: forall x. Rep FFITypeErrorReason x -> FFITypeErrorReason
$cfrom :: forall x. FFITypeErrorReason -> Rep FFITypeErrorReason x
Generic, FFITypeErrorReason -> ()
forall a. (a -> ()) -> NFData a
rnf :: FFITypeErrorReason -> ()
$crnf :: FFITypeErrorReason -> ()
NFData)
instance TVars FFITypeError where
apSubst :: Subst -> FFITypeError -> FFITypeError
apSubst Subst
su (FFITypeError Type
t FFITypeErrorReason
r) = Type -> FFITypeErrorReason -> FFITypeError
FFITypeError forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t forall a b. (a -> b) -> a -> b
!$ 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 forall a b. (a -> b) -> a -> b
!$ 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) = 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 -> forall a. Monoid a => a
mempty
FFITypeErrorReason
FFIBadFloatSize -> forall a. Monoid a => a
mempty
FFITypeErrorReason
FFIBadArrayType -> forall a. Monoid a => a
mempty
FFIBadComponentTypes [FFITypeError]
errs -> forall t. FVS t => t -> Set TVar
fvs [FFITypeError]
errs
FFITypeErrorReason
FFIBadType -> forall a. Monoid a => a
mempty
FFITypeErrorReason
FFINotFunction -> 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 forall a b. (a -> b) -> a -> b
$ Doc
"Type unsupported for FFI:" Doc -> Doc -> Doc
$$
[Doc] -> Doc
vcat
[ forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names Type
t
, Doc
"Due to:"
, 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 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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"