From 00e216a6e8a8c7a787c391befcd88b8d6944c1fb Mon Sep 17 00:00:00 2001 From: Bretton Date: Sat, 18 Nov 2023 04:12:49 -0600 Subject: [PATCH 1/3] Allow type synonyms inside other type synonyms Instantiate the body of a type synonym declaration with the existing type synonym map before adding it to the map, so that the map never contains any uninstantiated type synonyms. --- src/SAWScript/MGU.hs | 14 +++++++++++--- src/SAWScript/Value.hs | 4 +++- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index 47ab549f28..d9e34ce0fc 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -17,6 +17,7 @@ Stability : provisional module SAWScript.MGU ( checkDecl , checkDeclGroup + , instantiateType ) where import SAWScript.AST @@ -264,8 +265,12 @@ bindPatternSchema pat s@(Forall vs t) m = bindTypedef :: LName -> Type -> TI a -> TI a bindTypedef n t m = - TI $ local (\ro -> ro { typedefEnv = M.insert (getVal n) t $ typedefEnv ro }) - $ unTI m + TI $ + local + (\ro -> + let t' = instantiateType (typedefEnv ro) t + in ro { typedefEnv = M.insert (getVal n) t' $ typedefEnv ro }) + $ unTI m -- FIXME: This function may miss type variables that occur in the type -- of a binding that has been shadowed by another value with the same @@ -382,10 +387,13 @@ instance Instantiate Type where TySkolemVar _ _ -> ty LType pos ty' -> LType pos (instantiate nts ty') +instantiateType :: Instantiate t => Map Name Type -> t -> t +instantiateType tenv = instantiate (M.assocs tenv) + instantiateM :: Instantiate t => t -> TI t instantiateM t = do s <- TI $ asks typedefEnv - return $ instantiate (M.assocs s) t + return $ instantiateType s t -- }}} diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 7875521e1e..f2a88fac9c 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -77,6 +77,7 @@ import qualified Text.LLVM.AST as LLVM (Type) import qualified Text.LLVM.PP as LLVM (ppType) import SAWScript.JavaExpr (JavaType(..)) import SAWScript.JavaPretty (prettyClass) +import SAWScript.MGU (instantiateType) import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity(..)) import SAWScript.Proof import SAWScript.Prover.SolverStats @@ -504,7 +505,8 @@ extendLocal :: SS.LName -> Maybe SS.Schema -> Maybe String -> Value -> LocalEnv extendLocal x mt md v env = LocalLet x mt md v : env addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW -addTypedef name ty rw = rw { rwTypedef = M.insert name ty (rwTypedef rw) } +addTypedef name ty rw = rw { rwTypedef = M.insert name ty' (rwTypedef rw) } + where ty' = instantiateType (rwTypedef rw) ty mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW mergeLocalEnv sc env rw = foldrM addBinding rw env From 2187d815cb74afdc5cb7a5fea7bbd332e23b3f18 Mon Sep 17 00:00:00 2001 From: Bretton Date: Sat, 18 Nov 2023 05:13:15 -0600 Subject: [PATCH 2/3] Add test for #1985 --- intTests/test1985/test.saw | 12 ++++++++++++ intTests/test1985/test.sh | 3 +++ 2 files changed, 15 insertions(+) create mode 100644 intTests/test1985/test.saw create mode 100644 intTests/test1985/test.sh diff --git a/intTests/test1985/test.saw b/intTests/test1985/test.saw new file mode 100644 index 0000000000..2a7c862134 --- /dev/null +++ b/intTests/test1985/test.saw @@ -0,0 +1,12 @@ +// Test top level typedefs +typedef Foo = Int; +typedef Bar = Foo; +let thing : Bar = 2; + +// Test local typedefs +let local = do { + typedef LocalFoo = Bar; + typedef LocalBar = LocalFoo; + let local_thing : LocalBar = 3; + return (); +}; diff --git a/intTests/test1985/test.sh b/intTests/test1985/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1985/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw From 17f0ed75808454dfa2415cdc482e1d243005bfba Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 4 Dec 2023 22:01:01 -0600 Subject: [PATCH 3/3] Use Map in SAWScript.MGU.instantiate --- src/SAWScript/MGU.hs | 16 +++++++--------- src/SAWScript/Value.hs | 4 ++-- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index d9e34ce0fc..14507d401e 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -17,7 +17,7 @@ Stability : provisional module SAWScript.MGU ( checkDecl , checkDeclGroup - , instantiateType + , instantiate ) where import SAWScript.AST @@ -268,7 +268,7 @@ bindTypedef n t m = TI $ local (\ro -> - let t' = instantiateType (typedefEnv ro) t + let t' = instantiate (typedefEnv ro) t in ro { typedefEnv = M.insert (getVal n) t' $ typedefEnv ro }) $ unTI m @@ -370,7 +370,8 @@ instance AppSubst Decl where -- Instantiate {{{ class Instantiate t where - instantiate :: [(Name, Type)] -> t -> t + -- | @instantiate m x@ applies the map @m@ to type variables in @x@. + instantiate :: Map Name Type -> t -> t instance (Instantiate a) => Instantiate (Maybe a) where instantiate nts = fmap (instantiate nts) @@ -382,18 +383,15 @@ instance Instantiate Type where instantiate nts ty = case ty of TyCon tc ts -> TyCon tc (instantiate nts ts) TyRecord fs -> TyRecord (fmap (instantiate nts) fs) - TyVar n -> maybe ty id (lookup n nts) + TyVar n -> M.findWithDefault ty n nts TyUnifyVar _ -> ty TySkolemVar _ _ -> ty LType pos ty' -> LType pos (instantiate nts ty') -instantiateType :: Instantiate t => Map Name Type -> t -> t -instantiateType tenv = instantiate (M.assocs tenv) - instantiateM :: Instantiate t => t -> TI t instantiateM t = do s <- TI $ asks typedefEnv - return $ instantiateType s t + return $ instantiate s t -- }}} @@ -492,7 +490,7 @@ inferE (ln, expr) = case expr of return (Var x, t) Just (Forall as t) -> do ts <- mapM (const newType) as - return (Var x, instantiate (zip as ts) t) + return (Var x, instantiate (M.fromList (zip as ts)) t) Function pat body -> do (pt, pat') <- newTypePattern pat diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index f2a88fac9c..532c4bd654 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -77,7 +77,7 @@ import qualified Text.LLVM.AST as LLVM (Type) import qualified Text.LLVM.PP as LLVM (ppType) import SAWScript.JavaExpr (JavaType(..)) import SAWScript.JavaPretty (prettyClass) -import SAWScript.MGU (instantiateType) +import SAWScript.MGU (instantiate) import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity(..)) import SAWScript.Proof import SAWScript.Prover.SolverStats @@ -506,7 +506,7 @@ extendLocal x mt md v env = LocalLet x mt md v : env addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW addTypedef name ty rw = rw { rwTypedef = M.insert name ty' (rwTypedef rw) } - where ty' = instantiateType (rwTypedef rw) ty + where ty' = instantiate (rwTypedef rw) ty mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW mergeLocalEnv sc env rw = foldrM addBinding rw env