Module Inferno.Decoder

module Make (S : sig ... end) (U : sig ... end) (O : sig ... end) : sig ... end

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.