From elpi Require Import elpi.

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 i:term, i: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.indt I _ _ _ _ [_] _) "not a record",
  coq.CS.canonical-projections I Ps, % get the projections generated by Coq
  std.forall Ps (declare-abbrev {std.append Args [T]}).

pred declare-abbrev i:list term, i: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 Typecheck.
Elpi Export import.projections. (* make the command available *)

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. (* Notation p2 := (readme.p2 nat 3 x) *)
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.