{-# LANGUAGE DeriveAnyClass    #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}

-- | Errors from typechecking foreign functions.
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"