I have a term of type string
that stack-overflows Tacred.compute
but I can't print it because it also stack-overflows Printer.pr_econstr_env
. I think it should be a concatenation of three strings but I can't say for certain. Are there other ways of printing terms that I could use to find out what exactly is in this term?
I can reduce it with Redexpr.cbv_vm
and print the result but then I only know the resulting bytes, not the structure.
(From that I already know it's roughly 300 bytes so the stack overflows are somewhat surprising)
Oh, I spoke too soon. I didn't use the right printing options. It seems cbv_vm
also overflows the stack. This must be a cursed string!
(The printing options matter because the string is actually the output of an earlier call to pr_econstr_env
translated into a coq string
.)
You could write an Ltac or Ltac2 procedure that prints it bit by bit, e.g.,
Ltac print term :=
lazymatch term with
| ?f ?x => idtac "(APP (";
print f;
idtac ") (";
print x;
idtac "))"
| forall x : ?T, ?f
=> idtac "(FORALL" x ": (";
print T;
idtac "), (";
let F' := fresh in
let __ := constr:(forall x : T,
match f return Prop with
| F' => ltac:(let f := (eval cbv delta [F'] in F') in
clear F';
print f;
exact True)
end) in
idtac "))"
| fun x : ?T => ?f
=> idtac "(FUN" x ": (";
print T;
idtac ") => (";
let F' := fresh in
let __ := constr:(fun x : T =>
match f return Prop with
| F' => ltac:(let f := (eval cbv delta [F'] in F') in
clear F';
print f;
exact True)
end) in
idtac "))"
| let x : ?T := ?v in ?f
=> idtac "(LET" x ": (";
print T;
idtac ") := (";
print v;
idtac ") IN (";
let F' := fresh in
let __ := constr:(let x : T := v in
match f return Prop with
| F' => ltac:(let f := (eval cbv delta [F'] in F') in
clear F';
print f;
exact True)
end) in
idtac "))"
| ?term => idtac "(UNRECOGNIZED (";
idtac term;
idtac "))"
end.
Require Import Coq.ZArith.ZArith.
Goal True.
let v := (eval cbv delta in Z.div_eucl) in
print v.
You can do better by using Ltac2's Constr.Unsafe.kind
(or using the same in OCaml)
That's an interesting idea. Thanks!
Last updated: Dec 01 2023 at 06:01 UTC