Feature request: Make sharing explicit in printed representation of terms

[cpitclaudel]

Description of the problem

I regularly run into performance problems related to sharing, and I find hard to figure out what is and isn't shared in a Coq term. Consider the following, trivial example:

Inductive Tree := Branch (t1 t2: Tree) | Leaf {A} (a: A).

Fixpoint complete_tree {A} (n: nat) (a: A) :=
  match n with
  | 0 => Leaf a
  | S n => let subtree := complete_tree n a in
          Branch subtree subtree
  end.

Fixpoint complete_tree_slow {A} (n: nat) (a: A) :=
  match n with
  | 0 => Leaf a
  | S n => Branch (complete_tree_slow n a) (complete_tree_slow n a)
  end.

Both of these look the same when printed:

Compute (complete_tree 3).
(* = Branch (Branch (Branch Leaf Leaf) (Branch Leaf Leaf))
            (Branch (Branch Leaf Leaf) (Branch Leaf Leaf)) *)
Compute (complete_tree_slow 3).
(* = Branch (Branch (Branch Leaf Leaf) (Branch Leaf Leaf))
            (Branch (Branch Leaf Leaf) (Branch Leaf Leaf)) *)

But of course their behaviors differ significantly:

Definition ignore {A} (a: A) := tt.
Compute (ignore (complete_tree 1500)).
Compute (ignore (complete_tree_slow 30)).

Contrast this with, say, Lisp's printing of recursive and nested structures:

ELISP> (defun complete-tree (n)
         (if (= n 0)
             nil
           (let ((subtree (complete-tree (- n 1))))
             `[,subtree ,subtree])))
ELISP> (setq print-circle nil)
ELISP> (complete-tree 3)
[[[nil nil]
  [nil nil]]
 [[nil nil]
  [nil nil]]]

ELISP> (setq print-circle t)
ELISP> (complete-tree 3)
[#2=[#1=[nil nil]
        #1#]
    #2#]

Two questions:

• Is there a way in Coq to print terms with explicit indications of what is and isn't shared?
• Do any of the reduction engines do memoization, to speed up calculations on structures with sharing? (Or even better, do any use hashconsing to speed up calculations regardless of sharing?)
• Do any of the reduction engines preserve sharing? The following suggests that they don't:

  Definition a :=
    Eval compute in (complete_tree 100).

• Do any of the reduction engines mark already-reduced terms to save themselves the trouble of re-reducing them? This suggests not:

  Definition a :=
    Eval compute in (complete_tree 20).
  
  Definition aa :=
    Eval compute in a.
  
  Definition aaa :=
    Eval compute in aa.

Thanks!

Coq Version

8.10

[ppedrot]

1. Not that I know of
2. Kernel reduction uses an ad-hoc call-by-need reduction with sharing
3. No
4. No

Note that compute is call-by-value, if you want the call-by-need reduction use lazy instead. Also, Coq uses hashconsing somehow, but I could write a book of horrors on that topic.