{-# OPTIONS_GHC -Wunused-imports #-}
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.Syntax.Common.Pretty as P
import Agda.Utils.Impossible
type Matrix a = Array (Int,Int) a
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
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
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Matrix a -> Matrix a) -> Matrix a -> Matrix a
forall a b. (a -> b) -> a -> b
$ ((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, Int), a)] -> Matrix a) -> [((Int, Int), a)] -> Matrix a
forall a b. (a -> b) -> a -> b
$
[ ((Int
i, Int
j), (Matrix a
a Matrix 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
a Matrix 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
a Matrix 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)]
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
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
foldr oplus Nothing [ Just v | (j', v) <- es, j == 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
(i, n) <- [(node, Int)]
nodes
let 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)]
]
return (i, es)
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)
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
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 :: 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
data Constraint
= NewFlex FlexId Scope
| Arc Node Int Node
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 = []
data Graph = Graph
{ Graph -> Map Int (Int -> Bool)
flexScope :: Map FlexId Scope
, Graph -> Map Node Int
nodeMap :: Map Node NodeId
, Graph -> Map Int Node
intMap :: Map NodeId Node
, Graph -> Int
nextNode :: NodeId
, Graph -> Int -> Int -> Weight
graph :: NodeId -> NodeId -> 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)
type GM = State Graph
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.insert x scope (flexScope st) }
_ <- Node -> GM Int
addNode (Int -> Node
Flex Int
x)
return ()
addNode :: Node -> GM Int
addNode :: Node -> GM Int
addNode Node
n = do
st <- StateT Graph Identity Graph
forall s (m :: * -> *). MonadState s m => m s
get
case Map.lookup n (nodeMap 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.insert n i (nodeMap st)
, intMap = Map.insert i n (intMap st)
, nextNode = i + 1
}
Int -> GM Int
forall a. a -> StateT Graph Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
addEdge :: Node -> Int -> Node -> GM ()
addEdge :: Node -> Int -> Node -> GM ()
addEdge Node
n1 Int
k Node
n2 = do
i1 <- Node -> GM Int
addNode Node
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 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
put $ st { graph = 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]]
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) =
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.<>
(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
m Matrix 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']
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
| SizeConst Weight
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 :: 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
solve :: Constraints -> Maybe Solution
solve :: [Constraint] -> Maybe Solution
solve [Constraint]
cs =
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
Maybe Solution
solution
where
gr :: Graph
gr = [Constraint] -> Graph
buildGraph [Constraint]
cs
n :: Int
n = Graph -> Int
nextNode Graph
gr
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
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)
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
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
ns :: [Node]
ns = Map Node Int -> [Node]
forall k a. Map k a -> [k]
Map.keys (Graph -> Map Node Int
nodeMap Graph
gr)
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
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
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
solvable :: Bool
solvable = (Weight -> Bool) -> [Weight] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Weight
Finite Int
0) [ Matrix Weight
m Matrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
! (Int
i, Int
i) | Int
i <- [Int]
rInds ]
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 :: [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
m Matrix Weight -> (Int, Int) -> Weight
forall i e. Ix i => Array i e -> i -> e
! (Int
row, Int
col)) of
(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 :: [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 =
[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
m Matrix 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
col Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Solution
subst
(Bool, Weight)
_ ->
Maybe Solution
forall a. Maybe a
Nothing
Maybe Node
_ -> Int -> Solution -> Maybe Solution
loop3 (Int
col Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Solution
subst