Update for "newtype" -> "nominal type" renaming

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -35,7 +35,7 @@ module Verifier.SAW.Cryptol
   , importSchema
 
   , defaultPrimitiveOptions
-  , genNewtypeConstructors
+  , genNominalConstructors
   , exportValueWithSchema
   ) where
 
@@ -76,7 +76,7 @@ import qualified Cryptol.Utils.Ident as C
   , modNameChunksText
   )
 import qualified Cryptol.Utils.RecordMap as C
-import Cryptol.TypeCheck.Type as C (Newtype(..))
+import Cryptol.TypeCheck.Type as C (NominalType(..))
 import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
 import Cryptol.Utils.PP (pretty)
 
@@ -266,7 +266,7 @@ importType sc env ty =
     C.TRec fm ->
       importType sc env (C.tTuple (map snd (C.canonicalFields fm)))
 
-    C.TNewtype nt ts ->
+    C.TNominal nt ts ->
       do let s = C.listSubst (zip (map C.TVBound (C.ntParams nt)) ts)
          case ntDef nt of
            C.Struct stru -> go (plainSubst s (C.TRec (C.ntFields stru)))
@@ -1009,7 +1009,7 @@ importExpr sc env expr =
                       ("Expected filed " ++ show x ++ " in normal RecordSel")
                       (elemIndex x (map fst (C.canonicalFields fm)))
                     scTupleSelector sc e' (i+1) (length (C.canonicalFields fm))
-               C.TNewtype nt _args ->
+               C.TNominal nt _args ->
                  do let fs = case C.ntDef nt of
                                C.Struct s -> C.ntFields s
                                C.Enum {} ->
@@ -1138,6 +1138,9 @@ importExpr sc env expr =
       -- generated if-then-else
       Fold.foldrM (propGuardToIte typ') err arms
 
+    C.ECase {} -> panic "importExpr"
+                    ["`case` expressions are not yet supported"]
+
   where
     the :: String -> Maybe a -> IO a
     the what = maybe (panic "importExpr" ["internal type error", what]) return
@@ -1244,6 +1247,8 @@ importExpr' sc env schema expr =
     C.ELocated _ e ->
       importExpr' sc env schema e
 
+    C.ECase {} -> panic "importExpr" ["`case` is not yet supported"]
+
     C.EList     {} -> fallback
     C.ESel      {} -> fallback
     C.ESet      {} -> fallback
@@ -1289,7 +1294,7 @@ plainSubst s ty =
     C.TUser f ts t -> C.TUser f (map (plainSubst s) ts) (plainSubst s t)
     C.TRec fs      -> C.TRec (fmap (plainSubst s) fs)
     C.TVar x       -> C.apSubst s (C.TVar x)
-    C.TNewtype nt ts -> C.TNewtype nt (fmap (plainSubst s) ts)
+    C.TNominal nt ts -> C.TNominal nt (fmap (plainSubst s) ts)
 
 
 -- | Generate a URI representing a cryptol name from a sequence of
@@ -1651,10 +1656,10 @@ proveEq sc env t1 t2
 tNoUser :: C.Type -> C.Type
 tNoUser initialTy =
   case C.tNoUser initialTy of
-    C.TNewtype nt params
+    C.TNominal nt params
       | C.Struct fs <- C.ntDef nt ->
         if null params then C.TRec (C.ntFields fs)
-                       else error "tNoUser: Newtype with parameters"
+                       else panic "tNoUser" ["Nominal type with parameters"]
                         -- XXX: We should instantiate, see #2019
     t -> t
 
@@ -1918,8 +1923,8 @@ exportValue ty v = case ty of
   TV.TVAbstract{} ->
     error "exportValue: TODO abstract types"
 
-  -- newtypes
-  TV.TVNewtype _ _ fields ->
+  -- nominal types
+  TV.TVNominal _ _ fields ->
     case fields of
       TV.TVStruct fs -> exportValue (TV.TVRec fs) v
       TV.TVEnum {}   -> error "exportValue: TODO enum"
@@ -1998,36 +2003,37 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
     _ -> panic "importFirstOrderValue"
                 ["Expected finite value of type:", show t, "but got", show v]
 
--- | Generate functions to construct newtypes in the term environment.
--- (I.e., make identity functions that take the record the newtype wraps.)
-genNewtypeConstructors :: SharedContext -> Map C.Name Newtype -> Env -> IO Env
-genNewtypeConstructors sc newtypes env0 =
-  foldM genConstr env0 newtypes
+-- | Generate functions for nominal in the term environment.
+-- (I.e., for structs, make identity functions that take the record the
+-- newtype wraps.)
+genNominalConstructors :: SharedContext -> Map C.Name NominalType -> Env -> IO Env
+genNominalConstructors sc nominal env0 =
+  foldM genConstr env0 nominal
   where
-    genConstr :: Env -> Newtype -> IO Env
+    genConstr :: Env -> NominalType -> IO Env
     genConstr env nt = do
-      let conTs = C.newtypeConTypes nt
-      constrs <- forM (newtypeConstrs nt) $ \(x,e) ->
+      let conTs = C.nominalTypeConTypes nt
+      constrs <- forM (nominalConstrs nt) $ \(x,e) ->
         do e' <- importExpr sc env e
            pure (x,(e',0))
       let env' = env { envE = foldr (uncurry Map.insert) (envE env) constrs
                      , envC = foldr (uncurry Map.insert) (envC env) conTs
                      }
       return env'
 
-    newtypeConstrs :: Newtype -> [(C.Name,C.Expr)]
-    newtypeConstrs nt =
+    nominalConstrs :: NominalType -> [(C.Name,C.Expr)]
+    nominalConstrs nt =
       case C.ntDef nt of
         C.Struct fs ->
           let recTy = C.TRec (C.ntFields fs)
               fn    = C.EAbs paramName recTy (C.EVar paramName)
               con   = C.ntConName fs
               paramName = C.asLocal C.NSValue con
            in [(con, foldr tFn fn (C.ntParams nt))]
-        C.Enum {} -> error "genNewtypeConstrurctrs: `enum` is not yet supported"
+        C.Enum {} -> error "genNominalConstrurctrs: `enum` is not yet supported"
       where
 
         tFn tp body =
           if elem (C.tpKind tp) [C.KType, C.KNum]
             then C.ETAbs tp body
-            else panic "genNewtypeConstructors" ["illegal newtype parameter kind", show (C.tpKind tp)]
+            else panic "genNominalConstructors" ["illegal nominal type parameter kind", show (C.tpKind tp)]

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -314,8 +314,8 @@ mkCryEnv env =
           infInp <- MB.genInferInput P.emptyRange prims NoParams ifaceDecls
           let newtypeCons = Map.fromList
                               [ con
-                              | nt <- Map.elems (TM.inpNewtypes infInp)
-                              , con <- T.newtypeConTypes nt
+                              | nt <- Map.elems (TM.inpNominalTypes infInp)
+                              , con <- T.nominalTypeConTypes nt
                               ]
           pure (newtypeCons `Map.union` TM.inpVars infInp)
      let types' = Map.union (eExtraTypes env) types
@@ -416,11 +416,11 @@ loadCryptolModule sc primOpts env path = do
                   $ ME.meLoadedModules modEnv''
 
   let newDeclGroups = concatMap T.mDecls newModules
-  let newNewtypes   = Map.difference (ME.loadedNewtypes modEnv')
-                                     (ME.loadedNewtypes modEnv)
+  let newNominal    = Map.difference (ME.loadedNominalTypes modEnv')
+                                     (ME.loadedNominalTypes modEnv)
 
   newTermEnv <-
-    do cEnv <- C.genNewtypeConstructors sc newNewtypes oldCryEnv
+    do cEnv <- C.genNominalConstructors sc newNominal oldCryEnv
        newCryEnv <- C.importTopLevelDeclGroups sc primOpts cEnv newDeclGroups
        traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
@@ -518,11 +518,11 @@ importModule sc env src as vis imps = do
                     $ ME.lmLoadedModules
                     $ ME.meLoadedModules modEnv'
   let newDeclGroups = concatMap T.mDecls newModules
-  let newNewtypes   = Map.difference (ME.loadedNewtypes modEnv')
-                                     (ME.loadedNewtypes modEnv)
+  let newNominal    = Map.difference (ME.loadedNominalTypes modEnv')
+                                     (ME.loadedNominalTypes modEnv)
 
   newTermEnv <-
-    do cEnv      <- C.genNewtypeConstructors sc newNewtypes oldCryEnv
+    do cEnv      <- C.genNominalConstructors sc newNominal oldCryEnv
        newCryEnv <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions
                                                             cEnv newDeclGroups
        traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
@@ -752,7 +752,7 @@ typeNoUser t =
     T.TVar {}      -> t
     T.TUser _ _ ty -> typeNoUser ty
     T.TRec fields  -> T.TRec (fmap typeNoUser fields)
-    T.TNewtype nt ts -> T.TNewtype nt (fmap typeNoUser ts)
+    T.TNominal nt ts -> T.TNominal nt (fmap typeNoUser ts)
 
 schemaNoUser :: T.Schema -> T.Schema
 schemaNoUser (T.Forall params props ty) = T.Forall params props (typeNoUser ty)

saw/SAWScript/REPL/Monad.hs

@@ -35,7 +35,7 @@ module SAWScript.REPL.Monad (
     -- ** Environment
   , getCryptolEnv, modifyCryptolEnv, setCryptolEnv
   , getModuleEnv, setModuleEnv
-  , getTSyns, getNewtypes, getVars
+  , getTSyns, getNominalTypes, getVars
   , getExprNames
   , getTypeNames
   , getPropertyNames
@@ -397,11 +397,11 @@ getTSyns  = do
   let decls = getAllIfaceDecls me
   return (M.ifTySyns decls)
 
-getNewtypes :: REPL (Map.Map T.Name T.Newtype)
-getNewtypes = do
+getNominalTypes :: REPL (Map.Map T.Name T.NominalType)
+getNominalTypes = do
   me <- getModuleEnv
   let decls = getAllIfaceDecls me
-  return (M.ifNewtypes decls)
+  return (M.ifNominalTypes decls)
 
 -- | Get visible variable names.
 getExprNames :: REPL [String]

src/SAWScript/Builtins.hs

@@ -1945,7 +1945,7 @@ defaultTypedTerm opts sc cfg tt@(TypedTerm (TypedTermSchema schema) trm)
         C.TUser f ts t -> C.TUser f (map (plainSubst s) ts) (plainSubst s t)
         C.TRec fs      -> C.TRec (fmap (plainSubst s) fs)
         C.TVar x       -> C.apSubst s (C.TVar x)
-        C.TNewtype nt ts -> C.TNewtype nt (fmap (plainSubst s) ts)
+        C.TNominal nt ts -> C.TNominal nt (fmap (plainSubst s) ts)
 
 defaultTypedTerm _opts _sc _cfg tt = return tt
 

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -253,8 +253,8 @@ resolveSAWTerm cc tp tm =
       fail "resolveSAWTerm: unsupported function type"
     Cryptol.TVAbstract _ _ ->
       fail "resolveSAWTerm: unsupported abstract type"
-    Cryptol.TVNewtype{} ->
-      fail "resolveSAWTerm: unsupported newtype"
+    Cryptol.TVNominal {} ->
+      fail "resolveSAWTerm: unsupported nominal type"
   where
     sym = cc^.jccSym
 
@@ -303,7 +303,7 @@ toJVMType tp =
     Cryptol.TVRec _flds -> Nothing
     Cryptol.TVFun _ _ -> Nothing
     Cryptol.TVAbstract _ _ -> Nothing
-    Cryptol.TVNewtype{} -> Nothing
+    Cryptol.TVNominal {} -> Nothing
 
 equalValsPred ::
   JVMCrucibleContext ->

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -870,8 +870,8 @@ resolveSAWTerm cc tp tm =
         fail "resolveSAWTerm: invalid function type"
       Cryptol.TVAbstract _ _ ->
         fail "resolveSAWTerm: invalid abstract type"
-      Cryptol.TVNewtype{} ->
-        fail "resolveSAWTerm: invalid newtype"
+      Cryptol.TVNominal {} ->
+        fail "resolveSAWTerm: invalid nominal type"
   where
     sym = cc^.ccSym
     dl = Crucible.llvmDataLayout (ccTypeCtx cc)
@@ -932,7 +932,7 @@ toLLVMType dl tp =
     Cryptol.TVRec _flds -> Left (NotYetSupported "record")
     Cryptol.TVFun _ _ -> Left (Impossible "function")
     Cryptol.TVAbstract _ _ -> Left (Impossible "abstract")
-    Cryptol.TVNewtype{} -> Left (Impossible "newtype")
+    Cryptol.TVNominal {} -> Left (Impossible "nominal")
 
 toLLVMStorageType ::
   forall w .

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

@@ -870,8 +870,8 @@ resolveSAWTerm mcc tp tm =
       fail "resolveSAWTerm: unsupported function type"
     Cryptol.TVAbstract _ _ ->
       fail "resolveSAWTerm: unsupported abstract type"
-    Cryptol.TVNewtype{} ->
-      fail "resolveSAWTerm: unsupported newtype"
+    Cryptol.TVNominal {} ->
+      fail "resolveSAWTerm: unsupported nominal type"
   where
     sym = mcc ^. mccSym
     col = mcc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection
@@ -943,7 +943,7 @@ toMIRType tp =
     Cryptol.TVRec _flds -> Left (NotYetSupported "record")
     Cryptol.TVFun _ _ -> Left (Impossible "function")
     Cryptol.TVAbstract _ _ -> Left (Impossible "abstract")
-    Cryptol.TVNewtype{} -> Left (Impossible "newtype")
+    Cryptol.TVNominal {} -> Left (Impossible "nominal")
 
 -- | Check if two MIR references are equal.
 equalRefsPred ::