From 4ef6a65b98fbb69ec0d372c5e7819ef75cb833c3 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 20 Nov 2024 17:04:24 -0500 Subject: [PATCH] Add more equality --- src/haz3lcore/dynamics/FilterAction.re | 6 +++--- .../dynamics/InvalidOperationError.re | 2 +- src/haz3lcore/dynamics/VarBstMap.re | 7 ++++++- src/haz3lcore/dynamics/VarBstMap.rei | 2 ++ src/haz3lcore/lang/Operators.re | 20 +++++++++---------- src/haz3lcore/lang/term/IdTagged.re | 2 ++ src/haz3lcore/statics/Var.re | 2 +- src/haz3lcore/tiles/Id.re | 1 + 8 files changed, 26 insertions(+), 16 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterAction.re b/src/haz3lcore/dynamics/FilterAction.re index 6a4dce5ca3..e176847b84 100644 --- a/src/haz3lcore/dynamics/FilterAction.re +++ b/src/haz3lcore/dynamics/FilterAction.re @@ -1,14 +1,14 @@ -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type action = | Step | Eval; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type count = | One | All; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type t = (action, count); let string_of_t = v => { diff --git a/src/haz3lcore/dynamics/InvalidOperationError.re b/src/haz3lcore/dynamics/InvalidOperationError.re index b317e64254..41bf053a6f 100644 --- a/src/haz3lcore/dynamics/InvalidOperationError.re +++ b/src/haz3lcore/dynamics/InvalidOperationError.re @@ -1,4 +1,4 @@ -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type t = | InvalidOfString | IndexOutOfBounds diff --git a/src/haz3lcore/dynamics/VarBstMap.re b/src/haz3lcore/dynamics/VarBstMap.re index 2952690388..89a6787014 100644 --- a/src/haz3lcore/dynamics/VarBstMap.re +++ b/src/haz3lcore/dynamics/VarBstMap.re @@ -29,7 +29,7 @@ module Inner = { }; module VarBstMap0 = { - [@deriving (show({with_path: false}), sexp, yojson)] + [@deriving (show({with_path: false}), sexp, yojson, eq)] type t_('a) = Inner.t('a); let empty = Inner.empty; @@ -61,6 +61,8 @@ module VarBstMap0 = { let to_list = ctx => ctx |> Inner.to_seq |> List.of_seq; let of_list = bindings => bindings |> List.to_seq |> Inner.of_seq; + + let equal = Inner.equal; }; module Ordered = { @@ -206,6 +208,9 @@ module Ordered = { let without_keys = (keys, m) => { filterk(((s, _)) => !List.exists(x => x == s, keys), m); }; + + let equal_t_ = (cmp, m1, m2) => + VarBstMap0.equal(cmp, m1.map, m2.map) && m1.rev_order == m2.rev_order; }; include VarBstMap0; diff --git a/src/haz3lcore/dynamics/VarBstMap.rei b/src/haz3lcore/dynamics/VarBstMap.rei index 36a3a20659..01e1b24ad2 100644 --- a/src/haz3lcore/dynamics/VarBstMap.rei +++ b/src/haz3lcore/dynamics/VarBstMap.rei @@ -174,4 +174,6 @@ module Ordered: { [without_keys] removes all entires with the given keys from the map */ let without_keys: (list(Var.t), t_('a)) => t_('a); + + let equal_t_: (('a, 'a) => bool, t_('a), t_('a)) => bool; }; diff --git a/src/haz3lcore/lang/Operators.re b/src/haz3lcore/lang/Operators.re index aa8842b72b..eda4adcc9c 100644 --- a/src/haz3lcore/lang/Operators.re +++ b/src/haz3lcore/lang/Operators.re @@ -1,21 +1,21 @@ -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_un_bool = | Not; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_un_meta = | Unquote; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_un_int = | Minus; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_bin_bool = | And | Or; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_bin_int = | Plus | Minus @@ -29,7 +29,7 @@ type op_bin_int = | Equals | NotEquals; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_bin_float = | Plus | Minus @@ -43,25 +43,25 @@ type op_bin_float = | Equals | NotEquals; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_bin_string = | Concat | Equals; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_un = | Meta(op_un_meta) | Int(op_un_int) | Bool(op_un_bool); -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type op_bin = | Int(op_bin_int) | Float(op_bin_float) | Bool(op_bin_bool) | String(op_bin_string); -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type ap_direction = | Forward | Reverse; diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/haz3lcore/lang/term/IdTagged.re index 3812b0e83f..d701d14de1 100644 --- a/src/haz3lcore/lang/term/IdTagged.re +++ b/src/haz3lcore/lang/term/IdTagged.re @@ -14,6 +14,8 @@ type t('a) = { term: 'a, }; +// TODO This fully ignores ids for equality +let equal = (eq, a, b) => eq(a.term, b.term); // To be used if you want to remove the id from the debug output // let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit = // (fmt_a, formatter, ta) => { diff --git a/src/haz3lcore/statics/Var.re b/src/haz3lcore/statics/Var.re index 68c3d9d1b3..c52558d0ec 100644 --- a/src/haz3lcore/statics/Var.re +++ b/src/haz3lcore/statics/Var.re @@ -1,6 +1,6 @@ open Util; -[@deriving (show({with_path: false}), sexp, yojson)] +[@deriving (show({with_path: false}), sexp, yojson, eq)] type t = string; let eq = String.equal; diff --git a/src/haz3lcore/tiles/Id.re b/src/haz3lcore/tiles/Id.re index 5046dd63c5..ac80856592 100644 --- a/src/haz3lcore/tiles/Id.re +++ b/src/haz3lcore/tiles/Id.re @@ -58,6 +58,7 @@ let t_of_yojson: Yojson.Safe.t => Uuidm.t = type t = Uuidm.t; +let equal: (t, t) => bool = (==); let mk: unit => t = Uuidm.v4_gen(Random.State.make_self_init()); let compare: (t, t) => int = Uuidm.compare;