WIP: RPC support for newtypes and other opaque types

+ `readBack` now introduces fresh names which can be sent back to an RPC client when the structure of the value cannot be uniquely/ unambiguously syntactically represented. + `getCryptolExpr` needs to be modified, likely to return a `Expr Name` instead of the current return type `Expr PName`, since the fresh names introduced by `readBack` cannot be represented as `PName`s. + saw-remote-api compatibility for changes to `getCryptolExpr` should be considered (i.e., it also uses that function but in a slightly different monad, however that monad _also_ has a ModuleEnv from Cryptol so it should be possible to define it in a way it works for both servers).
2024-10-05 18:08:04 +03:00 · 2021-05-12 14:52:15 -07:00 · 2021-05-12 14:52:15 -07:00 · f9d9f30f59
commit f9d9f30f59
parent 282613d320
9 changed files with 265 additions and 140 deletions
--- a/cryptol-remote-api/python/cryptol/cryptoltypes.py
+++ b/cryptol-remote-api/python/cryptol/cryptoltypes.py
@ -30,6 +30,16 @@ class CryptolLiteral(CryptolCode):
    def __to_cryptol__(self, ty : CryptolType) -> Any:
        return self._code

+class CryptolNewtype(CryptolCode):
+    def __init__(self, newtype : Newtype, fields : Dict[str, Any]) -> None:
+        self._newtype = newtype
+        self._fields = fields
+
+    def __to_cryptol__(self, ty : CryptolType) -> Any:
+        return {'expression': 'newtype',
+                'newtype': self._name,
+                'arguments': [to_cryptol(arg) for arg in self._rands]}
+
 class CryptolApplication(CryptolCode):
    def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None:
        self._rator = rator
@ -407,6 +417,16 @@ class Record(CryptolType):
    def __repr__(self) -> str:
        return f"Record({self.fields!r})"

+
+class Newtype(CryptolType):
+    def __init__(self, name : str, uid : int, args : List[CryptolType]) -> None:
+        self.name = name
+        self.uid  = uid
+        self.args = args
+
+    def __repr__(self) -> str:
+        return f"Newtype({self.name!r}, {self.uid!r}, {self.args!r})"
+
 def to_type(t : Any) -> CryptolType:
    if t['type'] == 'variable':
        return Var(t['name'], to_kind(t['kind']))
@ -450,6 +470,8 @@ def to_type(t : Any) -> CryptolType:
        return Tuple(*map(to_type, t['contents']))
    elif t['type'] == 'record':
        return Record({k : to_type(t['fields'][k]) for k in t['fields']})
+    elif t['type'] == 'newtype':
+        return Newtype(t['name'], t['uid'], map(to_type, t['arguments']))
    elif t['type'] == 'Integer':
        return Integer()
    elif t['type'] == 'Rational':
--- a/cryptol-remote-api/src/CryptolServer.hs
+++ b/cryptol-remote-api/src/CryptolServer.hs
@ -13,10 +13,11 @@ import Data.Containers.ListUtils (nubOrd)
 import Data.Text (Text)

 import Cryptol.Eval (EvalOpts(..))
-import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv, ModuleInput(..))
+import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
 import Cryptol.ModuleSystem.Env
-  (getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules,
-   initialModuleEnv, meSearchPath, ModulePath(..))
+  (getLoadedModules, lmFilePath, lmFingerprint,
+   initialModuleEnv, ModulePath(..))
+import Cryptol.ModuleSystem.Name (FreshM(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
 import Cryptol.Parser.AST (ModName)
 import Cryptol.TypeCheck( defaultSolverConfig )
@ -73,15 +74,19 @@ instance CryptolMethod CryptolNotification where
 getModuleEnv :: CryptolCommand ModuleEnv
 getModuleEnv = CryptolCommand $ const $ view moduleEnv <$> Argo.getState

-getTCSolver :: CryptolCommand SMT.Solver
-getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
-
 setModuleEnv :: ModuleEnv -> CryptolCommand ()
 setModuleEnv me =
  CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv me s)

-runModuleCmd :: ModuleCmd a -> CryptolCommand a
-runModuleCmd cmd =
+modifyModuleEnv :: (ModuleEnv -> ModuleEnv) -> CryptolCommand ()
+modifyModuleEnv f =
+  CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv (f (view moduleEnv s)) s)
+
+getTCSolver :: CryptolCommand SMT.Solver
+getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
+
+liftModuleCmd :: ModuleCmd a -> CryptolCommand a
+liftModuleCmd cmd =
    do Options callStacks evOpts <- getOptions
       s <- CryptolCommand $ const Argo.getState
       reader <- CryptolCommand $ const Argo.getFileReader
@ -140,6 +145,14 @@ extendSearchPath paths =
  over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me }


+instance FreshM CryptolCommand where
+  liftSupply f = do
+    serverState <- CryptolCommand $ const Argo.getState
+    let mEnv = view moduleEnv serverState
+        (res, supply') = f (meSupply $ mEnv)
+        mEnv' = mEnv { meSupply = supply' }
+    CryptolCommand $ const (Argo.modifyState $ set moduleEnv mEnv')
+    pure res


 -- | Check that all of the modules loaded in the Cryptol environment
--- a/cryptol-remote-api/src/CryptolServer/Check.hs
+++ b/cryptol-remote-api/src/CryptolServer/Check.hs
@ -35,13 +35,13 @@ import Cryptol.TypeCheck.Solve (defaultReplExpr)
 import CryptolServer
    ( getTCSolver,
      getModuleEnv,
-      runModuleCmd,
+      liftModuleCmd,
      CryptolMethod(raise),
      CryptolCommand )
 import CryptolServer.Exceptions (evalPolyErr)
 import CryptolServer.Data.Expression
-    ( readBack, observe, getExpr, Expression )
-import CryptolServer.Data.Type
+    ( readBack, liftEval, getExpr, Expression )
+import CryptolServer.Data.Type ( JSONType(..) )
 import Cryptol.Utils.PP (pretty)

 checkDescr :: Doc.Block
@ -53,7 +53,7 @@ checkDescr =
 check :: CheckParams -> CryptolCommand CheckResult
 check (CheckParams jsonExpr cMode) =
  do e <- getExpr jsonExpr
-     (_expr, ty, schema) <- runModuleCmd (CM.checkExpr e)
+     (_expr, ty, schema) <- liftModuleCmd (CM.checkExpr e)
     -- TODO? validEvalContext expr, ty, schema
     s <- getTCSolver
     perhapsDef <- liftIO (defaultReplExpr s ty schema)
@ -65,7 +65,7 @@ check (CheckParams jsonExpr cMode) =
           let theType = apSubst su (AST.sType schema)
           tenv  <- CEE.envTypes . deEnv . meDynEnv <$> getModuleEnv
           let tval = CET.evalValType tenv theType
-           val <- runModuleCmd (CM.evalExpr checked)
+           val <- liftModuleCmd (CM.evalExpr checked)
           pure (val,tval)
         let (isExaustive, randomTestNum) = case cMode of
                                              ExhaustiveCheckMode -> (True, 0)
@ -85,8 +85,10 @@ check (CheckParams jsonExpr cMode) =

 convertTestArg :: (CET.TValue, CEC.Value) -> CryptolCommand (JSONType, Expression)
 convertTestArg (t, v) = do
-   e <- observe $ readBack t v
-   return (JSONType mempty (CET.tValTy t), e)
+   me <- readBack t v
+   case me of
+     Nothing -> error $ "type is not convertable: " ++ (show t)
+     Just e -> return (JSONType mempty (CET.tValTy t), e)

 convertTestResult ::
  [CET.TValue] {- ^ Argument types -} ->
--- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs
+++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs
@ -10,7 +10,6 @@ module CryptolServer.Data.Expression
  ) where

 import Control.Applicative
-import Control.Exception (throwIO)
 import Control.Monad.IO.Class
 import Data.Aeson as JSON hiding (Encoding, Value, decode)
 import qualified Data.ByteString as BS
@ -29,8 +28,7 @@ import Data.Text.Encoding (encodeUtf8)
 import Numeric (showHex)

 import Cryptol.Backend.Monad
-import Cryptol.Backend.Concrete hiding (Concrete)
-import qualified Cryptol.Backend.Concrete as C
+import qualified Cryptol.Eval.Concrete as Concrete
 import Cryptol.Backend.SeqMap (enumerateSeqMap)
 import Cryptol.Backend.WordValue (asWordVal)

@ -38,13 +36,18 @@ import Cryptol.Eval (evalSel)
 import Cryptol.Eval.Concrete (Value)
 import Cryptol.Eval.Type (TValue(..), tValTy)
 import Cryptol.Eval.Value (GenValue(..))
+import Cryptol.ModuleSystem (getPrimMap, evalDecls)
+import Cryptol.ModuleSystem.Env (deNames,meDynEnv)
+import Cryptol.ModuleSystem.Name
+  (Name, mkDeclared, NameSource( SystemName ),
+   nameUnique, nameIdent, liftSupply)
+import Cryptol.ModuleSystem.NamingEnv (singletonE, shadowing)

-
-import Cryptol.Parser
-import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type,
-          ExportType(..))
+import qualified Cryptol.Parser as CP
+import qualified Cryptol.Parser.AST as CP
 import Cryptol.Parser.Position (Located(..), emptyRange)
 import Cryptol.Parser.Selector
+import qualified Cryptol.TypeCheck.AST as TC
 import Cryptol.Utils.Ident
 import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)

@ -82,6 +85,8 @@ instance JSON.ToJSON LetBinding where
           , "definition" .= def
           ]

+-- | Cryptol expressions which can be serialized into JSON and sent
+-- to an RPC client.
 data Expression =
    Bit !Bool
  | Unit
@ -91,17 +96,30 @@ data Expression =
  | Tuple ![Expression]
  | Integer !Integer
  | IntegerModulo !Integer !Integer -- ^ value, modulus
-  | Concrete !Text
+  | UniqueName !Int !Text
+    -- ^ Essentially a Cryptol.ModuleSystem.Name's nameUnique and nameIdent.
+    -- Used when we need to send a result back to an RPC client
+  | Concrete !Text -- ^ Concrete Cryptol syntax as a string -- the Cryptol parser
+                   -- will establish it's meaning based on the current focus/context
  | Let ![LetBinding] !Expression
  | Application !Expression !(NonEmpty Expression)
  | TypeApplication !Expression !TypeArguments
  deriving (Eq, Show)

 newtype TypeArguments = TypeArguments (Map Ident JSONPType)
-  deriving (Eq, Show) via Map Ident (Type PName)
+  deriving (Eq, Show) via Map Ident (CP.Type CP.PName)

-data ExpressionTag =
-    TagNum | TagRecord | TagSequence | TagTuple | TagUnit | TagLet | TagApp | TagTypeApp | TagIntMod
+data ExpressionTag
+  = TagNum
+  | TagRecord
+  | TagSequence
+  | TagTuple
+  | TagUnit
+  | TagLet
+  | TagApp
+  | TagTypeApp
+  | TagIntMod
+  | TagUniqueName

 instance JSON.FromJSON ExpressionTag where
  parseJSON =
@ -116,18 +134,20 @@ instance JSON.FromJSON ExpressionTag where
      "call"           -> pure TagApp
      "instantiate"    -> pure TagTypeApp
      "integer modulo" -> pure TagIntMod
+      "unique name"    -> pure TagUniqueName
      _                -> empty

 instance JSON.ToJSON ExpressionTag where
-  toJSON TagNum      = "bits"
-  toJSON TagRecord   = "record"
-  toJSON TagSequence = "sequence"
-  toJSON TagTuple    = "tuple"
-  toJSON TagUnit     = "unit"
-  toJSON TagLet      = "let"
-  toJSON TagApp      = "call"
-  toJSON TagTypeApp  = "instantiate"
-  toJSON TagIntMod   = "integer modulo"
+  toJSON TagNum        = "bits"
+  toJSON TagRecord     = "record"
+  toJSON TagSequence   = "sequence"
+  toJSON TagTuple      = "tuple"
+  toJSON TagUnit       = "unit"
+  toJSON TagLet        = "let"
+  toJSON TagApp        = "call"
+  toJSON TagTypeApp    = "instantiate"
+  toJSON TagIntMod     = "integer modulo"
+  toJSON TagUniqueName = "unique name"

 instance JSON.FromJSON TypeArguments where
  parseJSON =
@ -182,6 +202,8 @@ instance JSON.FromJSON Expression where
                  TypeApplication <$> o .: "generic" <*> o .: "arguments"
                TagIntMod ->
                  IntegerModulo <$> o .: "integer" <*> o .: "modulus"
+                TagUniqueName ->
+                  IntegerModulo <$> o .: "unique" <*> o .: "identifier"

 instance ToJSON Encoding where
  toJSON Hex = String "hex"
@ -227,6 +249,11 @@ instance JSON.ToJSON Expression where
           , "function" .= fun
           , "arguments" .= args
           ]
+  toJSON (UniqueName unique name) =
+    object [ "expression" .= TagUniqueName
+           , "unique" .= toJSON unique
+           , "identifier" .= toJSON name
+           ]
  toJSON (TypeApplication gen _args) =
    -- It would be dead code to do anything here, as type
    -- instantiations are not values. This code is called only as part
@ -275,79 +302,89 @@ hexDigit 'F' = pure 15
 hexDigit c   = Argo.raise (invalidHex c)


-getExpr :: Expression -> CryptolCommand (Expr PName)
+-- nameUniqueToName :: Int -> Argo.Command ServerState Name
+-- nameUniqueToName n = do
+--   evalEnv <- meEvalEnv <$> view moduleEnv <$> Argo.getState
+--   error "TODO"
+
+
+getExpr :: Expression -> CryptolCommand (CP.Expr CP.PName)
 getExpr = CryptolCommand . const . getCryptolExpr

 -- N.B., used in SAWServer as well, hence the more generic monad
-getCryptolExpr :: (Argo.Method m, Monad m) => Expression -> m (Expr PName)
+getCryptolExpr ::
+  (Argo.Method m, Monad m) =>
+  Expression ->
+  m (CP.Expr CP.PName)
+getCryptolExpr (UniqueName unique name) = error "TODO / FIXME"
 getCryptolExpr Unit =
  return $
-    ETyped
-      (ETuple [])
-      (TTuple [])
+    CP.ETyped
+      (CP.ETuple [])
+      (CP.TTuple [])
 getCryptolExpr (Bit b) =
  return $
-    ETyped
-      (EVar (UnQual (mkIdent $ if b then "True" else "False")))
-      TBit
+    CP.ETyped
+      (CP.EVar (CP.UnQual (mkIdent $ if b then "True" else "False")))
+      CP.TBit
 getCryptolExpr (Integer i) =
  return $
-    ETyped
-      (ELit (ECNum i (DecLit (pack (show i)))))
-      (TUser (UnQual (mkIdent "Integer")) [])
+    CP.ETyped
+      (CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
+      (CP.TUser (CP.UnQual (mkIdent "Integer")) [])
 getCryptolExpr (IntegerModulo i n) =
  return $
-    ETyped
-      (ELit (ECNum i (DecLit (pack (show i)))))
-      (TUser (UnQual (mkIdent "Z")) [TNum n])
+    CP.ETyped
+      (CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
+      (CP.TUser (CP.UnQual (mkIdent "Z")) [CP.TNum n])
 getCryptolExpr (Num enc txt w) =
  do d <- decode enc txt
-     return $ ETyped
-       (ELit (ECNum d (DecLit txt)))
-       (TSeq (TNum w) TBit)
+     return $ CP.ETyped
+       (CP.ELit (CP.ECNum d (CP.DecLit txt)))
+       (CP.TSeq (CP.TNum w) CP.TBit)
 getCryptolExpr (Record fields) =
-  fmap (ERecord . recordFromFields) $ for (HM.toList fields) $
+  fmap (CP.ERecord . recordFromFields) $ for (HM.toList fields) $
  \(recName, spec) ->
    (mkIdent recName,) . (emptyRange,) <$> getCryptolExpr spec
 getCryptolExpr (Sequence elts) =
-  EList <$> traverse getCryptolExpr elts
+  CP.EList <$> traverse getCryptolExpr elts
 getCryptolExpr (Tuple projs) =
-  ETuple <$> traverse getCryptolExpr projs
+  CP.ETuple <$> traverse getCryptolExpr projs
 getCryptolExpr (Concrete syntax) =
-  case parseExpr syntax of
+  case CP.parseExpr syntax of
    Left err ->
      Argo.raise (cryptolParseErr syntax err)
    Right e -> pure e
 getCryptolExpr (Let binds body) =
-  EWhere <$> getCryptolExpr body <*> traverse mkBind binds
+  CP.EWhere <$> getCryptolExpr body <*> traverse mkBind binds
  where
    mkBind (LetBinding x rhs) =
-      DBind .
+      CP.DBind .
      (\bindBody ->
-         Bind { bName = fakeLoc (UnQual (mkIdent x))
-              , bParams = []
-              , bDef = bindBody
-              , bSignature = Nothing
-              , bInfix = False
-              , bFixity = Nothing
-              , bPragmas = []
-              , bMono = True
-              , bDoc = Nothing
-              , bExport = Public
+         CP.Bind { CP.bName = fakeLoc (CP.UnQual (mkIdent x))
+              , CP.bParams = []
+              , CP.bDef = bindBody
+              , CP.bSignature = Nothing
+              , CP.bInfix = False
+              , CP.bFixity = Nothing
+              , CP.bPragmas = []
+              , CP.bMono = True
+              , CP.bDoc = Nothing
+              , CP.bExport = CP.Public
              }) .
      fakeLoc .
-      DExpr <$>
+      CP.DExpr <$>
        getCryptolExpr rhs

    fakeLoc = Located emptyRange
 getCryptolExpr (Application fun (arg :| [])) =
-  EApp <$> getCryptolExpr fun <*> getCryptolExpr arg
+  CP.EApp <$> getCryptolExpr fun <*> getCryptolExpr arg
 getCryptolExpr (Application fun (arg1 :| (arg : args))) =
  getCryptolExpr (Application (Application fun (arg1 :| [])) (arg :| args))
 getCryptolExpr (TypeApplication gen (TypeArguments args)) =
-  EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args))
+  CP.EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args))
  where
-    inst (n, t) = NamedInst (Named (Located emptyRange n) (unJSONPType t))
+    inst (n, t) = CP.NamedInst (CP.Named (Located emptyRange n) (unJSONPType t))

 -- TODO add tests that this is big-endian
 -- | Interpret a ByteString as an Integer
@ -355,63 +392,109 @@ bytesToInt :: BS.ByteString -> Integer
 bytesToInt bs =
  BS.foldl' (\acc w -> (acc * 256) + toInteger w) 0 bs

-readBack :: TValue -> Value -> Eval Expression
+-- | Read back a typed value if possible.
+readBack :: TValue -> Value -> CryptolCommand (Maybe Expression)
 readBack ty val =
  case ty of
-    -- TODO, add actual support for newtypes
-    TVNewtype _u _ts _tfs -> liftIO $ throwIO (invalidType (tValTy ty))
-
-    TVRec tfs ->
-      Record . HM.fromList <$>
-        sequence [ do fv <- evalSel C.Concrete val (RecordSel f Nothing)
-                      fa <- readBack t fv
-                      return (identText f, fa)
-                 | (f, t) <- canonicalFields tfs
-                 ]
+    TVRec tfs -> do
+      vals <- mapM readBackRecFld $ canonicalFields tfs
+      pure $ (Record . HM.fromList) <$> sequence vals
    TVTuple [] ->
-      pure Unit
-    TVTuple ts ->
-      Tuple <$> sequence [ do v <- evalSel C.Concrete val (TupleSel n Nothing)
-                              a <- readBack t v
-                              return a
-                         | (n, t) <- zip [0..] ts
-                         ]
+      pure $ Just Unit
+    TVTuple ts -> do
+      vals <- mapM readBackTupleFld $ zip [0..] ts
+      pure $ Tuple <$> sequence vals
    TVBit ->
      case val of
-        VBit b -> pure (Bit b)
+        VBit b -> pure $ Just $ Bit b
        _ -> mismatchPanic
    TVInteger ->
      case val of
-        VInteger i -> pure (Integer i)
+        VInteger i -> pure $ Just $ Integer i
        _ -> mismatchPanic
    TVIntMod n ->
      case val of
-        VInteger i -> pure (IntegerModulo i n)
+        VInteger i -> pure $ Just $ IntegerModulo i n
        _ -> mismatchPanic
-    TVSeq len contents
+    TVSeq len elemTy
      | len == 0 ->
-        return Unit
-      | contents == TVBit
-      , VWord width wv <- val ->
-        do BV w v <- asWordVal C.Concrete wv
-           let hexStr = T.pack $ showHex v ""
-           let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1))
-           return $ Num Hex (T.justifyRight paddedLen '0' hexStr) w
-      | VSeq _l (enumerateSeqMap len -> vs) <- val ->
-        Sequence <$> mapM (>>= readBack contents) vs
+        pure $ Just Unit
+      | elemTy == TVBit
+      , VWord width wv <- val -> do
+        Concrete.BV w v <- liftEval $ asWordVal Concrete.Concrete wv
+        let hexStr = T.pack $ showHex v ""
+        let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1))
+        pure $ Just $  Num Hex (T.justifyRight paddedLen '0' hexStr) w
+      | VSeq _l (enumerateSeqMap len -> mVals) <- val -> do
+        vals <- liftEval $ sequence mVals
+        es <- mapM (readBack elemTy) vals
+        pure $ Sequence <$> sequence es

-    other -> liftIO $ throwIO (invalidType (tValTy other))
+    _ -> do
+      -- The above cases are for types that can unambiguously be converted into
+      -- syntax; this case instead tries to essentially let-bind the value to a
+      -- fresh variable so we can send that to the RPC client instead. They
+      -- obviously won't be able to directly inspect the value, but they can
+      -- pass it to other functions/commands via a RPC.
+      mName <- bindValToFreshName "rpc" ty val
+      case mName of
+        Nothing -> pure Nothing
+        Just name -> pure $ Just $ UniqueName (nameUnique name) (identText $ nameIdent name)
  where
+    mismatchPanic :: CryptolCommand (Maybe Expression)
    mismatchPanic =
      error $ "Internal error: readBack: value '" <>
              show val <>
              "' didn't match type '" <>
              show (tValTy ty) <>
              "'"
+    readBackRecFld :: (Ident, TValue) -> CryptolCommand (Maybe (Text, Expression))
+    readBackRecFld (fldId, fldTy) = do
+      fldVal <- liftEval $ evalSel Concrete.Concrete val (RecordSel fldId Nothing)
+      fldExpr <- readBack fldTy fldVal
+      pure $ (identText fldId,) <$> fldExpr
+    readBackTupleFld :: (Int, TValue) -> CryptolCommand (Maybe Expression)
+    readBackTupleFld (i, iTy) = do
+      iVal <- liftEval $ evalSel Concrete.Concrete val (TupleSel i Nothing)
+      readBack iTy iVal


-observe :: Eval a -> CryptolCommand a
-observe e = liftIO (runEval mempty e)
+bindValToFreshName :: Text -> TValue -> Concrete.Value -> CryptolCommand (Maybe Name)
+bindValToFreshName name ty val = do
+  prims   <- liftModuleCmd getPrimMap
+  mb      <- liftEval (Concrete.toExpr prims ty val)
+  case mb of
+    Nothing   -> return Nothing
+    Just expr -> do
+      name' <- genFreshName
+      let schema = TC.Forall { TC.sVars  = []
+                              , TC.sProps = []
+                              , TC.sType  = tValTy ty
+                          }
+          decl = TC.Decl { TC.dName       = name'
+                          , TC.dSignature  = schema
+                          , TC.dDefinition = TC.DExpr expr
+                          , TC.dPragmas    = []
+                          , TC.dInfix      = False
+                          , TC.dFixity     = Nothing
+                          , TC.dDoc        = Nothing
+                          }
+      liftModuleCmd (evalDecls [TC.NonRecursive decl])
+      denv <- meDynEnv <$> getModuleEnv
+      let nenv' = singletonE (CP.UnQual (mkIdent name)) name'
+                              `shadowing` deNames denv
+      modifyModuleEnv $ \me -> me {meDynEnv = denv { deNames = nenv' }}
+      return $ Just name'
+  where
+    genFreshName :: CryptolCommand Name
+    genFreshName =
+      liftSupply (mkDeclared NSValue mpath SystemName ident Nothing emptyRange)
+      where ident = mkIdent name
+            mpath = TopModule interactiveName

-mkEApp :: Expr PName -> [Expr PName] -> Expr PName
-mkEApp f args = foldl EApp f args
+
+liftEval :: Eval a -> CryptolCommand a
+liftEval e = liftIO (runEval mempty e)
+
+mkEApp :: CP.Expr CP.PName -> [CP.Expr CP.PName] -> CP.Expr CP.PName
+mkEApp f args = foldl CP.EApp f args
--- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs
+++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs
@ -7,6 +7,7 @@ module CryptolServer.EvalExpr
  ) where

 import qualified Argo.Doc as Doc
+import Control.Exception (throwIO)
 import Control.Monad.IO.Class
 import Data.Aeson as JSON

@ -37,29 +38,31 @@ evalExpression (EvalExprParams jsonExpr) =
     evalExpression' e

 evalExpression' :: P.Expr PName -> CryptolCommand JSON.Value
-evalExpression' e =
-  do (_expr, ty, schema) <- runModuleCmd (checkExpr e)
-     -- TODO: see Cryptol REPL for how to check whether we
-     -- can actually evaluate things, which we can't do in
-     -- a parameterized module
-     s <- getTCSolver
-     perhapsDef <- liftIO (defaultReplExpr s ty schema)
-     case perhapsDef of
-       Nothing ->
-         raise (evalPolyErr schema)
-       Just (tys, checked) ->
-         do -- TODO: warnDefaults here
-            let su = listParamSubst tys
-            let theType = apSubst su (sType schema)
-            tenv  <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv
-            let tval = E.evalValType tenv theType
-            res <- runModuleCmd (evalExpr checked)
-            val <- observe $ readBack tval res
-            return (JSON.object [ "value" .= val
-                                , "type string" .= pretty theType
-                                , "type" .= JSONSchema (Forall [] [] theType)
-                                ])
-
+evalExpression' e = do
+  (_expr, ty, schema) <- liftModuleCmd (checkExpr e)
+  -- TODO: see Cryptol REPL for how to check whether we
+  -- can actually evaluate things, which we can't do in
+  -- a parameterized module
+  s <- getTCSolver
+  perhapsDef <- liftIO (defaultReplExpr s ty schema)
+  case perhapsDef of
+    Nothing ->
+      raise (evalPolyErr schema)
+    Just (tys, checked) ->
+      do -- TODO: warnDefaults here
+         let su = listParamSubst tys
+         let theType = apSubst su (sType schema)
+         tenv  <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv
+         let tval = E.evalValType tenv theType
+         val <- liftModuleCmd (evalExpr checked)
+         mExpr<- readBack tval val
+         case mExpr of
+           Just expr ->
+             pure $  JSON.object [ "value" .= expr
+                                 , "type string" .= pretty theType
+                                 , "type" .= JSONSchema (Forall [] [] theType)
+                                 ]
+           Nothing -> liftIO $ throwIO (invalidType theType)
 newtype EvalExprParams =
  EvalExprParams Expression

--- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs
+++ b/cryptol-remote-api/src/CryptolServer/LoadModule.hs
@ -25,7 +25,7 @@ loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path

 loadFile :: LoadFileParams -> CryptolCommand ()
 loadFile (LoadFileParams fn) =
-  void $ runModuleCmd (loadModuleByPath fn)
+  void $ liftModuleCmd (loadModuleByPath fn)

 newtype LoadFileParams
  = LoadFileParams FilePath
@ -49,7 +49,7 @@ loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)."

 loadModule :: LoadModuleParams -> CryptolCommand ()
 loadModule (LoadModuleParams mn) =
-  void $ runModuleCmd (loadModuleByName mn)
+  void $ liftModuleCmd (loadModuleByName mn)

 newtype JSONModuleName
  = JSONModuleName { unJSONModName :: ModName }
--- a/cryptol-remote-api/src/CryptolServer/Sat.hs
+++ b/cryptol-remote-api/src/CryptolServer/Sat.hs
@ -44,7 +44,7 @@ proveSatDescr =
 proveSat :: ProveSatParams -> CryptolCommand ProveSatResult
 proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
  do e <- getExpr jsonExpr
-     (_expr, ty, schema) <- runModuleCmd (checkExpr e)
+     (_expr, ty, schema) <- liftModuleCmd (checkExpr e)
     -- TODO validEvalContext expr, ty, schema
     me <- getModuleEnv
     let decls = deDecls (meDynEnv me)
@ -72,7 +72,7 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
            sbvCfg <- liftIO (setupProver name) >>= \case
                        Left msg -> error msg
                        Right (_ws, sbvCfg) -> return sbvCfg
-            (_firstProver, res) <- runModuleCmd $ satProve sbvCfg cmd
+            (_firstProver, res) <- liftModuleCmd $ satProve sbvCfg cmd
            _stats <- liftIO (readIORef timing)
            case res of
              ProverError msg -> raise (proverError msg)
@ -86,9 +86,11 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
    satResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)]
    satResult es = traverse result es

-    result (t, _, v) =
-      do e <- observe $ readBack t v
-         return (JSONType mempty (tValTy t), e)
+    result (t, _, v) = do
+      me <- readBack t v
+      case me of
+        Nothing -> error $ "type is not convertable: " ++ (show t)
+        Just e -> pure (JSONType mempty (tValTy t), e)

 data ProveSatResult
  = Unsatisfiable
--- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs
+++ b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs
@ -24,7 +24,7 @@ checkTypeDescr =
 checkType :: TypeCheckParams -> CryptolCommand JSON.Value
 checkType (TypeCheckParams e) =
  do e' <- getExpr e
-     (_expr, _ty, schema) <- runModuleCmd (checkExpr e')
+     (_expr, _ty, schema) <- liftModuleCmd (checkExpr e')
     return (JSON.object [ "type schema" .= JSONSchema schema ])
  where
    -- FIXME: Why is this check not being used?
--- a/tests/regression/cplx.cry
+++ b/tests/regression/cplx.cry
@ -1,6 +1,6 @@
 // This is a development of rational complex numbers

-type Q = Rational
+type Q = Integer

 // Complex rational numbers in rectangular coordinates
 newtype CplxQ =