From 503a54869b64dd29cbcc9f916d0f27a7e701f07f Mon Sep 17 00:00:00 2001
From: Nicolas Abril <nicolas.abril@protonmail.ch>
Date: Fri, 5 Apr 2024 18:32:20 +0200
Subject: [PATCH] Output list of non-normalized defs after pre-reduce (#115)

---
 Cargo.lock                  |  2 +-
 Cargo.toml                  |  2 +-
 src/run/net.rs              |  9 ++++++---
 src/transform/pre_reduce.rs | 17 +++++++++++------
 4 files changed, 19 insertions(+), 11 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 5aec7373..0ddac1cc 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -280,7 +280,7 @@ checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
 
 [[package]]
 name = "hvm-core"
-version = "0.2.22"
+version = "0.2.23"
 dependencies = [
  "arrayvec",
  "clap",
diff --git a/Cargo.toml b/Cargo.toml
index 1d03d41d..0a99170e 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "hvm-core"
-version = "0.2.22"
+version = "0.2.23"
 edition = "2021"
 description = "HVM-Core is a massively parallel Interaction Combinator evaluator."
 license = "MIT"
diff --git a/src/run/net.rs b/src/run/net.rs
index d4da5068..a81dc3d6 100644
--- a/src/run/net.rs
+++ b/src/run/net.rs
@@ -40,8 +40,11 @@ impl<'h, M: Mode> Net<'h, M> {
 
 impl<'a, M: Mode> Net<'a, M> {
   /// Reduces at most `limit` redexes.
+  ///
+  /// If normalized, returns `Some(num_redexes)`.
+  /// If stopped because the limit was reached, returns `None`.
   #[inline(always)]
-  pub fn reduce(&mut self, limit: usize) -> usize {
+  pub fn reduce(&mut self, limit: usize) -> Option<usize> {
     assert!(!M::LAZY);
     let mut count = 0;
 
@@ -49,10 +52,10 @@ impl<'a, M: Mode> Net<'a, M> {
       self.interact(a, b);
       count += 1;
       if count >= limit {
-        break;
+        return None;
       }
     }
-    count
+    Some(count)
   }
 
   // Lazy mode weak head normalizer
diff --git a/src/transform/pre_reduce.rs b/src/transform/pre_reduce.rs
index b8cf6916..4e41df00 100644
--- a/src/transform/pre_reduce.rs
+++ b/src/transform/pre_reduce.rs
@@ -33,7 +33,7 @@ impl Book {
   ///
   /// Defs that are not in the book are treated as inert defs.
   ///
-  /// `max_memory` is measured in words.
+  /// `max_memory` is measured in bytes.
   pub fn pre_reduce(
     &mut self,
     skip: &dyn Fn(&str) -> bool,
@@ -65,24 +65,29 @@ impl Book {
 
     let State { seen, rewrites, .. } = state;
 
+    let mut not_normal = vec![];
     for (nam, state) in seen {
-      if let SeenState::Reduced(net) = state {
+      if let SeenState::Reduced { net, normal } = state {
+        if !normal {
+          not_normal.push(nam.clone());
+        }
         self.nets.insert(nam, net);
       }
     }
 
-    PreReduceStats { rewrites, errors: vec![] }
+    PreReduceStats { rewrites, not_normal, errors: vec![] }
   }
 }
 
 pub struct PreReduceStats {
   pub rewrites: Rewrites,
+  pub not_normal: Vec<String>,
   pub errors: Vec<String>,
 }
 
 enum SeenState {
   Cycled,
-  Reduced(Net),
+  Reduced { net: Net, normal: bool },
 }
 
 /// A Def that pushes all interactions to its inner Vec.
@@ -138,7 +143,7 @@ impl<'a> State<'a> {
 
     let mut rt = run::Net::<run::Strict>::new(self.area);
     rt.boot(self.host.defs.get(nam).expect("No function."));
-    rt.reduce(self.max_rwts as usize);
+    let n_reduced = rt.reduce(self.max_rwts as usize);
 
     self.rewrites += rt.rwts;
 
@@ -155,6 +160,6 @@ impl<'a> State<'a> {
     };
 
     // Replace the "Cycled" state with the "Reduced" state
-    *self.seen.get_mut(nam).unwrap() = SeenState::Reduced(net);
+    *self.seen.get_mut(nam).unwrap() = SeenState::Reduced { net, normal: n_reduced.is_some() };
   }
 }