-
Notifications
You must be signed in to change notification settings - Fork 50
/
elpi-ltac.elpi
125 lines (101 loc) · 4.77 KB
/
elpi-ltac.elpi
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
/* elpi-ltac: building blocks for tactics */
/* license: GNU Lesser General Public License Version 2.1 or later */
/* ------------------------------------------------------------------------- */
typeabbrev tactic (sealed-goal -> (list sealed-goal -> prop)).
typeabbrev open-tactic (goal -> (list sealed-goal -> prop)).
% The one tactic ------------------------------------------------------------
pred refine i:term, i:goal, o:list sealed-goal.
refine T G GS :- refine.elaborate T G GS.
pred refine.elaborate i:term, i:goal, o:list sealed-goal.
refine.elaborate T (goal _ RawEv Ty Ev _) GS :-
rm-evar RawEv Ev,
@keepunivs! => coq.elaborate-skeleton T Ty TR ok,
coq.ltac.collect-goals TR GS _,
RawEv = T,
Ev = TR.
pred refine.typecheck i:term, i:goal, o:list sealed-goal.
refine.typecheck T (goal _ RawEv Ty Ev _) GS :-
rm-evar RawEv Ev,
coq.typecheck T Ty ok,
coq.ltac.collect-goals T GS _,
RawEv = T,
Ev = T.
pred refine.no_check i:term, i:goal, o:list sealed-goal.
refine.no_check T (goal _ RawEv _ Ev _) GS :-
rm-evar RawEv Ev,
coq.ltac.collect-goals T GS _,
RawEv = T,
Ev = T.
% calling other tactics, with arguments ---------------------------------------
pred coq.ltac i:string, i:sealed-goal, o:list sealed-goal.
coq.ltac Tac G GS :- coq.ltac.open (coq.ltac.call-ltac1 Tac) G GS.
namespace coq.ltac {
pred call i:string, i:list argument, i:goal, o:list sealed-goal.
call Tac Args G GS :-
set-goal-arguments Args G (seal G) (seal G1),
coq.ltac.call-ltac1 Tac G1 GS.
pred set-goal-arguments i:list argument, i:goal, i:sealed-goal, o:sealed-goal.
set-goal-arguments A G (nabla SG) (nabla R) :- pi x\ set-goal-arguments A G (SG x) (R x).
set-goal-arguments A (goal Ctx1 _ _ _ _) (seal (goal Ctx2 REv2 Ty2 Ev2 _)) (seal (goal Ctx2 REv2 Ty2 Ev2 I)) :- same_term Ctx1 Ctx2, !,
A = I.
set-goal-arguments A (goal Ctx1 _ _ _ _) (seal (goal Ctx2 REv2 Ty2 Ev2 _)) (seal (goal Ctx2 REv2 Ty2 Ev2 I)) :-
std.map A (private.move-goal-argument Ctx1 Ctx2) I.
% Tacticals ----------------------------------------------------------------
pred try i:tactic, i:sealed-goal, o:list sealed-goal.
try T G GS :- T G GS.
try _ G [G].
:index(_ 1)
pred all i:tactic, i:list sealed-goal, o:list sealed-goal.
all T [G|Gs] O :- T G O1, all T Gs O2, std.append O1 O2 O.
all _ [] [].
pred thenl i:list tactic, i:sealed-goal, o:list sealed-goal.
thenl [] G [G].
thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS.
pred repeat i:tactic, i:sealed-goal, o:list sealed-goal.
repeat T G GS :- T G GS1, all (repeat T) GS1 GS.
repeat _ G [G].
pred repeat! i:tactic, i:sealed-goal, o:list sealed-goal.
repeat! T G GS :- T G GS1, !, all (repeat T) GS1 GS.
repeat! _ G [G].
pred or i:list tactic, i:sealed-goal, o:list sealed-goal.
or TL G GS :- std.exists TL (t\ t G GS).
:index(_ 1)
pred open i:open-tactic, i:sealed-goal, o:list sealed-goal.
open T (nabla G) O :- (pi x\ open T (G x) (NG x)), private.distribute-nabla NG O.
open _ (seal (goal _ _ _ Solution _)) [] :- not (var Solution), !. % solved by side effect
open T (seal (goal Ctx _ _ _ _ as G)) O :-
std.filter Ctx private.not-already-assumed Ctx1,
Ctx1 => T G O,
if (var O)
(G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
true.
% helper code ---------------------------------------------------------------
namespace private {
:index(_ _ 1)
pred move-goal-argument i:list prop, i:list prop, i:argument, o:argument.
move-goal-argument _ _ (int _ as A) A.
move-goal-argument _ _ (str _ as A) A.
move-goal-argument _ _ (tac _) _ :-
coq.error "NIY: move tactic goal argument to another context".
move-goal-argument C D (trm T) (trm T1) :-
std.rev C Cr, std.rev D Dr,
std.assert! (move-term Cr Dr T T1) "cannot move goal argument to the right context", !.
:index(2)
pred move-term i:list prop, i:list prop, i:term, o:term.
move-term [] _ T T1 :- copy T T1.
move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY ], !,
copy X Y => move-term C1 C2 T T1.
move-term [def X _ TX BX|C1] [def Y _ TY BY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY, copy BX BX1, same_term BX1 BY ], !,
copy X Y => move-term C1 C2 T T1.
move-term [decl X _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
move-term [def X _ _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
move-term C1 [_|C2] T T1 :- move-term C1 C2 T T1.
pred distribute-nabla i:(term -> list sealed-goal), o:list sealed-goal.
distribute-nabla (_\ []) [].
distribute-nabla (x\ [X x| XS x]) [nabla X|R] :- (pi x\ occurs x (X x)), !,
distribute-nabla XS R.
distribute-nabla (x\ [X| XS x]) [X|R] :- distribute-nabla XS R.
pred not-already-assumed i:prop.
not-already-assumed (decl X _ _Ty) :- not(decl X _ _ ; def X _ _ _).
not-already-assumed (def X _ _Ty _Bo) :- not(decl X _ _ ; def X _ _ _).
}}