Quoting function is slow when quoting itself.

[JasonGross]

Here is code that takes a while to run:

Require Import Template.Template.

Quote Recursively Definition aterm := Ast.term.
Time Quote Recursively Definition aterm' := aterm. (* Finished transaction in 49. secs (48.703u,0.172s) *)

Any chance of making this faster?

[gmalecha]

This isn't surprising is it? The term that you are constructing is 78 thousand lines of code. It is quoting ever single constructor in the Ast.term data type representation. If you have suggestions on how to improve the performance, feel free to note them.

[JasonGross]

I'm trying to implement Löb's theorem and type-theoretic quines. Writing a quine requires being able to quote the Ast.term data type, and also quote the quotation of it.

Perhaps let-expanding strings, so that each string is only mentioned once in the quoted term, would speed things up?

[gmalecha]

Let-declaring the strings would probably be helpful, I'm not certain that it would be enough, but it would be better. Then you would end up with the problem that quoting a quoted term would have extra "let" declarations at the head.

[gmalecha]

Happy to reopen if there are ideas on how to handle the performance problem. A more concise representation? Would hashconsing be enough?

For now, I think that should be marked as wontfix.