Skip to content

remove dead-code #533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 26, 2025
Merged

remove dead-code #533

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 0 additions & 3 deletions HB/builders.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,6 @@ builders.end :- std.do! [
acc-clauses current Clauses,
acc-clauses current ExportClausesFiltered,

% Clauses => ExportClausesFiltered => current-mode no-builder =>
% instance.declare-factory-sort-factory GR,

log.coq.env.end-module-name Name Exports,
log.coq.env.end-module-name ModName _,
export.module {calc (ModName ^ "." ^ Name)} Exports,
Expand Down
4 changes: 0 additions & 4 deletions HB/factory.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -294,8 +294,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
@global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],
% @global! => log.coq.coercion.declare FactorySortCoe,

% NewClauses => instance.declare-factory-sort-deps (indt R),

log.coq.env.end-module-name "Exports" Exports,
log.coq.env.end-module-name Module _,

Expand Down Expand Up @@ -366,8 +364,6 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
acc-clauses current NewClauses,
%@global! => log.coq.coercion.declare FactorySortCoe,

% NewClauses => instance.declare-factory-sort-deps (const C),

log.coq.env.end-module-name "Exports" Exports,
log.coq.env.end-module-name Module _,

Expand Down
66 changes: 0 additions & 66 deletions HB/instance.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,72 +191,6 @@ decl-const-in-struct Name S STy CS:- std.do![
if-verbose (coq.say {header} "structure instance" Name "declared"),
].


pred declare-factory-sort-deps i:gref.
declare-factory-sort-deps GR :- std.do! [
if-verbose (coq.say {header} "required instances on factory sort for" GR),
Name is "SortInstances" ^ {std.any->string {new_int}},
log.coq.env.begin-module Name none,
log.coq.env.begin-section Name,
mk-factory-sort-deps GR CSL,
log.coq.env.end-section-name Name,
log.coq.env.end-module-name Name _,
std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
].

pred declare-factory-sort-factory i:gref.
declare-factory-sort-factory GR :- std.do! [
if-verbose (coq.say {header} "required instances on factory sort for" GR),
Name is "SortInstances" ^ {std.any->string {new_int}},
log.coq.env.begin-module Name none,
log.coq.env.begin-section Name,
mk-factory-sort-factory GR CFL CSL,
log.coq.env.end-section-name Name,
log.coq.env.end-module-name Name _,
std.forall {std.append CFL CSL} (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
].

pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant.

pred mk-factory-sort-deps i:gref, o:list (pair id constant).
mk-factory-sort-deps AliasGR CSL :- std.do! [
std.assert-ok! (factory-alias->gref AliasGR GR) "HB: mk-factory-sort-deps",
gref-deps GR MLwPRaw,
context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
log.coq.env.add-section-variable-noimplicits "f" FSort CF,
GCF = global (const CF),
factory-sort (coercion GRFSort _ GR _),
SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GRFSort KSort,
coq.mk-app KSort [GCF] KFSortEta,
list-w-params_list MLwP ML,
std.length ML NMLArgs,
coq.mk-n-holes NMLArgs SortMLHoles,
std.append {std.append SortParams [SortKey|SortMLHoles]} [GCF] KFSortArgs,
coq.mk-app (global GRFSort) KFSortArgs KFSort,
std.assert-ok! (coq.unify-eq KFSortEta KFSort) "HB: KRSort not an app",
std.map SortMSL
(c\ o\ sigma m t\ c = mixin-src _ m t, o = mixin-src KFSort m t)
KFSortMSL,
KFSortMSL =>
synthesis.under-mixin-src-from-factory.do! KFSort GCF
[declare-all KFSort {findall-classes-for ML} CSL]
].

pred mk-factory-sort-factory i:gref, o:list (pair id constant), o:list (pair id constant).
mk-factory-sort-factory AliasGR CFL CSL :- std.do! [
std.assert-ok! (factory-alias->gref AliasGR GR) "HB",
gref-deps GR MLwPRaw,
context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
log.coq.env.add-section-variable-noimplicits "f" FSort CF,
std.length {list-w-params_list MLwP} NMLArgs,
coq.mk-n-holes NMLArgs SortMLHoles,
GCF = global (const CF),
coq.mk-app (global GR) {std.append SortParams [GCF|SortMLHoles]} FGCF,
declare-const "_" GCF (arity FGCF) CFL CSL
].

% create instances for all possible combinations of types and structure compatible
pred saturate-instances i:cs-pattern.
saturate-instances Filter :- std.do! [
Expand Down
Loading