{-# OPTIONS_GHC -Wunused-imports #-}
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.Monad.Base (TCM)
import Agda.TypeChecking.Pretty (PrettyTCM)
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.SizedTypes.Syntax hiding (CTrans, simplify1)
import qualified Agda.TypeChecking.SizedTypes.Syntax as S
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.Syntax.Common.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 :: forall n e. Edge n e -> n
src = Edge n e -> n
forall n e. Edge n e -> n
Graph.source
dest :: Edge n e -> n
dest :: forall n e. 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 :: forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n e
g n
s 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 :: forall n e. 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 :: forall n e. Ord n => [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 :: forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge Edge n e
e 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 :: forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
outgoing Graph r f a
g Node r f
s = Graph r f a -> [Node r f] -> [Edge (Node 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 :: forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
incoming Graph r f a
g Node r f
t = Graph r f a -> [Node r f] -> [Edge (Node 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 :: forall b a. (b -> a -> b) -> b -> Set a -> b
setFoldl b -> a -> b
step b
start = (b -> a -> b) -> b -> [a] -> b
forall b a. (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 :: forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos 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
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 a -> n -> Graph n a
step Graph n a
g n
v = (Graph n a -> Edge n a -> Graph n a)
-> Graph n a -> [Edge n a] -> Graph n a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Edge n a -> Graph n a -> Graph n a)
-> Graph n a -> Edge n a -> Graph n a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Edge n a -> Graph n a -> Graph n a
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph n a
g ([Edge n a] -> Graph n a) -> [Edge n a] -> Graph n a
forall a b. (a -> b) -> a -> b
$
[ n -> n -> a -> Edge n a
forall n e. n -> n -> e -> Edge n e
Edge n
u n
w (a -> Edge n a) -> a -> Edge n a
forall a b. (a -> b) -> a -> b
$ a
l1 a -> a -> a
forall a. Dioid a => a -> a -> a
`compose` a
l2
| n
u <- [n]
srcs
, n
w <- [n]
dests
, a
l1 <- Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList (Maybe a -> [a]) -> Maybe a -> [a]
forall a b. (a -> b) -> a -> b
$ Graph n a -> n -> n -> Maybe a
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n a
g n
u n
v
, a
l2 <- Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList (Maybe a -> [a]) -> Maybe a -> [a]
forall a b. (a -> b) -> a -> b
$ Graph n a -> n -> n -> Maybe a
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n a
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
$c== :: Weight -> Weight -> Bool
== :: Weight -> Weight -> Bool
$c/= :: Weight -> Weight -> Bool
/= :: Weight -> Weight -> Bool
Eq, Int -> Weight -> ShowS
[Weight] -> ShowS
Weight -> String
(Int -> Weight -> ShowS)
-> (Weight -> String) -> ([Weight] -> ShowS) -> Show Weight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Weight -> ShowS
showsPrec :: Int -> Weight -> ShowS
$cshow :: Weight -> String
show :: Weight -> String
$cshowList :: [Weight] -> ShowS
showList :: [Weight] -> ShowS
Show)
instance Pretty Weight where
pretty :: Weight -> Doc
pretty (Offset Offset
x) = Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
x
pretty Weight
Infinity = Doc
"∞"
instance Ord Weight where
Weight
x <= :: Weight -> Weight -> Bool
<= Weight
Infinity = Bool
True
Weight
Infinity <= Weight
y = Bool
False
Offset Offset
x <= Offset 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 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 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 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
Weight
Infinity + :: Weight -> Weight -> Weight
+ Weight
y = Weight
Infinity
Weight
x + Weight
Infinity = Weight
Infinity
Offset Offset
x + Offset 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
Weight
Infinity - :: Weight -> Weight -> Weight
- Offset Offset
y = Weight
Infinity
Offset Offset
x - Offset 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
Weight
x - Weight
Infinity = Weight
forall a. HasCallStack => a
__IMPOSSIBLE__
abs :: Weight -> Weight
abs (Offset 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 Weight
Infinity = Weight
Infinity
signum :: Weight -> Weight
signum (Offset 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 Weight
Infinity = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset
1
fromInteger :: Integer -> Weight
fromInteger Integer
x = Offset -> Weight
Offset (Integer -> Offset
forall a. Num a => Integer -> a
fromInteger Integer
x)
Weight
x * :: Weight -> Weight -> Weight
* Weight
y = Weight
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Plus Weight Offset Weight where
plus :: Weight -> Offset -> Weight
plus Weight
w 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
< Int
0)
instance Negative Offset where
negative :: Offset -> Bool
negative (O Int
x) = Int -> Bool
forall a. Negative a => a -> Bool
negative Int
x
instance Negative Weight where
negative :: Weight -> Bool
negative Weight
Infinity = Bool
False
negative (Offset 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
$cshowsPrec :: Int -> Label -> ShowS
showsPrec :: Int -> Label -> ShowS
$cshow :: Label -> String
show :: Label -> String
$cshowList :: [Label] -> ShowS
showList :: [Label] -> ShowS
Show)
toWeight :: Label -> Weight
toWeight :: Label -> Weight
toWeight (Label Cmp
Le Offset
w) = Offset -> Weight
Offset Offset
w
toWeight (Label Cmp
Lt 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 Label
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 Offset
w == :: Label -> Label -> Bool
== Label Cmp
cmp' 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'
Label
LInf == Label
LInf = Bool
True
Label
_ == Label
_ = Bool
False
instance Ord Label where
Label Cmp
Lt Offset
w <= :: Label -> Label -> Bool
<= Label Cmp
Lt Offset
w' = Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
Label Cmp
Le Offset
w <= Label Cmp
Le Offset
w' = Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
Label Cmp
Lt Offset
w <= Label Cmp
Le 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 Cmp
Le Offset
w <= Label Cmp
Lt 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'
Label
_ <= Label
LInf = Bool
True
LInf{} <= Label{} = Bool
False
instance Pretty Label where
pretty :: Label -> Doc
pretty (Label Cmp
cmp 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 Label
LInf = Doc
"∞"
instance MeetSemiLattice Label where
Label
LInf meet :: Label -> Label -> Label
`meet` Label
l = Label
l
Label
l `meet` Label
LInf = Label
l
Label Cmp
Lt Offset
w `meet` Label Cmp
Lt 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 Cmp
Le Offset
w `meet` Label Cmp
Le 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 Cmp
Lt Offset
w `meet` Label Cmp
Le 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 Cmp
Le Offset
w `meet` Label Cmp
Lt 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 Label
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 = Weight
0
instance Dioid Label where
compose :: Label -> Label -> Label
compose (Label Cmp
Lt Offset
w) (Label Cmp
Lt 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 Offset
w) (Label Cmp
cmp' 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 Label
_ Label
LInf = Label
LInf
compose Label
LInf Label
_ = Label
LInf
unitCompose :: Label
unitCompose = Cmp -> Offset -> Label
Label Cmp
Le Offset
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
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
showsPrec :: Int -> Node rigid flex -> ShowS
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
show :: Node rigid flex -> String
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
showList :: [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
$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
/= :: 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
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
compare :: Node rigid flex -> Node rigid flex -> Ordering
$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
>= :: Node rigid flex -> Node rigid flex -> Bool
$cmax :: 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
$cmin :: 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
Ord)
instance (Pretty rigid, Pretty flex) => Pretty (Node rigid flex) where
pretty :: Node rigid flex -> Doc
pretty Node rigid flex
NodeZero = Doc
"0"
pretty Node rigid flex
NodeInfty = Doc
"∞"
pretty (NodeRigid rigid
x) = rigid -> Doc
forall a. Pretty a => a -> Doc
pretty rigid
x
pretty (NodeFlex flex
x) = flex -> Doc
forall a. Pretty a => a -> Doc
pretty flex
x
isFlexNode :: Node rigid flex -> Maybe flex
isFlexNode :: forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode (NodeFlex flex
x) = flex -> Maybe flex
forall a. a -> Maybe a
Just flex
x
isFlexNode Node rigid flex
_ = Maybe flex
forall a. Maybe a
Nothing
isZeroNode :: Node rigid flex -> Bool
isZeroNode :: forall rigid flex. Node rigid flex -> Bool
isZeroNode NodeZero{} = Bool
True
isZeroNode Node rigid flex
_ = Bool
False
isInftyNode :: Node rigid flex -> Bool
isInftyNode :: forall rigid flex. Node rigid flex -> Bool
isInftyNode NodeInfty{} = Bool
True
isInftyNode Node rigid flex
_ = Bool
False
nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr :: forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node rigid flex
n =
case Node rigid flex
n of
Node rigid flex
NodeZero -> Offset -> SizeExpr' rigid flex
forall rigid flex. Offset -> SizeExpr' rigid flex
Const Offset
0
Node rigid flex
NodeInfty -> SizeExpr' rigid flex
forall rigid flex. SizeExpr' rigid flex
Infty
NodeRigid rigid
i -> rigid -> Offset -> SizeExpr' rigid flex
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid rigid
i Offset
0
NodeFlex flex
x -> flex -> Offset -> SizeExpr' rigid flex
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex flex
x Offset
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 Node r f
u Node r f
v a
l) meet :: Edge' r f a -> Edge' r f a -> Edge' r f a
`meet` e' :: Edge' r f a
e'@(Edge Node r f
u' Node r f
v' 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 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 Node r f
u Node r f
v a
l) compose :: Edge' r f a -> Edge' r f a -> Edge' r f a
`compose` e' :: Edge' r f a
e'@(Edge Node r f
v' Node r f
w 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 :: forall r f a. 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 :: 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
NodeZero Graphs r f a
gs = ([], Graphs r f a
gs)
mentions Node r f
NodeInfty Graphs r f a
gs = ([], Graphs r f a
gs)
mentions NodeRigid{} Graphs r f a
gs = ([], Graphs r f a
gs)
mentions Node r f
n Graphs r f a
gs = (Graph 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 r f a -> Set (Node r f)) -> Graph r f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph 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 :: 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 e :: Edge' r f a
e@(Edge Node r f
src Node r f
dest a
l) Graphs r f a
gs =
let (Graphs r f a
gsSrc , 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
(Graphs r f a
gsDest, 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 :: forall r f a.
(Ord r, Ord f, Dioid a) =>
Set (Node r f) -> Graph r f a -> Graph r f a
reflClos Set (Node r f)
ns 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 {e} {rigid} {flex}.
(Dioid e, Ord rigid, Ord flex) =>
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 Graph (Node rigid flex) e
g 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 b a. (b -> a -> b) -> b -> [a] -> b
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]
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 :: 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 Graph r f a
h Graph r f a
g = (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Edge (Node r f) a -> Bool
test (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 Node r f
src Node r f
dest 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
Maybe a
Nothing -> Bool
False
Just a
l' ->
(a
l' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
l) Bool -> Bool -> Bool
|| ( String -> Bool -> Bool
forall a. String -> a -> a
trace
( String
"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 a b. a -> Edge (Node r f) b -> 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]
++ String
" 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 a b. a -> Edge (Node r f) b -> 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 :: forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr = \case
Const Offset
n -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeZero , Offset
n)
Rigid rigid
i Offset
n -> (rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid rigid
i, Offset
n)
Flex flex
x Offset
n -> (flex -> Node rigid flex
forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x , Offset
n)
SizeExpr' rigid flex
Infty -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty , Offset
0)
edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint :: forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint (Constraint SizeExpr' rigid flex
lexp Cmp
cmp SizeExpr' rigid flex
rexp) =
let (Node rigid flex
leftNode , Offset
n) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
lexp
(Node rigid flex
rightNode, 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 -> Edge (Node rigid flex) Label
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 :: forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [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 (Node rigid flex) Label
g = (Graph (Node rigid flex) Label
-> LabelledEdge rigid flex -> Graph (Node rigid flex) Label)
-> Graph (Node rigid flex) Label
-> [LabelledEdge rigid flex]
-> Graph (Node rigid flex) Label
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((LabelledEdge rigid flex
-> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label)
-> Graph (Node rigid flex) Label
-> LabelledEdge rigid flex
-> Graph (Node rigid flex) Label
forall a b c. (a -> b -> c) -> b -> a -> c
flip LabelledEdge rigid flex
-> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph (Node rigid flex) Label
forall n e. Graph n e
Graph.empty [LabelledEdge rigid flex]
edges
in Graph (Node rigid flex) Label
g
graphsFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints :: forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints [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 (FlexOf [Constraint' rigid flex])
forall a. Flexs a => a -> Set (FlexOf a)
flexs [Constraint' rigid flex]
cs
fedges :: [LabelledEdge rigid flex]
fedges = [[LabelledEdge rigid flex]] -> [LabelledEdge rigid flex]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[LabelledEdge rigid flex]] -> [LabelledEdge rigid flex])
-> [[LabelledEdge rigid flex]] -> [LabelledEdge rigid flex]
forall a b. (a -> b) -> a -> b
$ [flex]
-> (flex -> [LabelledEdge rigid flex])
-> [[LabelledEdge rigid flex]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [flex]
xs ((flex -> [LabelledEdge rigid flex])
-> [[LabelledEdge rigid flex]])
-> (flex -> [LabelledEdge rigid flex])
-> [[LabelledEdge rigid flex]]
forall a b. (a -> b) -> a -> b
$ \ flex
x ->
[ Node rigid flex
-> Node rigid flex -> Label -> LabelledEdge rigid flex
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 Offset
0)
, Node rigid flex
-> Node rigid flex -> Label -> LabelledEdge rigid flex
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 Offset
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 b a. (b -> a -> b) -> b -> [a] -> b
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]
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 Error = TCM Doc
type CTrans r f = Constraint' r f -> Either Error [Constraint' r f]
simplify1 :: (Pretty f, Pretty r, Eq r)
=> CTrans r f
-> CTrans r f
simplify1 :: forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 CTrans r f
f Constraint' r f
c = case CTrans r f -> CTrans r f
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
S.simplify1 ((TCMT IO Doc -> Maybe [Constraint' r f])
-> ([Constraint' r f] -> Maybe [Constraint' r f])
-> Either (TCMT IO Doc) [Constraint' r f]
-> Maybe [Constraint' r f]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe [Constraint' r f] -> TCMT IO Doc -> Maybe [Constraint' r f]
forall a b. a -> b -> a
const Maybe [Constraint' r f]
forall a. Maybe a
Nothing) [Constraint' r f] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
Just (Either (TCMT IO Doc) [Constraint' r f] -> Maybe [Constraint' r f])
-> CTrans r f -> CTrans r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CTrans r f
f) Constraint' r f
c of
Maybe [Constraint' r f]
Nothing -> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f])
-> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> Constraint' r f -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty Constraint' r f
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> TCMT IO Doc
"is inconsistent"
Just [Constraint' r f]
cs -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. b -> Either a b
Right [Constraint' r f]
cs
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 Error (HypGraph rigid flex)
hypGraph :: forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
Set rigid
-> [Hyp' rigid flex] -> Either (TCMT IO Doc) (HypGraph rigid flex)
hypGraph Set rigid
is [Hyp' rigid flex]
hyps0 = do
hyps <- [[Hyp' rigid flex]] -> [Hyp' rigid flex]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Hyp' rigid flex]] -> [Hyp' rigid flex])
-> Either (TCMT IO Doc) [[Hyp' rigid flex]]
-> Either (TCMT IO Doc) [Hyp' rigid flex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
-> [Hyp' rigid flex] -> Either (TCMT IO Doc) [[Hyp' rigid flex]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
-> Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 ((Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
-> Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
-> (Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
-> Hyp' rigid flex
-> Either (TCMT IO Doc) [Hyp' rigid flex]
forall a b. (a -> b) -> a -> b
$ \ Hyp' rigid flex
c -> [Hyp' rigid flex] -> Either (TCMT IO Doc) [Hyp' rigid flex]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Hyp' rigid flex
c]) [Hyp' rigid flex]
hyps0
let g = Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos (Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label)
-> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$
Set (Node rigid flex)
-> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
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) (Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label)
-> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$
[Hyp' rigid flex] -> Graph (Node rigid flex) Label
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Hyp' rigid flex]
hyps
when (negative g) $ Left "size hypotheses graph has negative loop"
return g
hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label
hypConn :: forall r f.
(Ord r, Ord f) =>
HypGraph r f -> Node r f -> Node r f -> Label
hypConn HypGraph r f
hg Node r f
n1 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 Offset
0
| Just 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 Error [Constraint' rigid flex]
simplifyWithHypotheses :: forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either (TCMT IO Doc) [Constraint' rigid flex]
simplifyWithHypotheses HypGraph rigid flex
hg [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 (TCMT IO Doc) [[Constraint' rigid flex]]
-> Either (TCMT IO Doc) [Constraint' rigid flex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint' rigid flex
-> Either (TCMT IO Doc) [Constraint' rigid flex])
-> [Constraint' rigid flex]
-> Either (TCMT IO Doc) [[Constraint' rigid flex]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Constraint' rigid flex
-> Either (TCMT IO Doc) [Constraint' rigid flex])
-> Constraint' rigid flex
-> Either (TCMT IO Doc) [Constraint' rigid flex]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 Constraint' rigid flex
-> Either (TCMT IO Doc) [Constraint' rigid flex]
test) [Constraint' rigid flex]
cons
where
test :: Constraint' rigid flex
-> Either (TCMT IO Doc) [Constraint' rigid flex]
test Constraint' rigid flex
c = do
let Edge Node rigid flex
n1 Node rigid flex
n2 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 (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Label
l' Label -> Label -> Bool
forall a. Ord a => a -> a -> Bool
<= Label
l) (Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ())
-> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Either (TCMT IO Doc) ()
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) ())
-> TCMT IO Doc -> Either (TCMT IO Doc) ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> Constraint' rigid flex -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty Constraint' rigid flex
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+>
TCMT IO Doc
"not consistent with size hypotheses"
[Constraint' rigid flex]
-> Either (TCMT IO Doc) [Constraint' rigid flex]
forall a. a -> Either (TCMT IO Doc) a
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 Error (ConGraph r f)
constraintGraph :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f]
-> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
constraintGraph [Constraint' r f]
cons0 Graph (Node r f) Label
hg = do
String -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either (TCMT IO Doc) ())
-> String -> Either (TCMT IO Doc) ()
forall a b. (a -> b) -> a -> b
$ String
"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
cons <- Graph (Node r f) Label
-> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either (TCMT IO Doc) [Constraint' rigid flex]
simplifyWithHypotheses Graph (Node r f) Label
hg [Constraint' r f]
cons0
traceM $ "simplified constraints cons = " ++ prettyShow cons
let g = Graph (Node r f) Label -> Graph (Node r f) Label
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos (Graph (Node r f) Label -> Graph (Node r f) Label)
-> Graph (Node r f) Label -> Graph (Node r f) Label
forall a b. (a -> b) -> a -> b
$ [Constraint' r f] -> Graph (Node r f) Label
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cons
traceM $ "transitive graph g = " ++ prettyShow (graphToList g)
when (negative g) $ Left $
"size constraint graph has negative loops"
unless (hg `implies` g) $ Left $
"size constraint graph constrains size hypotheses"
return 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 Error ([f], ConGraphs r f)
constraintGraphs :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f]
-> HypGraph r f -> Either (TCMT IO Doc) ([f], ConGraphs r f)
constraintGraphs [Constraint' r f]
cons0 ConGraph r f
hg = do
String -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either (TCMT IO Doc) ())
-> String -> Either (TCMT IO Doc) ()
forall a b. (a -> b) -> a -> b
$ String
"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
cons <- ConGraph r f
-> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either (TCMT IO Doc) [Constraint' rigid flex]
simplifyWithHypotheses ConGraph r f
hg [Constraint' r f]
cons0
traceM $ "simplified constraints cons = " ++ prettyShow cons
let gs0 = [Constraint' r f] -> [ConGraph r f]
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints [Constraint' r f]
cons
traceM $ "constraint forest gs0 = " ++ prettyShow (map graphToList gs0)
let gs1 = (ConGraph r f -> ConGraph r f) -> [ConGraph r f] -> [ConGraph r f]
forall a b. (a -> b) -> [a] -> [b]
map ConGraph r f -> ConGraph r f
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos [ConGraph r f]
gs0
traceM $ "transitive forest gs1 = " ++ prettyShow (map graphToList gs1)
let (xss,gs) = unzip $ map infinityFlexs gs1
xs = [[f]] -> [f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[f]]
xss
unless (null xs) $ do
traceM $ "flexibles to set to oo = " ++ prettyShow xs
traceM $ "forest after oo-subst = " ++ prettyShow (map graphToList gs)
when (negative gs) $ Left $ "size constraint graph has negative loop"
traceM $ "we are free of negative loops"
forM_ gs $ \ ConGraph r f
g -> Bool -> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConGraph r f
hg ConGraph r f -> ConGraph 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` ConGraph r f
g) (Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ())
-> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Either (TCMT IO Doc) ()
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) ())
-> TCMT IO Doc -> Either (TCMT IO Doc) ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"size constraint graph constrains size hypotheses"
traceM $ "any constraint between rigids is implied by the hypotheses"
return (xs, gs)
infinityFlexs :: (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs :: forall r f. (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs 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 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 [f]
xs (NodeFlex f
x) | f
x f -> [f] -> Bool
forall a. Eq a => a -> [a] -> 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 [f]
xs 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 [f]
xs (Edge Node r f
n1 Node r f
n2 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 [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 Node rigid flex
NodeInfty Node rigid flex
NodeInfty (Label Cmp
Le Offset
_)) = Bool
False
h Edge (Node rigid flex) Label
_ = Bool
True
instance Plus Offset Weight Weight where
plus :: Offset -> Weight -> Weight
plus Offset
e Weight
Infinity = Weight
Infinity
plus Offset
e (Offset 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 SizeExpr' r f
e Weight
Infinity = SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
plus SizeExpr' r f
e (Offset 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 SizeExpr' r f
e 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 :: forall r f. Bound r f
emptyBound = Map f (Set (SizeExpr' r f))
forall k a. Map k a
Map.empty
data Bounds r f = Bounds
{ forall r f. Bounds r f -> Bound r f
lowerBounds :: Bound r f
, forall r f. Bounds r f -> Bound r f
upperBounds :: Bound r f
, forall r f. Bounds r f -> Set f
mustBeFinite :: Set f
}
edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound :: forall r f. LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound LabelledEdge r f
e =
case LabelledEdge r f
e of
(Edge Node r f
n1 Node r f
n2 Label
LInf) -> Maybe (f, SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Edge Node r f
NodeZero (NodeFlex f
x) (Label Cmp
Le Offset
o)) | Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
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 Offset
0)
(Edge Node r f
NodeZero (NodeFlex f
x) (Label Cmp
Lt Offset
o)) | Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
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 Offset
0)
(Edge Node r f
n1 (NodeFlex f
x) 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)))
LabelledEdge r f
_ -> Maybe (f, SizeExpr' r f)
forall a. Maybe a
Nothing
edgeToUpperBound :: LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
edgeToUpperBound :: forall r f. LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
edgeToUpperBound LabelledEdge r f
e =
case LabelledEdge r f
e of
(Edge Node r f
n1 Node r f
n2 Label
LInf) -> Maybe (f, Cmp, SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(Edge Node r f
n1 Node r f
NodeInfty (Label Cmp
Le Offset
_)) -> Maybe (f, Cmp, SizeExpr' r f)
forall a. Maybe a
Nothing
(Edge (NodeFlex f
x) Node r f
NodeInfty (Label Cmp
Lt Offset
_)) -> (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 f
x) Node r f
n2 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))
LabelledEdge r f
_ -> Maybe (f, Cmp, SizeExpr' r f)
forall a. Maybe a
Nothing
graphToLowerBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
graphToLowerBounds :: forall r f. (Ord r, Ord f) => [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 b a. (b -> a -> b) -> b -> [a] -> b
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
$ \ Bound r f
bs 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
Maybe (f, SizeExpr' r f)
Nothing -> Bound r f
bs
Just (f
x, Flex{}) -> Bound r f
bs
Just (f
x, 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 :: forall r f.
(Ord r, Ord f) =>
[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 b a. (b -> a -> b) -> b -> [a] -> b
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
$ \ (Bound r f
bs, Set f
fs) 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
Maybe (f, Cmp, SizeExpr' r f)
Nothing -> (Bound r f
bs, Set f
fs)
Just (f
x, Cmp
_, Flex{}) -> (Bound r f
bs, Set f
fs)
Just (f
x, Cmp
Lt, SizeExpr' r f
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 (f
x, Cmp
Le, 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)
Maybe (f, Cmp, SizeExpr' r f)
_ -> (Bound r f, Set f)
forall a. HasCallStack => a
__IMPOSSIBLE__
bounds :: (Ord r, Ord f) => ConGraph r f -> Bounds r f
bounds :: forall r f. (Ord r, Ord f) => ConGraph r f -> Bounds r f
bounds 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
(Bound r f
ubs, 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 :: forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
smallest HypGraph r f
hg [Node r f]
ns
| Node r f
forall rigid flex. Node rigid flex
NodeZero Node r f -> [Node r f] -> Bool
forall a. Eq a => a -> [a] -> 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 Node r f
NodeInfty = Bool
False
hasNoPred 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 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')
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
guard (toWeight l <= 0)
return ()
largest ::(Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
largest :: forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
largest HypGraph r f
hg [Node r f]
ns
| Node r f
forall rigid flex. Node rigid flex
NodeInfty Node r f -> [Node r f] -> Bool
forall a. Eq a => a -> [a] -> 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 Node r f
NodeZero = Bool
False
hasNoSucc 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 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')
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'
guard (toWeight l <= 0)
return ()
commonSuccs :: (Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs :: 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 r f a
hg [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 {e}.
[Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) 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 (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
buildmap = ([Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e])
-> [(Node r f, [Edge (Node r f) e])]
-> Map (Node r f) [Edge (Node r f) e]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e]
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(Node r f, [Edge (Node r f) e])]
-> Map (Node r f) [Edge (Node r f) e])
-> ([Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])])
-> [Edge (Node r f) e]
-> Map (Node r f) [Edge (Node r f) e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge (Node r f) e -> (Node r f, [Edge (Node r f) e]))
-> [Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])]
forall a b. (a -> b) -> [a] -> [b]
map (\ Edge (Node r f) e
e -> (Edge (Node r f) e -> Node r f
forall n e. Edge n e -> n
dest Edge (Node r f) e
e, [Edge (Node r f) e
e]))
intersectAll :: [Map k [a]] -> Map k [a]
intersectAll [] = Map k [a]
forall k a. Map k a
Map.empty
intersectAll (Map k [a]
m:[Map k [a]]
ms) = (Map k [a] -> Map k [a] -> Map k [a])
-> Map k [a] -> [Map k [a]] -> Map k [a]
forall b a. (b -> a -> b) -> b -> [a] -> b
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 :: forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonPreds Graph r f a
hg [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 {e}.
[Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) 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 (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
buildmap = ([Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e])
-> [(Node r f, [Edge (Node r f) e])]
-> Map (Node r f) [Edge (Node r f) e]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e]
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(Node r f, [Edge (Node r f) e])]
-> Map (Node r f) [Edge (Node r f) e])
-> ([Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])])
-> [Edge (Node r f) e]
-> Map (Node r f) [Edge (Node r f) e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge (Node r f) e -> (Node r f, [Edge (Node r f) e]))
-> [Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])]
forall a b. (a -> b) -> [a] -> [b]
map (\ Edge (Node r f) e
e -> (Edge (Node r f) e -> Node r f
forall n e. Edge n e -> n
src Edge (Node r f) e
e, [Edge (Node r f) e
e]))
intersectAll :: [Map k [a]] -> Map k [a]
intersectAll [] = Map k [a]
forall k a. Map k a
Map.empty
intersectAll (Map k [a]
m:[Map k [a]]
ms) = (Map k [a] -> Map k [a] -> Map k [a])
-> Map k [a] -> [Map k [a]] -> Map k [a]
forall b a. (b -> a -> b) -> b -> [a] -> b
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' :: 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
node1, Offset
n) (Node r f
node2, 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 (String
"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
[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 Node r f
node1x Node r f
n1 Label
l1 ,
Edge Node r f
node2x Node r f
n2 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 a. a -> Maybe a
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
[Edge' r f Label]
_ -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
[Node r f]
_ -> 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 (String
"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]
++ String
" 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]
++ String
" 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' :: 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
node1, Offset
n) (Node r f
node2, 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 (String
"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
[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 Node r f
n1 Node r f
node1x Label
l1 ,
Edge Node r f
n2 Node r f
node2x 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 a. a -> Maybe a
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
[Edge' r f Label]
_ -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
[Node r f]
_ -> 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 (String
"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]
++ String
" 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]
++ String
" 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 :: 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
a1 SizeExpr' r f
a2 =
case (SizeExpr' r f
a1, SizeExpr' r f
a2) of
(Flex{}, SizeExpr' r f
_) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(SizeExpr' r f
_, Flex{}) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(SizeExpr' r f
Infty, 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
(SizeExpr' r f
a1, SizeExpr' r f
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 Offset
n , Const 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 Offset
n , Rigid r
j 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 r
i Offset
n, Const 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 r
i Offset
n, Rigid r
j 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 :: 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
a1 SizeExpr' r f
a2 =
case (SizeExpr' r f
a1, SizeExpr' r f
a2) of
(Flex{}, SizeExpr' r f
_) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(SizeExpr' r f
_, Flex{}) -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
(SizeExpr' r f
Infty, SizeExpr' r f
a2) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a2
(SizeExpr' r f
a1, SizeExpr' r f
Infty) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a1
(Const Offset
n , Const 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 Offset
n , Rigid r
i 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 r
i Offset
n, Const 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 r
i Offset
n, Rigid r
j 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 :: forall r f.
(Ord r, Ord f) =>
HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
findRigidBelow HypGraph r f
hg (Rigid r
i Offset
m) | Offset
m Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
< Offset
0 = do
let v :: Node r f
v = r -> Node r f
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
v
filt :: Edge' r f Label -> Maybe (Node r f, Offset)
filt e :: Edge' r f Label
e@(Edge Node r f
n Node r f
n' Label
l)
| Node r f
n' Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
v =
case Label -> Weight
toWeight Label
l of
Weight
Infinity -> Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
Offset Offset
o -> if Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
m then (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
Just (Node r f
n, Offset
o) else Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
| Bool
otherwise = Maybe (Node r f, 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)
filt [Edge' r f Label]
preds
(n, o) <- do
case [(Node r f, Offset)]
cands of
[] -> Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
[(Node r f, Offset)
c] -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Node r f, Offset)
c
[(Node r f, Offset)]
_ -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
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
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
o
unless (offset >= 0) __IMPOSSIBLE__
return $ nodeToSizeExpr n `plus` offset
findRigidBelow HypGraph r f
hg SizeExpr' r f
e = Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
solveGraph
:: forall r f. (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> ConGraph r f
-> Either Error (Solution r f)
solveGraph :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> HypGraph r f
-> Either (TCMT IO Doc) (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg HypGraph r f
g = do
let (Bounds Bound r f
lbs Bound r f
ubs 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 :: [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 ]
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 (TCMT IO Doc) [Maybe (f, SizeExpr' r f)]
-> Either (TCMT IO Doc) [(f, SizeExpr' r f)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[f]
-> (f -> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f)))
-> Either (TCMT IO Doc) [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 (TCMT IO Doc) (Maybe (f, SizeExpr' r f)))
-> Either (TCMT IO Doc) [Maybe (f, SizeExpr' r f)])
-> (f -> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f)))
-> Either (TCMT IO Doc) [Maybe (f, SizeExpr' r f)]
forall a b. (a -> b) -> a -> b
$ \ f
x -> (SizeExpr' r f -> (f, SizeExpr' r f))
-> Maybe (SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f
x,) (Maybe (SizeExpr' r f) -> Maybe (f, SizeExpr' r f))
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
-> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"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
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SizeExpr' r f] -> String
forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
lx)
String -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"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
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SizeExpr' r f] -> String
forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
ux)
lb <- do
case [SizeExpr' r f]
lx of
[] -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
(SizeExpr' r f
a:[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
Just SizeExpr' r f
l -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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)
Nothing -> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"inconsistent lower bound for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> f -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => f -> m Doc
P.prettyTCM f
x
ub <- do
case ux of
[] -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
(SizeExpr' r f
a:[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 SizeExpr' r f
l | SizeExpr' r f -> Bool
forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' r f
l -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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 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 (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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'
Maybe (SizeExpr' r f)
_ -> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"inconsistent upper bound for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> f -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => f -> m Doc
P.prettyTCM f
x
case (lb, ub) of
(Just SizeExpr' r f
l, Maybe (SizeExpr' r f)
Nothing) -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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
(Maybe (SizeExpr' r f)
Nothing, Just SizeExpr' r f
u) -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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
u
(Just SizeExpr' r f
l, Just SizeExpr' r f
u) -> do
String -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"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
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
l)
String -> Either (TCMT IO Doc) ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"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
": " 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
Polarity
Least -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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
Polarity
Greatest -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (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
u
(Maybe (SizeExpr' r f), Maybe (SizeExpr' r f))
_ -> Maybe (SizeExpr' r f)
-> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
return $ Solution $ Map.fromDistinctAscList xas
solveGraphs
:: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> ConGraphs r f
-> Either Error (Solution r f)
solveGraphs :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> ConGraphs r f
-> Either (TCMT IO Doc) (Solution r f)
solveGraphs Polarities f
pols HypGraph r f
hg 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 (TCMT IO Doc) [Map f (SizeExpr' r f)]
-> Either (TCMT IO Doc) (Solution r f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HypGraph r f -> Either (TCMT IO Doc) (Map f (SizeExpr' r f)))
-> ConGraphs r f -> Either (TCMT IO Doc) [Map f (SizeExpr' r f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 (TCMT IO Doc) (Solution r f))
-> HypGraph r f
-> Either (TCMT IO Doc) (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 (TCMT IO Doc) (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> HypGraph r f
-> Either (TCMT IO Doc) (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 Error ()
verifySolution :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> [Constraint' r f] -> Solution r f -> Either (TCMT IO Doc) ()
verifySolution HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol = do
cs <- [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f])
-> [Constraint' r f] -> Either (TCMT IO Doc) [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
traceM $ "substituted constraints " ++ prettyShow cs
cs <-
concat <$> mapM (simplify1 $ \ Constraint' r f
c -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c]) cs
traceM $ "simplified substituted constraints " ++ prettyShow cs
let 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
unless (hg `implies` g) $
Left "solution not implied by hypotheses"
iterateSolver
:: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either Error (Solution r f)
iterateSolver :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either (TCMT IO Doc) (Solution r f)
iterateSolver Polarities f
pols HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol0 = do
g <- [Constraint' r f]
-> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f]
-> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
constraintGraph [Constraint' r f]
cs HypGraph r f
hg
sol <- solveGraph pols hg g
traceM $ "(partial) solution " ++ prettyShow sol
if null sol then return sol0 else
iterateSolver pols hg (subst sol cs) $ Solution $
Map.unionWith __IMPOSSIBLE__ (theSolution sol) $
theSolution $ subst sol sol0
testSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]
testSuccs :: forall f. Ord f => 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
hg [Node String f
forall {flex}. Node String flex
n1,Node String f
forall {flex}. Node String flex
n2]
where
n1 :: Node String flex
n1 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"i"
n2 :: Node String flex
n2 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"j"
n3 :: Node String flex
n3 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"k"
n4 :: Node String flex
n4 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"l"
n5 :: Node String flex
n5 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"m"
hg :: Graph String f Label
hg = [Edge' String f Label] -> Graph String f Label
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
[ Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n3 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
1
, Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
2
, Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
3
, Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n3 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
4
, Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
5
, Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
6
]
testLub :: (Pretty f, Ord f, Show f) => Maybe (SizeExpr' [Char] f)
testLub :: forall f. (Pretty f, Ord f, Show f) => 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
hg (String -> Offset -> SizeExpr' String f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid String
"i" Offset
0) (String -> Offset -> SizeExpr' String f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid String
"j" Offset
2)
where
n1 :: Node String flex
n1 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"i"
n2 :: Node String flex
n2 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"j"
n3 :: Node String flex
n3 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"k"
n4 :: Node String flex
n4 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"l"
n5 :: Node String flex
n5 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"m"
hg :: HypGraph String f
hg = [Edge (Node String f) Label] -> HypGraph String f
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
[ Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n3 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
0
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
2
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
4
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n3 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
1
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
3
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
5
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n3 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
0
, Node String f
-> Node String f -> Label -> Edge (Node String f) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n3 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge (Node String f) Label)
-> Label -> Edge (Node String f) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Lt Offset
0
]