{- | Construct a graph from constraints
@
   x + n <= y   becomes   x ---(-n)---> y
   x <= n + y   becomes   x ---(+n)---> y
@
the default edge (= no edge) is labelled with infinity.

Building the graph involves keeping track of the node names.
We do this in a finite map, assigning consecutive numbers to nodes.
-}
module Agda.Utils.Warshall where

import Control.Monad.State

import Data.Maybe
import Data.Array
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map

import Agda.Utils.SemiRing
import Agda.Utils.List (nubOn)
import Agda.Utils.Pretty as P

import Agda.Utils.Impossible

type Matrix a = Array (Int,Int) a

-- assuming a square matrix
warshall :: SemiRing a => Matrix a -> Matrix a
warshall :: Matrix a -> Matrix a
warshall Matrix a
a0 = Int -> Matrix a -> Matrix a
loop Int
r Matrix a
a0 where
  b :: ((Int, Int), (Int, Int))
b@((Int
r,Int
c),(Int
r',Int
c')) = Matrix a -> ((Int, Int), (Int, Int))
forall i e. Array i e -> (i, i)
bounds Matrix a
a0 -- assuming r == c and r' == c'
  loop :: Int -> Matrix a -> Matrix a
loop Int
k Matrix a
a | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
r' =
    Int -> Matrix a -> Matrix a
loop (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (((Int, Int), (Int, Int)) -> [((Int, Int), a)] -> Matrix a
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array ((Int, Int), (Int, Int))
b [ ((Int
i,Int
j),
                           (Matrix a
aMatrix a -> (Int, Int) -> a
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
j)) a -> a -> a
forall a. SemiRing a => a -> a -> a
`oplus` ((Matrix a
aMatrix a -> (Int, Int) -> a
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
k)) a -> a -> a
forall a. SemiRing a => a -> a -> a
`otimes` (Matrix a
aMatrix a -> (Int, Int) -> a
forall i e. Ix i => Array i e -> i -> e
!(Int
k,Int
j))))
                        | Int
i <- [Int
r..Int
r'], Int
j <- [Int
c..Int
c'] ])
           | Bool
otherwise = Matrix a
a

type AdjList node edge = Map node [(node, edge)]

-- | Warshall's algorithm on a graph represented as an adjacency list.
warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edge
warshallG :: AdjList node edge -> AdjList node edge
warshallG AdjList node edge
g = Array (Int, Int) (Maybe edge) -> AdjList node edge
fromMatrix (Array (Int, Int) (Maybe edge) -> AdjList node edge)
-> Array (Int, Int) (Maybe edge) -> AdjList node edge
forall a b. (a -> b) -> a -> b
$ Array (Int, Int) (Maybe edge) -> Array (Int, Int) (Maybe edge)
forall a. SemiRing a => Matrix a -> Matrix a
warshall Array (Int, Int) (Maybe edge)
m
  where
    nodes :: [(node, Int)]
nodes = [node] -> [Int] -> [(node, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((node -> node) -> [node] -> [node]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn node -> node
forall a. a -> a
id ([node] -> [node]) -> [node] -> [node]
forall a b. (a -> b) -> a -> b
$ AdjList node edge -> [node]
forall k a. Map k a -> [k]
Map.keys AdjList node edge
g [node] -> [node] -> [node]
forall a. [a] -> [a] -> [a]
++ ((node, edge) -> node) -> [(node, edge)] -> [node]
forall a b. (a -> b) -> [a] -> [b]
map (node, edge) -> node
forall a b. (a, b) -> a
fst ([[(node, edge)]] -> [(node, edge)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(node, edge)]] -> [(node, edge)])
-> [[(node, edge)]] -> [(node, edge)]
forall a b. (a -> b) -> a -> b
$ AdjList node edge -> [[(node, edge)]]
forall k a. Map k a -> [a]
Map.elems AdjList node edge
g))
                [Int
0..]
    len :: Int
len   = [(node, Int)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(node, Int)]
nodes
    b :: ((Int, Int), (Int, Int))
b     = ((Int
0,Int
0), (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1,Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))

    edge :: node -> node -> Maybe edge
edge node
i node
j = do
      [(node, edge)]
es <- node -> AdjList node edge -> Maybe [(node, edge)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup node
i AdjList node edge
g
      (Maybe edge -> Maybe edge -> Maybe edge)
-> Maybe edge -> [Maybe edge] -> Maybe edge
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe edge -> Maybe edge -> Maybe edge
forall a. SemiRing a => a -> a -> a
oplus Maybe edge
forall a. Maybe a
Nothing [ edge -> Maybe edge
forall a. a -> Maybe a
Just edge
v | (node
j', edge
v) <- [(node, edge)]
es, node
j node -> node -> Bool
forall a. Eq a => a -> a -> Bool
== node
j' ]

    m :: Array (Int, Int) (Maybe edge)
m = ((Int, Int), (Int, Int))
-> [((Int, Int), Maybe edge)] -> Array (Int, Int) (Maybe edge)
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array ((Int, Int), (Int, Int))
b [ ((Int
n, Int
m), node -> node -> Maybe edge
edge node
i node
j) | (node
i, Int
n) <- [(node, Int)]
nodes, (node
j, Int
m) <- [(node, Int)]
nodes ]

    fromMatrix :: Array (Int, Int) (Maybe edge) -> AdjList node edge
fromMatrix Array (Int, Int) (Maybe edge)
matrix = ([(node, edge)] -> [(node, edge)] -> [(node, edge)])
-> [(node, [(node, edge)])] -> AdjList node edge
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [(node, edge)] -> [(node, edge)] -> [(node, edge)]
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(node, [(node, edge)])] -> AdjList node edge)
-> [(node, [(node, edge)])] -> AdjList node edge
forall a b. (a -> b) -> a -> b
$ do
      (node
i, Int
n) <- [(node, Int)]
nodes
      let es :: [(node, edge)]
es = [ ((node, Int) -> node
forall a b. (a, b) -> a
fst ([(node, Int)]
nodes [(node, Int)] -> Int -> (node, Int)
forall a. [a] -> Int -> a
!! Int
m), edge
e)
               | Int
m <- [Int
0..Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
               , Just edge
e <- [Array (Int, Int) (Maybe edge)
matrix Array (Int, Int) (Maybe edge) -> (Int, Int) -> Maybe edge
forall i e. Ix i => Array i e -> i -> e
! (Int
n, Int
m)]
               ]
      (node, [(node, edge)]) -> [(node, [(node, edge)])]
forall (m :: * -> *) a. Monad m => a -> m a
return (node
i, [(node, edge)]
es)

-- | Edge weight in the graph, forming a semi ring.
data Weight
  = Finite Int
  | Infinite
  deriving (Weight -> Weight -> Bool
(Weight -> Weight -> Bool)
-> (Weight -> Weight -> Bool) -> Eq Weight
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Weight -> Weight -> Bool
$c/= :: Weight -> Weight -> Bool
== :: Weight -> Weight -> Bool
$c== :: Weight -> Weight -> Bool
Eq, Int -> Weight -> ShowS
[Weight] -> ShowS
Weight -> String
(Int -> Weight -> ShowS)
-> (Weight -> String) -> ([Weight] -> ShowS) -> Show Weight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Weight] -> ShowS
$cshowList :: [Weight] -> ShowS
show :: Weight -> String
$cshow :: Weight -> String
showsPrec :: Int -> Weight -> ShowS
$cshowsPrec :: Int -> Weight -> ShowS
Show)

inc :: Weight -> Int -> Weight
inc :: Weight -> Int -> Weight
inc Weight
Infinite   Int
n = Weight
Infinite
inc (Finite Int
k) Int
n = Int -> Weight
Finite (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)

instance Pretty Weight where
  pretty :: Weight -> Doc
pretty (Finite Int
i) = Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
  pretty Weight
Infinite   = Doc
"."

instance Ord Weight where
  Weight
a <= :: Weight -> Weight -> Bool
<= Weight
Infinite = Bool
True
  Weight
Infinite <= Weight
b = Bool
False
  Finite Int
a <= Finite Int
b = Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
b

instance SemiRing Weight where
  ozero :: Weight
ozero = Weight
Infinite
  oone :: Weight
oone  = Int -> Weight
Finite Int
0

  oplus :: Weight -> Weight -> Weight
oplus = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
min

  otimes :: Weight -> Weight -> Weight
otimes Weight
Infinite Weight
_ = Weight
Infinite
  otimes Weight
_ Weight
Infinite = Weight
Infinite
  otimes (Finite Int
a) (Finite Int
b) = Int -> Weight
Finite (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b)

-- constraints ---------------------------------------------------

-- | Nodes of the graph are either
-- - flexible variables (with identifiers drawn from @Int@),
-- - rigid variables (also identified by @Int@s), or
-- - constants (like 0, infinity, or anything between).

data Node = Rigid Rigid
          | Flex  FlexId
            deriving (Node -> Node -> Bool
(Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c== :: Node -> Node -> Bool
Eq, Eq Node
Eq Node
-> (Node -> Node -> Ordering)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Bool)
-> (Node -> Node -> Node)
-> (Node -> Node -> Node)
-> Ord Node
Node -> Node -> Bool
Node -> Node -> Ordering
Node -> Node -> Node
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmax :: Node -> Node -> Node
>= :: Node -> Node -> Bool
$c>= :: Node -> Node -> Bool
> :: Node -> Node -> Bool
$c> :: Node -> Node -> Bool
<= :: Node -> Node -> Bool
$c<= :: Node -> Node -> Bool
< :: Node -> Node -> Bool
$c< :: Node -> Node -> Bool
compare :: Node -> Node -> Ordering
$ccompare :: Node -> Node -> Ordering
$cp1Ord :: Eq Node
Ord)

data Rigid = RConst Weight
           | RVar RigidId
             deriving (Rigid -> Rigid -> Bool
(Rigid -> Rigid -> Bool) -> (Rigid -> Rigid -> Bool) -> Eq Rigid
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rigid -> Rigid -> Bool
$c/= :: Rigid -> Rigid -> Bool
== :: Rigid -> Rigid -> Bool
$c== :: Rigid -> Rigid -> Bool
Eq, Eq Rigid
Eq Rigid
-> (Rigid -> Rigid -> Ordering)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Bool)
-> (Rigid -> Rigid -> Rigid)
-> (Rigid -> Rigid -> Rigid)
-> Ord Rigid
Rigid -> Rigid -> Bool
Rigid -> Rigid -> Ordering
Rigid -> Rigid -> Rigid
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Rigid -> Rigid -> Rigid
$cmin :: Rigid -> Rigid -> Rigid
max :: Rigid -> Rigid -> Rigid
$cmax :: Rigid -> Rigid -> Rigid
>= :: Rigid -> Rigid -> Bool
$c>= :: Rigid -> Rigid -> Bool
> :: Rigid -> Rigid -> Bool
$c> :: Rigid -> Rigid -> Bool
<= :: Rigid -> Rigid -> Bool
$c<= :: Rigid -> Rigid -> Bool
< :: Rigid -> Rigid -> Bool
$c< :: Rigid -> Rigid -> Bool
compare :: Rigid -> Rigid -> Ordering
$ccompare :: Rigid -> Rigid -> Ordering
$cp1Ord :: Eq Rigid
Ord)

type NodeId  = Int
type RigidId = Int
type FlexId  = Int
type Scope   = RigidId -> Bool
-- ^ Which rigid variables a flex may be instatiated to.

instance Pretty Node where
  pretty :: Node -> Doc
pretty (Flex  Int
i)                   = Doc
"?" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
  pretty (Rigid (RVar Int
i))            = Doc
"v" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i
  pretty (Rigid (RConst Weight
Infinite))   = Doc
"#"
  pretty (Rigid (RConst (Finite Int
n))) = Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n

infinite :: Rigid -> Bool
infinite :: Rigid -> Bool
infinite (RConst Weight
Infinite) = Bool
True
infinite Rigid
_                 = Bool
False

-- | @isBelow r w r'@
--   checks, if @r@ and @r'@ are connected by @w@ (meaning @w@ not infinite),
--   whether @r + w <= r'@.
--   Precondition: not the same rigid variable.
isBelow :: Rigid -> Weight -> Rigid -> Bool
isBelow :: Rigid -> Weight -> Rigid -> Bool
isBelow Rigid
_ Weight
Infinite Rigid
_ = Bool
True
isBelow Rigid
_ Weight
n (RConst Weight
Infinite) = Bool
True
isBelow (RConst (Finite Int
i)) (Finite Int
n) (RConst (Finite Int
j)) = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
j
isBelow Rigid
_ Weight
_ Rigid
_ = Bool
False -- rigid variables are not related

-- | A constraint is an edge in the graph.
data Constraint
  = NewFlex FlexId Scope
  | Arc Node Int Node
    -- ^ For @Arc v1 k v2@  at least one of @v1@ or @v2@ is a @MetaV@ (Flex),
    --                      the other a @MetaV@ or a @Var@ (Rigid).
    --   If @k <= 0@ this means  @suc^(-k) v1 <= v2@
    --   otherwise               @v1 <= suc^k v3@.

instance Pretty Constraint where
  pretty :: Constraint -> Doc
pretty (NewFlex Int
i Int -> Bool
s) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Doc
"SizeMeta(?", Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i, Doc
")" ]
  pretty (Arc Node
v1 Int
k Node
v2)
    | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Node -> Doc
forall a. Pretty a => a -> Doc
pretty Node
v1, Doc
"<=", Node -> Doc
forall a. Pretty a => a -> Doc
pretty Node
v2 ]
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Node -> Doc
forall a. Pretty a => a -> Doc
pretty Node
v1, Doc
"+", Int -> Doc
forall a. Pretty a => a -> Doc
pretty (-Int
k), Doc
"<=", Node -> Doc
forall a. Pretty a => a -> Doc
pretty Node
v2 ]
    | Bool
otherwise = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Node -> Doc
forall a. Pretty a => a -> Doc
pretty Node
v1, Doc
"<=", Node -> Doc
forall a. Pretty a => a -> Doc
pretty Node
v2, Doc
"+", Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
k ]

type Constraints = [Constraint]

emptyConstraints :: Constraints
emptyConstraints :: [Constraint]
emptyConstraints = []

-- graph (matrix) ------------------------------------------------

data Graph = Graph
  { Graph -> Map Int (Int -> Bool)
flexScope :: Map FlexId Scope           -- ^ Scope for each flexible var.
  , Graph -> Map Node Int
nodeMap   :: Map Node NodeId            -- ^ Node labels to node numbers.
  , Graph -> Map Int Node
intMap    :: Map NodeId Node            -- ^ Node numbers to node labels.
  , Graph -> Int
nextNode  :: NodeId                     -- ^ Number of nodes @n@.
  , Graph -> Int -> Int -> Weight
graph     :: NodeId -> NodeId -> Weight -- ^ The edges (restrict to @[0..n[@).
  }

-- | The empty graph: no nodes, edges are all undefined (infinity weight).
initGraph :: Graph
initGraph :: Graph
initGraph = Map Int (Int -> Bool)
-> Map Node Int
-> Map Int Node
-> Int
-> (Int -> Int -> Weight)
-> Graph
Graph Map Int (Int -> Bool)
forall k a. Map k a
Map.empty Map Node Int
forall k a. Map k a
Map.empty Map Int Node
forall k a. Map k a
Map.empty Int
0 (\ Int
x Int
y -> Weight
Infinite)

-- | The Graph Monad, for constructing a graph iteratively.
type GM = State Graph

-- | Add a size meta node.
addFlex :: FlexId -> Scope -> GM ()
addFlex :: Int -> (Int -> Bool) -> GM ()
addFlex Int
x Int -> Bool
scope = do
  (Graph -> Graph) -> GM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Graph -> Graph) -> GM ()) -> (Graph -> Graph) -> GM ()
forall a b. (a -> b) -> a -> b
$ \ Graph
st -> Graph
st { flexScope :: Map Int (Int -> Bool)
flexScope = Int
-> (Int -> Bool) -> Map Int (Int -> Bool) -> Map Int (Int -> Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
x Int -> Bool
scope (Graph -> Map Int (Int -> Bool)
flexScope Graph
st) }
  Int
_ <- Node -> GM Int
addNode (Int -> Node
Flex Int
x)
  () -> GM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Lookup identifier of a node.
--   If not present, it is added first.
addNode :: Node -> GM Int
addNode :: Node -> GM Int
addNode Node
n = do
  Graph
st <- StateT Graph Identity Graph
forall s (m :: * -> *). MonadState s m => m s
get
  case Node -> Map Node Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node
n (Graph -> Map Node Int
nodeMap Graph
st) of
    Just Int
i -> Int -> GM Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
    Maybe Int
Nothing -> do
      let i :: Int
i = Graph -> Int
nextNode Graph
st
      Graph -> GM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Graph -> GM ()) -> Graph -> GM ()
forall a b. (a -> b) -> a -> b
$ Graph
st { nodeMap :: Map Node Int
nodeMap  = Node -> Int -> Map Node Int -> Map Node Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Node
n Int
i (Graph -> Map Node Int
nodeMap Graph
st)
               , intMap :: Map Int Node
intMap   = Int -> Node -> Map Int Node -> Map Int Node
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
i Node
n (Graph -> Map Int Node
intMap Graph
st)
               , nextNode :: Int
nextNode = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
               }
      Int -> GM Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

-- | @addEdge n1 k n2@
--   improves the weight of egde @n1->n2@ to be at most @k@.
--   Also adds nodes if not yet present.
addEdge :: Node -> Int -> Node -> GM ()
addEdge :: Node -> Int -> Node -> GM ()
addEdge Node
n1 Int
k Node
n2 = do
  Int
i1 <- Node -> GM Int
addNode Node
n1
  Int
i2 <- Node -> GM Int
addNode Node
n2
  Graph
st <- StateT Graph Identity Graph
forall s (m :: * -> *). MonadState s m => m s
get
  let graph' :: Int -> Int -> Weight
graph' Int
x Int
y = if (Int
x,Int
y) (Int, Int) -> (Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
i1,Int
i2) then Int -> Weight
Finite Int
k Weight -> Weight -> Weight
forall a. SemiRing a => a -> a -> a
`oplus` Graph -> Int -> Int -> Weight
graph Graph
st Int
x Int
y
                   else Graph -> Int -> Int -> Weight
graph Graph
st Int
x Int
y
  Graph -> GM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Graph -> GM ()) -> Graph -> GM ()
forall a b. (a -> b) -> a -> b
$ Graph
st { graph :: Int -> Int -> Weight
graph = Int -> Int -> Weight
graph' }

addConstraint :: Constraint -> GM ()
addConstraint :: Constraint -> GM ()
addConstraint (NewFlex Int
x Int -> Bool
scope) = Int -> (Int -> Bool) -> GM ()
addFlex Int
x Int -> Bool
scope
addConstraint (Arc Node
n1 Int
k Node
n2)     = Node -> Int -> Node -> GM ()
addEdge Node
n1 Int
k Node
n2

buildGraph :: Constraints -> Graph
buildGraph :: [Constraint] -> Graph
buildGraph [Constraint]
cs = GM () -> Graph -> Graph
forall s a. State s a -> s -> s
execState ((Constraint -> GM ()) -> [Constraint] -> GM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Constraint -> GM ()
addConstraint [Constraint]
cs) Graph
initGraph

mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight
mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight
mkMatrix Int
n Int -> Int -> Weight
g = ((Int, Int), (Int, Int)) -> [((Int, Int), Weight)] -> Matrix Weight
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array ((Int
0,Int
0),(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
                 [ ((Int
i,Int
j), Int -> Int -> Weight
g Int
i Int
j) | Int
i <- [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1], Int
j <- [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]

-- displaying matrices with row and column labels --------------------

-- | A matrix with row descriptions in @b@ and column descriptions in @c@.
data LegendMatrix a b c = LegendMatrix
  { LegendMatrix a b c -> Matrix a
matrix   :: Matrix a
  , LegendMatrix a b c -> Int -> b
rowdescr :: Int -> b
  , LegendMatrix a b c -> Int -> c
coldescr :: Int -> c
  }

instance (Pretty a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) where
  pretty :: LegendMatrix a b c -> Doc
pretty (LegendMatrix Matrix a
m Int -> b
rd Int -> c
cd) =
    -- first show column description
    let ((Int
r,Int
c),(Int
r',Int
c')) = Matrix a -> ((Int, Int), (Int, Int))
forall i e. Array i e -> (i, i)
bounds Matrix a
m
    in (Int -> Doc -> Doc) -> Doc -> [Int] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Int
j Doc
s -> Doc
"\t" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> c -> Doc
forall a. Pretty a => a -> Doc
pretty (Int -> c
cd Int
j) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
s) Doc
"" [Int
c .. Int
c'] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<>
    -- then output rows
       (Int -> Doc -> Doc) -> Doc -> [Int] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Int
i Doc
s -> Doc
"\n" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> b -> Doc
forall a. Pretty a => a -> Doc
pretty (Int -> b
rd Int
i) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<>
                (Int -> Doc -> Doc) -> Doc -> [Int] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Int
j Doc
t -> Doc
"\t" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> a -> Doc
forall a. Pretty a => a -> Doc
pretty (Matrix a
mMatrix a -> (Int, Int) -> a
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
j)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
t)
                      Doc
s
                      [Int
c .. Int
c'])
             Doc
"" [Int
r .. Int
r']

-- solving the constraints -------------------------------------------

-- | A solution assigns to each flexible variable a size expression
--   which is either a constant or a @v + n@ for a rigid variable @v@.
type Solution = Map Int SizeExpr

emptySolution :: Solution
emptySolution :: Solution
emptySolution = Solution
forall k a. Map k a
Map.empty

extendSolution :: Solution -> Int -> SizeExpr -> Solution
extendSolution :: Solution -> Int -> SizeExpr -> Solution
extendSolution Solution
subst Int
k SizeExpr
v = Int -> SizeExpr -> Solution -> Solution
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
k SizeExpr
v Solution
subst

data SizeExpr = SizeVar RigidId Int   -- ^ e.g. x + 5
              | SizeConst Weight      -- ^ a number or infinity

instance Pretty SizeExpr where
  pretty :: SizeExpr -> Doc
pretty (SizeVar Int
n Int
0) = Node -> Doc
forall a. Pretty a => a -> Doc
pretty (Rigid -> Node
Rigid (Int -> Rigid
RVar Int
n))
  pretty (SizeVar Int
n Int
k) = Node -> Doc
forall a. Pretty a => a -> Doc
pretty (Rigid -> Node
Rigid (Int -> Rigid
RVar Int
n)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
"+" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
k
  pretty (SizeConst Weight
w) = Weight -> Doc
forall a. Pretty a => a -> Doc
pretty Weight
w

-- | @sizeRigid r n@ returns the size expression corresponding to @r + n@
sizeRigid :: Rigid -> Int -> SizeExpr
sizeRigid :: Rigid -> Int -> SizeExpr
sizeRigid (RConst Weight
k) Int
n = Weight -> SizeExpr
SizeConst (Weight -> Int -> Weight
inc Weight
k Int
n)
sizeRigid (RVar Int
i)   Int
n = Int -> Int -> SizeExpr
SizeVar Int
i Int
n

{-
apply :: SizeExpr -> Solution -> SizeExpr
apply e@(SizeExpr (Rigid _) _) phi = e
apply e@(SizeExpr (Flex  x) i) phi = case Map.lookup x phi of
  Nothing -> e
  Just (SizeExpr v j) -> SizeExpr v (i + j)

after :: Solution -> Solution -> Solution
after psi phi = Map.map (\ e -> e `apply` phi) psi
-}

{- compute solution

a solution CANNOT exist if

  v < v  for a rigid variable v

  -- Andreas, 2012-09-19 OUTDATED are:

  -- v <= v' for rigid variables v,v'

  -- x < v   for a flexible variable x and a rigid variable v


thus, for each flexible x, only one of the following cases is possible

  r+n <= x+m <= infty  for a unique rigid r  (meaning r --(m-n)--> x)
  x <= r+n             for a unique rigid r  (meaning x --(n)--> r)

we are looking for the least values for flexible variables that solve
the constraints.  Algorithm

while flexible variables and rigid rows left
  find a rigid variable row i
    for all flexible columns j
      if i --n--> j with n<=0 (meaning i+n <= j) then j = i + n

while flexible variables j left
  search the row j for entry i
    if j --n--> i with n >= 0 (meaning j <= i + n) then j = i + n

-}

solve :: Constraints -> Maybe Solution
solve :: [Constraint] -> Maybe Solution
solve [Constraint]
cs = -- trace (prettyShow cs) $
   -- trace (prettyShow lm0) $
    -- trace (prettyShow lm) $ -- trace (prettyShow d) $
     let solution :: Maybe Solution
solution = if Bool
solvable then [Int] -> [Rigid] -> Solution -> Maybe Solution
loop1 [Int]
flexs [Rigid]
rigids Solution
emptySolution
                    else Maybe Solution
forall a. Maybe a
Nothing
     in -- trace (prettyShow solution) $
         Maybe Solution
solution
   where -- compute the graph and its transitive closure m
         gr :: Graph
gr  = [Constraint] -> Graph
buildGraph [Constraint]
cs
         n :: Int
n   = Graph -> Int
nextNode Graph
gr            -- number of nodes
         m0 :: Matrix Weight
m0  = Int -> (Int -> Int -> Weight) -> Matrix Weight
mkMatrix Int
n (Graph -> Int -> Int -> Weight
graph Graph
gr)
         m :: Matrix Weight
m   = Matrix Weight -> Matrix Weight
forall a. SemiRing a => Matrix a -> Matrix a
warshall Matrix Weight
m0

         -- tracing only: build output version of transitive graph
         legend :: Int -> Node
legend Int
i = Maybe Node -> Node
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Node -> Node) -> Maybe Node -> Node
forall a b. (a -> b) -> a -> b
$ Int -> Map Int Node -> Maybe Node
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i (Graph -> Map Int Node
intMap Graph
gr) -- trace only
         lm0 :: LegendMatrix Weight Node Node
lm0 = Matrix Weight
-> (Int -> Node) -> (Int -> Node) -> LegendMatrix Weight Node Node
forall a b c.
Matrix a -> (Int -> b) -> (Int -> c) -> LegendMatrix a b c
LegendMatrix Matrix Weight
m0 Int -> Node
legend Int -> Node
legend            -- trace only
         lm :: LegendMatrix Weight Node Node
lm  = Matrix Weight
-> (Int -> Node) -> (Int -> Node) -> LegendMatrix Weight Node Node
forall a b c.
Matrix a -> (Int -> b) -> (Int -> c) -> LegendMatrix a b c
LegendMatrix Matrix Weight
m Int -> Node
legend Int -> Node
legend             -- trace only

         -- compute the sets of flexible and rigid node numbers
         ns :: [Node]
ns  = Map Node Int -> [Node]
forall k a. Map k a -> [k]
Map.keys (Graph -> Map Node Int
nodeMap Graph
gr)
         -- a set of flexible variables
         flexs :: [Int]
flexs  = ([Int] -> Node -> [Int]) -> [Int] -> [Node] -> [Int]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\ [Int]
l -> \case (Flex Int
i ) -> Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
l
                                            (Rigid Rigid
_) -> [Int]
l)     [] [Node]
ns
         -- a set of rigid variables
         rigids :: [Rigid]
rigids = ([Rigid] -> Node -> [Rigid]) -> [Rigid] -> [Node] -> [Rigid]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\ [Rigid]
l -> \case (Flex Int
_ ) -> [Rigid]
l
                                            (Rigid Rigid
i) -> Rigid
i Rigid -> [Rigid] -> [Rigid]
forall a. a -> [a] -> [a]
: [Rigid]
l) [] [Node]
ns

         -- rigid matrix indices
         rInds :: [Int]
rInds = ([Int] -> Rigid -> [Int]) -> [Int] -> [Rigid] -> [Int]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\ [Int]
l Rigid
r -> let Just Int
i = Node -> Map Node Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node
Rigid Rigid
r) (Graph -> Map Node Int
nodeMap Graph
gr)
                                       in Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
l) [] [Rigid]
rigids

         -- check whether there is a solution
         -- d   = [ m!(i,i) | i <- [0 .. (n-1)] ]  -- diagonal
-- a rigid variable might not be less than it self, so no -.. on the
-- rigid part of the diagonal
         solvable :: Bool
solvable = (Weight -> Bool) -> [Weight] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ Weight
x -> Weight
x Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Weight
Finite Int
0) [ Matrix Weight
mMatrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
i) | Int
i <- [Int]
rInds ] Bool -> Bool -> Bool
&& Bool
True

{-  Andreas, 2012-09-19
    We now can have constraints between rigid variables, like i < j.
    Thus we skip the following two test.  However, a solution must be
    checked for consistency with the constraints on rigid vars.

-- a rigid variable might not be bounded below by infinity or
-- bounded above by a constant
-- it might not be related to another rigid variable
           all (\ (r,  r') -> r == r' ||
                let Just row = (Map.lookup (Rigid r)  (nodeMap gr))
                    Just col = (Map.lookup (Rigid r') (nodeMap gr))
                    edge = m!(row,col)
                in  isBelow r edge r' )
             [ (r,r') | r <- rigids, r' <- rigids ]
           &&
-- a flexible variable might not be strictly below a rigid variable
           all (\ (x, v) ->
                let Just row = (Map.lookup (Flex x)  (nodeMap gr))
                    Just col = (Map.lookup (Rigid (RVar v)) (nodeMap gr))
                    edge = m!(row,col)
                in  edge >= Finite 0)
             [ (x,v) | x <- flexs, (RVar v) <- rigids ]
-}

         inScope :: FlexId -> Rigid -> Bool
         inScope :: Int -> Rigid -> Bool
inScope Int
x (RConst Weight
_) = Bool
True
         inScope Int
x (RVar Int
v)   = Int -> Bool
scope Int
v
             where Just Int -> Bool
scope = Int -> Map Int (Int -> Bool) -> Maybe (Int -> Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
x (Graph -> Map Int (Int -> Bool)
flexScope Graph
gr)

{- loop1

while flexible variables and rigid rows left
  find a rigid variable row i
    for all flexible columns j
      if i --n--> j with n<=0 (meaning i + n <= j) then j = i + n

-}
         loop1 :: [FlexId] -> [Rigid] -> Solution -> Maybe Solution
         loop1 :: [Int] -> [Rigid] -> Solution -> Maybe Solution
loop1 [] [Rigid]
rgds Solution
subst = Solution -> Maybe Solution
forall a. a -> Maybe a
Just Solution
subst
         loop1 [Int]
flxs [] Solution
subst = [Int] -> Solution -> Maybe Solution
loop2 [Int]
flxs Solution
subst
         loop1 [Int]
flxs (Rigid
r:[Rigid]
rgds) Solution
subst =
            let row :: Int
row = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Node -> Map Node Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node
Rigid Rigid
r) (Graph -> Map Node Int
nodeMap Graph
gr)
                ([Int]
flxs',Solution
subst') =
                  (([Int], Solution) -> Int -> ([Int], Solution))
-> ([Int], Solution) -> [Int] -> ([Int], Solution)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\ ([Int]
flx,Solution
sub) Int
f ->
                          let col :: Int
col = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Node -> Map Node Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int -> Node
Flex Int
f) (Graph -> Map Node Int
nodeMap Graph
gr)
                          in  case (Int -> Rigid -> Bool
inScope Int
f Rigid
r, Matrix Weight
mMatrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
!(Int
row,Int
col)) of
--                                Finite z | z <= 0 ->
                                (Bool
True, Finite Int
z) ->
                                   let trunc :: p -> p
trunc p
z | p
z p -> p -> Bool
forall a. Ord a => a -> a -> Bool
>= p
0 = p
0
                                            | Bool
otherwise = -p
z
                                   in ([Int]
flx, Solution -> Int -> SizeExpr -> Solution
extendSolution Solution
sub Int
f (Rigid -> Int -> SizeExpr
sizeRigid Rigid
r (Int -> Int
forall p. (Ord p, Num p) => p -> p
trunc Int
z)))
                                (Bool, Weight)
_ -> (Int
f Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
flx, Solution
sub)
                     ) ([], Solution
subst) [Int]
flxs
            in [Int] -> [Rigid] -> Solution -> Maybe Solution
loop1 [Int]
flxs' [Rigid]
rgds Solution
subst'

{- loop2

while flexible variables j left
  search the row j for entry i
    if j --n--> i with n >= 0 (meaning j <= i + n) then j = i

-}
         loop2 :: [FlexId] -> Solution -> Maybe Solution
         loop2 :: [Int] -> Solution -> Maybe Solution
loop2 [] Solution
subst = Solution -> Maybe Solution
forall a. a -> Maybe a
Just Solution
subst
         loop2 (Int
f:[Int]
flxs) Solution
subst = Int -> Solution -> Maybe Solution
loop3 Int
0 Solution
subst
           where row :: Int
row = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Node -> Map Node Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int -> Node
Flex Int
f) (Graph -> Map Node Int
nodeMap Graph
gr)
                 loop3 :: Int -> Solution -> Maybe Solution
loop3 Int
col Solution
subst | Int
col Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n =
                   -- default to infinity
                    [Int] -> Solution -> Maybe Solution
loop2 [Int]
flxs (Solution -> Int -> SizeExpr -> Solution
extendSolution Solution
subst Int
f (Weight -> SizeExpr
SizeConst Weight
Infinite))
                 loop3 Int
col Solution
subst =
                   case Int -> Map Int Node -> Maybe Node
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
col (Graph -> Map Int Node
intMap Graph
gr) of
                     Just (Rigid Rigid
r) | Bool -> Bool
not (Rigid -> Bool
infinite Rigid
r) ->
                       case (Int -> Rigid -> Bool
inScope Int
f Rigid
r, Matrix Weight
mMatrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
!(Int
row,Int
col)) of
                        (Bool
True, Finite Int
z) | Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 ->
                            [Int] -> Solution -> Maybe Solution
loop2 [Int]
flxs (Solution -> Int -> SizeExpr -> Solution
extendSolution Solution
subst Int
f (Rigid -> Int -> SizeExpr
sizeRigid Rigid
r Int
z))
                        (Bool
_, Weight
Infinite) -> Int -> Solution -> Maybe Solution
loop3 (Int
colInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Solution
subst
                        (Bool, Weight)
_ -> -- trace ("unusable rigid: " ++ prettyShow r ++ " for flex " ++ prettyShow f)
                              Maybe Solution
forall a. Maybe a
Nothing  -- NOT: loop3 (col+1) subst
                     Maybe Node
_ -> Int -> Solution -> Maybe Solution
loop3 (Int
colInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Solution
subst