{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.SizedTypes.WarshallSolver where

import Prelude hiding ( null, truncate )


import Control.Monad

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

import Agda.TypeChecking.Monad.Base (TCM)
import Agda.TypeChecking.Pretty (PrettyTCM)
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.SizedTypes.Syntax hiding (CTrans, simplify1)
import qualified Agda.TypeChecking.SizedTypes.Syntax as S
import Agda.TypeChecking.SizedTypes.Utils

import Agda.Utils.Graph.AdjacencyMap.Unidirectional
  (Edge(..), Nodes(..), nodes, computeNodes)
-- (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.Syntax.Common.Pretty

import Agda.Utils.Impossible

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

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

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

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

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

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

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

-- | 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


-- | Error messages produced by the solver.

type Error = TCM Doc

type CTrans r f = Constraint' r f -> Either Error [Constraint' r f]

simplify1 :: (Pretty f, Pretty r, Eq r)
  => CTrans r f
  -> CTrans r f
simplify1 :: forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 CTrans r f
f Constraint' r f
c = case CTrans r f -> CTrans r f
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
S.simplify1 ((TCMT IO Doc -> Maybe [Constraint' r f])
-> ([Constraint' r f] -> Maybe [Constraint' r f])
-> Either (TCMT IO Doc) [Constraint' r f]
-> Maybe [Constraint' r f]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe [Constraint' r f] -> TCMT IO Doc -> Maybe [Constraint' r f]
forall a b. a -> b -> a
const Maybe [Constraint' r f]
forall a. Maybe a
Nothing) [Constraint' r f] -> Maybe [Constraint' r f]
forall a. a -> Maybe a
Just (Either (TCMT IO Doc) [Constraint' r f] -> Maybe [Constraint' r f])
-> CTrans r f -> CTrans r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CTrans r f
f) Constraint' r f
c of
  Maybe [Constraint' r f]
Nothing -> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. a -> Either a b
Left (TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f])
-> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> Constraint' r f -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty Constraint' r f
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> TCMT IO Doc
"is inconsistent"
  Just [Constraint' r f]
cs -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. b -> Either a b
Right [Constraint' r f]
cs

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

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

type ConGraphs r f = Graphs r f Label

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

-- | 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
          l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n' Node r f
n
          guard (toWeight l <= 0)
          return ()

-- | 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
          l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
forall n e. Ord n => Graph n e -> n -> n -> Maybe e
lookupEdge HypGraph r f
hg Node r f
n Node r f
n'
          guard (toWeight l <= 0)
          return ()

{-|  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
  (n, o) <- do
    case [(Node r f, Offset)]
cands of
      []  -> Maybe (Node r f, Offset)
forall a. Maybe a
Nothing
      [(Node r f, Offset)
c] -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Node r f, Offset)
c
      [(Node r f, Offset)]
_   -> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Node r f, Offset) -> Maybe (Node r f, Offset))
-> (Node r f, Offset) -> Maybe (Node r f, Offset)
forall a b. (a -> b) -> a -> b
$
               ((Node r f, Offset) -> (Node r f, Offset) -> Ordering)
-> [(Node r f, Offset)] -> (Node r f, Offset)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
List.maximumBy (Offset -> Offset -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Offset -> Offset -> Ordering)
-> ((Node r f, Offset) -> Offset)
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Node r f, Offset) -> Offset
forall a b. (a, b) -> b
snd) ([(Node r f, Offset)] -> (Node r f, Offset))
-> [(Node r f, Offset)] -> (Node r f, Offset)
forall a b. (a -> b) -> a -> b
$
                 ((Node r f, Offset) -> Bool)
-> [(Node r f, Offset)] -> [(Node r f, Offset)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Node r f
forall rigid flex. Node rigid flex
NodeZero Node r f -> Node r f -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Node r f -> Bool)
-> ((Node r f, Offset) -> Node r f) -> (Node r f, Offset) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node r f, Offset) -> Node r f
forall a b. (a, b) -> a
fst) [(Node r f, Offset)]
cands
  let offset = Offset
m Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
o
  unless (offset >= 0) __IMPOSSIBLE__
  return $ nodeToSizeExpr n `plus` offset
findRigidBelow HypGraph r f
hg SizeExpr' r f
e = Maybe (SizeExpr' r f)
forall a. HasCallStack => a
__IMPOSSIBLE__
  -- error $ "findRigidBelow: impossible: " ++ prettyShow e


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

-- | 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 (TCMT IO Doc) (Solution r f)
solveGraphs Polarities f
pols HypGraph r f
hg ConGraphs r f
gs =
  Map f (SizeExpr' r f) -> Solution r f
forall rigid flex.
Map flex (SizeExpr' rigid flex) -> Solution rigid flex
Solution (Map f (SizeExpr' r f) -> Solution r f)
-> ([Map f (SizeExpr' r f)] -> Map f (SizeExpr' r f))
-> [Map f (SizeExpr' r f)]
-> Solution r f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Map f (SizeExpr' r f)] -> Map f (SizeExpr' r f)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ([Map f (SizeExpr' r f)] -> Solution r f)
-> Either (TCMT IO Doc) [Map f (SizeExpr' r f)]
-> Either (TCMT IO Doc) (Solution r f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HypGraph r f -> Either (TCMT IO Doc) (Map f (SizeExpr' r f)))
-> ConGraphs r f -> Either (TCMT IO Doc) [Map f (SizeExpr' r f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Solution r f -> Map f (SizeExpr' r f)
forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution (Solution r f -> Map f (SizeExpr' r f))
-> (HypGraph r f -> Either (TCMT IO Doc) (Solution r f))
-> HypGraph r f
-> Either (TCMT IO Doc) (Map f (SizeExpr' r f))
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Polarities f
-> HypGraph r f
-> HypGraph r f
-> Either (TCMT IO Doc) (Solution r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> HypGraph r f
-> Either (TCMT IO Doc) (Solution r f)
solveGraph Polarities f
pols HypGraph r f
hg) ConGraphs r f
gs

-- * 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 (TCMT IO Doc) ()
verifySolution HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol = do
  cs <- [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f])
-> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a b. (a -> b) -> a -> b
$ Solution r f -> [Constraint' r f] -> [Constraint' r f]
forall r f a. Substitute r f a => Solution r f -> a -> a
subst Solution r f
sol [Constraint' r f]
cs
  traceM $ "substituted constraints " ++ prettyShow cs
  cs <- -- maybe (Left "solution produces inconsistency") Right $
          concat <$> mapM (simplify1 $ \ Constraint' r f
c -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
forall a. a -> Either (TCMT IO Doc) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' r f
c]) cs
  traceM $ "simplified substituted constraints " ++ prettyShow cs
  -- cs <- maybe (Left "solution produces inconsistency") Right $
  --         simplifyWithHypotheses hg cs
  let g = [Constraint' r f] -> HypGraph r f
forall rigid flex.
(Ord rigid, Ord flex) =>
[Constraint' rigid flex] -> Graph rigid flex Label
graphFromConstraints [Constraint' r f]
cs
  unless (hg `implies` g) $
    Left "solution not implied by hypotheses"
{-
  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 (TCMT IO Doc) (Solution r f)
iterateSolver Polarities f
pols HypGraph r f
hg [Constraint' r f]
cs Solution r f
sol0 = do
  g <- [Constraint' r f]
-> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f) =>
[Constraint' r f]
-> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
constraintGraph [Constraint' r f]
cs HypGraph r f
hg
  sol <- solveGraph pols hg g
  traceM $ "(partial) solution " ++ prettyShow sol
  if null sol then return sol0 else
    iterateSolver pols hg (subst sol cs) $ Solution $
      Map.unionWith __IMPOSSIBLE__ (theSolution sol) $
        theSolution $ subst sol sol0

-- * 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
         ]