Skip to content
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

Jump to bottom

#[primitive] HB.mixin breaks the types of constants lifting mixin projections #386

Open
pi8027 opened this issue Sep 14, 2023 · 6 comments · May be fixed by #423
Open

#[primitive] HB.mixin breaks the types of constants lifting mixin projections #386

pi8027 opened this issue Sep 14, 2023 · 6 comments · May be fixed by #423

Comments

@pi8027
Copy link
Member

pi8027 commented Sep 14, 2023

Example:

From Coq Require Import ssreflect ssrfun.
From HB Require Import structures.

#[primitive]
HB.mixin Record AddMonoid_of_TYPE S := {
  zero : S;
  add : S -> S -> S;
  addrA : associative add;
  add0r : left_id zero add;
  addr0 : right_id zero add;
}.

HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.

Check addrA.
(*
addrA
     : associative (AddMonoid_of_TYPE.add _ (AddMonoid.class ?s))
where
?s : [ |- AddMonoid.type]
*)

The type of addrA should be associative add.
@gares
Copy link
Member

gares commented Sep 14, 2023

Iirc there is a piece of code cleaning up the type. I guess it is broken if the primitive term constructors shows up

@pi8027
Copy link
Member Author

pi8027 commented Sep 29, 2023

@gares Can you point out the part of the code declaring these constants and synthesizing their types? I have a rough idea of how to fix the issue.

@gares
Copy link
Member

gares commented Sep 29, 2023

clean-op-ty in structure.elpi is what I suspect messes up things.

@gares
Copy link
Member

gares commented Sep 29, 2023

hierarchy-builder/HB/structure.elpi

Lines 201 to 237 in 7d4f095

% 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
pred clean-op-ty i:list prop, i:term, i:term, o:term.
clean-op-ty [] _ T1 T2 :- copy T1 T2.
clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
gref-deps (const Po) MLwP,
w-params.nparams MLwP NParams,
std.length {list-w-params_list MLwP} NMixins,
(pi L L1 L2 Params Rest PoArgs\
copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
std.split-at NParams L Params [_|Rest],
std.drop NMixins Rest PoArgs,
std.append Params [S|PoArgs] L1,
std.map L1 copy L2) =>
clean-op-ty Ops S T1 T2.
pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
i:list term, i:term, i:w-args A, o:pair term term.
operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ ParamsOp _) (pr Bo Ty) :- std.do! [
mk-app (global Struct) Params StructType,
mk-app Psort Params PsortP,
mk-app Pclass Params PclassP,
Bo = fun `s` StructType Body,
Ty = prod `s` StructType BodyTy,
(@pi-decl `s` StructType s\ sigma Carrier Class\ std.do! [
mk-app PsortP [s] Carrier,
mk-app PclassP [s] Class,
synthesis.under-mixin-src-from-factory.do! Carrier Class [
% just in case..
synthesis.infer-all-gref-deps ParamsOp Carrier (const Poperation) (Body s),
std.assert-ok! (coq.typecheck (Body s) (DirtyTy s)) "export-1-operation: Body illtyped",
clean-op-ty EXI s (DirtyTy s) (BodyTy s),
],
]),
].

@pi8027
Copy link
Member Author

pi8027 commented Sep 29, 2023 •
edited
Loading

Thanks. I believe that constructing the types of these constants from the declaration of the record type is much easier than doing so from the types of the projections. While the latter requires some replacements using copy (as we can see in clean-op-ty), the former should be just a matter of substitution.

@pi8027
Copy link
Member Author

pi8027 commented Sep 29, 2023

I will take a closer look when I have some time.

This was referenced Feb 1, 2024
Merged
Open
@gares gares linked a pull request Jun 13, 2024 that will close this issue
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix #386 math-comp/hierarchy-builder
2 participants
@pi8027 @gares