Use Dolmen attribute to store well founded order
This PR used the well designed Dolmen to store custom attributes on constructors of ADT and ADT themself. This design has two advantages:
- We don't need to store an extra global state for the total order generated in the module
Nest. - We have a total order per ADT instead of a global order for all the ADT types.
To be more specific, we generate a bijection between ADT constructors and the interval [0, n[ where n is the number of constructors.
This PR have been tested and we have no regression at all. I'm running benchmarks for the legacy frontend too.
Can you clarify why we store the
hashon the type?Since the (term) constructors for distinct types are distinct, couldn't we just store the hash associated with each term constructor on the term itself? It seems like it would avoid a bunch of ceremony to get the hashing function from the type.
Sure, it's simpler. This PR have been really complicated to write actually, I have redone it from scratch several times.
LGTM
Nit: I did not notice earlier, but I am not a fan of the "cstr" abbreviation and would very much prefer "constr", if we need to abbreviate at all — we are not writing C and I don't think we need to import their hatred for vowels. Plus my brain reads "cstr" as "C string".
Sadly, I prefer this option but I use it mainly because it is the convention in Dolmen too :). I agree to uniform all of them to constr.