-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Lambda
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Generating lambda-expressions, constraints, and named functions, for (limited)
-- higher-order function support in SBV.
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Lambda (
            lambda,      lambdaStr
          , namedLambda, namedLambdaStr
          , constraint,  constraintStr
        ) where

import Control.Monad       (join)
import Control.Monad.Trans (liftIO, MonadIO)

import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.SMT.SMTLib2
import Data.SBV.Utils.PrettyNum

import           Data.SBV.Core.Symbolic hiding   (mkNewState, fresh)
import qualified Data.SBV.Core.Symbolic as     S (mkNewState)

import Data.IORef (readIORef, modifyIORef')
import Data.List

import qualified Data.Foldable      as F
import qualified Data.Map.Strict    as M

import qualified Data.Generics.Uniplate.Data as G

data Defn = Defn [String]                        -- The uninterpreted names referred to in the body
                 (Maybe [(Quantifier, String)])  -- Param declaration groups, if any
                 (Int -> String)                 -- Body, given the tab amount.

-- | Maka a new substate from the incoming state, sharing parts as necessary
inSubState :: MonadIO m => State -> (State -> m b) -> m b
inSubState :: forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState State -> m b
comp = do
        Int
ll <- IO Int -> m Int
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> m Int) -> IO Int -> m Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef (State -> IORef Int
rLambdaLevel State
inState)
        State
stEmpty <- SMTConfig -> SBVRunMode -> m State
forall (m :: * -> *).
MonadIO m =>
SMTConfig -> SBVRunMode -> m State
S.mkNewState (State -> SMTConfig
stCfg State
inState) (Int -> SBVRunMode
LambdaGen (Int
ll Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

        let share :: (State -> t) -> t
share State -> t
fld = State -> t
fld State
inState   -- reuse the field from the parent-context
            fresh :: (State -> t) -> t
fresh State -> t
fld = State -> t
fld State
stEmpty   -- create a new field here

        -- freshen certain fields, sharing some from the parent, and run the comp
        -- Here's the guidance:
        --
        --    * Anything that's "shared" updates the calling context. It better be the case
        --      that the caller can handle that info.
        --    * Anything that's "fresh" will be used in this substate, and will be forgotten.
        --      It better be the case that in "toLambda" below, you do something with it.
        --
        -- Note the above applies to all the IORefs, which is most of the state, though
        -- not all. For the time being, those are pathCond, stCfg, and startTime; which
        -- don't really impact anything.
        State -> m b
comp State {
                   -- These are not IORefs; so we share by copying  the value; changes won't be copied back
                     sbvContext :: SBVContext
sbvContext          = (State -> SBVContext) -> SBVContext
forall {t}. (State -> t) -> t
share State -> SBVContext
sbvContext
                   , pathCond :: SVal
pathCond            = (State -> SVal) -> SVal
forall {t}. (State -> t) -> t
share State -> SVal
pathCond
                   , startTime :: UTCTime
startTime           = (State -> UTCTime) -> UTCTime
forall {t}. (State -> t) -> t
share State -> UTCTime
startTime

                   -- These are shared IORef's; and is shared, so they will be copied back to the parent state
                   , rProgInfo :: IORef ProgInfo
rProgInfo           = (State -> IORef ProgInfo) -> IORef ProgInfo
forall {t}. (State -> t) -> t
share State -> IORef ProgInfo
rProgInfo
                   , rIncState :: IORef IncState
rIncState           = (State -> IORef IncState) -> IORef IncState
forall {t}. (State -> t) -> t
share State -> IORef IncState
rIncState
                   , rCInfo :: IORef [(String, CV)]
rCInfo              = (State -> IORef [(String, CV)]) -> IORef [(String, CV)]
forall {t}. (State -> t) -> t
share State -> IORef [(String, CV)]
rCInfo
                   , rUsedKinds :: IORef KindSet
rUsedKinds          = (State -> IORef KindSet) -> IORef KindSet
forall {t}. (State -> t) -> t
share State -> IORef KindSet
rUsedKinds
                   , rUsedLbls :: IORef (Set String)
rUsedLbls           = (State -> IORef (Set String)) -> IORef (Set String)
forall {t}. (State -> t) -> t
share State -> IORef (Set String)
rUsedLbls
                   , rUIMap :: IORef UIMap
rUIMap              = (State -> IORef UIMap) -> IORef UIMap
forall {t}. (State -> t) -> t
share State -> IORef UIMap
rUIMap
                   , rUserFuncs :: IORef (Set String)
rUserFuncs          = (State -> IORef (Set String)) -> IORef (Set String)
forall {t}. (State -> t) -> t
share State -> IORef (Set String)
rUserFuncs
                   , rCgMap :: IORef CgMap
rCgMap              = (State -> IORef CgMap) -> IORef CgMap
forall {t}. (State -> t) -> t
share State -> IORef CgMap
rCgMap
                   , rDefns :: IORef [(SMTDef, SBVType)]
rDefns              = (State -> IORef [(SMTDef, SBVType)]) -> IORef [(SMTDef, SBVType)]
forall {t}. (State -> t) -> t
share State -> IORef [(SMTDef, SBVType)]
rDefns
                   , rSMTOptions :: IORef [SMTOption]
rSMTOptions         = (State -> IORef [SMTOption]) -> IORef [SMTOption]
forall {t}. (State -> t) -> t
share State -> IORef [SMTOption]
rSMTOptions
                   , rOptGoals :: IORef [Objective (SV, SV)]
rOptGoals           = (State -> IORef [Objective (SV, SV)]) -> IORef [Objective (SV, SV)]
forall {t}. (State -> t) -> t
share State -> IORef [Objective (SV, SV)]
rOptGoals
                   , rAsserts :: IORef [(String, Maybe CallStack, SV)]
rAsserts            = (State -> IORef [(String, Maybe CallStack, SV)])
-> IORef [(String, Maybe CallStack, SV)]
forall {t}. (State -> t) -> t
share State -> IORef [(String, Maybe CallStack, SV)]
rAsserts
                   , rOutstandingAsserts :: IORef Bool
rOutstandingAsserts = (State -> IORef Bool) -> IORef Bool
forall {t}. (State -> t) -> t
share State -> IORef Bool
rOutstandingAsserts
                   , rPartitionVars :: IORef [String]
rPartitionVars      = (State -> IORef [String]) -> IORef [String]
forall {t}. (State -> t) -> t
share State -> IORef [String]
rPartitionVars

                   -- Everything else is fresh in the substate; i.e., will not copy back
                   , stCfg :: SMTConfig
stCfg               = (State -> SMTConfig) -> SMTConfig
forall {t}. (State -> t) -> t
fresh State -> SMTConfig
stCfg
                   , runMode :: IORef SBVRunMode
runMode             = (State -> IORef SBVRunMode) -> IORef SBVRunMode
forall {t}. (State -> t) -> t
fresh State -> IORef SBVRunMode
runMode
                   , rctr :: IORef Int
rctr                = (State -> IORef Int) -> IORef Int
forall {t}. (State -> t) -> t
fresh State -> IORef Int
rctr
                   , rLambdaLevel :: IORef Int
rLambdaLevel        = (State -> IORef Int) -> IORef Int
forall {t}. (State -> t) -> t
fresh State -> IORef Int
rLambdaLevel
                   , rtblMap :: IORef TableMap
rtblMap             = (State -> IORef TableMap) -> IORef TableMap
forall {t}. (State -> t) -> t
fresh State -> IORef TableMap
rtblMap
                   , rArrayMap :: IORef ArrayMap
rArrayMap           = (State -> IORef ArrayMap) -> IORef ArrayMap
forall {t}. (State -> t) -> t
fresh State -> IORef ArrayMap
rArrayMap
                   , rAICache :: IORef (Cache ArrayIndex)
rAICache            = (State -> IORef (Cache ArrayIndex)) -> IORef (Cache ArrayIndex)
forall {t}. (State -> t) -> t
fresh State -> IORef (Cache ArrayIndex)
rAICache
                   , rinps :: IORef Inputs
rinps               = (State -> IORef Inputs) -> IORef Inputs
forall {t}. (State -> t) -> t
fresh State -> IORef Inputs
rinps
                   , rlambdaInps :: IORef LambdaInputs
rlambdaInps         = (State -> IORef LambdaInputs) -> IORef LambdaInputs
forall {t}. (State -> t) -> t
fresh State -> IORef LambdaInputs
rlambdaInps
                   , rConstraints :: IORef (Seq (Bool, [(String, String)], SV))
rConstraints        = (State -> IORef (Seq (Bool, [(String, String)], SV)))
-> IORef (Seq (Bool, [(String, String)], SV))
forall {t}. (State -> t) -> t
fresh State -> IORef (Seq (Bool, [(String, String)], SV))
rConstraints
                   , rObservables :: IORef (Seq (Name, CV -> Bool, SV))
rObservables        = (State -> IORef (Seq (Name, CV -> Bool, SV)))
-> IORef (Seq (Name, CV -> Bool, SV))
forall {t}. (State -> t) -> t
fresh State -> IORef (Seq (Name, CV -> Bool, SV))
rObservables
                   , routs :: IORef [SV]
routs               = (State -> IORef [SV]) -> IORef [SV]
forall {t}. (State -> t) -> t
fresh State -> IORef [SV]
routs
                   , spgm :: IORef SBVPgm
spgm                = (State -> IORef SBVPgm) -> IORef SBVPgm
forall {t}. (State -> t) -> t
fresh State -> IORef SBVPgm
spgm
                   , rconstMap :: IORef CnstMap
rconstMap           = (State -> IORef CnstMap) -> IORef CnstMap
forall {t}. (State -> t) -> t
fresh State -> IORef CnstMap
rconstMap
                   , rexprMap :: IORef ExprMap
rexprMap            = (State -> IORef ExprMap) -> IORef ExprMap
forall {t}. (State -> t) -> t
fresh State -> IORef ExprMap
rexprMap
                   , rSVCache :: IORef (Cache SV)
rSVCache            = (State -> IORef (Cache SV)) -> IORef (Cache SV)
forall {t}. (State -> t) -> t
fresh State -> IORef (Cache SV)
rSVCache
                   , rQueryState :: IORef (Maybe QueryState)
rQueryState         = (State -> IORef (Maybe QueryState)) -> IORef (Maybe QueryState)
forall {t}. (State -> t) -> t
fresh State -> IORef (Maybe QueryState)
rQueryState

                   -- keep track of our parent
                   , parentState :: Maybe State
parentState         = State -> Maybe State
forall a. a -> Maybe a
Just State
inState
                   }

-- In this case, we expect just one group of parameters, with universal quantification
extractAllUniversals :: [(Quantifier, String)] -> String
extractAllUniversals :: [(Quantifier, String)] -> String
extractAllUniversals [(Quantifier
ALL, String
s)] = String
s
extractAllUniversals [(Quantifier, String)]
other      = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                  , String
"*** Data.SBV.Lambda: Impossible happened. Got existential quantifiers."
                                                  , String
"***"
                                                  , String
"***  Params: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Quantifier, String)] -> String
forall a. Show a => a -> String
show [(Quantifier, String)]
other
                                                  , String
"***"
                                                  , String
"*** Please report this as a bug!"
                                                  ]


-- | Generic creator for anonymous lamdas.
lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b
lambdaGen :: forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
lambdaGen Defn -> b
trans State
inState Kind
fk a
f = State -> (State -> m b) -> m b
forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
trans (Defn -> b) -> m Defn -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> Kind -> SymbolicT m () -> m Defn
forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
fk (State -> a -> SymbolicT m ()
forall (m :: * -> *) a. Lambda m a => State -> a -> m ()
mkLambda State
st a
f)

-- | Create an SMTLib lambda, in the given state.
lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTDef
lambda :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m SMTDef
lambda State
inState Kind
fk = (Defn -> SMTDef) -> State -> Kind -> a -> m SMTDef
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
lambdaGen Defn -> SMTDef
mkLam State
inState Kind
fk
   where mkLam :: Defn -> SMTDef
mkLam (Defn [String]
frees Maybe [(Quantifier, String)]
params Int -> String
body) = Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTLam Kind
fk [String]
frees ([(Quantifier, String)] -> String
extractAllUniversals ([(Quantifier, String)] -> String)
-> Maybe [(Quantifier, String)] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(Quantifier, String)]
params) Int -> String
body

-- | Create an anonymous lambda, rendered as n SMTLib string
lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m String
lambdaStr :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m String
lambdaStr = (Defn -> String) -> State -> Kind -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
lambdaGen Defn -> String
mkLam
   where mkLam :: Defn -> String
mkLam (Defn [String]
_frees Maybe [(Quantifier, String)]
Nothing       Int -> String
body) = Int -> String
body Int
0
         mkLam (Defn [String]
_frees (Just [(Quantifier, String)]
params) Int -> String
body) = String
"(lambda " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Quantifier, String)] -> String
extractAllUniversals [(Quantifier, String)]
params String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
body Int
2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Generaic creator for named functions,
namedLambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen :: forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen Defn -> b
trans State
inState Kind
fk a
f = State -> (State -> m b) -> m b
forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
trans (Defn -> b) -> m Defn -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> Kind -> SymbolicT m () -> m Defn
forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
fk (State -> a -> SymbolicT m ()
forall (m :: * -> *) a. Lambda m a => State -> a -> m ()
mkLambda State
st a
f)

-- | Create a named SMTLib function, in the given state.
namedLambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> Kind -> a -> m SMTDef
namedLambda :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> String -> Kind -> a -> m SMTDef
namedLambda State
inState String
nm Kind
fk = (Defn -> SMTDef) -> State -> Kind -> a -> m SMTDef
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen Defn -> SMTDef
mkDef State
inState Kind
fk
   where mkDef :: Defn -> SMTDef
mkDef (Defn [String]
frees Maybe [(Quantifier, String)]
params Int -> String
body) = String
-> Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTDef String
nm Kind
fk [String]
frees ([(Quantifier, String)] -> String
extractAllUniversals ([(Quantifier, String)] -> String)
-> Maybe [(Quantifier, String)] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(Quantifier, String)]
params) Int -> String
body

-- | Create a named SMTLib function, in the given state, string version
namedLambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> SBVType -> a -> m String
namedLambdaStr :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> String -> SBVType -> a -> m String
namedLambdaStr State
inState String
nm SBVType
t = (Defn -> String) -> State -> Kind -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen Defn -> String
mkDef State
inState Kind
fk
   where mkDef :: Defn -> String
mkDef (Defn [String]
frees Maybe [(Quantifier, String)]
params Int -> String
body) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [(SMTDef, SBVType)] -> [String]
declUserFuns [(String
-> Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTDef String
nm Kind
fk [String]
frees ([(Quantifier, String)] -> String
extractAllUniversals ([(Quantifier, String)] -> String)
-> Maybe [(Quantifier, String)] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(Quantifier, String)]
params) Int -> String
body, SBVType
t)]
         fk :: Kind
fk = case SBVType
t of
                SBVType [] -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"namedLambdaStr: Invalid type for " 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
", empty!"
                SBVType [Kind]
xs -> [Kind] -> Kind
forall a. HasCallStack => [a] -> a
last [Kind]
xs

-- | Generic constraint generator.
constraintGen :: (MonadIO m, Constraint (SymbolicT m) a) => ([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen :: forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen [String] -> (Int -> String) -> b
trans inState :: State
inState@State{IORef ProgInfo
rProgInfo :: State -> IORef ProgInfo
rProgInfo :: IORef ProgInfo
rProgInfo} a
f = do
   -- indicate we have quantifiers
   IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef ProgInfo -> (ProgInfo -> ProgInfo) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef ProgInfo
rProgInfo (\ProgInfo
u -> ProgInfo
u{hasQuants = True})

   let mkDef :: Defn -> b
mkDef (Defn [String]
deps Maybe [(Quantifier, String)]
Nothing       Int -> String
body) = [String] -> (Int -> String) -> b
trans [String]
deps Int -> String
body
       mkDef (Defn [String]
deps (Just [(Quantifier, String)]
params) Int -> String
body) = [String] -> (Int -> String) -> b
trans [String]
deps ((Int -> String) -> b) -> (Int -> String) -> b
forall a b. (a -> b) -> a -> b
$ \Int
i -> [String] -> String
unwords (((Quantifier, String) -> String)
-> [(Quantifier, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, String) -> String
mkGroup [(Quantifier, String)]
params) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
                                                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
body (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)
                                                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate ([(Quantifier, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Quantifier, String)]
params) Char
')'
       mkGroup :: (Quantifier, String) -> String
mkGroup (Quantifier
ALL, String
s) = String
"(forall " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
       mkGroup (Quantifier
EX,  String
s) = String
"(exists " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

   State -> (State -> m b) -> m b
forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
mkDef (Defn -> b) -> m Defn -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> Kind -> SymbolicT m () -> m Defn
forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
KBool (State -> a -> SymbolicT m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st a
f SymbolicT m () -> (() -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= () -> SymbolicT m ()
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => () -> m ()
output SymbolicT m () -> SymbolicT m () -> SymbolicT m ()
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> SymbolicT m ()
forall a. a -> SymbolicT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | A constraint can be turned into a boolean
instance Constraint Symbolic a => QuantifiedBool a where
  quantifiedBool :: a -> SBool
quantifiedBool a
qb = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
forall {m :: * -> *}. MonadIO m => State -> m SV
f
    where f :: State -> m SV
f State
st = IO SV -> m SV
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> a -> IO SV
forall (m :: * -> *) a.
(MonadIO m, Constraint (SymbolicT m) a) =>
State -> a -> m SV
constraint State
st a
qb

-- | Generate a constraint.
constraint :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m SV
constraint :: forall (m :: * -> *) a.
(MonadIO m, Constraint (SymbolicT m) a) =>
State -> a -> m SV
constraint State
st = m (m SV) -> m SV
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m SV) -> m SV) -> (a -> m (m SV)) -> a -> m SV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> (Int -> String) -> m SV) -> State -> a -> m (m SV)
forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen [String] -> (Int -> String) -> m SV
forall {m :: * -> *} {t} {p}.
(MonadIO m, Num t) =>
p -> (t -> String) -> m SV
mkSV State
st
   where mkSV :: p -> (t -> String) -> m SV
mkSV p
_deps t -> String
d = IO SV -> m SV
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp (String -> Op
QuantifiedBool (t -> String
d t
0)) [])

-- | Generate a constraint, string version
constraintStr :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m String
constraintStr :: forall (m :: * -> *) a.
(MonadIO m, Constraint (SymbolicT m) a) =>
State -> a -> m String
constraintStr = ([String] -> (Int -> String) -> String) -> State -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen [String] -> (Int -> String) -> String
forall {t}. Num t => [String] -> (t -> String) -> String
toStr
   where toStr :: [String] -> (t -> String) -> String
toStr [String]
deps t -> String
body = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"; user defined axiom: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
depInfo [String]
deps
                                            , String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
body t
2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                            ]

         depInfo :: [String] -> String
depInfo [] = String
""
         depInfo [String]
ds = String
"[Refers to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
ds String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"

-- | Convert to an appropriate SMTLib representation.
convert :: MonadIO m => State -> Kind -> SymbolicT m () -> m Defn
convert :: forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
expectedKind SymbolicT m ()
comp = do
   ((), Result
res)   <- State -> SymbolicT m () -> m ((), Result)
forall (m :: * -> *) a.
MonadIO m =>
State -> SymbolicT m a -> m (a, Result)
runSymbolicInState State
st SymbolicT m ()
comp
   ProgInfo
curProgInfo <- IO ProgInfo -> m ProgInfo
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgInfo -> m ProgInfo) -> IO ProgInfo -> m ProgInfo
forall a b. (a -> b) -> a -> b
$ IORef ProgInfo -> IO ProgInfo
forall a. IORef a -> IO a
readIORef (State -> IORef ProgInfo
rProgInfo State
st)
   Defn -> m Defn
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Defn -> m Defn) -> Defn -> m Defn
forall a b. (a -> b) -> a -> b
$ ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda ProgInfo
curProgInfo (State -> SMTConfig
stCfg State
st) Kind
expectedKind Result
res

-- | Convert the result of a symbolic run to a more abstract representation
toLambda :: ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda :: ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda ProgInfo
curProgInfo SMTConfig
cfg Kind
expectedKind result :: Result
result@Result{resAsgns :: Result -> SBVPgm
resAsgns = SBVPgm Seq (SV, SBVExpr)
asgnsSeq} = Result -> Defn
sh Result
result
 where tbd :: [String] -> a
tbd [String]
xs = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"*** Data.SBV.lambda: Unsupported construct." String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"", String
report])
       bad :: [String] -> a
bad [String]
xs = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"*** Data.SBV.lambda: Impossible happened."   String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"", String
bugReport])
       report :: String
report    = String
"Please request this as a feature at https://github.com/LeventErkok/sbv/issues"
       bugReport :: String
bugReport = String
"Please report this at https://github.com/LeventErkok/sbv/issues"

       sh :: Result -> Defn
sh (Result ProgInfo
_hasQuants    -- Has quantified booleans? Does not apply

                  KindSet
_ki           -- Kind info, we're assuming that all the kinds used are already available in the surrounding context.
                                -- There's no way to create a new kind in a lambda. If a new kind is used, it should be registered.

                  [(String, CV)]
_qcInfo       -- Quickcheck info, does not apply, ignored

                  [(String, CV -> Bool, SV)]
observables   -- Observables: There's no way to display these, so ignore

                  [(String, [String])]
_codeSegs     -- UI code segments: Again, shouldn't happen; if present, error out

                  ResultInp
is            -- Inputs

                  ( CnstMap
_allConsts  -- Not needed, consts are sufficient for this translation
                  , [(SV, CV)]
consts      -- constants used
                  )

                  [((Int, Kind, Kind), [SV])]
tbls          -- Tables

                  [(Int, ArrayInfo)]
_arrs         -- Arrays                : nothing to do with them
                  [(String, (Bool, Maybe [String], SBVType))]
_uis          -- Uninterpeted constants: nothing to do with them
                  [(SMTDef, SBVType)]
_axs          -- Axioms definitions    : nothing to do with them

                  SBVPgm
pgm           -- Assignments

                  Seq (Bool, [(String, String)], SV)
cstrs         -- Additional constraints: Not currently supported inside lambda's
                  [(String, Maybe CallStack, SV)]
assertions    -- Assertions: Not currently supported inside lambda's

                  [SV]
outputs       -- Outputs of the lambda (should be singular)
         )
         | Bool -> Bool
not (Seq (Bool, [(String, String)], SV) -> Bool
forall a. Seq a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Bool, [(String, String)], SV)
cstrs)
         = [String] -> Defn
forall {a}. [String] -> a
tbd [ String
"Constraints."
               , String
"  Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Bool, [(String, String)], SV) -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (Bool, [(String, String)], SV)
cstrs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" additional constraint(s)."
               ]
         | Bool -> Bool
not ([(String, Maybe CallStack, SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, Maybe CallStack, SV)]
assertions)
         = [String] -> Defn
forall {a}. [String] -> a
tbd [ String
"Assertions."
               , String
"  Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String
n | (String
n, Maybe CallStack
_, SV
_) <- [(String, Maybe CallStack, SV)]
assertions]
               ]
         | Bool -> Bool
not ([(String, CV -> Bool, SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, CV -> Bool, SV)]
observables)
         = [String] -> Defn
forall {a}. [String] -> a
tbd [ String
"Observables."
               , String
"  Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String
n | (String
n, CV -> Bool
_, SV
_) <- [(String, CV -> Bool, SV)]
observables]
               ]
         | SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
out Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
expectedKind
         = [String] -> Defn
forall {a}. [String] -> a
bad [ String
"Expected kind and final kind do not match"
               , String
"   Saw     : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
out)
               , String
"   Expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
expectedKind
               ]
         | Bool
True
         = Defn
res
         where res :: Defn
res = [String] -> Maybe [(Quantifier, String)] -> (Int -> String) -> Defn
Defn ([String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String
nm | Uninterpreted String
nm <- Seq (SV, SBVExpr) -> [Op]
forall from to. Biplate from to => from -> [to]
G.universeBi Seq (SV, SBVExpr)
asgnsSeq])
                          Maybe [(Quantifier, String)]
mbParam
                          (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> (Int -> [String]) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String]
body)

               params :: [(Quantifier, SV)]
params = case ResultInp
is of
                          ResultTopInps ([NamedSymVar], [NamedSymVar])
as -> [String] -> [(Quantifier, SV)]
forall {a}. [String] -> a
bad [ String
"Top inputs"
                                                  , String
"   Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([NamedSymVar], [NamedSymVar]) -> String
forall a. Show a => a -> String
show ([NamedSymVar], [NamedSymVar])
as
                                                  ]
                          ResultLamInps [(Quantifier, NamedSymVar)]
xs -> ((Quantifier, NamedSymVar) -> (Quantifier, SV))
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, SV)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Quantifier
q, NamedSymVar
v) -> (Quantifier
q, NamedSymVar -> SV
getSV NamedSymVar
v)) [(Quantifier, NamedSymVar)]
xs

               mbParam :: Maybe [(Quantifier, String)]
mbParam
                 | [(Quantifier, SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Quantifier, SV)]
params = Maybe [(Quantifier, String)]
forall a. Maybe a
Nothing
                 | Bool
True        = [(Quantifier, String)] -> Maybe [(Quantifier, String)]
forall a. a -> Maybe a
Just [(Quantifier
q, [SV] -> String
forall {a}. (Show a, HasKind a) => [a] -> String
paramList (((Quantifier, SV) -> SV) -> [(Quantifier, SV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, SV) -> SV
forall a b. (a, b) -> b
snd [(Quantifier, SV)]
l)) | l :: [(Quantifier, SV)]
l@((Quantifier
q, SV
_) : [(Quantifier, SV)]
_)  <- [[(Quantifier, SV)]]
pGroups]
                 where pGroups :: [[(Quantifier, SV)]]
pGroups = ((Quantifier, SV) -> (Quantifier, SV) -> Bool)
-> [(Quantifier, SV)] -> [[(Quantifier, SV)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Quantifier
q1, SV
_) (Quantifier
q2, SV
_) -> Quantifier
q1 Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
q2) [(Quantifier, SV)]
params
                       paramList :: [a] -> String
paramList [a]
ps = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: [String] -> String
unwords ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\a
p -> Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType (a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
p) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")  [a]
ps) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

               body :: Int -> [String]
body Int
tabAmnt
                 | [(((Int, Kind, Kind), [SV]), [String])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(((Int, Kind, Kind), [SV]), [String])]
constTables
                 , [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables
                 , Just String
e <- [(SV, String)] -> SV -> Maybe String
simpleBody ([(SV, String)]
constBindings [(SV, String)] -> [(SV, String)] -> [(SV, String)]
forall a. [a] -> [a] -> [a]
++ [(SV, String)]
svBindings) SV
out
                 = [String
tab String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e]
                 | Bool
True
                 = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
tab String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$   [(SV, String) -> String
forall {a}. Show a => (a, String) -> String
mkLet (SV, String)
sv  | (SV, String)
sv <- [(SV, String)]
constBindings]
                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(((Int, Kind, Kind), [SV]), [String]) -> String
forall {a} {b}. Show a => (((a, Kind, Kind), [SV]), b) -> String
mkTable (((Int, Kind, Kind), [SV]), [String])
t | (((Int, Kind, Kind), [SV]), [String])
t  <- [(((Int, Kind, Kind), [SV]), [String])]
constTables]
                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(SV, String)]
-> [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
-> [String]
forall {a} {b}.
(Show a, Show b) =>
[(SV, String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [(SV, String)]
svBindings [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables
                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [SV -> String
forall a. Show a => a -> String
show SV
out String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
totalClose Char
')']

                 where tab :: String
tab          = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
tabAmnt Char
' '
                       mkBind :: String -> String -> String
mkBind String
l String
r   = String
"(let ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                       mkLet :: (a, String) -> String
mkLet (a
s, String
v) = String -> String -> String
mkBind (a -> String
forall a. Show a => a -> String
show a
s) String
v

                       mkTable :: (((a, Kind, Kind), [SV]), b) -> String
mkTable (((a
i, Kind
ak, Kind
rk), [SV]
elts), b
_) = String -> String -> String
mkBind String
nm (String -> Kind -> Kind -> [SV] -> String
lambdaTable ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Char -> Char
forall a b. a -> b -> a
const Char
' ') String
nm) Kind
ak Kind
rk [SV]
elts)
                          where nm :: String
nm = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

                       totalClose :: Int
totalClose = [(SV, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SV, String)]
constBindings
                                  Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(SV, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SV, String)]
svBindings
                                  Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(((Int, Kind, Kind), [SV]), [String])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(((Int, Kind, Kind), [SV]), [String])]
constTables
                                  Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables

                       walk :: [(SV, String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk []  []        = []
                       walk []  [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible: Ran out of bindings, but tables remain: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> String
forall a. Show a => a -> String
show [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining
                       walk (cur :: (SV, String)
cur@(SV Kind
_ NodeId
nd, String
_) : [(SV, String)]
rest)  [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining =  (((Int, Int), (((a, Kind, Kind), [SV]), b)) -> String)
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((((a, Kind, Kind), [SV]), b) -> String
forall {a} {b}. Show a => (((a, Kind, Kind), [SV]), b) -> String
mkTable ((((a, Kind, Kind), [SV]), b) -> String)
-> (((Int, Int), (((a, Kind, Kind), [SV]), b))
    -> (((a, Kind, Kind), [SV]), b))
-> ((Int, Int), (((a, Kind, Kind), [SV]), b))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int), (((a, Kind, Kind), [SV]), b))
-> (((a, Kind, Kind), [SV]), b)
forall a b. (a, b) -> b
snd) [((Int, Int), (((a, Kind, Kind), [SV]), b))]
ready
                                                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(SV, String) -> String
forall {a}. Show a => (a, String) -> String
mkLet (SV, String)
cur]
                                                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(SV, String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [(SV, String)]
rest [((Int, Int), (((a, Kind, Kind), [SV]), b))]
notReady
                          where ([((Int, Int), (((a, Kind, Kind), [SV]), b))]
ready, [((Int, Int), (((a, Kind, Kind), [SV]), b))]
notReady) = (((Int, Int), (((a, Kind, Kind), [SV]), b)) -> Bool)
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))]
-> ([((Int, Int), (((a, Kind, Kind), [SV]), b))],
    [((Int, Int), (((a, Kind, Kind), [SV]), b))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\((Int, Int)
need, (((a, Kind, Kind), [SV]), b)
_) -> (Int, Int)
need (Int, Int) -> (Int, Int) -> Bool
forall a. Ord a => a -> a -> Bool
< NodeId -> (Int, Int)
getLLI NodeId
nd) [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining

               getLLI :: NodeId -> (Int, Int)
               getLLI :: NodeId -> (Int, Int)
getLLI (NodeId (SBVContext
_, Int
l, Int
i)) = (Int
l, Int
i)

               -- if we have just one definition returning it, simplify
               simpleBody :: [(SV, String)] -> SV -> Maybe String
               simpleBody :: [(SV, String)] -> SV -> Maybe String
simpleBody [(SV
v, String
e)] SV
o | SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
o = String -> Maybe String
forall a. a -> Maybe a
Just String
e
               simpleBody [(SV, String)]
_        SV
_          = Maybe String
forall a. Maybe a
Nothing

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

               constants :: [(SV, CV)]
constants = ((SV, CV) -> Bool) -> [(SV, CV)] -> [(SV, CV)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SV
falseSV, SV
trueSV]) (SV -> Bool) -> ((SV, CV) -> SV) -> (SV, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, CV) -> SV
forall a b. (a, b) -> a
fst) [(SV, CV)]
consts

               constBindings, svBindings :: [(SV, String)]
               constBindings :: [(SV, String)]
constBindings = ((SV, CV) -> (SV, String)) -> [(SV, CV)] -> [(SV, String)]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> (SV, String)
mkConst [(SV, CV)]
constants
               svBindings :: [(SV, String)]
svBindings    = ((SV, SBVExpr) -> (SV, String))
-> [(SV, SBVExpr)] -> [(SV, String)]
forall a b. (a -> b) -> [a] -> [b]
map (SV, SBVExpr) -> (SV, String)
forall {a}. (a, SBVExpr) -> (a, String)
mkAsgn [(SV, SBVExpr)]
assignments

               mkConst :: (SV, CV) -> (SV, String)
               mkConst :: (SV, CV) -> (SV, String)
mkConst (SV
sv, CV
cv) = (SV
sv, RoundingMode -> CV -> String
cvToSMTLib (SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg) CV
cv)

               out :: SV
               out :: SV
out = case [SV]
outputs of
                       [SV
o] -> SV
o
                       [SV]
_   -> [String] -> SV
forall {a}. [String] -> a
bad [ String
"Unexpected non-singular output"
                                  , String
"   Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> String
forall a. Show a => a -> String
show [SV]
outputs
                                  ]

               rm :: RoundingMode
rm = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg

               -- NB. The following is dead-code, since we ensure tbls is empty
               -- We used to support this, but there are issues, so dropping support
               -- See, for instance, https://github.com/LeventErkok/sbv/issues/664
               (IntMap String
tableMap, [(((Int, Kind, Kind), [SV]), [String])]
constTables, [(((Int, Kind, Kind), [SV]), [String])]
nonConstTablesUnindexed) = RoundingMode
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> (IntMap String, [(((Int, Kind, Kind), [SV]), [String])],
    [(((Int, Kind, Kind), [SV]), [String])])
constructTables RoundingMode
rm [(SV, CV)]
consts [((Int, Kind, Kind), [SV])]
tbls

               -- Index each non-const table with the largest index of SV it needs
               nonConstTables :: [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables = [ ([(Int, Int)] -> (Int, Int)
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Int
0, Int
0) (Int, Int) -> [(Int, Int)] -> [(Int, Int)]
forall a. a -> [a] -> [a]
: [NodeId -> (Int, Int)
getLLI NodeId
n | SV Kind
_ NodeId
n <- [SV]
elts]), (((Int, Kind, Kind), [SV]), [String])
nct)
                                | nct :: (((Int, Kind, Kind), [SV]), [String])
nct@(((Int, Kind, Kind)
_, [SV]
elts), [String]
_) <- [(((Int, Kind, Kind), [SV]), [String])]
nonConstTablesUnindexed]

               lambdaTable :: String -> Kind -> Kind -> [SV] -> String
               lambdaTable :: String -> Kind -> Kind -> [SV] -> String
lambdaTable String
extraSpace Kind
ak Kind
rk [SV]
elts = String
"(lambda ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ak String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
space String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> [SV] -> String
forall {a}. Show a => Integer -> [a] -> String
chain Integer
0 [SV]
elts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                 where cnst :: Kind -> Integer -> String
cnst Kind
k Integer
i = RoundingMode -> CV -> String
cvtCV RoundingMode
rm (Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (Integer
i::Integer))

                       lv :: String
lv = String
"idx"

                       -- If more than 5 elts, use new-lines
                       long :: Bool
long = Bool -> Bool
not ([SV] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Int -> [SV] -> [SV]
forall a. Int -> [a] -> [a]
drop Int
5 [SV]
elts))
                       space :: String
space
                         | Bool
long
                         = String
"\n                  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
extraSpace
                         | Bool
True
                         = String
" "

                       chain :: Integer -> [a] -> String
chain Integer
_ []     = Kind -> Integer -> String
cnst Kind
rk Integer
0
                       chain Integer
_ [a
x]    = a -> String
forall a. Show a => a -> String
show a
x
                       chain Integer
i (a
x:[a]
xs) = String
"(ite (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> Integer -> String
cnst Kind
ak Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") "
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
space
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> [a] -> String
chain (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) [a]
xs
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

               mkAsgn :: (a, SBVExpr) -> (a, String)
mkAsgn (a
sv, SBVExpr
e) = (a
sv, SBVExpr -> String
converter SBVExpr
e)
               converter :: SBVExpr -> String
converter = ProgInfo
-> SolverCapabilities
-> RoundingMode
-> IntMap String
-> FunctionMap
-> SBVExpr
-> String
cvtExp ProgInfo
curProgInfo SolverCapabilities
solverCaps RoundingMode
rm IntMap String
tableMap FunctionMap
forall {k} {a}. Map k a
funcMap
                 where solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
                       funcMap :: Map k a
funcMap    = Map k a
forall {k} {a}. Map k a
M.empty

{- HLint ignore module "Use second" -}