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.Pretty (PrettyTCM)
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.SizedTypes.Syntax
import Agda.TypeChecking.SizedTypes.Utils

import Agda.Utils.Graph.AdjacencyMap.Unidirectional
  (Edge(..), Nodes(..), nodes, computeNodes)
-- (Edge'(..), allNodes, emptyGraph, insertEdge, graphToList, graphFromList, nodes, lookupEdge, outgoing, incoming, diagonal, transClos)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph

import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty

import Agda.Utils.Impossible

type Graph r f a = Graph.Graph (Node r f) a
type Edge' r f a = Graph.Edge  (Node r f) a
type Key r f = Edge' r f ()
type Nodes r f = Graph.Nodes (Node r f)
type LabelledEdge r f = Edge' r f Label

src :: Edge n e -> n
src :: forall n e. Edge n e -> n
src = forall n e. Edge n e -> n
Graph.source

dest :: Edge n e -> n
dest :: forall n e. Edge n e -> n
dest = 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 = 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 = 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 = 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
  | forall a. Top a => a -> Bool
isTop (forall n e. Edge n e -> e
label Edge n e
e) = Graph n e
g
  | Bool
otherwise       = forall n e.
Ord n =>
(e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
Graph.insertEdgeWith forall a. MeetSemiLattice a => a -> a -> a
meet Edge n e
e Graph n e
g

-- | Compute list of edges that start in a given node.
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 = forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesFrom Graph r f a
g [Node r f
s]

-- | Compute list of edges that target a given node.
--
--   Note: expensive for unidirectional graph representations.
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 = forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesTo Graph r f a
g [Node r f
t]

-- | @Set.foldl@ does not exist in legacy versions of the @containers@ package.
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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' b -> a -> b
step b
start forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toAscList
-- setFoldl = Set.foldl'

-- | Floyd-Warshall algorithm.
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 = forall b a. (b -> a -> b) -> b -> Set a -> b
setFoldl Graph n a -> n -> Graph n a
step Graph n a
g forall a b. (a -> b) -> a -> b
$ forall n. Nodes n -> Set n
allNodes Nodes n
ns
  where
    ns :: Nodes n
ns       = forall n e. Ord n => Graph n e -> Nodes n
computeNodes Graph n a
g
    srcs :: [n]
srcs     = forall a. Set a -> [a]
Set.toAscList forall a b. (a -> b) -> a -> b
$ forall n. Nodes n -> Set n
srcNodes Nodes n
ns
    dests :: [n]
dests    = forall a. Set a -> [a]
Set.toAscList forall a b. (a -> b) -> a -> b
$ forall n. Nodes n -> Set n
tgtNodes Nodes n
ns
    -- @step g v@ adds all intermediate edges @u --> w@ via @v@ to @g@
    -- step :: (Ord n, Dioid a) => Graph.Graph n n a -> n -> Graph.Graph n n a
    step :: Graph n a -> n -> Graph n a
step Graph n a
g n
v = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph n a
g forall a b. (a -> b) -> a -> b
$
      [ forall n e. n -> n -> e -> Edge n e
Edge n
u n
w forall a b. (a -> b) -> a -> b
$ a
l1 forall a. Dioid a => a -> a -> a
`compose` a
l2
        | n
u <- [n]
srcs
        , n
w <- [n]
dests
        , a
l1 <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n a
g n
u n
v
        , a
l2 <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph n a
g n
v n
w
      ]

-- * Edge weights

data Weight
  = Offset Offset
  | Infinity
  deriving (Weight -> Weight -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Weight -> Weight -> Bool
$c/= :: Weight -> Weight -> Bool
== :: Weight -> Weight -> Bool
$c== :: Weight -> Weight -> Bool
Eq, Int -> Weight -> ShowS
[Weight] -> ShowS
Weight -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Weight] -> ShowS
$cshowList :: [Weight] -> ShowS
show :: Weight -> String
$cshow :: Weight -> String
showsPrec :: Int -> Weight -> ShowS
$cshowsPrec :: Int -> Weight -> ShowS
Show)

instance Pretty Weight where
  pretty :: Weight -> Doc
pretty (Offset Offset
x) = 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 forall a. Ord a => a -> a -> Bool
<= Offset
y

instance MeetSemiLattice Weight where
  meet :: Weight -> Weight -> Weight
meet = 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 (forall a. Enum a => a -> a
succ Offset
x)
  succ (Weight
Infinity) = Weight
Infinity
  pred :: Weight -> Weight
pred (Offset Offset
x) = Offset -> Weight
Offset (forall a. Enum a => a -> a
pred Offset
x)
  pred (Weight
Infinity) = Weight
Infinity
  toEnum :: Int -> Weight
toEnum = Offset -> Weight
Offset forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum
  fromEnum :: Weight -> Int
fromEnum (Offset Offset
x) = forall a. Enum a => a -> Int
fromEnum Offset
x
  fromEnum (Weight
Infinity) = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Partial implementation of @Num@.
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 forall a b. (a -> b) -> a -> b
$ Offset
x 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 forall a b. (a -> b) -> a -> b
$ Offset
x forall a. Num a => a -> a -> a
- Offset
y
  Weight
x        - Weight
Infinity = forall a. HasCallStack => a
__IMPOSSIBLE__
  abs :: Weight -> Weight
abs (Offset Offset
x)      = Offset -> Weight
Offset forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
abs Offset
x
  abs Weight
Infinity        = Weight
Infinity
  signum :: Weight -> Weight
signum (Offset Offset
x)   = Offset -> Weight
Offset forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
signum Offset
x
  signum Weight
Infinity     = Offset -> Weight
Offset forall a b. (a -> b) -> a -> b
$ Offset
1
  fromInteger :: Integer -> Weight
fromInteger Integer
x       = Offset -> Weight
Offset (forall a. Num a => Integer -> a
fromInteger Integer
x)
  Weight
x * :: Weight -> Weight -> Weight
* Weight
y = forall a. HasCallStack => a
__IMPOSSIBLE__

instance Plus Weight Offset Weight where
  plus :: Weight -> Offset -> Weight
plus Weight
w Offset
k = Weight
w forall a. Num a => a -> a -> a
+ (Offset -> Weight
Offset Offset
k)

-- | Test for negativity, used to detect negative cycles.
class Negative a where
  negative :: a -> Bool

{- leads to Undecidable/OverlappingInstances:
instance (Ord a, Num a) => Negative a where
  negative = (< 0)
-}

instance Negative Int where
  negative :: Int -> Bool
negative = (forall a. Ord a => a -> a -> Bool
< Int
0)

instance Negative Offset where
  negative :: Offset -> Bool
negative (O Int
x) = 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) = forall a. Negative a => a -> Bool
negative Offset
x

-- * Edge labels

-- | Going from @Lt@ to @Le@ is @pred@, going from @Le@ to @Lt@ is @succ@.
--
--   @X --(R,n)--> Y@
--   means  @X (R) Y + n@.
--   [                      ... if @n@ positive
--     and    @X + (-n) (R) Y@  if @n@ negative. ]
data Label
  = Label { Label -> Cmp
lcmp :: Cmp, Label -> Offset
loffset :: Offset }
  | LInf  -- ^ Nodes not connected.
  deriving (Int -> Label -> ShowS
[Label] -> ShowS
Label -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Label] -> ShowS
$cshowList :: [Label] -> ShowS
show :: Label -> String
$cshow :: Label -> String
showsPrec :: Int -> Label -> ShowS
$cshowsPrec :: Int -> Label -> ShowS
Show)


-- | Convert a label to a weight, decrementing in case of 'Lt'.
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 forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
pred Offset
w
toWeight Label
LInf         = Weight
Infinity

instance Negative Label where
  negative :: Label -> Bool
negative = forall a. Negative a => a -> Bool
negative 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 forall a. Eq a => a -> a -> Bool
== Cmp
cmp' Bool -> Bool -> Bool
&& Offset
w 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 forall a. Ord a => a -> a -> Bool
<= Offset
w'
  Label Cmp
Le  Offset
w <= Label Cmp
Le Offset
w' = Offset
w forall a. Ord a => a -> a -> Bool
<= Offset
w'
  Label Cmp
Lt  Offset
w <= Label Cmp
Le Offset
w' = forall a. Enum a => a -> a
pred Offset
w forall a. Ord a => a -> a -> Bool
<= Offset
w'
  Label Cmp
Le  Offset
w <= Label Cmp
Lt Offset
w' = forall a. Enum a => a -> a
succ Offset
w 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) = forall a. Pretty a => a -> Doc
pretty Cmp
cmp forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty Offset
w
  pretty Label
LInf          = Doc
"∞"

instance MeetSemiLattice Label where
  -- one label is neutral
  Label
LInf       meet :: Label -> Label -> Label
`meet` Label
l           = Label
l
  Label
l          `meet` Label
LInf        = Label
l
  -- other cases
  Label Cmp
Lt Offset
w `meet` Label Cmp
Lt Offset
w' = Cmp -> Offset -> Label
Label Cmp
Lt forall a b. (a -> b) -> a -> b
$ Offset
w      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 forall a b. (a -> b) -> a -> b
$ Offset
w      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 forall a b. (a -> b) -> a -> b
$      Offset
w forall a. MeetSemiLattice a => a -> a -> a
`meet` 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 forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
succ Offset
w 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

-- * Semiring with idempotent '+' == dioid

instance Dioid Weight where
  compose :: Weight -> Weight -> Weight
compose     = 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 forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
pred forall a b. (a -> b) -> a -> b
$ Offset
w forall a. Num a => a -> a -> a
+ Offset
w'
  compose (Label Cmp
cmp Offset
w) (Label Cmp
cmp' Offset
w') = Cmp -> Offset -> Label
Label (forall a. Dioid a => a -> a -> a
compose Cmp
cmp Cmp
cmp') forall a b. (a -> b) -> a -> b
$ Offset
w 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

-- * Graphs

-- ** Nodes

data Node rigid flex
  = NodeZero
  | NodeInfty
  | NodeRigid rigid
  | NodeFlex  flex
  deriving (Int -> Node rigid flex -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
showList :: [Node rigid flex] -> ShowS
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
show :: Node rigid flex -> String
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
showsPrec :: Int -> Node rigid flex -> ShowS
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
Show, Node rigid flex -> Node rigid flex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
/= :: Node rigid flex -> Node rigid flex -> Bool
$c/= :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
== :: Node rigid flex -> Node rigid flex -> Bool
$c== :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
Eq, Node rigid flex -> Node rigid flex -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {rigid} {flex}.
(Ord rigid, Ord flex) =>
Eq (Node rigid flex)
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
min :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmin :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
max :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmax :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
>= :: Node rigid flex -> Node rigid flex -> Bool
$c>= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
> :: Node rigid flex -> Node rigid flex -> Bool
$c> :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
<= :: Node rigid flex -> Node rigid flex -> Bool
$c<= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
< :: Node rigid flex -> Node rigid flex -> Bool
$c< :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
compare :: Node rigid flex -> Node rigid flex -> Ordering
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
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) = forall a. Pretty a => a -> Doc
pretty rigid
x
  pretty (NodeFlex  flex
x) = 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) = forall a. a -> Maybe a
Just flex
x
isFlexNode Node rigid 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    -> forall rigid flex. Offset -> SizeExpr' rigid flex
Const Offset
0
    Node rigid flex
NodeInfty   -> forall rigid flex. SizeExpr' rigid flex
Infty
    NodeRigid rigid
i -> forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid rigid
i Offset
0
    NodeFlex flex
x  -> forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex flex
x Offset
0

-- ** Edges

-- | An edge is negative if its label is.
instance Negative a => Negative (Edge' r f a) where
  negative :: Edge' r f a -> Bool
negative = forall a. Negative a => a -> Bool
negative forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Eq a => a -> a -> Bool
== Node r f
u' Bool -> Bool -> Bool
&& Node r f
v forall a. Eq a => a -> a -> Bool
== Node r f
v' = forall n e. n -> n -> e -> Edge n e
Edge Node r f
u Node r f
v forall a b. (a -> b) -> a -> b
$ a
l forall a. MeetSemiLattice a => a -> a -> a
`meet` a
l'
    | Bool
otherwise          = forall a. HasCallStack => a
__IMPOSSIBLE__
       -- error $ show e ++ " `meet` " ++ show e'

instance (Ord r, Ord f, Top a) => Top (Edge' r f a) where
  top :: Edge' r f a
top = forall a. HasCallStack => a
__IMPOSSIBLE__
  isTop :: Edge' r f a -> Bool
isTop Edge' r f a
e = forall a. Top a => a -> Bool
isTop (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 forall a. Eq a => a -> a -> Bool
== Node r f
v'    = forall n e. n -> n -> e -> Edge n e
Edge Node r f
u Node r f
w forall a b. (a -> b) -> a -> b
$ a
l forall a. Dioid a => a -> a -> a
`compose` a
l'
   | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
      -- error $ show e ++ " `compose` " ++ show e'
  unitCompose :: Edge' r f a
unitCompose  = forall a. HasCallStack => a
__IMPOSSIBLE__

-- ** Graphs

-- | A graph forest.
type Graphs r f a = [Graph r f a]

emptyGraphs :: Graphs r f a
emptyGraphs :: forall r f a. Graphs r f a
emptyGraphs = []

-- | Split a list of graphs @gs@ into those that mention node @n@ and those that do not.
--   If @n@ is zero or infinity, we regard it as "not mentioned".
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 = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (forall a. Ord a => a -> Set a -> Bool
Set.member Node r f
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Graph n e -> Set n
nodes) Graphs r f a
gs

-- | Add an edge to a graph forest.
--   Graphs that share a node with the edge are joined.
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 =
  -- Note: If we started from an empty forest
  -- and only added edges via @addEdge@, then
  -- @gsSrc@ and @gsDest@ contain each at most one graph.
  let (Graphs r f a
gsSrc , Graphs r f a
gsNotSrc)  = 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) = 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 forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge Edge' r f a
e (forall n e. Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
Graph.unionsWith forall a. MeetSemiLattice a => a -> a -> a
meet forall a b. (a -> b) -> a -> b
$ Graphs r f a
gsSrc forall a. [a] -> [a] -> [a]
++ Graphs r f a
gsDest) forall a. a -> [a] -> [a]
: Graphs r f a
gsNotDest

-- | Reflexive closure.  Add edges @0 -> n -> n -> oo@ for all nodes @n@.
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 = forall b a. (b -> a -> b) -> b -> Set a -> b
setFoldl 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
    -- have at least the nodes in @ns@
    ns' :: Set (Node r f)
ns'      = forall n e. Graph n e -> Set n
nodes Graph r f a
g forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (Node r f)
ns
    -- add the trivial edges for all nodes 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = [ forall n e. n -> n -> e -> Edge n e
Edge forall rigid flex. Node rigid flex
NodeZero Node rigid flex
n  forall a. Dioid a => a
unitCompose
           , forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
n        Node rigid flex
n  forall a. Dioid a => a
unitCompose
           , forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
n forall rigid flex. Node rigid flex
NodeInfty forall a. Dioid a => a
unitCompose
           ]

-- UNUSED
-- -- | Reflexive-transitive closure.
-- complete :: (Pretty a, Dioid a) => Graph r f a -> Graph r f a
-- complete = transClos . reflClos

-- | A graph is 'negative' if it contains a negative loop (diagonal edge).
--   Makes sense on transitive graphs.
instance (Ord r, Ord f, Negative a) => Negative (Graph r f a) where
  negative :: Graph r f a -> Bool
negative = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Negative a => a -> Bool
negative forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Negative a => a -> Bool
negative

-- | @h `implies` g@ if any edge in @g@ between rigids and constants
--   is implied by a corresponding edge in @h@, which means that
--   the edge in @g@ carries at most the information of the one in @h@.
--
--   Application: Constraint implication: Constraints are compatible
--   with hypotheses.
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
-- iterate 'test' over all edges in g
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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Edge (Node r f) a -> Bool
test (forall n e. Graph n e -> [Edge n e]
graphToList Graph r f a
g)
  where
    -- NB: doing the @test k l@ before the recursive @b@ gives
    -- opportunity to short-cut the conjunction @&&@.
    -- test :: Key -> a -> Bool
    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)
      | forall rigid flex. Node rigid flex -> Bool
isZeroNode Node r f
src, Bool -> Bool
not (forall a. Negative a => a -> Bool
negative a
l) = Bool
True
      | forall rigid flex. Node rigid flex -> Bool
isInftyNode Node r f
dest                 = Bool
True
      | forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode Node r f
src          = Bool
True
      | forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode Node r f
dest         = Bool
True
      | forall a. Top a => a -> Bool
isTop a
l                          = Bool
True
      | Bool
otherwise = case 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' forall a. Ord a => a -> a -> Bool
<= a
l) Bool -> Bool -> Bool
|| ( forall a. String -> a -> a
trace
                           ( String
"edge " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (a
l forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Edge (Node r f) a
k)
                               forall a. [a] -> [a] -> [a]
++ String
" not implied by "
                               forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (a
l' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Edge (Node r f) a
k)
                           )
                           forall a b. (a -> b) -> a -> b
$ Bool
False
                       )

-- implies h g = Map.foldlWithKey (\ b k l -> test k l && b) True g
--   -- NB: doing the @test k l@ before the recursive @b@ gives
--   -- opportunity to short-cut the conjunction @&&@.
--   where
--     -- test :: Key -> a -> Bool
--     test k@(Edge src dest ()) l
--       | isZeroNode src, not (negative l) = True
--       | isInftyNode dest                 = True
--       | isJust $ isFlexNode src          = True
--       | isJust $ isFlexNode dest         = True
--       | isTop l                          = True
--       | otherwise = case lookupEdge h src dest of
--         Nothing -> False
--         Just l' -> if l' <= l then True else
--           trace ("edge " ++ show (l <$ k) ++ " not implied by " ++ show (l' <$ k)) $
--             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 -> (forall rigid flex. Node rigid flex
NodeZero   , Offset
n)
  Rigid rigid
i Offset
n -> (forall rigid flex. rigid -> Node rigid flex
NodeRigid rigid
i, Offset
n)
  Flex  flex
x Offset
n -> (forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x , Offset
n)
  SizeExpr' rigid flex
Infty     -> (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) = forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
lexp
      (Node rigid flex
rightNode, Offset
m) = forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
rexp
  in forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
leftNode Node rigid flex
rightNode (Cmp -> Offset -> Label
Label Cmp
cmp forall a b. (a -> b) -> a -> b
$ Offset
m forall a. Num a => a -> a -> a
- Offset
n)

-- | Build a graph from list of simplified constraints.
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 -- convert to edges
      edges :: [LabelledEdge rigid flex]
edges = forall a b. (a -> b) -> [a] -> [b]
map forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint [Constraint' rigid flex]
cs
      -- build a graph from the edges
      g :: Graph (Node rigid flex) Label
g     = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) forall n e. Graph n e
Graph.empty [LabelledEdge rigid flex]
edges
  in  Graph (Node rigid flex) Label
g

-- | Build a graph from list of simplified constraints.
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 -- convert to edges
      edges :: [LabelledEdge rigid flex]
edges = forall a b. (a -> b) -> [a] -> [b]
map forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint [Constraint' rigid flex]
cs
      -- get all the flexibles mentioned in constraints
      xs :: [flex]
xs    = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. Flexs a => a -> Set (FlexOf a)
flexs [Constraint' rigid flex]
cs
      -- for each flexible X, add edges 0 <= X and X <= oo
      fedges :: [LabelledEdge rigid flex]
fedges = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [flex]
xs forall a b. (a -> b) -> a -> b
$ \ flex
x ->
        [ forall n e. n -> n -> e -> Edge n e
Edge forall rigid flex. Node rigid flex
NodeZero (forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x) (Cmp -> Offset -> Label
Label Cmp
Le Offset
0)
        , forall n e. n -> n -> e -> Edge n e
Edge (forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x) forall rigid flex. Node rigid flex
NodeInfty (Cmp -> Offset -> Label
Label Cmp
Le Offset
0)
        ]
      -- build a graph from the edges
      gs :: Graphs rigid flex Label
gs    = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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) forall r f a. Graphs r f a
emptyGraphs ([LabelledEdge rigid flex]
fedges forall a. [a] -> [a] -> [a]
++ [LabelledEdge rigid flex]
edges)
  in  Graphs rigid flex Label
gs

-- Build hypotheses graph, complete it, check for negative loops.

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 Error (HypGraph rigid flex)
hypGraph Set rigid
is [Hyp' rigid flex]
hyps0 = do
  -- get a list of hypothesis from a list of constraints
  [Hyp' rigid flex]
hyps <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 forall a b. (a -> b) -> a -> b
$ \ Hyp' rigid flex
c -> forall (m :: * -> *) a. Monad m => a -> m a
return [Hyp' rigid flex
c]) [Hyp' rigid flex]
hyps0
  let g :: Graph (Node rigid flex) Label
g = forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos forall a b. (a -> b) -> a -> b
$
            forall r f a.
(Ord r, Ord f, Dioid a) =>
Set (Node r f) -> Graph r f a -> Graph r f a
reflClos (forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall rigid flex. rigid -> Node rigid flex
NodeRigid Set rigid
is) forall a b. (a -> b) -> a -> b
$
              forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Hyp' rigid flex]
hyps
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Negative a => a -> Bool
negative Graph (Node rigid flex) Label
g) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Error
"size hypotheses graph has negative loop"
  forall (m :: * -> *) a. Monad m => a -> m a
return Graph (Node rigid flex) Label
g

hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label
-- hypConn hg NodeZero n2  = Label Le 0  -- WRONG: not the best information
-- hypConn hg n1 NodeInfty = Label Le 0
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 forall a. Eq a => a -> a -> Bool
== Node r f
n2                                = Cmp -> Offset -> Label
Label Cmp
Le Offset
0
  | Just Label
l <- 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                               = 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 Error [Constraint' rigid flex]
simplifyWithHypotheses HypGraph rigid flex
hg [Constraint' rigid flex]
cons = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 Constraint' rigid flex -> Either Error [Constraint' rigid flex]
test) [Constraint' rigid flex]
cons
  where
    -- Test whether a constraint is compatible with the hypotheses:
    -- Succeeds, if constraint is implied by hypotheses,
    -- fails otherwise.
    test :: Constraint' rigid flex -> Either Error [Constraint' rigid flex]
test Constraint' rigid flex
c = do
      let Edge Node rigid flex
n1 Node rigid flex
n2 Label
l = forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint Constraint' rigid flex
c
          l' :: Label
l' = 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
      -- l' <- lookupEdge hg n1 n2
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Label
l' forall a. Ord a => a -> a -> Bool
<= Label
l) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
        Error
"size constraint" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty Constraint' rigid flex
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+>
        Error
"not consistent with size hypotheses"
      forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' rigid flex
c]
      -- if (l' <= l) then Just [c] else Nothing

-- Build constraint graph, complete it, check for negative loops.
-- Check that hypotheses graph implies constraint graphs (rigids).

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 Error (HypGraph r f)
constraintGraph [Constraint' r f]
cons0 Graph (Node r f) Label
hg = do
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"original constraints cons0 = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons0
  -- Simplify constraints, ensure they are locally consistent with
  -- hypotheses.
  [Constraint' r f]
cons <- forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either Error [Constraint' rigid flex]
simplifyWithHypotheses Graph (Node r f) Label
hg [Constraint' r f]
cons0
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"simplified constraints cons = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons
  -- Build a transitive graph from constraints.
  let g :: Graph (Node r f) Label
g = forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos forall a b. (a -> b) -> a -> b
$ forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cons
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"transitive graph g = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall n e. Graph n e -> [Edge n e]
graphToList Graph (Node r f) Label
g)
  -- Ensure it has no negative loops.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Negative a => a -> Bool
negative Graph (Node r f) Label
g) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
    Error
"size constraint graph has negative loops"
  -- Ensure it does not constrain the hypotheses.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Graph (Node r f) Label
hg 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 (Node r f) Label
g) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
    Error
"size constraint graph constrains size hypotheses"
  forall (m :: * -> *) a. Monad m => a -> m a
return Graph (Node r f) Label
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 Error ([f], ConGraphs r f)
constraintGraphs [Constraint' r f]
cons0 ConGraph r f
hg = do
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"original constraints cons0 = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons0
  -- Simplify constraints, ensure they are locally consistent with
  -- hypotheses.
  [Constraint' r f]
cons <- forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either Error [Constraint' rigid flex]
simplifyWithHypotheses ConGraph r f
hg [Constraint' r f]
cons0
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"simplified constraints cons = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons
  -- Build a transitive graph forest from constraints.
  let gs0 :: [ConGraph r f]
gs0 = forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graphs rigid flex Label
graphsFromConstraints [Constraint' r f]
cons
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"constraint forest gs0 = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall a b. (a -> b) -> [a] -> [b]
map forall n e. Graph n e -> [Edge n e]
graphToList [ConGraph r f]
gs0)
  let gs1 :: [ConGraph r f]
gs1 = forall a b. (a -> b) -> [a] -> [b]
map forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos [ConGraph r f]
gs0
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"transitive forest gs1 = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall a b. (a -> b) -> [a] -> [b]
map forall n e. Graph n e -> [Edge n e]
graphToList [ConGraph r f]
gs1)
  -- Check for flexibles to be set to infinity
  let ([[f]]
xss,[ConGraph r f]
gs) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall r f. (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs [ConGraph r f]
gs1
      xs :: [f]
xs       = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[f]]
xss
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [f]
xs) forall a b. (a -> b) -> a -> b
$ do
    forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"flexibles to set to oo = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [f]
xs
    forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"forest after oo-subst  = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall a b. (a -> b) -> [a] -> [b]
map forall n e. Graph n e -> [Edge n e]
graphToList [ConGraph r f]
gs)
  -- Ensure none has negative loops.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Negative a => a -> Bool
negative [ConGraph r f]
gs) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Error
"size constraint graph has negative loop"
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"we are free of negative loops"
  -- Ensure it does not constrain the hypotheses.
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ConGraph r f]
gs forall a b. (a -> b) -> a -> b
$ \ ConGraph r f
g -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConGraph r f
hg 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) forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
    Error
"size constraint graph constrains size hypotheses"
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"any constraint between rigids is implied by the hypotheses"
  forall (m :: * -> *) a. Monad m => a -> m a
return ([f]
xs, [ConGraph r f]
gs)

-- | If we have an edge @X + n <= X@ (with n >= 0), we must set @X = oo@.
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, forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
infFlexs ConGraph r f
g)
  where
    -- get the flexibles that need to be set to infinity
    infFlexs :: [f]
infFlexs = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {e} {rigid} {b}.
Negative e =>
Edge (Node rigid b) e -> Maybe b
flexNeg forall a b. (a -> b) -> a -> b
$ 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
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. Negative a => a -> Bool
negative Edge (Node rigid b) e
e
      forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode (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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [f]
xs = 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) = forall n e. n -> n -> e -> Edge n e
Edge (forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs Node r f
n1) (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 = forall n e. Ord n => [Edge n e] -> Graph n e
graphFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter forall {rigid} {flex}. Edge (Node rigid flex) Label -> Bool
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Graph n e -> [Edge n e]
graphToList
    where
      -- filter out edges @oo + k <= oo@
      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


-- * Compute solution from constraint graph.

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 forall a b. (a -> b) -> a -> b
$ 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   = forall rigid flex. SizeExpr' rigid flex
Infty
  plus SizeExpr' r f
e (Offset Offset
x) = 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 = forall a b c. Plus a b c => a -> b -> c
plus SizeExpr' r f
e (Label -> Weight
toWeight Label
l)

-- | Lower or upper bound for a flexible variable
type Bound r f = Map f (Set (SizeExpr' r f))

emptyBound :: Bound r f
emptyBound :: forall r f. Bound r f
emptyBound = 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
    -- ^ These metas are < ∞.
  }

-- | Compute a lower bound for a flexible from an edge.
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) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (Edge Node r f
NodeZero (NodeFlex f
x) (Label Cmp
Le Offset
o)) | Offset
o forall a. Ord a => a -> a -> Bool
>= Offset
0 -> forall a. a -> Maybe a
Just (f
x, 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 forall a. Ord a => a -> a -> Bool
>= Offset
1 -> forall a. a -> Maybe a
Just (f
x, forall rigid flex. Offset -> SizeExpr' rigid flex
Const Offset
0)
    (Edge Node r f
n1 (NodeFlex f
x) Label
l) -> forall a. a -> Maybe a
Just (f
x, forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n1 forall a b c. Plus a b c => a -> b -> c
`plus` (- (Label -> Weight
toWeight Label
l)))
    LabelledEdge r f
_ -> forall a. Maybe a
Nothing

-- | Compute an upper bound for a flexible from an edge.
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) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (Edge Node r f
n1           Node r f
NodeInfty (Label Cmp
Le Offset
_)) -> forall a. Maybe a
Nothing
    (Edge (NodeFlex f
x) Node r f
NodeInfty (Label Cmp
Lt Offset
_)) -> forall a. a -> Maybe a
Just (f
x, Cmp
Lt, forall rigid flex. SizeExpr' rigid flex
Infty)
    (Edge (NodeFlex f
x) Node r f
n2        Label
l           ) -> forall a. a -> Maybe a
Just (f
x, Cmp
Le, forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n2 forall a b c. Plus a b c => a -> b -> c
`plus` (Label -> Weight
toWeight Label
l))
    LabelledEdge r f
_ -> forall a. Maybe a
Nothing

-- | Compute the lower bounds for all flexibles in a graph.
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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall r f. Bound r f
emptyBound forall a b. (a -> b) -> a -> b
$ \ Bound r f
bs LabelledEdge r f
e ->
  case 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  -- ignore flexible bounds
    Just (f
x, SizeExpr' r f
a)      -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.union f
x (forall a. a -> Set a
Set.singleton SizeExpr' r f
a) Bound r f
bs

-- | Compute the upper bounds for all flexibles in a graph.
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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall r f. Bound r f
emptyBound, forall a. Set a
Set.empty) forall a b. (a -> b) -> a -> b
$ \ (Bound r f
bs, Set f
fs) LabelledEdge r f
e ->
  case 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)  -- ignore flexible bounds
    Just (f
x, Cmp
Lt, SizeExpr' r f
Infty) -> (Bound r f
bs, 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)     -> (forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.union f
x (forall a. a -> Set a
Set.singleton SizeExpr' r f
a) Bound r f
bs, Set f
fs)
    Maybe (f, Cmp, SizeExpr' r f)
_                   -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Compute the bounds for all flexibles in a graph.
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 = 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     = forall n e. Graph n e -> [Edge n e]
graphToList ConGraph r f
g
        lbs :: Bound r f
lbs       = 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) = forall r f.
(Ord r, Ord f) =>
[LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds [Edge (Node r f) Label]
edges


-- | Compute the relative minima in a set of nodes (those that do not have
--   a predecessor in the set).
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
  | forall rigid flex. Node rigid flex
NodeZero forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node r f]
ns = [forall rigid flex. Node rigid flex
NodeZero]
  | Bool
otherwise          = 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 = forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node r f -> Maybe ()
strictEdge [Node r f]
ns where
        -- is there an edge n -l-> n' with l <= 0
        strictEdge :: Node r f -> Maybe ()
strictEdge Node r f
n' = do
          forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Node r f
n forall a. Eq a => a -> a -> Bool
/= Node r f
n')  -- exclude loops
          Label
l <- 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
          forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Label -> Weight
toWeight Label
l forall a. Ord a => a -> a -> Bool
<= Weight
0)
          forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Compute the relative maxima in a set of nodes (those that do not have
--   a successor in the set).
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
  | forall rigid flex. Node rigid flex
NodeInfty forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node r f]
ns = [forall rigid flex. Node rigid flex
NodeInfty]
  | Bool
otherwise          = 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 = forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node r f -> Maybe ()
strictEdge [Node r f]
ns where
        -- is there an edge n -l-> n' with l <= 0
        strictEdge :: Node r f -> Maybe ()
strictEdge Node r f
n' = do
          forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Node r f
n forall a. Eq a => a -> a -> Bool
/= Node r f
n')  -- exclude loops
          Label
l <- 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'
          forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Label -> Weight
toWeight Label
l forall a. Ord a => a -> a -> Bool
<= Weight
0)
          forall (m :: * -> *) a. Monad m => a -> m a
return ()

{-|  Given source nodes n1,n2,... find all target nodes m1,m2, such
     that for all j, there are edges  n_i --l_ij--> m_j  for all i.
     Return these edges as a map from target notes to a list of edges.
     We assume the graph is reflexive-transitive.
 -}
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 = forall {k} {a}. Ord k => [Map k [a]] -> Map k [a]
intersectAll forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall {e}.
[Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
buildmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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            = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\ Edge (Node r f) e
e -> (forall n e. Edge n e -> n
dest Edge (Node r f) e
e, [Edge (Node r f) e
e]))
     -- __IMPOSSIBLE__ because it is not a multi-graph; there is at most one egde per (src,dest)
   intersectAll :: [Map k [a]] -> Map k [a]
intersectAll []     = forall k a. Map k a
Map.empty
   intersectAll (Map k [a]
m:[Map k [a]]
ms) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith forall a. [a] -> [a] -> [a]
(++)) Map k [a]
m [Map k [a]]
ms

{-|  Given target nodes m1,m2,... find all source nodes n1,n2, such
     that for all j, there are edges  n_i --l_ij--> m_j  for all i.
     Return these edges as a map from target notes to a list of edges.
     We assume the graph is reflexive-transitive.
 -}
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 = forall {k} {a}. Ord k => [Map k [a]] -> Map k [a]
intersectAll forall a b. (a -> b) -> a -> b
$  forall a b. (a -> b) -> [a] -> [b]
map (forall {e}.
[Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
buildmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\ Edge (Node r f) e
e -> (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 []     = forall k a. Map k a
Map.empty
   intersectAll (Map k [a]
m:[Map k [a]]
ms) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith forall a. [a] -> [a] -> [a]
(++)) Map k [a]
m [Map k [a]]
ms

-- | Compute the sup of two different rigids or a rigid and a constant.
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     = 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 = forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
smallest HypGraph r f
hg forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
Map.keys Map (Node r f) [Edge' r f Label]
sucs
  forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"lub': sucs = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map (Node r f) [Edge' r f Label]
sucs) -- FIXME: prettyShow
  case [Node r f]
sucNodes of
    -- there is a unique smallest common successor n0 of node1 and node2
    [Node r f
n0] -> do
      -- then there are exactly two edges node1 --l1--> n0 and node2 --l2--> n0
      -- Andreas, 2017-04-28, issue #2558: The following invariant does not hold always
      -- -- with non-positive weights l1, l2
      let es :: [Edge' r f Label]
es = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 forall a. Eq a => a -> a -> Bool
== Node r f
n1)         forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 forall a. Eq a => a -> a -> Bool
== Node r f
n2)         forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node1 forall a. Eq a => a -> a -> Bool
== Node r f
node1x)  forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node2 forall a. Eq a => a -> a -> Bool
== Node r f
node2x)  forall a. HasCallStack => a
__IMPOSSIBLE__
          -- Andreas, 2017-04-28, issue #2558: The following invariant does not hold always
          -- unless (toWeight l1 <= 0) __IMPOSSIBLE__
          -- unless (toWeight l2 <= 0) __IMPOSSIBLE__
          let o :: Weight
              o :: Weight
o = forall a. Ord a => a -> a -> a
max (Offset
n forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l1) (Offset
m forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l2)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n0 forall a b c. Plus a b c => a -> b -> c
`plus` Weight
o
        [Edge' r f Label]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    -- otherwise, we cannot compute the sup
    [Node r f]
_ -> do
      let SizeExpr' r f
a1 :: SizeExpr' r f = forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node1 forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n
      let SizeExpr' r f
a2 :: SizeExpr' r f = forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node2 forall a b c. Plus a b c => a -> b -> c
`plus` Offset
m
      forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"cannot compute lub of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a1 forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a2 forall a. [a] -> [a] -> [a]
++ String
" because sucNodes = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Node r f]
sucNodes)
      forall a. Maybe a
Nothing

-- | Compute the inf of two different rigids or a rigid and a constant.
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     = 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 = forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
largest HypGraph r f
hg forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
Map.keys Map (Node r f) [Edge' r f Label]
preds
  forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"glb': preds = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map (Node r f) [Edge' r f Label]
preds) -- FIXME: prettyShow
  case [Node r f]
predNodes of
    -- there is a unique greatest common predecessor n0 of node1 and node2
    [Node r f
n0] -> do
      -- then there are exactly two edges n0 --l1--> node1 and n0 --l2--> node2
      -- Andreas, 2017-04-28, issue #2558: The following invariant may not hold always
      -- -- with non-positive weigths l1, l2
      let es :: [Edge' r f Label]
es = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 forall a. Eq a => a -> a -> Bool
== Node r f
n1)         forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 forall a. Eq a => a -> a -> Bool
== Node r f
n2)         forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node1 forall a. Eq a => a -> a -> Bool
== Node r f
node1x)  forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node2 forall a. Eq a => a -> a -> Bool
== Node r f
node2x)  forall a. HasCallStack => a
__IMPOSSIBLE__
          -- Andreas, 2017-04-28, issue #2558: The following invariant may not hold always
          -- unless (toWeight l1 <= 0) __IMPOSSIBLE__
          -- unless (toWeight l2 <= 0) __IMPOSSIBLE__
          let o :: Weight
              o :: Weight
o = forall a. Ord a => a -> a -> a
max (Offset
n forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l1) (Offset
m forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l2)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n0 forall a b c. Plus a b c => a -> b -> c
`plus` Weight
o
        [Edge' r f Label]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    -- otherwise, we cannot compute the sup
    [Node r f]
_ -> do
      let SizeExpr' r f
a1 :: SizeExpr' r f = forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node1 forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n
      let SizeExpr' r f
a2 :: SizeExpr' r f = forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node2 forall a b c. Plus a b c => a -> b -> c
`plus` Offset
m
      forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"cannot compute glb of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a1 forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a2 forall a. [a] -> [a] -> [a]
++ String
" because predNodes = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Node r f]
predNodes)
      forall a. Maybe a
Nothing

-- | Compute the least upper bound (sup).
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
_)   -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (SizeExpr' r f
_, Flex{})   -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (SizeExpr' r f
Infty, SizeExpr' r f
a2)   -> forall a. a -> Maybe a
Just forall rigid flex. SizeExpr' rigid flex
Infty
    (SizeExpr' r f
a1, SizeExpr' r f
Infty)   -> forall a. a -> Maybe a
Just forall rigid flex. SizeExpr' rigid flex
Infty
    (Const Offset
n  , Const Offset
m  )
                  -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall rigid flex. Offset -> SizeExpr' rigid flex
Const forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
max Offset
n Offset
m
    (Const Offset
n  , Rigid r
j Offset
m)
      | Offset
m forall a. Ord a => a -> a -> Bool
>= Offset
n    -> forall a. a -> Maybe a
Just SizeExpr' r f
a2
      | Bool
otherwise -> 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 (forall rigid flex. Node rigid flex
NodeZero, Offset
n) (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)
    (Rigid r
i Offset
n, Const Offset
m  )
      | Offset
n forall a. Ord a => a -> a -> Bool
>= Offset
m    -> forall a. a -> Maybe a
Just SizeExpr' r f
a1
      | Bool
otherwise -> 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 (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (forall rigid flex. Node rigid flex
NodeZero, Offset
m)
    (Rigid r
i Offset
n, Rigid r
j Offset
m)
      | r
i forall a. Eq a => a -> a -> Bool
== r
j    -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
max Offset
n Offset
m
      | Bool
otherwise -> 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 (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)

{- Finding the glb of two rigid size expressions in hypotheses graph

  a1 = Rigid i n
  a2 = Rigid j m

  Find the topological predecessors of (NodeRigid i)
  Find the topological predecessors of (NodeRigid j)

-}

-- | Compute the greatest lower bound (inf) of size expressions relative
--   to a hypotheses graph.
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
_) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (SizeExpr' r f
_, Flex{}) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (SizeExpr' r f
Infty, SizeExpr' r f
a2) -> forall a. a -> Maybe a
Just SizeExpr' r f
a2
    (SizeExpr' r f
a1, SizeExpr' r f
Infty) -> forall a. a -> Maybe a
Just SizeExpr' r f
a1
    (Const Offset
n  , Const Offset
m  )          -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall rigid flex. Offset -> SizeExpr' rigid flex
Const forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
min Offset
n Offset
m
    (Const Offset
n  , Rigid r
i Offset
m)
      | Offset
n forall a. Ord a => a -> a -> Bool
<= Offset
m    -> forall a. a -> Maybe a
Just SizeExpr' r f
a1
      | Bool
otherwise -> 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 (forall rigid flex. Node rigid flex
NodeZero, Offset
n) (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
m)
    (Rigid r
i Offset
n, Const Offset
m  )
      | Offset
m forall a. Ord a => a -> a -> Bool
<= Offset
n    -> forall a. a -> Maybe a
Just SizeExpr' r f
a2
      | Bool
otherwise -> 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 (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (forall rigid flex. Node rigid flex
NodeZero, Offset
m)
    (Rigid r
i Offset
n, Rigid r
j Offset
m)
      | r
i forall a. Eq a => a -> a -> Bool
== r
j    -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
min Offset
n Offset
m
      | Bool
otherwise -> 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 (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)
{-
    (Rigid i n, Rigid j m) -> do
      let iLeqj = Map.lookup (Edge (NodeRigid i) (NodeRigid j) ()) hg
          jLeqi = Map.lookup (Edge (NodeRigid j) (NodeRigid i) ()) hg
      case (iLeqj, jLeqi) of
        (Nothing, Nothing) -> Nothing -- maximum as size expression
        (Just l, Nothing) | Offset k <- toWeight l ->
          if k + n <= m then Just a1
          else Nothing -- no guaranteed infimum
        (Nothing, Just l) | Offset k <- toWeight l ->
          if k + m <= n then Just a2
          else Nothing
        (Just{}, Just{}) -> Nothing
{-
      let lbi = incoming hg (NodeRigid i)
          lbj = incoming hg (NodeRigid j)
          srci = Set.fromList $ map src lbi
          srcj = Set.fromList $ map src lbj
          srcs =  Set.intersection srci srcj
-}
    _ -> trace ("cannot compute glb of " ++ prettyShow a1 ++ " and " ++ prettyShow a2) $
      Nothing -- TODO!
-}

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 forall a. Ord a => a -> a -> Bool
< Offset
0 = do
  let v :: Node r f
v     = forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i
      preds :: [Edge' r f Label]
preds = 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' forall a. Eq a => a -> a -> Bool
== Node r f
v   =
          case Label -> Weight
toWeight Label
l of
            Weight
Infinity -> forall a. Maybe a
Nothing
            Offset Offset
o -> if Offset
o forall a. Ord a => a -> a -> Bool
<= Offset
m then forall a. a -> Maybe a
Just (Node r f
n, Offset
o) else forall a. Maybe a
Nothing
        | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
            -- error $ "findRigidBelow: impossible: " ++ prettyShow e
      cands :: [(Node r f, Offset)]
cands = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Edge' r f Label -> Maybe (Node r f, Offset)
filt [Edge' r f Label]
preds
  (Node r f
n, Offset
o) <- do
    case [(Node r f, Offset)]
cands of
      []  -> forall a. Maybe a
Nothing
      [(Node r f, Offset)
c] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Node r f, Offset)
c
      [(Node r f, Offset)]
_   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
               forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
List.maximumBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$
                 forall a. (a -> Bool) -> [a] -> [a]
filter ((forall rigid flex. Node rigid flex
NodeZero forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Node r f, Offset)]
cands
  let offset :: Offset
offset = Offset
m forall a. Num a => a -> a -> a
- Offset
o
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Offset
offset forall a. Ord a => a -> a -> Bool
>= Offset
0) forall a. HasCallStack => a
__IMPOSSIBLE__
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n forall a b c. Plus a b c => a -> b -> c
`plus` Offset
offset
findRigidBelow HypGraph r f
hg SizeExpr' r f
e = forall a. HasCallStack => a
__IMPOSSIBLE__
  -- error $ "findRigidBelow: impossible: " ++ prettyShow e


solveGraph
  :: (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 Error (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) = forall r f. (Ord r, Ord f) => ConGraph r f -> Bounds r f
bounds HypGraph r f
g
      -- flexibles to solve for
      xs :: [f]
xs = forall a. Set a -> [a]
Set.toAscList forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ forall k a. Map k a -> Set k
Map.keysSet Bound r f
lbs, forall k a. Map k a -> Set k
Map.keysSet Bound r f
ubs, Set f
fs ]
  -- iterate over all flexible variables
  [(f, SizeExpr' r f)]
xas <- forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [f]
xs forall a b. (a -> b) -> a -> b
$ \ f
x -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      -- get lower and upper bounds for flexible x
      let lx :: [SizeExpr' r f]
lx = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. Set a
Set.empty f
x Bound r f
lbs
          ux :: [SizeExpr' r f]
ux = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. Set a
Set.empty f
x Bound r f
ubs
      forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"lower bounds for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow f
x forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
lx)
      forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"upper bounds for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow f
x forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
ux)
      -- compute maximum of lower bounds
      Maybe (SizeExpr' r f)
lb <- do
        case [SizeExpr' r f]
lx of
          []     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
          (SizeExpr' r f
a:[SizeExpr' r f]
as) -> do
            case forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (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  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. TruncateOffset a => a -> a
truncateOffset SizeExpr' r f
l
              Maybe (SizeExpr' r f)
Nothing -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
                Error
"inconsistent lower bound for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM f
x
      -- compute minimum of upper bounds
      Maybe (SizeExpr' r f)
ub <- do
        case [SizeExpr' r f]
ux of
          []     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
          (SizeExpr' r f
a:[SizeExpr' r f]
as) -> do
            case forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (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 | forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' r f
l                  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SizeExpr' r f
l
                     | Just SizeExpr' r f
l' <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SizeExpr' r f
l'
              Maybe (SizeExpr' r f)
_ -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
                Error
"inconsistent upper bound for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM f
x
      case (Maybe (SizeExpr' r f)
lb, Maybe (SizeExpr' r f)
ub) of
        (Just SizeExpr' r f
l, Maybe (SizeExpr' r f)
Nothing) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SizeExpr' r f
l  -- solve x = lower bound
        (Maybe (SizeExpr' r f)
Nothing, Just SizeExpr' r f
u) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SizeExpr' r f
u  -- solve x = upper bound
        (Just SizeExpr' r f
l,  Just SizeExpr' r f
u) -> do
          forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"lower bound for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow f
x forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
l)
          forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"upper bound for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow f
x forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
u)
          case forall flex. Ord flex => Polarities flex -> flex -> Polarity
getPolarity Polarities f
pols f
x of
            Polarity
Least    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SizeExpr' r f
l
            Polarity
Greatest -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SizeExpr' r f
u
        (Maybe (SizeExpr' r f), Maybe (SizeExpr' r f))
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution forall a b. (a -> b) -> a -> b
$ forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(f, SizeExpr' r f)]
xas

-- | Solve a forest of constraint graphs relative to a hypotheses graph.
--   Concatenate individual solutions.
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 Error (Solution r f)
solveGraphs Polarities f
pols HypGraph r f
hg ConGraphs r f
gs =
  forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> 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 Error (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg) ConGraphs r f
gs

-- * Verify solution

-- | Check that after substitution of the solution,
--   constraints are implied by hypotheses.
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 Error ()
verifySolution HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol = do
  [Constraint' r f]
cs <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol [Constraint' r f]
cs
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"substituted constraints " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cs
  [Constraint' r f]
cs <- -- maybe (Left "solution produces inconsistency") Right $
          forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 forall a b. (a -> b) -> a -> b
$ \ Constraint' r f
c -> forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c]) [Constraint' r f]
cs
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"simplified substituted constraints " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cs
  -- cs <- maybe (Left "solution produces inconsistency") Right $
  --         simplifyWithHypotheses hg cs
  let g :: HypGraph r f
g = forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HypGraph r f
hg forall r f a.
(Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
 Negative a) =>
Graph r f a -> Graph r f a -> Bool
`implies` HypGraph r f
g) forall a b. (a -> b) -> a -> b
$
    forall a b. a -> Either a b
Left Error
"solution not implied by hypotheses"
{-
  case simplifyWithHypotheses hg $ subst sol cs of
    Nothing -> Left "solution produces inconsistency"
    Just [] -> Right ()
    Just cs -> Left $ "solution leaves constraints " ++ prettyShow cs
-}

-- | Iterate solver until no more metas can be solved.
--
--   This might trigger a (wanted) error on the second iteration (see Issue 2096)
--   which would otherwise go unnoticed.

iterateSolver
  :: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
  => Polarities f
     -- ^ Meta variable polarities (prefer lower or upper solution?).
  -> HypGraph r f
     -- ^ Hypotheses (assumed to have no metas, so, fixed during iteration).
  -> [Constraint' r f]
     -- ^ Constraints to solve.
  -> Solution r f
     -- ^ Previous substitution (already applied to constraints).
  -> Either Error (Solution r f)
     -- ^ Accumulated substition.

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 Error (Solution r f)
iterateSolver Polarities f
pols HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol0 = do
  HypGraph r f
g <- forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f] -> HypGraph r f -> Either Error (HypGraph r f)
constraintGraph [Constraint' r f]
cs HypGraph r f
hg
  Solution r f
sol <- 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 Error (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg HypGraph r f
g
  forall (f :: * -> *). Applicative f => String -> f ()
traceM forall a b. (a -> b) -> a -> b
$ String
"(partial) solution " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Solution r f
sol
  if forall a. Null a => a -> Bool
null Solution r f
sol then forall (m :: * -> *) a. Monad m => a -> m a
return Solution r f
sol0 else
    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 Error (Solution r f)
iterateSolver Polarities f
pols HypGraph r f
hg (forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol [Constraint' r f]
cs) forall a b. (a -> b) -> a -> b
$ forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution forall a b. (a -> b) -> a -> b
$
      forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. HasCallStack => a
__IMPOSSIBLE__ (forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution Solution r f
sol) forall a b. (a -> b) -> a -> b
$
        forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution forall a b. (a -> b) -> a -> b
$ forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol Solution r f
sol0

-- * Tests

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 = 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 (Node String f) Label
hg [forall {flex}. Node String flex
n1,forall {flex}. Node String flex
n2]
  where
    n1 :: Node String flex
n1 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"i"
    n2 :: Node String flex
n2 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"j"
    n3 :: Node String flex
n3 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"k"
    n4 :: Node String flex
n4 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"l"
    n5 :: Node String flex
n5 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"m"
    hg :: Graph (Node String f) Label
hg = forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
         [ forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n1 forall {flex}. Node String flex
n3 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
1
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n1 forall {flex}. Node String flex
n4 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
2
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n1 forall {flex}. Node String flex
n5 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
3
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n2 forall {flex}. Node String flex
n3 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
4
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n2 forall {flex}. Node String flex
n4 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
5
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n2 forall {flex}. Node String flex
n5 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
6
         ]

-- testLub = smallest hg $ Map.keys $ commonSuccs hg [n1,n2] --
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 = 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 Graph (Node String f) Label
hg (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid String
"i" Offset
0) (forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid String
"j" Offset
2)
  where
    n1 :: Node String flex
n1 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"i"
    n2 :: Node String flex
n2 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"j"
    n3 :: Node String flex
n3 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"k"
    n4 :: Node String flex
n4 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"l"
    n5 :: Node String flex
n5 = forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"m"
    hg :: Graph (Node String f) Label
hg = forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
         [ forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n1 forall {flex}. Node String flex
n3 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
0
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n1 forall {flex}. Node String flex
n4 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
2
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n1 forall {flex}. Node String flex
n5 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
4
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n2 forall {flex}. Node String flex
n3 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
1
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n2 forall {flex}. Node String flex
n4 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
3
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n2 forall {flex}. Node String flex
n5 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
5
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n3 forall {flex}. Node String flex
n4 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
0
         , forall n e. n -> n -> e -> Edge n e
Graph.Edge forall {flex}. Node String flex
n3 forall {flex}. Node String flex
n5 forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Lt Offset
0
         ]