237 lines
6.7 KiB
OCaml
237 lines
6.7 KiB
OCaml
(* This module defines facilities for working with syntax, in nominal and
|
|
de Bruijn representations. *)
|
|
|
|
type index =
|
|
int
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* The following module offers a facility for translating names to de Bruijn
|
|
indices. It is parameterized over the type of names, which must come with
|
|
a comparison function, so as to allow an efficient implementation of maps. *)
|
|
|
|
module Nominal2deBruijn (N : Map.OrderedType) = struct
|
|
|
|
module M =
|
|
Map.Make(N)
|
|
|
|
(* For efficiency reasons, we must work internally with de Bruijn levels,
|
|
as opposed to de Bruijn indices, and perform the conversion to an index
|
|
at the last moment. *)
|
|
|
|
type env = {
|
|
(* A map of every name to a de Bruijn level. *)
|
|
map: int M.t;
|
|
(* The current de Bruijn level. It is equal to the level of the most
|
|
recently bound name. Its absolute value is irrelevant. *)
|
|
current: int;
|
|
}
|
|
|
|
(* The empty environment. *)
|
|
|
|
let empty =
|
|
{ map = M.empty; current = 0 }
|
|
|
|
(* [lookup env x] translates the name [x] to a de Bruijn index. The
|
|
environment [env] must have been previously extended with [x],
|
|
otherwise [Unbound x] is raised. *)
|
|
|
|
exception Unbound of N.t
|
|
|
|
let lookup { map; current } x =
|
|
(* Looking up the map produces a de Bruijn level, which we
|
|
convert to a de Bruijn index by subtracting it from the
|
|
current level. *)
|
|
try
|
|
current - M.find x map
|
|
with Not_found ->
|
|
raise (Unbound x)
|
|
|
|
(* [extend env x] extends the environment with a new binding of the
|
|
name [x], producing a new environment. Any previous bindings of
|
|
this name are shadowed. *)
|
|
|
|
let extend { map; current } x =
|
|
let current = current + 1 in
|
|
let map = M.add x current map in
|
|
{ map; current }
|
|
|
|
(* [slide env x] extends the environment with a new binding of the
|
|
name [x], producing a new environment. Any previous bindings of
|
|
this name are shadowed. In contrast with [extend env x], instead
|
|
of mapping [x] to a distinct index, [slide env x] maps [x] to the
|
|
same index as the last introduced name. This exotic function can
|
|
be useful, e.g., when mapping term variables to type indices. *)
|
|
|
|
let slide { map; current } x =
|
|
(* Do not increment [current]. Thus, [x] receives the de Bruijn
|
|
index 0, as in [extend], but the indices of the previous
|
|
variables are not shifted up. *)
|
|
let map = M.add x current map in
|
|
{ map; current }
|
|
|
|
(* [bump env] skips an index, i.e., it shifts the range of the environment
|
|
[env] up by one. This exotic function can be useful, e.g., when mapping
|
|
term variables to type indices. Note that [extend env x] is equivalent
|
|
to [slide (bump env) x]. *)
|
|
|
|
let bump { map; current } =
|
|
let current = current + 1 in
|
|
{ map; current }
|
|
|
|
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
|
|
bindings of [env2] shadow any binding of the same variable in [env1]. *)
|
|
|
|
let concat env1 env2 =
|
|
(* We need to shift the de Bruijn levels of [env2] (and its
|
|
[current] value) by as many bindings as there are in [env1]. *)
|
|
let shift _x in1 in2 =
|
|
match in2 with
|
|
| None -> in1
|
|
| Some lvl -> Some (env1.current + lvl)
|
|
in
|
|
{
|
|
current = env1.current + env2.current;
|
|
map = M.merge shift env1.map env2.map;
|
|
}
|
|
end
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* This signature defines the functions that we need in order to be able
|
|
to implement binding representations on top of some syntax. *)
|
|
|
|
(* The signatures that follow mention two types [v] and [t]. Think of them as
|
|
``values'' and ``terms'', where the syntax of terms supports substitution
|
|
of values for variables. They can be the same type, of course. They are
|
|
parameterized over a representation of variables ['var] and a
|
|
representation of binders ['binder]. *)
|
|
|
|
module type VAR = sig
|
|
|
|
type ('var, 'binder) v
|
|
|
|
(* The function [var] expects a variable [x] and injects it into the
|
|
syntax of values. *)
|
|
|
|
val var:
|
|
'var ->
|
|
('var, 'binder) v
|
|
|
|
end
|
|
|
|
module type TRAVERSE = sig
|
|
|
|
type ('var, 'binder) v
|
|
type ('var, 'binder) t
|
|
|
|
(* [traverse lookup extend env t] can be thought of, roughly, as the result of
|
|
applying the substitution [lookup env] to the term [t] in a
|
|
capture-avoiding manner. The function [lookup], when supplied with a
|
|
suitable environment, maps variables to values. The function [extend]
|
|
updates the environment when a binder is crossed; it returns a pair of
|
|
the updated environment and a new binder. The parameter [env] is the
|
|
initial environment. *)
|
|
|
|
val traverse:
|
|
('env -> 'var1 -> ('var2, 'binder2) v) ->
|
|
('env -> 'binder1 -> 'env * 'binder2) ->
|
|
'env -> ('var1, 'binder1) t -> ('var2, 'binder2) t
|
|
|
|
end
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* A renaming function, [map], is defined in terms of [var] and [traverse].
|
|
It is analogous to [traverse], except that its argument [lookup] has type
|
|
['env -> 'var1 -> 'var2]. *)
|
|
|
|
module MakeMap
|
|
(V : VAR)
|
|
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
|
= struct
|
|
|
|
let map lookup extend env t =
|
|
T.traverse (fun env x -> V.var (lookup env x)) extend env t
|
|
|
|
end
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* Translation of a nominal representation to a de Bruijn representation. *)
|
|
|
|
module MakeTranslate
|
|
(V : VAR)
|
|
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
|
(N : Map.OrderedType)
|
|
= struct
|
|
|
|
include MakeMap(V)(T)
|
|
|
|
include Nominal2deBruijn(N)
|
|
|
|
let translate_open env t =
|
|
map
|
|
lookup
|
|
(fun env x -> extend env x, ())
|
|
env
|
|
t
|
|
|
|
let translate t = translate_open empty t
|
|
|
|
end
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* Weakening in a de Bruijn representation; also known as lifting. *)
|
|
|
|
module MakeLift
|
|
(V : VAR)
|
|
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
|
= struct
|
|
|
|
include MakeMap(V)(T)
|
|
|
|
let lift_var w k x =
|
|
if k <= x then w + x else x
|
|
|
|
let cross k () =
|
|
k + 1, ()
|
|
|
|
let lift w k t =
|
|
if w = 0 then
|
|
(* Fast path. *)
|
|
t
|
|
else
|
|
map (lift_var w) cross k t
|
|
|
|
end
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* Substitution in a de Bruijn representation. *)
|
|
|
|
module MakeSubst
|
|
(V : VAR)
|
|
(TVV : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v and type ('v, 'b) t = ('v, 'b) V.v)
|
|
(TVT : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
|
= struct
|
|
|
|
include MakeLift(V)(TVV)
|
|
|
|
let subst_var v k x =
|
|
if x < k then
|
|
V.var x
|
|
else if x = k then
|
|
v
|
|
else
|
|
V.var (x - 1)
|
|
|
|
let subst v k t =
|
|
TVT.traverse (fun l x ->
|
|
subst_var (lift l 0 v) (l + k) x
|
|
) cross 0 t
|
|
|
|
end
|
|
|