From 4e8b5a4f6d402b0cafa5310b8a32ab96747a6e2e Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Thu, 16 Nov 2023 17:44:05 -0500
Subject: [PATCH] Add the ability to format more than one file at a time.

---
 examples/wip.rs | 32 ++++++++++++-----------------
 src/main.rs     | 54 ++++++++++++++++++++++++++++---------------------
 2 files changed, 44 insertions(+), 42 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index 2707203..345f1c9 100644
--- a/examples/wip.rs
+++ b/examples/wip.rs
@@ -1,24 +1,18 @@
 verus! {
 
-#[allow(unused_macros)]
-macro_rules! no_usize_overflows {
-  ($e:expr,) => {
-    true
-  };
-  ($($e:expr),*) => {
-    no_usize_overflows!(@@internal 0, $($e),*)
-  };
-  (@@internal $total:expr,) => {
-    true
-  };
-  (@@internal $total:expr, $a:expr) => {
-    usize::MAX - $total >= $a
-  };
-  (@@internal $total:expr, $a:expr, $($rest:expr),*) => {
-    usize::MAX - $total >= $a
-      &&
-    no_usize_overflows!(@@internal ($total + $a), $($rest),*)
-  };
+pub fn clone_vec_u8() {
+    let i = 0;
+    while i < v.len() 
+        invariant
+            i <= v.len(),
+            i == out.len(),
+            forall|j| #![auto] 0 <= j < i ==> out@[j] == v@[j],
+        ensures
+            i > 0,
+        decreases 72,
+    {
+        i = i + 1;
+    }
 }
 
 } // verus!
diff --git a/src/main.rs b/src/main.rs
index 22e8313..ecb99f8 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -16,38 +16,23 @@ struct Args {
     /// Run in 'check' mode. Exits with 0 only if the file is formatted correctly.
     #[arg(long = "check")]
     check: bool,
-    /// Input file to be formatted
-    file: PathBuf,
+    /// Input files to be formatted
+    files: Vec<PathBuf>,
     /// Print debugging output (can be repeated for more detail)
     #[arg(short = 'd', long = "debug", action = clap::ArgAction::Count)]
     debug_level: u8,
 }
 
-// TODO: Call rustfmt on the code too (maybe include an option to skip it)
-fn main() -> anyhow::Result<()> {
-    let args = Args::parse();
-
-    tracing_subscriber::fmt()
-        .with_timer(tracing_subscriber::fmt::time::uptime())
-        .with_level(true)
-        .with_target(false)
-        .with_max_level(match args.debug_level {
-            0 => tracing::Level::WARN,
-            1 => tracing::Level::INFO,
-            2 => tracing::Level::DEBUG,
-            _ => tracing::Level::TRACE,
-        })
-        .init();
-
-    let unparsed_file = fs::read_to_string(&args.file)?;
+fn format_file(file: &PathBuf, check: bool) -> anyhow::Result<()> {
+    let unparsed_file = fs::read_to_string(file)?;
     let formatted_output = parse_and_format(&unparsed_file)?;
 
-    if args.check {
+    if check {
         if unparsed_file == formatted_output {
             info!("✨Perfectly formatted✨");
             return Ok(());
         } else {
-            info!("Found some differences");
+            info!("Found some differences in {}", file.display());
             error!("Input found not to be well formatted");
             let diff = similar::udiff::unified_diff(
                 similar::Algorithm::Patience,
@@ -55,12 +40,35 @@ fn main() -> anyhow::Result<()> {
                 &formatted_output,
                 3,
                 Some(("original", "formatted")),
-            );
+                );
             println!("{diff}");
             return Err(anyhow!("invalid formatting"));
         }
     } else {
-        fs::write(args.file, formatted_output)?;
+        fs::write(file, formatted_output)?;
         Ok(())
     }
 }
+
+// TODO: Call rustfmt on the code too (maybe include an option to skip it)
+fn main() -> anyhow::Result<()> {
+    let args = Args::parse();
+    if args.files.len() == 0 {
+        return Err(anyhow!("No files specified"));
+    }
+
+    tracing_subscriber::fmt()
+        .with_timer(tracing_subscriber::fmt::time::uptime())
+        .with_level(true)
+        .with_target(false)
+        .with_max_level(match args.debug_level {
+            0 => tracing::Level::WARN,
+            1 => tracing::Level::INFO,
+            2 => tracing::Level::DEBUG,
+            _ => tracing::Level::TRACE,
+        })
+        .init();
+    // TODO: This errors out when we first find an ill-formatted file.
+    //       Consider going through all of the files, regardless.
+    args.files.iter().try_fold((), |_, file| format_file(&file, args.check))
+}