{-# 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
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"