Record import

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

From elpi Require Import elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]



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:

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

Section test.
Variable x : r nat 3.
x is declared

import.projections x.
Print p2.
Notation p2 := (p2 nat 3 x)

Check p1 : nat. (* check p1 is already applied to x *)
Top.p1 nat 3 x : nat
     : nat

End test.
Fail Check p1 : nat. (* the abbreviation is gone *)
The command has indeed failed with message:
The term "p1" has type "forall (T : Type) (t : T), r T t -> nat"
while it is expected to have type "nat".

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

Module test.
Interactive Module test started

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

End test.
Module test is defined

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

Section test2.
Variable x : r1 bool.
x is declared

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

End test2.