clafer-0.3.5: src/Language/Clafer/Intermediate/SimpleScopeAnalyzer.hs
{-
Copyright (C) 2012-2014 Jimmy Liang, Kacper Bak <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 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 lower bounds.
-- If the model only has Clafers (ie. no constraints) then the lower bound is tight.
-- scopeAnalysis :: IModule -> Map IClafer Integer
simpleScopeAnalysis :: IModule -> [(String, Integer)]
simpleScopeAnalysis IModule{mDecls = decls'} =
[(a, b) | (a, b) <- finalAnalysis, isReferenceOrSuper a, b /= 0]
where
finalAnalysis = Map.toList $ foldl analyzeComponent supersAnalysis connectedComponents
isReferenceOrSuper uid' =
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'
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
lowCard clafer =
max low constraintLow
where
low = fst $ fromJust $ card clafer
constraintLow = 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 reference analysis and this analysis
Map.insertWith max (uid clafer) scope analysis
where
scope
| isAbstract clafer = sum subclaferScopes
| otherwise = parentScope * lowCard clafer
subclaferScopes = map (findOrError " subclafer scope not found" analysis) $ filter isConcrete' subclafers
parentScope =
case parent' of
Just parent'' -> findOrError " parent scope not found" analysis parent''
Nothing -> rootScope
subclafers = Map.findWithDefault [] (uid clafer) subclaferMap
parent' = 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
lowerBound = max 1 $ fst (fromJust $ card clafer)
analysis' = case (directSuper clafers clafer) of
(Just c) -> Map.alter ((if isReference clafer then maxLB else incLB) lowerBound) (uid c) analysis
Nothing -> analysis
incLB lb' Nothing = Just lb'
incLB lb' (Just lb) = Just (lb + lb')
maxLB lb' Nothing = Just lb'
maxLB lb' (Just lb) = Just (max lb lb')
analyzeSupers _ 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 =
mapMaybe asClafer (elements clafer)
where
asClafer (IEClafer claf) = Just claf
asClafer _ = Nothing
-- 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"