package lrgrep
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=84a1874d0c063da371e19c84243aac7c40bfcb9aaf204251e0eb0d1f077f2cde
sha512=5a16ff42a196fd741bc64a1bdd45b4dca0098633e73aa665829a44625ec15382891c3643fa210dbe3704336eab095d4024e093e37ae5313810f6754de6119d55
doc/utils/Utils/Order_chain/index.html
Module Utils.Order_chainSource
An order chain is a data structure designed to incrementally construct a totally ordered set represented as an interval 0,n[. The order is progressively refined by accumulating constraints: - starting with a single element, - getting an element strictly larger than an existing one, - getting an element strictly larger than an existing one and strictly smaller than all existing elements that are larger. This data structure is used by the dynamic priority optimizations of LRGrep automata.
Abstract type of an order chain
An element of an order chain
next e returns an element larger than e in the order chain. No new element is created if there already are larger ones.
extend e generates an element that is larger than e but strictly smaller than all elements in the chain that are larger than e.
freeze t finalizes the order chain t and returns the cardinal of the set. It should be called after all necessary constraints have been accumulated. It can be called only once, and the chain cannot be extended after.