--
-- (c) 2012 Wei Ke
--      license:          GPL-3
--      license-file:     LICENSE
--
-- |
-- The "St" module defines the configuration 'Conf',
-- the graph operations on state graphs,
-- and the operational semantics as the transformation rules between configurations.
--
module St(Conf(..), transCf) where

import ErrMsg
import Misc
import Graph
import RgAS
import Env
import Ty

data Conf = TermCf G        -- ^terminated configurations
          | NonTermCf K_ G  -- ^non-terminated configurations

swing :: G -> [E] -> [N] -> G
swing (G _ es r) ds vs = gc (es +../ [E s la t | (E s la _, t) <- zip ds vs]) r

new :: R -> G -> N -> E -> G
new (R _ res _) (G ns es r) t (E n la _) = gc es'' r where
    o = uniNO ns
    oest = getOutEdges res t
    es'' = es +. E n la o +../ [E o la' l | E _ la' l <- oest] 
     
transCf :: FunImpTab -> R -> Conf -> ErrMsg (Conf, String)
transCf fs env@(R _ res rsm) cf = trans cf where
    trans cf'@(TermCf _) = 
            return (cf', "")
    trans (NonTermCf k g) =
            case k of 
                Skip_ -> 
                    return (TermCf g, "")
                Decl_ tps -> 
                    return (TermCf (pushTps ini g tps), "")
                End_ _ -> 
                    return (TermCf (pop g), "")
                Assign_ ep1 ep2 -> do
                    d <- leval g ep1
                    n <- eval g ep2
                    return (TermCf (swing g [d] [n]), "")
                New_ t ep -> do 
                    d <- leval g ep
                    return (TermCf (new env g t d), "")
                Enter o vs xs rs -> do 
                    ns <- mape (eval g) vs
                    qs <- mape (po g) rs
                    return (TermCf (push g ([slfLa] ++ [LA x | x <- xs] ++ [LP x | x <- xs]) ([o] ++ ns ++ qs)), "")
                Leave xs cas rs -> do
                    ds <- mape (\(ep, x) -> searchTg g (LP x) |? "variable not found: " ++ show x >>= \q -> spo g ep q) (zip rs xs)
                    ns <- mape (eval g) [ep | ep <- zipCams xs cas]
                    return (TermCf (pop (swing g ds ns)), "")
                Invk_ ep m vs xs cas rs -> do
                    o <- eval g ep
                    s <- findTgG g o staLa |? "static table not found: " ++ show o
                    NK k' <- findTg res s (LA m) |? "method body not found" ++ show m
                    return (NonTermCf (Seq_ (Enter o vs xs rs) (Seq_ k' (Leave xs cas rs))) g, "")
                Seq_ k1 k2 -> do
                    (cf', output) <- trans (NonTermCf k1 g)
                    case cf' of
                        TermCf g' -> return (NonTermCf k2 g', output)
                        NonTermCf k1' g' -> return (NonTermCf (Seq_ k1' k2) g', output)
                If_ ep k1 k2 -> do
                    n <- eval g ep
                    case n of
                        NV (VBool False) -> return (NonTermCf k2 g, "")
                        NV (VBool True) -> return (NonTermCf k1 g, "")
                        _ -> fail ("mistyped if condition: " ++ show n)
                wk@(While_ ep k') -> do
                    n <- eval g ep
                    case n of
                        NV (VBool False) -> return (TermCf g, "")
                        NV (VBool True) -> return (NonTermCf (Seq_ k' wk) g, "")
                        _ -> fail ("mistyped while condition: " ++ show n)
                Print_ eol eps -> do
                    ns <- mape (eval g) eps
                    return (TermCf g, concat (map pr ns) ++ if eol then "\n" else "")
                   
    eval _ (Lit_ v) = return (NV v)
    eval g ep@(App_ s eps) =
            do
                f <- lookup s fs |? "function not found: " ++ s
                ns <- mape (eval g) eps
                f ns ++# ": " ++ show ep
    eval g@(G _ es _) ep'@(Cast_ t ep) =
            do
                n <- eval g ep
                s <- findTg es n staLa |? "static table not found: " ++ show n
                sm <- lookup s rsm |? "super class list not found: " ++ show s
                sm `contains` t |? "typecast not a superclass: " ++ show ep' 
                return n
    eval g Self_ =
            do
                n <- searchTg g slfLa |? "self not found"
                return n
    eval g (Var_ x) =
            do
                n <- searchTg g (LA x) |? "variable not found: " ++ show x
                return n                
    eval g@(G _ es _) (Attr_ ep a) =
            do
                n <- eval g ep
                n' <- findTg es n (LA a) |? "attribute not found: " ++ show a
                return n'                
    eval _ Wild_ = fail "illegal expression: _"
    
    leval g (Var_ x) = search g (LA x) |? "variable not found: " ++ show x
    leval g (Attr_ ep a) =
            do
                q <- eval g ep
                d <- findEdgeG g q (LA a) |? "attribute not found: " ++ show a
                return d
    leval (G ns _ _) Wild_ = 
            do
                let n = uniNO ns
                return (E n (LA (A_"")) n)                
    leval _ ep = fail ("illegal l-expression: " ++ show ep)
    
    po _ (Var_ _) = return (NV VNull)
    po g (Attr_ ep _) = eval g ep
    po _ Wild_ = return (NV VNull)
    po _ ep = fail ("illegal l-expression: " ++ show ep)
    
    spo g ep@(Var_ _) (NV VNull) = leval (popDirty g) ep
    spo (G _ es _) (Attr_ _ a) q | q /= NV VNull =
            do
                d <- findEdge es q (LA a) |? "attribute not found: " ++ show a
                return d
    spo g ep@Wild_ (NV VNull) = leval g ep
    spo _ ep _ = fail ("illegal l-expression: " ++ show ep)
    
    zipCams (x:xs) (Nothing:cas) = (Var_ x):(zipCams xs cas)
    zipCams (x:xs) (Just t:cas) = (Cast_ t (Var_ x)):(zipCams xs cas)
    zipCams _ _ =  []

    pr (NV (VInt x)) = show x
    pr (NV (VBool x)) = show x
    pr (NV (VTxt x)) = x
    pr (NV VNull) = "Nil"
    pr (NO x) = "@" ++ show x
    pr _ = "@???"

--
-- end of St
--
-- --$Id: St.hs 1182 2012-11-12 10:11:40Z wke@IPM.EDU.MO $