{-# 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
(Include -> Include -> Bool)
-> (Include -> Include -> Bool) -> Eq Include
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Include -> Include -> Bool
== :: Include -> Include -> Bool
$c/= :: Include -> Include -> Bool
/= :: Include -> Include -> Bool
Eq, Eq Include
Eq Include =>
(Include -> Include -> Ordering)
-> (Include -> Include -> Bool)
-> (Include -> Include -> Bool)
-> (Include -> Include -> Bool)
-> (Include -> Include -> Bool)
-> (Include -> Include -> Include)
-> (Include -> Include -> Include)
-> Ord 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
$ccompare :: Include -> Include -> Ordering
compare :: Include -> Include -> Ordering
$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
>= :: Include -> Include -> Bool
$cmax :: Include -> Include -> Include
max :: Include -> Include -> Include
$cmin :: Include -> Include -> Include
min :: Include -> Include -> Include
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 ((Include -> String) -> [Include] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Include -> String
renderInclude ([Include] -> [String]) -> [Include] -> [String]
forall a b. (a -> b) -> a -> b
$ Set Include -> [Include]
forall a. Set a -> [a]
Set.toAscList Set Include
incs)
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
Pretty.render (TransUnit -> Doc
forall a. Pretty a => a -> Doc
C.pretty (TransUnit -> Doc) -> TransUnit -> Doc
forall a b. (a -> b) -> a -> b
$ TransUnit -> TransUnit
C.translate ([Decln] -> [FunDef] -> TransUnit
C.TransUnit [Decln]
cdecls []))
  where ([Decln]
cdecls, Set Include
incs) = Writer (Set Include) [Decln] -> ([Decln], Set Include)
forall w a. Writer w a -> (a, w)
runWriter (Writer (Set Include) [Decln] -> ([Decln], Set Include))
-> Writer (Set Include) [Decln] -> ([Decln], Set Include)
forall a b. (a -> b) -> a -> b
$ ((Name, FFIFunType) -> WriterT (Set Include) Identity Decln)
-> [(Name, FFIFunType)] -> Writer (Set Include) [Decln]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Name, FFIFunType) -> WriterT (Set Include) Identity Decln
convertFun [(Name, FFIFunType)]
decls

renderInclude :: Include -> String
renderInclude :: Include -> String
renderInclude (Include String
inc) = String
"#include <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
inc String -> String -> String
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) -> WriterT (Set Include) Identity Decln
convertFun (Name
fName, FFIFunType {[TParam]
[FFIType]
FFIType
ffiTParams :: [TParam]
ffiArgTypes :: [FFIType]
ffiRetType :: FFIType
ffiTParams :: FFIFunType -> [TParam]
ffiArgTypes :: FFIFunType -> [FFIType]
ffiRetType :: FFIFunType -> FFIType
..}) = do
  let tpIdent :: TParam -> Maybe Ident
tpIdent = (Name -> Ident) -> Maybe Name -> Maybe Ident
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Ident
nameIdent (Maybe Name -> Maybe Ident)
-> (TParam -> Maybe Name) -> TParam -> Maybe Ident
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> Maybe Name
tpName
  [Param]
typeParams <- (String -> WriterT (Set Include) Identity Param)
-> [String] -> WriterT (Set Include) Identity [Param]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse String -> WriterT (Set Include) Identity Param
convertTypeParam ([Maybe Ident] -> [String]
pickNames ((TParam -> Maybe Ident) -> [TParam] -> [Maybe Ident]
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show @Integer Integer
i | Integer
i <- [Integer
0..]]
  [Param]
inParams <- ParamDir
-> [(String, FFIType)] -> WriterT (Set Include) Identity [Param]
convertMultiType ParamDir
In ([(String, FFIType)] -> WriterT (Set Include) Identity [Param])
-> [(String, FFIType)] -> WriterT (Set Include) Identity [Param]
forall a b. (a -> b) -> a -> b
$ [String] -> [FFIType] -> [(String, FFIType)]
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
    GenHeaderM ConvertResult
-> (ConvertResult -> (Type, [Param]))
-> WriterT (Set Include) Identity (Type, [Param])
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, (Param -> Param) -> [Param] -> [Param]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Param -> Param
prefixParam String
"out") [Param]
ps)
  -- Avoid possible name collisions
  let params :: [Param]
params = (Set String, [Param]) -> [Param]
forall a b. (a, b) -> b
snd ((Set String, [Param]) -> [Param])
-> (Set String, [Param]) -> [Param]
forall a b. (a -> b) -> a -> b
$ (Set String -> Param -> (Set String, Param))
-> Set String -> [Param] -> (Set String, [Param])
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 Set String
forall a. Set a
Set.empty ([Param] -> (Set String, [Param]))
-> [Param] -> (Set String, [Param])
forall a b. (a -> b) -> a -> b
$
        [Param]
typeParams [Param] -> [Param] -> [Param]
forall a. [a] -> [a] -> [a]
++ [Param]
inParams [Param] -> [Param] -> [Param]
forall a. [a] -> [a] -> [a]
++ [Param]
outParams
      renameParam :: Set String -> Param -> (Set String, Param)
renameParam Set String
names (C.Param Type
u String
name) =
        (String -> Set String -> Set String
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' = (String -> Bool) -> (String -> String) -> String -> String
forall a. (a -> Bool) -> (a -> a) -> a -> a
until (String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set String
names) (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_") String
name
  Decln -> WriterT (Set Include) Identity Decln
forall a. a -> WriterT (Set Include) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Decln -> WriterT (Set Include) Identity Decln)
-> Decln -> WriterT (Set Include) Identity Decln
forall a b. (a -> b) -> a -> b
$ Maybe StorageSpec -> Type -> String -> [Param] -> Decln
C.FunDecln Maybe StorageSpec
forall a. Maybe a
Nothing Type
retType (Ident -> String
unpackIdent (Ident -> String) -> Ident -> String
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 -> WriterT (Set Include) Identity Param
convertTypeParam String
name = (Type -> String -> Param
`C.Param` String
name) (Type -> Param)
-> WriterT (Set Include) Identity Type
-> WriterT (Set Include) Identity Param
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT (Set Include) Identity 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 (Type -> ConvertResult)
-> WriterT (Set Include) Identity Type -> GenHeaderM ConvertResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT (Set Include) Identity Type
uint8T
convertType ParamDir
_ (FFIBasic FFIBasicType
t) = FFIBasicType -> GenHeaderM ConvertResult
convertBasicType FFIBasicType
t
convertType ParamDir
_ (FFIArray [Type]
_ FFIBasicType
t) = do
  Type
u <- FFIBasicType -> WriterT (Set Include) Identity Type
convertBasicTypeInArray FFIBasicType
t
  ConvertResult -> GenHeaderM ConvertResult
forall a. a -> WriterT (Set Include) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConvertResult -> GenHeaderM ConvertResult)
-> ConvertResult -> GenHeaderM ConvertResult
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 ([Param] -> ConvertResult)
-> WriterT (Set Include) Identity [Param]
-> GenHeaderM ConvertResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParamDir
-> [(String, FFIType)] -> WriterT (Set Include) Identity [Param]
convertMultiType ParamDir
dir
  -- We name the tuple components using their indices
  ([String] -> [FFIType] -> [(String, FFIType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Integer -> String) -> [Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
componentSuffix (String -> String) -> (Integer -> String) -> Integer -> String
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 ([Param] -> ConvertResult)
-> WriterT (Set Include) Identity [Param]
-> GenHeaderM ConvertResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParamDir
-> [(String, FFIType)] -> WriterT (Set Include) Identity [Param]
convertMultiType ParamDir
dir ([String] -> [FFIType] -> [(String, FFIType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
names [FFIType]
ts)
  where
  ([Ident]
fs,[FFIType]
ts) = [(Ident, FFIType)] -> ([Ident], [FFIType])
forall a b. [(a, b)] -> ([a], [b])
unzip (RecordMap Ident FFIType -> [(Ident, FFIType)]
forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields RecordMap Ident FFIType
tMap)
  names :: [String]
names   = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
componentSuffix ([Maybe Ident] -> [String]
pickNames ((Ident -> Maybe Ident) -> [Ident] -> [Maybe Ident]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Maybe Ident
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)] -> WriterT (Set Include) Identity [Param]
convertMultiType ParamDir
dir = ([[Param]] -> [Param])
-> WriterT (Set Include) Identity [[Param]]
-> WriterT (Set Include) Identity [Param]
forall a b.
(a -> b)
-> WriterT (Set Include) Identity a
-> WriterT (Set Include) Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Param]] -> [Param]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (WriterT (Set Include) Identity [[Param]]
 -> WriterT (Set Include) Identity [Param])
-> ([(String, FFIType)]
    -> WriterT (Set Include) Identity [[Param]])
-> [(String, FFIType)]
-> WriterT (Set Include) Identity [Param]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, FFIType) -> WriterT (Set Include) Identity [Param])
-> [(String, FFIType)] -> WriterT (Set Include) Identity [[Param]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse \(String
prefix, FFIType
t) ->
  ParamDir -> FFIType -> GenHeaderM ConvertResult
convertType ParamDir
dir FFIType
t
    GenHeaderM ConvertResult
-> (ConvertResult -> [Param])
-> WriterT (Set Include) Identity [Param]
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 -> (Param -> Param) -> [Param] -> [Param]
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 (Type -> ConvertResult)
-> WriterT (Set Include) Identity Type -> GenHeaderM ConvertResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FFIBasicValType -> WriterT (Set Include) Identity Type
convertBasicValType FFIBasicValType
bvt
    FFIBasicRef FFIBasicRefType
brt -> do Type
t <- FFIBasicRefType -> WriterT (Set Include) Identity Type
convertBasicRefType FFIBasicRefType
brt
                          ConvertResult -> GenHeaderM ConvertResult
forall a. a -> WriterT (Set Include) Identity a
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 -> WriterT (Set Include) Identity Type
convertBasicTypeInArray FFIBasicType
bt =
  case FFIBasicType
bt of
    FFIBasicVal FFIBasicValType
bvt -> FFIBasicValType -> WriterT (Set Include) Identity Type
convertBasicValType FFIBasicValType
bvt
    FFIBasicRef FFIBasicRefType
brt -> FFIBasicRefType -> WriterT (Set Include) Identity Type
convertBasicRefType FFIBasicRefType
brt

-- | Convert a basic Cryptol FFI type to a value C type.
convertBasicValType :: FFIBasicValType -> GenHeaderM C.Type
convertBasicValType :: FFIBasicValType -> WriterT (Set Include) Identity Type
convertBasicValType (FFIWord Integer
_ FFIWordSize
s) =
  case FFIWordSize
s of
    FFIWordSize
FFIWord8  -> WriterT (Set Include) Identity Type
uint8T
    FFIWordSize
FFIWord16 -> WriterT (Set Include) Identity Type
uint16T
    FFIWordSize
FFIWord32 -> WriterT (Set Include) Identity Type
uint32T
    FFIWordSize
FFIWord64 -> WriterT (Set Include) Identity Type
uint64T
convertBasicValType (FFIFloat Integer
_ Integer
_ FFIFloatSize
s) =
  case FFIFloatSize
s of
    FFIFloatSize
FFIFloat32 -> Type -> WriterT (Set Include) Identity Type
forall a. a -> WriterT (Set Include) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> WriterT (Set Include) Identity Type)
-> Type -> WriterT (Set Include) Identity Type
forall a b. (a -> b) -> a -> b
$ TypeSpec -> Type
C.TypeSpec TypeSpec
C.Float
    FFIFloatSize
FFIFloat64 -> Type -> WriterT (Set Include) Identity Type
forall a. a -> WriterT (Set Include) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> WriterT (Set Include) Identity Type)
-> Type -> WriterT (Set Include) Identity Type
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 -> WriterT (Set Include) Identity Type
convertBasicRefType FFIBasicRefType
brt =
  case FFIBasicRefType
brt of
    FFIInteger {} -> WriterT (Set Include) Identity Type
mpzT
    FFIBasicRefType
FFIRational   -> WriterT (Set Include) Identity 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 String -> String -> String
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
'_' Char -> String -> String
forall a. a -> [a] -> [a]
:)

sizeT, uint8T, uint16T, uint32T, uint64T, mpzT, mpqT :: GenHeaderM C.Type
sizeT :: WriterT (Set Include) Identity Type
sizeT = Include -> String -> WriterT (Set Include) Identity Type
typedefFromInclude Include
stddefH String
"size_t"
uint8T :: WriterT (Set Include) Identity Type
uint8T = Include -> String -> WriterT (Set Include) Identity Type
typedefFromInclude Include
stdintH String
"uint8_t"
uint16T :: WriterT (Set Include) Identity Type
uint16T = Include -> String -> WriterT (Set Include) Identity Type
typedefFromInclude Include
stdintH String
"uint16_t"
uint32T :: WriterT (Set Include) Identity Type
uint32T = Include -> String -> WriterT (Set Include) Identity Type
typedefFromInclude Include
stdintH String
"uint32_t"
uint64T :: WriterT (Set Include) Identity Type
uint64T = Include -> String -> WriterT (Set Include) Identity Type
typedefFromInclude Include
stdintH String
"uint64_t"
mpzT :: WriterT (Set Include) Identity Type
mpzT = Include -> String -> WriterT (Set Include) Identity Type
typedefFromInclude Include
gmpH String
"mpz_t"
mpqT :: WriterT (Set Include) Identity Type
mpqT = Include -> String -> WriterT (Set Include) Identity 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 -> WriterT (Set Include) Identity Type
typedefFromInclude Include
inc String
u = do
  Set Include -> WriterT (Set Include) Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Set Include -> WriterT (Set Include) Identity ())
-> Set Include -> WriterT (Set Include) Identity ()
forall a b. (a -> b) -> a -> b
$ Include -> Set Include
forall a. a -> Set a
Set.singleton Include
inc
  Type -> WriterT (Set Include) Identity Type
forall a. a -> WriterT (Set Include) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> WriterT (Set Include) Identity Type)
-> Type -> WriterT (Set Include) Identity Type
forall a b. (a -> b) -> a -> b
$ TypeSpec -> Type
C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
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 = (Set String, [String]) -> [String]
forall a b. (a, b) -> b
snd ((Set String -> Maybe Ident -> (Set String, String))
-> Set String -> [Maybe Ident] -> (Set String, [String])
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 Set String
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 String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [ Int
0 :: Int .. ] ]
        String
y' : [String]
_ = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
known) [String]
ys
    in (String -> Set String -> Set String
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 = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter Char -> Bool
ok (Ident -> String
unpackIdent Ident
i), Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char -> Bool
isAlphaNum Char
x