    -----------------------------------------------------------------------------
    -- |
    -- 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 #-}
    {-# LANGUAGE TupleSections #-}

    {-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}

    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

    import Data.SBV.Core.Symbolic (ResultInp(..), ProgInfo(..))

    -- 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 :: forall a. Maybe String -> String -> SBVCodeGen a -> IO a
    compileToC Maybe String
    mbDirName String
    nm SBVCodeGen a
    f = do (a
    retVal, CgConfig
    cfg, CgPgmBundle
    bundle) <- String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    forall a. String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC' String
    nm SBVCodeGen a
    f
                                   Maybe String -> (CgConfig, CgPgmBundle) -> IO ()
    renderCgPgmBundle Maybe String
    mbDirName (CgConfig
    cfg, CgPgmBundle
    bundle)
                                   a -> IO a
    forall a. 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' :: forall a. String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC' String
    nm SBVCodeGen a
    f = do [Integer]
    rands <- StdGen -> [Integer]
    forall g. RandomGen g => g -> [Integer]
    forall a g. (Random a, RandomGen g) => g -> [a]
    randoms (StdGen -> [Integer]) -> IO StdGen -> IO [Integer]
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` IO StdGen
    forall (m :: * -> *). MonadIO m => m StdGen
    newStdGen
                          SBVToC
    -> CgConfig
    -> String
    -> SBVCodeGen a
    -> IO (a, CgConfig, CgPgmBundle)
    forall l a.
    CgTarget l =>
    l
    -> CgConfig
    -> String
    -> SBVCodeGen a
    -> IO (a, CgConfig, CgPgmBundle)
    codeGen SBVToC
    SBVToC (CgConfig
    defaultCgConfig { cgDriverVals :: [Integer]
    cgDriverVals = [Integer]
    rands }) String
    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 :: forall a.
    Maybe String -> String -> [(String, SBVCodeGen a)] -> IO [a]
    compileToCLib Maybe String
    mbDirName String
    libName [(String, SBVCodeGen a)]
    comps = do ([a]
    retVal, CgConfig
    cfg, CgPgmBundle
    pgm) <- String
    -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    forall a.
    String
    -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    compileToCLib' String
    libName [(String, SBVCodeGen a)]
    comps
                                               Maybe String -> (CgConfig, CgPgmBundle) -> IO ()
    renderCgPgmBundle Maybe String
    mbDirName (CgConfig
    cfg, CgPgmBundle
    pgm)
                                               [a] -> IO [a]
    forall a. 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' :: forall a.
    String
    -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
    compileToCLib' String
    libName [(String, SBVCodeGen a)]
    comps = do [(a, CgConfig, CgPgmBundle)]
    resCfgBundles <- ((String, SBVCodeGen a) -> IO (a, CgConfig, CgPgmBundle))
    -> [(String, SBVCodeGen a)] -> IO [(a, CgConfig, CgPgmBundle)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle))
    -> (String, SBVCodeGen a) -> IO (a, CgConfig, CgPgmBundle)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    forall a. String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    compileToC') [(String, SBVCodeGen a)]
    comps
                                      let (CgConfig
    finalCfg, CgPgmBundle
    finalPgm) = String -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
    mergeToLib String
    libName [(CgConfig
    c, CgPgmBundle
    b) | (a
    _, CgConfig
    c, CgPgmBundle
    b) <- [(a, CgConfig, CgPgmBundle)]
    resCfgBundles]
                                      ([a], CgConfig, CgPgmBundle) -> IO ([a], CgConfig, CgPgmBundle)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([a
    r | (a
    r, CgConfig
    _, CgPgmBundle
    _) <- [(a, CgConfig, CgPgmBundle)]
    resCfgBundles], CgConfig
    finalCfg, CgPgmBundle
    finalPgm)

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

    -- token for the target language
    data SBVToC = SBVToC

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

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

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

    cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle
    cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle
    cgen CgConfig
    cfg String
    nm CgState
    st 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..
       = String -> ()
    forall a. NFData a => a -> ()
    rnf (Doc -> String
    render Doc
    sig) () -> CgPgmBundle -> CgPgmBundle
    forall a b. a -> b -> b
    `seq` String -> ()
    forall a. NFData a => a -> ()
    rnf (Doc -> String
    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)
    -> [(String, (CgPgmKind, [Doc]))] -> CgPgmBundle
    CgPgmBundle (Maybe Int, Maybe CgSRealType)
    bundleKind
                            ([(String, (CgPgmKind, [Doc]))] -> CgPgmBundle)
    -> [(String, (CgPgmKind, [Doc]))] -> CgPgmBundle
    forall a b. (a -> b) -> a -> b
    $ [(String, (CgPgmKind, [Doc]))] -> [(String, (CgPgmKind, [Doc]))]
    forall {a} {b}. [(a, (CgPgmKind, b))] -> [(a, (CgPgmKind, b))]
    filt [ (String
    "Makefile",  ([String] -> CgPgmKind
    CgMakefile [String]
    flags, [Bool -> String -> String -> [String] -> Doc
    genMake (CgConfig -> Bool
    cgGenDriver CgConfig
    cfg) String
    nm String
    nmd [String]
    flags]))
                                   , (String
    nm  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".h", ([Doc] -> CgPgmKind
    CgHeader [Doc
    sig],   [(Maybe Int, Maybe CgSRealType) -> String -> [Doc] -> Doc -> Doc
    genHeader (Maybe Int, Maybe CgSRealType)
    bundleKind String
    nm [Doc
    sig] Doc
    extProtos]))
                                   , (String
    nmd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".c", (CgPgmKind
    CgDriver,         CgConfig
    -> [Integer]
    -> String
    -> [(String, CgVal)]
    -> [(String, CgVal)]
    -> Maybe SV
    -> [Doc]
    genDriver CgConfig
    cfg [Integer]
    randVals String
    nm [(String, CgVal)]
    ins [(String, CgVal)]
    outs Maybe SV
    mbRet))
                                   , (String
    nm  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".c", (CgPgmKind
    CgSource,         [Doc]
    body))
                                   ]

            ([Doc]
    body, [String]
    flagsNeeded) = CgConfig
    -> String
    -> Doc
    -> Result
    -> [(String, CgVal)]
    -> [(String, CgVal)]
    -> Maybe SV
    -> Doc
    -> ([Doc], [String])
    genCProg CgConfig
    cfg String
    nm Doc
    sig Result
    sbvProg [(String, CgVal)]
    ins [(String, 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 [(a, (CgPgmKind, b))]
    xs  = [(a, (CgPgmKind, b))
    c | c :: (a, (CgPgmKind, b))
    c@(a
    _, (CgPgmKind
    k, b
    _)) <- [(a, (CgPgmKind, b))]
    xs, CgPgmKind -> Bool
    need CgPgmKind
    k]
              where need :: CgPgmKind -> Bool
    need 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 :: String
    nmd      = String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_driver"
            sig :: Doc
    sig      = String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc
    pprCFunHeader String
    nm [(String, CgVal)]
    ins [(String, CgVal)]
    outs Maybe SV
    mbRet
            ins :: [(String, CgVal)]
    ins      = CgState -> [(String, CgVal)]
    cgInputs CgState
    st
            outs :: [(String, CgVal)]
    outs     = CgState -> [(String, CgVal)]
    cgOutputs CgState
    st
            mbRet :: Maybe SV
    mbRet    = case CgState -> [CgVal]
    cgReturns CgState
    st of
                         []           -> Maybe SV
    forall a. Maybe a
    Nothing
                         [CgAtomic SV
    o] -> SV -> Maybe SV
    forall a. a -> Maybe a
    Just SV
    o
                         [CgArray [SV]
    _]  -> String -> Maybe SV
    forall a. String -> a
    tbd String
    "Non-atomic return values"
                         [CgVal]
    _            -> String -> Maybe SV
    forall a. String -> a
    tbd String
    "Multiple return values"
            extProtos :: Doc
    extProtos = case CgState -> [String]
    cgPrototypes CgState
    st of
                         [] -> Doc
    empty
                         [String]
    xs -> [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text String
    "/* User given prototypes: */" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc
    text [String]
    xs
            extDecls :: Doc
    extDecls  = case CgState -> [String]
    cgDecls CgState
    st of
                         [] -> Doc
    empty
                         [String]
    xs -> [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text String
    "/* User given declarations: */" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc
    text [String]
    xs
            flags :: [String]
    flags    = [String]
    flagsNeeded [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ CgState -> [String]
    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 :: String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc
    pprCFunHeader String
    fn [(String, CgVal)]
    ins [(String, CgVal)]
    outs Maybe SV
    mbRet = Doc
    retType Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    fn Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma (((String, CgVal) -> Doc) -> [(String, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, CgVal) -> Doc
    mkParam [(String, CgVal)]
    ins [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ ((String, CgVal) -> Doc) -> [(String, CgVal)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, CgVal) -> Doc
    mkPParam [(String, CgVal)]
    outs)))
      where retType :: Doc
    retType = case Maybe SV
    mbRet of
                       Maybe SV
    Nothing -> String -> Doc
    text String
    "void"
                       Just SV
    sv -> Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv

    mkParam, mkPParam :: (String, CgVal) -> Doc
    mkParam :: (String, CgVal) -> Doc
    mkParam  (String
    n, CgAtomic SV
    sv)     = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    True  SV
    sv Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    n
    mkParam  (String
    _, CgArray  [])     = String -> Doc
    forall a. String -> a
    die String
    "mkParam: CgArray with no elements!"
    mkParam  (String
    n, CgArray  (SV
    sv:[SV]
    _)) = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    True  SV
    sv Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "*" Doc -> Doc -> Doc
    P.<> String -> Doc
    text String
    n
    mkPParam :: (String, CgVal) -> Doc
    mkPParam (String
    n, CgAtomic SV
    sv)     = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "*" Doc -> Doc -> Doc
    P.<> String -> Doc
    text String
    n
    mkPParam (String
    _, CgArray  [])     = String -> Doc
    forall a. String -> a
    die String
    "mPkParam: CgArray with no elements!"
    mkPParam (String
    n, CgArray  (SV
    sv:[SV]
    _)) = Bool -> SV -> Doc
    forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    False SV
    sv Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "*" Doc -> Doc -> Doc
    P.<> String -> Doc
    text String
    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 Int
    w SV
    sv = String -> Doc
    text String
    "const" Doc -> Doc -> Doc
    <+> String -> Doc
    pad (SV -> String
    forall a. HasKind a => a -> String
    showCType SV
    sv) Doc -> Doc -> Doc
    <+> String -> Doc
    text (SV -> String
    forall a. Show a => a -> String
    show SV
    sv)
      where pad :: String -> Doc
    pad String
    s = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s) Char
    ' '

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

    -- | Renders as "s0", etc, or the corresponding constant
    showSV :: CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV :: CgConfig -> [(SV, CV)] -> SV -> Doc
    showSV CgConfig
    cfg [(SV, CV)]
    consts SV
    sv
      | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV                 = String -> Doc
    text String
    "false"
      | SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV                  = String -> Doc
    text String
    "true"
      | Just 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                          = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ SV -> String
    forall a. Show a => a -> String
    show SV
    sv

    -- | Words as it would map to a C word
    pprCWord :: HasKind a => Bool -> a -> Doc
    pprCWord :: forall a. HasKind a => Bool -> a -> Doc
    pprCWord Bool
    cnst a
    v = (if Bool
    cnst then String -> Doc
    text String
    "const" else Doc
    empty) Doc -> Doc -> Doc
    <+> String -> Doc
    text (a -> String
    forall a. HasKind a => a -> String
    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 :: forall a. HasKind a => a -> String
    showCType a
    i = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    i of
                    KBounded Bool
    False Int
    1 -> String
    "SBool"
                    Kind
    k                -> Kind -> String
    forall a. Show a => a -> String
    show Kind
    k

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

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

            specF :: CgSRealType -> Doc
            specF :: CgSRealType -> Doc
    specF CgSRealType
    CgFloat      = String -> Doc
    text String
    "%a"
            specF CgSRealType
    CgDouble     = String -> Doc
    text String
    "%a"
            specF CgSRealType
    CgLongDouble = String -> Doc
    text String
    "%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 CgConfig
    cfg  (CV Kind
    KReal (CAlgReal (AlgRational Bool
    _ 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 CgSRealType
    CgFloat      = String -> Doc
    text String
    "F"
            sRealSuffix CgSRealType
    CgDouble     = Doc
    empty
            sRealSuffix CgSRealType
    CgLongDouble = String -> Doc
    text String
    "L"
    mkConst CgConfig
    cfg (CV Kind
    KUnbounded       (CInteger 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 CgConfig
    cfg (CV (KBounded Bool
    sg Int
    sz) (CInteger Integer
    i)) = Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst (CgConfig -> Bool
    cgShowU8InHex CgConfig
    cfg) Integer
    i (Bool
    sg,   Int
    sz)
    mkConst CgConfig
    cfg (CV Kind
    KBool            (CInteger Integer
    i)) = Bool -> Integer -> (Bool, Int) -> Doc
    showSizedConst (CgConfig -> Bool
    cgShowU8InHex CgConfig
    cfg) Integer
    i (Bool
    False, Int
    1)
    mkConst CgConfig
    _   (CV Kind
    KFloat           (CFloat Float
    f))   = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Float -> String
    showCFloat Float
    f
    mkConst CgConfig
    _   (CV Kind
    KDouble          (CDouble Double
    d))  = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Double -> String
    showCDouble Double
    d
    mkConst CgConfig
    _   (CV Kind
    KString          (CString String
    s))  = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> String
    forall a. Show a => a -> String
    show String
    s
    mkConst CgConfig
    _   (CV Kind
    KChar            (CChar Char
    c))    = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Char -> String
    forall a. Show a => a -> String
    show Char
    c
    mkConst CgConfig
    _   CV
    cv                                 = String -> Doc
    forall a. String -> a
    die (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "mkConst: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    cv

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

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

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

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

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

    -- | Generate the C program
    genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc -> ([Doc], [String])
    genCProg :: CgConfig
    -> String
    -> Doc
    -> Result
    -> [(String, CgVal)]
    -> [(String, CgVal)]
    -> Maybe SV
    -> Doc
    -> ([Doc], [String])
    genCProg CgConfig
    cfg String
    fn Doc
    proto (Result ProgInfo
    pinfo Set Kind
    kindInfo [(String, CV)]
    _tvals [(String, CV -> Bool, SV)]
    _ovals [(String, [String])]
    cgs ResultInp
    topInps (CnstMap
    _, [(SV, CV)]
    preConsts) [((Int, Kind, Kind), [SV])]
    tbls [(Int, ArrayInfo)]
    arrs [(String, (Maybe [String], SBVType))]
    _uis [SMTDef]
    axioms (SBVPgm Seq (SV, SBVExpr)
    asgns) Seq (Bool, [(String, String)], SV)
    cstrs [(String, Maybe CallStack, SV)]
    origAsserts [SV]
    _) [(String, CgVal)]
    inVars [(String, CgVal)]
    outVars Maybe SV
    mbRet 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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV->C: Unbounded integers are not supported by the C compiler."
              String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "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
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV->C: SReal values are not supported by the C compiler."
              String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\nUse 'cgSRealType' to specify a custom type for SReal representation."
      | Bool -> Bool
    not ([String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    usorts)
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV->C: Cannot compile functions with uninterpreted sorts: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    usorts
      | ProgInfo -> Bool
    hasQuants ProgInfo
    pinfo
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "SBV->C: Cannot compile in the presence of quantified variables."
      | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [SpecialRelOp] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (ProgInfo -> [SpecialRelOp]
    progSpecialRels ProgInfo
    pinfo)
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "SBV->C: Cannot compile in the presence of special relations."
      | Bool -> Bool
    not ([SMTDef] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SMTDef]
    axioms)
      = String -> ([Doc], [String])
    forall a. HasCallStack => String -> a
    error String
    "SBV->C: Cannot compile in the presence of 'smtFunction' definitions, use 'compileToCLib' instead."
      | Bool -> Bool
    not (Seq (Bool, [(String, String)], SV) -> Bool
    forall a. Seq a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Bool, [(String, String)], SV)
    cstrs)
      = String -> ([Doc], [String])
    forall a. String -> a
    tbd String
    "Explicit constraints"
      | Bool -> Bool
    not ([(Int, ArrayInfo)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Int, ArrayInfo)]
    arrs)
      = String -> ([Doc], [String])
    forall a. String -> a
    tbd String
    "User specified arrays"
      | Bool
    True
      = ([Doc
    pre, Doc
    header, Doc
    post], [String]
    flagsNeeded)
     where asserts :: [(String, Maybe CallStack, SV)]
    asserts | CgConfig -> Bool
    cgIgnoreAsserts CgConfig
    cfg = []
                   | Bool
    True                = [(String, Maybe CallStack, SV)]
    origAsserts

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

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

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

           post :: Doc
    post   = String -> Doc
    text String
    ""
                 Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat (((String, [String]) -> Doc) -> [(String, [String])] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, [String]) -> Doc
    codeSeg [(String, [String])]
    cgs)
                 Doc -> Doc -> Doc
    $$ Doc
    extDecls
                 Doc -> Doc -> Doc
    $$ Doc
    proto
                 Doc -> Doc -> Doc
    $$ String -> Doc
    text String
    "{"
                 Doc -> Doc -> Doc
    $$ String -> Doc
    text String
    ""
                 Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    2 (   [Doc] -> Doc
    vcat (((String, CgVal) -> [Doc]) -> [(String, CgVal)] -> [Doc]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Bool -> (Bool, (String, CgVal)) -> [Doc]
    genIO Bool
    True ((Bool, (String, CgVal)) -> [Doc])
    -> ((String, CgVal) -> (Bool, (String, CgVal)))
    -> (String, CgVal)
    -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\(String, CgVal)
    v -> ((String, CgVal) -> Bool
    isAlive (String, CgVal)
    v, (String, CgVal)
    v))) [(String, 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) (((String, Maybe CallStack, SV) -> (Int, Doc))
    -> [(String, Maybe CallStack, SV)] -> [(Int, Doc)]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, Maybe CallStack, SV) -> (Int, Doc)
    genAssert [(String, Maybe CallStack, SV)]
    asserts))
                            Doc -> Doc -> Doc
    $$ Bool -> Doc
    sepIf (Bool -> Bool
    not ([(SV, SBVExpr)] -> Bool
    forall a. [a] -> 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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Int, Kind, Kind), [SV])]
    tbls))
                            Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat (((String, CgVal) -> [Doc]) -> [(String, CgVal)] -> [Doc]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Bool -> (Bool, (String, CgVal)) -> [Doc]
    genIO Bool
    False ((Bool, (String, CgVal)) -> [Doc])
    -> ((String, CgVal) -> (Bool, (String, CgVal)))
    -> (String, CgVal)
    -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool
    True,)) [(String, 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
    $$ String -> Doc
    text String
    "}"
                 Doc -> Doc -> Doc
    $$ String -> Doc
    text String
    ""

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

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

           -- Do we need any linker flags for C?
           flagsNeeded :: [String]
    flagsNeeded = [String] -> [String]
    forall a. Eq a => [a] -> [a]
    nub ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((Op, Kind) -> [String]
    getLDFlag ((Op, Kind) -> [String])
    -> ((SV, SBVExpr) -> (Op, Kind)) -> (SV, SBVExpr) -> [String]
    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 (a
    sv, SBVApp Op
    o [SV]
    _) = (Op
    o, a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    sv)

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

           ins :: [NamedSymVar]
    ins = case ResultInp
    topInps of
                   ResultTopInps ([NamedSymVar]
    is, []) -> [NamedSymVar]
    is
                   ResultTopInps ([NamedSymVar], [NamedSymVar])
    is       -> String -> [NamedSymVar]
    forall a. String -> a
    die (String -> [NamedSymVar]) -> String -> [NamedSymVar]
    forall a b. (a -> b) -> a -> b
    $ String
    "Unexpected trackers: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([NamedSymVar], [NamedSymVar]) -> String
    forall a. Show a => a -> String
    show ([NamedSymVar], [NamedSymVar])
    is
                   ResultLamInps [(Quantifier, NamedSymVar)]
    is       -> String -> [NamedSymVar]
    forall a. String -> a
    die (String -> [NamedSymVar]) -> String -> [NamedSymVar]
    forall a b. (a -> b) -> a -> b
    $ String
    "Unexpected inputs  : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(Quantifier, NamedSymVar)] -> String
    forall a. Show a => a -> String
    show [(Quantifier, NamedSymVar)]
    is

           typeWidth :: Int
    typeWidth = Int -> [Int] -> Int
    forall {t}. (Num t, Ord t) => t -> [t] -> t
    getMax Int
    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) | (SV
    s, SBVExpr
    _) <- [(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) | NamedSymVar SV
    s Name
    _ <- [NamedSymVar]
    ins]
                    where len :: Kind -> Int
    len KReal{}            = Int
    5
                          len KFloat{}           = Int
    6 -- SFloat
                          len KDouble{}          = Int
    7 -- SDouble
                          len KString{}          = Int
    7 -- SString
                          len KChar{}            = Int
    5 -- SChar
                          len KUnbounded{}       = Int
    8
                          len Kind
    KBool              = Int
    5 -- SBool
                          len (KBounded Bool
    False Int
    n) = Int
    5 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> String
    forall a. Show a => a -> String
    show Int
    n) -- SWordN
                          len (KBounded Bool
    True  Int
    n) = Int
    4 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> String
    forall a. Show a => a -> String
    show Int
    n) -- SIntN
                          len KRational{}        = String -> Int
    forall a. String -> a
    die   String
    "Rational."
                          len KFP{}              = String -> Int
    forall a. String -> a
    die   String
    "Arbitrary float."
                          len (KList Kind
    s)          = String -> Int
    forall a. String -> a
    die (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "List sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    s
                          len (KSet  Kind
    s)          = String -> Int
    forall a. String -> a
    die (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "Set sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    s
                          len (KTuple [Kind]
    s)         = String -> Int
    forall a. String -> a
    die (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "Tuple sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> String
    forall a. Show a => a -> String
    show [Kind]
    s
                          len (KMaybe Kind
    k)         = String -> Int
    forall a. String -> a
    die (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "Maybe sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                          len (KEither Kind
    k1 Kind
    k2)    = String -> Int
    forall a. String -> a
    die (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "Either sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    k1, Kind
    k2)
                          len (KUserSort String
    s Maybe [String]
    _)    = String -> Int
    forall a. String -> a
    die (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "Uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

                          getMax :: t -> [t] -> t
    getMax t
    8 [t]
    _      = t
    8  -- 8 is the max we can get with SInteger, so don't bother looking any further
                          getMax t
    m []     = t
    m
                          getMax t
    m (t
    x:[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 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]
    : ((String, CgVal) -> Set SV) -> [(String, CgVal)] -> [Set SV]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, CgVal) -> Set SV
    forall {a}. (a, CgVal) -> Set SV
    usedCgVal [(String, 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 (a
    _, CgAtomic SV
    s)  = SV -> Set SV
    forall a. a -> Set a
    Set.singleton SV
    s
                   usedCgVal (a
    _, CgArray [SV]
    ss)  = [SV] -> Set SV
    forall a. Ord a => [a] -> Set a
    Set.fromList [SV]
    ss
                   usedAsgn :: (a, SBVExpr) -> Set SV
    usedAsgn  (a
    _, SBVApp Op
    o [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 (Int, Kind, Kind, Int)
    _ SV
    a SV
    b)             = [SV] -> Set SV
    forall a. Ord a => [a] -> Set a
    Set.fromList [SV
    a, SV
    b]
                   opSWs (IEEEFP (FP_Cast Kind
    _ Kind
    _ SV
    s)) = SV -> Set SV
    forall a. a -> Set a
    Set.singleton SV
    s
                   opSWs Op
    _                        = Set SV
    forall a. Set a
    Set.empty

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

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

           mkRet :: SV -> Doc
    mkRet SV
    sv = String -> Doc
    text String
    "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 ((Int
    i, Kind
    _, Kind
    k), [SV]
    elts) =  (Int
    location, Doc
    static Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "const" Doc -> Doc -> Doc
    <+> String -> Doc
    text (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k) Doc -> Doc -> Doc
    <+> String -> Doc
    text (String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i) Doc -> Doc -> Doc
    P.<> String -> Doc
    text String
    "[] = {"
                                                  Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    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
    $$ String -> Doc
    text String
    "};")
             where static :: Doc
    static   = if Int
    location Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == -Int
    1 then String -> Doc
    text String
    "static" else Doc
    empty
                   location :: Int
    location = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (-Int
    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 Kind
    _ (NodeId (Int
    _, Int
    n))) | SV -> Bool
    isConst SV
    s = -Int
    1
                                              | Bool
    True      = Int
    n

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

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

      where addIf :: [Int] -> Doc
            addIf :: [Int] -> Doc
    addIf [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 (String -> Doc
    text String
    "+") [Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "?" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    c Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    0) | (Doc
    a, 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 FPOp
    w [(SV, CV)]
    consts [(SV, Doc)]
    as Doc
    var = FPOp -> Doc
    cvt FPOp
    w
      where same :: b -> (b, b)
    same b
    f                   = (b
    f, b
    f)
            named :: t -> t -> (t -> b) -> (b, b)
    named t
    fnm t
    dnm t -> b
    f          = (t -> b
    f t
    fnm, t -> b
    f t
    dnm)

            cvt :: FPOp -> Doc
    cvt (FP_Cast Kind
    from Kind
    to SV
    m)     = case Maybe CV -> Maybe (Either String String)
    checkRM (SV
    m SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts) of
                                            Maybe (Either String String)
    Nothing          -> ([Doc] -> Doc) -> Doc
    forall {t}. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ \[Doc
    a] -> Doc -> Doc
    parens (String -> Doc
    text (Kind -> String
    forall a. Show a => a -> String
    show Kind
    to)) Doc -> Doc -> Doc
    <+> Doc -> Doc
    rnd Doc
    a
                                            Just (Left  String
    msg) -> String -> Doc
    forall a. String -> a
    die String
    msg
                                            Just (Right String
    msg) -> String -> Doc
    forall a. String -> a
    tbd String
    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 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 :: String
    f = if Kind -> Bool
    forall a. HasKind a => a -> Bool
    isFloat Kind
    from then String
    "rintf" else String
    "rint"
                                                   in String -> Doc
    text String
    f Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                                 | Bool
    True
                                                 = Doc
    a

            cvt (FP_Reinterpret Kind
    f Kind
    t) = case (Kind
    f, Kind
    t) of
                                         (KBounded Bool
    False Int
    32, Kind
    KFloat)  -> ([Doc] -> Doc) -> Doc
    forall {t}. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc] -> Doc
    cpy String
    "sizeof(SFloat)"
                                         (KBounded Bool
    False Int
    64, Kind
    KDouble) -> ([Doc] -> Doc) -> Doc
    forall {t}. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc] -> Doc
    cpy String
    "sizeof(SDouble)"
                                         (Kind
    KFloat,  KBounded Bool
    False Int
    32) -> ([Doc] -> Doc) -> Doc
    forall {t}. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc] -> Doc
    cpy String
    "sizeof(SWord32)"
                                         (Kind
    KDouble, KBounded Bool
    False Int
    64) -> ([Doc] -> Doc) -> Doc
    forall {t}. ([Doc] -> t) -> t
    cast (([Doc] -> Doc) -> Doc) -> ([Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [Doc] -> Doc
    cpy String
    "sizeof(SWord64)"
                                         (Kind, Kind)
    _                            -> String -> Doc
    forall a. String -> a
    die (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Reinterpretation from : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    t
                                        where cpy :: String -> [Doc] -> Doc
    cpy String
    sz = \[Doc
    a] -> let alhs :: Doc
    alhs = String -> Doc
    text String
    "&" Doc -> Doc -> Doc
    P.<> Doc
    var
                                                                   arhs :: Doc
    arhs = String -> Doc
    text String
    "&" Doc -> Doc -> Doc
    P.<> Doc
    a
                                                               in String -> Doc
    text String
    "memcpy" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    alhs, Doc
    arhs, String -> Doc
    text String
    sz]))
            cvt FPOp
    FP_Abs               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "fabsf" String
    "fabs" ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    _ [Doc
    a] -> String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_Neg               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "-" Doc -> Doc -> Doc
    P.<> Doc
    a
            cvt FPOp
    FP_Add               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a, Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "+" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FPOp
    FP_Sub               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a, Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "-" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FPOp
    FP_Mul               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a, Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "*" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FPOp
    FP_Div               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a, Doc
    b] -> Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "/" Doc -> Doc -> Doc
    <+> Doc
    b
            cvt FPOp
    FP_FMA               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "fmaf"  String
    "fma"  ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    _ [Doc
    a, Doc
    b, Doc
    c] -> String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b, Doc
    c]))
            cvt FPOp
    FP_Sqrt              = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "sqrtf" String
    "sqrt" ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    _ [Doc
    a]       -> String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_Rem               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "fmodf" String
    "fmod" ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    _ [Doc
    a, Doc
    b]    -> String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b]))
            cvt FPOp
    FP_RoundToIntegral   = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "rintf" String
    "rint" ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    _ [Doc
    a]       -> String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_Min               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "fminf" String
    "fmin" ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    k [Doc
    a, Doc
    b]    -> Kind -> Doc -> Doc -> Doc -> Doc
    wrapMinMax Kind
    k Doc
    a Doc
    b (String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b])))
            cvt FPOp
    FP_Max               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    -> String
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall {t} {b}. t -> t -> (t -> b) -> (b, b)
    named String
    "fmaxf" String
    "fmax" ((String -> Kind -> [Doc] -> Doc)
     -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
    -> (String -> Kind -> [Doc] -> Doc)
    -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
    forall a b. (a -> b) -> a -> b
    $ \String
    nm Kind
    k [Doc
    a, Doc
    b]    -> Kind -> Doc -> Doc -> Doc -> Doc
    wrapMinMax Kind
    k Doc
    a Doc
    b (String -> Doc
    text String
    nm Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc
    a, Doc
    b])))
            cvt FPOp
    FP_ObjEqual          = let mkIte :: Doc -> Doc -> Doc -> Doc
    mkIte   Doc
    x Doc
    y Doc
    z = Doc
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "?" Doc -> Doc -> Doc
    <+> Doc
    y Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> Doc
    z
                                           chkNaN :: Doc -> Doc
    chkNaN  Doc
    x     = String -> Doc
    text String
    "isnan"   Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    x
                                           signbit :: Doc -> Doc
    signbit Doc
    x     = String -> Doc
    text String
    "signbit" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    x
                                           eq :: Doc -> Doc -> Doc
    eq      Doc
    x Doc
    y   = Doc -> Doc
    parens (Doc
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "==" Doc -> Doc -> Doc
    <+> Doc
    y)
                                           eqZero :: Doc -> Doc
    eqZero  Doc
    x     = Doc -> Doc -> Doc
    eq Doc
    x (String -> Doc
    text String
    "0")
                                           negZero :: Doc -> Doc
    negZero Doc
    x     = Doc -> Doc
    parens (Doc -> Doc
    signbit Doc
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&" Doc -> Doc -> Doc
    <+> Doc -> Doc
    eqZero Doc
    x)
                                       in (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a, 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 FPOp
    FP_IsNormal          = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "isnormal" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_IsSubnormal       = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "FP_SUBNORMAL == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_IsZero            = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "FP_ZERO == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_IsInfinite        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "isinf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_IsNaN             = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "isnan" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_IsNegative        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "!isnan" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "signbit"  Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
            cvt FPOp
    FP_IsPositive        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
    forall {a}. (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    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
    $ \Kind
    _ [Doc
    a] -> String -> Doc
    text String
    "!isnan" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "!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
                       []            -> []
                       ((SV
    m, Doc
    _):[(SV, Doc)]
    args) -> case SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    m of
                                          KUserSort String
    "RoundingMode" Maybe [String]
    _ -> case Maybe CV -> Maybe (Either String String)
    checkRM (SV
    m SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts) of
                                                                          Maybe (Either String String)
    Nothing          -> [(SV, Doc)]
    args
                                                                          Just (Left  String
    msg) -> String -> [(SV, Doc)]
    forall a. String -> a
    die String
    msg
                                                                          Just (Right String
    msg) -> String -> [(SV, Doc)]
    forall a. String -> a
    tbd String
    msg
                                          Kind
    _                          -> [(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 String String)
    checkRM (Just cv :: CV
    cv@(CV (KUserSort String
    "RoundingMode" Maybe [String]
    _) CVal
    v)) =
                  case CVal
    v of
                    CUserSort (Maybe Int
    _, String
    "RoundNearestTiesToEven") -> Maybe (Either String String)
    forall a. Maybe a
    Nothing
                    CUserSort (Maybe Int
    _, String
    s)                        -> Either String String -> Maybe (Either String String)
    forall a. a -> Maybe a
    Just (String -> Either String String
    forall a b. b -> Either a b
    Right (String -> Either String String) -> String -> Either String String
    forall a b. (a -> b) -> a -> b
    $ String
    "handleIEEE: Unsupported rounding-mode: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> String
    forall a. Show a => a -> String
    show FPOp
    w)
                    CVal
    _                                       -> Either String String -> Maybe (Either String String)
    forall a. a -> Maybe a
    Just (String -> Either String String
    forall a b. a -> Either a b
    Left  (String -> Either String String) -> String -> Either String String
    forall a b. (a -> b) -> a -> b
    $ String
    "handleIEEE: Unexpected value for rounding-mode: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    cv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> String
    forall a. Show a => a -> String
    show FPOp
    w)
            checkRM (Just CV
    cv) = Either String String -> Maybe (Either String String)
    forall a. a -> Maybe a
    Just (String -> Either String String
    forall a b. a -> Either a b
    Left  (String -> Either String String) -> String -> Either String String
    forall a b. (a -> b) -> a -> b
    $ String
    "handleIEEE: Expected rounding-mode, but got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    cv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> String
    forall a. Show a => a -> String
    show FPOp
    w)
            checkRM Maybe CV
    Nothing   = Either String String -> Maybe (Either String String)
    forall a. a -> Maybe a
    Just (String -> Either String String
    forall a b. b -> Either a b
    Right (String -> Either String String) -> String -> Either String String
    forall a b. (a -> b) -> a -> b
    $ String
    "handleIEEE: Non-constant rounding-mode for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> String
    forall a. Show a => a -> String
    show FPOp
    w)

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

            dispatch :: (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> a
    dispatch (Kind -> [Doc] -> a
    fOp, Kind -> [Doc] -> a
    dOp) = (Kind -> [Doc] -> a, Kind -> [Doc] -> a) -> [(SV, Doc)] -> a
    forall {a} {b} {a}.
    HasKind a =>
    (Kind -> [b] -> a, Kind -> [b] -> a) -> [(a, b)] -> a
    pickOp (Kind -> [Doc] -> a
    fOp, Kind -> [Doc] -> a
    dOp) [(SV, Doc)]
    fpArgs
            cast :: ([Doc] -> t) -> t
    cast [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 Kind
    k Doc
    a Doc
    b Doc
    s = Doc -> Doc
    parens Doc
    cond Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "?" Doc -> Doc -> Doc
    <+> Doc
    zero Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> Doc
    s
              where zero :: Doc
    zero = String -> Doc
    text (String -> Doc) -> String -> 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 -> String
    showCFloat Float
    0 else Double -> String
    showCDouble Double
    0
                    cond :: Doc
    cond =                   Doc -> Doc
    parens (String -> Doc
    text String
    "FP_ZERO == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a)                                      -- a is zero
                           Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (String -> Doc
    text String
    "FP_ZERO == fpclassify" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    b)                                      -- b is zero
                           Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (String -> Doc
    text String
    "signbit" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "!=" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "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 CgConfig
    cfg [(SV, CV)]
    consts (SBVApp Op
    op [SV]
    opArgs) Doc
    lhs (Doc
    typ, 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
    <+> String -> Doc
    text String
    "=" Doc -> Doc -> Doc
    <+> Doc
    rhs
      where doNotAssign :: Op -> Bool
    doNotAssign (IEEEFP FP_Reinterpret{}) = Bool
    True   -- generates a memcpy instead; no simple assignment
            doNotAssign Op
    _                         = 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, String)]
    cBinOps = [ (Op
    Plus, String
    "+"),  (Op
    Times, String
    "*"), (Op
    Minus, String
    "-")
                      , (Op
    Equal, String
    "=="), (Op
    NotEqual, String
    "!="), (Op
    LessThan, String
    "<"), (Op
    GreaterThan, String
    ">"), (Op
    LessEq, String
    "<="), (Op
    GreaterEq, String
    ">=")
                      , (Op
    And, String
    "&"), (Op
    Or, String
    "|"), (Op
    XOr, String
    "^")
                      ]

            -- see if we can find a constant shift; makes the output way more readable
            getShiftAmnt :: Doc -> [SV] -> Doc
    getShiftAmnt 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 Kind
    _  (CInteger Integer
    i)) -> Integer -> Doc
    integer Integer
    i
                                        Maybe CV
    _                         -> Doc
    def
            getShiftAmnt Doc
    def [SV]
    _       = Doc
    def

            p :: Op -> [Doc] -> Doc
            p :: Op -> [Doc] -> Doc
    p (ArrRead ArrayIndex
    _)       [Doc]
    _  = String -> Doc
    forall a. String -> a
    tbd String
    "User specified arrays (ArrRead)"
            p (ArrEq ArrayIndex
    _ ArrayIndex
    _)       [Doc]
    _  = String -> Doc
    forall a. String -> a
    tbd String
    "User specified arrays (ArrEq)"
            p (Label String
    s)        [Doc
    a] = Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "/*" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    s Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "*/"
            p (IEEEFP FPOp
    w)         [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 PBOp
    pb) [Doc]
    as = PBOp -> [Doc] -> Doc
    handlePB PBOp
    pb [Doc]
    as
            p (OverflowOp OvOp
    o) [Doc]
    _      = String -> Doc
    forall a. String -> a
    tbd (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Overflow operations" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ OvOp -> String
    forall a. Show a => a -> String
    show OvOp
    o
            p (KindCast Kind
    _ Kind
    to)   [Doc
    a] = Doc -> Doc
    parens (String -> Doc
    text (Kind -> String
    forall a. Show a => a -> String
    show Kind
    to)) Doc -> Doc -> Doc
    <+> Doc
    a
            p (Uninterpreted String
    s) [] = String -> Doc
    text String
    "/* Uninterpreted constant */" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    s
            p (Uninterpreted String
    s) [Doc]
    as = String -> Doc
    text String
    "/* Uninterpreted function */" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    s Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc]
    as))
            p (Extract Int
    i Int
    j) [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. HasCallStack => [a] -> a
    head [SV]
    opArgs) Doc
    a
            p Op
    Join [Doc
    a, 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 (SV
    s1 : SV
    s2 : [SV]
    _) = [SV]
    opArgs in (SV
    s1, SV
    s2, Doc
    a, Doc
    b))
            p (Rol Int
    i) [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. HasCallStack => [a] -> a
    head [SV]
    opArgs)
            p (Ror Int
    i) [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. HasCallStack => [a] -> a
    head [SV]
    opArgs)
            p Op
    Shl     [Doc
    a, 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 Op
    Shr     [Doc
    a, 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 Op
    Not [Doc
    a]              = case SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    opArgs) of
                                       -- be careful about booleans, bitwise complement is not correct for them!
                                       Kind
    KBool -> String -> Doc
    text String
    "!" Doc -> Doc -> Doc
    P.<> Doc
    a
                                       Kind
    _     -> String -> Doc
    text String
    "~" Doc -> Doc -> Doc
    P.<> Doc
    a
            p Op
    Ite [Doc
    a, Doc
    b, Doc
    c] = Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "?" Doc -> Doc -> Doc
    <+> Doc
    b Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> Doc
    c
            p (LkUp (Int
    t, Kind
    k, Kind
    _, Int
    len) SV
    ind 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 [Doc
    index, 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 = String -> Doc
    text String
    "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 Doc
    cnd = Doc
    cnd Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "?" Doc -> Doc -> Doc
    <+> Doc
    defVal Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> Doc
    lkUp

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

                    canOverflow :: Bool -> b -> Bool
    canOverflow Bool
    True  b
    sz = (Integer
    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
    -b
    1)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    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 Bool
    False b
    sz = (Integer
    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
    -Integer
    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

                    (Bool
    needsCheckL, Bool
    needsCheckR) = case Kind
    k of
                                                   Kind
    KBool           -> (Bool
    False, Bool -> Int -> Bool
    forall {b}. Integral b => Bool -> b -> Bool
    canOverflow Bool
    False (Int
    1::Int))
                                                   KBounded Bool
    sg Int
    sz  -> (Bool
    sg, Bool -> Int -> Bool
    forall {b}. Integral b => Bool -> b -> Bool
    canOverflow Bool
    sg Int
    sz)
                                                   Kind
    KReal           -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with real value"
                                                   Kind
    KFloat          -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with float value"
                                                   Kind
    KDouble         -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with double value"
                                                   KFP{}           -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with arbitrary float value"
                                                   Kind
    KRational       -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with rational value"
                                                   Kind
    KString         -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with string value"
                                                   Kind
    KChar           -> String -> (Bool, Bool)
    forall a. String -> a
    die String
    "array index with character value"
                                                   Kind
    KUnbounded      -> case CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg of
                                                                        Maybe Int
    Nothing -> (Bool
    True, Bool
    True) -- won't matter, it'll be rejected later
                                                                        Just Int
    i  -> (Bool
    True, Bool -> Int -> Bool
    forall {b}. Integral b => Bool -> b -> Bool
    canOverflow Bool
    True Int
    i)
                                                   KList     Kind
    s     -> String -> (Bool, Bool)
    forall a. String -> a
    die (String -> (Bool, Bool)) -> String -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ String
    "List sort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    s
                                                   KSet      Kind
    s     -> String -> (Bool, Bool)
    forall a. String -> a
    die (String -> (Bool, Bool)) -> String -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ String
    "Set sort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    s
                                                   KTuple    [Kind]
    s     -> String -> (Bool, Bool)
    forall a. String -> a
    die (String -> (Bool, Bool)) -> String -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ String
    "Tuple sort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> String
    forall a. Show a => a -> String
    show [Kind]
    s
                                                   KMaybe    Kind
    ek    -> String -> (Bool, Bool)
    forall a. String -> a
    die (String -> (Bool, Bool)) -> String -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ String
    "Maybe sort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                                                   KEither   Kind
    k1 Kind
    k2 -> String -> (Bool, Bool)
    forall a. String -> a
    die (String -> (Bool, Bool)) -> String -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ String
    "Either sort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    k1, Kind
    k2)
                                                   KUserSort String
    s Maybe [String]
    _   -> String -> (Bool, Bool)
    forall a. String -> a
    die (String -> (Bool, Bool)) -> String -> (Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ String
    "Uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    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 Op
    Quot [Doc
    a, Doc
    b] = let k :: Kind
    k = SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [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 (Integer
    0::Integer)
                            in Kind -> String -> Doc -> Doc -> Doc -> Doc
    protectDiv0 Kind
    k String
    "/" Doc
    z Doc
    a Doc
    b
            p Op
    Rem  [Doc
    a, Doc
    b] = Kind -> String -> Doc -> Doc -> Doc -> Doc
    protectDiv0 (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    opArgs)) String
    "%" Doc
    a Doc
    a Doc
    b
            p Op
    UNeg [Doc
    a]    = Doc -> Doc
    parens (String -> Doc
    text String
    "-" Doc -> Doc -> Doc
    <+> Doc
    a)
            p Op
    Abs  [Doc
    a]    = let f :: Kind -> Doc
    f Kind
    KFloat             = String -> Doc
    text String
    "fabsf" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f Kind
    KDouble            = String -> Doc
    text String
    "fabs"  Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f (KBounded Bool
    False Int
    _) = String -> Doc
    text String
    "/* unsigned, skipping call to abs */" Doc -> Doc -> Doc
    <+> Doc
    a
                                f (KBounded Bool
    True Int
    32) = String -> Doc
    text String
    "labs"  Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f (KBounded Bool
    True Int
    64) = String -> Doc
    text String
    "llabs" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f Kind
    KUnbounded         = case CgConfig -> Maybe Int
    cgInteger CgConfig
    cfg of
                                                         Maybe Int
    Nothing -> Kind -> Doc
    f (Kind -> Doc) -> Kind -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Kind
    KBounded Bool
    True Int
    32 -- won't matter, it'll be rejected later
                                                         Just 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 Kind
    KReal              = case CgConfig -> Maybe CgSRealType
    cgReal CgConfig
    cfg of
                                                         Maybe CgSRealType
    Nothing           -> Kind -> Doc
    f Kind
    KDouble -- won't matter, it'll be rejected later
                                                         Just CgSRealType
    CgFloat      -> Kind -> Doc
    f Kind
    KFloat
                                                         Just CgSRealType
    CgDouble     -> Kind -> Doc
    f Kind
    KDouble
                                                         Just CgSRealType
    CgLongDouble -> String -> Doc
    text String
    "fabsl" Doc -> Doc -> Doc
    P.<> Doc -> Doc
    parens Doc
    a
                                f Kind
    _                  = String -> Doc
    text String
    "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. HasCallStack => [a] -> a
    head [SV]
    opArgs))
            -- for And/Or, translate to boolean versions if on boolean kind
            p Op
    And [Doc
    a, Doc
    b] | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    opArgs) Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool = Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&" Doc -> Doc -> Doc
    <+> Doc
    b
            p Op
    Or  [Doc
    a, Doc
    b] | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    opArgs) Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool = Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "||" Doc -> Doc -> Doc
    <+> Doc
    b
            p Op
    o [Doc
    a, Doc
    b]
              | Just String
    co <- Op -> [(Op, String)] -> Maybe String
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    o [(Op, String)]
    cBinOps
              = Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    co Doc -> Doc -> Doc
    <+> Doc
    b

            p Op
    Implies [Doc
    a, Doc
    b] | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    opArgs) Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool = Doc -> Doc
    parens (String -> Doc
    text String
    "!" Doc -> Doc -> Doc
    P.<> Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "||" Doc -> Doc -> Doc
    <+> Doc
    b)

            p Op
    NotEqual [Doc]
    xs = [Doc] -> Doc
    mkDistinct [Doc]
    xs
            p Op
    o [Doc]
    args = String -> Doc
    forall a. String -> a
    die (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Received operator " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Op -> String
    forall a. Show a => a -> String
    show Op
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " applied to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Doc] -> String
    forall a. Show a => a -> String
    show [Doc]
    args

            -- generate a pairwise inequality check
            mkDistinct :: [Doc] -> Doc
    mkDistinct [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 (Doc
    e:[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 Doc
    e1 Doc
    e2  = Doc -> Doc
    parens (Doc
    e1 Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "!=" Doc -> Doc -> Doc
    <+> Doc
    e2)

                    -- like punctuate, but more spacing
                    andAll :: [Doc] -> [Doc]
    andAll []     = []
                    andAll (Doc
    d:[Doc]
    ds) = Doc -> [Doc] -> [Doc]
    go Doc
    d [Doc]
    ds
                         where go :: Doc -> [Doc] -> [Doc]
    go Doc
    d' [] = [Doc
    d']
                               go Doc
    d' (Doc
    e:[Doc]
    es) = (Doc
    d' Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "&&") 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 -> String -> Doc -> Doc -> Doc -> Doc
    protectDiv0 Kind
    k String
    divOp Doc
    def Doc
    a Doc
    b = case Kind
    k of
                                            Kind
    KFloat  -> Doc
    res
                                            Kind
    KDouble -> Doc
    res
                                            Kind
    _       -> Doc
    wrap
               where res :: Doc
    res  = Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    divOp Doc -> Doc -> Doc
    <+> Doc
    b
                     wrap :: Doc
    wrap = Doc -> Doc
    parens (Doc
    b Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "== 0") Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "?" Doc -> Doc -> Doc
    <+> Doc
    def Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ":" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens Doc
    res

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

            rotate :: Bool -> Int -> Doc -> c -> Doc
    rotate Bool
    toLeft Int
    i Doc
    a c
    s
              | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    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
    == Int
    0  = Doc
    a
              | Bool
    True    = case c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf c
    s of
                            KBounded Bool
    True Int
    _             -> String -> Doc
    forall a. String -> a
    tbd (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Rotation of signed quantities: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Bool, Int, c) -> String
    forall a. Show a => a -> String
    show (Bool
    toLeft, Int
    i, c
    s)
                            KBounded Bool
    False 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 Bool
    False Int
    sz           ->     Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    cop  Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    i)
                                                          Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "|"
                                                          Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    cop' Doc -> Doc -> Doc
    <+> Int -> Doc
    int (Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i))
                            Kind
    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
                            Kind
    _                           -> String -> Doc
    forall a. String -> a
    tbd (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Rotation for unbounded quantity: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Bool, Int, c) -> String
    forall a. Show a => a -> String
    show (Bool
    toLeft, Int
    i, c
    s)
              where (String
    cop, String
    cop') | Bool
    toLeft = (String
    "<<", String
    ">>")
                                | Bool
    True   = (String
    ">>", String
    "<<")

            -- 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 Int
    hi Int
    lo a
    i Doc
    a  -- Isolate the bit-extraction case
              | Int
    hi Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    lo, KBounded Bool
    _ 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
    >= Int
    0
              = if Int
    hi Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0
                then String -> Doc
    text String
    "(SBool)" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "& 1")
                else String -> Doc
    text String
    "(SBool)" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Doc -> Doc
    parens (Doc
    a Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    ">>" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    hi) Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "& 1")
            extract Int
    hi Int
    lo a
    i Doc
    a
              | Int
    srcSize Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [Int
    64, Int
    32, Int
    16]
              = String -> Doc
    forall a. String -> a
    bad String
    "Unsupported source size"
              | (Int
    hi Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    8 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    0 Bool -> Bool -> Bool
    || Int
    lo Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    8 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    0
              = String -> Doc
    forall a. String -> a
    bad String
    "Unsupported non-byte-aligned extraction"
              | Int
    tgtSize Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    8 Bool -> Bool -> Bool
    || Int
    tgtSize Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `mod` Int
    8 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    0
              = String -> Doc
    forall a. String -> a
    bad String
    "Unsupported target size"
              | Bool
    True
              = String -> Doc
    text String
    cast Doc -> Doc -> Doc
    <+> Doc
    shifted
              where bad :: String -> a
    bad String
    why    = String -> a
    forall a. String -> a
    tbd (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "extract with " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int, Kind, a) -> String
    forall a. Show a => a -> String
    show (Int
    hi, Int
    lo, Kind
    k, a
    i) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (Reason: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    why String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".)"

                    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
    + Int
    1
                    signChange :: Bool
    signChange = Int
    srcSize Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    tgtSize

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

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

            -- TBD: ditto here for join, just like extract above
            join :: (b, b, Doc, Doc) -> Doc
    join (b
    i, b
    j, Doc
    a, 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 Bool
    False  Int
    8, KBounded Bool
    False  Int
    8) -> Doc -> Doc
    parens (Doc -> Doc
    parens (String -> Doc
    text String
    "(SWord16)" Doc -> Doc -> Doc
    <+> Doc
    a) Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "<< 8")  Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "|" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (String -> Doc
    text String
    "(SWord16)" Doc -> Doc -> Doc
    <+> Doc
    b)
                                  (KBounded Bool
    False Int
    16, KBounded Bool
    False Int
    16) -> Doc -> Doc
    parens (Doc -> Doc
    parens (String -> Doc
    text String
    "(SWord32)" Doc -> Doc -> Doc
    <+> Doc
    a) Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "<< 16") Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "|" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (String -> Doc
    text String
    "(SWord32)" Doc -> Doc -> Doc
    <+> Doc
    b)
                                  (KBounded Bool
    False Int
    32, KBounded Bool
    False Int
    32) -> Doc -> Doc
    parens (Doc -> Doc
    parens (String -> Doc
    text String
    "(SWord64)" Doc -> Doc -> Doc
    <+> Doc
    a) Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "<< 32") Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "|" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (String -> Doc
    text String
    "(SWord64)" Doc -> Doc -> Doc
    <+> Doc
    b)
                                  (Kind
    k1,                Kind
    k2)                -> String -> Doc
    forall a. String -> a
    tbd (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "join with " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ((Kind, b), (Kind, b)) -> String
    forall a. Show a => a -> String
    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 Doc
    d = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Char
    '"' Char -> String -> String
    forall a. a -> [a] -> [a]
    : Doc -> String
    ppSameLine Doc
    d String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\""

    -- Remove newlines.. Useful when generating Makefile and such
    ppSameLine :: Doc -> String
    ppSameLine :: Doc -> String
    ppSameLine = String -> String
    trim (String -> String) -> (Doc -> String) -> Doc -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> String
    render
     where trim :: String -> String
    trim String
    ""        = String
    ""
           trim (Char
    '\n':String
    cs) = Char
    ' ' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    trim ((Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace String
    cs)
           trim (Char
    c:String
    cs)    = Char
    c   Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    trim String
    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 [Doc]
    ds = (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Doc
    text (String -> Doc) -> (String -> String) -> String -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    pad) [String]
    ss
      where ss :: [String]
    ss    = (Doc -> String) -> [Doc] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> String
    render [Doc]
    ds
            l :: Int
    l     = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (Int
    0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : (String -> Int) -> [String] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    ss)
            pad :: String -> String
    pad String
    s = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s) Char
    ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    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 :: String -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
    mergeToLib String
    libName [(CgConfig, CgPgmBundle)]
    cfgBundles
      | [(Maybe Int, Maybe CgSRealType)] -> Int
    forall a. [a] -> 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
    /= Int
    1
      = String -> (CgConfig, CgPgmBundle)
    forall a. HasCallStack => String -> a
    error (String -> (CgConfig, CgPgmBundle))
    -> String -> (CgConfig, CgPgmBundle)
    forall a b. (a -> b) -> a -> b
    $  String
    "Cannot merge programs with differing SInteger/SReal mappings. Received the following kinds:\n"
              String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unlines (((Maybe Int, Maybe CgSRealType) -> String)
    -> [(Maybe Int, Maybe CgSRealType)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe Int, Maybe CgSRealType) -> String
    forall a. Show a => a -> String
    show [(Maybe Int, Maybe CgSRealType)]
    nubKinds)
      | Bool
    True
      = (CgConfig
    finalCfg, (Maybe Int, Maybe CgSRealType)
    -> [(String, (CgPgmKind, [Doc]))] -> CgPgmBundle
    CgPgmBundle (Maybe Int, Maybe CgSRealType)
    bundleKind ([(String, (CgPgmKind, [Doc]))] -> CgPgmBundle)
    -> [(String, (CgPgmKind, [Doc]))] -> CgPgmBundle
    forall a b. (a -> b) -> a -> b
    $ [(String, (CgPgmKind, [Doc]))]
    sources [(String, (CgPgmKind, [Doc]))]
    -> [(String, (CgPgmKind, [Doc]))] -> [(String, (CgPgmKind, [Doc]))]
    forall a. [a] -> [a] -> [a]
    ++ (String, (CgPgmKind, [Doc]))
    libHeader (String, (CgPgmKind, [Doc]))
    -> [(String, (CgPgmKind, [Doc]))] -> [(String, (CgPgmKind, [Doc]))]
    forall a. a -> [a] -> [a]
    : [(String, (CgPgmKind, [Doc]))
    libDriver | Bool
    anyDriver] [(String, (CgPgmKind, [Doc]))]
    -> [(String, (CgPgmKind, [Doc]))] -> [(String, (CgPgmKind, [Doc]))]
    forall a. [a] -> [a] -> [a]
    ++ [(String, (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 (Maybe Int, Maybe CgSRealType)
    k [(String, (CgPgmKind, [Doc]))]
    _ <- [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. HasCallStack => [a] -> a
    head [(Maybe Int, Maybe CgSRealType)]
    nubKinds
            files :: [(String, (CgPgmKind, [Doc]))]
    files       = [[(String, (CgPgmKind, [Doc]))]] -> [(String, (CgPgmKind, [Doc]))]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(String, (CgPgmKind, [Doc]))]
    fs | CgPgmBundle (Maybe Int, Maybe CgSRealType)
    _ [(String, (CgPgmKind, [Doc]))]
    fs <- [CgPgmBundle]
    bundles]
            sigs :: [Doc]
    sigs        = [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Doc]
    ss | (String
    _, (CgHeader [Doc]
    ss, [Doc]
    _)) <- [(String, (CgPgmKind, [Doc]))]
    files]
            anyMake :: Bool
    anyMake     = Bool -> Bool
    not ([()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | (String
    _, (CgMakefile{}, [Doc]
    _)) <- [(String, (CgPgmKind, [Doc]))]
    files])
            drivers :: [[Doc]]
    drivers     = [[Doc]
    ds | (String
    _, (CgPgmKind
    CgDriver, [Doc]
    ds)) <- [(String, (CgPgmKind, [Doc]))]
    files]
            anyDriver :: Bool
    anyDriver   = Bool -> Bool
    not ([[Doc]] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Doc]]
    drivers)
            mkFlags :: [String]
    mkFlags     = [String] -> [String]
    forall a. Eq a => [a] -> [a]
    nub ([[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]
    xs | (String
    _, (CgMakefile [String]
    xs, [Doc]
    _)) <- [(String, (CgPgmKind, [Doc]))]
    files])
            sources :: [(String, (CgPgmKind, [Doc]))]
    sources     = [(String
    f, (CgPgmKind
    CgSource, [Doc
    pre, Doc
    libHInclude, Doc
    post])) | (String
    f, (CgPgmKind
    CgSource, [Doc
    pre, Doc
    _, Doc
    post])) <- [(String, (CgPgmKind, [Doc]))]
    files]
            sourceNms :: [String]
    sourceNms   = ((String, (CgPgmKind, [Doc])) -> String)
    -> [(String, (CgPgmKind, [Doc]))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, (CgPgmKind, [Doc])) -> String
    forall a b. (a, b) -> a
    fst [(String, (CgPgmKind, [Doc]))]
    sources
            libHeader :: (String, (CgPgmKind, [Doc]))
    libHeader   = (String
    libName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".h", ([Doc] -> CgPgmKind
    CgHeader [Doc]
    sigs, [(Maybe Int, Maybe CgSRealType) -> String -> [Doc] -> Doc -> Doc
    genHeader (Maybe Int, Maybe CgSRealType)
    bundleKind String
    libName [Doc]
    sigs Doc
    empty]))
            libHInclude :: Doc
    libHInclude = String -> Doc
    text String
    "#include" Doc -> Doc -> Doc
    <+> String -> Doc
    text (String -> String
    forall a. Show a => a -> String
    show (String
    libName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".h"))
            libMake :: (String, (CgPgmKind, [Doc]))
    libMake     = (String
    "Makefile", ([String] -> CgPgmKind
    CgMakefile [String]
    mkFlags, [Bool -> String -> [String] -> [String] -> Doc
    genLibMake Bool
    anyDriver String
    libName [String]
    sourceNms [String]
    mkFlags]))
            libDriver :: (String, (CgPgmKind, [Doc]))
    libDriver   = (String
    libName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_driver.c", (CgPgmKind
    CgDriver, String -> Doc -> [(String, [Doc])] -> [Doc]
    mergeDrivers String
    libName Doc
    libHInclude ([String] -> [[Doc]] -> [(String, [Doc])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    takeBaseName [String]
    sourceNms) [[Doc]]
    drivers)))
            finalCfg :: CgConfig
    finalCfg    = case [(CgConfig, CgPgmBundle)]
    cfgBundles of
                            []         -> CgConfig
    defaultCgConfig
                            ((CgConfig
    c, CgPgmBundle
    _):[(CgConfig, CgPgmBundle)]
    _) -> CgConfig
    c

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

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

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

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

            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
                           ]

    {- HLint ignore module "Redundant lambda" -}