Use Dolmen attribute to store well founded order #1153

Halbaroth · 2024-06-20T14:30:35Z

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.

bclement-ocp

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.

If the issue is that this is not compatible with the legacy frontend (which it might very well not be): do we need this in 2.6 or can we postpone to 2.7 so that we don't have to deal with the legacy frontend? It looks like it would simplify this PR a great deal.

src/lib/frontend/d_cnf.ml

src/lib/reasoners/adt_rel.ml

src/lib/structures/fpa_rounding.ml

src/lib/structures/ty.ml

src/lib/structures/uid.ml

Halbaroth · 2024-07-09T13:28:45Z

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.

bclement-ocp

I am a bit concerned by the amount of implicit dependencies currently and have suggested places where (I think) we can add runtime checks ensuring that we catch errors early if we try to create uids without an order attached, which should help with maintainability in the future.

I also made some other comments regarding dead code and missing documentation that should be fixed.

bclement-ocp · 2024-07-10T07:28:51Z

src/lib/frontend/d_cnf.ml

    ) ->
    (* Records and adts that only have one case are treated in the same way,
       and considered as records. *)
-    Nest.add_nest [adt];
+    let uid = Uid.of_ty_cst ty_c in


Why no Nest.attach_orders here?

Because we never send record values to the ADT theory so we never use the total order.

Makes sense — the order is also trivial. I think it still makes sense to have an order attached to all constructors for consistency.

I did this modification. We have an order on all constructors because we check it in Uid.of_ty_cst now ;)

src/lib/structures/uid.ml

bclement-ocp · 2024-07-10T07:34:11Z

src/lib/util/lists.mli

+
+val find_index : ('a -> bool) -> 'a list -> int option
+(** [find_index f l] returns [Some i], where [i] is the index of the first
+    element of the list [l] that satisfies [f x], if there is such an element.
+
+    It returns [None] if there is no such element. *)


Looks like this is no longer used?

bclement-ocp · 2024-07-10T07:40:17Z

src/lib/structures/uid.ml


 let[@inline always] of_dolmen id = Dolmen id
+let[@inline always] of_term_cst id = Term_cst id


Is it correct to say that of_term_cst should only be called on term constructors that have had an order attached? Could we had an assertion for this here?

It is not true because we use it also for unique constructor of record but I can generate an order for these constructors too and add an assertion here.

Actually, we cannot put an assertion here as destructors are also of type term_cst.

bclement-ocp · 2024-07-10T07:40:51Z

src/lib/structures/uid.mli

+(** Tag used to attach the order of constructor. Used to
+    retrieve efficiency the order of the constructor in [to_int]. *)
+
+val perfect_hash : t -> int


This should be documented, and in particular it should be documented that it must only be called on uids to which an order has been attached by the Nest module, and that it can only be called on term constructors.

bclement-ocp · 2024-07-10T07:44:01Z

src/lib/structures/uid.mli

 type t = private
  | Hstring : Hstring.t -> t
  | Dolmen : 'a DE.id -> t
+  | Term_cst : DE.term_cst -> t
+  | Ty_cst : DE.ty_cst -> t


This is orthogonal to the PR but if we define

type _ t = | Hstring : Hstring.t -> 'a t | Term_cst : DE.term_cst -> DE.ty t | Ty_cst : DE.ty_cst -> DE.type_fun t | Ty_var : DE.ty_var -> DE.type_ t type term_cst = DE.ty t type ty_var = DE.type_ t type ty_cst = DE.type_fun t

then we can expose the "kind" of uid in the type and gain type safety (in particular, perfect_hash can be of type Uid.term_cst -> int).

I applied the change in this PR. It is definitively a better approach. Thanks :)

bclement-ocp · 2024-07-10T07:45:32Z

src/lib/structures/uid.mli

+val order_tag : int Dolmen.Std.Tag.t
+(** Tag used to attach the order of constructor. Used to
+    retrieve efficiency the order of the constructor in [to_int]. *)


Nit: in the current design, I believe moving order_tag and perfect_hash to Nest would allow hiding order_tag from the interface.

bclement-ocp · 2024-07-10T07:47:21Z

src/lib/frontend/d_cnf.ml

+    let uid = Uid.of_ty_cst ty_c in
+    Nest.attach_orders [adt];


Note: I think that keeping the let uid = Uid.of_ty_cst ty_c in after the call to Nest.attach_orders allows to have an assertion in Uid.of_ty_cst that the type has had order tags attached.

Halbaroth · 2024-07-10T14:18:52Z

src/lib/frontend/d_cnf.ml

+  let fresh_ty ?(is_var = true) ?(name = None) () =
    if is_var
    then Ty.fresh_tvar ()
    else
-      match id with
-      | Some id -> Ty.text [] (Uid.of_dolmen id)
+      match name with
+      | Some n -> Ty.text [] (Uid.of_string n)
      | None -> Ty.fresh_empty_text ()

-  let update_ty_store ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id () in
+  let update_ty_store ?(is_var = true) ?name id =
+    let ty = fresh_ty ~is_var ~name () in
    store_ty id ty

-  let update_ty_store_ret ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id () in
+  let update_ty_store_ret ?(is_var = true) ?name id =
+    let ty = fresh_ty ~is_var ~name () in


Using a polymorphic GADT for Uid.t almost works every but I ran into an annoying issue here.

It makes sense to use ty_cst for the constructor of applications of abstract types in Ty.t but in elim_toplevel_forall in D_cnf, we remove the top level binders for both type and term variables. Basically, we replace a type variable ty_var by an uninterpreted type using Text. So we need to convert a ty_var into a ty_cst, which is not permit by Dolmen.

I rollback my modifications done in #1098.

This PR used the well designed Dolmen to store a custom attribute 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.

bclement-ocp

Looks good overall — two small changes regarding Dolmen API use and we should be ready to merge 👍

bclement-ocp · 2024-07-11T04:51:48Z

src/lib/frontend/d_cnf.ml

-      match id with
-      | Some id -> Ty.text [] (Uid.of_dolmen id)
+      match name with
+      | Some n -> Ty.text [] (Uid.of_string n)


I think this might re-introduce some of the potential name clashes that #1098 was intended to remove.

When converting a variable → type for the purpose of quantifier elimination, we should fall back to the Ty.fresh_empty_text () here — see my comment in store_tyv below.

bclement-ocp · 2024-07-11T04:56:08Z

src/lib/frontend/d_cnf.ml

+    let name = get_basename t_v.DE.path in
+    update_ty_store ~is_var ~name t_v


update_ty_store is a simple wrapper here, we could call fresh_ty directly and keep the existing code, which would avoid using Uid.of_string:

Suggested change

let name = get_basename t_v.DE.path in

update_ty_store ~is_var ~name t_v

let ty = fresh_ty ~is_var () in

store_ty t_v ty

Alternatively, we can create an identifier from the name of the variable:

Suggested change

let name = get_basename t_v.DE.path in

update_ty_store ~is_var ~name t_v

let id = DE.Ty.Const.mk t_v.DE.path 0 in

let ty = fresh_ty ~is_var ~id in

store_ty t_v ty

bclement-ocp · 2024-07-11T04:58:25Z

src/lib/frontend/d_cnf.ml

    ) ->
    (* Records and adts that only have one case are treated in the same way,
       and considered as records. *)
-    Nest.add_nest [adt];
+    let uid = Uid.of_ty_cst ty_c in


Makes sense — the order is also trivial. I think it still makes sense to have an order attached to all constructors for consistency.

bclement-ocp · 2024-07-11T05:00:51Z

src/lib/structures/fpa_rounding.ml

  let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  let () =
+    match DStd.Expr.Ty.definition ty_cst with
+    | Some def -> Nest.attach_orders [def]
+    | None -> assert false
+  in


Suggested change

let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in

let () =

match DStd.Expr.Ty.definition ty_cst with

| Some def -> Nest.attach_orders [def]

| None -> assert false

in

let def, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in

Nest.attach_orders [def];

bclement-ocp · 2024-07-11T05:03:04Z

src/lib/structures/uid.ml

+
+let order_tag : int DStd.Tag.t = DStd.Tag.create ()
+
+let has_order id =


It is somewhat confusing that has_order can return true for terms that have no order attached. Something like has_order_if_constructor would be clearer.

bclement-ocp · 2024-07-11T05:08:22Z

src/lib/structures/uid.ml

+  (* This assertion ensures that the API of the [Nest] module have been
+     correctly used, that is [Nest.attach_orders] have been called on
+     the nest of [id] if [id] is a constructor of ADT. *)
+  if not @@ has_order id then Fmt.failwith "not order on %a" DE.Id.print id;


Suggested change

if not @@ has_order id then Fmt.failwith "not order on %a" DE.Id.print id;

if not @@ has_order id then Fmt.invalid_arg "no order on %a" DE.Id.print id;

bclement-ocp

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".

Halbaroth · 2024-07-11T09:42:18Z

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.

* Use Dolmen attributes to store well founded order This PR used the well designed Dolmen library (thanks Guillaume) to store a custom attribute on constructors of ADT. This design has two advantages: 1. We do not 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. As an aside, this PR refactors the way we manage Dolmen identifiers. The new approach is safer as OCaml's typechecker can ensure some invariants for us.

CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)

Halbaroth added the clean-up label Jun 20, 2024

Halbaroth added this to the 2.6.0 milestone Jun 20, 2024

Halbaroth force-pushed the order-attribute branch 5 times, most recently from 660da05 to 55692f7 Compare July 9, 2024 11:48

Halbaroth marked this pull request as ready for review July 9, 2024 11:50

Halbaroth requested a review from bclement-ocp July 9, 2024 11:52

bclement-ocp reviewed Jul 9, 2024

View reviewed changes

Halbaroth force-pushed the order-attribute branch 3 times, most recently from a5e45f8 to 63937f1 Compare July 9, 2024 16:09

Halbaroth requested a review from bclement-ocp July 9, 2024 16:09

bclement-ocp requested changes Jul 10, 2024

View reviewed changes

Halbaroth force-pushed the order-attribute branch 2 times, most recently from 0c5f5ef to ff87e7e Compare July 10, 2024 14:16

Halbaroth commented Jul 10, 2024

View reviewed changes

Halbaroth added 3 commits July 10, 2024 16:24

review changes

7ac984a

Remove dead code

f421b43

Halbaroth force-pushed the order-attribute branch from ff87e7e to 02d9834 Compare July 10, 2024 14:25

Halbaroth added 3 commits July 10, 2024 16:26

Use polymorphic GADT for UId.t

39ba617

Do not expose the order tag

30e7141

Add an assertion in of_term_cst

02d9834

Halbaroth requested a review from bclement-ocp July 10, 2024 14:26

linter

8951c2b

bclement-ocp requested changes Jul 11, 2024

View reviewed changes

Halbaroth requested a review from bclement-ocp July 11, 2024 08:18

review changes 2

2b11a43

bclement-ocp approved these changes Jul 11, 2024

View reviewed changes

Halbaroth merged commit 98e1392 into OCamlPro:next Jul 11, 2024
14 checks passed

bclement-ocp mentioned this pull request Sep 24, 2024

[new release] alt-ergo (4 packages) (2.6.0) ocaml/opam-repository#26609

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use Dolmen attribute to store well founded order #1153

Use Dolmen attribute to store well founded order #1153

Halbaroth commented Jun 20, 2024 •

edited

Loading

bclement-ocp left a comment

Halbaroth commented Jul 9, 2024

bclement-ocp left a comment

bclement-ocp Jul 10, 2024

Halbaroth Jul 10, 2024

bclement-ocp Jul 11, 2024

Halbaroth Jul 11, 2024

bclement-ocp Jul 10, 2024

bclement-ocp Jul 10, 2024

Halbaroth Jul 10, 2024

Halbaroth Jul 10, 2024

bclement-ocp Jul 10, 2024

bclement-ocp Jul 10, 2024

Halbaroth Jul 10, 2024

bclement-ocp Jul 10, 2024

bclement-ocp Jul 10, 2024

Halbaroth Jul 10, 2024 •

edited

Loading

bclement-ocp left a comment

bclement-ocp Jul 11, 2024

bclement-ocp Jul 11, 2024

bclement-ocp Jul 11, 2024

bclement-ocp Jul 11, 2024

bclement-ocp Jul 11, 2024

bclement-ocp Jul 11, 2024

bclement-ocp left a comment

Halbaroth commented Jul 11, 2024


		let[@inline always] of_dolmen id = Dolmen id
		let[@inline always] of_term_cst id = Term_cst id

		let name = get_basename t_v.DE.path in
		update_ty_store ~is_var ~name t_v

-    let name = get_basename t_v.DE.path in
-    update_ty_store ~is_var ~name t_v
+    let id = DE.Ty.Const.mk t_v.DE.path 0 in
+    let ty = fresh_ty ~is_var ~id in
+    store_ty t_v ty


		let order_tag : int DStd.Tag.t = DStd.Tag.create ()

		let has_order id =

	if not @@ has_order id then Fmt.failwith "not order on %a" DE.Id.print id;
	if not @@ has_order id then Fmt.invalid_arg "no order on %a" DE.Id.print id;

Use Dolmen attribute to store well founded order #1153

Use Dolmen attribute to store well founded order #1153

Conversation

Halbaroth commented Jun 20, 2024 • edited Loading

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Jul 9, 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

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 Jul 10, 2024 • edited Loading

Choose a reason for hiding this comment

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

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Jul 11, 2024

Halbaroth commented Jun 20, 2024 •

edited

Loading

Halbaroth Jul 10, 2024 •

edited

Loading