-----------------------------------------------------------------------------
-- |
-- 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 TupleSections         #-}
{-# LANGUAGE UndecidableInstances  #-}

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

module Data.SBV.Lambda (
            lambda,      lambdaStr
          , namedLambda, namedLambdaStr
          , constraint,  constraintStr
          , LambdaScope(..)
        ) 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)
import qualified Data.SBV.Core.Symbolic as     S (mkNewState)

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

import qualified Data.Foldable as F
import qualified Data.Set      as Set

import qualified Data.Generics.Uniplate.Data as G

-- | What's the scope of the generated lambda?
data LambdaScope = HigherOrderArg   -- This lambda will be firstified, hence can't have any free variables
                 | TopLevel         -- This lambda is used to represent a quantified axiom, can have free vars

data Defn = Defn [String]                        -- The uninterpreted names referred to in the body
                 [String]                        -- Free variables (i.e., not uninterpreted nor bound in the definition itself)
                 (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 => LambdaScope -> State -> (State -> m b) -> m b
inSubState :: forall (m :: * -> *) b.
MonadIO m =>
LambdaScope -> State -> (State -> m b) -> m b
inSubState LambdaScope
scope State
inState State -> m b
comp = do

        let noNesting :: b
noNesting = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                        , String
"*** Data.SBV.Lambda: Detected nested lambda-definitions."
                                        , String
"***"
                                        , String
"*** SBV uses firstification to deal-with lambdas, and SMTLib's first-order nature does not allow"
                                        , String
"*** for easy translation of nested lambdas. As SMTLib gets higher-order features, SBV will eventually"
                                        , String
"*** relax this restriction. In the mean-time, please rewrite your program without using nested-lambdas"
                                        , String
"*** if possible. If this workaround isn't applicable, please report this as a use-case for further"
                                        , String
"*** possible enhancements."
                                        ]

        newLevel <- do ll <- IO (Maybe Int) -> m (Maybe Int)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Int) -> m (Maybe Int))
-> IO (Maybe Int) -> m (Maybe Int)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe Int)
rLambdaLevel State
inState)
                       pure $ case ll of
                                Maybe Int
Nothing -> Maybe Int
forall {b}. b
noNesting
                                Just Int
i  -> case LambdaScope
scope of
                                             LambdaScope
HigherOrderArg -> Maybe Int
forall a. Maybe a
Nothing
                                             LambdaScope
TopLevel       -> Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

        stEmpty <- S.mkNewState (stCfg inState) (LambdaGen newLevel)

        let share State -> t
fld = State -> t
fld State
inState   -- reuse the field from the parent-context
            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.
        comp State {
                   -- These are not IORefs; so we share by copying  the value; changes won't be copied back
                     sbvContext          = share sbvContext
                   , pathCond            = share pathCond
                   , startTime           = share startTime

                   -- These are shared IORef's; and is shared, so they will be copied back to the parent state
                   , rProgInfo           = share rProgInfo
                   , rIncState           = share rIncState
                   , rCInfo              = share rCInfo
                   , rUsedKinds          = share rUsedKinds
                   , rUsedLbls           = share rUsedLbls
                   , rUIMap              = share rUIMap
                   , rUserFuncs          = share rUserFuncs
                   , rCgMap              = share rCgMap
                   , rDefns              = share rDefns
                   , rSMTOptions         = share rSMTOptions
                   , rOptGoals           = share rOptGoals
                   , rAsserts            = share rAsserts
                   , rOutstandingAsserts = share rOutstandingAsserts
                   , rPartitionVars      = share rPartitionVars

                   -- Everything else is fresh in the substate; i.e., will not copy back
                   , stCfg               = fresh stCfg
                   , runMode             = fresh runMode
                   , rctr                = fresh rctr
                   , rLambdaLevel        = fresh rLambdaLevel
                   , rtblMap             = fresh rtblMap
                   , rinps               = fresh rinps
                   , rlambdaInps         = fresh rlambdaInps
                   , rConstraints        = fresh rConstraints
                   , rObservables        = fresh rObservables
                   , routs               = fresh routs
                   , spgm                = fresh spgm
                   , rconstMap           = fresh rconstMap
                   , rexprMap            = fresh rexprMap
                   , rSVCache            = fresh rSVCache
                   , rQueryState         = fresh rQueryState

                   -- keep track of our parent
                   , parentState         = Just 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) => LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
lambdaGen :: forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
lambdaGen LambdaScope
scope Defn -> b
trans State
inState Kind
fk a
f = LambdaScope -> State -> (State -> m b) -> m b
forall (m :: * -> *) b.
MonadIO m =>
LambdaScope -> State -> (State -> m b) -> m b
inSubState LambdaScope
scope State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
handle (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)
  where handle :: Defn -> b
handle d :: Defn
d@(Defn [String]
_ [String]
frees Maybe [(Quantifier, String)]
_ Int -> String
_) =
            case LambdaScope
scope of
              LambdaScope
TopLevel       -> Defn -> b
trans Defn
d
              LambdaScope
HigherOrderArg -> if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
frees
                                then Defn -> b
trans Defn
d
                                else String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                     , String
"*** Data.SBV.Lambda: Detected free variables passed to a lambda."
                                                     , String
"***"
                                                     , String
"***  Free vars : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
frees
                                                     , String
"***  Definition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
shift (String -> [String]
lines (Defn -> String
sh Defn
d))
                                                     , String
"***"
                                                     , String
"*** In certain contexts, SBV only allows closed-lambdas, i.e., those that do not have any free variables in."
                                                     , String
"***"
                                                     , String
"*** Please rewrite your program to pass the free variable as an explicit argument to the lambda if possible."
                                                     , String
"*** If this workaround isn't applicable, please report this as a use-case for further possible enhancements."
                                                     ]

        sh :: Defn -> String
sh (Defn [String]
_unints [String]
_frees Maybe [(Quantifier, String)]
Nothing       Int -> String
body) = Int -> String
body Int
0
        sh (Defn [String]
_unints [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
")"

        shift :: [String] -> String
shift []     = []
        shift (String
x:[String]
xs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (String
x String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
tab [String]
xs)
          where tab :: String -> String
tab String
s = String
"***              " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

-- | Create an SMTLib lambda, in the given state.
lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> LambdaScope -> Kind -> a -> m SMTDef
lambda :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> LambdaScope -> Kind -> a -> m SMTDef
lambda State
inState LambdaScope
scope Kind
fk = LambdaScope -> (Defn -> SMTDef) -> State -> Kind -> a -> m SMTDef
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
lambdaGen LambdaScope
scope Defn -> SMTDef
mkLam State
inState Kind
fk
   where mkLam :: Defn -> SMTDef
mkLam (Defn [String]
unints [String]
_frees Maybe [(Quantifier, String)]
params Int -> String
body) = Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTLam Kind
fk [String]
unints ([(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. The kind passed is the kind of the final result.
lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> LambdaScope -> Kind -> a -> m SMTLambda
lambdaStr :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> LambdaScope -> Kind -> a -> m SMTLambda
lambdaStr State
st LambdaScope
scope Kind
k a
a = String -> SMTLambda
SMTLambda (String -> SMTLambda) -> m String -> m SMTLambda
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LambdaScope -> (Defn -> String) -> State -> Kind -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
lambdaGen LambdaScope
scope Defn -> String
mkLam State
st Kind
k a
a
   where mkLam :: Defn -> String
mkLam (Defn [String]
_unints [String]
_frees Maybe [(Quantifier, String)]
Nothing       Int -> String
body) = Int -> String
body Int
0
         mkLam (Defn [String]
_unints [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) => LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen :: forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen LambdaScope
scope Defn -> b
trans State
inState Kind
fk a
f = LambdaScope -> State -> (State -> m b) -> m b
forall (m :: * -> *) b.
MonadIO m =>
LambdaScope -> State -> (State -> m b) -> m b
inSubState LambdaScope
scope 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) => LambdaScope -> State -> String -> Kind -> a -> m SMTDef
namedLambda :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> State -> String -> Kind -> a -> m SMTDef
namedLambda LambdaScope
scope State
inState String
nm Kind
fk = LambdaScope -> (Defn -> SMTDef) -> State -> Kind -> a -> m SMTDef
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen LambdaScope
scope Defn -> SMTDef
mkDef State
inState Kind
fk
   where mkDef :: Defn -> SMTDef
mkDef (Defn [String]
unints [String]
_frees Maybe [(Quantifier, String)]
params Int -> String
body) = String
-> Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTDef String
nm Kind
fk [String]
unints ([(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) => LambdaScope -> State -> String -> SBVType -> a -> m String
namedLambdaStr :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> State -> String -> SBVType -> a -> m String
namedLambdaStr LambdaScope
scope State
inState String
nm SBVType
t = LambdaScope -> (Defn -> String) -> State -> Kind -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
LambdaScope -> (Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen LambdaScope
scope Defn -> String
mkDef State
inState Kind
fk
   where mkDef :: Defn -> String
mkDef (Defn [String]
unints [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]
unints ([(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) => LambdaScope -> ([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen :: forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
LambdaScope
-> ([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen LambdaScope
scope [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 [String]
_frees Maybe [(Quantifier, String)]
Nothing       Int -> String
body) = [String] -> (Int -> String) -> b
trans [String]
deps Int -> String
body
       mkDef (Defn [String]
deps [String]
_frees (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

   LambdaScope -> State -> (State -> m b) -> m b
forall (m :: * -> *) b.
MonadIO m =>
LambdaScope -> State -> (State -> m b) -> m b
inSubState LambdaScope
scope 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.
-- We allow free variables here (first arg of constraintGen). This might prove to be not kosher!
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
. LambdaScope
-> ([String] -> (Int -> String) -> m SV) -> State -> a -> m (m SV)
forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
LambdaScope
-> ([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen LambdaScope
TopLevel [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
-- We allow free variables here (first arg of constraintGen). This might prove to be not kosher!
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 = LambdaScope
-> ([String] -> (Int -> String) -> String)
-> State
-> a
-> m String
forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
LambdaScope
-> ([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen LambdaScope
TopLevel [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
   ((), res)   <- State -> SymbolicT m () -> m ((), Result)
forall (m :: * -> *) a.
MonadIO m =>
State -> SymbolicT m a -> m (a, Result)
runSymbolicInState State
st SymbolicT m ()
comp
   curProgInfo <- liftIO $ readIORef (rProgInfo st)
   level       <- liftIO $ readIORef (rLambdaLevel st)
   pure $ toLambda level curProgInfo (stCfg st) expectedKind res

-- | Convert the result of a symbolic run to a more abstract representation
toLambda :: Maybe Int -> ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda :: Maybe Int -> ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda Maybe Int
level 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] -> b
tbd [String]
xs = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
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] -> b
bad [String]
xs = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
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

                  [(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 {b}. [String] -> b
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 {b}. [String] -> b
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]
               ]

         {- Simply ignore the observables, instead of choking on them,
          - This allows for more robust coding, though it might be confusing.
         | not (null observables)
         = tbd [ "Observables."
               , "  Saw: " ++ intercalate ", " [n | (n, _, _) <- 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 {b}. [String] -> b
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]
-> [String]
-> Maybe [(Quantifier, String)]
-> (Int -> String)
-> Defn
Defn ([String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String
nm | Uninterpreted String
nm <- [Op] -> [Op]
forall from to. Biplate from to => from -> [to]
G.universeBi [Op]
allOps])
                          [String]
frees
                          Maybe [(Quantifier, String)]
mbParam
                          Int -> String
body

               -- Below can simply be defined as: nub (sort (G.universeBi asgnsSeq))
               -- Alas, it turns out this is really expensive when we have nested lambdas, so we do an explicit walk
               allOps :: [Op]
allOps = Set Op -> [Op]
forall a. Set a -> [a]
Set.toList (Set Op -> [Op]) -> Set Op -> [Op]
forall a b. (a -> b) -> a -> b
$ (Set Op -> (SV, SBVExpr) -> Set Op)
-> Set Op -> Seq (SV, SBVExpr) -> Set Op
forall b a. (b -> a -> b) -> b -> Seq a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Set Op
sofar (SV
_, SBVApp Op
o [SV]
_) -> Op -> Set Op -> Set Op
forall a. Ord a => a -> Set a -> Set a
Set.insert Op
o Set Op
sofar) Set Op
forall a. Set a
Set.empty Seq (SV, SBVExpr)
asgnsSeq

               params :: [(Quantifier, SV)]
params = case ResultInp
is of
                          ResultTopInps ([NamedSymVar], [NamedSymVar])
as -> [String] -> [(Quantifier, SV)]
forall {b}. [String] -> b
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

               frees :: [String]
frees = (SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show ([SV] -> [String]) -> [SV] -> [String]
forall a b. (a -> b) -> a -> b
$ [SV] -> [SV]
forall a. Eq a => [a] -> [a]
nub [SV]
allUses [SV] -> [SV] -> [SV]
forall a. Eq a => [a] -> [a] -> [a]
\\ [SV] -> [SV]
forall a. Eq a => [a] -> [a]
nub [SV]
allDefs
                 where ([SV]
defs, [[SV]]
uses) = [(SV, [SV])] -> ([SV], [[SV]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(SV
d, [SV]
u) | (SV
d, SBVApp Op
_ [SV]
u) <- Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, SBVExpr)
asgnsSeq]
                       allDefs :: [SV]
allDefs      = [SV]
defs [SV] -> [SV] -> [SV]
forall a. [a] -> [a] -> [a]
++ ((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)]
params [SV] -> [SV] -> [SV]
forall a. [a] -> [a] -> [a]
++ ((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> SV
forall a b. (a, b) -> a
fst [(SV, CV)]
constants
                       allUses :: [SV]
allUses      = [[SV]] -> [SV]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SV]]
uses

               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), Maybe String)] -> SV -> Maybe String
simpleBody (((SV, String) -> ((SV, String), Maybe String))
-> [(SV, String)] -> [((SV, String), Maybe String)]
forall a b. (a -> b) -> [a] -> [b]
map (, Maybe String
forall a. Maybe a
Nothing) [(SV, String)]
constBindings [((SV, String), Maybe String)]
-> [((SV, String), Maybe String)] -> [((SV, String), Maybe String)]
forall a. [a] -> [a] -> [a]
++ [((SV, String), Maybe String)]
svBindings) SV
out
                 = String
tab String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
                 | Bool
True
                 = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (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), Maybe String)]
-> [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
-> [String]
forall {a} {b}.
(Show a, Show b) =>
[((SV, String), Maybe String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [((SV, String), Maybe String)]
svBindings [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables
                                                   [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
shift 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
shift String -> String -> String
forall a. [a] -> [a] -> [a]
++ 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

                       -- Align according to level.
                       shift :: String
shift = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
24 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
16 Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) Char
' '

                       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), Maybe String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((SV, String), Maybe 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), Maybe 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), Maybe String)
cur@((SV Kind
_ NodeId
nd, String
_), Maybe String
_) : [((SV, String), Maybe 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), Maybe String) -> String
forall {a}. Show a => ((a, String), Maybe String) -> String
mkLocalBind ((SV, String), Maybe String)
cur]
                                                                      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [((SV, String), Maybe String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [((SV, String), Maybe 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
                                mkLocalBind :: ((a, String), Maybe String) -> String
mkLocalBind ((a, String)
b, Maybe String
Nothing) = (a, String) -> String
forall {a}. Show a => (a, String) -> String
mkLet (a, String)
b
                                mkLocalBind ((a, String)
b, Just String
l)  = (a, String) -> String
forall {a}. Show a => (a, String) -> String
mkLet (a, String)
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l

               getLLI :: NodeId -> (Int, Int)
               getLLI :: NodeId -> (Int, Int)
getLLI (NodeId (SBVContext
_, Maybe Int
mbl, Int
i)) = (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
mbl, Int
i)

               -- if we have just one definition returning it, and if the expression itself is simple enough (single-line), simplify
               -- If the line has new-lines we typically don't want to mess with it, but that causes a memory leak
               -- (see https://github.com/LeventErkok/sbv/issues/733), so only do it if we're being verbose for debugging purposes.
               mkPretty :: Bool
mkPretty = SMTConfig -> Bool
verbose SMTConfig
cfg

               simpleBody :: [((SV, String), Maybe String)] -> SV -> Maybe String
               simpleBody :: [((SV, String), Maybe String)] -> SV -> Maybe String
simpleBody [((SV
v, String
e), Maybe String
Nothing)] SV
o | SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
o, Bool -> Bool
not Bool
mkPretty Bool -> Bool -> Bool
|| Char
'\n' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` String
e = String -> Maybe String
forall a. a -> Maybe a
Just String
e
               simpleBody [((SV, String), Maybe 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 :: [(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
                 where 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)

               svBindings :: [((SV, String), Maybe String)]
               svBindings :: [((SV, String), Maybe String)]
svBindings = ((SV, SBVExpr) -> ((SV, String), Maybe String))
-> [(SV, SBVExpr)] -> [((SV, String), Maybe String)]
forall a b. (a -> b) -> [a] -> [b]
map (SV, SBVExpr) -> ((SV, String), Maybe String)
forall {a}. (a, SBVExpr) -> ((a, String), Maybe String)
mkAsgn [(SV, SBVExpr)]
assignments
                 where mkAsgn :: (a, SBVExpr) -> ((a, String), Maybe String)
mkAsgn (a
sv, e :: SBVExpr
e@(SBVApp (Label String
l) [SV]
_)) = ((a
sv, SBVExpr -> String
converter SBVExpr
e), String -> Maybe String
forall a. a -> Maybe a
Just String
l)
                       mkAsgn (a
sv, SBVExpr
e)                      = ((a
sv, SBVExpr -> String
converter SBVExpr
e), Maybe String
forall a. Maybe a
Nothing)

                       converter :: SBVExpr -> String
converter = SMTConfig
-> ProgInfo
-> SolverCapabilities
-> RoundingMode
-> TableMap
-> SBVExpr
-> String
cvtExp SMTConfig
cfg ProgInfo
curProgInfo (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)) RoundingMode
rm TableMap
tableMap


               out :: SV
               out :: SV
out = case [SV]
outputs of
                       [SV
o] -> SV
o
                       [SV]
_   -> [String] -> SV
forall {b}. [String] -> b
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
               (TableMap
tableMap, [(((Int, Kind, Kind), [SV]), [String])]
constTables, [(((Int, Kind, Kind), [SV]), [String])]
nonConstTablesUnindexed) = RoundingMode
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> (TableMap, [(((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
")"

{- HLint ignore module "Use second" -}