From fe592e0581cd1af58eebec66a85f7066b391a0a8 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Thu, 4 Apr 2024 20:05:10 +0200 Subject: [PATCH] Output list of non-normalized defs after pre-reduce --- src/run/net.rs | 9 ++++++--- src/transform/pre_reduce.rs | 22 +++++++++++++++------- 2 files changed, 21 insertions(+), 10 deletions(-) diff --git a/src/run/net.rs b/src/run/net.rs index d4da5068..7c8d78e6 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 { 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..fbfb3f2a 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,32 @@ impl Book { let State { seen, rewrites, .. } = state; + let mut not_normal = vec![]; for (nam, state) in seen { - if let SeenState::Reduced(net) = state { - self.nets.insert(nam, net); + match state { + SeenState::Reduced { net, normal } => { + 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, pub errors: Vec, } enum SeenState { Cycled, - Reduced(Net), + Reduced { net: Net, normal: bool }, } /// A Def that pushes all interactions to its inner Vec. @@ -138,7 +146,7 @@ impl<'a> State<'a> { let mut rt = run::Net::::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 +163,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() }; } }