From 56f3b1d5817fbdcac72818148c5f0123dcdd26fa Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 10 Jul 2024 14:08:18 +0200
Subject: [PATCH] [TC] compilation of primitive projections to their
 compatibility constants

---
 apps/tc/elpi/ho_compile.elpi     |  5 +++--
 apps/tc/tests/canonical_struct.v | 21 ++++++++++++++++++++-
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 2ce8b11d7..2d3b388a6 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,7 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
-        decompile-term-aux (primitive _ as X) L X L :- !.
+        decompile-term-aux (primitive (proj P _)) L (global (const Y)) L :- !, coq.env.primitive-projection? P Y.
         decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
           name Y X S,
           decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
@@ -334,7 +334,8 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
+      decompile-problematic-term (primitive (proj P _)) A (global (const Y)) A :- !, 
+        coq.env.primitive-projection? P Y.
       
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
         prune V S, !, fold-map T L T' L2.
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 838c10d3d..1a36e4330 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,4 +99,23 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
\ No newline at end of file
+End CS5.
+
+Module CS6.
+  #[projections(primitive=yes)]
+  Structure ofe := Ofe { ofe_car : Type; }.
+
+  #[projections(primitive=no)] (* TODO: Putting primitive to yes leads to a unification error. Why? *)
+  Structure cmra := { cmra_car :> Type; }.
+  Canonical Structure cmra_ofeO (A : cmra) : ofe := Ofe A.
+
+  Class C (I : Type).
+  Instance c : forall (A : ofe), C ((A).(ofe_car)) := {}.
+
+  Section s.
+    Context {cmra : cmra}.
+    Goal C (cmra_car cmra).
+      apply _.
+    Qed.
+  End s.
+End CS6.