creusot_std/
model.rs

1//! Logical models of types: [`View`] and [`DeepModel`]
2use crate::prelude::*;
3use core::cmp::Ordering;
4
5/// The view of a type is its logical model as typically used to specify a data
6/// structure. It is typically "shallow", and does not involve the model of
7/// other types contained by the datastructure.
8/// This kind of model is mostly useful for notation purposes,
9/// because this trait is linked to the `@` notation of pearlite.
10#[diagnostic::on_unimplemented(
11    message = "Cannot take the view of `{Self}`",
12    label = "no implementation for `{Self}@`"
13)]
14pub trait View {
15    type ViewTy;
16    #[logic]
17    #[intrinsic("view")]
18    fn view(self) -> Self::ViewTy;
19}
20
21/// The derive macro for the `DeepModel` trait.
22///
23/// This macro can be used to implement `DeepModel` by recursively delegating into `DeepModel` of
24/// each individual field. For a struct, it generates a new struct and for an enum it generates a
25/// new enum. Other types are not supported. The generated type is named the same as the type this
26/// is derived for with the `DeepModel` suffix appended to it.
27///
28/// The visibility of the generated types and their fields will be the same (including the
29/// `non_exhaustive` attribute, if present) and the types of the fields will be the `DeepModelTy` of
30/// the corresponding field. For instance, `pub struct Foo { bar: u32 }` will become
31/// `pub struct FooDeepModel { bar: Int }`.
32///
33/// To avoid exposing private fields, the generated `deep_model` method will have openess restricted
34/// to the most restrictive visibility of the type. If the type is public but its field is private,
35/// the resulting openess will be private. `#[non_exhaustive]` acts as if the type had an additional
36/// `pub(crate)` field. The visibility is computed as intersection, so paths `super::super` and
37/// `super` will become `super`. If the visibility cannot be computed precisely a conservative
38/// default is used - the private visibility. Therefore it's not recommended to mix styles of
39/// specifying the visibility - either use relative (`super::super::...`) or absolute
40/// (`crate::foo::bar`) in all items.
41///
42/// While this works well for structs that are either fully private or fully public, mixed
43/// visibility has the consequence that your downstream users may have hard time verifying their
44/// code because it won't see the relationship between the fields of struct and its deep model. This
45/// cannot be solved automatically and in such case a more precise manual implementation may be
46/// required.
47pub use crate::base_macros::DeepModel;
48
49/// The deep model corresponds to the model used for specifying
50/// operations such as equality, hash function or ordering, which are
51/// computed deeply in a data structure.
52/// Typically, such a model recursively calls deep models of inner types.
53pub trait DeepModel {
54    type DeepModelTy;
55    #[logic]
56    fn deep_model(self) -> Self::DeepModelTy;
57}
58
59impl<T: DeepModel + ?Sized> DeepModel for &T {
60    type DeepModelTy = T::DeepModelTy;
61    #[logic(open, inline)]
62    fn deep_model(self) -> Self::DeepModelTy {
63        (*self).deep_model()
64    }
65}
66
67impl<T: DeepModel + ?Sized> DeepModel for &mut T {
68    type DeepModelTy = T::DeepModelTy;
69    #[logic(open, inline)]
70    fn deep_model(self) -> Self::DeepModelTy {
71        (*self).deep_model()
72    }
73}
74
75impl DeepModel for bool {
76    type DeepModelTy = bool;
77
78    #[logic(open, inline)]
79    fn deep_model(self) -> Self::DeepModelTy {
80        self
81    }
82}
83
84impl DeepModel for Int {
85    type DeepModelTy = Int;
86
87    #[logic(open, inline)]
88    fn deep_model(self) -> Self::DeepModelTy {
89        self
90    }
91}
92
93impl DeepModel for Ordering {
94    type DeepModelTy = Ordering;
95
96    #[logic(open, inline)]
97    fn deep_model(self) -> Self::DeepModelTy {
98        self
99    }
100}
creusot_std/model.rs

creusot_std/
model.rs
