{- | 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 Prelude hiding ((!!))

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 :: forall a. SemiRing a => 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 :: forall edge node.
(SemiRing edge, Ord node) =>
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 a. [a] -> 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 a b. (a -> b -> b) -> b -> [a] -> b
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. HasCallStack => [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 a. a -> [a]
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
$c== :: Weight -> Weight -> Bool
== :: Weight -> Weight -> Bool
$c/= :: Weight -> Weight -> Bool
/= :: 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
$cshowsPrec :: Int -> Weight -> ShowS
showsPrec :: Int -> Weight -> ShowS
$cshow :: Weight -> String
show :: Weight -> String
$cshowList :: [Weight] -> ShowS
showList :: [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
$c== :: Node -> Node -> Bool
== :: Node -> Node -> Bool
$c/= :: Node -> Node -> Bool
/= :: 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
$ccompare :: Node -> Node -> Ordering
compare :: Node -> Node -> Ordering
$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
>= :: Node -> Node -> Bool
$cmax :: Node -> Node -> Node
max :: Node -> Node -> Node
$cmin :: Node -> Node -> Node
min :: Node -> Node -> 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
$c== :: Rigid -> Rigid -> Bool
== :: Rigid -> Rigid -> Bool
$c/= :: Rigid -> Rigid -> Bool
/= :: 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
$ccompare :: Rigid -> Rigid -> Ordering
compare :: Rigid -> Rigid -> Ordering
$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
>= :: Rigid -> Rigid -> Bool
$cmax :: Rigid -> Rigid -> Rigid
max :: Rigid -> Rigid -> Rigid
$cmin :: Rigid -> Rigid -> Rigid
min :: Rigid -> Rigid -> 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 a. a -> StateT Graph Identity a
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 a. a -> StateT Graph Identity a
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 a. a -> StateT Graph Identity a
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
  { forall a b c. LegendMatrix a b c -> Matrix a
matrix   :: Matrix a
  , forall a b c. LegendMatrix a b c -> Int -> b
rowdescr :: Int -> b
  , forall a b c. 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 a b. (a -> b -> b) -> b -> [a] -> b
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 a b. (a -> b -> b) -> b -> [a] -> b
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 a b. (a -> b -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 :: a -> a
trunc a
z | a
z a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = a
0
                                            | Bool
otherwise = -a
z
                                   in ([Int]
flx, Solution -> Int -> SizeExpr -> Solution
extendSolution Solution
sub Int
f (Rigid -> Int -> SizeExpr
sizeRigid Rigid
r (Int -> Int
forall {a}. (Ord a, Num a) => a -> a
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