Skip to content

Commit 16318c8

Browse files
proux01proux01
committed
Remove unused eta expansion
Compilation of MathComp: before: 20:36 (1.26 GB) HB.structure: 03:10 HB.instance: 02:29 after: 17:46 (1.24 GB) HB.structure: 01:37 HB.instance: 02:18
1 parent dd5d0f8 commit 16318c8

File tree

7 files changed

+21
-76
lines changed

7 files changed

+21
-76
lines changed

‎HB/structure.elpi‎

Lines changed: 1 addition & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -160,37 +160,14 @@ declare Module BSkel Sort :- std.do! [
160160

161161
@global! => log.coq.notation.add-abbreviation "on" 1
162162
{{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
163-
OnAbbrev,
164-
165-
log.coq.env.begin-module "EtaAndMixinExports" none,
166-
167-
if (get-option "primitive" tt) true (
168-
if-verbose (coq.say {header} "eta expanded instances"),
169-
NewClauses => std.do! [
170-
w-params.fold MLwP mk-fun
171-
(private.mk-hb-eta.on Structure SortProjection OnAbbrev) EtaInstanceBody,
172-
w-params.fold MLwP (mk-parameter explicit)
173-
(private.mk-hb-eta.arity Structure ClassName SortProjection)
174-
EtaInstanceArity,
175-
instance.declare-const "_" EtaInstanceBody EtaInstanceArity _
176-
]
177-
),
178-
179-
% std.flatten {std.map NewMixins mixin->factories} NewFactories,
180-
% NewClauses => std.forall NewFactories instance.declare-factory-sort-factory,
181-
182-
log.coq.env.end-module-name "EtaAndMixinExports" EtaExports,
163+
_OnAbbrev,
183164

184165
log.coq.env.end-module-name Module ModulePath,
185166

186167
if-verbose (coq.say {header} "end modules; export" Exports),
187168

188169
export.module {calc (Module ^ ".Exports")} Exports,
189170

190-
if-verbose (coq.say {header} "export" EtaExports),
191-
192-
export.module {calc (Module ^ ".EtaAndMixinExports")} EtaExports,
193-
194171
if-verbose (coq.say {header} "exporting operations"),
195172
ClassAlias => Factories => GRDepsClauses =>
196173
private.export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,
@@ -681,32 +658,4 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :-
681658
@pi-decl N Ty t\
682659
product->triples (B t) (Rest t) C.
683660

684-
pred mk-hb-eta.on i:structure, i:term, i:abbreviation,
685-
i:list term, i:name, i:term, i:A, o:term.
686-
mk-hb-eta.on Structure SortProjection OnAbbrev
687-
Params NT _T _ (fun NT Ty Body) :- !, std.do! [
688-
coq.mk-app (global Structure) Params Ty,
689-
@pi-decl NT Ty s\ sigma Tm\ std.do! [
690-
coq.mk-app {{lib:@hb.eta}}
691-
[_, {coq.mk-app SortProjection {std.append Params [s]}}]
692-
Tm,
693-
std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
694-
coq.notation.abbreviation OnAbbrev [Tm] (Body s)
695-
]
696-
].
697-
698-
pred mk-hb-eta.arity i:structure, i:classname, i:term, i:list term,
699-
i:name, i:term, i:A, o:arity.
700-
mk-hb-eta.arity Structure ClassName SortProjection
701-
Params NT _T _ Out :- !, std.do! [
702-
coq.mk-app (global Structure) Params Ty,
703-
(@pi-decl NT Ty s\ sigma Tm\ std.do! [
704-
coq.mk-app {{lib:@hb.eta}}
705-
[_, {coq.mk-app SortProjection {std.append Params [s]}}] Tm,
706-
std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
707-
coq.mk-app (global ClassName) {std.append Params [Tm]} (Concl s)
708-
]),
709-
Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s)
710-
].
711-
712661
}}

‎tests/about.v.out‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,6 @@ HB: add comes from mixin AddMonoid_of_TYPE
112112
HB: AddAG.sort is a canonical projection
113113
(from "./examples/demo1/hierarchy_5.v", line 73)
114114
HB: AddAG.sort has the following canonical values:
115-
- @eta
116115
- Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
117116
- Z
118117

@@ -135,7 +134,6 @@ HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
135134
HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
136135
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
137136

138-
HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid
139137
HB: synthesized in file File "(stdin)", line 5, column 0, character 127:
140138
Interactive Module hierarchy_5 started
141139
Interactive Module AddComoid started

‎tests/about.v.out.15‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,6 @@ HB: add comes from mixin AddMonoid_of_TYPE
112112
HB: AddAG.sort is a canonical projection
113113
(from "./examples/demo1/hierarchy_5.v", line 73)
114114
HB: AddAG.sort has the following canonical values:
115-
- @eta
116115
- Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
117116
- Z
118117

@@ -135,7 +134,6 @@ HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
135134
HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
136135
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
137136

138-
HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid
139137
HB: synthesized in file File "(stdin)", line 5, column 122, character 127:
140138
Interactive Module hierarchy_5 started
141139
Interactive Module AddComoid started

‎tests/hnf.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,9 @@ HB.end.
1010

1111
#[hnf] HB.instance Definition _ := f.Build nat (3 + 2).
1212
Print Datatypes_nat__canonical__hnf_S.
13-
Print HB_unnamed_mixin_12.
13+
Print HB_unnamed_mixin_8.
1414

1515
HB.instance Definition _ := f.Build bool (3 + 2).
1616
Print Datatypes_bool__canonical__hnf_S.
17-
Print HB_unnamed_mixin_16.
17+
Print HB_unnamed_mixin_12.
1818

‎tests/hnf.v.out‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
Datatypes_nat__canonical__hnf_S =
2-
{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
2+
{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |}
33
: S.type
4-
HB_unnamed_mixin_12 =
5-
{| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
4+
HB_unnamed_mixin_8 =
5+
{| M.x := f.y nat HB_unnamed_factory_6 + 1 |}
66
: M.axioms_ nat
77
Datatypes_bool__canonical__hnf_S =
8-
{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
8+
{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
99
: S.type
10-
HB_unnamed_mixin_16 =
11-
Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
10+
HB_unnamed_mixin_12 =
11+
Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9
1212
: M.axioms_ bool

‎tests/hnf.v.out.15‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
Datatypes_nat__canonical__hnf_S =
2-
{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
2+
{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |}
33
: S.type
4-
HB_unnamed_mixin_12 =
5-
{| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
4+
HB_unnamed_mixin_8 =
5+
{| M.x := f.y nat HB_unnamed_factory_6 + 1 |}
66
: M.axioms_ nat
77
Datatypes_bool__canonical__hnf_S =
8-
{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
8+
{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
99
: S.type
10-
HB_unnamed_mixin_16 =
11-
Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
10+
HB_unnamed_mixin_12 =
11+
Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9
1212
: M.axioms_ bool

‎tests/hnf.v.out.16‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
Datatypes_nat__canonical__hnf_S =
2-
{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
2+
{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |}
33
: S.type
4-
HB_unnamed_mixin_12 =
5-
{| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
4+
HB_unnamed_mixin_8 =
5+
{| M.x := f.y nat HB_unnamed_factory_6 + 1 |}
66
: M.axioms_ nat
77
Datatypes_bool__canonical__hnf_S =
8-
{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
8+
{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
99
: S.type
10-
HB_unnamed_mixin_16 =
11-
Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
10+
HB_unnamed_mixin_12 =
11+
Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9
1212
: M.axioms_ bool

0 commit comments

Comments
 (0)