How hard would it be to use elpi to write a `Record Import var`

command with the following spec:

Assume that `var`

is a term whose type is a record with `n`

parameters. For each projection `proj`

in the record, emit a `Local Notation proj := (@proj <n underscores> var).`

(Ideally for primitive records we would not get the compatibility constant but instead the primitive projection applied to `var`

.)

Here it is. Maybe in the case the input is a term one should make a definition on the fly.

```
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.
```

If you find this useful I can put it in the repo, among the other examples.

If you really want to put `_`

in place of `Args`

there is a `coq.mk-n-holes`

API and `coq.env.indt`

also given you the number of paramters.

Btw, I did forget to check the record type is fully applied, (check that `std.length Args`

is equal to the number of declared parameters).

Belatedly (sorry, I'm not actively checking this channel): this looks awesome, thanks! I'll try it out shortly. (Holes vs arguments doesn't matter to me unless getting it to work with primitive records requires one or the other.)

I tried it out some at https://github.com/mit-plv/coqutil/compare/master...elpi-record-import and I quite like it. It's impressive that elpi makes prototyping stuff like this easy. Next time I get really frustrated with implicit argument elaboration I will actually try and replace typeclasses with this (and some hack for type-base projection name scoping).

Great, I'll put the code above among the other examples and link it from the readme so that others can find it as well.

Last updated: Jun 06 2023 at 23:01 UTC