    {- | Construct a graph from constraints
    @
       x + n <= y   becomes   x ---(-n)---> y
       x <= n + y   becomes   x ---(+n)---> y
    @
    the default edge (= no edge) is labelled with infinity.

    Building the graph involves keeping track of the node names.
    We do this in a finite map, assigning consecutive numbers to nodes.
    -}
    module Agda.Utils.Warshall where

    import Control.Monad.State

    import Data.Maybe
    import Data.Array
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map

    import Agda.Utils.SemiRing
    import Agda.Utils.List (nubOn)
    import Agda.Utils.Pretty as P

    import Agda.Utils.Impossible

    type Matrix a = Array (Int,Int) a

    -- assuming a square matrix
    warshall :: SemiRing a => Matrix a -> Matrix a
    warshall :: forall a. SemiRing a => Matrix a -> Matrix a
    warshall Matrix a
    a0 = Int -> Matrix a -> Matrix a
    loop Int
    r Matrix a
    a0 where
      b :: ((Int, Int), (Int, Int))
    b@((Int
    r,Int
    c),(Int
    r',Int
    c')) = Matrix a -> ((Int, Int), (Int, Int))
    forall i e. Array i e -> (i, i)
    bounds Matrix a
    a0 -- assuming r == c and r' == c'
      loop :: Int -> Matrix a -> Matrix a
    loop Int
    k Matrix a
    a | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    r' =
        Int -> Matrix a -> Matrix a
    loop (Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (((Int, Int), (Int, Int)) -> [((Int, Int), a)] -> Matrix a
    forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
    array ((Int, Int), (Int, Int))
    b [ ((Int
    i,Int
    j),
                               (Matrix a
    aMatrix a -> (Int, Int) -> a
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    i,Int
    j)) a -> a -> a
    forall a. SemiRing a => a -> a -> a
    `oplus` ((Matrix a
    aMatrix a -> (Int, Int) -> a
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    i,Int
    k)) a -> a -> a
    forall a. SemiRing a => a -> a -> a
    `otimes` (Matrix a
    aMatrix a -> (Int, Int) -> a
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    k,Int
    j))))
                            | Int
    i <- [Int
    r..Int
    r'], Int
    j <- [Int
    c..Int
    c'] ])
               | Bool
    otherwise = Matrix a
    a

    type AdjList node edge = Map node [(node, edge)]

    -- | Warshall's algorithm on a graph represented as an adjacency list.
    warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edge
    warshallG :: forall edge node.
    (SemiRing edge, Ord node) =>
    AdjList node edge -> AdjList node edge
    warshallG AdjList node edge
    g = Array (Int, Int) (Maybe edge) -> AdjList node edge
    fromMatrix (Array (Int, Int) (Maybe edge) -> AdjList node edge)
    -> Array (Int, Int) (Maybe edge) -> AdjList node edge
    forall a b. (a -> b) -> a -> b
    $ Array (Int, Int) (Maybe edge) -> Array (Int, Int) (Maybe edge)
    forall a. SemiRing a => Matrix a -> Matrix a
    warshall Array (Int, Int) (Maybe edge)
    m
      where
        nodes :: [(node, Int)]
    nodes = [node] -> [Int] -> [(node, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((node -> node) -> [node] -> [node]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn node -> node
    forall a. a -> a
    id ([node] -> [node]) -> [node] -> [node]
    forall a b. (a -> b) -> a -> b
    $ AdjList node edge -> [node]
    forall k a. Map k a -> [k]
    Map.keys AdjList node edge
    g [node] -> [node] -> [node]
    forall a. [a] -> [a] -> [a]
    ++ ((node, edge) -> node) -> [(node, edge)] -> [node]
    forall a b. (a -> b) -> [a] -> [b]
    map (node, edge) -> node
    forall a b. (a, b) -> a
    fst ([[(node, edge)]] -> [(node, edge)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[(node, edge)]] -> [(node, edge)])
    -> [[(node, edge)]] -> [(node, edge)]
    forall a b. (a -> b) -> a -> b
    $ AdjList node edge -> [[(node, edge)]]
    forall k a. Map k a -> [a]
    Map.elems AdjList node edge
    g))
                    [Int
    0..]
        len :: Int
    len   = [(node, Int)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(node, Int)]
    nodes
        b :: ((Int, Int), (Int, Int))
    b     = ((Int
    0,Int
    0), (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1,Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1))

        edge :: node -> node -> Maybe edge
    edge node
    i node
    j = do
          [(node, edge)]
    es <- node -> AdjList node edge -> Maybe [(node, edge)]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup node
    i AdjList node edge
    g
          (Maybe edge -> Maybe edge -> Maybe edge)
    -> Maybe edge -> [Maybe edge] -> Maybe edge
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Maybe edge -> Maybe edge -> Maybe edge
    forall a. SemiRing a => a -> a -> a
    oplus Maybe edge
    forall a. Maybe a
    Nothing [ edge -> Maybe edge
    forall a. a -> Maybe a
    Just edge
    v | (node
    j', edge
    v) <- [(node, edge)]
    es, node
    j node -> node -> Bool
    forall a. Eq a => a -> a -> Bool
    == node
    j' ]

        m :: Array (Int, Int) (Maybe edge)
    m = ((Int, Int), (Int, Int))
    -> [((Int, Int), Maybe edge)] -> Array (Int, Int) (Maybe edge)
    forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
    array ((Int, Int), (Int, Int))
    b [ ((Int
    n, Int
    m), node -> node -> Maybe edge
    edge node
    i node
    j) | (node
    i, Int
    n) <- [(node, Int)]
    nodes, (node
    j, Int
    m) <- [(node, Int)]
    nodes ]

        fromMatrix :: Array (Int, Int) (Maybe edge) -> AdjList node edge
    fromMatrix Array (Int, Int) (Maybe edge)
    matrix = ([(node, edge)] -> [(node, edge)] -> [(node, edge)])
    -> [(node, [(node, edge)])] -> AdjList node edge
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith [(node, edge)] -> [(node, edge)] -> [(node, edge)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(node, [(node, edge)])] -> AdjList node edge)
    -> [(node, [(node, edge)])] -> AdjList node edge
    forall a b. (a -> b) -> a -> b
    $ do
          (node
    i, Int
    n) <- [(node, Int)]
    nodes
          let es :: [(node, edge)]
    es = [ ((node, Int) -> node
    forall a b. (a, b) -> a
    fst ([(node, Int)]
    nodes [(node, Int)] -> Int -> (node, Int)
    forall a. [a] -> Int -> a
    !! Int
    m), edge
    e)
                   | Int
    m <- [Int
    0..Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
                   , Just edge
    e <- [Array (Int, Int) (Maybe edge)
    matrix Array (Int, Int) (Maybe edge) -> (Int, Int) -> Maybe edge
    forall i e. Ix i => Array i e -> i -> e
    ! (Int
    n, Int
    m)]
                   ]
          (node, [(node, edge)]) -> [(node, [(node, edge)])]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (node
    i, [(node, edge)]
    es)

    -- | Edge weight in the graph, forming a semi ring.
    data Weight
      = Finite Int
      | Infinite
      deriving (Weight -> Weight -> Bool
    (Weight -> Weight -> Bool)
    -> (Weight -> Weight -> Bool) -> Eq Weight
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Weight -> Weight -> Bool
    $c/= :: Weight -> Weight -> Bool
    == :: Weight -> Weight -> Bool
    $c== :: Weight -> Weight -> Bool
    Eq, Int -> Weight -> ShowS
    [Weight] -> ShowS
    Weight -> String
    (Int -> Weight -> ShowS)
    -> (Weight -> String) -> ([Weight] -> ShowS) -> Show Weight
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Weight] -> ShowS
    $cshowList :: [Weight] -> ShowS
    show :: Weight -> String
    $cshow :: Weight -> String
    showsPrec :: Int -> Weight -> ShowS
    $cshowsPrec :: Int -> Weight -> ShowS
    Show)

    inc :: Weight -> Int -> Weight
    inc :: Weight -> Int -> Weight
    inc Weight
    Infinite   Int
    n = Weight
    Infinite
    inc (Finite Int
    k) Int
    n = Int -> Weight
    Finite (Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n)

    instance Pretty Weight where
      pretty :: Weight -> Doc
    pretty (Finite Int
    i) = Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i
      pretty Weight
    Infinite   = Doc
    "."

    instance Ord Weight where
      Weight
    a <= :: Weight -> Weight -> Bool
    <= Weight
    Infinite = Bool
    True
      Weight
    Infinite <= Weight
    b = Bool
    False
      Finite Int
    a <= Finite Int
    b = Int
    a Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    b

    instance SemiRing Weight where
      ozero :: Weight
    ozero = Weight
    Infinite
      oone :: Weight
    oone  = Int -> Weight
    Finite Int
    0

      oplus :: Weight -> Weight -> Weight
    oplus = Weight -> Weight -> Weight
    forall a. Ord a => a -> a -> a
    min

      otimes :: Weight -> Weight -> Weight
    otimes Weight
    Infinite Weight
    _ = Weight
    Infinite
      otimes Weight
    _ Weight
    Infinite = Weight
    Infinite
      otimes (Finite Int
    a) (Finite Int
    b) = Int -> Weight
    Finite (Int
    a Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    b)

    -- constraints ---------------------------------------------------

    -- | Nodes of the graph are either
    -- - flexible variables (with identifiers drawn from @Int@),
    -- - rigid variables (also identified by @Int@s), or
    -- - constants (like 0, infinity, or anything between).

    data Node = Rigid Rigid
              | Flex  FlexId
                deriving (Node -> Node -> Bool
    (Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Node -> Node -> Bool
    $c/= :: Node -> Node -> Bool
    == :: Node -> Node -> Bool
    $c== :: Node -> Node -> Bool
    Eq, Eq Node
    Eq Node
    -> (Node -> Node -> Ordering)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Node)
    -> (Node -> Node -> Node)
    -> Ord Node
    Node -> Node -> Bool
    Node -> Node -> Ordering
    Node -> Node -> Node
    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
    min :: Node -> Node -> Node
    $cmin :: Node -> Node -> Node
    max :: Node -> Node -> Node
    $cmax :: Node -> Node -> Node
    >= :: Node -> Node -> Bool
    $c>= :: Node -> Node -> Bool
    > :: Node -> Node -> Bool
    $c> :: Node -> Node -> Bool
    <= :: Node -> Node -> Bool
    $c<= :: Node -> Node -> Bool
    < :: Node -> Node -> Bool
    $c< :: Node -> Node -> Bool
    compare :: Node -> Node -> Ordering
    $ccompare :: Node -> Node -> Ordering
    Ord)

    data Rigid = RConst Weight
               | RVar RigidId
                 deriving (Rigid -> Rigid -> Bool
    (Rigid -> Rigid -> Bool) -> (Rigid -> Rigid -> Bool) -> Eq Rigid
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Rigid -> Rigid -> Bool
    $c/= :: Rigid -> Rigid -> Bool
    == :: Rigid -> Rigid -> Bool
    $c== :: Rigid -> Rigid -> Bool
    Eq, Eq Rigid
    Eq Rigid
    -> (Rigid -> Rigid -> Ordering)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Rigid)
    -> (Rigid -> Rigid -> Rigid)
    -> Ord Rigid
    Rigid -> Rigid -> Bool
    Rigid -> Rigid -> Ordering
    Rigid -> Rigid -> Rigid
    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
    min :: Rigid -> Rigid -> Rigid
    $cmin :: Rigid -> Rigid -> Rigid
    max :: Rigid -> Rigid -> Rigid
    $cmax :: Rigid -> Rigid -> Rigid
    >= :: Rigid -> Rigid -> Bool
    $c>= :: Rigid -> Rigid -> Bool
    > :: Rigid -> Rigid -> Bool
    $c> :: Rigid -> Rigid -> Bool
    <= :: Rigid -> Rigid -> Bool
    $c<= :: Rigid -> Rigid -> Bool
    < :: Rigid -> Rigid -> Bool
    $c< :: Rigid -> Rigid -> Bool
    compare :: Rigid -> Rigid -> Ordering
    $ccompare :: Rigid -> Rigid -> Ordering
    Ord)

    type NodeId  = Int
    type RigidId = Int
    type FlexId  = Int
    type Scope   = RigidId -> Bool
    -- ^ Which rigid variables a flex may be instatiated to.

    instance Pretty Node where
      pretty :: Node -> Doc
    pretty (Flex  Int
    i)                   = Doc
    "?" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i
      pretty (Rigid (RVar Int
    i))            = Doc
    "v" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i
      pretty (Rigid (RConst Weight
    Infinite))   = Doc
    "#"
      pretty (Rigid (RConst (Finite Int
    n))) = Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    n

    infinite :: Rigid -> Bool
    infinite :: Rigid -> Bool
    infinite (RConst Weight
    Infinite) = Bool
    True
    infinite Rigid
    _                 = Bool
    False

    -- | @isBelow r w r'@
    --   checks, if @r@ and @r'@ are connected by @w@ (meaning @w@ not infinite),
    --   whether @r + w <= r'@.
    --   Precondition: not the same rigid variable.
    isBelow :: Rigid -> Weight -> Rigid -> Bool
    isBelow :: Rigid -> Weight -> Rigid -> Bool
    isBelow Rigid
    _ Weight
    Infinite Rigid
    _ = Bool
    True
    isBelow Rigid
    _ Weight
    n (RConst Weight
    Infinite) = Bool
    True
    isBelow (RConst (Finite Int
    i)) (Finite Int
    n) (RConst (Finite Int
    j)) = Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    j
    isBelow Rigid
    _ Weight
    _ Rigid
    _ = Bool
    False -- rigid variables are not related

    -- | A constraint is an edge in the graph.
    data Constraint
      = NewFlex FlexId Scope
      | Arc Node Int Node
        -- ^ For @Arc v1 k v2@  at least one of @v1@ or @v2@ is a @MetaV@ (Flex),
        --                      the other a @MetaV@ or a @Var@ (Rigid).
        --   If @k <= 0@ this means  @suc^(-k) v1 <= v2@
        --   otherwise               @v1 <= suc^k v3@.

    instance Pretty Constraint where
      pretty :: Constraint -> Doc
    pretty (NewFlex Int
    i Int -> Bool
    s) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Doc
    "SizeMeta(?", Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    i, Doc
    ")" ]
      pretty (Arc Node
    v1 Int
    k Node
    v2)
        | Int
    k Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0    = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty Node
    v1, Doc
    "<=", Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty Node
    v2 ]
        | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0     = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty Node
    v1, Doc
    "+", Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty (-Int
    k), Doc
    "<=", Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty Node
    v2 ]
        | Bool
    otherwise = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat [ Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty Node
    v1, Doc
    "<=", Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty Node
    v2, Doc
    "+", Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    k ]

    type Constraints = [Constraint]

    emptyConstraints :: Constraints
    emptyConstraints :: [Constraint]
    emptyConstraints = []

    -- graph (matrix) ------------------------------------------------

    data Graph = Graph
      { Graph -> Map Int (Int -> Bool)
    flexScope :: Map FlexId Scope           -- ^ Scope for each flexible var.
      , Graph -> Map Node Int
    nodeMap   :: Map Node NodeId            -- ^ Node labels to node numbers.
      , Graph -> Map Int Node
    intMap    :: Map NodeId Node            -- ^ Node numbers to node labels.
      , Graph -> Int
    nextNode  :: NodeId                     -- ^ Number of nodes @n@.
      , Graph -> Int -> Int -> Weight
    graph     :: NodeId -> NodeId -> Weight -- ^ The edges (restrict to @[0..n[@).
      }

    -- | The empty graph: no nodes, edges are all undefined (infinity weight).
    initGraph :: Graph
    initGraph :: Graph
    initGraph = Map Int (Int -> Bool)
    -> Map Node Int
    -> Map Int Node
    -> Int
    -> (Int -> Int -> Weight)
    -> Graph
    Graph Map Int (Int -> Bool)
    forall k a. Map k a
    Map.empty Map Node Int
    forall k a. Map k a
    Map.empty Map Int Node
    forall k a. Map k a
    Map.empty Int
    0 (\ Int
    x Int
    y -> Weight
    Infinite)

    -- | The Graph Monad, for constructing a graph iteratively.
    type GM = State Graph

    -- | Add a size meta node.
    addFlex :: FlexId -> Scope -> GM ()
    addFlex :: Int -> (Int -> Bool) -> GM ()
    addFlex Int
    x Int -> Bool
    scope = do
      (Graph -> Graph) -> GM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Graph -> Graph) -> GM ()) -> (Graph -> Graph) -> GM ()
    forall a b. (a -> b) -> a -> b
    $ \ Graph
    st -> Graph
    st { flexScope :: Map Int (Int -> Bool)
    flexScope = Int
    -> (Int -> Bool) -> Map Int (Int -> Bool) -> Map Int (Int -> Bool)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Int
    x Int -> Bool
    scope (Graph -> Map Int (Int -> Bool)
    flexScope Graph
    st) }
      Int
    _ <- Node -> GM Int
    addNode (Int -> Node
    Flex Int
    x)
      () -> GM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Lookup identifier of a node.
    --   If not present, it is added first.
    addNode :: Node -> GM Int
    addNode :: Node -> GM Int
    addNode Node
    n = do
      Graph
    st <- StateT Graph Identity Graph
    forall s (m :: * -> *). MonadState s m => m s
    get
      case Node -> Map Node Int -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Node
    n (Graph -> Map Node Int
    nodeMap Graph
    st) of
        Just Int
    i -> Int -> GM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i
        Maybe Int
    Nothing -> do
          let i :: Int
    i = Graph -> Int
    nextNode Graph
    st
          Graph -> GM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Graph -> GM ()) -> Graph -> GM ()
    forall a b. (a -> b) -> a -> b
    $ Graph
    st { nodeMap :: Map Node Int
    nodeMap  = Node -> Int -> Map Node Int -> Map Node Int
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Node
    n Int
    i (Graph -> Map Node Int
    nodeMap Graph
    st)
                   , intMap :: Map Int Node
    intMap   = Int -> Node -> Map Int Node -> Map Int Node
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Int
    i Node
    n (Graph -> Map Int Node
    intMap Graph
    st)
                   , nextNode :: Int
    nextNode = Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1
                   }
          Int -> GM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i

    -- | @addEdge n1 k n2@
    --   improves the weight of egde @n1->n2@ to be at most @k@.
    --   Also adds nodes if not yet present.
    addEdge :: Node -> Int -> Node -> GM ()
    addEdge :: Node -> Int -> Node -> GM ()
    addEdge Node
    n1 Int
    k Node
    n2 = do
      Int
    i1 <- Node -> GM Int
    addNode Node
    n1
      Int
    i2 <- Node -> GM Int
    addNode Node
    n2
      Graph
    st <- StateT Graph Identity Graph
    forall s (m :: * -> *). MonadState s m => m s
    get
      let graph' :: Int -> Int -> Weight
    graph' Int
    x Int
    y = if (Int
    x,Int
    y) (Int, Int) -> (Int, Int) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Int
    i1,Int
    i2) then Int -> Weight
    Finite Int
    k Weight -> Weight -> Weight
    forall a. SemiRing a => a -> a -> a
    `oplus` Graph -> Int -> Int -> Weight
    graph Graph
    st Int
    x Int
    y
                       else Graph -> Int -> Int -> Weight
    graph Graph
    st Int
    x Int
    y
      Graph -> GM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Graph -> GM ()) -> Graph -> GM ()
    forall a b. (a -> b) -> a -> b
    $ Graph
    st { graph :: Int -> Int -> Weight
    graph = Int -> Int -> Weight
    graph' }

    addConstraint :: Constraint -> GM ()
    addConstraint :: Constraint -> GM ()
    addConstraint (NewFlex Int
    x Int -> Bool
    scope) = Int -> (Int -> Bool) -> GM ()
    addFlex Int
    x Int -> Bool
    scope
    addConstraint (Arc Node
    n1 Int
    k Node
    n2)     = Node -> Int -> Node -> GM ()
    addEdge Node
    n1 Int
    k Node
    n2

    buildGraph :: Constraints -> Graph
    buildGraph :: [Constraint] -> Graph
    buildGraph [Constraint]
    cs = GM () -> Graph -> Graph
    forall s a. State s a -> s -> s
    execState ((Constraint -> GM ()) -> [Constraint] -> GM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Constraint -> GM ()
    addConstraint [Constraint]
    cs) Graph
    initGraph

    mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight
    mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight
    mkMatrix Int
    n Int -> Int -> Weight
    g = ((Int, Int), (Int, Int)) -> [((Int, Int), Weight)] -> Matrix Weight
    forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
    array ((Int
    0,Int
    0),(Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1,Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))
                     [ ((Int
    i,Int
    j), Int -> Int -> Weight
    g Int
    i Int
    j) | Int
    i <- [Int
    0..Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1], Int
    j <- [Int
    0..Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1]]

    -- displaying matrices with row and column labels --------------------

    -- | A matrix with row descriptions in @b@ and column descriptions in @c@.
    data LegendMatrix a b c = LegendMatrix
      { forall a b c. LegendMatrix a b c -> Matrix a
    matrix   :: Matrix a
      , forall a b c. LegendMatrix a b c -> Int -> b
    rowdescr :: Int -> b
      , forall a b c. LegendMatrix a b c -> Int -> c
    coldescr :: Int -> c
      }

    instance (Pretty a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) where
      pretty :: LegendMatrix a b c -> Doc
    pretty (LegendMatrix Matrix a
    m Int -> b
    rd Int -> c
    cd) =
        -- first show column description
        let ((Int
    r,Int
    c),(Int
    r',Int
    c')) = Matrix a -> ((Int, Int), (Int, Int))
    forall i e. Array i e -> (i, i)
    bounds Matrix a
    m
        in (Int -> Doc -> Doc) -> Doc -> [Int] -> Doc
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ Int
    j Doc
    s -> Doc
    "\t" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> c -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Int -> c
    cd Int
    j) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    s) Doc
    "" [Int
    c .. Int
    c'] Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<>
        -- then output rows
           (Int -> Doc -> Doc) -> Doc -> [Int] -> Doc
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ Int
    i Doc
    s -> Doc
    "\n" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Int -> b
    rd Int
    i) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<>
                    (Int -> Doc -> Doc) -> Doc -> [Int] -> Doc
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ Int
    j Doc
    t -> Doc
    "\t" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Matrix a
    mMatrix a -> (Int, Int) -> a
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    i,Int
    j)) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    t)
                          Doc
    s
                          [Int
    c .. Int
    c'])
                 Doc
    "" [Int
    r .. Int
    r']

    -- solving the constraints -------------------------------------------

    -- | A solution assigns to each flexible variable a size expression
    --   which is either a constant or a @v + n@ for a rigid variable @v@.
    type Solution = Map Int SizeExpr

    emptySolution :: Solution
    emptySolution :: Solution
    emptySolution = Solution
    forall k a. Map k a
    Map.empty

    extendSolution :: Solution -> Int -> SizeExpr -> Solution
    extendSolution :: Solution -> Int -> SizeExpr -> Solution
    extendSolution Solution
    subst Int
    k SizeExpr
    v = Int -> SizeExpr -> Solution -> Solution
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Int
    k SizeExpr
    v Solution
    subst

    data SizeExpr = SizeVar RigidId Int   -- ^ e.g. x + 5
                  | SizeConst Weight      -- ^ a number or infinity

    instance Pretty SizeExpr where
      pretty :: SizeExpr -> Doc
    pretty (SizeVar Int
    n Int
    0) = Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Rigid -> Node
    Rigid (Int -> Rigid
    RVar Int
    n))
      pretty (SizeVar Int
    n Int
    k) = Node -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Rigid -> Node
    Rigid (Int -> Rigid
    RVar Int
    n)) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    "+" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    k
      pretty (SizeConst Weight
    w) = Weight -> Doc
    forall a. Pretty a => a -> Doc
    pretty Weight
    w

    -- | @sizeRigid r n@ returns the size expression corresponding to @r + n@
    sizeRigid :: Rigid -> Int -> SizeExpr
    sizeRigid :: Rigid -> Int -> SizeExpr
    sizeRigid (RConst Weight
    k) Int
    n = Weight -> SizeExpr
    SizeConst (Weight -> Int -> Weight
    inc Weight
    k Int
    n)
    sizeRigid (RVar Int
    i)   Int
    n = Int -> Int -> SizeExpr
    SizeVar Int
    i Int
    n

    {-
    apply :: SizeExpr -> Solution -> SizeExpr
    apply e@(SizeExpr (Rigid _) _) phi = e
    apply e@(SizeExpr (Flex  x) i) phi = case Map.lookup x phi of
      Nothing -> e
      Just (SizeExpr v j) -> SizeExpr v (i + j)

    after :: Solution -> Solution -> Solution
    after psi phi = Map.map (\ e -> e `apply` phi) psi
    -}

    {- compute solution

    a solution CANNOT exist if

      v < v  for a rigid variable v

      -- Andreas, 2012-09-19 OUTDATED are:

      -- v <= v' for rigid variables v,v'

      -- x < v   for a flexible variable x and a rigid variable v

    thus, for each flexible x, only one of the following cases is possible

      r+n <= x+m <= infty  for a unique rigid r  (meaning r --(m-n)--> x)
      x <= r+n             for a unique rigid r  (meaning x --(n)--> r)

    we are looking for the least values for flexible variables that solve
    the constraints.  Algorithm

    while flexible variables and rigid rows left
      find a rigid variable row i
        for all flexible columns j
          if i --n--> j with n<=0 (meaning i+n <= j) then j = i + n

    while flexible variables j left
      search the row j for entry i
        if j --n--> i with n >= 0 (meaning j <= i + n) then j = i + n

    -}

    solve :: Constraints -> Maybe Solution
    solve :: [Constraint] -> Maybe Solution
    solve [Constraint]
    cs = -- trace (prettyShow cs) $
       -- trace (prettyShow lm0) $
        -- trace (prettyShow lm) $ -- trace (prettyShow d) $
         let solution :: Maybe Solution
    solution = if Bool
    solvable then [Int] -> [Rigid] -> Solution -> Maybe Solution
    loop1 [Int]
    flexs [Rigid]
    rigids Solution
    emptySolution
                        else Maybe Solution
    forall a. Maybe a
    Nothing
         in -- trace (prettyShow solution) $
             Maybe Solution
    solution
       where -- compute the graph and its transitive closure m
             gr :: Graph
    gr  = [Constraint] -> Graph
    buildGraph [Constraint]
    cs
             n :: Int
    n   = Graph -> Int
    nextNode Graph
    gr            -- number of nodes
             m0 :: Matrix Weight
    m0  = Int -> (Int -> Int -> Weight) -> Matrix Weight
    mkMatrix Int
    n (Graph -> Int -> Int -> Weight
    graph Graph
    gr)
             m :: Matrix Weight
    m   = Matrix Weight -> Matrix Weight
    forall a. SemiRing a => Matrix a -> Matrix a
    warshall Matrix Weight
    m0

             -- tracing only: build output version of transitive graph
             legend :: Int -> Node
    legend Int
    i = Maybe Node -> Node
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Node -> Node) -> Maybe Node -> Node
    forall a b. (a -> b) -> a -> b
    $ Int -> Map Int Node -> Maybe Node
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Int
    i (Graph -> Map Int Node
    intMap Graph
    gr) -- trace only
             lm0 :: LegendMatrix Weight Node Node
    lm0 = Matrix Weight
    -> (Int -> Node) -> (Int -> Node) -> LegendMatrix Weight Node Node
    forall a b c.
    Matrix a -> (Int -> b) -> (Int -> c) -> LegendMatrix a b c
    LegendMatrix Matrix Weight
    m0 Int -> Node
    legend Int -> Node
    legend            -- trace only
             lm :: LegendMatrix Weight Node Node
    lm  = Matrix Weight
    -> (Int -> Node) -> (Int -> Node) -> LegendMatrix Weight Node Node
    forall a b c.
    Matrix a -> (Int -> b) -> (Int -> c) -> LegendMatrix a b c
    LegendMatrix Matrix Weight
    m Int -> Node
    legend Int -> Node
    legend             -- trace only

             -- compute the sets of flexible and rigid node numbers
             ns :: [Node]
    ns  = Map Node Int -> [Node]
    forall k a. Map k a -> [k]
    Map.keys (Graph -> Map Node Int
    nodeMap Graph
    gr)
             -- a set of flexible variables
             flexs :: [Int]
    flexs  = ([Int] -> Node -> [Int]) -> [Int] -> [Node] -> [Int]
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' (\ [Int]
    l -> \case (Flex Int
    i ) -> Int
    i Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int]
    l
                                                (Rigid Rigid
    _) -> [Int]
    l)     [] [Node]
    ns
             -- a set of rigid variables
             rigids :: [Rigid]
    rigids = ([Rigid] -> Node -> [Rigid]) -> [Rigid] -> [Node] -> [Rigid]
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' (\ [Rigid]
    l -> \case (Flex Int
    _ ) -> [Rigid]
    l
                                                (Rigid Rigid
    i) -> Rigid
    i Rigid -> [Rigid] -> [Rigid]
    forall a. a -> [a] -> [a]
    : [Rigid]
    l) [] [Node]
    ns

             -- rigid matrix indices
             rInds :: [Int]
    rInds = ([Int] -> Rigid -> [Int]) -> [Int] -> [Rigid] -> [Int]
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' (\ [Int]
    l Rigid
    r -> let Just Int
    i = Node -> Map Node Int -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Rigid -> Node
    Rigid Rigid
    r) (Graph -> Map Node Int
    nodeMap Graph
    gr)
                                           in Int
    i Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int]
    l) [] [Rigid]
    rigids

             -- check whether there is a solution
             -- d   = [ m!(i,i) | i <- [0 .. (n-1)] ]  -- diagonal
    -- a rigid variable might not be less than it self, so no -.. on the
    -- rigid part of the diagonal
             solvable :: Bool
    solvable = (Weight -> Bool) -> [Weight] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (\ Weight
    x -> Weight
    x Weight -> Weight -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int -> Weight
    Finite Int
    0) [ Matrix Weight
    mMatrix Weight -> (Int, Int) -> Weight
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    i,Int
    i) | Int
    i <- [Int]
    rInds ] Bool -> Bool -> Bool
    && Bool
    True

    {-  Andreas, 2012-09-19
        We now can have constraints between rigid variables, like i < j.
        Thus we skip the following two test.  However, a solution must be
        checked for consistency with the constraints on rigid vars.

    -- a rigid variable might not be bounded below by infinity or
    -- bounded above by a constant
    -- it might not be related to another rigid variable
               all (\ (r,  r') -> r == r' ||
                    let Just row = (Map.lookup (Rigid r)  (nodeMap gr))
                        Just col = (Map.lookup (Rigid r') (nodeMap gr))
                        edge = m!(row,col)
                    in  isBelow r edge r' )
                 [ (r,r') | r <- rigids, r' <- rigids ]
               &&
    -- a flexible variable might not be strictly below a rigid variable
               all (\ (x, v) ->
                    let Just row = (Map.lookup (Flex x)  (nodeMap gr))
                        Just col = (Map.lookup (Rigid (RVar v)) (nodeMap gr))
                        edge = m!(row,col)
                    in  edge >= Finite 0)
                 [ (x,v) | x <- flexs, (RVar v) <- rigids ]
    -}

             inScope :: FlexId -> Rigid -> Bool
             inScope :: Int -> Rigid -> Bool
    inScope Int
    x (RConst Weight
    _) = Bool
    True
             inScope Int
    x (RVar Int
    v)   = Int -> Bool
    scope Int
    v
                 where Just Int -> Bool
    scope = Int -> Map Int (Int -> Bool) -> Maybe (Int -> Bool)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Int
    x (Graph -> Map Int (Int -> Bool)
    flexScope Graph
    gr)

    {- loop1

    while flexible variables and rigid rows left
      find a rigid variable row i
        for all flexible columns j
          if i --n--> j with n<=0 (meaning i + n <= j) then j = i + n

    -}
             loop1 :: [FlexId] -> [Rigid] -> Solution -> Maybe Solution
             loop1 :: [Int] -> [Rigid] -> Solution -> Maybe Solution
    loop1 [] [Rigid]
    rgds Solution
    subst = Solution -> Maybe Solution
    forall a. a -> Maybe a
    Just Solution
    subst
             loop1 [Int]
    flxs [] Solution
    subst = [Int] -> Solution -> Maybe Solution
    loop2 [Int]
    flxs Solution
    subst
             loop1 [Int]
    flxs (Rigid
    r:[Rigid]
    rgds) Solution
    subst =
                let row :: Int
    row = Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Node Int -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Rigid -> Node
    Rigid Rigid
    r) (Graph -> Map Node Int
    nodeMap Graph
    gr)
                    ([Int]
    flxs',Solution
    subst') =
                      (([Int], Solution) -> Int -> ([Int], Solution))
    -> ([Int], Solution) -> [Int] -> ([Int], Solution)
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' (\ ([Int]
    flx,Solution
    sub) Int
    f ->
                              let col :: Int
    col = Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Node Int -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Int -> Node
    Flex Int
    f) (Graph -> Map Node Int
    nodeMap Graph
    gr)
                              in  case (Int -> Rigid -> Bool
    inScope Int
    f Rigid
    r, Matrix Weight
    mMatrix Weight -> (Int, Int) -> Weight
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    row,Int
    col)) of
    --                                Finite z | z <= 0 ->
                                    (Bool
    True, Finite Int
    z) ->
                                       let trunc :: p -> p
    trunc p
    z | p
    z p -> p -> Bool
    forall a. Ord a => a -> a -> Bool
    >= p
    0 = p
    0
                                                | Bool
    otherwise = -p
    z
                                       in ([Int]
    flx, Solution -> Int -> SizeExpr -> Solution
    extendSolution Solution
    sub Int
    f (Rigid -> Int -> SizeExpr
    sizeRigid Rigid
    r (Int -> Int
    forall {p}. (Ord p, Num p) => p -> p
    trunc Int
    z)))
                                    (Bool, Weight)
    _ -> (Int
    f Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int]
    flx, Solution
    sub)
                         ) ([], Solution
    subst) [Int]
    flxs
                in [Int] -> [Rigid] -> Solution -> Maybe Solution
    loop1 [Int]
    flxs' [Rigid]
    rgds Solution
    subst'

    {- loop2

    while flexible variables j left
      search the row j for entry i
        if j --n--> i with n >= 0 (meaning j <= i + n) then j = i

    -}
             loop2 :: [FlexId] -> Solution -> Maybe Solution
             loop2 :: [Int] -> Solution -> Maybe Solution
    loop2 [] Solution
    subst = Solution -> Maybe Solution
    forall a. a -> Maybe a
    Just Solution
    subst
             loop2 (Int
    f:[Int]
    flxs) Solution
    subst = Int -> Solution -> Maybe Solution
    loop3 Int
    0 Solution
    subst
               where row :: Int
    row = Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Node -> Map Node Int -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (Int -> Node
    Flex Int
    f) (Graph -> Map Node Int
    nodeMap Graph
    gr)
                     loop3 :: Int -> Solution -> Maybe Solution
    loop3 Int
    col Solution
    subst | Int
    col Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n =
                       -- default to infinity
                        [Int] -> Solution -> Maybe Solution
    loop2 [Int]
    flxs (Solution -> Int -> SizeExpr -> Solution
    extendSolution Solution
    subst Int
    f (Weight -> SizeExpr
    SizeConst Weight
    Infinite))
                     loop3 Int
    col Solution
    subst =
                       case Int -> Map Int Node -> Maybe Node
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Int
    col (Graph -> Map Int Node
    intMap Graph
    gr) of
                         Just (Rigid Rigid
    r) | Bool -> Bool
    not (Rigid -> Bool
    infinite Rigid
    r) ->
                           case (Int -> Rigid -> Bool
    inScope Int
    f Rigid
    r, Matrix Weight
    mMatrix Weight -> (Int, Int) -> Weight
    forall i e. Ix i => Array i e -> i -> e
    !(Int
    row,Int
    col)) of
                            (Bool
    True, Finite Int
    z) | Int
    z Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0 ->
                                [Int] -> Solution -> Maybe Solution
    loop2 [Int]
    flxs (Solution -> Int -> SizeExpr -> Solution
    extendSolution Solution
    subst Int
    f (Rigid -> Int -> SizeExpr
    sizeRigid Rigid
    r Int
    z))
                            (Bool
    _, Weight
    Infinite) -> Int -> Solution -> Maybe Solution
    loop3 (Int
    colInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Solution
    subst
                            (Bool, Weight)
    _ -> -- trace ("unusable rigid: " ++ prettyShow r ++ " for flex " ++ prettyShow f)
                                  Maybe Solution
    forall a. Maybe a
    Nothing  -- NOT: loop3 (col+1) subst
                         Maybe Node
    _ -> Int -> Solution -> Maybe Solution
    loop3 (Int
    colInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Solution
    subst