{-# LANGUAGE BlockArguments   #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE RecordWildCards  #-}
{-# LANGUAGE TypeApplications #-}

-- | Generate C header files from foreign declarations.
module Cryptol.Eval.FFI.GenHeader
  ( generateForeignHeader
  ) where

import           Control.Monad.Writer.Strict
import           Data.Functor
import           Data.Char(isAlphaNum)
import           Data.List
import           Data.Set                      (Set)
import qualified Data.Set                      as Set
import           Language.C99.Pretty           as C
import qualified Language.C99.Simple           as C
import qualified Text.PrettyPrint              as Pretty

import           Cryptol.ModuleSystem.Name
import           Cryptol.TypeCheck.FFI.FFIType
import           Cryptol.TypeCheck.Type
import           Cryptol.Utils.Ident
import           Cryptol.Utils.RecordMap

-- | @Include foo@ represents an include statement @#include <foo>@
newtype Include = Include String deriving (Include -> Include -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Include -> Include -> Bool
$c/= :: Include -> Include -> Bool
== :: Include -> Include -> Bool
$c== :: Include -> Include -> Bool
Eq, Eq Include
Include -> Include -> Bool
Include -> Include -> Ordering
Include -> Include -> Include
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Include -> Include -> Include
$cmin :: Include -> Include -> Include
max :: Include -> Include -> Include
$cmax :: Include -> Include -> Include
>= :: Include -> Include -> Bool
$c>= :: Include -> Include -> Bool
> :: Include -> Include -> Bool
$c> :: Include -> Include -> Bool
<= :: Include -> Include -> Bool
$c<= :: Include -> Include -> Bool
< :: Include -> Include -> Bool
$c< :: Include -> Include -> Bool
compare :: Include -> Include -> Ordering
$ccompare :: Include -> Include -> Ordering
Ord)

-- | The monad for generating headers. We keep track of which headers we need to
-- include and add them to the output at the end.
type GenHeaderM = Writer (Set Include)

-- | Generate a C header file from the given foreign declarations.
generateForeignHeader :: [(Name, FFIFunType)] -> String
generateForeignHeader :: [(Name, FFIFunType)] -> String
generateForeignHeader [(Name, FFIFunType)]
decls =
  [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map Include -> String
renderInclude forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toAscList Set Include
incs)
  forall a. [a] -> [a] -> [a]
++ Doc -> String
Pretty.render (forall a. Pretty a => a -> Doc
C.pretty forall a b. (a -> b) -> a -> b
$ TransUnit -> TransUnit
C.translate ([Decln] -> [FunDef] -> TransUnit
C.TransUnit [Decln]
cdecls []))
  where ([Decln]
cdecls, Set Include
incs) = forall w a. Writer w a -> (a, w)
runWriter forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Name, FFIFunType) -> GenHeaderM Decln
convertFun [(Name, FFIFunType)]
decls

renderInclude :: Include -> String
renderInclude :: Include -> String
renderInclude (Include String
inc) = String
"#include <" forall a. [a] -> [a] -> [a]
++ String
inc forall a. [a] -> [a] -> [a]
++ String
">"

-- | The "direction" of a parameter (input or output).
data ParamDir = In | Out

-- | The result of converting a Cryptol type into its C representation.
data ConvertResult
  = Direct C.Type -- ^ A type that can be directly returned if it is a return
                  -- type and passed as a single parameter if it is a Cryptol
                  -- parameter type.
  | Params [C.Param] -- ^ A type that is turned into a number of parameters,
                     -- for both Cryptol parameter and return type cases.

-- | Convert a Cryptol foreign declaration into a C function declaration.
convertFun :: (Name, FFIFunType) -> GenHeaderM C.Decln
convertFun :: (Name, FFIFunType) -> GenHeaderM Decln
convertFun (Name
fName, FFIFunType {[TParam]
[FFIType]
FFIType
ffiRetType :: FFIFunType -> FFIType
ffiArgTypes :: FFIFunType -> [FFIType]
ffiTParams :: FFIFunType -> [TParam]
ffiRetType :: FFIType
ffiArgTypes :: [FFIType]
ffiTParams :: [TParam]
..}) = do
  let tpIdent :: TParam -> Maybe Ident
tpIdent = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Ident
nameIdent forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> Maybe Name
tpName
  [Param]
typeParams <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse String -> GenHeaderM Param
convertTypeParam ([Maybe Ident] -> [String]
pickNames (forall a b. (a -> b) -> [a] -> [b]
map TParam -> Maybe Ident
tpIdent [TParam]
ffiTParams))
  -- Name the input args in0, in1, etc
  let inPrefixes :: [String]
inPrefixes =
        case [FFIType]
ffiArgTypes of
          [FFIType
_] -> [String
"in"]
          [FFIType]
_   -> [String
"in" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show @Integer Integer
i | Integer
i <- [Integer
0..]]
  [Param]
inParams <- ParamDir -> [(String, FFIType)] -> GenHeaderM [Param]
convertMultiType ParamDir
In forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [String]
inPrefixes [FFIType]
ffiArgTypes
  (Type
retType, [Param]
outParams) <- ParamDir -> FFIType -> GenHeaderM ConvertResult
convertType ParamDir
Out FFIType
ffiRetType
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Direct Type
u  -> (Type
u, [])
      -- Name the output arg out
      Params [Param]
ps -> (TypeSpec -> Type
C.TypeSpec TypeSpec
C.Void, forall a b. (a -> b) -> [a] -> [b]
map (String -> Param -> Param
prefixParam String
"out") [Param]
ps)
  -- Avoid possible name collisions
  let params :: [Param]
params = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL Set String -> Param -> (Set String, Param)
renameParam forall a. Set a
Set.empty forall a b. (a -> b) -> a -> b
$
        [Param]
typeParams forall a. [a] -> [a] -> [a]
++ [Param]
inParams forall a. [a] -> [a] -> [a]
++ [Param]
outParams
      renameParam :: Set String -> Param -> (Set String, Param)
renameParam Set String
names (C.Param Type
u String
name) =
        (forall a. Ord a => a -> Set a -> Set a
Set.insert String
name' Set String
names, Type -> String -> Param
C.Param Type
u String
name')
        where name' :: String
name' = forall a. (a -> Bool) -> (a -> a) -> a -> a
until (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set String
names) (forall a. [a] -> [a] -> [a]
++ String
"_") String
name
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Maybe StorageSpec -> Type -> String -> [Param] -> Decln
C.FunDecln forall a. Maybe a
Nothing Type
retType (Ident -> String
unpackIdent forall a b. (a -> b) -> a -> b
$ Name -> Ident
nameIdent Name
fName) [Param]
params


-- | Convert a Cryptol type parameter to a C value parameter.
convertTypeParam :: String -> GenHeaderM C.Param
convertTypeParam :: String -> GenHeaderM Param
convertTypeParam String
name = (Type -> String -> Param
`C.Param` String
name) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenHeaderM Type
sizeT

-- | Convert a Cryptol parameter or return type to C.
convertType :: ParamDir -> FFIType -> GenHeaderM ConvertResult
convertType :: ParamDir -> FFIType -> GenHeaderM ConvertResult
convertType ParamDir
_ FFIType
FFIBool = Type -> ConvertResult
Direct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenHeaderM Type
uint8T
convertType ParamDir
_ (FFIBasic FFIBasicType
t) = FFIBasicType -> GenHeaderM ConvertResult
convertBasicType FFIBasicType
t
convertType ParamDir
_ (FFIArray [Type]
_ FFIBasicType
t) = do
  Type
u <- FFIBasicType -> GenHeaderM Type
convertBasicTypeInArray FFIBasicType
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Param] -> ConvertResult
Params [Type -> String -> Param
C.Param (Type -> Type
C.Ptr Type
u) String
""]
convertType ParamDir
dir (FFITuple [FFIType]
ts) = [Param] -> ConvertResult
Params forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParamDir -> [(String, FFIType)] -> GenHeaderM [Param]
convertMultiType ParamDir
dir
  -- We name the tuple components using their indices
  (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map (String -> String
componentSuffix forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show @Integer) [Integer
0..]) [FFIType]
ts)
convertType ParamDir
dir (FFIRecord RecordMap Ident FFIType
tMap) =
  [Param] -> ConvertResult
Params forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParamDir -> [(String, FFIType)] -> GenHeaderM [Param]
convertMultiType ParamDir
dir (forall a b. [a] -> [b] -> [(a, b)]
zip [String]
names [FFIType]
ts)
  where
  ([Ident]
fs,[FFIType]
ts) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields RecordMap Ident FFIType
tMap)
  names :: [String]
names   = forall a b. (a -> b) -> [a] -> [b]
map String -> String
componentSuffix ([Maybe Ident] -> [String]
pickNames (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Maybe a
Just [Ident]
fs))

-- | Convert many Cryptol types, each associated with a prefix, to C parameters
-- named with their prefixes.
convertMultiType :: ParamDir -> [(C.Ident, FFIType)] -> GenHeaderM [C.Param]
convertMultiType :: ParamDir -> [(String, FFIType)] -> GenHeaderM [Param]
convertMultiType ParamDir
dir = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse \(String
prefix, FFIType
t) ->
  ParamDir -> FFIType -> GenHeaderM ConvertResult
convertType ParamDir
dir FFIType
t
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Direct Type
u -> [Type -> String -> Param
C.Param Type
u' String
prefix]
        where u' :: Type
u' = case ParamDir
dir of
                ParamDir
In  -> Type
u
                -- Turn direct return types into pointer out parameters
                ParamDir
Out -> Type -> Type
C.Ptr Type
u
      Params [Param]
ps -> forall a b. (a -> b) -> [a] -> [b]
map (String -> Param -> Param
prefixParam String
prefix) [Param]
ps

{- | Convert a basic Cryptol FFI type to a C type with its corresponding
calling convention.  At present all value types use the same calling
convention no matter if they are inputs or outputs, so we don't
need the 'ParamDir'. -}
convertBasicType :: FFIBasicType -> GenHeaderM ConvertResult
convertBasicType :: FFIBasicType -> GenHeaderM ConvertResult
convertBasicType FFIBasicType
bt =
  case FFIBasicType
bt of
    FFIBasicVal FFIBasicValType
bvt -> Type -> ConvertResult
Direct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FFIBasicValType -> GenHeaderM Type
convertBasicValType FFIBasicValType
bvt
    FFIBasicRef FFIBasicRefType
brt -> do Type
t <- FFIBasicRefType -> GenHeaderM Type
convertBasicRefType FFIBasicRefType
brt
                          forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Param] -> ConvertResult
Params [Type -> String -> Param
C.Param Type
t String
""])

-- | Convert a basic Cryptol FFI type to a C type.
-- This is used when the type is stored in array.
convertBasicTypeInArray :: FFIBasicType -> GenHeaderM C.Type
convertBasicTypeInArray :: FFIBasicType -> GenHeaderM Type
convertBasicTypeInArray FFIBasicType
bt =
  case FFIBasicType
bt of
    FFIBasicVal FFIBasicValType
bvt -> FFIBasicValType -> GenHeaderM Type
convertBasicValType FFIBasicValType
bvt
    FFIBasicRef FFIBasicRefType
brt -> FFIBasicRefType -> GenHeaderM Type
convertBasicRefType FFIBasicRefType
brt

-- | Convert a basic Cryptol FFI type to a value C type.
convertBasicValType :: FFIBasicValType -> GenHeaderM C.Type
convertBasicValType :: FFIBasicValType -> GenHeaderM Type
convertBasicValType (FFIWord Integer
_ FFIWordSize
s) =
  case FFIWordSize
s of
    FFIWordSize
FFIWord8  -> GenHeaderM Type
uint8T
    FFIWordSize
FFIWord16 -> GenHeaderM Type
uint16T
    FFIWordSize
FFIWord32 -> GenHeaderM Type
uint32T
    FFIWordSize
FFIWord64 -> GenHeaderM Type
uint64T
convertBasicValType (FFIFloat Integer
_ Integer
_ FFIFloatSize
s) =
  case FFIFloatSize
s of
    FFIFloatSize
FFIFloat32 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TypeSpec -> Type
C.TypeSpec TypeSpec
C.Float
    FFIFloatSize
FFIFloat64 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TypeSpec -> Type
C.TypeSpec TypeSpec
C.Double

-- | Convert a basic Cryptol FFI type to a reference C type.
convertBasicRefType :: FFIBasicRefType -> GenHeaderM C.Type
convertBasicRefType :: FFIBasicRefType -> GenHeaderM Type
convertBasicRefType FFIBasicRefType
brt =
  case FFIBasicRefType
brt of
    FFIInteger {} -> GenHeaderM Type
mpzT
    FFIBasicRefType
FFIRational   -> GenHeaderM Type
mpqT

prefixParam :: C.Ident -> C.Param -> C.Param
prefixParam :: String -> Param -> Param
prefixParam String
pre (C.Param Type
u String
name) = Type -> String -> Param
C.Param Type
u (String
pre forall a. [a] -> [a] -> [a]
++ String
name)

-- | Create a suffix corresponding to some component name of some larger type.
componentSuffix :: String -> C.Ident
componentSuffix :: String -> String
componentSuffix = (Char
'_' forall a. a -> [a] -> [a]
:)

sizeT, uint8T, uint16T, uint32T, uint64T, mpzT, mpqT :: GenHeaderM C.Type
sizeT :: GenHeaderM Type
sizeT = Include -> String -> GenHeaderM Type
typedefFromInclude Include
stddefH String
"size_t"
uint8T :: GenHeaderM Type
uint8T = Include -> String -> GenHeaderM Type
typedefFromInclude Include
stdintH String
"uint8_t"
uint16T :: GenHeaderM Type
uint16T = Include -> String -> GenHeaderM Type
typedefFromInclude Include
stdintH String
"uint16_t"
uint32T :: GenHeaderM Type
uint32T = Include -> String -> GenHeaderM Type
typedefFromInclude Include
stdintH String
"uint32_t"
uint64T :: GenHeaderM Type
uint64T = Include -> String -> GenHeaderM Type
typedefFromInclude Include
stdintH String
"uint64_t"
mpzT :: GenHeaderM Type
mpzT = Include -> String -> GenHeaderM Type
typedefFromInclude Include
gmpH String
"mpz_t"
mpqT :: GenHeaderM Type
mpqT = Include -> String -> GenHeaderM Type
typedefFromInclude Include
gmpH String
"mpq_t"

stddefH, stdintH, gmpH :: Include
stddefH :: Include
stddefH = String -> Include
Include String
"stddef.h"
stdintH :: Include
stdintH = String -> Include
Include String
"stdint.h"
gmpH :: Include
gmpH = String -> Include
Include String
"gmp.h"


-- | Return a type with the given name, included from some header file.
typedefFromInclude :: Include -> C.Ident -> GenHeaderM C.Type
typedefFromInclude :: Include -> String -> GenHeaderM Type
typedefFromInclude Include
inc String
u = do
  forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton Include
inc
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TypeSpec -> Type
C.TypeSpec forall a b. (a -> b) -> a -> b
$ String -> TypeSpec
C.TypedefName String
u

-- | Given some Cryptol identifiers (normal ones, not operators)
-- pick suitable unique C names for them
pickNames :: [Maybe Ident] -> [String]
pickNames :: [Maybe Ident] -> [String]
pickNames [Maybe Ident]
xs = forall a b. (a, b) -> b
snd (forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL Set String -> Maybe Ident -> (Set String, String)
add forall a. Set a
Set.empty [Maybe Ident]
xs)
  where
  add :: Set String -> Maybe Ident -> (Set String, String)
add Set String
known Maybe Ident
x =
    let y :: String
y      = Maybe Ident -> String
simplify Maybe Ident
x
        ys :: [String]
ys     = String
y forall a. a -> [a] -> [a]
: [ String
y forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i | Int
i <- [ Int
0 :: Int .. ] ]
        String
y' : [String]
_ = forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
known) [String]
ys
    in (forall a. Ord a => a -> Set a -> Set a
Set.insert String
y' Set String
known, String
y')

  simplify :: Maybe Ident -> String
simplify Maybe Ident
x = case Maybe Ident
x of
                 Just Ident
i | let y :: String
y = forall a. (a -> Bool) -> [a] -> [a]
filter Char -> Bool
ok (Ident -> String
unpackIdent Ident
i), Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
y) -> String
y
                 Maybe Ident
_ -> String
"zz"

  ok :: Char -> Bool
ok Char
x     = Char
x forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char -> Bool
isAlphaNum Char
x