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