Commit 7ebdb8e6 authored by POTTIER Francois's avatar POTTIER Francois

Defined the type [def].

Introduced an isomorphism with [abs], but it does not look worth exploiting.
parent 4e010cca
......@@ -15,6 +15,25 @@ type ('bn, 'term) abs =
(* -------------------------------------------------------------------------- *)
(* A definition is a binding form of the form [let x = t1 in t2].
The name [x] is in scope in [t2], but not in [t1]. *)
type ('bn, 'term) def =
'bn * 'term * 'term
(* This type is isomorphic to ['term * ('bn, 'term) abs]. *)
(* This isomorphism is exploited below; it facilitates the construction of
visitor methods for [def], based on visitor methods for [abs]. *)
let into : 'term * ('bn, 'term) abs -> ('bn, 'term) def =
fun (t1, (x, t2)) -> (x, t1, t2)
let outof : ('bn, 'term) def -> 'term * ('bn, 'term) abs =
fun (x, t1, t2) -> (t1, (x, t2))
(* -------------------------------------------------------------------------- *)
(* 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. *)
......@@ -57,6 +76,27 @@ class virtual ['self] map = object (self : 'self)
let x', env' = self#extend x env in
x', f env' body
method private visit_def: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2) ->
'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def
= fun b f env def ->
let t1, a2 = outof def in
into (
f env t1,
self#visit_abs b f env a2
)
(* TEMPORARY direct version:
method private visit_def: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2) ->
'env -> ('bn1, 'term1) def -> ('bn2, 'term2) def
= fun _ f env (x, t1, t2) ->
let x', env' = self#extend x env in
x', f env t1, f env' t2
*)
end
(* -------------------------------------------------------------------------- *)
......
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