creusot_contracts/logic/
set.rs

1use crate::{logic::Mapping, prelude::*};
2use std::marker::PhantomData;
3
4/// A (possibly infinite) set type.
5#[opaque]
6#[builtin("set.Set.set")]
7pub struct Set<T: ?Sized>(PhantomData<T>);
8
9impl<T: ?Sized> Set<T> {
10    /// The empty set.
11    #[logic]
12    #[builtin("set.Set.empty", ascription)]
13    pub fn empty() -> Self {
14        dead
15    }
16
17    /// Build a set from a predicate, given as a `Mapping`.
18    #[logic]
19    #[builtin("identity")]
20    pub fn from_predicate(_: Mapping<T, bool>) -> Self {
21        dead
22    }
23
24    /// Returns `true` if `e` is in the set.
25    #[logic(open, inline)]
26    pub fn contains(self, e: T) -> bool {
27        Self::mem(e, self)
28    }
29
30    /// [`Self::contains`], but with the order of arguments flipped.
31    ///
32    /// This is how the function is defined in why3.
33    #[doc(hidden)]
34    #[logic]
35    #[builtin("set.Set.mem")]
36    pub fn mem(_: T, _: Self) -> bool {
37        dead
38    }
39
40    /// Returns a new set, where `e` has been added if it was not present.
41    #[logic(open, inline)]
42    pub fn insert(self, e: T) -> Self {
43        Self::add(e, self)
44    }
45
46    /// [`Self::insert`], but with the order of arguments flipped.
47    ///
48    /// This is how the function is defined in why3.
49    #[doc(hidden)]
50    #[logic]
51    #[builtin("set.Set.add")]
52    pub fn add(_: T, _: Self) -> Self {
53        dead
54    }
55
56    /// Returns `true` if the set contains no elements.
57    #[logic]
58    #[builtin("set.Set.is_empty")]
59    pub fn is_empty(self) -> bool {
60        dead
61    }
62
63    /// Returns a new set, where `e` is no longer present.
64    #[logic(open, inline)]
65    pub fn remove(self, a: T) -> Self {
66        Self::rem(a, self)
67    }
68
69    /// [`Self::remove`], but with the order of arguments flipped.
70    ///
71    /// This is how the function is defined in why3.
72    #[doc(hidden)]
73    #[logic]
74    #[builtin("set.Set.remove")]
75    pub fn rem(_: T, _: Self) -> Self {
76        dead
77    }
78
79    /// Returns a new set, which is the union of `self` and `other`.
80    ///
81    /// An element is in the result if it is in `self` _or_ if it is in `other`.
82    #[logic]
83    #[builtin("set.Set.union")]
84    pub fn union(self, _: Self) -> Self {
85        dead
86    }
87}
creusot_contracts/logic/set.rs

creusot_contracts/logic/
set.rs
