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

    -- | This module defines a nicer intermediate representation of Cryptol types
    -- allowed for the FFI, which the typechecker generates then stores in the AST.
    -- This way the FFI evaluation code does not have to examine the raw type
    -- signatures again.
    module Cryptol.TypeCheck.FFI.FFIType where

    import           Control.DeepSeq
    import           GHC.Generics

    import           Cryptol.TypeCheck.Type
    import           Cryptol.Utils.Ident
    import           Cryptol.Utils.RecordMap

    -- | Type of a foreign function.
    data FFIFunType = FFIFunType
      { -- | Note: any type variables within this function type must be bound here.
        FFIFunType -> [TParam]
    ffiTParams  :: [TParam]
      , FFIFunType -> [FFIType]
    ffiArgTypes :: [FFIType]
      , FFIFunType -> FFIType
    ffiRetType  :: FFIType }
      deriving (Int -> FFIFunType -> ShowS
    [FFIFunType] -> ShowS
    FFIFunType -> String
    (Int -> FFIFunType -> ShowS)
    -> (FFIFunType -> String)
    -> ([FFIFunType] -> ShowS)
    -> Show FFIFunType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIFunType -> ShowS
    showsPrec :: Int -> FFIFunType -> ShowS
    $cshow :: FFIFunType -> String
    show :: FFIFunType -> String
    $cshowList :: [FFIFunType] -> ShowS
    showList :: [FFIFunType] -> ShowS
    Show, (forall x. FFIFunType -> Rep FFIFunType x)
    -> (forall x. Rep FFIFunType x -> FFIFunType) -> Generic FFIFunType
    forall x. Rep FFIFunType x -> FFIFunType
    forall x. FFIFunType -> Rep FFIFunType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIFunType -> Rep FFIFunType x
    from :: forall x. FFIFunType -> Rep FFIFunType x
    $cto :: forall x. Rep FFIFunType x -> FFIFunType
    to :: forall x. Rep FFIFunType x -> FFIFunType
    Generic, FFIFunType -> ()
    (FFIFunType -> ()) -> NFData FFIFunType
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIFunType -> ()
    rnf :: FFIFunType -> ()
    NFData)

    -- | Type of a value that can be passed to or returned from a foreign function.
    data FFIType
      = FFIBool
      | FFIBasic FFIBasicType
      -- | [n][m][p]T --> FFIArray [n, m, p] T
      | FFIArray [Type] FFIBasicType
      | FFITuple [FFIType]
      | FFIRecord (RecordMap Ident FFIType)
      deriving (Int -> FFIType -> ShowS
    [FFIType] -> ShowS
    FFIType -> String
    (Int -> FFIType -> ShowS)
    -> (FFIType -> String) -> ([FFIType] -> ShowS) -> Show FFIType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIType -> ShowS
    showsPrec :: Int -> FFIType -> ShowS
    $cshow :: FFIType -> String
    show :: FFIType -> String
    $cshowList :: [FFIType] -> ShowS
    showList :: [FFIType] -> ShowS
    Show, (forall x. FFIType -> Rep FFIType x)
    -> (forall x. Rep FFIType x -> FFIType) -> Generic FFIType
    forall x. Rep FFIType x -> FFIType
    forall x. FFIType -> Rep FFIType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIType -> Rep FFIType x
    from :: forall x. FFIType -> Rep FFIType x
    $cto :: forall x. Rep FFIType x -> FFIType
    to :: forall x. Rep FFIType x -> FFIType
    Generic, FFIType -> ()
    (FFIType -> ()) -> NFData FFIType
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIType -> ()
    rnf :: FFIType -> ()
    NFData)

    -- | Types which can be elements of FFI arrays.
    data FFIBasicType
      = FFIBasicVal FFIBasicValType
      | FFIBasicRef FFIBasicRefType
      deriving (Int -> FFIBasicType -> ShowS
    [FFIBasicType] -> ShowS
    FFIBasicType -> String
    (Int -> FFIBasicType -> ShowS)
    -> (FFIBasicType -> String)
    -> ([FFIBasicType] -> ShowS)
    -> Show FFIBasicType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIBasicType -> ShowS
    showsPrec :: Int -> FFIBasicType -> ShowS
    $cshow :: FFIBasicType -> String
    show :: FFIBasicType -> String
    $cshowList :: [FFIBasicType] -> ShowS
    showList :: [FFIBasicType] -> ShowS
    Show, (forall x. FFIBasicType -> Rep FFIBasicType x)
    -> (forall x. Rep FFIBasicType x -> FFIBasicType)
    -> Generic FFIBasicType
    forall x. Rep FFIBasicType x -> FFIBasicType
    forall x. FFIBasicType -> Rep FFIBasicType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIBasicType -> Rep FFIBasicType x
    from :: forall x. FFIBasicType -> Rep FFIBasicType x
    $cto :: forall x. Rep FFIBasicType x -> FFIBasicType
    to :: forall x. Rep FFIBasicType x -> FFIBasicType
    Generic, FFIBasicType -> ()
    (FFIBasicType -> ()) -> NFData FFIBasicType
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIBasicType -> ()
    rnf :: FFIBasicType -> ()
    NFData)

    -- | Basic type which is passed and returned directly by value.
    data FFIBasicValType
      = FFIWord
          Integer     -- ^ The size of the Cryptol type
          FFIWordSize -- ^ The machine word size that it corresponds to
      | FFIFloat
          Integer      -- ^ Exponent
          Integer      -- ^ Precision
          FFIFloatSize -- ^ The machine float size that it corresponds to
      deriving (Int -> FFIBasicValType -> ShowS
    [FFIBasicValType] -> ShowS
    FFIBasicValType -> String
    (Int -> FFIBasicValType -> ShowS)
    -> (FFIBasicValType -> String)
    -> ([FFIBasicValType] -> ShowS)
    -> Show FFIBasicValType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIBasicValType -> ShowS
    showsPrec :: Int -> FFIBasicValType -> ShowS
    $cshow :: FFIBasicValType -> String
    show :: FFIBasicValType -> String
    $cshowList :: [FFIBasicValType] -> ShowS
    showList :: [FFIBasicValType] -> ShowS
    Show, (forall x. FFIBasicValType -> Rep FFIBasicValType x)
    -> (forall x. Rep FFIBasicValType x -> FFIBasicValType)
    -> Generic FFIBasicValType
    forall x. Rep FFIBasicValType x -> FFIBasicValType
    forall x. FFIBasicValType -> Rep FFIBasicValType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIBasicValType -> Rep FFIBasicValType x
    from :: forall x. FFIBasicValType -> Rep FFIBasicValType x
    $cto :: forall x. Rep FFIBasicValType x -> FFIBasicValType
    to :: forall x. Rep FFIBasicValType x -> FFIBasicValType
    Generic, FFIBasicValType -> ()
    (FFIBasicValType -> ()) -> NFData FFIBasicValType
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIBasicValType -> ()
    rnf :: FFIBasicValType -> ()
    NFData)

    data FFIWordSize
      = FFIWord8
      | FFIWord16
      | FFIWord32
      | FFIWord64
      deriving (Int -> FFIWordSize -> ShowS
    [FFIWordSize] -> ShowS
    FFIWordSize -> String
    (Int -> FFIWordSize -> ShowS)
    -> (FFIWordSize -> String)
    -> ([FFIWordSize] -> ShowS)
    -> Show FFIWordSize
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIWordSize -> ShowS
    showsPrec :: Int -> FFIWordSize -> ShowS
    $cshow :: FFIWordSize -> String
    show :: FFIWordSize -> String
    $cshowList :: [FFIWordSize] -> ShowS
    showList :: [FFIWordSize] -> ShowS
    Show, (forall x. FFIWordSize -> Rep FFIWordSize x)
    -> (forall x. Rep FFIWordSize x -> FFIWordSize)
    -> Generic FFIWordSize
    forall x. Rep FFIWordSize x -> FFIWordSize
    forall x. FFIWordSize -> Rep FFIWordSize x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIWordSize -> Rep FFIWordSize x
    from :: forall x. FFIWordSize -> Rep FFIWordSize x
    $cto :: forall x. Rep FFIWordSize x -> FFIWordSize
    to :: forall x. Rep FFIWordSize x -> FFIWordSize
    Generic, FFIWordSize -> ()
    (FFIWordSize -> ()) -> NFData FFIWordSize
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIWordSize -> ()
    rnf :: FFIWordSize -> ()
    NFData)

    data FFIFloatSize
      = FFIFloat32
      | FFIFloat64
      deriving (Int -> FFIFloatSize -> ShowS
    [FFIFloatSize] -> ShowS
    FFIFloatSize -> String
    (Int -> FFIFloatSize -> ShowS)
    -> (FFIFloatSize -> String)
    -> ([FFIFloatSize] -> ShowS)
    -> Show FFIFloatSize
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIFloatSize -> ShowS
    showsPrec :: Int -> FFIFloatSize -> ShowS
    $cshow :: FFIFloatSize -> String
    show :: FFIFloatSize -> String
    $cshowList :: [FFIFloatSize] -> ShowS
    showList :: [FFIFloatSize] -> ShowS
    Show, (forall x. FFIFloatSize -> Rep FFIFloatSize x)
    -> (forall x. Rep FFIFloatSize x -> FFIFloatSize)
    -> Generic FFIFloatSize
    forall x. Rep FFIFloatSize x -> FFIFloatSize
    forall x. FFIFloatSize -> Rep FFIFloatSize x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIFloatSize -> Rep FFIFloatSize x
    from :: forall x. FFIFloatSize -> Rep FFIFloatSize x
    $cto :: forall x. Rep FFIFloatSize x -> FFIFloatSize
    to :: forall x. Rep FFIFloatSize x -> FFIFloatSize
    Generic, FFIFloatSize -> ()
    (FFIFloatSize -> ()) -> NFData FFIFloatSize
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIFloatSize -> ()
    rnf :: FFIFloatSize -> ()
    NFData)

    -- | Basic type which is passed and returned by reference through a parameter.
    data FFIBasicRefType
      = FFIInteger
          (Maybe Type) -- ^ Modulus (Just for Z, Nothing for Integer)
      | FFIRational
      deriving (Int -> FFIBasicRefType -> ShowS
    [FFIBasicRefType] -> ShowS
    FFIBasicRefType -> String
    (Int -> FFIBasicRefType -> ShowS)
    -> (FFIBasicRefType -> String)
    -> ([FFIBasicRefType] -> ShowS)
    -> Show FFIBasicRefType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FFIBasicRefType -> ShowS
    showsPrec :: Int -> FFIBasicRefType -> ShowS
    $cshow :: FFIBasicRefType -> String
    show :: FFIBasicRefType -> String
    $cshowList :: [FFIBasicRefType] -> ShowS
    showList :: [FFIBasicRefType] -> ShowS
    Show, (forall x. FFIBasicRefType -> Rep FFIBasicRefType x)
    -> (forall x. Rep FFIBasicRefType x -> FFIBasicRefType)
    -> Generic FFIBasicRefType
    forall x. Rep FFIBasicRefType x -> FFIBasicRefType
    forall x. FFIBasicRefType -> Rep FFIBasicRefType x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FFIBasicRefType -> Rep FFIBasicRefType x
    from :: forall x. FFIBasicRefType -> Rep FFIBasicRefType x
    $cto :: forall x. Rep FFIBasicRefType x -> FFIBasicRefType
    to :: forall x. Rep FFIBasicRefType x -> FFIBasicRefType
    Generic, FFIBasicRefType -> ()
    (FFIBasicRefType -> ()) -> NFData FFIBasicRefType
    forall a. (a -> ()) -> NFData a
    $crnf :: FFIBasicRefType -> ()
    rnf :: FFIBasicRefType -> ()
    NFData)