{- | 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')) = 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 forall a. Ord a => a -> a -> Bool
<= Int
r' =
    Int -> Matrix a -> Matrix a
loop (Int
kforall a. Num a => a -> a -> a
+Int
1) (forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array ((Int, Int), (Int, Int))
b [ ((Int
i,Int
j),
                           (Matrix a
aforall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
j)) forall a. SemiRing a => a -> a -> a
`oplus` ((Matrix a
aforall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
k)) forall a. SemiRing a => a -> a -> a
`otimes` (Matrix a
aforall 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 forall a b. (a -> b) -> a -> b
$ forall a. SemiRing a => Matrix a -> Matrix a
warshall Array (Int, Int) (Maybe edge)
m
  where
    nodes :: [(node, Int)]
nodes = forall a b. [a] -> [b] -> [(a, b)]
zip (forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
Map.keys AdjList node edge
g forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems AdjList node edge
g))
                [Int
0..]
    len :: Int
len   = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(node, Int)]
nodes
    b :: ((Int, Int), (Int, Int))
b     = ((Int
0,Int
0), (Int
len forall a. Num a => a -> a -> a
- Int
1,Int
len forall a. Num a => a -> a -> a
- Int
1))

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

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

instance Pretty Weight where
  pretty :: Weight -> Doc
pretty (Finite Int
i) = 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 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 = 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 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
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
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
Ord)

data Rigid = RConst Weight
           | RVar RigidId
             deriving (Rigid -> Rigid -> Bool
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
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
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
"?" forall a. Semigroup a => a -> a -> a
P.<> forall a. Pretty a => a -> Doc
pretty Int
i
  pretty (Rigid (RVar Int
i))            = Doc
"v" forall a. Semigroup a => a -> a -> a
P.<> forall a. Pretty a => a -> Doc
pretty Int
i
  pretty (Rigid (RConst Weight
Infinite))   = Doc
"#"
  pretty (Rigid (RConst (Finite Int
n))) = 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 forall a. Num a => a -> a -> a
+ Int
n 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 Scope
s) = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Doc
"SizeMeta(?", forall a. Pretty a => a -> Doc
pretty Int
i, Doc
")" ]
  pretty (Arc Node
v1 Int
k Node
v2)
    | Int
k forall a. Eq a => a -> a -> Bool
== Int
0    = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ forall a. Pretty a => a -> Doc
pretty Node
v1, Doc
"<=", forall a. Pretty a => a -> Doc
pretty Node
v2 ]
    | Int
k forall a. Ord a => a -> a -> Bool
< Int
0     = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ forall a. Pretty a => a -> Doc
pretty Node
v1, Doc
"+", forall a. Pretty a => a -> Doc
pretty (-Int
k), Doc
"<=", forall a. Pretty a => a -> Doc
pretty Node
v2 ]
    | Bool
otherwise = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ forall a. Pretty a => a -> Doc
pretty Node
v1, Doc
"<=", forall a. Pretty a => a -> Doc
pretty Node
v2, 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 Scope
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 Scope
-> Map Node Int
-> Map Int Node
-> Int
-> (Int -> Int -> Weight)
-> Graph
Graph forall k a. Map k a
Map.empty forall k a. Map k a
Map.empty 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 -> Scope -> GM ()
addFlex Int
x Scope
scope = do
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ Graph
st -> Graph
st { flexScope :: Map Int Scope
flexScope = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
x Scope
scope (Graph -> Map Int Scope
flexScope Graph
st) }
  Int
_ <- Node -> GM Int
addNode (Int -> Node
Flex Int
x)
  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 <- forall s (m :: * -> *). MonadState s m => m s
get
  case 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
    Maybe Int
Nothing -> do
      let i :: Int
i = Graph -> Int
nextNode Graph
st
      forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ Graph
st { nodeMap :: Map Node Int
nodeMap  = 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   = 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 forall a. Num a => a -> a -> a
+ Int
1
               }
      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 <- forall s (m :: * -> *). MonadState s m => m s
get
  let graph' :: Int -> Int -> Weight
graph' Int
x Int
y = if (Int
x,Int
y) forall a. Eq a => a -> a -> Bool
== (Int
i1,Int
i2) then Int -> Weight
Finite Int
k 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
  forall s (m :: * -> *). MonadState s m => s -> m ()
put 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 Scope
scope) = Int -> Scope -> GM ()
addFlex Int
x Scope
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 = forall s a. State s a -> s -> s
execState (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 = forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array ((Int
0,Int
0),(Int
nforall a. Num a => a -> a -> a
-Int
1,Int
nforall 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
nforall a. Num a => a -> a -> a
-Int
1], Int
j <- [Int
0..Int
nforall 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')) = forall i e. Array i e -> (i, i)
bounds Matrix a
m
    in forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Int
j Doc
s -> Doc
"\t" forall a. Semigroup a => a -> a -> a
P.<> forall a. Pretty a => a -> Doc
pretty (Int -> c
cd Int
j) forall a. Semigroup a => a -> a -> a
P.<> Doc
s) Doc
"" [Int
c .. Int
c'] forall a. Semigroup a => a -> a -> a
P.<>
    -- then output rows
       forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Int
i Doc
s -> Doc
"\n" forall a. Semigroup a => a -> a -> a
P.<> forall a. Pretty a => a -> Doc
pretty (Int -> b
rd Int
i) forall a. Semigroup a => a -> a -> a
P.<>
                forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Int
j Doc
t -> Doc
"\t" forall a. Semigroup a => a -> a -> a
P.<> forall a. Pretty a => a -> Doc
pretty (Matrix a
mforall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
j)) 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 = 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 = 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) = forall a. Pretty a => a -> Doc
pretty (Rigid -> Node
Rigid (Int -> Rigid
RVar Int
n))
  pretty (SizeVar Int
n Int
k) = forall a. Pretty a => a -> Doc
pretty (Rigid -> Node
Rigid (Int -> Rigid
RVar Int
n)) forall a. Semigroup a => a -> a -> a
P.<> Doc
"+" forall a. Semigroup a => a -> a -> a
P.<> forall a. Pretty a => a -> Doc
pretty Int
k
  pretty (SizeConst Weight
w) = 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 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   = 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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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 = 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  = 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  = forall k a. Map k a -> [k]
Map.keys (Graph -> Map Node Int
nodeMap Graph
gr)
         -- a set of flexible variables
         flexs :: [Int]
flexs  = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\ [Int]
l -> \case (Flex Int
i ) -> Int
i forall a. a -> [a] -> [a]
: [Int]
l
                                            (Rigid Rigid
_) -> [Int]
l)     [] [Node]
ns
         -- a set of rigid variables
         rigids :: [Rigid]
rigids = 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 forall a. a -> [a] -> [a]
: [Rigid]
l) [] [Node]
ns

         -- rigid matrix indices
         rInds :: [Int]
rInds = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\ [Int]
l Rigid
r -> let Just Int
i = 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 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ Weight
x -> Weight
x forall a. Ord a => a -> a -> Bool
>= Int -> Weight
Finite Int
0) [ Matrix Weight
mforall 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)   = Scope
scope Int
v
             where Just Scope
scope = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
x (Graph -> Map Int Scope
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 = 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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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') =
                  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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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
mforall 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 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 (forall {a}. (Ord a, Num a) => a -> a
trunc Int
z)))
                                (Bool, Weight)
_ -> (Int
f 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 = 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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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 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 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
mforall i e. Ix i => Array i e -> i -> e
!(Int
row,Int
col)) of
                        (Bool
True, Finite Int
z) | Int
z 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
colforall a. Num a => a -> a -> a
+Int
1) Solution
subst
                        (Bool, Weight)
_ -> -- trace ("unusable rigid: " ++ prettyShow r ++ " for flex " ++ prettyShow f)
                              forall a. Maybe a
Nothing  -- NOT: loop3 (col+1) subst
                     Maybe Node
_ -> Int -> Solution -> Maybe Solution
loop3 (Int
colforall a. Num a => a -> a -> a
+Int
1) Solution
subst