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

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

{-# OPTIONS_GHC -Wall -Werror #-}

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

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

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

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

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

import GHC.Stack

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

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

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

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

-- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle'
compileToCLib' :: String -> [(String, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
compileToCLib' :: FilePath
-> [(FilePath, SBVCodeGen a)] -> IO ([a], CgConfig, CgPgmBundle)
compileToCLib' FilePath
libName [(FilePath, SBVCodeGen a)]
comps = do [(a, CgConfig, CgPgmBundle)]
resCfgBundles <- ((FilePath, SBVCodeGen a) -> IO (a, CgConfig, CgPgmBundle))
-> [(FilePath, SBVCodeGen a)] -> IO [(a, CgConfig, CgPgmBundle)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle))
-> (FilePath, SBVCodeGen a) -> IO (a, CgConfig, CgPgmBundle)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
forall a. FilePath -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
compileToC') [(FilePath, SBVCodeGen a)]
comps
                                  let (CgConfig
finalCfg, CgPgmBundle
finalPgm) = FilePath -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
mergeToLib FilePath
libName [(CgConfig
c, CgPgmBundle
b) | (a
_, CgConfig
c, CgPgmBundle
b) <- [(a, CgConfig, CgPgmBundle)]
resCfgBundles]
                                  ([a], CgConfig, CgPgmBundle) -> IO ([a], CgConfig, CgPgmBundle)
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 -> FilePath
targetName SBVToC
_ = FilePath
"C"
  translate :: SBVToC -> CgConfig -> FilePath -> CgState -> Result -> CgPgmBundle
translate SBVToC
_  = CgConfig -> FilePath -> CgState -> Result -> CgPgmBundle
cgen

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

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

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

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

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

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

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

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

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

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

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

-- | The printf specifier for the type
specifier :: CgConfig -> SV -> Doc
specifier :: CgConfig -> SV -> Doc
specifier 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       -> FilePath -> Doc
text FilePath
"%s"
                     Kind
KChar         -> FilePath -> Doc
text FilePath
"%c"
                     KList Kind
k       -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"list sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
k
                     KSet  Kind
k       -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"set sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
k
                     KUserSort FilePath
s Maybe [FilePath]
_ -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"user sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s
                     KTuple [Kind]
k      -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"tuple sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Kind] -> FilePath
forall a. Show a => a -> FilePath
show [Kind]
k
                     KMaybe  Kind
k     -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"maybe sort: "  FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
k
                     KEither Kind
k1 Kind
k2 -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"either sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> FilePath
forall a. Show a => a -> FilePath
show (Kind
k1, Kind
k2)
  where u8InHex :: Bool
u8InHex = CgConfig -> Bool
cgShowU8InHex CgConfig
cfg

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

        specF :: CgSRealType -> Doc
        specF :: CgSRealType -> Doc
specF CgSRealType
CgFloat      = FilePath -> Doc
text FilePath
"%a"
        specF CgSRealType
CgDouble     = FilePath -> Doc
text FilePath
"%a"
        specF CgSRealType
CgLongDouble = FilePath -> Doc
text FilePath
"%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      = FilePath -> Doc
text FilePath
"F"
        sRealSuffix CgSRealType
CgDouble     = Doc
empty
        sRealSuffix CgSRealType
CgLongDouble = FilePath -> Doc
text FilePath
"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))   = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ Float -> FilePath
showCFloat Float
f
mkConst CgConfig
_   (CV Kind
KDouble          (CDouble Double
d))  = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ Double -> FilePath
showCDouble Double
d
mkConst CgConfig
_   (CV Kind
KString          (CString FilePath
s))  = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
s
mkConst CgConfig
_   (CV Kind
KChar            (CChar Char
c))    = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ Char -> FilePath
forall a. Show a => a -> FilePath
show Char
c
mkConst CgConfig
_   CV
cv                                 = FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"mkConst: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ CV -> FilePath
forall a. Show a => a -> FilePath
show CV
cv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

       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) | (Quantifier
_, NamedSymVar SV
s Name
_) <- ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [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
+ FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n) -- SWordN
                      len (KBounded Bool
True  Int
n) = Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n) -- SIntN
                      len (KList Kind
s)          = FilePath -> Int
forall a. FilePath -> a
die (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
"List sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
s
                      len (KSet  Kind
s)          = FilePath -> Int
forall a. FilePath -> a
die (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
"Set sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
s
                      len (KTuple [Kind]
s)         = FilePath -> Int
forall a. FilePath -> a
die (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
"Tuple sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Kind] -> FilePath
forall a. Show a => a -> FilePath
show [Kind]
s
                      len (KMaybe Kind
k)         = FilePath -> Int
forall a. FilePath -> a
die (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
"Maybe sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
k
                      len (KEither Kind
k1 Kind
k2)    = FilePath -> Int
forall a. FilePath -> a
die (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
"Either sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> FilePath
forall a. Show a => a -> FilePath
show (Kind
k1, Kind
k2)
                      len (KUserSort FilePath
s Maybe [FilePath]
_)    = FilePath -> Int
forall a. FilePath -> a
die (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
"Uninterpreted sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
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]
: ((FilePath, CgVal) -> Set SV) -> [(FilePath, CgVal)] -> [Set SV]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath, CgVal) -> Set SV
forall a. (a, CgVal) -> Set SV
usedCgVal [(FilePath, CgVal)]
outVars [Set SV] -> [Set SV] -> [Set SV]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> Set SV) -> [(SV, SBVExpr)] -> [Set SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, SBVExpr) -> Set SV
forall a. (a, SBVExpr) -> Set SV
usedAsgn [(SV, SBVExpr)]
assignments)
         where retSWs :: Set SV
retSWs = Set SV -> (SV -> Set SV) -> Maybe SV -> Set SV
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set SV
forall a. Set a
Set.empty SV -> Set SV
forall a. a -> Set a
Set.singleton Maybe SV
mbRet

               usedCgVal :: (a, CgVal) -> Set SV
usedCgVal (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 :: (FilePath, CgVal) -> Bool
isAlive (FilePath
_, CgAtomic SV
sv) = SV
sv SV -> Set SV -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SV
usedVariables
       isAlive (FilePath
_, CgVal
_)           = Bool
True

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

       mkRet :: SV -> Doc
mkRet SV
sv = FilePath -> Doc
text FilePath
"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
<+> FilePath -> Doc
text FilePath
"const" Doc -> Doc -> Doc
<+> FilePath -> Doc
text (Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
k) Doc -> Doc -> Doc
<+> FilePath -> Doc
text (FilePath
"table" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i) Doc -> Doc -> Doc
P.<> FilePath -> Doc
text FilePath
"[] = {"
                                              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
$$ FilePath -> Doc
text FilePath
"};")
         where static :: Doc
static   = if Int
location Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1 then FilePath -> Doc
text FilePath
"static" else Doc
empty
               location :: Int
location = [Int] -> Int
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
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 :: (FilePath, Maybe CallStack, SV) -> (Int, Doc)
genAssert (FilePath
msg, Maybe CallStack
cs, SV
sv) = (SV -> Int
getNodeId SV
sv, Doc
doc)
         where doc :: Doc
doc =     FilePath -> Doc
text FilePath
"/* ASSERTION:" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
msg
                     Doc -> Doc -> Doc
$$  Doc -> ([FilePath] -> Doc) -> Maybe [FilePath] -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty ([Doc] -> Doc
vcat ([Doc] -> Doc) -> ([FilePath] -> [Doc]) -> [FilePath] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> Doc) -> [FilePath] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Doc
text) (Maybe [(FilePath, SrcLoc)] -> Maybe [FilePath]
locInfo (CallStack -> [(FilePath, SrcLoc)]
getCallStack (CallStack -> [(FilePath, SrcLoc)])
-> Maybe CallStack -> Maybe [(FilePath, SrcLoc)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe CallStack
cs))
                     Doc -> Doc -> Doc
$$  FilePath -> Doc
text FilePath
" */"
                     Doc -> Doc -> Doc
$$  FilePath -> Doc
text FilePath
"if" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens (CgConfig -> [(SV, CV)] -> SV -> Doc
showSV CgConfig
cfg [(SV, CV)]
consts SV
sv)
                     Doc -> Doc -> Doc
$$  FilePath -> Doc
text FilePath
"{"
                     Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat [Doc
errOut, FilePath -> Doc
text FilePath
"exit(-1);"])
                     Doc -> Doc -> Doc
$$  FilePath -> Doc
text FilePath
"}"
                     Doc -> Doc -> Doc
$$  FilePath -> Doc
text FilePath
""
               errOut :: Doc
errOut = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"fprintf(stderr, \"%s:%d:ASSERTION FAILED: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
msg FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\\n\", __FILE__, __LINE__);"
               locInfo :: Maybe [(FilePath, SrcLoc)] -> Maybe [FilePath]
locInfo (Just [(FilePath, SrcLoc)]
ps) = let loc :: (FilePath, SrcLoc) -> FilePath
loc (FilePath
f, SrcLoc
sl) = [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SrcLoc -> FilePath
srcLocFile SrcLoc
sl, FilePath
":", Int -> FilePath
forall a. Show a => a -> FilePath
show (SrcLoc -> Int
srcLocStartLine SrcLoc
sl), FilePath
":", Int -> FilePath
forall a. Show a => a -> FilePath
show (SrcLoc -> Int
srcLocStartCol SrcLoc
sl), FilePath
":", FilePath
f ]
                                   in case ((FilePath, SrcLoc) -> FilePath)
-> [(FilePath, SrcLoc)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath, SrcLoc) -> FilePath
loc [(FilePath, SrcLoc)]
ps of
                                         []     -> Maybe [FilePath]
forall a. Maybe a
Nothing
                                         (FilePath
f:[FilePath]
rs) -> [FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just ([FilePath] -> Maybe [FilePath]) -> [FilePath] -> Maybe [FilePath]
forall a b. (a -> b) -> a -> b
$ (FilePath
" * SOURCE   : " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f) FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath
" *            " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++)  [FilePath]
rs
               locInfo Maybe [(FilePath, SrcLoc)]
_         = Maybe [FilePath]
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
<+> FilePath -> Doc
text FilePath
"<=" 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
<+> FilePath -> Doc
text FilePath
">=" 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
<+> FilePath -> Doc
text FilePath
"==" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
k
                    PB_Le [Int]
cs   Int
k -> [Int] -> Doc
addIf [Int]
cs         Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"<=" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
k
                    PB_Ge [Int]
cs   Int
k -> [Int] -> Doc
addIf [Int]
cs         Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
">=" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
k
                    PB_Eq [Int]
cs   Int
k -> [Int] -> Doc
addIf [Int]
cs         Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"==" 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 (FilePath -> Doc
text FilePath
"+") [Doc -> Doc
parens (Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"?" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
c Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" 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 FilePath FilePath)
checkRM (SV
m SV -> [(SV, CV)] -> Maybe CV
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SV, CV)]
consts) of
                                        Maybe (Either FilePath FilePath)
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 (FilePath -> Doc
text (Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
to)) Doc -> Doc -> Doc
<+> Doc -> Doc
rnd Doc
a
                                        Just (Left  FilePath
msg) -> FilePath -> Doc
forall a. FilePath -> a
die FilePath
msg
                                        Just (Right FilePath
msg) -> FilePath -> Doc
forall a. FilePath -> a
tbd FilePath
msg
                                      where -- if we're converting from float to some integral like; first use rint/rintf to do the internal conversion and then cast.
                                            rnd :: Doc -> Doc
rnd Doc
a
                                             | (Kind -> Bool
forall a. HasKind a => a -> Bool
isFloat Kind
from Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isDouble Kind
from) Bool -> Bool -> Bool
&& (Kind -> Bool
forall a. HasKind a => a -> Bool
isBounded Kind
to Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isUnbounded Kind
to)
                                             = let f :: FilePath
f = if Kind -> Bool
forall a. HasKind a => a -> Bool
isFloat Kind
from then FilePath
"rintf" else FilePath
"rint"
                                               in FilePath -> Doc
text FilePath
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
$ FilePath -> [Doc] -> Doc
cpy FilePath
"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
$ FilePath -> [Doc] -> Doc
cpy FilePath
"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
$ FilePath -> [Doc] -> Doc
cpy FilePath
"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
$ FilePath -> [Doc] -> Doc
cpy FilePath
"sizeof(SWord64)"
                                     (Kind, Kind)
_                            -> FilePath -> Doc
forall a. FilePath -> a
die (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Reinterpretation from : " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" to " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
t
                                    where cpy :: FilePath -> [Doc] -> Doc
cpy FilePath
sz = \[Doc
a] -> let alhs :: Doc
alhs = FilePath -> Doc
text FilePath
"&" Doc -> Doc -> Doc
P.<> Doc
var
                                                               arhs :: Doc
arhs = FilePath -> Doc
text FilePath
"&" Doc -> Doc -> Doc
P.<> Doc
a
                                                           in FilePath -> Doc
text FilePath
"memcpy" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc
alhs, Doc
arhs, FilePath -> Doc
text FilePath
sz]))
        cvt FPOp
FP_Abs               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"fabsf" FilePath
"fabs" ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_Neg               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"-" Doc -> Doc -> Doc
P.<> Doc
a
        cvt FPOp
FP_Add               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a, Doc
b] -> Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"+" Doc -> Doc -> Doc
<+> Doc
b
        cvt FPOp
FP_Sub               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a, Doc
b] -> Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"-" Doc -> Doc -> Doc
<+> Doc
b
        cvt FPOp
FP_Mul               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a, Doc
b] -> Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"*" Doc -> Doc -> Doc
<+> Doc
b
        cvt FPOp
FP_Div               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a, Doc
b] -> Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"/" Doc -> Doc -> Doc
<+> Doc
b
        cvt FPOp
FP_FMA               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"fmaf"  FilePath
"fma"  ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
_ [Doc
a, Doc
b, Doc
c] -> FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc
a, Doc
b, Doc
c]))
        cvt FPOp
FP_Sqrt              = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"sqrtf" FilePath
"sqrt" ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
_ [Doc
a]       -> FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_Rem               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"fmodf" FilePath
"fmod" ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
_ [Doc
a, Doc
b]    -> FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc
a, Doc
b]))
        cvt FPOp
FP_RoundToIntegral   = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"rintf" FilePath
"rint" ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
_ [Doc
a]       -> FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_Min               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"fminf" FilePath
"fmin" ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
k [Doc
a, Doc
b]    -> Kind -> Doc -> Doc -> Doc -> Doc
wrapMinMax Kind
k Doc
a Doc
b (FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc
a, Doc
b])))
        cvt FPOp
FP_Max               = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall t b. t -> t -> (t -> b) -> (b, b)
named FilePath
"fmaxf" FilePath
"fmax" ((FilePath -> Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (FilePath -> Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \FilePath
nm Kind
k [Doc
a, Doc
b]    -> Kind -> Doc -> Doc -> Doc -> Doc
wrapMinMax Kind
k Doc
a Doc
b (FilePath -> Doc
text FilePath
nm Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc
a, Doc
b])))
        cvt FPOp
FP_ObjEqual          = let mkIte :: Doc -> Doc -> Doc -> Doc
mkIte   Doc
x Doc
y Doc
z = Doc
x Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"?" Doc -> Doc -> Doc
<+> Doc
y Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" Doc -> Doc -> Doc
<+> Doc
z
                                       chkNaN :: Doc -> Doc
chkNaN  Doc
x     = FilePath -> Doc
text FilePath
"isnan"   Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
x
                                       signbit :: Doc -> Doc
signbit Doc
x     = FilePath -> Doc
text FilePath
"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
<+> FilePath -> Doc
text FilePath
"==" Doc -> Doc -> Doc
<+> Doc
y)
                                       eqZero :: Doc -> Doc
eqZero  Doc
x     = Doc -> Doc -> Doc
eq Doc
x (FilePath -> Doc
text FilePath
"0")
                                       negZero :: Doc -> Doc
negZero Doc
x     = Doc -> Doc
parens (Doc -> Doc
signbit Doc
x Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"&&" Doc -> Doc -> Doc
<+> Doc -> Doc
eqZero Doc
x)
                                   in (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \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 p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"isnormal" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_IsSubnormal       = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"FP_SUBNORMAL == fpclassify" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_IsZero            = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"FP_ZERO == fpclassify" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_IsInfinite        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"isinf" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_IsNaN             = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"isnan" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_IsNegative        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"!isnan" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"&&" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"signbit"  Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a
        cvt FPOp
FP_IsPositive        = (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall p. (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch ((Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall b. b -> (b, b)
same ((Kind -> [Doc] -> Doc)
 -> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc))
-> (Kind -> [Doc] -> Doc)
-> (Kind -> [Doc] -> Doc, Kind -> [Doc] -> Doc)
forall a b. (a -> b) -> a -> b
$ \Kind
_ [Doc
a] -> FilePath -> Doc
text FilePath
"!isnan" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"&&" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"!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 FilePath
"RoundingMode" Maybe [FilePath]
_ -> case Maybe CV -> Maybe (Either FilePath FilePath)
checkRM (SV
m SV -> [(SV, CV)] -> Maybe CV
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SV, CV)]
consts) of
                                                                      Maybe (Either FilePath FilePath)
Nothing          -> [(SV, Doc)]
args
                                                                      Just (Left  FilePath
msg) -> FilePath -> [(SV, Doc)]
forall a. FilePath -> a
die FilePath
msg
                                                                      Just (Right FilePath
msg) -> FilePath -> [(SV, Doc)]
forall a. FilePath -> a
tbd FilePath
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 FilePath FilePath)
checkRM (Just cv :: CV
cv@(CV (KUserSort FilePath
"RoundingMode" Maybe [FilePath]
_) CVal
v)) =
              case CVal
v of
                CUserSort (Maybe Int
_, FilePath
"RoundNearestTiesToEven") -> Maybe (Either FilePath FilePath)
forall a. Maybe a
Nothing
                CUserSort (Maybe Int
_, FilePath
s)                        -> Either FilePath FilePath -> Maybe (Either FilePath FilePath)
forall a. a -> Maybe a
Just (FilePath -> Either FilePath FilePath
forall a b. b -> Either a b
Right (FilePath -> Either FilePath FilePath)
-> FilePath -> Either FilePath FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"handleIEEE: Unsupported rounding-mode: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" for: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FPOp -> FilePath
forall a. Show a => a -> FilePath
show FPOp
w)
                CVal
_                                       -> Either FilePath FilePath -> Maybe (Either FilePath FilePath)
forall a. a -> Maybe a
Just (FilePath -> Either FilePath FilePath
forall a b. a -> Either a b
Left  (FilePath -> Either FilePath FilePath)
-> FilePath -> Either FilePath FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"handleIEEE: Unexpected value for rounding-mode: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ CV -> FilePath
forall a. Show a => a -> FilePath
show CV
cv FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" for: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FPOp -> FilePath
forall a. Show a => a -> FilePath
show FPOp
w)
        checkRM (Just CV
cv) = Either FilePath FilePath -> Maybe (Either FilePath FilePath)
forall a. a -> Maybe a
Just (FilePath -> Either FilePath FilePath
forall a b. a -> Either a b
Left  (FilePath -> Either FilePath FilePath)
-> FilePath -> Either FilePath FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"handleIEEE: Expected rounding-mode, but got: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ CV -> FilePath
forall a. Show a => a -> FilePath
show CV
cv FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" for: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FPOp -> FilePath
forall a. Show a => a -> FilePath
show FPOp
w)
        checkRM Maybe CV
Nothing   = Either FilePath FilePath -> Maybe (Either FilePath FilePath)
forall a. a -> Maybe a
Just (FilePath -> Either FilePath FilePath
forall a b. b -> Either a b
Right (FilePath -> Either FilePath FilePath)
-> FilePath -> Either FilePath FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"handleIEEE: Non-constant rounding-mode for: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FPOp -> FilePath
forall a. Show a => a -> FilePath
show FPOp
w)

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

        dispatch :: (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> p
dispatch (Kind -> [Doc] -> p
fOp, Kind -> [Doc] -> p
dOp) = (Kind -> [Doc] -> p, Kind -> [Doc] -> p) -> [(SV, Doc)] -> p
forall a b p.
HasKind a =>
(Kind -> [b] -> p, Kind -> [b] -> p) -> [(a, b)] -> p
pickOp (Kind -> [Doc] -> p
fOp, Kind -> [Doc] -> p
dOp) [(SV, Doc)]
fpArgs
        cast :: ([Doc] -> t) -> t
cast [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
<+> FilePath -> Doc
text FilePath
"?" Doc -> Doc -> Doc
<+> Doc
zero Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" Doc -> Doc -> Doc
<+> Doc
s
          where zero :: Doc
zero = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KFloat then Float -> FilePath
showCFloat Float
0 else Double -> FilePath
showCDouble Double
0
                cond :: Doc
cond =                   Doc -> Doc
parens (FilePath -> Doc
text FilePath
"FP_ZERO == fpclassify" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a)                                      -- a is zero
                       Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"&&" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text FilePath
"FP_ZERO == fpclassify" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
b)                                      -- b is zero
                       Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"&&" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text FilePath
"signbit" Doc -> Doc -> Doc
P.<> Doc -> Doc
parens Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"!=" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"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
<+> FilePath -> Doc
text FilePath
"=" 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, FilePath)]
cBinOps = [ (Op
Plus, FilePath
"+"),  (Op
Times, FilePath
"*"), (Op
Minus, FilePath
"-")
                  , (Op
Equal, FilePath
"=="), (Op
NotEqual, FilePath
"!="), (Op
LessThan, FilePath
"<"), (Op
GreaterThan, FilePath
">"), (Op
LessEq, FilePath
"<="), (Op
GreaterEq, FilePath
">=")
                  , (Op
And, FilePath
"&"), (Op
Or, FilePath
"|"), (Op
XOr, FilePath
"^")
                  ]

        -- 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]
_  = FilePath -> Doc
forall a. FilePath -> a
tbd FilePath
"User specified arrays (ArrRead)"
        p (ArrEq ArrayIndex
_ ArrayIndex
_)       [Doc]
_  = FilePath -> Doc
forall a. FilePath -> a
tbd FilePath
"User specified arrays (ArrEq)"
        p (Label FilePath
s)        [Doc
a] = Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"/*" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
s Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"*/"
        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]
_      = FilePath -> Doc
forall a. FilePath -> a
tbd (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Overflow operations" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ OvOp -> FilePath
forall a. Show a => a -> FilePath
show OvOp
o
        p (KindCast Kind
_ Kind
to)   [Doc
a] = Doc -> Doc
parens (FilePath -> Doc
text (Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
to)) Doc -> Doc -> Doc
<+> Doc
a
        p (Uninterpreted FilePath
s) [] = FilePath -> Doc
text FilePath
"/* Uninterpreted constant */" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
s
        p (Uninterpreted FilePath
s) [Doc]
as = FilePath -> Doc
text FilePath
"/* Uninterpreted function */" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
s Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
as))
        p (Extract 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. [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. [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. [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. [a] -> a
head [SV]
opArgs) of
                                   -- be careful about booleans, bitwise complement is not correct for them!
                                   Kind
KBool -> FilePath -> Doc
text FilePath
"!" Doc -> Doc -> Doc
P.<> Doc
a
                                   Kind
_     -> FilePath -> Doc
text FilePath
"~" Doc -> Doc -> Doc
P.<> Doc
a
        p Op
Ite [Doc
a, Doc
b, Doc
c] = Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"?" Doc -> Doc -> Doc
<+> Doc
b Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" 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 = FilePath -> Doc
text FilePath
"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
<+> FilePath -> Doc
text FilePath
"?" Doc -> Doc -> Doc
<+> Doc
defVal Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" Doc -> Doc -> Doc
<+> Doc
lkUp

                checkLeft :: Doc
checkLeft  = Doc
index Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"< 0"
                checkRight :: Doc
checkRight = Doc
index Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
">=" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
len
                checkBoth :: Doc
checkBoth  = Doc -> Doc
parens (Doc
checkLeft Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"||" 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           -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die FilePath
"array index with real value"
                                               Kind
KFloat          -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die FilePath
"array index with float value"
                                               Kind
KDouble         -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die FilePath
"array index with double value"
                                               Kind
KString         -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die FilePath
"array index with string value"
                                               Kind
KChar           -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die FilePath
"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     -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"List sort " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
s
                                               KSet      Kind
s     -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"Set sort " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
s
                                               KTuple    [Kind]
s     -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"Tuple sort " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Kind] -> FilePath
forall a. Show a => a -> FilePath
show [Kind]
s
                                               KMaybe    Kind
ek    -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"Maybe sort " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Kind -> FilePath
forall a. Show a => a -> FilePath
show Kind
ek
                                               KEither   Kind
k1 Kind
k2 -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"Either sort " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> FilePath
forall a. Show a => a -> FilePath
show (Kind
k1, Kind
k2)
                                               KUserSort FilePath
s Maybe [FilePath]
_   -> FilePath -> (Bool, Bool)
forall a. FilePath -> a
die (FilePath -> (Bool, Bool)) -> FilePath -> (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"Uninterpreted sort: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s

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

        -- generate a pairwise inequality check
        mkDistinct :: [Doc] -> Doc
mkDistinct [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
<+> FilePath -> Doc
text FilePath
"!=" 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
<+> FilePath -> Doc
text FilePath
"&&") Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc -> [Doc] -> [Doc]
go Doc
e [Doc]
es

        -- Div0 needs to protect, but only when the arguments are not float/double. (Div by 0 for those are well defined to be Inf/NaN etc.)
        protectDiv0 :: Kind -> FilePath -> Doc -> Doc -> Doc -> Doc
protectDiv0 Kind
k FilePath
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
<+> FilePath -> Doc
text FilePath
divOp Doc -> Doc -> Doc
<+> Doc
b
                 wrap :: Doc
wrap = Doc -> Doc
parens (Doc
b Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"== 0") Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"?" Doc -> Doc -> Doc
<+> Doc
def Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" 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
<+> FilePath -> Doc
text FilePath
cop Doc -> Doc -> Doc
<+> Doc
i
          where cop :: FilePath
cop | Bool
toLeft = FilePath
"<<"
                    | Bool
True   = FilePath
">>"

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

        -- 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 FilePath -> Doc
text FilePath
"(SBool)" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"& 1")
            else FilePath -> Doc
text FilePath
"(SBool)" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc -> Doc
parens (Doc
a Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
">>" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
hi) Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"& 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]
          = FilePath -> Doc
forall a. FilePath -> a
bad FilePath
"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
          = FilePath -> Doc
forall a. FilePath -> a
bad FilePath
"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
          = FilePath -> Doc
forall a. FilePath -> a
bad FilePath
"Unsupported target size"
          | Bool
True
          = FilePath -> Doc
text FilePath
cast Doc -> Doc -> Doc
<+> Doc
shifted
          where bad :: FilePath -> a
bad FilePath
why    = FilePath -> a
forall a. FilePath -> a
tbd (FilePath -> a) -> FilePath -> a
forall a b. (a -> b) -> a -> b
$ FilePath
"extract with " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Int, Int, Kind, a) -> FilePath
forall a. Show a => a -> FilePath
show (Int
hi, Int
lo, Kind
k, a
i) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" (Reason: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
why FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
".)"

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

                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
<+> FilePath -> Doc
text FilePath
">>" 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 (FilePath -> Doc
text FilePath
"(SWord16)" Doc -> Doc -> Doc
<+> Doc
a) Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"<< 8")  Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"|" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text FilePath
"(SWord16)" Doc -> Doc -> Doc
<+> Doc
b)
                              (KBounded Bool
False Int
16, KBounded Bool
False Int
16) -> Doc -> Doc
parens (Doc -> Doc
parens (FilePath -> Doc
text FilePath
"(SWord32)" Doc -> Doc -> Doc
<+> Doc
a) Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"<< 16") Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"|" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text FilePath
"(SWord32)" Doc -> Doc -> Doc
<+> Doc
b)
                              (KBounded Bool
False Int
32, KBounded Bool
False Int
32) -> Doc -> Doc
parens (Doc -> Doc
parens (FilePath -> Doc
text FilePath
"(SWord64)" Doc -> Doc -> Doc
<+> Doc
a) Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"<< 32") Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"|" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text FilePath
"(SWord64)" Doc -> Doc -> Doc
<+> Doc
b)
                              (Kind
k1,                Kind
k2)                -> FilePath -> Doc
forall a. FilePath -> a
tbd (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"join with " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ((Kind, b), (Kind, b)) -> FilePath
forall a. Show a => a -> FilePath
show ((Kind
k1, b
i), (Kind
k2, b
j))

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

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

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

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

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

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

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

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

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