--
-- (c) 2012 Wei Ke
--      license:          GPL-3
--      license-file:     LICENSE
--
-- |
-- The "Ty" module defines the graph nodes 'N', the edge labels 'La',
-- the visibility table 'VisTab', the original program command lists 'P', 
-- the environment dependent commands 'K_' and program command lists 'P_', 
-- and the type operations and type-checking rules.
--
module Ty ( La(..), isaLa, staLa, scpLa, slfLa
          , VisTab
          , K_(..)
          , Typing_(..), unzipTps_, zipTps_
          , Ep_(..)
          , P_(..)
          , N(..), isNC, isNO, ini, iniL
          , E, H, G, Ns, Es
          , uniNS, uniNO
          , teqH
          , shlo, conj, clo, cloH, insT, reuseInsT, gecls, ssj, subty
          , isTy, isCc, isInsGe, getSta
          , height, search, searchTg, push, pushTps, pop, popDirty, newDeltaTps
          , tcPrg', tcMainCmd', consTyHPrg'
          )

where

import Data.List
import Data.Maybe
import Control.Monad

import ErrMsg
import Misc
import qualified Zp
import Graph
import RgAS

--
-- | 
-- special symbol name
--
data B_ = B_ String deriving (Eq, Ord)

--
-- |
-- edge labels
--
data La = LA A_     -- ^ variables, attributes, methods
        | LB B_     -- ^ special labels: isa, sta, scope and self
        | LX X_     -- ^ type variables as labels
        | LP A_     -- ^ special labels to parent objects
    deriving (Eq, Ord)

instance Show La where
    show (LA (A_ s))   = s
    show (LP (A_ s))   = s ++ "*"
    show (LB (B_"$"))  = "$"
    show (LB (B_ s))   = "%" ++ s
    show (LX (X_ _ s)) = "\'" ++ s

isLA :: La -> Bool       
isLA (LA _) = True
isLA _      = False
   
isLX :: La -> Bool       
isLX (LX _) = True
isLX _      = False

--
-- |  
-- special edge labels
--
isaLa, staLa, scpLa, slfLa :: La
isaLa = LB (B_"isa")
staLa = LB (B_"sigma")
scpLa = LB (B_"$")
slfLa = LB (B_"self")

--
-- |
-- original program command lists
--
data P  = P [(U_, A_, Cmd)] ([Typing], Cmd) deriving Show

-- |
-- visibility tables
--
type VisTab = [(U_, A_, Vis)]

--
-- |
-- environment dependent commands
--
data K_ = Skip_
        | Decl_ [Typing_]
        | End_ [A_]
        | New_ N Ep_
        | Assign_ Ep_ Ep_
        | Invk_ Ep_ A_ [Ep_] [A_] [Maybe N] [Ep_]
        | Seq_ K_ K_
        | If_ Ep_ K_ K_
        | While_ Ep_ K_
        | Print_ Bool [Ep_]
        | Enter N [Ep_] [A_] [Ep_]
        | Leave [A_] [Maybe N] [Ep_]
    deriving (Eq, Ord)
    
instance Show K_ where
    show _ = "<<K_>>"

--
-- |
-- environment dependent typings
--
data Typing_ = Typing_ N A_ deriving (Eq, Ord, Show)

unzipTps_ :: [Typing_] -> ([N], [A_])
unzipTps_ (Typing_ t x:tps) =  (t:ts, x:xs) where (ts, xs) = unzipTps_ tps
unzipTps_ _                 =  ([], [])

zipTps_ :: [N] -> [A_] -> [Typing_]
zipTps_ (n:ns) (x:xs) =  Typing_ n x:(zipTps_ ns xs)
zipTps_ _ _           =  []

--
-- |
-- environment dependent expressions
--
data Ep_ 
        = Self_
        | Lit_ V_
        | App_ String [Ep_]
        | Var_ A_
        | Attr_ Ep_ A_
        | Cast_ N Ep_
        | Wild_
    deriving (Eq, Ord)

instance Show Ep_ where
    show Self_         = "self"
    show (Lit_ x)      = show x
    show (App_ f eps)  = f ++ "(" ++ showElems eps ++ ")"
    show (Var_ (A_ x)) = x
    show (Attr_ ep (A_ x)) 
                       = show ep ++ "." ++ x
    show (Cast_ t ep)  = "(" ++ show t ++ ") " ++ show ep
    show Wild_         = "_"

--
-- |
-- environment dependent program command lists
--
        
data P_ = P_ [(U_, A_, K_)] ([Typing_], K_) deriving Show

--
-- |
-- nodes
--
data N  = NP D_     -- ^ primitive types
        | NC U_     -- ^ classes
        | NX X_     -- ^ type variables
        | NS Int    -- ^ structural types
        | NO Int    -- ^ objects
        | NV V_     -- ^ primitive type values
        | NK K_     -- ^ environment dependent commands
    deriving (Eq, Ord)
    
instance Show N where
    show (NP INT)    = "Int"
    show (NP BOOL)   = "Bool"
    show (NP TXT)    = "Txt"
    show (NP NULL)   = "Null"
    show (NP WILD)   = "_"
    show (NC (U_ s)) = "(" ++ s ++ ")"
    show (NX (X_ (U_ q) s)) 
                     = "(" ++ q ++ "\'" ++ s ++ ")"
    show (NS x)      = "(" ++ show x ++ ")"
    show (NO x)      = "@" ++ show x
    show (NV x)      = "#" ++ show x
    show (NK x)      = show x
       
isNC :: N -> Bool       
isNC (NC _) =  True
isNC _      =  False

isNConst :: N -> Bool
isNConst (NP _) = True
isNConst (NC _) = True
isNConst _      = False
    
isNO :: N -> Bool       
isNO (NO _) = True
isNO _ = False

minNS, maxNS, minNO, maxNO :: N
minNS = NS 0
maxNS = NS maxBound
minNO = NO 0
maxNO = NO maxBound

ini :: N -> N
ini (NP INT)    = NV (VInt 0)
ini (NP BOOL)   = NV (VBool False)
ini (NP TXT)    = NV (VTxt "")
ini _           = NV VNull 
    
iniL :: N -> Ep
iniL (NP INT)   = Lit (VInt 0)
iniL (NP BOOL)  = Lit (VBool False)
iniL (NP TXT)   = Lit (VTxt "")
iniL _          = Lit VNull 

-- 
-- concrete types for graphs
--

type E  = Eg N La   -- ^ edges

type H  = Hg N La   -- ^ type graphs

type G  = Gg N La   -- ^ rooted graphs

type Ns = Nsg N     -- ^ sets of nodes

type Es = Esg N La  -- ^ sets of edges

uniNS :: Ns -> N
uniNS ns = case nodeLT ns maxNS of Just (NS i) -> NS (i+1) ; _ -> minNS

uniNO :: Ns -> N
uniNO ns = case nodeLT ns maxNO of Just (NO i) -> NO (i+1) ; _ -> minNO

--
-- type-equivalence and basic relations
--

teqm :: G -> G -> Maybe [(Ns, Ns)]
teqm (G _ esx rx) (G _ esy ry) = teq0 [(singleton rx, singleton ry)] where

    elx = toList esx
    ely = toList esy

    fstadd (s, t) tg = (s +. tg, t)

    sndadd (s, t) tg = (s, t +. tg)

    findQ sel n q = find (\p -> sel p `contains` n) q
    
    findQ2 sel n1 n2 q = find (\p -> let ns = sel p in (ns `contains` n1) && (ns `contains` n2)) q

    teq0 q = 
            case findm (\(s, t) -> findExt esx fst s >>= \e -> return (t, e)) q of
                Just (t, E _ la x') -> case findAny esy t la of
                    Just (E _ _ y') -> case addTg fstadd x' snd y' of 
                        Just q' -> teq0 q'
                        _       -> teq0 ((singleton x', singleton y'):q)
                    _ -> Nothing
                _ -> case findm (\(s, t) -> findExt esy snd t >>= \e -> return (s, e)) q of
                        Just (s, E _ la y') -> case findAny esx s la of
                            Just (E _ _ x') -> case addTg sndadd y' fst x' of 
                                Just q' -> teq0 q'
                                _       -> teq0 ((singleton x', singleton y'):q)
                            _ -> Nothing
                        _ -> teq1 q
        where
        
        findExt es sel ns = findm (\n -> find (\(E _ _ tg) -> isNothing (findQ sel tg q)) (getOutEdges es n)) (toList ns)
        findAny es ns la = findm (\n -> findEdge es n la) (toList ns)
        
        addTg seladd tg1 sel tg2 = 
                do  let zp = Zp.find (\p -> sel p `contains` tg2) (Zp.start q)
                    p <- Zp.current zp
                    return (Zp.finish (Zp.replace zp (seladd p tg1)))
    
    teq1 q = 
            case findm2 (\e1 e2 -> mergeDiffTg fst e1 e2) elx of
                Just q' -> teq1 q'
                _ -> case findm2 (\e1 e2 -> mergeDiffTg snd e1 e2) ely of
                    Just q' -> teq1 q'
                    _ -> teq2 q
        where 
        
        mergeDiffTg sel (E n1 la1 n1') (E n2 la2 n2') 
                | la1 == la2 && isJust (findQ2 sel n1 n2 q) = mergeTg sel n1' n2'       
                | otherwise = Nothing

        mergeTg sel tg1 tg2 =
                do  let zp1 = Zp.find (\p -> sel p `contains` tg1) (Zp.start q)
                    (s1, t1) <- Zp.current zp1
                    let zp2 = Zp.find (\p -> sel p `contains` tg2) (Zp.rewind (Zp.remove zp1))
                    (s2, t2) <- Zp.current zp2
                    return (Zp.finish (Zp.replace zp2 (s1 +.. s2, t1 +.. t2)))
                
    teq2 q = 
            if any (\(s, t) -> conflictNs (s +.. t)) q then Nothing
            else if any (\(s, t) -> conflictLas (toList s) (toList t)) q then Nothing
            else Just q                        
        where
        
        conflictLas [x] [y] = not (setEq (getOutLas esx x) (getOutLas esy y))
        conflictLas (x:xs) [y] = conflictLas [x] [y] || conflictLas xs [y]
        conflictLas xs@(x:_) (y:ys) = conflictLas [x] [y] || conflictLas xs ys
        conflictLas _ _ = undefined

        conflictNs ns = size ns > 1 && (isJust (nodeLT ns minNS) || isJust (nodeGT ns maxNS)) 

teq :: G -> G -> Bool
teq g g' = isJust (teqm g g')
    
teqH :: H -> N -> N -> Bool
teqH = greltoh teq

subcls :: G -> G -> Bool
subcls g' g = teq g' g || isJust (findTgGr g' isaLa >>= \n -> teqm (gcG g' n) g)

subclsH :: H -> N -> N -> Bool
subclsH = greltoh subcls

shlocover :: G -> G -> Bool
shlocover g' g =  all (\(E _ la n) -> isJust (findTgGr g' la >>= \n' -> teqm (gcG g n) (gcG g' n'))) (getOutEdgesGr g)

cover :: G -> G -> Bool
cover g'@(G _ es' r') (G _ es r) = cvr g' (ts r) && cvr gs' (ss r) where
    gs' = fromJust (findTg es' r' staLa >>= \s' -> return (gcG g' s'))
    ts x = x:fromJust ((findTg es x isaLa >>= \n -> return (ts n)) `mplus` return [])
    ss x = fromJust (findTg es x staLa):fromJust ((findTg es x isaLa >>= \n -> return (ss n)) `mplus` return [])
    cvr gx xs = all (\x -> shlocover gx (gcWith1stLev isLA es x)) xs

supcover :: G -> G-> Bool
supcover g' g = (findTgGr g isaLa, True) ?>>= \n -> subcls g' (gcG g n)

supcoverH :: H -> N -> N -> Bool
supcoverH = greltoh supcover

--
-- type operations
--

reuseEqTy :: H -> (H, N) -> (H, N)
reuseEqTy h@(H ns _) p@(h', n') = (find (\n -> teq (gcH h n) (gcH h' n')) (toList ns), p) ?>>= \n -> (h, n) 

shlo :: H -> N -> (H, N)
shlo (H ns es) r =  (H ns' es', r') where
    (ns', r') = newNode uniNS ns
    es' = es +../ [E r' la t | E _ la t <- getOutEdges es r]

conj :: H -> [N] -> Maybe (H, N)
conj h@(H ns es) rs =
        do  let allLas = [la | la <- getAllLas es, isLA la]
            ats <- mcat [dist la (coTg [la]) | la <- allLas]
            mts <- mcat [dist la (coTg [staLa, la]) | la <- allLas]
            let (ns', [r,s]) = rep 2 (newNode uniNS) ns
                es' = es +. E r staLa s +../ [E r la t | (la, t) <- ats] +../ [E s la t | (la, t) <- mts]
            return (H ns' es', r) where

    dist x ms = ms >>= \y -> return (x, y)
    
    mcat mps = foldm (\mps' mp -> mp >>= \(la, xs) -> return ([(la, x) | x <- xs] ++ mps')) (return []) mps

    coTg las =
            case ts of 
                t:ts' -> all (\x -> teqH h t x) ts' &>> return [t]
                _     -> return []
        where
                
        ts = [t | E _ _ t <- fromJust (findAll rs [])]
        findAll [] es' = return es'
        findAll (n:ns') es' = (findTg es n isaLa >>= \n' -> return (n':ns')) `mplus` (return ns') >>= \ns'' ->
                              (findTrace es n las >>= \e -> findAll ns'' (e:es')) `mplus` (findAll ns'' es')

clo :: Es -> N -> Maybe G
clo es t =
        do  let G ns' es' _ = gc es t
            (h', t') <- conj (H ns' es') [t]
            return (gcH h' t')

cloG :: G -> Maybe G
cloG (G _ es r) = clo es r

cloH :: H -> N -> Maybe G
cloH (H _ es) t = clo es t

clocover :: G -> G -> Bool
clocover g' g = (cloG g', False) ?>>= \g'' -> cover g'' g
                
clocoverH :: H -> N -> N -> Bool
clocoverH =  greltoh clocover

mfr :: G -> La -> Maybe [E]
mfr g m =
        do  G _ es r <- cloG g
            n <- findTraceTg es r [staLa, m]
            return (getOutEdges es n)

insT :: Sst N -> H -> N -> (H, N)
insT sst (H ns es) t = (H ns' es', fromJust (lookupSst f t)) where
    (ns', es', f) = ins0 ns es [t] sst
    
    ins0 xs ds [] m = (xs, ds, m)
    ins0 xs ds (r:ts) m | isJust (lookupSst m r) = ins0 xs ds ts m
    ins0 xs ds (r@(NS _):ts) m = ins0 xs' ds' ts m' where
        (xs'', j) = newNode uniNS xs
        ros = getOutEdges ds r
        (xs', ds'', m') = ins0 xs'' ds [n | E _ _ n <- ros] (r :- j:m)
        ds' = ds'' +../ [E j la (fromJust (lookupSst m' n)) | E _ la n <- ros]
    ins0 xs ds (r:ts) m = ins0 xs ds ts (r :- r:m)

reuseInsT :: Sst N -> H -> N -> (H, N)
reuseInsT sst h t = reuseEqTy h (insT sst h t)

insGe :: Sst N -> H -> N -> (H, N)
insGe sst h t = insT sst h' n where (h', n) = shlo h t

reuseInsGe :: Sst N -> H -> N -> (H, N)
reuseInsGe sst h t = reuseEqTy h (insGe sst h t)

--
-- type graph construction
--

type F = [(Te, N)]

insTe :: Te -> Sst Te -> Te
insTe te sst =
        case lookupSst sst te of
            Just y -> y
            _ -> case te of
                TCj cl sst' -> TCj cl [x :- insTe y sst | x :- y <- sst']
                TCn tes     -> TCn [insTe x sst | x <- tes]
                _           -> te

getTraceTg :: H -> N -> [La] -> N
getTraceTg h n las = fromJust (findTraceTgH h n las) 

getSta :: H -> N -> N
getSta h n =  fromJust (findTgH h n staLa) 

getStaTg :: H -> N -> La -> N
getStaTg h n la =  getTraceTg h n [staLa, la] 

consTyH :: Program -> H
consTyH p = gcs es nl where
    (H ns es, _) = consTyH' p
    nl = [n | n <- toList ns, isNConst n]

consTyH' :: Program -> (H, F)
consTyH' (Program cdecls _) =  (h1, theF1) where

    (h0, emptySta) = newNodeH uniNS emptyH

    (h1, theF1) = (h0, []) 
              >>> (foldCdecls consSta)
              >>> (foldCdecls consExt)
              >>> (foldCdecls consTV)
              >>> (foldCdecls consAttr)
              >>> (foldCdecls consMeth)
              >>> (foldCdecls consPar)
              >>> (consIns) 
              >>> (consConj)
              >>> (foldCdecls consMemCnstr)
              >>> (consPrimSta)
    
    (x, y) >>> f = f x y
    
    foldCdecls f = \x y -> foldl (\(x', y') cdecl -> f cdecl x' y') (x, y) cdecls

    ensureTe te h@(H ns es) theF =
            case lookup te theF of
                Just n -> (n, h, theF)
                _      -> case te of
                    TP d     -> let n = NP d  in (n, H (ns +. n) es, (te, n):theF) 
                    TC cl    -> let n = NC cl in (n, H (ns +. n) es, (te, n):theF)
                    TX tv    -> let n = NX tv in (n, H (ns +. n) es, (te, n):theF)
                    TCn tes  -> let (_, H ns'' es'', theF'') = 
                                        foldl (\(_, hx, theFx) x -> ensureTe x hx theFx) (undefined, h, theF) tes
                                    (ns', n) = newNode uniNS ns''
                                in  (n, H ns' es'', (te, n):theF'')
                    TCj _ ss -> let (_, H ns'' es'', theF'') = 
                                        foldl (\(_, hx, theFx) x -> ensureTe x hx theFx) (undefined, h, theF) zs
                                    zs = foldl (\zs' (l :- r) -> l:r:zs') [] ss
                                    (ns', n) = newNode uniNS ns''
                                in  (n, H ns' es'', (te, n):theF'')
    getTe te theF = fromJust (lookup te theF)
            
    ensureEdgeNS h@(H ns es) n la =
            case findTg es n la of
                Just n' -> (h, n')
                _       -> let (ns', n') = newNode uniNS ns in (H ns' (es +. E n la n'), n')

    ensureEdgeNC h@(H _ es) e@(E n la n') = 
            case findTg es n la of
                Just n'' -> (h, n'')
                _        -> (addEdgesH h [e], n')
        
    ensureTyping h theF n (Typing te a) = (h', theF') where
        (t, h'', theF') = ensureTe te h theF
        (h', _) = ensureEdgeNC h'' (E n (LA a) t)
        
    shloTake (H ns es) n n' = H ns (es +../ [E n la t | E _ la t <- getOutEdges es n'])

    consSta (Cdecl cl _ _ _ _) h theF = (H ns' es', theF') where
        (s, h'', theF') = ensureTe (TC cl) h theF
        (H ns' es', _) = ensureEdgeNS h'' s staLa
    
    consExt (Cdecl cl _ (Just te) _ _) h theF = (H ns' (es' +. E s isaLa t), theF') where
        (s, h'', theF'') = ensureTe (TC cl) h theF
        (t, H ns' es', theF') = ensureTe te h'' theF''
    consExt _ h theF = (h, theF)
    
    consTV (Cdecl cl (XSpec tv scnstr mcnstr:ys) ext adefs mdefs) h theF = 
            consTV (Cdecl cl ys ext adefs mdefs) h' theF' where
        
        s = getSta h (getTe (TC cl) theF)
        (t, ha, theFa) = ensureTe (TX tv) h theF
        (hb, _) = ensureEdgeNC ha (E s (LX tv) t)
        (hc, theFc) = consSupCnstr t scnstr hb theFa
        (h', theF') = walkMemCnstr mcnstr hc theFc
        
        consSupCnstr n (Just te) hx theFx = (hx', theFx') where
            (sc, hx'', theFx') = ensureTe te hx theFx
            (hx', _) = ensureEdgeNC hx'' (E n isaLa sc)
        consSupCnstr _ _ hx theFx = (hx, theFx)
            
        walkMemCnstr (Just te) hx theFx = (hx', theFx') where
            (_, hx', theFx') = ensureTe te hx theFx
        walkMemCnstr _ hx theFx = (hx, theFx)
    consTV _ h theF = (h, theF)

    consAttr (Cdecl cl xspec ext (Adef _ tp:ys) mdefs) h theF = consAttr (Cdecl cl xspec ext ys mdefs) h' theF' where
        s = getTe (TC cl) theF
        (h', theF') = ensureTyping h theF s tp
    consAttr _ h theF = (h, theF)
    
    consMeth (Cdecl cl xspec ext adefs (Mdef a _ _:ys)) h theF = consMeth (Cdecl cl xspec ext adefs ys) h' theF where
        s = getSta h (getTe (TC cl) theF)
        (h', _) = ensureEdgeNS h s (LA a)
    consMeth _ h theF = (h, theF)
    
    consPar (Cdecl cl xspec ext adefs (Mdef _ [] _:ys)) h theF = consPar (Cdecl cl xspec ext adefs ys) h theF 
    consPar (Cdecl cl xspec ext adefs (Mdef a (tp:zs) k:ys)) h theF = 
            consPar (Cdecl cl xspec ext adefs (Mdef a zs k:ys)) h' theF' where
        s = getStaTg h (getTe (TC cl) theF) (LA a)
        (h', theF') = ensureTyping h theF s tp
    consPar _ h theF = (h, theF)
    
    consIns h theF = 
            case find isRawCj theF of
                Just (TCj cl sst, j) -> cons0 cl sst j
                _                    -> (h, theF)
        where
        
        cons0 cl sst j = consIns h' theF' where
            u = getTe (TC cl) theF
            (h'', theF'') = insEdges h theF (getOutEdgesH h u) j
            ms = getOutEdgesH h'' (getSta h'' u)
            (h''', theF''') = insEdges h'' theF'' ms (getSta h'' j)
            (h', theF') = foldl (\(hx, theFx) (E _ la y) -> insEdges hx theFx (getOutEdgesH hx y) (getStaTg hx j la))
                                (h''', theF''') ms
             
            insEdges hx theFx (E _ la t:xs) s' =
                    case find (\(_, y) -> t == y) theF of
                        Just (x, _) -> let (t', hx'', theFx') = ensureTe (insTe x sst) hx theFx
                                           (hx', _) = ensureEdgeNC hx'' (E s' la t')
                                       in  insEdges hx' theFx' xs s' 
                        _           -> let (hx', _) = ensureEdgeNS hx s' la in insEdges hx' theFx xs s'  
            insEdges hx theFx _ _ = (hx, theFx)
    
        isRawCj (TCj _ _, n) = isNothing (findEdgeH h n staLa) 
        isRawCj _ = False
        
    consConj h theF = (foldl (\hx (tes, n) -> cons0 tes n hx) h [(tes, n) | (TCn tes, n) <- theF], theF) where
        cons0 tes n hx = hx' where
            Just (hx'', n') = conj hx [getTe te theF | te <- tes]
            hx' = shloTake hx'' n n'
            
    consMemCnstr (Cdecl cl (XSpec tv _ (Just te):ys) ext adefs mdefs) h theF = 
            consMemCnstr (Cdecl cl ys ext adefs mdefs) h' theF where
        n = getTe (TX tv) theF
        n' = getTe te theF
        h' = shloTake h n n'
    consMemCnstr (Cdecl cl (XSpec tv _ _:ys) ext adefs mdefs) (H ns es) theF = 
            consMemCnstr (Cdecl cl ys ext adefs mdefs) (H ns es') theF where
        n = getTe (TX tv) theF
        es' = es +. E n staLa emptySta
    consMemCnstr _ h theF = (h, theF)
    
    consPrimSta h theF = (foldl (\hx n -> cons0 hx n) h [NP INT, NP BOOL, NP TXT, NP NULL, NP WILD], theF) where
        cons0 (H ns es) n = H ns' es' where
            ns' = ns +. n
            es' = es +. E n staLa emptySta

--            
-- P construction
--

consP :: Program -> P
consP (Program cdecls (Mainm tps k)) = P (foldl cons0 [] cdecls) (tps, k) where
    cons0 ms (Cdecl cl _ _ _ mdefs) = foldl (\ms' (Mdef m _ k') -> (cl, m, k'):ms') ms mdefs

--
-- VisTab construction
--

consVisTab :: Program -> VisTab
consVisTab (Program cdecls _) = foldl cons0 [] cdecls where
    cons0 vs (Cdecl cl _ _ adefs _) = foldl (\vs' (Adef vis (Typing _ la)) -> (cl, la, vis):vs') vs adefs

--            
-- type checking
--

type NPart = ([N], [N], [N], [N], [N], [N], [N], [N], [N])

ssj :: H -> N -> [Ssti N]
ssj h j = [NX x :- t | E _ (LX x) t <- getOutEdgesH h (getSta h j)]

tvar :: H -> N -> [X_]
tvar h n = (findTgH h n staLa, []) ?>>= \s -> [tv | LX tv <- getOutLasH h s]

gecls :: H -> N -> Maybe N
gecls h@(H ns _) n@(NS _) =  (tvs /= []) &>> find (\n' -> setEq (tvar h n') tvs) ts where
    tvs = tvar h n
    ts = [n' | n'@(NC _) <- toList ns]
gecls _ _ = Nothing

--
-- well-formed type substitution
--

wfSst :: VisTab -> H -> Sst N -> ErrMsg () 
wfSst viss h sst = all wfSsti sst |? "bad type substitution: " ++ show sst where
    wfSsti (tv :- u) = clocoverH h' u j && pubover viss h' u j && supcoverH h' u j where (h', j) = insGe sst h tv

--
--
  
isInsGe :: H -> N -> N -> Sst N -> Bool
isInsGe h j n sst =  teqH h' j j' where (h', j') = insGe sst h n

--
-- well-formed type graph
--

wfTyH :: VisTab -> H -> ErrMsg NPart
wfTyH viss h@(H ns es) =
        do  isAcyclic [e | e@(E _ la _) <- el, la == isaLa] |? "cyclic is-a edges"
            wf0 nl [] [] [] [] [] [] [] [] [] where

    nl = toList ns
    el = toList es

    wf0 [] dts mfs stas gstas gcls cls tvs cns cjs =
            do 
                all (`elem` cls ++ cjs) [n | e@(E _ _ n) <- el, isNonTVIsa e] 
                    |? "bad class is-a targets" 
                all (`elem` cls ++ cjs ++ tvs) [n | e@(E _ _ n) <- el, isTVIsa e] 
                    |? "bad type var is-a targets"
                all (`notElem` gcls) [n | E _ _ n <- el] 
                    |? "using generic class as type"
                isDisjoint [tvar h ge | ge <- gcls] 
                    |? "type var shared by generic classes"
                return (dts, mfs, stas, gstas, gcls, cls, tvs, cns, cjs)
    wf0 (x:xs) dts mfs stas gstas gcls cls tvs cns cjs =
            let olasx = getOutLas es x in case x of
                NP _ -> 
                    do -- 1. primitive type
                        s <- findSta x 
                            |? "primitive without static table" 
                        getOutEdges es s == [] 
                            |? "static table not empty"
                        wf0 xs (x:dts) mfs stas gstas gcls cls tvs cns cjs
                NS _ -> 
                    case findSta x of
                        Nothing -> 
                            if allLAsToTys x && all isLA olasx && all1InLAs x then -- 2. method frame
                                wf0 xs dts (x:mfs) stas gstas gcls cls tvs cns cjs
                            else if allLAsNotToTys x && all1InStaLas x then -- 3/4. static table
                                if all isLA olasx then -- 3. non-generic static table
                                    wf0 xs dts mfs (x:stas) gstas gcls cls tvs cns cjs
                                else do -- 4. generic static table
                                    allLXsToTys x && all (\la -> isLA la || isLX la) olasx 
                                        |? "bad generic static table"  
                                    wf0 xs dts mfs stas (x:gstas) gcls cls tvs cns cjs
                            else fail "unexpected structural node"
                        Just s  -> let olass = getOutLas es s in
                            if allLAsNotToTys s && all isLA olass then -- 8. class conjunction
                                wf0 xs dts mfs stas gstas gcls cls tvs (x:cns) cjs
                            else do -- 9. class instantiation
                                any isLX olass 
                                    |? "class instantiation without type var"
                                let sst = ssj h x
                                wfSst viss h sst
                                any (\n -> isNC n && isInsGe h x n sst) nl 
                                    |? "bad class instantiation"
                                wf0 xs dts mfs stas gstas gcls cls tvs cns (x:cjs)
                NC _ ->
                    do -- 5/6. class
                        s <- findSta x |? "class without static table"
                        let olass = getOutLas es s 
                        allLAsToTys x && allLAsNotToTys s && all isClsLa olasx 
                            |? "bad target of class or static table" 
                        case all isLA olass of 
                            True ->    -- 6. non-generic class
                                wf0 xs dts mfs stas gstas gcls (x:cls) tvs cns cjs
                            _ -> 
                                do -- 5. generic class
                                    all isGeStaEdge (getOutEdges es s) 
                                        |? "bad generic static table"
                                    all (`elem` [tv | LX tv <- getOutLas es s]) 
                                        [tv | let G gns _ _ = gcH h x, NX tv <- toList gns]
                                        |? "type var not in generic static table"
                                    wf0 xs dts mfs stas gstas (x:gcls) cls tvs cns cjs
                NX _ ->
                    do -- 7. type variable
                        s <- findSta x 
                            |? "type variable without static table"  
                        allLAsNotToTys s && all isLA (getOutLas es s) 
                            |? "bad target of class or static table"
                        wf0 xs dts mfs stas gstas gcls cls (x:tvs) cns cjs
                _ -> fail "unexpected object, value or command node"
            ++# ": " ++ show x

    isAcyclic [] = True
    isAcyclic ds | exts == [] = False
                 | otherwise = isAcyclic ints where
        (ints, exts) = partition (\(E _ _ y) -> any (\(E x _ _) -> x == y) ds) ds

    findSta x = findTg es x staLa
    
    isGeStaEdge (E _ (LA _) _) = True
    isGeStaEdge (E _ (LX tv) (NX tv')) = tv == tv'
    isGeStaEdge _ = False
    
    isNonTVIsa (E (NX _) _ _) = False
    isNonTVIsa (E _ la _) = la == isaLa
       
    isTVIsa (E (NX _) la _) = la == isaLa
    isTVIsa _ = False
       
    isClsLa la = isLA la || la == staLa || la == isaLa
    
    allLAsToTys x = all (\(E _ la y) -> not (isLA la) || isJust (findSta y)) (getOutEdges es x)
    
    all1InLAs x = (\las -> all isLA las && las /= []) (getInLas es x)

    all1InStaLas x = (\las -> all (== staLa) las && las /= []) (getInLas es x)

    allLAsNotToTys x = all (\(E _ la y) -> not (isLA la) || isNothing (findSta y)) (getOutEdges es x)

    allLXsToTys x = all (\(E _ la y) -> not (isLX la) || isJust (findSta y)) (getOutEdges es x)
    
--
--

isTy :: Es -> N -> Bool
isTy es n = isJust (findEdge es n staLa)
        
isCc :: H -> N -> Bool
isCc h n = case n of NC _ -> tvar h n == []
                     NS _ -> tvar h n /= []
                     _    -> False

pairftotps :: ([La] -> [N] -> a) -> (N -> N) -> [Typing_] -> a
pairftotps pairf f tps = 
        let (ts, xs) = unzipTps_ tps
        in  pairf [LA x | x <- xs] [f(t) | t <- ts]

newScope :: Ns -> [La] -> [N] -> (N, [E])
newScope ns las ts = (r, el) where
    r = uniNO ns
    el = [E r la t | (la, t) <- zip las ts]

push :: G -> [La] -> [N] -> G
push (G ns es r) las ts =  G (ns +../ (r':ts)) (es +../ (E r' scpLa r:el)) r' where
    (r', el) = newScope ns las ts
  
popDirty :: G -> G
popDirty (G ns es r) = G ns es r' where Just r' = findTg es r scpLa  
  
pop :: G -> G
pop delta = gcGr (popDirty delta)  
  
pushTps :: (N -> N) -> G -> [Typing_] -> G
pushTps f g tps = pairftotps (push g) f tps
        
newDelta :: [La] -> [N] -> G
newDelta las ts = G (fromList (r:ts)) (fromList el) r where
    (r, el) = newScope empty las ts

newDeltaTps :: (N -> N) -> [Typing_] -> G
newDeltaTps f tps = pairftotps newDelta f tps

search :: G -> La -> Maybe E
search g la = prefixFindGr g scpLa la

searchTg :: G -> La -> Maybe N
searchTg g la = search g la >>= \(E _ _ n) -> return n

var :: G -> [La]
var g = [la | E _ la t <- getOutEdgesGr g, not (isNO t)]

height :: G -> Int
height (G _ es r) = height0 r where
    height0 n = (findTg es n scpLa, 0) ?>>= \n' -> 1 + height0 n'

--
-- subtyping of type nodes
--

subty :: VisTab -> H -> N -> N -> Bool
subty _ (H _ _) _ (NP WILD)  = True
subty _ (H _ es) (NP NULL) t | isU t && isTy es t = True where
    isU (NP INT) = False
    isU (NP BOOL) = False
    isU (NP TXT) = False
    isU _ = True
subty _ h t' t               | subclsH h t' t = True
subty viss h t' t@(NS _)     | tvar h t == [] && clocoverH h t' t && pubover viss h t' t = True 
subty _ _ _ _                = False

--
-- visibility of attributes
--

attrVis :: VisTab -> H -> N -> La -> ErrMsg Vis
attrVis viss h@(H _ es) t@(NC cl) la@(LA x) = 
        case find (\(cl', x', _) -> cl == cl' && x == x') viss of
            Just (_, _, vis) -> case findTg es t isaLa >>= \t' -> prefixFind es t' isaLa la >>= \_ -> return t' of
                Just t' -> do
                    vis' <- attrVis viss h t' la
                    vis >= vis' && vis' > Priv |? "inconsistent inherited visibility"
                    return vis
                _ -> return vis
            _ -> do 
                t' <- findTg es t isaLa |? "no visibility specification"
                vis' <- attrVis viss h t' la
                vis' > Priv |? "private inherited visibility"
                return vis'
attrVis viss h@(H _ es) t@(NS _) la = 
        do  _ <- findEdge es t la |? "attribute not found"
            case gecls h t of
                Just ge -> attrVis viss h ge la
                _ -> return Pub
attrVis _ (H _ es)  t@(NX _) la = 
        do  _ <- findEdge es t la |? "attribute not found"
            return Pub
attrVis _ _ _ _ = fail "visibility not derivable"

pubover :: VisTab -> H -> N -> N -> Bool
pubover viss h t' t = 
        case cloH h t of
            Just (G _ es r) -> all pub0 [la | la@(LA _) <- getOutLas es r]
            _               -> False
    where pub0 la = case attrVis viss h t' la of OK Pub -> True
                                                 _      -> False

sees :: G -> H -> N -> Vis -> Bool
sees delta h u Priv = (searchTg delta slfLa, False) ?>>= \u' -> teqH h u' u
sees delta h u Prot = (searchTg delta slfLa, False) ?>>= \u' -> subclsH h u u'
sees _ _ _ _        = True

--
-- type-checking of type expressions
--

tcTe :: VisTab -> H -> Te -> ErrMsg (H, N)
tcTe _ h (TP x) =
        return (h, NP x)
tcTe _ h te@(TC x) =
        do  let n = NC x
            containsH h n   |? "undefined class"
            tvar h n == []  |? "using generic class as type"
            return (h, n)
            ++# ": " ++ show te
tcTe _ h (TX x) =
        return (h, NX x)
tcTe viss h te@(TCn tes) =
        do  (h', ns) <- folde2 (tcTe viss) h tes 
            (h'', n) <- conj h' ns |? "bad conjunction" 
            return (h'', n)
            ++# ": " ++ show te
tcTe viss h te@(TCj cl sst) =
        do  let (tvs, tes) = unzipSst sst
                nvs        = [NX v | TX v <- tvs]
                u          = NC cl 
            containsH h u |? "undefined generic class"
            all isTX tvs && nvs `setEq` [NX v | v <- tvar h u] |? "bad type var list"
            (h', ns) <- folde2 (tcTe viss) h tes
            let sst' = zipSst nvs ns
            wfSst viss h' sst'
            return (reuseInsGe sst' h' u)
            ++# ": " ++ show te

tcCam :: VisTab -> H -> (N, Maybe Te) -> ErrMsg (H, Maybe N)
tcCam _ h (_, Nothing) = return (h, Nothing)
tcCam viss h (t, Just te') =
        do  isCe te' |? "cast not class expression"
            (h', t') <- tcTe viss h te'
            case subty viss h' t t' of
                True -> return (h, Nothing)
                _    -> do
                    subty viss h' t' t |? "cast not subtype related"
                    return (h', Just t')
            ++# ": " ++ show te'

--
-- type-checking of expressions
--

tcEp :: VisTab -> G -> H -> Ep -> ErrMsg (H, (Ep_, N))
tcEp _ _ h (Lit v@(VInt _)) =
        return (h, (Lit_ v, NP INT))
tcEp _ _ h (Lit v@(VBool _)) =
        return (h, (Lit_ v, NP BOOL))
tcEp _ _ h (Lit v@(VTxt _)) =  
        return (h, (Lit_ v, NP TXT))
tcEp _ _ h (Lit v@VNull) =  
        return (h, (Lit_ v, NP NULL))
tcEp _ _ _ Wild =
        fail "bad expression: _"
tcEp viss delta h ep@(App (Fun fn ptes rte) eps) = 
        do  (h', pns) <- folde2 (tcTe viss) h ptes
            (h'', rns) <- tcTe viss h' rte
            (h''', ps) <- folde2 (tcEp viss delta) h'' eps
            let (eps_, ens) = unzip ps
            length pns == length ens && all (\(pn, en) -> subty viss h''' en pn) (zip pns ens)
                |? "mismatched actual parameter: " ++ show ep
            return (h''', (App_ fn eps_, rns)) 
tcEp _ delta h Self =
        do  u <- searchTg delta slfLa 
                |? "variable not found: " ++ show Self
            return (h, (Self_, u))
tcEp _ delta h ep@(Var x) =
        do  t <- searchTg delta (LA x) 
                |? "variable not found: " ++ show ep
            return (h, (Var_ x, t))
tcEp viss delta h ep@(Attr ep' a) =
        do  (h', (ep_', u)) <- tcEp viss delta h ep'
            G _ es r <- cloH h' u 
                |? "unexpected member closure error: " ++ show u
            let la = LA a
            t <- findTg es r la 
                |? "attribute not found: " ++ show ep
            vis <- attrVis viss h' u la ++# ": " ++ show ep
            sees delta h' u vis 
                |? "attribute not visible: " ++ show ep 
            return (h', (Attr_ ep_' a, t))
tcEp viss delta h (Cast te ep') =
        do  isCe te |? "cast not class expression: " ++ show te
            (h', u) <- tcTe viss h te
            (h'', (ep_', u')) <- tcEp viss delta h' ep'
            case subty viss h'' u' u of
                True -> return (h'', (ep_', u'))
                _    -> do
                    subty viss h'' u u' |? "cast not subtype related: " ++ show (te, ep')
                    return (h'', (Cast_ u ep_', u))
                    
tcVe :: VisTab -> G -> H -> (N, Ep) -> ErrMsg (H, (Ep_, N))
tcVe viss delta h (t, Wild) = tcEp viss delta h (iniL t)
tcVe viss delta h (_, ep)   = tcEp viss delta h ep

tcRe :: VisTab -> G -> H -> Ep -> ErrMsg (H, (Ep_, N))
tcRe _ _ h Wild      = return (h, (Wild_, NP WILD))
tcRe viss delta h ep = tcEp viss delta h ep 

--
-- type-checking of commands
--
                            
tcLocalK :: VisTab -> G -> H-> Cmd -> ErrMsg ((H, G, Int), K_)
tcLocalK _ delta h Skip =
        return ((h, delta, height delta), Skip_)
tcLocalK viss delta h k@(Invk ep m vs xs cas rs) =
        do  (h1, (ep_, u)) <- tcEp viss delta h ep 

            oesm <- mfr (gcH h1 u) (LA m) 
                |? "method frame not found: " ++ show u 
            xps <- arrangeBy xs [(x', t'') | E _ (LA x') t'' <- oesm] 
                |? "mismatched parameter list: " ++ show xs 
            let (_, ts'') = unzip xps

            length vs == length ts'' 
                |? "mismatched value parameter list: " ++ show vs 
            (h2, vps) <- folde2 (tcVe viss delta) h1 (zip ts'' vs)
            let (vs_, ts) = unzip vps
            all (\(x, y) -> subty viss h2 x y) (zip ts ts'') 
                |? "mistyped value parameter list: " ++ show vs

            (h3, rps) <- folde2 (tcRe viss delta) h2 rs 
            let (rs_, ts') = unzip rps
            length ts' == length ts'' 
                |? "mismatched result parameter list: " ++ show rs 
            all (\(x, y) -> subty viss h3 x y) (zip ts'' ts') 
                |? "mistyped result parameter list: " ++ show rs

            (h4, cas_) <- folde2 (tcCam viss) h3 (zip ts'' cas)
            return ((h4, delta, height delta), Invk_ ep_ m vs_ xs cas_ rs_)
            
            ++# errCtx ("command: " ++ show k)
tcLocalK viss delta h k@(Assign lep ep) =
        do  isLE lep 
                |? "not l-expression: " ++ show lep
            (h', (lep_, t)) <- tcRe viss delta h lep
            (h'', (ep_, t')) <- tcVe viss delta h' (t, ep)
            subty viss h'' t' t 
                |? "mistyped assignment: " ++ show (lep, ep)
            return ((h'', delta, height delta), Assign_ lep_ ep_)
            
            ++# errCtx ("command: " ++ show k)
tcLocalK viss delta h k@(New te lep) =
        do  isLE lep 
                |? "not l-expression: " ++ show lep
            (h', u) <- tcTe viss h te
            isCc h' u 
                |? "not concrete class: " ++ show te
            (h'', (lep_, u')) <- tcEp viss delta h' lep
            subty viss h'' u u' 
                |? "mistyped new: " ++ show (te, lep)
            return ((h'', delta, height delta), New_ u lep_)
            
            ++# errCtx ("command: " ++ show k)
tcLocalK viss delta h k@(Decl tps) =
        do  let (tes, xs) = unzipTps tps
            (h', ts) <- folde2 (tcTe viss) h tes
            let rou    = height delta
                delta' = push delta [LA x | x <- xs] ts
            return ((h', delta', rou), Decl_ (zipTps_ ts xs))
            
            ++# errCtx ("command: " ++ show k)
tcLocalK _ delta h k@(End xs) =
        do  let rou = height delta
            rou > 0 
                |? "bottom of type context"
            let las = var delta
            all isLA las 
                |? "bad scope: " ++ show las
            setEq xs [y | LA y <- las] 
                |? "mismatched scope: " ++ show las
            return ((h, pop delta, rou - 1), End_ xs)
            
            ++# errCtx ("command: " ++ show k)
tcLocalK viss delta h (Seq k1 k2) =
        do  ((h', delta', rou1), k1') <- tcLocalK viss delta h k1
            ((h'', delta'', rou2), k2') <- tcLocalK viss delta' h' k2
            return ((h'', delta'', min rou1 rou2), Seq_ k1' k2')
tcLocalK viss delta h k@(If ep k1 k2) =
        do  (h1, (ep_, t)) <- tcEp viss delta h ep
            t == (NP BOOL) 
                |? "mistyped if-condition: " ++ show ep
                ++# errCtx ("command: " ++ showPartCmd k)
            (h2, k1') <- tcK viss delta h1 k1
            (h3, k2') <- tcK viss delta h2 k2
            return ((h3, delta, height delta), If_ ep_ k1' k2')
tcLocalK viss delta h k@(While ep k') =
        do  (h', (ep_, t)) <- tcEp viss delta h ep
            t == (NP BOOL) 
                |? "mistyped while-condition: " ++ show ep
                ++# errCtx ("command: " ++ showPartCmd k)
            (h'', k'') <- tcK viss delta h' k'
            return ((h'', delta, height delta), While_ ep_ k'')
tcLocalK viss delta h k@(Print eol eps) =
        do  (h', epps) <- folde2 (tcEp viss delta) h eps
            let (eps_, _) = unzip epps
            return ((h', delta, height delta), Print_ eol eps_)
            
            ++# errCtx ("command: " ++ show k)

tcK :: VisTab -> G -> H -> Cmd -> ErrMsg (H, K_)
tcK viss delta h k =
        do  ((h', delta', rou), k_) <- tcLocalK viss delta h k
            rou == height delta 
                |? "type context underbroken: " ++ show k
            delta == delta' 
                |? "type context not restored: " ++ show k
            return (h', k_)

tcMainCmd' :: FunTab -> VisTab -> G -> H -> Cmd -> ErrMsg (G, H, K_)
tcMainCmd' funs viss delta h c =
        do  k <- fixMainCmd' funs c
            ((h', delta', _), k') <- tcLocalK viss delta h k
            return (delta', h', k')

--
--

self :: H -> N -> (H, N)
self h n | tvar h n /= [] = shlo h n
         | otherwise      = (h, n)

--
-- type-checking of methods
--

tcMeth :: VisTab -> H -> (U_, A_, Cmd) -> ErrMsg (H, (U_, A_, K_))
tcMeth viss h (cl, m, k) =
        do  let (h', j) = self h (NC cl)
            oesm <- mfr (gcH h' j) (LA m) 
                |? "method frame not found: " ++ show j 
            let (las, ts) = unzip [(la, t) | E _ la t <- oesm]
            (h'', k_) <- tcK viss (newDelta (slfLa:las) (j:ts)) h' k
            return (h'', (cl, m, k_))
            
            ++# errCtx ("method: " ++ show (cl, m))     

--
-- type-checking of main method
--

tcMain :: VisTab -> H -> ([Typing], Cmd) -> ErrMsg (H, ([Typing_], K_))     
tcMain viss h (tps, k) =
        do  let (tes, xs) = unzipTps tps
            (h', ts) <- folde2 (tcTe viss) h tes
            (h'', k_) <- tcK viss (newDelta [LA x | x <- xs] ts) h' k
            return (h'', (zipTps_ ts xs, k_)) 
            
            ++# errCtx ("main method")     

--
-- type-checking of program
--

tcP :: VisTab -> H -> P -> ErrMsg (H, P_)
tcP viss h (P mds mmd) =
        do  (h', mds_) <- folde2 (tcMeth viss) h mds
            (h'', mmd_) <- tcMain viss h' mmd
            return (h'', P_ mds_ mmd_)
                     
tcPrg :: Program -> ErrMsg (H, P_, VisTab)
tcPrg prg =
        do  let h    = consTyH prg
                viss = consVisTab prg
            _ <- wfTyH viss h
            (h', p') <- tcP viss h (consP prg)
            return (h', p', viss)
             
tcPrg' :: Program' -> ErrMsg (H, P_, VisTab, FunTab)
tcPrg' prg' =
        do  (funs, prg) <- fixPrg' prg'
            (h, p, viss) <- tcPrg prg
            return (h, p, viss, funs)

consTyHPrg' :: Program' -> ErrMsg H
consTyHPrg' prg' =
        do  (_, prg) <- fixPrg' prg'
            return (consTyH prg)

--
-- end of Ty
--
-- --$Id: Ty.hs 1189 2012-11-14 05:57:21Z wke@IPM.EDU.MO $