{-# LANGUAGE NoMonomorphismRestriction #-}
module Agda.TypeChecking.SizedTypes.WarshallSolver where
import Prelude hiding ( null, truncate )
import Control.Monad
import Data.Function (on)
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Agda.TypeChecking.SizedTypes.Syntax
import Agda.TypeChecking.SizedTypes.Utils
import Agda.Utils.Graph.AdjacencyMap.Unidirectional
(Edge(..), Nodes(..), nodes, computeNodes)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Impossible
type Graph r f a = Graph.Graph (Node r f) a
type Edge' r f a = Graph.Edge (Node r f) a
type Key r f = Edge' r f ()
type Nodes r f = Graph.Nodes (Node r f)
type LabelledEdge r f = Edge' r f Label
src :: Edge n e -> n
src :: Edge n e -> n
src = Edge n e -> n
forall n e. Edge n e -> n
Graph.source
dest :: Edge n e -> n
dest :: Edge n e -> n
dest = Edge n e -> n
forall n e. Edge n e -> n
Graph.target
lookupEdge :: Ord n => Graph.Graph n e -> n -> n -> Maybe e
lookupEdge :: Graph n e -> n -> n -> Maybe e
lookupEdge g :: Graph n e
g s :: n
s t :: n
t = n -> n -> Graph n e -> Maybe e
forall n e. Ord n => n -> n -> Graph n e -> Maybe e
Graph.lookup n
s n
t Graph n e
g
graphToList :: Graph.Graph n e -> [Edge n e]
graphToList :: Graph n e -> [Edge n e]
graphToList = Graph n e -> [Edge n e]
forall n e. Graph n e -> [Edge n e]
Graph.edges
graphFromList :: Ord n => [Edge n e] -> Graph.Graph n e
graphFromList :: [Edge n e] -> Graph n e
graphFromList = [Edge n e] -> Graph n e
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
insertEdge :: (Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph.Graph n e -> Graph.Graph n e
insertEdge :: Edge n e -> Graph n e -> Graph n e
insertEdge e :: Edge n e
e g :: Graph n e
g
| e -> Bool
forall a. Top a => a -> Bool
isTop (Edge n e -> e
forall n e. Edge n e -> e
label Edge n e
e) = Graph n e
g
| Bool
otherwise = (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
forall n e.
Ord n =>
(e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
Graph.insertEdgeWith e -> e -> e
forall a. MeetSemiLattice a => a -> a -> a
meet Edge n e
e Graph n e
g
outgoing :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
outgoing :: Graph r f a -> Node r f -> [Edge' r f a]
outgoing g :: Graph r f a
g s :: Node r f
s = Graph r f a -> [Node r f] -> [Edge' r f a]
forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesFrom Graph r f a
g [Node r f
s]
incoming :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
incoming :: Graph r f a -> Node r f -> [Edge' r f a]
incoming g :: Graph r f a
g t :: Node r f
t = Graph r f a -> [Node r f] -> [Edge' r f a]
forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesTo Graph r f a
g [Node r f
t]
setFoldl :: (b -> a -> b) -> b -> Set a -> b
setFoldl :: (b -> a -> b) -> b -> Set a -> b
setFoldl step :: b -> a -> b
step start :: b
start = (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' b -> a -> b
step b
start ([a] -> b) -> (Set a -> [a]) -> Set a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toAscList
transClos :: forall n a . (Ord n, Dioid a) => Graph.Graph n a -> Graph.Graph n a
transClos :: Graph n a -> Graph n a
transClos g :: Graph n a
g = (Graph n a -> n -> Graph n a) -> Graph n a -> Set n -> Graph n a
forall b a. (b -> a -> b) -> b -> Set a -> b
setFoldl Graph n a -> n -> Graph n a
forall e. Dioid e => Graph n e -> n -> Graph n e
step Graph n a
g (Set n -> Graph n a) -> Set n -> Graph n a
forall a b. (a -> b) -> a -> b
$ Nodes n -> Set n
forall n. Nodes n -> Set n
allNodes Nodes n
ns
where
ns :: Nodes n
ns = Graph n a -> Nodes n
forall n e. Ord n => Graph n e -> Nodes n
computeNodes Graph n a
g
srcs :: [n]
srcs = Set n -> [n]
forall a. Set a -> [a]
Set.toAscList (Set n -> [n]) -> Set n -> [n]
forall a b. (a -> b) -> a -> b
$ Nodes n -> Set n
forall n. Nodes n -> Set n
srcNodes Nodes n
ns
dests :: [n]
dests = Set n -> [n]
forall a. Set a -> [a]
Set.toAscList (Set n -> [n]) -> Set n -> [n]
forall a b. (a -> b) -> a -> b
$ Nodes n -> Set n
forall n. Nodes n -> Set n
tgtNodes Nodes n
ns
step :: Graph n e -> n -> Graph n e
step g :: Graph n e
g v :: n
v = (Graph n e -> Edge n e -> Graph n e)
-> Graph n e -> [Edge n e] -> Graph n e
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Edge n e -> Graph n e -> Graph n e)
-> Graph n e -> Edge n e -> Graph n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Edge n e -> Graph n e -> Graph n e
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph n e
g ([Edge n e] -> Graph n e) -> [Edge n e] -> Graph n e
forall a b. (a -> b) -> a -> b
$
[ n -> n -> e -> Edge n e
forall n e. n -> n -> e -> Edge n e
Edge n
u n
w (e -> Edge n e) -> e -> Edge n e
forall a b. (a -> b) -> a -> b
$ e
l1 e -> e -> e
forall a. Dioid a => a -> a -> a
`compose` e
l2
| n
u <- [n]
srcs
, n
w <- [n]
dests
, e
l1 <- Maybe e -> [e]
forall a. Maybe a -> [a]
maybeToList (Maybe e -> [e]) -> Maybe e -> [e]
forall a b. (a -> b) -> a -> b
$ Graph n e -> n -> n -> Maybe e
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n e
g n
u n
v
, e
l2 <- Maybe e -> [e]
forall a. Maybe a -> [a]
maybeToList (Maybe e -> [e]) -> Maybe e -> [e]
forall a b. (a -> b) -> a -> b
$ Graph n e -> n -> n -> Maybe e
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n e
g n
v n
w
]
data Weight
= Offset Offset
| Infinity
deriving (Weight -> Weight -> Bool
(Weight -> Weight -> Bool)
-> (Weight -> Weight -> Bool) -> Eq Weight
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Weight -> Weight -> Bool
$c/= :: Weight -> Weight -> Bool
== :: Weight -> Weight -> Bool
$c== :: Weight -> Weight -> Bool
Eq, Int -> Weight -> ShowS
[Weight] -> ShowS
Weight -> String
(Int -> Weight -> ShowS)
-> (Weight -> String) -> ([Weight] -> ShowS) -> Show Weight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Weight] -> ShowS
$cshowList :: [Weight] -> ShowS
show :: Weight -> String
$cshow :: Weight -> String
showsPrec :: Int -> Weight -> ShowS
$cshowsPrec :: Int -> Weight -> ShowS
Show)
instance Pretty Weight where
pretty :: Weight -> Doc
pretty (Offset x :: Offset
x) = Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
x
pretty Infinity = "∞"
instance Ord Weight where
x :: Weight
x <= :: Weight -> Weight -> Bool
<= Infinity = Bool
True
Infinity <= y :: Weight
y = Bool
False
Offset x :: Offset
x <= Offset y :: Offset
y = Offset
x Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
y
instance MeetSemiLattice Weight where
meet :: Weight -> Weight -> Weight
meet = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
min
instance Top Weight where
top :: Weight
top = Weight
Infinity
instance Enum Weight where
succ :: Weight -> Weight
succ (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Offset
forall a. Enum a => a -> a
succ Offset
x)
succ (Weight
Infinity) = Weight
Infinity
pred :: Weight -> Weight
pred (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Offset
forall a. Enum a => a -> a
pred Offset
x)
pred (Weight
Infinity) = Weight
Infinity
toEnum :: Int -> Weight
toEnum = Offset -> Weight
Offset (Offset -> Weight) -> (Int -> Offset) -> Int -> Weight
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Offset
forall a. Enum a => Int -> a
toEnum
fromEnum :: Weight -> Int
fromEnum (Offset x :: Offset
x) = Offset -> Int
forall a. Enum a => a -> Int
fromEnum Offset
x
fromEnum (Weight
Infinity) = Int
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Num Weight where
Infinity + :: Weight -> Weight -> Weight
+ y :: Weight
y = Weight
Infinity
x :: Weight
x + Infinity = Weight
Infinity
Offset x :: Offset
x + Offset y :: Offset
y = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset
x Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
y
Infinity - :: Weight -> Weight -> Weight
- Offset y :: Offset
y = Weight
Infinity
Offset x :: Offset
x - Offset y :: Offset
y = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset
x Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
y
x :: Weight
x - Infinity = Weight
forall a. HasCallStack => a
__IMPOSSIBLE__
abs :: Weight -> Weight
abs (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Num a => a -> a
abs Offset
x
abs Infinity = Weight
Infinity
signum :: Weight -> Weight
signum (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Num a => a -> a
signum Offset
x
signum Infinity = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ 1
fromInteger :: Integer -> Weight
fromInteger x :: Integer
x = Offset -> Weight
Offset (Integer -> Offset
forall a. Num a => Integer -> a
fromInteger Integer
x)
x :: Weight
x * :: Weight -> Weight -> Weight
* y :: Weight
y = Weight
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Plus Weight Offset Weight where
plus :: Weight -> Offset -> Weight
plus w :: Weight
w k :: Offset
k = Weight
w Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
+ (Offset -> Weight
Offset Offset
k)
class Negative a where
negative :: a -> Bool
instance Negative Int where
negative :: Int -> Bool
negative = (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0)
instance Negative Offset where
negative :: Offset -> Bool
negative (O x :: Int
x) = Int -> Bool
forall a. Negative a => a -> Bool
negative Int
x
instance Negative Weight where
negative :: Weight -> Bool
negative Infinity = Bool
False
negative (Offset x :: Offset
x) = Offset -> Bool
forall a. Negative a => a -> Bool
negative Offset
x
data Label
= Label { Label -> Cmp
lcmp :: Cmp, Label -> Offset
loffset :: Offset }
| LInf
deriving (Int -> Label -> ShowS
[Label] -> ShowS
Label -> String
(Int -> Label -> ShowS)
-> (Label -> String) -> ([Label] -> ShowS) -> Show Label
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Label] -> ShowS
$cshowList :: [Label] -> ShowS
show :: Label -> String
$cshow :: Label -> String
showsPrec :: Int -> Label -> ShowS
$cshowsPrec :: Int -> Label -> ShowS
Show)
toWeight :: Label -> Weight
toWeight :: Label -> Weight
toWeight (Label Le w :: Offset
w) = Offset -> Weight
Offset Offset
w
toWeight (Label Lt w :: Offset
w) = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Enum a => a -> a
pred Offset
w
toWeight LInf = Weight
Infinity
instance Negative Label where
negative :: Label -> Bool
negative = Weight -> Bool
forall a. Negative a => a -> Bool
negative (Weight -> Bool) -> (Label -> Weight) -> Label -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> Weight
toWeight
instance Eq Label where
Label cmp :: Cmp
cmp w :: Offset
w == :: Label -> Label -> Bool
== Label cmp' :: Cmp
cmp' w' :: Offset
w' = Cmp
cmp Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
cmp' Bool -> Bool -> Bool
&& Offset
w Offset -> Offset -> Bool
forall a. Eq a => a -> a -> Bool
== Offset
w'
LInf == LInf = Bool
True
_ == _ = Bool
False
instance Ord Label where
Label Lt w :: Offset
w <= :: Label -> Label -> Bool
<= Label Lt w' :: Offset
w' = Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
Label Le w :: Offset
w <= Label Le w' :: Offset
w' = Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
Label Lt w :: Offset
w <= Label Le w' :: Offset
w' = Offset -> Offset
forall a. Enum a => a -> a
pred Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
Label Le w :: Offset
w <= Label Lt w' :: Offset
w' = Offset -> Offset
forall a. Enum a => a -> a
succ Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
_ <= LInf = Bool
True
LInf{} <= Label{} = Bool
False
instance Pretty Label where
pretty :: Label -> Doc
pretty (Label cmp :: Cmp
cmp w :: Offset
w) = Cmp -> Doc
forall a. Pretty a => a -> Doc
pretty Cmp
cmp Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
w
pretty LInf = "∞"
instance MeetSemiLattice Label where
LInf meet :: Label -> Label -> Label
`meet` l :: Label
l = Label
l
l :: Label
l `meet` LInf = Label
l
Label Lt w :: Offset
w `meet` Label Lt w' :: Offset
w' = Cmp -> Offset -> Label
Label Cmp
Lt (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. MeetSemiLattice a => a -> a -> a
`meet` Offset
w'
Label Le w :: Offset
w `meet` Label Le w' :: Offset
w' = Cmp -> Offset -> Label
Label Cmp
Le (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. MeetSemiLattice a => a -> a -> a
`meet` Offset
w'
Label Lt w :: Offset
w `meet` Label Le w' :: Offset
w' = Cmp -> Offset -> Label
Label Cmp
Lt (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. MeetSemiLattice a => a -> a -> a
`meet` Offset -> Offset
forall a. Enum a => a -> a
succ Offset
w'
Label Le w :: Offset
w `meet` Label Lt w' :: Offset
w' = Cmp -> Offset -> Label
Label Cmp
Lt (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Enum a => a -> a
succ Offset
w Offset -> Offset -> Offset
forall a. MeetSemiLattice a => a -> a -> a
`meet` Offset
w'
instance Top Label where
top :: Label
top = Label
LInf
isTop :: Label -> Bool
isTop Label{} = Bool
False
isTop LInf = Bool
True
instance Dioid Weight where
compose :: Weight -> Weight -> Weight
compose = Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
(+)
unitCompose :: Weight
unitCompose = 0
instance Dioid Label where
compose :: Label -> Label -> Label
compose (Label Lt w :: Offset
w) (Label Lt w' :: Offset
w') = Cmp -> Offset -> Label
Label Cmp
Lt (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Enum a => a -> a
pred (Offset -> Offset) -> Offset -> Offset
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
w'
compose (Label cmp :: Cmp
cmp w :: Offset
w) (Label cmp' :: Cmp
cmp' w' :: Offset
w') = Cmp -> Offset -> Label
Label (Cmp -> Cmp -> Cmp
forall a. Dioid a => a -> a -> a
compose Cmp
cmp Cmp
cmp') (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
w'
compose _ LInf = Label
LInf
compose LInf _ = Label
LInf
unitCompose :: Label
unitCompose = Cmp -> Offset -> Label
Label Cmp
Le 0
data Node rigid flex
= NodeZero
| NodeInfty
| NodeRigid rigid
| NodeFlex flex
deriving (Int -> Node rigid flex -> ShowS
[Node rigid flex] -> ShowS
Node rigid flex -> String
(Int -> Node rigid flex -> ShowS)
-> (Node rigid flex -> String)
-> ([Node rigid flex] -> ShowS)
-> Show (Node rigid flex)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
showList :: [Node rigid flex] -> ShowS
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
show :: Node rigid flex -> String
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
showsPrec :: Int -> Node rigid flex -> ShowS
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
Show, Node rigid flex -> Node rigid flex -> Bool
(Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> Eq (Node rigid flex)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
/= :: Node rigid flex -> Node rigid flex -> Bool
$c/= :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
== :: Node rigid flex -> Node rigid flex -> Bool
$c== :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
Eq, Eq (Node rigid flex)
Eq (Node rigid flex) =>
(Node rigid flex -> Node rigid flex -> Ordering)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Node rigid flex)
-> (Node rigid flex -> Node rigid flex -> Node rigid flex)
-> Ord (Node rigid flex)
Node rigid flex -> Node rigid flex -> Bool
Node rigid flex -> Node rigid flex -> Ordering
Node rigid flex -> Node rigid flex -> Node rigid flex
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 flex. (Ord rigid, Ord flex) => Eq (Node rigid flex)
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
min :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmin :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
max :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmax :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
>= :: Node rigid flex -> Node rigid flex -> Bool
$c>= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
> :: Node rigid flex -> Node rigid flex -> Bool
$c> :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
<= :: Node rigid flex -> Node rigid flex -> Bool
$c<= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
< :: Node rigid flex -> Node rigid flex -> Bool
$c< :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
compare :: Node rigid flex -> Node rigid flex -> Ordering
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
$cp1Ord :: forall rigid flex. (Ord rigid, Ord flex) => Eq (Node rigid flex)
Ord)
instance (Pretty rigid, Pretty flex) => Pretty (Node rigid flex) where
pretty :: Node rigid flex -> Doc
pretty NodeZero = "0"
pretty NodeInfty = "∞"
pretty (NodeRigid x :: rigid
x) = rigid -> Doc
forall a. Pretty a => a -> Doc
pretty rigid
x
pretty (NodeFlex x :: flex
x) = flex -> Doc
forall a. Pretty a => a -> Doc
pretty flex
x
isFlexNode :: Node rigid flex -> Maybe flex
isFlexNode :: Node rigid flex -> Maybe flex
isFlexNode (NodeFlex x :: flex
x) = flex -> Maybe flex
forall a. a -> Maybe a
Just flex
x
isFlexNode _ = Maybe flex
forall a. Maybe a
Nothing
isZeroNode :: Node rigid flex -> Bool
isZeroNode :: Node rigid flex -> Bool
isZeroNode NodeZero{} = Bool
True
isZeroNode _ = Bool
False
isInftyNode :: Node rigid flex -> Bool
isInftyNode :: Node rigid flex -> Bool
isInftyNode NodeInfty{} = Bool
True
isInftyNode _ = Bool
False
nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr n :: Node rigid flex
n =
case Node rigid flex
n of
NodeZero -> Offset -> SizeExpr' rigid flex
forall rigid flex. Offset -> SizeExpr' rigid flex
Const 0
NodeInfty -> SizeExpr' rigid flex
forall rigid flex. SizeExpr' rigid flex
Infty
NodeRigid i :: rigid
i -> rigid -> Offset -> SizeExpr' rigid flex
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid rigid
i 0
NodeFlex x :: flex
x -> flex -> Offset -> SizeExpr' rigid flex
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex flex
x 0
instance Negative a => Negative (Edge' r f a) where
negative :: Edge' r f a -> Bool
negative = a -> Bool
forall a. Negative a => a -> Bool
negative (a -> Bool) -> (Edge' r f a -> a) -> Edge' r f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge' r f a -> a
forall n e. Edge n e -> e
label
instance (Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) where
e :: Edge' r f a
e@(Edge u :: Node r f
u v :: Node r f
v l :: a
l) meet :: Edge' r f a -> Edge' r f a -> Edge' r f a
`meet` e' :: Edge' r f a
e'@(Edge u' :: Node r f
u' v' :: Node r f
v' l' :: a
l')
| Node r f
u Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
u' Bool -> Bool -> Bool
&& Node r f
v Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
v' = Node r f -> Node r f -> a -> Edge' r f a
forall n e. n -> n -> e -> Edge n e
Edge Node r f
u Node r f
v (a -> Edge' r f a) -> a -> Edge' r f a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
`meet` a
l'
| Bool
otherwise = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
instance (Ord r, Ord f, Top a) => Top (Edge' r f a) where
top :: Edge' r f a
top = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
isTop :: Edge' r f a -> Bool
isTop e :: Edge' r f a
e = a -> Bool
forall a. Top a => a -> Bool
isTop (Edge' r f a -> a
forall n e. Edge n e -> e
label Edge' r f a
e)
instance (Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) where
e :: Edge' r f a
e@(Edge u :: Node r f
u v :: Node r f
v l :: a
l) compose :: Edge' r f a -> Edge' r f a -> Edge' r f a
`compose` e' :: Edge' r f a
e'@(Edge v' :: Node r f
v' w :: Node r f
w l' :: a
l')
| Node r f
v Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
v' = Node r f -> Node r f -> a -> Edge' r f a
forall n e. n -> n -> e -> Edge n e
Edge Node r f
u Node r f
w (a -> Edge' r f a) -> a -> Edge' r f a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Dioid a => a -> a -> a
`compose` a
l'
| Bool
otherwise = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
unitCompose :: Edge' r f a
unitCompose = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
type Graphs r f a = [Graph r f a]
emptyGraphs :: Graphs r f a
emptyGraphs :: Graphs r f a
emptyGraphs = []
mentions :: (Ord r, Ord f) => Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions :: Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions NodeZero gs :: Graphs r f a
gs = ([], Graphs r f a
gs)
mentions NodeInfty gs :: Graphs r f a
gs = ([], Graphs r f a
gs)
mentions NodeRigid{} gs :: Graphs r f a
gs = ([], Graphs r f a
gs)
mentions n :: Node r f
n gs :: Graphs r f a
gs = (Graph (Node r f) a -> Bool)
-> Graphs r f a -> (Graphs r f a, Graphs r f a)
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Node r f -> Set (Node r f) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Node r f
n (Set (Node r f) -> Bool)
-> (Graph (Node r f) a -> Set (Node r f))
-> Graph (Node r f) a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph (Node r f) a -> Set (Node r f)
forall n e. Graph n e -> Set n
nodes) Graphs r f a
gs
addEdge :: (Ord r, Ord f, MeetSemiLattice a, Top a) => Edge' r f a -> Graphs r f a -> Graphs r f a
addEdge :: Edge' r f a -> Graphs r f a -> Graphs r f a
addEdge e :: Edge' r f a
e@(Edge src :: Node r f
src dest :: Node r f
dest l :: a
l) gs :: Graphs r f a
gs =
let (gsSrc :: Graphs r f a
gsSrc , gsNotSrc :: Graphs r f a
gsNotSrc) = Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
forall r f a.
(Ord r, Ord f) =>
Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions Node r f
src Graphs r f a
gs
(gsDest :: Graphs r f a
gsDest, gsNotDest :: Graphs r f a
gsNotDest) = Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
forall r f a.
(Ord r, Ord f) =>
Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions Node r f
dest Graphs r f a
gsNotSrc
in Edge' r f a -> Graph (Node r f) a -> Graph (Node r f) a
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge Edge' r f a
e ((a -> a -> a) -> Graphs r f a -> Graph (Node r f) a
forall n e. Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
Graph.unionsWith a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
meet (Graphs r f a -> Graph (Node r f) a)
-> Graphs r f a -> Graph (Node r f) a
forall a b. (a -> b) -> a -> b
$ Graphs r f a
gsSrc Graphs r f a -> Graphs r f a -> Graphs r f a
forall a. [a] -> [a] -> [a]
++ Graphs r f a
gsDest) Graph (Node r f) a -> Graphs r f a -> Graphs r f a
forall a. a -> [a] -> [a]
: Graphs r f a
gsNotDest
reflClos :: (Ord r, Ord f, Dioid a) => Set (Node r f) -> Graph r f a -> Graph r f a
reflClos :: Set (Node r f) -> Graph r f a -> Graph r f a
reflClos ns :: Set (Node r f)
ns g :: Graph r f a
g = (Graph r f a -> Node r f -> Graph r f a)
-> Graph r f a -> Set (Node r f) -> Graph r f a
forall b a. (b -> a -> b) -> b -> Set a -> b
setFoldl Graph r f a -> Node r f -> Graph r f a
forall rigid flex e.
(Ord rigid, Ord flex, Dioid e) =>
Graph (Node rigid flex) e
-> Node rigid flex -> Graph (Node rigid flex) e
step Graph r f a
g Set (Node r f)
ns' where
ns' :: Set (Node r f)
ns' = Graph r f a -> Set (Node r f)
forall n e. Graph n e -> Set n
nodes Graph r f a
g Set (Node r f) -> Set (Node r f) -> Set (Node r f)
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (Node r f)
ns
step :: Graph (Node rigid flex) e
-> Node rigid flex -> Graph (Node rigid flex) e
step g :: Graph (Node rigid flex) e
g n :: Node rigid flex
n = (Graph (Node rigid flex) e
-> Edge (Node rigid flex) e -> Graph (Node rigid flex) e)
-> Graph (Node rigid flex) e
-> [Edge (Node rigid flex) e]
-> Graph (Node rigid flex) e
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Edge (Node rigid flex) e
-> Graph (Node rigid flex) e -> Graph (Node rigid flex) e)
-> Graph (Node rigid flex) e
-> Edge (Node rigid flex) e
-> Graph (Node rigid flex) e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Edge (Node rigid flex) e
-> Graph (Node rigid flex) e -> Graph (Node rigid flex) e
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph (Node rigid flex) e
g [Edge (Node rigid flex) e]
forall e. Dioid e => [Edge (Node rigid flex) e]
es where
es :: [Edge (Node rigid flex) e]
es = [ Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
forall rigid flex. Node rigid flex
NodeZero Node rigid flex
n e
forall a. Dioid a => a
unitCompose
, Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
n Node rigid flex
n e
forall a. Dioid a => a
unitCompose
, Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
n Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty e
forall a. Dioid a => a
unitCompose
]
instance (Ord r, Ord f, Negative a) => Negative (Graph r f a) where
negative :: Graph r f a -> Bool
negative = (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Edge (Node r f) a -> Bool
forall a. Negative a => a -> Bool
negative ([Edge (Node r f) a] -> Bool)
-> (Graph r f a -> [Edge (Node r f) a]) -> Graph r f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph r f a -> [Edge (Node r f) a]
forall n e. Ord n => Graph n e -> [Edge n e]
Graph.diagonal
instance (Ord r, Ord f, Negative a) => Negative (Graphs r f a) where
negative :: Graphs r f a -> Bool
negative = (Graph r f a -> Bool) -> Graphs r f a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Graph r f a -> Bool
forall a. Negative a => a -> Bool
negative
implies :: (Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a, Negative a)
=> Graph r f a -> Graph r f a -> Bool
implies :: Graph r f a -> Graph r f a -> Bool
implies h :: Graph r f a
h g :: Graph r f a
g = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Edge (Node r f) a -> Bool
test ([Edge (Node r f) a] -> [Bool]) -> [Edge (Node r f) a] -> [Bool]
forall a b. (a -> b) -> a -> b
$ Graph r f a -> [Edge (Node r f) a]
forall n e. Graph n e -> [Edge n e]
graphToList Graph r f a
g
where
test :: Edge (Node r f) a -> Bool
test k :: Edge (Node r f) a
k@(Edge src :: Node r f
src dest :: Node r f
dest l :: a
l)
| Node r f -> Bool
forall rigid flex. Node rigid flex -> Bool
isZeroNode Node r f
src, Bool -> Bool
not (a -> Bool
forall a. Negative a => a -> Bool
negative a
l) = Bool
True
| Node r f -> Bool
forall rigid flex. Node rigid flex -> Bool
isInftyNode Node r f
dest = Bool
True
| Maybe f -> Bool
forall a. Maybe a -> Bool
isJust (Maybe f -> Bool) -> Maybe f -> Bool
forall a b. (a -> b) -> a -> b
$ Node r f -> Maybe f
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode Node r f
src = Bool
True
| Maybe f -> Bool
forall a. Maybe a -> Bool
isJust (Maybe f -> Bool) -> Maybe f -> Bool
forall a b. (a -> b) -> a -> b
$ Node r f -> Maybe f
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode Node r f
dest = Bool
True
| a -> Bool
forall a. Top a => a -> Bool
isTop a
l = Bool
True
| Bool
otherwise = case Graph r f a -> Node r f -> Node r f -> Maybe a
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph r f a
h Node r f
src Node r f
dest of
Nothing -> Bool
False
Just l' :: a
l' -> if a
l' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
l then Bool
True else
String -> Bool -> Bool
forall a. String -> a -> a
trace ("edge " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Edge (Node r f) a -> String
forall a. Pretty a => a -> String
prettyShow (a
l a -> Edge (Node r f) a -> Edge (Node r f) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Edge (Node r f) a
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not implied by " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Edge (Node r f) a -> String
forall a. Pretty a => a -> String
prettyShow (a
l' a -> Edge (Node r f) a -> Edge (Node r f) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Edge (Node r f) a
k)) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
Bool
False
nodeFromSizeExpr :: SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr :: SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr e :: SizeExpr' rigid flex
e = case SizeExpr' rigid flex
e of
Const n :: Offset
n -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeZero , Offset
n)
Rigid i :: rigid
i n :: Offset
n -> (rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid rigid
i, Offset
n)
Flex x :: flex
x n :: Offset
n -> (flex -> Node rigid flex
forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x , Offset
n)
Infty -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty , 0)
edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint (Constraint lexp :: SizeExpr' rigid flex
lexp cmp :: Cmp
cmp rexp :: SizeExpr' rigid flex
rexp) =
let (leftNode :: Node rigid flex
leftNode , n :: Offset
n) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
lexp
(rightNode :: Node rigid flex
rightNode, m :: Offset
m) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
rexp
in Node rigid flex
-> Node rigid flex -> Label -> LabelledEdge rigid flex
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
leftNode Node rigid flex
rightNode (Cmp -> Offset -> Label
Label Cmp
cmp (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n)
graphFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints :: [Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints cs :: [Constraint' rigid flex]
cs =
let
edges :: [LabelledEdge rigid flex]
edges = (Constraint' rigid flex -> LabelledEdge rigid flex)
-> [Constraint' rigid flex] -> [LabelledEdge rigid flex]
forall a b. (a -> b) -> [a] -> [b]
map Constraint' rigid flex -> LabelledEdge rigid flex
forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint [Constraint' rigid flex]
cs
g :: Graph rigid flex Label
g = (Graph rigid flex Label
-> LabelledEdge rigid flex -> Graph rigid flex Label)
-> Graph rigid flex Label
-> [LabelledEdge rigid flex]
-> Graph rigid flex Label
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((LabelledEdge rigid flex
-> Graph rigid flex Label -> Graph rigid flex Label)
-> Graph rigid flex Label
-> LabelledEdge rigid flex
-> Graph rigid flex Label
forall a b c. (a -> b -> c) -> b -> a -> c
flip LabelledEdge rigid flex
-> Graph rigid flex Label -> Graph rigid flex Label
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph rigid flex Label
forall n e. Graph n e
Graph.empty [LabelledEdge rigid flex]
edges
in Graph rigid flex Label
g
graphsFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints :: [Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints cs :: [Constraint' rigid flex]
cs =
let
edges :: [LabelledEdge rigid flex]
edges = (Constraint' rigid flex -> LabelledEdge rigid flex)
-> [Constraint' rigid flex] -> [LabelledEdge rigid flex]
forall a b. (a -> b) -> [a] -> [b]
map Constraint' rigid flex -> LabelledEdge rigid flex
forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint [Constraint' rigid flex]
cs
xs :: [flex]
xs = Set flex -> [flex]
forall a. Set a -> [a]
Set.toList (Set flex -> [flex]) -> Set flex -> [flex]
forall a b. (a -> b) -> a -> b
$ [Constraint' rigid flex] -> Set flex
forall flex a. Flexs flex a => a -> Set flex
flexs [Constraint' rigid flex]
cs
fedges :: [Edge (Node rigid flex) Label]
fedges = [[Edge (Node rigid flex) Label]] -> [Edge (Node rigid flex) Label]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Edge (Node rigid flex) Label]]
-> [Edge (Node rigid flex) Label])
-> [[Edge (Node rigid flex) Label]]
-> [Edge (Node rigid flex) Label]
forall a b. (a -> b) -> a -> b
$ [flex]
-> (flex -> [Edge (Node rigid flex) Label])
-> [[Edge (Node rigid flex) Label]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [flex]
xs ((flex -> [Edge (Node rigid flex) Label])
-> [[Edge (Node rigid flex) Label]])
-> (flex -> [Edge (Node rigid flex) Label])
-> [[Edge (Node rigid flex) Label]]
forall a b. (a -> b) -> a -> b
$ \ x :: flex
x ->
[ Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
forall rigid flex. Node rigid flex
NodeZero (flex -> Node rigid flex
forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x) (Cmp -> Offset -> Label
Label Cmp
Le 0)
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Edge (flex -> Node rigid flex
forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x) Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty (Cmp -> Offset -> Label
Label Cmp
Le 0)
]
gs :: Graphs rigid flex Label
gs = (Graphs rigid flex Label
-> LabelledEdge rigid flex -> Graphs rigid flex Label)
-> Graphs rigid flex Label
-> [LabelledEdge rigid flex]
-> Graphs rigid flex Label
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((LabelledEdge rigid flex
-> Graphs rigid flex Label -> Graphs rigid flex Label)
-> Graphs rigid flex Label
-> LabelledEdge rigid flex
-> Graphs rigid flex Label
forall a b c. (a -> b -> c) -> b -> a -> c
flip LabelledEdge rigid flex
-> Graphs rigid flex Label -> Graphs rigid flex Label
forall r f a.
(Ord r, Ord f, MeetSemiLattice a, Top a) =>
Edge' r f a -> Graphs r f a -> Graphs r f a
addEdge) Graphs rigid flex Label
forall r f a. Graphs r f a
emptyGraphs ([LabelledEdge rigid flex]
forall rigid. [Edge (Node rigid flex) Label]
fedges [LabelledEdge rigid flex]
-> [LabelledEdge rigid flex] -> [LabelledEdge rigid flex]
forall a. [a] -> [a] -> [a]
++ [LabelledEdge rigid flex]
edges)
in Graphs rigid flex Label
gs
type Hyp = Constraint
type Hyp' = Constraint'
type HypGraph r f = Graph r f Label
hypGraph :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
Set rigid -> [Hyp' rigid flex] -> Either String (HypGraph rigid flex)
hypGraph :: Set rigid
-> [Hyp' rigid flex] -> Either String (HypGraph rigid flex)
hypGraph is :: Set rigid
is hyps0 :: [Hyp' rigid flex]
hyps0 = do
[Hyp' rigid flex]
hyps <- [[Hyp' rigid flex]] -> [Hyp' rigid flex]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Hyp' rigid flex]] -> [Hyp' rigid flex])
-> Either String [[Hyp' rigid flex]]
-> Either String [Hyp' rigid flex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Hyp' rigid flex -> Either String [Hyp' rigid flex])
-> [Hyp' rigid flex] -> Either String [[Hyp' rigid flex]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Hyp' rigid flex -> Either String [Hyp' rigid flex])
-> Hyp' rigid flex -> Either String [Hyp' rigid flex]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 ((Hyp' rigid flex -> Either String [Hyp' rigid flex])
-> Hyp' rigid flex -> Either String [Hyp' rigid flex])
-> (Hyp' rigid flex -> Either String [Hyp' rigid flex])
-> Hyp' rigid flex
-> Either String [Hyp' rigid flex]
forall a b. (a -> b) -> a -> b
$ \ c :: Hyp' rigid flex
c -> [Hyp' rigid flex] -> Either String [Hyp' rigid flex]
forall (m :: * -> *) a. Monad m => a -> m a
return [Hyp' rigid flex
c]) [Hyp' rigid flex]
hyps0
let g :: HypGraph rigid flex
g = HypGraph rigid flex -> HypGraph rigid flex
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos (HypGraph rigid flex -> HypGraph rigid flex)
-> HypGraph rigid flex -> HypGraph rigid flex
forall a b. (a -> b) -> a -> b
$
Set (Node rigid flex) -> HypGraph rigid flex -> HypGraph rigid flex
forall r f a.
(Ord r, Ord f, Dioid a) =>
Set (Node r f) -> Graph r f a -> Graph r f a
reflClos ((rigid -> Node rigid flex) -> Set rigid -> Set (Node rigid flex)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid Set rigid
is) (HypGraph rigid flex -> HypGraph rigid flex)
-> HypGraph rigid flex -> HypGraph rigid flex
forall a b. (a -> b) -> a -> b
$
[Hyp' rigid flex] -> HypGraph rigid flex
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Hyp' rigid flex]
hyps
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HypGraph rigid flex -> Bool
forall a. Negative a => a -> Bool
negative HypGraph rigid flex
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left "size hypotheses graph has negative loop"
HypGraph rigid flex -> Either String (HypGraph rigid flex)
forall (m :: * -> *) a. Monad m => a -> m a
return HypGraph rigid flex
g
hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label
hypConn :: HypGraph r f -> Node r f -> Node r f -> Label
hypConn hg :: HypGraph r f
hg n1 :: Node r f
n1 n2 :: Node r f
n2
| Node r f
n1 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n2 = Cmp -> Offset -> Label
Label Cmp
Le 0
| Just l :: Label
l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n1 Node r f
n2 = Label
l
| Bool
otherwise = Label
forall a. Top a => a
top
simplifyWithHypotheses :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex -> [Constraint' rigid flex] -> Either String [Constraint' rigid flex]
simplifyWithHypotheses :: HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either String [Constraint' rigid flex]
simplifyWithHypotheses hg :: HypGraph rigid flex
hg cons :: [Constraint' rigid flex]
cons = [[Constraint' rigid flex]] -> [Constraint' rigid flex]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constraint' rigid flex]] -> [Constraint' rigid flex])
-> Either String [[Constraint' rigid flex]]
-> Either String [Constraint' rigid flex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint' rigid flex -> Either String [Constraint' rigid flex])
-> [Constraint' rigid flex]
-> Either String [[Constraint' rigid flex]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Constraint' rigid flex -> Either String [Constraint' rigid flex])
-> Constraint' rigid flex -> Either String [Constraint' rigid flex]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 Constraint' rigid flex -> Either String [Constraint' rigid flex]
test) [Constraint' rigid flex]
cons
where
test :: Constraint' rigid flex -> Either String [Constraint' rigid flex]
test c :: Constraint' rigid flex
c = do
let Edge n1 :: Node rigid flex
n1 n2 :: Node rigid flex
n2 l :: Label
l = Constraint' rigid flex -> Edge (Node rigid flex) Label
forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint Constraint' rigid flex
c
l' :: Label
l' = HypGraph rigid flex -> Node rigid flex -> Node rigid flex -> Label
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> Node r f -> Node r f -> Label
hypConn HypGraph rigid flex
hg Node rigid flex
n1 Node rigid flex
n2
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Label
l' Label -> Label -> Bool
forall a. Ord a => a -> a -> Bool
<= Label
l) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
"size constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Constraint' rigid flex -> String
forall a. Pretty a => a -> String
prettyShow Constraint' rigid flex
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not consistent with size hypotheses"
[Constraint' rigid flex] -> Either String [Constraint' rigid flex]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' rigid flex
c]
type ConGraph r f = Graph r f Label
constraintGraph :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either String (ConGraph r f)
constraintGraph :: [Constraint' r f] -> HypGraph r f -> Either String (HypGraph r f)
constraintGraph cons0 :: [Constraint' r f]
cons0 hg :: HypGraph r f
hg = do
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "original constraints cons0 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons0
[Constraint' r f]
cons <- HypGraph r f
-> [Constraint' r f] -> Either String [Constraint' r f]
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either String [Constraint' rigid flex]
simplifyWithHypotheses HypGraph r f
hg [Constraint' r f]
cons0
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "simplified constraints cons = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons
let g :: HypGraph r f
g = HypGraph r f -> HypGraph r f
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos (HypGraph r f -> HypGraph r f) -> HypGraph r f -> HypGraph r f
forall a b. (a -> b) -> a -> b
$ [Constraint' r f] -> HypGraph r f
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cons
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "transitive graph g = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Edge (Node r f) Label] -> String
forall a. Pretty a => a -> String
prettyShow (HypGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList HypGraph r f
g)
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HypGraph r f -> Bool
forall a. Negative a => a -> Bool
negative HypGraph r f
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
"size constraint graph has negative loops"
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HypGraph r f
hg HypGraph r f -> HypGraph r f -> Bool
forall r f a.
(Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
Negative a) =>
Graph r f a -> Graph r f a -> Bool
`implies` HypGraph r f
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
"size constraint graph constrains size hypotheses"
HypGraph r f -> Either String (HypGraph r f)
forall (m :: * -> *) a. Monad m => a -> m a
return HypGraph r f
g
type ConGraphs r f = Graphs r f Label
constraintGraphs :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either String ([f], ConGraphs r f)
constraintGraphs :: [Constraint' r f]
-> HypGraph r f -> Either String ([f], ConGraphs r f)
constraintGraphs cons0 :: [Constraint' r f]
cons0 hg :: HypGraph r f
hg = do
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "original constraints cons0 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons0
[Constraint' r f]
cons <- HypGraph r f
-> [Constraint' r f] -> Either String [Constraint' r f]
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either String [Constraint' rigid flex]
simplifyWithHypotheses HypGraph r f
hg [Constraint' r f]
cons0
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "simplified constraints cons = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons
let gs0 :: ConGraphs r f
gs0 = [Constraint' r f] -> ConGraphs r f
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints [Constraint' r f]
cons
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "constraint forest gs0 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Edge (Node r f) Label]] -> String
forall a. Pretty a => a -> String
prettyShow ((HypGraph r f -> [Edge (Node r f) Label])
-> ConGraphs r f -> [[Edge (Node r f) Label]]
forall a b. (a -> b) -> [a] -> [b]
map HypGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList ConGraphs r f
gs0)
let gs1 :: ConGraphs r f
gs1 = (HypGraph r f -> HypGraph r f) -> ConGraphs r f -> ConGraphs r f
forall a b. (a -> b) -> [a] -> [b]
map HypGraph r f -> HypGraph r f
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos ConGraphs r f
gs0
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "transitive forest gs1 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Edge (Node r f) Label]] -> String
forall a. Pretty a => a -> String
prettyShow ((HypGraph r f -> [Edge (Node r f) Label])
-> ConGraphs r f -> [[Edge (Node r f) Label]]
forall a b. (a -> b) -> [a] -> [b]
map HypGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList ConGraphs r f
gs1)
let (xss :: [[f]]
xss,gs :: ConGraphs r f
gs) = [([f], HypGraph r f)] -> ([[f]], ConGraphs r f)
forall a b. [(a, b)] -> ([a], [b])
unzip ([([f], HypGraph r f)] -> ([[f]], ConGraphs r f))
-> [([f], HypGraph r f)] -> ([[f]], ConGraphs r f)
forall a b. (a -> b) -> a -> b
$ (HypGraph r f -> ([f], HypGraph r f))
-> ConGraphs r f -> [([f], HypGraph r f)]
forall a b. (a -> b) -> [a] -> [b]
map HypGraph r f -> ([f], HypGraph r f)
forall r f. (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs ConGraphs r f
gs1
xs :: [f]
xs = [[f]] -> [f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[f]]
xss
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([f] -> Bool
forall a. Null a => a -> Bool
null [f]
xs) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ do
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "flexibles to set to oo = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [f] -> String
forall a. Pretty a => a -> String
prettyShow [f]
xs
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "forest after oo-subst = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Edge (Node r f) Label]] -> String
forall a. Pretty a => a -> String
prettyShow ((HypGraph r f -> [Edge (Node r f) Label])
-> ConGraphs r f -> [[Edge (Node r f) Label]]
forall a b. (a -> b) -> [a] -> [b]
map HypGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList ConGraphs r f
gs)
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConGraphs r f -> Bool
forall a. Negative a => a -> Bool
negative ConGraphs r f
gs) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "size constraint graph has negative loop"
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "we are free of negative loops"
ConGraphs r f
-> (HypGraph r f -> Either String ()) -> Either String ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ConGraphs r f
gs ((HypGraph r f -> Either String ()) -> Either String ())
-> (HypGraph r f -> Either String ()) -> Either String ()
forall a b. (a -> b) -> a -> b
$ \ g :: HypGraph r f
g -> Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HypGraph r f
hg HypGraph r f -> HypGraph r f -> Bool
forall r f a.
(Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
Negative a) =>
Graph r f a -> Graph r f a -> Bool
`implies` HypGraph r f
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
"size constraint graph constrains size hypotheses"
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "any constraint between rigids is implied by the hypotheses"
([f], ConGraphs r f) -> Either String ([f], ConGraphs r f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([f]
xs, ConGraphs r f
gs)
infinityFlexs :: (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs :: ConGraph r f -> ([f], ConGraph r f)
infinityFlexs g :: ConGraph r f
g = ([f]
infFlexs, [f] -> ConGraph r f -> ConGraph r f
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
infFlexs ConGraph r f
g)
where
infFlexs :: [f]
infFlexs = (Edge (Node r f) Label -> Maybe f)
-> [Edge (Node r f) Label] -> [f]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Edge (Node r f) Label -> Maybe f
forall e rigid b. Negative e => Edge (Node rigid b) e -> Maybe b
flexNeg ([Edge (Node r f) Label] -> [f]) -> [Edge (Node r f) Label] -> [f]
forall a b. (a -> b) -> a -> b
$ ConGraph r f -> [Edge (Node r f) Label]
forall n e. Ord n => Graph n e -> [Edge n e]
Graph.diagonal ConGraph r f
g
flexNeg :: Edge (Node rigid b) e -> Maybe b
flexNeg e :: Edge (Node rigid b) e
e = do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Edge (Node rigid b) e -> Bool
forall a. Negative a => a -> Bool
negative Edge (Node rigid b) e
e
Node rigid b -> Maybe b
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode (Edge (Node rigid b) e -> Node rigid b
forall n e. Edge n e -> n
src Edge (Node rigid b) e
e)
class SetToInfty f a where
setToInfty :: [f] -> a -> a
instance (Eq f) => SetToInfty f (Node r f) where
setToInfty :: [f] -> Node r f -> Node r f
setToInfty xs :: [f]
xs (NodeFlex x :: f
x) | f
x f -> [f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [f]
xs = Node r f
forall rigid flex. Node rigid flex
NodeInfty
setToInfty xs :: [f]
xs n :: Node r f
n = Node r f
n
instance (Eq f) => SetToInfty f (Edge' r f a) where
setToInfty :: [f] -> Edge' r f a -> Edge' r f a
setToInfty xs :: [f]
xs (Edge n1 :: Node r f
n1 n2 :: Node r f
n2 l :: a
l) = Node r f -> Node r f -> a -> Edge' r f a
forall n e. n -> n -> e -> Edge n e
Edge ([f] -> Node r f -> Node r f
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs Node r f
n1) ([f] -> Node r f -> Node r f
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs Node r f
n2) a
l
instance (Ord r, Ord f) => SetToInfty f (ConGraph r f) where
setToInfty :: [f] -> ConGraph r f -> ConGraph r f
setToInfty xs :: [f]
xs = [Edge (Node r f) Label] -> ConGraph r f
forall n e. Ord n => [Edge n e] -> Graph n e
graphFromList ([Edge (Node r f) Label] -> ConGraph r f)
-> (ConGraph r f -> [Edge (Node r f) Label])
-> ConGraph r f
-> ConGraph r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge (Node r f) Label -> Bool)
-> [Edge (Node r f) Label] -> [Edge (Node r f) Label]
forall a. (a -> Bool) -> [a] -> [a]
filter Edge (Node r f) Label -> Bool
forall rigid flex. Edge (Node rigid flex) Label -> Bool
h ([Edge (Node r f) Label] -> [Edge (Node r f) Label])
-> (ConGraph r f -> [Edge (Node r f) Label])
-> ConGraph r f
-> [Edge (Node r f) Label]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge (Node r f) Label -> Edge (Node r f) Label)
-> [Edge (Node r f) Label] -> [Edge (Node r f) Label]
forall a b. (a -> b) -> [a] -> [b]
map ([f] -> Edge (Node r f) Label -> Edge (Node r f) Label
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs) ([Edge (Node r f) Label] -> [Edge (Node r f) Label])
-> (ConGraph r f -> [Edge (Node r f) Label])
-> ConGraph r f
-> [Edge (Node r f) Label]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList
where
h :: Edge (Node rigid flex) Label -> Bool
h (Edge NodeInfty NodeInfty (Label Le _)) = Bool
False
h _ = Bool
True
instance Plus Offset Weight Weight where
plus :: Offset -> Weight -> Weight
plus e :: Offset
e Infinity = Weight
Infinity
plus e :: Offset
e (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a b c. Plus a b c => a -> b -> c
plus Offset
e Offset
x
instance Plus (SizeExpr' r f) Weight (SizeExpr' r f) where
plus :: SizeExpr' r f -> Weight -> SizeExpr' r f
plus e :: SizeExpr' r f
e Infinity = SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
plus e :: SizeExpr' r f
e (Offset x :: Offset
x) = SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
plus SizeExpr' r f
e Offset
x
instance Plus (SizeExpr' r f) Label (SizeExpr' r f) where
plus :: SizeExpr' r f -> Label -> SizeExpr' r f
plus e :: SizeExpr' r f
e l :: Label
l = SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
plus SizeExpr' r f
e (Label -> Weight
toWeight Label
l)
type Bound r f = Map f (Set (SizeExpr' r f))
emptyBound :: Bound r f
emptyBound :: Bound r f
emptyBound = Bound r f
forall k a. Map k a
Map.empty
data Bounds r f = Bounds
{ Bounds r f -> Bound r f
lowerBounds :: Bound r f
, Bounds r f -> Bound r f
upperBounds :: Bound r f
, Bounds r f -> Set f
mustBeFinite :: Set f
}
edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound e :: LabelledEdge r f
e =
case LabelledEdge r f
e of
(Edge n1 :: Node r f
n1 n2 :: Node r f
n2 LInf) -> Maybe (f, SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Edge NodeZero (NodeFlex x :: f
x) (Label Le o :: Offset
o)) | Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const 0)
(Edge NodeZero (NodeFlex x :: f
x) (Label Lt o :: Offset
o)) | Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const 0)
(Edge n1 :: Node r f
n1 (NodeFlex x :: f
x) l :: Label
l) -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n1 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` (- (Label -> Weight
toWeight Label
l)))
_ -> Maybe (f, SizeExpr' r f)
forall a. Maybe a
Nothing
edgeToUpperBound :: LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
edgeToUpperBound :: LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
edgeToUpperBound e :: LabelledEdge r f
e =
case LabelledEdge r f
e of
(Edge n1 :: Node r f
n1 n2 :: Node r f
n2 LInf) -> Maybe (f, Cmp, SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Edge n1 :: Node r f
n1 NodeInfty (Label Le _)) -> Maybe (f, Cmp, SizeExpr' r f)
forall a. Maybe a
Nothing
(Edge (NodeFlex x :: f
x) NodeInfty (Label Lt _)) -> (f, Cmp, SizeExpr' r f) -> Maybe (f, Cmp, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Cmp
Lt, SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty)
(Edge (NodeFlex x :: f
x) n2 :: Node r f
n2 l :: Label
l ) -> (f, Cmp, SizeExpr' r f) -> Maybe (f, Cmp, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Cmp
Le, Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n2 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` (Label -> Weight
toWeight Label
l))
_ -> Maybe (f, Cmp, SizeExpr' r f)
forall a. Maybe a
Nothing
graphToLowerBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
graphToLowerBounds :: [LabelledEdge r f] -> Bound r f
graphToLowerBounds = ((Bound r f -> LabelledEdge r f -> Bound r f)
-> Bound r f -> [LabelledEdge r f] -> Bound r f)
-> Bound r f
-> (Bound r f -> LabelledEdge r f -> Bound r f)
-> [LabelledEdge r f]
-> Bound r f
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bound r f -> LabelledEdge r f -> Bound r f)
-> Bound r f -> [LabelledEdge r f] -> Bound r f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bound r f
forall r f. Bound r f
emptyBound ((Bound r f -> LabelledEdge r f -> Bound r f)
-> [LabelledEdge r f] -> Bound r f)
-> (Bound r f -> LabelledEdge r f -> Bound r f)
-> [LabelledEdge r f]
-> Bound r f
forall a b. (a -> b) -> a -> b
$ \ bs :: Bound r f
bs e :: LabelledEdge r f
e ->
case LabelledEdge r f -> Maybe (f, SizeExpr' r f)
forall r f. LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound LabelledEdge r f
e of
Nothing -> Bound r f
bs
Just (x :: f
x, Flex{}) -> Bound r f
bs
Just (x :: f
x, a :: SizeExpr' r f
a) -> (Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f))
-> f -> Set (SizeExpr' r f) -> Bound r f -> Bound r f
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union f
x (SizeExpr' r f -> Set (SizeExpr' r f)
forall a. a -> Set a
Set.singleton SizeExpr' r f
a) Bound r f
bs
graphToUpperBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds :: [LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds = (((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> (Bound r f, Set f) -> [LabelledEdge r f] -> (Bound r f, Set f))
-> (Bound r f, Set f)
-> ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> [LabelledEdge r f]
-> (Bound r f, Set f)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> (Bound r f, Set f) -> [LabelledEdge r f] -> (Bound r f, Set f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bound r f
forall r f. Bound r f
emptyBound, Set f
forall a. Set a
Set.empty) (((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> [LabelledEdge r f] -> (Bound r f, Set f))
-> ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> [LabelledEdge r f]
-> (Bound r f, Set f)
forall a b. (a -> b) -> a -> b
$ \ (bs :: Bound r f
bs, fs :: Set f
fs) e :: LabelledEdge r f
e ->
case LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
forall r f. LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
edgeToUpperBound LabelledEdge r f
e of
Nothing -> (Bound r f
bs, Set f
fs)
Just (x :: f
x, _, Flex{}) -> (Bound r f
bs, Set f
fs)
Just (x :: f
x, Lt, Infty) -> (Bound r f
bs, f -> Set f -> Set f
forall a. Ord a => a -> Set a -> Set a
Set.insert f
x Set f
fs)
Just (x :: f
x, Le, a :: SizeExpr' r f
a) -> ((Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f))
-> f -> Set (SizeExpr' r f) -> Bound r f -> Bound r f
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union f
x (SizeExpr' r f -> Set (SizeExpr' r f)
forall a. a -> Set a
Set.singleton SizeExpr' r f
a) Bound r f
bs, Set f
fs)
_ -> (Bound r f, Set f)
forall a. HasCallStack => a
__IMPOSSIBLE__
bounds :: (Ord r, Ord f) => ConGraph r f -> Bounds r f
bounds :: ConGraph r f -> Bounds r f
bounds g :: ConGraph r f
g = Bound r f -> Bound r f -> Set f -> Bounds r f
forall r f. Bound r f -> Bound r f -> Set f -> Bounds r f
Bounds Bound r f
lbs Bound r f
ubs Set f
fs
where edges :: [Edge (Node r f) Label]
edges = ConGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList ConGraph r f
g
lbs :: Bound r f
lbs = [Edge (Node r f) Label] -> Bound r f
forall r f. (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
graphToLowerBounds [Edge (Node r f) Label]
edges
(ubs :: Bound r f
ubs, fs :: Set f
fs) = [Edge (Node r f) Label] -> (Bound r f, Set f)
forall r f.
(Ord r, Ord f) =>
[LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds [Edge (Node r f) Label]
edges
smallest ::(Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
smallest :: HypGraph r f -> [Node r f] -> [Node r f]
smallest hg :: HypGraph r f
hg ns :: [Node r f]
ns
| Node r f
forall rigid flex. Node rigid flex
NodeZero Node r f -> [Node r f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node r f]
ns = [Node r f
forall rigid flex. Node rigid flex
NodeZero]
| Bool
otherwise = (Node r f -> Bool) -> [Node r f] -> [Node r f]
forall a. (a -> Bool) -> [a] -> [a]
filter Node r f -> Bool
hasNoPred [Node r f]
ns where
hasNoPred :: Node r f -> Bool
hasNoPred NodeInfty = Bool
False
hasNoPred n :: Node r f
n = [()] -> Bool
forall a. Null a => a -> Bool
null ([()] -> Bool) -> [()] -> Bool
forall a b. (a -> b) -> a -> b
$ (Node r f -> Maybe ()) -> [Node r f] -> [()]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node r f -> Maybe ()
strictEdge [Node r f]
ns where
strictEdge :: Node r f -> Maybe ()
strictEdge n' :: Node r f
n' = do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Node r f
n Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/= Node r f
n')
Label
l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n' Node r f
n
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Label -> Weight
toWeight Label
l Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= 0)
() -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
largest ::(Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
largest :: HypGraph r f -> [Node r f] -> [Node r f]
largest hg :: HypGraph r f
hg ns :: [Node r f]
ns
| Node r f
forall rigid flex. Node rigid flex
NodeInfty Node r f -> [Node r f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node r f]
ns = [Node r f
forall rigid flex. Node rigid flex
NodeInfty]
| Bool
otherwise = (Node r f -> Bool) -> [Node r f] -> [Node r f]
forall a. (a -> Bool) -> [a] -> [a]
filter Node r f -> Bool
hasNoSucc [Node r f]
ns where
hasNoSucc :: Node r f -> Bool
hasNoSucc NodeZero = Bool
False
hasNoSucc n :: Node r f
n = [()] -> Bool
forall a. Null a => a -> Bool
null ([()] -> Bool) -> [()] -> Bool
forall a b. (a -> b) -> a -> b
$ (Node r f -> Maybe ()) -> [Node r f] -> [()]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node r f -> Maybe ()
strictEdge [Node r f]
ns where
strictEdge :: Node r f -> Maybe ()
strictEdge n' :: Node r f
n' = do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Node r f
n Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/= Node r f
n')
Label
l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n Node r f
n'
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Label -> Weight
toWeight Label
l Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= 0)
() -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
commonSuccs :: (Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs :: Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs hg :: Graph r f a
hg srcs :: [Node r f]
srcs = [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall k a. Ord k => [Map k [a]] -> Map k [a]
intersectAll ([Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a])
-> [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall a b. (a -> b) -> a -> b
$ (Node r f -> Map (Node r f) [Edge' r f a])
-> [Node r f] -> [Map (Node r f) [Edge' r f a]]
forall a b. (a -> b) -> [a] -> [b]
map ([Edge' r f a] -> Map (Node r f) [Edge' r f a]
forall k e. Ord k => [Edge k e] -> Map k [Edge k e]
buildmap ([Edge' r f a] -> Map (Node r f) [Edge' r f a])
-> (Node r f -> [Edge' r f a])
-> Node r f
-> Map (Node r f) [Edge' r f a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph r f a -> Node r f -> [Edge' r f a]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
outgoing Graph r f a
hg) [Node r f]
srcs
where
buildmap :: [Edge k e] -> Map k [Edge k e]
buildmap = [(k, [Edge k e])] -> Map k [Edge k e]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, [Edge k e])] -> Map k [Edge k e])
-> ([Edge k e] -> [(k, [Edge k e])])
-> [Edge k e]
-> Map k [Edge k e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge k e -> (k, [Edge k e])) -> [Edge k e] -> [(k, [Edge k e])]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: Edge k e
e -> (Edge k e -> k
forall n e. Edge n e -> n
dest Edge k e
e, [Edge k e
e]))
intersectAll :: [Map k [a]] -> Map k [a]
intersectAll [] = Map k [a]
forall k a. Map k a
Map.empty
intersectAll (m :: Map k [a]
m:ms :: [Map k [a]]
ms) = (Map k [a] -> Map k [a] -> Map k [a])
-> Map k [a] -> [Map k [a]] -> Map k [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([a] -> [a] -> [a]) -> Map k [a] -> Map k [a] -> Map k [a]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)) Map k [a]
m [Map k [a]]
ms
commonPreds :: (Ord r, Ord f) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonPreds :: Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonPreds hg :: Graph r f a
hg tgts :: [Node r f]
tgts = [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall k a. Ord k => [Map k [a]] -> Map k [a]
intersectAll ([Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a])
-> [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall a b. (a -> b) -> a -> b
$ (Node r f -> Map (Node r f) [Edge' r f a])
-> [Node r f] -> [Map (Node r f) [Edge' r f a]]
forall a b. (a -> b) -> [a] -> [b]
map ([Edge' r f a] -> Map (Node r f) [Edge' r f a]
forall k e. Ord k => [Edge k e] -> Map k [Edge k e]
buildmap ([Edge' r f a] -> Map (Node r f) [Edge' r f a])
-> (Node r f -> [Edge' r f a])
-> Node r f
-> Map (Node r f) [Edge' r f a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph r f a -> Node r f -> [Edge' r f a]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
incoming Graph r f a
hg) [Node r f]
tgts
where
buildmap :: [Edge k e] -> Map k [Edge k e]
buildmap = [(k, [Edge k e])] -> Map k [Edge k e]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, [Edge k e])] -> Map k [Edge k e])
-> ([Edge k e] -> [(k, [Edge k e])])
-> [Edge k e]
-> Map k [Edge k e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge k e -> (k, [Edge k e])) -> [Edge k e] -> [(k, [Edge k e])]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: Edge k e
e -> (Edge k e -> k
forall n e. Edge n e -> n
src Edge k e
e, [Edge k e
e]))
intersectAll :: [Map k [a]] -> Map k [a]
intersectAll [] = Map k [a]
forall k a. Map k a
Map.empty
intersectAll (m :: Map k [a]
m:ms :: [Map k [a]]
ms) = (Map k [a] -> Map k [a] -> Map k [a])
-> Map k [a] -> [Map k [a]] -> Map k [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([a] -> [a] -> [a]) -> Map k [a] -> Map k [a] -> Map k [a]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)) Map k [a]
m [Map k [a]]
ms
lub'
:: forall r f . (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' :: HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' hg :: HypGraph r f
hg (node1 :: Node r f
node1, n :: Offset
n) (node2 :: Node r f
node2, m :: Offset
m) = do
let sucs :: Map (Node r f) [Edge' r f Label]
sucs = HypGraph r f -> [Node r f] -> Map (Node r f) [Edge' r f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs HypGraph r f
hg [Node r f
node1, Node r f
node2]
sucNodes :: [Node r f]
sucNodes = HypGraph r f -> [Node r f] -> [Node r f]
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
smallest HypGraph r f
hg ([Node r f] -> [Node r f]) -> [Node r f] -> [Node r f]
forall a b. (a -> b) -> a -> b
$ Map (Node r f) [Edge' r f Label] -> [Node r f]
forall k a. Map k a -> [k]
Map.keys Map (Node r f) [Edge' r f Label]
sucs
String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("lub': sucs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map (Node r f) [Edge' r f Label] -> String
forall a. Show a => a -> String
show Map (Node r f) [Edge' r f Label]
sucs)
case [Node r f]
sucNodes of
[n0 :: Node r f
n0] -> do
let es :: [Edge' r f Label]
es = [Edge' r f Label] -> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a. a -> Maybe a -> a
fromMaybe [Edge' r f Label]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Edge' r f Label] -> [Edge' r f Label])
-> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a b. (a -> b) -> a -> b
$ Node r f
-> Map (Node r f) [Edge' r f Label] -> Maybe [Edge' r f Label]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node r f
n0 Map (Node r f) [Edge' r f Label]
sucs
case [Edge' r f Label]
es of
[ Edge node1x :: Node r f
node1x n1 :: Node r f
n1 l1 :: Label
l1 ,
Edge node2x :: Node r f
node2x n2 :: Node r f
n2 l2 :: Label
l2 ] -> do
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n1) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n2) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node1 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node1x) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node2 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node2x) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let o :: Weight
o :: Weight
o = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
max (Offset
n Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l1) (Offset
m Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l2)
SizeExpr' r f -> Maybe (SizeExpr' r f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n0 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Weight
o
_ -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> do
let SizeExpr' r f
a1 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node1 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n
let SizeExpr' r f
a2 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node2 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
m
String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("cannot compute lub of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " because sucNodes = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Node r f] -> String
forall a. Pretty a => a -> String
prettyShow [Node r f]
sucNodes)
Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
glb'
:: forall r f . (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
glb' :: HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
glb' hg :: HypGraph r f
hg (node1 :: Node r f
node1, n :: Offset
n) (node2 :: Node r f
node2, m :: Offset
m) = do
let preds :: Map (Node r f) [Edge' r f Label]
preds = HypGraph r f -> [Node r f] -> Map (Node r f) [Edge' r f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonPreds HypGraph r f
hg [Node r f
node1, Node r f
node2]
predNodes :: [Node r f]
predNodes = HypGraph r f -> [Node r f] -> [Node r f]
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
largest HypGraph r f
hg ([Node r f] -> [Node r f]) -> [Node r f] -> [Node r f]
forall a b. (a -> b) -> a -> b
$ Map (Node r f) [Edge' r f Label] -> [Node r f]
forall k a. Map k a -> [k]
Map.keys Map (Node r f) [Edge' r f Label]
preds
String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("glb': preds = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map (Node r f) [Edge' r f Label] -> String
forall a. Show a => a -> String
show Map (Node r f) [Edge' r f Label]
preds)
case [Node r f]
predNodes of
[n0 :: Node r f
n0] -> do
let es :: [Edge' r f Label]
es = [Edge' r f Label] -> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a. a -> Maybe a -> a
fromMaybe [Edge' r f Label]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Edge' r f Label] -> [Edge' r f Label])
-> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a b. (a -> b) -> a -> b
$ Node r f
-> Map (Node r f) [Edge' r f Label] -> Maybe [Edge' r f Label]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node r f
n0 Map (Node r f) [Edge' r f Label]
preds
case [Edge' r f Label]
es of
[ Edge n1 :: Node r f
n1 node1x :: Node r f
node1x l1 :: Label
l1 ,
Edge n2 :: Node r f
n2 node2x :: Node r f
node2x l2 :: Label
l2] -> do
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n1) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n2) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node1 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node1x) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node2 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node2x) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let o :: Weight
o :: Weight
o = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
max (Offset
n Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l1) (Offset
m Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l2)
SizeExpr' r f -> Maybe (SizeExpr' r f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n0 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Weight
o
_ -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> do
let SizeExpr' r f
a1 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node1 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n
let SizeExpr' r f
a2 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node2 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
m
String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("cannot compute glb of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " because predNodes = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Node r f] -> String
forall a. Pretty a => a -> String
prettyShow [Node r f]
predNodes)
Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
lub
:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> SizeExpr' r f
-> SizeExpr' r f
-> Maybe (SizeExpr' r f)
lub :: HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
lub hg :: HypGraph r f
hg a1 :: SizeExpr' r f
a1 a2 :: SizeExpr' r f
a2 =
case (SizeExpr' r f
a1, SizeExpr' r f
a2) of
(Flex{}, _) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(_, Flex{}) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Infty, a2 :: SizeExpr' r f
a2) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
(a1 :: SizeExpr' r f
a1, Infty) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
(Const n :: Offset
n , Const m :: Offset
m )
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a. Ord a => a -> a -> a
max Offset
n Offset
m
(Const n :: Offset
n , Rigid j :: r
j m :: Offset
m)
| Offset
m Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
n -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a2
| Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' HypGraph r f
hg (Node r f
forall rigid flex. Node rigid flex
NodeZero, Offset
n) (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)
(Rigid i :: r
i n :: Offset
n, Const m :: Offset
m )
| Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
m -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a1
| Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' HypGraph r f
hg (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (Node r f
forall rigid flex. Node rigid flex
NodeZero, Offset
m)
(Rigid i :: r
i n :: Offset
n, Rigid j :: r
j m :: Offset
m)
| r
i r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
j -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a. Ord a => a -> a -> a
max Offset
n Offset
m
| Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' HypGraph r f
hg (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)
glb
:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> SizeExpr' r f
-> SizeExpr' r f
-> Maybe (SizeExpr' r f)
glb :: HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
glb hg :: HypGraph r f
hg a1 :: SizeExpr' r f
a1 a2 :: SizeExpr' r f
a2 =
case (SizeExpr' r f
a1, SizeExpr' r f
a2) of
(Flex{}, _) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(_, Flex{}) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Infty, a2 :: SizeExpr' r f
a2) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a2
(a1 :: SizeExpr' r f
a1, Infty) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a1
(Const n :: Offset
n , Const m :: Offset
m ) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a. Ord a => a -> a -> a
min Offset
n Offset
m
(Const n :: Offset
n , Rigid i :: r
i m :: Offset
m)
| Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
m -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a1
| Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
glb' HypGraph r f
hg (Node r f
forall rigid flex. Node rigid flex
NodeZero, Offset
n) (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
m)
(Rigid i :: r
i n :: Offset
n, Const m :: Offset
m )
| Offset
m Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
n -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a2
| Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
glb' HypGraph r f
hg (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (Node r f
forall rigid flex. Node rigid flex
NodeZero, Offset
m)
(Rigid i :: r
i n :: Offset
n, Rigid j :: r
j m :: Offset
m)
| r
i r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
j -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a. Ord a => a -> a -> a
min Offset
n Offset
m
| Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
glb' HypGraph r f
hg (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)
findRigidBelow :: (Ord r, Ord f) => HypGraph r f -> (SizeExpr' r f) -> Maybe (SizeExpr' r f)
findRigidBelow :: HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
findRigidBelow hg :: HypGraph r f
hg (Rigid i :: r
i m :: Offset
m) | Offset
m Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = do
let v :: Node r flex
v = r -> Node r flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i
preds :: [Edge' r f Label]
preds = HypGraph r f -> Node r f -> [Edge' r f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
incoming HypGraph r f
hg Node r f
forall flex. Node r flex
v
filt :: Edge (Node r flex) Label -> Maybe (Node r flex, Offset)
filt e :: Edge (Node r flex) Label
e@(Edge n :: Node r flex
n n' :: Node r flex
n' l :: Label
l)
| Node r flex
n' Node r flex -> Node r flex -> Bool
forall a. Eq a => a -> a -> Bool
== Node r flex
forall flex. Node r flex
v =
case Label -> Weight
toWeight Label
l of
Infinity -> Maybe (Node r flex, Offset)
forall a. Maybe a
Nothing
Offset o :: Offset
o -> if Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
m then (Node r flex, Offset) -> Maybe (Node r flex, Offset)
forall a. a -> Maybe a
Just (Node r flex
n, Offset
o) else Maybe (Node r flex, Offset)
forall a. Maybe a
Nothing
| Bool
otherwise = Maybe (Node r flex, Offset)
forall a. HasCallStack => a
__IMPOSSIBLE__
cands :: [(Node r f, Offset)]
cands = (Edge' r f Label -> Maybe (Node r f, Offset))
-> [Edge' r f Label] -> [(Node r f, Offset)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Edge' r f Label -> Maybe (Node r f, Offset)
forall flex.
Eq flex =>
Edge (Node r flex) Label -> Maybe (Node r flex, Offset)
filt [Edge' r f Label]
preds
(n :: Node r f
n, o :: Offset
o) <- do
case [(Node r f, Offset)]
cands of
[] -> Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
[c :: (Node r f, Offset)
c] -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node r f, Offset)
c
_ -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Node r f, Offset) -> Maybe (Node r f, Offset))
-> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a b. (a -> b) -> a -> b
$
((Node r f, Offset) -> (Node r f, Offset) -> Ordering)
-> [(Node r f, Offset)] -> (Node r f, Offset)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
List.maximumBy (Offset -> Offset -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Offset -> Offset -> Ordering)
-> ((Node r f, Offset) -> Offset)
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Node r f, Offset) -> Offset
forall a b. (a, b) -> b
snd) ([(Node r f, Offset)] -> (Node r f, Offset))
-> [(Node r f, Offset)] -> (Node r f, Offset)
forall a b. (a -> b) -> a -> b
$
((Node r f, Offset) -> Bool)
-> [(Node r f, Offset)] -> [(Node r f, Offset)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Node r f
forall rigid flex. Node rigid flex
NodeZero Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Node r f -> Bool)
-> ((Node r f, Offset) -> Node r f) -> (Node r f, Offset) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node r f, Offset) -> Node r f
forall a b. (a, b) -> a
fst) [(Node r f, Offset)]
cands
let offset :: Offset
offset = Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
o
Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Offset
offset Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= 0) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
SizeExpr' r f -> Maybe (SizeExpr' r f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
offset
findRigidBelow hg :: HypGraph r f
hg e :: SizeExpr' r f
e = Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
solveGraph
:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> ConGraph r f
-> Either String (Solution r f)
solveGraph :: Polarities f
-> HypGraph r f -> HypGraph r f -> Either String (Solution r f)
solveGraph pols :: Polarities f
pols hg :: HypGraph r f
hg g :: HypGraph r f
g = do
let (Bounds lbs :: Bound r f
lbs ubs :: Bound r f
ubs fs :: Set f
fs) = HypGraph r f -> Bounds r f
forall r f. (Ord r, Ord f) => ConGraph r f -> Bounds r f
bounds HypGraph r f
g
xs :: [f]
xs = Set f -> [f]
forall a. Set a -> [a]
Set.toAscList (Set f -> [f]) -> Set f -> [f]
forall a b. (a -> b) -> a -> b
$ [Set f] -> Set f
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ Bound r f -> Set f
forall k a. Map k a -> Set k
Map.keysSet Bound r f
lbs, Bound r f -> Set f
forall k a. Map k a -> Set k
Map.keysSet Bound r f
ubs, Set f
fs ]
[(f, SizeExpr' r f)]
xas <- [Maybe (f, SizeExpr' r f)] -> [(f, SizeExpr' r f)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (f, SizeExpr' r f)] -> [(f, SizeExpr' r f)])
-> Either String [Maybe (f, SizeExpr' r f)]
-> Either String [(f, SizeExpr' r f)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[f]
-> (f -> Either String (Maybe (f, SizeExpr' r f)))
-> Either String [Maybe (f, SizeExpr' r f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [f]
xs ((f -> Either String (Maybe (f, SizeExpr' r f)))
-> Either String [Maybe (f, SizeExpr' r f)])
-> (f -> Either String (Maybe (f, SizeExpr' r f)))
-> Either String [Maybe (f, SizeExpr' r f)]
forall a b. (a -> b) -> a -> b
$ \ x :: f
x -> do
let lx :: [SizeExpr' r f]
lx = Set (SizeExpr' r f) -> [SizeExpr' r f]
forall a. Set a -> [a]
Set.toList (Set (SizeExpr' r f) -> [SizeExpr' r f])
-> Set (SizeExpr' r f) -> [SizeExpr' r f]
forall a b. (a -> b) -> a -> b
$ Set (SizeExpr' r f) -> f -> Bound r f -> Set (SizeExpr' r f)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set (SizeExpr' r f)
forall a. Set a
Set.empty f
x Bound r f
lbs
ux :: [SizeExpr' r f]
ux = Set (SizeExpr' r f) -> [SizeExpr' r f]
forall a. Set a -> [a]
Set.toList (Set (SizeExpr' r f) -> [SizeExpr' r f])
-> Set (SizeExpr' r f) -> [SizeExpr' r f]
forall a b. (a -> b) -> a -> b
$ Set (SizeExpr' r f) -> f -> Bound r f -> Set (SizeExpr' r f)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set (SizeExpr' r f)
forall a. Set a
Set.empty f
x Bound r f
ubs
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("lower bounds for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SizeExpr' r f] -> String
forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
lx)
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("upper bounds for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SizeExpr' r f] -> String
forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
ux)
Maybe (SizeExpr' r f)
lb <- do
case [SizeExpr' r f]
lx of
[] -> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
(a :: SizeExpr' r f
a:as :: [SizeExpr' r f]
as) -> do
case (SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> [SizeExpr' r f] -> Maybe (SizeExpr' r f)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
lub HypGraph r f
hg) SizeExpr' r f
a [SizeExpr' r f]
as of
Nothing -> String -> Either String (Maybe (SizeExpr' r f))
forall a b. a -> Either a b
Left (String -> Either String (Maybe (SizeExpr' r f)))
-> String -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ "inconsistent lower bound for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x
Just l :: SizeExpr' r f
l -> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> SizeExpr' r f
forall a. TruncateOffset a => a -> a
truncateOffset SizeExpr' r f
l
Maybe (SizeExpr' r f)
ub <- do
case [SizeExpr' r f]
ux of
[] -> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
(a :: SizeExpr' r f
a:as :: [SizeExpr' r f]
as) -> do
case (SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> [SizeExpr' r f] -> Maybe (SizeExpr' r f)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
glb HypGraph r f
hg) SizeExpr' r f
a [SizeExpr' r f]
as of
Just l :: SizeExpr' r f
l | SizeExpr' r f -> Bool
forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' r f
l -> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
l
| Just l' :: SizeExpr' r f
l' <- HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
findRigidBelow HypGraph r f
hg SizeExpr' r f
l -> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
l'
_ -> String -> Either String (Maybe (SizeExpr' r f))
forall a b. a -> Either a b
Left (String -> Either String (Maybe (SizeExpr' r f)))
-> String -> Either String (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ "inconsistent upper bound for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x
case (Maybe (SizeExpr' r f)
lb, Maybe (SizeExpr' r f)
ub) of
(Just l :: SizeExpr' r f
l, Nothing) -> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f)))
-> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, SizeExpr' r f
l)
(Nothing, Just u :: SizeExpr' r f
u) -> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f)))
-> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, SizeExpr' r f
u)
(Just l :: SizeExpr' r f
l, Just u :: SizeExpr' r f
u) -> do
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("lower bound for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
l)
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("upper bound for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
u)
case Polarities f -> f -> Polarity
forall flex. Ord flex => Polarities flex -> flex -> Polarity
getPolarity Polarities f
pols f
x of
Least -> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f)))
-> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, SizeExpr' r f
l)
Greatest -> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f)))
-> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, SizeExpr' r f
u)
_ -> Maybe (f, SizeExpr' r f)
-> Either String (Maybe (f, SizeExpr' r f))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (f, SizeExpr' r f)
forall a. Maybe a
Nothing
Solution r f -> Either String (Solution r f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Solution r f -> Either String (Solution r f))
-> Solution r f -> Either String (Solution r f)
forall a b. (a -> b) -> a -> b
$ Map f (SizeExpr' r f) -> Solution r f
forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution (Map f (SizeExpr' r f) -> Solution r f)
-> Map f (SizeExpr' r f) -> Solution r f
forall a b. (a -> b) -> a -> b
$ [(f, SizeExpr' r f)] -> Map f (SizeExpr' r f)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(f, SizeExpr' r f)]
xas
solveGraphs
:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> ConGraphs r f
-> Either String (Solution r f)
solveGraphs :: Polarities f
-> HypGraph r f -> ConGraphs r f -> Either String (Solution r f)
solveGraphs pols :: Polarities f
pols hg :: HypGraph r f
hg gs :: ConGraphs r f
gs =
Map f (SizeExpr' r f) -> Solution r f
forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution (Map f (SizeExpr' r f) -> Solution r f)
-> ([Map f (SizeExpr' r f)] -> Map f (SizeExpr' r f))
-> [Map f (SizeExpr' r f)]
-> Solution r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Map f (SizeExpr' r f)] -> Map f (SizeExpr' r f)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ([Map f (SizeExpr' r f)] -> Solution r f)
-> Either String [Map f (SizeExpr' r f)]
-> Either String (Solution r f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HypGraph r f -> Either String (Map f (SizeExpr' r f)))
-> ConGraphs r f -> Either String [Map f (SizeExpr' r f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solution r f -> Map f (SizeExpr' r f)
forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution (Solution r f -> Map f (SizeExpr' r f))
-> (HypGraph r f -> Either String (Solution r f))
-> HypGraph r f
-> Either String (Map f (SizeExpr' r f))
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Polarities f
-> HypGraph r f -> HypGraph r f -> Either String (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
Polarities f
-> HypGraph r f -> HypGraph r f -> Either String (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg) ConGraphs r f
gs
verifySolution
:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either String ()
verifySolution :: HypGraph r f
-> [Constraint' r f] -> Solution r f -> Either String ()
verifySolution hg :: HypGraph r f
hg cs :: [Constraint' r f]
cs sol :: Solution r f
sol = do
[Constraint' r f]
cs <- [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint' r f] -> Either String [Constraint' r f])
-> [Constraint' r f] -> Either String [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ Solution r f -> [Constraint' r f] -> [Constraint' r f]
forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol [Constraint' r f]
cs
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "substituted constraints " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cs
[Constraint' r f]
cs <-
[[Constraint' r f]] -> [Constraint' r f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constraint' r f]] -> [Constraint' r f])
-> Either String [[Constraint' r f]]
-> Either String [Constraint' r f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint' r f -> Either String [Constraint' r f])
-> [Constraint' r f] -> Either String [[Constraint' r f]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Constraint' r f -> Either String [Constraint' r f])
-> Constraint' r f -> Either String [Constraint' r f]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 ((Constraint' r f -> Either String [Constraint' r f])
-> Constraint' r f -> Either String [Constraint' r f])
-> (Constraint' r f -> Either String [Constraint' r f])
-> Constraint' r f
-> Either String [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ \ c :: Constraint' r f
c -> [Constraint' r f] -> Either String [Constraint' r f]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c]) [Constraint' r f]
cs
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "simplified substituted constraints " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cs
let g :: HypGraph r f
g = [Constraint' r f] -> HypGraph r f
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cs
Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HypGraph r f
hg HypGraph r f -> HypGraph r f -> Bool
forall r f a.
(Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
Negative a) =>
Graph r f a -> Graph r f a -> Bool
`implies` HypGraph r f
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$
String -> Either String ()
forall a b. a -> Either a b
Left "solution not implied by hypotheses"
iterateSolver
:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either String (Solution r f)
iterateSolver :: Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either String (Solution r f)
iterateSolver pols :: Polarities f
pols hg :: HypGraph r f
hg cs :: [Constraint' r f]
cs sol0 :: Solution r f
sol0 = do
HypGraph r f
g <- [Constraint' r f] -> HypGraph r f -> Either String (HypGraph r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f] -> HypGraph r f -> Either String (HypGraph r f)
constraintGraph [Constraint' r f]
cs HypGraph r f
hg
Solution r f
sol <- Polarities f
-> HypGraph r f -> HypGraph r f -> Either String (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
Polarities f
-> HypGraph r f -> HypGraph r f -> Either String (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg HypGraph r f
g
String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "(partial) solution " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solution r f -> String
forall a. Pretty a => a -> String
prettyShow Solution r f
sol
if Solution r f -> Bool
forall a. Null a => a -> Bool
null Solution r f
sol then Solution r f -> Either String (Solution r f)
forall (m :: * -> *) a. Monad m => a -> m a
return Solution r f
sol0 else
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either String (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either String (Solution r f)
iterateSolver Polarities f
pols HypGraph r f
hg (Solution r f -> [Constraint' r f] -> [Constraint' r f]
forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol [Constraint' r f]
cs) (Solution r f -> Either String (Solution r f))
-> Solution r f -> Either String (Solution r f)
forall a b. (a -> b) -> a -> b
$ Map f (SizeExpr' r f) -> Solution r f
forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution (Map f (SizeExpr' r f) -> Solution r f)
-> Map f (SizeExpr' r f) -> Solution r f
forall a b. (a -> b) -> a -> b
$
(SizeExpr' r f -> SizeExpr' r f -> SizeExpr' r f)
-> Map f (SizeExpr' r f)
-> Map f (SizeExpr' r f)
-> Map f (SizeExpr' r f)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith SizeExpr' r f -> SizeExpr' r f -> SizeExpr' r f
forall a. HasCallStack => a
__IMPOSSIBLE__ (Solution r f -> Map f (SizeExpr' r f)
forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution Solution r f
sol) (Map f (SizeExpr' r f) -> Map f (SizeExpr' r f))
-> Map f (SizeExpr' r f) -> Map f (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$
Solution r f -> Map f (SizeExpr' r f)
forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution (Solution r f -> Map f (SizeExpr' r f))
-> Solution r f -> Map f (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Solution r f -> Solution r f -> Solution r f
forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol Solution r f
sol0
testSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]
testSuccs :: Map (Node String f) [Edge' String f Label]
testSuccs = Graph String f Label
-> [Node String f] -> Map (Node String f) [Edge' String f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs Graph String f Label
forall rigid flex.
(Ord rigid, Ord flex, IsString rigid) =>
Graph (Node rigid flex) Label
hg [Node String f
forall rigid flex. IsString rigid => Node rigid flex
n1,Node String f
forall rigid flex. IsString rigid => Node rigid flex
n2]
where
n1 :: Node rigid flex
n1 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "i"
n2 :: Node rigid flex
n2 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "j"
n3 :: Node rigid flex
n3 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "k"
n4 :: Node rigid flex
n4 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "l"
n5 :: Node rigid flex
n5 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "m"
hg :: Graph (Node rigid flex) Label
hg = [Edge (Node rigid flex) Label] -> Graph (Node rigid flex) Label
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
[ Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 1
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 2
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 3
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 4
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 5
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 6
]
testLub :: (Pretty f, Ord f, Show f) => Maybe (SizeExpr' [Char] f)
testLub :: Maybe (SizeExpr' String f)
testLub = HypGraph String f
-> SizeExpr' String f
-> SizeExpr' String f
-> Maybe (SizeExpr' String f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
lub HypGraph String f
forall rigid flex.
(Ord rigid, Ord flex, IsString rigid) =>
Graph (Node rigid flex) Label
hg (String -> Offset -> SizeExpr' String f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid "i" 0) (String -> Offset -> SizeExpr' String f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid "j" 2)
where
n1 :: Node rigid flex
n1 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "i"
n2 :: Node rigid flex
n2 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "j"
n3 :: Node rigid flex
n3 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "k"
n4 :: Node rigid flex
n4 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "l"
n5 :: Node rigid flex
n5 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "m"
hg :: Graph (Node rigid flex) Label
hg = [Edge (Node rigid flex) Label] -> Graph (Node rigid flex) Label
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
[ Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 0
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 2
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 4
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 1
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 3
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 5
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 0
, Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Lt 0
]