Inferno.Decoder
This module offers performs decoding, which is the task of traversing the data structure maintained by the unifier and transforming it into a data representation selected by the user (typically, some form of tree). It is parameterized by the term structure S
, by the unifier U
, and by the data representation O
. Read-only access to the unifier's data structure suffices. Two decoding algorithms are proposed: the acyclic decoder does not tolerate cycles, and produces ordinary trees; whereas the cyclic decoder can deal with cycles, and produces trees that contain μ binders.