Revert "Implement Eq and Hash for Type"

This reverts commit 91af963.

Author: coord-e

src/chc.rs

@@ -389,7 +389,7 @@ impl Function {
 }
 
 /// A logical term.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub enum Term<V = TermVarIdx> {
     Null,
     Var(V),
@@ -988,7 +988,7 @@ impl Pred {
 }
 
 /// An atom is a predicate applied to a list of terms.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct Atom<V = TermVarIdx> {
     pub pred: Pred,
     pub args: Vec<Term<V>>,
@@ -1081,7 +1081,7 @@ impl<V> Atom<V> {
 /// While it allows arbitrary [`Atom`] in its `Atom` variant, we only expect atoms with known
 /// predicates (i.e., predicates other than `Pred::Var`) to appear in formulas. It is our TODO to
 /// enforce this restriction statically. Also see the definition of [`Body`].
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub enum Formula<V = TermVarIdx> {
     Atom(Atom<V>),
     Not(Box<Formula<V>>),
@@ -1300,7 +1300,7 @@ impl<V> Formula<V> {
 }
 
 /// The body part of a clause, consisting of atoms and a formula.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct Body<V = TermVarIdx> {
     pub atoms: Vec<Atom<V>>,
     /// NOTE: This doesn't contain predicate variables. Also see [`Formula`].

src/rty.rs

@@ -118,7 +118,7 @@ impl FunctionAbi {
 /// In Thrust, function types are closed. Because of that, function types, thus its parameters and
 /// return type only refer to the parameters of the function itself using [`FunctionParamIdx`] and
 /// do not accept other type of variables from the environment.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct FunctionType {
     pub params: IndexVec<FunctionParamIdx, RefinedType<FunctionParamIdx>>,
     pub ret: Box<RefinedType<FunctionParamIdx>>,
@@ -203,7 +203,7 @@ impl FunctionType {
 }
 
 /// The kind of a reference, which is either mutable or immutable.
-#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum RefKind {
     Mut,
     Immut,
@@ -228,7 +228,7 @@ where
 }
 
 /// The kind of a pointer, which is either a reference or an owned pointer.
-#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum PointerKind {
     Ref(RefKind),
     Own,
@@ -268,7 +268,7 @@ impl PointerKind {
 }
 
 /// A pointer type.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct PointerType<T> {
     pub kind: PointerKind,
     pub elem: Box<RefinedType<T>>,
@@ -381,7 +381,7 @@ impl<T> PointerType<T> {
 /// Note that the current implementation uses tuples to represent structs. See
 /// implementation in `crate::refine::template` module for details.
 /// It is our TODO to improve the struct representation.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct TupleType<T> {
     pub elems: Vec<RefinedType<T>>,
 }
@@ -505,7 +505,7 @@ impl EnumDatatypeDef {
 /// An enum type.
 ///
 /// An enum type includes its type arguments and the argument types can refer to outer variables `T`.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct EnumType<T> {
     pub symbol: chc::DatatypeSymbol,
     pub args: IndexVec<TypeParamIdx, RefinedType<T>>,
@@ -607,7 +607,7 @@ impl<T> EnumType<T> {
 }
 
 /// A type parameter.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct ParamType {
     pub idx: TypeParamIdx,
 }
@@ -636,7 +636,7 @@ impl ParamType {
 }
 
 /// An underlying type of a refinement type.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub enum Type<T> {
     Int,
     Bool,
@@ -1042,7 +1042,7 @@ impl<T> ShiftExistential for RefinedTypeVar<T> {
 /// A formula, potentially equipped with an existential quantifier.
 ///
 /// Note: This is not to be confused with [`crate::chc::Formula`] in the [`crate::chc`] module, which is a different notion.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct Formula<V> {
     pub existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
     pub body: chc::Body<V>,
@@ -1283,7 +1283,7 @@ impl<T> Instantiator<T> {
 }
 
 /// A refinement type.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone)]
 pub struct RefinedType<FV = Closed> {
     pub ty: Type<FV>,
     pub refinement: Refinement<FV>,