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.

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.

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"

I see. So while one can define parametric instances within sections, one really has to list the parameters for parametric mixins.

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:

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

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`

.

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.

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.

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

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: Apr 21 2024 at 02:41 UTC