    -----------------------------------------------------------------------------
    -- |
    -- 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.IntMap.Strict as IM

    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
                         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
                       , rtblMap :: IORef TableMap
    rtblMap      = (State -> IORef TableMap) -> IORef TableMap
    forall {t}. (State -> t) -> t
    share State -> IORef TableMap
    rtblMap
                       , rArrayMap :: IORef ArrayMap
    rArrayMap    = (State -> IORef ArrayMap) -> IORef ArrayMap
    forall {t}. (State -> t) -> t
    share State -> IORef ArrayMap
    rArrayMap
                       , rAICache :: IORef (Cache ArrayIndex)
    rAICache     = (State -> IORef (Cache ArrayIndex)) -> IORef (Cache ArrayIndex)
    forall {t}. (State -> t) -> t
    share State -> IORef (Cache ArrayIndex)
    rAICache
                       , 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]
    rDefns       = (State -> IORef [SMTDef]) -> IORef [SMTDef]
    forall {t}. (State -> t) -> t
    share State -> IORef [SMTDef]
    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

                       -- 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
                       , 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 -> Kind -> a -> m String
    namedLambdaStr :: forall (m :: * -> *) a.
    (MonadIO m, Lambda (SymbolicT m) a) =>
    State -> String -> Kind -> a -> m String
    namedLambdaStr State
    inState String
    nm Kind
    fk = (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] -> [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]

    -- | 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  -- This contains the CV->SV map, which isn't needed for lambdas since we don't support tables
                      , [(SV, CV)]
    consts      -- constants used
                      )

                      [((Int, Kind, Kind), [SV])]
    _tbls         -- Tables                : nothing to do with them
                      [(Int, ArrayInfo)]
    _arrs         -- Arrays                : nothing to do with them
                      [(String, (Maybe [String], SBVType))]
    _uis          -- Uninterpeted constants: nothing to do with them
                      [SMTDef]
    _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
                     | Just String
    e <- [(SV, String)] -> SV -> Maybe String
    simpleBody [(SV, String)]
    bindings SV
    out
                     = [Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    tabAmnt Char
    ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    e]
                     | Bool
    True
                     = let tab :: String
    tab = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    tabAmnt Char
    ' '
                       in    [String
    tab String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "(let ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))" | (SV
    s, String
    v) <- [(SV, String)]
    bindings]
                          [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    tab 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 ([(SV, String)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(SV, String)]
    bindings) Char
    ')']

                   -- 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

                   bindings :: [(SV, String)]
                   bindings :: [(SV, String)]
    bindings = ((SV, CV) -> (SV, String)) -> [(SV, CV)] -> [(SV, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, CV) -> (SV, String)
    mkConst [(SV, CV)]
    constants [(SV, String)] -> [(SV, String)] -> [(SV, String)]
    forall a. [a] -> [a] -> [a]
    ++ ((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
                                      ]

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

    {- HLint ignore module "Use second" -}