[DRAFT] new syntax about hierarchy-builder HOT 13 CLOSED

I like mixin and factory to be attributes.
I don't like much the builder line.

I'm just brainstorming

from hierarchy-builder.

We could also indent things like

#[mixin] HB
Record .....

and hope to be able to write, one day,

#[hb.mixin]
Record .....

from hierarchy-builder.

and hope to be able to write, one day,

#[hb.mixin]
Record .....

That would be really nice...

from hierarchy-builder.

#[factory]
HB Record Monoid_of_Type.axioms A := { ... } as f.
#[builder] HB Definition _ : AbGroup.axioms A _ := AbGroup.Axioms A (foo f).
HB End.

I do not like the fact that the presence of HB End depends on an attribute...

from hierarchy-builder.

It is already the case of other coq commands, iirc #[program] can change if the command opens goals or not...

An alternative would be to turn End into something different, eg Export Builders.

Another option is to let one list after the factory record the names of the builders, and implicitly end the module when the last one is declared (a bit a la next Obligation )

from hierarchy-builder.

Actually, we could tell the user which builders are required (proviso factories come after structure). Am I right?

from hierarchy-builder.

Actually, we could tell the user which builders are required (proviso factories come after structure). Am I right?

We could, but that would be too verbose...

from hierarchy-builder.

Actually, my preference goes to:

(* a mixin is necessarily a record *)
HB Mixin AbGroup.axioms T of Monoid.axioms T & .. := Axioms { opp : T -> T; ..  }.

(* a factory can be a record or a definition *)
HB Factory Record Monoid_of_Type.axioms T of .. & .. := Axioms { foo : .. ; .. }.
HB Builders (T : Type) (f : Monoid_of_Type.axioms T). 
 #[hb.instance T]
 Definition _ : AbGroup.axioms T := AbGroup.Axioms T (foo f).
HB End.

HB Structure Ring of Foo.axioms & Bar.axioms.

Definition X_isFoo : Foo.axioms X := ...
Definition X_isBar : Bar.axioms X := ...
(* equivalent to #[hb.instance X] for the two definitions above *)
HB Instance X X_isFoo X_isBar.

from hierarchy-builder.

I think that I will not merge attributes yet in coq-elpi.
All the rest is doable, but using Record or Definition as a prefix, otherwise it is too ambiguous (were does the telescope begin?)

from hierarchy-builder.

So it will be always HB Instance X... or HB Instance Definition ...
and HB Mixin Definition .. or HB Mixin Record ...

from hierarchy-builder.

and the tentation HB.Mixin is so strong ;-)

Anyway, the current syntax with no capitals looks so much lighter to me... maybe HB.mixin ?

from hierarchy-builder.

HB Factory Record Monoid_of_Type.axioms T of .. & .. := Axioms { foo : .. ; .. }.

I'm wondering what is the purpose of Module.axioms... can't we just put Module (and define a Module.axiom as per contract)?

from hierarchy-builder.

I'm wondering what is the purpose of Module.axioms... can't we just put Module (and define a Module.axiom as per contract)?

Mmmh, we could. I am not sure whether I prefer a "contract" or explicit naming though... but we already have a contract for .type and .sort, so let's go for .axioms.

from hierarchy-builder.