{-# 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FFIFunType] -> ShowS
$cshowList :: [FFIFunType] -> ShowS
show :: FFIFunType -> String
$cshow :: FFIFunType -> String
showsPrec :: Int -> FFIFunType -> ShowS
$cshowsPrec :: Int -> FFIFunType -> ShowS
Show, 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
$cto :: forall x. Rep FFIFunType x -> FFIFunType
$cfrom :: forall x. FFIFunType -> Rep FFIFunType x
Generic, FFIFunType -> ()
forall a. (a -> ()) -> NFData a
rnf :: FFIFunType -> ()
$crnf :: 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FFIType] -> ShowS
$cshowList :: [FFIType] -> ShowS
show :: FFIType -> String
$cshow :: FFIType -> String
showsPrec :: Int -> FFIType -> ShowS
$cshowsPrec :: Int -> FFIType -> ShowS
Show, 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
$cto :: forall x. Rep FFIType x -> FFIType
$cfrom :: forall x. FFIType -> Rep FFIType x
Generic, FFIType -> ()
forall a. (a -> ()) -> NFData a
rnf :: FFIType -> ()
$crnf :: FFIType -> ()
NFData)

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

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

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