creusot_contracts/
model.rs

1//! Logical models of types: [`View`] and [`DeepModel`]
2use crate::*;
3
4/// The view of a type is its logical model as typically used to specify a data
5/// structure. It is typically "shallow", and does not involve the model of
6/// other types contained by the datastructure.
7/// This kind of model is mostly useful for notation purposes,
8/// because this trait is linked to the `@` notation of pearlite.
9#[diagnostic::on_unimplemented(
10    message = "Cannot take the view of `{Self}`",
11    label = "no implementation for `{Self}@`"
12)]
13pub trait View {
14    type ViewTy;
15    #[logic]
16    fn view(self) -> Self::ViewTy;
17}
18
19pub use crate::base_macros::DeepModel;
20
21/// The deep model corresponds to the model used for specifying
22/// operations such as equality, hash function or ordering, which are
23/// computed deeply in a data structure.
24/// Typically, such a model recursively calls deep models of inner types.
25pub trait DeepModel {
26    type DeepModelTy;
27    #[logic]
28    fn deep_model(self) -> Self::DeepModelTy;
29}
30
31impl<T: DeepModel + ?Sized> DeepModel for &T {
32    type DeepModelTy = T::DeepModelTy;
33    #[logic(open, inline)]
34    fn deep_model(self) -> Self::DeepModelTy {
35        (*self).deep_model()
36    }
37}
38
39impl<T: View + ?Sized> View for &T {
40    type ViewTy = T::ViewTy;
41    #[logic(open, inline)]
42    fn view(self) -> Self::ViewTy {
43        (*self).view()
44    }
45}
46
47impl<T: DeepModel + ?Sized> DeepModel for &mut T {
48    type DeepModelTy = T::DeepModelTy;
49    #[logic(open, inline)]
50    fn deep_model(self) -> Self::DeepModelTy {
51        (*self).deep_model()
52    }
53}
54
55impl<T: View + ?Sized> View for &mut T {
56    type ViewTy = T::ViewTy;
57    #[logic(open, inline)]
58    fn view(self) -> Self::ViewTy {
59        (*self).view()
60    }
61}
62
63impl DeepModel for bool {
64    type DeepModelTy = bool;
65
66    #[logic(open, inline)]
67    fn deep_model(self) -> Self::DeepModelTy {
68        self
69    }
70}
71
72impl DeepModel for Int {
73    type DeepModelTy = Int;
74
75    #[logic(open, inline)]
76    fn deep_model(self) -> Self::DeepModelTy {
77        self
78    }
79}
80
81impl View for String {
82    type ViewTy = Seq<char>;
83
84    #[logic(opaque)]
85    fn view(self) -> Self::ViewTy {
86        dead
87    }
88}
89
90impl DeepModel for std::cmp::Ordering {
91    type DeepModelTy = std::cmp::Ordering;
92
93    #[logic(open, inline)]
94    fn deep_model(self) -> Self::DeepModelTy {
95        self
96    }
97}
creusot_contracts/model.rs

creusot_contracts/
model.rs
