Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Output list of non-normalized defs after pre-reduce #115

Merged
merged 3 commits into from
Apr 5, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
9 changes: 6 additions & 3 deletions src/run/net.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,19 +40,22 @@ 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;

while let Some((a, b)) = self.redexes.pop() {
self.interact(a, b);
count += 1;
if count >= limit {
break;
return None;
}
}
count
Some(count)
}

// Lazy mode weak head normalizer
Expand Down
17 changes: 11 additions & 6 deletions src/transform/pre_reduce.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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;

Expand All @@ -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() };
}
}
Loading