{-
 Copyright (C) 2012-2014 Jimmy Liang, Kacper Bak, Michał Antkiewicz <http://gsd.uwaterloo.ca>

 Permission is hereby granted, free of charge, to any person obtaining a copy of
 this software and associated documentation files (the "Software"), to deal in
 the Software without restriction, including without limitation the rights to
 use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 of the Software, and to permit persons to whom the Software is furnished to do
 so, subject to the following conditions:

 The above copyright notice and this permission notice shall be included in all
 copies or substantial portions of the Software.

 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
-}
module Language.Clafer.Intermediate.SimpleScopeAnalyzer (simpleScopeAnalysis) where

import Language.Clafer.Common
import Control.Lens hiding (elements, assign)
import Data.Graph
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Ord
import Data.Ratio
import Language.Clafer.Intermediate.Intclafer
import Prelude hiding (exp)


isReference :: IClafer -> Bool
isReference = _isOverlapping . _super
isConcrete :: IClafer -> Bool
isConcrete = not . isReference
isSuperest :: [IClafer] -> IClafer -> Bool
isSuperest clafers clafer = isNothing $ directSuper clafers clafer


-- | Collects the global cardinality and hierarchy information into proper, not necessarily lower, bounds.
simpleScopeAnalysis :: IModule -> [(String, Integer)]
simpleScopeAnalysis IModule{_mDecls = decls'} =
    [(a, b) | (a, b) <- finalAnalysis, isReferenceOrSuper a, b /= 1]
    where
    finalAnalysis = Map.toList $ foldl analyzeComponent supersAndRefsAnalysis connectedComponents
    
    isReferenceOrSuper uid' =
        isConcrete clafer || isReference clafer || isSuperest clafers clafer
        where
        clafer = findClafer uid'
        
    isConcrete' uid' = isConcrete $ findClafer uid'
    
    upperCards u =
        Map.findWithDefault (error $ "No upper cardinality for clafer named \"" ++ u ++ "\".") u upperCardsMap
    upperCardsMap = Map.fromList [(_uid c, snd $ fromJust $ _card c) | c <- clafers]
    
    supersAnalysis = foldl (analyzeSupers clafers) Map.empty decls'
    supersAndRefsAnalysis = foldl (analyzeRefs clafers) supersAnalysis decls'
    constraintAnalysis = analyzeConstraints constraints upperCards
    (subclaferMap, parentMap) = analyzeHierarchy clafers
    connectedComponents = analyzeDependencies clafers
    clafers = concatMap findClafers decls'
    constraints = concatMap findConstraints decls'
    findClafer uid' = fromJust $ find (isEqClaferId uid') clafers
    
    lowerOrUpperFixedCard analysis' clafer =
        maximum [cardLb, cardUb, lowFromConstraints, oneForStar, targetScopeForStar ]
        where
        Just (cardLb, cardUb) = _card clafer
        oneForStar = if (cardLb == 0 && cardUb == -1) then 1 else 0
        targetScopeForStar = if (isReference clafer && cardUb == -1) 
            then case (directSuper clafers clafer) of
                    (Just targetClafer) -> Map.findWithDefault 0 (_uid targetClafer) analysis'
                    Nothing -> 0
            else 0
        lowFromConstraints = Map.findWithDefault 0 (_uid clafer) constraintAnalysis
    
    analyzeComponent analysis' component =
        case flattenSCC component of
            [uid'] -> analyzeSingleton uid' analysis'
            uids  ->
                foldr analyzeSingleton assume uids
                where
                -- assume that each of the scopes in the component is 1 while solving
                assume = foldr (`Map.insert` 1) analysis' uids
        where
        analyzeSingleton uid' analysis'' = analyze analysis'' $ findClafer uid'
    
    analyze :: Map String Integer -> IClafer -> Map String Integer
    analyze analysis' clafer =
        -- Take the max between the supers and references analysis and this analysis
        Map.insertWith max (_uid clafer) scope analysis'
        where
        scope
            | _isAbstract clafer  = sum subclaferScopes
            | otherwise          = parentScope * (lowerOrUpperFixedCard analysis' clafer)
        
        subclaferScopes = map (findOrError " subclafer scope not found" analysis') $ filter isConcrete' subclafers
        parentScope  =
            case parentMaybe of
                Just parent'' -> findOrError " parent scope not found" analysis' parent''
                Nothing      -> rootScope
        subclafers = Map.findWithDefault [] (_uid clafer) subclaferMap
        parentMaybe = Map.lookup (_uid clafer) parentMap
        rootScope = 1
        findOrError message m key = Map.findWithDefault (error $ key ++ message) key m
        
analyzeSupers :: [IClafer] -> Map String Integer -> IElement -> Map String Integer    
analyzeSupers clafers analysis (IEClafer clafer) =
    foldl (analyzeSupers clafers) analysis' (_elements clafer)
    where
    (Just (cardLb, cardUb)) = _card clafer
    lowerOrFixedUpperBound = maximum [1, cardLb, cardUb ]
    analysis' = if (isReference clafer) 
                then analysis
                else case (directSuper clafers clafer) of
                  (Just c) -> Map.alter (incLB lowerOrFixedUpperBound) (_uid c) analysis
                  Nothing -> analysis                     
    incLB lb' Nothing = Just lb'
    incLB lb' (Just lb) = Just (lb + lb')
analyzeSupers _ analysis _ = analysis

analyzeRefs :: [IClafer] -> Map String Integer -> IElement -> Map String Integer    
analyzeRefs clafers analysis (IEClafer clafer) =
    foldl (analyzeRefs clafers) analysis' (_elements clafer)
    where
    (Just (cardLb, cardUb)) = _card clafer
    lowerOrFixedUpperBound = maximum [1, cardLb, cardUb]
    analysis' = if (isReference clafer) 
                then case (directSuper clafers clafer) of
                    (Just c) -> Map.alter (maxLB lowerOrFixedUpperBound) (_uid c) analysis
                    Nothing -> analysis
                else analysis                     
    maxLB lb' Nothing = Just lb'
    maxLB lb' (Just lb) = Just (max lb lb')
analyzeRefs _ analysis _ = analysis

analyzeConstraints :: [PExp] -> (String -> Integer) -> Map String Integer
analyzeConstraints constraints upperCards =
    foldr analyzeConstraint Map.empty $ filter isOneOrSomeConstraint constraints
    where
    isOneOrSomeConstraint PExp{_exp = IDeclPExp{_quant = quant'}} =
        -- Only these two quantifiers requires an increase in scope to satisfy.
        case quant' of
            IOne -> True
            ISome -> True
            _     -> False
    isOneOrSomeConstraint _ = False
    
    -- Only considers how quantifiers affect scope. Other types of constraints are not considered.
    -- Constraints of the type [some path1.path2] or [no path1.path2], etc.
    analyzeConstraint PExp{_exp = IDeclPExp{_oDecls = [], _bpexp = bpexp'}} analysis =
        foldr atLeastOne analysis path'
        where
        path' = dropThisAndParent $ unfoldJoins bpexp'
        atLeastOne = Map.insertWith max `flip` 1
        
    -- Constraints of the type [all disj a : path1.path2] or [some b : path3.path4], etc.
    analyzeConstraint PExp{_exp = IDeclPExp{_oDecls = decls'}} analysis =
        foldr analyzeDecl analysis decls'
    analyzeConstraint _ analysis = analysis

    analyzeDecl IDecl{_isDisj = isDisj', _decls = decls', _body = body'} analysis =
        foldr (uncurry insert') analysis $ zip path' scores
        where
        -- Take the first element in the path', and change its effective lower cardinality.
        -- Can overestimate the scope.
        path' = dropThisAndParent $ unfoldJoins body'
        -- "disj a;b;c" implies at least 3 whereas "a;b;c" implies at least one.
        minScope = if isDisj' then fromIntegral $ length decls' else 1
        insert' = Map.insertWith max
        
        scores = assign path' minScope
        
        {-
         - abstract Z
         -   C *
         -     D : integer *
         -
         - A : Z
         -   B : integer
         -   [some disj a;b;c;d : D | a = 1 && b = 2 && c = 3 && d = B]
         -}
         -- Need at least 4 D's per A.
         -- Either
         -- a) Make the effective lower cardinality of C=4 and D=1
         -- b) Make the effective lower cardinality of C=1 and D=4
         -- c) Some other combination.
         -- Choose b, a greedy algorithm that starts from the lowest child progressing upwards.
         
        {-
         - abstract Z
         -   C *
         -     D : integer 3..*
         -
         - A : Z
         -   B : integer
         -   [some disj a;b;c;d : D | a = 1 && b = 2 && c = 3 && d = B]
         -}
         -- The algorithm we do is greedy so it will chose D=3.
         -- However, it still needs more D's so it will choose C=2
         -- C=2, D=3
         -- This might not be optimum since now the scope allows for 6 D's.
         -- A better solution might be C=2, D=2.
         -- Well too bad, we are using the greedy algorithm.
    assign [] _ = [1]
    assign (p : ps) score =
        pScore : ps'
        where
        --upper = upperCards p
        ps' = assign ps score
        psScore = product $ ps'
        pDesireScore = ceiling (score % psScore)
        pMaxScore = upperCards p
        pScore = min' pDesireScore pMaxScore
        
    min' a b = if b == -1 then a else min a b
        
    -- The each child has at most one parent. No matter what the path in a quantifier
    -- looks like, we ignore the parent parts.
    dropThisAndParent = dropWhile (== "parent") . dropWhile (== "this")


analyzeDependencies :: [IClafer] -> [SCC String]
analyzeDependencies clafers = connComponents
    where
    connComponents  = stronglyConnComp [(key, key, depends) | (key, depends) <- dependencyGraph]
    dependencies    = concatMap (dependency clafers) clafers
    dependencyGraph = Map.toList $ Map.fromListWith (++) [(a, [b]) | (a, b) <- dependencies]

dependency :: [IClafer] -> IClafer -> [(String, String)]
dependency clafers clafer =
    selfDependency : (maybeToList superDependency ++ childDependencies)
    where
     -- This is to make the "stronglyConnComp" from Data.Graph play nice. Otherwise,
     -- clafers with no dependencies will not appear in the result.
    selfDependency = (_uid clafer, _uid clafer)
    superDependency
        | isReference clafer = Nothing
        | otherwise =
            do
                super' <- directSuper clafers clafer
                -- Need to analyze clafer before its super
                return (_uid super', _uid clafer)
    -- Need to analyze clafer before its children
    childDependencies = [(_uid child, _uid clafer) | child <- childClafers clafer]
        

analyzeHierarchy :: [IClafer] -> (Map String [String], Map String String)
analyzeHierarchy clafers =
    foldl hierarchy (Map.empty, Map.empty) clafers
    where
    hierarchy (subclaferMap, parentMap) clafer = (subclaferMap', parentMap')
        where
            subclaferMap' = 
                case super' of
                    Just super'' -> Map.insertWith (++) (_uid super'') [_uid clafer] subclaferMap
                    Nothing     -> subclaferMap
            super' = directSuper clafers clafer
            parentMap' = foldr (flip Map.insert $ _uid clafer) parentMap (map _uid $ childClafers clafer)
    
directSuper :: [IClafer] -> IClafer -> Maybe IClafer
directSuper clafers clafer =
    second $ findHierarchy getSuper clafers clafer
    where
    second [] = Nothing
    second [_] = Nothing
    second (_:x:_) = Just x
    

-- Finds all ancestors
findClafers :: IElement -> [IClafer]
findClafers (IEClafer clafer) = clafer : concatMap findClafers (_elements clafer)
findClafers _ = []


-- Find all constraints
findConstraints :: IElement -> [PExp]
findConstraints IEConstraint{_cpexp = c} = [c]
findConstraints (IEClafer clafer) = concatMap findConstraints (_elements clafer)
findConstraints _ = []

-- Finds all the direct ancestors (ie. children)
childClafers :: IClafer -> [IClafer]
childClafers clafer = clafer ^.. elements.traversed.iClafer
    
-- Unfold joins
-- If the expression is a tree of only joins, then this function will flatten
-- the joins into a list.
-- Otherwise, returns an empty list.
unfoldJoins :: PExp -> [String]
unfoldJoins pexp =
    fromMaybe [] $ unfoldJoins' pexp
    where
    unfoldJoins' PExp{_exp = (IFunExp "." args)} =
        return $ args >>= unfoldJoins
    unfoldJoins' PExp{_exp = IClaferId{_sident = sident'}} =
        return $ [sident']
    unfoldJoins' _ =
        fail "not a join"