-----------------------------------------------------------------------------
-- |
-- 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, VarContext(..))

#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 Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 Int
i
  | Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int
8, Int
16, Int
32, Int
64]
  = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ String
"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' (\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 CgSRealType
CgFloat      = String
"float"
  show CgSRealType
CgDouble     = String
"double"
  show CgSRealType
CgLongDouble = String
"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 CgSRealType
rt = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 constituent functions has a driver. (See 'Data.SBV.Tools.CodeGen.compileToCLib'.)
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 [Integer]
vs = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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] -> [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 Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\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 Kind
k 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
. VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Maybe Quantifier -> VarContext
NonQueryVar (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' (\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 Kind
k Int
sz String
nm
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = String -> SBVCodeGen [SVal]
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen [SVal]) -> String -> SBVCodeGen [SVal]
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" 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
. VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Maybe Quantifier -> VarContext
NonQueryVar (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' (\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 String
nm 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' (\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 String
nm [SVal]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" 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' (\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 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' (\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 [SVal]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ String
"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' (\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 String
nm = do SBV a
r <- SBVCodeGen (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_
                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' (\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 Int
sz String
nm
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
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
$ String
"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]
++ String
" 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)
sbvForall_) [Int
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' (\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 String
nm 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' (\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 String
nm [SBV a]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
" 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' (\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 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' (\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 [SBV a]
vs
  | Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ String
"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' (\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 CgPgmKind
CgDriver = Bool
True
isCgDriver CgPgmKind
_        = Bool
False

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

-- A simple way to print bundles, mostly for debugging purposes.
instance Show CgPgmBundle where
   show :: CgPgmBundle -> String
show (CgPgmBundle (Maybe Int, Maybe CgSRealType)
_ [(String, (CgPgmKind, [Doc]))]
fs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\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 (String
f, (CgPgmKind
_, [Doc]
ds)) =  String
"== 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]
++ String
" ================\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]
++ String
"== 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]
++ String
" =================="

-- | 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 CgConfig
cgConfig String
nm (SBVCodeGen StateT CgState Symbolic a
comp) = do
   ((a
retVal, CgState
st'), 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
$ String
"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]
++ String
" 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 Maybe String
Nothing        (CgConfig
_  , CgPgmBundle
bundle)              = CgPgmBundle -> IO ()
forall a. Show a => a -> IO ()
print CgPgmBundle
bundle
renderCgPgmBundle (Just String
dirName) (CgConfig
cfg, CgPgmBundle (Maybe Int, Maybe CgSRealType)
_ [(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
$ String
"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]
++ String
".."
                      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 (\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
                  (Bool
True, [String]
_) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                  (Bool
_,   []) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                  (Bool, [String])
_         -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"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
== Int
1 then String
"file:" else String
"files:")
                                  (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\String
fn -> String -> IO ()
putStrLn (Char
'\t' Char -> String -> String
forall a. a -> [a] -> [a]
: String
fn)) [String]
dups
                                  String -> IO ()
putStr String
"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` String
"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 String
"Done."
                else String -> IO ()
putStrLn String
"Aborting."

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

        renderFile :: (String, (a, [Doc])) -> IO ()
renderFile (String
f, (a
_, [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
$ String
"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 -> 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 String
x | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
x = String
""
                | Bool
True          = String
x