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

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

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

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

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

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

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

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

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

import GHC.Stack

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

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

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

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

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

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

-- token for the target language
data SBVToC = SBVToC

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Almost a "show", but map "SWord1" to "SBool"
-- which is used for extracting one-bit words. This is OK since C's bool type
-- handles arithmetic fine, and maps nicely to our `SWord 1`. (Same isn't true for `SInt 1`, which
-- doesn't have an easy counter-part on the C side.
showCType :: HasKind a => a -> String
showCType :: forall a. HasKind a => a -> String
showCType a
i = case a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
i of
                KBounded Bool
False Int
1 -> String
"SBool"
                Kind
k                -> Kind -> String
forall a. Show a => a -> String
show Kind
k

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

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

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

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

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

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

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

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

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

-- | Generate the C program
genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SV -> Doc -> ([Doc], [String])
genCProg :: CgConfig
-> String
-> Doc
-> Result
-> [(String, CgVal)]
-> [(String, CgVal)]
-> Maybe SV
-> Doc
-> ([Doc], [String])
genCProg CgConfig
cfg String
fn Doc
proto (Result ProgInfo
pinfo Set Kind
kindInfo [(String, CV)]
_tvals [(String, CV -> Bool, SV)]
_ovals [(String, [String])]
cgs ResultInp
topInps (CnstMap
_, [(SV, CV)]
preConsts) [((Int, Kind, Kind), [SV])]
tbls [(String, (Bool, Maybe [String], SBVType))]
_uis [(SMTDef, SBVType)]
axioms (SBVPgm Seq (SV, SBVExpr)
asgns) Seq (Bool, [(String, String)], SV)
cstrs [(String, Maybe CallStack, SV)]
origAsserts [SV]
_) [(String, CgVal)]
inVars [(String, CgVal)]
outVars Maybe SV
mbRet Doc
extDecls
  | Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing (CgConfig -> Maybe Int
cgInteger CgConfig
cfg) Bool -> Bool -> Bool
&& Kind
KUnbounded Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
forall a b. (a -> b) -> a -> b
$ String
"SBV->C: Unbounded integers are not supported by the C compiler."
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."
  | Kind
KString Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Strings"
  | Kind
KChar Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Characters"
  | (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isSet Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Sets (SSet)"
  | (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isList Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Lists (SList)"
  | (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isTuple Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Tuples (STupleN)"
  | (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isMaybe Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Optional (SMaybe) values"
  | (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isEither Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. String -> a
notyet String
"Either (SEither) values"
  | Maybe CgSRealType -> Bool
forall a. Maybe a -> Bool
isNothing (CgConfig -> Maybe CgSRealType
cgReal CgConfig
cfg) Bool -> Bool -> Bool
&& Kind
KReal Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
forall a b. (a -> b) -> a -> b
$ String
"SBV->C: SReal values are not supported by the C compiler."
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nUse 'cgSRealType' to specify a custom type for SReal representation."
  | Bool -> Bool
not ([Kind] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Kind]
unsupportedBVs)
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
forall a b. (a -> b) -> a -> b
$ String
"SBV->C: Unsupported bit-vector type(s): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
forall a. Show a => a -> String
show [Kind]
unsupportedBVs)
  | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
usorts)
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error (String -> ([Doc], [String])) -> String -> ([Doc], [String])
forall a b. (a -> b) -> a -> b
$ String
"SBV->C: Cannot compile functions with uninterpreted sorts: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
usorts
  | ProgInfo -> Bool
hasQuants ProgInfo
pinfo
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error String
"SBV->C: Cannot compile in the presence of quantified variables."
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [SpecialRelOp] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ProgInfo -> [SpecialRelOp]
progSpecialRels ProgInfo
pinfo)
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error String
"SBV->C: Cannot compile in the presence of special relations."
  | Bool -> Bool
not ([(SMTDef, SBVType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(SMTDef, SBVType)]
axioms)
  = String -> ([Doc], [String])
forall a. HasCallStack => String -> a
error String
"SBV->C: Cannot compile in the presence of 'smtFunction' definitions, use 'compileToCLib' instead."
  | Bool -> Bool
not (Seq (Bool, [(String, String)], SV) -> Bool
forall a. Seq a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Bool, [(String, String)], SV)
cstrs)
  = String -> ([Doc], [String])
forall a. String -> a
tbd String
"Explicit constraints"
  | Bool
True
  = ([Doc
pre, Doc
header, Doc
post], [String]
flagsNeeded)
 where notyet :: String -> b
notyet String
m = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"SBV->C: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" are currently not supported by the C compiler. Please get in touch if you'd like support for this feature!"

       asserts :: [(String, Maybe CallStack, SV)]
asserts | CgConfig -> Bool
cgIgnoreAsserts CgConfig
cfg = []
               | Bool
True                = [(String, Maybe CallStack, SV)]
origAsserts

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

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

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

       unsupportedBVs :: [Kind]
unsupportedBVs = [Kind
k | k :: Kind
k@(KBounded Bool
sg Int
sz) <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kindInfo, (Bool -> Bool
not (Bool -> Bool) -> ((Bool, Int) -> Bool) -> (Bool, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, Int) -> Bool
forall {a}. (Eq a, Num a) => (Bool, a) -> Bool
supported) (Bool
sg, Int
sz)]
         where supported :: (Bool, a) -> Bool
supported (Bool
False, a
sz) = a
sz a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a
1, a
8, a
16, a
32, a
64]
               supported (Bool
True,  a
sz) = a
sz a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [   a
8, a
16, a
32, a
64]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        hd :: String -> [a] -> a
hd String
_ (a
h:[a]
_) = a
h
        hd String
w []    = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.C.ppExpr: Impossible happened: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", received empty list!"

        p :: Op -> [Doc] -> Doc
        p :: Op -> [Doc] -> Doc
p ReadArray{}       [Doc]
_  = String -> Doc
forall a. String -> a
tbd String
"User specified arrays (ReadArray)"
        p WriteArray{}      [Doc]
_  = String -> Doc
forall a. String -> a
tbd String
"User specified arrays (WriteArray)"
        p (Label String
s)        [Doc
a] = Doc
a Doc -> Doc -> Doc
<+> String -> Doc
text String
"/*" Doc -> Doc -> Doc
<+> String -> Doc
text String
s Doc -> Doc -> Doc
<+> String -> Doc
text String
"*/"
        p (IEEEFP FPOp
w)         [Doc]
as = FPOp -> [(SV, CV)] -> [(SV, Doc)] -> Doc -> Doc
handleIEEE FPOp
w  [(SV, CV)]
consts ([SV] -> [Doc] -> [(SV, Doc)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SV]
opArgs [Doc]
as) Doc
var
        p (PseudoBoolean PBOp
pb) [Doc]
as = PBOp -> [Doc] -> Doc
handlePB PBOp
pb [Doc]
as
        p (OverflowOp OvOp
o) [Doc]
_      = String -> Doc
forall a. String -> a
tbd (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Overflow operations" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OvOp -> String
forall a. Show a => a -> String
show OvOp
o
        p (KindCast Kind
_ Kind
to)   [Doc
a] = Doc -> Doc
parens (String -> Doc
text (Kind -> String
forall a. Show a => a -> String
show Kind
to)) Doc -> Doc -> Doc
<+> Doc
a
        p (Uninterpreted String
s) [] = String -> Doc
text String
"/* Uninterpreted constant */" Doc -> Doc -> Doc
<+> String -> Doc
text String
s
        p (Uninterpreted String
s) [Doc]
as = String -> Doc
text String
"/* Uninterpreted function */" Doc -> Doc -> Doc
<+> String -> Doc
text String
s Doc -> Doc -> Doc
P.<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
as))
        p (Extract Int
i Int
j) [Doc
a]    = Int -> Int -> SV -> Doc -> Doc
forall {a}. (HasKind a, Show a) => Int -> Int -> a -> Doc -> Doc
extract Int
i Int
j (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"Extract" [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 (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"Rol" [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 (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"Ror" [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 (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"Not" [SV]
opArgs) of
                                   -- be careful about booleans, bitwise complement is not correct for them!
                                   Kind
KBool -> String -> Doc
text String
"!" Doc -> Doc -> Doc
P.<> Doc
a
                                   Kind
_     -> String -> Doc
text String
"~" Doc -> Doc -> Doc
P.<> Doc
a
        p Op
Ite [Doc
a, Doc
b, Doc
c] = Doc
a Doc -> Doc -> Doc
<+> String -> Doc
text String
"?" Doc -> Doc -> Doc
<+> Doc
b Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Doc
c
        p (LkUp (Int
t, Kind
k, Kind
_, Int
len) SV
ind SV
def) []
          | Bool -> Bool
not Bool
rtc                    = Doc
lkUp -- ignore run-time-checks per user request
          | Bool
needsCheckL Bool -> Bool -> Bool
&& Bool
needsCheckR = Doc -> Doc
cndLkUp Doc
checkBoth
          | Bool
needsCheckL                = Doc -> Doc
cndLkUp Doc
checkLeft
          | Bool
needsCheckR                = Doc -> Doc
cndLkUp Doc
checkRight
          | Bool
True                       = Doc
lkUp
          where [Doc
index, Doc
defVal] = (SV -> Doc) -> [SV] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (CgConfig -> [(SV, CV)] -> SV -> Doc
showSV CgConfig
cfg [(SV, CV)]
consts) [SV
ind, SV
def]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

{- HLint ignore module "Redundant lambda" -}