Janno (Jun 16 2020 at 21:14): Janno (Jun 16 2020 at 21:14):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?
Janno (Jun 16 2020 at 21:16):I can reduce it with Redexpr.cbv_vm and print the result but then I only know the resulting bytes, not the structure.
Janno (Jun 16 2020 at 21:17):(From that I already know it's roughly 300 bytes so the stack overflows are somewhat surprising)
Janno (Jun 16 2020 at 21:26):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!
Janno (Jun 16 2020 at 21:27):(The printing options matter because the string is actually the output of an earlier call to pr_econstr_env translated into a coq string.)
Jason Gross (Jun 22 2020 at 18:21):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)
Janno (Jun 22 2020 at 19:30):That's an interesting idea. Thanks!
Last updated: Dec 01 2023 at 06:01 UTC