diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index 583fde840b58678942d4df11c32cb3d861dfe902..a6df65ff5008a5e7469a376fd4c7895c69dd735b 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -16,18 +16,35 @@ use indent_write::indentable::Indentable;
use crate::{display_list, make_indent, write_list, BASE_INDENT};
-/// A Rocq path of the form `From A.B.C Require Import D`.
+/// A Rocq import of the form `From A.B.C Require Import D`.
+///
+/// If the `path` is empty, it is of the form `Require Import A`.
#[derive(Clone, Eq, PartialEq, Hash, Debug)]
-pub struct Path {
+pub struct Import {
pub path: Option<String>,
- pub module: String,
+ module: String,
}
-impl fmt::Display for Path {
+impl fmt::Display for Import {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self.path {
- None => write!(f, "Require Export {}.\n", self.module),
- Some(ref path) => write!(f, "From {} Require Export {}.\n", path, self.module),
+ None => write!(f, "Require Import {}.\n", self.module),
+ Some(ref path) => write!(f, "From {} Require Import {}.\n", path, self.module),
+ }
+ }
+}
+
+impl Import {
+ #[must_use]
+ pub const fn new(module: String) -> Self {
+ Self { module, path: None }
+ }
+
+ #[must_use]
+ pub const fn new_with_path(module: String, path: String) -> Self {
+ Self {
+ module,
+ path: Some(path),
}
}
}
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 6b3017daa6749865afee20dafcd7b4c4d6c45f9a..0e23c8d84859e63dd48adfcfe4748364ffcdb74e 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -104,7 +104,7 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
type_translator: &'rcx TypeTranslator<'rcx, 'tcx>,
functions: &'rcx [LocalDefId],
/// the second component determines whether to include it in the code file as well
- extra_imports: HashSet<(coq::Path, bool)>,
+ extra_imports: HashSet<(coq::Import, bool)>,
/// extra Coq module dependencies
extra_dependencies: HashSet<String>,
coq_path_prefix: String,
@@ -1256,7 +1256,7 @@ where
let module_attrs = get_module_attributes(env)?;
// process imports
- let mut imports: HashSet<coq::Path> = HashSet::new();
+ let mut imports: HashSet<coq::Import> = HashSet::new();
crate_spec.imports.into_iter().map(|path| imports.insert(path)).count();
module_attrs
.values()
diff --git a/rr_frontend/translation/src/shim_registry.rs b/rr_frontend/translation/src/shim_registry.rs
index 39530d122aee574d6b2e68ead09d955fb2f20b25..34f4f3d9f5dd5973340a8fa21753b256569609d4 100644
--- a/rr_frontend/translation/src/shim_registry.rs
+++ b/rr_frontend/translation/src/shim_registry.rs
@@ -152,7 +152,7 @@ pub struct ShimRegistry<'a> {
/// adt shims
adt_shims: Vec<AdtShim<'a>>,
/// extra imports
- imports: Vec<coq::Path>,
+ imports: Vec<coq::Import>,
/// extra module dependencies
depends: Vec<String>,
}
@@ -228,10 +228,7 @@ impl<'a> ShimRegistry<'a> {
let _name =
name.as_str().ok_or(format!("Expected string for \"refinedrust_name\" attribute"))?;
- let coq_path = coq::Path {
- path: Some(path.to_string()),
- module: module.to_string(),
- };
+ let coq_path = coq::Import::new_with_path(module.to_string(), path.to_string());
self.imports.push(coq_path);
let depends = obj
@@ -316,7 +313,7 @@ impl<'a> ShimRegistry<'a> {
&self.adt_shims
}
- pub fn get_extra_imports(&self) -> &[coq::Path] {
+ pub fn get_extra_imports(&self) -> &[coq::Import] {
&self.imports
}
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 56f078f0913fbc841babf656c96dbb84a83f6980..cada47ca0589c026f8d99712528648c3fcff1c07 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -19,7 +19,7 @@ pub trait CrateAttrParser {
#[derive(Clone, Debug)]
pub struct CrateAttrs {
- pub imports: Vec<coq::Path>,
+ pub imports: Vec<coq::Import>,
pub prefix: Option<String>,
pub includes: Vec<String>,
pub package: Option<String>,
@@ -37,7 +37,7 @@ impl VerboseCrateAttrParser {
impl CrateAttrParser for VerboseCrateAttrParser {
fn parse_crate_attrs<'a>(&'a mut self, attrs: &'a [&'a AttrItem]) -> Result<CrateAttrs, String> {
let meta = ();
- let mut imports: Vec<coq::Path> = Vec::new();
+ let mut imports: Vec<coq::Import> = Vec::new();
let mut includes: Vec<String> = Vec::new();
let mut prefix: Option<String> = None;
let mut package: Option<String> = None;
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 bb7eafa003de265f194a74c01664f0cf9d4edd5f..d28a3744e193c580fdfa3891cc3f147b83ef45e8 100644
--- a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
@@ -24,7 +24,7 @@ pub trait ModuleAttrParser {
#[derive(Clone, Debug)]
pub struct ModuleAttrs {
- pub imports: Vec<coq::Path>,
+ pub imports: Vec<coq::Import>,
pub includes: Vec<String>,
pub context_params: Vec<coq::Param>,
}
@@ -44,7 +44,7 @@ impl ModuleAttrParser for VerboseModuleAttrParser {
attrs: &'a [&'a AttrItem],
) -> Result<ModuleAttrs, String> {
let meta = ();
- let mut imports: Vec<coq::Path> = Vec::new();
+ let mut imports: Vec<coq::Import> = Vec::new();
let mut includes: Vec<String> = Vec::new();
let mut context_params = Vec::new();
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 831af6267d0b453bb95fa5001fbe9f75dd316c6b..cba50ff9b7fc113cb57bbea88b8f75e9371e68f2 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -176,9 +176,9 @@ impl<'a> Parse<ParseMeta<'a>> for RRParams {
}
}
-pub struct CoqPath(coq::Path);
+pub struct CoqPath(coq::Import);
-impl From<CoqPath> for coq::Path {
+impl From<CoqPath> for coq::Import {
fn from(path: CoqPath) -> Self {
path.0
}
@@ -195,15 +195,9 @@ impl<U> Parse<U> for CoqPath {
let module: parse::LitStr = input.parse(meta)?;
let module = module.value();
- Ok(Self(coq::Path {
- path: Some(path_or_module),
- module,
- }))
+ Ok(Self(coq::Import::new_with_path(module, path_or_module)))
} else {
- Ok(Self(coq::Path {
- path: None,
- module: path_or_module,
- }))
+ Ok(Self(coq::Import::new(path_or_module)))
}
}
}