Merge pull request #1986 from GaloisInc/T1985

Allow type synonyms inside other type synonyms

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 ();
+};

intTests/test1985/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

src/SAWScript/MGU.hs

@@ -17,6 +17,7 @@ Stability   : provisional
 module SAWScript.MGU
        ( checkDecl
        , checkDeclGroup
+       , instantiate
        ) 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' = instantiate (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
@@ -365,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)
@@ -377,15 +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')
 
 instantiateM :: Instantiate t => t -> TI t
 instantiateM t = do
   s <- TI $ asks typedefEnv
-  return $ instantiate (M.assocs s) t
+  return $ instantiate s t
 
 -- }}}
 
@@ -484,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

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 (instantiate)
 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' = instantiate (rwTypedef rw) ty
 
 mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW
 mergeLocalEnv sc env rw = foldrM addBinding rw env