Skip to content

Commit 873e45e

Browse files
FissoreDFissoreD
committed
refactor option names
1 parent ebf039f commit 873e45e

File tree

4 files changed

+47
-26
lines changed

4 files changed

+47
-26
lines changed

‎apps/tc/elpi/solver.elpi‎

Lines changed: 24 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,16 @@
11
/* license: GNU Lesser General Public License Version 2.1 or later */
22
/* ------------------------------------------------------------------------- */
33

4+
pred time-solve i:prop.
5+
time-solve P :-
6+
std.time P Time,
7+
if (is-option-active {oTC-time}) (coq.say "[TC] Total resolution time is:" Time) true.
8+
49
msolve L N :- !,
5-
coq.ltac.all (coq.ltac.open solve) {std.rev L} N.
10+
time-solve (coq.ltac.all (coq.ltac.open solve-aux) {std.rev L} N).
11+
12+
solve A L :- time-solve (solve-aux A L).
13+
614

715
pred build-context-clauses i:list prop, o:list prop.
816
% Add the section's definition to the given context
@@ -20,48 +28,49 @@ tc-recursive-search Ty Sol :-
2028
std.time (coq.safe-dest-app Ty (global TC) TL',
2129
std.append TL' [Sol] TL,
2230
coq.elpi.predicate {gref->pred-name TC} TL Q, Q) Time,
23-
if (is-option-active {oTC-resolution-time}) (coq.say "Instance search" Time) true.
31+
if (is-option-active {oTC-time-instance-search}) (coq.say "[TC] Instance search time is:" Time) true.
2432

2533
:if "solve-print-goal"
2634
solve (goal Ctx _ Ty _ _) _ :-
2735
coq.say "Ctx" Ctx "Ty" Ty, fail.
2836

29-
% solve (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
37+
pred solve-aux i:goal, o:list sealed-goal.
38+
% solve-aux (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
3039
% @pi-decl N Ty x\
3140
% declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
32-
% solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
41+
% solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
3342
% if (Sol x = app [HD, x]) (S = HD) (S = fun N Ty Sol).
34-
% solve (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
43+
% solve-aux (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
3544
% % intros_if_needed Prod C []
3645
% (@pi-decl N Ty x\
3746
% declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
38-
% solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
47+
% solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
3948
% coq.safe-dest-app (Sol x) Hd (Args x)),
4049
% if (pi x\ last-no-error (Args x) x, std.drop-last 1 (Args x) NewArgs)
4150
% (coq.mk-app Hd NewArgs Out, refine Out G GL) (
4251
% % coq.say "Not eta" (Sol x) x (fun N Ty Sol),
4352
% XX = (fun N Ty Sol)).
44-
% solve (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
53+
% solve-aux (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
4554
% declare-evar C T P S',
4655
% G' = (goal C T P S' A),
4756
% refine (fun N _ _) G' GL1,
48-
% coq.ltac.all (coq.ltac.open solve) GL1 _,
57+
% coq.ltac.all (coq.ltac.open solve-aux) GL1 _,
4958
% refine S' G GL.
50-
solve (goal C _ (prod N Ty F) _ _ as G) GL :- !,
59+
solve-aux (goal C _ (prod N Ty F) _ _ as G) GL :- !,
5160
(@pi-decl N Ty x\
5261
declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
53-
solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
62+
solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
5463
if (pi x\
5564
% also check the head does not contain x
5665
coq.safe-dest-app (Sol x) Hd (Args x),
5766
last-no-error (Args x) x,
5867
std.drop-last 1 (Args x) NewArgs)
5968
(coq.mk-app Hd NewArgs Out, refine Out G GL1) (refine (fun N _ _) G GL1),
60-
coq.ltac.all (coq.ltac.open solve) GL1 GL.
61-
% solve (goal _ _ (prod N _ _) _ _ as G) GL :- !,
69+
coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
70+
% solve-aux (goal _ _ (prod N _ _) _ _ as G) GL :- !,
6271
% refine (fun N _ _) G GL1,
63-
% coq.ltac.all (coq.ltac.open solve) GL1 GL.
64-
solve (goal Ctx _ Ty Sol _ as G) GL :-
72+
% coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
73+
solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
6574
var Sol,
6675
build-context-clauses Ctx Clauses,
6776
% @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1,
@@ -74,7 +83,7 @@ solve (goal Ctx _ Ty Sol _ as G) GL :-
7483
if (is-option-active {oTC-ignore-eta-reduction})
7584
(Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
7685
std.time (refine Proof' G GL) Refine-Time,
77-
if (is-option-active {oTC-time-refine}) (coq.say "Refine Time" Refine-Time) true;
86+
if (is-option-active {oTC-time-refine}) (coq.say "[TC] Refine time is:" Refine-Time) true;
7887
coq.error "illtyped solution:" {coq.term->string Proof}
7988
)
8089
(GL = [seal G]).

‎apps/tc/theories/add_commands.v‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,10 @@ Elpi Accumulate File base.
4343
Elpi Accumulate File tc_aux.
4444
Elpi Accumulate File create_tc_predicate.
4545
Elpi Accumulate lp:{{
46-
main _ :-
47-
coq.TC.db-tc TC,
48-
std.forall TC (add-class-gr classic).
46+
% Ignore is the list of classes we do not want to add
47+
main IgnoreStr :-
48+
std.map IgnoreStr (x\r\ sigma S\ str S = x, coq.locate S r) IgnoreGR,
49+
std.forall {coq.TC.db-tc} (x\ if (std.mem IgnoreGR x) true (add-class-gr classic x)).
4950
}}.
5051
Elpi Typecheck.
5152

‎apps/tc/theories/db.v‎

Lines changed: 18 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,21 +11,34 @@ Elpi Db tc_options.db lp:{{
1111
pred oTC-ignore-eta-reduction o:list string.
1212
oTC-ignore-eta-reduction ["TC", "IgnoreEtaReduction"].
1313

14-
pred oTC-resolution-time o:list string.
15-
oTC-resolution-time ["TC", "ResolutionTime"].
14+
% Time taken by only instance search (we time tc-recursive-search)
15+
pred oTC-time-instance-search o:list string.
16+
oTC-time-instance-search ["TC", "Time", "Instance", "Search"].
1617

17-
pred oTC-clauseNameShortName o:list string.
18-
oTC-clauseNameShortName ["TC", "NameShortPath"].
18+
% Time taken by the whole search in tc
19+
pred oTC-time o:list string.
20+
oTC-time ["TC", "Time"].
1921

22+
% Time taken to refine the solution
2023
pred oTC-time-refine o:list string.
21-
oTC-time-refine ["TC", "TimeRefine"].
24+
oTC-time-refine ["TC", "Time", "Refine"].
25+
26+
pred oTC-clauseNameShortName o:list string.
27+
oTC-clauseNameShortName ["TC", "NameShortPath"].
2228

2329
pred oTC-debug o:list string.
2430
oTC-debug ["TC", "Debug"].
2531

2632
pred oTC-use-pattern-fragment-compiler o:list string.
2733
oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].
2834

35+
pred all-options o:list ((list string) -> prop).
36+
all-options [
37+
oTC-ignore-eta-reduction, oTC-time-refine, oTC-time,
38+
oTC-clauseNameShortName, oTC-time-instance-search, oTC-debug,
39+
oTC-use-pattern-fragment-compiler
40+
].
41+
2942
pred is-option-active i:list string.
3043
is-option-active Opt :-
3144
coq.option.get Opt (coq.option.bool tt).

‎apps/tc/theories/tc.v‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,9 +45,7 @@ Elpi Accumulate File create_tc_predicate.
4545
Elpi Accumulate File solver.
4646
Elpi Query lp:{{
4747
sigma Options\
48-
Options = [oTC-ignore-eta-reduction, oTC-resolution-time,
49-
oTC-clauseNameShortName, oTC-time-refine, oTC-debug,
50-
oTC-use-pattern-fragment-compiler],
48+
all-options Options,
5149
std.forall Options (x\ sigma Args\ x Args,
5250
coq.option.add Args (coq.option.bool ff) ff).
5351
}}.

0 commit comments

Comments
 (0)