creusot_std/
model.rs

1//! Logical models of types: [`View`] and [`DeepModel`]
2use crate::prelude::*;
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    #[intrinsic("view")]
17    fn view(self) -> Self::ViewTy;
18}
19
20pub use crate::base_macros::DeepModel;
21
22/// The deep model corresponds to the model used for specifying
23/// operations such as equality, hash function or ordering, which are
24/// computed deeply in a data structure.
25/// Typically, such a model recursively calls deep models of inner types.
26pub trait DeepModel {
27    type DeepModelTy;
28    #[logic]
29    fn deep_model(self) -> Self::DeepModelTy;
30}
31
32impl<T: DeepModel + ?Sized> DeepModel for &T {
33    type DeepModelTy = T::DeepModelTy;
34    #[logic(open, inline)]
35    fn deep_model(self) -> Self::DeepModelTy {
36        (*self).deep_model()
37    }
38}
39
40impl<T: DeepModel + ?Sized> DeepModel for &mut T {
41    type DeepModelTy = T::DeepModelTy;
42    #[logic(open, inline)]
43    fn deep_model(self) -> Self::DeepModelTy {
44        (*self).deep_model()
45    }
46}
47
48impl DeepModel for bool {
49    type DeepModelTy = bool;
50
51    #[logic(open, inline)]
52    fn deep_model(self) -> Self::DeepModelTy {
53        self
54    }
55}
56
57impl DeepModel for Int {
58    type DeepModelTy = Int;
59
60    #[logic(open, inline)]
61    fn deep_model(self) -> Self::DeepModelTy {
62        self
63    }
64}
65
66#[cfg(feature = "std")]
67impl View for String {
68    type ViewTy = Seq<char>;
69
70    #[logic(opaque)]
71    fn view(self) -> Self::ViewTy {
72        dead
73    }
74}
75
76impl DeepModel for core::cmp::Ordering {
77    type DeepModelTy = core::cmp::Ordering;
78
79    #[logic(open, inline)]
80    fn deep_model(self) -> Self::DeepModelTy {
81        self
82    }
83}
creusot_std/model.rs

creusot_std/
model.rs
