HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Warshall

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.

  • 16 types
  • 17 values
  • PackageAgda-2.7.0.1
  • Exports33
  • LanguageHaskell2010
  • LicenceMIT
  • SourceWarshall.hs
typetype AdjList node edge = Map node [(node, edge)]
#
datadata Weight
#

Edge weight in the graph, forming a semi ring.

Constructors

Instances5Eq, Ord, Show, Pretty, SemiRing
  • Eq WeightDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
  • Ord WeightDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
  • Show WeightDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
  • Pretty WeightDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
  • SemiRing WeightDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
datadata Node
#

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

Constructors

Instances3Eq, Ord, Pretty
  • Eq NodeDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
  • Ord NodeDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
  • Pretty NodeDefined in Agda-2.7.0.1 · Agda.Utils.Warshall
typetype Scope = RigidId -> Bool
#

Which rigid variables a flex may be instatiated to.

valueisBelow :: Rigid -> Weight -> Rigid -> Bool
#

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.

datadata Constraint
#

A constraint is an edge in the graph.

Constructors

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

Instances1Pretty
valueinitGraph :: Graph
#

The empty graph: no nodes, edges are all undefined (infinity weight).

typetype GM = State Graph
#

The Graph Monad, for constructing a graph iteratively.

valueaddNode :: Node -> GM Int
#

Lookup identifier of a node. If not present, it is added first.

valueaddEdge :: Node -> Int -> Node -> GM ()
#

addEdge n1 k n2 improves the weight of egde n1->n2 to be at most k. Also adds nodes if not yet present.

typetype Solution = Map Int SizeExpr
#

A solution assigns to each flexible variable a size expression which is either a constant or a v + n for a rigid variable v.