1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
use crate::{logic::ops::IndexLogic, *};
/// A mapping: map every value of type `A` to a value of type `B`.
///
/// # Pearlite syntax
///
/// Mappings have special support in pearlite code: you may write a closure to create a
/// mapping.
///
/// ## Example
///
/// ```
/// # use creusot_contracts::{logic::Mapping, *};
/// let value = snapshot!(4);
/// let map: Snapshot<Mapping<Int, Int>> = snapshot!(|n| if n % 2 == 0 { 0 } else { *value });
/// proof_assert!(map.get(1) == 4);
/// ```
#[trusted]
#[cfg_attr(creusot, creusot::builtins = "map.Map.map")]
pub struct Mapping<A: ?Sized, B: ?Sized>(std::marker::PhantomData<A>, std::marker::PhantomData<B>);
impl<A: ?Sized, B: ?Sized> Mapping<A, B> {
/// Get the value associated with `a` in the map.
#[trusted]
#[logic]
#[creusot::builtins = "map.Map.get"]
#[allow(unused_variables)]
pub fn get(self, a: A) -> B
where
B: Sized, // TODO : don't require this (problem: return type needs to be sized)
{
dead
}
/// Returns a new mapping, where `a` is now mapped to `b`.
#[trusted]
#[logic]
#[creusot::builtins = "map.Map.set"]
#[allow(unused_variables)]
pub fn set(self, a: A, b: B) -> Self {
dead
}
/// Create a mapping, where every value of type `a` is mapped to `b`.
#[trusted]
#[logic]
#[creusot::builtins = "map.Const.const"]
#[allow(unused_variables)]
pub fn cst(b: B) -> Self {
dead
}
}
impl<A: ?Sized, B> IndexLogic<A> for Mapping<A, B> {
type Item = B;
#[logic]
#[open]
fn index_logic(self, a: A) -> B {
self.get(a)
}
}