[sc-515] Implement eta-reduction pass

src/lib.rs

@@ -1,4 +1,12 @@
-#![feature(const_type_id, extern_types, inline_const, generic_const_exprs, new_uninit)]
+#![feature(
+  const_type_id,
+  extern_types,
+  inline_const,
+  generic_const_exprs,
+  new_uninit,
+  strict_overflow_ops,
+  iter_map_windows
+)]
 #![cfg_attr(feature = "trace", feature(const_type_name))]
 #![allow(non_snake_case, incomplete_features)]
 

src/main.rs

@@ -336,6 +336,9 @@ fn load_book(files: &[String], transform_opts: &TransformOpts) -> Book {
     );
   }
   for (_, def) in &mut book.nets {
+    if transform_passes.eta_reduce {
+      def.eta_reduce();
+    }
     for tree in def.trees_mut() {
       if transform_passes.coalesce_ctrs {
         tree.coalesce_constructors();

src/transform.rs

@@ -1,3 +1,4 @@
 pub mod coalesce_ctrs;
 pub mod encode_adts;
+pub mod eta_reduce;
 pub mod pre_reduce;

src/transform/eta_reduce.rs

@@ -0,0 +1,126 @@
+use std::collections::HashMap;
+
+use crate::ast::{Net, Tree};
+
+/// Converts (x y), (x y) into x, x
+impl Net {
+  pub fn eta_reduce(&mut self) {
+    let mut phase1 = Phase1::default();
+    phase1.walk_and_sort_net(self);
+    println!("{:?}", phase1.gaps);
+    let mut phase2 = Phase2 { gaps: phase1.gaps };
+    phase2.reduce_net(self);
+  }
+}
+
+#[derive(Debug)]
+enum NodeType {
+  Var(isize),
+  Ctr(u16),
+  Other,
+  Hole,
+}
+
+#[derive(Default)]
+struct Phase1<'a> {
+  vars: HashMap<&'a str, usize>,
+  gaps: Vec<NodeType>,
+}
+
+impl<'a> Phase1<'a> {
+  fn walk_and_sort_net(&mut self, net: &'a mut Net) {
+    self.walk_and_sort_tree(&mut net.root);
+    for (a, b) in net.redexes.iter_mut() {
+      self.walk_and_sort_tree(a);
+      self.walk_and_sort_tree(b);
+    }
+  }
+  fn walk_and_sort_tree(&mut self, tree: &'a mut Tree) {
+    match tree {
+      Tree::Ctr { lab, ports } => {
+        let last_port = ports.len() - 1;
+        for (idx, i) in ports.iter_mut().enumerate() {
+          if idx != last_port {
+            self.gaps.push(NodeType::Ctr(*lab));
+          }
+          self.walk_and_sort_tree(i);
+        }
+      }
+      Tree::Var { nam } => {
+        let nam: &str = &*nam;
+        if let Some(i) = self.vars.get(nam) {
+          let j = self.gaps.len() as isize;
+          self.gaps.push(NodeType::Var(*i as isize - j));
+          self.gaps[*i] = NodeType::Var(j - *i as isize);
+        } else {
+          self.vars.insert(nam, self.gaps.len());
+          self.gaps.push(NodeType::Hole);
+        }
+      }
+      _ => {
+        self.gaps.push(NodeType::Other);
+        for i in tree.children_mut() {
+          self.walk_and_sort_tree(i);
+        }
+      }
+    }
+  }
+}
+
+struct Phase2 {
+  gaps: Vec<NodeType>,
+}
+
+impl Phase2 {
+  fn reduce_net(&mut self, net: &mut Net) {
+    let mut index = 0;
+    self.reduce_tree(&mut net.root, &mut index);
+    for (a, b) in net.redexes.iter_mut() {
+      self.reduce_tree(a, &mut index);
+      self.reduce_tree(b, &mut index);
+    }
+  }
+  fn reduce_tree(&mut self, tree: &mut Tree, index: &mut usize) {
+    match tree {
+      ctr @ Tree::Ctr { .. } => {
+        let Tree::Ctr { lab, ports } = ctr else { unreachable!() };
+        // reduce from the inside of the n-ary node to the outside
+        let mut indices = vec![];
+        let last_port = ports.len() - 1;
+        for (idx, i) in ports.iter_mut().enumerate() {
+          indices.push(*index);
+          if idx != last_port {
+            *index += 1;
+          }
+          self.reduce_tree(i, index);
+        }
+        while indices.len() > 1 {
+          let tail_var = indices.pop().unwrap();
+          let head_ctr = indices.pop().unwrap();
+          let head_var = head_ctr + 1;
+          if let (NodeType::Var(off1), NodeType::Var(off2)) = (&self.gaps[head_var], &self.gaps[tail_var]) {
+            if off1 == off2 {
+              if let NodeType::Ctr(other_lab) = &self.gaps[head_ctr.strict_add_signed(*off1)] {
+                if other_lab == lab {
+                  indices.push(head_var);
+                  ports.pop();
+                  continue;
+                }
+              }
+            }
+          }
+          break;
+        }
+        if ports.len() == 1 {
+          *ctr = ports.pop().unwrap();
+        }
+      }
+      tree => {
+        *index += 1;
+        for i in tree.children_mut() {
+          self.reduce_tree(i, index);
+        }
+      }
+    }
+  }
+}