From d8bac1307bb4e4c005ce1a92ecbe3bde8734b3dd Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 9 Nov 2024 20:33:04 +0100
Subject: [PATCH] Reprove product

---
 DataflowRewriter/Module.lean   | 22 ++++++++++++++++------
 DataflowRewriter/Rewriter.lean |  3 +++
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/DataflowRewriter/Module.lean b/DataflowRewriter/Module.lean
index 4b2ef5d..3ec9a85 100644
--- a/DataflowRewriter/Module.lean
+++ b/DataflowRewriter/Module.lean
@@ -693,7 +693,7 @@ theorem refines_φ_product {J K} [Nonempty J] [Nonempty I] {imod₂ : Module Ide
   [MatchInterface imod₂ smod₂] {φ₁ φ₂} :
     imod ⊑_{φ₁} smod →
     imod₂ ⊑_{φ₂} smod₂ →
-    imod.product imod₂ ⊑_{λ a b => φ₁ a.1 b.1 ∧ φ₂ a.2 b.2} smod.product smod₂ := by stop
+    imod.product imod₂ ⊑_{λ a b => φ₁ a.1 b.1 ∧ φ₂ a.2 b.2} smod.product smod₂ := by
   intro href₁ href₂
   have mm_prod : MatchInterface (imod.product imod₂) (smod.product smod₂) := by apply MatchInterface_product
   unfold refines_φ at *
@@ -779,13 +779,15 @@ theorem refines_φ_product {J K} [Nonempty J] [Nonempty I] {imod₂ : Module Ide
           cases h : AssocList.find? ident imod.inputs; rw [h] at hruleIn'none
           rw [h] at this; simp [-AssocList.find?_eq] at this; assumption
           rw [h] at this; rw [h] at hruleIn'none; injection hruleIn'none
+        have hrule_another : (AssocList.mapVal (fun x => @liftL S K) smod.inputs).find? ident = none := by
+          rw [←AssocList.find?_map_comm]; simp only [*]; rfl
         have : (AssocList.mapVal (fun x => liftR) smod₂.inputs).find? ident = some (@liftR S _ Srule) := by
           rw [←AssocList.find?_map_comm]; rw [HSrule]; rfl
         have s : (smod.product smod₂).inputs.getIO ident = liftR (smod₂.inputs.getIO ident) := by
           skip; dsimp [Module.product, PortMap.getIO];
           rw [AssocList.append_find_right, this]
           · rw [HSrule]; rfl
-          · rw [hruleIn'none]
+          · rw [hrule_another]
         rw [rw_rule_execution s]
         dsimp [liftL]; refine ⟨?_, rfl⟩; convert hrule₃; simp
       · solve_by_elim [existSR_append_right, existSR_liftR']
@@ -834,6 +836,7 @@ theorem refines_φ_product {J K} [Nonempty J] [Nonempty I] {imod₂ : Module Ide
       · assumption
       · apply hφ.right
     case inr =>
+      rcases hruleIn' with ⟨hruleIn'none, hruleIn'⟩
       rw [AssocList.find?_mapVal] at hruleIn'
       cases h : AssocList.find? ident imod₂.outputs; rw [h] at hruleIn'; injection hruleIn'
       rename_i rule'; rw [h] at hruleIn'; simp at hruleIn'; subst_vars
@@ -862,14 +865,21 @@ theorem refines_φ_product {J K} [Nonempty J] [Nonempty I] {imod₂ : Module Ide
           simp [-AssocList.find?_eq] at this
           exact Option.isSome_iff_exists.mp this
         rcases this with ⟨Srule, HSrule⟩
+        have : smod.outputs.find? ident = none := by
+          have := ‹MatchInterface imod smod›.outputs_present ident
+          rw [AssocList.find?_mapVal] at hruleIn'none
+          cases h : AssocList.find? ident imod.outputs; rw [h] at hruleIn'none
+          rw [h] at this; simp [-AssocList.find?_eq] at this; assumption
+          rw [h] at this; rw [h] at hruleIn'none; injection hruleIn'none
+        have hrule_another : (AssocList.mapVal (fun x => @liftL S K) smod.outputs).find? ident = none := by
+          rw [←AssocList.find?_map_comm]; simp only [*]; rfl
         have : (AssocList.mapVal (fun x => liftR) smod₂.outputs).find? ident = some (@liftR S _ Srule) := by
           rw [←AssocList.find?_map_comm]; rw [HSrule]; rfl
         have s : (smod.product smod₂).outputs.getIO ident = liftR (smod₂.outputs.getIO ident) := by
-          have : Disjoint smod smod₂ := MatchInterface_Disjoint hdisj
-          rcases this with ⟨l,r⟩
           skip; dsimp [Module.product, PortMap.getIO];
-          rw [AssocList.append_find_right_disjoint (a := (AssocList.mapVal (fun x => liftL) smod.outputs)) (AssocList.disjoint_keys_mapVal_both r) this]
-          rw [HSrule]; rfl
+          rw [AssocList.append_find_right, this]
+          · rw [HSrule]; rfl
+          · rw [hrule_another]
         rw [rw_rule_execution s]
         dsimp [liftL]; refine ⟨?_, rfl⟩; convert hrule₃; simp
       · solve_by_elim [existSR_append_right, existSR_liftR']
diff --git a/DataflowRewriter/Rewriter.lean b/DataflowRewriter/Rewriter.lean
index 14d5d34..04d91c4 100644
--- a/DataflowRewriter/Rewriter.lean
+++ b/DataflowRewriter/Rewriter.lean
@@ -211,6 +211,9 @@ def followInput' (g : ExprHigh String) (inst input : String) : RewriteResult (Ne
 def followInput (g : ExprHigh String) (inst input : String) : Option (NextNode String) :=
   (followInput' g inst input).toOption
 
+def findType (g : ExprHigh String) (typ : String) : List String :=
+  g.modules.foldl (λ l a b => if b.snd = typ then a :: l else l) []
+
 def calcSucc (g : ExprHigh String) : Option (Std.HashMap String (Array String)) :=
   g.modules.foldlM (λ succ k v => do
       let a ← v.fst.output.foldlM (λ succ' (k' v' : InternalPort String) => do