From 4308ca649fcdf2a87bad6831450f230805cbd61e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:43:45 -0700 Subject: [PATCH] [sledge] Remove unnecessary hash functions Reviewed By: ngorogiannis Differential Revision: D22170519 fbshipit-source-id: 2c916272a --- sledge/src/fol.mli | 5 ++--- sledge/src/ses/term.ml | 22 ++++++---------------- sledge/src/ses/term.mli | 19 ++++++++----------- 3 files changed, 16 insertions(+), 30 deletions(-) diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index f3d95cdd3..11a20c71b 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -7,7 +7,7 @@ (** Variables *) module Var : sig - type t [@@deriving compare, equal, hash, sexp] + type t [@@deriving compare, equal, sexp] type strength = t -> [`Universal | `Existential | `Anonymous] option val pp : t pp @@ -17,7 +17,6 @@ module Var : sig module Set : sig include NS.Set.S with type elt := t - val hash_fold_t : t Hash.folder val sexp_of_t : t -> Sexp.t val t_of_sexp : Sexp.t -> t val ppx : strength -> t pp @@ -58,7 +57,7 @@ end (** Terms *) module Term : sig - type t [@@deriving compare, equal, hash, sexp] + type t [@@deriving compare, equal, sexp] val ppx : Var.strength -> t pp val pp : t pp diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml index 66ad524a8..f19f45ca3 100644 --- a/sledge/src/ses/term.ml +++ b/sledge/src/ses/term.ml @@ -40,35 +40,25 @@ type opN = Concat | Record [@@deriving compare, equal, hash, sexp] module rec Set : sig include NS.Set.S with type elt := T.t - val hash : t -> int - val hash_fold_t : t Hash.folder val t_of_sexp : Sexp.t -> t end = struct include NS.Set.Make (T) - - let hash_fold_t = hash_fold_t T.hash_fold_t - let hash = Hash.of_fold hash_fold_t - include Provide_of_sexp (T) end and Qset : sig include NS.Qset.S with type elt := T.t - val hash : t -> int - val hash_fold_t : t Hash.folder val t_of_sexp : Sexp.t -> t end = struct include NS.Qset.Make (T) - let hash_fold_t = hash_fold_t T.hash_fold_t - let hash = Hash.of_fold hash_fold_t let t_of_sexp = t_of_sexp T.t_of_sexp end and T : sig - type set = Set.t [@@deriving compare, equal, hash, sexp] - type qset = Qset.t [@@deriving compare, equal, hash, sexp] + type set = Set.t [@@deriving compare, equal, sexp] + type qset = Qset.t [@@deriving compare, equal, sexp] type t = | Var of {id: int; name: string} @@ -85,10 +75,10 @@ and T : sig | Integer of {data: Z.t} | Rational of {data: Q.t} | RecRecord of int - [@@deriving compare, equal, hash, sexp] + [@@deriving compare, equal, sexp] end = struct - type set = Set.t [@@deriving compare, equal, hash, sexp] - type qset = Qset.t [@@deriving compare, equal, hash, sexp] + type set = Set.t [@@deriving compare, equal, sexp] + type qset = Qset.t [@@deriving compare, equal, sexp] type t = | Var of {id: int; name: string} @@ -105,7 +95,7 @@ end = struct | Integer of {data: Z.t} | Rational of {data: Q.t} | RecRecord of int - [@@deriving compare, equal, hash, sexp] + [@@deriving compare, equal, sexp] (* Note: solve (and invariant) requires Qset.min_elt to return a non-coefficient, so Integer and Rational terms must compare higher than diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli index 017e85605..445927e47 100644 --- a/sledge/src/ses/term.mli +++ b/sledge/src/ses/term.mli @@ -26,7 +26,7 @@ type op1 = [Integer] types. *) | Splat (** Iterated concatenation of a single byte *) | Select of int (** Select an index from a record *) -[@@deriving compare, equal, hash, sexp] +[@@deriving compare, equal, sexp] type op2 = | Eq (** Equal test *) @@ -45,36 +45,34 @@ type op2 = | Ashr (** Arithmetic shift right, bitwise *) | Sized (** Size-tagged sequence *) | Update of int (** Constant record with updated index *) -[@@deriving compare, equal, hash, sexp] +[@@deriving compare, equal, sexp] type op3 = | Conditional (** If-then-else *) | Extract (** Extract a slice of an sequence value *) -[@@deriving compare, equal, hash, sexp] +[@@deriving compare, equal, sexp] type opN = | Concat (** Byte-array concatenation *) | Record (** Record (array / struct) constant *) -[@@deriving compare, equal, hash, sexp] +[@@deriving compare, equal, sexp] module rec Set : sig include NS.Set.S with type elt := T.t - val hash_fold_t : t Hash.folder val t_of_sexp : Sexp.t -> t end and Qset : sig include NS.Qset.S with type elt := T.t - val hash_fold_t : t Hash.folder val t_of_sexp : Sexp.t -> t end and T : sig - type set = Set.t [@@deriving compare, equal, hash, sexp] + type set = Set.t [@@deriving compare, equal, sexp] - type qset = Qset.t [@@deriving compare, equal, hash, sexp] + type qset = Qset.t [@@deriving compare, equal, sexp] and t = private | Var of {id: int; name: string} @@ -93,7 +91,7 @@ and T : sig | Integer of {data: Z.t} (** Integer constant *) | Rational of {data: Q.t} (** Rational constant *) | RecRecord of int (** Reference to ancestor recursive record *) - [@@deriving compare, equal, hash, sexp] + [@@deriving compare, equal, sexp] end include module type of T with type t = T.t @@ -101,7 +99,7 @@ include module type of T with type t = T.t (** Term.Var is re-exported as Var *) module Var : sig type term := t - type t = private term [@@deriving compare, equal, hash, sexp] + type t = private term [@@deriving compare, equal, sexp] type strength = t -> [`Universal | `Existential | `Anonymous] option module Map : Map.S with type key := t @@ -109,7 +107,6 @@ module Var : sig module Set : sig include NS.Set.S with type elt := t - val hash_fold_t : t Hash.folder val sexp_of_t : t -> Sexp.t val t_of_sexp : Sexp.t -> t val ppx : strength -> t pp