From 8b05c5952821b63d0baa423b661f6eaab9972832 Mon Sep 17 00:00:00 2001
From: FranchuFranchu <fff999abc999@gmail.com>
Date: Thu, 14 Mar 2024 17:06:10 -0300
Subject: [PATCH] Document eta reduction.

---
 src/transform/eta_reduce.rs | 54 ++++++++++++++++++++++++++++++++++++-
 1 file changed, 53 insertions(+), 1 deletion(-)

diff --git a/src/transform/eta_reduce.rs b/src/transform/eta_reduce.rs
index 67e2b4ad..1f0572ae 100644
--- a/src/transform/eta_reduce.rs
+++ b/src/transform/eta_reduce.rs
@@ -1,9 +1,61 @@
+//! Carries out simple eta-reduction, to reduce the amount of rewrites at runtime.
+//!
+//! ### Eta-equivalence
+//! 
+//! In interaction combinators, there are some nets that are equivalent and
+//! have no observable difference
+//! 
+//! ![Image of eta-equivalence](https://i.postimg.cc/XYVxdMFW/image.png)
+//!
+//! This module implements the eta-equivalence rule at the top-left of the image above
+//!
+//! ```txt
+//!     /|-, ,-|\     eta_reduce
+//! ---| |  X  | |-- ~~~~~~~~~~~~> -------------
+//!     \|-' '-|/
+//! ```
+//!
+//! In hvm-core's AST representation, this reduction looks like this
+//! 
+//! ```txt
+//! {lab x y} ... {lab x y} ~~~~~~~~> x ..... x
+//! ```
+//! 
+//! Essentially, both occurrences of the same constructor are replaced by a
+//! variable.
+//! 
+//! ### The algorithm
+//! 
+//! The code uses a two-pass O(n) algorithm, where `n` is the amount of nodes
+//! in the AST
+//! 
+//! In the first pass, a node-list is built out of an ordered traversal of the AST.
+//! Crucially, the node list stores variable offsets instead of the variable's names 
+//! Since the AST's order is consistent, the ordering of nodes in the node list can be
+//! reproduced with a traversal.
+//! 
+//! This means that each occurrence of a vaiable is encoded with the offset in the node-list to 
+//! the _other_ occurrence of the variable.
+//! 
+//! For example, if we start with the net: `[(x y) (x y)]`
+//!
+//! The resulting node list will look like this:
+//!
+//! `[Ctr(1), Ctr(0), Var(3), Var(3), Ctr(0), Var(-3), Var(-3)]`
+//!
+//! The second pass uses the node list to find repeated constructors. If a constructor's 
+//! children are both variables with the same offset, then we lookup that offset relative to
+//! the constructor. If it is equal to the first constructor, it means both of them are equal
+//! and they can be replaced with a variable.
+
+
+
 use std::{collections::HashMap, ops::RangeFrom};
 
 use crate::ast::{Net, Tree};
 
-/// Converts `(x y), (x y)` into `x, x`.
 impl Net {
+  /// Carries out simple eta-reduction
   pub fn eta_reduce(&mut self) {
     let mut phase1 = Phase1::default();
     for tree in self.trees() {