    -- |
    -- Module      :  Cryptol.Symbolic
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ViewPatterns #-}

    module Cryptol.Symbolic where

    import Control.Monad.IO.Class
    import Control.Monad (replicateM, when, zipWithM, foldM)
    import Control.Monad.Writer (WriterT, runWriterT, tell, lift)
    import Data.List (intercalate, genericLength)
    import Data.IORef(IORef)
    import qualified Control.Exception as X

    import qualified Data.SBV.Dynamic as SBV
    import           Data.SBV (Timing(SaveTiming))
    import           Data.SBV.Internals (showTDiff)

    import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
    import qualified Cryptol.ModuleSystem.Env as M
    import qualified Cryptol.ModuleSystem.Base as M
    import qualified Cryptol.ModuleSystem.Monad as M

    import Cryptol.Symbolic.Prims
    import Cryptol.Symbolic.Value

    import qualified Cryptol.Eval as Eval
    import qualified Cryptol.Eval.Monad as Eval
    import qualified Cryptol.Eval.Type as Eval
    import qualified Cryptol.Eval.Value as Eval
    import           Cryptol.Eval.Env (GenEvalEnv(..))
    import Cryptol.TypeCheck.AST
    import Cryptol.Utils.Ident (Ident)
    import Cryptol.Utils.PP
    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.Logger(logPutStrLn)

    import Prelude ()
    import Prelude.Compat

    import Data.Time (NominalDiffTime)

    type EvalEnv = GenEvalEnv SBool SWord

    -- External interface ----------------------------------------------------------

    proverConfigs :: [(String, SBV.SMTConfig)]
    proverConfigs :: [(String, SMTConfig)]
    proverConfigs =
      [ ("cvc4"     , SMTConfig
    SBV.cvc4     )
      , ("yices"    , SMTConfig
    SBV.yices    )
      , ("z3"       , SMTConfig
    SBV.z3       )
      , ("boolector", SMTConfig
    SBV.boolector)
      , ("mathsat"  , SMTConfig
    SBV.mathSAT  )
      , ("abc"      , SMTConfig
    SBV.abc      )
      , ("offline"  , SMTConfig
    SBV.defaultSMTCfg )
      , ("any"      , SMTConfig
    SBV.defaultSMTCfg )
      ]

    proverNames :: [String]
    proverNames :: [String]
    proverNames = ((String, SMTConfig) -> String)
    -> [(String, SMTConfig)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, SMTConfig) -> String
    forall a b. (a, b) -> a
    fst [(String, SMTConfig)]
    proverConfigs

    lookupProver :: String -> SBV.SMTConfig
    lookupProver :: String -> SMTConfig
    lookupProver s :: String
    s =
      case String -> [(String, SMTConfig)] -> Maybe SMTConfig
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    s [(String, SMTConfig)]
    proverConfigs of
        Just cfg :: SMTConfig
    cfg -> SMTConfig
    cfg
        -- should be caught by UI for setting prover user variable
        Nothing  -> String -> [String] -> SMTConfig
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.Symbolic" [ "invalid prover: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s ]

    type SatResult = [(Type, Expr, Eval.Value)]

    data SatNum = AllSat | SomeSat Int
      deriving (Int -> SatNum -> String -> String
    [SatNum] -> String -> String
    SatNum -> String
    (Int -> SatNum -> String -> String)
    -> (SatNum -> String)
    -> ([SatNum] -> String -> String)
    -> Show SatNum
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [SatNum] -> String -> String
    $cshowList :: [SatNum] -> String -> String
    show :: SatNum -> String
    $cshow :: SatNum -> String
    showsPrec :: Int -> SatNum -> String -> String
    $cshowsPrec :: Int -> SatNum -> String -> String
    Show)

    data QueryType = SatQuery SatNum | ProveQuery
      deriving (Int -> QueryType -> String -> String
    [QueryType] -> String -> String
    QueryType -> String
    (Int -> QueryType -> String -> String)
    -> (QueryType -> String)
    -> ([QueryType] -> String -> String)
    -> Show QueryType
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [QueryType] -> String -> String
    $cshowList :: [QueryType] -> String -> String
    show :: QueryType -> String
    $cshow :: QueryType -> String
    showsPrec :: Int -> QueryType -> String -> String
    $cshowsPrec :: Int -> QueryType -> String -> String
    Show)

    data ProverCommand = ProverCommand {
        ProverCommand -> QueryType
    pcQueryType :: QueryType
        -- ^ The type of query to run
      , ProverCommand -> String
    pcProverName :: String
        -- ^ Which prover to use (one of the strings in 'proverConfigs')
      , ProverCommand -> Bool
    pcVerbose :: Bool
        -- ^ Verbosity flag passed to SBV
      , ProverCommand -> Bool
    pcValidate :: Bool
        -- ^ Model validation flag passed to SBV
      , ProverCommand -> IORef ProverStats
    pcProverStats :: !(IORef ProverStats)
        -- ^ Record timing information here
      , ProverCommand -> [DeclGroup]
    pcExtraDecls :: [DeclGroup]
        -- ^ Extra declarations to bring into scope for symbolic
        -- simulation
      , ProverCommand -> Maybe String
    pcSmtFile :: Maybe FilePath
        -- ^ Optionally output the SMTLIB query to a file
      , ProverCommand -> Expr
    pcExpr :: Expr
        -- ^ The typechecked expression to evaluate
      , ProverCommand -> Schema
    pcSchema :: Schema
        -- ^ The 'Schema' of @pcExpr@
      }

    type ProverStats = NominalDiffTime

    -- | A prover result is either an error message, an empty result (eg
    -- for the offline prover), a counterexample or a lazy list of
    -- satisfying assignments.
    data ProverResult = AllSatResult [SatResult] -- LAZY
                      | ThmResult    [Type]
                      | EmptyResult
                      | ProverError  String

    satSMTResults :: SBV.SatResult -> [SBV.SMTResult]
    satSMTResults :: SatResult -> [SMTResult]
    satSMTResults (SBV.SatResult r :: SMTResult
    r) = [SMTResult
    r]

    allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
    allSatSMTResults :: AllSatResult -> [SMTResult]
    allSatSMTResults (SBV.AllSatResult (_, _, _, rs :: [SMTResult]
    rs)) = [SMTResult]
    rs

    thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
    thmSMTResults :: ThmResult -> [SMTResult]
    thmSMTResults (SBV.ThmResult r :: SMTResult
    r) = [SMTResult
    r]

    proverError :: String -> M.ModuleCmd (Maybe SBV.Solver, ProverResult)
    proverError :: String -> ModuleCmd (Maybe Solver, ProverResult)
    proverError msg :: String
    msg (_,modEnv :: ModuleEnv
    modEnv) =
      (Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
     [ModuleWarning])
    -> IO
         (Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
          [ModuleWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((Maybe Solver, ProverResult), ModuleEnv)
    -> Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv)
    forall a b. b -> Either a b
    Right ((Maybe Solver
    forall a. Maybe a
    Nothing, String -> ProverResult
    ProverError String
    msg), ModuleEnv
    modEnv), [])

    satProve :: ProverCommand -> M.ModuleCmd (Maybe SBV.Solver, ProverResult)
    satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)
    satProve ProverCommand {..} =
      (String -> ModuleCmd (Maybe Solver, ProverResult))
    -> ModuleCmd (Maybe Solver, ProverResult)
    -> ModuleCmd (Maybe Solver, ProverResult)
    forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack String -> ModuleCmd (Maybe Solver, ProverResult)
    proverError (ModuleCmd (Maybe Solver, ProverResult)
     -> ModuleCmd (Maybe Solver, ProverResult))
    -> ModuleCmd (Maybe Solver, ProverResult)
    -> ModuleCmd (Maybe Solver, ProverResult)
    forall a b. (a -> b) -> a -> b
    $ \(evo :: EvalOpts
    evo,modEnv :: ModuleEnv
    modEnv) ->

      (EvalOpts, ModuleEnv)
    -> ModuleM (Maybe Solver, ProverResult)
    -> IO
         (Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
          [ModuleWarning])
    forall a.
    (EvalOpts, ModuleEnv)
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    M.runModuleM (EvalOpts
    evo,ModuleEnv
    modEnv) (ModuleM (Maybe Solver, ProverResult)
     -> IO
          (Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
           [ModuleWarning]))
    -> ModuleM (Maybe Solver, ProverResult)
    -> IO
         (Either ModuleError ((Maybe Solver, ProverResult), ModuleEnv),
          [ModuleWarning])
    forall a b. (a -> b) -> a -> b
    $ do
      let (isSat :: Bool
    isSat, mSatNum :: Maybe Int
    mSatNum) = case QueryType
    pcQueryType of
            ProveQuery -> (Bool
    False, Maybe Int
    forall a. Maybe a
    Nothing)
            SatQuery sn :: SatNum
    sn -> case SatNum
    sn of
              SomeSat n :: Int
    n -> (Bool
    True, Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    n)
              AllSat    -> (Bool
    True, Maybe Int
    forall a. Maybe a
    Nothing)
      let extDgs :: [DeclGroup]
    extDgs = ModuleEnv -> [DeclGroup]
    allDeclGroups ModuleEnv
    modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ [DeclGroup]
    pcExtraDecls
      [SMTConfig]
    provers <-
        case String
    pcProverName of
          "any" -> IO [SMTConfig] -> ModuleT IO [SMTConfig]
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    M.io IO [SMTConfig]
    SBV.sbvAvailableSolvers
          _ -> [SMTConfig] -> ModuleT IO [SMTConfig]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String -> SMTConfig
    lookupProver String
    pcProverName) { transcript :: Maybe String
    SBV.transcript = Maybe String
    pcSmtFile
                                                   , allSatMaxModelCount :: Maybe Int
    SBV.allSatMaxModelCount = Maybe Int
    mSatNum
                                                   }]

      let provers' :: [SMTConfig]
    provers' = [ SMTConfig
    p { timing :: Timing
    SBV.timing = IORef ProverStats -> Timing
    SaveTiming IORef ProverStats
    pcProverStats
                         , verbose :: Bool
    SBV.verbose = Bool
    pcVerbose
                         , validateModel :: Bool
    SBV.validateModel = Bool
    pcValidate
                         } | SMTConfig
    p <- [SMTConfig]
    provers ]
      let tyFn :: FinType -> WriterT [SBool] Symbolic Value
    tyFn = if Bool
    isSat then FinType -> WriterT [SBool] Symbolic Value
    existsFinType else FinType -> WriterT [SBool] Symbolic Value
    forallFinType
      let lPutStrLn :: String -> ModuleM ()
    lPutStrLn = (Logger -> String -> IO ()) -> String -> ModuleM ()
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    M.withLogger Logger -> String -> IO ()
    logPutStrLn
      let doEval :: MonadIO m => Eval.Eval a -> m a
          doEval :: Eval a -> m a
    doEval m :: Eval a
    m  = IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> m a) -> IO a -> m a
    forall a b. (a -> b) -> a -> b
    $ EvalOpts -> Eval a -> IO a
    forall a. EvalOpts -> Eval a -> IO a
    Eval.runEval EvalOpts
    evo Eval a
    m
      let runProver :: (SMTConfig -> t -> IO t)
    -> (t -> [SMTResult])
    -> t
    -> ModuleT IO (Maybe Solver, [SMTResult])
    runProver fn :: SMTConfig -> t -> IO t
    fn tag :: t -> [SMTResult]
    tag e :: t
    e = do
            case [SMTConfig]
    provers of
              [prover :: SMTConfig
    prover] -> do
                Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $
                  String -> ModuleM ()
    lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ "Trying proof with " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                                            Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    SBV.name (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    prover))
                t
    res <- IO t -> ModuleT IO t
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    M.io (SMTConfig -> t -> IO t
    fn SMTConfig
    prover t
    e)
                Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $
                  String -> ModuleM ()
    lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ "Got result from " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                                            Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    SBV.name (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    prover))
                (Maybe Solver, [SMTResult])
    -> ModuleT IO (Maybe Solver, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solver -> Maybe Solver
    forall a. a -> Maybe a
    Just (SMTSolver -> Solver
    SBV.name (SMTConfig -> SMTSolver
    SBV.solver SMTConfig
    prover)), t -> [SMTResult]
    tag t
    res)
              _ ->
                (Maybe Solver, [SMTResult])
    -> ModuleT IO (Maybe Solver, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( Maybe Solver
    forall a. Maybe a
    Nothing
                       , [ SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
    SBV.ProofError
                             SMTConfig
    prover
                             [":sat with option prover=any requires option satNum=1"]
                             Maybe SMTResult
    forall a. Maybe a
    Nothing
                         | SMTConfig
    prover <- [SMTConfig]
    provers ]
                       )
          runProvers :: ([SMTConfig] -> t -> IO (a, ProverStats, t))
    -> (t -> b) -> t -> ModuleT IO (Maybe a, b)
    runProvers fn :: [SMTConfig] -> t -> IO (a, ProverStats, t)
    fn tag :: t -> b
    tag e :: t
    e = do
            Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $
              String -> ModuleM ()
    lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ "Trying proof with " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                      String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((SMTConfig -> String) -> [SMTConfig] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Solver -> String
    forall a. Show a => a -> String
    show (Solver -> String) -> (SMTConfig -> Solver) -> SMTConfig -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTSolver -> Solver
    SBV.name (SMTSolver -> Solver)
    -> (SMTConfig -> SMTSolver) -> SMTConfig -> Solver
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTConfig -> SMTSolver
    SBV.solver) [SMTConfig]
    provers)
            (firstProver :: a
    firstProver, timeElapsed :: ProverStats
    timeElapsed, res :: t
    res) <- IO (a, ProverStats, t) -> ModuleT IO (a, ProverStats, t)
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    M.io ([SMTConfig] -> t -> IO (a, ProverStats, t)
    fn [SMTConfig]
    provers' t
    e)
            Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $
              String -> ModuleM ()
    lPutStrLn (String -> ModuleM ()) -> String -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ "Got result from " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    firstProver String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                                                ", time: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ProverStats -> String
    showTDiff ProverStats
    timeElapsed
            (Maybe a, b) -> ModuleT IO (Maybe a, b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    firstProver, t -> b
    tag t
    res)
      let runFn :: Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult])
    runFn = case QueryType
    pcQueryType of
            ProveQuery -> ([SMTConfig]
     -> Symbolic SBool -> IO (Solver, ProverStats, ThmResult))
    -> (ThmResult -> [SMTResult])
    -> Symbolic SBool
    -> ModuleT IO (Maybe Solver, [SMTResult])
    forall a t t b.
    Show a =>
    ([SMTConfig] -> t -> IO (a, ProverStats, t))
    -> (t -> b) -> t -> ModuleT IO (Maybe a, b)
    runProvers [SMTConfig]
    -> Symbolic SBool -> IO (Solver, ProverStats, ThmResult)
    SBV.proveWithAny ThmResult -> [SMTResult]
    thmSMTResults
            SatQuery sn :: SatNum
    sn -> case SatNum
    sn of
              SomeSat 1 -> ([SMTConfig]
     -> Symbolic SBool -> IO (Solver, ProverStats, SatResult))
    -> (SatResult -> [SMTResult])
    -> Symbolic SBool
    -> ModuleT IO (Maybe Solver, [SMTResult])
    forall a t t b.
    Show a =>
    ([SMTConfig] -> t -> IO (a, ProverStats, t))
    -> (t -> b) -> t -> ModuleT IO (Maybe a, b)
    runProvers [SMTConfig]
    -> Symbolic SBool -> IO (Solver, ProverStats, SatResult)
    SBV.satWithAny SatResult -> [SMTResult]
    satSMTResults
              _         -> (SMTConfig -> Symbolic SBool -> IO AllSatResult)
    -> (AllSatResult -> [SMTResult])
    -> Symbolic SBool
    -> ModuleT IO (Maybe Solver, [SMTResult])
    forall t t.
    (SMTConfig -> t -> IO t)
    -> (t -> [SMTResult])
    -> t
    -> ModuleT IO (Maybe Solver, [SMTResult])
    runProver SMTConfig -> Symbolic SBool -> IO AllSatResult
    SBV.allSatWith AllSatResult -> [SMTResult]
    allSatSMTResults
      let addAsm :: SBool -> SBool -> SBool
    addAsm = case QueryType
    pcQueryType of
            ProveQuery -> \x :: SBool
    x y :: SBool
    y -> SBool -> SBool -> SBool
    SBV.svOr (SBool -> SBool
    SBV.svNot SBool
    x) SBool
    y
            SatQuery _ -> \x :: SBool
    x y :: SBool
    y -> SBool -> SBool -> SBool
    SBV.svAnd SBool
    x SBool
    y
      case Schema -> Either String [FinType]
    predArgTypes Schema
    pcSchema of
        Left msg :: String
    msg -> (Maybe Solver, ProverResult)
    -> ModuleM (Maybe Solver, ProverResult)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Solver
    forall a. Maybe a
    Nothing, String -> ProverResult
    ProverError String
    msg)
        Right ts :: [FinType]
    ts -> do Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ String -> ModuleM ()
    lPutStrLn "Simulating..."
                       Value
    v <- Eval Value -> ModuleT IO Value
    forall (m :: * -> *) a. MonadIO m => Eval a -> m a
    doEval (Eval Value -> ModuleT IO Value) -> Eval Value -> ModuleT IO Value
    forall a b. (a -> b) -> a -> b
    $ do GenEvalEnv SBool SBool SBool
    env <- [DeclGroup]
    -> GenEvalEnv SBool SBool SBool
    -> Eval (GenEvalEnv SBool SBool SBool)
    forall b w i.
    EvalPrims b w i =>
    [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    Eval.evalDecls [DeclGroup]
    extDgs GenEvalEnv SBool SBool SBool
    forall a. Monoid a => a
    mempty
                                        GenEvalEnv SBool SBool SBool -> Expr -> Eval Value
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    Eval.evalExpr GenEvalEnv SBool SBool SBool
    env Expr
    pcExpr
                       PrimMap
    prims <- ModuleM PrimMap
    M.getPrimMap
                       (Maybe Solver, [SMTResult])
    runRes <- Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult])
    runFn (Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult]))
    -> Symbolic SBool -> ModuleT IO (Maybe Solver, [SMTResult])
    forall a b. (a -> b) -> a -> b
    $ do
                                   (args :: [Value]
    args, asms :: [SBool]
    asms) <- WriterT [SBool] Symbolic [Value] -> Symbolic ([Value], [SBool])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT ((FinType -> WriterT [SBool] Symbolic Value)
    -> [FinType] -> WriterT [SBool] Symbolic [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM FinType -> WriterT [SBool] Symbolic Value
    tyFn [FinType]
    ts)
                                   SBool
    b <- Eval SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => Eval a -> m a
    doEval (Value -> SBool
    forall b w i. GenValue b w i -> b
    fromVBit (Value -> SBool) -> Eval Value -> Eval SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                                          (Value -> Eval Value -> Eval Value)
    -> Value -> [Eval Value] -> Eval Value
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM Value -> Eval Value -> Eval Value
    forall b w i.
    GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    fromVFun Value
    v ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    args))
                                   SBool -> Symbolic SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SBool -> SBool -> SBool
    addAsm SBool
    b [SBool]
    asms)
                       let (firstProver :: Maybe Solver
    firstProver, results :: [SMTResult]
    results) = (Maybe Solver, [SMTResult])
    runRes
                       ProverResult
    esatexprs <- case [SMTResult]
    results of
                         -- allSat can return more than one as long as
                         -- they're satisfiable
                         (SBV.Satisfiable {} : _) -> do
                           [[(Type, Expr, Value)]]
    tevss <- (SMTResult -> ModuleT IO [(Type, Expr, Value)])
    -> [SMTResult] -> ModuleT IO [[(Type, Expr, Value)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SMTResult -> ModuleT IO [(Type, Expr, Value)]
    forall (m :: * -> *).
    MonadIO m =>
    SMTResult -> m [(Type, Expr, Value)]
    mkTevs [SMTResult]
    results
                           ProverResult -> ModuleT IO ProverResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ [[(Type, Expr, Value)]] -> ProverResult
    AllSatResult [[(Type, Expr, Value)]]
    tevss
                           where
                             mkTevs :: SMTResult -> m [(Type, Expr, Value)]
    mkTevs result :: SMTResult
    result = do
                               let Right (_, cvs :: [CV]
    cvs) = SMTResult -> Either String (Bool, [CV])
    SBV.getModelAssignment SMTResult
    result
                                   (vs :: [Value]
    vs, _) = [FinType] -> [CV] -> ([Value], [CV])
    parseValues [FinType]
    ts [CV]
    cvs
                                   sattys :: [Type]
    sattys = FinType -> Type
    unFinType (FinType -> Type) -> [FinType] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ts
                               [Maybe Expr]
    satexprs <-
                                 Eval [Maybe Expr] -> m [Maybe Expr]
    forall (m :: * -> *) a. MonadIO m => Eval a -> m a
    doEval ((Type -> Value -> Eval (Maybe Expr))
    -> [Type] -> [Value] -> Eval [Maybe Expr]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (PrimMap -> Type -> Value -> Eval (Maybe Expr)
    Eval.toExpr PrimMap
    prims) [Type]
    sattys [Value]
    vs)
                               case [Type] -> [Expr] -> [Value] -> [(Type, Expr, Value)]
    forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
    zip3 [Type]
    sattys ([Expr] -> [Value] -> [(Type, Expr, Value)])
    -> Maybe [Expr] -> Maybe ([Value] -> [(Type, Expr, Value)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Maybe Expr] -> Maybe [Expr]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [Maybe Expr]
    satexprs) Maybe ([Value] -> [(Type, Expr, Value)])
    -> Maybe [Value] -> Maybe [(Type, Expr, Value)]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Value] -> Maybe [Value]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Value]
    vs of
                                 Nothing ->
                                   String -> [String] -> m [(Type, Expr, Value)]
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.Symbolic.sat"
                                     [ "unable to make assignment into expression" ]
                                 Just tevs :: [(Type, Expr, Value)]
    tevs -> [(Type, Expr, Value)] -> m [(Type, Expr, Value)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Type, Expr, Value)] -> m [(Type, Expr, Value)])
    -> [(Type, Expr, Value)] -> m [(Type, Expr, Value)]
    forall a b. (a -> b) -> a -> b
    $ [(Type, Expr, Value)]
    tevs
                         -- prove returns only one
                         [SBV.Unsatisfiable {}] ->
                           ProverResult -> ModuleT IO ProverResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ [Type] -> ProverResult
    ThmResult (FinType -> Type
    unFinType (FinType -> Type) -> [FinType] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ts)
                         -- unsat returns empty
                         [] -> ProverResult -> ModuleT IO ProverResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ [Type] -> ProverResult
    ThmResult (FinType -> Type
    unFinType (FinType -> Type) -> [FinType] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ts)
                         -- otherwise something is wrong
                         _ -> ProverResult -> ModuleT IO ProverResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProverResult -> ModuleT IO ProverResult)
    -> ProverResult -> ModuleT IO ProverResult
    forall a b. (a -> b) -> a -> b
    $ String -> ProverResult
    ProverError ([SMTResult] -> String
    rshow [SMTResult]
    results)
                                where rshow :: [SMTResult] -> String
    rshow | Bool
    isSat = AllSatResult -> String
    forall a. Show a => a -> String
    show (AllSatResult -> String)
    -> ([SMTResult] -> AllSatResult) -> [SMTResult] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .  (Bool, Bool, Bool, [SMTResult]) -> AllSatResult
    SBV.AllSatResult ((Bool, Bool, Bool, [SMTResult]) -> AllSatResult)
    -> ([SMTResult] -> (Bool, Bool, Bool, [SMTResult]))
    -> [SMTResult]
    -> AllSatResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool
    False,Bool
    False,Bool
    False,)
                                            | Bool
    otherwise = ThmResult -> String
    forall a. Show a => a -> String
    show (ThmResult -> String)
    -> ([SMTResult] -> ThmResult) -> [SMTResult] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTResult -> ThmResult
    SBV.ThmResult (SMTResult -> ThmResult)
    -> ([SMTResult] -> SMTResult) -> [SMTResult] -> ThmResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [SMTResult] -> SMTResult
    forall a. [a] -> a
    head
                       (Maybe Solver, ProverResult)
    -> ModuleM (Maybe Solver, ProverResult)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Solver
    firstProver, ProverResult
    esatexprs)

    satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
    satProveOffline :: ProverCommand -> ModuleCmd (Either String String)
    satProveOffline ProverCommand {..} =
      (String -> ModuleCmd (Either String String))
    -> ModuleCmd (Either String String)
    -> ModuleCmd (Either String String)
    forall a. (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack (\msg :: String
    msg (_,modEnv :: ModuleEnv
    modEnv) -> (Either ModuleError (Either String String, ModuleEnv),
     [ModuleWarning])
    -> IO
         (Either ModuleError (Either String String, ModuleEnv),
          [ModuleWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Either String String, ModuleEnv)
    -> Either ModuleError (Either String String, ModuleEnv)
    forall a b. b -> Either a b
    Right (String -> Either String String
    forall a b. a -> Either a b
    Left String
    msg, ModuleEnv
    modEnv), [])) (ModuleCmd (Either String String)
     -> ModuleCmd (Either String String))
    -> ModuleCmd (Either String String)
    -> ModuleCmd (Either String String)
    forall a b. (a -> b) -> a -> b
    $
      \(evOpts :: EvalOpts
    evOpts,modEnv :: ModuleEnv
    modEnv) -> do
        let isSat :: Bool
    isSat = case QueryType
    pcQueryType of
              ProveQuery -> Bool
    False
              SatQuery _ -> Bool
    True
        let extDgs :: [DeclGroup]
    extDgs = ModuleEnv -> [DeclGroup]
    allDeclGroups ModuleEnv
    modEnv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ [DeclGroup]
    pcExtraDecls
        let tyFn :: FinType -> WriterT [SBool] Symbolic Value
    tyFn = if Bool
    isSat then FinType -> WriterT [SBool] Symbolic Value
    existsFinType else FinType -> WriterT [SBool] Symbolic Value
    forallFinType
        let addAsm :: SBool -> SBool -> SBool
    addAsm = if Bool
    isSat then SBool -> SBool -> SBool
    SBV.svAnd else \x :: SBool
    x y :: SBool
    y -> SBool -> SBool -> SBool
    SBV.svOr (SBool -> SBool
    SBV.svNot SBool
    x) SBool
    y
        case Schema -> Either String [FinType]
    predArgTypes Schema
    pcSchema of
          Left msg :: String
    msg -> (Either ModuleError (Either String String, ModuleEnv),
     [ModuleWarning])
    -> IO
         (Either ModuleError (Either String String, ModuleEnv),
          [ModuleWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Either String String, ModuleEnv)
    -> Either ModuleError (Either String String, ModuleEnv)
    forall a b. b -> Either a b
    Right (String -> Either String String
    forall a b. a -> Either a b
    Left String
    msg, ModuleEnv
    modEnv), [])
          Right ts :: [FinType]
    ts ->
            do Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    pcVerbose (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Logger -> String -> IO ()
    logPutStrLn (EvalOpts -> Logger
    Eval.evalLogger EvalOpts
    evOpts) "Simulating..."
               Value
    v <- IO Value -> IO Value
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Value -> IO Value) -> IO Value -> IO Value
    forall a b. (a -> b) -> a -> b
    $ EvalOpts -> Eval Value -> IO Value
    forall a. EvalOpts -> Eval a -> IO a
    Eval.runEval EvalOpts
    evOpts (Eval Value -> IO Value) -> Eval Value -> IO Value
    forall a b. (a -> b) -> a -> b
    $
                       do GenEvalEnv SBool SBool SBool
    env <- [DeclGroup]
    -> GenEvalEnv SBool SBool SBool
    -> Eval (GenEvalEnv SBool SBool SBool)
    forall b w i.
    EvalPrims b w i =>
    [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    Eval.evalDecls [DeclGroup]
    extDgs GenEvalEnv SBool SBool SBool
    forall a. Monoid a => a
    mempty
                          GenEvalEnv SBool SBool SBool -> Expr -> Eval Value
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    Eval.evalExpr GenEvalEnv SBool SBool SBool
    env Expr
    pcExpr
               String
    smtlib <- Bool -> Symbolic SBool -> IO String
    SBV.generateSMTBenchmark Bool
    isSat (Symbolic SBool -> IO String) -> Symbolic SBool -> IO String
    forall a b. (a -> b) -> a -> b
    $ do
                 (args :: [Value]
    args, asms :: [SBool]
    asms) <- WriterT [SBool] Symbolic [Value] -> Symbolic ([Value], [SBool])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT ((FinType -> WriterT [SBool] Symbolic Value)
    -> [FinType] -> WriterT [SBool] Symbolic [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM FinType -> WriterT [SBool] Symbolic Value
    tyFn [FinType]
    ts)
                 SBool
    b <- IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool) -> IO SBool -> Symbolic SBool
    forall a b. (a -> b) -> a -> b
    $ EvalOpts -> Eval SBool -> IO SBool
    forall a. EvalOpts -> Eval a -> IO a
    Eval.runEval EvalOpts
    evOpts
                            (Value -> SBool
    forall b w i. GenValue b w i -> b
    fromVBit (Value -> SBool) -> Eval Value -> Eval SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Eval Value -> Eval Value)
    -> Value -> [Eval Value] -> Eval Value
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM Value -> Eval Value -> Eval Value
    forall b w i.
    GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    fromVFun Value
    v ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    args))
                 SBool -> Symbolic SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SBool -> SBool -> SBool
    addAsm SBool
    b [SBool]
    asms)
               (Either ModuleError (Either String String, ModuleEnv),
     [ModuleWarning])
    -> IO
         (Either ModuleError (Either String String, ModuleEnv),
          [ModuleWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Either String String, ModuleEnv)
    -> Either ModuleError (Either String String, ModuleEnv)
    forall a b. b -> Either a b
    Right (String -> Either String String
    forall a b. b -> Either a b
    Right String
    smtlib, ModuleEnv
    modEnv), [])

    protectStack :: (String -> M.ModuleCmd a)
                 -> M.ModuleCmd a
                 -> M.ModuleCmd a
    protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a
    protectStack mkErr :: String -> ModuleCmd a
    mkErr cmd :: ModuleCmd a
    cmd modEnv :: (EvalOpts, ModuleEnv)
    modEnv =
      (AsyncException -> Maybe ())
    -> IO (ModuleRes a) -> (() -> IO (ModuleRes a)) -> IO (ModuleRes a)
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    X.catchJust AsyncException -> Maybe ()
    isOverflow (ModuleCmd a
    cmd (EvalOpts, ModuleEnv)
    modEnv) () -> IO (ModuleRes a)
    handler
      where isOverflow :: AsyncException -> Maybe ()
    isOverflow X.StackOverflow = () -> Maybe ()
    forall a. a -> Maybe a
    Just ()
            isOverflow _               = Maybe ()
    forall a. Maybe a
    Nothing
            msg :: String
    msg = "Symbolic evaluation failed to terminate."
            handler :: () -> IO (ModuleRes a)
    handler () = String -> ModuleCmd a
    mkErr String
    msg (EvalOpts, ModuleEnv)
    modEnv

    parseValues :: [FinType] -> [SBV.CV] -> ([Eval.Value], [SBV.CV])
    parseValues :: [FinType] -> [CV] -> ([Value], [CV])
    parseValues [] cvs :: [CV]
    cvs = ([], [CV]
    cvs)
    parseValues (t :: FinType
    t : ts :: [FinType]
    ts) cvs :: [CV]
    cvs = (Value
    v Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : [Value]
    vs, [CV]
    cvs'')
      where (v :: Value
    v, cvs' :: [CV]
    cvs') = FinType -> [CV] -> (Value, [CV])
    parseValue FinType
    t [CV]
    cvs
            (vs :: [Value]
    vs, cvs'' :: [CV]
    cvs'') = [FinType] -> [CV] -> ([Value], [CV])
    parseValues [FinType]
    ts [CV]
    cvs'

    parseValue :: FinType -> [SBV.CV] -> (Eval.Value, [SBV.CV])
    parseValue :: FinType -> [CV] -> (Value, [CV])
    parseValue FTBit [] = String -> [String] -> (Value, [CV])
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
    parseValue FTBit (cv :: CV
    cv : cvs :: [CV]
    cvs) = (Bool -> Value
    forall b w i. b -> GenValue b w i
    Eval.VBit (CV -> Bool
    SBV.cvToBool CV
    cv), [CV]
    cvs)
    parseValue FTInteger cvs :: [CV]
    cvs =
      case Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    SBV.genParse Kind
    SBV.KUnbounded [CV]
    cvs of
        Just (x :: Integer
    x, cvs' :: [CV]
    cvs') -> (Integer -> Value
    forall b w i. i -> GenValue b w i
    Eval.VInteger Integer
    x, [CV]
    cvs')
        Nothing        -> String -> [String] -> (Value, [CV])
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.Symbolic.parseValue" [ "no integer" ]
    parseValue (FTIntMod _) cvs :: [CV]
    cvs = FinType -> [CV] -> (Value, [CV])
    parseValue FinType
    FTInteger [CV]
    cvs
    parseValue (FTSeq 0 FTBit) cvs :: [CV]
    cvs = (Integer -> Integer -> Value
    forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
    Eval.word 0 0, [CV]
    cvs)
    parseValue (FTSeq n :: Int
    n FTBit) cvs :: [CV]
    cvs =
      case Kind -> [CV] -> Maybe (Integer, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    SBV.genParse (Bool -> Int -> Kind
    SBV.KBounded Bool
    False Int
    n) [CV]
    cvs of
        Just (x :: Integer
    x, cvs' :: [CV]
    cvs') -> (Integer -> Integer -> Value
    forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
    Eval.word (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n) Integer
    x, [CV]
    cvs')
        Nothing        -> (Integer -> Eval (WordValue Bool BV Integer) -> Value
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord ([Value] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Value]
    vs) (Eval (WordValue Bool BV Integer) -> Value)
    -> Eval (WordValue Bool BV Integer) -> Value
    forall a b. (a -> b) -> a -> b
    $ WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer))
    -> WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
    forall a b. (a -> b) -> a -> b
    $ BV -> WordValue Bool BV Integer
    forall b w i. w -> WordValue b w i
    Eval.WordVal (BV -> WordValue Bool BV Integer)
    -> BV -> WordValue Bool BV Integer
    forall a b. (a -> b) -> a -> b
    $
                             [Bool] -> BV
    forall b w i. BitWord b w i => [b] -> w
    Eval.packWord ((Value -> Bool) -> [Value] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Bool
    forall b w i. GenValue b w i -> b
    fromVBit [Value]
    vs), [CV]
    cvs')
          where (vs :: [Value]
    vs, cvs' :: [CV]
    cvs') = [FinType] -> [CV] -> ([Value], [CV])
    parseValues (Int -> FinType -> [FinType]
    forall a. Int -> a -> [a]
    replicate Int
    n FinType
    FTBit) [CV]
    cvs
    parseValue (FTSeq n :: Int
    n t :: FinType
    t) cvs :: [CV]
    cvs =
                          (Integer -> SeqMap Bool BV Integer -> Value
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    Eval.VSeq (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n) (SeqMap Bool BV Integer -> Value)
    -> SeqMap Bool BV Integer -> Value
    forall a b. (a -> b) -> a -> b
    $ [Eval Value] -> SeqMap Bool BV Integer
    forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
    Eval.finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    vs)
                          , [CV]
    cvs'
                          )
      where (vs :: [Value]
    vs, cvs' :: [CV]
    cvs') = [FinType] -> [CV] -> ([Value], [CV])
    parseValues (Int -> FinType -> [FinType]
    forall a. Int -> a -> [a]
    replicate Int
    n FinType
    t) [CV]
    cvs
    parseValue (FTTuple ts :: [FinType]
    ts) cvs :: [CV]
    cvs = ([Eval Value] -> Value
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    Eval.VTuple ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    vs), [CV]
    cvs')
      where (vs :: [Value]
    vs, cvs' :: [CV]
    cvs') = [FinType] -> [CV] -> ([Value], [CV])
    parseValues [FinType]
    ts [CV]
    cvs
    parseValue (FTRecord fs :: [(Ident, FinType)]
    fs) cvs :: [CV]
    cvs = ([(Ident, Eval Value)] -> Value
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    Eval.VRecord ([Ident] -> [Eval Value] -> [(Ident, Eval Value)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Ident]
    ns ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    vs)), [CV]
    cvs')
      where (ns :: [Ident]
    ns, ts :: [FinType]
    ts) = [(Ident, FinType)] -> ([Ident], [FinType])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Ident, FinType)]
    fs
            (vs :: [Value]
    vs, cvs' :: [CV]
    cvs') = [FinType] -> [CV] -> ([Value], [CV])
    parseValues [FinType]
    ts [CV]
    cvs

    allDeclGroups :: M.ModuleEnv -> [DeclGroup]
    allDeclGroups :: ModuleEnv -> [DeclGroup]
    allDeclGroups = (Module -> [DeclGroup]) -> [Module] -> [DeclGroup]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Module -> [DeclGroup]
    mDecls ([Module] -> [DeclGroup])
    -> (ModuleEnv -> [Module]) -> ModuleEnv -> [DeclGroup]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleEnv -> [Module]
    M.loadedNonParamModules

    data FinType
        = FTBit
        | FTInteger
        | FTIntMod Integer
        | FTSeq Int FinType
        | FTTuple [FinType]
        | FTRecord [(Ident, FinType)]

    numType :: Integer -> Maybe Int
    numType :: Integer -> Maybe Int
    numType n :: Integer
    n
      | 0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n Bool -> Bool -> Bool
    && Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    forall a. Bounded a => a
    maxBound :: Int) = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
      | Bool
    otherwise = Maybe Int
    forall a. Maybe a
    Nothing

    finType :: TValue -> Maybe FinType
    finType :: TValue -> Maybe FinType
    finType ty :: TValue
    ty =
      case TValue
    ty of
        Eval.TVBit            -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just FinType
    FTBit
        Eval.TVInteger        -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just FinType
    FTInteger
        Eval.TVIntMod n :: Integer
    n       -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just (Integer -> FinType
    FTIntMod Integer
    n)
        Eval.TVSeq n :: Integer
    n t :: TValue
    t        -> Int -> FinType -> FinType
    FTSeq (Int -> FinType -> FinType)
    -> Maybe Int -> Maybe (FinType -> FinType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Maybe Int
    numType Integer
    n Maybe (FinType -> FinType) -> Maybe FinType -> Maybe FinType
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TValue -> Maybe FinType
    finType TValue
    t
        Eval.TVTuple ts :: [TValue]
    ts       -> [FinType] -> FinType
    FTTuple ([FinType] -> FinType) -> Maybe [FinType] -> Maybe FinType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> Maybe FinType) -> [TValue] -> Maybe [FinType]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse TValue -> Maybe FinType
    finType [TValue]
    ts
        Eval.TVRec fields :: [(Ident, TValue)]
    fields     -> [(Ident, FinType)] -> FinType
    FTRecord ([(Ident, FinType)] -> FinType)
    -> Maybe [(Ident, FinType)] -> Maybe FinType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Ident, TValue) -> Maybe (Ident, FinType))
    -> [(Ident, TValue)] -> Maybe [(Ident, FinType)]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((TValue -> Maybe FinType)
    -> (Ident, TValue) -> Maybe (Ident, FinType)
    forall (f :: * -> *) a b t.
    Functor f =>
    (a -> f b) -> (t, a) -> f (t, b)
    traverseSnd TValue -> Maybe FinType
    finType) [(Ident, TValue)]
    fields
        Eval.TVAbstract {}    -> Maybe FinType
    forall a. Maybe a
    Nothing
        _                     -> Maybe FinType
    forall a. Maybe a
    Nothing

    unFinType :: FinType -> Type
    unFinType :: FinType -> Type
    unFinType fty :: FinType
    fty =
      case FinType
    fty of
        FTBit        -> Type
    tBit
        FTInteger    -> Type
    tInteger
        FTIntMod n :: Integer
    n   -> Type -> Type
    tIntMod (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n)
        FTSeq l :: Int
    l ety :: FinType
    ety  -> Type -> Type -> Type
    tSeq (Int -> Type
    forall a. Integral a => a -> Type
    tNum Int
    l) (FinType -> Type
    unFinType FinType
    ety)
        FTTuple ftys :: [FinType]
    ftys -> [Type] -> Type
    tTuple (FinType -> Type
    unFinType (FinType -> Type) -> [FinType] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ftys)
        FTRecord fs :: [(Ident, FinType)]
    fs  -> [(Ident, Type)] -> Type
    tRec ([Ident] -> [Type] -> [(Ident, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Ident]
    fns [Type]
    tys)
          where
            fns :: [Ident]
    fns = (Ident, FinType) -> Ident
    forall a b. (a, b) -> a
    fst ((Ident, FinType) -> Ident) -> [(Ident, FinType)] -> [Ident]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Ident, FinType)]
    fs
            tys :: [Type]
    tys = FinType -> Type
    unFinType (FinType -> Type)
    -> ((Ident, FinType) -> FinType) -> (Ident, FinType) -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, FinType) -> FinType
    forall a b. (a, b) -> b
    snd ((Ident, FinType) -> Type) -> [(Ident, FinType)] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Ident, FinType)]
    fs

    predArgTypes :: Schema -> Either String [FinType]
    predArgTypes :: Schema -> Either String [FinType]
    predArgTypes schema :: Schema
    schema@(Forall ts :: [TParam]
    ts ps :: [Type]
    ps ty :: Type
    ty)
      | [TParam] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TParam]
    ts Bool -> Bool -> Bool
    && [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Type]
    ps =
          case TValue -> Maybe [FinType]
    go (TValue -> Maybe [FinType])
    -> Either Nat' TValue -> Either Nat' (Maybe [FinType])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (HasCallStack => TypeEnv -> Type -> Either Nat' TValue
    TypeEnv -> Type -> Either Nat' TValue
    Eval.evalType TypeEnv
    forall a. Monoid a => a
    mempty Type
    ty) of
            Right (Just fts :: [FinType]
    fts) -> [FinType] -> Either String [FinType]
    forall a b. b -> Either a b
    Right [FinType]
    fts
            _ -> String -> Either String [FinType]
    forall a b. a -> Either a b
    Left (String -> Either String [FinType])
    -> String -> Either String [FinType]
    forall a b. (a -> b) -> a -> b
    $ "Not a valid predicate type:\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    schema)
      | Bool
    otherwise = String -> Either String [FinType]
    forall a b. a -> Either a b
    Left (String -> Either String [FinType])
    -> String -> Either String [FinType]
    forall a b. (a -> b) -> a -> b
    $ "Not a monomorphic type:\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    schema)
      where
        go :: TValue -> Maybe [FinType]
        go :: TValue -> Maybe [FinType]
    go Eval.TVBit             = [FinType] -> Maybe [FinType]
    forall a. a -> Maybe a
    Just []
        go (Eval.TVFun ty1 :: TValue
    ty1 ty2 :: TValue
    ty2)   = (:) (FinType -> [FinType] -> [FinType])
    -> Maybe FinType -> Maybe ([FinType] -> [FinType])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TValue -> Maybe FinType
    finType TValue
    ty1 Maybe ([FinType] -> [FinType])
    -> Maybe [FinType] -> Maybe [FinType]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TValue -> Maybe [FinType]
    go TValue
    ty2
        go _                      = Maybe [FinType]
    forall a. Maybe a
    Nothing

    inBoundsIntMod :: Integer -> SInteger -> SBool
    inBoundsIntMod :: Integer -> SBool -> SBool
    inBoundsIntMod n :: Integer
    n x :: SBool
    x =
      SBool -> SBool -> SBool
    SBV.svAnd (SBool -> SBool -> SBool
    SBV.svLessEq (Integer -> SBool
    forall b w i. BitWord b w i => Integer -> i
    Eval.integerLit 0) SBool
    x) (SBool -> SBool -> SBool
    SBV.svLessThan SBool
    x (Integer -> SBool
    forall b w i. BitWord b w i => Integer -> i
    Eval.integerLit Integer
    n))

    forallFinType :: FinType -> WriterT [SBool] SBV.Symbolic Value
    forallFinType :: FinType -> WriterT [SBool] Symbolic Value
    forallFinType ty :: FinType
    ty =
      case FinType
    ty of
        FTBit         -> SBool -> Value
    forall b w i. b -> GenValue b w i
    VBit (SBool -> Value)
    -> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Symbolic SBool
    forallSBool_
        FTInteger     -> SBool -> Value
    forall b w i. i -> GenValue b w i
    VInteger (SBool -> Value)
    -> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Symbolic SBool
    forallSInteger_
        FTIntMod n :: Integer
    n    -> do SBool
    x <- Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Symbolic SBool
    forallSInteger_
                            [SBool] -> WriterT [SBool] Symbolic ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Integer -> SBool -> SBool
    inBoundsIntMod Integer
    n SBool
    x]
                            Value -> WriterT [SBool] Symbolic Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Value
    forall b w i. i -> GenValue b w i
    VInteger SBool
    x)
        FTSeq 0 FTBit -> Value -> WriterT [SBool] Symbolic Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> WriterT [SBool] Symbolic Value)
    -> Value -> WriterT [SBool] Symbolic Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> Value
    forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
    Eval.word 0 0
        FTSeq n :: Int
    n FTBit -> Integer -> Eval (WordValue SBool SBool SBool) -> Value
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n) (Eval (WordValue SBool SBool SBool) -> Value)
    -> (SBool -> Eval (WordValue SBool SBool SBool)) -> SBool -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
    -> (SBool -> WordValue SBool SBool SBool)
    -> SBool
    -> Eval (WordValue SBool SBool SBool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBool -> WordValue SBool SBool SBool
    forall b w i. w -> WordValue b w i
    Eval.WordVal (SBool -> Value)
    -> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Int -> Symbolic SBool
    forallBV_ Int
    n)
        FTSeq n :: Int
    n t :: FinType
    t     -> do [Value]
    vs <- Int
    -> WriterT [SBool] Symbolic Value
    -> WriterT [SBool] Symbolic [Value]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    n (FinType -> WriterT [SBool] Symbolic Value
    forallFinType FinType
    t)
                            Value -> WriterT [SBool] Symbolic Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> WriterT [SBool] Symbolic Value)
    -> Value -> WriterT [SBool] Symbolic Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap SBool SBool SBool -> Value
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n) (SeqMap SBool SBool SBool -> Value)
    -> SeqMap SBool SBool SBool -> Value
    forall a b. (a -> b) -> a -> b
    $ [Eval Value] -> SeqMap SBool SBool SBool
    forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
    Eval.finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    vs)
        FTTuple ts :: [FinType]
    ts    -> [Eval Value] -> Value
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ([Eval Value] -> Value)
    -> WriterT [SBool] Symbolic [Eval Value]
    -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FinType -> WriterT [SBool] Symbolic (Eval Value))
    -> [FinType] -> WriterT [SBool] Symbolic [Eval Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Value -> Eval Value)
    -> WriterT [SBool] Symbolic Value
    -> WriterT [SBool] Symbolic (Eval Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready (WriterT [SBool] Symbolic Value
     -> WriterT [SBool] Symbolic (Eval Value))
    -> (FinType -> WriterT [SBool] Symbolic Value)
    -> FinType
    -> WriterT [SBool] Symbolic (Eval Value)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FinType -> WriterT [SBool] Symbolic Value
    forallFinType) [FinType]
    ts
        FTRecord fs :: [(Ident, FinType)]
    fs   -> [(Ident, Eval Value)] -> Value
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord ([(Ident, Eval Value)] -> Value)
    -> WriterT [SBool] Symbolic [(Ident, Eval Value)]
    -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value))
    -> [(Ident, FinType)]
    -> WriterT [SBool] Symbolic [(Ident, Eval Value)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((FinType -> WriterT [SBool] Symbolic (Eval Value))
    -> (Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value)
    forall (f :: * -> *) a b t.
    Functor f =>
    (a -> f b) -> (t, a) -> f (t, b)
    traverseSnd ((Value -> Eval Value)
    -> WriterT [SBool] Symbolic Value
    -> WriterT [SBool] Symbolic (Eval Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready (WriterT [SBool] Symbolic Value
     -> WriterT [SBool] Symbolic (Eval Value))
    -> (FinType -> WriterT [SBool] Symbolic Value)
    -> FinType
    -> WriterT [SBool] Symbolic (Eval Value)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FinType -> WriterT [SBool] Symbolic Value
    forallFinType)) [(Ident, FinType)]
    fs

    existsFinType :: FinType -> WriterT [SBool] SBV.Symbolic Value
    existsFinType :: FinType -> WriterT [SBool] Symbolic Value
    existsFinType ty :: FinType
    ty =
      case FinType
    ty of
        FTBit         -> SBool -> Value
    forall b w i. b -> GenValue b w i
    VBit (SBool -> Value)
    -> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Symbolic SBool
    existsSBool_
        FTInteger     -> SBool -> Value
    forall b w i. i -> GenValue b w i
    VInteger (SBool -> Value)
    -> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Symbolic SBool
    existsSInteger_
        FTIntMod n :: Integer
    n    -> do SBool
    x <- Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift Symbolic SBool
    existsSInteger_
                            [SBool] -> WriterT [SBool] Symbolic ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Integer -> SBool -> SBool
    inBoundsIntMod Integer
    n SBool
    x]
                            Value -> WriterT [SBool] Symbolic Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Value
    forall b w i. i -> GenValue b w i
    VInteger SBool
    x)
        FTSeq 0 FTBit -> Value -> WriterT [SBool] Symbolic Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> WriterT [SBool] Symbolic Value)
    -> Value -> WriterT [SBool] Symbolic Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> Value
    forall b w i. BitWord b w i => Integer -> Integer -> GenValue b w i
    Eval.word 0 0
        FTSeq n :: Int
    n FTBit -> Integer -> Eval (WordValue SBool SBool SBool) -> Value
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n) (Eval (WordValue SBool SBool SBool) -> Value)
    -> (SBool -> Eval (WordValue SBool SBool SBool)) -> SBool -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
    -> (SBool -> WordValue SBool SBool SBool)
    -> SBool
    -> Eval (WordValue SBool SBool SBool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBool -> WordValue SBool SBool SBool
    forall b w i. w -> WordValue b w i
    Eval.WordVal (SBool -> Value)
    -> WriterT [SBool] Symbolic SBool -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Symbolic SBool -> WriterT [SBool] Symbolic SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Int -> Symbolic SBool
    existsBV_ Int
    n)
        FTSeq n :: Int
    n t :: FinType
    t     -> do [Value]
    vs <- Int
    -> WriterT [SBool] Symbolic Value
    -> WriterT [SBool] Symbolic [Value]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    n (FinType -> WriterT [SBool] Symbolic Value
    existsFinType FinType
    t)
                            Value -> WriterT [SBool] Symbolic Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> WriterT [SBool] Symbolic Value)
    -> Value -> WriterT [SBool] Symbolic Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap SBool SBool SBool -> Value
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n) (SeqMap SBool SBool SBool -> Value)
    -> SeqMap SBool SBool SBool -> Value
    forall a b. (a -> b) -> a -> b
    $ [Eval Value] -> SeqMap SBool SBool SBool
    forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
    Eval.finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready [Value]
    vs)
        FTTuple ts :: [FinType]
    ts    -> [Eval Value] -> Value
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ([Eval Value] -> Value)
    -> WriterT [SBool] Symbolic [Eval Value]
    -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FinType -> WriterT [SBool] Symbolic (Eval Value))
    -> [FinType] -> WriterT [SBool] Symbolic [Eval Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Value -> Eval Value)
    -> WriterT [SBool] Symbolic Value
    -> WriterT [SBool] Symbolic (Eval Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready (WriterT [SBool] Symbolic Value
     -> WriterT [SBool] Symbolic (Eval Value))
    -> (FinType -> WriterT [SBool] Symbolic Value)
    -> FinType
    -> WriterT [SBool] Symbolic (Eval Value)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FinType -> WriterT [SBool] Symbolic Value
    existsFinType) [FinType]
    ts
        FTRecord fs :: [(Ident, FinType)]
    fs   -> [(Ident, Eval Value)] -> Value
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord ([(Ident, Eval Value)] -> Value)
    -> WriterT [SBool] Symbolic [(Ident, Eval Value)]
    -> WriterT [SBool] Symbolic Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value))
    -> [(Ident, FinType)]
    -> WriterT [SBool] Symbolic [(Ident, Eval Value)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((FinType -> WriterT [SBool] Symbolic (Eval Value))
    -> (Ident, FinType) -> WriterT [SBool] Symbolic (Ident, Eval Value)
    forall (f :: * -> *) a b t.
    Functor f =>
    (a -> f b) -> (t, a) -> f (t, b)
    traverseSnd ((Value -> Eval Value)
    -> WriterT [SBool] Symbolic Value
    -> WriterT [SBool] Symbolic (Eval Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Eval Value
    forall a. a -> Eval a
    Eval.ready (WriterT [SBool] Symbolic Value
     -> WriterT [SBool] Symbolic (Eval Value))
    -> (FinType -> WriterT [SBool] Symbolic Value)
    -> FinType
    -> WriterT [SBool] Symbolic (Eval Value)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FinType -> WriterT [SBool] Symbolic Value
    existsFinType)) [(Ident, FinType)]
    fs