-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Compilers.CodeGen
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Code generation utilities
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                        #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Compilers.CodeGen (
        -- * The codegen monad
          SBVCodeGen(..), cgSym

        -- * Specifying inputs, SBV variants
        , cgInput,  cgInputArr
        , cgOutput, cgOutputArr
        , cgReturn, cgReturnArr

        -- * Specifying inputs, SVal variants
        , svCgInput,  svCgInputArr
        , svCgOutput, svCgOutputArr
        , svCgReturn, svCgReturnArr

        -- * Settings
        , cgPerformRTCs, cgSetDriverValues
        , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles, cgShowU8UsingHex
        , cgIntegerSize, cgSRealType, CgSRealType(..)

        -- * Infrastructure
        , CgTarget(..), CgConfig(..), CgState(..), CgPgmBundle(..), CgPgmKind(..), CgVal(..)
        , defaultCgConfig, initCgState, isCgDriver, isCgMakefile

        -- * Generating collateral
        , cgGenerateDriver, cgGenerateMakefile, codeGen, renderCgPgmBundle
        ) where

import Control.Monad             (filterM, replicateM, unless)
import Control.Monad.Trans       (MonadIO(liftIO), lift)
import Control.Monad.State.Lazy  (MonadState, StateT(..), modify')
import Data.Char                 (toLower, isSpace)
import Data.List                 (nub, isPrefixOf, intercalate, (\\))
import System.Directory          (createDirectoryIfMissing, doesDirectoryExist, doesFileExist)
import System.FilePath           ((</>))
import System.IO                 (hFlush, stdout)

import           Text.PrettyPrint.HughesPJ      (Doc, vcat)
import qualified Text.PrettyPrint.HughesPJ as P (render)

import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (MonadSymbolic(..), svToSymSV, svMkSymVar, outputSVal)

#if MIN_VERSION_base(4,11,0)
import Control.Monad.Fail as Fail
#endif

-- | Abstract over code generation for different languages
class CgTarget a where
  targetName :: a -> String
  translate  :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle

-- | Options for code-generation.
data CgConfig = CgConfig {
          CgConfig -> Bool
cgRTC                :: Bool               -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.
        , CgConfig -> Maybe Int
cgInteger            :: Maybe Int          -- ^ Bit-size to use for representing SInteger (if any)
        , CgConfig -> Maybe CgSRealType
cgReal               :: Maybe CgSRealType  -- ^ Type to use for representing SReal (if any)
        , CgConfig -> [Integer]
cgDriverVals         :: [Integer]          -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
        , CgConfig -> Bool
cgGenDriver          :: Bool               -- ^ If 'True', will generate a driver program
        , CgConfig -> Bool
cgGenMakefile        :: Bool               -- ^ If 'True', will generate a makefile
        , CgConfig -> Bool
cgIgnoreAsserts      :: Bool               -- ^ If 'True', will ignore 'Data.SBV.sAssert' calls
        , CgConfig -> Bool
cgOverwriteGenerated :: Bool               -- ^ If 'True', will overwrite the generated files without prompting.
        , CgConfig -> Bool
cgShowU8InHex        :: Bool               -- ^ If 'True', then 8-bit unsigned values will be shown in hex as well, otherwise decimal. (Other types always shown in hex.)
        }

-- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.
defaultCgConfig :: CgConfig
defaultCgConfig :: CgConfig
defaultCgConfig = CgConfig :: Bool
-> Maybe Int
-> Maybe CgSRealType
-> [Integer]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> CgConfig
CgConfig { cgRTC :: Bool
cgRTC                = Bool
False
                           , cgInteger :: Maybe Int
cgInteger            = Maybe Int
forall a. Maybe a
Nothing
                           , cgReal :: Maybe CgSRealType
cgReal               = Maybe CgSRealType
forall a. Maybe a
Nothing
                           , cgDriverVals :: [Integer]
cgDriverVals         = []
                           , cgGenDriver :: Bool
cgGenDriver          = Bool
True
                           , cgGenMakefile :: Bool
cgGenMakefile        = Bool
True
                           , cgIgnoreAsserts :: Bool
cgIgnoreAsserts      = Bool
False
                           , cgOverwriteGenerated :: Bool
cgOverwriteGenerated = Bool
False
                           , cgShowU8InHex :: Bool
cgShowU8InHex        = Bool
False
                           }

-- | Abstraction of target language values
data CgVal = CgAtomic SV
           | CgArray  [SV]

-- | Code-generation state
data CgState = CgState {
          CgState -> [(String, CgVal)]
cgInputs         :: [(String, CgVal)]
        , CgState -> [(String, CgVal)]
cgOutputs        :: [(String, CgVal)]
        , CgState -> [CgVal]
cgReturns        :: [CgVal]
        , CgState -> [String]
cgPrototypes     :: [String]    -- extra stuff that goes into the header
        , CgState -> [String]
cgDecls          :: [String]    -- extra stuff that goes into the top of the file
        , CgState -> [String]
cgLDFlags        :: [String]    -- extra options that go to the linker
        , CgState -> CgConfig
cgFinalConfig    :: CgConfig
        }

-- | Initial configuration for code-generation
initCgState :: CgState
initCgState :: CgState
initCgState = CgState :: [(String, CgVal)]
-> [(String, CgVal)]
-> [CgVal]
-> [String]
-> [String]
-> [String]
-> CgConfig
-> CgState
CgState {
          cgInputs :: [(String, CgVal)]
cgInputs         = []
        , cgOutputs :: [(String, CgVal)]
cgOutputs        = []
        , cgReturns :: [CgVal]
cgReturns        = []
        , cgPrototypes :: [String]
cgPrototypes     = []
        , cgDecls :: [String]
cgDecls          = []
        , cgLDFlags :: [String]
cgLDFlags        = []
        , cgFinalConfig :: CgConfig
cgFinalConfig    = CgConfig
defaultCgConfig
        }

-- | The code-generation monad. Allows for precise layout of input values
-- reference parameters (for returning composite values in languages such as C),
-- and return values.
newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
                   deriving ( Functor SBVCodeGen
a -> SBVCodeGen a
Functor SBVCodeGen =>
(forall a. a -> SBVCodeGen a)
-> (forall a b.
    SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b)
-> (forall a b c.
    (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c)
-> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b)
-> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a)
-> Applicative SBVCodeGen
SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
forall a. a -> SBVCodeGen a
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
$c<* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
*> :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
$c*> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
liftA2 :: (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
$cliftA2 :: forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
<*> :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
$c<*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
pure :: a -> SBVCodeGen a
$cpure :: forall a. a -> SBVCodeGen a
$cp1Applicative :: Functor SBVCodeGen
Applicative, a -> SBVCodeGen b -> SBVCodeGen a
(a -> b) -> SBVCodeGen a -> SBVCodeGen b
(forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b)
-> (forall a b. a -> SBVCodeGen b -> SBVCodeGen a)
-> Functor SBVCodeGen
forall a b. a -> SBVCodeGen b -> SBVCodeGen a
forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SBVCodeGen b -> SBVCodeGen a
$c<$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b
$cfmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
Functor, Applicative SBVCodeGen
a -> SBVCodeGen a
Applicative SBVCodeGen =>
(forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b)
-> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b)
-> (forall a. a -> SBVCodeGen a)
-> Monad SBVCodeGen
SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall a. a -> SBVCodeGen a
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> SBVCodeGen a
$creturn :: forall a. a -> SBVCodeGen a
>> :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
$c>> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
>>= :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
$c>>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
$cp1Monad :: Applicative SBVCodeGen
Monad, Monad SBVCodeGen
Monad SBVCodeGen =>
(forall a. IO a -> SBVCodeGen a) -> MonadIO SBVCodeGen
IO a -> SBVCodeGen a
forall a. IO a -> SBVCodeGen a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> SBVCodeGen a
$cliftIO :: forall a. IO a -> SBVCodeGen a
$cp1MonadIO :: Monad SBVCodeGen
MonadIO, MonadState CgState
                            , MonadIO SBVCodeGen
SBVCodeGen State
MonadIO SBVCodeGen => SBVCodeGen State -> MonadSymbolic SBVCodeGen
forall (m :: * -> *). MonadIO m => m State -> MonadSymbolic m
symbolicEnv :: SBVCodeGen State
$csymbolicEnv :: SBVCodeGen State
$cp1MonadSymbolic :: MonadIO SBVCodeGen
MonadSymbolic
#if MIN_VERSION_base(4,11,0)
                            , Monad SBVCodeGen
Monad SBVCodeGen =>
(forall a. String -> SBVCodeGen a) -> MonadFail SBVCodeGen
String -> SBVCodeGen a
forall a. String -> SBVCodeGen a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
fail :: String -> SBVCodeGen a
$cfail :: forall a. String -> SBVCodeGen a
$cp1MonadFail :: Monad SBVCodeGen
Fail.MonadFail
#endif
                            )

-- | Reach into symbolic monad from code-generation
cgSym :: Symbolic a -> SBVCodeGen a
cgSym :: Symbolic a -> SBVCodeGen a
cgSym = StateT CgState Symbolic a -> SBVCodeGen a
forall a. StateT CgState Symbolic a -> SBVCodeGen a
SBVCodeGen (StateT CgState Symbolic a -> SBVCodeGen a)
-> (Symbolic a -> StateT CgState Symbolic a)
-> Symbolic a
-> SBVCodeGen a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbolic a -> StateT CgState Symbolic a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: 'False'.
cgPerformRTCs :: Bool -> SBVCodeGen ()
cgPerformRTCs :: Bool -> SBVCodeGen ()
cgPerformRTCs b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgRTC :: Bool
cgRTC = Bool
b } })

-- | Sets number of bits to be used for representing the 'SInteger' type in the generated C code.
-- The argument must be one of @8@, @16@, @32@, or @64@. Note that this is essentially unsafe as
-- the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as
-- typical in most C implementations.
cgIntegerSize :: Int -> SBVCodeGen ()
cgIntegerSize :: Int -> SBVCodeGen ()
cgIntegerSize i :: Int
i
  | Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [8, 16, 32, 64]
  = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
True
  = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgInteger :: Maybe Int
cgInteger = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i }})

-- | Possible mappings for the 'SReal' type when translated to C. Used in conjunction
-- with the function 'cgSRealType'. Note that the particular characteristics of the
-- mapped types depend on the platform and the compiler used for compiling the generated
-- C program. See <http://en.wikipedia.org/wiki/C_data_types> for details.
data CgSRealType = CgFloat      -- ^ @float@
                 | CgDouble     -- ^ @double@
                 | CgLongDouble -- ^ @long double@
                 deriving CgSRealType -> CgSRealType -> Bool
(CgSRealType -> CgSRealType -> Bool)
-> (CgSRealType -> CgSRealType -> Bool) -> Eq CgSRealType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CgSRealType -> CgSRealType -> Bool
$c/= :: CgSRealType -> CgSRealType -> Bool
== :: CgSRealType -> CgSRealType -> Bool
$c== :: CgSRealType -> CgSRealType -> Bool
Eq

-- 'Show' instance for 'cgSRealType' displays values as they would be used in a C program
instance Show CgSRealType where
  show :: CgSRealType -> String
show CgFloat      = "float"
  show CgDouble     = "double"
  show CgLongDouble = "long double"

-- | Sets the C type to be used for representing the 'SReal' type in the generated C code.
-- The setting can be one of C's @"float"@, @"double"@, or @"long double"@, types, depending
-- on the precision needed. Note that this is essentially unsafe as the semantics of
-- infinite precision SReal values becomes reduced to the corresponding floating point type in
-- C, and hence it is subject to rounding errors.
cgSRealType :: CgSRealType -> SBVCodeGen ()
cgSRealType :: CgSRealType -> SBVCodeGen ()
cgSRealType rt :: CgSRealType
rt = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s {cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgReal :: Maybe CgSRealType
cgReal = CgSRealType -> Maybe CgSRealType
forall a. a -> Maybe a
Just CgSRealType
rt }})

-- | Should we generate a driver program? Default: 'True'. When a library is generated, it will have
-- a driver if any of the contituent functions has a driver. (See 'Data.SBV.Tools.CodeGen.compileToCLib'.)
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgGenDriver :: Bool
cgGenDriver = Bool
b } })

-- | Should we generate a Makefile? Default: 'True'.
cgGenerateMakefile :: Bool -> SBVCodeGen ()
cgGenerateMakefile :: Bool -> SBVCodeGen ()
cgGenerateMakefile b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgGenMakefile :: Bool
cgGenMakefile = Bool
b } })

-- | Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues vs :: [Integer]
vs = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgDriverVals :: [Integer]
cgDriverVals = [Integer]
vs } })

-- | Ignore assertions (those generated by 'Data.SBV.sAssert' calls) in the generated C code
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
cgIgnoreSAssert b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgIgnoreAsserts :: Bool
cgIgnoreAsserts = Bool
b } })

-- | Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
cgAddPrototype :: [String] -> SBVCodeGen ()
cgAddPrototype :: [String] -> SBVCodeGen ()
cgAddPrototype ss :: [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> let old :: [String]
old = CgState -> [String]
cgPrototypes CgState
s
                                       new :: [String]
new = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
old then [String]
ss else [String]
old [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [""] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ss
                                   in CgState
s { cgPrototypes :: [String]
cgPrototypes = [String]
new })

-- | If passed 'True', then we will not ask the user if we're overwriting files as we generate
-- the C code. Otherwise, we'll prompt.
cgOverwriteFiles :: Bool -> SBVCodeGen ()
cgOverwriteFiles :: Bool -> SBVCodeGen ()
cgOverwriteFiles b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgOverwriteGenerated :: Bool
cgOverwriteGenerated = Bool
b } })

-- | If passed 'True', then we will show 'SWord 8' type in hex. Otherwise we'll show it in decimal. All signed
-- types are shown decimal, and all unsigned larger types are shown hexadecimal otherwise.
cgShowU8UsingHex :: Bool -> SBVCodeGen ()
cgShowU8UsingHex :: Bool -> SBVCodeGen ()
cgShowU8UsingHex b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgShowU8InHex :: Bool
cgShowU8InHex = Bool
b } })


-- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl ss :: [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgDecls :: [String]
cgDecls = CgState -> [String]
cgDecls CgState
s [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ss })

-- | Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.
cgAddLDFlags :: [String] -> SBVCodeGen ()
cgAddLDFlags :: [String] -> SBVCodeGen ()
cgAddLDFlags ss :: [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgLDFlags :: [String]
cgLDFlags = CgState -> [String]
cgLDFlags CgState
s [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ss })

-- | Creates an atomic input in the generated code.
svCgInput :: Kind -> String -> SBVCodeGen SVal
svCgInput :: Kind -> String -> SBVCodeGen SVal
svCgInput k :: Kind
k nm :: String
nm = do SVal
r  <- SBVCodeGen State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SBVCodeGen State -> (State -> SBVCodeGen SVal) -> SBVCodeGen SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> SBVCodeGen SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> SBVCodeGen SVal)
-> (State -> IO SVal) -> State -> SBVCodeGen SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Kind
k Maybe String
forall a. Maybe a
Nothing
                    SV
sv <- SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
r
                    (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
                    SVal -> SBVCodeGen SVal
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
r

-- | Creates an array input in the generated code.
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
svCgInputArr k :: Kind
k sz :: Int
sz nm :: String
nm
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen [SVal]
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen [SVal]) -> String -> SBVCodeGen [SVal]
forall a b. (a -> b) -> a -> b
$ "SBV.cgInputArr: Array inputs must have at least one element, given " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
  | Bool
True   = do [SVal]
rs  <- SBVCodeGen State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SBVCodeGen State
-> (State -> SBVCodeGen [SVal]) -> SBVCodeGen [SVal]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO [SVal] -> SBVCodeGen [SVal]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [SVal] -> SBVCodeGen [SVal])
-> (State -> IO [SVal]) -> State -> SBVCodeGen [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IO SVal -> IO [SVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
sz (IO SVal -> IO [SVal]) -> (State -> IO SVal) -> State -> IO [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Kind
k Maybe String
forall a. Maybe a
Nothing
                [SV]
sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
rs
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
                [SVal] -> SBVCodeGen [SVal]
forall (m :: * -> *) a. Monad m => a -> m a
return [SVal]
rs

-- | Creates an atomic output in the generated code.
svCgOutput :: String -> SVal -> SBVCodeGen ()
svCgOutput :: String -> SVal -> SBVCodeGen ()
svCgOutput nm :: String
nm v :: SVal
v = do ()
_ <- SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal SVal
v
                     SV
sv <- SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
v
                     (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })

-- | Creates an array output in the generated code.
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
svCgOutputArr nm :: String
nm vs :: [SVal]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgOutputArr: Array outputs must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
  | Bool
True   = do (SVal -> SBVCodeGen ()) -> [SVal] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal [SVal]
vs
                [SV]
sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
vs
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })
  where sz :: Int
sz = [SVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
vs

-- | Creates a returned (unnamed) value in the generated code.
svCgReturn :: SVal -> SBVCodeGen ()
svCgReturn :: SVal -> SBVCodeGen ()
svCgReturn v :: SVal
v = do ()
_ <- SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal SVal
v
                  SV
sv <- SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
v
                  (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = SV -> CgVal
CgAtomic SV
sv CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })

-- | Creates a returned (unnamed) array value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr vs :: [SVal]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgReturnArr: Array returns must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz
  | Bool
True   = do (SVal -> SBVCodeGen ()) -> [SVal] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal [SVal]
vs
                [SV]
sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
vs
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = [SV] -> CgVal
CgArray [SV]
sws CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
  where sz :: Int
sz = [SVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
vs

-- | Creates an atomic input in the generated code.
cgInput :: SymVal a => String -> SBVCodeGen (SBV a)
cgInput :: String -> SBVCodeGen (SBV a)
cgInput nm :: String
nm = do SBV a
r <- SBVCodeGen (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_
                SV
sv <- SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
r
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
                SBV a -> SBVCodeGen (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV a
r

-- | Creates an array input in the generated code.
cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr :: Int -> String -> SBVCodeGen [SBV a]
cgInputArr sz :: Int
sz nm :: String
nm
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen [SBV a]
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen [SBV a]) -> String -> SBVCodeGen [SBV a]
forall a b. (a -> b) -> a -> b
$ "SBV.cgInputArr: Array inputs must have at least one element, given " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
  | Bool
True   = do [SBV a]
rs <- (Int -> SBVCodeGen (SBV a)) -> [Int] -> SBVCodeGen [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SBVCodeGen (SBV a) -> Int -> SBVCodeGen (SBV a)
forall a b. a -> b -> a
const SBVCodeGen (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_) [1..Int
sz]
                [SV]
sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
rs
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
                [SBV a] -> SBVCodeGen [SBV a]
forall (m :: * -> *) a. Monad m => a -> m a
return [SBV a]
rs

-- | Creates an atomic output in the generated code.
cgOutput :: String -> SBV a -> SBVCodeGen ()
cgOutput :: String -> SBV a -> SBVCodeGen ()
cgOutput nm :: String
nm v :: SBV a
v = do SBV a
_ <- SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v
                   SV
sv <- SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
v
                   (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })

-- | Creates an array output in the generated code.
cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
cgOutputArr :: String -> [SBV a] -> SBVCodeGen ()
cgOutputArr nm :: String
nm vs :: [SBV a]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgOutputArr: Array outputs must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
  | Bool
True   = do (SBV a -> SBVCodeGen (SBV a)) -> [SBV a] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs
                [SV]
sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
vs
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })
  where sz :: Int
sz = [SBV a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV a]
vs

-- | Creates a returned (unnamed) value in the generated code.
cgReturn :: SBV a -> SBVCodeGen ()
cgReturn :: SBV a -> SBVCodeGen ()
cgReturn v :: SBV a
v = do SBV a
_ <- SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v
                SV
sv <- SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
v
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = SV -> CgVal
CgAtomic SV
sv CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })

-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
cgReturnArr :: [SBV a] -> SBVCodeGen ()
cgReturnArr vs :: [SBV a]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgReturnArr: Array returns must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz
  | Bool
True   = do (SBV a -> SBVCodeGen (SBV a)) -> [SBV a] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs
                [SV]
sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
vs
                (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = [SV] -> CgVal
CgArray [SV]
sws CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
  where sz :: Int
sz = [SBV a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV a]
vs

-- | Representation of a collection of generated programs.
data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]

-- | Different kinds of "files" we can produce. Currently this is quite "C" specific.
data CgPgmKind = CgMakefile [String]  -- list of flags to pass to linker
               | CgHeader [Doc]
               | CgSource
               | CgDriver

-- | Is this a driver program?
isCgDriver :: CgPgmKind -> Bool
isCgDriver :: CgPgmKind -> Bool
isCgDriver CgDriver = Bool
True
isCgDriver _        = Bool
False

-- | Is this a make file?
isCgMakefile :: CgPgmKind -> Bool
isCgMakefile :: CgPgmKind -> Bool
isCgMakefile CgMakefile{} = Bool
True
isCgMakefile _            = Bool
False

-- A simple way to print bundles, mostly for debugging purposes.
instance Show CgPgmBundle where
   show :: CgPgmBundle -> String
show (CgPgmBundle _ fs :: [(String, (CgPgmKind, [Doc]))]
fs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, (CgPgmKind, [Doc])) -> String)
-> [(String, (CgPgmKind, [Doc]))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, (CgPgmKind, [Doc])) -> String
showFile [(String, (CgPgmKind, [Doc]))]
fs
    where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
          showFile :: (String, (CgPgmKind, [Doc])) -> String
showFile (f :: String
f, (_, ds :: [Doc]
ds)) =  "== BEGIN: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ================\n"
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render' ([Doc] -> Doc
vcat [Doc]
ds)
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ "== END: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " =================="

-- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection
-- of makefiles, source code, headers, etc.
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
codeGen :: l
-> CgConfig
-> String
-> SBVCodeGen a
-> IO (a, CgConfig, CgPgmBundle)
codeGen l :: l
l cgConfig :: CgConfig
cgConfig nm :: String
nm (SBVCodeGen comp :: StateT CgState Symbolic a
comp) = do
   ((retVal :: a
retVal, st' :: CgState
st'), res :: Result
res) <- SBVRunMode
-> SymbolicT IO (a, CgState) -> IO ((a, CgState), Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic SBVRunMode
CodeGen (SymbolicT IO (a, CgState) -> IO ((a, CgState), Result))
-> SymbolicT IO (a, CgState) -> IO ((a, CgState), Result)
forall a b. (a -> b) -> a -> b
$ StateT CgState Symbolic a -> CgState -> SymbolicT IO (a, CgState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT CgState Symbolic a
comp CgState
initCgState { cgFinalConfig :: CgConfig
cgFinalConfig = CgConfig
cgConfig }
   let st :: CgState
st = CgState
st' { cgInputs :: [(String, CgVal)]
cgInputs       = [(String, CgVal)] -> [(String, CgVal)]
forall a. [a] -> [a]
reverse (CgState -> [(String, CgVal)]
cgInputs CgState
st')
                , cgOutputs :: [(String, CgVal)]
cgOutputs      = [(String, CgVal)] -> [(String, CgVal)]
forall a. [a] -> [a]
reverse (CgState -> [(String, CgVal)]
cgOutputs CgState
st')
                }
       allNamedVars :: [String]
allNamedVars = ((String, CgVal) -> String) -> [(String, CgVal)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, CgVal) -> String
forall a b. (a, b) -> a
fst (CgState -> [(String, CgVal)]
cgInputs CgState
st [(String, CgVal)] -> [(String, CgVal)] -> [(String, CgVal)]
forall a. [a] -> [a] -> [a]
++ CgState -> [(String, CgVal)]
cgOutputs CgState
st)
       dupNames :: [String]
dupNames = [String]
allNamedVars [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String]
allNamedVars
   Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dupNames) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "SBV.codeGen: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " has following argument names duplicated: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
dupNames

   (a, CgConfig, CgPgmBundle) -> IO (a, CgConfig, CgPgmBundle)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
retVal, CgState -> CgConfig
cgFinalConfig CgState
st, l -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
forall a.
CgTarget a =>
a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
translate l
l (CgState -> CgConfig
cgFinalConfig CgState
st) String
nm CgState
st Result
res)

-- | Render a code-gen bundle to a directory or to stdout
renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
renderCgPgmBundle :: Maybe String -> (CgConfig, CgPgmBundle) -> IO ()
renderCgPgmBundle Nothing        (_  , bundle :: CgPgmBundle
bundle)              = CgPgmBundle -> IO ()
forall a. Show a => a -> IO ()
print CgPgmBundle
bundle
renderCgPgmBundle (Just dirName :: String
dirName) (cfg :: CgConfig
cfg, CgPgmBundle _ files :: [(String, (CgPgmKind, [Doc]))]
files) = do

        Bool
b <- String -> IO Bool
doesDirectoryExist String
dirName
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Creating directory " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
dirName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".."
                      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dirName

        [String]
dups <- (String -> IO Bool) -> [String] -> IO [String]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\fn :: String
fn -> String -> IO Bool
doesFileExist (String
dirName String -> String -> String
</> String
fn)) (((String, (CgPgmKind, [Doc])) -> String)
-> [(String, (CgPgmKind, [Doc]))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, (CgPgmKind, [Doc])) -> String
forall a b. (a, b) -> a
fst [(String, (CgPgmKind, [Doc]))]
files)

        Bool
goOn <- case (Bool
overWrite, [String]
dups) of
                  (True, _) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                  (_,   []) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                  _         -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Code generation would overwrite the following " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
dups Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then "file:" else "files:")
                                  (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\fn :: String
fn -> String -> IO ()
putStrLn ('\t' Char -> String -> String
forall a. a -> [a] -> [a]
: String
fn)) [String]
dups
                                  String -> IO ()
putStr "Continue? [yn] "
                                  Handle -> IO ()
hFlush Handle
stdout
                                  String
resp <- IO String
getLine
                                  Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
resp String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` "yes"

        if Bool
goOn then do ((String, (CgPgmKind, [Doc])) -> IO ())
-> [(String, (CgPgmKind, [Doc]))] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String, (CgPgmKind, [Doc])) -> IO ()
forall a. (String, (a, [Doc])) -> IO ()
renderFile [(String, (CgPgmKind, [Doc]))]
files
                        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn "Done."
                else String -> IO ()
putStrLn "Aborting."

  where overWrite :: Bool
overWrite = CgConfig -> Bool
cgOverwriteGenerated CgConfig
cfg

        renderFile :: (String, (a, [Doc])) -> IO ()
renderFile (f :: String
f, (_, ds :: [Doc]
ds)) = do let fn :: String
fn = String
dirName String -> String -> String
</> String
f
                                     Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Generating: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".."
                                     String -> String -> IO ()
writeFile String
fn (Doc -> String
render' ([Doc] -> Doc
vcat [Doc]
ds))

-- | An alternative to Pretty's @render@, which might have "leading" white-space in empty lines. This version
-- eliminates such whitespace.
render' :: Doc -> String
render' :: Doc -> String
render' = [String] -> String
unlines ([String] -> String) -> (Doc -> [String]) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
clean ([String] -> [String]) -> (Doc -> [String]) -> Doc -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> [String]) -> (Doc -> String) -> Doc -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
P.render
  where clean :: String -> String
clean x :: String
x | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
x = ""
                | Bool
True          = String
x