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: Oct 13 2024 at 01:02 UTC