verdict_parser/common/
option_deep.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// An Option type with "deep" View
7#[derive(Debug, View, PolyfillClone, Structural, Eq, PartialEq)]
8pub enum OptionDeep<T> {
9    Some(T),
10    None,
11}
12
13impl<T> OptionDeep<T> {
14    pub open spec fn spec_unwrap_or(self, default: T) -> T {
15        match self {
16            OptionDeep::Some(t) => t,
17            OptionDeep::None => default,
18        }
19    }
20
21    #[verifier::when_used_as_spec(spec_unwrap_or)]
22    #[inline(always)]
23    pub fn unwrap_or(self, default: T) -> (res: T)
24        ensures res == self.spec_unwrap_or(default)
25    {
26        match self {
27            OptionDeep::Some(t) => t,
28            OptionDeep::None => default,
29        }
30    }
31
32    pub open spec fn spec_as_ref(&self) -> Option<&T> {
33        match self {
34            OptionDeep::Some(t) => Some(t),
35            OptionDeep::None => None,
36        }
37    }
38
39    #[verifier::when_used_as_spec(spec_as_ref)]
40    #[inline(always)]
41    pub fn as_ref(&self) -> (res: Option<&T>)
42        ensures res == self.spec_as_ref()
43    {
44        match self {
45            OptionDeep::Some(t) => Some(t),
46            OptionDeep::None => None,
47        }
48    }
49
50    pub open spec fn spec_from_opt(opt: Option<T>) -> Self {
51        match opt {
52            Some(t) => OptionDeep::Some(t),
53            None => OptionDeep::None,
54        }
55    }
56
57    #[verifier::when_used_as_spec(spec_from_opt)]
58    #[inline(always)]
59    pub fn from_opt(opt: Option<T>) -> (res: Self)
60        ensures res == Self::spec_from_opt(opt)
61    {
62        match opt {
63            Some(t) => OptionDeep::Some(t),
64            None => OptionDeep::None,
65        }
66    }
67
68    pub open spec fn spec_to_opt(self) -> Option<T> {
69        match self {
70            OptionDeep::Some(t) => Some(t),
71            OptionDeep::None => None,
72        }
73    }
74
75    #[verifier::when_used_as_spec(spec_to_opt)]
76    #[inline(always)]
77    pub fn to_opt(self) -> (res: Option<T>)
78        ensures res == self.spec_to_opt()
79    {
80        match self {
81            OptionDeep::Some(t) => Some(t),
82            OptionDeep::None => None,
83        }
84    }
85}
86
87}
verdict_parser/common/option_deep.rs

verdict_parser/common/
option_deep.rs
