Commit 9c3d8921 authored by POTTIER Francois's avatar POTTIER Francois

Comments.

parent 4112b064
......@@ -2,35 +2,22 @@ type void
(* -------------------------------------------------------------------------- *)
(* A universal, concrete type of single-name abstractions. *)
(* We wish to represent all kinds of abstractions -- e.g. in nominal style,
in de Bruijn style, etc. -- so we parameterize the abstraction over the
type ['bn] of the bound name and over the type ['term] of the body. This
makes this type definition almost trivial -- it is just a pair -- but it
still serves as a syntactic marker of where abstractions are located. *)
type ('bn, 'term) abs =
'bn * 'term
(* -------------------------------------------------------------------------- *)
(* The main effect of an abstraction is to cause the environment to be
enriched when the abstraction is traversed. The following classes define
where the environment is enriched. *)
(* The main effect of a binding construct is to cause the environment to be
enriched when the abstraction is traversed. The following visitor methods
define where the environment is enriched. *)
(* These classes do not know the type of the environment, and do not know how
(* These methods do not know the type of the environment, and do not know how
it is enriched or looked up; the latter task is delegated to the virtual
methods [extend] and [lookup]. The implementation of these methods is
provided by separate ``kits''. *)
(* We need several varieties of visitor, which is a bit painful. As of now,
(* We need several varieties of visitors, which is a bit painful. As of now,
[iter], [map], [endo], [iter2] are required: see [ToolboxInput]. *)
(* The method [visit_abs] is polymorphic in the type of terms. This is
important, as it means that one can use several instances of [abs] in a
single type definition and still be able to construct well-typed
visitors. *)
(* The visitor methods are polymorphic in the type of terms. This is
important, as it means that one can use several instances of a binding
construct in a single type definition and still be able to construct
well-typed visitors. *)
(* The virtual methods [extend] and [lookup] are not polymorphic in the types
of bound names and environments. On the contrary, each kit comes with
......@@ -38,6 +25,19 @@ type ('bn, 'term) abs =
(* -------------------------------------------------------------------------- *)
(* A universal, concrete type of single-name abstractions. *)
(* We wish to represent all kinds of abstractions -- e.g. in nominal style,
in de Bruijn style, etc. -- so we parameterize the abstraction over the
type ['bn] of the bound name and over the type ['term] of the body. This
makes this type definition almost trivial -- it is just a pair -- but it
still serves as a syntactic marker of where abstractions are located. *)
type ('bn, 'term) abs =
'bn * 'term
(* -------------------------------------------------------------------------- *)
(* [iter] *)
class virtual ['self] iter = object (self : 'self)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment