Decoder: fix and improve the documentation comment.
This commit is contained in:
parent
331fa6bc7d
commit
a709fca0b5
|
@ -11,15 +11,23 @@
|
|||
|
||||
open Signatures
|
||||
|
||||
(**This module offers performs decoding, which is the task of traversing the
|
||||
data structure maintained by the unifier and transforming it into a data
|
||||
(**This module 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 {i acyclic decoder}
|
||||
does not tolerate cycles, and produces ordinary trees; whereas the {i
|
||||
cyclic decoder} can deal with cycles, and produces trees that contain μ
|
||||
binders. *)
|
||||
suffices.
|
||||
|
||||
Two decoding algorithms are proposed: the {i acyclic decoder} does not
|
||||
tolerate cycles, and produces ordinary trees; whereas the {i cyclic
|
||||
decoder} can deal with cycles, and produces trees that contain μ
|
||||
binders.
|
||||
|
||||
The cyclic decoder can produce μ binders and μ-bound type variables.
|
||||
Neither decoder has specific support for printing ordinary (∀-bound)
|
||||
type variables. In the eyes of the decoders, a type variable is just
|
||||
a vertex that has no structure; it is up to the user-supplied function
|
||||
[O.structure] to determine how such a vertex must be printed. *)
|
||||
module Make
|
||||
(S : sig (** @inline *) include OSTRUCTURE end)
|
||||
(U : sig (** @inline *) include MUNIFIER
|
||||
|
|
Loading…
Reference in New Issue