GaloisInc · mergify · May 21, 2021 · Apr 27, 2021 · Apr 15, 2021 · May 18, 2021
diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -1208,22 +1208,37 @@ ecCat =
          -- Case for (TCNum m, TCInf)
          (\ (a:sort 0) -> streamAppend a m));
 
-ecSplitAt : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a ->
-             #(seq m a, seq n a);
-ecSplitAt =
+ecTake : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq m a;
+ecTake =
+  Num_rec
+    (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq m a)
+
+    (\ (m:Nat) ->
+       Num_rec
+         (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> Vec m a)
+         -- The case (TCNum m, TCNum n)
+         (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> take a m n xs)
+         -- The case (TCNum m, infinity)
+         (\ (a:sort 0) -> \ (xs: Stream a) -> streamTake a m xs))
+
+    (Num_rec
+      (\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a)
+        -- The case (TCInf, TCNum n)
+	(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
+	-- The case (TCInf, TCInf)
+	(\ (a:sort 0) -> \ (xs:Stream a) -> xs));
+
+ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a;
+ecDrop =
   finNumRec
-    (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a ->
-       #(seq m a, seq n a))
+    (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq n a)
     (\ (m:Nat) ->
        Num_rec
-         (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a ->
-            #(Vec m a, seq n a))
+         (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a)
          -- The case (TCNum n, TCNum m)
-         (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) ->
-            (take a m n xs, drop a m n xs))
+         (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs)
          -- The case (TCNum m, infinity)
-         (\ (a:sort 0) -> \ (xs: Stream a) ->
-            (streamTake a m xs, streamDrop a m xs)));
+         (\ (a:sort 0) -> \ (xs: Stream a) -> streamDrop a m xs));
 
 ecJoin : (m n : Num) -> (a : sort 0) -> seq m (seq n a) -> seq (tcMul m n) a;
 ecJoin m =

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -35,6 +35,8 @@ import Text.URI
 
 import qualified Cryptol.Eval.Type as TV
 import qualified Cryptol.Backend.Monad as V
+import qualified Cryptol.Backend.SeqMap as V
+import qualified Cryptol.Backend.WordValue as V
 import qualified Cryptol.Eval.Value as V
 import qualified Cryptol.Eval.Concrete as V
 import Cryptol.Eval.Type (evalValType)
@@ -45,6 +47,7 @@ import qualified Cryptol.ModuleSystem.Name as C
 import qualified Cryptol.Utils.Ident as C
   ( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim
   , ModName, modNameToText, identText, interactiveName
+  , ModPath(..), modPathSplit
   )
 import qualified Cryptol.Utils.RecordMap as C
 import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
@@ -740,7 +743,8 @@ prelPrims =
 
     -- -- Sequences primitives
   , ("#",            flip scGlobalDef "Cryptol.ecCat")         -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
-  , ("splitAt",      flip scGlobalDef "Cryptol.ecSplitAt")     -- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c)
+  , ("take",         flip scGlobalDef "Cryptol.ecTake")        -- {front, back, a} [front + back]a -> [front]a
+  , ("drop",         flip scGlobalDef "Cryptol.ecDrop")        -- {front, back, a} (fin front) => [front + back]a -> [back]a
   , ("join",         flip scGlobalDef "Cryptol.ecJoin")        -- {a,b,c} (fin b) => [a][b]c -> [a * b]c
   , ("split",        flip scGlobalDef "Cryptol.ecSplit")       -- {a,b,c} (fin b) => [a * b] c -> [a][b] c
   , ("reverse",      flip scGlobalDef "Cryptol.ecReverse")     -- {a,b} (fin a) => [a] b -> [a] b
@@ -1231,18 +1235,20 @@ importName cnm =
   case C.nameInfo cnm of
     C.Parameter -> fail ("Cannot import non-top-level name: " ++ show cnm)
     C.Declared modNm _
-      | modNm == C.interactiveName ->
+      | modNm == C.TopModule C.interactiveName ->
           let shortNm = C.identText (C.nameIdent cnm)
               aliases = [shortNm]
               uri = cryptolURI [shortNm] (Just (C.nameUnique cnm))
            in pure (ImportedName uri aliases)
 
       | otherwise ->
-          let modNmTxt  = C.modNameToText modNm
-              modNms = Text.splitOn "::" modNmTxt
-              shortNm = C.identText (C.nameIdent cnm)
-              aliases = [shortNm, modNmTxt <> "::" <> shortNm]
-              uri = cryptolURI (modNms ++ [shortNm]) Nothing
+          let (topMod, nested) = C.modPathSplit modNm
+              modNmTxt = C.modNameToText topMod
+              modNms   = (Text.splitOn "::" modNmTxt) ++ map C.identText nested
+              shortNm  = C.identText (C.nameIdent cnm)
+              longNm   = Text.intercalate "::" ([modNmTxt] ++ map C.identText nested ++ [shortNm])
+              aliases  = [shortNm, longNm]
+              uri      = cryptolURI (modNms ++ [shortNm]) Nothing
            in pure (ImportedName uri aliases)
 
 -- | Currently this imports declaration groups by inlining all the
@@ -1646,22 +1652,22 @@ scCryptolEq sc x y =
 
 -- | Convert from SAWCore's Value type to Cryptol's, guided by the
 -- Cryptol type schema.
-exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value
+exportValueWithSchema :: C.Schema -> SC.CValue -> V.Eval V.Value
 exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v
-exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema")
+exportValueWithSchema _ _ = pure (V.VPoly mempty (error "exportValueWithSchema"))
 -- TODO: proper support for polymorphic values
 
-exportValue :: TV.TValue -> SC.CValue -> V.Value
+exportValue :: TV.TValue -> SC.CValue -> V.Eval V.Value
 exportValue ty v = case ty of
 
   TV.TVBit ->
-    V.VBit (SC.toBool v)
+    pure (V.VBit (SC.toBool v))
 
   TV.TVInteger ->
-    V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")
+    pure (V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer"))
 
   TV.TVIntMod _modulus ->
-    V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")
+    pure (V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod"))
 
   TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")"
 
@@ -1673,28 +1679,29 @@ exportValue ty v = case ty of
     case v of
       SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w)
       SC.VVector xs
-        | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs))
-                            (V.finiteSeqMap . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)))
-        | otherwise   -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $
-                            map (V.ready . exportValue e . SC.runIdentity . force) $ Vector.toList xs
+        | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) <$>
+            V.bitmapWordVal V.Concrete (toInteger (Vector.length xs))
+                 (V.finiteSeqMap V.Concrete . map (V.ready . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)
+        | otherwise   -> pure . V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $
+                            map (\x -> exportValue e (SC.runIdentity (force x))) (Vector.toList xs)
       _ -> error $ "exportValue (on seq type " ++ show ty ++ ")"
 
   -- infinite streams
   TV.TVStream e ->
     case v of
-      SC.VExtra (SC.CStream trie) -> V.VStream (V.IndexSeqMap $ \i -> V.ready $ exportValue e (IntTrie.apply trie i))
+      SC.VExtra (SC.CStream trie) -> pure $ V.VStream (V.indexSeqMap $ \i -> exportValue e (IntTrie.apply trie i))
       _ -> error $ "exportValue (on seq type " ++ show ty ++ ")"
 
   -- tuples
-  TV.TVTuple etys -> V.VTuple (exportTupleValue etys v)
+  TV.TVTuple etys -> pure $ V.VTuple $ exportTupleValue etys v
 
   -- records
   TV.TVRec fields ->
-      V.VRecord (C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v)
+      pure . V.VRecord . C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v
 
   -- functions
   TV.TVFun _aty _bty ->
-    V.VFun mempty (error "exportValue: TODO functions")
+    pure $ V.VFun mempty (error "exportValue: TODO functions")
 
   -- abstract types
   TV.TVAbstract{} ->
@@ -1709,8 +1716,8 @@ exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value]
 exportTupleValue tys v =
   case (tys, v) of
     ([]    , SC.VUnit    ) -> []
-    ([t]   , _           ) -> [V.ready $ exportValue t v]
-    (t : ts, SC.VPair x y) -> (V.ready $ exportValue t (run x)) : exportTupleValue ts (run y)
+    ([t]   , _           ) -> [exportValue t v]
+    (t : ts, SC.VPair x y) -> (exportValue t (run x)) : exportTupleValue ts (run y)
     _                      -> error $ "exportValue: expected tuple"
   where
     run = SC.runIdentity . force
@@ -1719,12 +1726,11 @@ exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> [(C.Ident, V.Eval V.
 exportRecordValue fields v =
   case (fields, v) of
     ([]         , SC.VUnit    ) -> []
-    ([(n, t)]   , _           ) -> [(n, V.ready $ exportValue t v)]
-    ((n, t) : ts, SC.VPair x y) ->
-      (n, V.ready $ exportValue t (run x)) : exportRecordValue ts (run y)
+    ([(n, t)]   , _           ) -> [(n, exportValue t v)]
+    ((n, t) : ts, SC.VPair x y) -> (n, exportValue t (run x)) : exportRecordValue ts (run y)
     (_, SC.VRecordValue (alistAllFields
                          (map (C.identText . fst) fields) -> Just ths)) ->
-      zipWith (\(n,t) x -> (n, V.ready $ exportValue t (run x))) fields ths
+      zipWith (\(n,t) x -> (n, exportValue t (run x))) fields ths
     _                              -> error $ "exportValue: expected record"
   where
     run = SC.runIdentity . force
@@ -1733,20 +1739,23 @@ fvAsBool :: FirstOrderValue -> Bool
 fvAsBool (FOVBit b) = b
 fvAsBool _ = error "fvAsBool: expected FOVBit value"
 
-exportFirstOrderValue :: FirstOrderValue -> V.Value
+exportFirstOrderValue :: FirstOrderValue -> V.Eval V.Value
 exportFirstOrderValue fv =
   case fv of
-    FOVBit b    -> V.VBit b
-    FOVInt i    -> V.VInteger i
-    FOVIntMod _ i -> V.VInteger i
-    FOVWord w x -> V.word V.Concrete (toInteger w) x
+    FOVBit b      -> pure (V.VBit b)
+    FOVInt i      -> pure (V.VInteger i)
+    FOVIntMod _ i -> pure (V.VInteger i)
+    FOVWord w x   -> V.word V.Concrete (toInteger w) x
     FOVVec t vs
-      | t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap . map (V.ready . V.VBit . fvAsBool) $ vs)))
-      | otherwise   -> V.VSeq  len (V.finiteSeqMap (map (V.ready . exportFirstOrderValue) vs))
+      | t == FOTBit -> V.VWord len <$> (V.bitmapWordVal V.Concrete len
+                          (V.finiteSeqMap V.Concrete . map (V.ready . fvAsBool) $ vs))
+      | otherwise   -> pure (V.VSeq len (V.finiteSeqMap V.Concrete (map exportFirstOrderValue vs)))
       where len = toInteger (length vs)
     FOVArray{}  -> error $ "exportFirstOrderValue: unsupported FOT Array"
-    FOVTuple vs -> V.VTuple (map (V.ready . exportFirstOrderValue) vs)
-    FOVRec vm   -> V.VRecord $ C.recordFromFields [ (C.mkIdent n, V.ready $ exportFirstOrderValue v) | (n, v) <- Map.assocs vm ]
+    FOVTuple vs -> pure $ V.VTuple $ map exportFirstOrderValue vs
+    FOVRec vm   ->
+      do let vm' = fmap exportFirstOrderValue vm
+         pure $ V.VRecord $ C.recordFromFields [ (C.mkIdent n, v) | (n, v) <- Map.assocs vm' ]
 
 importFirstOrderValue :: FirstOrderType -> V.Value -> IO FirstOrderValue
 importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
@@ -1755,7 +1764,7 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
   go t v = case (t,v) of
     (FOTBit         , V.VBit b)        -> return (FOVBit b)
     (FOTInt         , V.VInteger i)    -> return (FOVInt i)
-    (FOTVec _ FOTBit, V.VWord w wv)    -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete =<< wv)
+    (FOTVec _ FOTBit, V.VWord w wv)    -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete wv)
     (FOTVec _ ty    , V.VSeq len xs)   -> FOVVec ty <$> traverse (go ty =<<) (V.enumerateSeqMap len xs)
     (FOTTuple tys   , V.VTuple xs)     -> FOVTuple <$> traverse (\(ty, x) -> go ty =<< x) (zip tys xs)
     (FOTRec fs      , V.VRecord xs)    ->

diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -153,7 +153,7 @@ nameMatcher xs =
     case modNameChunks (textToModName (pack xs)) of
       []  -> const False
       [x] -> (packIdent x ==) . MN.nameIdent
-      cs -> let m = MN.Declared (packModName (map pack (init cs))) MN.UserName
+      cs -> let m = MN.Declared (C.TopModule (packModName (map pack (init cs)))) MN.UserName
                 i = packIdent (last cs)
              in \n -> MN.nameIdent n == i && MN.nameInfo n == m
 
@@ -253,7 +253,7 @@ getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv
           syms = case vis of
                    OnlyPublic       -> MI.ifPublic ifc
                    PublicAndPrivate -> MI.ifPublic ifc `mappend` M.ifPrivate ifc
-      return $ MN.interpImport i syms
+      return $ MN.interpImportIface i syms
 
 getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls
 getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me)))
@@ -364,13 +364,13 @@ loadCryptolModule sc env path = do
   newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups
   newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
-  let names = MEx.eBinds (T.mExports m) -- :: Set T.Name
+  let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
   let tm' = Map.filterWithKey (\k _ -> Set.member k names) $
             Map.intersectionWith TypedTerm types newTermEnv
   let env' = env { eModuleEnv = modEnv''
                  , eTermEnv = newTermEnv
                  }
-  let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.eTypes (T.mExports m))) (T.mTySyns m)
+  let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) (T.mTySyns m)
   return (CryptolModule sm' tm', env')
 
 bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv
@@ -430,7 +430,7 @@ bindIdent ident env = (name, env')
     modEnv = eModuleEnv env
     supply = ME.meSupply modEnv
     fixity = Nothing
-    (name, supply') = MN.mkDeclared interactiveName MN.UserName ident fixity P.emptyRange supply
+    (name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply
     modEnv' = modEnv { ME.meSupply = supply' }
     env' = env { eModuleEnv = modEnv' }
 
@@ -467,17 +467,8 @@ bindInteger (ident, n) env =
 
 --------------------------------------------------------------------------------
 
--- FIXME: This definition was copied from a local declaration inside
--- function 'defaultRW' in module 'Cryptol.REPL.Monad'. The cryptol
--- package should probably export it so we don't have to copy it.
 meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig
-meSolverConfig env =
-  TM.SolverConfig
-  { TM.solverPath = "z3"
-  , TM.solverArgs = [ "-smt2", "-in" ]
-  , TM.solverVerbose = 0
-  , TM.solverPreludePath = ME.meSearchPath env
-  }
+meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)
 
 resolveIdentifier ::
   (?fileReader :: FilePath -> IO ByteString) =>
@@ -496,7 +487,7 @@ resolveIdentifier env nm =
     SMT.withSolver (meSolverConfig modEnv) $ \s ->
     do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
        (res, _ws) <- MM.runModuleM (minp s) $
-          MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm))
+          MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm))
        case res of
          Left _ -> pure Nothing
          Right (x,_) -> pure (Just x)
@@ -557,18 +548,12 @@ parseDecls sc env input = do
     -- Convert from 'Decl' to 'TopDecl' so that types will be generalized
     let topdecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npdecls ]
 
-    -- Label each TopDecl with the "interactive" module for unique name generation
-    let (mdecls :: [MN.InModule (P.TopDecl P.PName)]) = map (MN.InModule interactiveName) topdecls
-    nameEnv1 <- MN.liftSupply (MN.namingEnv' mdecls)
-
     -- Resolve names
-    let nameEnv = nameEnv1 `MR.shadowing` getNamingEnv env
-    (rdecls :: [P.TopDecl T.Name]) <- MM.interactive (MB.rename interactiveName nameEnv (traverse MR.rename topdecls))
+    (_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls))
 
     -- Create a Module to contain the declarations
     let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName
                            , P.mInstance = Nothing
-                           , P.mImports = []
                            , P.mDecls = rdecls
                            }
 
@@ -636,7 +621,7 @@ declareName env mname input = do
   let modEnv = eModuleEnv env
   (cname, modEnv') <-
     liftModuleM modEnv $ MM.interactive $
-    MN.liftSupply (MN.mkDeclared mname MN.UserName (P.getIdent pname) Nothing P.emptyRange)
+    MN.liftSupply (MN.mkDeclared C.NSValue (C.TopModule mname) MN.UserName (P.getIdent pname) Nothing P.emptyRange)
   let env' = env { eModuleEnv = modEnv' }
   return (cname, env')
 

diff --git a/deps/cryptol b/deps/cryptol
diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs
@@ -55,6 +55,7 @@ import Cryptol.Parser (ParseError,ppError)
 import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
 import Cryptol.Parser.NoPat (Error)
 import qualified Cryptol.TypeCheck.AST as T
+import Cryptol.Utils.Ident (Namespace(..))
 import Cryptol.Utils.PP
 
 #if !MIN_VERSION_base(4,8,0)
@@ -297,13 +298,13 @@ getNewtypes = do
 getExprNames :: REPL [String]
 getExprNames =
   do fNames <- fmap getNamingEnv getCryptolEnv
-     return (map (show . pp) (Map.keys (MN.neExprs fNames)))
+     return (map (show . pp) (Map.keys (MN.namespaceMap NSValue fNames)))
 
 -- | Get visible type signature names.
 getTypeNames :: REPL [String]
 getTypeNames  =
   do fNames <- fmap getNamingEnv getCryptolEnv
-     return (map (show . pp) (Map.keys (MN.neTypes fNames)))
+     return (map (show . pp) (Map.keys (MN.namespaceMap NSType fNames)))
 
 getPropertyNames :: REPL [String]
 getPropertyNames =

diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -16,8 +16,6 @@ import Data.List hiding (sort)
 import Data.Maybe
 import Data.Ord
 
-import Verifier.SAW.CryptolEnv (meSolverConfig)
-
 import Cryptol.Eval (EvalOpts(..))
 import qualified Cryptol.ModuleSystem as M
 import Cryptol.ModuleSystem.Name
@@ -27,6 +25,9 @@ import qualified Cryptol.TypeCheck.AST as AST
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.PP
 
+import Verifier.SAW.CryptolEnv( meSolverConfig )
+
+
 -- | Parse a Cryptol module into a list of declarations
 --   Yields an Interaction so that we can talk to the user about what went wrong
 getDeclsCryptol :: FilePath -> IO (Interaction (Maybe [Decl]))

diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
@@ -340,7 +340,7 @@ evaluate sc t =
 
 evaluateTypedTerm :: SharedContext -> TypedTerm -> IO C.Value
 evaluateTypedTerm sc (TypedTerm schema trm) =
-  exportValueWithSchema schema <$> evaluate sc trm
+  C.runEval mempty . exportValueWithSchema schema =<< evaluate sc trm
 
 applyValue :: Value -> Value -> TopLevel Value
 applyValue (VLambda f) x = f x