    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Compilers.C
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Compilation of symbolic programs to C
    -----------------------------------------------------------------------------

    {-# LANGUAGE CPP           #-}
    {-# LANGUAGE PatternGuards #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Compilers.C(compileToC, compileToCLib, compileToC', compileToCLib') where

    import Control.DeepSeq                (rnf)
    import Data.Char                      (isSpace)
    import Data.List                      (nub, intercalate, intersperse)
    import Data.Maybe                     (isJust, isNothing, fromJust)
    import qualified Data.Foldable as F   (toList)
    import qualified Data.Set      as Set (member, union, unions, empty, toList, singleton, fromList)
    import System.FilePath                (takeBaseName, replaceExtension)
    import System.Random

    -- Work around the fact that GHC 8.4.1 started exporting <>.. Hmm..
    import Text.PrettyPrint.HughesPJ
    import qualified Text.PrettyPrint.HughesPJ as P ((<>))

    import Data.SBV.Core.Data
    import Data.SBV.Compilers.CodeGen

    import Data.SBV.Utils.PrettyNum   (chex, showCFloat, showCDouble)

    import GHC.Stack

    ---------------------------------------------------------------------------
    -- * API
    ---------------------------------------------------------------------------

    -- | Given a symbolic computation, render it as an equivalent collection of files
    -- that make up a C program:
    --
    --   * The first argument is the directory name under which the files will be saved. To save
    --     files in the current directory pass @'Just' \".\"@. Use 'Nothing' for printing to stdout.
    --
    --   * The second argument is the name of the C function to generate.
    --
    --   * The final argument is the function to be compiled.
    --
    -- Compilation will also generate a @Makefile@,  a header file, and a driver (test) program, etc. As a
    -- result, we return whatever the code-gen function returns. Most uses should simply have @()@ as
    -- the return type here, but the value can be useful if you want to chain the result of
    -- one compilation act to the next.
    compileToC :: Maybe FilePath -> String -> SBVCodeGen a -> IO a
    compileToC :: Maybe FilePath -> FilePath -> SBVCodeGen a -> IO a
    compileToC mbDirName :: Maybe FilePath
    mbDirName nm :: FilePath
    nm f :: SBVCodeGen a
    f = do (retVal :: a
    retVal, cfg :: CgConfig
    cfg, bundle :: CgPgmBundle
    bundle) <- FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    forall a. FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC' FilePath
    nm SBVCodeGen a
    f
                                   Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
    renderCgPgmBundle Maybe FilePath
    mbDirName (CgConfig
    cfg, CgPgmBundle
    bundle)
                                   a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    retVal

    -- | Lower level version of 'compileToC', producing a 'CgPgmBundle'
    compileToC' :: String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC' :: FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC' nm :: FilePath
    nm f :: SBVCodeGen a
    f = do [Integer]
    rands <- StdGen -> [Integer]
    forall a g. (Random a, RandomGen g) => g -> [a]
    randoms (StdGen -> [Integer]) -> IO StdGen -> IO [Integer]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` IO StdGen
    newStdGen
                          SBVToC
    -> CgConfig
    -> FilePath
    -> SBVCodeGen a
    -> IO (a, CgConfig, CgPgmBundle)
    forall l a.
    CgTarget l =>
    l
    -> CgConfig
    -> FilePath
    -> SBVCodeGen a
    -> IO (a, CgConfig, CgPgmBundle)
    codeGen SBVToC
    SBVToC (CgConfig
    defaultCgConfig { cgDriverVals :: [Integer]
    cgDriverVals = [Integer]
    rands }) FilePath
    nm SBVCodeGen a
    f

    -- | Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code
    -- from multiple functions that work together as a library.
    --
    --   * The first argument is the directory name under which the files will be saved. To save
    --     files in the current directory pass @'Just' \".\"@. Use 'Nothing' for printing to stdout.
    --
    --   * The second argument is the name of the archive to generate.
    --
    --   * The third argument is the list of functions to include, in the form of function-name/code pairs, similar
    --     to the second and third arguments of 'compileToC', except in a list.
    compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen a)] -> IO [a]
    compileToCLib :: Maybe FilePath -> FilePath -> [(FilePath, SBVCodeGen a)] -> IO [a]
    compileToCLib mbDirName :: Maybe FilePath
    mbDirName libName :: FilePath
    libName comps :: [(FilePath, SBVCodeGen a)]
    comps = do (retVal :: [a]
    retVal, cfg :: CgConfig
    cfg, pgm :: CgPgmBundle
    pgm) <- FilePath
    -> [(FilePath, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    forall a.
    FilePath
    -> [(FilePath, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    compileToCLib' FilePath
    libName [(FilePath, SBVCodeGen a)]
    comps
                                               Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
    renderCgPgmBundle Maybe FilePath
    mbDirName (CgConfig
    cfg, CgPgmBundle
    pgm)
                                               [a] -> IO [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a]
    retVal

    -- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle'
    compileToCLib' :: String -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    compileToCLib' :: FilePath
    -> [(FilePath, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    compileToCLib' libName :: FilePath
    libName comps :: [(FilePath, SBVCodeGen a)]
    comps = do [(a, CgConfig, CgPgmBundle)]
    resCfgBundles <- ((FilePath, SBVCodeGen a) -> IO (a, CgConfig, CgPgmBundle))
    -> [(FilePath, SBVCodeGen a)] -> IO [(a, CgConfig, CgPgmBundle)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle))
    -> (FilePath, SBVCodeGen a) -> IO (a, CgConfig, CgPgmBundle)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    forall a. FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC') [(FilePath, SBVCodeGen a)]
    comps
                                      let (finalCfg :: CgConfig
    finalCfg, finalPgm :: CgPgmBundle
    finalPgm) = FilePath -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
    mergeToLib FilePath
    libName [(CgConfig
    c, CgPgmBundle
    b) | (_, c :: CgConfig
    c, b :: CgPgmBundle
    b) <- [(a, CgConfig, CgPgmBundle)]
    resCfgBundles]
                                      ([a], CgConfig, CgPgmBundle) -> IO ([a], CgConfig, CgPgmBundle)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([a
    r | (r :: a
    r, _, _) <- [(a, CgConfig, CgPgmBundle)]
    resCfgBundles], CgConfig
    finalCfg, CgPgmBundle
    finalPgm)

    ---------------------------------------------------------------------------
    -- * Implementation
    ---------------------------------------------------------------------------

    -- token for the target language
    data SBVToC = SBVToC

    instance CgTarget SBVToC where
      targetName :: SBVToC -> FilePath
    targetName _ = "C"
      translate :: SBVToC -> CgConfig -> FilePath -> CgState -> Result -> CgPgmBundle
    translate _  = CgConfig -> FilePath -> CgState -> Result -> CgPgmBundle
    cgen

    -- Unexpected input, or things we will probably never support
    die :: String -> a
    die :: FilePath -> a
    die msg :: FilePath
    msg = FilePath -> a
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> a) -> FilePath -> a
    forall a b. (a -> b) -> a -> b
    $ "SBV->C: Unexpected: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    msg

    -- Unsupported features, or features TBD
    tbd :: String -> a
    tbd :: FilePath -> a
    tbd msg :: FilePath
    msg = FilePath -> a
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> a) -> FilePath -> a
    forall a b. (a -> b) -> a -> b
    $ "SBV->C: Not yet supported: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    msg

    cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle
    cgen :: CgConfig -> FilePath -> CgState -> Result -> CgPgmBundle
    cgen cfg :: CgConfig
    cfg nm :: FilePath
    nm st :: CgState
    st sbvProg :: Result
    sbvProg
       -- we rnf the main pg and the sig to make sure any exceptions in type conversion pop-out early enough
       -- this is purely cosmetic, of course..
       = FilePath -> ()
    forall a. NFData a => a -> ()
    rnf (Doc -> FilePath
    render Doc
    sig) () -> CgPgmBundle -> CgPgmBundle
    forall a b. a -> b -> b
    `seq` FilePath -> ()
    forall a. NFData a => a -> ()
    rnf (Doc -> FilePath
    render ([Doc] -> Doc
    vcat [Doc]
    body)) () -> CgPgmBundle -> CgPgmBundle
    forall a b. a -> b -> b
    `seq` CgPgmBundle
    result
      where result :: CgPgmBundle
    result = (Maybe Int, Maybe CgSRealType)
    -> [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle
    CgPgmBundle (Maybe Int, Maybe CgSRealType)
    bundleKind
                            ([(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle)
    -> [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle
    forall a b. (a -> b) -> a -> b
    $ [(FilePath, (CgPgmKind, [Doc]))]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    forall a b. [(a, (CgPgmKind, b))] -> [(a, (CgPgmKind, b))]
    filt [ ("Makefile",  ([FilePath] -> CgPgmKind
    CgMakefile [FilePath]
    flags, [Bool -> FilePath -> FilePath -> [FilePath] -> Doc
    genMake (CgConfig -> Bool
    cgGenDriver CgConfig
    cfg) FilePath
    nm FilePath
    nmd [FilePath]
    flags]))
                                   , (FilePath
    nm  FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".h", ([Doc] -> CgPgmKind
    CgHeader [Doc
    sig],   [(Maybe Int, Maybe CgSRealType) -> FilePath -> [Doc] -> Doc -> Doc
    genHeader (Maybe Int, Maybe CgSRealType)
    bundleKind FilePath
    nm [Doc
    sig] Doc
    extProtos]))
                                   , (FilePath
    nmd FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".c", (CgPgmKind
    CgDriver,         CgConfig
    -> [Integer]
    -> FilePath
    -> [(FilePath, CgVal)]
    -> [(FilePath, CgVal)]
    -> Maybe SV
    -> [Doc]
    genDriver CgConfig
    cfg [Integer]
    randVals FilePath
    nm [(FilePath, CgVal)]
    ins [(FilePath, CgVal)]
    outs Maybe SV
    mbRet))
                                   , (FilePath
    nm  FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".c", (CgPgmKind
    CgSource,         [Doc]
    body))
                                   ]

            (body :: [Doc]
    body, flagsNeeded :: [FilePath]
    flagsNeeded) = CgConfig
    -> FilePath
    -> Doc
    -> Result
    -> [(FilePath, CgVal)]
    -> [(FilePath, CgVal)]
    -> Maybe SV
    -> Doc
    -> ([Doc], [FilePath])
    genCProg CgConfig
    cfg FilePath
    nm Doc
    sig Result
    sbvProg [(FilePath, CgVal)]
    ins [(FilePath, CgVal)]
    outs Maybe SV
    mbRet Doc
    extDecls

            bundleKind :: (Maybe Int, Maybe CgSRealType)
    bundleKind = (CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg, CgConfig -> Maybe CgSRealType
    cgReal CgConfig
    cfg)

            randVals :: [Integer]
    randVals = CgConfig -> [Integer]
    cgDriverVals CgConfig
    cfg

            filt :: [(a, (CgPgmKind, b))] -> [(a, (CgPgmKind, b))]
    filt xs :: [(a, (CgPgmKind, b))]
    xs  = [(a, (CgPgmKind, b))
    c | c :: (a, (CgPgmKind, b))
    c@(_, (k :: CgPgmKind
    k, _)) <- [(a, (CgPgmKind, b))]
    xs, CgPgmKind -> Bool
    need CgPgmKind
    k]
              where need :: CgPgmKind -> Bool
    need k :: CgPgmKind
    k | CgPgmKind -> Bool
    isCgDriver   CgPgmKind
    k = CgConfig -> Bool
    cgGenDriver CgConfig
    cfg
                           | CgPgmKind -> Bool
    isCgMakefile CgPgmKind
    k = CgConfig -> Bool
    cgGenMakefile CgConfig
    cfg
                           | Bool
    True           = Bool
    True

            nmd :: FilePath
    nmd      = FilePath
    nm FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "_driver"
            sig :: Doc
    sig      = FilePath
    -> [(FilePath, CgVal)] -> [(FilePath, CgVal)] -> Maybe SV -> Doc
    pprCFunHeader FilePath
    nm [(FilePath, CgVal)]
    ins [(FilePath, CgVal)]
    outs Maybe SV
    mbRet
            ins :: [(FilePath, CgVal)]
    ins      = CgState -> [(FilePath, CgVal)]
    cgInputs CgState
    st
            outs :: [(FilePath, CgVal)]
    outs     = CgState -> [(FilePath, CgVal)]
    cgOutputs CgState
    st
            mbRet :: Maybe SV
    mbRet    = case CgState -> [CgVal]
    cgReturns CgState
    st of
                         []           -> Maybe SV
    forall a. Maybe a
    Nothing
                         [CgAtomic o :: SV
    o] -> SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    o
                         [CgArray _]  -> FilePath -> Maybe SV
    forall a. FilePath -> a
    tbd "Non-atomic return values"
                         _            -> FilePath -> Maybe SV
    forall a. FilePath -> a
    tbd "Multiple return values"
            extProtos :: Doc
    extProtos = case CgState -> [FilePath]
    cgPrototypes CgState
    st of
                         [] -> Doc
    empty
                         xs :: [FilePath]
    xs -> [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Doc
    text "/* User given prototypes: */" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (FilePath -> Doc) -> [FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Doc
    text [FilePath]
    xs
            extDecls :: Doc
    extDecls  = case CgState -> [FilePath]
    cgDecls CgState
    st of
                         [] -> Doc
    empty
                         xs :: [FilePath]
    xs -> [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Doc
    text "/* User given declarations: */" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (FilePath -> Doc) -> [FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Doc
    text [FilePath]
    xs
            flags :: [FilePath]
    flags    = [FilePath]
    flagsNeeded [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ CgState -> [FilePath]
    cgLDFlags CgState
    st

    -- | Pretty print a functions type. If there is only one output, we compile it
    -- as a function that returns that value. Otherwise, we compile it as a void function
    -- that takes return values as pointers to be updated.
    pprCFunHeader :: String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc
    pprCFunHeader :: FilePath
    -> [(FilePath, CgVal)] -> [(FilePath, CgVal)] -> Maybe SV -> Doc
    pprCFunHeader fn :: FilePath
    fn ins :: [(FilePath, CgVal)]
    ins outs :: [(FilePath, CgVal)]
    outs mbRet :: Maybe SV
    mbRet = Doc
    retType Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    fn Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma (((FilePath, CgVal) -> Doc) -> [(FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> Doc
    mkParam [(FilePath, CgVal)]
    ins [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ ((FilePath, CgVal) -> Doc) -> [(FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> Doc
    mkPParam [(FilePath, CgVal)]
    outs)))
      where retType :: Doc
    retType = case Maybe SV
    mbRet of
                       Nothing -> FilePath -> Doc
    text "void"
                       Just sv :: SV
    sv -> Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv

    mkParam, mkPParam :: (String, CgVal) -> Doc
    mkParam :: (FilePath, CgVal) -> Doc
    mkParam  (n :: FilePath
    n, CgAtomic sv :: SV
    sv)     = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    True  SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    n
    mkParam  (_, CgArray  [])     = FilePath -> Doc
    forall a. FilePath -> a
    die "mkParam: CgArray with no elements!"
    mkParam  (n :: FilePath
    n, CgArray  (sv :: SV
    sv:_)) = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    True  SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text FilePath
    n
    mkPParam :: (FilePath, CgVal) -> Doc
    mkPParam (n :: FilePath
    n, CgAtomic sv :: SV
    sv)     = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text FilePath
    n
    mkPParam (_, CgArray  [])     = FilePath -> Doc
    forall a. FilePath -> a
    die "mPkParam: CgArray with no elements!"
    mkPParam (n :: FilePath
    n, CgArray  (sv :: SV
    sv:_)) = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text FilePath
    n

    -- | Renders as "const SWord8 s0", etc. the first parameter is the width of the typefield
    declSV :: Int -> SV -> Doc
    declSV :: Int -> SV -> Doc
    declSV w :: Int
    w sv :: SV
    sv = FilePath -> Doc
    text "const" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    pad (SV -> FilePath
    forall a. HasKind a => a -> FilePath
    showCType SV
    sv) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text (SV -> FilePath
    forall a. Show a => a -> FilePath
    show SV
    sv)
      where pad :: FilePath -> Doc
    pad s :: FilePath
    s = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    s FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> FilePath
    forall a. Int -> a -> [a]
    replicate (Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length FilePath
    s) ' '

    -- | Return the proper declaration and the result as a pair. No consts
    declSVNoConst :: Int -> SV -> (Doc, Doc)
    declSVNoConst :: Int -> SV -> (Doc, Doc)
    declSVNoConst w :: Int
    w sv :: SV
    sv = (FilePath -> Doc
    text "     " Doc -> Doc -> Doc
    <+> FilePath -> Doc
    pad (SV -> FilePath
    forall a. HasKind a => a -> FilePath
    showCType SV
    sv), FilePath -> Doc
    text (SV -> FilePath
    forall a. Show a => a -> FilePath
    show SV
    sv))
      where pad :: FilePath -> Doc
    pad s :: FilePath
    s = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    s FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> FilePath
    forall a. Int -> a -> [a]
    replicate (Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length FilePath
    s) ' '

    -- | Renders as "s0", etc, or the corresponding constant
    showSV :: CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV :: CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV cfg :: CgConfig
    cfg consts :: [(SV, CV)]
    consts sv :: SV
    sv
      | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV                 = FilePath -> Doc
    text "false"
      | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV                  = FilePath -> Doc
    text "true"
      | Just cv :: CV
    cv <- SV
    sv SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts = CgConfig -> CV -> Doc
    mkConst CgConfig
    cfg CV
    cv
      | Bool
    True                          = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ SV -> FilePath
    forall a. Show a => a -> FilePath
    show SV
    sv

    -- | Words as it would map to a C word
    pprCWord :: HasKind a => Bool -> a -> Doc
    pprCWord :: Bool -> a -> Doc
    pprCWord cnst :: Bool
    cnst v :: a
    v = (if Bool
    cnst then FilePath -> Doc
    text "const" else Doc
    empty) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text (a -> FilePath
    forall a. HasKind a => a -> FilePath
    showCType a
    v)

    -- | Almost a "show", but map "SWord1" to "SBool"
    -- which is used for extracting one-bit words.
    showCType :: HasKind a => a -> String
    showCType :: a -> FilePath
    showCType i :: a
    i = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    i of
                    KBounded False 1 -> "SBool"
                    k :: Kind
    k                -> Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k

    -- | The printf specifier for the type
    specifier :: CgConfig -> SV -> Doc
    specifier :: CgConfig -> SV -> Doc
    specifier cfg :: CgConfig
    cfg sv :: SV
    sv = case SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    sv of
                         KBool              -> (Bool, Int) -> Doc
    spec (Bool
    False, 1)
                         KBounded b :: Bool
    b i :: Int
    i       -> (Bool, Int) -> Doc
    spec (Bool
    b, Int
    i)
                         KUnbounded         -> (Bool, Int) -> Doc
    spec (Bool
    True, Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg))
                         KReal              -> CgSRealType -> Doc
    specF (Maybe CgSRealType -> CgSRealType
    forall a. HasCallStack => Maybe a -> a
    fromJust (CgConfig -> Maybe CgSRealType
    cgReal CgConfig
    cfg))
                         KFloat             -> CgSRealType -> Doc
    specF CgSRealType
    CgFloat
                         KDouble            -> CgSRealType -> Doc
    specF CgSRealType
    CgDouble
                         KString            -> FilePath -> Doc
    text "%s"
                         KChar              -> FilePath -> Doc
    text "%c"
                         KList k :: Kind
    k            -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "list sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k
                         KSet  k :: Kind
    k            -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "set sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k
                         KUninterpreted s :: FilePath
    s _ -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "uninterpreted sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    s
                         KTuple k :: [Kind]
    k           -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "tuple sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> FilePath
    forall a. Show a => a -> FilePath
    show [Kind]
    k
                         KMaybe  k :: Kind
    k          -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "maybe sort: "  FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k
                         KEither k1 :: Kind
    k1 k2 :: Kind
    k2      -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "either sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> FilePath
    forall a. Show a => a -> FilePath
    show (Kind
    k1, Kind
    k2)
      where u8InHex :: Bool
    u8InHex = CgConfig -> Bool
    cgShowU8InHex CgConfig
    cfg

            spec :: (Bool, Int) -> Doc
            spec :: (Bool, Int) -> Doc
    spec (False,  1) = FilePath -> Doc
    text "%d"
            spec (False,  8)
              | Bool
    u8InHex      = FilePath -> Doc
    text "0x%02\"PRIx8\""
              | Bool
    True         = FilePath -> Doc
    text "%\"PRIu8\""
            spec (True,   8) = FilePath -> Doc
    text "%\"PRId8\""
            spec (False, 16) = FilePath -> Doc
    text "0x%04\"PRIx16\"U"
            spec (True,  16) = FilePath -> Doc
    text "%\"PRId16\""
            spec (False, 32) = FilePath -> Doc
    text "0x%08\"PRIx32\"UL"
            spec (True,  32) = FilePath -> Doc
    text "%\"PRId32\"L"
            spec (False, 64) = FilePath -> Doc
    text "0x%016\"PRIx64\"ULL"
            spec (True,  64) = FilePath -> Doc
    text "%\"PRId64\"LL"
            spec (s :: Bool
    s, sz :: Int
    sz)     = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Format specifier at type " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (if Bool
    s then "SInt" else "SWord") FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    sz

            specF :: CgSRealType -> Doc
            specF :: CgSRealType -> Doc
    specF CgFloat      = FilePath -> Doc
    text "%a"
            specF CgDouble     = FilePath -> Doc
    text "%a"
            specF CgLongDouble = FilePath -> Doc
    text "%Lf"

    -- | Make a constant value of the given type. We don't check for out of bounds here, as it should not be needed.
    --   There are many options here, using binary, decimal, etc. We simply use decimal for values 8-bits or less,
    --   and hex otherwise.
    mkConst :: CgConfig -> CV -> Doc
    mkConst :: CgConfig -> CV -> Doc
    mkConst cfg :: CgConfig
    cfg  (CV KReal (CAlgReal (AlgRational _ r :: Rational
    r))) = Double -> Doc
    double (Rational -> Double
    forall a. Fractional a => Rational -> a
    fromRational Rational
    r :: Double) Doc -> Doc -> Doc
    P.<> CgSRealType -> Doc
    sRealSuffix (Maybe CgSRealType -> CgSRealType
    forall a. HasCallStack => Maybe a -> a
    fromJust (CgConfig -> Maybe CgSRealType
    cgReal CgConfig
    cfg))
      where sRealSuffix :: CgSRealType -> Doc
    sRealSuffix CgFloat      = FilePath -> Doc
    text "F"
            sRealSuffix CgDouble     = Doc
    empty
            sRealSuffix CgLongDouble = FilePath -> Doc
    text "L"
    mkConst cfg :: CgConfig
    cfg (CV KUnbounded       (CInteger i :: Integer
    i)) = Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst (CgConfig -> Bool
    cgShowU8InHex CgConfig
    cfg) Integer
    i (Bool
    True, Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg))
    mkConst cfg :: CgConfig
    cfg (CV (KBounded sg :: Bool
    sg sz :: Int
    sz) (CInteger i :: Integer
    i)) = Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst (CgConfig -> Bool
    cgShowU8InHex CgConfig
    cfg) Integer
    i (Bool
    sg,   Int
    sz)
    mkConst cfg :: CgConfig
    cfg (CV KBool            (CInteger i :: Integer
    i)) = Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst (CgConfig -> Bool
    cgShowU8InHex CgConfig
    cfg) Integer
    i (Bool
    False, 1)
    mkConst _   (CV KFloat           (CFloat f :: Float
    f))   = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Float -> FilePath
    showCFloat Float
    f
    mkConst _   (CV KDouble          (CDouble d :: Double
    d))  = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Double -> FilePath
    showCDouble Double
    d
    mkConst _   (CV KString          (CString s :: FilePath
    s))  = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    s
    mkConst _   (CV KChar            (CChar c :: Char
    c))    = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Char -> FilePath
    forall a. Show a => a -> FilePath
    show Char
    c
    mkConst _   cv :: CV
    cv                                 = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "mkConst: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ CV -> FilePath
    forall a. Show a => a -> FilePath
    show CV
    cv

    showSizedConst :: Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst :: Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst _   i :: Integer
    i   (False,  1) = FilePath -> Doc
    text (if Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then "false" else "true")
    showSizedConst u8h :: Bool
    u8h i :: Integer
    i t :: (Bool, Int)
    t@(False,  8)
      | Bool
    u8h                            = FilePath -> Doc
    text (Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i)
      | Bool
    True                           = Integer -> Doc
    integer Integer
    i
    showSizedConst _   i :: Integer
    i   (True,   8) = Integer -> Doc
    integer Integer
    i
    showSizedConst _   i :: Integer
    i t :: (Bool, Int)
    t@(False, 16) = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i
    showSizedConst _   i :: Integer
    i t :: (Bool, Int)
    t@(True,  16) = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i
    showSizedConst _   i :: Integer
    i t :: (Bool, Int)
    t@(False, 32) = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i
    showSizedConst _   i :: Integer
    i t :: (Bool, Int)
    t@(True,  32) = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i
    showSizedConst _   i :: Integer
    i t :: (Bool, Int)
    t@(False, 64) = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i
    showSizedConst _   i :: Integer
    i t :: (Bool, Int)
    t@(True,  64) = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> (Bool, Int) -> Integer -> FilePath
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> FilePath
    chex Bool
    False Bool
    True (Bool, Int)
    t Integer
    i
    showSizedConst _   i :: Integer
    i   (True,  1)  = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Signed 1-bit value " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Integer -> FilePath
    forall a. Show a => a -> FilePath
    show Integer
    i
    showSizedConst _   i :: Integer
    i   (s :: Bool
    s, sz :: Int
    sz)     = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Constant " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Integer -> FilePath
    forall a. Show a => a -> FilePath
    show Integer
    i FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " at type " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (if Bool
    s then "SInt" else "SWord") FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    sz

    -- | Generate a makefile. The first argument is True if we have a driver.
    genMake :: Bool -> String -> String -> [String] -> Doc
    genMake :: Bool -> FilePath -> FilePath -> [FilePath] -> Doc
    genMake ifdr :: Bool
    ifdr fn :: FilePath
    fn dn :: FilePath
    dn ldFlags :: [FilePath]
    ldFlags = (Doc -> Doc -> Doc) -> [Doc] -> Doc
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Doc -> Doc -> Doc
    ($$) [Doc
    l | (True, l :: Doc
    l) <- [(Bool, Doc)]
    lns]
     where ifld :: Bool
    ifld = Bool -> Bool
    not ([FilePath] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [FilePath]
    ldFlags)
           ld :: Doc
    ld | Bool
    ifld = FilePath -> Doc
    text "${LDFLAGS}"
              | Bool
    True = Doc
    empty
           lns :: [(Bool, Doc)]
    lns = [ (Bool
    True, FilePath -> Doc
    text "# Makefile for" Doc -> Doc -> Doc
    <+> Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ". Automatically generated by SBV. Do not edit!")
                 , (Bool
    True, FilePath -> Doc
    text "")
                 , (Bool
    True, FilePath -> Doc
    text "# include any user-defined .mk file in the current directory.")
                 , (Bool
    True, FilePath -> Doc
    text "-include *.mk")
                 , (Bool
    True, FilePath -> Doc
    text "")
                 , (Bool
    True, FilePath -> Doc
    text "CC?=gcc")
                 , (Bool
    True, FilePath -> Doc
    text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer")
                 , (Bool
    ifld, FilePath -> Doc
    text "LDFLAGS?=" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ([FilePath] -> FilePath
    unwords [FilePath]
    ldFlags))
                 , (Bool
    True, FilePath -> Doc
    text "")
                 , (Bool
    ifdr, FilePath -> Doc
    text "all:" Doc -> Doc -> Doc
    <+> Doc
    nmd)
                 , (Bool
    ifdr, FilePath -> Doc
    text "")
                 , (Bool
    True, Doc
    nmo Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text (": " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    ppSameLine ([Doc] -> Doc
    hsep [Doc
    nmc, Doc
    nmh])))
                 , (Bool
    True, FilePath -> Doc
    text "\t${CC} ${CCFLAGS}" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "-c $< -o $@")
                 , (Bool
    True, FilePath -> Doc
    text "")
                 , (Bool
    ifdr, Doc
    nmdo Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Doc
    nmdc)
                 , (Bool
    ifdr, FilePath -> Doc
    text "\t${CC} ${CCFLAGS}" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "-c $< -o $@")
                 , (Bool
    ifdr, FilePath -> Doc
    text "")
                 , (Bool
    ifdr, Doc
    nmd Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text (": " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    ppSameLine ([Doc] -> Doc
    hsep [Doc
    nmo, Doc
    nmdo])))
                 , (Bool
    ifdr, FilePath -> Doc
    text "\t${CC} ${CCFLAGS}" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "$^ -o $@" Doc -> Doc -> Doc
    <+> Doc
    ld)
                 , (Bool
    ifdr, FilePath -> Doc
    text "")
                 , (Bool
    True, FilePath -> Doc
    text "clean:")
                 , (Bool
    True, FilePath -> Doc
    text "\trm -f *.o")
                 , (Bool
    True, FilePath -> Doc
    text "")
                 , (Bool
    ifdr, FilePath -> Doc
    text "veryclean: clean")
                 , (Bool
    ifdr, FilePath -> Doc
    text "\trm -f" Doc -> Doc -> Doc
    <+> Doc
    nmd)
                 , (Bool
    ifdr, FilePath -> Doc
    text "")
                 ]
           nm :: Doc
    nm   = FilePath -> Doc
    text FilePath
    fn
           nmd :: Doc
    nmd  = FilePath -> Doc
    text FilePath
    dn
           nmh :: Doc
    nmh  = Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".h"
           nmc :: Doc
    nmc  = Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".c"
           nmo :: Doc
    nmo  = Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".o"
           nmdc :: Doc
    nmdc = Doc
    nmd Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".c"
           nmdo :: Doc
    nmdo = Doc
    nmd Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".o"

    -- | Generate the header
    genHeader :: (Maybe Int, Maybe CgSRealType) -> String -> [Doc] -> Doc -> Doc
    genHeader :: (Maybe Int, Maybe CgSRealType) -> FilePath -> [Doc] -> Doc -> Doc
    genHeader (ik :: Maybe Int
    ik, rk :: Maybe CgSRealType
    rk) fn :: FilePath
    fn sigs :: [Doc]
    sigs protos :: Doc
    protos =
         FilePath -> Doc
    text "/* Header file for" Doc -> Doc -> Doc
    <+> Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ". Automatically generated by SBV. Do not edit! */"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#ifndef" Doc -> Doc -> Doc
    <+> Doc
    tag
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#define" Doc -> Doc -> Doc
    <+> Doc
    tag
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <stdio.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <stdlib.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <inttypes.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <stdint.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <stdbool.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <string.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <math.h>"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* The boolean type */"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef bool SBool;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* The float type */"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef float SFloat;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* The double type */"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef double SDouble;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* Unsigned bit-vectors */"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef uint8_t  SWord8;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef uint16_t SWord16;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef uint32_t SWord32;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef uint64_t SWord64;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* Signed bit-vectors */"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef int8_t  SInt8;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef int16_t SInt16;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef int32_t SInt32;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "typedef int64_t SInt64;"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ Doc
    imapping
      Doc -> Doc -> Doc
    $$ Doc
    rmapping
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ("/* Entry point prototype" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    plu FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ": */")
      Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat ((Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc -> Doc
    P.<> Doc
    semi) [Doc]
    sigs)
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
      Doc -> Doc -> Doc
    $$ Doc
    protos
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#endif /*" Doc -> Doc -> Doc
    <+> Doc
    tag Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*/"
      Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
     where nm :: Doc
    nm  = FilePath -> Doc
    text FilePath
    fn
           tag :: Doc
    tag = FilePath -> Doc
    text "__" Doc -> Doc -> Doc
    P.<> Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "__HEADER_INCLUDED__"
           plu :: FilePath
    plu = if [Doc] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Doc]
    sigs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 1 then "s" else ""
           imapping :: Doc
    imapping = case Maybe Int
    ik of
                        Nothing -> Doc
    empty
                        Just i :: Int
    i  ->    FilePath -> Doc
    text "/* User requested mapping for SInteger.                                 */"
                                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* NB. Loss of precision: Target type is subject to modular arithmetic. */"
                                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ("typedef SInt" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    i FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " SInteger;")
                                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
           rmapping :: Doc
    rmapping = case Maybe CgSRealType
    rk of
                        Nothing -> Doc
    empty
                        Just t :: CgSRealType
    t  ->    FilePath -> Doc
    text "/* User requested mapping for SReal.                          */"
                                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* NB. Loss of precision: Target type is subject to rounding. */"
                                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ("typedef " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ CgSRealType -> FilePath
    forall a. Show a => a -> FilePath
    show CgSRealType
    t FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " SReal;")
                                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""

    sepIf :: Bool -> Doc
    sepIf :: Bool -> Doc
    sepIf b :: Bool
    b = if Bool
    b then FilePath -> Doc
    text "" else Doc
    empty

    -- | Generate an example driver program
    genDriver :: CgConfig -> [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> [Doc]
    genDriver :: CgConfig
    -> [Integer]
    -> FilePath
    -> [(FilePath, CgVal)]
    -> [(FilePath, CgVal)]
    -> Maybe SV
    -> [Doc]
    genDriver cfg :: CgConfig
    cfg randVals :: [Integer]
    randVals fn :: FilePath
    fn inps :: [(FilePath, CgVal)]
    inps outs :: [(FilePath, CgVal)]
    outs mbRet :: Maybe SV
    mbRet = [Doc
    pre, Doc
    header, Doc
    body, Doc
    post]
     where pre :: Doc
    pre    =  FilePath -> Doc
    text "/* Example driver program for" Doc -> Doc -> Doc
    <+> Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ". */"
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* Automatically generated by SBV. Edit as you see fit! */"
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <stdio.h>"
           header :: Doc
    header =  FilePath -> Doc
    text "#include" Doc -> Doc -> Doc
    <+> Doc -> Doc
    doubleQuotes (Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".h")
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "int main(void)"
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "{"
           body :: Doc
    body   =  FilePath -> Doc
    text ""
                  Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 (   [Doc] -> Doc
    vcat ((([Doc], FilePath, CgVal) -> Doc)
    -> [([Doc], FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Doc], FilePath, CgVal) -> Doc
    mkInp [([Doc], FilePath, CgVal)]
    pairedInputs)
                          Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat (((FilePath, CgVal) -> Doc) -> [(FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> Doc
    mkOut [(FilePath, CgVal)]
    outs)
                          Doc -> Doc -> Doc
    $$ Bool -> Doc
    sepIf (Bool -> Bool
    not ([()] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | (_, _, CgArray{}) <- [([Doc], FilePath, CgVal)]
    pairedInputs]) Bool -> Bool -> Bool
    || Bool -> Bool
    not ([(FilePath, CgVal)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(FilePath, CgVal)]
    outs))
                          Doc -> Doc -> Doc
    $$ Doc
    call
                          Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
                          Doc -> Doc -> Doc
    $$ (case Maybe SV
    mbRet of
                                  Just sv :: SV
    sv -> FilePath -> Doc
    text "printf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens (Doc -> Doc
    printQuotes (Doc
    fcall Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> CgConfig -> SV -> Doc
    specifier CgConfig
    cfg SV
    sv Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "\\n")
                                                                                  Doc -> Doc -> Doc
    P.<> Doc
    comma Doc -> Doc -> Doc
    <+> Doc
    resultVar) Doc -> Doc -> Doc
    P.<> Doc
    semi
                                  Nothing -> FilePath -> Doc
    text "printf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens (Doc -> Doc
    printQuotes (Doc
    fcall Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "->\\n")) Doc -> Doc -> Doc
    P.<> Doc
    semi)
                          Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat (((FilePath, CgVal) -> Doc) -> [(FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> Doc
    display [(FilePath, CgVal)]
    outs)
                          )
           post :: Doc
    post   =   FilePath -> Doc
    text ""
                  Doc -> Doc -> Doc
    $+$ Int -> Doc -> Doc
    nest 2 (FilePath -> Doc
    text "return 0" Doc -> Doc -> Doc
    P.<> Doc
    semi)
                  Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "}"
                  Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text ""
           nm :: Doc
    nm = FilePath -> Doc
    text FilePath
    fn
           pairedInputs :: [([Doc], FilePath, CgVal)]
    pairedInputs = [Integer] -> [(FilePath, CgVal)] -> [([Doc], FilePath, CgVal)]
    forall a b.
    (Integral a, Show b) =>
    [a] -> [(b, CgVal)] -> [([Doc], b, CgVal)]
    matchRands [Integer]
    randVals [(FilePath, CgVal)]
    inps
           matchRands :: [a] -> [(b, CgVal)] -> [([Doc], b, CgVal)]
    matchRands _      []                                 = []
           matchRands []     _                                  = FilePath -> [([Doc], b, CgVal)]
    forall a. FilePath -> a
    die "Run out of driver values!"
           matchRands (r :: a
    r:rs :: [a]
    rs) ((n :: b
    n, CgAtomic sv :: SV
    sv)            : cs :: [(b, CgVal)]
    cs) = ([SV -> a -> Doc
    forall a a. (Integral a, HasKind a) => a -> a -> Doc
    mkRVal SV
    sv a
    r], b
    n, SV -> CgVal
    CgAtomic SV
    sv) ([Doc], b, CgVal) -> [([Doc], b, CgVal)] -> [([Doc], b, CgVal)]
    forall a. a -> [a] -> [a]
    : [a] -> [(b, CgVal)] -> [([Doc], b, CgVal)]
    matchRands [a]
    rs [(b, CgVal)]
    cs
           matchRands _      ((n :: b
    n, CgArray [])             : _ ) = FilePath -> [([Doc], b, CgVal)]
    forall a. FilePath -> a
    die (FilePath -> [([Doc], b, CgVal)])
    -> FilePath -> [([Doc], b, CgVal)]
    forall a b. (a -> b) -> a -> b
    $ "Unsupported empty array input " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ b -> FilePath
    forall a. Show a => a -> FilePath
    show b
    n
           matchRands rs :: [a]
    rs     ((n :: b
    n, a :: CgVal
    a@(CgArray sws :: [SV]
    sws@(sv :: SV
    sv:_))) : cs :: [(b, CgVal)]
    cs)
              | [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    frs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    l                                 = FilePath -> [([Doc], b, CgVal)]
    forall a. FilePath -> a
    die "Run out of driver values!"
              | Bool
    True                                            = ((a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV -> a -> Doc
    forall a a. (Integral a, HasKind a) => a -> a -> Doc
    mkRVal SV
    sv) [a]
    frs, b
    n, CgVal
    a) ([Doc], b, CgVal) -> [([Doc], b, CgVal)] -> [([Doc], b, CgVal)]
    forall a. a -> [a] -> [a]
    : [a] -> [(b, CgVal)] -> [([Doc], b, CgVal)]
    matchRands [a]
    srs [(b, CgVal)]
    cs
              where l :: Int
    l          = [SV] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SV]
    sws
                    (frs :: [a]
    frs, srs :: [a]
    srs) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    l [a]
    rs
           mkRVal :: a -> a -> Doc
    mkRVal sv :: a
    sv r :: a
    r = CgConfig -> CV -> Doc
    mkConst CgConfig
    cfg (CV -> Doc) -> CV -> Doc
    forall a b. (a -> b) -> a -> b
    $ Kind -> a -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    sv) a
    r
           mkInp :: ([Doc], FilePath, CgVal) -> Doc
    mkInp (_,  _, CgAtomic{})         = Doc
    empty  -- constant, no need to declare
           mkInp (_,  n :: FilePath
    n, CgArray [])         = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Unsupported empty array value for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    n
           mkInp (vs :: [Doc]
    vs, n :: FilePath
    n, CgArray sws :: [SV]
    sws@(sv :: SV
    sv:_)) =  Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    True SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    n Doc -> Doc -> Doc
    P.<> Doc -> Doc
    brackets (Int -> Doc
    int ([SV] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SV]
    sws)) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "= {"
                                                          Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 4 ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]
    align [Doc]
    vs)))
                                                          Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "};"
                                             Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
                                             Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "printf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens (Doc -> Doc
    printQuotes (FilePath -> Doc
    text "Contents of input array" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    n Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ":\\n")) Doc -> Doc -> Doc
    P.<> Doc
    semi
                                             Doc -> Doc -> Doc
    $$ (FilePath, CgVal) -> Doc
    display (FilePath
    n, [SV] -> CgVal
    CgArray [SV]
    sws)
                                             Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
           mkOut :: (FilePath, CgVal) -> Doc
    mkOut (v :: FilePath
    v, CgAtomic sv :: SV
    sv)            = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    v Doc -> Doc -> Doc
    P.<> Doc
    semi
           mkOut (v :: FilePath
    v, CgArray [])             = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Unsupported empty array value for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    v
           mkOut (v :: FilePath
    v, CgArray sws :: [SV]
    sws@(sv :: SV
    sv:_))     = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    v Doc -> Doc -> Doc
    P.<> Doc -> Doc
    brackets (Int -> Doc
    int ([SV] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SV]
    sws)) Doc -> Doc -> Doc
    P.<> Doc
    semi
           resultVar :: Doc
    resultVar = FilePath -> Doc
    text "__result"
           call :: Doc
    call = case Maybe SV
    mbRet of
                    Nothing -> Doc
    fcall Doc -> Doc -> Doc
    P.<> Doc
    semi
                    Just sv :: SV
    sv -> Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    True SV
    sv Doc -> Doc -> Doc
    <+> Doc
    resultVar Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> Doc
    fcall Doc -> Doc -> Doc
    P.<> Doc
    semi
           fcall :: Doc
    fcall = Doc
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ((([Doc], FilePath, CgVal) -> Doc)
    -> [([Doc], FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Doc], FilePath, CgVal) -> Doc
    mkCVal [([Doc], FilePath, CgVal)]
    pairedInputs [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ ((FilePath, CgVal) -> Doc) -> [(FilePath, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> Doc
    mkOVal [(FilePath, CgVal)]
    outs)))
           mkCVal :: ([Doc], FilePath, CgVal) -> Doc
    mkCVal ([v :: Doc
    v], _, CgAtomic{}) = Doc
    v
           mkCVal (vs :: [Doc]
    vs,  n :: FilePath
    n, CgAtomic{}) = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Unexpected driver value computed for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    n FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Doc -> FilePath
    render ([Doc] -> Doc
    hcat [Doc]
    vs)
           mkCVal (_,   n :: FilePath
    n, CgArray{})  = FilePath -> Doc
    text FilePath
    n
           mkOVal :: (FilePath, CgVal) -> Doc
    mkOVal (n :: FilePath
    n, CgAtomic{})      = FilePath -> Doc
    text "&" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text FilePath
    n
           mkOVal (n :: FilePath
    n, CgArray{})       = FilePath -> Doc
    text FilePath
    n
           display :: (FilePath, CgVal) -> Doc
    display (n :: FilePath
    n, CgAtomic sv :: SV
    sv)         = FilePath -> Doc
    text "printf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens (Doc -> Doc
    printQuotes (FilePath -> Doc
    text " " Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    n Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> CgConfig -> SV -> Doc
    specifier CgConfig
    cfg SV
    sv
                                                                                    Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "\\n") Doc -> Doc -> Doc
    P.<> Doc
    comma Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    n) Doc -> Doc -> Doc
    P.<> Doc
    semi
           display (n :: FilePath
    n, CgArray [])         =  FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Unsupported empty array value for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    n
           display (n :: FilePath
    n, CgArray sws :: [SV]
    sws@(sv :: SV
    sv:_)) =   FilePath -> Doc
    text "int" Doc -> Doc -> Doc
    <+> Doc
    nctr Doc -> Doc -> Doc
    P.<> Doc
    semi
                                            Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "for(" Doc -> Doc -> Doc
    P.<> Doc
    nctr Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "= 0;" Doc -> Doc -> Doc
    <+> Doc
    nctr Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "<" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    len Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "; ++" Doc -> Doc -> Doc
    P.<> Doc
    nctr Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ")"
                                            Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 (FilePath -> Doc
    text "printf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens (Doc -> Doc
    printQuotes (FilePath -> Doc
    text " " Doc -> Doc -> Doc
    <+> Doc
    entrySpec Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> Doc
    spec Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "\\n")
                                                                     Doc -> Doc -> Doc
    P.<> Doc
    comma Doc -> Doc -> Doc
    <+> Doc
    nctr Doc -> Doc -> Doc
    <+> Doc
    comma Doc -> Doc -> Doc
    P.<> Doc
    entry) Doc -> Doc -> Doc
    P.<> Doc
    semi)
                      where nctr :: Doc
    nctr      = FilePath -> Doc
    text FilePath
    n Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "_ctr"
                            entry :: Doc
    entry     = FilePath -> Doc
    text FilePath
    n Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "[" Doc -> Doc -> Doc
    P.<> Doc
    nctr Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "]"
                            entrySpec :: Doc
    entrySpec = FilePath -> Doc
    text FilePath
    n Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "[%" Doc -> Doc -> Doc
    P.<> Int -> Doc
    int Int
    tab Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "d]"
                            spec :: Doc
    spec      = CgConfig -> SV -> Doc
    specifier CgConfig
    cfg SV
    sv
                            len :: Int
    len       = [SV] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SV]
    sws
                            tab :: Int
    tab       = FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ Int -> FilePath
    forall a. Show a => a -> FilePath
    show (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)

    -- | Generate the C program
    genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc -> ([Doc], [String])
    genCProg :: CgConfig
    -> FilePath
    -> Doc
    -> Result
    -> [(FilePath, CgVal)]
    -> [(FilePath, CgVal)]
    -> Maybe SV
    -> Doc
    -> ([Doc], [FilePath])
    genCProg cfg :: CgConfig
    cfg fn :: FilePath
    fn proto :: Doc
    proto (Result kindInfo :: Set Kind
    kindInfo _tvals :: [(FilePath, CV)]
    _tvals _ovals :: [(FilePath, CV -> Bool, SV)]
    _ovals cgs :: [(FilePath, [FilePath])]
    cgs ins :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
    ins preConsts :: [(SV, CV)]
    preConsts tbls :: [((Int, Kind, Kind), [SV])]
    tbls arrs :: [(Int, ArrayInfo)]
    arrs _uis :: [(FilePath, SBVType)]
    _uis _axioms :: [(FilePath, [FilePath])]
    _axioms (SBVPgm asgns :: Seq (SV, SBVExpr)
    asgns) cstrs :: Seq (Bool, [(FilePath, FilePath)], SV)
    cstrs origAsserts :: [(FilePath, Maybe CallStack, SV)]
    origAsserts _) inVars :: [(FilePath, CgVal)]
    inVars outVars :: [(FilePath, CgVal)]
    outVars mbRet :: Maybe SV
    mbRet extDecls :: Doc
    extDecls
      | Maybe Int -> Bool
    forall a. Maybe a -> Bool
    isNothing (CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg) Bool -> Bool -> Bool
    && Kind
    KUnbounded Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> ([Doc], [FilePath]))
    -> FilePath -> ([Doc], [FilePath])
    forall a b. (a -> b) -> a -> b
    $ "SBV->C: Unbounded integers are not supported by the C compiler."
              FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."
      | Kind
    KString Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Strings are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | Kind
    KChar Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Characters are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isSet Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Sets (SSet) are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isList Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Lists (SList) are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isTuple Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Tuples (STupleN) are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isMaybe Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Optional (SMaybe) values are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isEither Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Either (SEither) values are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"
      | Maybe CgSRealType -> Bool
    forall a. Maybe a -> Bool
    isNothing (CgConfig -> Maybe CgSRealType
    cgReal CgConfig
    cfg) Bool -> Bool -> Bool
    && Kind
    KReal Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> ([Doc], [FilePath]))
    -> FilePath -> ([Doc], [FilePath])
    forall a b. (a -> b) -> a -> b
    $ "SBV->C: SReal values are not supported by the C compiler."
              FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\nUse 'cgSRealType' to specify a custom type for SReal representation."
      | Bool -> Bool
    not ([FilePath] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [FilePath]
    usorts)
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> ([Doc], [FilePath]))
    -> FilePath -> ([Doc], [FilePath])
    forall a b. (a -> b) -> a -> b
    $ "SBV->C: Cannot compile functions with uninterpreted sorts: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> [FilePath] -> FilePath
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [FilePath]
    usorts
      | Bool -> Bool
    not (Seq (Bool, [(FilePath, FilePath)], SV) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Bool, [(FilePath, FilePath)], SV)
    cstrs)
      = FilePath -> ([Doc], [FilePath])
    forall a. FilePath -> a
    tbd "Explicit constraints"
      | Bool -> Bool
    not ([(Int, ArrayInfo)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Int, ArrayInfo)]
    arrs)
      = FilePath -> ([Doc], [FilePath])
    forall a. FilePath -> a
    tbd "User specified arrays"
      | [Quantifier] -> Bool
    needsExistentials (((Quantifier, NamedSymVar) -> Quantifier)
    -> [(Quantifier, NamedSymVar)] -> [Quantifier]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier, NamedSymVar) -> Quantifier
    forall a b. (a, b) -> a
    fst (([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(Quantifier, NamedSymVar)]
    forall a b. (a, b) -> a
    fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
    ins))
      = FilePath -> ([Doc], [FilePath])
    forall a. HasCallStack => FilePath -> a
    error "SBV->C: Cannot compile functions with existentially quantified variables."
      | Bool
    True
      = ([Doc
    pre, Doc
    header, Doc
    post], [FilePath]
    flagsNeeded)
     where asserts :: [(FilePath, Maybe CallStack, SV)]
    asserts | CgConfig -> Bool
    cgIgnoreAsserts CgConfig
    cfg = []
                   | Bool
    True                = [(FilePath, Maybe CallStack, SV)]
    origAsserts

           usorts :: [FilePath]
    usorts = [FilePath
    s | KUninterpreted s :: FilePath
    s _ <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo, FilePath
    s FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    /= "RoundingMode"] -- No support for any sorts other than RoundingMode!

           pre :: Doc
    pre    =  FilePath -> Doc
    text "/* File:" Doc -> Doc -> Doc
    <+> Doc -> Doc
    doubleQuotes (Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".c") Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ". Automatically generated by SBV. Do not edit! */"
                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""

           header :: Doc
    header = FilePath -> Doc
    text "#include" Doc -> Doc -> Doc
    <+> Doc -> Doc
    doubleQuotes (Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ".h")

           post :: Doc
    post   = FilePath -> Doc
    text ""
                 Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat (((FilePath, [FilePath]) -> Doc)
    -> [(FilePath, [FilePath])] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, [FilePath]) -> Doc
    codeSeg [(FilePath, [FilePath])]
    cgs)
                 Doc -> Doc -> Doc
    $$ Doc
    extDecls
                 Doc -> Doc -> Doc
    $$ Doc
    proto
                 Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "{"
                 Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
                 Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 (   [Doc] -> Doc
    vcat (((FilePath, CgVal) -> [Doc]) -> [(FilePath, CgVal)] -> [Doc]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Bool -> (Bool, (FilePath, CgVal)) -> [Doc]
    genIO Bool
    True ((Bool, (FilePath, CgVal)) -> [Doc])
    -> ((FilePath, CgVal) -> (Bool, (FilePath, CgVal)))
    -> (FilePath, CgVal)
    -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\v :: (FilePath, CgVal)
    v -> ((FilePath, CgVal) -> Bool
    isAlive (FilePath, CgVal)
    v, (FilePath, CgVal)
    v))) [(FilePath, CgVal)]
    inVars)
                            Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat ([(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)] -> [Doc]
    merge ((((Int, Kind, Kind), [SV]) -> (Int, Doc))
    -> [((Int, Kind, Kind), [SV])] -> [(Int, Doc)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int, Kind, Kind), [SV]) -> (Int, Doc)
    genTbl [((Int, Kind, Kind), [SV])]
    tbls) (((SV, SBVExpr) -> (Int, Doc)) -> [(SV, SBVExpr)] -> [(Int, Doc)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, SBVExpr) -> (Int, Doc)
    genAsgn [(SV, SBVExpr)]
    assignments) (((FilePath, Maybe CallStack, SV) -> (Int, Doc))
    -> [(FilePath, Maybe CallStack, SV)] -> [(Int, Doc)]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, Maybe CallStack, SV) -> (Int, Doc)
    genAssert [(FilePath, Maybe CallStack, SV)]
    asserts))
                            Doc -> Doc -> Doc
    $$ Bool -> Doc
    sepIf (Bool -> Bool
    not ([(SV, SBVExpr)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(SV, SBVExpr)]
    assignments) Bool -> Bool -> Bool
    || Bool -> Bool
    not ([((Int, Kind, Kind), [SV])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Int, Kind, Kind), [SV])]
    tbls))
                            Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat (((Bool, (FilePath, CgVal)) -> [Doc])
    -> [(Bool, (FilePath, CgVal))] -> [Doc]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Bool -> (Bool, (FilePath, CgVal)) -> [Doc]
    genIO Bool
    False) ([Bool] -> [(FilePath, CgVal)] -> [(Bool, (FilePath, CgVal))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    True) [(FilePath, CgVal)]
    outVars))
                            Doc -> Doc -> Doc
    $$ Doc -> (SV -> Doc) -> Maybe SV -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    empty SV -> Doc
    mkRet Maybe SV
    mbRet
                           )
                 Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "}"
                 Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""

           nm :: Doc
    nm = FilePath -> Doc
    text FilePath
    fn

           assignments :: [(SV, SBVExpr)]
    assignments = Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (SV, SBVExpr)
    asgns

           -- Do we need any linker flags for C?
           flagsNeeded :: [FilePath]
    flagsNeeded = [FilePath] -> [FilePath]
    forall a. Eq a => [a] -> [a]
    nub ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> a -> b
    $ ((SV, SBVExpr) -> [FilePath]) -> [(SV, SBVExpr)] -> [FilePath]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((Op, Kind) -> [FilePath]
    getLDFlag ((Op, Kind) -> [FilePath])
    -> ((SV, SBVExpr) -> (Op, Kind)) -> (SV, SBVExpr) -> [FilePath]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SV, SBVExpr) -> (Op, Kind)
    forall a. HasKind a => (a, SBVExpr) -> (Op, Kind)
    opRes) [(SV, SBVExpr)]
    assignments
              where opRes :: (a, SBVExpr) -> (Op, Kind)
    opRes (sv :: a
    sv, SBVApp o :: Op
    o _) = (Op
    o, a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    sv)

           codeSeg :: (FilePath, [FilePath]) -> Doc
    codeSeg (fnm :: FilePath
    fnm, ls :: [FilePath]
    ls) =  FilePath -> Doc
    text "/* User specified custom code for" Doc -> Doc -> Doc
    <+> Doc -> Doc
    doubleQuotes (FilePath -> Doc
    text FilePath
    fnm) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*/"
                             Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat ((FilePath -> Doc) -> [FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Doc
    text [FilePath]
    ls)
                             Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""

           typeWidth :: Int
    typeWidth = Int -> [Int] -> Int
    forall t. (Num t, Ord t) => t -> [t] -> t
    getMax 0 ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $ [Kind -> Int
    len (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s) | (s :: SV
    s, _) <- [(SV, SBVExpr)]
    assignments] [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [Kind -> Int
    len (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s) | (_, (s :: SV
    s, _)) <- ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(Quantifier, NamedSymVar)]
    forall a b. (a, b) -> a
    fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
    ins]
                    where len :: Kind -> Int
    len KReal{}              = 5
                          len KFloat{}             = 6 -- SFloat
                          len KDouble{}            = 7 -- SDouble
                          len KString{}            = 7 -- SString
                          len KChar{}              = 5 -- SChar
                          len KUnbounded{}         = 8
                          len KBool                = 5 -- SBool
                          len (KBounded False n :: Int
    n)   = 5 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    n) -- SWordN
                          len (KBounded True  n :: Int
    n)   = 4 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    n) -- SIntN
                          len (KList s :: Kind
    s)            = FilePath -> Int
    forall a. FilePath -> a
    die (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ "List sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    s
                          len (KSet  s :: Kind
    s)            = FilePath -> Int
    forall a. FilePath -> a
    die (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ "Set sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    s
                          len (KTuple s :: [Kind]
    s)           = FilePath -> Int
    forall a. FilePath -> a
    die (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ "Tuple sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> FilePath
    forall a. Show a => a -> FilePath
    show [Kind]
    s
                          len (KMaybe k :: Kind
    k)           = FilePath -> Int
    forall a. FilePath -> a
    die (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ "Maybe sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k
                          len (KEither k1 :: Kind
    k1 k2 :: Kind
    k2)      = FilePath -> Int
    forall a. FilePath -> a
    die (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ "Either sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> FilePath
    forall a. Show a => a -> FilePath
    show (Kind
    k1, Kind
    k2)
                          len (KUninterpreted s :: FilePath
    s _) = FilePath -> Int
    forall a. FilePath -> a
    die (FilePath -> Int) -> FilePath -> Int
    forall a b. (a -> b) -> a -> b
    $ "Uninterpreted sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    s

                          getMax :: t -> [t] -> t
    getMax 8 _      = 8  -- 8 is the max we can get with SInteger, so don't bother looking any further
                          getMax m :: t
    m []     = t
    m
                          getMax m :: t
    m (x :: t
    x:xs :: [t]
    xs) = t -> [t] -> t
    getMax (t
    m t -> t -> t
    forall a. Ord a => a -> a -> a
    `max` t
    x) [t]
    xs

           consts :: [(SV, CV)]
    consts = (SV
    falseSV, CV
    falseCV) (SV, CV) -> [(SV, CV)] -> [(SV, CV)]
    forall a. a -> [a] -> [a]
    : (SV
    trueSV, CV
    trueCV) (SV, CV) -> [(SV, CV)] -> [(SV, CV)]
    forall a. a -> [a] -> [a]
    : [(SV, CV)]
    preConsts

           isConst :: SV -> Bool
    isConst s :: SV
    s = Maybe CV -> Bool
    forall a. Maybe a -> Bool
    isJust (SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup SV
    s [(SV, CV)]
    consts)

           -- TODO: The following is brittle. We should really have a function elsewhere
           -- that walks the SBVExprs and collects the SWs together.
           usedVariables :: Set SV
    usedVariables = [Set SV] -> Set SV
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions (Set SV
    retSWs Set SV -> [Set SV] -> [Set SV]
    forall a. a -> [a] -> [a]
    : ((FilePath, CgVal) -> Set SV) -> [(FilePath, CgVal)] -> [Set SV]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> Set SV
    forall a. (a, CgVal) -> Set SV
    usedCgVal [(FilePath, CgVal)]
    outVars [Set SV] -> [Set SV] -> [Set SV]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> Set SV) -> [(SV, SBVExpr)] -> [Set SV]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, SBVExpr) -> Set SV
    forall a. (a, SBVExpr) -> Set SV
    usedAsgn [(SV, SBVExpr)]
    assignments)
             where retSWs :: Set SV
    retSWs = Set SV -> (SV -> Set SV) -> Maybe SV -> Set SV
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Set SV
    forall a. Set a
    Set.empty SV -> Set SV
    forall a. a -> Set a
    Set.singleton Maybe SV
    mbRet

                   usedCgVal :: (a, CgVal) -> Set SV
    usedCgVal (_, CgAtomic s :: SV
    s)  = SV -> Set SV
    forall a. a -> Set a
    Set.singleton SV
    s
                   usedCgVal (_, CgArray ss :: [SV]
    ss)  = [SV] -> Set SV
    forall a. Ord a => [a] -> Set a
    Set.fromList [SV]
    ss
                   usedAsgn :: (a, SBVExpr) -> Set SV
    usedAsgn  (_, SBVApp o :: Op
    o ss :: [SV]
    ss) = Set SV -> Set SV -> Set SV
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (Op -> Set SV
    opSWs Op
    o) ([SV] -> Set SV
    forall a. Ord a => [a] -> Set a
    Set.fromList [SV]
    ss)

                   opSWs :: Op -> Set SV
    opSWs (LkUp _ a :: SV
    a b :: SV
    b)             = [SV] -> Set SV
    forall a. Ord a => [a] -> Set a
    Set.fromList [SV
    a, SV
    b]
                   opSWs (IEEEFP (FP_Cast _ _ s :: SV
    s)) = SV -> Set SV
    forall a. a -> Set a
    Set.singleton SV
    s
                   opSWs _                        = Set SV
    forall a. Set a
    Set.empty

           isAlive :: (String, CgVal) -> Bool
           isAlive :: (FilePath, CgVal) -> Bool
    isAlive (_, CgAtomic sv :: SV
    sv) = SV
    sv SV -> Set SV -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set SV
    usedVariables
           isAlive (_, _)           = Bool
    True

           genIO :: Bool -> (Bool, (String, CgVal)) -> [Doc]
           genIO :: Bool -> (Bool, (FilePath, CgVal)) -> [Doc]
    genIO True  (alive :: Bool
    alive, (cNm :: FilePath
    cNm, CgAtomic sv :: SV
    sv)) = [Int -> SV -> Doc
    declSV Int
    typeWidth SV
    sv  Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    cNm Doc -> Doc -> Doc
    P.<> Doc
    semi               | Bool
    alive]
           genIO False (alive :: Bool
    alive, (cNm :: FilePath
    cNm, CgAtomic sv :: SV
    sv)) = [FilePath -> Doc
    text "*" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text FilePath
    cNm Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts SV
    sv Doc -> Doc -> Doc
    P.<> Doc
    semi | Bool
    alive]
           genIO isInp :: Bool
    isInp (_,     (cNm :: FilePath
    cNm, CgArray sws :: [SV]
    sws)) = (SV -> Int -> Doc) -> [SV] -> [Int] -> [Doc]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith SV -> Int -> Doc
    forall a. Show a => SV -> a -> Doc
    genElt [SV]
    sws [(0::Int)..]
             where genElt :: SV -> a -> Doc
    genElt sv :: SV
    sv i :: a
    i
                     | Bool
    isInp = Int -> SV -> Doc
    declSV Int
    typeWidth SV
    sv Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    entry       Doc -> Doc -> Doc
    P.<> Doc
    semi
                     | Bool
    True  = FilePath -> Doc
    text FilePath
    entry          Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts SV
    sv Doc -> Doc -> Doc
    P.<> Doc
    semi
                     where entry :: FilePath
    entry = FilePath
    cNm FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "[" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ a -> FilePath
    forall a. Show a => a -> FilePath
    show a
    i FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "]"

           mkRet :: SV -> Doc
    mkRet sv :: SV
    sv = FilePath -> Doc
    text "return" Doc -> Doc -> Doc
    <+> CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts SV
    sv Doc -> Doc -> Doc
    P.<> Doc
    semi

           genTbl :: ((Int, Kind, Kind), [SV]) -> (Int, Doc)
           genTbl :: ((Int, Kind, Kind), [SV]) -> (Int, Doc)
    genTbl ((i :: Int
    i, _, k :: Kind
    k), elts :: [SV]
    elts) =  (Int
    location, Doc
    static Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "const" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text (Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ("table" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    i) Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text "[] = {"
                                                  Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 4 ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ([Doc] -> [Doc]
    align ((SV -> Doc) -> [SV] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts) [SV]
    elts))))
                                                  Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "};")
             where static :: Doc
    static   = if Int
    location Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == -1 then FilePath -> Doc
    text "static" else Doc
    empty
                   location :: Int
    location = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (-1 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : (SV -> Int) -> [SV] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> Int
    getNodeId [SV]
    elts)

           getNodeId :: SV -> Int
    getNodeId s :: SV
    s@(SV _ (NodeId n :: Int
    n)) | SV -> Bool
    isConst SV
    s = -1
                                         | Bool
    True      = Int
    n

           genAsgn :: (SV, SBVExpr) -> (Int, Doc)
           genAsgn :: (SV, SBVExpr) -> (Int, Doc)
    genAsgn (sv :: SV
    sv, n :: SBVExpr
    n) = (SV -> Int
    getNodeId SV
    sv, CgConfig -> [(SV, CV)] -> SBVExpr -> Doc -> (Doc, Doc) -> Doc
    ppExpr CgConfig
    cfg [(SV, CV)]
    consts SBVExpr
    n (Int -> SV -> Doc
    declSV Int
    typeWidth SV
    sv) (Int -> SV -> (Doc, Doc)
    declSVNoConst Int
    typeWidth SV
    sv) Doc -> Doc -> Doc
    P.<> Doc
    semi)

           -- merge tables intermixed with assignments and assertions, paying attention to putting tables as
           -- early as possible and tables right after.. Note that the assignment list (second argument) is sorted on its order
           merge :: [(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)] -> [Doc]
           merge :: [(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)] -> [Doc]
    merge tables :: [(Int, Doc)]
    tables asgnments :: [(Int, Doc)]
    asgnments asrts :: [(Int, Doc)]
    asrts = ((Int, Doc) -> Doc) -> [(Int, Doc)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Doc) -> Doc
    forall a b. (a, b) -> b
    snd ([(Int, Doc)] -> [Doc]) -> [(Int, Doc)] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ [(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)]
    forall a b. Ord a => [(a, b)] -> [(a, b)] -> [(a, b)]
    merge2 [(Int, Doc)]
    asrts ([(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)]
    forall a b. Ord a => [(a, b)] -> [(a, b)] -> [(a, b)]
    merge2 [(Int, Doc)]
    tables [(Int, Doc)]
    asgnments)
             where merge2 :: [(a, b)] -> [(a, b)] -> [(a, b)]
    merge2 []               as :: [(a, b)]
    as                  = [(a, b)]
    as
                   merge2 ts :: [(a, b)]
    ts               []                  = [(a, b)]
    ts
                   merge2 ts :: [(a, b)]
    ts@((i :: a
    i, t :: b
    t):trest :: [(a, b)]
    trest) as :: [(a, b)]
    as@((i' :: a
    i', a :: b
    a):arest :: [(a, b)]
    arest)
                     | a
    i a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    < a
    i'                                 = (a
    i,  b
    t)  (a, b) -> [(a, b)] -> [(a, b)]
    forall a. a -> [a] -> [a]
    : [(a, b)] -> [(a, b)] -> [(a, b)]
    merge2 [(a, b)]
    trest [(a, b)]
    as
                     | Bool
    True                                   = (a
    i', b
    a) (a, b) -> [(a, b)] -> [(a, b)]
    forall a. a -> [a] -> [a]
    : [(a, b)] -> [(a, b)] -> [(a, b)]
    merge2 [(a, b)]
    ts [(a, b)]
    arest

           genAssert :: (FilePath, Maybe CallStack, SV) -> (Int, Doc)
    genAssert (msg :: FilePath
    msg, cs :: Maybe CallStack
    cs, sv :: SV
    sv) = (SV -> Int
    getNodeId SV
    sv, Doc
    doc)
             where doc :: Doc
    doc =     FilePath -> Doc
    text "/* ASSERTION:" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    msg
                         Doc -> Doc -> Doc
    $$  Doc -> ([FilePath] -> Doc) -> Maybe [FilePath] -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    empty ([Doc] -> Doc
    vcat ([Doc] -> Doc) -> ([FilePath] -> [Doc]) -> [FilePath] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (FilePath -> Doc) -> [FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Doc
    text) (Maybe [(FilePath, SrcLoc)] -> Maybe [FilePath]
    locInfo (CallStack -> [(FilePath, SrcLoc)]
    getCallStack (CallStack -> [(FilePath, SrcLoc)])
    -> Maybe CallStack -> Maybe [(FilePath, SrcLoc)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Maybe CallStack
    cs))
                         Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text " */"
                         Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "if" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens (CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts SV
    sv)
                         Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "{"
                         Doc -> Doc -> Doc
    $+$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat [Doc
    errOut, FilePath -> Doc
    text "exit(-1);"])
                         Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "}"
                         Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text ""
                   errOut :: Doc
    errOut = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "fprintf(stderr, \"%s:%d:ASSERTION FAILED: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    msg FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\\n\", __FILE__, __LINE__);"
                   locInfo :: Maybe [(FilePath, SrcLoc)] -> Maybe [FilePath]
    locInfo (Just ps :: [(FilePath, SrcLoc)]
    ps) = let loc :: (FilePath, SrcLoc) -> FilePath
    loc (f :: FilePath
    f, sl :: SrcLoc
    sl) = [FilePath] -> FilePath
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [SrcLoc -> FilePath
    srcLocFile SrcLoc
    sl, ":", Int -> FilePath
    forall a. Show a => a -> FilePath
    show (SrcLoc -> Int
    srcLocStartLine SrcLoc
    sl), ":", Int -> FilePath
    forall a. Show a => a -> FilePath
    show (SrcLoc -> Int
    srcLocStartCol SrcLoc
    sl), ":", FilePath
    f ]
                                       in case ((FilePath, SrcLoc) -> FilePath)
    -> [(FilePath, SrcLoc)] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, SrcLoc) -> FilePath
    loc [(FilePath, SrcLoc)]
    ps of
                                             []     -> Maybe [FilePath]
    forall a. Maybe a
    Nothing
                                             (f :: FilePath
    f:rs :: [FilePath]
    rs) -> [FilePath] -> Maybe [FilePath]
    forall a. a -> Maybe a
    Just ([FilePath] -> Maybe [FilePath]) -> [FilePath] -> Maybe [FilePath]
    forall a b. (a -> b) -> a -> b
    $ (" * SOURCE   : " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    f) FilePath -> [FilePath] -> [FilePath]
    forall a. a -> [a] -> [a]
    : (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (" *            " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++)  [FilePath]
    rs
                   locInfo _         = Maybe [FilePath]
    forall a. Maybe a
    Nothing

    handlePB :: PBOp -> [Doc] -> Doc
    handlePB :: PBOp -> [Doc] -> Doc
    handlePB o :: PBOp
    o args :: [Doc]
    args = case PBOp
    o of
                        PB_AtMost  k :: Int
    k -> [Int] -> Doc
    addIf (Int -> [Int]
    forall a. a -> [a]
    repeat 1) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "<=" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    k
                        PB_AtLeast k :: Int
    k -> [Int] -> Doc
    addIf (Int -> [Int]
    forall a. a -> [a]
    repeat 1) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ">=" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    k
                        PB_Exactly k :: Int
    k -> [Int] -> Doc
    addIf (Int -> [Int]
    forall a. a -> [a]
    repeat 1) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "==" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    k
                        PB_Le cs :: [Int]
    cs   k :: Int
    k -> [Int] -> Doc
    addIf [Int]
    cs         Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "<=" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    k
                        PB_Ge cs :: [Int]
    cs   k :: Int
    k -> [Int] -> Doc
    addIf [Int]
    cs         Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ">=" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    k
                        PB_Eq cs :: [Int]
    cs   k :: Int
    k -> [Int] -> Doc
    addIf [Int]
    cs         Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "==" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    k

      where addIf :: [Int] -> Doc
            addIf :: [Int] -> Doc
    addIf cs :: [Int]
    cs = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    intersperse (FilePath -> Doc
    text "+") [Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "?" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    c Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Int -> Doc
    int 0) | (a :: Doc
    a, c :: Int
    c) <- [Doc] -> [Int] -> [(Doc, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Doc]
    args [Int]
    cs]

    handleIEEE :: FPOp -> [(SV, CV)] -> [(SV, Doc)] -> Doc -> Doc
    handleIEEE :: FPOp -> [(SV, CV)] -> [(SV, Doc)] -> Doc -> Doc
    handleIEEE w :: FPOp
    w consts :: [(SV, CV)]
    consts as :: [(SV, Doc)]
    as var :: Doc
    var = FPOp -> Doc
    cvt FPOp
    w
      where same :: b -> (b, b)
    same f :: b
    f                   = (b
    f, b
    f)
            named :: t -> t -> (t -> b) -> (b, b)
    named fnm :: t
    fnm dnm :: t
    dnm f :: t -> b
    f          = (t -> b
    f t
    fnm, t -> b
    f t
    dnm)

            cvt :: FPOp -> Doc
    cvt (FP_Cast from :: Kind
    from to :: Kind
    to m :: SV
    m)     = case Maybe CV -> Maybe (Either FilePath FilePath)
    checkRM (SV
    m SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts) of
                                            Nothing          -> ([Doc] -> Doc) -> Doc
    forall t. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ \[a :: Doc
    a] -> Doc -> Doc
    parens (FilePath -> Doc
    text (Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    to)) Doc -> Doc -> Doc
    <+> Doc -> Doc
    rnd Doc
    a
                                            Just (Left  msg :: FilePath
    msg) -> FilePath -> Doc
    forall a. FilePath -> a
    die FilePath
    msg
                                            Just (Right msg :: FilePath
    msg) -> FilePath -> Doc
    forall a. FilePath -> a
    tbd FilePath
    msg
                                          where -- if we're converting from float to some integral like; first use rint/rintf to do the internal conversion and then cast.
                                                rnd :: Doc -> Doc
    rnd a :: Doc
    a
                                                 | (Kind -> Bool
    forall a. HasKind a => a -> Bool
    isFloat Kind
    from Bool -> Bool -> Bool
    || Kind -> Bool
    forall a. HasKind a => a -> Bool
    isDouble Kind
    from) Bool -> Bool -> Bool
    && (Kind -> Bool
    forall a. HasKind a => a -> Bool
    isBounded Kind
    to Bool -> Bool -> Bool
    || Kind -> Bool
    forall a. HasKind a => a -> Bool
    isUnbounded Kind
    to)
                                                 = let f :: FilePath
    f = if Kind -> Bool
    forall a. HasKind a => a -> Bool
    isFloat Kind
    from then "rintf" else "rint"
                                                   in FilePath -> Doc
    text FilePath
    f Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                                 | Bool
    True
                                                 = Doc
    a

            cvt (FP_Reinterpret f :: Kind
    f t :: Kind
    t) = case (Kind
    f, Kind
    t) of
                                         (KBounded False 32, KFloat)  -> ([Doc] -> Doc) -> Doc
    forall t. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [Doc] -> Doc
    cpy "sizeof(SFloat)"
                                         (KBounded False 64, KDouble) -> ([Doc] -> Doc) -> Doc
    forall t. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [Doc] -> Doc
    cpy "sizeof(SDouble)"
                                         (KFloat,  KBounded False 32) -> ([Doc] -> Doc) -> Doc
    forall t. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [Doc] -> Doc
    cpy "sizeof(SWord32)"
                                         (KDouble, KBounded False 64) -> ([Doc] -> Doc) -> Doc
    forall t. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [Doc] -> Doc
    cpy "sizeof(SWord64)"
                                         _                            -> FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Reinterpretation from : " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    f FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " to " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    t
                                        where cpy :: FilePath -> [Doc] -> Doc
    cpy sz :: FilePath
    sz = \[a :: Doc
    a] -> let alhs :: Doc
    alhs = FilePath -> Doc
    text "&" Doc -> Doc -> Doc
    P.<> Doc
    var
                                                                   arhs :: Doc
    arhs = FilePath -> Doc
    text "&" Doc -> Doc -> Doc
    P.<> Doc
    a
                                                               in FilePath -> Doc
    text "memcpy" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    alhs, Doc
    arhs, FilePath -> Doc
    text FilePath
    sz]))
            cvt FP_Abs               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "fabsf" "fabs" ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm _ [a :: Doc
    a] -> FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_Neg               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "-" Doc -> Doc -> Doc
    P.<> Doc
    a
            cvt FP_Add               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a, b :: Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "+" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FP_Sub               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a, b :: Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "-" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FP_Mul               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a, b :: Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FP_Div               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a, b :: Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "/" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FP_FMA               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "fmaf"  "fma"  ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm _ [a :: Doc
    a, b :: Doc
    b, c :: Doc
    c] -> FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b, Doc
    c]))
            cvt FP_Sqrt              = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "sqrtf" "sqrt" ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm _ [a :: Doc
    a]       -> FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_Rem               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "fmodf" "fmod" ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm _ [a :: Doc
    a, b :: Doc
    b]    -> FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b]))
            cvt FP_RoundToIntegral   = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "rintf" "rint" ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm _ [a :: Doc
    a]       -> FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_Min               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "fminf" "fmin" ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm k :: Kind
    k [a :: Doc
    a, b :: Doc
    b]    -> Kind -> Doc -> Doc -> Doc -> Doc
    wrapMinMax Kind
    k Doc
    a Doc
    b (FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b])))
            cvt FP_Max               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath
    -> FilePath
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall t b. t -> t -> (t -> b) -> (b, b)
    named "fmaxf" "fmax" ((FilePath -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (FilePath -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \nm :: FilePath
    nm k :: Kind
    k [a :: Doc
    a, b :: Doc
    b]    -> Kind -> Doc -> Doc -> Doc -> Doc
    wrapMinMax Kind
    k Doc
    a Doc
    b (FilePath -> Doc
    text FilePath
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b])))
            cvt FP_ObjEqual          = let mkIte :: Doc -> Doc -> Doc -> Doc
    mkIte   x :: Doc
    x y :: Doc
    y z :: Doc
    z = Doc
    x Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "?" Doc -> Doc -> Doc
    <+> Doc
    y Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Doc
    z
                                           chkNaN :: Doc -> Doc
    chkNaN  x :: Doc
    x     = FilePath -> Doc
    text "isnan"   Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    x
                                           signbit :: Doc -> Doc
    signbit x :: Doc
    x     = FilePath -> Doc
    text "signbit" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    x
                                           eq :: Doc -> Doc -> Doc
    eq      x :: Doc
    x y :: Doc
    y   = Doc -> Doc
    parens (Doc
    x Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "==" Doc -> Doc -> Doc
    <+> Doc
    y)
                                           eqZero :: Doc -> Doc
    eqZero  x :: Doc
    x     = Doc -> Doc -> Doc
    eq Doc
    x (FilePath -> Doc
    text "0")
                                           negZero :: Doc -> Doc
    negZero x :: Doc
    x     = Doc -> Doc
    parens (Doc -> Doc
    signbit Doc
    x Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&" Doc -> Doc -> Doc
    <+> Doc -> Doc
    eqZero Doc
    x)
                                       in (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a, b :: Doc
    b] -> Doc -> Doc -> Doc -> Doc
    mkIte (Doc -> Doc
    chkNaN Doc
    a) (Doc -> Doc
    chkNaN Doc
    b) (Doc -> Doc -> Doc -> Doc
    mkIte (Doc -> Doc
    negZero Doc
    a) (Doc -> Doc
    negZero Doc
    b) (Doc -> Doc -> Doc -> Doc
    mkIte (Doc -> Doc
    negZero Doc
    b) (Doc -> Doc
    negZero Doc
    a) (Doc -> Doc -> Doc
    eq Doc
    a Doc
    b)))
            cvt FP_IsNormal          = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "isnormal" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_IsSubnormal       = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "FP_SUBNORMAL == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_IsZero            = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "FP_ZERO == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_IsInfinite        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "isinf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_IsNaN             = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "isnan" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_IsNegative        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "!isnan" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "signbit"  Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FP_IsPositive        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall b. b -> (b, b)
    same ((Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \_ [a :: Doc
    a] -> FilePath -> Doc
    text "!isnan" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "!signbit" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a

            -- grab the rounding-mode, if present, and make sure it's RoundNearestTiesToEven. Otherwise skip.
            fpArgs :: [(SV, Doc)]
    fpArgs = case [(SV, Doc)]
    as of
                       []            -> []
                       ((m :: SV
    m, _):args :: [(SV, Doc)]
    args) -> case SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    m of
                                          KUninterpreted "RoundingMode" _ -> case Maybe CV -> Maybe (Either FilePath FilePath)
    checkRM (SV
    m SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts) of
                                                                               Nothing          -> [(SV, Doc)]
    args
                                                                               Just (Left  msg :: FilePath
    msg) -> FilePath -> [(SV, Doc)]
    forall a. FilePath -> a
    die FilePath
    msg
                                                                               Just (Right msg :: FilePath
    msg) -> FilePath -> [(SV, Doc)]
    forall a. FilePath -> a
    tbd FilePath
    msg
                                          _                               -> [(SV, Doc)]
    as

            -- Check that the RM is RoundNearestTiesToEven.
            -- If we start supporting other rounding-modes, this would be the point where we'd insert the rounding-mode set/reset code
            -- instead of merely returning OK or not
            checkRM :: Maybe CV -> Maybe (Either FilePath FilePath)
    checkRM (Just cv :: CV
    cv@(CV (KUninterpreted "RoundingMode" _) v :: CVal
    v)) =
                  case CVal
    v of
                    CUserSort (_, "RoundNearestTiesToEven") -> Maybe (Either FilePath FilePath)
    forall a. Maybe a
    Nothing
                    CUserSort (_, s :: FilePath
    s)                        -> Either FilePath FilePath -> Maybe (Either FilePath FilePath)
    forall a. a -> Maybe a
    Just (FilePath -> Either FilePath FilePath
    forall a b. b -> Either a b
    Right (FilePath -> Either FilePath FilePath)
    -> FilePath -> Either FilePath FilePath
    forall a b. (a -> b) -> a -> b
    $ "handleIEEE: Unsupported rounding-mode: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    s FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " for: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> FilePath
    forall a. Show a => a -> FilePath
    show FPOp
    w)
                    _                                       -> Either FilePath FilePath -> Maybe (Either FilePath FilePath)
    forall a. a -> Maybe a
    Just (FilePath -> Either FilePath FilePath
    forall a b. a -> Either a b
    Left  (FilePath -> Either FilePath FilePath)
    -> FilePath -> Either FilePath FilePath
    forall a b. (a -> b) -> a -> b
    $ "handleIEEE: Unexpected value for rounding-mode: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ CV -> FilePath
    forall a. Show a => a -> FilePath
    show CV
    cv FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " for: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> FilePath
    forall a. Show a => a -> FilePath
    show FPOp
    w)
            checkRM (Just cv :: CV
    cv) = Either FilePath FilePath -> Maybe (Either FilePath FilePath)
    forall a. a -> Maybe a
    Just (FilePath -> Either FilePath FilePath
    forall a b. a -> Either a b
    Left  (FilePath -> Either FilePath FilePath)
    -> FilePath -> Either FilePath FilePath
    forall a b. (a -> b) -> a -> b
    $ "handleIEEE: Expected rounding-mode, but got: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ CV -> FilePath
    forall a. Show a => a -> FilePath
    show CV
    cv FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " for: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> FilePath
    forall a. Show a => a -> FilePath
    show FPOp
    w)
            checkRM Nothing   = Either FilePath FilePath -> Maybe (Either FilePath FilePath)
    forall a. a -> Maybe a
    Just (FilePath -> Either FilePath FilePath
    forall a b. b -> Either a b
    Right (FilePath -> Either FilePath FilePath)
    -> FilePath -> Either FilePath FilePath
    forall a b. (a -> b) -> a -> b
    $ "handleIEEE: Non-constant rounding-mode for: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> FilePath
    forall a. Show a => a -> FilePath
    show FPOp
    w)

            pickOp :: (Kind -> [b] -> p, Kind -> [b] -> p) -> [(a, b)] -> p
    pickOp _          []             = FilePath -> p
    forall a. FilePath -> a
    die (FilePath -> p) -> FilePath -> p
    forall a b. (a -> b) -> a -> b
    $ "Cannot determine float/double kind for op: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> FilePath
    forall a. Show a => a -> FilePath
    show FPOp
    w
            pickOp (fOp :: Kind -> [b] -> p
    fOp, dOp :: Kind -> [b] -> p
    dOp) args :: [(a, b)]
    args@((a :: a
    a,_):_) = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    a of
                                                 KFloat  -> Kind -> [b] -> p
    fOp Kind
    KFloat  (((a, b) -> b) -> [(a, b)] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map (a, b) -> b
    forall a b. (a, b) -> b
    snd [(a, b)]
    args)
                                                 KDouble -> Kind -> [b] -> p
    dOp Kind
    KDouble (((a, b) -> b) -> [(a, b)] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map (a, b) -> b
    forall a b. (a, b) -> b
    snd [(a, b)]
    args)
                                                 k :: Kind
    k       -> FilePath -> p
    forall a. FilePath -> a
    die (FilePath -> p) -> FilePath -> p
    forall a b. (a -> b) -> a -> b
    $ "handleIEEE: Expected double/float args, but got: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    k FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " for: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> FilePath
    forall a. Show a => a -> FilePath
    show FPOp
    w

            dispatch :: (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
    dispatch (fOp :: Kind -> [Doc] -> p
    fOp, dOp :: Kind -> [Doc] -> p
    dOp) = (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> [(SV, Doc)] -> p
    forall a b p.
    HasKind a =>
    (Kind -> [b] -> p, Kind -> [b] -> p) -> [(a, b)] -> p
    pickOp (Kind -> [Doc] -> p
    fOp, Kind -> [Doc] -> p
    dOp) [(SV, Doc)]
    fpArgs
            cast :: ([Doc] -> t) -> t
    cast f :: [Doc] -> t
    f              = [Doc] -> t
    f (((SV, Doc) -> Doc) -> [(SV, Doc)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, Doc) -> Doc
    forall a b. (a, b) -> b
    snd [(SV, Doc)]
    fpArgs)

            -- In SMT-Lib, fpMin/fpMax is underspecified when given +0/-0 as the two arguments. (In any order.)
            -- In C, the second argument is returned. (I think, might depend on the architecture, optimizations etc.).
            -- We'll translate it so that we deterministically return +0.
            -- There's really no good choice here.
            wrapMinMax :: Kind -> Doc -> Doc -> Doc -> Doc
    wrapMinMax k :: Kind
    k a :: Doc
    a b :: Doc
    b s :: Doc
    s = Doc -> Doc
    parens Doc
    cond Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "?" Doc -> Doc -> Doc
    <+> Doc
    zero Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Doc
    s
              where zero :: Doc
    zero = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ if Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KFloat then Float -> FilePath
    showCFloat 0 else Double -> FilePath
    showCDouble 0
                    cond :: Doc
    cond =                   Doc -> Doc
    parens (FilePath -> Doc
    text "FP_ZERO == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a)                                      -- a is zero
                           Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (FilePath -> Doc
    text "FP_ZERO == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    b)                                      -- b is zero
                           Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (FilePath -> Doc
    text "signbit" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "!=" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "signbit" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    b)       -- a and b differ in sign

    ppExpr :: CgConfig -> [(SV, CV)] -> SBVExpr -> Doc -> (Doc, Doc) -> Doc
    ppExpr :: CgConfig -> [(SV, CV)] -> SBVExpr -> Doc -> (Doc, Doc) -> Doc
    ppExpr cfg :: CgConfig
    cfg consts :: [(SV, CV)]
    consts (SBVApp op :: Op
    op opArgs :: [SV]
    opArgs) lhs :: Doc
    lhs (typ :: Doc
    typ, var :: Doc
    var)
      | Op -> Bool
    doNotAssign Op
    op
      = Doc
    typ Doc -> Doc -> Doc
    <+> Doc
    var Doc -> Doc -> Doc
    P.<> Doc
    semi Doc -> Doc -> Doc
    <+> Doc
    rhs
      | Bool
    True
      = Doc
    lhs Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "=" Doc -> Doc -> Doc
    <+> Doc
    rhs
      where doNotAssign :: Op -> Bool
    doNotAssign (IEEEFP FP_Reinterpret{}) = Bool
    True   -- generates a memcpy instead; no simple assignment
            doNotAssign _                         = Bool
    False  -- generates simple assignment

            rhs :: Doc
    rhs = Op -> [Doc] -> Doc
    p Op
    op ((SV -> Doc) -> [SV] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts) [SV]
    opArgs)

            rtc :: Bool
    rtc = CgConfig -> Bool
    cgRTC CgConfig
    cfg

            cBinOps :: [(Op, FilePath)]
    cBinOps = [ (Op
    Plus, "+"),  (Op
    Times, "*"), (Op
    Minus, "-")
                      , (Op
    Equal, "=="), (Op
    NotEqual, "!="), (Op
    LessThan, "<"), (Op
    GreaterThan, ">"), (Op
    LessEq, "<="), (Op
    GreaterEq, ">=")
                      , (Op
    And, "&"), (Op
    Or, "|"), (Op
    XOr, "^")
                      ]

            -- see if we can find a constant shift; makes the output way more readable
            getShiftAmnt :: Doc -> [SV] -> Doc
    getShiftAmnt def :: Doc
    def [_, sv :: SV
    sv] = case SV
    sv SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts of
                                        Just (CV _  (CInteger i :: Integer
    i)) -> Integer -> Doc
    integer Integer
    i
                                        _                         -> Doc
    def
            getShiftAmnt def :: Doc
    def _       = Doc
    def

            p :: Op -> [Doc] -> Doc
            p :: Op -> [Doc] -> Doc
    p (ArrRead _)       _  = FilePath -> Doc
    forall a. FilePath -> a
    tbd "User specified arrays (ArrRead)"
            p (ArrEq _ _)       _  = FilePath -> Doc
    forall a. FilePath -> a
    tbd "User specified arrays (ArrEq)"
            p (Label s :: FilePath
    s)        [a :: Doc
    a] = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "/*" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    s Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "*/"
            p (IEEEFP w :: FPOp
    w)         as :: [Doc]
    as = FPOp -> [(SV, CV)] -> [(SV, Doc)] -> Doc -> Doc
    handleIEEE FPOp
    w  [(SV, CV)]
    consts ([SV] -> [Doc] -> [(SV, Doc)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [SV]
    opArgs [Doc]
    as) Doc
    var
            p (PseudoBoolean pb :: PBOp
    pb) as :: [Doc]
    as = PBOp -> [Doc] -> Doc
    handlePB PBOp
    pb [Doc]
    as
            p (OverflowOp o :: OvOp
    o) _      = FilePath -> Doc
    forall a. FilePath -> a
    tbd (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Overflow operations" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ OvOp -> FilePath
    forall a. Show a => a -> FilePath
    show OvOp
    o
            p (KindCast _ to :: Kind
    to)   [a :: Doc
    a] = Doc -> Doc
    parens (FilePath -> Doc
    text (Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    to)) Doc -> Doc -> Doc
    <+> Doc
    a
            p (Uninterpreted s :: FilePath
    s) [] = FilePath -> Doc
    text "/* Uninterpreted constant */" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    s
            p (Uninterpreted s :: FilePath
    s) as :: [Doc]
    as = FilePath -> Doc
    text "/* Uninterpreted function */" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    s Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc]
    as))
            p (Extract i :: Int
    i j :: Int
    j) [a :: Doc
    a]    = Int -> Int -> SV -> Doc -> Doc
    forall a. (HasKind a, Show a) => Int -> Int -> a -> Doc -> Doc
    extract Int
    i Int
    j ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs) Doc
    a
            p Join [a :: Doc
    a, b :: Doc
    b]          = (SV, SV, Doc, Doc) -> Doc
    forall b b.
    (HasKind b, HasKind b, Show b, Show b) =>
    (b, b, Doc, Doc) -> Doc
    join (let (s1 :: SV
    s1 : s2 :: SV
    s2 : _) = [SV]
    opArgs in (SV
    s1, SV
    s2, Doc
    a, Doc
    b))
            p (Rol i :: Int
    i) [a :: Doc
    a]          = Bool -> Int -> Doc -> SV -> Doc
    forall c. (HasKind c, Show c) => Bool -> Int -> Doc -> c -> Doc
    rotate Bool
    True  Int
    i Doc
    a ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs)
            p (Ror i :: Int
    i) [a :: Doc
    a]          = Bool -> Int -> Doc -> SV -> Doc
    forall c. (HasKind c, Show c) => Bool -> Int -> Doc -> c -> Doc
    rotate Bool
    False Int
    i Doc
    a ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs)
            p Shl     [a :: Doc
    a, i :: Doc
    i]       = Bool -> Doc -> Doc -> Doc
    shift  Bool
    True  (Doc -> [SV] -> Doc
    getShiftAmnt Doc
    i [SV]
    opArgs) Doc
    a -- The order of i/a being reversed here is
            p Shr     [a :: Doc
    a, i :: Doc
    i]       = Bool -> Doc -> Doc -> Doc
    shift  Bool
    False (Doc -> [SV] -> Doc
    getShiftAmnt Doc
    i [SV]
    opArgs) Doc
    a -- intentional and historical (from the days when Shl/Shr had a constant parameter.)
            p Not [a :: Doc
    a]              = case SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs) of
                                       -- be careful about booleans, bitwise complement is not correct for them!
                                       KBool -> FilePath -> Doc
    text "!" Doc -> Doc -> Doc
    P.<> Doc
    a
                                       _     -> FilePath -> Doc
    text "~" Doc -> Doc -> Doc
    P.<> Doc
    a
            p Ite [a :: Doc
    a, b :: Doc
    b, c :: Doc
    c] = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "?" Doc -> Doc -> Doc
    <+> Doc
    b Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Doc
    c
            p (LkUp (t :: Int
    t, k :: Kind
    k, _, len :: Int
    len) ind :: SV
    ind def :: SV
    def) []
              | Bool -> Bool
    not Bool
    rtc                    = Doc
    lkUp -- ignore run-time-checks per user request
              | Bool
    needsCheckL Bool -> Bool -> Bool
    && Bool
    needsCheckR = Doc -> Doc
    cndLkUp Doc
    checkBoth
              | Bool
    needsCheckL                = Doc -> Doc
    cndLkUp Doc
    checkLeft
              | Bool
    needsCheckR                = Doc -> Doc
    cndLkUp Doc
    checkRight
              | Bool
    True                       = Doc
    lkUp
              where [index :: Doc
    index, defVal :: Doc
    defVal] = (SV -> Doc) -> [SV] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts) [SV
    ind, SV
    def]

                    lkUp :: Doc
    lkUp = FilePath -> Doc
    text "table" Doc -> Doc -> Doc
    P.<> Int -> Doc
    int Int
    t Doc -> Doc -> Doc
    P.<> Doc -> Doc
    brackets (CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts SV
    ind)
                    cndLkUp :: Doc -> Doc
    cndLkUp cnd :: Doc
    cnd = Doc
    cnd Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "?" Doc -> Doc -> Doc
    <+> Doc
    defVal Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Doc
    lkUp

                    checkLeft :: Doc
    checkLeft  = Doc
    index Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "< 0"
                    checkRight :: Doc
    checkRight = Doc
    index Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ">=" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    len
                    checkBoth :: Doc
    checkBoth  = Doc -> Doc
    parens (Doc
    checkLeft Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "||" Doc -> Doc -> Doc
    <+> Doc
    checkRight)

                    canOverflow :: Bool -> b -> Bool
    canOverflow True  sz :: b
    sz = (2::Integer)Integer -> b -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(b
    szb -> b -> b
    forall a. Num a => a -> a -> a
    -1)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    len
                    canOverflow False sz :: b
    sz = (2::Integer)Integer -> b -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^b
    sz    Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    len

                    (needsCheckL :: Bool
    needsCheckL, needsCheckR :: Bool
    needsCheckR) = case Kind
    k of
                                                   KBool              -> (Bool
    False, Bool -> Int -> Bool
    forall b. Integral b => Bool -> b -> Bool
    canOverflow Bool
    False (1::Int))
                                                   KBounded sg :: Bool
    sg sz :: Int
    sz     -> (Bool
    sg, Bool -> Int -> Bool
    forall b. Integral b => Bool -> b -> Bool
    canOverflow Bool
    sg Int
    sz)
                                                   KReal              -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die "array index with real value"
                                                   KFloat             -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die "array index with float value"
                                                   KDouble            -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die "array index with double value"
                                                   KString            -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die "array index with string value"
                                                   KChar              -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die "array index with character value"
                                                   KUnbounded         -> case CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg of
                                                                           Nothing -> (Bool
    True, Bool
    True) -- won't matter, it'll be rejected later
                                                                           Just i :: Int
    i  -> (Bool
    True, Bool -> Int -> Bool
    forall b. Integral b => Bool -> b -> Bool
    canOverflow Bool
    True Int
    i)
                                                   KList     s :: Kind
    s        -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "List sort " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    s
                                                   KSet      s :: Kind
    s        -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "Set sort " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    s
                                                   KTuple    s :: [Kind]
    s        -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "Tuple sort " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> FilePath
    forall a. Show a => a -> FilePath
    show [Kind]
    s
                                                   KMaybe    ek :: Kind
    ek       -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "Maybe sort " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Kind -> FilePath
    forall a. Show a => a -> FilePath
    show Kind
    ek
                                                   KEither   k1 :: Kind
    k1 k2 :: Kind
    k2    -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "Either sort " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> FilePath
    forall a. Show a => a -> FilePath
    show (Kind
    k1, Kind
    k2)
                                                   KUninterpreted s :: FilePath
    s _ -> FilePath -> (Bool, Bool)
    forall a. FilePath -> a
    die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "Uninterpreted sort: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    s

            -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x
            -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior.
            -- Brief googling suggests C99 does indeed truncate toward 0, but other C compilers might differ.
            p Quot [a :: Doc
    a, b :: Doc
    b] = let k :: Kind
    k = SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs)
                                z :: Doc
    z = CgConfig -> CV -> Doc
    mkConst CgConfig
    cfg (CV -> Doc) -> CV -> Doc
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k (0::Integer)
                            in Kind -> FilePath -> Doc -> Doc -> Doc -> Doc
    protectDiv0 Kind
    k "/" Doc
    z Doc
    a Doc
    b
            p Rem  [a :: Doc
    a, b :: Doc
    b] = Kind -> FilePath -> Doc -> Doc -> Doc -> Doc
    protectDiv0 (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs)) "%" Doc
    a Doc
    a Doc
    b
            p UNeg [a :: Doc
    a]    = Doc -> Doc
    parens (FilePath -> Doc
    text "-" Doc -> Doc -> Doc
    <+> Doc
    a)
            p Abs  [a :: Doc
    a]    = let f :: Kind -> Doc
    f KFloat             = FilePath -> Doc
    text "fabsf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f KDouble            = FilePath -> Doc
    text "fabs"  Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f (KBounded False _) = FilePath -> Doc
    text "/* unsigned, skipping call to abs */" Doc -> Doc -> Doc
    <+> Doc
    a
                                f (KBounded True 32) = FilePath -> Doc
    text "labs"  Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f (KBounded True 64) = FilePath -> Doc
    text "llabs" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f KUnbounded         = case CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg of
                                                         Nothing -> Kind -> Doc
    f (Kind -> Doc) -> Kind -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Kind
    KBounded Bool
    True 32 -- won't matter, it'll be rejected later
                                                         Just i :: Int
    i  -> Kind -> Doc
    f (Kind -> Doc) -> Kind -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Kind
    KBounded Bool
    True Int
    i
                                f KReal              = case CgConfig -> Maybe CgSRealType
    cgReal CgConfig
    cfg of
                                                         Nothing           -> Kind -> Doc
    f Kind
    KDouble -- won't matter, it'll be rejected later
                                                         Just CgFloat      -> Kind -> Doc
    f Kind
    KFloat
                                                         Just CgDouble     -> Kind -> Doc
    f Kind
    KDouble
                                                         Just CgLongDouble -> FilePath -> Doc
    text "fabsl" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f _                  = FilePath -> Doc
    text "abs" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                            in Kind -> Doc
    f (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs))
            -- for And/Or, translate to boolean versions if on boolean kind
            p And [a :: Doc
    a, b :: Doc
    b] | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs) Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&" Doc -> Doc -> Doc
    <+> Doc
    b
            p Or  [a :: Doc
    a, b :: Doc
    b] | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    opArgs) Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "||" Doc -> Doc -> Doc
    <+> Doc
    b
            p o :: Op
    o [a :: Doc
    a, b :: Doc
    b]
              | Just co :: FilePath
    co <- Op -> [(Op, FilePath)] -> Maybe FilePath
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    o [(Op, FilePath)]
    cBinOps
              = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    co Doc -> Doc -> Doc
    <+> Doc
    b
            p NotEqual xs :: [Doc]
    xs = [Doc] -> Doc
    mkDistinct [Doc]
    xs
            p o :: Op
    o args :: [Doc]
    args = FilePath -> Doc
    forall a. FilePath -> a
    die (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Received operator " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Op -> FilePath
    forall a. Show a => a -> FilePath
    show Op
    o FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " applied to " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [Doc] -> FilePath
    forall a. Show a => a -> FilePath
    show [Doc]
    args

            -- generate a pairwise inequality check
            mkDistinct :: [Doc] -> Doc
    mkDistinct args :: [Doc]
    args = [Doc] -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> [Doc]
    andAll ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> [Doc]
    walk [Doc]
    args
              where walk :: [Doc] -> [Doc]
    walk []     = []
                    walk (e :: Doc
    e:es :: [Doc]
    es) = (Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc -> Doc
    pair Doc
    e) [Doc]
    es [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc] -> [Doc]
    walk [Doc]
    es

                    pair :: Doc -> Doc -> Doc
    pair e1 :: Doc
    e1 e2 :: Doc
    e2  = Doc -> Doc
    parens (Doc
    e1 Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "!=" Doc -> Doc -> Doc
    <+> Doc
    e2)

                    -- like punctuate, but more spacing
                    andAll :: [Doc] -> [Doc]
    andAll []     = []
                    andAll (d :: Doc
    d:ds :: [Doc]
    ds) = Doc -> [Doc] -> [Doc]
    go Doc
    d [Doc]
    ds
                         where go :: Doc -> [Doc] -> [Doc]
    go d' :: Doc
    d' [] = [Doc
    d']
                               go d' :: Doc
    d' (e :: Doc
    e:es :: [Doc]
    es) = (Doc
    d' Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "&&") Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : Doc -> [Doc] -> [Doc]
    go Doc
    e [Doc]
    es

            -- Div0 needs to protect, but only when the arguments are not float/double. (Div by 0 for those are well defined to be Inf/NaN etc.)
            protectDiv0 :: Kind -> FilePath -> Doc -> Doc -> Doc -> Doc
    protectDiv0 k :: Kind
    k divOp :: FilePath
    divOp def :: Doc
    def a :: Doc
    a b :: Doc
    b = case Kind
    k of
                                            KFloat  -> Doc
    res
                                            KDouble -> Doc
    res
                                            _       -> Doc
    wrap
               where res :: Doc
    res  = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    divOp Doc -> Doc -> Doc
    <+> Doc
    b
                     wrap :: Doc
    wrap = Doc -> Doc
    parens (Doc
    b Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "== 0") Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "?" Doc -> Doc -> Doc
    <+> Doc
    def Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ":" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens Doc
    res

            shift :: Bool -> Doc -> Doc -> Doc
    shift toLeft :: Bool
    toLeft i :: Doc
    i a :: Doc
    a = Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    cop Doc -> Doc -> Doc
    <+> Doc
    i
              where cop :: FilePath
    cop | Bool
    toLeft = "<<"
                        | Bool
    True   = ">>"

            rotate :: Bool -> Int -> Doc -> c -> Doc
    rotate toLeft :: Bool
    toLeft i :: Int
    i a :: Doc
    a s :: c
    s
              | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0   = Bool -> Int -> Doc -> c -> Doc
    rotate (Bool -> Bool
    not Bool
    toLeft) (-Int
    i) Doc
    a c
    s
              | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0  = Doc
    a
              | Bool
    True    = case c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf c
    s of
                            KBounded True _             -> FilePath -> Doc
    forall a. FilePath -> a
    tbd (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Rotation of signed quantities: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (Bool, Int, c) -> FilePath
    forall a. Show a => a -> FilePath
    show (Bool
    toLeft, Int
    i, c
    s)
                            KBounded False sz :: Int
    sz | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    sz -> Bool -> Int -> Doc -> c -> Doc
    rotate Bool
    toLeft (Int
    i Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    sz) Doc
    a c
    s
                            KBounded False sz :: Int
    sz           ->     Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    cop  Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    i)
                                                          Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "|"
                                                          Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    cop' Doc -> Doc -> Doc
    <+> Int -> Doc
    int (Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i))
                            KUnbounded                  -> Bool -> Doc -> Doc -> Doc
    shift Bool
    toLeft (Int -> Doc
    int Int
    i) Doc
    a -- For SInteger, rotate is the same as shift in Haskell
                            _                           -> FilePath -> Doc
    forall a. FilePath -> a
    tbd (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "Rotation for unbounded quantity: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (Bool, Int, c) -> FilePath
    forall a. Show a => a -> FilePath
    show (Bool
    toLeft, Int
    i, c
    s)
              where (cop :: FilePath
    cop, cop' :: FilePath
    cop') | Bool
    toLeft = ("<<", ">>")
                                | Bool
    True   = (">>", "<<")

            -- TBD: below we only support the values for extract that are "easy" to implement. These should cover
            -- almost all instances actually generated by SBV, however.
            extract :: Int -> Int -> a -> Doc -> Doc
    extract hi :: Int
    hi lo :: Int
    lo i :: a
    i a :: Doc
    a  -- Isolate the bit-extraction case
              | Int
    hi Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    lo, KBounded _ sz :: Int
    sz <- a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    i, Int
    hi Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    sz, Int
    hi Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0
              = if Int
    hi Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
                then FilePath -> Doc
    text "(SBool)" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "& 1")
                else FilePath -> Doc
    text "(SBool)" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ">>" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    hi) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "& 1")
            extract hi :: Int
    hi lo :: Int
    lo i :: a
    i a :: Doc
    a
              | Int
    srcSize Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [64, 32, 16]
              = FilePath -> Doc
    forall a. FilePath -> a
    bad "Unsupported source size"
              | (Int
    hi Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1) Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` 8 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 0 Bool -> Bool -> Bool
    || Int
    lo Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` 8 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 0
              = FilePath -> Doc
    forall a. FilePath -> a
    bad "Unsupported non-byte-aligned extraction"
              | Int
    tgtSize Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 8 Bool -> Bool -> Bool
    || Int
    tgtSize Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` 8 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 0
              = FilePath -> Doc
    forall a. FilePath -> a
    bad "Unsupported target size"
              | Bool
    True
              = FilePath -> Doc
    text FilePath
    cast Doc -> Doc -> Doc
    <+> Doc
    shifted
              where bad :: FilePath -> a
    bad why :: FilePath
    why    = FilePath -> a
    forall a. FilePath -> a
    tbd (FilePath -> a) -> FilePath -> a
    forall a b. (a -> b) -> a -> b
    $ "extract with " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int, Kind, a) -> FilePath
    forall a. Show a => a -> FilePath
    show (Int
    hi, Int
    lo, Kind
    k, a
    i) FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " (Reason: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    why FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".)"

                    k :: Kind
    k          = a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    i
                    srcSize :: Int
    srcSize    = Kind -> Int
    forall a. HasKind a => a -> Int
    intSizeOf Kind
    k
                    tgtSize :: Int
    tgtSize    = Int
    hi Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    lo Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1
                    signChange :: Bool
    signChange = Int
    srcSize Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    tgtSize

                    cast :: FilePath
    cast
                      | Bool
    signChange Bool -> Bool -> Bool
    && Kind -> Bool
    forall a. HasKind a => a -> Bool
    hasSign Kind
    k = "(SWord" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    srcSize FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ")"
                      | Bool
    signChange              = "(SInt"  FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    srcSize FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ")"
                      | Bool
    True                    = "(SWord" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    tgtSize FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ")"

                    shifted :: Doc
    shifted
                      | Int
    lo Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 = Doc
    a
                      | Bool
    True    = Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ">>" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    lo)

            -- TBD: ditto here for join, just like extract above
            join :: (b, b, Doc, Doc) -> Doc
    join (i :: b
    i, j :: b
    j, a :: Doc
    a, b :: Doc
    b) = case (b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf b
    i, b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf b
    j) of
                                  (KBounded False  8, KBounded False  8) -> Doc -> Doc
    parens (Doc -> Doc
    parens (FilePath -> Doc
    text "(SWord16)" Doc -> Doc -> Doc
    <+> Doc
    a) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "<< 8")  Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "|" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (FilePath -> Doc
    text "(SWord16)" Doc -> Doc -> Doc
    <+> Doc
    b)
                                  (KBounded False 16, KBounded False 16) -> Doc -> Doc
    parens (Doc -> Doc
    parens (FilePath -> Doc
    text "(SWord32)" Doc -> Doc -> Doc
    <+> Doc
    a) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "<< 16") Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "|" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (FilePath -> Doc
    text "(SWord32)" Doc -> Doc -> Doc
    <+> Doc
    b)
                                  (KBounded False 32, KBounded False 32) -> Doc -> Doc
    parens (Doc -> Doc
    parens (FilePath -> Doc
    text "(SWord64)" Doc -> Doc -> Doc
    <+> Doc
    a) Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "<< 32") Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "|" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (FilePath -> Doc
    text "(SWord64)" Doc -> Doc -> Doc
    <+> Doc
    b)
                                  (k1 :: Kind
    k1,                k2 :: Kind
    k2)                -> FilePath -> Doc
    forall a. FilePath -> a
    tbd (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ "join with " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ((Kind, b), (Kind, b)) -> FilePath
    forall a. Show a => a -> FilePath
    show ((Kind
    k1, b
    i), (Kind
    k2, b
    j))

    -- same as doubleQuotes, except we have to make sure there are no line breaks..
    -- Otherwise breaks the generated code.. sigh
    printQuotes :: Doc -> Doc
    printQuotes :: Doc -> Doc
    printQuotes d :: Doc
    d = FilePath -> Doc
    text (FilePath -> Doc) -> FilePath -> Doc
    forall a b. (a -> b) -> a -> b
    $ '"' Char -> FilePath -> FilePath
    forall a. a -> [a] -> [a]
    : Doc -> FilePath
    ppSameLine Doc
    d FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\""

    -- Remove newlines.. Useful when generating Makefile and such
    ppSameLine :: Doc -> String
    ppSameLine :: Doc -> FilePath
    ppSameLine = FilePath -> FilePath
    trim (FilePath -> FilePath) -> (Doc -> FilePath) -> Doc -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> FilePath
    render
     where trim :: FilePath -> FilePath
    trim ""        = ""
           trim ('\n':cs :: FilePath
    cs) = ' ' Char -> FilePath -> FilePath
    forall a. a -> [a] -> [a]
    : FilePath -> FilePath
    trim ((Char -> Bool) -> FilePath -> FilePath
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace FilePath
    cs)
           trim (c :: Char
    c:cs :: FilePath
    cs)    = Char
    c   Char -> FilePath -> FilePath
    forall a. a -> [a] -> [a]
    : FilePath -> FilePath
    trim FilePath
    cs

    -- Align a bunch of docs to occupy the exact same length by padding in the left by space
    -- this is ugly and inefficient, but easy to code..
    align :: [Doc] -> [Doc]
    align :: [Doc] -> [Doc]
    align ds :: [Doc]
    ds = (FilePath -> Doc) -> [FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath -> Doc
    text (FilePath -> Doc) -> (FilePath -> FilePath) -> FilePath -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FilePath -> FilePath
    pad) [FilePath]
    ss
      where ss :: [FilePath]
    ss    = (Doc -> FilePath) -> [Doc] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> FilePath
    render [Doc]
    ds
            l :: Int
    l     = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : (FilePath -> Int) -> [FilePath] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [FilePath]
    ss)
            pad :: FilePath -> FilePath
    pad s :: FilePath
    s = Int -> Char -> FilePath
    forall a. Int -> a -> [a]
    replicate (Int
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length FilePath
    s) ' ' FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    s

    -- | Merge a bunch of bundles to generate code for a library. For the final
    -- config, we simply return the first config we receive, or the default if none.
    mergeToLib :: String -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
    mergeToLib :: FilePath -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
    mergeToLib libName :: FilePath
    libName cfgBundles :: [(CgConfig, CgPgmBundle)]
    cfgBundles
      | [(Maybe Int, Maybe CgSRealType)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Maybe Int, Maybe CgSRealType)]
    nubKinds Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 1
      = FilePath -> (CgConfig, CgPgmBundle)
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> (CgConfig, CgPgmBundle))
    -> FilePath -> (CgConfig, CgPgmBundle)
    forall a b. (a -> b) -> a -> b
    $  "Cannot merge programs with differing SInteger/SReal mappings. Received the following kinds:\n"
              FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [FilePath] -> FilePath
    unlines (((Maybe Int, Maybe CgSRealType) -> FilePath)
    -> [(Maybe Int, Maybe CgSRealType)] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe Int, Maybe CgSRealType) -> FilePath
    forall a. Show a => a -> FilePath
    show [(Maybe Int, Maybe CgSRealType)]
    nubKinds)
      | Bool
    True
      = (CgConfig
    finalCfg, (Maybe Int, Maybe CgSRealType)
    -> [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle
    CgPgmBundle (Maybe Int, Maybe CgSRealType)
    bundleKind ([(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle)
    -> [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle
    forall a b. (a -> b) -> a -> b
    $ [(FilePath, (CgPgmKind, [Doc]))]
    sources [(FilePath, (CgPgmKind, [Doc]))]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    forall a. [a] -> [a] -> [a]
    ++ (FilePath, (CgPgmKind, [Doc]))
    libHeader (FilePath, (CgPgmKind, [Doc]))
    -> [(FilePath, (CgPgmKind, [Doc]))]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    forall a. a -> [a] -> [a]
    : [(FilePath, (CgPgmKind, [Doc]))
    libDriver | Bool
    anyDriver] [(FilePath, (CgPgmKind, [Doc]))]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    forall a. [a] -> [a] -> [a]
    ++ [(FilePath, (CgPgmKind, [Doc]))
    libMake | Bool
    anyMake])
      where bundles :: [CgPgmBundle]
    bundles     = ((CgConfig, CgPgmBundle) -> CgPgmBundle)
    -> [(CgConfig, CgPgmBundle)] -> [CgPgmBundle]
    forall a b. (a -> b) -> [a] -> [b]
    map (CgConfig, CgPgmBundle) -> CgPgmBundle
    forall a b. (a, b) -> b
    snd [(CgConfig, CgPgmBundle)]
    cfgBundles
            kinds :: [(Maybe Int, Maybe CgSRealType)]
    kinds       = [(Maybe Int, Maybe CgSRealType)
    k | CgPgmBundle k :: (Maybe Int, Maybe CgSRealType)
    k _ <- [CgPgmBundle]
    bundles]
            nubKinds :: [(Maybe Int, Maybe CgSRealType)]
    nubKinds    = [(Maybe Int, Maybe CgSRealType)]
    -> [(Maybe Int, Maybe CgSRealType)]
    forall a. Eq a => [a] -> [a]
    nub [(Maybe Int, Maybe CgSRealType)]
    kinds
            bundleKind :: (Maybe Int, Maybe CgSRealType)
    bundleKind  = [(Maybe Int, Maybe CgSRealType)] -> (Maybe Int, Maybe CgSRealType)
    forall a. [a] -> a
    head [(Maybe Int, Maybe CgSRealType)]
    nubKinds
            files :: [(FilePath, (CgPgmKind, [Doc]))]
    files       = [[(FilePath, (CgPgmKind, [Doc]))]]
    -> [(FilePath, (CgPgmKind, [Doc]))]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(FilePath, (CgPgmKind, [Doc]))]
    fs | CgPgmBundle _ fs :: [(FilePath, (CgPgmKind, [Doc]))]
    fs <- [CgPgmBundle]
    bundles]
            sigs :: [Doc]
    sigs        = [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Doc]
    ss | (_, (CgHeader ss :: [Doc]
    ss, _)) <- [(FilePath, (CgPgmKind, [Doc]))]
    files]
            anyMake :: Bool
    anyMake     = Bool -> Bool
    not ([()] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | (_, (CgMakefile{}, _)) <- [(FilePath, (CgPgmKind, [Doc]))]
    files])
            drivers :: [[Doc]]
    drivers     = [[Doc]
    ds | (_, (CgDriver, ds :: [Doc]
    ds)) <- [(FilePath, (CgPgmKind, [Doc]))]
    files]
            anyDriver :: Bool
    anyDriver   = Bool -> Bool
    not ([[Doc]] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Doc]]
    drivers)
            mkFlags :: [FilePath]
    mkFlags     = [FilePath] -> [FilePath]
    forall a. Eq a => [a] -> [a]
    nub ([[FilePath]] -> [FilePath]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[FilePath]
    xs | (_, (CgMakefile xs :: [FilePath]
    xs, _)) <- [(FilePath, (CgPgmKind, [Doc]))]
    files])
            sources :: [(FilePath, (CgPgmKind, [Doc]))]
    sources     = [(FilePath
    f, (CgPgmKind
    CgSource, [Doc
    pre, Doc
    libHInclude, Doc
    post])) | (f :: FilePath
    f, (CgSource, [pre :: Doc
    pre, _, post :: Doc
    post])) <- [(FilePath, (CgPgmKind, [Doc]))]
    files]
            sourceNms :: [FilePath]
    sourceNms   = ((FilePath, (CgPgmKind, [Doc])) -> FilePath)
    -> [(FilePath, (CgPgmKind, [Doc]))] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, (CgPgmKind, [Doc])) -> FilePath
    forall a b. (a, b) -> a
    fst [(FilePath, (CgPgmKind, [Doc]))]
    sources
            libHeader :: (FilePath, (CgPgmKind, [Doc]))
    libHeader   = (FilePath
    libName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".h", ([Doc] -> CgPgmKind
    CgHeader [Doc]
    sigs, [(Maybe Int, Maybe CgSRealType) -> FilePath -> [Doc] -> Doc -> Doc
    genHeader (Maybe Int, Maybe CgSRealType)
    bundleKind FilePath
    libName [Doc]
    sigs Doc
    empty]))
            libHInclude :: Doc
    libHInclude = FilePath -> Doc
    text "#include" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text (FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show (FilePath
    libName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".h"))
            libMake :: (FilePath, (CgPgmKind, [Doc]))
    libMake     = ("Makefile", ([FilePath] -> CgPgmKind
    CgMakefile [FilePath]
    mkFlags, [Bool -> FilePath -> [FilePath] -> [FilePath] -> Doc
    genLibMake Bool
    anyDriver FilePath
    libName [FilePath]
    sourceNms [FilePath]
    mkFlags]))
            libDriver :: (FilePath, (CgPgmKind, [Doc]))
    libDriver   = (FilePath
    libName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "_driver.c", (CgPgmKind
    CgDriver, FilePath -> Doc -> [(FilePath, [Doc])] -> [Doc]
    mergeDrivers FilePath
    libName Doc
    libHInclude ([FilePath] -> [[Doc]] -> [(FilePath, [Doc])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> FilePath
    takeBaseName [FilePath]
    sourceNms) [[Doc]]
    drivers)))
            finalCfg :: CgConfig
    finalCfg    = case [(CgConfig, CgPgmBundle)]
    cfgBundles of
                            []         -> CgConfig
    defaultCgConfig
                            ((c :: CgConfig
    c, _):_) -> CgConfig
    c

    -- | Create a Makefile for the library
    genLibMake :: Bool -> String -> [String] -> [String] -> Doc
    genLibMake :: Bool -> FilePath -> [FilePath] -> [FilePath] -> Doc
    genLibMake ifdr :: Bool
    ifdr libName :: FilePath
    libName fs :: [FilePath]
    fs ldFlags :: [FilePath]
    ldFlags = (Doc -> Doc -> Doc) -> [Doc] -> Doc
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Doc -> Doc -> Doc
    ($$) [Doc
    l | (True, l :: Doc
    l) <- [(Bool, Doc)]
    lns]
     where ifld :: Bool
    ifld = Bool -> Bool
    not ([FilePath] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [FilePath]
    ldFlags)
           ld :: Doc
    ld | Bool
    ifld = FilePath -> Doc
    text "${LDFLAGS}"
              | Bool
    True = Doc
    empty
           lns :: [(Bool, Doc)]
    lns = [ (Bool
    True, FilePath -> Doc
    text "# Makefile for" Doc -> Doc -> Doc
    <+> Doc
    nm Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ". Automatically generated by SBV. Do not edit!")
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 , (Bool
    True,  FilePath -> Doc
    text "# include any user-defined .mk file in the current directory.")
                 , (Bool
    True,  FilePath -> Doc
    text "-include *.mk")
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 , (Bool
    True,  FilePath -> Doc
    text "CC?=gcc")
                 , (Bool
    True,  FilePath -> Doc
    text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer")
                 , (Bool
    ifld,  FilePath -> Doc
    text "LDFLAGS?=" Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ([FilePath] -> FilePath
    unwords [FilePath]
    ldFlags))
                 , (Bool
    True,  FilePath -> Doc
    text "AR?=ar")
                 , (Bool
    True,  FilePath -> Doc
    text "ARFLAGS?=cr")
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 , (Bool -> Bool
    not Bool
    ifdr,  FilePath -> Doc
    text ("all: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    liba))
                 , (Bool
    ifdr,      FilePath -> Doc
    text ("all: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [FilePath] -> FilePath
    unwords [FilePath
    liba, FilePath
    libd]))
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 , (Bool
    True,  FilePath -> Doc
    text FilePath
    liba Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text (": " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [FilePath] -> FilePath
    unwords [FilePath]
    os))
                 , (Bool
    True,  FilePath -> Doc
    text "\t${AR} ${ARFLAGS} $@ $^")
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 , (Bool
    ifdr,  FilePath -> Doc
    text FilePath
    libd Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text (": " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [FilePath] -> FilePath
    unwords [FilePath
    libd FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".c", FilePath
    libh]))
                 , (Bool
    ifdr,  FilePath -> Doc
    text ("\t${CC} ${CCFLAGS} $< -o $@ " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    liba) Doc -> Doc -> Doc
    <+> Doc
    ld)
                 , (Bool
    ifdr,  FilePath -> Doc
    text "")
                 , (Bool
    True,  [Doc] -> Doc
    vcat ((FilePath -> FilePath -> Doc) -> [FilePath] -> [FilePath] -> [Doc]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith FilePath -> FilePath -> Doc
    mkObj [FilePath]
    os [FilePath]
    fs))
                 , (Bool
    True,  FilePath -> Doc
    text "clean:")
                 , (Bool
    True,  FilePath -> Doc
    text "\trm -f *.o")
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 , (Bool
    True,  FilePath -> Doc
    text "veryclean: clean")
                 , (Bool -> Bool
    not Bool
    ifdr,  FilePath -> Doc
    text "\trm -f" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    liba)
                 , (Bool
    ifdr,      FilePath -> Doc
    text "\trm -f" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text ([FilePath] -> FilePath
    unwords [FilePath
    liba, FilePath
    libd]))
                 , (Bool
    True,  FilePath -> Doc
    text "")
                 ]
           nm :: Doc
    nm = FilePath -> Doc
    text FilePath
    libName
           liba :: FilePath
    liba = FilePath
    libName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".a"
           libh :: FilePath
    libh = FilePath
    libName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ".h"
           libd :: FilePath
    libd = FilePath
    libName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "_driver"
           os :: [FilePath]
    os   = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath -> FilePath -> FilePath
    `replaceExtension` ".o") [FilePath]
    fs
           mkObj :: FilePath -> FilePath -> Doc
    mkObj o :: FilePath
    o f :: FilePath
    f =  FilePath -> Doc
    text FilePath
    o Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text (": " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [FilePath] -> FilePath
    unwords [FilePath
    f, FilePath
    libh])
                     Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "\t${CC} ${CCFLAGS} -c $< -o $@"
                     Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""

    -- | Create a driver for a library
    mergeDrivers :: String -> Doc -> [(FilePath, [Doc])] -> [Doc]
    mergeDrivers :: FilePath -> Doc -> [(FilePath, [Doc])] -> [Doc]
    mergeDrivers libName :: FilePath
    libName inc :: Doc
    inc ds :: [(FilePath, [Doc])]
    ds = Doc
    pre Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : ((FilePath, [Doc]) -> [Doc]) -> [(FilePath, [Doc])] -> [Doc]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (FilePath, [Doc]) -> [Doc]
    mkDFun [(FilePath, [Doc])]
    ds [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [[FilePath] -> Doc
    callDrivers (((FilePath, [Doc]) -> FilePath)
    -> [(FilePath, [Doc])] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, [Doc]) -> FilePath
    forall a b. (a, b) -> a
    fst [(FilePath, [Doc])]
    ds)]
      where pre :: Doc
    pre =  FilePath -> Doc
    text "/* Example driver program for" Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text FilePath
    libName Doc -> Doc -> Doc
    P.<> FilePath -> Doc
    text ". */"
                Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "/* Automatically generated by SBV. Edit as you see fit! */"
                Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
                Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "#include <stdio.h>"
                Doc -> Doc -> Doc
    $$ Doc
    inc
            mkDFun :: (FilePath, [Doc]) -> [Doc]
    mkDFun (f :: FilePath
    f, [_pre :: Doc
    _pre, _header :: Doc
    _header, body :: Doc
    body, _post :: Doc
    _post]) = [Doc
    header, Doc
    body, Doc
    post]
               where header :: Doc
    header =  FilePath -> Doc
    text ""
                            Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ("void " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    f FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "_driver(void)")
                            Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "{"
                     post :: Doc
    post   =  FilePath -> Doc
    text "}"
            mkDFun (f :: FilePath
    f, _) = FilePath -> [Doc]
    forall a. FilePath -> a
    die (FilePath -> [Doc]) -> FilePath -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ "mergeDrivers: non-conforming driver program for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    f
            callDrivers :: [FilePath] -> Doc
    callDrivers fs :: [FilePath]
    fs =   FilePath -> Doc
    text ""
                           Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "int main(void)"
                           Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "{"
                           Doc -> Doc -> Doc
    $+$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((FilePath -> Doc) -> [FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Doc
    call [FilePath]
    fs))
                           Doc -> Doc -> Doc
    $$  Int -> Doc -> Doc
    nest 2 (FilePath -> Doc
    text "return 0;")
                           Doc -> Doc -> Doc
    $$  FilePath -> Doc
    text "}"
            call :: FilePath -> Doc
    call f :: FilePath
    f =  FilePath -> Doc
    text FilePath
    psep
                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text FilePath
    ptag
                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text FilePath
    psep
                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text (FilePath
    f FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "_driver();")
                   Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text ""
               where tag :: FilePath
    tag  = "** Driver run for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    f FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ":"
                     ptag :: FilePath
    ptag = "printf(\"" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    tag FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\\n\");"
                     lsep :: FilePath
    lsep = Int -> Char -> FilePath
    forall a. Int -> a -> [a]
    replicate (FilePath -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length FilePath
    tag) '='
                     psep :: FilePath
    psep = "printf(\"" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    lsep FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\\n\");"

    -- Does this operation with this result kind require an LD flag?
    getLDFlag :: (Op, Kind) -> [String]
    getLDFlag :: (Op, Kind) -> [FilePath]
    getLDFlag (o :: Op
    o, k :: Kind
    k) = Op -> [FilePath]
    flag Op
    o
      where math :: [FilePath]
    math = ["-lm"]

            flag :: Op -> [FilePath]
    flag (IEEEFP FP_Cast{})                                     = [FilePath]
    math
            flag (IEEEFP fop :: FPOp
    fop)       | FPOp
    fop FPOp -> [FPOp] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [FPOp]
    requiresMath           = [FilePath]
    math
            flag Abs                | Kind
    k Kind -> [Kind] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Kind
    KFloat, Kind
    KDouble, Kind
    KReal] = [FilePath]
    math
            flag _                                                      = []

            requiresMath :: [FPOp]
    requiresMath = [ FPOp
    FP_Abs
                           , FPOp
    FP_FMA
                           , FPOp
    FP_Sqrt
                           , FPOp
    FP_Rem
                           , FPOp
    FP_Min
                           , FPOp
    FP_Max
                           , FPOp
    FP_RoundToIntegral
                           , FPOp
    FP_ObjEqual
                           , FPOp
    FP_IsSubnormal
                           , FPOp
    FP_IsInfinite
                           , FPOp
    FP_IsNaN
                           , FPOp
    FP_IsNegative
                           , FPOp
    FP_IsPositive
                           , FPOp
    FP_IsNormal
                           , FPOp
    FP_IsZero
                           ]

    {-# ANN module ("HLint: ignore Redundant lambda" :: String) #-}