From 21bc48150f162f5b806f5a161d5172e690afccde Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 13 Nov 2024 12:42:09 +0100
Subject: [PATCH] Add fixed size join component

---
 DataflowRewriter/Component.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/DataflowRewriter/Component.lean b/DataflowRewriter/Component.lean
index ca1deb4..1e42738 100644
--- a/DataflowRewriter/Component.lean
+++ b/DataflowRewriter/Component.lean
@@ -269,6 +269,23 @@ Essentially tagger + join without internal rule
     internals := []
   }
 
+namespace FixedSize
+
+def BoundedList T n := { ls : List T // ls.length <= n }
+
+@[drunfold] def join T T' n : NatModule (BoundedList T n × BoundedList T' n) :=
+  { inputs := [ (0, ⟨ T, λ (oldListL, oldListR) newElement (newListL, newListR) =>
+                      newListL.val = newElement :: oldListL.val ∧ newListR = oldListR ⟩)
+              , (1, ⟨ T', λ (oldListL, oldListR) newElement (newListL, newListR) =>
+                      newListR.val = newElement :: oldListR.val ∧ newListL = oldListL⟩)].toAssocList,
+    outputs := [(0, ⟨ T × T', λ (oldListL, oldListR) (oldElementL, oldElementR) (newListL, newListR) =>
+                         oldListL.val = newListL.val.concat oldElementL
+                         ∧ oldListR.val = newListR.val.concat oldElementR ⟩)].toAssocList,
+    internals := []
+  }
+
+end FixedSize
+
 end DataflowRewriter.NatModule
 
 namespace DataflowRewriter.StringModule