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