From 2d563d7c2e899fe2663e733fdfbb08ee417057da Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Sat, 27 Apr 2024 02:09:07 +0200
Subject: [PATCH] clippy: Fix single_char_add_str
---
rr_frontend/.cargo/config.toml | 1 -
rr_frontend/radium/src/code.rs | 14 ++++++-------
rr_frontend/radium/src/specs.rs | 20 +++++++++----------
.../verbose_function_spec_parser.rs | 4 ++--
.../translation/src/type_translator.rs | 2 +-
5 files changed, 20 insertions(+), 21 deletions(-)
diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index 3d7742e6..4e39d7fd 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -81,7 +81,6 @@ rustflags = [
# clippy::style
"-Aclippy::new_without_default",
- "-Aclippy::single_char_add_str",
"-Aclippy::single_component_path_imports",
"-Aclippy::single_match",
"-Aclippy::toplevel_ref_arg",
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 2ce6d6e7..8a57d80d 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -613,9 +613,9 @@ impl Stmt {
let mut fmt_targets = String::with_capacity(100);
- fmt_targets.push_str("[");
+ fmt_targets.push('[');
push_str_list!(fmt_targets, bs, "; ", |tgt| tgt.caesium_fmt(0));
- fmt_targets.push_str("]");
+ fmt_targets.push(']');
let fmt_default = def.caesium_fmt(0);
@@ -740,7 +740,7 @@ fn make_map_string(sep0: &str, sep: &str, els: Vec<(String, String)>) -> String
out.push_str(format!("<[{sep}\"{}\" :={}{}{}]>%E $", key, sep0, value, sep).as_str());
}
out.push_str(sep);
- out.push_str("∅");
+ out.push('∅');
out
}
@@ -749,7 +749,7 @@ fn make_lft_map_string(els: Vec<(String, String)>) -> String {
for (key, value) in &els {
out.push_str(format!("named_lft_update \"{}\" {} $ ", key, value).as_str());
}
- out.push_str("∅");
+ out.push('∅');
out
}
@@ -761,7 +761,7 @@ impl FunctionCode {
let format_stack_layout = |layout: std::slice::Iter<'_, (String, SynType)>| {
let mut formatted_args: String = String::with_capacity(100);
- formatted_args.push_str("[");
+ formatted_args.push('[');
push_str_list!(formatted_args, layout, "; ", |(ref name, ref st)| {
let ly = st.layout_term(&[]); //should be closed already
@@ -1124,7 +1124,7 @@ impl<'def> Function<'def> {
if p_count > 1 {
ip_params.push_str(" ]");
}
- ip_params.push_str(" ");
+ ip_params.push(' ');
p_count += 1;
ip_params.push_str(format!("{}", n).as_str());
}
@@ -1138,7 +1138,7 @@ impl<'def> Function<'def> {
} else {
// no params, but still need to provide something to catch the unit
// (and no empty intropatterns are allowed)
- ip_params.push_str("?");
+ ip_params.push('?');
}
// generate intro pattern for lifetimes
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 01861315..68c4029b 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -1299,7 +1299,7 @@ impl<'def> AbstractVariant<'def> {
typarams.push(format!("({} : syn_type)", names.syn_type));
typarams_use.push(format!("{}", names.syn_type));
}
- out.push_str("\n");
+ out.push('\n');
write!(out, "{}", self.generate_coq_sls_def_core(&typarams, &typarams_use)).unwrap();
@@ -1313,7 +1313,7 @@ impl<'def> AbstractVariant<'def> {
out.push_str(&format!("struct_t {} +[", CoqAppTerm::new(&self.sls_def_name, sls_app)));
push_str_list!(out, &self.subst_fields, ";", |(_, ty)| ty.to_string());
- out.push_str("]");
+ out.push(']');
out
}
@@ -1389,7 +1389,7 @@ impl<'def> AbstractVariant<'def> {
}
out.push_str(".\n");
}
- out.push_str("\n");
+ out.push('\n');
// write coq parameters
let (context_names, dep_sigma) = format_extra_context_items(extra_context, &mut out).unwrap();
@@ -1895,7 +1895,7 @@ impl<'def> AbstractEnum<'def> {
out.push_str(&format!("Section {}.\n", self.els_def_name));
out.push_str(&format!("{indent}Context `{{!refinedrustGS Σ}}.\n"));
- out.push_str("\n");
+ out.push('\n');
// add syntype parameters
let mut typarams = Vec::new();
@@ -2093,7 +2093,7 @@ impl<'def> AbstractEnum<'def> {
}
out.push_str(".\n");
}
- out.push_str("\n");
+ out.push('\n');
let rt_params: Vec<_> = self.ty_params.iter().map(|x| x.refinement_type.clone()).collect();
@@ -2661,7 +2661,7 @@ impl<'def> FunctionSpec<'def> {
out.push_str("λ Ï, [");
push_str_list!(out, &self.elctx, ", ", |(ref lft1, ref lft2)| format!("({lft1}, {lft2})"));
- out.push_str("]");
+ out.push(']');
out
}
@@ -2699,8 +2699,8 @@ impl<'def> FunctionSpec<'def> {
let mut pattern = String::with_capacity(100);
let mut types = String::with_capacity(100);
- pattern.push_str("(");
- types.push_str("(");
+ pattern.push('(');
+ types.push('(');
let mut need_sep = false;
for (name, t) in v {
@@ -2715,8 +2715,8 @@ impl<'def> FunctionSpec<'def> {
need_sep = true;
}
- pattern.push_str(")");
- types.push_str(")");
+ pattern.push(')');
+ types.push(')');
(pattern, CoqType::Literal(types))
}
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 7fd53165..52cc4879 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
@@ -504,7 +504,7 @@ where
} else {
pre_rfn.push_str("-[");
push_str_list!(pre_rfn, pre_types.clone(), "; ", |x| format!("#({})", x.1));
- pre_rfn.push_str("]");
+ pre_rfn.push(']');
pre_tys = pre_types.iter().map(|x| x.0.clone()).collect();
}
@@ -561,7 +561,7 @@ where
CapturePostRfn::ImmutOrConsume(pat) => format!("#({pat})"),
CapturePostRfn::Mut(pat, gvar) => format!("#(#({pat}), {gvar})"),
});
- post_term.push_str("]");
+ post_term.push(']');
builder
.spec
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 69168bb3..4eea6b38 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -876,7 +876,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
rfn.push_str("-[");
push_str_list!(rfn, &field_refinements, "; ", "#({})");
- rfn.push_str("]");
+ rfn.push(']');
invariant_spec.provide_abstracted_refinement(rfn);
}
--
GitLab