content: {-# 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 (Show, Generic, NFData)
  
  data FFITypeErrorReason
    = FFIBadWordSize
    | FFIBadFloatSize
    | FFIBadArrayType
    | FFIBadComponentTypes [FFITypeError]
    | FFIBadType
    | FFINotFunction
    deriving (Show, Generic, NFData)
  
  instance TVars FFITypeError where
    apSubst su (FFITypeError t r) = FFITypeError !$ apSubst su t !$ apSubst su r
  
  instance TVars FFITypeErrorReason where
    apSubst su r =
      case r of
        FFIBadWordSize            -> r
        FFIBadFloatSize           -> r
        FFIBadArrayType           -> r
        FFIBadComponentTypes errs -> FFIBadComponentTypes !$ apSubst su errs
        FFIBadType                -> r
        FFINotFunction            -> r
  
  instance FVS FFITypeError where
    fvs (FFITypeError t r) = fvs (t, r)
  
  instance FVS FFITypeErrorReason where
    fvs r =
      case r of
        FFIBadWordSize            -> mempty
        FFIBadFloatSize           -> mempty
        FFIBadArrayType           -> mempty
        FFIBadComponentTypes errs -> fvs errs
        FFIBadType                -> mempty
        FFINotFunction            -> mempty
  
  instance PP (WithNames FFITypeError) where
    ppPrec _ (WithNames (FFITypeError t r) names) =
      nest 2 $ "Type unsupported for FFI:" $$
        vcat
          [ ppWithNames names t
          , "Due to:"
          , ppWithNames names r ]
  
  instance PP (WithNames FFITypeErrorReason) where
    ppPrec _ (WithNames r names) =
      case r of
        FFIBadWordSize -> vcat
          [ "Unsupported word size"
          , "Only words of up to 64 bits are supported" ]
        FFIBadFloatSize -> vcat
          [ "Unsupported Float format"
          , "Only Float32 and Float64 are supported" ]
        FFIBadArrayType -> vcat
          [ "Unsupported sequence element type"
          , "Only words or floats are supported as the element type of"
          , "(possibly multidimensional) sequences"
          ]
        FFIBadComponentTypes errs ->
          indent 2 $ vcat $ map (ppWithNames names) errs
        FFIBadType -> vcat
          [ "Only Bit, words, floats, Integer, Z, Rational, sequences, or structs"
          , "or tuples of the above are supported as FFI argument or return types"
          ]
        FFINotFunction -> "FFI binding must be a function"
  