Merge pull request #1015 from GaloisInc/newtypes

Newtypes

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,58 @@ 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
+    -- 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
                  ]
-    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/Data/Type.hs

@@ -211,6 +211,8 @@ instance JSON.ToJSON JSONType where
         , "name" .= show (ppWithNames ns v)
         ]
       convert (TUser _n _args def) = convert def
+      convert (TNewtype nt ts) =
+        error "JSON conversion of newtypes is not yet supported TODO"
       convert (TRec fields) =
         JSON.object
         [ "type" .= T.pack "record"

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,10 @@ evalExpression' e =
          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 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