From a392493d421aead0d7505f4f1d0dc183bf49aa15 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Tue, 16 Apr 2024 17:08:33 +0200
Subject: [PATCH] clippy: Fix use_self
---
rr_frontend/.cargo/config.toml | 1 -
rr_frontend/analysis/src/analysis_error.rs | 8 +--
rr_frontend/attribute_parse/src/parse.rs | 63 ++++++++++---------
rr_frontend/radium/src/code.rs | 49 +++++++--------
rr_frontend/radium/src/coq.rs | 2 +-
rr_frontend/radium/src/specs.rs | 52 +++++++--------
.../src/environment/borrowck/facts.rs | 12 ++--
.../src/environment/borrowck/regions.rs | 2 +-
.../translation/src/environment/loops.rs | 8 +--
.../src/environment/polonius_info.rs | 4 +-
.../src/spec_parsers/const_attr_parser.rs | 2 +-
.../src/spec_parsers/crate_attr_parser.rs | 2 +-
.../src/spec_parsers/enum_spec_parser.rs | 4 +-
.../translation/src/spec_parsers/mod.rs | 4 +-
.../src/spec_parsers/module_attr_parser.rs | 2 +-
.../src/spec_parsers/parse_utils.rs | 30 ++++-----
.../src/spec_parsers/struct_spec_parser.rs | 26 ++++----
.../verbose_function_spec_parser.rs | 18 +++---
rr_frontend/translation/src/utils.rs | 2 +-
19 files changed, 143 insertions(+), 148 deletions(-)
diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index 8ec3cc54..5783092e 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -30,7 +30,6 @@ rustflags = [
"-Aclippy::empty_line_after_doc_comments",
"-Aclippy::option_if_let_else",
"-Aclippy::string_lit_as_bytes",
- "-Aclippy::use_self",
"-Aclippy::useless_let_if_seq",
# clippy::pedantic
diff --git a/rr_frontend/analysis/src/analysis_error.rs b/rr_frontend/analysis/src/analysis_error.rs
index 5e712f4e..a66c6818 100644
--- a/rr_frontend/analysis/src/analysis_error.rs
+++ b/rr_frontend/analysis/src/analysis_error.rs
@@ -22,19 +22,19 @@ pub enum AnalysisError {
impl AnalysisError {
pub fn to_pretty_str(&self, mir: &mir::Body) -> String {
match self {
- AnalysisError::UnsupportedStatement(location) => {
+ Self::UnsupportedStatement(location) => {
let stmt = location_to_stmt_str(*location, mir);
format!("Unsupported statement at {:?}: {}", location, stmt)
},
- AnalysisError::NoStateBeforeLocation(location) => {
+ Self::NoStateBeforeLocation(location) => {
let stmt = location_to_stmt_str(*location, mir);
format!("There is no state before the statement at {:?} ({})", location, stmt)
},
- AnalysisError::NoStateAfterBlock(bb) => {
+ Self::NoStateAfterBlock(bb) => {
let terminator = &mir[*bb].terminator();
format!("There is no state after the terminator of block {:?} ({:?})", bb, terminator.kind)
},
- AnalysisError::NoStateAfterSuccessor(bb_src, bb_dst) => {
+ Self::NoStateAfterSuccessor(bb_src, bb_dst) => {
let terminator = &mir[*bb_src].terminator();
format!(
"There is no state for the block {:?} after the terminator of block {:?} ({:?})",
diff --git a/rr_frontend/attribute_parse/src/parse.rs b/rr_frontend/attribute_parse/src/parse.rs
index 715367d5..3e493c06 100644
--- a/rr_frontend/attribute_parse/src/parse.rs
+++ b/rr_frontend/attribute_parse/src/parse.rs
@@ -38,20 +38,20 @@ pub trait IntoSpans<S> {
fn into_spans(self) -> S;
}
-impl IntoSpans<[Span; 1]> for Span {
- fn into_spans(self) -> [Span; 1] {
+impl IntoSpans<[Self; 1]> for Span {
+ fn into_spans(self) -> [Self; 1] {
[self]
}
}
-impl IntoSpans<[Span; 2]> for Span {
- fn into_spans(self) -> [Span; 2] {
+impl IntoSpans<[Self; 2]> for Span {
+ fn into_spans(self) -> [Self; 2] {
[self, self]
}
}
-impl IntoSpans<[Span; 3]> for Span {
- fn into_spans(self) -> [Span; 3] {
+impl IntoSpans<[Self; 3]> for Span {
+ fn into_spans(self) -> [Self; 3] {
[self, self, self]
}
}
@@ -122,7 +122,8 @@ impl ParseBuffer {
pub fn new(stream: &rustc_ast::tokenstream::TokenStream) -> Self {
// TODO; maybe avoid the cloning
let trees: Vec<TokenTree> = stream.trees().map(|c| c.clone()).collect();
- ParseBuffer {
+
+ Self {
trees,
index: Cell::new(0),
}
@@ -232,7 +233,7 @@ where
U: ?Sized,
{
fn parse(input: ParseStream, meta: &U) -> ParseResult<Self> {
- input.parse(meta).map(Box::new)
+ input.parse(meta).map(Self::new)
}
}
@@ -461,7 +462,7 @@ where
fn parse(input: ParseStream, _: &U) -> ParseResult<Self> {
let lit = input.expect_literal()?;
match lit.0.kind {
- LitKind::Str => Ok(LitStr {
+ LitKind::Str => Ok(Self {
span: lit.1,
sym: lit.0.symbol,
}),
@@ -481,7 +482,7 @@ where
{
fn parse(input: ParseStream, _: &U) -> ParseResult<Self> {
let (sym, span) = input.expect_ident()?;
- Ok(Ident { span, sym })
+ Ok(Self { span, sym })
}
}
@@ -521,7 +522,7 @@ where
LitKind::Integer => {
let sym = lit.0.symbol;
if let Some((digits, suffix)) = value::parse_lit_int(&sym.to_string()) {
- Ok(LitInt {
+ Ok(Self {
span: lit.1,
sym: lit.0.symbol,
digits: digits,
@@ -655,7 +656,7 @@ pub struct BigInt {
impl BigInt {
pub const fn new() -> Self {
- BigInt { digits: Vec::new() }
+ Self { digits: Vec::new() }
}
pub fn to_string(&self) -> String {
@@ -720,7 +721,7 @@ pub struct Punctuated<T, P> {
impl<T, P> Punctuated<T, P> {
/// Creates an empty punctuated sequence.
pub const fn new() -> Self {
- Punctuated {
+ Self {
inner: Vec::new(),
last: None,
}
@@ -942,7 +943,7 @@ impl<T, P> Punctuated<T, P> {
P: Parse<U>,
U: ?Sized,
{
- let mut punctuated = Punctuated::new();
+ let mut punctuated = Self::new();
loop {
if input.is_empty() {
@@ -999,7 +1000,7 @@ impl<T, P> Punctuated<T, P> {
P: Peek + Parse<U>,
U: ?Sized,
{
- let mut punctuated = Punctuated::new();
+ let mut punctuated = Self::new();
loop {
let value = parser(input, meta)?;
@@ -1022,7 +1023,7 @@ where
P: Default,
{
fn from_iter<I: IntoIterator<Item = T>>(i: I) -> Self {
- let mut ret = Punctuated::new();
+ let mut ret = Self::new();
ret.extend(i);
ret
}
@@ -1041,7 +1042,7 @@ where
impl<T, P> FromIterator<Pair<T, P>> for Punctuated<T, P> {
fn from_iter<I: IntoIterator<Item = Pair<T, P>>>(i: I) -> Self {
- let mut ret = Punctuated::new();
+ let mut ret = Self::new();
ret.extend(i);
ret
}
@@ -1104,7 +1105,7 @@ impl<'a, T, P> IntoIterator for &'a Punctuated<T, P> {
impl<T, P> Default for Punctuated<T, P> {
fn default() -> Self {
- Punctuated::new()
+ Self::new()
}
}
@@ -1244,7 +1245,7 @@ where
P: Clone,
{
fn clone(&self) -> Self {
- IntoPairs {
+ Self {
inner: self.inner.clone(),
last: self.last.clone(),
}
@@ -1289,7 +1290,7 @@ where
T: Clone,
{
fn clone(&self) -> Self {
- IntoIter {
+ Self {
inner: self.inner.clone(),
}
}
@@ -1410,21 +1411,21 @@ impl<T, P> Pair<T, P> {
/// following punctuation.
pub fn into_value(self) -> T {
match self {
- Pair::Punctuated(t, _) | Pair::End(t) => t,
+ Self::Punctuated(t, _) | Self::End(t) => t,
}
}
/// Borrows the syntax tree node from this punctuated pair.
pub const fn value(&self) -> &T {
match self {
- Pair::Punctuated(t, _) | Pair::End(t) => t,
+ Self::Punctuated(t, _) | Self::End(t) => t,
}
}
/// Mutably borrows the syntax tree node from this punctuated pair.
pub fn value_mut(&mut self) -> &mut T {
match self {
- Pair::Punctuated(t, _) | Pair::End(t) => t,
+ Self::Punctuated(t, _) | Self::End(t) => t,
}
}
@@ -1432,8 +1433,8 @@ impl<T, P> Pair<T, P> {
/// the final one and there is no trailing punctuation.
pub const fn punct(&self) -> Option<&P> {
match self {
- Pair::Punctuated(_, p) => Some(p),
- Pair::End(_) => None,
+ Self::Punctuated(_, p) => Some(p),
+ Self::End(_) => None,
}
}
@@ -1441,8 +1442,8 @@ impl<T, P> Pair<T, P> {
/// following punctuation.
pub fn new(t: T, p: Option<P>) -> Self {
match p {
- Some(p) => Pair::Punctuated(t, p),
- None => Pair::End(t),
+ Some(p) => Self::Punctuated(t, p),
+ None => Self::End(t),
}
}
@@ -1450,8 +1451,8 @@ impl<T, P> Pair<T, P> {
/// optional following punctuation.
pub fn into_tuple(self) -> (T, Option<P>) {
match self {
- Pair::Punctuated(t, p) => (t, Some(p)),
- Pair::End(t) => (t, None),
+ Self::Punctuated(t, p) => (t, Some(p)),
+ Self::End(t) => (t, None),
}
}
}
@@ -1463,8 +1464,8 @@ where
{
fn clone(&self) -> Self {
match self {
- Pair::Punctuated(t, p) => Pair::Punctuated(t.clone(), p.clone()),
- Pair::End(t) => Pair::End(t.clone()),
+ Self::Punctuated(t, p) => Self::Punctuated(t.clone(), p.clone()),
+ Self::End(t) => Self::End(t.clone()),
}
}
}
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 6e102b9c..5e52044d 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -137,8 +137,7 @@ impl RustType {
let is_raw = as_use.is_raw();
if let Some(def) = as_use.def {
// translate type parameter instantiations
- let typarams: Vec<_> =
- as_use.ty_params.iter().map(|ty| RustType::of_type(ty, env)).collect();
+ let typarams: Vec<_> = as_use.ty_params.iter().map(|ty| Self::of_type(ty, env)).collect();
let def = def.borrow();
let def = def.as_ref().unwrap();
let ty_name = if is_raw {
@@ -152,14 +151,14 @@ impl RustType {
}
},
Type::Enum(ae_use) => {
- let typarams: Vec<_> = ae_use.ty_params.iter().map(|ty| RustType::of_type(ty, env)).collect();
+ let typarams: Vec<_> = ae_use.ty_params.iter().map(|ty| Self::of_type(ty, env)).collect();
let def = ae_use.def.borrow();
let def = def.as_ref().unwrap();
Self::Lit(vec![def.public_type_name().to_string()], typarams)
},
Type::LiteralParam(lit) => Self::TyVar(lit.rust_name.clone()),
Type::Literal(lit) => {
- let typarams: Vec<_> = lit.params.iter().map(|ty| RustType::of_type(ty, env)).collect();
+ let typarams: Vec<_> = lit.params.iter().map(|ty| Self::of_type(ty, env)).collect();
Self::Lit(vec![lit.def.type_term.clone()], typarams)
},
Type::Uninit(_) => {
@@ -313,9 +312,9 @@ pub enum Expr {
}
impl Expr {
- pub fn with_optional_annotation(e: Expr, a: Option<Annotation>, why: Option<String>) -> Expr {
+ pub fn with_optional_annotation(e: Self, a: Option<Annotation>, why: Option<String>) -> Self {
match a {
- Some(a) => Expr::Annot {
+ Some(a) => Self::Annot {
a,
e: Box::new(e),
why,
@@ -583,27 +582,27 @@ impl Stmt {
let ind = make_indent(indent);
let ind = ind.as_str();
match self {
- Stmt::GotoBlock(block) => {
+ Self::GotoBlock(block) => {
format!("{ind}Goto \"_bb{}\"", block)
},
- Stmt::Return(e) => {
+ Self::Return(e) => {
format!("{ind}return ({})", e)
},
- Stmt::Assign { ot, e1, e2, s } => {
+ Self::Assign { ot, e1, e2, s } => {
let formatted_s = s.caesium_fmt(indent);
format!("{ind}{} <-{{ {} }} {};\n{}", e1, ot, e2, formatted_s.as_str())
},
- Stmt::ExprS { e, s } => {
+ Self::ExprS { e, s } => {
let formatted_s = s.caesium_fmt(indent);
format!("{ind}expr: {};\n{}", e, formatted_s.as_str())
},
- Stmt::Annot { a, s, why } => {
+ Self::Annot { a, s, why } => {
let formatted_s = s.caesium_fmt(indent);
let why_fmt = if let Some(why) = why { format!(" (* {why} *)") } else { format!("") };
format!("{ind}annot: {};{why_fmt}\n{}", a, formatted_s.as_str())
},
- Stmt::If { ot, e, s1, s2 } => {
+ Self::If { ot, e, s1, s2 } => {
let formatted_s1 = s1.caesium_fmt(indent + 1);
let formatted_s2 = s2.caesium_fmt(indent + 1);
format!(
@@ -614,14 +613,14 @@ impl Stmt {
formatted_s2.as_str()
)
},
- Stmt::AssertS { e, s } => {
+ Self::AssertS { e, s } => {
let formatted_s = s.caesium_fmt(indent);
format!("{ind}assert{{ {} }}: {};\n{}", OpType::BoolOp, e, formatted_s)
},
- Stmt::Stuck => {
+ Self::Stuck => {
format!("{ind}StuckS")
},
- Stmt::Switch {
+ Self::Switch {
e,
it,
index_map,
@@ -656,9 +655,9 @@ impl Stmt {
}
/// Annotate a statement with a list of annotations
- pub fn with_annotations(mut s: Stmt, a: Vec<Annotation>, why: Option<String>) -> Stmt {
+ pub fn with_annotations(mut s: Self, a: Vec<Annotation>, why: Option<String>) -> Self {
for annot in a.into_iter() {
- s = Stmt::Annot {
+ s = Self::Annot {
a: annot,
s: Box::new(s),
why: why.clone(),
@@ -876,14 +875,10 @@ pub struct StackMap {
impl StackMap {
pub fn new() -> Self {
- let local_map = Vec::new();
- let arg_map = Vec::new();
- let names = HashSet::new();
-
- StackMap {
- arg_map,
- local_map,
- used_names: names,
+ Self {
+ arg_map: Vec::new(),
+ local_map: Vec::new(),
+ used_names: HashSet::new(),
}
}
@@ -938,8 +933,8 @@ pub struct FunctionCodeBuilder {
}
impl FunctionCodeBuilder {
- pub fn new() -> FunctionCodeBuilder {
- FunctionCodeBuilder {
+ pub fn new() -> Self {
+ Self {
stack_layout: StackMap::new(),
basic_blocks: BTreeMap::new(),
}
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index 84fde962..3b63f2f0 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -221,7 +221,7 @@ impl CoqType {
/// index `i` in the vector).
/// The types in `substi` should not contain variables themselves, as this substitution
/// operation is capture-incurring!
- pub fn subst(&mut self, substi: &Vec<CoqType>) {
+ pub fn subst(&mut self, substi: &Vec<Self>) {
match self {
Self::Ttype(box t) => t.subst(substi),
Self::Prod(v) => {
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index a63c458a..e0e54611 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -85,18 +85,18 @@ pub enum IntType {
impl Display for IntType {
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
match self {
- IntType::I8 => write!(f, "I8"),
- IntType::I16 => write!(f, "I16"),
- IntType::I32 => write!(f, "I32"),
- IntType::I64 => write!(f, "I64"),
- IntType::I128 => write!(f, "I128"),
- IntType::U8 => write!(f, "U8"),
- IntType::U16 => write!(f, "U16"),
- IntType::U32 => write!(f, "U32"),
- IntType::U64 => write!(f, "U64"),
- IntType::U128 => write!(f, "U128"),
- IntType::ISize => write!(f, "ISize"),
- IntType::USize => write!(f, "USize"),
+ Self::I8 => write!(f, "I8"),
+ Self::I16 => write!(f, "I16"),
+ Self::I32 => write!(f, "I32"),
+ Self::I64 => write!(f, "I64"),
+ Self::I128 => write!(f, "I128"),
+ Self::U8 => write!(f, "U8"),
+ Self::U16 => write!(f, "U16"),
+ Self::U32 => write!(f, "U32"),
+ Self::U64 => write!(f, "U64"),
+ Self::U128 => write!(f, "U128"),
+ Self::ISize => write!(f, "ISize"),
+ Self::USize => write!(f, "USize"),
}
}
}
@@ -235,7 +235,7 @@ impl Display for SynType {
impl SynType {
fn layout_term_core<F, G>(&self, env: &[Option<F>], to_syntype: G) -> Layout
where
- G: Fn(&F) -> SynType,
+ G: Fn(&F) -> Self,
{
match self {
Self::Int(it) => Layout::IntLayout(*it),
@@ -260,17 +260,17 @@ impl SynType {
/// Get a Coq term for the layout of this syntactic type.
/// This may call the Coq-level layout algorithm that we assume.
pub fn layout_term_typaram(&self, env: &[Option<LiteralTyParam>]) -> Layout {
- self.layout_term_core(env, |x| SynType::Literal(x.syn_type.clone()))
+ self.layout_term_core(env, |x| Self::Literal(x.syn_type.clone()))
}
/// See `layout_term_typaram`.
- pub fn layout_term(&self, env: &[Option<SynType>]) -> Layout {
+ pub fn layout_term(&self, env: &[Option<Self>]) -> Layout {
self.layout_term_core(env, |x| x.clone())
}
fn optype_core<F, G>(&self, env: &[Option<F>], to_syntype: G) -> OpType
where
- G: Fn(&F) -> SynType,
+ G: Fn(&F) -> Self,
{
match self {
Self::Int(it) => OpType::IntOp(*it),
@@ -296,11 +296,11 @@ impl SynType {
/// Note that we may also always use UntypedOp, but this here computes the more specific
/// op_type that triggers more UB on invalid values.
pub fn optype_typaram(&self, env: &[Option<LiteralTyParam>]) -> OpType {
- self.optype_core(env, |x| SynType::Literal(x.syn_type.clone()))
+ self.optype_core(env, |x| Self::Literal(x.syn_type.clone()))
}
/// See `optype_typaram`.
- pub fn optype(&self, env: &[Option<SynType>]) -> OpType {
+ pub fn optype(&self, env: &[Option<Self>]) -> OpType {
self.optype_core(env, |x| x.clone())
}
@@ -316,7 +316,7 @@ impl SynType {
/// index `i` in the vector).
/// The types in `substi` should not contain variables themselves, as this substitution
/// operation is capture-incurring!
- pub fn subst(&mut self, substi: &[Option<SynType>]) {
+ pub fn subst(&mut self, substi: &[Option<Self>]) {
match self {
Self::Var(i) => {
if let Some(Some(ta)) = substi.get(*i) {
@@ -349,8 +349,8 @@ impl TypeAnnotMeta {
self.escaped_lfts.is_empty() && self.escaped_tyvars.is_empty()
}
- pub fn empty() -> TypeAnnotMeta {
- TypeAnnotMeta {
+ pub fn empty() -> Self {
+ Self {
escaped_lfts: HashSet::new(),
escaped_tyvars: HashSet::new(),
}
@@ -363,7 +363,7 @@ impl TypeAnnotMeta {
}
}
- pub fn join(&mut self, s: &TypeAnnotMeta) {
+ pub fn join(&mut self, s: &Self) {
let lfts: HashSet<_> = self.escaped_lfts.union(&s.escaped_lfts).cloned().collect();
let tyvars: HashSet<_> = self.escaped_tyvars.union(&s.escaped_tyvars).cloned().collect();
@@ -767,7 +767,7 @@ impl TyOwnSpec {
with_later: bool,
annot_meta: TypeAnnotMeta,
) -> Self {
- TyOwnSpec {
+ Self {
loc,
with_later,
rfn,
@@ -2522,7 +2522,7 @@ impl Layout {
pub struct CoqBinder(CoqName, CoqType);
impl CoqBinder {
pub const fn new(n: CoqName, t: CoqType) -> Self {
- CoqBinder(n, t)
+ Self(n, t)
}
}
@@ -2610,8 +2610,8 @@ pub struct IPropPredicate {
}
impl IPropPredicate {
- pub fn new(binders: Vec<CoqBinder>, prop: IProp) -> IPropPredicate {
- IPropPredicate { binders, prop }
+ pub fn new(binders: Vec<CoqBinder>, prop: IProp) -> Self {
+ Self { binders, prop }
}
}
diff --git a/rr_frontend/translation/src/environment/borrowck/facts.rs b/rr_frontend/translation/src/environment/borrowck/facts.rs
index cc9f5462..9dbf4699 100644
--- a/rr_frontend/translation/src/environment/borrowck/facts.rs
+++ b/rr_frontend/translation/src/environment/borrowck/facts.rs
@@ -50,19 +50,19 @@ pub enum PointType {
}
impl std::cmp::PartialOrd for PointType {
- fn partial_cmp(&self, other: &PointType) -> Option<std::cmp::Ordering> {
+ fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
let res = match (self, other) {
- (PointType::Start, PointType::Start) => std::cmp::Ordering::Equal,
- (PointType::Start, PointType::Mid) => std::cmp::Ordering::Less,
- (PointType::Mid, PointType::Start) => std::cmp::Ordering::Greater,
- (PointType::Mid, PointType::Mid) => std::cmp::Ordering::Equal,
+ (Self::Start, Self::Start) => std::cmp::Ordering::Equal,
+ (Self::Start, Self::Mid) => std::cmp::Ordering::Less,
+ (Self::Mid, Self::Start) => std::cmp::Ordering::Greater,
+ (Self::Mid, Self::Mid) => std::cmp::Ordering::Equal,
};
Some(res)
}
}
impl std::cmp::Ord for PointType {
- fn cmp(&self, other: &PointType) -> std::cmp::Ordering {
+ fn cmp(&self, other: &Self) -> std::cmp::Ordering {
self.partial_cmp(other).unwrap()
}
}
diff --git a/rr_frontend/translation/src/environment/borrowck/regions.rs b/rr_frontend/translation/src/environment/borrowck/regions.rs
index 8f7b7253..eb494082 100644
--- a/rr_frontend/translation/src/environment/borrowck/regions.rs
+++ b/rr_frontend/translation/src/environment/borrowck/regions.rs
@@ -25,7 +25,7 @@ pub enum PlaceRegionsError {
// TODO: extend to more nested things (nested tuples/structs?)
impl PlaceRegions {
fn new() -> Self {
- PlaceRegions(HashMap::new())
+ Self(HashMap::new())
}
fn add_local(&mut self, local: mir::Local, rvid: facts::Region) {
diff --git a/rr_frontend/translation/src/environment/loops.rs b/rr_frontend/translation/src/environment/loops.rs
index c6b7f255..5e765668 100644
--- a/rr_frontend/translation/src/environment/loops.rs
+++ b/rr_frontend/translation/src/environment/loops.rs
@@ -59,8 +59,8 @@ impl PlaceAccessKind {
/// Does the access write to the path?
const fn is_write_access(&self) -> bool {
match &self {
- PlaceAccessKind::Store | PlaceAccessKind::Move => true,
- PlaceAccessKind::Read | PlaceAccessKind::MutableBorrow | PlaceAccessKind::SharedBorrow => false,
+ Self::Store | Self::Move => true,
+ Self::Read | Self::MutableBorrow | Self::SharedBorrow => false,
}
}
}
@@ -227,7 +227,7 @@ pub struct ProcedureLoops {
}
impl ProcedureLoops {
- pub fn new<'a, 'tcx: 'a>(mir: &'a mir::Body<'tcx>, real_edges: &RealEdges) -> ProcedureLoops {
+ pub fn new<'a, 'tcx: 'a>(mir: &'a mir::Body<'tcx>, real_edges: &RealEdges) -> Self {
let dominators = dominators(&mir.basic_blocks);
let mut back_edges: HashSet<(_, _)> = HashSet::new();
@@ -344,7 +344,7 @@ impl ProcedureLoops {
}
debug!("nonconditional_loop_blocks: {:?}", nonconditional_loop_blocks);
- ProcedureLoops {
+ Self {
loop_heads,
loop_head_depths,
loop_bodies,
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index 0164cce2..585382bb 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -1610,7 +1610,7 @@ impl AdditionalFacts {
}
/// Derive additional facts from the borrow checker facts.
- pub fn new(all_facts: &facts::AllInputFacts, output: &facts::AllOutputFacts) -> AdditionalFacts {
+ pub fn new(all_facts: &facts::AllInputFacts, output: &facts::AllOutputFacts) -> Self {
let (zombie_requires, zombie_borrow_live_at, borrow_become_zombie_at) =
Self::derive_zombie_requires(all_facts, output);
@@ -1630,7 +1630,7 @@ impl AdditionalFacts {
let mut loans: Vec<_> = all_facts.loan_issued_at.iter().map(|&(_, l, _)| l).collect();
loans.sort();
- AdditionalFacts {
+ Self {
loans,
reborrows,
reborrows_direct,
diff --git a/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs
index a90baf20..2e9d881f 100644
--- a/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs
@@ -30,7 +30,7 @@ pub struct VerboseConstAttrParser {}
impl VerboseConstAttrParser {
pub const fn new() -> Self {
- VerboseConstAttrParser {}
+ Self {}
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
index f1196cc7..9c26c5f8 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -30,7 +30,7 @@ pub struct VerboseCrateAttrParser {}
impl VerboseCrateAttrParser {
pub const fn new() -> Self {
- VerboseCrateAttrParser {}
+ Self {}
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
index 69c82dfb..88abe477 100644
--- a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
@@ -61,7 +61,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for EnumPattern {
})
.collect();
}
- Ok(EnumPattern { pat, args })
+ Ok(Self { pat, args })
}
}
@@ -69,7 +69,7 @@ pub struct VerboseEnumSpecParser {}
impl VerboseEnumSpecParser {
pub const fn new() -> Self {
- VerboseEnumSpecParser {}
+ Self {}
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/mod.rs b/rr_frontend/translation/src/spec_parsers/mod.rs
index 2da95261..8bbfe49d 100644
--- a/rr_frontend/translation/src/spec_parsers/mod.rs
+++ b/rr_frontend/translation/src/spec_parsers/mod.rs
@@ -20,7 +20,7 @@ impl<F> parse::Parse<F> for RustPath {
let x: parse::Punctuated<parse::Ident, parse::MToken![::]> =
parse::Punctuated::parse_separated_nonempty(input, meta)?;
let path = x.into_iter().map(|x| x.value()).collect();
- Ok(RustPath { path })
+ Ok(Self { path })
}
}
@@ -65,7 +65,7 @@ where
let args: Vec<_> = args.into_iter().collect();
let x = args[0].value();
let y = args[1].value();
- Ok(ShimAnnot {
+ Ok(Self {
code_name: x,
spec_name: y,
})
diff --git a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
index 1fe713d4..dd3b4b20 100644
--- a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
@@ -33,7 +33,7 @@ pub struct VerboseModuleAttrParser {}
impl VerboseModuleAttrParser {
pub const fn new() -> Self {
- VerboseModuleAttrParser {}
+ Self {}
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 80d0bd91..7e64968d 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -28,9 +28,9 @@ where
fn parse(input: parse::ParseStream, meta: &U) -> parse::ParseResult<Self> {
if let Ok(ident) = parse::Ident::parse(input, meta) {
// it's an identifer
- Ok(IdentOrTerm::Ident(ident.value()))
+ Ok(Self::Ident(ident.value()))
} else {
- parse::LitStr::parse(input, meta).map(|s| IdentOrTerm::Term(s.value()))
+ parse::LitStr::parse(input, meta).map(|s| Self::Term(s.value()))
}
}
}
@@ -38,8 +38,8 @@ where
impl ToString for IdentOrTerm {
fn to_string(&self) -> String {
match self {
- IdentOrTerm::Ident(s) => s.to_string(),
- IdentOrTerm::Term(s) => s.to_string(),
+ Self::Ident(s) => s.to_string(),
+ Self::Term(s) => s.to_string(),
}
}
}
@@ -79,14 +79,14 @@ impl<'a> parse::Parse<ParseMeta<'a>> for LiteralTypeWithRef {
let ty: parse::LitStr = input.parse(meta)?;
let (ty, meta) = process_coq_literal(&ty.value(), *meta);
- Ok(LiteralTypeWithRef {
+ Ok(Self {
rfn,
ty: Some(ty),
raw,
meta,
})
} else {
- Ok(LiteralTypeWithRef {
+ Ok(Self {
rfn,
ty: None,
raw,
@@ -108,7 +108,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for LiteralType {
let ty: parse::LitStr = input.parse(meta)?;
let (ty, meta) = process_coq_literal(&ty.value(), *meta);
- Ok(LiteralType { ty, meta })
+ Ok(Self { ty, meta })
}
}
@@ -126,7 +126,7 @@ impl<'a> Parse<ParseMeta<'a>> for IProp {
let lit: parse::LitStr = input.parse(meta)?;
let (lit, _) = process_coq_literal(&lit.value(), *meta);
- Ok(IProp(specs::IProp::Atom(lit)))
+ Ok(Self(specs::IProp::Atom(lit)))
}
}
@@ -151,9 +151,9 @@ impl<'a> parse::Parse<ParseMeta<'a>> for RRParam {
let ty: parse::LitStr = input.parse(meta)?;
let (ty, _) = process_coq_literal(&ty.value(), *meta);
let ty = specs::CoqType::Literal(ty);
- Ok(RRParam { name, ty })
+ Ok(Self { name, ty })
} else {
- Ok(RRParam {
+ Ok(Self {
name,
ty: specs::CoqType::Infer,
})
@@ -171,7 +171,7 @@ impl<'a> Parse<ParseMeta<'a>> for RRParams {
fn parse(input: ParseStream, meta: &ParseMeta) -> ParseResult<Self> {
let params: parse::Punctuated<RRParam, MToken![,]> =
parse::Punctuated::<_, _>::parse_terminated(input, meta)?;
- Ok(RRParams {
+ Ok(Self {
params: params.into_iter().collect(),
})
}
@@ -196,12 +196,12 @@ impl<U> Parse<U> for CoqPath {
let module: parse::LitStr = input.parse(meta)?;
let module = module.value();
- Ok(CoqPath(specs::CoqPath {
+ Ok(Self(specs::CoqPath {
path: Some(path_or_module),
module,
}))
} else {
- Ok(CoqPath(specs::CoqPath {
+ Ok(Self(specs::CoqPath {
path: None,
module: path_or_module,
}))
@@ -229,7 +229,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for RRCoqContextItem {
}
//annot_meta.
- Ok(RRCoqContextItem {
+ Ok(Self {
item: item_str,
at_end,
})
@@ -245,7 +245,7 @@ impl<U> parse::Parse<U> for RRGlobalCoqContextItem {
fn parse(input: parse::ParseStream, meta: &U) -> parse::ParseResult<Self> {
let item: parse::LitStr = input.parse(meta)?;
- Ok(RRGlobalCoqContextItem { item: item.value() })
+ Ok(Self { item: item.value() })
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
index 44b1371f..c391b3cf 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -52,12 +52,12 @@ impl<'a> parse::Parse<ParseMeta<'a>> for RfnPattern {
input.parse::<_, parse::MToken![:]>(meta)?;
let ty: parse::LitStr = input.parse(meta)?;
let (ty, _) = process_coq_literal(ty.value().as_str(), *meta);
- Ok(RfnPattern {
+ Ok(Self {
rfn_pat: pat,
rfn_type: Some(specs::CoqType::Literal(ty)),
})
} else {
- Ok(RfnPattern {
+ Ok(Self {
rfn_pat: pat,
rfn_type: None,
})
@@ -87,15 +87,15 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
match macro_cmd.value().as_str() {
"iris" => {
let prop: IProp = input.parse(meta)?;
- Ok(MetaIProp::Iris(prop.into()))
+ Ok(Self::Iris(prop.into()))
},
"own" => {
let prop: IProp = input.parse(meta)?;
- Ok(MetaIProp::Own(prop.into()))
+ Ok(Self::Own(prop.into()))
},
"shr" => {
let prop: IProp = input.parse(meta)?;
- Ok(MetaIProp::Shared(prop.into()))
+ Ok(Self::Shared(prop.into()))
},
"type" => {
let loc_str: parse::LitStr = input.parse(meta)?;
@@ -116,7 +116,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
annot_meta.join(&annot_meta3);
let spec = specs::TyOwnSpec::new(loc_str, rfn_str, type_str, true, annot_meta);
- Ok(MetaIProp::Type(spec))
+ Ok(Self::Type(spec))
},
_ => {
panic!("invalid macro command: {:?}", macro_cmd.value());
@@ -134,11 +134,11 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
let (pure_str, _annot_meta) = process_coq_literal(&pure_prop.value(), *meta);
// TODO: should we use annot_meta?
- Ok(MetaIProp::Pure(pure_str, Some(name_str)))
+ Ok(Self::Pure(pure_str, Some(name_str)))
} else {
// this is a
let (lit, _) = process_coq_literal(&name_or_prop_str.value(), *meta);
- Ok(MetaIProp::Pure(lit, None))
+ Ok(Self::Pure(lit, None))
}
}
}
@@ -156,10 +156,10 @@ impl<U> parse::Parse<U> for InvariantSpecFlags {
fn parse(input: parse::ParseStream, meta: &U) -> parse::ParseResult<Self> {
let mode: parse::Ident = input.parse(meta)?;
match mode.value().as_str() {
- "persistent" => Ok(InvariantSpecFlags(specs::InvariantSpecFlags::Persistent)),
- "plain" => Ok(InvariantSpecFlags(specs::InvariantSpecFlags::Plain)),
- "na" => Ok(InvariantSpecFlags(specs::InvariantSpecFlags::NonAtomic)),
- "atomic" => Ok(InvariantSpecFlags(specs::InvariantSpecFlags::Atomic)),
+ "persistent" => Ok(Self(specs::InvariantSpecFlags::Persistent)),
+ "plain" => Ok(Self(specs::InvariantSpecFlags::Plain)),
+ "na" => Ok(Self(specs::InvariantSpecFlags::NonAtomic)),
+ "atomic" => Ok(Self(specs::InvariantSpecFlags::Atomic)),
_ => {
panic!("invalid ADT mode: {:?}", mode.value())
},
@@ -171,7 +171,7 @@ pub struct VerboseInvariantSpecParser {}
impl VerboseInvariantSpecParser {
pub const fn new() -> Self {
- VerboseInvariantSpecParser {}
+ Self {}
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
index d9f6c91b..4531cc6d 100644
--- a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
@@ -62,7 +62,7 @@ impl<'a> Parse<ParseMeta<'a>> for RRArgs {
fn parse(input: ParseStream, meta: &ParseMeta) -> ParseResult<Self> {
let args: parse::Punctuated<LiteralTypeWithRef, MToken![,]> =
parse::Punctuated::<_, _>::parse_terminated(input, meta)?;
- Ok(RRArgs {
+ Ok(Self {
args: args.into_iter().collect(),
})
}
@@ -96,14 +96,14 @@ impl<'a> parse::Parse<ParseMeta<'a>> for ClosureCaptureSpec {
format!("Did not expect type specification for capture postcondition"),
))
} else {
- Ok(ClosureCaptureSpec {
+ Ok(Self {
variable: name,
pre: pre_spec,
post: Some(post_spec),
})
}
} else {
- Ok(ClosureCaptureSpec {
+ Ok(Self {
variable: name,
pre: pre_spec,
post: None,
@@ -150,11 +150,11 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
annot_meta.join(&annot_meta3);
let spec = specs::TyOwnSpec::new(loc_str, rfn_str, type_str, false, annot_meta);
- Ok(MetaIProp::Type(spec))
+ Ok(Self::Type(spec))
},
"iris" => {
let prop: IProp = input.parse(meta)?;
- Ok(MetaIProp::Iris(prop.into()))
+ Ok(Self::Iris(prop.into()))
},
"observe" => {
let gname: parse::LitStr = input.parse(meta)?;
@@ -163,12 +163,12 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
let term: parse::LitStr = input.parse(meta)?;
let (term, _meta) = process_coq_literal(&term.value(), *meta);
- Ok(MetaIProp::Observe(gname.value(), term))
+ Ok(Self::Observe(gname.value(), term))
},
"linktime" => {
let term: parse::LitStr = input.parse(meta)?;
let (term, _meta) = process_coq_literal(&term.value(), *meta);
- Ok(MetaIProp::Linktime(term))
+ Ok(Self::Linktime(term))
},
_ => {
panic!("invalid macro command: {:?}", macro_cmd.value());
@@ -186,11 +186,11 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
let (pure_str, _annot_meta) = process_coq_literal(&pure_prop.value(), *meta);
// TODO: should we use annot_meta?
- Ok(MetaIProp::Pure(pure_str, Some(name_str)))
+ Ok(Self::Pure(pure_str, Some(name_str)))
} else {
// this is a
let (lit, _) = process_coq_literal(&name_or_prop_str.value(), *meta);
- Ok(MetaIProp::Pure(lit, None))
+ Ok(Self::Pure(lit, None))
}
}
}
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index 82419454..e9d18c37 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -96,7 +96,7 @@ impl FlatType {
/// Try to convert a flat type to a type.
pub fn to_type<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<ty::Ty<'tcx>> {
match self {
- FlatType::Adt(path_with_args) => {
+ Self::Adt(path_with_args) => {
let (did, flat_args) = path_with_args.to_item(tcx)?;
let ty: ty::EarlyBinder<ty::Ty<'tcx>> = tcx.type_of(did);
--
GitLab