Skip to content

Commit 87fe610

Browse files
FissoreDFissoreD
committed
refactor imports in apps/tc
1 parent 0807188 commit 87fe610

File tree

9 files changed

+23
-25
lines changed

9 files changed

+23
-25
lines changed

‎apps/tc/elpi/alias.elpi‎

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

4+
accumulate base.
5+
46
pred alias i:term, o:term.
57

68
pred replace-with-alias.aux i:list term, o:list term, o:bool.

‎apps/tc/elpi/compiler.elpi‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
/* license: GNU Lesser General Public License Version 2.1 or later */
22
/* ------------------------------------------------------------------------- */
33

4+
accumulate base.
5+
accumulate tc_aux.
6+
47
% returns the classes on which the current gref depends
58
pred get-class-dependencies i:gref, o:list gref.
69
get-class-dependencies GR Res :-

‎apps/tc/elpi/create_tc_predicate.elpi‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
/* license: GNU Lesser General Public License Version 2.1 or later */
22
/* ------------------------------------------------------------------------- */
3+
4+
accumulate base.
5+
accumulate tc_aux.
6+
37
pred string->coq-mode i:string, o:hint-mode.
48
string->coq-mode "bang" mode-ground :- !.
59
string->coq-mode "plus" mode-input :- !.

‎apps/tc/elpi/parser_addInstances.elpi‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
/* license: GNU Lesser General Public License Version 2.1 or later */
22
/* ------------------------------------------------------------------------- */
33

4+
accumulate base.
5+
accumulate tc_aux.
6+
accumulate compiler.
7+
48
kind enum type.
59
type path string -> string -> enum.
610
type addInstPrio int -> string -> enum.

‎apps/tc/elpi/rewrite_forward.elpi‎

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

4+
accumulate base.
5+
46
pred forward i:term, o:term, o:list (pair (list term) term).
57

68
% Auxiliary function for rewrite-forward

‎apps/tc/elpi/solver.elpi‎

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

4+
accumulate base.
5+
46
pred time-solve i:prop.
57
time-solve P :-
68
std.time P Time,

‎apps/tc/elpi/tc_aux.elpi‎

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

4+
accumulate base.
5+
46
% Contains the list of classes that
57
% cannot be compiled
68

‎apps/tc/theories/add_commands.v‎

Lines changed: 1 addition & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -3,18 +3,14 @@
33

44
From elpi.apps Require Import db.
55

6-
From elpi.apps.tc Extra Dependency "base.elpi" as base.
76
From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
87
From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
98
From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
10-
From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
119
From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
1210

1311
Elpi Command TC.AddAllInstances.
1412
Elpi Accumulate Db tc.db.
1513
Elpi Accumulate Db tc_options.db.
16-
Elpi Accumulate File base.
17-
Elpi Accumulate File tc_aux.
1814
Elpi Accumulate File compiler.
1915
Elpi Accumulate lp:{{
2016
main L :-
@@ -26,9 +22,6 @@ Elpi Typecheck.
2622
Elpi Command TC.AddInstances.
2723
Elpi Accumulate Db tc.db.
2824
Elpi Accumulate Db tc_options.db.
29-
Elpi Accumulate File base.
30-
Elpi Accumulate File tc_aux.
31-
Elpi Accumulate File compiler.
3225
Elpi Accumulate File parser_addInstances.
3326
Elpi Accumulate lp:{{
3427
main Arguments :-
@@ -39,8 +32,6 @@ Elpi Typecheck.
3932
Elpi Command TC.AddAllClasses.
4033
Elpi Accumulate Db tc.db.
4134
Elpi Accumulate Db tc_options.db.
42-
Elpi Accumulate File base.
43-
Elpi Accumulate File tc_aux.
4435
Elpi Accumulate File create_tc_predicate.
4536
Elpi Accumulate lp:{{
4637
% Ignore is the list of classes we do not want to add
@@ -53,8 +44,6 @@ Elpi Typecheck.
5344
Elpi Command TC.AddClasses.
5445
Elpi Accumulate Db tc.db.
5546
Elpi Accumulate Db tc_options.db.
56-
Elpi Accumulate File base.
57-
Elpi Accumulate File tc_aux.
5847
Elpi Accumulate File create_tc_predicate.
5948
Elpi Accumulate lp:{{
6049
main L :-
@@ -68,9 +57,8 @@ Elpi Typecheck.
6857
Elpi Command TC.AddHook.
6958
Elpi Accumulate Db tc.db.
7059
Elpi Accumulate Db tc_options.db.
71-
Elpi Accumulate File base.
72-
Elpi Accumulate File tc_aux.
7360
Elpi Accumulate lp:{{
61+
accumulate elpi/tc_aux.
7462
pred addHook i:grafting, i:string.
7563
addHook Grafting NewName :-
7664
@global! => add-tc-db NewName Grafting (hook NewName).
@@ -99,8 +87,6 @@ Elpi Typecheck.
9987
Elpi Command TC.Declare.
10088
Elpi Accumulate Db tc.db.
10189
Elpi Accumulate Db tc_options.db.
102-
Elpi Accumulate File base.
103-
Elpi Accumulate File tc_aux.
10490
Elpi Accumulate File create_tc_predicate.
10591
Elpi Accumulate lp:{{
10692
main [indt-decl D] :- declare-class D.

‎apps/tc/theories/tc.v‎

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,8 @@
33

44
Declare ML Module "coq-elpi-tc.plugin".
55

6-
From elpi.apps.tc Extra Dependency "base.elpi" as base.
76
From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
8-
From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
97
From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
10-
From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
118
From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
129

1310
From elpi.apps Require Import db.
@@ -38,14 +35,13 @@ Elpi Typecheck.
3835
Elpi Tactic TC.Solver.
3936
Elpi Accumulate Db tc.db.
4037
Elpi Accumulate Db tc_options.db.
41-
Elpi Accumulate File base.
42-
Elpi Accumulate File tc_aux.
4338
Elpi Accumulate File compiler.
4439
Elpi Accumulate File create_tc_predicate.
4540
Elpi Accumulate File solver.
4641
Elpi Query lp:{{
4742
sigma Options\
48-
std.forall {all-options} (x\ sigma L\ x L,
43+
all-options Options,
44+
std.forall Options (x\ sigma L\ x L,
4945
coq.option.add L (coq.option.bool ff) ff).
5046
}}.
5147
Elpi Typecheck.
@@ -62,8 +58,6 @@ Elpi Query lp:{{
6258
Elpi Command TC.Compiler.
6359
Elpi Accumulate Db tc.db.
6460
Elpi Accumulate Db tc_options.db.
65-
Elpi Accumulate File base.
66-
Elpi Accumulate File tc_aux.
6761
Elpi Accumulate File create_tc_predicate.
6862
Elpi Accumulate File compiler.
6963
Elpi Accumulate lp:{{
@@ -87,9 +81,8 @@ Elpi Typecheck.
8781
Elpi Command TC.Set_deterministic.
8882
Elpi Accumulate Db tc.db.
8983
Elpi Accumulate Db tc_options.db.
90-
Elpi Accumulate File base.
91-
Elpi Accumulate File tc_aux.
9284
Elpi Accumulate lp:{{
85+
accumulate elpi/tc_aux.
9386
main [str ClassStr] :-
9487
coq.locate ClassStr ClassGR,
9588
std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class",

0 commit comments

Comments
 (0)