module Agda.TypeChecking.SizedTypes.WarshallSolver where

import Prelude hiding ( null, truncate )


import Control.Monad

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

import Agda.TypeChecking.Pretty (PrettyTCM)
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.SizedTypes.Syntax
import Agda.TypeChecking.SizedTypes.Utils

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

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

import Agda.Utils.Impossible

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

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

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

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

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

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

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

-- | Compute list of edges that start in a given node.
outgoing :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
outgoing :: forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
outgoing Graph r f a
g Node r f
s = Graph r f a -> [Node r f] -> [Edge (Node r f) a]
forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesFrom Graph r f a
g [Node r f
s]

-- | Compute list of edges that target a given node.
--
--   Note: expensive for unidirectional graph representations.
incoming :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
incoming :: forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
incoming Graph r f a
g Node r f
t = Graph r f a -> [Node r f] -> [Edge (Node r f) a]
forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
Graph.edgesTo Graph r f a
g [Node r f
t]

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

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

-- * 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
$c== :: Weight -> Weight -> Bool
== :: Weight -> Weight -> Bool
$c/= :: Weight -> Weight -> Bool
/= :: Weight -> Weight -> Bool
Eq, Int -> Weight -> ShowS
[Weight] -> ShowS
Weight -> String
(Int -> Weight -> ShowS)
-> (Weight -> String) -> ([Weight] -> ShowS) -> Show Weight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Weight -> ShowS
showsPrec :: Int -> Weight -> ShowS
$cshow :: Weight -> String
show :: Weight -> String
$cshowList :: [Weight] -> ShowS
showList :: [Weight] -> ShowS
Show)

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

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

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

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

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

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

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

-- | 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
< Int
0)

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

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

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


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

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

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

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

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

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

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

-- * 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 = Weight
0

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

-- * 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
$cshowsPrec :: forall rigid flex.
(Show rigid, Show flex) =>
Int -> Node rigid flex -> ShowS
showsPrec :: Int -> Node rigid flex -> ShowS
$cshow :: forall rigid flex.
(Show rigid, Show flex) =>
Node rigid flex -> String
show :: Node rigid flex -> String
$cshowList :: forall rigid flex.
(Show rigid, Show flex) =>
[Node rigid flex] -> ShowS
showList :: [Node rigid flex] -> ShowS
Show, Node rigid flex -> Node rigid flex -> Bool
(Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> Eq (Node rigid flex)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
$c== :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
== :: Node rigid flex -> Node rigid flex -> Bool
$c/= :: forall rigid flex.
(Eq rigid, Eq flex) =>
Node rigid flex -> Node rigid flex -> Bool
/= :: Node rigid flex -> Node rigid flex -> Bool
Eq, Eq (Node rigid flex)
Eq (Node rigid flex)
-> (Node rigid flex -> Node rigid flex -> Ordering)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Bool)
-> (Node rigid flex -> Node rigid flex -> Node rigid flex)
-> (Node rigid flex -> Node rigid flex -> Node rigid flex)
-> Ord (Node rigid flex)
Node rigid flex -> Node rigid flex -> Bool
Node rigid flex -> Node rigid flex -> Ordering
Node rigid flex -> Node rigid flex -> Node rigid flex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {rigid} {flex}.
(Ord rigid, Ord flex) =>
Eq (Node rigid flex)
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
$ccompare :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Ordering
compare :: Node rigid flex -> Node rigid flex -> Ordering
$c< :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
< :: Node rigid flex -> Node rigid flex -> Bool
$c<= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
<= :: Node rigid flex -> Node rigid flex -> Bool
$c> :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
> :: Node rigid flex -> Node rigid flex -> Bool
$c>= :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Bool
>= :: Node rigid flex -> Node rigid flex -> Bool
$cmax :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
max :: Node rigid flex -> Node rigid flex -> Node rigid flex
$cmin :: forall rigid flex.
(Ord rigid, Ord flex) =>
Node rigid flex -> Node rigid flex -> Node rigid flex
min :: Node rigid flex -> Node rigid flex -> Node rigid flex
Ord)

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

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

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

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

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

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

instance (Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) where
  e :: Edge' r f a
e@(Edge Node r f
u Node r f
v a
l) compose :: Edge' r f a -> Edge' r f a -> Edge' r f a
`compose` e' :: Edge' r f a
e'@(Edge Node r f
v' Node r f
w a
l')
   | Node r f
v Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
v'    = Node r f -> Node r f -> a -> Edge' r f a
forall n e. n -> n -> e -> Edge n e
Edge Node r f
u Node r f
w (a -> Edge' r f a) -> a -> Edge' r f a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Dioid a => a -> a -> a
`compose` a
l'
   | Bool
otherwise = Edge' r f a
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- 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 :: forall r f a. Graphs r f a
emptyGraphs = []

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

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

-- | Reflexive closure.  Add edges @0 -> n -> n -> oo@ for all nodes @n@.
reflClos :: (Ord r, Ord f, Dioid a) => Set (Node r f) -> Graph r f a -> Graph r f a
reflClos :: forall r f a.
(Ord r, Ord f, Dioid a) =>
Set (Node r f) -> Graph r f a -> Graph r f a
reflClos Set (Node r f)
ns Graph r f a
g = (Graph r f a -> Node r f -> Graph r f a)
-> Graph r f a -> Set (Node r f) -> Graph r f a
forall b a. (b -> a -> b) -> b -> Set a -> b
setFoldl Graph r f a -> Node r f -> Graph r f a
forall {e} {rigid} {flex}.
(Dioid e, Ord rigid, Ord flex) =>
Graph (Node rigid flex) e
-> Node rigid flex -> Graph (Node rigid flex) e
step Graph r f a
g Set (Node r f)
ns' where
    -- 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 Graph (Node rigid flex) e
g Node rigid flex
n = (Graph (Node rigid flex) e
 -> Edge (Node rigid flex) e -> Graph (Node rigid flex) e)
-> Graph (Node rigid flex) e
-> [Edge (Node rigid flex) e]
-> Graph (Node rigid flex) e
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Edge (Node rigid flex) e
 -> Graph (Node rigid flex) e -> Graph (Node rigid flex) e)
-> Graph (Node rigid flex) e
-> Edge (Node rigid flex) e
-> Graph (Node rigid flex) e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Edge (Node rigid flex) e
-> Graph (Node rigid flex) e -> Graph (Node rigid flex) e
forall n e.
(Ord n, MeetSemiLattice e, Top e) =>
Edge n e -> Graph n e -> Graph n e
insertEdge) Graph (Node rigid flex) e
g [Edge (Node rigid flex) e]
es where
      es :: [Edge (Node rigid flex) e]
es = [ Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
forall rigid flex. Node rigid flex
NodeZero Node rigid flex
n  e
forall a. Dioid a => a
unitCompose
           , Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
n        Node rigid flex
n  e
forall a. Dioid a => a
unitCompose
           , Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
forall n e. n -> n -> e -> Edge n e
Edge Node rigid flex
n Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty e
forall a. Dioid a => a
unitCompose
           ]

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

-- implies h g = Map.foldlWithKey (\ b k l -> test k l && b) True g
--   -- NB: doing the @test k l@ before the recursive @b@ gives
--   -- opportunity to short-cut the conjunction @&&@.
--   where
--     -- test :: Key -> a -> Bool
--     test k@(Edge src dest ()) l
--       | isZeroNode src, not (negative l) = True
--       | isInftyNode dest                 = True
--       | isJust $ isFlexNode src          = True
--       | isJust $ isFlexNode dest         = True
--       | isTop l                          = True
--       | otherwise = case lookupEdge h src dest of
--         Nothing -> False
--         Just l' -> if l' <= l then True else
--           trace ("edge " ++ show (l <$ k) ++ " not implied by " ++ show (l' <$ k)) $
--             False

nodeFromSizeExpr :: SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr :: forall rigid flex.
SizeExpr' rigid flex -> (Node rigid flex, Offset)
nodeFromSizeExpr = \case
  Const   Offset
n -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeZero   , Offset
n)
  Rigid rigid
i Offset
n -> (rigid -> Node rigid flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid rigid
i, Offset
n)
  Flex  flex
x Offset
n -> (flex -> Node rigid flex
forall rigid flex. flex -> Node rigid flex
NodeFlex flex
x , Offset
n)
  SizeExpr' rigid flex
Infty     -> (Node rigid flex
forall rigid flex. Node rigid flex
NodeInfty  , Offset
0)

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

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

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

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

type Hyp = Constraint
type Hyp' = Constraint'
type HypGraph r f = Graph r f Label

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

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

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

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

type ConGraph r f = Graph r f Label

constraintGraph ::
  (Ord r, Ord f, Pretty r, Pretty f) =>
  [Constraint' r f] -> HypGraph r f -> Either Error (ConGraph r f)
constraintGraph :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f] -> HypGraph r f -> Either Error (HypGraph r f)
constraintGraph [Constraint' r f]
cons0 Graph (Node r f) Label
hg = do
  String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either Error ()) -> String -> Either Error ()
forall a b. (a -> b) -> a -> b
$ String
"original constraints cons0 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Constraint' r f] -> String
forall a. Pretty a => a -> String
prettyShow [Constraint' r f]
cons0
  -- Simplify constraints, ensure they are locally consistent with
  -- hypotheses.
  [Constraint' r f]
cons <- Graph (Node r f) Label
-> [Constraint' r f] -> Either Error [Constraint' r f]
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either Error [Constraint' rigid flex]
simplifyWithHypotheses Graph (Node r f) Label
hg [Constraint' r f]
cons0
  String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either Error ()) -> String -> Either Error ()
forall a b. (a -> b) -> a -> b
$ String
"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 :: Graph (Node r f) Label
g = Graph (Node r f) Label -> Graph (Node r f) Label
forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
transClos (Graph (Node r f) Label -> Graph (Node r f) Label)
-> Graph (Node r f) Label -> Graph (Node r f) Label
forall a b. (a -> b) -> a -> b
$ [Constraint' r f] -> Graph (Node r f) Label
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cons
  String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either Error ()) -> String -> Either Error ()
forall a b. (a -> b) -> a -> b
$ String
"transitive graph g = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Edge (Node r f) Label] -> String
forall a. Pretty a => a -> String
prettyShow (Graph (Node r f) Label -> [Edge (Node r f) Label]
forall n e. Graph n e -> [Edge n e]
graphToList Graph (Node r f) Label
g)
  -- Ensure it has no negative loops.
  Bool -> Either Error () -> Either Error ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Graph (Node r f) Label -> Bool
forall a. Negative a => a -> Bool
negative Graph (Node r f) Label
g) (Either Error () -> Either Error ())
-> Either Error () -> Either Error ()
forall a b. (a -> b) -> a -> b
$ Error -> Either Error ()
forall a b. a -> Either a b
Left (Error -> Either Error ()) -> Error -> Either Error ()
forall a b. (a -> b) -> a -> b
$
    Error
"size constraint graph has negative loops"
  -- Ensure it does not constrain the hypotheses.
  Bool -> Either Error () -> Either Error ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Graph (Node r f) Label
hg Graph (Node r f) Label -> Graph (Node r f) Label -> 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` Graph (Node r f) Label
g) (Either Error () -> Either Error ())
-> Either Error () -> Either Error ()
forall a b. (a -> b) -> a -> b
$ Error -> Either Error ()
forall a b. a -> Either a b
Left (Error -> Either Error ()) -> Error -> Either Error ()
forall a b. (a -> b) -> a -> b
$
    Error
"size constraint graph constrains size hypotheses"
  Graph (Node r f) Label -> Either Error (Graph (Node r f) Label)
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return Graph (Node r f) Label
g

type ConGraphs r f = Graphs r f Label

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

-- | If we have an edge @X + n <= X@ (with n >= 0), we must set @X = oo@.
infinityFlexs :: (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs :: forall r f. (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
infinityFlexs ConGraph r f
g = ([f]
infFlexs, [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 Edge (Node rigid b) e
e = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Edge (Node rigid b) e -> Bool
forall a. Negative a => a -> Bool
negative Edge (Node rigid b) e
e
      Node rigid b -> Maybe b
forall rigid flex. Node rigid flex -> Maybe flex
isFlexNode (Edge (Node rigid b) e -> Node rigid b
forall n e. Edge n e -> n
src Edge (Node rigid b) e
e)

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

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

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

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


-- * Compute solution from constraint graph.

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

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

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

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

emptyBound :: Bound r f
emptyBound :: forall r f. Bound r f
emptyBound = Map f (Set (SizeExpr' r f))
forall k a. Map k a
Map.empty

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

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

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

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

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

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


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

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

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

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

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

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

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

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

  a1 = Rigid i n
  a2 = Rigid j m

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

-}

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

findRigidBelow :: (Ord r, Ord f) => HypGraph r f -> (SizeExpr' r f) -> Maybe (SizeExpr' r f)
findRigidBelow :: forall r f.
(Ord r, Ord f) =>
HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
findRigidBelow HypGraph r f
hg (Rigid r
i Offset
m) | Offset
m Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
< Offset
0 = do
  let v :: Node r f
v     = r -> Node r f
forall rigid flex. rigid -> Node rigid flex
NodeRigid r
i
      preds :: [Edge' r f Label]
preds = HypGraph r f -> Node r f -> [Edge' r f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> Node r f -> [Edge' r f a]
incoming HypGraph r f
hg Node r f
v
      filt :: Edge' r f Label -> Maybe (Node r f, Offset)
filt e :: Edge' r f Label
e@(Edge Node r f
n Node r f
n' Label
l)
        | Node r f
n' Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
== Node r f
v   =
          case Label -> Weight
toWeight Label
l of
            Weight
Infinity -> Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
            Offset Offset
o -> if Offset
o Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
<= Offset
m then (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
Just (Node r f
n, Offset
o) else Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
        | Bool
otherwise = Maybe (Node r f, Offset)
forall a. HasCallStack => a
__IMPOSSIBLE__
            -- 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)
filt [Edge' r f Label]
preds
  (Node r f
n, Offset
o) <- do
    case [(Node r f, Offset)]
cands of
      []  -> Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
      [(Node r f, Offset)
c] -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Node r f, Offset)
c
      [(Node r f, Offset)]
_   -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Node r f, Offset) -> Maybe (Node r f, Offset))
-> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a b. (a -> b) -> a -> b
$
               ((Node r f, Offset) -> (Node r f, Offset) -> Ordering)
-> [(Node r f, Offset)] -> (Node r f, Offset)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
List.maximumBy (Offset -> Offset -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Offset -> Offset -> Ordering)
-> ((Node r f, Offset) -> Offset)
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Node r f, Offset) -> Offset
forall a b. (a, b) -> b
snd) ([(Node r f, Offset)] -> (Node r f, Offset))
-> [(Node r f, Offset)] -> (Node r f, Offset)
forall a b. (a -> b) -> a -> b
$
                 ((Node r f, Offset) -> Bool)
-> [(Node r f, Offset)] -> [(Node r f, Offset)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Node r f
forall rigid flex. Node rigid flex
NodeZero Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Node r f -> Bool)
-> ((Node r f, Offset) -> Node r f) -> (Node r f, Offset) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node r f, Offset) -> Node r f
forall a b. (a, b) -> a
fst) [(Node r f, Offset)]
cands
  let offset :: Offset
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
>= Offset
0) Maybe ()
forall a. HasCallStack => a
__IMPOSSIBLE__
  SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ Node r f -> SizeExpr' r f
forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
nodeToSizeExpr Node r f
n SizeExpr' r f -> Offset -> SizeExpr' r f
forall a b c. Plus a b c => a -> b -> c
`plus` Offset
offset
findRigidBelow HypGraph r f
hg 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, PrettyTCM f, Show r, Show f)
  => Polarities f
  -> HypGraph r f
  -> ConGraph r f
  -> Either Error (Solution r f)
solveGraph :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f -> HypGraph r f -> Either Error (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg HypGraph r f
g = do
  let (Bounds Bound r f
lbs Bound r f
ubs Set f
fs) = 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 Error [Maybe (f, SizeExpr' r f)]
-> Either Error [(f, SizeExpr' r f)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [f]
-> (f -> Either Error (Maybe (f, SizeExpr' r f)))
-> Either Error [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 Error (Maybe (f, SizeExpr' r f)))
 -> Either Error [Maybe (f, SizeExpr' r f)])
-> (f -> Either Error (Maybe (f, SizeExpr' r f)))
-> Either Error [Maybe (f, SizeExpr' r f)]
forall a b. (a -> b) -> a -> b
$ \ f
x -> (SizeExpr' r f -> (f, SizeExpr' r f))
-> Maybe (SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f
x,) (Maybe (SizeExpr' r f) -> Maybe (f, SizeExpr' r f))
-> Either Error (Maybe (SizeExpr' r f))
-> Either Error (Maybe (f, SizeExpr' r f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      -- get lower and upper bounds for flexible x
      let lx :: [SizeExpr' r f]
lx = 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 Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"lower bounds for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SizeExpr' r f] -> String
forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
lx)
      String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"upper bounds for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SizeExpr' r f] -> String
forall a. Pretty a => a -> String
prettyShow [SizeExpr' r f]
ux)
      -- compute maximum of lower bounds
      Maybe (SizeExpr' r f)
lb <- do
        case [SizeExpr' r f]
lx of
          []     -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
          (SizeExpr' r f
a:[SizeExpr' r f]
as) -> do
            case (SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> [SizeExpr' r f] -> Maybe (SizeExpr' r f)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
lub HypGraph r f
hg) SizeExpr' r f
a [SizeExpr' r f]
as of
              Just SizeExpr' r f
l  -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> SizeExpr' r f
forall a. TruncateOffset a => a -> a
truncateOffset SizeExpr' r f
l
              Maybe (SizeExpr' r f)
Nothing -> Error -> Either Error (Maybe (SizeExpr' r f))
forall a b. a -> Either a b
Left (Error -> Either Error (Maybe (SizeExpr' r f)))
-> Error -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$
                Error
"inconsistent lower bound for" Error -> Error -> Error
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> f -> Error
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => f -> m Doc
P.prettyTCM f
x
      -- compute minimum of upper bounds
      Maybe (SizeExpr' r f)
ub <- do
        case [SizeExpr' r f]
ux of
          []     -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
          (SizeExpr' r f
a:[SizeExpr' r f]
as) -> do
            case (SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f))
-> SizeExpr' r f -> [SizeExpr' r f] -> Maybe (SizeExpr' r f)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
glb HypGraph r f
hg) SizeExpr' r f
a [SizeExpr' r f]
as of
              Just SizeExpr' r f
l | SizeExpr' r f -> Bool
forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' r f
l                  -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
l
                     | Just SizeExpr' r f
l' <- HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
forall r f.
(Ord r, Ord f) =>
HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
findRigidBelow HypGraph r f
hg SizeExpr' r f
l -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
l'
              Maybe (SizeExpr' r f)
_ -> Error -> Either Error (Maybe (SizeExpr' r f))
forall a b. a -> Either a b
Left (Error -> Either Error (Maybe (SizeExpr' r f)))
-> Error -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$
                Error
"inconsistent upper bound for" Error -> Error -> Error
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> f -> Error
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => f -> m Doc
P.prettyTCM f
x
      case (Maybe (SizeExpr' r f)
lb, Maybe (SizeExpr' r f)
ub) of
        (Just SizeExpr' r f
l, Maybe (SizeExpr' r f)
Nothing) -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (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  -- solve x = lower bound
        (Maybe (SizeExpr' r f)
Nothing, Just SizeExpr' r f
u) -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
u  -- solve x = upper bound
        (Just SizeExpr' r f
l,  Just SizeExpr' r f
u) -> do
          String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"lower bound for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
l)
          String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String
"upper bound for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f -> String
forall a. Pretty a => a -> String
prettyShow f
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SizeExpr' r f -> String
forall a. Pretty a => a -> String
prettyShow SizeExpr' r f
u)
          case Polarities f -> f -> Polarity
forall flex. Ord flex => Polarities flex -> flex -> Polarity
getPolarity Polarities f
pols f
x of
            Polarity
Least    -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
l
            Polarity
Greatest -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f)))
-> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a b. (a -> b) -> a -> b
$ SizeExpr' r f -> Maybe (SizeExpr' r f)
forall a. a -> Maybe a
Just SizeExpr' r f
u
        (Maybe (SizeExpr' r f), Maybe (SizeExpr' r f))
_ -> Maybe (SizeExpr' r f) -> Either Error (Maybe (SizeExpr' r f))
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (SizeExpr' r f)
forall a. Maybe a
Nothing
  Solution r f -> Either Error (Solution r f)
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solution r f -> Either Error (Solution r f))
-> Solution r f -> Either Error (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. [(k, a)] -> Map k a
Map.fromDistinctAscList [(f, SizeExpr' r f)]
xas

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

-- * Verify solution

-- | Check that after substitution of the solution,
--   constraints are implied by hypotheses.
verifySolution
  :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
  => HypGraph r f
  -> [Constraint' r f]
  -> Solution r f
  -> Either Error ()
verifySolution :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
HypGraph r f
-> [Constraint' r f] -> Solution r f -> Either Error ()
verifySolution HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol = do
  [Constraint' r f]
cs <- [Constraint' r f] -> Either Error [Constraint' r f]
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint' r f] -> Either Error [Constraint' r f])
-> [Constraint' r f] -> Either Error [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 Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either Error ()) -> String -> Either Error ()
forall a b. (a -> b) -> a -> b
$ String
"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 Error [[Constraint' r f]]
-> Either Error [Constraint' r f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint' r f -> Either Error [Constraint' r f])
-> [Constraint' r f] -> Either Error [[Constraint' r f]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Constraint' r f -> Either Error [Constraint' r f])
-> Constraint' r f -> Either Error [Constraint' r f]
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 ((Constraint' r f -> Either Error [Constraint' r f])
 -> Constraint' r f -> Either Error [Constraint' r f])
-> (Constraint' r f -> Either Error [Constraint' r f])
-> Constraint' r f
-> Either Error [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ \ Constraint' r f
c -> [Constraint' r f] -> Either Error [Constraint' r f]
forall a. a -> Either Error a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c]) [Constraint' r f]
cs
  String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either Error ()) -> String -> Either Error ()
forall a b. (a -> b) -> a -> b
$ String
"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 Error () -> Either Error ()
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 Error () -> Either Error ())
-> Either Error () -> Either Error ()
forall a b. (a -> b) -> a -> b
$
    Error -> Either Error ()
forall a b. a -> Either a b
Left Error
"solution not implied by hypotheses"
{-
  case simplifyWithHypotheses hg $ subst sol cs of
    Nothing -> Left "solution produces inconsistency"
    Just [] -> Right ()
    Just cs -> Left $ "solution leaves constraints " ++ prettyShow cs
-}

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

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

iterateSolver :: forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either Error (Solution r f)
iterateSolver Polarities f
pols HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol0 = do
  HypGraph r f
g <- [Constraint' r f] -> HypGraph r f -> Either Error (HypGraph r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f] -> HypGraph r f -> Either Error (HypGraph r f)
constraintGraph [Constraint' r f]
cs HypGraph r f
hg
  Solution r f
sol <- Polarities f
-> HypGraph r f -> HypGraph r f -> Either Error (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f -> HypGraph r f -> Either Error (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg HypGraph r f
g
  String -> Either Error ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> Either Error ()) -> String -> Either Error ()
forall a b. (a -> b) -> a -> b
$ String
"(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 Error (Solution r f)
forall a. a -> Either Error a
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 Error (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either Error (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 Error (Solution r f))
-> Solution r f -> Either Error (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 :: forall f. Ord f => Map (Node String f) [Edge' String f Label]
testSuccs = Graph String f Label
-> [Node String f] -> Map (Node String f) [Edge' String f Label]
forall r f a.
(Ord r, Ord f) =>
Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
commonSuccs Graph String f Label
hg [Node String f
forall {flex}. Node String flex
n1,Node String f
forall {flex}. Node String flex
n2]
  where
    n1 :: Node String flex
n1 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"i"
    n2 :: Node String flex
n2 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"j"
    n3 :: Node String flex
n3 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"k"
    n4 :: Node String flex
n4 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"l"
    n5 :: Node String flex
n5 = String -> Node String flex
forall rigid flex. rigid -> Node rigid flex
NodeRigid String
"m"
    hg :: Graph String f Label
hg = [Edge' String f Label] -> Graph String f Label
forall n e. Ord n => [Edge n e] -> Graph n e
Graph.fromEdges
         [ Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n3 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
1
         , Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
2
         , Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n1 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
3
         , Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n3 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
4
         , Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n4 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
5
         , Node String f -> Node String f -> Label -> Edge' String f Label
forall n e. n -> n -> e -> Edge n e
Graph.Edge Node String f
forall {flex}. Node String flex
n2 Node String f
forall {flex}. Node String flex
n5 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
forall a b. (a -> b) -> a -> b
$ Cmp -> Offset -> Label
Label Cmp
Le Offset
6
         ]

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