[TC] compilation of primitive projections to their compatibility constants

Author: FissoreD

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.

apps/tc/tests/canonical_struct.v

@@ -99,4 +99,23 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
+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.