From 8e43c3de3a79232800ea4619d7894a7bb0342e8b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 6 Nov 2024 16:51:33 +0100
Subject: [PATCH] Add comments to the dynamatic printer

---
 DataflowRewriter/Component.lean        | 6 +++---
 DataflowRewriter/DynamaticPrinter.lean | 8 ++++++--
 DataflowRewriter/Module.lean           | 1 -
 3 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/DataflowRewriter/Component.lean b/DataflowRewriter/Component.lean
index dd046dd..fa4a83f 100644
--- a/DataflowRewriter/Component.lean
+++ b/DataflowRewriter/Component.lean
@@ -177,7 +177,7 @@ Essentially tagger + join without internal rule
           (tag ∈ oldOrder ∧ oldMap.find? tag = none) ∧
           newMap = oldMap.cons tag el ∧ newOrder = oldOrder ∧ newVal = oldVal ⟩),
         -- Enq a value to be tagged
-        (0, ⟨ T, λ (oldOrder, oldMap, oldVal) v (newOrder, newMap, newVal) =>
+        (1, ⟨ T, λ (oldOrder, oldMap, oldVal) v (newOrder, newMap, newVal) =>
           -- Tag must be used, but no value ready, otherwise block:
           newMap = oldMap ∧ newOrder = oldOrder ∧ newVal = v :: oldVal ⟩)
       ].toAssocList,
@@ -191,8 +191,8 @@ Essentially tagger + join without internal rule
         -- Dequeue + free tag
       (1, ⟨ T, λ (oldorder, oldmap, oldVal) el (neworder, newmap, newVal) =>
         -- tag must be used otherwise, but no value brought, undefined behavior:
-        ∃ l tag , oldorder = l.cons tag ∧ oldmap.find? tag = some el ∧
-        newmap = oldmap.eraseAll tag ∧ neworder = l ∧ newVal = oldVal ⟩),
+        ∃ tag , oldorder = neworder.concat tag ∧ oldmap.find? tag = some el ∧
+        newmap = oldmap.eraseAll tag ∧ newVal = oldVal ⟩),
         ].toAssocList,
     internals := []
   }
diff --git a/DataflowRewriter/DynamaticPrinter.lean b/DataflowRewriter/DynamaticPrinter.lean
index 3adaccb..3bef931 100644
--- a/DataflowRewriter/DynamaticPrinter.lean
+++ b/DataflowRewriter/DynamaticPrinter.lean
@@ -35,7 +35,8 @@ def interfaceTypes (m : AssocList String String) :=
   , ("Fork6", (some "Fork", "in1:32", "out1:32 out2:32 out3:32 out4:32 out5:32 out6:32", []))
   , ("TagggedFork", (none, "in1:32", "out1:32 out2:32", []))
 
-  , ("CntrlMerge", (none, "in1:32 in2:32", "out1:32 out2?:1", []))
+  -- TODO FIX DELAY
+  , ("CntrlMerge", (none, "in1:32 in2:32", "out1:32 out2?:1", [("delay", "1.234510"), ("delay2", "1.234510")]))
   , ("TagggedCntrlMerge", (none, "in1:32 in2:32", "out1:32 out2?:1", []))
 
   , ("Branch", (none, "in1:32 in2?:1", "out1+:32 out2-:32", []))
@@ -59,6 +60,9 @@ def interfaceTypes (m : AssocList String String) :=
   , ("Aligner", (none, "in1:32 in2:32", "out1:32 out2:32", []))
   , ("TaggerCntrlAligner", (none, "in1:32 in2:32", "out1:32 out2:32", []))
 
+  -- TODO WRONG
+  , ("Sink", (none, "in1:32 in2:32", "out1:32 out2:32", []))
+
   -- Constants are currently axiomatised
   , ("ConstantA", (some "Constant", "in1:0", "out1:32", [("value", m.find? "A" |>.getD "unrecognised")]))
   , ("ConstantB", (some "Constant", "in1:0", "out1:32", [("value", m.find? "B" |>.getD "unrecognised")]))
@@ -102,7 +106,7 @@ def dynamaticString (a: ExprHigh String) (m : AssocList String String): Option S
   let modules ←
     a.modules.foldlM
       (λ s k v => do
-        let fmt := (interfaceTypes m).find? v.snd |>.getD (some v.snd, "", "", [])
+        let fmt := (interfaceTypes m).find? v.snd |>.getD (some v.snd, "", "", [("unsupported", "true")])
         return s ++ s!"  {k} [type = \"{fmt.1.getD v.snd}\", label = \"{k}: {v.snd}\", in = \"{fmt.2.1}\", out = \"{fmt.2.2.1}\"{formatOptions fmt.2.2.2}];\n"
         ) ""
   let connections :=
diff --git a/DataflowRewriter/Module.lean b/DataflowRewriter/Module.lean
index 09600e0..49d5fd7 100644
--- a/DataflowRewriter/Module.lean
+++ b/DataflowRewriter/Module.lean
@@ -673,7 +673,6 @@ theorem refines_product {J K} [Nonempty J] [Nonempty I] (imod₂ : Module Ident
   specialize ref₂ hφ₂
   all_goals sorry
 
-
 theorem refines_connect {o i} :
     imod ⊑ smod →
     imod.connect' o i ⊑ smod.connect' o i := by sorry