-- -- (c) 2012 Wei Ke -- license: GPL-3 -- license-file: LICENSE -- -- A type checker and runtime system of rCOS/g -- following the definitions in the "ggts-FCS" article: -- -- Title: A graph-based generic type system for object-oriented programs -- Authors: Wei Ke, Zhiming Liu, Shuling Wang and Liang Zhao -- Accepted by: Frontier of Computer Science -- Year: 2012 -- -- Programmed by: Wei Ke -- -- Date: 16/09/2012 (0.1) -- initial release -- -- Date: 30/09/2012 (0.2) -- added monadic ErrMsg -- changed to the `do' notation -- split to multiple modules -- added the Wild actual result parameter -- added a monadic parser using Parsec -- -- Date: 09/10/2012 (0.3) -- added visibility, environment, state transition, built-in functions -- -- Date: 30/10/2012 (0.4) -- added interactive session -- -- Date: 15/11/2012 (0.5) -- fixed some bugs -- stored nodes and edges in containers (Data.Set and Data.Map) -- changed Graph types to abstract -- -- | -- The "Main" module runs test cases, invokes the type checker and runtime system -- on the specified rCOS/g source @_file_@, and provides an interactive session. -- -- Usage: -- -- > TC built-in tests. -- > TC _file_ type-check _file_. -- > TC --gamma _file_ construct the initial type graph of _file_ only. -- > TC --env _file_ type-check and build environment of _file_. -- > TC --run _file_ type-check and run _file_. -- > TC --inter _file_ type-check and run _file_, -- > followed by an interactive session. -- module Main(main) where import System.Environment import System.IO import System.IO.Error import qualified Control.Exception as E import ErrMsg import Misc import Graph import RgAS import RgParser import Ty import Env import St main :: IO () main = do xs <- getArgs case xs of [] -> doList [ test1_Fig2u , test2_Fig2l , test3_Fig3 , test4_Fig5lt , test5_prg_Fig5 , test6_prg_Fig1 , test7_prg_Fig0 , test8_prg_Fig4 , test9_prg_Sec51 , testA_prg_Fib , help ] "--gamma":f:_ -> prGammaFile f "--env":f:_ -> prEnvFile f "--run":f:args -> prRunFile f args "--inter":f:args -> prInterRunFile f args ['-':_] -> help f:_ -> prTcFile f where doList [] = return () doList [t] = t doList (t:ts) = do t putStrLn "" doList ts help :: IO () help = putStrLn "\ \A type checker and runtime system of rCOS/g (ggts-FCS).\n\ \See http://a319-101.ipm.edu.mo/~wke/ggts/impl/ for more information.\n\ \ \n\ \Usage:\n\ \ TC built-in tests.\n\ \ TC _file_ type-check _file_.\n\ \ TC --gamma _file_ build the initial type graph of _file_ only.\n\ \ TC --env _file_ type-check and build the environment of _file_.\n\ \ TC --run _file_ type-check and run _file_.\n\ \ TC --inter _file_ type-check and run _file_, \n\ \ followed by an interactive session.\n\ \" prSection :: String -> IO () prSection s = putStrLn ("\n---- " ++ s ++ " ----") prTcFile :: FilePath -> IO () prTcFile f = do m <- tc f case m of OK (h, _, _, _) -> do prSection "Type graph" print h err -> print err tc :: FilePath -> IO (ErrMsg (H, P_, VisTab, FunTab)) tc f = do r <- parsePrg'File f putStrLn "Type-checking ..." return (r >>= \prg' -> tcPrg' prg') prGammaFile :: FilePath -> IO () prGammaFile f = do r <- parsePrg'File f case (r >>= \prg' -> consTyHPrg' prg') of OK h -> do prSection "Type graph" print h err -> print err prEnvFile :: FilePath -> IO () prEnvFile f = do m <- tc f case m of OK (h, p, viss, _) -> do prSection "Type graph" print h let env = consEnv viss p h prSection "Environment graph" print env err -> print err prRunFile :: FilePath -> [String] -> IO () prRunFile f args = do m <- tc f case m of OK (h, p, viss, _) -> do erg <- run (builtInFunTabWithArgs args) viss p h case erg of OK (_, g) -> do prSection "Resulted stable state graph" print g err -> print err err -> print err prInterRunFile :: FilePath -> [String] -> IO () prInterRunFile f args = do m <- tc f case m of OK (h, p@(P_ _ (tps, _)), viss, funs) -> do let ft = builtInFunTabWithArgs args erg <- run ft viss p h case erg of OK (env, g) -> do prSection "Interactive session, ended by EOF" inter funs ft viss p (newDeltaTps id tps) h env g _ -> return () err -> print err tcString :: String -> ErrMsg (H, P_, VisTab, FunTab) tcString s = parsePrg'String s >>= \prg' -> tcPrg' prg' takeHP :: ErrMsg (H, P_, VisTab, [Fun]) -> ErrMsg (H, P_) takeHP x = x >>= \(h, p, _, _) -> return (h, p) envString :: String -> ErrMsg R envString s = tcString s >>= \(h, p, viss, _) -> return (consEnv viss p h) runString :: String -> IO (ErrMsg G) runString s = case tcString s of OK (h, p, viss, _) -> run builtInFunTab viss p h >>= \erg -> return (erg >>= \(_, g) -> return g) Err e -> return (Err e :: ErrMsg G) runMainCmd :: FunImpTab -> R -> K_ -> G -> IO (ErrMsg G) runMainCmd ft env k g = next (NonTermCf k g, "") where next (TermCf g', output) = do putStr output return (OK g') next (cf@(NonTermCf _ _), output) = do putStr output case transCf ft env cf of OK x -> next x Err s -> return (Err s) run :: FunImpTab -> VisTab -> P_ -> H -> IO (ErrMsg (R, G)) run ft viss p@(P_ _ (tps, k)) h = do let env = consEnv viss p h putStrLn "Running ..." gm <- runMainCmd ft env k (newDeltaTps ini tps) return (gm >>= \g -> return (env, g)) inter :: FunTab -> FunImpTab -> VisTab -> P_ -> G -> H -> R -> G -> IO () inter funs ft viss p delta h@(H ns _) env g = do putStr "> " hFlush stdout lnm <- catchIOError (getLine >>= \ln -> return (Just ln)) (\e -> if isEOFError e then return Nothing else ioError e) case lnm of Just ln -> case parseCmd'String ln >>= \c -> tcMainCmd' funs viss delta h c of OK (delta', h'@(H ns' _), k) -> do let env' = if ns' /= ns then consEnv viss p h' else env gm <- E.catchJust (\e -> case e of E.UserInterrupt -> Just () ; _ -> Nothing) (runMainCmd ft env' k g) (\_ -> return (Err "<>")) case gm of OK g' -> inter funs ft viss p delta' h' env' g' err -> prErrCont err err -> prErrCont err _ -> do prSection ("Resulted " ++ (if height g > 0 then "***unstable" else "stable") ++ " state graph") print g where prErrCont err = print err >> inter funs ft viss p delta h env g -- -- -- -- -- test cases -- test1_Fig2u :: IO () test1_Fig2u = do putStrLn "Test 1 (Fig. 2 upper): " putStrLn (" graph h: " ++ show h) putStrLn (" nodes u,v,w,r: " ++ show u ++ show v ++ show w ++ show r) putStrLn (" t-eq u v: " ++ show (teqH h u v)) putStrLn (" t-eq v r: " ++ show (teqH h v r)) putStrLn (" t-eq v Bool: " ++ show (teqH h v (NP BOOL))) where (h1, [u,v,w,r]) = rep 4 (newNodeH uniNS) emptyH h2 = addNodesH h1 [NP BOOL] a = LA(A_"a") b = LA(A_"b") h = addEdgesH h2 [E u a v, E v a w, E w a r, E r a r, E u b (NP BOOL), E v b (NP BOOL), E w b (NP BOOL), E r b (NP BOOL)] test2_Fig2l :: IO () test2_Fig2l = do putStrLn "Test 2 (Fig. 2 lower): " putStrLn (" graph h: " ++ show h) putStrLn (" nodes u,v,x,y: " ++ show u ++ show v ++ show x ++ show y) putStrLn (" t-eq u v: " ++ show (teqH h u v)) putStrLn (" t-eq u x: " ++ show (teqH h u x)) where (h1, [u, v, x, y]) = rep 4 (newNodeH uniNS) emptyH h2 = addNodesH h1 [NP INT, NP TXT] [a1, a2, b, p, q] = [LA(A_ s) | s <- ["a1","a2","b","p","q"]] h = addEdgesH h2 [E u b u, E u p (NP INT), E u a1 x, E x q (NP TXT), E x a2 v, E v a1 y, E v b v, E v p (NP INT), E y q (NP TXT), E y a2 v] test3_Fig3 :: IO () test3_Fig3 = do putStrLn "Test 3 (Fig. 3): " putStrLn (" graph h: " ++ show h) putStrLn (" nodes v1,v2,r1,r2: " ++ show v1 ++ show v2 ++ show r1 ++ show r2) putStrLn (" t-eq v1 v2: " ++ show (teqH h v1 v2)) putStrLn (" t-eq r1 r2: " ++ show (teqH h r1 r2)) where (h1, [n1, n2, n3, n4, n5, n6, n7, n8, n9, n10]) = rep 10 (newNodeH uniNS) emptyH [a, b, x, y, z, m, m1, m2, m3] = [LA(A_ s) | s <- ["a","b","x","y","z","m","m1","m2","m3"]] [_B, _C1, _C2, _D, _T1, _T2, _T3] = [NC(U_ s) | s <- ["B","C1","C2","D","T1","T2","T3"]] h2 = addNodesH h1 [_B, _C1, _C2, _D, _T1, _T2, _T3] h3 = addEdgesH h2 [E _B b _B, E _B staLa n7, E n7 m n4, E n4 x _D, E n4 y _C2, E _C2 b _T3, E _C2 staLa n1, E n1 m3 n2, E n2 z _T3, E _D staLa n5, E _D b _T3, E n5 m3 n3, E n5 m2 n6, E n3 z _T3, E n6 y _T2, E n8 y _T2, E n9 m1 n10, E n9 m2 n8, E n10 x _T1, E _C1 a _T1, E _C1 staLa n9, E _C1 isaLa _D] (h4, v1) = shlo h3 _B (h5, v2) = shlo h4 _B Just (h6, r1) = conj h5 [_C1, _C2] Just (h, r2) = conj h6 [_C1, _C2] test4_Fig5lt :: IO () test4_Fig5lt = do putStrLn "Test 4 (Fig. 5 List & Tree): " putStrLn (" graph h: " ++ show h) putStrLn (" nodes nTnw,nTne,nTsw,nTse,nLn,nLs: " ++ show nTnw ++ show nTne ++ show nTsw ++ show nTse ++ show nLn ++ show nLs) putStrLn (" nodes shlo List (sL), shlo Tree (sT): " ++ show sL ++ show sT) putStrLn (" t-eq sL nLs: " ++ show (teqH h sL nLs)) putStrLn (" t-eq sT nTsw: " ++ show (teqH h sT nTsw)) putStrLn (" isInsGe nTne List : " ++ show (isInsGe h nTne list [gamma :- sT])) where (h1, [nTnw, nTne, nTsw, nTse, nLn, nLs]) = rep 6 (newNodeH uniNS) emptyH tree = NC (U_"Tree") delta = NX (X_ (U_"Tree") "delta") list = NC (U_"List") gamma = NX (X_ (U_"List") "gamma") a = LA(A_"a") b = LA(A_"b") h2 = addNodesH h1 [tree, list, delta, gamma] h3 = addEdgesH h2 [E tree isaLa nTnw, E nTnw b nTne, E nTnw a delta, E nTne isaLa nTse, E nTsw isaLa nTnw, E nTse a nTsw, E nTse b nTne, E list isaLa nLn, E nLn b nLs, E nLn a gamma, E nLs isaLa nLn] (h4, sL) = shlo h3 list (h, sT) = shlo h4 tree test5_prg_Fig5 :: IO () test5_prg_Fig5 = do putStrLn "Test 5 (program of Fig. 5): " putStrLn (" env prg_Fig5: " ++ show (envString prg_Fig5)) prg_Fig5 :: String prg_Fig5 = "\ \ class Pair { \n\ \ pub. alpha a; \n\ \ pub. beta b; \n\ \ pr(Txt x, Int y) { \n\ \ var Txt rx, Int ry; \n\ \ if ( isz(self.a) ) self.a.pr(\"*\", 1 : x, y : rx, ry); else skip; \n\ \ if ( isz(self.b) ) self.b.pr(\"*\", 2 : x, y : rx, ry); else {} \n\ \ end rx, ry; \n\ \ } \n\ \ } \n\ \ \n\ \ class List \n\ \ ext. Pair> {} \n\ \ \n\ \ class Tree \n\ \ ext. Pair>> \n\ \ {} \n\ \ \n\ \ class Printable { \n\ \ pr(Txt x, Int y) {} \n\ \ } \n\ \ \n\ \ class Empty {} \n\ \ \n\ \ fun isz(&Empty) -> Bool; \n\ \ \n\ \ main { \n\ \ Tree tr, Bool bo; \n\ \ var Bool bo2; \n\ \ var Bool bo3; \n\ \ Tree.new(tr); \n\ \ bo := true; \n\ \ bo2 := bo; \n\ \ bo3 := bo2; \n\ \ end bo3; \n\ \ end bo2; \n\ \ } \n\ \" test6_prg_Fig1 :: IO () test6_prg_Fig1 = do putStrLn "Test 6 (program of Fig. 1): " putStrLn (" env prg_Fig1: " ++ show (envString prg_Fig1)) prg_Fig1 :: String prg_Fig1 = "\ \ main {} \n\ \ \n\ \ class C ext. D { \n\ \ Txt a; \n\ \ beta b; \n\ \ m1(Txt x) { \n\ \ x := \"x\"; \n\ \ self.a := x; \n\ \ var Int x, Bool y; \n\ \ self.m4(200, true : y, x : x, y); \n\ \ self.m4(false, 100 : x, y : _, x); \n\ \ end y, x; \n\ \ } \n\ \ } \n\ \ \n\ \ class I { \n\ \ m2(Txt x, Txt y) { skip; } \n\ \ } \n\ \ \n\ \ class D { \n\ \ Int i; \n\ \ m3(Int x) {} \n\ \ m4(Bool x, Int y) { \n\ \ if ( x ) { \n\ \ x := false; \n\ \ while ( ge(y, 100) ) y := sub(y, 13); \n\ \ } else skip; \n\ \ } \n\ \ } \n\ \ \n\ \ class N { // this class is not in Fig. 1 \n\ \ m1(Txt x) {} \n\ \ Txt a; \n\ \ m2(Txt x, Txt y) { x := y; } \n\ \ m3(Int x) {} \n\ \ m4(Bool x, Int y) {} \n\ \ m5(C x, D y) { \n\ \ x := (C) y; \n\ \ y := x; \n\ \ var &(I, C) z; \n\ \ N.new(z); \n\ \ x.b := (N)z; \n\ \ z := self; \n\ \ end z; \n\ \ } \n\ \ I b; \n\ \ Int i; \n\ \ priv. Int j; \n\ \ } \n\ \ \n\ \ fun ge(Int, Int) -> Bool; \n\ \ fun sub(Int, Int) -> Int; \n\ \" test7_prg_Fig0 :: IO () test7_prg_Fig0 = do let hpv = tcString prg_Fig0 putStrLn "Test 7 (program of Fig. in Introduction): " putStrLn (" tcPrg prg_Fig0: " ++ show (hpv >>= \(h, p, _, _) -> return (h, p))) case hpv of OK (h, (P_ _ (tps, _)), viss, funs) -> do putStrLn " tcK h (Decl A x, B y" putStrLn " Assign x (y . a . b . a . b)" putStrLn " End x, y" putStrLn (" : " ++ let OK c = parseCmd'String "var A x, B y; x := y.a.b.a.b; end x, y;" in show (tcMainCmd' funs viss (newDeltaTps id tps) h c)) _ -> return () prg_Fig0 :: String prg_Fig0 = "\ \ class A { pub. beta b; } \n\ \ class B { pub. A a; } \n\ \ main { \n\ \ var A x, B y; \n\ \ x.b.a := x; \n\ \ x := y.a.b.a; \n\ \ end x, y; \n\ \ } \n\ \" test8_prg_Fig4 :: IO () test8_prg_Fig4 = do putStrLn "Test 8 (program of Fig. 4): " putStrLn (" tcPrg prg_Fig4: " ++ show (takeHP (tcString prg_Fig4))) prg_Fig4 :: String prg_Fig4 = "\ \ class C { \n\ \ pub. alpha a; \n\ \ pub. beta b; \n\ \ } \n\ \ \n\ \ class B { \n\ \ pub. A a; \n\ \ } \n\ \ \n\ \ class A { \n\ \ pub. B b; \n\ \ pub. alpha2 e; \n\ \ } \n\ \ \n\ \ main { \n\ \ var A x, B y, \n\ \ C> z; \n\ \ x.b.a := x; \n\ \ x := y.a.b.a; \n\ \ x.b := y; \n\ \ z.b.b := z.b.a; \n\ \ z.b.a := \"z\"; \n\ \ z.a := x.e; \n\ \ end x,y,z; \n\ \ } \n\ \" test9_prg_Sec51 :: IO () test9_prg_Sec51 = do putStrLn "Test 9 (program of 5.1 well-formed type substitutions): " putStrLn (" tcPrg prg_Sec51: " ++ show (takeHP (tcString prg_Sec51))) prg_Sec51 :: String prg_Sec51 = "\ \ class C { \n\ \ pub. alpha a; \n\ \ pub. beta b; \n\ \ m() { self.b := self.a; } \n\ \ } \n\ \ \n\ \ class B {} \n\ \ \n\ \ class A ext. B {} \n\ \ \n\ \ main { \n\ \ var C x, \n\ \ C y, \n\ \ C z, \n\ \ C w; \n\ \ end x, y, z, w; \n\ \ } \n\ \" testA_prg_Fib :: IO () testA_prg_Fib = do putStrLn "Test A (Fibonacci): " putStrLn (" tcPrg prg_Fib: ") eg <- runString prg_Fib print eg prg_Fib :: String prg_Fib = "\ \ class Fib { \n\ \ priv. Int a; \n\ \ priv. Int b; \n\ \ \n\ \ init(Int a, Int b) { \n\ \ self.a := a; \n\ \ self.b := b; \n\ \ } \n\ \ \n\ \ next(Int n) { \n\ \ print self.a, \",\",; \n\ \ print self.b; \n\ \ if ( gtInt(n, 1) ) { \n\ \ self.a := add(self.a, self.b); \n\ \ self.b := add(self.a, self.b); \n\ \ self.next(sub(n, 2) : n : _); \n\ \ } else if ( gtInt(n, 0) ) { \n\ \ self.b := add(self.a, self.b); \n\ \ self.a := sub(self.b, self.a); \n\ \ print self.b; \n\ \ } else skip; \n\ \ } \n\ \ } \n\ \ \n\ \ main { \n\ \ Fib fib, Int n; \n\ \ \n\ \ Fib.new(fib); \n\ \ n := 100; \n\ \ \n\ \ fib.init(0, 1 : a, b : _, _); \n\ \ fib.next(n : n : _); \n\ \ } \n\ \" -- -- end of Main -- -- --$Id: Main.hs 1193 2012-11-15 05:36:23Z wke@IPM.EDU.MO $