{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

module Warshall where

{- 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.
-}


import Control.Monad.State
import Data.Maybe -- fromJust
import Data.Array
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.List as List

-- import Debug.Trace
-- import Util

traceSolve :: String -> a -> a
traceSolve :: forall a. String -> a -> a
traceSolve String
_msg = a -> a
forall a. a -> a
id
-- traceSolve = trace

traceSolveM :: Monad m => String -> m ()
traceSolveM :: forall (m :: * -> *). Monad m => String -> m ()
traceSolveM String
_msg = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
-- traceSolveM = traceM

-- semi rings ----------------------------------------------------

class SemiRing a where
  oplus  :: a -> a -> a
  otimes :: a -> a -> a
  ozero  :: a -- neutral for oplus, dominant for otimes
  oone   :: a -- neutral for otimes

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
forall {e}.
SemiRing e =>
Int -> Array (Int, Int) e -> Array (Int, Int) e
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 -> Array (Int, Int) e -> Array (Int, Int) e
loop Int
k Array (Int, Int) e
a | Int
k Int -> Scope
forall a. Ord a => a -> a -> Bool
<= Int
r' =
    Int -> Array (Int, Int) e -> Array (Int, Int) e
loop (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (((Int, Int), (Int, Int)) -> [((Int, Int), e)] -> Array (Int, Int) e
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array ((Int, Int), (Int, Int))
b [ ((Int
i,Int
j),
                           (Array (Int, Int) e
aArray (Int, Int) e -> (Int, Int) -> e
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
j)) e -> e -> e
forall a. SemiRing a => a -> a -> a
`oplus` ((Array (Int, Int) e
aArray (Int, Int) e -> (Int, Int) -> e
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
k)) e -> e -> e
forall a. SemiRing a => a -> a -> a
`otimes` (Array (Int, Int) e
aArray (Int, Int) e -> (Int, Int) -> e
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 = Array (Int, Int) e
a

-- 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)

inc :: Weight -> Int -> Weight
inc :: Weight -> Int -> Weight
inc Weight
Infinite   Int
_ = 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 Show Weight where
  show :: Weight -> String
show (Finite Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i
  show Weight
Infinite   = String
"."

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

instance SemiRing Weight where
  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)

  ozero :: Weight
ozero = Weight
Infinite
  oone :: Weight
oone  = Int -> Weight
Finite Int
0

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

-- nodes of the graph are either
-- - flexible variables (with identifiers drawn from Int),
-- - rigid variables (also identified by Ints), or
-- - constants (like 0, infinity, or anything between)

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

instance Show rigid => Show (Node rigid) where
  show :: Node rigid -> String
show (Flex  Int
i) = String
"?" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (Rigid rigid
r) = rigid -> String
forall a. Show a => a -> String
show rigid
r

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)

instance Show Rigid where
  show :: Rigid -> String
show (RVar Int
i) = String
"v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (RConst Weight
Infinite)   = String
"#"
  show (RConst (Finite Int
n)) = Int -> String
forall a. Show a => a -> String
show Int
n

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

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)
-- wether 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
_ (RConst Weight
Infinite) = Bool
True
-- isBelow (RConst Infinite)   n (RConst (Finite _)) = False
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 -> Scope
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 Constrnt edgeLabel rigid flexScope
  = NewFlex FlexId flexScope
  | Arc (Node rigid) edgeLabel (Node rigid)
-- Arc v1 k v2  at least one of v1,v2 is a VMeta (Flex),
--              the other a VMeta or a VGen (Rigid)
-- if k <= 0 this means  $^(-k) v1 <= v2
-- otherwise                    v1 <= $^k v3

type Constraint = Constrnt Weight Rigid Scope

arc :: Node Rigid -> Int -> Node Rigid -> Constraint
arc :: Node Rigid -> Int -> Node Rigid -> Constrnt Weight Rigid Scope
arc Node Rigid
a Int
k Node Rigid
b = Node Rigid -> Weight -> Node Rigid -> Constrnt Weight Rigid Scope
forall edgeLabel rigid flexScope.
Node rigid
-> edgeLabel -> Node rigid -> Constrnt edgeLabel rigid flexScope
Arc Node Rigid
a (Int -> Weight
Finite Int
k) Node Rigid
b

instance Show Constraint where
  show :: Constrnt Weight Rigid Scope -> String
show (NewFlex Int
i Scope
_) = String
"SizeMeta(?" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Arc Node Rigid
v1 (Finite Int
k) Node Rigid
v2)
    | Int
k Int -> Scope
forall a. Eq a => a -> a -> Bool
== Int
0 = Node Rigid -> String
forall a. Show a => a -> String
show Node Rigid
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node Rigid -> String
forall a. Show a => a -> String
show Node Rigid
v2
    | Int
k Int -> Scope
forall a. Ord a => a -> a -> Bool
< Int
0  = Node Rigid -> String
forall a. Show a => a -> String
show Node Rigid
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (-Int
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node Rigid -> String
forall a. Show a => a -> String
show Node Rigid
v2
    | Bool
otherwise  = Node Rigid -> String
forall a. Show a => a -> String
show Node Rigid
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node Rigid -> String
forall a. Show a => a -> String
show Node Rigid
v2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
  show Constrnt Weight Rigid Scope
_ = String
forall a. HasCallStack => a
undefined

type Constraints = [Constraint]

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

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

data Graph edgeLabel rigid flexScope = Graph
  { forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map Int flexScope
flexScope :: Map FlexId flexScope       -- scope for each flexible var
  , forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap :: Map (Node rigid) NodeId      -- node labels to node numbers
  , forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map Int (Node rigid)
intMap  :: Map NodeId (Node rigid)      -- node numbers to node labels
  , forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int
nextNode :: NodeId                      -- number of nodes (n)
  , forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int -> Int -> edgeLabel
graph :: NodeId -> NodeId -> edgeLabel  -- the edges (restrict to [0..n[)
  }

-- the empty graph: no nodes, edges are all undefined (infinity weight)
initGraph :: SemiRing edgeLabel => Graph edgeLabel rigid flexScope
initGraph :: forall edgeLabel rigid flexScope.
SemiRing edgeLabel =>
Graph edgeLabel rigid flexScope
initGraph = Map Int flexScope
-> Map (Node rigid) Int
-> Map Int (Node rigid)
-> Int
-> (Int -> Int -> edgeLabel)
-> Graph edgeLabel rigid flexScope
forall edgeLabel rigid flexScope.
Map Int flexScope
-> Map (Node rigid) Int
-> Map Int (Node rigid)
-> Int
-> (Int -> Int -> edgeLabel)
-> Graph edgeLabel rigid flexScope
Graph Map Int flexScope
forall k a. Map k a
Map.empty Map (Node rigid) Int
forall k a. Map k a
Map.empty Map Int (Node rigid)
forall k a. Map k a
Map.empty Int
0 (\ Int
_ Int
_ -> edgeLabel
forall a. SemiRing a => a
ozero)

-- the Graph Monad, for constructing a graph iteratively
type GM edgeLabel rigid flexScope = State (Graph edgeLabel rigid flexScope)

addFlex :: FlexId -> flexScope -> GM edgeLabel rigid flexScope ()
addFlex :: forall flexScope edgeLabel rigid.
Int -> flexScope -> GM edgeLabel rigid flexScope ()
addFlex Int
x flexScope
scope = do
  st <- StateT
  (Graph edgeLabel rigid flexScope)
  Identity
  (Graph edgeLabel rigid flexScope)
forall s (m :: * -> *). MonadState s m => m s
get
  put $ st { flexScope = Map.insert x scope (flexScope st) }


-- i <- addNode n  returns number of node n. if not present, it is added first
addNode :: (Eq rigid, Ord rigid) => (Node rigid) -> GM edgeLabel rigid flexScope Int
addNode :: forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid) =>
Node rigid -> GM edgeLabel rigid flexScope Int
addNode Node rigid
n = do
  st <- StateT
  (Graph edgeLabel rigid flexScope)
  Identity
  (Graph edgeLabel rigid flexScope)
forall s (m :: * -> *). MonadState s m => m s
get
  case Map.lookup n (nodeMap st) of
    Just Int
i -> Int -> StateT (Graph edgeLabel rigid flexScope) Identity Int
forall a. a -> StateT (Graph edgeLabel rigid flexScope) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
    Maybe Int
Nothing -> do let i :: Int
i = Graph edgeLabel rigid flexScope -> Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int
nextNode Graph edgeLabel rigid flexScope
st
                  Graph edgeLabel rigid flexScope
-> StateT (Graph edgeLabel rigid flexScope) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Graph edgeLabel rigid flexScope
 -> StateT (Graph edgeLabel rigid flexScope) Identity ())
-> Graph edgeLabel rigid flexScope
-> StateT (Graph edgeLabel rigid flexScope) Identity ()
forall a b. (a -> b) -> a -> b
$ Graph edgeLabel rigid flexScope
st { nodeMap = Map.insert n i (nodeMap st)
                           , intMap = Map.insert i n (intMap st)
                           , nextNode = i + 1
                           }
                  Int -> StateT (Graph edgeLabel rigid flexScope) Identity Int
forall a. a -> StateT (Graph edgeLabel rigid flexScope) 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 :: (Eq rigid, Ord rigid, SemiRing edgeLabel) => (Node rigid) -> edgeLabel -> (Node rigid) -> GM edgeLabel rigid flexScope ()
addEdge :: forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
Node rigid
-> edgeLabel -> Node rigid -> GM edgeLabel rigid flexScope ()
addEdge Node rigid
n1 edgeLabel
k Node rigid
n2 = do
  i1 <- Node rigid -> GM edgeLabel rigid flexScope Int
forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid) =>
Node rigid -> GM edgeLabel rigid flexScope Int
addNode Node rigid
n1
  i2 <- addNode n2
  st <- get
  let 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 edgeLabel
k edgeLabel -> edgeLabel -> edgeLabel
forall a. SemiRing a => a -> a -> a
`oplus` (Graph edgeLabel rigid flexScope -> Int -> Int -> edgeLabel
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int -> Int -> edgeLabel
graph Graph edgeLabel rigid flexScope
st) Int
x Int
y
                   else Graph edgeLabel rigid flexScope -> Int -> Int -> edgeLabel
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int -> Int -> edgeLabel
graph Graph edgeLabel rigid flexScope
st Int
x Int
y
  put $ st { graph = graph' }

addConstraint :: (Eq rigid, Ord rigid, SemiRing edgeLabel) =>
  Constrnt edgeLabel rigid flexScope -> GM edgeLabel rigid flexScope ()
addConstraint :: forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
Constrnt edgeLabel rigid flexScope
-> GM edgeLabel rigid flexScope ()
addConstraint (NewFlex Int
x flexScope
scope) = do
  Int -> flexScope -> GM edgeLabel rigid flexScope ()
forall flexScope edgeLabel rigid.
Int -> flexScope -> GM edgeLabel rigid flexScope ()
addFlex Int
x flexScope
scope
  Node rigid
-> edgeLabel -> Node rigid -> GM edgeLabel rigid flexScope ()
forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
Node rigid
-> edgeLabel -> Node rigid -> GM edgeLabel rigid flexScope ()
addEdge (Int -> Node rigid
forall rigid. Int -> Node rigid
Flex Int
x) edgeLabel
forall a. SemiRing a => a
oone (Int -> Node rigid
forall rigid. Int -> Node rigid
Flex Int
x) -- add dummy edge to make sure each meta variable
                              -- is in the matrix and gets solved
addConstraint (Arc Node rigid
n1 edgeLabel
k Node rigid
n2)     = Node rigid
-> edgeLabel -> Node rigid -> GM edgeLabel rigid flexScope ()
forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
Node rigid
-> edgeLabel -> Node rigid -> GM edgeLabel rigid flexScope ()
addEdge Node rigid
n1 edgeLabel
k Node rigid
n2

buildGraph :: (Eq rigid, Ord rigid, SemiRing edgeLabel) =>
  [Constrnt edgeLabel rigid flexScope] -> Graph edgeLabel rigid flexScope
buildGraph :: forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
[Constrnt edgeLabel rigid flexScope]
-> Graph edgeLabel rigid flexScope
buildGraph [Constrnt edgeLabel rigid flexScope]
cs = State (Graph edgeLabel rigid flexScope) ()
-> Graph edgeLabel rigid flexScope
-> Graph edgeLabel rigid flexScope
forall s a. State s a -> s -> s
execState ((Constrnt edgeLabel rigid flexScope
 -> State (Graph edgeLabel rigid flexScope) ())
-> [Constrnt edgeLabel rigid flexScope]
-> State (Graph edgeLabel rigid flexScope) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Constrnt edgeLabel rigid flexScope
-> State (Graph edgeLabel rigid flexScope) ()
forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
Constrnt edgeLabel rigid flexScope
-> GM edgeLabel rigid flexScope ()
addConstraint [Constrnt edgeLabel rigid flexScope]
cs) Graph edgeLabel rigid flexScope
forall edgeLabel rigid flexScope.
SemiRing edgeLabel =>
Graph edgeLabel rigid flexScope
initGraph

mkMatrix :: Int -> (Int -> Int -> a) -> Matrix a
mkMatrix :: forall a. Int -> (Int -> Int -> a) -> Matrix a
mkMatrix Int
n Int -> Int -> a
g = ((Int, Int), (Int, Int)) -> [((Int, Int), a)] -> Array (Int, Int) a
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 -> a
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 (Show a, Show b, Show c) => Show (LegendMatrix a b c) where
  show :: LegendMatrix a b c -> String
show (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 -> ShowS) -> String -> [Int] -> String
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 String
s -> String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
forall a. Show a => a -> String
show (Int -> c
cd Int
j) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) String
"" [Int
c .. Int
c'] String -> ShowS
forall a. [a] -> [a] -> [a]
++
    -- then output rows
       (Int -> ShowS) -> String -> [Int] -> String
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 String
s -> String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show (Int -> b
rd Int
i) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                (Int -> ShowS) -> String -> [Int] -> String
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 String
t -> String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Matrix a
mMatrix a -> (Int, Int) -> a
forall i e. Ix i => Array i e -> i -> e
!(Int
i,Int
j)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t)
                      (String
s)
                      [Int
c .. Int
c'])
             String
"" [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 MaxExpr

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 = ([SizeExpr] -> [SizeExpr] -> [SizeExpr])
-> Int -> [SizeExpr] -> Solution -> Solution
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [SizeExpr] -> [SizeExpr] -> [SizeExpr]
forall a. [a] -> [a] -> [a]
(++) Int
k [SizeExpr
v] Solution
subst

type MaxExpr = [SizeExpr]
-- newtype MaxExpr = MaxExpr { sizeExprs :: [SizeExpr] } deriving (Show)

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

instance Show SizeExpr where
  show :: SizeExpr -> String
show (SizeVar Int
n Int
0) = Node Rigid -> String
forall a. Show a => a -> String
show (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Int -> Rigid
RVar Int
n))
  show (SizeVar Int
n Int
k) = Node Rigid -> String
forall a. Show a => a -> String
show (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Int -> Rigid
RVar Int
n)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
  show (SizeConst (Finite Int
i)) = Int -> String
forall a. Show a => a -> String
show Int
i
  show (SizeConst Weight
Infinite)   = String
"#"

-- 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
-}

{-
solve :: Constraints -> Maybe Solution
solve cs = if any (\ x -> x < Finite 0) d then Nothing
     else Map.
   where gr = buildGraph cs
         n  = nextNode gr
         m  = mkMatrix n (graph gr)
         m' = warshall m
         d  = [ m!(i,i) | i <- [0 .. (n-1)] ]
         ns = keys (nodeMap gr)
-}

{- compute solution

a solution CANNOT exist if

  v < v  for a rigid variable v

  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


-}

solve :: Constraints -> Maybe Solution
solve :: Constraints -> Maybe Solution
solve Constraints
cs = String -> Maybe Solution -> Maybe Solution
forall a. String -> a -> a
traceSolve (LegendMatrix Weight (Node Rigid) (Node Rigid) -> String
forall a. Show a => a -> String
show LegendMatrix Weight (Node Rigid) (Node Rigid)
lm0) (Maybe Solution -> Maybe Solution)
-> Maybe Solution -> Maybe Solution
forall a b. (a -> b) -> a -> b
$ String -> Maybe Solution -> Maybe Solution
forall a. String -> a -> a
traceSolve (LegendMatrix Weight (Node Rigid) (Node Rigid) -> String
forall a. Show a => a -> String
show LegendMatrix Weight (Node Rigid) (Node Rigid)
lm) (Maybe Solution -> Maybe Solution)
-> Maybe Solution -> Maybe Solution
forall a b. (a -> b) -> a -> b
$ String -> Maybe Solution -> Maybe Solution
forall a. String -> a -> a
traceSolve (Constraints -> String
forall a. Show a => a -> String
show Constraints
cs) (Maybe Solution -> Maybe Solution)
-> Maybe Solution -> Maybe Solution
forall a b. (a -> b) -> a -> b
$
     let solution :: Maybe Solution
solution = if Bool
solvable then [Rigid] -> Solution -> Maybe Solution
loop1 [Rigid]
rigids Solution
emptySolution
                    else Maybe Solution
forall a. Maybe a
Nothing
     in String -> Maybe Solution -> Maybe Solution
forall a. String -> a -> a
traceSolve (String
"solution = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Solution -> String
forall a. Show a => a -> String
show Maybe Solution
solution) (Maybe Solution -> Maybe Solution)
-> Maybe Solution -> Maybe Solution
forall a b. (a -> b) -> a -> b
$
          Maybe Solution
solution
   where -- compute the graph and its transitive closure m
         gr :: Graph Weight Rigid Scope
gr  = Constraints -> Graph Weight Rigid Scope
forall rigid edgeLabel flexScope.
(Eq rigid, Ord rigid, SemiRing edgeLabel) =>
[Constrnt edgeLabel rigid flexScope]
-> Graph edgeLabel rigid flexScope
buildGraph Constraints
cs
         n :: Int
n   = Graph Weight Rigid Scope -> Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int
nextNode Graph Weight Rigid Scope
gr            -- number of nodes
         m0 :: Matrix Weight
m0  = Int -> (Int -> Int -> Weight) -> Matrix Weight
forall a. Int -> (Int -> Int -> a) -> Matrix a
mkMatrix Int
n (Graph Weight Rigid Scope -> Int -> Int -> Weight
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Int -> Int -> edgeLabel
graph Graph Weight Rigid Scope
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 Rigid
legend Int
i = Maybe (Node Rigid) -> Node Rigid
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Node Rigid) -> Node Rigid)
-> Maybe (Node Rigid) -> Node Rigid
forall a b. (a -> b) -> a -> b
$ Int -> Map Int (Node Rigid) -> Maybe (Node Rigid)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i (Graph Weight Rigid Scope -> Map Int (Node Rigid)
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map Int (Node rigid)
intMap Graph Weight Rigid Scope
gr) -- trace only
         lm0 :: LegendMatrix Weight (Node Rigid) (Node Rigid)
lm0 = Matrix Weight
-> (Int -> Node Rigid)
-> (Int -> Node Rigid)
-> LegendMatrix Weight (Node Rigid) (Node Rigid)
forall a b c.
Matrix a -> (Int -> b) -> (Int -> c) -> LegendMatrix a b c
LegendMatrix Matrix Weight
m0 Int -> Node Rigid
legend Int -> Node Rigid
legend            -- trace only
         lm :: LegendMatrix Weight (Node Rigid) (Node Rigid)
lm  = Matrix Weight
-> (Int -> Node Rigid)
-> (Int -> Node Rigid)
-> LegendMatrix Weight (Node Rigid) (Node Rigid)
forall a b c.
Matrix a -> (Int -> b) -> (Int -> c) -> LegendMatrix a b c
LegendMatrix Matrix Weight
m Int -> Node Rigid
legend Int -> Node Rigid
legend             -- trace only

         -- compute the sets of flexible and rigid node numbers
         ns :: [Node Rigid]
ns  = Map (Node Rigid) Int -> [Node Rigid]
forall k a. Map k a -> [k]
Map.keys (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr)
         -- a set of flexible variables
         flexs :: [Int]
flexs  = ([Int] -> Node Rigid -> [Int]) -> [Int] -> [Node Rigid] -> [Int]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ [Int]
l Node Rigid
k -> case Node Rigid
k of (Flex Int
i) -> Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
l
                                            (Rigid Rigid
_) -> [Int]
l) [] [Node Rigid]
ns
         -- a set of rigid variables
         rigids :: [Rigid]
rigids = ([Rigid] -> Node Rigid -> [Rigid])
-> [Rigid] -> [Node Rigid] -> [Rigid]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ [Rigid]
l Node Rigid
k -> case Node Rigid
k of (Flex Int
_) -> [Rigid]
l
                                            (Rigid Rigid
i) -> Rigid
i Rigid -> [Rigid] -> [Rigid]
forall a. a -> [a] -> [a]
: [Rigid]
l) [] [Node Rigid]
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
foldl (\ [Int]
l Rigid
r -> let Just Int
i = Node Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid Rigid
r) (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
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
>= Weight
forall a. SemiRing a => a
oone) [ 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
&&
-- 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
           ((Rigid, Rigid) -> Bool) -> [(Rigid, Rigid)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (Rigid
r,  Rigid
r') -> Rigid
r Rigid -> Rigid -> Bool
forall a. Eq a => a -> a -> Bool
== Rigid
r' Bool -> Bool -> Bool
||
                let Just Int
row = (Node Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid Rigid
r)  (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr))
                    Just Int
col = (Node Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid Rigid
r') (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr))
                    edge :: Weight
edge = Matrix Weight
mMatrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
!(Int
row,Int
col)
                in  Rigid -> Weight -> Rigid -> Bool
isBelow Rigid
r Weight
edge Rigid
r' )
             [ (Rigid
r,Rigid
r') | Rigid
r <- [Rigid]
rigids, Rigid
r' <- [Rigid]
rigids ]
           Bool -> Bool -> Bool
&&
-- a flexible variable might not be strictly below a rigid variable
           ((Int, Int) -> Bool) -> [(Int, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (Int
x, Int
v) ->
                let Just Int
row = (Node Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
x)  (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr))
                    Just Int
col = (Node Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Int -> Rigid
RVar Int
v)) (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr))
                    edge :: Weight
edge = Matrix Weight
mMatrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
!(Int
row,Int
col)
                in  Weight
edge Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Weight
Finite Int
0)
             [ (Int
x,Int
v) | Int
x <- [Int]
flexs, (RVar Int
v) <- [Rigid]
rigids ]

        -- UNUSED:
        --  inScope :: FlexId -> Rigid -> Bool
        --  inScope x (RConst _) = True
        --  inScope x (RVar v)   = case Map.lookup x (flexScope gr) of
        --              Just scope -> scope v
        --              Nothing    -> error $ "Warshall.inScope panic: flexible " ++ show x ++ " does not carry scope info when assigning it rigid variable " ++ show v

{- 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
        add i + n to the solution of j

-}

         loop1 :: [Rigid] -> Solution -> Maybe Solution
         loop1 :: [Rigid] -> Solution -> Maybe Solution
loop1 (Rigid
r:[Rigid]
rgds) Solution
subst = [Rigid] -> Solution -> Maybe Solution
loop1 [Rigid]
rgds 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 Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid Rigid
r) (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr)
            subst' :: Solution
subst' =
                  (Solution -> Int -> Solution) -> Solution -> [Int] -> Solution
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ 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 Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
f) (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr)
                          in  case (Bool
True -- inScope f r  -- SEEMS WRONG TO IGNORE THINGS NOT IN SCOPE
                                   , 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_z :: Int
trunc_z | Int
z Int -> Scope
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int
0
                                            | Bool
otherwise = -Int
z
                                   in Solution -> Int -> SizeExpr -> Solution
extendSolution Solution
sub Int
f (Rigid -> Int -> SizeExpr
sizeRigid Rigid
r (Int
trunc_z))
                                (Bool, Weight)
_ -> Solution
sub
                     ) Solution
subst [Int]
flexs
         loop1 [] Solution
subst = case [Int]
flexs [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ (Solution -> [Int]
forall k a. Map k a -> [k]
Map.keys Solution
subst) of
            [] -> Solution -> Maybe Solution
forall a. a -> Maybe a
Just Solution
subst
            [Int]
flexs' -> [Int] -> Solution -> Maybe Solution
loop2 [Int]
flexs' 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 -> Maybe Solution
forall a. a -> Maybe a
Just
         loop2 (Int
f:[Int]
flxs) = Int -> Solution -> Maybe Solution
loop3 Int
0
           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 Rigid -> Map (Node Rigid) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
f) (Graph Weight Rigid Scope -> Map (Node Rigid) Int
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map (Node rigid) Int
nodeMap Graph Weight Rigid Scope
gr)
                 loop3 :: Int -> Solution -> Maybe Solution
loop3 Int
col Solution
subst | Int
col Int -> Scope
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 Rigid) -> Maybe (Node Rigid)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
col (Graph Weight Rigid Scope -> Map Int (Node Rigid)
forall edgeLabel rigid flexScope.
Graph edgeLabel rigid flexScope -> Map Int (Node rigid)
intMap Graph Weight Rigid Scope
gr) of
                     Just (Rigid Rigid
r) | Bool -> Bool
not (Rigid -> Bool
infinite Rigid
r) ->
                       case (Bool
True -- inScope f 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 -> Scope
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)
_ -> Maybe Solution
forall a. Maybe a
Nothing
                     Maybe (Node Rigid)
_ -> Int -> Solution -> Maybe Solution
loop3 (Int
colInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Solution
subst