Skip to content

solve mixin dependencies via TC #596

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

Open
gares wants to merge 9 commits into
base: master
Choose a base branch
from
+134 −11
Open

solve mixin dependencies via TC #596

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
56e85cd
wip
Tragicus Jun 4, 2026
cc23d4c
wip
Tragicus Jun 4, 2026
9c85b36
use projection instead of unification to extract the mixin from the c…
Tragicus Jun 5, 2026
b8d2401
Revert "use projection instead of unification to extract the mixin fr…
Tragicus Jun 5, 2026
48db6fd
fix Build notation, Build implicits, instance elaboration and clause …
Tragicus Jun 8, 2026
5ec8c23
add alias for Axioms_ with different implicits
Tragicus Jun 8, 2026
06adff4
override tc solver for mixin's axioms_
Tragicus Jun 12, 2026
d111865
fix override
Tragicus Jun 12, 2026
15582e1
declare mixin instances only for the first class
Tragicus Jun 17, 2026
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
4 changes: 2 additions & 2 deletions HB/common/database.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,9 +433,9 @@ has-CS-instance? TyTerm (indt Struct) :-
coq.CS.db-for (const Proj) Pat L,
not(L = []).

pred structure-nparams i:structure, o:int.
func structure-nparams structure -> int.
structure-nparams Structure NParams :-
class-def (class Class Structure _),
class-def (class Class Structure _), !,
factory->nparams Class NParams.

func factory? term -> w-args factoryname.
Expand Down
8 changes: 7 additions & 1 deletion HB/common/stdpp.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,12 @@ constraint print-ctx mixin-src {

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

func coq.mk-n-fun int, (func list term -> term), list term -> term.
coq.mk-n-fun 0 F L R :- !, F {std.rev L} R.
coq.mk-n-fun N F L (fun _ _ (x\ R x)) :-
calc (N - 1) N1,
pi x\ coq.mk-n-fun N1 F [x|L] (R x).

func coq.term-is-gref? term -> gref.
coq.term-is-gref? (global GR) GR.
coq.term-is-gref? (pglobal GR _) GR.
Expand Down Expand Up @@ -364,4 +370,4 @@ constraint seen? seen! purge-seen! {
rule purge-seen! \ (seen! _ _).
rule \ purge-seen!.
}
}
}
26 changes: 21 additions & 5 deletions HB/factory.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -269,7 +269,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
coq.env.indt R tt _ _ _ [K] _,
GRK = indc K,
@global! => log.coq.arguments.set-implicit (indt R) [[]],
@global! => log.coq.arguments.set-implicit GRK [[]],

factories-provide GRFSwP MLwP,
w-params.nparams MLwP NParams,
Expand All @@ -283,9 +282,11 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance

if-verbose (coq.say {header} "declare notation Build"),

GRDepsClauses => coq.env.add-const "Axioms" (global GRK) _ ff GRK0,
GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst BuildAbbrev,

GRDepsClauses => phant.add-abbreviation "Build_" PhGRK BuildConst BuildAbbrev,
calc (NParams + 1) NParams1,
GRDepsClauses => coq.notation.add-abbreviation "Build" NParams1 {coq.mk-n-fun NParams1 (args\ coq.mk-app (global (const GRK0)) {std.append args {coq.mk-n-holes {std.length {list-w-params_list MLwP}}}}) []} tt _,
if-verbose (coq.say {header} "declare notation axioms"),

if (D = asset-mixin)
Expand All @@ -297,6 +298,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
if-verbose (coq.say {header} "start module Exports"),

log.coq.env.begin-module "Exports" none,
coq.TC.declare-class (indt R),
coq.TC.override-solver "TC.Solver" ["axioms_"],
std.flatten [Clauses, GRDepsClauses, [
is-factory (indt R),
factory->constructor (indt R) GRK,
Expand All @@ -309,8 +312,19 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance

list-w-params_list MLwP MLwoP,
std.map MLwoP (_\ r\ r = maximal) Implicits,
std.map {std.iota NParams} (_\ r\ r = explicit) Explicits,
/* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */
@global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],


NewImplicits = [explicit|{std.append Explicits Implicits}],
coq.arguments.set-default-implicit GRK,
coq.arguments.implicit GRK [GRKImplicits|_],
std.drop {std.length NewImplicits} GRKImplicits RImplicits,

if (std.forall RImplicits(x\ x = explicit))
(@global! => log.coq.arguments.set-implicit (const GRK0) [NewImplicits])
(@global! => log.coq.arguments.set-implicit (const GRK0) [NewImplicits, {std.append NewImplicits RImplicits}]),
% @global! => log.coq.coercion.declare FactorySortCoe,

log.coq.env.end-module-name "Exports" Exports,
Expand Down Expand Up @@ -351,6 +365,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance

log.coq.env.end-section-name Module,

% TODO: make the mixins implicit.
@global! => log.coq.arguments.set-implicit GRK [[]],

factories-provide GRFSwP MLwP,
Expand All @@ -363,7 +378,8 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance

if (mixin->first-class F _) (PhGRK = PhGRK0)
(phant.append-fun-unify PhGRK0 PhGRK),
GRDepsClauses => phant.add-abbreviation "Build" PhGRK _ _,
@global! => log.coq.arguments.set-implicit GRK [[]],
GRDepsClauses => coq.notation.add-abbreviation "Build" 0 (global GRK) tt _,

GRDepsClauses => mk-factory-abbrev "axioms" (const C) Clauses FactAbbrev,

Expand Down Expand Up @@ -436,4 +452,4 @@ mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref->deps



}}
}}
20 changes: 19 additions & 1 deletion HB/instance.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,24 @@ declare-existing T0 F0 :- std.do! [
acc-clauses current Clauses,
].

func elaborate-w-tc term -> term, term, diagnostic.
elaborate-w-tc (fun N BTy Skel) (prod N BTy Ty) (fun N BTy Body) Diag :-
@pi-decl N BTy x\ elaborate-w-tc (Skel x) (Ty x) (Body x) Diag.
elaborate-w-tc (app [KFactory|Args]) Ty Body Diag :-
coq.typecheck KFactory TyFactory ok,
coq.prod-tgt->gref TyFactory Factory,
factory->nparams Factory NParams,
std.length {list-w-params_list {gref->deps Factory}} NDeps,
calc (NParams + NDeps + 1) N,
N =< {std.length Args},
std.split-at N Args NArgs Rest,
std.assert-ok! (coq.elaborate-skeleton (app [KFactory|NArgs]) _ Head) "tc resolution of mixins failed",
coq.elaborate-skeleton {coq.mk-app Head Rest} Ty Body Diag.





% [declare-const N B Ty CFL CSL] adds a Definition N : Ty := B where Ty is a factory
% and equips the type the factory is used on with all the canonical structures
% that can be built using factory instance B. CFL contains the list of
Expand All @@ -26,7 +44,7 @@ func declare-const id, term, arity -> list (pair id constant), list (pair id con
declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
coq.arity->term TyWP Ty,
std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
std.assert-ok! (d\ elaborate-w-tc BodySkel Ty Body d; coq.elaborate-skeleton BodySkel Ty Body d) "Definition illtyped",

% handle parameters via a section -- begin
if (TyWP = arity SectionTy) (
Expand Down
52 changes: 51 additions & 1 deletion HB/structure.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@ declare Module BSkel Sort :- std.do! [
std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
std.filter ML (m\ not (mixin->first-class m _)) NewMixins,
std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass,
[class-def CurrentClass, StructKeyClause | GRDepsClauses] => MixinFirstClass => Factories => std.map-i ML (private.mixin-clause Structure) OptMixinClauses,
std.map-filter OptMixinClauses (c\c'\ c = some c') MixinClauses,


if-verbose (coq.say {header} "structure: new mixins" NewMixins),
Expand Down Expand Up @@ -126,10 +128,12 @@ declare Module BSkel Sort :- std.do! [
std.flatten [
Factories, [is-structure Structure],
NewJoins, [class-def CurrentClass], GRDepsClauses,
[gref->deps GRPack MLwP], MixinMems, [StructKeyClause]
[gref->deps GRPack MLwP], MixinMems, [StructKeyClause],
]
NewClauses,
acc-clauses current NewClauses,
std.map MixinClauses (c\ r\ r = clause _ _ c) MixinClauses0,
coq.elpi.accumulate-clauses current "tc.db" MixinClauses0,

if-verbose (coq.say {header} "stop module Exports"),
log.coq.env.end-module-name "Exports" Exports,
Expand Down Expand Up @@ -195,6 +199,52 @@ namespace private {

shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.

func clause.mk-n-pis int, list term, (func list term -> prop) -> prop.
clause.mk-n-pis 0 RArgs P Clause :- !, std.rev RArgs Args, P Args Clause.
clause.mk-n-pis N Args P (pi x\ Clause x) :-
calc (N - 1) N0,
pi x\ clause.mk-n-pis N0 [x|Args] P (Clause x).

func mixin-clause structure, int, mixinname -> option prop.
mixin-clause S I M Clause :-
structure-key SortProj _ S, !,
get-constructor S KS,
class-def (class (indt Class) S CMLwP), !,
if (not (mixin->first-class M (indt Class))) (Clause = none) (
get-constructor (indt Class) KC,
tc.gref->pred-name M PredName,
gref->deps M MDeps,

% tc-...-NModule_isLSemiModule.tc-axioms_ R T isNModule Inst :-
% coq.unify-eq T (Sort R ST) ok,
% coq.unify-eq ST (S.Pack R T CT) ok,
% coq.unify-eq CT (C.Axioms_ R T isNModule NModule_isLSemiModule),
% std.nth 1 [isNModule, NModule_isLSemiModule] Inst.
clause.mk-n-pis {structure-nparams S} [] (Params\ clause\
clause.mk-n-pis {factory->nparams M} [] (MParams\ clause\
clause.mk-n-pis {std.length {list-w-params_list CMLwP}} [] (MIL\ clause\
clause.mk-n-pis {std.length {list-w-params_list MDeps}} [] (MHDeps\ clause\
sigma Clause' MILI\
std.take I MIL MILI,
clause = (pi T ST CT Inst\ Clause' T ST CT Inst),
pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C\
std.append Params [ST] ParamsST,
coq.mk-app (global (const SortProj)) ParamsST SortParamsST,
coq.mk-app (global KS) {std.append Params [T, CT]} KSParamsC,
coq.mk-app (global KC) {std.append Params [T | MIL]} CBody,
coq.elpi.predicate PredName {std.append MParams {std.append [T | MHDeps] [Inst]}} C,
Clause' T ST CT Inst = (C :-
coq.unify-eq T SortParamsST ok,
coq.unify-eq ST KSParamsC ok,
coq.unify-eq CT CBody ok,
std.nth I MIL Inst)
) clause) clause) clause) Clause',
Clause = some Clause').





% const Po : forall p1 .. pm T m1 .. mn, Extra (Eg Extra = forall x y, x + y = y + z)
% const C : forall p1 .. pm s, Extra
% Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs
Expand Down
35 changes: 34 additions & 1 deletion HB/structures.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,11 @@
Definition ignore_disabled {T T'} (x : T) (x' : T') := x'.

(* ********************* structures ****************************** *)
From elpi Require Import elpi.
From elpi Require Import elpi tc.

From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.

Elpi TC Solver Override TC.Solver None.

Register unify as hb.unify.
Register id_phant as hb.id.
Expand Down Expand Up @@ -306,6 +310,7 @@

#[arguments(raw)] Elpi Command HB.about.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Expand Down Expand Up @@ -340,6 +345,7 @@

#[arguments(raw)] Elpi Command HB.howto.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -382,6 +388,7 @@

#[arguments(raw)] Elpi Command HB.status.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -412,6 +419,7 @@

#[arguments(raw)] Elpi Command HB.graph.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -460,7 +468,10 @@
*)

#[arguments(raw)] Elpi Command HB.mixin.
Elpi Accumulate Plugin "tc-builtin.elpi".

Check failure on line 471 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Builtins for file tc-builtin.elpi were not declared

Check failure on line 471 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.1) 

Builtins for file tc-builtin.elpi were not declared

Check failure on line 471 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (8.20) 

Builtins for file tc-builtin.elpi were not declared
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File tc_aux.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -543,6 +554,7 @@

Elpi Tactic HB.pack_for.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand All @@ -566,6 +578,7 @@

Elpi Tactic HB.pack.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -641,7 +654,10 @@
*)

#[arguments(raw)] Elpi Command HB.structure.
Elpi Accumulate Plugin "tc-builtin.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File tc_aux.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -724,7 +740,10 @@
*)

#[arguments(raw)] Elpi Command HB.saturate.
Elpi Accumulate Plugin "tc-builtin.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File tc_aux.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -775,6 +794,7 @@

#[arguments(raw)] Elpi Command HB.instance.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -816,7 +836,10 @@
(** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)

#[arguments(raw)] Elpi Command HB.factory.
Elpi Accumulate Plugin "tc-builtin.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File tc_aux.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -899,7 +922,10 @@
*)

#[arguments(raw)] Elpi Command HB.builders.
Elpi Accumulate Plugin "tc-builtin.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File tc_aux.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -941,6 +967,7 @@

#[arguments(raw)] Elpi Command HB.end.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -1015,6 +1042,7 @@

#[arguments(raw)] Elpi Command HB.export.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -1061,6 +1089,7 @@

#[arguments(raw)] Elpi Command HB.reexport.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -1143,7 +1172,10 @@
*)

#[arguments(raw)] Elpi Command HB.declare.
Elpi Accumulate Plugin "tc-builtin.elpi".
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File tc_aux.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down Expand Up @@ -1180,6 +1212,7 @@

#[arguments(raw)] Elpi Command HB.check.
Elpi Accumulate Db hb.db.
Elpi Accumulate Db tc.db.
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Expand Down
Loading