diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index 2f36fac5a0b58282ea89b9345666f2276a9cebc7..f12e4d7eb88b7f3bb5b1a91a9d3e458cb7cb5adc 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -25,12 +25,12 @@ pub struct Path(String);
impl Path {
#[must_use]
- pub const fn new(path: String) -> Self {
- Self(path)
+ pub fn new(path: &str) -> Self {
+ Self(path.to_string())
}
#[must_use]
- pub fn new_from_segments(segments: &[String]) -> Self {
+ pub fn new_from_segments(segments: &[&str]) -> Self {
Self(segments.join("."))
}
}
@@ -44,14 +44,17 @@ pub struct Module {
impl Module {
#[must_use]
- pub const fn new(name: String) -> Self {
- Self { name, path: None }
+ pub fn new(name: &str) -> Self {
+ Self {
+ name: name.to_string(),
+ path: None,
+ }
}
#[must_use]
- pub const fn new_with_path(name: String, path: Path) -> Self {
+ pub fn new_with_path(name: &str, path: Path) -> Self {
Self {
- name,
+ name: name.to_string(),
path: Some(path),
}
}
@@ -612,8 +615,8 @@ mod tests {
#[test]
fn modules_paths_none() {
- let module_a = Module::new("A".to_string());
- let module_b = Module::new("B".to_string());
+ let module_a = Module::new("A");
+ let module_b = Module::new("B");
let modules = vec![&module_a, &module_b];
assert_eq!(get_modules_path(&modules), vec![]);
@@ -621,37 +624,31 @@ mod tests {
#[test]
fn modules_paths_some_uniqueness() {
- let module_a = Module::new_with_path("A".to_string(), Path::new("a.b.c".to_string()));
- let module_b = Module::new_with_path("B".to_string(), Path::new("a.b.d".to_string()));
+ let module_a = Module::new_with_path("A", Path::new("a.b.c"));
+ let module_b = Module::new_with_path("B", Path::new("a.b.d"));
let modules = vec![&module_a, &module_b];
- assert_eq!(get_modules_path(&modules), vec![
- Path::new("a.b.c".to_string()),
- Path::new("a.b.d".to_string())
- ]);
+ assert_eq!(get_modules_path(&modules), vec![Path::new("a.b.c"), Path::new("a.b.d")]);
}
#[test]
fn modules_paths_some_duplicate() {
- let module_a = Module::new_with_path("A".to_string(), Path::new("a.b.c".to_string()));
- let module_b = Module::new_with_path("B".to_string(), Path::new("a.b.c".to_string()));
+ let module_a = Module::new_with_path("A", Path::new("a.b.c"));
+ let module_b = Module::new_with_path("B", Path::new("a.b.c"));
let modules = vec![&module_a, &module_b];
- assert_eq!(get_modules_path(&modules), vec![Path::new("a.b.c".to_string())]);
+ assert_eq!(get_modules_path(&modules), vec![Path::new("a.b.c")]);
}
#[test]
fn modules_paths_all() {
- let module_a = Module::new("A".to_string());
- let module_b = Module::new_with_path("B".to_string(), Path::new("a.b.c".to_string()));
- let module_c = Module::new_with_path("C".to_string(), Path::new("a.b.d".to_string()));
- let module_d = Module::new_with_path("D".to_string(), Path::new("a.b.d".to_string()));
+ let module_a = Module::new("A");
+ let module_b = Module::new_with_path("B", Path::new("a.b.c"));
+ let module_c = Module::new_with_path("C", Path::new("a.b.d"));
+ let module_d = Module::new_with_path("D", Path::new("a.b.d"));
let modules = vec![&module_a, &module_b, &module_c, &module_d];
- assert_eq!(get_modules_path(&modules), vec![
- Path::new("a.b.c".to_string()),
- Path::new("a.b.d".to_string())
- ]);
+ assert_eq!(get_modules_path(&modules), vec![Path::new("a.b.c"), Path::new("a.b.d")]);
}
#[test]
@@ -663,8 +660,8 @@ mod tests {
#[test]
fn display_none() {
- let module_a = Import::new(Module::new("A".to_string()));
- let module_b = Import::new(Module::new("B".to_string()));
+ let module_a = Import::new(Module::new("A"));
+ let module_b = Import::new(Module::new("B"));
let modules = vec![module_a, module_b];
assert_eq!(ImportList(&modules).to_string(), indoc! {"
@@ -674,8 +671,8 @@ mod tests {
#[test]
fn display_some_uniqueness() {
- let module_a = Import::new(Module::new_with_path("A".to_string(), Path::new("a.b.c".to_string())));
- let module_b = Import::new(Module::new_with_path("B".to_string(), Path::new("a.b.d".to_string())));
+ let module_a = Import::new(Module::new_with_path("A", Path::new("a.b.c")));
+ let module_b = Import::new(Module::new_with_path("B", Path::new("a.b.d")));
let modules = vec![module_a, module_b];
assert_eq!(ImportList(&modules).to_string(), indoc! {"
@@ -686,8 +683,8 @@ mod tests {
#[test]
fn display_some_duplicate() {
- let module_a = Import::new(Module::new_with_path("A".to_string(), Path::new("a.b.c".to_string())));
- let module_b = Import::new(Module::new_with_path("B".to_string(), Path::new("a.b.c".to_string())));
+ let module_a = Import::new(Module::new_with_path("A", Path::new("a.b.c")));
+ let module_b = Import::new(Module::new_with_path("B", Path::new("a.b.c")));
let modules = vec![module_a, module_b];
assert_eq!(ImportList(&modules).to_string(), indoc! {"
@@ -697,10 +694,10 @@ mod tests {
#[test]
fn display_all() {
- let module_a = Import::new(Module::new("A".to_string()));
- let module_b = Import::new(Module::new_with_path("B".to_string(), Path::new("a.b.c".to_string())));
- let module_c = Import::new(Module::new_with_path("C".to_string(), Path::new("a.b.d".to_string())));
- let module_d = Import::new(Module::new_with_path("D".to_string(), Path::new("a.b.d".to_string())));
+ let module_a = Import::new(Module::new("A"));
+ let module_b = Import::new(Module::new_with_path("B", Path::new("a.b.c")));
+ let module_c = Import::new(Module::new_with_path("C", Path::new("a.b.d")));
+ let module_d = Import::new(Module::new_with_path("D", Path::new("a.b.d")));
let modules = vec![module_a, module_b, module_c, module_d];
assert_eq!(ImportList(&modules).to_string(), indoc! {"
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index b609a28737141e6f428f386583b059c92b850777..b10a5478c0022a053bdbbf6d63e73435f6e0d7ca 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -343,22 +343,10 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
/// Write specifications of a verification unit.
fn write_specifications(&self, spec_path: &Path, code_path: &Path, stem: &str) {
let common_imports = vec![
- coq::Import::new(coq::Module::new_with_path(
- "lang".to_string(),
- coq::Path::new("caesium".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "notation".to_string(),
- coq::Path::new("caesium".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "typing".to_string(),
- coq::Path::new("refinedrust".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "shims".to_string(),
- coq::Path::new("refinedrust".to_string()),
- )),
+ coq::Import::new(coq::Module::new_with_path("lang", coq::Path::new("caesium"))),
+ coq::Import::new(coq::Module::new_with_path("notation", coq::Path::new("caesium"))),
+ coq::Import::new(coq::Module::new_with_path("typing", coq::Path::new("refinedrust"))),
+ coq::Import::new(coq::Module::new_with_path("shims", coq::Path::new("refinedrust"))),
];
let mut spec_file = io::BufWriter::new(fs::File::create(spec_path).unwrap());
@@ -366,8 +354,8 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
{
let mut spec_exports = vec![coq::Export::new(coq::Module::new_with_path(
- format!("generated_code_{stem}"),
- coq::Path::new_from_segments(&[self.coq_path_prefix.clone(), stem.to_string()]),
+ &format!("generated_code_{stem}"),
+ coq::Path::new_from_segments(&[&self.coq_path_prefix, &stem]),
))];
spec_exports.append(&mut self.extra_exports.iter().map(|(export, _)| export.clone()).collect());
@@ -509,22 +497,10 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
F: Fn(&str) -> std::path::PathBuf,
{
let common_imports = vec![
- coq::Import::new(coq::Module::new_with_path(
- "lang".to_string(),
- coq::Path::new("caesium".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "notation".to_string(),
- coq::Path::new("caesium".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "typing".to_string(),
- coq::Path::new("refinedrust".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "shims".to_string(),
- coq::Path::new("refinedrust".to_string()),
- )),
+ coq::Import::new(coq::Module::new_with_path("lang", coq::Path::new("caesium"))),
+ coq::Import::new(coq::Module::new_with_path("notation", coq::Path::new("caesium"))),
+ coq::Import::new(coq::Module::new_with_path("typing", coq::Path::new("refinedrust"))),
+ coq::Import::new(coq::Module::new_with_path("shims", coq::Path::new("refinedrust"))),
];
// write templates
@@ -540,12 +516,12 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
imports.append(&mut vec![
coq::Import::new(coq::Module::new_with_path(
- format!("generated_code_{stem}"),
- coq::Path::new_from_segments(&[self.coq_path_prefix.clone(), stem.to_string()]),
+ &format!("generated_code_{stem}"),
+ coq::Path::new_from_segments(&[&self.coq_path_prefix.clone(), &stem]),
)),
coq::Import::new(coq::Module::new_with_path(
- format!("generated_specs_{stem}"),
- coq::Path::new_from_segments(&[self.coq_path_prefix.clone(), stem.to_string()]),
+ &format!("generated_specs_{stem}"),
+ coq::Path::new_from_segments(&[&self.coq_path_prefix.clone(), &stem]),
)),
]);
@@ -591,22 +567,10 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
F: Fn(&str) -> std::path::PathBuf,
{
let common_imports = vec![
- coq::Import::new(coq::Module::new_with_path(
- "lang".to_string(),
- coq::Path::new("caesium".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "notation".to_string(),
- coq::Path::new("caesium".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "typing".to_string(),
- coq::Path::new("refinedrust".to_string()),
- )),
- coq::Import::new(coq::Module::new_with_path(
- "shims".to_string(),
- coq::Path::new("refinedrust".to_string()),
- )),
+ coq::Import::new(coq::Module::new_with_path("lang", coq::Path::new("caesium"))),
+ coq::Import::new(coq::Module::new_with_path("notation", coq::Path::new("caesium"))),
+ coq::Import::new(coq::Module::new_with_path("typing", coq::Path::new("refinedrust"))),
+ coq::Import::new(coq::Module::new_with_path("shims", coq::Path::new("refinedrust"))),
];
// write proofs
@@ -631,28 +595,16 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
imports.append(&mut vec![
coq::Import::new(coq::Module::new_with_path(
- format!("generated_code_{stem}"),
- coq::Path::new_from_segments(&[
- self.coq_path_prefix.clone(),
- stem.to_string(),
- "generated".to_string(),
- ]),
+ &format!("generated_code_{stem}"),
+ coq::Path::new_from_segments(&[&self.coq_path_prefix, &stem, "generated"]),
)),
coq::Import::new(coq::Module::new_with_path(
- format!("generated_specs_{stem}"),
- coq::Path::new_from_segments(&[
- self.coq_path_prefix.clone(),
- stem.to_string(),
- "generated".to_string(),
- ]),
+ &format!("generated_specs_{stem}"),
+ coq::Path::new_from_segments(&[&self.coq_path_prefix, &stem, "generated"]),
)),
coq::Import::new(coq::Module::new_with_path(
- format!("generated_template_{}", fun.name()),
- coq::Path::new_from_segments(&[
- self.coq_path_prefix.clone(),
- stem.to_string(),
- "generated".to_string(),
- ]),
+ &format!("generated_template_{}", fun.name()),
+ coq::Path::new_from_segments(&[&self.coq_path_prefix, &stem, "generated"]),
)),
]);
diff --git a/rr_frontend/translation/src/shim_registry.rs b/rr_frontend/translation/src/shim_registry.rs
index fefe346df5705eb355eabee9c184b1bbd0a286aa..02696b10fe30965022d9bf9bb1250c8a3c7440dd 100644
--- a/rr_frontend/translation/src/shim_registry.rs
+++ b/rr_frontend/translation/src/shim_registry.rs
@@ -221,15 +221,13 @@ impl<'a> ShimRegistry<'a> {
.get("refinedrust_path")
.ok_or(format!("Missing attribute \"refinedrust_path\""))?
.as_str()
- .ok_or(format!("Expected string for \"refinedrust_path\" attribute"))?
- .to_string();
+ .ok_or(format!("Expected string for \"refinedrust_path\" attribute"))?;
let module = obj
.get("refinedrust_module")
.ok_or(format!("Missing attribute \"refinedrust_module\""))?
.as_str()
- .ok_or(format!("Expected string for \"refinedrust_module\" attribute"))?
- .to_string();
+ .ok_or(format!("Expected string for \"refinedrust_module\" attribute"))?;
let _ = obj
.get("refinedrust_name")
@@ -249,8 +247,7 @@ impl<'a> ShimRegistry<'a> {
for dependency in dependencies {
let path = dependency
.as_str()
- .ok_or(format!("Expected string for element of \"module_dependencies\" array"))?
- .to_string();
+ .ok_or(format!("Expected string for element of \"module_dependencies\" array"))?;
self.dependencies.push(coq::Path::new(path));
}
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 20080b77f5d56a93c7aa411a820caca84ea3d2f2..98010ae4efb7c042081e26164048d4f0e668bc6c 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -195,9 +195,9 @@ impl<U> Parse<U> for CoqModule {
let module: parse::LitStr = input.parse(meta)?;
let module = module.value();
- Ok(Self(coq::Module::new_with_path(module, coq::Path::new(path_or_module))))
+ Ok(Self(coq::Module::new_with_path(&module, coq::Path::new(&path_or_module))))
} else {
- Ok(Self(coq::Module::new(path_or_module)))
+ Ok(Self(coq::Module::new(&path_or_module)))
}
}
}