Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Allow type synonyms inside other type synonyms #1986

Merged
merged 4 commits into from
Dec 5, 2023
Merged

Allow type synonyms inside other type synonyms #1986

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
00e216a
Allow type synonyms inside other type synonyms
qsctr Nov 18, 2023
2187d81
Add test for #1985
qsctr Nov 18, 2023
17f0ed7
Use Map in SAWScript.MGU.instantiate
qsctr Dec 5, 2023
6782359
Merge branch 'master' into T1985
mergify[bot] Dec 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
12 changes: 12 additions & 0 deletions intTests/test1985/test.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 ();
};
3 changes: 3 additions & 0 deletions intTests/test1985/test.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw
14 changes: 11 additions & 3 deletions src/SAWScript/MGU.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Stability : provisional
module SAWScript.MGU
( checkDecl
, checkDeclGroup
, instantiateType
) where

import SAWScript.AST
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This does almost the exact same thing as the instantiate method of the Instantiate class, except that this function uses a Map Name Type instead of [(Name, Type)]. I think using a Map makes more sense here—any objection to simply changing the type signature of instantiate to use a Map instead?

Either way, it would be worth leaving a comment saying precisely what we are instantiating. (Particularly, we're instantiating typedefs.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I've changed instantiate to use Map. It seems like it's not only used with typedefs, so I wrote a more general description.


instantiateM :: Instantiate t => t -> TI t
instantiateM t = do
s <- TI $ asks typedefEnv
return $ instantiate (M.assocs s) t
return $ instantiateType s t

-- }}}

Expand Down
4 changes: 3 additions & 1 deletion src/SAWScript/Value.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down