Record import
=============

Gives short names to record projections applied to a given record instance
("import" a record instance by naming its applied projections).

.. rocqtop:: in reset

   From elpi Require Import elpi.

.. rocqtop:: all

   Elpi Command import.projections.
   Elpi Accumulate lp:{{
   main [str S] :-
     coq.locate S GR,
     coq.env.typeof GR Ty,
     main-import-projections (global GR) Ty.
   main [trm TSkel] :-
     % input terms are not elaborated yet
     std.assert-ok! (coq.elaborate-skeleton TSkel Ty T) "input term illtyped",
     main-import-projections T Ty.

   pred main-import-projections term, term.
   main-import-projections T Ty :-
     std.assert! (coq.safe-dest-app Ty (global (indt I)) Args) "not an inductive term",
     std.assert! (coq.env.record? I PrimProjs) "not a record",
     coq.env.indt I _ _ NParams _ _ _,
     std.assert! (std.length Args NParams) "the record is not fully appplied",
     coq.env.projections I Ps, % get the projections generated by Rocq
     if (PrimProjs = tt)
        (std.forall Ps (declare-abbrev {std.append {coq.mk-n-holes NParams} [T]}))
        (std.forall Ps (declare-abbrev {std.append Args [T]})).

   pred declare-abbrev list term, option constant.
   declare-abbrev _ none.
   declare-abbrev Args (some Proj) :-
     coq.gref->id (const Proj) ID, % get the short name of the projection
     OnlyParsing = tt,
     coq.mk-app (global (const Proj)) Args T, % handles the case Args = []
     @local! ==> coq.notation.add-abbreviation ID 0 T OnlyParsing _.
   }}.

   Elpi Export import.projections. (* make the command available *)

Usage examples:

.. rocqtop:: all

   Record r T (t : T) := Build {
     p1 : nat;
     p2 : t = t;
     _ : p2 = refl_equal;
   }.

   Section test.
   Variable x : r nat 3.
   import.projections x.
   Print p2.
   Check p1 : nat. (* check p1 is already applied to x *)
   End test.

   Fail Check p1 : nat. (* the abbreviation is gone *)
   Check p1 : forall (T : Type) (t : T), r T t -> nat. (* p1 points again to the original projection *)

   Module test.
   import.projections (Build bool false 3 (refl_equal _) (refl_equal _)).
   Check refl_equal _ : p1 = 3. (* check the value of p1 is 3 *)
   End test.

   Set Primitive Projections.
   Unset Auto Template Polymorphism.
   Record r1 (A : Type) : Type := {
     f1 : A;
     f2 : nat;
   }.

   Section test2.
   Variable x : r1 bool.
   import.projections x.
   Unset Printing Primitive Projection Parameters.
   Check f1. (* there is an _, hence it is the primitive projection *)
   End test2.