From 5ad14f8deb2457ab860bb44feb3d3d45ef1da120 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 2 Feb 2020 19:20:16 +0100
Subject: [PATCH] Add option for specifying input files

---
 Cargo.toml                         |  1 +
 src/error.rs                       |  7 +++++++
 src/main.rs                        | 22 ++++++++++++----------
 src/translate/verify_properties.rs | 14 +++++++++++---
 4 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index ceed8ae..afbf59b 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -7,6 +7,7 @@ edition = "2018"
 [dependencies]
 log = "0.4"
 pretty_env_logger = "0.3"
+structopt = "0.3"
 
 [dependencies.clingo]
 path = "../clingo-rs"
diff --git a/src/error.rs b/src/error.rs
index 2bb2548..8c6c942 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -7,6 +7,7 @@ pub enum Kind
 	NotYetImplemented(&'static str),
 	DecodeIdentifier,
 	Translate,
+	ReadFile(std::path::PathBuf),
 }
 
 pub struct Error
@@ -56,6 +57,11 @@ impl Error
 	{
 		Self::new(Kind::Translate).with(source)
 	}
+
+	pub(crate) fn new_read_file<S: Into<Source>>(path: std::path::PathBuf, source: S) -> Self
+	{
+		Self::new(Kind::ReadFile(path)).with(source)
+	}
 }
 
 impl std::fmt::Debug for Error
@@ -72,6 +78,7 @@ impl std::fmt::Debug for Error
 				"not yet implemented ({})", description),
 			Kind::DecodeIdentifier => write!(formatter, "could not decode identifier"),
 			Kind::Translate => write!(formatter, "could not translate input program"),
+			Kind::ReadFile(path) => write!(formatter, "could not read file “{}”", path.display()),
 		}?;
 
 		if let Some(source) = &self.source
diff --git a/src/main.rs b/src/main.rs
index f9d7f4e..0005856 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,18 +1,20 @@
+use structopt::StructOpt as _;
+
+#[derive(Debug, structopt::StructOpt)]
+#[structopt(name = "anthem", about = "Use first-order theorem provers with answer set programs.")]
+struct Options
+{
+	#[structopt(parse(from_os_str))]
+	input: Vec<std::path::PathBuf>,
+}
+
 fn main()
 {
 	pretty_env_logger::init();
 
-	let program = match std::fs::read_to_string("test.lp")
-	{
-		Ok(value) => value,
-		Err(error) =>
-		{
-			log::error!("could not read input program: {}", error);
-			std::process::exit(1);
-		},
-	};
+	let options = Options::from_args();
 
-	if let Err(error) = anthem::translate::verify_properties::translate(&program)
+	if let Err(error) = anthem::translate::verify_properties::translate(&options.input)
 	{
 		log::error!("could not translate input program: {}", error);
 		std::process::exit(1)
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index 4b214dc..1b94720 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -88,12 +88,20 @@ impl clingo::Logger for Logger
 	}
 }
 
-pub fn translate(program: &str) -> Result<(), crate::Error>
+pub fn translate<P>(program_paths: &[P]) -> Result<(), crate::Error>
+where
+	P: AsRef<std::path::Path>
 {
 	let mut statement_handler = StatementHandler::new();
 
-	clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)
-		.map_err(|error| crate::Error::new_translate(error))?;
+	for program_path in program_paths
+	{
+		let program = std::fs::read_to_string(program_path.as_ref())
+			.map_err(|error| crate::Error::new_read_file(program_path.as_ref().to_path_buf(), error))?;
+
+		clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)
+			.map_err(|error| crate::Error::new_translate(error))?;
+	}
 
 	let context = statement_handler.context;
 	let mut definitions = context.definitions;