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