packages feed

paragon 0.1.21 → 0.1.22

raw patch · 20 files changed

+578/−485 lines, 20 files

Files

paragon.cabal view
@@ -1,5 +1,5 @@ Name:                   paragon-Version:                0.1.21+Version:                0.1.22 License:                BSD3 License-File:           LICENSE Author:                 Niklas Broberg
src/Language/Java/Paragon.hs view
@@ -78,7 +78,8 @@       -- Workaround for old and buggy 'filepath' versions       _directory = if null directoryRaw then "./" else directoryRaw   pp <- getPIPATH-  let pDirs = concat [ splitSearchPath dir | PiPath dir <- flags ] ++ pp+  let pDirsSpec = concat [ splitSearchPath dir | PiPath dir <- flags ] ++ pp+      pDirs = if null pDirsSpec then ["./"] else pDirsSpec   fc <- readFile filePath   runBaseErr $ do     ast <- liftShowEither $ parser compilationUnit fc
src/Language/Java/Paragon/Interaction.hs view
@@ -49,7 +49,7 @@ issueTracker = "http://code.google.com/p/paragon-java/issues/entry"  versionString :: String-versionString = "0.1.19"+versionString = "0.1.22"  libraryBase, typeCheckerBase :: String libraryBase = "Language.Java.Paragon"
src/Language/Java/Paragon/Monad/Base.hs view
@@ -3,7 +3,7 @@      ErrCtxt, Uniq, BaseM, runBaseM, runBaseErr,       MonadIO(..), MonadBase(..), -     liftEither, liftShowEither,+     liftEither, liftShowEither, tryCatch,       getUniqRef, getErrCtxt, withErrCtxt, @@ -73,14 +73,25 @@ class MonadIO m => MonadBase m where   liftBase :: BaseM a -> m a   withErrCtxt' :: (ErrCtxt -> ErrCtxt) -> m a -> m a+  tryM :: m a -> m (Either String a)  instance MonadBase BaseM where   liftBase = id   withErrCtxt' strff (BaseM f) = BaseM $ \ec u -> f (strff ec) u+  tryM (BaseM f) = BaseM $ \ec u -> do+                           esa <- f ec u+                           return $ Right esa   withErrCtxt :: MonadBase m => String -> m a -> m a withErrCtxt str = withErrCtxt' (. (str ++))++tryCatch :: MonadBase m => m a -> (String -> m a) -> m a+tryCatch tr ctch = do esa <- tryM tr+                      case esa of+                        Right a -> return a+                        Left err -> ctch err+  -------------------------------------------- --                                        --
src/Language/Java/Paragon/Monad/PiReader.hs view
@@ -53,6 +53,7 @@ instance MonadBase PiReader where   liftBase ba = PiReader $ \_ -> ba   withErrCtxt' ecf (PiReader f) = PiReader $ withErrCtxt' ecf . f+  tryM (PiReader f) = PiReader $ tryM . f  instance MonadIO PiReader where   liftIO = liftBase . liftIO
src/Language/Java/Paragon/NameResolution.hs view
@@ -1,9 +1,9 @@-{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TupleSections, QuasiQuotes #-} module Language.Java.Paragon.NameResolution (resolveNames) where  import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty--- import Language.Java.Paragon.Parser+import Language.Java.Paragon.QuasiQuoter import Language.Java.Paragon.Interaction  import Language.Java.Paragon.NameResolution.Monad@@ -28,10 +28,11 @@ resolveNames :: PiPath                -- PIPATH              -> CompilationUnit ()      -- Compilation unit to transform              -> BaseM (CompilationUnit ())-resolveNames piPath (CompilationUnit _ _pkg imps [td]) = runPiReader ("./":piPath) $ do+resolveNames piPath (CompilationUnit _ _pkg imps [td]) = runPiReader piPath $ do+  (_, javaLangExpnMap) <- buildMapFromImportName [impDeclQQ| import java.lang.*; |]   (imps', impExpnMap) <- buildMapFromImports imps   piExpnMap           <- buildMapFromPiPath-  let jipExpnMap = unionExpnMaps [javaExpnMap, impExpnMap, piExpnMap]+  let jipExpnMap = unionExpnMaps [javaExpnMap, javaLangExpnMap, impExpnMap, piExpnMap]   (tnExpnMap,supExpnMap) <- buildMapFromTd td jipExpnMap   -- We need to take the current name take precedence   let expnMap = Map.union tnExpnMap (unionExpnMaps [jipExpnMap,supExpnMap])@@ -658,7 +659,9 @@                   -- The package name 'java' is always in scope. javaExpnMap :: Expansion-javaExpnMap = Map.fromList $ mkPExpansion (Ident () "java")+javaExpnMap = Map.fromList $ +                mkPExpansion (Ident () "java")+  {- buildMapFromCurrentPkg :: FilePath -> PiReader Expansion
src/Language/Java/Paragon/NameResolution/Monad.hs view
@@ -37,6 +37,7 @@ instance MonadBase NameRes where   liftBase = liftPR . liftBase   withErrCtxt' prf (NameRes f) = NameRes $ withErrCtxt' prf . f+  tryM (NameRes f) = NameRes $ tryM . f  instance MonadIO NameRes where   liftIO = liftPR . liftIO
src/Language/Java/Paragon/PiGeneration.hs view
@@ -23,10 +23,10 @@ transformCompilationUnit :: CompilationUnit () -> CompilationUnit () transformCompilationUnit (CompilationUnit _ mpDecl _  [tdecl])   = let cu = CompilationUnit () mpDecl []  [transformTypeDecl tdecl]-    in expandLocals preName locals cu-        where prePre = fmap (\(PackageDecl _ n) -> n) mpDecl+    in {- expandLocals preName locals -} cu+{-        where prePre = fmap (\(PackageDecl _ n) -> n) mpDecl               preName = Name () TName prePre i-              (i, locals) = gatherLocalAlps tdecl+              (i, locals) = gatherLocalAlps tdecl -} transformCompilationUnit _ = panic (piGenModule ++ ".transformCompilationUnit") $                              "More than one type decl" 
src/Language/Java/Paragon/QuasiQuoter.hs view
@@ -47,7 +47,8 @@ stmtQQ = parserQQ stmt lhsQQ  = parserQQ lhs -varDeclQQ, methodBodyQQ, memberDeclQQ, fieldDeclQQ, methodDeclQQ, +impDeclQQ,+  varDeclQQ, methodBodyQQ, memberDeclQQ, fieldDeclQQ, methodDeclQQ,    modifiersQQ, formalParamQQ, blockStmtQQ, classDeclQQ, lockPropQQ :: QuasiQuoter varDeclQQ    = parserQQ varDecl methodBodyQQ = parserQQ methodBody @@ -59,3 +60,4 @@ blockStmtQQ  = parserQQ blockStmt classDeclQQ  = parserQQ classDecl lockPropQQ   = parserQQ lockProperties+impDeclQQ    = parserQQ importDecl
src/Language/Java/Paragon/QuasiQuoter/Lift.hs view
@@ -110,6 +110,7 @@        ''VarDeclId,        ''ExplConstrInv,        ''Stmt,+       ''ImportDecl,        ''EnumConstant, ''ForInit, ''SwitchBlock, ''Catch,        ''SwitchLabel, ''EnumBody]) 
src/Language/Java/Paragon/TypeCheck.hs view
@@ -46,16 +46,16 @@ ------------------------------------------------------------------------------------- -- Here goes TcTypeDecl.hs -typeCheckTd :: TypeCheck (TcDeclM r) TypeDecl+typeCheckTd :: TypeCheck TcDeclM TypeDecl typeCheckTd (ClassTypeDecl     _ cdecl) = ClassTypeDecl Nothing <$> typeCheckCd cdecl typeCheckTd (InterfaceTypeDecl _ idecl) = InterfaceTypeDecl Nothing <$> typeCheckId idecl -typeCheckId :: TypeCheck (TcDeclM r) InterfaceDecl+typeCheckId :: TypeCheck TcDeclM InterfaceDecl typeCheckId (InterfaceDecl _ _ms i tps supers (InterfaceBody _ memberDecls)) = do   --debug "typeCheckId"   withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do   let staticWPol = top-  withThisType i tps supers $ do+  registerThisType i tps supers   withFoldMap withTypeParam tps $    typeCheckActorFields memberDecls $ do     --debug "typeCheckLockDecls start"@@ -66,13 +66,14 @@     typeCheckPolicyFields memberDecls $ do      --debug "typeCheckSignatures start"      typeCheckSignatures memberDecls $ \constrWPol -> do+      registerThisTypeSigs i tps supers       --debug "typeCheckMemberDecls start"       InterfaceDecl Nothing (map notAppl _ms) (notAppl i)          (map notAppl tps) (map notAppl supers) .           InterfaceBody Nothing <$>               typeCheckMemberDecls staticWPol constrWPol memberDecls -typeCheckCd :: TypeCheck (TcDeclM r) ClassDecl+typeCheckCd :: TypeCheck TcDeclM ClassDecl typeCheckCd (ClassDecl _ ms i tps mSuper _impls (ClassBody _ decls)) = do   --debug "typeCheckCd"   withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do@@ -82,9 +83,9 @@       inits       = [ idecl | idecl@(InitDecl {}) <- decls ]       supers      = maybe [] (:[]) mSuper   withFoldMap withTypeParam tps $ do-  withThisType i tps supers $ do+  registerThisType i tps supers --  withFoldMap withSuperType (maybe [] (:[]) mSuper) $ do-   typeCheckActorFields memberDecls $ do+  typeCheckActorFields memberDecls $ do     debugPrint "typeCheckLockDecls start"     typeCheckLockDecls memberDecls $ do     debugPrint "typeCheckTypeMethods start"@@ -93,7 +94,7 @@     typeCheckPolicyFields memberDecls $ do      debugPrint "typeCheckSignatures start"      typeCheckSignatures memberDecls $ \constrWPol -> do-      withThisTypeSigs i tps supers $ do+        registerThisTypeSigs i tps supers         ClassDecl Nothing (map notAppl ms) (notAppl i)            (map notAppl tps) (fmap notAppl mSuper) (map notAppl _impls) .             ClassBody Nothing <$> do@@ -106,8 +107,8 @@ typeCheckCd _ = panic (typeCheckerBase ++ ".typeCheckCd")                 "Enum decls not yet supported" -withThisType :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM r a -> TcDeclM r a-withThisType i tps supers tcda = do+registerThisType :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM ()+registerThisType i tps supers = do     cTys   <- mapM evalSrcClsType supers     baseTm <- getTypeMap     let superTMs = flip map cTys $ \cTy -> @@ -117,17 +118,17 @@                               $ "Super type evaluated but now doesn't exist: " ++ show mErr                        Right superSig -> (tMembers superSig) { constrs = Map.empty } -    withTypeMap (\tm ->+    extendGlobalTypeMap (\tm ->         -- We insert an empty typemap at first,         -- since we are only using this when checking signatures         let thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) [])                          True False cTys [] emptyTM             newTm = tm { types = Map.insert i (tps,thisSig) (types tm) } -        in foldl merge newTm superTMs) $ tcda+        in foldl merge newTm superTMs)            -withThisTypeSigs :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM r a -> TcDeclM r a-withThisTypeSigs i tps supers tcba = do+registerThisTypeSigs :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM ()+registerThisTypeSigs i tps supers = do   cTys   <- mapM evalSrcClsType supers   baseTm <- getTypeMap   let superTMs = flip map cTys $ \cTy -> @@ -141,30 +142,8 @@       resTm  = foldl merge thisTm superTMs       thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) [])                    True False cTys [] resTm -- TODO: Include proper values-  withTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig) $-    tcba+  extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig) -withTypeParam :: TypeParam () -> TcDeclM r a -> TcDeclM r a-withTypeParam tp tcba = -    case tp of-      ActorParam _ i -> do-          let vti = VSig actorT top False False True-          withTypeMap (\tm -> -              tm { actors = Map.insert i (ActorTPVar i) (actors tm),-                   fields = Map.insert i vti (fields tm) }) $ tcba-      PolicyParam _ i -> do-           let vti = VSig policyT top False False True-           withTypeMap (\tm ->-              tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm),-                   fields = Map.insert i vti (fields tm) }) $ tcba-      LockStateParam _ i -> do-          let vti = VSig (lockT []) top False False True-          withTypeMap (\tm ->-              tm { fields = Map.insert i vti (fields tm) }) $ tcba-      TypeParam _ _i _ -> do-          --withTypeMap (\tm ->-          --    tm { types = Map.insert i ([],Map.empty) (types tm) }) $ -            tcba  --------------------------------------------------------------- -- Actors@@ -172,7 +151,7 @@ -- TODO: We may have a problem with boot-strapping here. -- We can stay clear of the problem for now, using careful -- Paragon coding, but we need to think about it and fix it eventually.-typeCheckActorFields :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a+typeCheckActorFields :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a typeCheckActorFields mDecls tcba = do     --debug "fetchActors"     let acts = [ (ms, vd) @@ -191,14 +170,14 @@         tcba                      where spawnActorVd, evalActorVd -- , aliasActorVd -                      :: ([Modifier ()],VarDecl ()) -> TcDeclM r a -> TcDeclM r a+                      :: ([Modifier ()],VarDecl ()) -> TcDeclM a -> TcDeclM a                   -- Only Nothing for initializer                   spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do                     a <- freshActorId (prettyPrint i)                     p <- getReadPolicy ms                     let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)-                    withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),-                                             fields = Map.insert i vti (fields tm) }) $+                    withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),+                                                    fields = Map.insert i vti (fields tm) }) $                       tcra                   spawnActorVd (_, VarDecl _ arvid _) _ =                       fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid@@ -226,8 +205,8 @@                                Just a -> return a                                Nothing -> aliasActorId --fail "Internal error: no such actor"                            _ -> aliasActorId-                    withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),-                                             fields = Map.insert i vti (fields tm) }) $+                    withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),+                                                    fields = Map.insert i vti (fields tm) }) $                       tcra                   evalActorVd (_, VarDecl _ _ Nothing) _ = panic (typeCheckerBase ++ ".evalActorVd") $ "No initializer"                   evalActorVd (_, VarDecl _ arvid _)   _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid@@ -237,18 +216,18 @@ --------------------------------------------------------------- -- Locks -typeCheckLockDecls :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a+typeCheckLockDecls :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a typeCheckLockDecls mds tcba = do   let ls = [ ld | ld@ LockDecl {} <- mds ]   withFoldMap typeCheckLockDecl ls $ tcba -typeCheckLockDecl :: MemberDecl () -> TcDeclM r a -> TcDeclM r a+typeCheckLockDecl :: MemberDecl () -> TcDeclM a -> TcDeclM a typeCheckLockDecl (LockDecl _ ms i mps mProps) tcba = do   lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do     pol <- getLockPolicy ms     prs <- evalSrcLockProps i mProps     return $ LSig pol (length mps) prs-  withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $+  withCurrentTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $     tcba  --typeCheckLockDecl (LockDecl _ _ _ _ _) _ = fail $ "Lock properties not yet supported"@@ -258,7 +237,7 @@ --------------------------------------------------------------- -- Typemethods -typeCheckTypeMethods :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a+typeCheckTypeMethods :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a typeCheckTypeMethods mds tcba = do   let tms = [ tmd | tmd@(MethodDecl _ ms _ _ _ _ _ _) <- mds,                     Typemethod () `elem` ms@@ -270,7 +249,7 @@       tcba  -- Precondition: only applied on actual typemethods-typeCheckTMSig :: MemberDecl () -> TcDeclM r a -> TcDeclM r a+typeCheckTMSig :: MemberDecl () -> TcDeclM a -> TcDeclM a typeCheckTMSig (MethodDecl _ ms tps retT i ps exns _) tcba = do   newMethMap <- withErrCtxt ("When checking signature of typemethod "                                 ++ prettyPrint i ++ ":\n") $ do@@ -302,16 +281,16 @@         newMethMap = Map.singleton (tps, tyPs, isVarArity) mti     return newMethMap -  withTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $+  withCurrentTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $        tcba  typeCheckTMSig md _ = panic (typeCheckerBase ++ ".typeCheckTMSig") $                       "Applied to non-method decl " ++ show md -addTMBody :: MemberDecl () -> TcDeclM r a -> TcDeclM r a+addTMBody :: MemberDecl () -> TcDeclM a -> TcDeclM a addTMBody (MethodDecl _ _ _ _ i ps _ (MethodBody _ (Just bl))) =     let pis = [ iP | FormalParam _ _ _ _ (VarId _ iP) <- ps ]-    in withTypeMap $ \tm -> tm { typemethods = Map.insert i (pis,bl) (typemethods tm) }+    in withCurrentTypeMap $ \tm -> tm { typemethods = Map.insert i (pis,bl) (typemethods tm) } addTMBody md = panic (typeCheckerBase ++ ".addTMBody") $                "Applied to non-method decl " ++ show md @@ -319,14 +298,14 @@ ------------------------------------------------------------------------------------- -- Policies -typeCheckPolicyFields :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a+typeCheckPolicyFields :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a typeCheckPolicyFields mds =     let pfs = [ pf | pf@(FieldDecl _ _ (PrimType _ (PolicyT _)) _) <- mds ] in     -- The 'map' here means fields can only refer to things above them     withFoldMap typeCheckPolicyField pfs  -- Precondition: only apply on policies-typeCheckPolicyField :: MemberDecl () -> TcDeclM r a -> TcDeclM r a+typeCheckPolicyField :: MemberDecl () -> TcDeclM a -> TcDeclM a typeCheckPolicyField fd@(FieldDecl _ ms t vds) tcba = do   --debug "typeCheckPolicyField"   -- 0. Flatten@@ -357,14 +336,14 @@       tcba              where -            addField :: VarFieldSig -> Ident () -> TcDeclM r a -> TcDeclM r a+            addField :: VarFieldSig -> Ident () -> TcDeclM a -> TcDeclM a             addField vti i = -                    withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) })+                    withCurrentTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) })  typeCheckPolicyField fd _ = panic (typeCheckerBase ++ ".typeCheckPolicyField") $                            "Applied to non-policy decl " ++ show fd -evalAddPolicyInit :: CodeState -> (Ident (), VarInit ()) -> TcDeclM r a -> TcDeclM r a+evalAddPolicyInit :: CodeState -> (Ident (), VarInit ()) -> TcDeclM a -> TcDeclM a evalAddPolicyInit st (i, InitExp _ eInit) tcba = do   --debug $ "evalAddInit: " ++ show i   tcPol <- withErrCtxt ("When evaluating the initializer of field " @@ -373,7 +352,7 @@   check (isPolicyType tyInit) $         "Cannot initialize policy field " ++ prettyPrint i ++         " with non-policy expression " ++ prettyPrint eInit ++ " of type " ++ prettyPrint tyInit-  withTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $+  withCurrentTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $     tcba evalAddPolicyInit _ (i, arrInit) _ =      fail $ "Cannot initialize policy field " ++ prettyPrint i ++@@ -382,19 +361,19 @@ ------------------------------------------------------------------------------ -- Signatures -typeCheckSignatures :: [MemberDecl ()] -> (ActorPolicy -> TcDeclM r a) -> TcDeclM r a+typeCheckSignatures :: [MemberDecl ()] -> (ActorPolicy -> TcDeclM a) -> TcDeclM a typeCheckSignatures mds tcbaf = do   st <- setupStartState   withFoldMap (typeCheckSignature st) mds $     getConstrPol >>= tcbaf -getConstrPol :: TcDeclM r ActorPolicy+getConstrPol :: TcDeclM ActorPolicy getConstrPol = do   mConstrs <- constrs <$> getTypeMap   let wPols = map cWrites $ Map.elems mConstrs   return $ foldl join bottom wPols -typeCheckSignature :: CodeState -> MemberDecl () -> TcDeclM r a -> TcDeclM r a+typeCheckSignature :: CodeState -> MemberDecl () -> TcDeclM a -> TcDeclM a -- Fields typeCheckSignature st (FieldDecl _ ms t vds) tcba      | t /= PrimType () (PolicyT ()) && t /= PrimType () (ActorT ()) = do@@ -413,7 +392,7 @@     mapM_ (typeCheckPolicyMod st) rPolExps     rPol <- getReadPolicy ms     check (Final () `elem` ms || (not $ includesThis rPol)) $-          "Non-final field may not reference " ++ prettyPrint thisP+          "Non-final field may not reference " ++ prettyPrint (thisP :: PrgPolicy TcActor)      -- 3. Add signature to typemap     return $ VSig {@@ -426,9 +405,9 @@   withFoldMap (addField vti) vds $     tcba -        where addField :: VarFieldSig -> VarDecl () -> TcDeclM r a -> TcDeclM r a+        where addField :: VarFieldSig -> VarDecl () -> TcDeclM a -> TcDeclM a               addField vti (VarDecl _ (VarId _ i) _) =-                  withTypeMap $ \tm -> +                  withCurrentTypeMap $ \tm ->                        tm { fields = Map.insert i vti (fields tm) }               addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd @@ -470,7 +449,7 @@                        (FormalParam _ _ _ b _ : _) -> b     return $ Map.singleton (tps, pTs, isVarArity) mti -  withTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $+  withCurrentTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $     tcba  -- Constructors@@ -504,7 +483,7 @@                        (FormalParam _ _ _ b _ : _) -> b     return (pTs, isVarArity, cti) -  withTypeMap (\tm -> tm { constrs = Map.insert (tps, pTs, isVA) cti (constrs tm) }) $+  withCurrentTypeMap (\tm -> tm { constrs = Map.insert (tps, pTs, isVA) cti (constrs tm) }) $     tcba  -- Locks -- already handled@@ -520,10 +499,10 @@  typeCheckSignature _ _ tcba = tcba -withParam :: (FormalParam (), TcType, ActorPolicy) -> TcDeclM r a -> TcDeclM r a+withParam :: (FormalParam (), TcType, ActorPolicy) -> TcDeclM a -> TcDeclM a withParam (FormalParam _ ms _ _ (VarId _ i), ty, p) = do     let vsig = VSig ty p True (Static () `elem` ms) (Final () `elem` ms)-    withTypeMap $ \tm -> +    withCurrentTypeMap $ \tm ->          tm { fields = Map.insert i vsig (fields tm) }  @@ -531,7 +510,7 @@     fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid  -typeCheckExnSig :: CodeState -> ExceptionSpec () -> TcDeclM r (TcType, ExnSig)+typeCheckExnSig :: CodeState -> ExceptionSpec () -> TcDeclM (TcType, ExnSig) typeCheckExnSig st (ExceptionSpec _ ms xT) = do   withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do     ty <- TcRefT <$> evalSrcRefType xT@@ -552,7 +531,7 @@              }     return (ty, xSig) -checkPolicyMods :: CodeState -> [Modifier ()] -> String -> TcDeclM r ()+checkPolicyMods :: CodeState -> [Modifier ()] -> String -> TcDeclM () checkPolicyMods st ms failStr = do   --debug $ "checkPolicyMods: " ++ show ms   let rPolExps = [ e | Reads  _ e <- ms ] @@ -560,7 +539,7 @@   check (length rPolExps <= 1 && length wPolExps <= 1) failStr   mapM_ (typeCheckPolicyMod st) $ rPolExps ++ wPolExps -checkLMMods :: [Modifier ()] -> TcDeclM r LockMods+checkLMMods :: [Modifier ()] -> TcDeclM LockMods checkLMMods ms = do   let cs = concat [ l | Closes _ l <- ms ]       os = concat [ l | Opens  _ l <- ms ]@@ -568,12 +547,12 @@   tcOs <- mapM evalLock os   return (tcCs, tcOs) -checkExpectsMods :: [Modifier ()] -> TcDeclM r [TcLock]+checkExpectsMods :: [Modifier ()] -> TcDeclM [TcLock] checkExpectsMods ms = do   let es = concat [ l | Expects _ l <- ms ]   mapM evalLock es -typeCheckParam :: CodeState -> FormalParam () -> TcDeclM r (TcType, ActorPolicy)+typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, ActorPolicy) typeCheckParam st (FormalParam _ ms t ell (VarId _ i)) = do   withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do     -- 1. Check parameter type@@ -586,7 +565,7 @@ typeCheckParam _ (FormalParam _ _ _ _ arvid) =     fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -typeCheckPolicyMod :: CodeState -> Policy () -> TcDeclM r (Policy T)+typeCheckPolicyMod :: CodeState -> Policy () -> TcDeclM (Policy T) typeCheckPolicyMod st polExp = do   -- tm <- getTypeMap   -- debug $ show tm@@ -605,21 +584,21 @@ -- Initializers  -- Precondition: Only init decls-typeCheckInitDecls :: ActorPolicy -> ActorPolicy -> [Decl ()] -> TcDeclM r [Decl T]+typeCheckInitDecls :: ActorPolicy -> ActorPolicy -> [Decl ()] -> TcDeclM [Decl T] typeCheckInitDecls sLim cLim is = do   stSt <- setupStartState   (sIs, st) <- go (typeCheckInitDecl sLim) stSt [] [ bl | InitDecl _ True  bl <- is ]   (iIs, _ ) <- go (typeCheckInitDecl cLim) st   [] [ bl | InitDecl _ False bl <- is ]   return (map (InitDecl Nothing True) sIs ++ map (InitDecl Nothing False) iIs) -      where go :: (CodeState -> Block () -> TcDeclM r (CodeState, Block T))-               -> CodeState -> [Block T] -> [Block ()] -> TcDeclM r ([Block T], CodeState)+      where go :: (CodeState -> Block () -> TcDeclM (CodeState, Block T))+               -> CodeState -> [Block T] -> [Block ()] -> TcDeclM ([Block T], CodeState)             go _ st acc [] = return (reverse acc, st)             go f st acc (bl:bls) = do (st', blT) <- f st bl                                       go f st' (blT:acc) bls    -typeCheckInitDecl :: ActorPolicy -> CodeState -> Block () -> TcDeclM r (CodeState, Block T)+typeCheckInitDecl :: ActorPolicy -> CodeState -> Block () -> TcDeclM (CodeState, Block T) typeCheckInitDecl lim st bl = do     tm <- getTypeMap     (newSB,cs) <- runTcCodeM (simpleEnv lim $ "initializer block") st $@@ -633,12 +612,12 @@ ------------------------------------------------------------------------------ -- Bodies -typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM r [MemberDecl T]+typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM [MemberDecl T] typeCheckMemberDecls sLim cLim ms = do   st <- setupStartState   mapM (typeCheckMemberDecl sLim cLim st) ms -typeCheckMemberDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck (TcDeclM r) MemberDecl+typeCheckMemberDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck TcDeclM MemberDecl typeCheckMemberDecl sLim cLim st fd@(FieldDecl {}) =     typeCheckFieldDecl sLim cLim st fd typeCheckMemberDecl _ _ st md@(MethodDecl {}) =@@ -647,7 +626,7 @@     typeCheckConstrDecl st cd typeCheckMemberDecl _ _ _ md = return $ notAppl md -typeCheckFieldDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck (TcDeclM r) MemberDecl+typeCheckFieldDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck TcDeclM MemberDecl typeCheckFieldDecl staticLim constrLim st (FieldDecl _ ms _t vds) = do   --debug $ "typeCheckFieldDecl:" ++ show fd   let lim = if Static () `elem` ms then staticLim else constrLim@@ -657,7 +636,7 @@ typeCheckFieldDecl _ _ _ md = panic (typeCheckerBase ++ ".typeCheckFieldDecl") $                               "Applied to non-field decl " ++ show md -typeCheckVarDecl :: ActorPolicy -> CodeState -> TypeCheck (TcDeclM r) VarDecl+typeCheckVarDecl :: ActorPolicy -> CodeState -> TypeCheck TcDeclM VarDecl typeCheckVarDecl lim st vd@(VarDecl _ (VarId _ i) mInit) = do   --debug $ "typeCheckVarDecl:" ++ show i   withErrCtxt ("When checking initializer of field " ++ prettyPrint i ++ ":\n") $ do@@ -691,7 +670,7 @@ typeCheckVarDecl _ _ vd = fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd  -typeCheckMethodDecl :: CodeState -> TypeCheck (TcDeclM r) MemberDecl+typeCheckMethodDecl :: CodeState -> TypeCheck TcDeclM MemberDecl typeCheckMethodDecl st (MethodDecl _ _ms tps _rt i ps _exs mb) = do   -- Lookup the correct function signature   debugPrint $ "Type-checking method " ++ prettyPrint i@@ -746,7 +725,7 @@                             "Applied to non-method decl " ++ show md  -typeCheckConstrDecl :: CodeState -> TypeCheck (TcDeclM r) MemberDecl+typeCheckConstrDecl :: CodeState -> TypeCheck TcDeclM MemberDecl typeCheckConstrDecl st (ConstructorDecl _ _ms tps ci ps _exs cb) = do   withErrCtxt ("When checking body of constructor " ++ prettyPrint ci ++ ":\n") $ do   --debug $ "Type-checking constructor:\n " ++ prettyPrint cd@@ -805,13 +784,13 @@ typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $                             "Applied to non-constructor decl " ++ show md -aliasIfActor :: (Ident (), TcType) -> TcDeclM r [(Ident (), ActorId)]+aliasIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)] aliasIfActor (i, ty)     | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]     | otherwise = return []                  -checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM r ()+checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM () checkExnMods st (xTy, lms) = do   let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st)   maybeM mExnSt $ \sX -> do@@ -820,11 +799,11 @@               ++ show lms  -tcMethodBody :: TypeCheck (TcCodeM r) MethodBody+tcMethodBody :: TypeCheck (TcCodeM) MethodBody tcMethodBody (MethodBody _ mBlock) =      MethodBody Nothing <$> maybe (return Nothing) ((Just <$>) . tcBlock) mBlock -tcConstrBody :: TypeCheck (TcCodeM r) ConstructorBody+tcConstrBody :: TypeCheck (TcCodeM) ConstructorBody tcConstrBody (ConstructorBody _ mEci stmts) = do   mEci' <- maybe (return Nothing) ((Just <$>) . tcEci) mEci   stmts' <- tcBlockStmts stmts
src/Language/Java/Paragon/TypeCheck/Constraints.hs view
@@ -16,8 +16,8 @@ constraintsModule :: String constraintsModule = typeCheckerBase ++ ".Constraints" -data Constraint = LRT (PrgPolicy TcAtom) [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)-  deriving Show+data Constraint = LRT [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)+  deriving (Show, Eq)  type ConstraintWMsg = (Constraint, String) 
src/Language/Java/Paragon/TypeCheck/Containment.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE PatternGuards #-}
 module Language.Java.Paragon.TypeCheck.Containment (lrt) where
 
 import Language.Java.Paragon.Syntax
@@ -9,40 +10,64 @@ import Language.Java.Paragon.TypeCheck.Locks
 
 import Language.Java.Paragon.Pretty
+import Language.Java.Paragon.Interaction
 
 import Debug.Trace
 
 import Data.List
 import Data.Maybe
 
-lrt :: PrgPolicy TcAtom -> 
+containmentModule :: String
+containmentModule = typeCheckerBase ++ ".Containment"
+
+lrt :: [TcClause TcAtom] -> 
        [TcLock] -> 
        TcPolicy TcActor -> 
        TcPolicy TcActor -> 
        Either Bool Constraint
-lrt TcThis _ _ _ = error "Error: TcThis instead of concrete global policy in lrt check."
-lrt (TcRigidVar _) _ _ _ = error "Error: Rigid var instead of concrete global policy in lrt check."
-lrt (TcJoin _ _) _ _ _ = error "Error: TcJoin instead of concrete global policy in lrt check."
-lrt (TcMeet _ _) _ _ _ = error "Error: TcJoin instead of concrete global policy in lrt check."
-lrt (TcPolicy g) ls (RealPolicy (TcPolicy p)) (RealPolicy (TcPolicy q)) = 
-    Left (lrtC g ls p q)
-lrt g ls (RealPolicy (TcRigidVar _)) q = lrt g ls top q
-lrt g ls p (RealPolicy (TcRigidVar _)) = lrt g ls p bottom
-lrt _ _ (RealPolicy _) (RealPolicy _) = 
-    error "Error: Non-computed policy provided to lrt"
-lrt g ls p@(RealPolicy _) q@(VarPolicy _) = Right (LRT g ls p q)
-lrt g ls p@(VarPolicy _) q@(RealPolicy _) = Right (LRT g ls p q)
-lrt g ls p@(VarPolicy _) q@(VarPolicy _) = Right (LRT g ls p q)
-lrt g ls p@(Join p1 p2) q = let
-    ap1 = lrt g ls p1 q
-    ap2 = lrt g ls p2 q
-    in either (\x -> if x then ap2 else Left False)
-              (\c -> either (\x -> if x then Right c else Left False)
-                            (\_ -> Right (LRT g ls p q) )
-                            ap2
-              )
-              ap1
-lrt _ _ _ (Join _ _) = error "Error: Join occurring on right-hand side of lrt check!"
+lrt g ls p q =
+    case (p, q) of
+      (_, Join _ _) -> panic (containmentModule ++ ".lrt")
+                       $ "Join occuring on the right-hand side of an lrt check: " ++ show q
+      (RealPolicy rp, RealPolicy rq) -> Left $ lrtReal g ls rp rq
+      (Join p1 p2, _) -> let
+                    ap1 = lrt g ls p1 q
+                    ap2 = lrt g ls p2 q
+                    in case (ap1, ap2) of
+                         _ | Left False `elem` [ap1, ap2] -> Left False
+                         (Left True, _) -> ap2
+                         (_, Left True) -> ap1 
+                         _ -> Right (LRT g ls p q)
+
+      (VarPolicy _, _) -> Right (LRT g ls p q)
+      (_, VarPolicy _) -> Right (LRT g ls p q)
+
+
+lrtReal :: [TcClause TcAtom] 
+        -> [TcLock]
+        -> PrgPolicy TcActor 
+        -> PrgPolicy TcActor 
+        -> Bool
+--lrtReal _ _ p q | any includesThis [p,q] =
+--                    panic (containmentModule ++ ".lrtReal")
+--                              $ "THIS in containment check: " ++ show (p,q)
+lrtReal g ls (TcPolicy p) (TcPolicy q) =  lrtC g ls p q
+lrtReal g ls (TcJoin p1 p2) q = lrtReal g ls p1 q && lrtReal g ls p2 q
+lrtReal g ls p (TcMeet q1 q2) = lrtReal g ls p q1 && lrtReal g ls p q2
+lrtReal g ls p q
+        | Just i <- firstRigid (TcJoin p q) = 
+                    let subi pol x = substPolicy [(i, x)] pol
+                        [[pb,pt],[qb,qt]] = map (\y -> map (subi y) [bottom, top]) [p,q]
+                    in lrtReal g ls pb qb && lrtReal g ls pt qt
+        | any includesThis [p,q] =
+                    let [[pb,pt],[qb,qt]] = map (\y -> map (flip substThis y) [bottom, top]) [p,q]
+                    in lrtReal g ls pb qb && lrtReal g ls pt qt
+lrtReal _ _ p q = 
+    panic (containmentModule ++ ".lrtReal") 
+    $ "Error: Non-computed policy provided to lrt: " ++ show (p, q)
+
+
+
 
 -- If either p or q at least contain a policy variable, 
 -- we know we'll send back a constraint
src/Language/Java/Paragon/TypeCheck/Evaluate.hs view
@@ -55,7 +55,7 @@   let def = foldl join bottom ppols   return $ mpol `orUse` def -}-evaluate :: Policy () -> TcDeclM r (TcPolicy TcActor)+evaluate :: Policy () -> TcDeclM (TcPolicy TcActor) evaluate = evalPolicy {-evaluate (PolicyExp _ pe) = evalPolicyExp pe evaluate (ExpName _ n) = -- getPolicy n@@ -74,7 +74,7 @@ evaluate (MethodInv _ mi) = evalTypeMethod mi evaluate e = fail $ "Unsupported type-level expression: " ++ prettyPrint e -}-evalTypeMethod :: MethodInvocation () -> TcDeclM r (TcPolicy TcActor)+evalTypeMethod :: MethodInvocation () -> TcDeclM (TcPolicy TcActor) evalTypeMethod = panic (evaluateModule ++ ".evalTypeMethod") ("undefined!")  orUse :: Maybe a -> a -> a
src/Language/Java/Paragon/TypeCheck/Monad.hs view
@@ -98,10 +98,10 @@ import Data.IORef import Data.List (union, intersperse) ---debug :: String -> TcDeclM r ()+--debug :: String -> TcDeclM () --debug str = liftIO $ finePrint $ "DEBUG: " ++ str ---debugTc :: String -> TcCodeM r ()+--debugTc :: String -> TcCodeM () --debugTc = liftTcDeclM . debug  monadModule :: String@@ -113,12 +113,12 @@  -- this ---getThisType :: TcCodeM r TcType+--getThisType :: TcCodeM TcType --getThisType = liftCont getThisT  -- returns -getReturn :: TcCodeM r (TcType, ActorPolicy)+getReturn :: TcCodeM (TcType, ActorPolicy) getReturn = do   mRet <- returnI <$> getEnv   case mRet of@@ -135,21 +135,21 @@ --fieldEnvToVars = withEnv $ \env -> env { vars = fields (typemap env) }  -extendVarEnvList :: [(Ident (), VarFieldSig)] -> TcCodeM r a -> TcCodeM r a+extendVarEnvList :: [(Ident (), VarFieldSig)] -> TcCodeM a -> TcCodeM a extendVarEnvList vs = withEnv $ \env ->   let oldVmap = vars env       newVmap = foldl (\m (i,vti) -> Map.insert i vti m) oldVmap vs   in env { vars = newVmap } -extendVarEnv :: Ident () -> VarFieldSig -> TcCodeM r a -> TcCodeM r a+extendVarEnv :: Ident () -> VarFieldSig -> TcCodeM a -> TcCodeM a --extendVarEnv i = extendVarEnvN i---extendVarEnvN :: Ident -> VarFieldSig -> TcCodeM r a -> TcCodeM r a+--extendVarEnvN :: Ident -> VarFieldSig -> TcCodeM a -> TcCodeM a extendVarEnv i vti = withEnv $ \env ->   let oldVmap = vars env       newVmap = Map.insert i vti oldVmap   in env { vars = newVmap } -lookupActorName :: ActorName () -> TcCodeM r (TcType, ActorPolicy)+lookupActorName :: ActorName () -> TcCodeM (TcType, ActorPolicy) lookupActorName (ActorName _ nam@(Name _ nt mPre i))     | nt == EName =          do (ty, pol, _) <- lookupVar mPre i@@ -166,7 +166,7 @@ -- | Lookup the prefix part of a name, which has to be dereferenceable. --   Returns the relevant type (Nothing if package), its typemap  --   and the accumulated policy of the name access path.-lookupPrefixName :: Name () -> TcCodeM r (Maybe TcType, TypeMap, ActorPolicy)+lookupPrefixName :: Name () -> TcCodeM (Maybe TcType, TypeMap, ActorPolicy) lookupPrefixName n@(Name _ EName Nothing i) = do     -- Special case: This *could* be a var, since those can only     -- appear first in the name, i.e. prefix == Nothing@@ -228,7 +228,7 @@  -- | Lookup the type and policy of a field or variable access path. --   Precondition: Name is the decomposition of an EName-lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM r (TcType, ActorPolicy, Bool)+lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM (TcType, ActorPolicy, Bool) lookupVar Nothing i = do   -- Could be a single variable   varMap <- vars <$> getEnv@@ -239,7 +239,7 @@     Nothing -> do       tm <- getTypeMap       case Map.lookup i $ fields tm of-        Just (VSig ty p _ _ _) -> return (ty, p, False)+        Just (VSig ty p param _ _) -> return (ty, p, param)         Nothing -> panic (monadModule ++ ".lookupVar")                     $ "Not a var or field: " ++ show i @@ -261,20 +261,20 @@     :: [TypeArgument ()]     -> [TcType]     -> [Sig]  -- Works for both methods and constrs-    -> TcCodeM r [Sig]+    -> TcCodeM [Sig] findBestMethod tArgs argTys candidates =   findBestFit =<< filterM isApplicable candidates -  where isApplicable :: Sig -> TcCodeM r Bool+  where isApplicable :: Sig -> TcCodeM Bool         isApplicable (tps, pTys, isVA) =              (&&) <$> checkArgs tps tArgs <*> checkTys isVA pTys argTys -        checkArgs :: [TypeParam ()] -> [TypeArgument ()] -> TcCodeM r Bool+        checkArgs :: [TypeParam ()] -> [TypeArgument ()] -> TcCodeM Bool         checkArgs [] [] = return True         checkArgs (tp:tps) (ta:tas) = (&&) <$> checkArg tp ta <*> checkArgs tps tas         checkArgs _ _ = return False -        checkArg :: TypeParam () -> TypeArgument () -> TcCodeM r Bool+        checkArg :: TypeParam () -> TypeArgument () -> TcCodeM Bool         checkArg _ _ = return True -- TODO: Type arguments not yet handled correctly          checkTys _ [] [] = return True@@ -287,11 +287,11 @@         checkTys b (p:ps) (a:as) = (&&) <$> (p =<: a) <*> checkTys b ps as         checkTys _ _ _ = return False -        findBestFit :: [Sig] -> TcCodeM r [Sig]+        findBestFit :: [Sig] -> TcCodeM [Sig]         findBestFit [] = return []         findBestFit (x:xs) = go [x] xs -        go :: [Sig] -> [Sig] -> TcCodeM r [Sig]+        go :: [Sig] -> [Sig] -> TcCodeM [Sig]         go xs [] = return xs         go xs (y:ys) = do           bs0 <- mapM (\x -> y `moreSpecificThan` x) xs@@ -299,7 +299,7 @@            else do bs1 <- mapM (\x -> x `moreSpecificThan` y) xs                    if and bs1 then go xs ys else go (y:xs) ys -        moreSpecificThan :: Sig -> Sig -> TcCodeM r Bool+        moreSpecificThan :: Sig -> Sig -> TcCodeM Bool         moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (=<:) ps2 ps1         moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do           let n = length ps1@@ -312,7 +312,7 @@              -> Ident ()           -- Method name              -> [TypeArgument ()]  -- Type arguments              -> [TcType]           -- Argument types-             -> TcCodeM r (ActorPolicy, [TypeParam ()], MethodSig)+             -> TcCodeM (ActorPolicy, [TypeParam ()], MethodSig) lookupMethod mPre i tArgs argTys = do   baseTm <- getTypeMap   (mPreTy, preTm, prePol) <- case mPre of@@ -363,7 +363,7 @@ --   so the policy of the access path is irrelevant. lookupLock :: Maybe (Name ()) -- Access path            -> Ident ()        -- Name of lock-           -> TcCodeM r LockSig+           -> TcCodeM LockSig lookupLock mPre i = do   baseTm <- getTypeMap   preTm <- case mPre of@@ -373,11 +373,9 @@                        return preTm   case Map.lookup i $ locks preTm of     Just lsig -> return lsig-    Nothing -> panic (monadModule ++ ".lookupLock")-               $ "Not a lock: " ++ show (Name () LName mPre i)-+    Nothing -> fail $ "Lock " ++ prettyPrint (Name () LName mPre i) ++ " not in scope" -getPolicy :: Name () -> TcCodeM r ActorPolicy+getPolicy :: Name () -> TcCodeM ActorPolicy getPolicy n = do   tm <- getTypeMap   case lookupNamed policies n tm of@@ -385,7 +383,7 @@     Just p -> return p  -lookupFieldT :: TcType -> Ident () -> TcCodeM r VarFieldSig+lookupFieldT :: TcType -> Ident () -> TcCodeM VarFieldSig lookupFieldT typ i = do   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ   aSig <- lookupTypeOfType typ@@ -398,7 +396,7 @@               -> Ident ()                -> [TypeArgument ()]                -> [TcType] -              -> TcCodeM r ([TypeParam ()], MethodSig)+              -> TcCodeM ([TypeParam ()], MethodSig) lookupMethodT typ i tArgs argTys = do   check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ   aSig <- lookupTypeOfType typ@@ -431,7 +429,7 @@ lookupConstr :: TcClassType               -> [TypeArgument ()]              -> [TcType] -             -> TcCodeM r ([TypeParam ()], ConstrSig)+             -> TcCodeM ([TypeParam ()], ConstrSig) lookupConstr ctyp tArgs argTys = do   debugPrint $ "\n\n######## Looking up constructor! ######## \n"   let typ = clsTypeToType ctyp@@ -460,7 +458,7 @@               Just csig -> return (tps, csig)                   ---lookupLock :: Name () -> TcCodeM r LockSig+--lookupLock :: Name () -> TcCodeM LockSig --lookupLock n = do --  tm <- getTypeMap --  -- debugTcCodeM $ show tm@@ -468,17 +466,17 @@ --    Nothing -> fail $ "Unknown lock: " ++ prettyPrint n --    Just lsig -> return lsig -lookupExn :: TcType -> TcCodeM r (ActorPolicy, ActorPolicy)+lookupExn :: TcType -> TcCodeM (ActorPolicy, ActorPolicy) lookupExn tyX = do   exnMap <- exnsE <$> getEnv   case Map.lookup tyX exnMap of     Just ps -> return ps     Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX -registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM r a -> TcCodeM r a+registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM a -> TcCodeM a registerExn tyX rX wX = registerExns [(tyX, (rX,wX))] -registerExns :: [(TcType, (ActorPolicy, ActorPolicy))] -> TcCodeM r a -> TcCodeM r a+registerExns :: [(TcType, (ActorPolicy, ActorPolicy))] -> TcCodeM a -> TcCodeM a registerExns tysPols =     withEnv $ \env ->          let oldMap = exnsE env@@ -486,44 +484,44 @@         in env { exnsE = newMap }  -extendLockEnv :: [TcLock] -> TcCodeM r a -> TcCodeM r a+extendLockEnv :: [TcLock] -> TcCodeM a -> TcCodeM a extendLockEnv locs = withEnv $ \env ->                          env { lockstate = lockstate env `union` locs } -getBranchPC :: Entity -> TcCodeM r [(ActorPolicy, String)]+getBranchPC :: Entity -> TcCodeM [(ActorPolicy, String)] getBranchPC e = do env <- getEnv                    -- debugTcCodeM $ "Env: " ++ show env                    return $ branchPC (Just e) env -getBranchPC_ :: TcCodeM r [(ActorPolicy, String)]+getBranchPC_ :: TcCodeM [(ActorPolicy, String)] getBranchPC_ = do env <- getEnv                   return $ branchPC Nothing env -extendBranchPC :: ActorPolicy -> String -> TcCodeM r a -> TcCodeM r a+extendBranchPC :: ActorPolicy -> String -> TcCodeM a -> TcCodeM a extendBranchPC p str = withEnv $ joinBranchPC p str -addBranchPCList :: [Ident ()] -> TcCodeM r a -> TcCodeM r a+addBranchPCList :: [Ident ()] -> TcCodeM a -> TcCodeM a addBranchPCList is =     withEnv $ \env ->         let (bm, def) = branchPCE env             newBm = foldl (\m i -> Map.insert (VarEntity (mkSimpleName EName i)) [] m) bm is         in env { branchPCE = (newBm, def) } -addBranchPC :: Entity -> TcCodeM r a -> TcCodeM r a+addBranchPC :: Entity -> TcCodeM a -> TcCodeM a addBranchPC ent =      withEnv $ \env ->          let (bm, def) = branchPCE env             newBm = Map.insert ent [] bm         in env { branchPCE = (newBm, def) } -getCurrentPC :: Entity -> TcCodeM r ActorPolicy+getCurrentPC :: Entity -> TcCodeM ActorPolicy getCurrentPC ent = do   bpcs <- fst . unzip <$> getBranchPC ent   epcs <- fst . unzip <$> getExnPC   return $ foldl join bottom (bpcs ++ epcs)  {-- Tying the knot for member policies-setFieldPol :: Ident -> TcPolicy -> TcCodeM r ()+setFieldPol :: Ident -> TcPolicy -> TcCodeM () setFieldPol i pF = do   fMap <- (fields . typemap) <$> getEnv   case Map.lookup (Name [i]) fMap of@@ -537,7 +535,7 @@             Just _  -> fail "panic: field policy already written when tying the knot"         _ -> fail "panic: field policy already set when tying the knot"       -setMethodPols :: Ident -> TcPolicy -> TcPolicy -> TcCodeM r ()+setMethodPols :: Ident -> TcPolicy -> TcPolicy -> TcCodeM () setMethodPols i retM  -} @@ -546,40 +544,40 @@ -------------------------------------------- {- -- Leave actor mappings from fields-startState :: TcCodeM r ()+startState :: TcCodeM () startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty } -}  -- Actor Analysis -getActorId :: Name () -> TcCodeM r ActorId+getActorId :: Name () -> TcCodeM ActorId getActorId n = do   actorMap <- actorSt <$> getState   case Map.lookup n actorMap of     Nothing -> liftTcDeclM $ aliasActorId     Just ai -> return $ aID ai -setActorId :: Name () -> ActorId -> TcCodeM r ()+setActorId :: Name () -> ActorId -> TcCodeM () setActorId n aid = updateState setAct   where setAct :: CodeState -> CodeState         setAct s@(CodeState { actorSt = actMap }) = s { actorSt = Map.adjust replId n actMap }         replId (AI _ st) = AI aid st  -newActorIdWith :: Ident () -> ActorId -> TcCodeM r ()+newActorIdWith :: Ident () -> ActorId -> TcCodeM () newActorIdWith i aid = do   updateState insertAct       where insertAct :: CodeState -> CodeState             insertAct s@(CodeState { actorSt = actMap }) =                  s { actorSt = Map.insert (mkSimpleName EName i) (AI aid Stable) actMap } -newActorId :: Ident () -> TcCodeM r ActorId+newActorId :: Ident () -> TcCodeM ActorId newActorId i = do    aid <- liftTcDeclM $ freshActorId (prettyPrint i)   newActorIdWith i aid   return aid -newAliasId :: Ident () -> TcCodeM r ActorId+newAliasId :: Ident () -> TcCodeM ActorId newAliasId i = do   aid <- liftTcDeclM aliasActorId   newActorIdWith i aid@@ -587,7 +585,7 @@   -scrambleActors :: Maybe TcType -> TcCodeM r ()+scrambleActors :: Maybe TcType -> TcCodeM () scrambleActors mtc = do   let stb = maybe FullV (FieldV . Just . typeName_) mtc   state <- getState@@ -597,10 +595,10 @@  -- Exception tracking -getExnPC :: TcCodeM r [(ActorPolicy, String)]+getExnPC :: TcCodeM [(ActorPolicy, String)] getExnPC = exnPC <$> getState -throwExn :: ExnType -> ActorPolicy -> TcCodeM r ()+throwExn :: ExnType -> ActorPolicy -> TcCodeM () throwExn et pX = do   uref <- getUniqRef   state <- getState@@ -609,7 +607,7 @@   mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap   setState $ state { exnS = mergedXmap }   -deactivateExn :: ExnType -> TcCodeM r ()+deactivateExn :: ExnType -> TcCodeM () deactivateExn et =      updateState $ \s ->          let oldEmap = exnS s@@ -617,7 +615,7 @@         in s { exnS = newEmap }    -activateExns :: [(ExnType, ExnSig)] -> TcCodeM r ()+activateExns :: [(ExnType, ExnSig)] -> TcCodeM () activateExns exns = do   uref <- getUniqRef   state <- getState@@ -631,44 +629,44 @@   mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap   setState $ state { exnS = mergedXmap } -getExnState :: ExnType -> TcCodeM r (Maybe CodeState)+getExnState :: ExnType -> TcCodeM (Maybe CodeState) getExnState et = do   eMap <- exnS <$> getState   return $ epState <$> Map.lookup et eMap -mergeActiveExnStates :: TcCodeM r ()+mergeActiveExnStates :: TcCodeM () mergeActiveExnStates = do   exnMap <- exnS <$> getState   mapM_ (mergeWithState . epState) $ Map.elems exnMap -useExnState :: CodeState -> TcCodeM r ()+useExnState :: CodeState -> TcCodeM () useExnState es = updateState (\s -> s { exnS = exnS es })  -- Lockstate tracking -getCurrentLockState :: TcCodeM r [TcLock]+getCurrentLockState :: TcCodeM [TcLock] getCurrentLockState = do   base <- lockstate <$> getEnv   mods <- lockMods <$> getState   return $ snd $ ([], base) ||>> mods -applyLockMods :: LockMods -> TcCodeM r ()+applyLockMods :: LockMods -> TcCodeM () applyLockMods lms = do   updateState $ \s -> s { lockMods = lockMods s ||>> lms } -openLock, closeLock :: TcLock -> TcCodeM r ()+openLock, closeLock :: TcLock -> TcCodeM () openLock  l = applyLockMods ([],[l]) closeLock l = applyLockMods ([l],[])  -- Policy inference -newMetaPolVar :: TcCodeM r ActorPolicy+newMetaPolVar :: TcCodeM ActorPolicy newMetaPolVar = do   uniq <- liftIO . getUniq =<< getUniqRef   ref  <- liftIO (newIORef Nothing)   return $ VarPolicy (TcMetaVar uniq ref) ---newRigidPolVar :: TcCodeM r TcPolicy+--newRigidPolVar :: TcCodeM TcPolicy --newRigidPolVar = do --  uniq <- lift . getUniq =<< getUniqRef --  return $ TcRigidVar uniq@@ -677,26 +675,22 @@ --       Working with constraints         -- -------------------------------------------- -constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM r ()+constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM () constraint ls p q str = do -- addConstraint $ LRT ls p1 p2   g <- getGlobalLockProps   case lrt g ls p q of     Left b -> do --      debugTc $ "constraint: p1: " ++ show p1 --      debugTc $ "constraint: p2: " ++ show p2-      check b str {--                $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2)-                 "\n* p = " ++ prettyPrint p1 ++-                 "\n* q = " ++ prettyPrint p2 ++-                 "\nin the presence of lock state {" ++-                   concat (intersperse ", " (map prettyPrint ls)) ++ "}" -}+      -- st <- getState+      check b (str {-++ "\n\nState: " ++ show st -})     Right c -> addConstraint c str -getGlobalLockProps :: TcCodeM r (PrgPolicy TcAtom)+getGlobalLockProps :: TcCodeM [TcClause TcAtom] getGlobalLockProps = do   cs <- go <$> getTypeMap   debugPrint $ "Fetching global lock props: " ++ show cs-  return $ TcPolicy cs+  return cs       where go :: TypeMap -> [TcClause TcAtom]             go tm = let lps = map lProps $ Map.elems $ locks tm                         tlps = map (go . tMembers . snd) $ Map.elems $ types tm@@ -706,21 +700,21 @@ locksToRec :: [TcLock] -> (PrgPolicy TcAtom) locksToRec ls = TcPolicy (map (\x -> TcClause x []) (map lockToAtom ls)) -constraintLS :: ActorPolicy -> ActorPolicy -> String -> TcCodeM r ()+constraintLS :: ActorPolicy -> ActorPolicy -> String -> TcCodeM () constraintLS p1 p2 str = do   l <- getCurrentLockState   withErrCtxt ("In the context of lock state: " ++ prettyPrint l ++ "\n") $     constraint l p1 p2 str -constraintPC :: [(ActorPolicy, String)] -> ActorPolicy -> (ActorPolicy -> String -> String) -> TcCodeM r ()+constraintPC :: [(ActorPolicy, String)] -> ActorPolicy -> (ActorPolicy -> String -> String) -> TcCodeM () constraintPC bpcs pW msgf = mapM_ (uncurry constraintPC_) bpcs-    where constraintPC_ :: ActorPolicy -> String -> TcCodeM r ()+    where constraintPC_ :: ActorPolicy -> String -> TcCodeM ()           -- Don't take lock state into account           constraintPC_ pPC src = constraint [] pPC pW (msgf pPC src)     -exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM r ()+exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM () exnConsistent caller exnTy (ExnSig rX wX _) = do     exnMap <- exnsE <$> getEnv     --debugTc $ "Using exnMap: " ++ show exnMap@@ -754,7 +748,7 @@ -- We don't give crap about backwards compatibility here, and even if we -- did, we would have to rule it out because it would be unsound. -isAssignableTo, (=<:) :: (Monad (m r), MonadTcDeclM m) => TcType -> TcType -> m r Bool+isAssignableTo, (=<:) :: MonadTcDeclM m => TcType -> TcType -> m Bool isAssignableTo t1 t2 = liftTcDeclM $      if t1 == t2 -- identity conversion      then return True@@ -762,10 +756,10 @@  (=<:) = flip isAssignableTo -isCastableTo, (<<:) :: (Monad (m r), MonadTcDeclM m) +isCastableTo, (<<:) :: MonadTcDeclM m                     => TcType                          -> TcType -                        -> m r (Bool, Bool) -- (Can be cast, needs reference narrowing)+                        -> m (Bool, Bool) -- (Can be cast, needs reference narrowing) isCastableTo t1 t2 = liftTcDeclM $ do   -- 'isAssignableTo' handles the cases of identity, primitive widening,   -- boxing + reference widening and unboxing + primitive widening.@@ -801,7 +795,7 @@ -- 2) rt/rt -> widening reference conversion -- 3) pt/rt -> boxing conversion + widening reference conversion -- 4) rt/pt -> unboxing conversion + widening primitive conversion-widensTo :: TcType -> TcType -> TcDeclM r Bool+widensTo :: TcType -> TcType -> TcDeclM Bool widensTo (TcPrimT pt1) (TcPrimT pt2) = return $ pt2 `elem` widenConvert pt1 widensTo (TcRefT   rt1) (TcRefT   rt2) = rt1 `subTypeOf` rt2 widensTo (TcPrimT pt1) t2@(TcRefT _) = @@ -818,10 +812,10 @@                | isActorType  t1 && t2 == actorT   = return True widensTo _ _ = return False -subTypeOf :: TcRefType -> TcRefType -> TcDeclM r Bool+subTypeOf :: TcRefType -> TcRefType -> TcDeclM Bool subTypeOf TcNullT _ = return True subTypeOf rt1 rt2 = (rt2 `elem`) <$> ([TcClsRefT objectT] ++) <$> superTypes rt1-  where superTypes :: TcRefType -> TcDeclM r [TcRefType]+  where superTypes :: TcRefType -> TcDeclM [TcRefType]         superTypes rt = do           tm <- getTypeMap           tsig <- case lookupTypeOfRefT rt tm of@@ -874,7 +868,7 @@   {--solve :: [ConstraintWMsg] -> TcDeclM r ()+solve :: [ConstraintWMsg] -> TcDeclM () solve cs =     liftIO $ do       wcs <- return [(p, q) | (LRT _ p q, _) <- cs]
src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs view
@@ -9,7 +9,6 @@      getEnv, withEnv,                                  -- Reader      getState, setState, updateState, mergeWithState,  -- State      addConstraint,                                    -- Writer-     tryCatch,                                         -- Error  --     withTypeMapAlwaysC,  @@ -41,7 +40,7 @@ ------------------------------------------------- -- All the cool methods of this monad -setupStartState :: TcDeclM r CodeState+setupStartState :: TcDeclM CodeState setupStartState = do   tm <- getTypeMap   let aMap = gatherActorInfo tm@@ -86,19 +85,15 @@  -- Running in parallel infix 1 |||-(|||) :: TcCodeM r a -> TcCodeM r b -> TcCodeM r (a,b)+(|||) :: TcCodeM a -> TcCodeM b -> TcCodeM (a,b) (TcCodeM f1) ||| (TcCodeM f2) = -    TcCodeM $ \ec te ts -> do-      esa <- f1 ec te ts-      esb <- f2 ec te ts-      case (esa, esb) of-        (Right (a, ts1, cs1), Right (b, ts2, cs2)) -> do-                          ts' <- mergeStatesDecl ts1 ts2-                          return $ Right ((a,b), ts', cs1 ++ cs2)-        (Left err, _) -> return $ Left err-        (_, Left err) -> return $ Left err+    TcCodeM $ \te ts -> do+      (a, ts1, cs1) <- f1 te ts+      (b, ts2, cs2) <- f2 te ts+      ts' <- mergeStatesDecl ts1 ts2+      return ((a,b), ts', cs1 ++ cs2) -mergeStatesDecl :: CodeState -> CodeState -> TcDeclM r CodeState+mergeStatesDecl :: CodeState -> CodeState -> TcDeclM CodeState mergeStatesDecl s1 s2 = do   u <- getUniqRef   liftIO $ mergeStates u s1 s2@@ -111,92 +106,77 @@ -------------------------------------------------- -- The monad used for typechecking code snippets -newtype TcCodeM r a = -    TcCodeM (ErrCtxt -> CodeEnv -> CodeState -> TcDeclM r (Either String (a, CodeState, [ConstraintWMsg])))+newtype TcCodeM a = +    TcCodeM (CodeEnv -> CodeState -> TcDeclM (a, CodeState, [ConstraintWMsg])) -runTcCodeM :: CodeEnv -> CodeState -> TcCodeM r a -> TcDeclM r (a, [ConstraintWMsg])+runTcCodeM :: CodeEnv -> CodeState -> TcCodeM a -> TcDeclM (a, [ConstraintWMsg]) runTcCodeM env state (TcCodeM f) = do-  esa <- f id env state-  case esa of-    Left err -> fail err-    Right (a,_,cs) -> return (a, cs)+  (a,_,cs) <- f env state+  return (a, cs) -instance Monad (TcCodeM r) where-  return x = TcCodeM $ \_ _ s -> return (Right (x, s, []))+instance Monad TcCodeM where+  return x = TcCodeM $ \_ s -> return (x, s, []) -  TcCodeM f >>= h = TcCodeM $ \ec e s0 -> do-                      esa <- f ec e s0-                      case esa of-                        Left err -> return $ Left err-                        Right (a, s1, cs1) -> do-                            let TcCodeM g = h a-                            esb <- g ec e s1-                            case esb of-                              Left err -> return $ Left err-                              Right (b, s2, cs2) -> return $ Right (b, s2, cs1 ++ cs2)+  TcCodeM f >>= h = TcCodeM $ \e s0 -> do+                      (a, s1, cs1) <- f e s0+                      let TcCodeM g = h a+                      (b, s2, cs2) <- g e s1+                      return (b, s2, cs1 ++ cs2) -  fail err = TcCodeM $ \ec _ _ -> return (Left $ ec err) -- TcCodeM $ \_ _ -> fail err+  fail err = TcCodeM $ \_ _ -> fail err -instance Functor (TcCodeM r) where+instance Functor TcCodeM where   fmap = liftM -instance Applicative (TcCodeM r) where+instance Applicative TcCodeM where   (<*>) = ap   pure = return -instance MonadIO (TcCodeM r) where+instance MonadIO TcCodeM where   liftIO = liftTcDeclM . liftIO -instance MonadBase (TcCodeM r) where+instance MonadBase TcCodeM where   liftBase = liftTcDeclM . liftBase-  withErrCtxt' ecf (TcCodeM f) = TcCodeM $ \ec e s -> (f (ecf ec) e s)+  withErrCtxt' ecf (TcCodeM f) = TcCodeM $ \e s -> withErrCtxt' ecf (f e s)+  tryM (TcCodeM f) = TcCodeM $ \e s -> do+                             esa <- tryM $ f e s+                             case esa of+                               Right (a, s', cs) -> return (Right a, s', cs)+                               Left err -> return (Left err, s, []) -instance MonadPR (TcCodeM r) where+instance MonadPR TcCodeM where   liftPR = liftTcDeclM . liftPR -instance MonadTcBaseM (TcCodeM r) where-  liftTcBaseM = liftTcDeclM . liftTcBaseM-  withTypeMap tmf (TcCodeM f) = TcCodeM $ \ec e s -> withTypeMap tmf (f ec e s)+--instance MonadTcBaseM TcCodeM where+--  liftTcBaseM = liftTcDeclM . liftTcBaseM+--  withTypeMap tmf (TcCodeM f) = TcCodeM $ \ec e s -> withTypeMap tmf (f ec e s)  instance MonadTcDeclM TcCodeM where-  liftTcDeclM tdm = TcCodeM $ \_ _ s -> Right . (,s,[]) <$> tdm--{--liftCallCC :: ((((a, CodeState, [ConstraintWMsg]) -> TcDeclM r (b, CodeState, [ConstraintWMsg]))-                 -> TcDeclM r (a, CodeState, [ConstraintWMsg]))-                  -> TcDeclM r (a, CodeState, [ConstraintWMsg]))-              -> ((a -> TcCodeM r b) -> TcCodeM r a) -> TcCodeM r a-liftCallCC ccc k = TcCodeM $ \e s -> ccc $ \c ->-                       let (TcCodeM f) = k (\a -> TcCodeM $ \_ _ -> c (a, s, []))-                       in f e s--withTypeMapAlwaysC :: (TypeMap -> TypeMap) -> TcCodeM r a -> TcCodeM r a-withTypeMapAlwaysC tmf tcm = liftCallCC callCC $ \cont -> do-                               withTypeMap tmf $ tcm >>= cont--}+  liftTcDeclM tdm = TcCodeM $ \_ s -> (,s,[]) <$> tdm+  withCurrentTypeMap tmf (TcCodeM f) = TcCodeM $ \e s -> withCurrentTypeMap tmf (f e s)   -- The environment -getEnv :: TcCodeM r CodeEnv-getEnv = TcCodeM (\_ e s -> return $ Right (e,s,[]))+getEnv :: TcCodeM CodeEnv+getEnv = TcCodeM (\e s -> return (e,s,[])) -withEnv :: (CodeEnv -> CodeEnv) -> TcCodeM r a -> TcCodeM r a-withEnv k (TcCodeM f) = TcCodeM $ \ec -> (f ec . k)+withEnv :: (CodeEnv -> CodeEnv) -> TcCodeM a -> TcCodeM a+withEnv k (TcCodeM f) = TcCodeM $ f . k   -- The state -getState :: TcCodeM r CodeState-getState = TcCodeM (\_ _ s -> return $ Right (s,s,[]))+getState :: TcCodeM CodeState+getState = TcCodeM (\_ s -> return (s,s,[])) -setState :: CodeState -> TcCodeM r ()-setState s = TcCodeM (\_ _ _ -> return $ Right ((),s,[]))+setState :: CodeState -> TcCodeM ()+setState s = TcCodeM (\_ _ -> return ((),s,[])) -updateState :: (CodeState -> CodeState) -> TcCodeM r ()+updateState :: (CodeState -> CodeState) -> TcCodeM () updateState f = getState >>= return . f >>= setState -mergeWithState :: CodeState -> TcCodeM r ()+mergeWithState :: CodeState -> TcCodeM () mergeWithState s = do   sOld <- getState   sNew <- liftTcDeclM $ mergeStatesDecl sOld s@@ -204,12 +184,12 @@  -- Constraints -addConstraint :: Constraint -> String -> TcCodeM r ()-addConstraint c str = TcCodeM (\_ _ s -> return $ Right ((), s, [(c,str)]))+addConstraint :: Constraint -> String -> TcCodeM ()+addConstraint c str = TcCodeM (\_ s -> return ((), s, [(c,str)]))  -- Exceptions--tryCatch :: TcCodeM r a -> (String -> TcCodeM r a) -> TcCodeM r a+{-+tryCatch :: TcCodeM a -> (String -> TcCodeM a) -> TcCodeM a tryCatch (TcCodeM f) ctch = TcCodeM $ \ec e s -> do                               esa <- f ec e s                               case esa of@@ -217,4 +197,4 @@                                 Left err -> do                                          let TcCodeM g = ctch err                                          g ec e s-+-}
src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs view
@@ -5,13 +5,14 @@       TcDeclM, runTcDeclM, TypeCheck, -     MonadTcDeclM(..), MonadTcBaseM(..),+     MonadTcDeclM(..), -- MonadTcBaseM(..), -     callCC, withTypeMapAlways,      fetchPkg, fetchType,       getTypeMap, getThisType, getSuperType, lookupTypeOfType, +     withTypeParam, extendGlobalTypeMap,+      evalSrcType, evalSrcRefType, evalSrcClsType,      evalSrcTypeArg, evalSrcNWTypeArg,      evalReturnType,@@ -52,8 +53,8 @@  type TypeCheck m ast = ast () -> m (ast T) -lookupTypeOfType :: MonadTcBaseM m => TcType -> m TypeSig-lookupTypeOfType ty = liftTcBaseM $ do+lookupTypeOfType :: MonadTcDeclM m => TcType -> m TypeSig+lookupTypeOfType ty = liftTcDeclM $ do   tm <- getTypeMap   debugPrint $ "lookupTypeOfType -- TypeMap:\n" ++ show tm   case lookupTypeOfT ty tm of@@ -62,20 +63,21 @@     Left (Just err) -> fail err  -fetchPkg :: Name () -> TcDeclM r ()+fetchPkg :: Name () -> TcDeclM () fetchPkg n = do   debugPrint $ "Fetching package " ++ prettyPrint n ++ " ..."   isP <- doesPkgExist n   if not isP    then fail $ "No such package: " ++ prettyPrint n    else do-     withTypeMapAlways (extendTypeMapP n emptyTM) $ do-               debugPrint $ "Done fetching package " ++ prettyPrint n-               return ()+     extendGlobalTypeMap (extendTypeMapP n emptyTM)+     debugPrint $ "Done fetching package " ++ prettyPrint n+     return ()                         -fetchType :: Name () -> TcDeclM r ([TypeParam ()], TypeSig)+fetchType :: Name () -> TcDeclM ([TypeParam ()], TypeSig) fetchType n@(Name _ _ _ typName) = do+  withFreshCurrentTypeMap $ do   debugPrint $ "Fetching type " ++ prettyPrint n ++ " ..."   isT <- doesTypeExist n   if not isT@@ -110,30 +112,30 @@                             tImpls   = implsTys,                             tMembers = superTm { constrs = Map.empty }                           }-               (rtps,rsig) <- withTypeMapAlways (extendTypeMapT n tps tsig) $ do-                                withFoldMap withTypeParam tps $ do-                                     let mDs = map unMemberDecl ds-                                     -- These will be written directly into the right-                                     -- places in" the TM, using the 'always' trick-                                     fetchActors n mDs-                                     fetchLocks  n mDs-                                     fetchPols   n mDs-                                     fetchTypeMethods n mDs-                                     fetchSignatures  n mDs+               extendGlobalTypeMap (extendTypeMapT n tps tsig) -                                     tm <- getTypeMap-                                     case lookupNamed types n tm of-                                       Just res -> do-                                         debugPrint $ "Done fetching type: " ++ prettyPrint n-                                         debugPrint $ "Result: " ++ show res ++ "\n"-                                         return res-                                       Nothing  -> panic (tcDeclMModule ++ ".fetchType") $-                                                   "Just fetched type " ++ show n ++ -                                                   " but now it doesn't exist!"-               withTypeMapAlways (extendTypeMapT n rtps rsig) $ do+--               (rtps,rsig) <- withTypeMapAlways (extendTypeMapT n tps tsig) $ do+               withFoldMap withTypeParam tps $ do+                 let mDs = map unMemberDecl ds+                 fetchActors n mDs $ do+                 fetchLocks  n mDs $ do+                 fetchPols   n mDs $ do+                 fetchTypeMethods n mDs $ do+                 fetchSignatures  n mDs+                  tm <- getTypeMap-                 debugPrint $ "TypeMap here: " ++ show tm ++ "\n"-                 return (rtps,rsig)+                 case lookupNamed types n tm of+                   Just res -> do+                     debugPrint $ "Done fetching type: " ++ prettyPrint n+                     debugPrint $ "Result: " ++ show res ++ "\n"+                     return res+                   Nothing  -> panic (tcDeclMModule ++ ".fetchType") $+                               "Just fetched type " ++ show n ++ +                              " but now it doesn't exist!"+--               withTypeMapAlways (extendTypeMapT n rtps rsig) $ do+--                 tm <- getTypeMap+--                 debugPrint $ "TypeMap here: " ++ show tm ++ "\n"+--                 return (rtps,rsig)                               where unMemberDecl :: Decl () -> MemberDecl ()                     unMemberDecl (MemberDecl _ md) = md@@ -159,14 +161,17 @@                             tImpls   = [],                             tMembers = superTm                           }-               withTypeMapAlways (extendTypeMapT n tps tsig) $ do-                withFoldMap withTypeParam tps $ do++               extendGlobalTypeMap (extendTypeMapT n tps tsig)++--               withTypeMapAlways (extendTypeMapT n tps tsig) $ do+               withFoldMap withTypeParam tps $ do                  -- These will be written directly into the right                  -- places in the TM, using the 'always' trick-                 fetchActors n mDs-                 fetchLocks  n mDs-                 fetchPols   n mDs-                 fetchTypeMethods n mDs+                 fetchActors n mDs $ do+                 fetchLocks  n mDs $ do+                 fetchPols   n mDs $ do+                 fetchTypeMethods n mDs $ do                  fetchSignatures  n mDs                   tm <- getTypeMap@@ -175,14 +180,15 @@                    Nothing  -> panic (tcDeclMModule ++ ".fetchType") $                                "Just fetched type " ++ show n ++                                 " but now it doesn't exist!"+        _ -> fail $ "Enums not yet supported"  fetchType n = panic (tcDeclMModule ++ ".fetchType") $ show n  -- Actors -fetchActors :: Name () -> [MemberDecl ()] -> TcDeclM r ()-fetchActors n mDecls = do+fetchActors :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a+fetchActors n mDecls tdra = do     --debug "fetchActors"     let acts = [ (ms, vd)                       | FieldDecl _ ms (PrimType _ (ActorT _)) vds <- mDecls @@ -190,22 +196,30 @@                      , Final () `elem` ms -- Static () `elem` ms                 ]     let -- (sfs,unstables)  = partition (\(ms, _) -> Final () `elem` ms) acts-        (spawns,stables) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs+        (spawns  , stables ) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs+        (sspawns , fspawns ) = partition (\(ms,_) -> Static () `elem` ms) spawns+        (sstables, fstables) = partition (\(ms,_) -> Static () `elem` ms) stables                                -    (sas, svs) <- unzip <$> mapM spawnActorVd spawns+    (ssas, ssvs) <- unzip <$> mapM spawnActorVd sspawns+    (fsas, fsvs) <- unzip <$> mapM spawnActorVd fspawns+    (seas, sevs) <- unzip <$> mapM evalActorVd  sstables+    (feas, fevs) <- unzip <$> mapM evalActorVd  fstables --    (aas, avs) <- unzip <$> mapM aliasActorVd unstables-    (eas, evs) <- unzip <$> mapM evalActorVd stables-    withTypeMapAlways (extendTypeMapN n . merge $---                         (\tm -> tm-                           emptyTM { actors = Map.fromList (sas {- ++ aas -} ++ eas),-                                     fields = Map.fromList (svs {- ++ avs -} ++ evs) }) $ do-                       debugPrint "Actors fetched"-                       return ()+--    (eas, evs) <- unzip <$> mapM evalActorVd stables+    let globTM = emptyTM { actors = Map.fromList (ssas ++ seas),+                           fields = Map.fromList (ssvs ++ fsvs ++ sevs ++ fevs) }+        loclTM = emptyTM { actors = Map.fromList (ssas ++ fsas ++ seas ++ feas),+                           fields = Map.fromList (ssvs ++ fsvs ++ sevs ++ fevs) }++    extendGlobalTypeMap (extendTypeMapN n $ merge globTM)+    withCurrentTypeMap (merge loclTM) $ do+      debugPrint "Actors fetched"+      tdra                        where spawnActorVd, evalActorVd --, aliasActorVd                    :: ([Modifier ()], VarDecl ())-                   -> TcDeclM r ((Ident (), ActorId), (Ident (),VarFieldSig))+                   -> TcDeclM ((Ident (), ActorId), (Ident (),VarFieldSig))                   -- Only Nothing for initializer                spawnActorVd (ms, VarDecl _ (VarId _ i) _) = do                  a <- freshActorId (prettyPrint i)@@ -247,8 +261,8 @@  -- locks -fetchLocks :: Name () -> [MemberDecl ()] -> TcDeclM r ()-fetchLocks n mds = do+fetchLocks :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a+fetchLocks n mds tdra = do   let lcs = [ (i, ms, mps, mProps) |                 LockDecl _ ms i mps mProps <- mds ]   lsigs <- flip mapM lcs $ \(i, ms, mps, mProps) -> do@@ -256,11 +270,13 @@                      modPrs <- getLockModProps i ms                      prs <- evalSrcLockProps i mProps                      return (i, LSig pol (length mps) (modPrs ++ prs))-  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { locks = Map.fromList lsigs })) $ do-                     debugPrint $ "Locks fetched"-                     return ()+  let newTM = emptyTM { locks = Map.fromList lsigs }+  extendGlobalTypeMap (extendTypeMapN n $ merge newTM)+  withCurrentTypeMap (merge newTM) $ do+       debugPrint $ "Locks fetched"+       tdra -getLockModProps :: Ident () -> [Modifier ()] -> TcDeclM r [TcClause TcAtom]+getLockModProps :: Ident () -> [Modifier ()] -> TcDeclM [TcClause TcAtom] getLockModProps lockI ms = do     let trans = evalSrcLockProps lockI $ Just [lockPropQQ| { #lockI('x,'y) : #lockI('x,'z), #lockI('z,'y) } |]         refl  = evalSrcLockProps lockI $ Just [lockPropQQ| { #lockI('x,'x) : } |]@@ -275,39 +291,51 @@  -- policies -fetchPols :: Name () -> [MemberDecl ()] -> TcDeclM r ()-fetchPols n mds = do-  let pols = [ (i,initz) | +fetchPols :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a+fetchPols n mds tdra = do+  let pols = [ (i,initz, Static () `elem` ms) |                   FieldDecl _ ms (PrimType _ (PolicyT _)) vds <- mds,                  VarDecl _ (VarId _ i) (Just (InitExp _ initz)) <- vds,-                 Static () `elem` ms, Final () `elem` ms+                 Final () `elem` ms              ]-  ips <- mapM fetchPol pols-  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { policies = Map.fromList ips })) $ do+      (spols, fpols) = partition (\(_,_,b) -> b) pols+      +  sips <- mapM fetchPol spols+  fips <- mapM fetchPol fpols++  -- TODO: Expand local locks!+  let globTM = emptyTM { policies = Map.fromList sips }+      loclTM = emptyTM { policies = Map.fromList $ sips ++ fips }+  extendGlobalTypeMap $ extendTypeMapN n $ merge globTM+  withCurrentTypeMap (merge loclTM) $ do+--  withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { policies = Map.fromList ips })) $ do                     debugPrint $ "Policies fetched"-                    return ()+                    tdra -      where fetchPol :: (Ident (), Exp ()) -> TcDeclM r (Ident (), ActorPolicy)-            fetchPol (i,e) = (i,) <$> evalPolicy e+      where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), ActorPolicy)+            fetchPol (i,e,_) = (i,) <$> evalPolicy e -- end policies  -- Working with typemethods-fetchTypeMethods :: Name () -> [MemberDecl ()] -> TcDeclM r ()-fetchTypeMethods n mds  = do+fetchTypeMethods :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a+fetchTypeMethods n mds tdra = do   let ipbs = [ (i,(ps,body)) |                 MethodDecl _ ms _ _ i ps _ (MethodBody _ (Just body)) <- mds,                Typemethod () `elem` ms              ]   ipidbs <- mapM paramsToIdents ipbs-  withTypeMapAlways (extendTypeMapN n -                     (merge $ emptyTM { typemethods = Map.fromList ipidbs })) $ do+  let newTM = emptyTM { typemethods = Map.fromList ipidbs }+  extendGlobalTypeMap $ extendTypeMapN n $ merge newTM+  withCurrentTypeMap (merge newTM) $ do+--  withTypeMapAlways (extendTypeMapN n +--                     (merge $ emptyTM { typemethods = Map.fromList ipidbs })) $ do                     debugPrint "TypeMethods fetched"-                    return ()+                    tdra      where paramsToIdents (i, (ps,b)) = do                               pids <- mapM paramIdent ps                               return (i, (pids,b))-          paramIdent :: FormalParam () -> TcDeclM r (Ident ())+          paramIdent :: FormalParam () -> TcDeclM (Ident ())           paramIdent (FormalParam _ _ _ _ (VarId _ i)) = return i           paramIdent (FormalParam _ _ _ _ arvid) =                fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid@@ -316,28 +344,29 @@  -- signatures of fields, methods and constructors -fetchSignatures :: Name () -> [MemberDecl ()] -> TcDeclM r ()+fetchSignatures :: Name () -> [MemberDecl ()] -> TcDeclM () fetchSignatures n memDs = do     fieldMap <- fetchFields memDs     methodMap <- fetchMethods memDs     constrMap <- fetchConstrs memDs-    withTypeMapAlways (extendTypeMapN n (merge $ emptyTM-                                                   { fields = fieldMap,-                                                     methods = methodMap,-                                                     constrs = constrMap })) $ do-      debugPrint "Signatures fetched"-      return ()-+    let newTM = emptyTM+                { fields = fieldMap,+                  methods = methodMap,+                  constrs = constrMap }+    extendGlobalTypeMap $ extendTypeMapN n $ merge newTM+    debugPrint "Signatures fetched"+    return ()+      where-   unVarDecl :: VarDecl () -> TcDeclM r (Ident ())+   unVarDecl :: VarDecl () -> TcDeclM (Ident ())    unVarDecl (VarDecl _ (VarId _ i) _) = return i    unVarDecl arvid = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -   fetchFields :: [MemberDecl ()] -> TcDeclM r (Map (Ident ()) VarFieldSig)+   fetchFields :: [MemberDecl ()] -> TcDeclM (Map (Ident ()) VarFieldSig)    fetchFields = go Map.empty        where go :: Map (Ident ()) VarFieldSig                  -> [MemberDecl ()] -                -> TcDeclM r (Map (Ident ()) VarFieldSig)+                -> TcDeclM (Map (Ident ()) VarFieldSig)              go acc [] = return acc              go fm (md:mds) =                   case md of@@ -352,11 +381,11 @@                    _ -> go fm mds     fetchMethods :: [MemberDecl ()] -                -> TcDeclM r (Map (Ident ()) MethodMap) +                -> TcDeclM (Map (Ident ()) MethodMap)     fetchMethods = go Map.empty        where go :: Map (Ident ()) MethodMap                 -> [MemberDecl ()]-                -> TcDeclM r (Map (Ident ()) MethodMap)+                -> TcDeclM (Map (Ident ()) MethodMap)              go acc [] = return acc              go mm (md:mds) =                   case md of@@ -391,7 +420,7 @@    fetchConstrs = go Map.empty        where go :: ConstrMap                 -> [MemberDecl ()]-                -> TcDeclM r ConstrMap+                -> TcDeclM ConstrMap              go acc [] = return acc              go cm (md:mds) =                   case md of@@ -419,7 +448,7 @@                    _ -> go cm mds                        -   eSpecToSig :: ExceptionSpec () -> TcDeclM r (TcType, ExnSig)+   eSpecToSig :: ExceptionSpec () -> TcDeclM (TcType, ExnSig)    eSpecToSig (ExceptionSpec _ ms eType) = do           ty <- evalSrcType (RefType () eType) -- should use evalSrcRefType           rPol <- getReadPolicy ms@@ -433,7 +462,7 @@                      }           return (ty, esig) -   paramInfo :: FormalParam () -> TcDeclM r (TcType, ActorPolicy)+   paramInfo :: FormalParam () -> TcDeclM (TcType, ActorPolicy)    paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do           pPol <- getParamPolicy i ms           pTy  <- evalSrcType ty@@ -441,31 +470,31 @@    paramInfo (FormalParam _ _ _ _ arvid) =              fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -withTypeParam :: TypeParam () -> TcDeclM r a -> TcDeclM r a+withTypeParam :: TypeParam () -> TcDeclM a -> TcDeclM a withTypeParam tp tcba =      case tp of       ActorParam _ i -> do           let vti = VSig actorT top False False True-          withTypeMap (\tm -> +          withCurrentTypeMap (\tm ->                tm { actors = Map.insert i (ActorTPVar i) (actors tm),                    fields = Map.insert i vti (fields tm) }) $ tcba       PolicyParam _ i -> do            let vti = VSig policyT top False False True-           withTypeMap (\tm ->+           withCurrentTypeMap (\tm ->               tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm),                    fields = Map.insert i vti (fields tm) }) $ tcba       LockStateParam _ i -> do           let vti = VSig (lockT []) top False False True-          withTypeMap (\tm ->+          withCurrentTypeMap (\tm ->               tm { fields = Map.insert i vti (fields tm) }) $ tcba       TypeParam _ _i _ -> do-          --withTypeMap (\tm ->+          --withCurrentTypeMap (\tm ->           --    tm { types = Map.insert i ([],Map.empty) (types tm) }) $              tcba   {--fetchSignature :: MemberDecl () -> TcDeclM r a -> TcDeclM r a+fetchSignature :: MemberDecl () -> TcDeclM a -> TcDeclM a fetchSignature memDecl tcba = do      --debug $ "fetchSignature: " ++ show memberDecl@@ -531,7 +560,7 @@       LockDecl {} -> fail "Lock properties not yet supported"       _ -> fail "Inner classes not yet supported" -  where eSpecToSig :: ExceptionSpec () -> TcDeclM r (TcType, ExnSig)+  where eSpecToSig :: ExceptionSpec () -> TcDeclM (TcType, ExnSig)         eSpecToSig (ExceptionSpec _ ms eType) = do           ty <- evalSrcType (RefType () eType) -- should use evalSrcRefType           rPol <- getReadPolicy ms@@ -545,7 +574,7 @@                      }           return (ty, esig) -        paramInfo :: FormalParam () -> TcDeclM r (TcType, TcPolicy)+        paramInfo :: FormalParam () -> TcDeclM (TcType, TcPolicy)         paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do           pPol <- getParamPolicy i ms           pTy  <- evalSrcType ty@@ -559,7 +588,7 @@ ------------------------------------------------------------  -------------------------------------------------------------------------------------      -getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM r ActorPolicy+getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM ActorPolicy getReadPolicy mods =      case [pol |Reads _ pol <- mods ] of -- !!0 -- Read Policy? what if no read policy?       [pol] -> evalPolicy pol@@ -578,14 +607,14 @@       [] -> return top       _ -> fail "At most one read modifier allowed per lock" -getParamPolicy :: Ident () -> [Modifier ()] -> TcDeclM r ActorPolicy+getParamPolicy :: Ident () -> [Modifier ()] -> TcDeclM ActorPolicy getParamPolicy i mods =     case [pol | Reads _ pol <- mods ] of        [pol] -> evalPolicy pol        [] -> return $ ofPol i        _ -> fail "At most one read modifier allowed per parameter" -getReturnPolicy :: [Modifier ()] -> [ActorPolicy] -> TcDeclM r ActorPolicy+getReturnPolicy :: [Modifier ()] -> [ActorPolicy] -> TcDeclM ActorPolicy getReturnPolicy mods pPols =      case [pol | Reads _ pol <- mods ] of       [pol] -> evalPolicy pol@@ -598,16 +627,16 @@ ------------------------------------------------------------------- -- Evaluating types -evalReturnType :: Maybe (Type ()) -> TcDeclM r TcType+evalReturnType :: Maybe (Type ()) -> TcDeclM TcType evalReturnType = maybe (return voidT) evalSrcType -evalSrcType :: Type () -> TcDeclM r TcType+evalSrcType :: Type () -> TcDeclM TcType evalSrcType (PrimType _ pt) = return $ TcPrimT pt evalSrcType (RefType  _ rt) = TcRefT <$> evalSrcRefType rt evalSrcType _ = panic (tcDeclMModule ++ ".evalSrcType")                 "AntiQType should not appear in AST being type-checked" -evalSrcRefType :: RefType () -> TcDeclM r TcRefType+evalSrcRefType :: RefType () -> TcDeclM TcRefType evalSrcRefType (TypeVariable _ i) = return $ TcTypeVar i evalSrcRefType (ArrayType _ t mps) = do   ty <- evalSrcType t@@ -616,7 +645,7 @@   return arrTy evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct -evalSrcClsType :: ClassType () -> TcDeclM r TcClassType+evalSrcClsType :: ClassType () -> TcDeclM TcClassType evalSrcClsType ct@(ClassType _ n tas) = do   debugPrint $ "Evaluating class type: " ++ show ct   baseTm <- getTypeMap@@ -634,7 +663,7 @@       where aux :: TypeMap                            -- Typemap of outer type (or top-level)                 -> [(Ident (), [TcTypeArg])]          -- Accumulated type (reversed)                 -> [(Ident (), [TypeArgument ()])]    -- Type to traverse-                -> TcDeclM r [(Ident (), [TcTypeArg])] -- Result (re-reversed)+                -> TcDeclM [(Ident (), [TcTypeArg])] -- Result (re-reversed)             aux _ accTy [] = return $ reverse accTy             aux tm accTy ((i,tas):rest) = do                  debug $ "Looking up type: " ++ show i@@ -656,11 +685,11 @@  --    TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs -}      -evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcDeclM r TcTypeArg+evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcDeclM TcTypeArg evalSrcTypeArg tp (ActualArg _ a) = evalSrcNWTypeArg tp a evalSrcTypeArg _ _ = fail "evalSrcTypeArg: Wildcards not yet supported" -evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcDeclM r TcTypeArg+evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcDeclM TcTypeArg -- Types may be names or types -- TODO: Check bounds evalSrcNWTypeArg (TypeParam {}) (ActualName _ n) = do     TcActualType . TcClsRefT <$> evalSrcClsType (ClassType () n [])@@ -684,7 +713,7 @@ evalSrcNWTypeArg (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls -} -evalPolicy :: Exp () -> TcDeclM r ActorPolicy+evalPolicy :: Exp () -> TcDeclM ActorPolicy evalPolicy e = case e of   ExpName _ n -> do     -- debug $ "evalPolicy: " ++ show n@@ -707,37 +736,37 @@   Paren _ p -> evalPolicy p   _ -> fail "evalPolicy: More here!" -evalPolicyExp :: PolicyExp () -> TcDeclM r ActorPolicy+evalPolicyExp :: PolicyExp () -> TcDeclM ActorPolicy evalPolicyExp (PolicyLit _ cs) = (RealPolicy . TcPolicy) <$> mapM evalClause cs evalPolicyExp (PolicyOf _ i)   = return $ RealPolicy $ TcRigidVar i evalPolicyExp (PolicyThis _)   = return $ RealPolicy $ TcThis evalPolicyExp (PolicyTypeVar _ i) = return $ RealPolicy $ TcRigidVar i -evalClause :: Clause () -> TcDeclM r (TcClause TcActor)+evalClause :: Clause () -> TcDeclM (TcClause TcActor) evalClause (Clause _ h b) = do   h' <- evalActor h   b' <- mapM evalAtom b   return $ TcClause h' b' -evalActorName :: ActorName () -> TcDeclM r ActorId+evalActorName :: ActorName () -> TcDeclM ActorId evalActorName (ActorName _ n) = evalActorId n evalActorName (ActorTypeVar _ i) = return $ ActorTPVar i -evalActor :: Actor () -> TcDeclM r TcActor+evalActor :: Actor () -> TcDeclM TcActor evalActor (Actor _ n) = TcActor <$> evalActorName n evalActor (Var _ i) = return $ TcVar i -evalActorId :: Name () -> TcDeclM r ActorId+evalActorId :: Name () -> TcDeclM ActorId evalActorId n = do   tm <- getTypeMap   case lookupNamed actors n tm of     Just aid -> return aid     Nothing -> aliasActorId -- fail $ "evalActor: No such actor: " ++ prettyPrint n -evalAtom :: Atom () -> TcDeclM r TcAtom+evalAtom :: Atom () -> TcDeclM TcAtom evalAtom (Atom _ n as) = TcAtom n <$> mapM evalActor as -evalLock :: Lock () -> TcDeclM r TcLock+evalLock :: Lock () -> TcDeclM TcLock evalLock (Lock _ n@(Name _ _nt mPre i) ans) = do   tm <- case mPre of           Nothing -> getTypeMap@@ -765,17 +794,17 @@ evalLock l = panic (tcDeclMModule ++ ".evalLock")              $ show l   -evalSrcLockProps :: Ident () -> Maybe (LockProperties ()) -> TcDeclM r [TcClause TcAtom]+evalSrcLockProps :: Ident () -> Maybe (LockProperties ()) -> TcDeclM [TcClause TcAtom] evalSrcLockProps _ Nothing = return [] evalSrcLockProps i (Just (LockProperties _ lcs)) = do   cs <- mapM (evalLClause i) lcs   debugPrint $ "Properties: " ++ show cs   return cs -evalLClause :: Ident () -> LClause () -> TcDeclM r (TcClause TcAtom)+evalLClause :: Ident () -> LClause () -> TcDeclM (TcClause TcAtom) evalLClause i (LClause _ h b) = TcClause <$> evalSimpleAtom i h <*> mapM evalAtom b -evalSimpleAtom :: Ident () -> Atom () -> TcDeclM r TcAtom+evalSimpleAtom :: Ident () -> Atom () -> TcDeclM TcAtom evalSimpleAtom i a@(Atom _ n _) = do   case n of     (Name _ _ Nothing aI) | aI == i -> evalAtom a@@ -783,7 +812,7 @@                 "\nExpected name: " ++ prettyPrint i ++                 "\nFound name: " ++ prettyPrint n -getActor :: ActorName () -> TcDeclM r ActorId+getActor :: ActorName () -> TcDeclM ActorId getActor (ActorName _ n) = do   tm <- getTypeMap   case lookupNamed actors n tm of@@ -791,21 +820,18 @@     Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n getActor (ActorTypeVar _ i) = return $ ActorTPVar i -freshActorId :: String -> TcDeclM r ActorId+freshActorId :: String -> TcDeclM ActorId freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef -aliasActorId :: TcDeclM r ActorId+aliasActorId :: TcDeclM ActorId aliasActorId = (liftIO . newAlias) =<< getUniqRef    ------------------------------------------------------+{----------------------------------------------------- -- The continuation monad  newtype TcDeclM r a = TcDeclM ((a -> TcBaseM r) -> TcBaseM r) -runTcDeclM :: TcClassType -> TcDeclM a a -> PiReader a-runTcDeclM ty (TcDeclM f) = runTcBaseM (f return) emptyTM ty- instance Monad (TcDeclM r) where   return x = TcDeclM $ \k -> k x @@ -872,51 +898,66 @@                              withTypeMapAlways tmf (TcDeclM f) = TcDeclM $ \k -> do                                       withTypeMap tmf $ f k-+-} ----------------------------------------------- -- Underlying non-cont'ed monad -newtype TcBaseM a = TcBaseM { runTcBaseM :: TypeMap -> TcClassType -> PiReader a }+newtype TcDeclM a = TcDeclM (TypeMap -> TypeMap -> TcClassType -> PiReader (a, TypeMap) ) -instance Monad TcBaseM where+runTcDeclM :: TcClassType -> TcDeclM a -> PiReader a+runTcDeclM ty (TcDeclM f) = fst <$> f emptyTM emptyTM ty++instance Monad TcDeclM where   return = liftPR . return -  TcBaseM f >>= k = TcBaseM $ \tm ty -> do-                       a <- f tm ty-                       let TcBaseM g = k a-                       g tm ty+  TcDeclM f >>= k = TcDeclM $ \ctm gtm ty -> do+                       (a, gtm') <- f ctm gtm ty+                       let TcDeclM g = k a+                       g ctm gtm' ty    fail = liftPR . fail -instance Functor TcBaseM where+instance Functor TcDeclM where   fmap = liftM -instance MonadIO TcBaseM where+instance Applicative TcDeclM where+  pure = return+  (<*>) = ap++instance MonadIO TcDeclM where   liftIO = liftPR . liftIO -instance MonadBase TcBaseM where+instance MonadBase TcDeclM where   liftBase = liftPR . liftBase+  withErrCtxt' prf (TcDeclM f) = TcDeclM $ \ctm gtm ty -> withErrCtxt' prf $ f ctm gtm ty+  tryM (TcDeclM f) = TcDeclM $ \ctm gtm ty -> do+                             esatm <- tryM (f ctm gtm ty)+                             case esatm of+                               Right (a, tm) -> return (Right a, tm)+                               Left err -> return (Left err, gtm) -  withErrCtxt' prf (TcBaseM f) = TcBaseM $ \tm ty -> withErrCtxt' prf $ f tm ty+instance MonadPR TcDeclM where+  liftPR pra = TcDeclM $ \_ gtm _ -> pra >>= \a -> return (a, gtm) -instance MonadPR TcBaseM where-  liftPR pra = TcBaseM $ \_ _ -> pra+class MonadPR m => MonadTcDeclM m where+  liftTcDeclM :: TcDeclM a -> m a+  withCurrentTypeMap :: (TypeMap -> TypeMap) -> m a -> m a -class MonadPR m => MonadTcBaseM m where-  liftTcBaseM :: TcBaseM a -> m a-  withTypeMap :: (TypeMap -> TypeMap) -> m a -> m a+instance MonadTcDeclM TcDeclM where+  liftTcDeclM = id+  withCurrentTypeMap = withCurrentTypeMapTB -instance MonadTcBaseM TcBaseM where-  liftTcBaseM = id-  withTypeMap = withTypeMapTB+extendGlobalTypeMap :: MonadTcDeclM m => (TypeMap -> TypeMap) -> m ()+extendGlobalTypeMap = liftTcDeclM . extendGlobalTypeMapTB+   -getTypeMap :: MonadTcBaseM m => m TypeMap-getTypeMap = liftTcBaseM getTypeMapTB+getTypeMap :: MonadTcDeclM m => m TypeMap+getTypeMap = liftTcDeclM getTypeMapTB -getThisType :: MonadTcBaseM m => m TcClassType-getThisType = liftTcBaseM getThisTypeTB+getThisType :: MonadTcDeclM m => m TcClassType+getThisType = liftTcDeclM getThisTypeTB -getSuperType :: MonadTcBaseM m => m TcClassType+getSuperType :: MonadTcDeclM m => m TcClassType getSuperType = do   thisTy <- getThisType   thisSig <- lookupTypeOfType (clsTypeToType thisTy)@@ -927,11 +968,18 @@           $ "Called on non-class with multiple super types"  -getTypeMapTB :: TcBaseM TypeMap-getTypeMapTB = TcBaseM $ \tm _ -> return tm+withFreshCurrentTypeMap :: TcDeclM a -> TcDeclM a+withFreshCurrentTypeMap = withCurrentTypeMap (const emptyTM) -getThisTypeTB :: TcBaseM TcClassType-getThisTypeTB = TcBaseM $ \_ ty -> return ty -withTypeMapTB :: (TypeMap -> TypeMap) -> TcBaseM a -> TcBaseM a-withTypeMapTB tmf (TcBaseM f) = TcBaseM $ \tm ty -> f (tmf tm) ty+getTypeMapTB :: TcDeclM TypeMap+getTypeMapTB = TcDeclM $ \ctm gtm _ -> return $ (ctm `merge` gtm, gtm)++getThisTypeTB :: TcDeclM TcClassType+getThisTypeTB = TcDeclM $ \_ gtm ty -> return (ty, gtm)++withCurrentTypeMapTB :: (TypeMap -> TypeMap) -> TcDeclM a -> TcDeclM a+withCurrentTypeMapTB tmf (TcDeclM f) = TcDeclM $ \ctm gtm ty -> f (tmf ctm) gtm ty++extendGlobalTypeMapTB :: (TypeMap -> TypeMap) -> TcDeclM ()+extendGlobalTypeMapTB tmf = TcDeclM $ \_ gtm _ -> return ((), tmf gtm)
src/Language/Java/Paragon/TypeCheck/Policy.hs view
@@ -1,11 +1,11 @@-{-# LANGUAGE CPP, DeriveDataTypeable #-}
+{-# LANGUAGE CPP, DeriveDataTypeable, PatternGuards #-}
 module Language.Java.Paragon.TypeCheck.Policy 
     (
      bottom, top, thisP, join, joinWThis, meet, {-recmeet,-} isTop, isBottom, includesThis,
      TcPolicy(..), PrgPolicy(..),{-TcPolicyRec(..),-} TcClause(..), TcAtom(..), TcActor(..), TcMetaVar(..),
      {- toPolicyLit, -} {-toRecPolicy,-}
      lockToAtom, 
-     {-zonkPolicy,-} substPolicy,
+     {-zonkPolicy,-} substPolicy, firstRigid, substThis,
      flowAtomString,
 
      ActorPolicy, AtomPolicy
@@ -19,8 +19,8 @@ import Language.Java.Paragon.TypeCheck.Locks
 
 import Data.IORef
-import Data.List ( (\\) {-, groupBy, nub-} )
-import Data.Maybe (fromJust)
+import Data.List ( (\\) {-, groupBy, nub-}  )
+import Data.Maybe 
 
 #ifdef BASE4
 import Data.Data
@@ -31,8 +31,8 @@ flowAtomString :: String
 flowAtomString = "$FLOW$"
 
-moduleString :: String
-moduleString = typeCheckerBase ++ ".Locks"
+policyModule :: String
+policyModule = typeCheckerBase ++ ".Policy"
 
 ---------------------------------------------------------------
 -- Basic policies
@@ -68,15 +68,15 @@ --  deriving (Data, Typeable)
 
 instance Data (TcMetaVar a) where
-    gunfold    = panic (moduleString ++ ": instance Data TcMetaVar (gunfold)")
+    gunfold    = panic (policyModule ++ ": instance Data TcMetaVar (gunfold)")
                  "Meta variables should never be reified"
-    toConstr   = panic (moduleString ++ ": instance Data TcMetaVar (toConstr)")
+    toConstr   = panic (policyModule ++ ": instance Data TcMetaVar (toConstr)")
                  "Meta variables should never be reified"
-    dataTypeOf = panic (moduleString ++ ": instance Data TcMetaVar (dataTypeOf)")
+    dataTypeOf = panic (policyModule ++ ": instance Data TcMetaVar (dataTypeOf)")
                  "Meta variables should never be reified"
 
 instance Typeable (TcMetaVar a) where
-    typeOf = panic (moduleString ++ ": instance Typeable TcMetaVar (typeOf)")
+    typeOf = panic (policyModule ++ ": instance Typeable TcMetaVar (typeOf)")
              "Meta variables should never be reified"
 
 instance Eq (TcMetaVar a) where
@@ -143,7 +143,7 @@   where toRecClause (TcClause act ats) = TcClause (TcAtom (mkSimpleLName (Ident () flowAtomString)) [act]) ats
 toRecPolicy (TcJoin p1 p2) = TcJoinRec (toRecPolicy p1) (toRecPolicy p2)
 toRecPolicy (TcMeet p1 p2) = TcMeetRec (toRecPolicy p1) (toRecPolicy p2)
-toRecPolicy _ = panic (moduleString ++ "toRecPolicy")
+toRecPolicy _ = panic (policyModule ++ "toRecPolicy")
                 "Cannot convert non-literal policy to a recursive one"
 -}
 
@@ -174,24 +174,43 @@ ----------------------------------}
 -- Basic policies
 
-bottom, top, thisP :: (TcPolicy TcActor)
-bottom = RealPolicy $ TcPolicy [TcClause (TcVar $ Ident () "x") []]
-top = RealPolicy $ TcPolicy []
-thisP = RealPolicy TcThis
+class IsPolicy p where
+  toPolicy :: PrgPolicy a -> p a
+  fromPolicy :: p a -> Maybe (PrgPolicy a)
+  includesThis :: p a -> Bool
 
-isTop, isBottom, includesThis :: (TcPolicy TcActor) -> Bool
-isTop = (== top)
-isBottom (RealPolicy (TcPolicy cs)) = any isBottomC cs
+instance IsPolicy PrgPolicy where
+  toPolicy = id
+  fromPolicy = Just
+  
+  includesThis TcThis = True
+  includesThis (TcJoin p q) = any includesThis [p,q]
+  includesThis (TcMeet p q) = any includesThis [p,q]
+  includesThis _ = False
+
+instance IsPolicy TcPolicy where
+  toPolicy = RealPolicy
+  fromPolicy (RealPolicy p) = Just p
+  fromPolicy _ = Nothing
+
+  includesThis (Join p q) = any includesThis [p,q]
+  includesThis (RealPolicy p) = includesThis p
+  includesThis _ = False
+
+bottom, top, thisP :: IsPolicy pol => pol TcActor
+bottom = toPolicy $ TcPolicy [TcClause (TcVar $ Ident () "x") []]
+top = toPolicy $ TcPolicy []
+thisP = toPolicy TcThis
+
+isTop, isBottom :: IsPolicy pol => pol TcActor -> Bool
+isTop pol | Just (TcPolicy []) <- fromPolicy pol = True
+isTop _ = False
+
+isBottom pol | Just (TcPolicy cs) <- fromPolicy pol = any isBottomC cs
   where isBottomC (TcClause (TcVar _) []) = True
         isBottomC _ = False
 isBottom _ = False
 
-includesThis (RealPolicy TcThis) = True
-includesThis (RealPolicy (TcJoin p q)) = any includesThis [RealPolicy p, RealPolicy q]
-includesThis (RealPolicy (TcMeet p q)) = any includesThis [RealPolicy p, RealPolicy q]
-includesThis (Join p q) = any includesThis [p, q]
-includesThis _ = False
-
 ----------------------------------
 -- meet and join
 
@@ -200,7 +219,7 @@ joinWThis p q = Join p q
 
 lubWThis :: (PrgPolicy TcActor) -> (PrgPolicy TcActor) -> (PrgPolicy TcActor)
-lubWThis TcThis p = p
+lubWThis TcThis q = q
 lubWThis p TcThis = p
 lubWThis p q = lub p q
 
@@ -268,7 +287,8 @@ 
 meet :: (TcPolicy TcActor) -> (TcPolicy TcActor) -> (TcPolicy TcActor)
 meet (RealPolicy p) (RealPolicy q) = RealPolicy $ glb p q
-meet _ _ = error "meet used on non-programmable policies"
+meet _ _ = panic (policyModule ++ ".meet") 
+           "meet used on non-programmable policies"
 
 {-TO FIX
 recmeet :: TcPolicyRec -> TcPolicyRec -> TcPolicyRec
@@ -279,8 +299,9 @@ ----------------------------------------------
 {-- Specialisation
 
-specialise :: [TcLock] -> TcPolicy -> TcPolicy
+specialise :: [TcLock] -> PrgPolicy TcActor -> PrgPolicy TcActor
 specialise ls (TcPolicy cs) = TcPolicy $ concatMap (specClause ls) cs
+specialise _ p = p
 
 specClause :: [TcLock] -> TcClause TcActor -> [TcClause TcActor]
 specClause ls (TcClause h atoms) = 
@@ -335,8 +356,8 @@               checkConsistent s = case nub s of
                                     [x] -> Just x
                                     _   -> Nothing
--}
 
+-}
 lockToAtom :: TcLock -> TcAtom
 lockToAtom (TcLock n aids) = TcAtom n $ map TcActor aids
 lockToAtom (TcLockVar i) = TcAtom (mkSimpleLName i) []
@@ -370,8 +391,9 @@ -- Policy substitution
 
 -- Invariant: policies are always closed by the env
-substPolicy :: [(Ident (), (PrgPolicy TcActor))] -> (PrgPolicy TcActor) -> (PrgPolicy TcActor)
-substPolicy env (TcRigidVar i) = fromJust $ lookup i env
+substPolicy :: [(Ident (), PrgPolicy TcActor)] -> PrgPolicy TcActor -> PrgPolicy TcActor
+substPolicy env (TcRigidVar i) 
+    | Just q <- lookup i env = q
 substPolicy env (TcJoin p1 p2) =
     let pol1 = substPolicy env p1
         pol2 = substPolicy env p2
@@ -381,6 +403,24 @@         pol2 = substPolicy env p2
     in pol1 `glb` pol2
 substPolicy _ p = p
+
+firstRigid :: PrgPolicy a -> Maybe (Ident ())
+firstRigid (TcRigidVar i) = Just i
+firstRigid (TcJoin p q) = listToMaybe $ catMaybes $ map firstRigid [p,q]
+firstRigid (TcMeet p q) = listToMaybe $ catMaybes $ map firstRigid [p,q]
+firstRigid _ = Nothing
+
+substThis :: PrgPolicy TcActor -> PrgPolicy TcActor -> PrgPolicy TcActor
+substThis p TcThis = p
+substThis p (TcJoin p1 p2) =
+    let pol1 = substThis p p1
+        pol2 = substThis p p2
+    in pol1 `lub` pol2
+substThis p (TcMeet p1 p2) =
+    let pol1 = substThis p p1
+        pol2 = substThis p p2
+    in pol1 `glb` pol2
+substThis _ p = p
 
 {-
 mkPolicySubst :: [TcPolicy] -> [TcPolicy] -> [(Ident (), TcPolicy)]
src/Language/Java/Paragon/TypeCheck/TcExp.hs view
@@ -45,7 +45,7 @@ --debugTc str = liftIO $ putStrLn $ "DEBUG: Tc: " ++ str --debugTc _ = return () -tcExp :: Exp () -> TcCodeM r (TcType, ActorPolicy, Exp T)+tcExp :: Exp () -> TcCodeM (TcType, ActorPolicy, Exp T)  -- Rule PAREN tcExp (Paren _ e) = do (ty, p, e') <- tcExp e@@ -337,7 +337,7 @@                           -> [Exp T]                          -- Accumulated annotated expressions                           -> [(Exp (), Maybe (Policy ()))]    -- Remaining dimexprs/pols                           -> ActorPolicy                      -- Policy of previous dimension-                          -> TcCodeM r ([ActorPolicy], [Exp T])+                          -> TcCodeM ([ActorPolicy], [Exp T])             checkDimExprs accP accE [] pPrev = return $ (reverse (pPrev:accP), reverse accE)             checkDimExprs accP accE ((e,mp):emps) pPrev = do               (tyE,pE,e') <- tcExp e@@ -392,7 +392,7 @@ -------------------------- -- Array initializers -tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck (TcCodeM r) ArrayInit+tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck TcCodeM ArrayInit tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do   (ps, inits') <- unzip <$> mapM (tcVarInit baseType pols) inits   mapM_ (\(p,e) -> constraintLS p pol1 $@@ -404,7 +404,7 @@   return $ ArrayInit Nothing inits' tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" -tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM r (ActorPolicy, VarInit T)+tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T) tcVarInit baseType pols (InitExp _ e) = do --  debugPrint $ "Pols: " ++ show pols --  debugPrint $ "Exp:  " ++ show e@@ -419,13 +419,13 @@   arr' <- tcArrayInit baseType pols arr   return (bottom, InitArray Nothing arr') -evalMaybePol :: Maybe (Policy ()) -> TcCodeM r ActorPolicy+evalMaybePol :: Maybe (Policy ()) -> TcCodeM ActorPolicy evalMaybePol = maybe (return bottom) (liftTcDeclM . evalPolicy)  -------------------------- -- Field Access -tcFieldAccess :: FieldAccess () -> TcCodeM r (TcType, ActorPolicy, FieldAccess T)+tcFieldAccess :: FieldAccess () -> TcCodeM (TcType, ActorPolicy, FieldAccess T) tcFieldAccess (PrimaryFieldAccess _ e fi) = do   (tyE,pE,e') <- tcExp e   case tyE of@@ -445,7 +445,7 @@ -- Instance creation  tcCreate :: TcClassType -> [TypeArgument ()] -> [Argument ()] -         -> TcCodeM r (TcType, ActorPolicy, [Argument T])+         -> TcCodeM (TcType, ActorPolicy, [Argument T]) tcCreate ctyT tas args = do   (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args   (tps,genCti) <- lookupConstr ctyT tas tysArgs@@ -507,7 +507,7 @@  -- | Check a method invocation, which could possibly represent --   a lock query expression.-tcMethodOrLockInv :: MethodInvocation () -> TcCodeM r (TcType, ActorPolicy, MethodInvocation T)+tcMethodOrLockInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T) tcMethodOrLockInv (MethodCallOrLockQuery _ (Name _ MOrLName mPre i) args) = do   -- We couldn't resolve without type information whether   -- this truly is a method or a lock.@@ -530,18 +530,20 @@             ++ " arguments but has been given " ++ show (length args)    (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args+  debugPrint $ "args': " ++ show args'   mapM_ (\ty -> check (isActorType ty) $                 "Trying to query lock with argument of type "                  ++ prettyPrint ty ++ "\n" ++                        "All arguments to lock query must be of type actor") tysArgs   let tyR = lockT [TcLock nam $ map (fromJust . mActorId) tysArgs]+  debugPrint $ "tyR: " ++ show tyR   return (tyR, foldl1 join (pL:psArgs),              MethodCallOrLockQuery (Just tyR) (notAppl nam) args')        tcMethodOrLockInv mi = tcMethodInv mi  -- | Check a true method invocation-tcMethodInv :: MethodInvocation () -> TcCodeM r (TcType, ActorPolicy, MethodInvocation T)+tcMethodInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T) tcMethodInv mi = do   debugPrint $ "tcMethodInv: " ++ prettyPrint mi   (n, msig, args, psArgs, pE, ef) <-@@ -582,8 +584,8 @@                   constraintLS argP parP $                       "Method applied to argument with too restrictive policy:\n" ++                        "Method invocation: " ++ prettyPrint mi ++ "\n" ++-                      "Argument: " ++ prettyPrint arg ++-                      "  with policy: " ++ prettyPrint argP +++                      "Argument: " ++ prettyPrint arg ++ "\n" +++                      "  with policy: " ++ prettyPrint argP ++ "\n" ++                       "Declared policy bound: " ++ prettyPrint parP              ) (zip3 args psArgs psPars)   -- Check E[branchPC](*) <= pW@@ -614,12 +616,17 @@ -- Policy expressions -- Treat them as pure compile-time for now -tcPolicyExp :: PolicyExp () -> TcCodeM r (PrgPolicy TcActor)+tcPolicyExp :: PolicyExp () -> TcCodeM (PrgPolicy TcActor) tcPolicyExp (PolicyLit _ cs) = do   tcCs <- mapM tcClause cs   return (TcPolicy tcCs) tcPolicyExp pe@(PolicyOf _ i) = do-  (_, _, param) <- lookupVar Nothing i+  vi@(_, _, param) <- lookupVar Nothing i+  debugPrint $ "tcPolicyExp: vi: " ++ show vi+  tm <- getTypeMap+  debugPrint $ "tcPolicyExp: TypeMap: " ++ show tm+  vm <- vars <$> getEnv+  debugPrint $ "tcPolicyExp: VarMap: " ++ show vm   check param $             "policyof may only be used on parameters: " ++ prettyPrint pe   return $ TcRigidVar i@@ -628,13 +635,13 @@   return $ TcRigidVar i tcPolicyExp (PolicyThis _) = return TcThis  -tcClause :: Clause () -> TcCodeM r (TcClause TcActor)+tcClause :: Clause () -> TcCodeM (TcClause TcActor) tcClause (Clause _ h ats) = do   tcH <- tcActor h   tcAs <- mapM tcAtom ats   return (TcClause tcH tcAs) -tcAtom :: Atom () -> TcCodeM r TcAtom+tcAtom :: Atom () -> TcCodeM TcAtom tcAtom (Atom _ n@(Name _ LName mPre i) as) = do   LSig _ ar _ <- lookupLock mPre i   check (length as == ar) $ "Arity mismatch in policy"@@ -643,11 +650,11 @@ tcAtom (Atom _ n _) = panic (tcExpModule ++ ".tcAtom") $                       "None-lock name: " ++ show n -tcActor :: Actor () -> TcCodeM r TcActor+tcActor :: Actor () -> TcCodeM TcActor tcActor (Var   _ i) = return $ TcVar i tcActor (Actor _ n) = TcActor <$> tcActorName n -tcActorName :: ActorName () -> TcCodeM r ActorId+tcActorName :: ActorName () -> TcCodeM ActorId tcActorName (ActorName    _ n) = getActorId n tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i @@ -655,7 +662,7 @@ --    Types of operators         -- ----------------------------------- -opType :: Op () -> TcType -> TcType -> TcCodeM r TcType+opType :: Op () -> TcType -> TcType -> TcCodeM TcType -- First the special cases: policy operators, and String conversion opType (Mult _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `join` p2)) opType (Add  _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `meet` p2))
src/Language/Java/Paragon/TypeCheck/TcStmt.hs view
@@ -26,7 +26,7 @@ --    Typechecking Statements    -- ----------------------------------- -tcStmt :: TypeCheck (TcCodeM r) Stmt+tcStmt :: TypeCheck TcCodeM Stmt  -- Rule EMPTY tcStmt (Empty _) = return $ Empty Nothing@@ -352,7 +352,7 @@ tcStmt s = fail $ "Unsupported statement: " ++ prettyPrint s  -withInits :: Maybe (ForInit ()) -> TcCodeM r a -> TcCodeM r (Maybe (ForInit T), a)+withInits :: Maybe (ForInit ()) -> TcCodeM a -> TcCodeM (Maybe (ForInit T), a) withInits Nothing tca = (Nothing,) <$> tca withInits (Just (ForInitExps _ es)) tca = do     (_,_,es') <- unzip3 <$> mapM tcExp es@@ -368,10 +368,10 @@ -- Typechecking Blocks and BlockStmts -- ---------------------------------------- -tcBlock :: TypeCheck (TcCodeM r) Block+tcBlock :: TypeCheck TcCodeM Block tcBlock (Block _ bss) = Block Nothing <$> tcBlockStmts bss -tcBlockStmts :: [BlockStmt ()] -> TcCodeM r [BlockStmt T]+tcBlockStmts :: [BlockStmt ()] -> TcCodeM [BlockStmt T] -- Rule EMPTYBLOCK tcBlockStmts [] = return [] @@ -395,7 +395,7 @@   tcLocalVars :: ActorPolicy -> TcType -> Bool -> [VarDecl ()] -            -> [VarDecl T] -> TcCodeM r a -> TcCodeM r ([VarDecl T], a)+            -> [VarDecl T] -> TcCodeM a -> TcCodeM ([VarDecl T], a) tcLocalVars _ _ _ [] acc cont = cont >>= \a -> return (reverse acc, a)  @@ -445,7 +445,7 @@     fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd  -localVarPol :: [Modifier ()] -> TcCodeM r ActorPolicy+localVarPol :: [Modifier ()] -> TcCodeM ActorPolicy localVarPol ms =      case [ p | Reads _ p <- ms ] of       [] -> newMetaPolVar --return bottom@@ -456,7 +456,7 @@ -- Typechecking Explicit Constructor Invocations -- --------------------------------------------------- -tcEci :: TypeCheck (TcCodeM r) ExplConstrInv+tcEci :: TypeCheck TcCodeM ExplConstrInv tcEci eci = do   (tyT, nwtas, as, con) <-        case eci of