module ISyntaxXRef(
                   updateIExprPosition,
                   updateITypePosition,
                   mapIExprPosition,
                   mapIExprPosition2,
                   mapIExprPositionConservative
                  ) where

import ISyntax
import Id
import Position(Position, noPosition, isUsefulPosition)

-- #############################################################################
-- #
-- #############################################################################

updateIExprPosition :: Position -> IExpr a -> IExpr a
updateIExprPosition pos (ILam i t e) = (ILam (setIdPosition pos i) t (updateIExprPosition pos e))
updateIExprPosition pos (IAps e ts [e0]) = (IAps (updateIExprPosition pos e) ts [(updateIExprPosition pos e0)])
updateIExprPosition pos (IAps e ts es) = (IAps (updateIExprPosition pos e) ts es)
updateIExprPosition pos (IVar i) = (IVar (setIdPosition pos i))
updateIExprPosition pos (ILAM i kind e) = (ILAM (setIdPosition pos i) kind (updateIExprPosition pos e))
updateIExprPosition pos iexpr@(ICon i (ICStateVar t isv)) = iexpr
updateIExprPosition pos (ICon i info) = (ICon (setIdPosition pos i) info)
updateIExprPosition pos (IRefT t p r) = (IRefT (updateITypePosition pos t) p r)


updateITypePosition :: Position -> IType -> IType
updateITypePosition pos (ITForAll i kind t) = (ITForAll (setIdPosition pos i) kind t)
updateITypePosition pos (ITAp t t') = (ITAp (updateITypePosition pos t) (updateITypePosition pos t'))
updateITypePosition pos (ITVar i) = (ITVar (setIdPosition pos i))
updateITypePosition pos (ITCon i kind sort) = (ITCon (setIdPosition pos i) kind sort)
updateITypePosition pos t@(ITNum _) = t
updateITypePosition pos t@(ITStr _) = t


updateIExprPosition2 :: Position -> IExpr a -> IExpr a
updateIExprPosition2 pos (ILam i t e) = (ILam (setIdPosition pos i) t (updateIExprPosition pos e))
updateIExprPosition2 pos iexpr@(IAps e@(ICon i (ICCon _ _)) ts [e0]) =
    if (not (isUsefulPosition (getIdPosition i)))
    then updateIExprPosition pos iexpr
    else iexpr
updateIExprPosition2 pos iexpr@(IAps e@(ICon i (ICPrim _ _)) ts es) =
    if (not (isUsefulPosition (getIdPosition i)))
    then updateIExprPosition pos iexpr
    else iexpr
updateIExprPosition2 pos (IAps e ts [e0]) = (IAps (updateIExprPosition pos e) ts [(updateIExprPosition pos e0)])
updateIExprPosition2 pos (IAps e ts es) = (IAps (updateIExprPosition pos e) ts es)
updateIExprPosition2 pos (IVar i) = (IVar (setIdPosition pos i))
updateIExprPosition2 pos (ILAM i kind e) = (ILAM (setIdPosition pos i) kind (updateIExprPosition pos e))
updateIExprPosition2 pos iexpr@(ICon i (ICStateVar t isv)) = iexpr
updateIExprPosition2 pos (ICon i info) = (ICon (setIdPosition pos i) info)
updateIExprPosition2 pos (IRefT t p r) = (IRefT (updateITypePosition pos t) p r)


mapIExprPosition :: Bool -> (IExpr a, IExpr a) -> IExpr a
mapIExprPosition False (expr_0, expr_1) = expr_1
mapIExprPosition True (expr_0, expr_1) =
    let positionModel = (getIExprPositionCross expr_0)
    in if (positionModel == noPosition) || (not (isUsefulPosition positionModel))
       then expr_1
       else let positionCurrent = (getIExprPositionCross expr_1)
            in if (positionModel == positionCurrent)
               then expr_1
               else if (isEquivIExprIncluded expr_1 expr_0)
                    then let pos = (getIExprPositionCross (head (extractEquivIExpr expr_1 expr_0)))
                             expr = (updateIExprPosition pos expr_1)
                         in expr
                    else (updateIExprPosition positionModel expr_1)

mapIExprPosition2 :: Bool -> (IExpr a, IExpr a) -> IExpr a
mapIExprPosition2 False (expr_0, expr_1) = expr_1
mapIExprPosition2 True (expr_0, expr_1) =
    let positionModel = (getIExprPositionCross expr_0)
    in if (positionModel == noPosition) || (not (isUsefulPosition positionModel))
       then expr_1
       else let positionCurrent = (getIExprPositionCross expr_1)
            in if (positionModel == positionCurrent)
               then expr_1
               else if (isEquivIExprIncluded expr_1 expr_0)
                    then let pos = (getIExprPositionCross (head (extractEquivIExpr expr_1 expr_0)))
                             expr = (updateIExprPosition2 pos expr_1)
                         in expr
                    else (updateIExprPosition2 positionModel expr_1)

mapIExprPositionConservative :: Bool -> (IExpr a,IExpr a) -> IExpr a
mapIExprPositionConservative False (expr_0, expr_1) = expr_1
mapIExprPositionConservative True (expr_0, expr_1) =
    let positionModel = (getIExprPositionCross expr_0)
    in if (positionModel == noPosition) || (not (isUsefulPosition positionModel))
       then expr_1
       else let positionCurrent = (getIExprPositionCross expr_1)
            in if (positionModel == positionCurrent) || (isUsefulPosition positionCurrent)
               then expr_1
               else if (isEquivIExprIncluded expr_1 expr_0)
                    then let pos = (getIExprPositionCross (head (extractEquivIExpr expr_1 expr_0)))
                             expr = (updateIExprPosition pos expr_1)
                         in expr
                    else (updateIExprPosition positionModel expr_1)

-- #############################################################################
-- #
-- #############################################################################

isEquivIExprIncluded :: IExpr a -> IExpr a -> Bool
isEquivIExprIncluded sub_expr expr@(ILam i t e) =
    ((equivIExprs expr sub_expr) || (isEquivIExprIncluded sub_expr e))
isEquivIExprIncluded sub_expr expr@(IAps e ts es) =
    ((equivIExprs expr sub_expr) || (or (map (equivIExprs sub_expr) es)))
isEquivIExprIncluded sub_expr expr@(IVar _) =
    (equivIExprs expr sub_expr)
isEquivIExprIncluded sub_expr expr@(ILAM i kind e) =
    ((equivIExprs expr sub_expr) || (isEquivIExprIncluded sub_expr e))
isEquivIExprIncluded sub_expr expr@(ICon _ _) =
    (equivIExprs expr sub_expr)
isEquivIExprIncluded sub_expr expr@(IRefT t p r) =
    (equivIExprs expr sub_expr)

-- #############################################################################
-- #
-- #############################################################################

extractEquivIExpr :: IExpr a -> IExpr a -> [IExpr a]
extractEquivIExpr sub_expr expr@(ILam i t e) = if (equivIExprs sub_expr expr)
                                               then [expr]
                                               else (extractEquivIExpr sub_expr e)

extractEquivIExpr sub_expr expr@(IAps e ts es) = if (equivIExprs sub_expr expr)
                                                 then [expr]
                                                 else (concatMap (extractEquivIExpr sub_expr) es)

extractEquivIExpr sub_expr expr@(IVar _) =  if (equivIExprs sub_expr expr)
                                            then [expr]
                                            else []

extractEquivIExpr sub_expr expr@(ILAM i kind e) =  if (equivIExprs sub_expr expr)
                                                   then [expr]
                                                   else (extractEquivIExpr sub_expr e)

extractEquivIExpr sub_expr expr@(ICon _ _) =  if (equivIExprs sub_expr expr)
                                              then [expr]
                                              else []

extractEquivIExpr sub_expr expr@(IRefT t p r) =  if (equivIExprs sub_expr expr)
                                                 then [expr]
                                                 else []

-- #############################################################################
-- #
-- #############################################################################

equivIExprs :: IExpr a -> IExpr a -> Bool
equivIExprs e0@(ILam i0 t0 ee0) e1@(ILam i1 t1 ee1) = ((equivId i0 i1) && (t0 == t1) && (ee0 == ee1))
equivIExprs e0@(IAps ee0 ts0 es0) e1@(IAps ee1 ts1 es1) = ((equivIExprs ee0 ee1) && (ts0 == ts1) && (es0 == es1))
equivIExprs e0@(IVar i0) e1@(IVar i1) = (equivId i0 i1)
equivIExprs e0@(ILAM i0 k0 ee0) e1@(ILAM i1 k1 ee1) = ((equivId i0 i1) && (k0 == k1) && (ee0 == ee1))
equivIExprs e0@(ICon i0 info0) e1@(ICon i1 info1) = ((equivId i0 i1) && (info0 == info1))
equivIExprs e0@(IRefT t0 p0 r0) e1@(IRefT t1 p1 r1) = (p0 == p1)
equivIExprs e0 e1 = False

equivId :: Id -> Id -> Bool
equivId id0 id1 = (id0 == id1) && (getIdProps id0 == getIdProps id1)

-- #############################################################################
-- #
-- #############################################################################