formally_support/
nominal.rs

1//
2// ::formally - the open-source formal methods toolchain
3//
4// Copyright (c) 2025 Nicola Gigante
5//
6// Permission is hereby granted, free of charge, to any person obtaining a copy
7// of this software and associated documentation files (the "Software"), to deal
8// in the Software without restriction, including without limitation the rights
9// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10// copies of the Software, and to permit persons to whom the Software is
11// furnished to do so, subject to the following conditions:
12//
13// The above copyright notice and this permission notice shall be included in
14// all copies or substantial portions of the Software.
15//
16// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
22// SOFTWARE.
23//
24
25use derive_more::From;
26use std::{
27    fmt::{Debug, Formatter},
28    hash::{Hash, Hasher},
29    ops::Deref,
30};
31
32/// Smart pointer wrapper for identity-based equality comparisons and hashing
33///
34/// [Nominal] wraps a [Deref] object to implement [Eq] and [Hash] based on the *value of the
35/// reference* to the pointee, instead of its eventual [Eq] and [Hash] instances.
36///
37/// This means wrapping a pointer or reference in a [Nominal] makes it compare and hash based on its
38/// identity as an object instead of its value, which would be the default in Rust.
39///
40/// In `formally`, this is used in places where two objects with the same value must nevertheless
41/// be considered distinct, most prominently the `Declared` and `Defined` types in the `smt` crate.
42#[derive(Clone, Default, From)]
43#[from(T)]
44#[repr(transparent)]
45pub struct Nominal<T>(pub T);
46
47impl<T> Nominal<T> {
48    /// Turns the [Nominal] into its underlying object.
49    pub fn into_inner(self) -> T {
50        self.0
51    }
52}
53
54impl<T> AsRef<T> for Nominal<T> {
55    fn as_ref(&self) -> &T {
56        &self.0
57    }
58}
59
60impl<T: Debug> Debug for Nominal<T> {
61    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
62        write!(f, "Nominal({:?})", self.0)
63    }
64}
65
66impl<T: Deref> Hash for Nominal<T> {
67    fn hash<H: Hasher>(&self, state: &mut H) {
68        let ptr = &*self.0 as *const T::Target;
69        ptr.hash(state)
70    }
71}
72
73impl<T: Deref> PartialEq for Nominal<T> {
74    fn eq(&self, other: &Self) -> bool {
75        let this = &*self.0 as *const T::Target;
76        let other = &*other.0 as *const T::Target;
77
78        std::ptr::eq(this, other)
79    }
80}
81
82impl<T: Deref> Eq for Nominal<T> {}
83
84impl<T> Deref for Nominal<T> {
85    type Target = T;
86
87    fn deref(&self) -> &T {
88        &self.0
89    }
90}
formally_support/nominal.rs

formally_support/
nominal.rs
