1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
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 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.
|
