Christian Doczkal (Jul 20 2020 at 15:51): Christian Doczkal (Jul 20 2020 at 15:51):It seems I have a knack for breaking things. The following was an attempt at defining a "type whose elements can be seen as elements of another structure":
From HB Require Import structures.
HB.mixin Record Setoid_of_Type A :=
{ eqv : A -> A -> Prop ; foo : True }.
HB.structure Definition Setoid := { A of Setoid_of_Type A }.
Infix "≡" := eqv (at level 79).
Section Sub.
Variable (A : Type) (X : Setoid.type).
HB.mixin Record Sub_for_Type := { elem : A -> Setoid.sort X }.
(* Error: Anomaly "File "kernel/safe_typing.ml", line 413, characters 2-8: Assertion failed." *)
Not sure that's the most reasonable thing to do, but getting anomalies from kernel/safe_typing.ml probably isn't what an HB command is supposed to do.
Enrico Tassi (Jul 20 2020 at 15:58):Hum, I guess I really need to improve this error ;-)
The problem is that HB.mixin starts a module, but you are inside a section.
Enrico Tassi (Jul 20 2020 at 16:04):I've just pushed a commit to (coq-elpi) master, it now says: "Error: This elpi code cannot be run within a section since it opens a module"
Christian Doczkal (Jul 20 2020 at 16:08):I see. So while one can define parametric instances within sections, one really has to list the parameters for parametric mixins.
Christian Doczkal (Jul 20 2020 at 16:26):Well, replacing everything following the Infix command with:
HB.mixin Record Refl_of_Type (X : Setoid.type) (A : Type) :=
{ elem_of : A -> Setoid.sort X; reflP (a : A) : (elem_of a) ≡ (elem_of a) }.
I get:
ty-deps: BUG: could not get the parameters and the dependencies of
(forall (X : Setoid.type) (A : Type) (elem_of : A -> X), (forall a : A, elem_of a ≡ elem_of a) -> axioms_ X A)
:grinning:
Enrico Tassi (Jul 20 2020 at 17:24):This is probably undocumented.
You should "flag" the type A with something like (A : indexed Type) where indexed is an identity function defined on top of the structures.v file
Enrico Tassi (Jul 20 2020 at 17:34): Christian Doczkal (Jul 20 2020 at 18:03):I'm not sure to follow. If I replace (A : Type) with (A : indexed Type), then the error persists unchanged. In particular, the error message does not mention indexed.
Enrico Tassi (Jul 20 2020 at 18:23):Yes, the error message sucks, but it should now show forall (X : setoid.type) (A : indexed Type)... (and you said unchanged, so I want to be sure...). Maybe there is a bug, but the code does look for indexed in order to determine parameters.
Christian Doczkal (Jul 20 2020 at 18:29):This:
From HB Require Import structures.
HB.mixin Record Setoid_of_Type A :=
{ eqv : A -> A -> Prop ; foo : True }.
HB.structure Definition Setoid := { A of Setoid_of_Type A }.
Infix "≡" := eqv (at level 79).
HB.mixin Record Refl_of_Type (X : Setoid.type) (A : indexed Type) :=
{ elem_of : A -> Setoid.sort X; reflP (a : A) : (elem_of a) ≡ (elem_of a) }.
still yields:
Error:
ty-deps: BUG: could not get the parameters and the dependencies of
(forall (X : Setoid.type) (A : Type) (elem_of : A -> X), (forall a : A, elem_of a ≡ elem_of a) -> axioms_ X A)
Ah, and while we're on the subject of HB.mixin. Is there a deeper reason why HB.mixin cannot take a pre-existing Record, along the lines of HB.instance. I was a bit sad when I noticed that HB.mixin does not support notations in records.
Enrico Tassi (Jul 20 2020 at 18:54):Accepting an existing record as a mixin is not trivial.
For the notation things, I looked at it, and my understanding is that the notations are (in Coq) lost just after the record declaration. In particular the type and number of arguments of the "fields" changes and the notation are not adjusted. This is why I did not try to support them :-/
The bug, well, it is there. I won't be able to look into it before wednesday
Christian Doczkal (Jul 20 2020 at 19:04):Enrico Tassi said:
For the notation things, I looked at it, and my understanding is that the notations are (in Coq) lost just after the record declaration. In particular the type and number of arguments of the "fields" changes and the notation are not adjusted. This is why I did not try to support them :-/
Well, if there were notations in HB.mixin records, I would probably remove the Ops structure from my development. That's the one that also caused the "criss-cross" inheritance. But writing down the 15 axioms without notations would be pretty much unreadable.
That being said, I managed to port the graph theory library to HB. :tada:
The only two things that are still not as nice as I would like is this test thing we talked about and the smashed notations ...
Last updated: May 28 2023 at 18:29 UTC