alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Use Dolmen attribute to store well founded order

Open Halbaroth opened this issue 1 year ago • 1 comments

This PR used the well designed Dolmen to store custom attributes on constructors of ADT and ADT themself. This design has two advantages:

  1. We don't need to store an extra global state for the total order generated in the module Nest.
  2. 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.

Halbaroth avatar Jun 20 '24 14:06 Halbaroth

Can you clarify why we store the hash on 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.

Halbaroth avatar Jul 09 '24 13:07 Halbaroth

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.

Halbaroth avatar Jul 11 '24 09:07 Halbaroth