Skip to content

Commit

Permalink
Simplify the followOutput function
Browse files Browse the repository at this point in the history
  • Loading branch information
ymherklotz committed Oct 31, 2024
1 parent 56c41f8 commit 5b211bd
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 8 deletions.
5 changes: 4 additions & 1 deletion DataflowRewriter/Rewriter.lean
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ structure NextNode (Ident) where
typ : Ident
connection : Connection Ident

def followOutput (g : ExprHigh String) (inst output : String) : RewriteResult (NextNode String) := do
def followOutput' (g : ExprHigh String) (inst output : 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")
Expand All @@ -97,4 +97,7 @@ def followOutput (g : ExprHigh String) (inst output : String) : RewriteResult (N
<| 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 output).toOption

end DataflowRewriter
13 changes: 6 additions & 7 deletions DataflowRewriter/Rewrites/MergeRewrite.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,16 @@ import DataflowRewriter.ExprHighElaborator

namespace DataflowRewriter.MergeRewrite

/--
The matcher takes in a dot graph and should return the cluster of nodes that
form the subgraph as a list of instance names.
-/
def matcher (g : ExprHigh String) : RewriteResult (List String) := do
let (.some list) ← g.modules.foldlM (λ nodes inst (pmap, typ) => do
if nodes.isSome then return nodes
unless typ = "merge" do return none
let nn ←
try followOutput g inst "out0"
catch
| .error s => return none
| .done => throw .done
unless nn.typ = "merge" do return none
unless nn.inputPort = "inp0" do return none
let (.some nn) := followOutput g inst "out0" | return none
unless nn.typ = "merge" && nn.inputPort = "inp0" do return none
return some [inst, nn.inst]
) none | throw .done
return list
Expand Down

0 comments on commit 5b211bd

Please sign in to comment.