search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
131 stars 33 forks source link

Remove `Ty.Tunit` #1148

Closed Halbaroth closed 3 months ago

Halbaroth commented 3 months ago

Dolmen exposes a builtin unit type Dolmen.Std.Expr.Ty.Const.unit, which is an ADT with only one constructor Dolmen.Std.Expr.Term.Cstr.void.

Alt-Ergo exposes two unit types...

  1. Ty.tunit but this type is never used!
  2. Ty.Tunit (notice the upper case!)

The AE type Ty.Tunit is neither an ADT nor a record but there is no good reason to have a specific constructor for this type. We do nothing special with expressions of type unit.

This PR removes Ty.Tunit and use the Dolmen type.

It means that Ty.tunit is the only ADT with a single constructor without payload represented by an Alt-Ergo ADT. Others are represented by records.

Halbaroth commented 3 months ago

We got +4-0 on ae-format. All the improvements have a goal of the form ... = void. It seems that Alt-Ergo didn't know that void is the unique value of type unit!

Unfortunately, AE is a bit slower (~ 1.2% slower) with this patch but I think it's acceptable as we got extra tests.

Halbaroth commented 3 months ago

Do we really need to have a unit (Ty.tunit) type at all?

We need to have this builtin type because unit is a builtin type in the native language of Alt-Ergo. I think this is the reason why Dolmen includes this type too.

Do you have an idea of where the slow down might be coming from?

I think it's because after this PR, we split on any value of type unit after the first assertion because it's domain in Adt_rel is obviously a singleton. I won't merge this PR now because I would like to mitigate this slowdown before.

bclement-ocp commented 3 months ago

I think it's because after this PR, we split on any value of type unit after the first assertion because it's domain in Adt_rel is obviously a singleton.

We should not be splitting on singleton domains (and we probably don't, or we would loop).

We should be propagating that any non-void (syntactically) value of unit type is equal to void, but that is correct and expected.

I don't think we need to spend too much time on this slowdown; I'd say it is within our statistical noise due to measurement error, GC behavior changes and the like.