Merge PR #13685: Add a debug printer for fconstr substitutions.

Reviewed-by: SkySkimmer

6 files changed, 60 insertions, 0 deletions

diff --git a/dev/include_printers b/dev/include_printers
index 7583762970..414468ca65 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -54,4 +54,6 @@
 
 #install_printer  (* fconstr *) ppfconstr;;
 
+#install_printer  (* fsubst *) ppfsubst;;
+
 #install_printer (* Future.computation *) ppfuture;;
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index bfc186c862..fe95a59d9b 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -23,6 +23,7 @@ install_printer Top_printers.ppconstr_expr
 install_printer Top_printers.ppglob_constr
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppfconstr
+install_printer Top_printers.ppfsubst
 install_printer Top_printers.ppnumtokunsigned
 install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4faa12af79..6ce347ad59 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -85,6 +85,15 @@ let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
+let ppfsubst s =
+  let (s, k) = Esubst.Internal.repr s in
+  let sep () = str ";" ++ spc () in
+  let pr = function
+  | Esubst.Internal.REL n -> str "<#" ++ int n ++ str ">"
+  | Esubst.Internal.VAL (k, x) -> pr_constr (Vars.lift k (CClosure.term_of_fconstr x))
+  in
+  pp @@ str "[" ++ prlist_with_sep sep pr s ++ str "| " ++ int k ++ str "]"
+
 let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
 let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 50495dc0a4..e8ed6c709e 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -52,6 +52,7 @@ val ppconstr_expr : Constrexpr.constr_expr -> unit
 val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
 val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
+val ppfsubst : CClosure.fconstr Esubst.subs -> unit
 
 val ppnumtokunsigned : NumTok.Unsigned.t -> unit
 val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit
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