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

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.Symbolic.What4
 ( W4ProverConfig
 , defaultProver
 , proverNames
 , setupProver
 , satProve
 , satProveOffline
 , W4Exception(..)
 ) where

import Control.Concurrent.Async
import Control.Monad.IO.Class
import Control.Monad (when, foldM, forM_)
import qualified Control.Exception as X
import System.IO (Handle)
import Data.Time
import Data.IORef
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NE
import System.Exit

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 qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Concrete.FloatHelpers as Concrete

import qualified Cryptol.Eval.Backend as Eval
import qualified Cryptol.Eval.Value as Eval
import           Cryptol.Eval.What4
import qualified Cryptol.Eval.What4.SFloat as W4
import           Cryptol.Symbolic
import           Cryptol.TypeCheck.AST
import           Cryptol.Utils.Ident (Ident)
import           Cryptol.Utils.Logger(logPutStrLn)
import           Cryptol.Utils.Panic (panic)
import           Cryptol.Utils.RecordMap

import qualified What4.Config as W4
import qualified What4.Interface as W4
import qualified What4.Expr.Builder as W4
import qualified What4.Expr.GroundEval as W4
import qualified What4.SatResult as W4
import qualified What4.SWord as SW
import           What4.Solver
import qualified What4.Solver.Adapter as W4

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Nonce


import Prelude ()
import Prelude.Compat

data W4Exception
  = W4Ex X.SomeException
  | W4PortfolioFailure [ (Either X.SomeException (Maybe String, String)) ]

instance Show W4Exception where
  show (W4Ex e) = X.displayException e
  show (W4PortfolioFailure exs) =
       unlines ("All solveres in the portfolio failed!":map f exs)
    where
    f (Left e) = X.displayException e
    f (Right (Nothing, msg)) = msg
    f (Right (Just nm, msg)) = nm ++ ": " ++ msg

instance X.Exception W4Exception

rethrowW4Exception :: IO a -> IO a
rethrowW4Exception m = X.catchJust f m (X.throwIO . W4Ex)
  where
  f e
    | Just ( _ :: X.AsyncException) <- X.fromException e = Nothing
    | Just ( _ :: Eval.Unsupported) <- X.fromException e = Nothing
    | otherwise = Just e

protectStack :: (String -> M.ModuleCmd a)
             -> M.ModuleCmd a
             -> M.ModuleCmd a
protectStack mkErr cmd modEnv =
  rethrowW4Exception $
  X.catchJust isOverflow (cmd modEnv) handler
  where isOverflow X.StackOverflow = Just ()
        isOverflow _               = Nothing
        msg = "Symbolic evaluation failed to terminate."
        handler () = mkErr msg modEnv


doEval :: MonadIO m => Eval.EvalOpts -> Eval.Eval a -> m a
doEval evo m = liftIO $ Eval.runEval evo m

-- | Returns definitions, together with the value and it safety predicate.
doW4Eval ::
  (W4.IsExprBuilder sym, MonadIO m) =>
  sym -> Eval.EvalOpts -> W4Eval sym a -> m (W4Defs sym (W4.Pred sym, a))
doW4Eval sym evo m =
  do res <- liftIO $ Eval.runEval evo (w4Eval m sym)
     case w4Result res of
       W4Error err  -> liftIO (X.throwIO err)
       W4Result p x -> pure res { w4Result = (p,x) }


data AnAdapter = AnAdapter (forall st. SolverAdapter st)

data W4ProverConfig
  = W4ProverConfig AnAdapter
  | W4Portfolio (NonEmpty AnAdapter)

proverConfigs :: [(String, W4ProverConfig)]
proverConfigs =
  [ ("w4-cvc4"     , W4ProverConfig (AnAdapter cvc4Adapter) )
  , ("w4-yices"    , W4ProverConfig (AnAdapter yicesAdapter) )
  , ("w4-z3"       , W4ProverConfig (AnAdapter z3Adapter) )
  , ("w4-boolector", W4ProverConfig (AnAdapter boolectorAdapter) )
  , ("w4-offline"  , W4ProverConfig (AnAdapter z3Adapter) )
  , ("w4-any"      , allSolvers)
  ]

allSolvers :: W4ProverConfig
allSolvers = W4Portfolio
  $ AnAdapter z3Adapter :|
  [ AnAdapter cvc4Adapter
  , AnAdapter boolectorAdapter
  , AnAdapter yicesAdapter
  ]

defaultProver :: W4ProverConfig
defaultProver = W4ProverConfig (AnAdapter z3Adapter)

proverNames :: [String]
proverNames = map fst proverConfigs

setupProver :: String -> IO (Either String ([String], W4ProverConfig))
setupProver nm =
  rethrowW4Exception $
  case lookup nm proverConfigs of
    Just cfg@(W4ProverConfig p) ->
      do st <- tryAdapter p
         let ws = case st of
                    Nothing -> []
                    Just ex -> [ "Warning: solver interaction failed with " ++ nm, "    " ++ show ex ]
         pure (Right (ws, cfg))

    Just (W4Portfolio ps) ->
      filterAdapters (NE.toList ps) >>= \case
         [] -> pure (Left "What4 could not communicate with any provers!")
         (p:ps') ->
           let msg = "What4 found the following solvers: " ++ show (adapterNames (p:ps')) in
           pure (Right ([msg], W4Portfolio (p:|ps')))

    Nothing -> pure (Left ("unknown solver name: " ++ nm))

  where
  adapterNames [] = []
  adapterNames (AnAdapter adpt : ps) =
    solver_adapter_name adpt : adapterNames ps

  filterAdapters [] = pure []
  filterAdapters (p:ps) =
    tryAdapter p >>= \case
      Just _err -> filterAdapters ps
      Nothing   -> (p:) <$> filterAdapters ps

  tryAdapter (AnAdapter adpt) =
     do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator
        W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym)
        W4.smokeTest sym adpt



proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
proverError msg (_, _, modEnv) =
  return (Right ((Nothing, ProverError msg), modEnv), [])


data CryptolState t = CryptolState



-- TODO? move this?
allDeclGroups :: M.ModuleEnv -> [DeclGroup]
allDeclGroups = concatMap mDecls . M.loadedNonParamModules

setupAdapterOptions :: W4ProverConfig -> W4.ExprBuilder t CryptolState fs -> IO ()
setupAdapterOptions cfg sym =
   case cfg of
     W4ProverConfig p -> setupAnAdapter p
     W4Portfolio ps -> mapM_ setupAnAdapter ps

  where
  setupAnAdapter (AnAdapter adpt) =
    W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym)


-- | Simulate and manipulate query into a form suitable to be sent
-- to a solver.
prepareQuery ::
  W4.IsSymExprBuilder sym =>
  sym ->
  ProverCommand ->
  M.ModuleT IO (Either String
                       ([FinType],[VarShape sym],W4.Pred sym, W4.Pred sym)
               )
prepareQuery sym ProverCommand { .. } =
  case predArgTypes pcQueryType pcSchema of
    Left msg -> pure (Left msg)
    Right ts ->
      do args <- liftIO (mapM (freshVariable sym) ts)
         res  <- simulate args
         liftIO
           do -- add the collected definitions to the goal
              let (safety,prop') = w4Result res
              b <- W4.andPred sym (w4Defs res) prop'

              -- Ignore the safety condition if the flag is set
              let safety' = if pcIgnoreSafety then W4.truePred sym else safety

              Right <$>
                case pcQueryType of
                  ProveQuery ->
                    do q <- W4.notPred sym =<< W4.andPred sym safety' b
                       pure (ts,args,safety',q)

                  SafetyQuery ->
                    do q <- W4.notPred sym safety
                       pure (ts,args,safety,q)

                  SatQuery _ ->
                    do q <- W4.andPred sym safety' b
                       pure (ts,args,safety',q)
  where
  simulate args =
    do let lPutStrLn = M.withLogger logPutStrLn
       when pcVerbose (lPutStrLn "Simulating...")
       evo    <- M.getEvalOpts
       modEnv <- M.getModuleEnv
       doW4Eval sym evo
         do let ?evalPrim = evalPrim sym
            let extDgs = allDeclGroups modEnv ++ pcExtraDecls
            env <- Eval.evalDecls (What4 sym) extDgs mempty
            v   <- Eval.evalExpr  (What4 sym) env    pcExpr
            appliedVal <-
              foldM Eval.fromVFun v (map (pure . varToSymValue sym) args)

            case pcQueryType of
              SafetyQuery ->
                do Eval.forceValue appliedVal
                   pure (W4.truePred sym)

              _ -> pure (Eval.fromVBit appliedVal)





satProve ::
  W4ProverConfig ->
  Bool ->
  ProverCommand ->
  M.ModuleCmd (Maybe String, ProverResult)

satProve solverCfg hashConsing ProverCommand {..} =
  protectStack proverError \(evo, byteReader, modEnv) ->
  M.runModuleM (evo, byteReader, modEnv)
  do sym     <- liftIO makeSym
     logData <- M.withLogger doLog ()
     start   <- liftIO getCurrentTime
     query   <- prepareQuery sym ProverCommand { .. }
     primMap <- M.getPrimMap
     liftIO
       do result <- runProver sym evo logData primMap query
          end <- getCurrentTime
          writeIORef pcProverStats (diffUTCTime end start)
          return result
  where
  makeSym =
    do sym <- W4.newExprBuilder W4.FloatIEEERepr
                                CryptolState
                                globalNonceGenerator
       setupAdapterOptions solverCfg sym
       when hashConsing (W4.startCaching sym)
       pure sym

  doLog lg () =
    pure
    defaultLogData
      { logCallbackVerbose = \i msg -> when (i > 2) (logPutStrLn lg msg)
      , logReason = "solver query"
      }

  runProver sym evo logData primMap q =
    case q of
      Left msg -> pure (Nothing, ProverError msg)
      Right (ts,args,safety,query) ->
        case pcQueryType of
          ProveQuery ->
            singleQuery sym solverCfg evo primMap logData ts args
                                                          (Just safety) query

          SafetyQuery ->
            singleQuery sym solverCfg evo primMap logData ts args
                                                          (Just safety) query

          SatQuery num ->
            multiSATQuery sym solverCfg evo primMap logData ts args
                                                            query num



satProveOffline ::
  W4ProverConfig ->
  Bool ->
  ProverCommand ->
  ((Handle -> IO ()) -> IO ()) ->
  M.ModuleCmd (Maybe String)

satProveOffline (W4Portfolio (p:|_)) hashConsing cmd outputContinuation =
  satProveOffline (W4ProverConfig p) hashConsing cmd outputContinuation

satProveOffline (W4ProverConfig (AnAdapter adpt)) hashConsing ProverCommand {..} outputContinuation =
  protectStack onError \(evo,byteReader,modEnv) ->
  M.runModuleM (evo,byteReader,modEnv)
   do sym <- liftIO makeSym
      ok  <- prepareQuery sym ProverCommand { .. }
      liftIO
        case ok of
          Left msg -> return (Just msg)
          Right (_ts,_args,_safety,query) ->
            do outputContinuation
                  (\hdl -> solver_adapter_write_smt2 adpt sym hdl [query])
               return Nothing
  where
  makeSym =
    do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState
                                                    globalNonceGenerator
       W4.extendConfig (W4.solver_adapter_config_options adpt)
                       (W4.getConfiguration sym)
       when hashConsing  (W4.startCaching sym)
       pure sym

  onError msg (_,_,modEnv) = pure (Right (Just msg, modEnv), [])


decSatNum :: SatNum -> SatNum
decSatNum (SomeSat n) | n > 0 = SomeSat (n-1)
decSatNum n = n


multiSATQuery ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  sym ->
  W4ProverConfig ->
  Eval.EvalOpts ->
  PrimMap ->
  W4.LogData ->
  [FinType] ->
  [VarShape sym] ->
  W4.Pred sym ->
  SatNum ->
  IO (Maybe String, ProverResult)
multiSATQuery sym solverCfg evo primMap logData ts args query (SomeSat n) | n <= 1 =
  singleQuery sym solverCfg evo primMap logData ts args Nothing query

multiSATQuery _sym (W4Portfolio _) _evo _primMap _logData _ts _args _query _satNum =
  fail "What4 portfolio solver cannot be used for multi SAT queries"

multiSATQuery sym (W4ProverConfig (AnAdapter adpt)) evo primMap logData ts args query satNum0 =
  do pres <- W4.solver_adapter_check_sat adpt sym logData [query] $ \res ->
         case res of
           W4.Unknown -> return (Left (ProverError "Solver returned UNKNOWN"))
           W4.Unsat _ -> return (Left (ThmResult (map unFinType ts)))
           W4.Sat (evalFn,_) ->
             do model <- computeModel evo primMap evalFn ts args
                blockingPred <- computeBlockingPred sym evalFn args
                return (Right (model, blockingPred))

     case pres of
       Left res -> pure (Just (solver_adapter_name adpt), res)
       Right (mdl,block) ->
         do mdls <- (mdl:) <$> computeMoreModels [block,query] (decSatNum satNum0)
            return (Just (solver_adapter_name adpt), AllSatResult mdls)

  where

  computeMoreModels _qs (SomeSat n) | n <= 0 = return [] -- should never happen...
  computeMoreModels qs (SomeSat n) | n <= 1 = -- final model
    W4.solver_adapter_check_sat adpt sym logData qs $ \res ->
         case res of
           W4.Unknown -> return []
           W4.Unsat _ -> return []
           W4.Sat (evalFn,_) ->
             do model <- computeModel evo primMap evalFn ts args
                return [model]

  computeMoreModels qs satNum =
    do pres <- W4.solver_adapter_check_sat adpt sym logData qs $ \res ->
         case res of
           W4.Unknown -> return Nothing
           W4.Unsat _ -> return Nothing
           W4.Sat (evalFn,_) ->
             do model <- computeModel evo primMap evalFn ts args
                blockingPred <- computeBlockingPred sym evalFn args
                return (Just (model, blockingPred))

       case pres of
         Nothing -> return []
         Just (mdl, block) ->
           (mdl:) <$> computeMoreModels (block:qs) (decSatNum satNum)

singleQuery ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  sym ->
  W4ProverConfig ->
  Eval.EvalOpts ->
  PrimMap ->
  W4.LogData ->
  [FinType] ->
  [VarShape sym] ->
  Maybe (W4.Pred sym) {- ^ optional safety predicate.  Nothing = SAT query -} ->
  W4.Pred sym ->
  IO (Maybe String, ProverResult)

singleQuery sym (W4Portfolio ps) evo primMap logData ts args msafe query =
  do as <- mapM async [ singleQuery sym (W4ProverConfig p) evo primMap logData ts args msafe query
                      | p <- NE.toList ps
                      ]
     waitForResults [] as

 where
 waitForResults exs [] = X.throwIO (W4PortfolioFailure exs)
 waitForResults exs as =
   do (winner, result) <- waitAnyCatch as
      let others = filter (/= winner) as
      case result of
        Left ex ->
          waitForResults (Left ex:exs) others
        Right (nm, ProverError err) ->
          waitForResults (Right (nm,err) : exs) others
        Right r ->
          do forM_ others (\a -> X.throwTo (asyncThreadId a) ExitSuccess)
             return r

singleQuery sym (W4ProverConfig (AnAdapter adpt)) evo primMap logData ts args msafe query =
  do pres <- W4.solver_adapter_check_sat adpt sym logData [query] $ \res ->
         case res of
           W4.Unknown -> return (ProverError "Solver returned UNKNOWN")
           W4.Unsat _ -> return (ThmResult (map unFinType ts))
           W4.Sat (evalFn,_) ->
             do model <- computeModel evo primMap evalFn ts args
                case msafe of
                  Just s ->
                    do s' <- W4.groundEval evalFn s
                       let cexType = if s' then PredicateFalsified else SafetyViolation
                       return (CounterExample cexType model)
                  Nothing -> return (AllSatResult [ model ])

     return (Just (W4.solver_adapter_name adpt), pres)


computeBlockingPred ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  sym ->
  W4.GroundEvalFn t ->
  [VarShape sym] ->
  IO (W4.Pred sym)
computeBlockingPred sym evalFn vs =
  do ps <- mapM (varBlockingPred sym evalFn) vs
     foldM (W4.orPred sym) (W4.falsePred sym) ps

varBlockingPred ::
  sym ~ W4.ExprBuilder t CryptolState fm =>
  sym ->
  W4.GroundEvalFn t ->
  VarShape sym ->
  IO (W4.Pred sym)
varBlockingPred sym evalFn v =
  case v of
    VarBit b ->
      do blit <- W4.groundEval evalFn b
         W4.notPred sym =<< W4.eqPred sym b (W4.backendPred sym blit)
    VarInteger i ->
      do ilit <- W4.groundEval evalFn i
         W4.notPred sym =<< W4.intEq sym i =<< W4.intLit sym ilit
    VarRational n d ->
      do n' <- W4.intLit sym =<< W4.groundEval evalFn n
         d' <- W4.intLit sym =<< W4.groundEval evalFn d
         x <- W4.intMul sym n d'
         y <- W4.intMul sym n' d
         W4.notPred sym =<< W4.intEq sym x y
    VarWord SW.ZBV -> return (W4.falsePred sym)
    VarWord (SW.DBV w) ->
      do wlit <- W4.groundEval evalFn w
         W4.notPred sym =<< W4.bvEq sym w =<< W4.bvLit sym (W4.bvWidth w) wlit

    VarFloat (W4.SFloat f)
      | fr@(W4.FloatingPointPrecisionRepr e p) <- sym `W4.fpReprOf` f
      , let wid = W4.addNat e p
      , Just W4.LeqProof <- W4.isPosNat wid ->
        do bits <- W4.groundEval evalFn f
           bv   <- W4.bvLit sym wid bits
           constF <- W4.floatFromBinary sym fr bv
           -- NOTE: we are using logical equality here
           W4.notPred sym =<< W4.floatEq sym f constF
      | otherwise -> panic "varBlockingPred" [ "1 >= 2 ???" ]

    VarFinSeq _n vs -> computeBlockingPred sym evalFn vs
    VarTuple vs     -> computeBlockingPred sym evalFn vs
    VarRecord fs    -> computeBlockingPred sym evalFn (recordElements fs)

computeModel ::
  Eval.EvalOpts ->
  PrimMap ->
  W4.GroundEvalFn t ->
  [FinType] ->
  [VarShape (W4.ExprBuilder t CryptolState fm)] ->
  IO [(Type, Expr, Concrete.Value)]
computeModel _ _ _ [] [] = return []
computeModel evo primMap evalFn (t:ts) (v:vs) =
  do v' <- varToConcreteValue evalFn v
     let t' = unFinType t
     e <- doEval evo (Concrete.toExpr primMap t' v') >>= \case
             Nothing -> panic "computeModel" ["could not compute counterexample expression"]
             Just e  -> pure e
     zs <- computeModel evo primMap evalFn ts vs
     return ((t',e,v'):zs)
computeModel _ _ _ _ _ = panic "computeModel" ["type/value list mismatch"]


data VarShape sym
  = VarBit (W4.Pred sym)
  | VarInteger (W4.SymInteger sym)
  | VarRational (W4.SymInteger sym) (W4.SymInteger sym)
  | VarFloat (W4.SFloat sym)
  | VarWord (SW.SWord sym)
  | VarFinSeq Int [VarShape sym]
  | VarTuple [VarShape sym]
  | VarRecord (RecordMap Ident (VarShape sym))

freshVariable :: W4.IsSymExprBuilder sym => sym -> FinType -> IO (VarShape sym)
freshVariable sym ty =
  case ty of
    FTBit         -> VarBit      <$> W4.freshConstant sym W4.emptySymbol W4.BaseBoolRepr
    FTInteger     -> VarInteger  <$> W4.freshConstant sym W4.emptySymbol W4.BaseIntegerRepr
    FTRational    -> VarRational
                        <$> W4.freshConstant sym W4.emptySymbol W4.BaseIntegerRepr
                        <*> W4.freshBoundedInt sym W4.emptySymbol (Just 1) Nothing
    FTIntMod 0    -> panic "freshVariable" ["0 modulus not allowed"]
    FTIntMod n    -> VarInteger  <$> W4.freshBoundedInt sym W4.emptySymbol (Just 0) (Just (n-1))
    FTFloat e p   -> VarFloat    <$> W4.fpFresh sym e p
    FTSeq n FTBit -> VarWord     <$> SW.freshBV sym W4.emptySymbol (toInteger n)
    FTSeq n t     -> VarFinSeq n <$> sequence (replicate n (freshVariable sym t))
    FTTuple ts    -> VarTuple    <$> mapM (freshVariable sym) ts
    FTRecord fs   -> VarRecord   <$> traverse (freshVariable sym) fs

varToSymValue :: W4.IsExprBuilder sym => sym -> VarShape sym -> Value sym
varToSymValue sym var =
  case var of
    VarBit b     -> Eval.VBit b
    VarInteger i -> Eval.VInteger i
    VarRational n d -> Eval.VRational (Eval.SRational n d)
    VarWord w    -> Eval.VWord (SW.bvWidth w) (return (Eval.WordVal w))
    VarFloat f   -> Eval.VFloat f
    VarFinSeq n vs -> Eval.VSeq (toInteger n) (Eval.finiteSeqMap (What4 sym) (map (pure . varToSymValue sym) vs))
    VarTuple vs  -> Eval.VTuple (map (pure . varToSymValue sym) vs)
    VarRecord fs -> Eval.VRecord (fmap (pure . varToSymValue sym) fs)

varToConcreteValue ::
  W4.GroundEvalFn t ->
  VarShape (W4.ExprBuilder t CryptolState fm) ->
  IO Concrete.Value
varToConcreteValue evalFn v =
  case v of
    VarBit b     -> Eval.VBit <$> W4.groundEval evalFn b
    VarInteger i -> Eval.VInteger <$> W4.groundEval evalFn i
    VarRational n d ->
       Eval.VRational <$> (Eval.SRational <$> W4.groundEval evalFn n <*> W4.groundEval evalFn d)
    VarWord SW.ZBV     ->
       pure (Eval.VWord 0 (pure (Eval.WordVal (Concrete.mkBv 0 0))))
    VarWord (SW.DBV x) ->
       do let w = W4.intValue (W4.bvWidth x)
          Eval.VWord w . pure . Eval.WordVal . Concrete.mkBv w . BV.asUnsigned <$> W4.groundEval evalFn x
    VarFloat fv@(W4.SFloat f) ->
      do let (e,p) = W4.fpSize fv
         bits <- W4.groundEval evalFn f
         pure $ Eval.VFloat $ Concrete.floatFromBits e p $ BV.asUnsigned bits

    VarFinSeq n vs ->
       do vs' <- mapM (varToConcreteValue evalFn) vs
          pure (Eval.VSeq (toInteger n) (Eval.finiteSeqMap Concrete.Concrete (map pure vs')))
    VarTuple vs ->
       do vs' <- mapM (varToConcreteValue evalFn) vs
          pure (Eval.VTuple (map pure vs'))
    VarRecord fs ->
       do fs' <- traverse (varToConcreteValue evalFn) fs
          pure (Eval.VRecord (fmap pure fs'))