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
21pub use crate::base_macros::DeepModel;
22
23/// The deep model corresponds to the model used for specifying
24/// operations such as equality, hash function or ordering, which are
25/// computed deeply in a data structure.
26/// Typically, such a model recursively calls deep models of inner types.
27pub trait DeepModel {
28    type DeepModelTy;
29    #[logic]
30    fn deep_model(self) -> Self::DeepModelTy;
31}
32
33impl<T: DeepModel + ?Sized> DeepModel for &T {
34    type DeepModelTy = T::DeepModelTy;
35    #[logic(open, inline)]
36    fn deep_model(self) -> Self::DeepModelTy {
37        (*self).deep_model()
38    }
39}
40
41impl<T: DeepModel + ?Sized> DeepModel for &mut T {
42    type DeepModelTy = T::DeepModelTy;
43    #[logic(open, inline)]
44    fn deep_model(self) -> Self::DeepModelTy {
45        (*self).deep_model()
46    }
47}
48
49impl DeepModel for bool {
50    type DeepModelTy = bool;
51
52    #[logic(open, inline)]
53    fn deep_model(self) -> Self::DeepModelTy {
54        self
55    }
56}
57
58impl DeepModel for Int {
59    type DeepModelTy = Int;
60
61    #[logic(open, inline)]
62    fn deep_model(self) -> Self::DeepModelTy {
63        self
64    }
65}
66
67impl DeepModel for Ordering {
68    type DeepModelTy = Ordering;
69
70    #[logic(open, inline)]
71    fn deep_model(self) -> Self::DeepModelTy {
72        self
73    }
74}
creusot_std/model.rs

creusot_std/
model.rs
