Commit f1d7e3a4 authored by POTTIER Francois's avatar POTTIER Francois

Name the functor input signature.

parent 2f81fc68
(* This functor is applied to a type of terms, equipped with visitor classes.
It produces a toolbox of useful functions that operate on terms. *)
module Make (Term : sig
(* Suppose there is a type of terms, which is parameterized over the
representations of free name occurrences and binding name occurrences. *)
type ('fn, 'bn) term
(* Suppose the type of terms is equipped with the following visitors. *)
(* The private virtual method [visit_'fn] is used to specify what should
be done at free name occurrences. The private virtual method [extend]
is used to indicate how the environment should be extended when an
abstraction is entered. In the [reduce] visitor, the private methods
[zero] and [plus] are used to specify how summaries should be computed,
while the private method [restrict] is used to specify how a summary
should be restricted when an abstraction is exited. *)
(* Suppose the data constructor for variables is named [TVar], so that
the method [visit_TVar] is used to specify what behavior at variables
is desired. *)
class virtual ['self] iter : object ('self)
method private virtual extend : 'bn -> 'env -> 'env
method private virtual visit_'fn : 'env -> 'fn -> _
method visit_term : 'env -> ('fn, 'bn) term -> unit
end
class virtual ['self] map : object ('self)
method private virtual extend : 'bn1 -> 'env -> 'bn2 * 'env
method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2
method visit_term : 'env -> ('fn1, 'bn1) term -> ('fn2, 'bn2) term
method private visit_TVar : 'env -> 'fn1 -> ('fn2, 'bn2) term
end
class virtual ['self] endo : object ('self)
method private virtual extend : 'bn -> 'env -> 'bn * 'env
method private virtual visit_'fn : 'env -> 'fn -> 'fn
method visit_term : 'env -> ('fn, 'bn) term -> ('fn, 'bn) term
method private visit_TVar : 'env -> ('fn, 'bn) term -> 'fn -> ('fn, 'bn) term
end
class virtual ['self] reduce : object ('self)
method private virtual extend : 'bn -> 'env -> 'env
method private virtual visit_'fn : 'env -> 'fn -> 'z
method private virtual zero : 'z
method private virtual plus : 'z -> 'z -> 'z
method private virtual restrict : 'bn -> 'z -> 'z
method visit_term : 'env -> ('fn, 'bn) term -> 'z
end
class virtual ['self] iter2 : object ('self)
method private virtual extend : 'bn1 -> 'bn2 -> 'env -> 'env
method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2 -> _
method visit_term : 'env -> ('fn1, 'bn1) term -> ('fn2, 'bn2) term -> unit
end
end) = struct
module Make (Term : ToolboxInput.INPUT) = struct
open Term
......
module type INPUT = sig
(* Suppose there is a type of terms, which is parameterized over the
representations of free name occurrences and binding name occurrences. *)
type ('fn, 'bn) term
(* Suppose the type of terms is equipped with the following visitors. *)
(* The private virtual method [visit_'fn] is used to specify what should
be done at free name occurrences. The private virtual method [extend]
is used to indicate how the environment should be extended when an
abstraction is entered. In the [reduce] visitor, the private methods
[zero] and [plus] are used to specify how summaries should be computed,
while the private method [restrict] is used to specify how a summary
should be restricted when an abstraction is exited. *)
(* Suppose the data constructor for variables is named [TVar], so that
the method [visit_TVar] is used to specify what behavior at variables
is desired. *)
class virtual ['self] iter : object ('self)
method private virtual extend : 'bn -> 'env -> 'env
method private virtual visit_'fn : 'env -> 'fn -> _
method visit_term : 'env -> ('fn, 'bn) term -> unit
end
class virtual ['self] map : object ('self)
method private virtual extend : 'bn1 -> 'env -> 'bn2 * 'env
method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2
method visit_term : 'env -> ('fn1, 'bn1) term -> ('fn2, 'bn2) term
method private visit_TVar : 'env -> 'fn1 -> ('fn2, 'bn2) term
end
class virtual ['self] endo : object ('self)
method private virtual extend : 'bn -> 'env -> 'bn * 'env
method private virtual visit_'fn : 'env -> 'fn -> 'fn
method visit_term : 'env -> ('fn, 'bn) term -> ('fn, 'bn) term
method private visit_TVar : 'env -> ('fn, 'bn) term -> 'fn -> ('fn, 'bn) term
end
class virtual ['self] reduce : object ('self)
method private virtual extend : 'bn -> 'env -> 'env
method private virtual visit_'fn : 'env -> 'fn -> 'z
method private virtual zero : 'z
method private virtual plus : 'z -> 'z -> 'z
method private virtual restrict : 'bn -> 'z -> 'z
method visit_term : 'env -> ('fn, 'bn) term -> 'z
end
class virtual ['self] iter2 : object ('self)
method private virtual extend : 'bn1 -> 'bn2 -> 'env -> 'env
method private virtual visit_'fn : 'env -> 'fn1 -> 'fn2 -> _
method visit_term : 'env -> ('fn1, 'bn1) term -> ('fn2, 'bn2) term -> unit
end
end
......@@ -11,4 +11,5 @@ KitShow
KitSubst
KitToDeBruijn
KitTrivial
ToolboxInput
Toolbox
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