Export a high-level representation of term substitutions.

2 files changed, 47 insertions, 0 deletions

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index afd8e3ef67..1c8575ef05 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -245,3 +245,38 @@ let rec lift_subst mk e s = match s with
   let t, e = tree_map mk e t in
   let rem = lift_subst mk e rem in
   Cons (h, t, rem)
+
+module Internal =
+struct
+
+type 'a or_rel = REL of int | VAL of int * 'a
+
+let to_rel shift = function
+| Var i -> REL (i + shift)
+| Arg v -> VAL (shift, v)
+
+let rec get_tree_subst shift accu = function
+| Leaf (w, x) ->
+  to_rel (shift + w) x :: accu
+| Node (w, x, l, r, _) ->
+  let accu = get_tree_subst (shift + w + eval l) accu r in
+  let accu = get_tree_subst (shift + w) accu l in
+  to_rel (shift + w) x :: accu
+
+let rec get_subst shift accu = function
+| Nil (w, n) ->
+  List.init n (fun i -> REL (w + i + shift + 1))
+| Cons (_, t, s) ->
+  let accu = get_subst (shift + eval t) accu s in
+  get_tree_subst shift accu t
+
+let rec get_shift accu = function
+| Nil (w, n) -> accu + w + n
+| Cons (_, t, s) -> get_shift (eval t + accu) s
+
+let repr (s : 'a subs) =
+  let shift = get_shift 0 s in
+  let subs = get_subst 0 [] s in
+  subs, shift
+
+end
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 8ff29ab07a..b0fbe680c3 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -94,3 +94,15 @@ val is_lift_id : lift -> bool
     That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ.
 *)
 val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs
+
+(** Debugging utilities *)
+module Internal :
+sig
+type 'a or_rel = REL of int | VAL of int * 'a
+
+(** High-level representation of a substitution. The first component is a list
+    that associates a value to an index, and the second component is the
+    relocation shift that must be applied to any variable pointing outside of
+    the substitution. *)
+val repr : 'a subs -> 'a or_rel list * int
+end