Fix name generation in fresh renaming

VCA-EPFL · Nov 9, 2024 · 6c6eebc · 6c6eebc
1 parent e03be27
commit 6c6eebc
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 187 deletions.
diff --git a/DataflowRewriter/Basic.lean b/DataflowRewriter/Basic.lean
@@ -185,6 +185,10 @@ def toIdentityPortMapping' (i : Interface Ident) : PortMapping Ident :=
   ⟨(i.input.map (λ a => (⟨.top, a.name⟩, a))).toAssocList,
    (i.output.map (λ a => (⟨.top, a.name⟩, a))).toAssocList⟩
 
+def toIdentityPortMapping'' (ident : Ident) (i : Interface Ident) : PortMapping Ident :=
+  ⟨(i.input.map (λ a => (⟨.internal ident, a.name⟩, a))).toAssocList,
+   (i.output.map (λ a => (⟨.internal ident, a.name⟩, a))).toAssocList⟩
+
 def toPortMapping (i : Interface Ident) (ident : Ident) : PortMapping Ident :=
   if i.isBaseModule
   then ⟨(i.input.map (λ a => (a, InternalPort.mk (.internal ident) a.name))).toAssocList,

diff --git a/DataflowRewriter/Rewriter.lean b/DataflowRewriter/Rewriter.lean
@@ -58,20 +58,20 @@ def liftError {α} : Except String α → Except RewriteError α
 
 end Rewrite
 
-def generate_renaming (fresh_prefix : String) (internals : List (InternalPort String)) :=
-  go 0 ∅ ∅ internals
+def generate_renaming (nameMap : AssocList String String) (fresh_prefix : String) (internals : List (InternalPort String)) :=
+  go 0 nameMap ∅ internals
   where
     go (n : Nat) (nameMap : AssocList String String) (p : PortMap String (InternalPort String))
-      : List (InternalPort String) → PortMap String (InternalPort String)
+      : List (InternalPort String) → PortMap String (InternalPort String) × AssocList String String
     | (⟨.internal inst, name⟩) :: b =>
       match nameMap.find? inst with
       | some inst' => go n nameMap (p.cons ⟨.internal inst, name⟩ ⟨.internal inst', name⟩) b
       | none =>
         let inst' := fresh_prefix ++ toString n
         let nameMap' := nameMap.cons inst inst'
-        go n nameMap (p.cons ⟨.internal inst, name⟩ ⟨.internal inst', name⟩) b
+        go (n+1) nameMap' (p.cons ⟨.internal inst, name⟩ ⟨.internal inst', name⟩) b
     | ⟨.top, name⟩ :: b => go n nameMap p b
-    | [] => p
+    | [] => (p, nameMap)
 
 /--
 Perform a rewrite in the graph by lowering it into an inductive expression using
@@ -91,10 +91,9 @@ language does not remember any names.
   let (ext_mapping, _) ← liftError <| e_sub.beq rewrite.input_expr
   let e_sub' := rewrite.output_expr.renameMapped ext_mapping.inverse
   let (e_sub'_vars_i, e_sub'_vars_o) := e_sub'.allVars
-  let int_mapping' : PortMapping String :=
-    ⟨ generate_renaming fresh_prefix (e_sub'_vars_i.filter (λ x => x ∉ ext_mapping.input.keysList))
-    , generate_renaming fresh_prefix (e_sub'_vars_o.filter (λ x => x ∉ ext_mapping.output.keysList))
-    ⟩
+  let (inputPortMap, nameMap) := generate_renaming ∅ fresh_prefix (e_sub'_vars_i.filter (λ x => x ∉ ext_mapping.input.keysList))
+  let (outputPortMap, _) := generate_renaming nameMap fresh_prefix (e_sub'_vars_o.filter (λ x => x ∉ ext_mapping.output.keysList))
+  let int_mapping' : PortMapping String := ⟨ inputPortMap, outputPortMap ⟩
   let e_renamed_sub' := e_sub'.renameMapped int_mapping'
   return g_lower.replace e_sub e_renamed_sub' |>.higherS fresh_prefix
 
@@ -115,10 +114,11 @@ proofs that are already present in the framework should be enough.
   /- Here we have to make sure that the context contains a renamed version of
   e_sub to show equivalence to the abstracted version, because the abstracted
   version has `.top` IO ports -/
-  let portMapping := e_sub.build_interface.toIdentityPortMapping
+  let portMapping := e_sub.build_interface.toIdentityPortMapping' -- abstraction.typ
   let abstracted := g_lower.abstract e_sub portMapping abstraction.typ
-  -- return (abstracted.higherS fresh_prefix, ⟨e_sub.renameMapped portMapping.inverse, abstraction.typ⟩)
-  return (abstracted.higherS fresh_prefix, ⟨e_sub, abstraction.typ⟩)
+  let e_sub' := e_sub.renameMapped portMapping.inverse
+  return (abstracted.higherS fresh_prefix, ⟨e_sub', abstraction.typ⟩)
+  -- return (abstracted.higherS fresh_prefix, ⟨e_sub, abstraction.typ⟩)
 
 /--
 Can be used to concretise the abstract node again.  Currently it assumes
@@ -132,8 +132,12 @@ are still fresh in the graph.
   -- may need to uniquify the concretisation internal connections
   let base ← ofOption (.error "Could not find base of concretisation")
     <| g_lower.findBase concretisation.typ
-  return g_lower.concretise (concretisation.expr.renameMapped base) base concretisation.typ
-         |>.higherS fresh_prefix
+  -- return g_lower.concretise (concretisation.expr.renameMapped base) base concretisation.typ
+  --        |>.higherS fresh_prefix
+  dbg_trace s!"{repr <| concretisation.typ}"
+  dbg_trace s!"{repr <| concretisation.expr.renameMapped base}"
+  let e_sub := concretisation.expr.renameMapped base
+  return g_lower.concretise e_sub base concretisation.typ |>.higherS fresh_prefix
 
 @[drunfold] def rewrite (fresh_prefix : String) (g : ExprHigh String) (rewrite : Rewrite String)
   : RewriteResult (ExprHigh String) := do
@@ -142,6 +146,7 @@ are still fresh in the graph.
       return (g'', c''::c', n+1)
     ) (g, [], 0)
   let g ← rewrite.run (fresh_prefix ++ s!"_R_") g
+  dbg_trace s!"before: {repr g}"
   c.foldlM (λ (g, n) (c : Concretisation String) => do
     let g' ← c.run (fresh_prefix ++ s!"_C_{n}_") g
     return (g', n+1)) (g, 0) |>.map Prod.fst

diff --git a/DataflowRewriter/Rewrites/BranchMuxToMerge.lean b/DataflowRewriter/Rewrites/BranchMuxToMerge.lean
@@ -223,176 +223,3 @@ def lhs' : ExprHigh String := [graph|
 end TEST
 
 end DataflowRewriter.BranchMuxToMerge
-
-DataflowRewriter.ExprLow.connect
-  { inst := DataflowRewriter.InstIdent.internal "fork", name := "out0" }
-  { inst := DataflowRewriter.InstIdent.internal "branch", name := "cond" }
-  (DataflowRewriter.ExprLow.connect
-    { inst := DataflowRewriter.InstIdent.internal "fork", name := "out1" }
-    { inst := DataflowRewriter.InstIdent.internal "mux", name := "cond" }
-    (DataflowRewriter.ExprLow.connect
-      { inst := DataflowRewriter.InstIdent.internal "branch", name := "true" }
-      { inst := DataflowRewriter.InstIdent.internal "m_left", name := "m_in" }
-      (DataflowRewriter.ExprLow.connect
-        { inst := DataflowRewriter.InstIdent.internal "branch", name := "false" }
-        { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_in" }
-        (DataflowRewriter.ExprLow.connect
-          { inst := DataflowRewriter.InstIdent.internal "m_left", name := "m_out" }
-          { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp0" }
-          (DataflowRewriter.ExprLow.connect
-            { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_out" }
-            { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp1" }
-            (DataflowRewriter.ExprLow.product
-              (DataflowRewriter.ExprLow.base
-                { input := Batteries.AssocList.cons
-                             { inst := DataflowRewriter.InstIdent.top, name := "cond" }
-                             { inst := DataflowRewriter.InstIdent.internal "branch", name := "cond" }
-                             (Batteries.AssocList.cons
-                               { inst := DataflowRewriter.InstIdent.top, name := "val" }
-                               { inst := DataflowRewriter.InstIdent.top, name := "i_branch" }
-                               (Batteries.AssocList.nil)),
-                  output := Batteries.AssocList.cons
-                              { inst := DataflowRewriter.InstIdent.top, name := "false" }
-                              { inst := DataflowRewriter.InstIdent.internal "branch", name := "false" }
-                              (Batteries.AssocList.cons
-                                { inst := DataflowRewriter.InstIdent.top, name := "true" }
-                                { inst := DataflowRewriter.InstIdent.internal "branch", name := "true" }
-                                (Batteries.AssocList.nil)) }
-                "branch")
-              (DataflowRewriter.ExprLow.product
-                (DataflowRewriter.ExprLow.base
-                  { input := Batteries.AssocList.cons
-                               { inst := DataflowRewriter.InstIdent.top, name := "m_in" }
-                               { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_in" }
-                               (Batteries.AssocList.nil),
-                    output := Batteries.AssocList.cons
-                                { inst := DataflowRewriter.InstIdent.top, name := "m_out" }
-                                { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_out" }
-                                (Batteries.AssocList.nil) }
-                  "mod_right")
-                (DataflowRewriter.ExprLow.product
-                  (DataflowRewriter.ExprLow.base
-                    { input := Batteries.AssocList.cons
-                                 { inst := DataflowRewriter.InstIdent.top, name := "inp1" }
-                                 { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp1" }
-                                 (Batteries.AssocList.cons
-                                   { inst := DataflowRewriter.InstIdent.top, name := "inp0" }
-                                   { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp0" }
-                                   (Batteries.AssocList.cons
-                                     { inst := DataflowRewriter.InstIdent.top, name := "cond" }
-                                     { inst := DataflowRewriter.InstIdent.internal "mux", name := "cond" }
-                                     (Batteries.AssocList.nil))),
-                      output := Batteries.AssocList.cons
-                                  { inst := DataflowRewriter.InstIdent.top, name := "out0" }
-                                  { inst := DataflowRewriter.InstIdent.top, name := "o_out" }
-                                  (Batteries.AssocList.nil) }
-                    "mux")
-                  (DataflowRewriter.ExprLow.product
-                    (DataflowRewriter.ExprLow.base
-                      { input := Batteries.AssocList.cons
-                                   { inst := DataflowRewriter.InstIdent.top, name := "m_in" }
-                                   { inst := DataflowRewriter.InstIdent.internal "m_left", name := "m_in" }
-                                   (Batteries.AssocList.nil),
-                        output := Batteries.AssocList.cons
-                                    { inst := DataflowRewriter.InstIdent.top, name := "m_out" }
-                                    { inst := DataflowRewriter.InstIdent.internal "m_left", name := "m_out" }
-                                    (Batteries.AssocList.nil) }
-                      "mod_left")
-                    (DataflowRewriter.ExprLow.base
-                      { input := Batteries.AssocList.cons
-                                   { inst := DataflowRewriter.InstIdent.top, name := "inp0" }
-                                   { inst := DataflowRewriter.InstIdent.top, name := "i_cond" }
-                                   (Batteries.AssocList.nil),
-                        output := Batteries.AssocList.cons
-                                    { inst := DataflowRewriter.InstIdent.top, name := "out1" }
-                                    { inst := DataflowRewriter.InstIdent.internal "fork", name := "out1" }
-                                    (Batteries.AssocList.cons
-                                      { inst := DataflowRewriter.InstIdent.top, name := "out0" }
-                                      { inst := DataflowRewriter.InstIdent.internal "fork", name := "out0" }
-                                      (Batteries.AssocList.nil)) }
-                      "fork"))))))))))
-
-DataflowRewriter.ExprLow.connect
-  { inst := DataflowRewriter.InstIdent.internal "fork", name := "out0" }
-  { inst := DataflowRewriter.InstIdent.internal "branch", name := "cond" }
-  (DataflowRewriter.ExprLow.connect
-    { inst := DataflowRewriter.InstIdent.internal "fork", name := "out1" }
-    { inst := DataflowRewriter.InstIdent.internal "mux", name := "cond" }
-    (DataflowRewriter.ExprLow.connect
-      { inst := DataflowRewriter.InstIdent.internal "branch", name := "true" }
-      { inst := DataflowRewriter.InstIdent.internal "m_left1", name := "m_in" }
-      (DataflowRewriter.ExprLow.connect
-        { inst := DataflowRewriter.InstIdent.internal "branch", name := "false" }
-        { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_in" }
-        (DataflowRewriter.ExprLow.connect
-          { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_out" }
-          { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp1" }
-          (DataflowRewriter.ExprLow.product
-            (DataflowRewriter.ExprLow.base
-              { input := Batteries.AssocList.cons
-                           { inst := DataflowRewriter.InstIdent.top, name := "cond" }
-                           { inst := DataflowRewriter.InstIdent.internal "branch", name := "cond" }
-                           (Batteries.AssocList.cons
-                             { inst := DataflowRewriter.InstIdent.top, name := "val" }
-                             { inst := DataflowRewriter.InstIdent.top, name := "i_branch" }
-                             (Batteries.AssocList.nil)),
-                output := Batteries.AssocList.cons
-                            { inst := DataflowRewriter.InstIdent.top, name := "false" }
-                            { inst := DataflowRewriter.InstIdent.internal "branch", name := "false" }
-                            (Batteries.AssocList.cons
-                              { inst := DataflowRewriter.InstIdent.top, name := "true" }
-                              { inst := DataflowRewriter.InstIdent.internal "branch", name := "true" }
-                              (Batteries.AssocList.nil)) }
-              "branch")
-            (DataflowRewriter.ExprLow.product
-              (DataflowRewriter.ExprLow.base
-                { input := Batteries.AssocList.cons
-                             { inst := DataflowRewriter.InstIdent.top, name := "m_in" }
-                             { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_in" }
-                             (Batteries.AssocList.nil),
-                  output := Batteries.AssocList.cons
-                              { inst := DataflowRewriter.InstIdent.top, name := "m_out" }
-                              { inst := DataflowRewriter.InstIdent.internal "m_right", name := "m_out" }
-                              (Batteries.AssocList.nil) }
-                "mod_right")
-              (DataflowRewriter.ExprLow.product
-                (DataflowRewriter.ExprLow.base
-                  { input := Batteries.AssocList.cons
-                               { inst := DataflowRewriter.InstIdent.top, name := "inp1" }
-                               { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp1" }
-                               (Batteries.AssocList.cons
-                                 { inst := DataflowRewriter.InstIdent.top, name := "inp0" }
-                                 { inst := DataflowRewriter.InstIdent.internal "mux", name := "inp0" }
-                                 (Batteries.AssocList.cons
-                                   { inst := DataflowRewriter.InstIdent.top, name := "cond" }
-                                   { inst := DataflowRewriter.InstIdent.internal "mux", name := "cond" }
-                                   (Batteries.AssocList.nil))),
-                    output := Batteries.AssocList.cons
-                                { inst := DataflowRewriter.InstIdent.top, name := "out0" }
-                                { inst := DataflowRewriter.InstIdent.top, name := "o_out" }
-                                (Batteries.AssocList.nil) }
-                  "mux")
-                (DataflowRewriter.ExprLow.product
-                  (DataflowRewriter.ExprLow.base
-                    { input := Batteries.AssocList.cons
-                                 { inst := DataflowRewriter.InstIdent.top, name := "m_in" }
-                                 { inst := DataflowRewriter.InstIdent.internal "m_left1", name := "m_in" }
-                                 (Batteries.AssocList.nil),
-                      output := Batteries.AssocList.cons
-                                  { inst := DataflowRewriter.InstIdent.top, name := "out0" }
-                                  { inst := DataflowRewriter.InstIdent.internal "m_left1", name := "out0" }
-                                  (Batteries.AssocList.nil) }
-                    "mod_left1")
-                  (DataflowRewriter.ExprLow.base
-                    { input := Batteries.AssocList.cons
-                                 { inst := DataflowRewriter.InstIdent.top, name := "inp0" }
-                                 { inst := DataflowRewriter.InstIdent.top, name := "i_cond" }
-                                 (Batteries.AssocList.nil),
-                      output := Batteries.AssocList.cons
-                                  { inst := DataflowRewriter.InstIdent.top, name := "out1" }
-                                  { inst := DataflowRewriter.InstIdent.internal "fork", name := "out1" }
-                                  (Batteries.AssocList.cons
-                                    { inst := DataflowRewriter.InstIdent.top, name := "out0" }
-                                    { inst := DataflowRewriter.InstIdent.internal "fork", name := "out0" }
-                                    (Batteries.AssocList.nil)) }
-                    "fork")))))))))