diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 2594589820..eb779d6faf 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/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,16 +2003,17 @@ 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 @@ -2015,8 +2021,8 @@ genNewtypeConstructors sc newtypes env0 = } 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) @@ -2024,10 +2030,10 @@ genNewtypeConstructors sc newtypes env0 = 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)] diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index be65d31cce..4276711491 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/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) diff --git a/deps/cryptol b/deps/cryptol index 3e072f76da..1e07d0d31c 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 3e072f76da01448015efd40f34cd74b82d0ce7fb +Subproject commit 1e07d0d31c6d3bb87a3c79e1a3be5d58b4bc0094 diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index e75aee760b..15fc84783f 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/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] diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index eb3ed0d806..a3de996e63 100644 --- a/src/SAWScript/Builtins.hs +++ b/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 diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 98f38a0d14..b63e7eb4f8 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/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 -> diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index b5fd1bdbf6..6cda7aaa69 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/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 . diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 57ce46397d..ad68fdcf1b 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/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 ::