Stream: Hierarchy Builder devs & users

Topic: Naming of builders


view this post on Zulip Reynald Affeldt (Feb 22 2022 at 09:58):

A consequence of the HB.instance Definition _ command is to generate made up names. One of them can be fixed by replacing _ by some identifier. What about the second one (which correspond to a constructor)? Although the naming scheme seems stable in general, inside a HB.Builders/HB.end section it seems to change on each execution.

view this post on Zulip Enrico Tassi (Feb 22 2022 at 12:34):

I think the real problem is that HB.instance generates as many instances as the current hierarchy demands and the given factory provides. So one would need a way to pass many names, but the number would change even if mixins are replaced by factories, making the code break.

So I'm not so sure what your use case for naming all the things is.

view this post on Zulip Reynald Affeldt (Feb 22 2022 at 13:16):

I am in a situation where I want to replace a few hand-made pack classes with HB.structures, at a certain point HB does not do “what I want”, but I can still make progress if I allow myself locally the explicit use of constructors, unfortunately I cannot compile the file in question because of random names, and thus I cannot go on with my porting. Of course, it is very likely that “what I want” is wrong and that I’d better figure it out first, but I would have also find it helpful to defer this activity to later. That would be my use case. :-/

view this post on Zulip Enrico Tassi (Feb 22 2022 at 14:09):

What are these constructors exactly?
I guess the best would be to name them reliably using something like Definition the_thing := HB.some_command inputs.

view this post on Zulip Reynald Affeldt (Feb 22 2022 at 14:33):

I am using a constructor whose name is something like Builders_7.Builders_7_e__canonical__blablah, and I am now trying to get rid of this use.

view this post on Zulip Enrico Tassi (Feb 22 2022 at 14:48):

And the use site? Can I look at the code?

view this post on Zulip Reynald Affeldt (Feb 22 2022 at 14:55):

Sure but it's wip. https://github.com/affeldt-aist/monae/blob/HB_nattrans/monad_transformer.v#L226-L241

view this post on Zulip Reynald Affeldt (Feb 22 2022 at 14:56):

I figured out a way to avoid the use of random names but this is still an awkard use of HB.

view this post on Zulip Reynald Affeldt (Feb 22 2022 at 15:11):

(I mean, I guess you do not want users to use X.Class and X.phant_Build explicitly.)

view this post on Zulip Enrico Tassi (Feb 22 2022 at 16:37):

So, the good news is that I could write:

Definition stateT (S : UU0) : monadT :=
  let m M := [the monad of MS S M] in
  let l M := [the monadM M [the monad of (MS S M)] of (@liftS S M)] in
  HB.pack m (isMonadT.Build m l).

The bad news is that I had to patch HB:

diff --git a/HB/pack.elpi b/HB/pack.elpi
index 3da251b..d98a54a 100644
--- a/HB/pack.elpi
+++ b/HB/pack.elpi
@@ -14,7 +14,7 @@ main Ty Args Instance :- std.do! [
   get-constructor Class KC,
   get-constructor Structure KS,

-  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "HB.pack: not a type",
+  std.assert-ok! (coq.elaborate-skeleton TSkel _ T) "HB.pack: not a well typed key",

   private.elab-factories FactoriesSkel T Factories,

The worst is that I had no idea what I was doing. In particular all these [the monad of ..] seem fishy

view this post on Zulip Enrico Tassi (Feb 23 2022 at 08:43):

BTW, I have the impression the definition becomes much nicer with the reverse coercion business


Last updated: Jan 29 2023 at 16:02 UTC