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.
module S : sig ... endmodule U : sig ... endmodule O : sig ... endval decode_variable : U.variable -> O.tyvardecode_variable v decodes the variable v.
val new_acyclic_decoder : unit -> U.variable -> O.tynew_acyclic_decoder() initiates a new decoding phase. It returns a decoding function decode, which can be used as many as times as one wishes. Decoding requires the graph to be acyclic: it is a bottom-up computation. decode internally performs memoization, so even if the decoder is called many times, the total cost of decoding is linear in the size of the graph fragment that is decoded.
As a caveat that one must bear in mind, when the type ty of decoded types is a type of abstract syntax trees, then the decoder actually produces a DAG of type ty. Traversing this DAG in a naive way, without paying attention to the fact that some subtrees may be shared, can result in a traversal whose complexity is exponential.
val new_cyclic_decoder : unit -> U.variable -> O.tynew_cyclic_decoder is analogous to new_acyclic_decoder, but tolerates cyclic graphs. The decoder detects cycles and uses the function mu to decode them into equirecursive types. The decoder performs memoization only at the vertices that do not participate in a cycle. This makes the complexity of decoding higher than the acyclic case, but we expect it to remain linear in practice.