Stream: Coq devs & plugin devs

Topic: How to print large terms


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Janno (Jun 16 2020 at 21:17):

(From that I already know it's roughly 300 bytes so the stack overflows are somewhat surprising)

view this post on Zulip 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!

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip Janno (Jun 22 2020 at 19:30):

That's an interesting idea. Thanks!


Last updated: Oct 21 2021 at 21:03 UTC