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

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

{-# OPTIONS_GHC -Wall -Werror #-}

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

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

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

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

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

import GHC.Stack

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

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

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

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

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

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

-- token for the target language
data SBVToC = SBVToC

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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