Extend `Print Canonical Projections` with a search functionality

The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.

2 files changed, 64 insertions, 0 deletions

diff --git a/test-suite/output/PrintCanonicalProjections.out b/test-suite/output/PrintCanonicalProjections.out
new file mode 100644
index 0000000000..a4e2251440
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.out
@@ -0,0 +1,18 @@
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+nat <- sort_eq ( nat_eqType )
+nat <- sort_TYPE ( nat_TYPE )
+prod <- sort_eq ( prod_eqType )
+prod <- sort_TYPE ( prod_TYPE )
+sum <- sort_eq ( sum_eqType )
+sum <- sort_TYPE ( sum_TYPE )
+sum <- sort_TYPE ( sum_TYPE )
+prod <- sort_TYPE ( prod_TYPE )
+nat <- sort_TYPE ( nat_TYPE )
+bool <- sort_TYPE ( bool_TYPE )
+sum <- sort_eq ( sum_eqType )
+prod <- sort_eq ( prod_eqType )
+nat <- sort_eq ( nat_eqType )
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+bool <- sort_eq ( bool_eqType )
diff --git a/test-suite/output/PrintCanonicalProjections.v b/test-suite/output/PrintCanonicalProjections.v
new file mode 100644
index 0000000000..808cdffe39
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.v
@@ -0,0 +1,46 @@
+Record TYPE := Pack_TYPE { sort_TYPE :> Type }.
+Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }.
+
+Definition eq_op (T : eqType) : T -> T -> bool :=
+  match T with Pack_eq _ op => op end.
+
+Definition bool_eqb b1 b2 :=
+  match b1, b2 with
+  | false, false => true
+  | true, true => true
+  | _, _ => false
+  end.
+
+Canonical bool_TYPE := Pack_TYPE bool.
+Canonical bool_eqType := Pack_eq bool bool_eqb.
+
+Canonical nat_TYPE := Pack_TYPE nat.
+Canonical nat_eqType := Pack_eq nat Nat.eqb.
+
+Definition prod_eqb (T U : eqType) (x y : T * U) :=
+  match x, y with
+  | (x1, x2), (y1, y2) =>
+    andb (eq_op _ x1 y1) (eq_op _ x2 y2)
+  end.
+
+Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U).
+Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U).
+
+Definition sum_eqb (T U : eqType) (x y : T + U) :=
+  match x, y with
+  | inl x, inl y => eq_op _ x y
+  | inr x, inr y => eq_op _ x y
+  | _, _ => false
+  end.
+
+Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U).
+Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U).
+
+Print Canonical Projections bool.
+Print Canonical Projections nat.
+Print Canonical Projections prod.
+Print Canonical Projections sum.
+Print Canonical Projections sort_TYPE.
+Print Canonical Projections sort_eq.
+Print Canonical Projections sort_TYPE bool.
+Print Canonical Projections bool_eqType.