From ad8c2b7dab1b0759d1c304350523d6d2cc9c7b24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Dec 2020 22:02:22 +0100
Subject: Register a printer for fconstr substitutions in the kernel.

---
 dev/include_printers | 2 ++
 dev/top_printers.dbg | 1 +
 dev/top_printers.ml  | 9 +++++++++
 dev/top_printers.mli | 1 +
 4 files changed, 13 insertions(+)

(limited to 'dev')

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
-- 
cgit v1.2.3