{-# LANGUAGE NoMonomorphismRestriction #-}

module Agda.TypeChecking.SizedTypes.WarshallSolver where

import Prelude hiding ( null, truncate )


import Control.Monad

import Data.Function (on)
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map

import Agda.TypeChecking.SizedTypes.Syntax
import Agda.TypeChecking.SizedTypes.Utils

import Agda.Utils.Graph.AdjacencyMap.Unidirectional
  (Edge(..), Nodes(..), nodes, computeNodes)
-- (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 :: Edge n e -> n
src = Edge n e -> n
forall n e. Edge n e -> n
Graph.source

dest :: Edge n e -> n
dest :: Edge n e -> n
dest = Edge n e -> n
forall n e. Edge n e -> n
Graph.target

lookupEdge :: Ord n => Graph.Graph n e -> n -> n -> Maybe e
lookupEdge :: Graph n e -> n -> n -> Maybe e
lookupEdge g :: Graph n e
g s :: n
s t :: n
t = n -> n -> Graph n e -> Maybe e
forall n e. Ord n => n -> n -> Graph n e -> Maybe e
Graph.lookup n
s n
t Graph n e
g

graphToList :: Graph.Graph n e -> [Edge n e]
graphToList :: Graph n e -> [Edge n e]
graphToList = Graph n e -> [Edge n e]
forall n e. Graph n e -> [Edge n e]
Graph.edges

graphFromList :: Ord n => [Edge n e] -> Graph.Graph n e
graphFromList :: [Edge n e] -> Graph n e
graphFromList = [Edge n e] -> Graph n e
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges

insertEdge :: (Ord n, MeetSemiLattice e, Top e) =>
              Edge n e -> Graph.Graph n e -> Graph.Graph n e
insertEdge :: Edge n e -> Graph n e -> Graph n e
insertEdge e :: Edge n e
e g :: Graph n e
g
  | e -> Bool
forall a. Top a => a -> Bool
isTop (Edge n e -> e
forall n e. Edge n e -> e
label Edge n e
e) = Graph n e
g
  | Bool
otherwise       = (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
forall n e.
Ord n =>
(e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
Graph.insertEdgeWith e -> e -> e
forall a. MeetSemiLattice a => a -> a -> a
meet Edge n e
e Graph n e
g

-- | 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 :: Graph r f a -> Node r f -> [Edge' r f a]
outgoing g :: Graph r f a
g s :: Node r f
s = Graph r f a -> [Node r f] -> [Edge' r f a]
forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesFrom Graph r f a
g [Node r f
s]

-- | 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 :: Graph r f a -> Node r f -> [Edge' r f a]
incoming g :: Graph r f a
g t :: Node r f
t = Graph r f a -> [Node r f] -> [Edge' r f a]
forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesTo Graph r f a
g [Node r f
t]

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

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

-- * Edge weights

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

instance Pretty Weight where
  pretty :: Weight -> Doc
pretty (Offset x :: Offset
x) = Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
x
  pretty Infinity   = "∞"

instance Ord Weight where
  x :: Weight
x        <= :: Weight -> Weight -> Bool
<= Infinity = Bool
True
  Infinity <= y :: Weight
y        = Bool
False
  Offset x :: Offset
x <= Offset y :: Offset
y = Offset
x Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
y

instance MeetSemiLattice Weight where
  meet :: Weight -> Weight -> Weight
meet = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
min

instance Top Weight where
  top :: Weight
top  = Weight
Infinity

instance Enum Weight where
  succ :: Weight -> Weight
succ (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Offset
forall a. Enum a => a -> a
succ Offset
x)
  succ (Weight
Infinity) = Weight
Infinity
  pred :: Weight -> Weight
pred (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Offset
forall a. Enum a => a -> a
pred Offset
x)
  pred (Weight
Infinity) = Weight
Infinity
  toEnum :: Int -> Weight
toEnum = Offset -> Weight
Offset (Offset -> Weight) -> (Int -> Offset) -> Int -> Weight
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Offset
forall a. Enum a => Int -> a
toEnum
  fromEnum :: Weight -> Int
fromEnum (Offset x :: Offset
x) = Offset -> Int
forall a. Enum a => a -> Int
fromEnum Offset
x
  fromEnum (Weight
Infinity) = Int
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Partial implementation of @Num@.
instance Num Weight where
  Infinity + :: Weight -> Weight -> Weight
+ y :: Weight
y        = Weight
Infinity
  x :: Weight
x + Infinity        = Weight
Infinity
  Offset x :: Offset
x + Offset y :: Offset
y = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset
x Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
y
  Infinity - :: Weight -> Weight -> Weight
- Offset y :: Offset
y = Weight
Infinity
  Offset x :: Offset
x - Offset y :: Offset
y = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset
x Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
y
  x :: Weight
x        - Infinity = Weight
forall a. HasCallStack => a
__IMPOSSIBLE__
  abs :: Weight -> Weight
abs (Offset x :: Offset
x)      = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Num a => a -> a
abs Offset
x
  abs Infinity        = Weight
Infinity
  signum :: Weight -> Weight
signum (Offset x :: Offset
x)   = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Num a => a -> a
signum Offset
x
  signum Infinity     = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ 1
  fromInteger :: Integer -> Weight
fromInteger x :: Integer
x       = Offset -> Weight
Offset (Integer -> Offset
forall a. Num a => Integer -> a
fromInteger Integer
x)
  x :: Weight
x * :: Weight -> Weight -> Weight
* y :: Weight
y = Weight
forall a. HasCallStack => a
__IMPOSSIBLE__

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

-- | 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 = (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0)

instance Negative Offset where
  negative :: Offset -> Bool
negative (O x :: Int
x) = Int -> Bool
forall a. Negative a => a -> Bool
negative Int
x

instance Negative Weight where
  negative :: Weight -> Bool
negative Infinity = Bool
False
  negative (Offset x :: Offset
x) = Offset -> Bool
forall a. Negative a => a -> Bool
negative Offset
x

-- * 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
(Int -> Label -> ShowS)
-> (Label -> String) -> ([Label] -> ShowS) -> Show Label
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Label] -> ShowS
$cshowList :: [Label] -> ShowS
show :: Label -> String
$cshow :: Label -> String
showsPrec :: Int -> Label -> ShowS
$cshowsPrec :: Int -> Label -> ShowS
Show)


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

instance Negative Label where
  negative :: Label -> Bool
negative = Weight -> Bool
forall a. Negative a => a -> Bool
negative (Weight -> Bool) -> (Label -> Weight) -> Label -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> Weight
toWeight

instance Eq Label where
  Label cmp :: Cmp
cmp w :: Offset
w == :: Label -> Label -> Bool
== Label cmp' :: Cmp
cmp' w' :: Offset
w' = Cmp
cmp Cmp -> Cmp -> Bool
forall a. Eq a => a -> a -> Bool
== Cmp
cmp' Bool -> Bool -> Bool
&& Offset
w Offset -> Offset -> Bool
forall a. Eq a => a -> a -> Bool
== Offset
w'
  LInf        == LInf          = Bool
True
  _           == _             = Bool
False

instance Ord Label where
  Label Lt  w :: Offset
w <= :: Label -> Label -> Bool
<= Label Lt w' :: Offset
w' = Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
  Label Le  w :: Offset
w <= Label Le w' :: Offset
w' = Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
  Label Lt  w :: Offset
w <= Label Le w' :: Offset
w' = Offset -> Offset
forall a. Enum a => a -> a
pred Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
  Label Le  w :: Offset
w <= Label Lt w' :: Offset
w' = Offset -> Offset
forall a. Enum a => a -> a
succ Offset
w Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
w'
  _           <= LInf        = Bool
True
  LInf{}      <= Label{}     = Bool
False

instance Pretty Label where
  pretty :: Label -> Doc
pretty (Label cmp :: Cmp
cmp w :: Offset
w) = Cmp -> Doc
forall a. Pretty a => a -> Doc
pretty Cmp
cmp Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
w
  pretty LInf          = "∞"

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

instance Top Label where
  top :: Label
top                 = Label
LInf
  isTop :: Label -> Bool
isTop Label{}       = Bool
False
  isTop LInf          = Bool
True

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

instance Dioid Weight where
  compose :: Weight -> Weight -> Weight
compose     = Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
(+)
  unitCompose :: Weight
unitCompose = 0

instance Dioid Label where
  compose :: Label -> Label -> Label
compose (Label Lt w :: Offset
w) (Label Lt w' :: Offset
w')    = Cmp -> Offset -> Label
Label Cmp
Lt (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset -> Offset
forall a. Enum a => a -> a
pred (Offset -> Offset) -> Offset -> Offset
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
w'
  compose (Label cmp :: Cmp
cmp w :: Offset
w) (Label cmp' :: Cmp
cmp' w' :: Offset
w') = Cmp -> Offset -> Label
Label (Cmp -> Cmp -> Cmp
forall a. Dioid a => a -> a -> a
compose Cmp
cmp Cmp
cmp') (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
w Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
w'
  compose _             LInf            = Label
LInf
  compose LInf          _               = Label
LInf
  unitCompose :: Label
unitCompose = Cmp -> Offset -> Label
Label Cmp
Le 0

-- * Graphs

-- ** Nodes

data Node rigid flex
  = NodeZero
  | NodeInfty
  | NodeRigid rigid
  | NodeFlex  flex
  deriving (Int -> Node rigid flex -> ShowS
[Node rigid flex] -> ShowS
Node rigid flex -> String
(Int -> Node rigid flex -> ShowS)
-> (Node rigid flex -> String)
-> ([Node rigid flex] -> ShowS)
-> Show (Node rigid flex)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
showList :: [Node rigid flex] -> ShowS
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
show :: Node rigid flex -> String
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
showsPrec :: Int -> Node rigid flex -> ShowS
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
Show, Node rigid flex -> Node rigid flex -> Bool
(Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> Eq (Node rigid flex)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
/= :: Node rigid flex -> Node rigid flex -> Bool
$c/= :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
== :: Node rigid flex -> Node rigid flex -> Bool
$c== :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
Eq, Eq (Node rigid flex)
Eq (Node rigid flex) =>
(Node rigid flex -> Node rigid flex -> Ordering)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Node rigid flex)
-> (Node rigid flex -> Node rigid flex -> Node rigid flex)
-> Ord (Node rigid flex)
Node rigid flex -> Node rigid flex -> Bool
Node rigid flex -> Node rigid flex -> Ordering
Node rigid flex -> Node rigid flex -> Node rigid flex
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall rigid flex. (Ord rigid, Ord flex) => Eq (Node rigid flex)
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
min :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmin :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
max :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmax :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
>= :: Node rigid flex -> Node rigid flex -> Bool
$c>= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
> :: Node rigid flex -> Node rigid flex -> Bool
$c> :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
<= :: Node rigid flex -> Node rigid flex -> Bool
$c<= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
< :: Node rigid flex -> Node rigid flex -> Bool
$c< :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
compare :: Node rigid flex -> Node rigid flex -> Ordering
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
$cp1Ord :: forall rigid flex. (Ord rigid, Ord flex) => Eq (Node rigid flex)
Ord)

instance (Pretty rigid, Pretty flex) => Pretty (Node rigid flex) where
  pretty :: Node rigid flex -> Doc
pretty NodeZero      = "0"
  pretty NodeInfty     = "∞"
  pretty (NodeRigid x :: rigid
x) = rigid -> Doc
forall a. Pretty a => a -> Doc
pretty rigid
x
  pretty (NodeFlex  x :: flex
x) = flex -> Doc
forall a. Pretty a => a -> Doc
pretty flex
x

isFlexNode :: Node rigid flex -> Maybe flex
isFlexNode :: Node rigid flex -> Maybe flex
isFlexNode (NodeFlex x :: flex
x) = flex -> Maybe flex
forall a. a -> Maybe a
Just flex
x
isFlexNode _            = Maybe flex
forall a. Maybe a
Nothing

isZeroNode :: Node rigid flex -> Bool
isZeroNode :: Node rigid flex -> Bool
isZeroNode NodeZero{} = Bool
True
isZeroNode _          = Bool
False

isInftyNode :: Node rigid flex -> Bool
isInftyNode :: Node rigid flex -> Bool
isInftyNode NodeInfty{} = Bool
True
isInftyNode _           = Bool
False

nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr n :: Node rigid flex
n =
  case Node rigid flex
n of
    NodeZero    -> Offset -> SizeExpr' rigid flex
forall rigid flex. Offset -> SizeExpr' rigid flex
Const 0
    NodeInfty   -> SizeExpr' rigid flex
forall rigid flex. SizeExpr' rigid flex
Infty
    NodeRigid i :: rigid
i -> rigid -> Offset -> SizeExpr' rigid flex
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid rigid
i 0
    NodeFlex x :: flex
x  -> flex -> Offset -> SizeExpr' rigid flex
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex flex
x 0

-- ** 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 = a -> Bool
forall a. Negative a => a -> Bool
negative (a -> Bool) -> (Edge' r f a -> a) -> Edge' r f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge' r f a -> a
forall n e. Edge n e -> e
label

-- instance Show a => Show (Edge' a) where
--   show (Edge u v l) = show u ++ " -(" ++ show l ++ ")-> " ++ show v

instance (Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) where
  e :: Edge' r f a
e@(Edge u :: Node r f
u v :: Node r f
v l :: a
l) meet :: Edge' r f a -> Edge' r f a -> Edge' r f a
`meet` e' :: Edge' r f a
e'@(Edge u' :: Node r f
u' v' :: Node r f
v' l' :: a
l')
    | Node r f
u Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
u' Bool -> Bool -> Bool
&& Node r f
v Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
v' = Node r f -> Node r f -> a -> Edge' r f a
forall n e. n -> n -> e -> Edge n e
Edge Node r f
u Node r f
v (a -> Edge' r f a) -> a -> Edge' r f a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
`meet` a
l'
    | Bool
otherwise          = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
       -- 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 = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
  isTop :: Edge' r f a -> Bool
isTop e :: Edge' r f a
e = a -> Bool
forall a. Top a => a -> Bool
isTop (Edge' r f a -> a
forall n e. Edge n e -> e
label Edge' r f a
e)

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

-- ** Graphs

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

emptyGraphs :: Graphs r f a
emptyGraphs :: 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 :: Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions NodeZero    gs :: Graphs r f a
gs = ([], Graphs r f a
gs)
mentions NodeInfty   gs :: Graphs r f a
gs = ([], Graphs r f a
gs)
mentions NodeRigid{} gs :: Graphs r f a
gs = ([], Graphs r f a
gs)
mentions n :: Node r f
n           gs :: Graphs r f a
gs = (Graph (Node r f) a -> Bool)
-> Graphs r f a -> (Graphs r f a, Graphs r f a)
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Node r f -> Set (Node r f) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Node r f
n (Set (Node r f) -> Bool)
-> (Graph (Node r f) a -> Set (Node r f))
-> Graph (Node r f) a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph (Node r f) a -> Set (Node r f)
forall n e. Graph n e -> Set n
nodes) Graphs r f a
gs

-- | 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 :: Edge' r f a -> Graphs r f a -> Graphs r f a
addEdge e :: Edge' r f a
e@(Edge src :: Node r f
src dest :: Node r f
dest l :: a
l) gs :: Graphs r f a
gs =
  -- 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 (gsSrc :: Graphs r f a
gsSrc , gsNotSrc :: Graphs r f a
gsNotSrc)  = Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
forall r f a.
(Ord r, Ord f) =>
Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions Node r f
src  Graphs r f a
gs
      (gsDest :: Graphs r f a
gsDest, gsNotDest :: Graphs r f a
gsNotDest) = Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
forall r f a.
(Ord r, Ord f) =>
Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
mentions Node r f
dest Graphs r f a
gsNotSrc
  in Edge' r f a -> Graph (Node r f) a -> Graph (Node r f) a
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge Edge' r f a
e ((a -> a -> a) -> Graphs r f a -> Graph (Node r f) a
forall n e. Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
Graph.unionsWith a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
meet (Graphs r f a -> Graph (Node r f) a)
-> Graphs r f a -> Graph (Node r f) a
forall a b. (a -> b) -> a -> b
$ Graphs r f a
gsSrc Graphs r f a -> Graphs r f a -> Graphs r f a
forall a. [a] -> [a] -> [a]
++ Graphs r f a
gsDest) Graph (Node r f) a -> Graphs r f a -> Graphs r f a
forall a. a -> [a] -> [a]
: Graphs r f a
gsNotDest

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

-- 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 = (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Edge (Node r f) a -> Bool
forall a. Negative a => a -> Bool
negative ([Edge (Node r f) a] -> Bool)
-> (Graph r f a -> [Edge (Node r f) a]) -> Graph r f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph r f a -> [Edge (Node r f) a]
forall n e. Ord n => Graph n e -> [Edge n e]
Graph.diagonal

instance (Ord r, Ord f, Negative a) => Negative (Graphs r f a) where
  negative :: Graphs r f a -> Bool
negative = (Graph r f a -> Bool) -> Graphs r f a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Graph r f a -> Bool
forall a. Negative a => a -> Bool
negative

-- | @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 :: Graph r f a -> Graph r f a -> Bool
implies h :: Graph r f a
h g :: Graph r f a
g = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Edge (Node r f) a -> Bool
test ([Edge (Node r f) a] -> [Bool]) -> [Edge (Node r f) a] -> [Bool]
forall a b. (a -> b) -> a -> b
$ Graph r f a -> [Edge (Node r f) a]
forall n e. Graph n e -> [Edge n e]
graphToList Graph r f a
g
  -- NB: doing the @test k l@ before the recursive @b@ gives
  -- opportunity to short-cut the conjunction @&&@.
  where
    -- test :: Key -> a -> Bool
    test :: Edge (Node r f) a -> Bool
test k :: Edge (Node r f) a
k@(Edge src :: Node r f
src dest :: Node r f
dest l :: a
l)
      | Node r f -> Bool
forall rigid flex. Node rigid flex -> Bool
isZeroNode Node r f
src, Bool -> Bool
not (a -> Bool
forall a. Negative a => a -> Bool
negative a
l) = Bool
True
      | Node r f -> Bool
forall rigid flex. Node rigid flex -> Bool
isInftyNode Node r f
dest                 = Bool
True
      | Maybe f -> Bool
forall a. Maybe a -> Bool
isJust (Maybe f -> Bool) -> Maybe f -> Bool
forall a b. (a -> b) -> a -> b
$ Node r f -> Maybe f
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode Node r f
src          = Bool
True
      | Maybe f -> Bool
forall a. Maybe a -> Bool
isJust (Maybe f -> Bool) -> Maybe f -> Bool
forall a b. (a -> b) -> a -> b
$ Node r f -> Maybe f
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode Node r f
dest         = Bool
True
      | a -> Bool
forall a. Top a => a -> Bool
isTop a
l                          = Bool
True
      | Bool
otherwise = case Graph r f a -> Node r f -> Node r f -> Maybe a
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge Graph r f a
h Node r f
src Node r f
dest of
        Nothing -> Bool
False
        Just l' :: a
l' -> if a
l' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
l then Bool
True else
          String -> Bool -> Bool
forall a. String -> a -> a
trace ("edge " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Edge (Node r f) a -> String
forall a. Pretty a => a -> String
prettyShow (a
l a -> Edge (Node r f) a -> Edge (Node r f) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Edge (Node r f) a
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not implied by " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Edge (Node r f) a -> String
forall a. Pretty a => a -> String
prettyShow (a
l' a -> Edge (Node r f) a -> Edge (Node r f) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Edge (Node r f) a
k)) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
            Bool
False
-- 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 :: SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr e :: SizeExpr' rigid flex
e = case SizeExpr' rigid flex
e of
  Const   n :: Offset
n -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeZero   , Offset
n)
  Rigid i :: rigid
i n :: Offset
n -> (rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid rigid
i, Offset
n)
  Flex  x :: flex
x n :: Offset
n -> (flex -> Node rigid flex
forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x , Offset
n)
  Infty     -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty  , 0)

edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint (Constraint lexp :: SizeExpr' rigid flex
lexp cmp :: Cmp
cmp rexp :: SizeExpr' rigid flex
rexp) =
  let (leftNode :: Node rigid flex
leftNode , n :: Offset
n) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
lexp
      (rightNode :: Node rigid flex
rightNode, m :: Offset
m) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr SizeExpr' rigid flex
rexp
  in Node rigid flex
-> Node rigid flex -> Label -> LabelledEdge rigid flex
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
leftNode Node rigid flex
rightNode (Cmp -> Offset -> Label
Label Cmp
cmp (Offset -> Label) -> Offset -> Label
forall a b. (a -> b) -> a -> b
$ Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
n)

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

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

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

hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label
-- hypConn hg NodeZero n2  = Label Le 0  -- WRONG: not the best information
-- hypConn hg n1 NodeInfty = Label Le 0
hypConn :: HypGraph r f -> Node r f -> Node r f -> Label
hypConn hg :: HypGraph r f
hg n1 :: Node r f
n1 n2 :: Node r f
n2
  | Node r f
n1 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n2                                = Cmp -> Offset -> Label
Label Cmp
Le 0
  | Just l :: Label
l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n1 Node r f
n2 = Label
l
  | Bool
otherwise                               = Label
forall a. Top a => a
top

simplifyWithHypotheses :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
  HypGraph rigid flex -> [Constraint' rigid flex] -> Either String [Constraint' rigid flex]
simplifyWithHypotheses :: HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either String [Constraint' rigid flex]
simplifyWithHypotheses hg :: HypGraph rigid flex
hg cons :: [Constraint' rigid flex]
cons = [[Constraint' rigid flex]] -> [Constraint' rigid flex]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constraint' rigid flex]] -> [Constraint' rigid flex])
-> Either String [[Constraint' rigid flex]]
-> Either String [Constraint' rigid flex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint' rigid flex -> Either String [Constraint' rigid flex])
-> [Constraint' rigid flex]
-> Either String [[Constraint' rigid flex]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Constraint' rigid flex -> Either String [Constraint' rigid flex])
-> Constraint' rigid flex -> Either String [Constraint' rigid flex]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 Constraint' rigid flex -> Either String [Constraint' rigid flex]
test) [Constraint' rigid flex]
cons
  where
    -- Test whether a constraint is compatible with the hypotheses:
    -- Succeeds, if constraint is implied by hypotheses,
    -- fails otherwise.
    test :: Constraint' rigid flex -> Either String [Constraint' rigid flex]
test c :: Constraint' rigid flex
c = do
      let Edge n1 :: Node rigid flex
n1 n2 :: Node rigid flex
n2 l :: Label
l = Constraint' rigid flex -> Edge (Node rigid flex) Label
forall rigid flex.
Constraint' rigid flex -> LabelledEdge rigid flex
edgeFromConstraint Constraint' rigid flex
c
          l' :: Label
l' = HypGraph rigid flex -> Node rigid flex -> Node rigid flex -> Label
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> Node r f -> Node r f -> Label
hypConn HypGraph rigid flex
hg Node rigid flex
n1 Node rigid flex
n2
      -- l' <- lookupEdge hg n1 n2
      Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Label
l' Label -> Label -> Bool
forall a. Ord a => a -> a -> Bool
<= Label
l) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
        "size constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Constraint' rigid flex -> String
forall a. Pretty a => a -> String
prettyShow Constraint' rigid flex
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not consistent with size hypotheses"
      [Constraint' rigid flex] -> Either String [Constraint' rigid flex]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' rigid flex
c]
      -- 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 String (ConGraph r f)
constraintGraph :: [Constraint' r f] -> HypGraph r f -> Either String (HypGraph r f)
constraintGraph cons0 :: [Constraint' r f]
cons0 hg :: HypGraph r f
hg = do
  String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "original constraints cons0 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons0
  -- Simplify constraints, ensure they are locally consistent with
  -- hypotheses.
  [Constraint' r f]
cons <- HypGraph r f
-> [Constraint' r f] -> Either String [Constraint' r f]
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either String [Constraint' rigid flex]
simplifyWithHypotheses HypGraph r f
hg [Constraint' r f]
cons0
  String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "simplified constraints cons = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons
  -- Build a transitive graph from constraints.
  let g :: HypGraph r f
g = HypGraph r f -> HypGraph r f
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos (HypGraph r f -> HypGraph r f) -> HypGraph r f -> HypGraph r f
forall a b. (a -> b) -> a -> b
$ [Constraint' r f] -> HypGraph r f
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cons
  String -> Either String ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ "transitive graph g = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Edge (Node r f) Label] -> String
forall a. Pretty a => a -> String
prettyShow (HypGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList HypGraph r f
g)
  -- Ensure it has no negative loops.
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HypGraph r f -> Bool
forall a. Negative a => a -> Bool
negative HypGraph r f
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
    "size constraint graph has negative loops"
  -- Ensure it does not constrain the hypotheses.
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HypGraph r f
hg HypGraph r f -> HypGraph r f -> Bool
forall r f a.
(Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
 Negative a) =>
Graph r f a -> Graph r f a -> Bool
`implies` HypGraph r f
g) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$
    "size constraint graph constrains size hypotheses"
  HypGraph r f -> Either String (HypGraph r f)
forall (m :: * -> *) a. Monad m => a -> m a
return HypGraph r f
g

type ConGraphs r f = Graphs r f Label

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

-- | 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 :: ConGraph r f -> ([f], ConGraph r f)
infinityFlexs g :: ConGraph r f
g = ([f]
infFlexs, [f] -> ConGraph r f -> ConGraph r f
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
infFlexs ConGraph r f
g)
  where
    -- get the flexibles that need to be set to infinity
    infFlexs :: [f]
infFlexs = (Edge (Node r f) Label -> Maybe f)
-> [Edge (Node r f) Label] -> [f]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Edge (Node r f) Label -> Maybe f
forall e rigid b. Negative e => Edge (Node rigid b) e -> Maybe b
flexNeg ([Edge (Node r f) Label] -> [f]) -> [Edge (Node r f) Label] -> [f]
forall a b. (a -> b) -> a -> b
$ ConGraph r f -> [Edge (Node r f) Label]
forall n e. Ord n => Graph n e -> [Edge n e]
Graph.diagonal ConGraph r f
g
    flexNeg :: Edge (Node rigid b) e -> Maybe b
flexNeg e :: Edge (Node rigid b) e
e = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Edge (Node rigid b) e -> Bool
forall a. Negative a => a -> Bool
negative Edge (Node rigid b) e
e
      Node rigid b -> Maybe b
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode (Edge (Node rigid b) e -> Node rigid b
forall n e. Edge n e -> n
src Edge (Node rigid b) e
e)

class SetToInfty f a where
  setToInfty :: [f] -> a -> a

instance (Eq f) => SetToInfty f (Node r f) where
  setToInfty :: [f] -> Node r f -> Node r f
setToInfty xs :: [f]
xs (NodeFlex x :: f
x) | f
x f -> [f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [f]
xs = Node r f
forall rigid flex. Node rigid flex
NodeInfty
  setToInfty xs :: [f]
xs n :: Node r f
n = Node r f
n

instance (Eq f) => SetToInfty f (Edge' r f a) where
  setToInfty :: [f] -> Edge' r f a -> Edge' r f a
setToInfty xs :: [f]
xs (Edge n1 :: Node r f
n1 n2 :: Node r f
n2 l :: a
l) = Node r f -> Node r f -> a -> Edge' r f a
forall n e. n -> n -> e -> Edge n e
Edge ([f] -> Node r f -> Node r f
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs Node r f
n1) ([f] -> Node r f -> Node r f
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs Node r f
n2) a
l

instance (Ord r, Ord f) => SetToInfty f (ConGraph r f) where
  setToInfty :: [f] -> ConGraph r f -> ConGraph r f
setToInfty xs :: [f]
xs = [Edge (Node r f) Label] -> ConGraph r f
forall n e. Ord n => [Edge n e] -> Graph n e
graphFromList ([Edge (Node r f) Label] -> ConGraph r f)
-> (ConGraph r f -> [Edge (Node r f) Label])
-> ConGraph r f
-> ConGraph r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge (Node r f) Label -> Bool)
-> [Edge (Node r f) Label] -> [Edge (Node r f) Label]
forall a. (a -> Bool) -> [a] -> [a]
filter Edge (Node r f) Label -> Bool
forall rigid flex. Edge (Node rigid flex) Label -> Bool
h ([Edge (Node r f) Label] -> [Edge (Node r f) Label])
-> (ConGraph r f -> [Edge (Node r f) Label])
-> ConGraph r f
-> [Edge (Node r f) Label]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge (Node r f) Label -> Edge (Node r f) Label)
-> [Edge (Node r f) Label] -> [Edge (Node r f) Label]
forall a b. (a -> b) -> [a] -> [b]
map ([f] -> Edge (Node r f) Label -> Edge (Node r f) Label
forall f a. SetToInfty f a => [f] -> a -> a
setToInfty [f]
xs) ([Edge (Node r f) Label] -> [Edge (Node r f) Label])
-> (ConGraph r f -> [Edge (Node r f) Label])
-> ConGraph r f
-> [Edge (Node r f) Label]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList
    where
      -- filter out edges @oo + k <= oo@
      h :: Edge (Node rigid flex) Label -> Bool
h (Edge NodeInfty NodeInfty (Label Le _)) = Bool
False
      h _ = Bool
True


-- * Compute solution from constraint graph.

instance Plus Offset Weight Weight where
  plus :: Offset -> Weight -> Weight
plus e :: Offset
e Infinity   = Weight
Infinity
  plus e :: Offset
e (Offset x :: Offset
x) = Offset -> Weight
Offset (Offset -> Weight) -> Offset -> Weight
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a b c. Plus a b c => a -> b -> c
plus Offset
e Offset
x

instance Plus (SizeExpr' r f) Weight (SizeExpr' r f) where
  plus :: SizeExpr' r f -> Weight -> SizeExpr' r f
plus e :: SizeExpr' r f
e Infinity   = SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
  plus e :: SizeExpr' r f
e (Offset x :: Offset
x) = SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
plus SizeExpr' r f
e Offset
x

instance Plus (SizeExpr' r f) Label (SizeExpr' r f) where
  plus :: SizeExpr' r f -> Label -> SizeExpr' r f
plus e :: SizeExpr' r f
e l :: Label
l = SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
plus SizeExpr' r f
e (Label -> Weight
toWeight Label
l)

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

emptyBound :: Bound r f
emptyBound :: Bound r f
emptyBound = Bound r f
forall k a. Map k a
Map.empty

data Bounds r f = Bounds
  { Bounds r f -> Bound r f
lowerBounds :: Bound r f
  , Bounds r f -> Bound r f
upperBounds :: Bound r f
  , Bounds r f -> Set f
mustBeFinite :: Set f
    -- ^ These metas are < ∞.
  }

-- | Compute a lower bound for a flexible from an edge.
edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound e :: LabelledEdge r f
e =
  case LabelledEdge r f
e of
    (Edge n1 :: Node r f
n1 n2 :: Node r f
n2 LInf) -> Maybe (f, SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Edge NodeZero (NodeFlex x :: f
x) (Label Le o :: Offset
o)) | Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const 0)
    (Edge NodeZero (NodeFlex x :: f
x) (Label Lt o :: Offset
o)) | Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const 0)
    (Edge n1 :: Node r f
n1 (NodeFlex x :: f
x) l :: Label
l) -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a. a -> Maybe a
Just (f
x, Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n1 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` (- (Label -> Weight
toWeight Label
l)))
    _ -> Maybe (f, SizeExpr' r f)
forall a. Maybe a
Nothing

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

-- | Compute the lower bounds for all flexibles in a graph.
graphToLowerBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
graphToLowerBounds :: [LabelledEdge r f] -> Bound r f
graphToLowerBounds = ((Bound r f -> LabelledEdge r f -> Bound r f)
 -> Bound r f -> [LabelledEdge r f] -> Bound r f)
-> Bound r f
-> (Bound r f -> LabelledEdge r f -> Bound r f)
-> [LabelledEdge r f]
-> Bound r f
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bound r f -> LabelledEdge r f -> Bound r f)
-> Bound r f -> [LabelledEdge r f] -> Bound r f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bound r f
forall r f. Bound r f
emptyBound ((Bound r f -> LabelledEdge r f -> Bound r f)
 -> [LabelledEdge r f] -> Bound r f)
-> (Bound r f -> LabelledEdge r f -> Bound r f)
-> [LabelledEdge r f]
-> Bound r f
forall a b. (a -> b) -> a -> b
$ \ bs :: Bound r f
bs e :: LabelledEdge r f
e ->
  case LabelledEdge r f -> Maybe (f, SizeExpr' r f)
forall r f. LabelledEdge r f -> Maybe (f, SizeExpr' r f)
edgeToLowerBound LabelledEdge r f
e of
    Nothing          -> Bound r f
bs
    Just (x :: f
x, Flex{}) -> Bound r f
bs  -- ignore flexible bounds
    Just (x :: f
x, a :: SizeExpr' r f
a)      -> (Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f))
-> f -> Set (SizeExpr' r f) -> Bound r f -> Bound r f
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union f
x (SizeExpr' r f -> Set (SizeExpr' r f)
forall a. a -> Set a
Set.singleton SizeExpr' r f
a) Bound r f
bs

-- | Compute the upper bounds for all flexibles in a graph.
graphToUpperBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds :: [LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds = (((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
 -> (Bound r f, Set f) -> [LabelledEdge r f] -> (Bound r f, Set f))
-> (Bound r f, Set f)
-> ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> [LabelledEdge r f]
-> (Bound r f, Set f)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> (Bound r f, Set f) -> [LabelledEdge r f] -> (Bound r f, Set f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bound r f
forall r f. Bound r f
emptyBound, Set f
forall a. Set a
Set.empty) (((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
 -> [LabelledEdge r f] -> (Bound r f, Set f))
-> ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
-> [LabelledEdge r f]
-> (Bound r f, Set f)
forall a b. (a -> b) -> a -> b
$ \ (bs :: Bound r f
bs, fs :: Set f
fs) e :: LabelledEdge r f
e ->
  case LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
forall r f. LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
edgeToUpperBound LabelledEdge r f
e of
    Nothing             -> (Bound r f
bs, Set f
fs)
    Just (x :: f
x, _, Flex{}) -> (Bound r f
bs, Set f
fs)  -- ignore flexible bounds
    Just (x :: f
x, Lt, Infty) -> (Bound r f
bs, f -> Set f -> Set f
forall a. Ord a => a -> Set a -> Set a
Set.insert f
x Set f
fs)
    Just (x :: f
x, Le, a :: SizeExpr' r f
a)     -> ((Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f))
-> f -> Set (SizeExpr' r f) -> Bound r f -> Bound r f
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union f
x (SizeExpr' r f -> Set (SizeExpr' r f)
forall a. a -> Set a
Set.singleton SizeExpr' r f
a) Bound r f
bs, Set f
fs)
    _                   -> (Bound r f, Set f)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Compute the bounds for all flexibles in a graph.
bounds :: (Ord r, Ord f) => ConGraph r f -> Bounds r f
bounds :: ConGraph r f -> Bounds r f
bounds g :: ConGraph r f
g = Bound r f -> Bound r f -> Set f -> Bounds r f
forall r f. Bound r f -> Bound r f -> Set f -> Bounds r f
Bounds Bound r f
lbs Bound r f
ubs Set f
fs
  where edges :: [Edge (Node r f) Label]
edges     = ConGraph r f -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList ConGraph r f
g
        lbs :: Bound r f
lbs       = [Edge (Node r f) Label] -> Bound r f
forall r f. (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
graphToLowerBounds [Edge (Node r f) Label]
edges
        (ubs :: Bound r f
ubs, fs :: Set f
fs) = [Edge (Node r f) Label] -> (Bound r f, Set f)
forall r f.
(Ord r, Ord f) =>
[LabelledEdge r f] -> (Bound r f, Set f)
graphToUpperBounds [Edge (Node r f) Label]
edges


-- | 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 :: HypGraph r f -> [Node r f] -> [Node r f]
smallest hg :: HypGraph r f
hg ns :: [Node r f]
ns
  | Node r f
forall rigid flex. Node rigid flex
NodeZero Node r f -> [Node r f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node r f]
ns = [Node r f
forall rigid flex. Node rigid flex
NodeZero]
  | Bool
otherwise          = (Node r f -> Bool) -> [Node r f] -> [Node r f]
forall a. (a -> Bool) -> [a] -> [a]
filter Node r f -> Bool
hasNoPred [Node r f]
ns where
      hasNoPred :: Node r f -> Bool
hasNoPred NodeInfty = Bool
False
      hasNoPred n :: Node r f
n = [()] -> Bool
forall a. Null a => a -> Bool
null ([()] -> Bool) -> [()] -> Bool
forall a b. (a -> b) -> a -> b
$ (Node r f -> Maybe ()) -> [Node r f] -> [()]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node r f -> Maybe ()
strictEdge [Node r f]
ns where
        -- is there an edge n -l-> n' with l <= 0
        strictEdge :: Node r f -> Maybe ()
strictEdge n' :: Node r f
n' = do
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Node r f
n Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/= Node r f
n')  -- exclude loops
          Label
l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n' Node r f
n
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Label -> Weight
toWeight Label
l Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= 0)
          () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | 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 :: HypGraph r f -> [Node r f] -> [Node r f]
largest hg :: HypGraph r f
hg ns :: [Node r f]
ns
  | Node r f
forall rigid flex. Node rigid flex
NodeInfty Node r f -> [Node r f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node r f]
ns = [Node r f
forall rigid flex. Node rigid flex
NodeInfty]
  | Bool
otherwise          = (Node r f -> Bool) -> [Node r f] -> [Node r f]
forall a. (a -> Bool) -> [a] -> [a]
filter Node r f -> Bool
hasNoSucc [Node r f]
ns where
      hasNoSucc :: Node r f -> Bool
hasNoSucc NodeZero = Bool
False
      hasNoSucc n :: Node r f
n = [()] -> Bool
forall a. Null a => a -> Bool
null ([()] -> Bool) -> [()] -> Bool
forall a b. (a -> b) -> a -> b
$ (Node r f -> Maybe ()) -> [Node r f] -> [()]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Node r f -> Maybe ()
strictEdge [Node r f]
ns where
        -- is there an edge n -l-> n' with l <= 0
        strictEdge :: Node r f -> Maybe ()
strictEdge n' :: Node r f
n' = do
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Node r f
n Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/= Node r f
n')  -- exclude loops
          Label
l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n Node r f
n'
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Label -> Weight
toWeight Label
l Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= 0)
          () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{-|  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 :: Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs hg :: Graph r f a
hg srcs :: [Node r f]
srcs = [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall k a. Ord k => [Map k [a]] -> Map k [a]
intersectAll ([Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a])
-> [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall a b. (a -> b) -> a -> b
$ (Node r f -> Map (Node r f) [Edge' r f a])
-> [Node r f] -> [Map (Node r f) [Edge' r f a]]
forall a b. (a -> b) -> [a] -> [b]
map ([Edge' r f a] -> Map (Node r f) [Edge' r f a]
forall k e. Ord k => [Edge k e] -> Map k [Edge k e]
buildmap ([Edge' r f a] -> Map (Node r f) [Edge' r f a])
-> (Node r f -> [Edge' r f a])
-> Node r f
-> Map (Node r f) [Edge' r f a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph r f a -> Node r f -> [Edge' r f a]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
outgoing Graph r f a
hg) [Node r f]
srcs
  where
   buildmap :: [Edge k e] -> Map k [Edge k e]
buildmap            = [(k, [Edge k e])] -> Map k [Edge k e]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, [Edge k e])] -> Map k [Edge k e])
-> ([Edge k e] -> [(k, [Edge k e])])
-> [Edge k e]
-> Map k [Edge k e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge k e -> (k, [Edge k e])) -> [Edge k e] -> [(k, [Edge k e])]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: Edge k e
e -> (Edge k e -> k
forall n e. Edge n e -> n
dest Edge k e
e, [Edge k e
e]))
   intersectAll :: [Map k [a]] -> Map k [a]
intersectAll []     = Map k [a]
forall k a. Map k a
Map.empty
   intersectAll (m :: Map k [a]
m:ms :: [Map k [a]]
ms) = (Map k [a] -> Map k [a] -> Map k [a])
-> Map k [a] -> [Map k [a]] -> Map k [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([a] -> [a] -> [a]) -> Map k [a] -> Map k [a] -> Map k [a]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)) Map k [a]
m [Map k [a]]
ms

{-|  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 :: Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonPreds hg :: Graph r f a
hg tgts :: [Node r f]
tgts = [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall k a. Ord k => [Map k [a]] -> Map k [a]
intersectAll ([Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a])
-> [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
forall a b. (a -> b) -> a -> b
$  (Node r f -> Map (Node r f) [Edge' r f a])
-> [Node r f] -> [Map (Node r f) [Edge' r f a]]
forall a b. (a -> b) -> [a] -> [b]
map ([Edge' r f a] -> Map (Node r f) [Edge' r f a]
forall k e. Ord k => [Edge k e] -> Map k [Edge k e]
buildmap ([Edge' r f a] -> Map (Node r f) [Edge' r f a])
-> (Node r f -> [Edge' r f a])
-> Node r f
-> Map (Node r f) [Edge' r f a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph r f a -> Node r f -> [Edge' r f a]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
incoming Graph r f a
hg) [Node r f]
tgts
  where
   buildmap :: [Edge k e] -> Map k [Edge k e]
buildmap = [(k, [Edge k e])] -> Map k [Edge k e]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, [Edge k e])] -> Map k [Edge k e])
-> ([Edge k e] -> [(k, [Edge k e])])
-> [Edge k e]
-> Map k [Edge k e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge k e -> (k, [Edge k e])) -> [Edge k e] -> [(k, [Edge k e])]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: Edge k e
e -> (Edge k e -> k
forall n e. Edge n e -> n
src Edge k e
e, [Edge k e
e]))
   intersectAll :: [Map k [a]] -> Map k [a]
intersectAll []     = Map k [a]
forall k a. Map k a
Map.empty
   intersectAll (m :: Map k [a]
m:ms :: [Map k [a]]
ms) = (Map k [a] -> Map k [a] -> Map k [a])
-> Map k [a] -> [Map k [a]] -> Map k [a]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([a] -> [a] -> [a]) -> Map k [a] -> Map k [a] -> Map k [a]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)) Map k [a]
m [Map k [a]]
ms

-- | 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' :: HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' hg :: HypGraph r f
hg (node1 :: Node r f
node1, n :: Offset
n) (node2 :: Node r f
node2, m :: Offset
m) = do
  let sucs :: Map (Node r f) [Edge' r f Label]
sucs     = HypGraph r f -> [Node r f] -> Map (Node r f) [Edge' r f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs HypGraph r f
hg [Node r f
node1, Node r f
node2]
      sucNodes :: [Node r f]
sucNodes = HypGraph r f -> [Node r f] -> [Node r f]
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
smallest HypGraph r f
hg ([Node r f] -> [Node r f]) -> [Node r f] -> [Node r f]
forall a b. (a -> b) -> a -> b
$ Map (Node r f) [Edge' r f Label] -> [Node r f]
forall k a. Map k a -> [k]
Map.keys Map (Node r f) [Edge' r f Label]
sucs
  String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("lub': sucs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map (Node r f) [Edge' r f Label] -> String
forall a. Show a => a -> String
show Map (Node r f) [Edge' r f Label]
sucs) -- FIXME: prettyShow
  case [Node r f]
sucNodes of
    -- there is a unique smallest common successor n0 of node1 and node2
    [n0 :: 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 = [Edge' r f Label] -> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a. a -> Maybe a -> a
fromMaybe [Edge' r f Label]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Edge' r f Label] -> [Edge' r f Label])
-> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a b. (a -> b) -> a -> b
$ Node r f
-> Map (Node r f) [Edge' r f Label] -> Maybe [Edge' r f Label]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node r f
n0 Map (Node r f) [Edge' r f Label]
sucs
      case [Edge' r f Label]
es of
        [ Edge node1x :: Node r f
node1x n1 :: Node r f
n1 l1 :: Label
l1 ,
          Edge node2x :: Node r f
node2x n2 :: Node r f
n2 l2 :: Label
l2 ] -> do
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n1)         Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n2)         Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node1 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node1x)  Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node2 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node2x)  Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          -- 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 = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
max (Offset
n Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l1) (Offset
m Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l2)
          SizeExpr' r f -> Maybe (SizeExpr' r f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n0 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Weight
o
        _ -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- otherwise, we cannot compute the sup
    _ -> do
      let SizeExpr' r f
a1 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node1 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n
      let SizeExpr' r f
a2 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node2 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
m
      String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("cannot compute lub of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " because sucNodes = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Node r f] -> String
forall a. Pretty a => a -> String
prettyShow [Node r f]
sucNodes)
      Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing

-- | 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' :: HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
glb' hg :: HypGraph r f
hg (node1 :: Node r f
node1, n :: Offset
n) (node2 :: Node r f
node2, m :: Offset
m) = do
  let preds :: Map (Node r f) [Edge' r f Label]
preds     = HypGraph r f -> [Node r f] -> Map (Node r f) [Edge' r f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonPreds HypGraph r f
hg [Node r f
node1, Node r f
node2]
      predNodes :: [Node r f]
predNodes = HypGraph r f -> [Node r f] -> [Node r f]
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> [Node r f] -> [Node r f]
largest HypGraph r f
hg ([Node r f] -> [Node r f]) -> [Node r f] -> [Node r f]
forall a b. (a -> b) -> a -> b
$ Map (Node r f) [Edge' r f Label] -> [Node r f]
forall k a. Map k a -> [k]
Map.keys Map (Node r f) [Edge' r f Label]
preds
  String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("glb': preds = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map (Node r f) [Edge' r f Label] -> String
forall a. Show a => a -> String
show Map (Node r f) [Edge' r f Label]
preds) -- FIXME: prettyShow
  case [Node r f]
predNodes of
    -- there is a unique greatest common predecessor n0 of node1 and node2
    [n0 :: 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 = [Edge' r f Label] -> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a. a -> Maybe a -> a
fromMaybe [Edge' r f Label]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Edge' r f Label] -> [Edge' r f Label])
-> Maybe [Edge' r f Label] -> [Edge' r f Label]
forall a b. (a -> b) -> a -> b
$ Node r f
-> Map (Node r f) [Edge' r f Label] -> Maybe [Edge' r f Label]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Node r f
n0 Map (Node r f) [Edge' r f Label]
preds
      case [Edge' r f Label]
es of
        [ Edge n1 :: Node r f
n1 node1x :: Node r f
node1x l1 :: Label
l1 ,
          Edge n2 :: Node r f
n2 node2x :: Node r f
node2x l2 :: Label
l2] -> do
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n1)         Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
n0 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
n2)         Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node1 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node1x)  Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Node r f
node2 Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
node2x)  Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          -- 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 = Weight -> Weight -> Weight
forall a. Ord a => a -> a -> a
max (Offset
n Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l1) (Offset
m Offset -> Weight -> Weight
forall a b c. Plus a b c => a -> b -> c
`plus` Label -> Weight
toWeight Label
l2)
          SizeExpr' r f -> Maybe (SizeExpr' r f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n0 SizeExpr' r f -> Weight -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Weight
o
        _ -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- otherwise, we cannot compute the sup
    _ -> do
      let SizeExpr' r f
a1 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node1 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
n
      let SizeExpr' r f
a2 :: SizeExpr' r f = Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
node2 SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
m
      String -> Maybe ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM ("cannot compute glb of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
a2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " because predNodes = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Node r f] -> String
forall a. Pretty a => a -> String
prettyShow [Node r f]
predNodes)
      Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing

-- | 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 :: HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
lub hg :: HypGraph r f
hg a1 :: SizeExpr' r f
a1 a2 :: SizeExpr' r f
a2 =
  case (SizeExpr' r f
a1, SizeExpr' r f
a2) of
    (Flex{}, _)   -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
    (_, Flex{})   -> Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Infty, a2 :: SizeExpr' r f
a2)   -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
    (a1 :: SizeExpr' r f
a1, Infty)   -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
forall rigid flex. SizeExpr' rigid flex
Infty
    (Const n :: Offset
n  , Const m :: Offset
m  )
                  -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Offset -> SizeExpr' r f
forall rigid flex. Offset -> SizeExpr' rigid flex
Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a. Ord a => a -> a -> a
max Offset
n Offset
m
    (Const n :: Offset
n  , Rigid j :: r
j m :: Offset
m)
      | Offset
m Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
n    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a2
      | Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' HypGraph r f
hg (Node r f
forall rigid flex. Node rigid flex
NodeZero, Offset
n) (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)
    (Rigid i :: r
i n :: Offset
n, Const m :: Offset
m  )
      | Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
m    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
a1
      | Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' HypGraph r f
hg (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (Node r f
forall rigid flex. Node rigid flex
NodeZero, Offset
m)
    (Rigid i :: r
i n :: Offset
n, Rigid j :: r
j m :: Offset
m)
      | r
i r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
j    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ r -> Offset -> SizeExpr' r f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid r
i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
forall a b. (a -> b) -> a -> b
$ Offset -> Offset -> Offset
forall a. Ord a => a -> a -> a
max Offset
n Offset
m
      | Bool
otherwise -> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)
lub' HypGraph r f
hg (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i, Offset
n) (r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
j, Offset
m)

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


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

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

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

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

-- * Tests

testSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]
testSuccs :: Map (Node String f) [Edge' String f Label]
testSuccs = Graph String f Label
-> [Node String f] -> Map (Node String f) [Edge' String f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs Graph String f Label
forall rigid flex.
(Ord rigid, Ord flex, IsString rigid) =>
Graph (Node rigid flex) Label
hg [Node String f
forall rigid flex. IsString rigid => Node rigid flex
n1,Node String f
forall rigid flex. IsString rigid => Node rigid flex
n2]
  where
    n1 :: Node rigid flex
n1 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "i"
    n2 :: Node rigid flex
n2 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "j"
    n3 :: Node rigid flex
n3 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "k"
    n4 :: Node rigid flex
n4 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "l"
    n5 :: Node rigid flex
n5 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "m"
    hg :: Graph (Node rigid flex) Label
hg = [Edge (Node rigid flex) Label] -> Graph (Node rigid flex) Label
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
         [ Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 1
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 2
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 3
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 4
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 5
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 6
         ]

-- testLub = smallest hg $ Map.keys $ commonSuccs hg [n1,n2] --
testLub :: (Pretty f, Ord f, Show f) => Maybe (SizeExpr' [Char] f)
testLub :: Maybe (SizeExpr' String f)
testLub = HypGraph String f
-> SizeExpr' String f
-> SizeExpr' String f
-> Maybe (SizeExpr' String f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
lub HypGraph String f
forall rigid flex.
(Ord rigid, Ord flex, IsString rigid) =>
Graph (Node rigid flex) Label
hg (String -> Offset -> SizeExpr' String f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid "i" 0) (String -> Offset -> SizeExpr' String f
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid "j" 2)
  where
    n1 :: Node rigid flex
n1 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "i"
    n2 :: Node rigid flex
n2 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "j"
    n3 :: Node rigid flex
n3 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "k"
    n4 :: Node rigid flex
n4 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "l"
    n5 :: Node rigid flex
n5 = rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid "m"
    hg :: Graph (Node rigid flex) Label
hg = [Edge (Node rigid flex) Label] -> Graph (Node rigid flex) Label
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
         [ Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 0
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 2
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n1 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 4
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 1
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 3
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n2 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 5
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n4 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le 0
         , Node rigid flex
-> Node rigid flex -> Label -> Edge (Node rigid flex) Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n3 Node rigid flex
forall rigid flex. IsString rigid => Node rigid flex
n5 (Label -> Edge (Node rigid flex) Label)
-> Label -> Edge (Node rigid flex) Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Lt 0
         ]