Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/VCA-EPFL/dataflow-rewriter
Browse files Browse the repository at this point in the history
  • Loading branch information
@threonorm
threonorm committed Nov 9, 2024
2 parents 9194b20 + 6bea376 commit e03be27
Show file tree
Hide file tree
Showing 7 changed files with 232 additions and 31 deletions.
11 changes: 11 additions & 0 deletions DataflowRewriter/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,6 +163,7 @@ end PortMapping
structure Interface (Ident) where
input : List (InternalPort Ident)
output : List (InternalPort Ident)
deriving Repr

namespace Interface

Expand All @@ -177,6 +178,13 @@ def toIdentityPortMapping (i : Interface Ident) : PortMapping Ident :=
⟨(i.input.map (λ a => (a, a))).toAssocList,
(i.output.map (λ a => (a, a))).toAssocList⟩

/--
Need to be careful with the renaming now.
-/
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 toPortMapping (i : Interface Ident) (ident : Ident) : PortMapping Ident :=
if i.isBaseModule
then ⟨(i.input.map (λ a => (a, InternalPort.mk (.internal ident) a.name))).toAssocList,
Expand All @@ -188,4 +196,7 @@ end Interface
def PortMapping.toInterface {Ident} (p : PortMapping Ident) : Interface Ident :=
⟨p.input.keysList, p.output.keysList⟩

def PortMapping.toInterface' {Ident} (p : PortMapping Ident) : Interface Ident :=
⟨p.input.toList.map Prod.snd, p.output.toList.map Prod.snd⟩

end DataflowRewriter
1 change: 0 additions & 1 deletion DataflowRewriter/Component.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,6 @@ Essentially tagger + join without internal rule
newMap = oldMap.cons tag el ∧ newOrder = oldOrder ∧ newVal = oldVal ⟩),
-- Enq a value to be tagged
(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,
outputs := [
Expand Down
2 changes: 1 addition & 1 deletion DataflowRewriter/ExprLow.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ def ofOption {α ε} (e : ε) : Option α → Except ε α
| _, _ => throw "beq error: expressions are structurally not similar"

@[drunfold] def build_interface : ExprLow Ident → Interface Ident
| .base map typ => map.toInterface
| .base map typ => map.toInterface'
| .connect o i e =>
let int := e.build_interface
⟨int.input.erase i, int.output.erase o⟩
Expand Down
2 changes: 1 addition & 1 deletion DataflowRewriter/Module.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
imod.product imod₂ ⊑_{λ a b => φ₁ a.1 b.1 ∧ φ₂ a.2 b.2} smod.product smod₂ := by stop
intro href₁ href₂
have mm_prod : MatchInterface (imod.product imod₂) (smod.product smod₂) := by apply MatchInterface_product
unfold refines_φ at *
Expand Down
29 changes: 20 additions & 9 deletions DataflowRewriter/Rewriter.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ structure Abstraction where
structure Concretisation where
expr : ExprLow Ident
typ : Ident
deriving Repr, Inhabited

structure Rewrite where
pattern : Pattern Ident
Expand Down Expand Up @@ -86,6 +87,7 @@ language does not remember any names.
let (g₁, g₂) ← ofOption (.error "could not extract graph") <| g.extract sub
let e_sub ← ofOption (.error "could not lower subgraph: graph is empty") <| g₁.lower
let g_lower := g₂.lower' e_sub
-- dbg_trace s!"e_sub:: {repr e_sub}\n\nrewrite.input_expr:: {repr rewrite.input_expr}"
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
Expand All @@ -110,8 +112,12 @@ proofs that are already present in the framework should be enough.
let (g₁, g₂) ← ofOption (.error "could not extract graph") <| g.extract sub
let e_sub ← ofOption (.error "could not lower subgraph: graph is empty") <| g₁ |>.lower
let g_lower := g₂ |>.lower' e_sub
/- 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 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⟩)

/--
Expand All @@ -131,12 +137,14 @@ are still fresh in the graph.

@[drunfold] def rewrite (fresh_prefix : String) (g : ExprHigh String) (rewrite : Rewrite String)
: RewriteResult (ExprHigh String) := do
let (g, c) ← rewrite.abstractions.foldlM (λ (g', c') a => do
let (g'', c'') ← a.run fresh_prefix g'
return (g'', c''::c')
) (g, [])
let g ← rewrite.run fresh_prefix g
c.foldlM (λ g c => c.run fresh_prefix g) g
let (g, c, _) ← rewrite.abstractions.foldlM (λ (g', c', n) a => do
let (g'', c'') ← a.run (fresh_prefix ++ s!"_A_{n}_") g'
return (g'', c''::c', n+1)
) (g, [], 0)
let g ← rewrite.run (fresh_prefix ++ s!"_R_") 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

/--
Loops over the [rewrite] function, applying one rewrite exhaustively until
Expand Down Expand Up @@ -166,18 +174,21 @@ deriving Repr
Follow an output to the next node. A similar function could be written to
follow the input to the previous node.
-/
def followOutput' (g : ExprHigh String) (inst output : String) : RewriteResult (NextNode String) := do
def followOutput' (g : ExprHigh String) (inst : String) (output : InternalPort String) : RewriteResult (NextNode String) := do
let (pmap, _) ← ofOption (.error "instance not in modules")
<| g.modules.find? inst
let localOutputName ← ofOption (.error "port not in instance portmap")
<| pmap.output.find? ⟨.top, output⟩
<| pmap.output.find? output
let c@⟨_, localInputName⟩ ← ofOption (.error "output not in connections")
<| g.connections.find? (λ c => c.output = localOutputName)
let (inst, iport) ← ofOption (.error "input port not in modules")
<| ExprHigh.findInputPort' localInputName g.modules
ofOption (.error "instance not in modules") <| (g.modules.findEntry? inst).map (λ x => ⟨inst, iport, x.2.1, x.2.2, c⟩)

def followOutput (g : ExprHigh String) (inst output : String) : Option (NextNode String) :=
(followOutput' g inst ⟨.top, output⟩).toOption

def followOutputFull (g : ExprHigh String) (inst : String) (output : InternalPort String) : Option (NextNode String) :=
(followOutput' g inst output).toOption

/--
Expand All @@ -202,7 +213,7 @@ 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
if v'.inst.isTop then return succ'
let out ← followOutput g k k'.name
let out ← followOutputFull g k k'
return succ'.push out.inst
) ∅
return succ.insert k a
Expand Down
184 changes: 182 additions & 2 deletions DataflowRewriter/Rewrites/BranchMuxToMerge.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ def lhs' : ExprHigh String := [graph|
m_right -> mux [out = "m_out", inp = "inp1"];
]

-- #eval IO.print lhs'
#eval IO.print lhs'
-- #eval IO.print lhs'.invert
#eval matcher lhs'
#eval IO.print lhs'
Expand Down Expand Up @@ -211,8 +211,188 @@ def lhs' : ExprHigh String := [graph|
m_right -> mux [out = "m_out", inp = "inp1"];
]

#eval rewrite.run "rw0_" lhs'
#eval matchModLeft lhs'
#eval matchModRight lhs'

-- #eval (Abstraction.mk matchModLeft "mod_left").run "rw0_" lhs' |>.toOption |>.get! |> Prod.fst
-- |> (Abstraction.mk matchModRight "mod_right").run "rw1_"
-- |> matchModRight
-- |> calcSucc
#eval _root_.DataflowRewriter.rewrite "rw0_" lhs' rewrite |>.toOption |>.get! |> IO.print

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")))))))))
Loading

0 comments on commit e03be27

Please sign in to comment.