Use the Dolmen identifiers for constructors and ADT names #1098

Halbaroth · 2024-04-24T16:43:16Z

We don't manage correctly incremental type declarations. For instance the following input is accepted by the SMT-LIB standard:

(set-logic ALL)
(push 1)
(declare-datatype t
  ((c1 (d1 Int)) (c2)))
(pop 1)
(declare-datatype t
  ((c2 (d1 Int)) (c1)))
(declare-const x t)
(declare-const y t)
(assert ((_ is c1) x))
(assert ((_ is c1) y))
(assert (distinct x y))
(check-sat)

(Notice that we switch the constructors c1 and c2 in our second declaration of the type t). AE answers unknown on next but it answers unsat if we remove the first declaration of t.

This PR fixes the issue for the new frontend only. So we got unsat with --frontend dolmen but we still got unknown with --frontend legacy.

The solution consists in using the unique identifiers produced by Dolmen for the constructors, destructors and names of ADTs. To reduce as much as possible the amount of modification done in the legacy typechecker, I wrapped Dolmen's identifiers in a new module Uid. This module agrees with Hstring if we use the constructors of_string or of_hstring and it uses Dolmen's identifiers if we use the constructor of_dolmen. Of course, we'll get rid of this module as soon as we remove the legacy frontend.

I didn't use a unique identifier for the constructor of builtin enumeration types. This case will be fixed after removing the legacy frontend.

This PR is supposed to be merged before #1093

bclement-ocp

I did not look thoroughly through the minutiæ of all mechanical changes from Hstring → Uid but the change looks correct overall. I do have some minor questions, and something needs to be done for record constructors which I think are broken in the legacy typechecker by this PR.

bclement-ocp · 2024-05-06T06:49:49Z

src/lib/structures/uid.ml

+
+type t =
+  | Fake of Hstring.t
+  | Unique of { name : Hstring.t; index : int }


Why use a separate Unique constructor with our own tag rather than directly use the Dolmen identifier?

Of course I tried to use the Dolmen identifier directly but I got a regression in our non-regression test suite. I should investigate.

Ok, I tried again with the original index produced by Dolmen. Now I got five regressions and it seems that Alt-Ergo ignores the timeout for them (make runtest never returns). Actually, if I run dune exec -- alt-ergo tests/adts/match_in_terms.ae, I cannot kill the processus with CTRL+C. I have to type pkill alt-ergo.

I suspect an issue with DE.Id.compare or DE.Id.equal.

Uhm they seems to be reasonable:

let compare v v' = compare v.index v'.index let equal v v' = compare v v' = 0

very strange ...

Thanks to Vincent, I got the bug with gdb. The issue comes from the fact that Dolmen identifiers can be infinite values and the polymorphic equality loops infinitely on them. I wrote another PR to remove as much as possible polymorphic comparison in lists.

Yeah, dolmen identifiers should never be compared using the polymorphic identity: besides being slow (compared to the comparison defined by dolmen), it may loop forever (because the Type identifiers loops on itself), or may fail at runtime (because ids contain tags that can contain arbitrary data such as functions).

bclement-ocp · 2024-05-06T06:58:23Z

src/lib/structures/ty.ml

+      (* TODO: FIIIIXXX *)
+      (*       Format.sprintf "%s___%s" record_constr n *)


I believe this is required for the legacy typechecker not to confuse constructors for distinct record types ; it should be moved to the legacy typechecker.ml rather than removed entirely.

bclement-ocp · 2024-05-06T07:05:31Z

src/lib/structures/ty.ml

@@ -514,19 +514,20 @@ let type_body name args = Decls.body name args


 (* smart constructors *)
-let tunit = Text ([],Hstring.make "unit")
+(* HACK: we should create a unique Dolmen identifier here. *)


We should instead use DStd.Ty.Const.unit.

I don't know Dolmen already contains a unit constant. I'll change it.

bclement-ocp · 2024-05-06T07:07:22Z

src/lib/structures/fpa_rounding.ml

+  let fake_reprs = List.map Uid.of_hstring hstring_smt_reprs in
+  Ty.Tsum (Uid.of_string "RoundingMode", fake_reprs)


Why use hstring rather than dolmen IDs here?

When I wrote this PR I didn't do it because I didn't want to have to manage unique identifiers in the legacy typechecker. Basically, if we use real unique identifiers and hstring identifiers, we have to ensure that the legacy typechecker won't recreate ADTs' constructors for builtin enums (and it does...).

Finally I found another way to use dolmen identifiers here. I modified the comparison functions of Uid. Now if we compare a Hstring and a Dolmen identifiers, we transform the Dolmen identifier into string.

the legacy typechecker won't recreate ADTs' constructors for builtin enums (and it does...).

Ah, I guess this is the issue of having different names for the AE and SMT enums, got it.

Now if we compare a Hstring and a Dolmen identifiers, we transform the Dolmen identifier into string.

Is this not re-introducing the dependency on string values that this PR is trying to eliminate?

Now the Dolmen frontend doesn't produce Uid.t of type Hstring anymore (but for abstract types, I'll change that). It means we always compare Dolmen identifiers here (for constructors, destructors and ADTs' names).

bclement-ocp · 2024-05-06T07:12:42Z

src/lib/structures/uid.ml

+module DE = DStd.Expr
+
+type t =
+  | Fake of Hstring.t


Nit: calling them Fake is confusing; what's fake about them?

It's fake unique identifier. It's not unique but I can rename it into Hstring.

bclement-ocp · 2024-05-07T11:57:48Z

src/lib/frontend/d_cnf.ml

-    type t = int
-    let equal = (=)
-    let hash = Fun.id
+type id = Id : 'a DE.id -> id


Suggested change

type id = Id : 'a DE.id -> id

type id = Id : 'a DE.id -> id[@@unboxed]

Halbaroth · 2024-05-10T15:20:36Z

The PR is ready for a second pass. I think we should test the legacy frontend with fpa on Marvin before merging it.

bclement-ocp

Yeah on paper the changes look correct but we definitely should check that there are no regressions. I am a bit lost by the many small changes now; I will take a deeper look after the weekend. I think there are many unneeded string/Hstring conversions now but we can clean that up later.

bclement-ocp · 2024-05-10T15:25:29Z

src/lib/frontend/d_cnf.ml


-  let fresh_ty ?(is_var = true) ?(name = None) () =
+  let fresh_ty ?(is_var = true) ?(id = None) () =


I think you want ?id here and ~id when fresh_ty is called.

(Currently fresh_ty has a ?id:Uid.t option optional argument, simply using ?id would make it a ?id:Uid.t argument)

bclement-ocp · 2024-05-10T15:28:26Z

src/lib/frontend/d_cnf.ml

      DStd.Expr.Id.mk ~builtin:B.Base
-        (DStd.Path.global (Hstring.view name))
+        (DStd.Path.global (Uid.show name))
        DStd.Expr.{ arity = 0; alias = No_alias }


This looks a bit weird; aren't we building a second Dolmen identifier with the same name as an existing one here?

Indeed, I thought it was correct but we duplicate the identifiers here. I fixed the issue by creating the constructors and the Dolmen type in Fpa_rounding.

bclement-ocp · 2024-05-10T15:30:39Z

src/lib/structures/uid.ml

+
+let pp ppf = function
+  | Hstring hs -> Hstring.print ppf hs
+  | Dolmen { path; _ } -> Fmt.string ppf @@ get_basename path


Why not DE.Id.print?

Halbaroth · 2024-05-13T07:39:52Z

I rebase this PR on #1117 to remove some polymorphic comparisons again ;)

bclement-ocp

Still a couple questions but overall I think this is ready to merge once rebased & if the benches are green.

bclement-ocp · 2024-05-13T08:41:37Z

src/lib/structures/uid.ml

+  | Hstring hs1, Hstring hs2 -> Hstring.equal hs1 hs2
+  | Dolmen id1, Dolmen id2 -> DE.Id.equal id1 id2
+  | _ ->
+    Hstring.equal (Hstring.make @@ show u1) (Hstring.make @@ show u2)


Isn't this a complicated way of writing String.equal (show u1) (show u2)? The complexity should be the same since Hstring.make requires a linear scan.

I thought it was a little bit faster because we compare integers if these Hstring already exist but we have to compute the hash of the strings, which may be linear in the length of them.

bclement-ocp · 2024-05-13T08:42:41Z

src/lib/structures/uid.ml

+  match u1, u2 with
+  | Hstring hs1, Hstring hs2 -> Hstring.compare hs1 hs2
+  | Dolmen id1, Dolmen id2 -> DE.Id.compare id1 id2
+  | _ -> Hstring.compare (Hstring.make @@ show u1) (Hstring.make @@ show u2)


Do we need the Hstring comparison here? Otherwise String.compare (show u1) (show u2) might be sufficient (complexity should be the same since Hstring.make requires a linear scan).

bclement-ocp · 2024-05-13T08:46:14Z

src/lib/structures/fpa_rounding.mli


 (** Equal to ["RoundingMode"], the SMT2 type of rounding modes. *)
 val fpa_rounding_mode_type_name : string

 (** Equal to ["fpa_rounding_mode"], the Alt-Ergo native rounding mode type. *)
 val fpa_rounding_mode_ae_type_name : string

+(** The Dolmen rounding mode type. *)
+val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.t


👍

Do we still need the various string conversion functions with this?

I don't think so

We still need them in both legacy and new frontend. In the new frontend, we use these functions in the typechecker to inject the AE identifiers into SMT-LIB identifiers.

We also use them in Expr because we need to convert a Hstring identifier into Fpa_rounding.rounding_mode.

I'm sure we can remove some of them after getting rid of the legacy frontend.

bclement-ocp · 2024-05-13T08:49:53Z

src/lib/structures/fpa_rounding.ml

+  let module DStd = Dolmen.Std in
+  let ty_cst = DE.Ty.Const.mk (DStd.Path.global "RoundingMode") 0 in
+  let cstrs =
+    List.map (fun c -> DStd.Path.global @@ to_smt_string c, []) cstrs
+  in
+  let _, cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  DE.Ty.apply ty_cst [], cstrs,
+  Ty.Tsum (Uid.of_dolmen ty_cst, List.map (fun (c, _) -> Uid.of_dolmen c) cstrs)


Note: I think this could be replaced with DStd.Expr.Ty.roundingMode. I don't think it is entirely trivial to do so, but might be worth a note in a comment.

I didn't the enum type is shipped with Dolmen. We can replace it easily. It's exactly the same code.

Uhm actually roundingMode is the SMT-LIB roundingMode, so it's not so obvious. I add a note.

The RoundingMode type from AE (SMT-LIB flavor) should be identical to the SMT-LIB RoundingMode, we made sure with @Stevendeo that the constructors are the same.

I put a note and I will do it in another PR, maybe after the release.

Halbaroth · 2024-05-16T16:48:13Z

No regression with the following combinations:

frontend legacy on ae-format
frontend legacy on ae-format-fpa with --enable-theories fpa
frontend dolmen on ae-format
frontend dolmen on ae-format-fpa with --enable-theories fpa

So this PR is ready for I hope a last check ;)

bclement-ocp

🎉

Halbaroth added the bug label Apr 24, 2024

Halbaroth added this to the 2.6.0 milestone Apr 24, 2024

Halbaroth force-pushed the unique-constructors branch from 7edf101 to f53b10e Compare April 24, 2024 16:46

Halbaroth marked this pull request as ready for review May 6, 2024 06:36

Halbaroth requested a review from bclement-ocp May 6, 2024 06:36

bclement-ocp reviewed May 6, 2024

View reviewed changes

bclement-ocp reviewed May 7, 2024

View reviewed changes

Halbaroth force-pushed the unique-constructors branch from 4105dbf to 6a81272 Compare May 10, 2024 14:41

bclement-ocp reviewed May 10, 2024

View reviewed changes

Halbaroth force-pushed the unique-constructors branch 2 times, most recently from b64ecd1 to 0446b52 Compare May 10, 2024 23:08

Halbaroth mentioned this pull request May 13, 2024

Get rid of Stdlib.compare and Stdlib.(=) #1117

Merged

bclement-ocp reviewed May 13, 2024

View reviewed changes

Halbaroth force-pushed the unique-constructors branch from 818f88b to c838a68 Compare May 13, 2024 12:32

Halbaroth added 14 commits May 13, 2024 14:33

Use the Dolmen identifiers for constructors and ADT names

1148780

Convenient constructors for unique identifiers

b9d7d94

poetry

21b0d6b

Add a test

bc01e94

Try to fix regressions with fpa

8fcd843

Rename Fake to Hstring

588a978

Use the unit id of Dolmen

8a933b3

Restore distinct constructor for distinct records

e1a7b1d

Use Dolmen identifiers directly in Uid

00674ca

Use Dolmen identifiers for abstract types

4a57d28

Avoid duplication for builtin enum type

2ab5103

Simplify fresh_ty type

acd48aa

rebase

6de6eba

String comparison

e8ab5c5

review changes

c838a68

Halbaroth requested a review from bclement-ocp May 16, 2024 16:48

bclement-ocp approved these changes May 16, 2024

View reviewed changes

Halbaroth merged commit 8e76dcd into OCamlPro:next May 16, 2024
14 checks passed

Halbaroth mentioned this pull request Jul 10, 2024

Use Dolmen attribute to store well founded order #1153

Merged

		(* TODO: FIIIIXXX *)
		(* Format.sprintf "%s___%s" record_constr n *)

		let fake_reprs = List.map Uid.of_hstring hstring_smt_reprs in
		Ty.Tsum (Uid.of_string "RoundingMode", fake_reprs)

	type id = Id : 'a DE.id -> id
	type id = Id : 'a DE.id -> id[@@unboxed]


		let fresh_ty ?(is_var = true) ?(name = None) () =
		let fresh_ty ?(is_var = true) ?(id = None) () =

Use the Dolmen identifiers for constructors and ADT names #1098

Use the Dolmen identifiers for constructors and ADT names #1098

Conversation

Halbaroth commented Apr 24, 2024 • edited Loading

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth May 10, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented May 10, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth May 10, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented May 13, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth May 13, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth May 13, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented May 16, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Apr 24, 2024 •

edited

Loading

Halbaroth May 10, 2024 •

edited

Loading

Halbaroth May 10, 2024 •

edited

Loading

Halbaroth May 13, 2024 •

edited

Loading

Halbaroth May 13, 2024 •

edited

Loading