use clap::Args;
use rossi::{NamedComponent, PrettyPrinter, parse_zip_file};
use std::fs;
use std::path::{Path, PathBuf};
use std::process::ExitCode;
use super::eventb_io::{self, CmdResult, InputFamily};
#[derive(Args)]
pub struct ImportArgs {
#[arg(required = true, value_name = "INPUT")]
inputs: Vec<PathBuf>,
#[arg(short, long, required = true, value_name = "OUTPUT")]
output: PathBuf,
#[arg(long)]
ascii: bool,
#[arg(long, value_name = "STR")]
indent: Option<String>,
#[arg(long, num_args = 0..=1, default_missing_value = "", require_equals = true, value_name = "ORDER")]
merge: Option<String>,
#[arg(short, long)]
verbose: bool,
}
pub fn run(cli: ImportArgs) -> ExitCode {
match run_inner(&cli) {
Ok(()) => ExitCode::SUCCESS,
Err(e) => {
eprintln!("rossi import: {e}");
ExitCode::from(1)
}
}
}
fn run_inner(cli: &ImportArgs) -> CmdResult<()> {
for input in &cli.inputs {
eventb_io::ensure_input(input, InputFamily::Rodin)?;
}
let mut all_components = Vec::new();
for input in &cli.inputs {
if cli.verbose {
eprintln!("Reading Rodin input: {}", input.display());
}
let components = parse_rodin_input(input)?;
if cli.verbose {
eprintln!(" Found {} component(s)", components.len());
}
all_components.extend(components);
}
if all_components.is_empty() {
return Err("No Event-B components found in input files".into());
}
let printer = PrettyPrinter {
use_unicode: !cli.ascii,
indent: cli.indent.clone().unwrap_or_else(|| " ".to_string()),
private_use_glyphs: false,
};
if let Some(ref order) = cli.merge {
if !order.is_empty() {
reorder_components(&mut all_components, order);
}
let mut output = String::new();
for (i, named) in all_components.iter().enumerate() {
if i > 0 {
output.push('\n');
}
output.push_str(&printer.print_component(&named.component));
output.push('\n');
}
if let Some(parent) = cli.output.parent()
&& !parent.as_os_str().is_empty()
{
fs::create_dir_all(parent)?;
}
fs::write(&cli.output, &output)?;
if cli.verbose {
eprintln!(
"Wrote {} component(s) to {}",
all_components.len(),
cli.output.display()
);
}
} else {
fs::create_dir_all(&cli.output)?;
for named in &all_components {
let filename = format!("{}.eventb", named.component.name());
let path = cli.output.join(&filename);
let text = printer.print_component(&named.component);
fs::write(&path, format!("{}\n", text))?;
if cli.verbose {
eprintln!(" Wrote {}", path.display());
}
}
if cli.verbose {
eprintln!(
"Wrote {} file(s) to {}",
all_components.len(),
cli.output.display()
);
}
}
Ok(())
}
fn parse_rodin_input(path: &Path) -> CmdResult<Vec<NamedComponent>> {
if path.is_dir() {
return parse_rodin_directory(path);
}
match path.extension().and_then(|e| e.to_str()) {
Some(ext) if ext.eq_ignore_ascii_case("zip") => Ok(parse_zip_file(path)?),
Some(ext) if eventb_io::is_rodin_xml_ext(ext) => {
eventb_io::parse_rodin_xml_file(path).map(|c| vec![c])
}
_ => Err(format!("Unsupported Rodin input: {}", path.display()).into()),
}
}
fn parse_rodin_directory(dir: &Path) -> CmdResult<Vec<NamedComponent>> {
let mut components = Vec::new();
for file in eventb_io::collect_rodin_xml_files(&[dir.to_path_buf()])? {
components.push(eventb_io::parse_rodin_xml_file(&file)?);
}
Ok(components)
}
fn reorder_components(components: &mut [NamedComponent], order: &str) {
let names: Vec<&str> = order.split(',').map(|s| s.trim()).collect();
for name in &names {
if !components.iter().any(|c| c.component.name() == *name) {
eprintln!("Warning: '{}' does not match any component", name);
}
}
let order_pos = |c: &NamedComponent| -> usize {
let n = c.component.name();
names
.iter()
.position(|&name| name == n)
.unwrap_or(usize::MAX)
};
components.sort_by_key(order_pos);
}