Skip to content

Commit a8502e9

Browse files
FissoreDFissoreD
committed
[TC] improve perf of goal compilation
1 parent 9026ada commit a8502e9

File tree

7 files changed

+228
-52
lines changed

7 files changed

+228
-52
lines changed

‎apps/tc/elpi/base.elpi‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -90,10 +90,13 @@ split-at-not-fatal N [X|XS] [X|LN] LM :- !, N1 is N - 1,
9090

9191
pred undup-same i:list A, o:list A.
9292
undup-same [] [].
93-
undup-same [X|Xs] [X|Ys] :-
94-
std.forall Xs (x\ not (x == X)), !,
95-
undup-same Xs Ys.
96-
undup-same [_|Xs] Ys :- undup-same Xs Ys.
93+
undup-same [X|Xs] Ys :- std.exists Xs (x\ x == X), !, undup-same Xs Ys.
94+
undup-same [X|Xs] [X|Ys] :- undup-same Xs Ys.
95+
96+
pred undup i:list A, o:list A.
97+
undup [] [].
98+
undup [X|Xs] Ys :- std.mem! Xs X, !, undup Xs Ys.
99+
undup [X|Xs] [X|Ys] :- undup Xs Ys.
97100

98101
:index (1)
99102
pred is-coq-term i:A.
@@ -168,3 +171,9 @@ pred close-term-no-prune-fun i:(term -> list term), i:term, o:list term.
168171
close-term-no-prune-fun (x\ []) _ [] :- !.
169172
close-term-no-prune-fun (x\ [X x | Xs x]) Ty [fun _ Ty X | Xs'] :-
170173
close-term-no-prune-fun Xs Ty Xs'.
174+
175+
pred free-names i:term, o:list term.
176+
free-names T L :-
177+
names N,
178+
(pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
179+
undup {std.rev L'} L.

‎apps/tc/elpi/compile_goal.elpi‎

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
namespace tc {
2+
shorten tc.{r-ar, range-arity}.
3+
4+
namespace compile {
5+
namespace goall {
6+
:index (_ _ 1)
7+
pred may-contract-to i:list term, i:term, i:term.
8+
may-contract-to _ N N :- !.
9+
% TODO: here we should do var V _ Scope and use scope: N can be in Scope but not in S
10+
may-contract-to L N (app [V|S]) :- var V, !,
11+
std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
12+
may-contract-to L N (app [N|A]) :-
13+
std.length A {std.length L},
14+
std.forall2 {std.rev L} A (may-contract-to []).
15+
may-contract-to L N (fun _ _ B) :-
16+
pi x\ may-contract-to [x|L] N (B x).
17+
18+
:index (_ 1)
19+
pred occurs-rigidly i:term, i:term.
20+
occurs-rigidly N N :- name N, !.
21+
occurs-rigidly _ (app [N|_]) :- var N, !, fail.
22+
occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
23+
occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
24+
25+
pred maybe-eta-aux i:term, i:list term.
26+
% TODO: here we should do var V _ Scope and use Scope: an elt in L can appear in Scope
27+
maybe-eta-aux (app[V|S]) L :- var V, !,
28+
std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
29+
maybe-eta-aux (app [_|A]) L :-
30+
SplitLen is {std.length A} - {std.length L},
31+
split-at-not-fatal SplitLen A HD TL,
32+
std.forall L (x\ not (exists! HD (occurs-rigidly x))),
33+
std.forall2 {std.rev L} TL (may-contract-to []).
34+
maybe-eta-aux (fun _ _ B) L :-
35+
pi x\ maybe-eta-aux (B x) [x|L].
36+
37+
pred maybe-eta i:term.
38+
maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
39+
40+
pred split-pf i:list term, i:list term, o:list term, o:list term.
41+
split-pf [] _ [] [] :- !.
42+
split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
43+
split-pf Xs _ [] Xs.
44+
45+
pred used i:term, i:term.
46+
used X (uvar _ S) :- std.mem! S X, !.
47+
used X (fun _ _ Bo) :- pi x\ used X (Bo x).
48+
49+
pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
50+
close-term-prune-safe-fun (x\ []) _ [] :- !.
51+
close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :-
52+
pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
53+
close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
54+
close-term-prune-safe-fun Xs Ty Xs'.
55+
56+
pred compile-full-aux-close i:(term -> term), i:term, i:list prop, o:(term -> term), o:list prop.
57+
compile-full-aux-close Bo Ty L Bo' L' :-
58+
(pi x\ compile-full-aux (Bo x) [] (Bo' x) (BoL x)),
59+
% TODO: maybe attach to the links the list of used binders, to simply make this check?
60+
% Maybe L' is a pair list links and list binders per link, this way we can easily prune
61+
close-term-no-prune-ty BoL Ty BoL',
62+
std.append L BoL' L'.
63+
64+
pred compile-full-aux i:term, i:list prop, o:term, o:list prop.
65+
compile-full-aux (global _ as G) L G L :- !.
66+
compile-full-aux (pglobal _ _ as G) L G L :- !.
67+
compile-full-aux (sort _ as G) L G L :- !.
68+
69+
% Link for coercion
70+
compile-full-aux (app [HD|_] as G) L G' [tc.link.cs G' G | L] :- tc.coercion-unify HD, !.
71+
72+
% Link for canonical structure
73+
compile-full-aux (app [global (const C) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.projection? C _, !.
74+
75+
% Link for primitive projection
76+
compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _, !.
77+
78+
% Link for eta-redex
79+
compile-full-aux (fun Name Ty Bo as G) L G' [tc.link.eta G' (fun Name Ty' Bo') | L'] :- maybe-eta G, !,
80+
compile-full-aux Ty L Ty' LTy,
81+
compile-full-aux-close Bo Ty LTy Bo' L'.
82+
83+
compile-full-aux (fun Name Ty Bo) L (fun Name Ty' Bo') L' :- !,
84+
compile-full-aux Ty L Ty' LTy,
85+
compile-full-aux-close Bo Ty LTy Bo' L'.
86+
87+
compile-full-aux (prod Name Ty Bo) L (prod Name Ty' Bo') L' :- !,
88+
compile-full-aux Ty L Ty' LTy,
89+
compile-full-aux-close Bo Ty LTy Bo' L'.
90+
91+
% NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
92+
% then the coq variable has not [x,y] in scope, it is applied to
93+
% them. Note also that t is a problematic term that cannot be
94+
% exposed to the else unification algorithm.
95+
% The solution is to build the following links:
96+
% X =η (λa.Y a)
97+
% a |- Y a =η (λb.Z a b)
98+
% and expose a variable W at toplevel having Z has head and [x, y]
99+
% as scope
100+
101+
% NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
102+
% name, we build a llam link.
103+
% The link will be: T x =L X a x
104+
% the exposed variable in the term will be T x
105+
106+
% NOTE: here a combination of eta and llam:
107+
% let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
108+
% y in scope, z and w are names and c, d are constants.
109+
% In this case, the links should be:
110+
% X x y =η (λa.Y x y a)
111+
% a |- Z x y a w =L (app[Y x y a, c w d])
112+
% The returned variable is Z x y a w
113+
114+
pred free-names i:term, o:list term.
115+
free-names T L :-
116+
names N,
117+
(pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
118+
undup {std.rev L'} L.
119+
120+
:index(_ _ _ _ 3)
121+
% TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
122+
% LHS Scope Ty Names PF NPF OLDLINKS NEW_VAR
123+
pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
124+
build-eta-llam-links LHS _ _ Names [] NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
125+
std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
126+
prune T Names,
127+
var T HD _.
128+
build-eta-llam-links LHS SC _Ty _ [X] [] OL HD [tc.link.eta LHS (fun _ _ (x\ V x)) | OL] :- !,
129+
prune V SC, var (V X) HD _. % TODO...
130+
build-eta-llam-links LHS SC _Ty Names [X|XS] NPF OL HD [tc.link.eta LHS (fun _ _ (x\ LHS' x)) | L] :- !,
131+
% TODO: unfold Ty if needed...
132+
std.append SC [X] SC',
133+
prune LHS' SC, build-eta-llam-links (LHS' X) SC' _ Names XS NPF OL HD L.
134+
135+
% Link for beta-redex (Uvar in PF)
136+
% BUILD CHAIN OF LINKS-ETA from X to V...
137+
% TODO: to avoid too many chain for the same var, maybe pass a list into the fold
138+
compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
139+
% By construction the scope of a uvar is a list of distinct name
140+
std.fold-map S L compile-full-aux S' L', % LS = Links built for S
141+
% std.assert-ok! (coq.typecheck V Ty) "Not typecheckable variable",
142+
split-pf S' Scope PF NPF,
143+
free-names T Names,
144+
build-eta-llam-links V Scope _ Names PF NPF L' G'' L'',
145+
prune G' Names,
146+
var G' G'' Names.
147+
148+
compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.
149+
150+
compile-full-aux (let N T B F) A (let N T1 B1 F1) A3 :- !,
151+
compile-full-aux T A T1 A1, compile-full-aux B A1 B1 A2,
152+
compile-full-aux-close F T A2 F1 A3.
153+
154+
compile-full-aux (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
155+
compile-full-aux Ty A Ty1 A1,
156+
compile-full-aux-close F Ty A1 F1 A2.
157+
158+
compile-full-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
159+
compile-full-aux T A T1 A1,
160+
compile-full-aux Rty A1 Rty1 A2,
161+
std.fold-map B A2 compile-full-aux B1 A3.
162+
163+
compile-full-aux (uvar _ _ as X) A X A :- !.
164+
compile-full-aux X A X A :- name X, !.
165+
166+
compile-full-aux A B _ _ :- coq.error "Fail to compile-full-aux" A B.
167+
168+
% takes a term t and returns a term t' and a list of links.
169+
pred compile-full i:term, o:term, o:list prop.
170+
compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
171+
}
172+
173+
pred goal' i:term, o:term, o:list prop.
174+
:name "compile-goal'"
175+
goal' Goal Goal' Links :-
176+
goall.compile-full-aux Goal [] Goal' Links.
177+
}
178+
}

‎apps/tc/elpi/ho_link.elpi‎

Lines changed: 19 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
namespace tc {
22
namespace link {
3+
pred relocate i:list term, i:list term, i:term, o:term.
4+
relocate [] [] T T' :- copy T T'.
5+
relocate [X|Xs] [Y|Ys] T T' :- (copy Y X :- !) => relocate Xs Ys T T'.
6+
37
pred get-vars i:term, o:list term.
48
get-vars T R :-
59
(pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) =>
@@ -61,12 +65,6 @@ namespace tc {
6165
pred scope-check i:term, i:term.
6266
scope-check (uvar _ L) T :- prune A L, A = T, !.
6367

64-
pred relocate i:list term, i:list term, i:term, o:term.
65-
relocate [] [] T T' :- copy T T', coq.say "Copy result is" T T'.
66-
relocate [X|Xs] [Y|Ys] T T' :-
67-
coq.say "Charging" (copy Y X),
68-
(copy Y X :- !) => relocate Xs Ys T T'.
69-
7068
pred collect-store o:list prop.
7169
pred collect-store-aux i:list prop, o:list prop.
7270

@@ -80,24 +78,14 @@ namespace tc {
8078
unify-eta A (fun _ _ _ as B) :- !, eta-expand A A', unify-eta A' B.
8179
unify-eta A B :- A = B.
8280

83-
constraint eta uvar relocate fun collect-store-aux solve-eta {
81+
constraint eta solve-eta {
8482
rule solve-eta \ (eta A B) <=> (unify-eta A B).
8583
rule \ solve-eta.
86-
% rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1))
87-
% \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2))
88-
% | (
89-
% pi x\ relocate L1 L2 (B2 x) (B2' x)
90-
% % coq.say "Deduplicating"
91-
% % (eta (uvar X L1) (fun _ T1 B1))
92-
% % (eta (uvar X L2) (fun _ T2 B2))
93-
% % "B2' is" (B2')
94-
% )
95-
% <=> (N1 : G1 ?- B1 = B2').
96-
97-
% TODO: link collect do not work since it closes links and
98-
% therefore variables are prune
99-
% rule \ (tc.link.eta A B) (collect-store-aux L R) | (coq.say A B {names}) <=> (collect-store-aux [tc.link.eta A B|L] R).
100-
% rule \ (collect-store-aux L R) <=> (R = L).
84+
% If two eta links have same lhs they rhs should unify
85+
rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1))
86+
\ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2))
87+
| (pi x\ relocate L1 L2 (B2 x) (B2' x))
88+
<=> (N1 : G1 ?- B1 = B2').
10189
}
10290

10391
pred eta i:term, i:term.
@@ -114,7 +102,9 @@ namespace tc {
114102
namespace llam {
115103
pred llam i:term, i:term.
116104
llam A (uvar _ S as T) :- distinct_names S, !, A = T.
117-
llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_,A|Vars].
105+
llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars,
106+
coq.say "Declaring constraint" (llam A (app [H|L])) [_,A|Vars],
107+
declare_constraint (llam A (app [H|L])) [_,A|Vars].
118108
llam (fun _ _ _ as F) (app [H | TL]) :-
119109
var H _ Scope, !,
120110
std.drop-last 1 TL TL',
@@ -124,9 +114,14 @@ namespace tc {
124114
pi x\ llam F Bo'.
125115
llam A B :- !, tc.unify-eq A B.
126116

127-
constraint solve-llam solve-llam-t llam {
117+
constraint solve-llam llam {
128118
rule solve-llam \ (llam A B) <=> (A = B).
129119
rule \ solve-llam.
120+
% If two llam links have same lhs they rhs should unify
121+
rule (N1 : G1 ?- llam (uvar X L1) T1)
122+
\ (N2 : G2 ?- llam (uvar X L2) T2)
123+
| (pi x\ relocate L1 L2 T2 T2')
124+
<=> (N1 : G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
130125
}
131126
}
132127

@@ -154,13 +149,6 @@ namespace tc {
154149
(coq.unify-eq V T ok).
155150
cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
156151

157-
% pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
158-
% unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
159-
% unify-rebinding-names [N|NS] T1 [V|VS] T2 C :- !, copy N V => unify-rebinding-names NS T1 VS T2 C.
160-
% unify-rebinding-names [] T1 VS T2 C :- !, unify-rebinding-names [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
161-
% unify-rebinding-names [_|NS] (prod _ _ F) [] T2 C :- !, % FIXME: reduction
162-
% assert! (pi x\ F x = F1) "restriction bug", unify-rebinding-names NS F1 [] T2 C.
163-
164152
pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
165153
unify-under-ctx [] [] A B V1 V2 :- copy A A', copy V1 V1', !, coq.unify-eq A' B ok, !, V1' = V2.
166154
unify-under-ctx [X|XS] [Y|YS] A B V1 V2:- (copy X Y :- !) => unify-under-ctx XS YS A B V1 V2.

‎apps/tc/elpi/solver.elpi‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L.
77

88
namespace tc {
99
pred build-query-from-goal i:term, i:term, o:prop, o:list prop.
10-
build-query-from-goal Goal Proof Q PostProcess :-
11-
tc.compile.goal Goal Goal' PostProcess, !,
10+
build-query-from-goal Goal Proof Q Links :-
11+
tc.compile.goal' Goal Goal' Links, !,
1212
coq.safe-dest-app Goal' (global TC) TL',
1313
std.append TL' [Proof] TL, !,
1414
coq.elpi.predicate {tc.gref->pred-name TC} TL Q.
@@ -29,10 +29,11 @@ namespace tc {
2929

3030
pred solve-under-context i:term, o:term.
3131
solve-under-context Ty Proof :-
32-
tc.time-it tc.oTC-time-compile-goal (build-query-from-goal Ty Proof Q PostProcess) "build query", !,
33-
if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q), !,
32+
tc.time-it tc.oTC-time-compile-goal (build-query-from-goal Ty Proof Q Links) "build query", !,
33+
if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q),
34+
if-true print-links (coq.say "[TC] the links are" Links),
3435
tc.time-it tc.oTC-time-instance-search (
35-
do PostProcess, Q,
36+
do Links, Q,
3637
tc.link.solve-cs,
3738
tc.link.solve-eta, % Trigger eta links
3839
tc.link.solve-llam % Trigger llam links
@@ -59,6 +60,7 @@ namespace tc {
5960
if-true print-goal-pp (coq.say "The goal is <<<" {coq.term->string Ty} ">>>"),
6061
tc.time-it tc.oTC-time-mode-check (tc.modes-check Ty) "mode check", !,
6162
tc.time-it _ (tc.compile.context Ctx CtxClause) "compile context", !,
63+
if-true print-ctx (coq.say "The context is" CtxClause),
6264
CtxClause => solve-under-context Ty Proof.
6365
solve-aux1 _ _ tc.mode_fail :- if-true (print-solution; print-solution-pp) (coq.say "Invalid mode call").
6466

@@ -68,5 +70,7 @@ namespace tc {
6870
pred print-goal-pp. % Print the goal with coq pp
6971
pred print-goal-after-search. % Print the goal in HOAS after instance search
7072
pred print-compiled-goal.
73+
pred print-links.
74+
pred print-ctx.
7175

7276
}

‎apps/tc/tests/bigTest.v‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
Set Warnings "-elpi.TC.hints".
2+
13
From elpi.apps Require Import tc.
24
Elpi TC Solver Override TC.Solver All.
35

‎apps/tc/tests/test.v‎

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
From elpi Require Import tc.
2+
Set Warnings "+elpi".
23

34
Section test_max_arity.
45
Elpi Query TC.Solver lp:{{
@@ -207,23 +208,15 @@ Module HO_81.
207208
Class c1 (T : Type).
208209
Instance i1 F : c1 F. Qed.
209210

210-
Elpi Accumulate TC.Solver lp:{{
211-
:before "compile-goal"
212-
tc.compile.goal Goal _ _ :-
213-
Goal = {{HO_81.c1 lp:_}}, !,
214-
tc.precomp.goal Goal _ Vars, !,
215-
tc.compile.goal.make-pairs Vars Pairs,
216-
std.assert! (Pairs = []) "", fail.
217-
}}.
218-
Elpi Typecheck TC.Solver.
219-
220211
Goal exists X, c1 X.
221212
eexists.
222213
(* Failure is good, since here we simply check that the number of
223214
uvar-pair built by tc.precomp is zero. This is because the type
224215
of ?X is Type (i.e. it has `arity` zero) *)
225-
Fail apply _.
226-
Abort.
216+
apply _.
217+
Unshelve.
218+
apply nat.
219+
Qed.
227220
End HO_81.
228221

229222
Module HO_8.

0 commit comments

Comments
 (0)