1 2{- | Construct a graph from constraints 3@ 4 x + n <= y becomes x ---(-n)---> y 5 x <= n + y becomes x ---(+n)---> y 6@ 7the default edge (= no edge) is labelled with infinity. 8 9Building the graph involves keeping track of the node names. 10We do this in a finite map, assigning consecutive numbers to nodes. 11-} 12module Agda.Utils.Warshall where 13 14import Control.Monad.State 15 16import Data.Maybe 17import Data.Array 18import qualified Data.List as List 19import Data.Map (Map) 20import qualified Data.Map as Map 21 22import Agda.Utils.SemiRing 23import Agda.Utils.List (nubOn) 24import Agda.Utils.Pretty as P 25 26type Matrix a = Array (Int,Int) a 27 28-- assuming a square matrix 29warshall :: SemiRing a => Matrix a -> Matrix a 30warshall a0 = loop r a0 where 31 b@((r,c),(r',c')) = bounds a0 -- assuming r == c and r' == c' 32 loop k a | k <= r' = 33 loop (k+1) (array b [ ((i,j), 34 (a!(i,j)) `oplus` ((a!(i,k)) `otimes` (a!(k,j)))) 35 | i <- [r..r'], j <- [c..c'] ]) 36 | otherwise = a 37 38type AdjList node edge = Map node [(node, edge)] 39 40-- | Warshall's algorithm on a graph represented as an adjacency list. 41warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edge 42warshallG g = fromMatrix $ warshall m 43 where 44 nodes = zip (nubOn id $ Map.keys g ++ map fst (concat $ Map.elems g)) 45 [0..] 46 len = length nodes 47 b = ((0,0), (len - 1,len - 1)) 48 49 edge i j = do 50 es <- Map.lookup i g 51 foldr oplus Nothing [ Just v | (j', v) <- es, j == j' ] 52 53 m = array b [ ((n, m), edge i j) | (i, n) <- nodes, (j, m) <- nodes ] 54 55 fromMatrix matrix = Map.fromList $ do 56 (i, n) <- nodes 57 let es = [ (fst (nodes !! m), e) 58 | m <- [0..len - 1] 59 , Just e <- [matrix ! (n, m)] 60 ] 61 return (i, es) 62 63-- | Edge weight in the graph, forming a semi ring. 64data Weight 65 = Finite Int 66 | Infinite 67 deriving (Eq, Show) 68 69inc :: Weight -> Int -> Weight 70inc Infinite n = Infinite 71inc (Finite k) n = Finite (k + n) 72 73instance Pretty Weight where 74 pretty (Finite i) = pretty i 75 pretty Infinite = "." 76 77instance Ord Weight where 78 a <= Infinite = True 79 Infinite <= b = False 80 Finite a <= Finite b = a <= b 81 82instance SemiRing Weight where 83 ozero = Infinite 84 oone = Finite 0 85 86 oplus = min 87 88 otimes Infinite _ = Infinite 89 otimes _ Infinite = Infinite 90 otimes (Finite a) (Finite b) = Finite (a + b) 91 92-- constraints --------------------------------------------------- 93 94-- | Nodes of the graph are either 95-- - flexible variables (with identifiers drawn from @Int@), 96-- - rigid variables (also identified by @Int@s), or 97-- - constants (like 0, infinity, or anything between). 98 99data Node = Rigid Rigid 100 | Flex FlexId 101 deriving (Eq, Ord) 102 103data Rigid = RConst Weight 104 | RVar RigidId 105 deriving (Eq, Ord) 106 107type NodeId = Int 108type RigidId = Int 109type FlexId = Int 110type Scope = RigidId -> Bool 111-- ^ Which rigid variables a flex may be instatiated to. 112 113instance Pretty Node where 114 pretty (Flex i) = "?" P.<> pretty i 115 pretty (Rigid (RVar i)) = "v" P.<> pretty i 116 pretty (Rigid (RConst Infinite)) = "#" 117 pretty (Rigid (RConst (Finite n))) = pretty n 118 119infinite :: Rigid -> Bool 120infinite (RConst Infinite) = True 121infinite _ = False 122 123-- | @isBelow r w r'@ 124-- checks, if @r@ and @r'@ are connected by @w@ (meaning @w@ not infinite), 125-- whether @r + w <= r'@. 126-- Precondition: not the same rigid variable. 127isBelow :: Rigid -> Weight -> Rigid -> Bool 128isBelow _ Infinite _ = True 129isBelow _ n (RConst Infinite) = True 130isBelow (RConst (Finite i)) (Finite n) (RConst (Finite j)) = i + n <= j 131isBelow _ _ _ = False -- rigid variables are not related 132 133-- | A constraint is an edge in the graph. 134data Constraint 135 = NewFlex FlexId Scope 136 | Arc Node Int Node 137 -- ^ For @Arc v1 k v2@ at least one of @v1@ or @v2@ is a @MetaV@ (Flex), 138 -- the other a @MetaV@ or a @Var@ (Rigid). 139 -- If @k <= 0@ this means @suc^(-k) v1 <= v2@ 140 -- otherwise @v1 <= suc^k v3@. 141 142instance Pretty Constraint where 143 pretty (NewFlex i s) = hcat [ "SizeMeta(?", pretty i, ")" ] 144 pretty (Arc v1 k v2) 145 | k == 0 = hcat [ pretty v1, "<=", pretty v2 ] 146 | k < 0 = hcat [ pretty v1, "+", pretty (-k), "<=", pretty v2 ] 147 | otherwise = hcat [ pretty v1, "<=", pretty v2, "+", pretty k ] 148 149type Constraints = [Constraint] 150 151emptyConstraints :: Constraints 152emptyConstraints = [] 153 154-- graph (matrix) ------------------------------------------------ 155 156data Graph = Graph 157 { flexScope :: Map FlexId Scope -- ^ Scope for each flexible var. 158 , nodeMap :: Map Node NodeId -- ^ Node labels to node numbers. 159 , intMap :: Map NodeId Node -- ^ Node numbers to node labels. 160 , nextNode :: NodeId -- ^ Number of nodes @n@. 161 , graph :: NodeId -> NodeId -> Weight -- ^ The edges (restrict to @[0..n[@). 162 } 163 164-- | The empty graph: no nodes, edges are all undefined (infinity weight). 165initGraph :: Graph 166initGraph = Graph Map.empty Map.empty Map.empty 0 (\ x y -> Infinite) 167 168-- | The Graph Monad, for constructing a graph iteratively. 169type GM = State Graph 170 171-- | Add a size meta node. 172addFlex :: FlexId -> Scope -> GM () 173addFlex x scope = do 174 modify $ \ st -> st { flexScope = Map.insert x scope (flexScope st) } 175 _ <- addNode (Flex x) 176 return () 177 178-- | Lookup identifier of a node. 179-- If not present, it is added first. 180addNode :: Node -> GM Int 181addNode n = do 182 st <- get 183 case Map.lookup n (nodeMap st) of 184 Just i -> return i 185 Nothing -> do 186 let i = nextNode st 187 put $ st { nodeMap = Map.insert n i (nodeMap st) 188 , intMap = Map.insert i n (intMap st) 189 , nextNode = i + 1 190 } 191 return i 192 193-- | @addEdge n1 k n2@ 194-- improves the weight of egde @n1->n2@ to be at most @k@. 195-- Also adds nodes if not yet present. 196addEdge :: Node -> Int -> Node -> GM () 197addEdge n1 k n2 = do 198 i1 <- addNode n1 199 i2 <- addNode n2 200 st <- get 201 let graph' x y = if (x,y) == (i1,i2) then Finite k `oplus` graph st x y 202 else graph st x y 203 put $ st { graph = graph' } 204 205addConstraint :: Constraint -> GM () 206addConstraint (NewFlex x scope) = addFlex x scope 207addConstraint (Arc n1 k n2) = addEdge n1 k n2 208 209buildGraph :: Constraints -> Graph 210buildGraph cs = execState (mapM_ addConstraint cs) initGraph 211 212mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight 213mkMatrix n g = array ((0,0),(n-1,n-1)) 214 [ ((i,j), g i j) | i <- [0..n-1], j <- [0..n-1]] 215 216-- displaying matrices with row and column labels -------------------- 217 218-- | A matrix with row descriptions in @b@ and column descriptions in @c@. 219data LegendMatrix a b c = LegendMatrix 220 { matrix :: Matrix a 221 , rowdescr :: Int -> b 222 , coldescr :: Int -> c 223 } 224 225instance (Pretty a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) where 226 pretty (LegendMatrix m rd cd) = 227 -- first show column description 228 let ((r,c),(r',c')) = bounds m 229 in foldr (\ j s -> "\t" P.<> pretty (cd j) P.<> s) "" [c .. c'] P.<> 230 -- then output rows 231 foldr (\ i s -> "\n" P.<> pretty (rd i) P.<> 232 foldr (\ j t -> "\t" P.<> pretty (m!(i,j)) P.<> t) 233 s 234 [c .. c']) 235 "" [r .. r'] 236 237-- solving the constraints ------------------------------------------- 238 239-- | A solution assigns to each flexible variable a size expression 240-- which is either a constant or a @v + n@ for a rigid variable @v@. 241type Solution = Map Int SizeExpr 242 243emptySolution :: Solution 244emptySolution = Map.empty 245 246extendSolution :: Solution -> Int -> SizeExpr -> Solution 247extendSolution subst k v = Map.insert k v subst 248 249data SizeExpr = SizeVar RigidId Int -- ^ e.g. x + 5 250 | SizeConst Weight -- ^ a number or infinity 251 252instance Pretty SizeExpr where 253 pretty (SizeVar n 0) = pretty (Rigid (RVar n)) 254 pretty (SizeVar n k) = pretty (Rigid (RVar n)) P.<> "+" P.<> pretty k 255 pretty (SizeConst w) = pretty w 256 257-- | @sizeRigid r n@ returns the size expression corresponding to @r + n@ 258sizeRigid :: Rigid -> Int -> SizeExpr 259sizeRigid (RConst k) n = SizeConst (inc k n) 260sizeRigid (RVar i) n = SizeVar i n 261 262{- 263apply :: SizeExpr -> Solution -> SizeExpr 264apply e@(SizeExpr (Rigid _) _) phi = e 265apply e@(SizeExpr (Flex x) i) phi = case Map.lookup x phi of 266 Nothing -> e 267 Just (SizeExpr v j) -> SizeExpr v (i + j) 268 269after :: Solution -> Solution -> Solution 270after psi phi = Map.map (\ e -> e `apply` phi) psi 271-} 272 273{- compute solution 274 275a solution CANNOT exist if 276 277 v < v for a rigid variable v 278 279 -- Andreas, 2012-09-19 OUTDATED are: 280 281 -- v <= v' for rigid variables v,v' 282 283 -- x < v for a flexible variable x and a rigid variable v 284 285 286thus, for each flexible x, only one of the following cases is possible 287 288 r+n <= x+m <= infty for a unique rigid r (meaning r --(m-n)--> x) 289 x <= r+n for a unique rigid r (meaning x --(n)--> r) 290 291we are looking for the least values for flexible variables that solve 292the constraints. Algorithm 293 294while flexible variables and rigid rows left 295 find a rigid variable row i 296 for all flexible columns j 297 if i --n--> j with n<=0 (meaning i+n <= j) then j = i + n 298 299while flexible variables j left 300 search the row j for entry i 301 if j --n--> i with n >= 0 (meaning j <= i + n) then j = i + n 302 303-} 304 305solve :: Constraints -> Maybe Solution 306solve cs = -- trace (prettyShow cs) $ 307 -- trace (prettyShow lm0) $ 308 -- trace (prettyShow lm) $ -- trace (prettyShow d) $ 309 let solution = if solvable then loop1 flexs rigids emptySolution 310 else Nothing 311 in -- trace (prettyShow solution) $ 312 solution 313 where -- compute the graph and its transitive closure m 314 gr = buildGraph cs 315 n = nextNode gr -- number of nodes 316 m0 = mkMatrix n (graph gr) 317 m = warshall m0 318 319 -- tracing only: build output version of transitive graph 320 legend i = fromJust $ Map.lookup i (intMap gr) -- trace only 321 lm0 = LegendMatrix m0 legend legend -- trace only 322 lm = LegendMatrix m legend legend -- trace only 323 324 -- compute the sets of flexible and rigid node numbers 325 ns = Map.keys (nodeMap gr) 326 -- a set of flexible variables 327 flexs = List.foldl' (\ l -> \case (Flex i ) -> i : l 328 (Rigid _) -> l) [] ns 329 -- a set of rigid variables 330 rigids = List.foldl' (\ l -> \case (Flex _ ) -> l 331 (Rigid i) -> i : l) [] ns 332 333 -- rigid matrix indices 334 rInds = List.foldl' (\ l r -> let Just i = Map.lookup (Rigid r) (nodeMap gr) 335 in i : l) [] rigids 336 337 -- check whether there is a solution 338 -- d = [ m!(i,i) | i <- [0 .. (n-1)] ] -- diagonal 339-- a rigid variable might not be less than it self, so no -.. on the 340-- rigid part of the diagonal 341 solvable = all (\ x -> x >= Finite 0) [ m!(i,i) | i <- rInds ] && True 342 343{- Andreas, 2012-09-19 344 We now can have constraints between rigid variables, like i < j. 345 Thus we skip the following two test. However, a solution must be 346 checked for consistency with the constraints on rigid vars. 347 348-- a rigid variable might not be bounded below by infinity or 349-- bounded above by a constant 350-- it might not be related to another rigid variable 351 all (\ (r, r') -> r == r' || 352 let Just row = (Map.lookup (Rigid r) (nodeMap gr)) 353 Just col = (Map.lookup (Rigid r') (nodeMap gr)) 354 edge = m!(row,col) 355 in isBelow r edge r' ) 356 [ (r,r') | r <- rigids, r' <- rigids ] 357 && 358-- a flexible variable might not be strictly below a rigid variable 359 all (\ (x, v) -> 360 let Just row = (Map.lookup (Flex x) (nodeMap gr)) 361 Just col = (Map.lookup (Rigid (RVar v)) (nodeMap gr)) 362 edge = m!(row,col) 363 in edge >= Finite 0) 364 [ (x,v) | x <- flexs, (RVar v) <- rigids ] 365-} 366 367 inScope :: FlexId -> Rigid -> Bool 368 inScope x (RConst _) = True 369 inScope x (RVar v) = scope v 370 where Just scope = Map.lookup x (flexScope gr) 371 372{- loop1 373 374while flexible variables and rigid rows left 375 find a rigid variable row i 376 for all flexible columns j 377 if i --n--> j with n<=0 (meaning i + n <= j) then j = i + n 378 379-} 380 loop1 :: [FlexId] -> [Rigid] -> Solution -> Maybe Solution 381 loop1 [] rgds subst = Just subst 382 loop1 flxs [] subst = loop2 flxs subst 383 loop1 flxs (r:rgds) subst = 384 let row = fromJust $ Map.lookup (Rigid r) (nodeMap gr) 385 (flxs',subst') = 386 List.foldl' (\ (flx,sub) f -> 387 let col = fromJust $ Map.lookup (Flex f) (nodeMap gr) 388 in case (inScope f r, m!(row,col)) of 389-- Finite z | z <= 0 -> 390 (True, Finite z) -> 391 let trunc z | z >= 0 = 0 392 | otherwise = -z 393 in (flx, extendSolution sub f (sizeRigid r (trunc z))) 394 _ -> (f : flx, sub) 395 ) ([], subst) flxs 396 in loop1 flxs' rgds subst' 397 398{- loop2 399 400while flexible variables j left 401 search the row j for entry i 402 if j --n--> i with n >= 0 (meaning j <= i + n) then j = i 403 404-} 405 loop2 :: [FlexId] -> Solution -> Maybe Solution 406 loop2 [] subst = Just subst 407 loop2 (f:flxs) subst = loop3 0 subst 408 where row = fromJust $ Map.lookup (Flex f) (nodeMap gr) 409 loop3 col subst | col >= n = 410 -- default to infinity 411 loop2 flxs (extendSolution subst f (SizeConst Infinite)) 412 loop3 col subst = 413 case Map.lookup col (intMap gr) of 414 Just (Rigid r) | not (infinite r) -> 415 case (inScope f r, m!(row,col)) of 416 (True, Finite z) | z >= 0 -> 417 loop2 flxs (extendSolution subst f (sizeRigid r z)) 418 (_, Infinite) -> loop3 (col+1) subst 419 _ -> -- trace ("unusable rigid: " ++ prettyShow r ++ " for flex " ++ prettyShow f) 420 Nothing -- NOT: loop3 (col+1) subst 421 _ -> loop3 (col+1) subst 422