example_import_projections.v

From elpi Require Import elpi.

(* "import" a record instance by naming it's applied projections *)

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.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 Coq
  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 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 *)
 
(**************************** usage examples *********************************)

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.

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.