{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
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
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)
type = Writer (Set Include)
generateForeignHeader :: [(Name, FFIFunType)] -> String
[(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
">"
data ParamDir = In | Out
data ConvertResult
= Direct C.Type
| Params [C.Param]
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))
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, [])
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)
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
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
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
(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))
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
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
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
""])
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
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
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)
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"
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
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