Stream: Elpi users & devs

Topic: Record Import


view this post on Zulip Jason Gross (Apr 21 2021 at 21:25):

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

view this post on Zulip Enrico Tassi (Apr 22 2021 at 08:15):

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.

view this post on Zulip Enrico Tassi (Apr 22 2021 at 08:26):

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

view this post on Zulip Jason Gross (Apr 29 2021 at 21:48):

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

view this post on Zulip Andres Erbsen (Apr 30 2021 at 01:02):

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

view this post on Zulip Enrico Tassi (Apr 30 2021 at 06:29):

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: Mar 28 2024 at 15:01 UTC