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