Module Generic_view.Spine

module Spine: Generic_view_spine

We call left spine the path from the root of a tree to its leftmost leaf. The spine generic view represent the possibly partial spine of a tree whose node are applications, and whose root is a data constructor.

The type is a GADT. The constructor App uses an existential quantification for the type of the argument. The representation of the argument type is useful when defining generic computations over a spine.

module T: sig .. end

type 'a t = 'a T.spine

A spine view converts a constructor value c(v0,...vn) to the form App (....(App (c', t0, v0)..., tn, vn) where tk is the representation of vk's type. and c' = Con (c\_desc, fun x0 ... xn -> c(x0,...,xn).

In essence, the spine view of a value gives a data constructor and a list of all its arguments together with their types.

<<spine view constructors for int lists>>= let nil = Con (nild, []) and cons ty hd tl = App (App (Con (cons_desc, fun x y -> x :: y), ty, hd) , List ty, tl) @

val spine : 'a Ty.T.ty -> 'a -> 'a T.spine

val view : 'a Ty.T.ty -> 'a -> 'a T.spine

view = spine

val rebuild : 'a T.spine -> 'a

Builds back a value from it's spine view.