Add newtype to the routines that transfer values back to expressions,

and use `TValue` instead of `Type` in more places.

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -34,13 +34,12 @@ import qualified Cryptol.Backend.Concrete as C
 
 import Cryptol.Eval (evalSel)
 import Cryptol.Eval.Concrete (Value)
+import Cryptol.Eval.Type (TValue(..), tValTy)
 import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap)
 import Cryptol.Parser
 import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type)
 import Cryptol.Parser.Position (Located(..), emptyRange)
 import Cryptol.Parser.Selector
-import Cryptol.TypeCheck.SimpType (tRebuild)
-import qualified Cryptol.TypeCheck.Type as TC
 import Cryptol.Utils.Ident
 import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
 
@@ -337,60 +336,57 @@ bytesToInt :: BS.ByteString -> Integer
 bytesToInt bs =
   BS.foldl' (\acc w -> (acc * 256) + toInteger w) 0 bs
 
-typeNum :: (Alternative f, Integral a) => TC.Type -> f a
-typeNum (tRebuild -> (TC.TCon (TC.TC (TC.TCNum n)) [])) =
-  pure $ fromIntegral n
-typeNum _ = empty
-
-readBack :: TC.Type -> Value -> Eval Expression
+readBack :: TValue -> Value -> Eval Expression
 readBack ty val =
-  case TC.tNoUser ty of
-    TC.TRec tfs ->
+  case ty of
+    TVNewtype u ts tfs -> error "readBack Newtype! TODO"
+
+    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
                  ]
-    TC.TCon (TC.TC (TC.TCTuple _)) [] ->
+    TVTuple [] ->
       pure Unit
-    TC.TCon (TC.TC (TC.TCTuple _)) ts ->
+    TVTuple ts ->
       Tuple <$> sequence [ do v <- evalSel C.Concrete val (TupleSel n Nothing)
                               a <- readBack t v
                               return a
                          | (n, t) <- zip [0..] ts
                          ]
-    TC.TCon (TC.TC TC.TCBit) [] ->
+    TVBit ->
       case val of
         VBit b -> pure (Bit b)
         _ -> mismatchPanic
-    TC.TCon (TC.TC TC.TCInteger) [] ->
+    TVInteger ->
       case val of
         VInteger i -> pure (Integer i)
         _ -> mismatchPanic
-    TC.TCon (TC.TC TC.TCIntMod) [typeNum -> Just n] ->
+    TVIntMod n ->
       case val of
         VInteger i -> pure (IntegerModulo i n)
         _ -> mismatchPanic
-    TC.TCon (TC.TC TC.TCSeq) [TC.tNoUser -> len, TC.tNoUser -> contents]
-      | len == TC.tZero ->
+    TVSeq len contents
+      | len == 0 ->
         return Unit
-      | contents == TC.TCon (TC.TC TC.TCBit) []
+      | contents == TVBit
       , VWord width wv <- val ->
         do BV w v <- wv >>= asWordVal C.Concrete
            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
-      | TC.TCon (TC.TC (TC.TCNum k)) [] <- len
-      , VSeq _l (enumerateSeqMap k -> vs) <- val ->
+      | VSeq _l (enumerateSeqMap len -> vs) <- val ->
         Sequence <$> mapM (>>= readBack contents) vs
-    other -> liftIO $ throwIO (invalidType other)
+
+    other -> liftIO $ throwIO (invalidType (tValTy other))
   where
     mismatchPanic =
       error $ "Internal error: readBack: value '" <>
               show val <>
               "' didn't match type '" <>
-              show ty <>
+              show (tValTy ty) <>
               "'"
 
 

cryptol-remote-api/src/CryptolServer/EvalExpr.hs

@@ -6,14 +6,16 @@ import Data.Aeson as JSON
 
 
 import Cryptol.ModuleSystem (checkExpr, evalExpr)
-import Cryptol.ModuleSystem.Env (meSolverConfig)
+import Cryptol.ModuleSystem.Env (meSolverConfig,deEnv,meDynEnv,loadedNewtypes)
 import Cryptol.TypeCheck.Solve (defaultReplExpr)
 import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
 import Cryptol.TypeCheck.Type (Schema(..))
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Parser.Name (PName)
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.PP (pretty)
+import qualified Cryptol.Eval.Env as E
+import qualified Cryptol.Eval.Type as E
 
 import CryptolServer
 import CryptolServer.Data.Expression
@@ -41,8 +43,11 @@ evalExpression' e =
          do -- TODO: warnDefaults here
             let su = listParamSubst tys
             let theType = apSubst su (sType schema)
+            tenv  <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv
+            ntEnv <- E.NewtypeEnv . loadedNewtypes <$> getModuleEnv
+            let tval = E.evalValType ntEnv tenv theType
             res <- runModuleCmd (evalExpr checked)
-            val <- observe $ readBack theType res
+            val <- observe $ readBack tval res
             return (JSON.object [ "value" .= val
                                 , "type string" .= pretty theType
                                 , "type" .= JSONSchema (Forall [] [] theType)

cryptol-remote-api/src/CryptolServer/Sat.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ViewPatterns #-}
 module CryptolServer.Sat (sat, ProveSatParams(..)) where
 
 import Control.Applicative
@@ -14,11 +15,12 @@ import Data.Text (Text)
 import qualified Data.Text as T
 
 import Cryptol.Eval.Concrete (Value)
+import Cryptol.Eval.Type (TValue, tValTy)
 import Cryptol.ModuleSystem (checkExpr)
 import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv, meSolverConfig)
 import Cryptol.Symbolic (ProverCommand(..), ProverResult(..), QueryType(..), SatNum(..))
 import Cryptol.Symbolic.SBV (proverNames, satProve, setupProver)
-import Cryptol.TypeCheck.AST (Expr, Type)
+import Cryptol.TypeCheck.AST (Expr)
 import Cryptol.TypeCheck.Solve (defaultReplExpr)
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
@@ -68,12 +70,12 @@ sat (ProveSatParams (Prover name) jsonExpr num) =
                 Satisfied <$> traverse satResult results
 
   where
-    satResult :: [(Type, Expr, Value)] -> CryptolMethod [(JSONType, Expression)]
+    satResult :: [(TValue, Expr, Value)] -> CryptolMethod [(JSONType, Expression)]
     satResult es = traverse result es
 
     result (t, _, v) =
       do e <- observe $ readBack t v
-         return (JSONType mempty t, e)
+         return (JSONType mempty (tValTy t), e)
 
 data SatResult = Unsatisfiable | Satisfied [[(JSONType, Expression)]]
 

cryptol-remote-api/src/CryptolServer/TypeCheck.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 module CryptolServer.TypeCheck (checkType, TypeCheckParams(..)) where
 
-import Control.Lens hiding ((.=))
+--import Control.Lens hiding ((.=))
 import Data.Aeson as JSON
 
 

src/Cryptol/Eval/Concrete.hs

@@ -63,57 +63,66 @@ type Value = GenValue Concrete
 
 -- | Given an expected type, returns an expression that evaluates to
 -- this value, if we can determine it.
-toExpr :: PrimMap -> AST.Type -> Value -> Eval (Maybe AST.Expr)
+toExpr :: PrimMap -> TValue -> Value -> Eval (Maybe AST.Expr)
 toExpr prims t0 v0 = findOne (go t0 v0)
   where
 
   prim n = ePrim prims (prelPrim n)
 
 
-  go :: AST.Type -> Value -> ChoiceT Eval Expr
+  go :: TValue -> Value -> ChoiceT Eval Expr
   go ty val =
-    case val of
-      VRecord vfs ->
-        do tfs <- maybe mismatch pure (tIsRec ty)
-           -- NB, vfs first argument to keep their display order
+    case (ty,val) of
+      (TVRec tfs, VRecord vfs) ->
+        do -- NB, vfs first argument to keep their display order
            res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs
            case res of
              Left _ -> mismatch -- different fields
              Right efs -> pure (ERec efs)
-      VTuple tvs ->
-        do ts <- maybe mismatch pure (tIsTuple ty)
-           guard (length ts == length tvs)
+
+      (TVNewtype (UserTC nm _) _ tfs, VRecord vfs) ->
+        do -- NB, vfs first argument to keep their display order
+           res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs
+           case res of
+             Left _ -> mismatch -- different fields
+             Right efs -> pure (EApp (EVar nm) (ERec efs))
+
+      (TVTuple ts, VTuple tvs) ->
+        do guard (length ts == length tvs)
            ETuple <$> (zipWithM go ts =<< lift (sequence tvs))
-      VBit b ->
+      (TVBit, VBit b) ->
         pure (prim (if b then "True" else "False"))
-      VInteger i ->
-        -- This works uniformly for values of type Integer or Z n
-        pure $ ETApp (ETApp (prim "number") (tNum i)) ty
-      VRational (SRational n d) ->
+      (TVInteger, VInteger i) ->
+        pure $ ETApp (ETApp (prim "number") (tNum i)) tInteger
+      (TVIntMod n, VInteger i) ->
+        pure $ ETApp (ETApp (prim "number") (tNum i)) (tIntMod (tNum n))
+
+      (TVRational, VRational (SRational n d)) ->
         do let n' = ETApp (ETApp (prim "number") (tNum n)) tInteger
            let d' = ETApp (ETApp (prim "number") (tNum d)) tInteger
            pure $ EApp (EApp (prim "ratio") n') d'
-      VFloat i ->
-        do (eT, pT) <- maybe mismatch pure (tIsFloat ty)
-           pure (floatToExpr prims eT pT (bfValue i))
-      VSeq n svs ->
-        do (_a, b) <- maybe mismatch pure (tIsSeq ty)
-           ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))
-           pure $ EList ses b
-      VWord _ wval ->
+
+      (TVFloat e p, VFloat i) ->
+           pure (floatToExpr prims (tNum e) (tNum p) (bfValue i))
+      (TVSeq _ b, VSeq n svs) ->
+        do ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))
+           pure $ EList ses (tValTy b)
+      (TVSeq n TVBit, VWord _ wval) ->
         do BV _ v <- lift (asWordVal Concrete =<< wval)
-           pure $ ETApp (ETApp (prim "number") (tNum v)) ty
-      VStream _  -> mzero
-      VFun{}     -> mzero
-      VPoly{}    -> mzero
-      VNumPoly{} -> mzero
+           pure $ ETApp (ETApp (prim "number") (tNum v)) (tWord (tNum n))
+
+      (_,VStream{})  -> mzero
+      (_,VFun{})     -> mzero
+      (_,VPoly{})    -> mzero
+      (_,VNumPoly{}) -> mzero
+      _ -> mismatch
     where
       mismatch :: forall a. ChoiceT Eval a
       mismatch =
         do doc <- lift (ppValue Concrete defaultPPOpts val)
            panic "Cryptol.Eval.Concrete.toExpr"
              ["type mismatch:"
-             , pretty ty
+             , pretty (tValTy ty)
              , render doc
              ]
 

src/Cryptol/Eval/Type.hs

@@ -42,7 +42,7 @@ data TValue
   | TVNewtype UserTC [Either Nat' TValue]
               (RecordMap Ident TValue)     -- ^ a named newtype
   | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type
-    deriving (Generic, NFData)
+    deriving (Generic, NFData, Eq)
 
 -- | Convert a type value back into a regular type
 tValTy :: TValue -> Type