use rossi::NamedComponent;
use rossi_build::project::{DiscoveredProject, discover_projects};
use rossi_build::repack::repackage_zip_bytes_multi;
use rossi_build::rodin_ids::RodinIds;
use rossi_build::{BuildResult, Project, ProjectComponent, Severity, build};
use super::eventb_io::CmdResult;
pub(crate) fn project_label(prefix: &str) -> &str {
if prefix.is_empty() {
"(root)"
} else {
prefix.trim_end_matches('/')
}
}
pub(crate) fn report_diagnostics(results: &[(String, BuildResult)]) {
let multi = results.len() > 1;
for (prefix, result) in results {
if multi && !result.diagnostics.is_empty() {
let label = project_label(prefix);
eprintln!("--- {label} ---");
}
for d in &result.diagnostics {
eprintln!("{d}");
}
}
}
fn failed_labels(results: &[(String, BuildResult)]) -> Vec<&str> {
results
.iter()
.filter(|(_, r)| r.failed_outright())
.map(|(prefix, _)| project_label(prefix))
.collect()
}
pub(crate) fn build_discovered(projects: Vec<DiscoveredProject>) -> Vec<(String, BuildResult)> {
projects
.into_iter()
.map(|dp| (dp.prefix.clone(), build(&dp.into_project())))
.collect()
}
pub(crate) fn build_archive_projects(
zip_bytes: &[u8],
fallback_name: &str,
) -> CmdResult<Vec<(String, BuildResult)>> {
Ok(build_discovered(discover_projects(
zip_bytes,
fallback_name,
)?))
}
pub(crate) fn repack_results(
src_bytes: &[u8],
results: &[(String, BuildResult)],
) -> std::io::Result<Vec<u8>> {
repackage_zip_bytes_multi(
src_bytes,
results
.iter()
.map(|(prefix, result)| (prefix.as_str(), result)),
)
}
pub(crate) fn gate_before_write(results: &[(String, BuildResult)]) -> CmdResult<Vec<&str>> {
let failed = failed_labels(results);
if results.len() == failed.len() && !failed.is_empty() {
report_diagnostics(results);
return Err("no project produced checked output; see the diagnostics above".into());
}
Ok(failed)
}
pub(crate) fn gate_after_write(
results: &[(String, BuildResult)],
failed: &[&str],
output_noun: &str,
) -> CmdResult<()> {
if !failed.is_empty() {
return Err(format!(
"project(s) {} produced no checked output; see the diagnostics above",
failed.join(", ")
)
.into());
}
let errors = error_diagnostic_count(results);
if errors > 0 {
return Err(format!(
"{errors} error diagnostic(s); {output_noun} was still written \
(erroneous elements are dropped and their files marked inaccurate)"
)
.into());
}
Ok(())
}
pub(crate) fn eb019_result(name: &str, components: Vec<NamedComponent>) -> BuildResult {
let project = Project::new(
name,
components
.into_iter()
.map(|nc| ProjectComponent {
filename: nc.filename,
component: nc.component,
rodin_ids: RodinIds::default(),
source: None,
})
.collect(),
);
build(&project)
}
pub(crate) fn error_diagnostic_count(results: &[(String, BuildResult)]) -> usize {
results
.iter()
.flat_map(|(_, r)| &r.diagnostics)
.filter(|d| d.severity == Severity::Error)
.count()
}