Skip to content

Commit

Permalink
Fix reduction and type checking for the last time
Browse files Browse the repository at this point in the history
  • Loading branch information
@ymherklotz
ymherklotz committed Oct 29, 2024
1 parent 38bc42e commit dd01af2
Showing 1 changed file with 16 additions and 21 deletions.
37 changes: 16 additions & 21 deletions DataflowRewriter/Examples/BranchMerge.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,13 +40,13 @@ section BranchMerge
bags [mod="bag"];
joiner [mod="join"];
-- Producing the tagged values
m -> joiner [out="out", inp="inp0"];
m -> joiner [out="out", inp="inp1"];
-- Push into the bag
joiner -> bags [out = "out0", inp = "enq"];
-- Connecting with the exporting interface
bags -> deq [out="deq"];
enq -> m [inp ="inp"];
enqT -> joiner [inp="inp1"];
enqT -> joiner [inp="inp0"];
]

#reduce bagged
Expand All @@ -55,22 +55,20 @@ section BranchMerge
def test TagT T S input output internals :=
bagged.build_module [("m", ⟨S, ({ inputs := [(⟨ .top, "inp"⟩ , input)].toAssocList,
outputs := [(⟨ .top, "out"⟩ , output)].toAssocList,
internals := internals })⟩), ("bag", ⟨_,StringModule.bagS (T × TagT)⟩), ("join", ⟨_,(NatModule.join T TagT).stringify⟩)].toAssocList
internals := internals })⟩), ("bag", ⟨_,StringModule.bagS (TagT × T)⟩), ("join", ⟨_,(NatModule.join TagT T).stringify⟩)].toAssocList

#check test

def test2 (TagT T S : Type) (input output : (T : Type) × (S → T → S → Prop))
(internals : List (S → S → Prop)) : (T : Type) × Module String T := by
precomputeTac test TagT T S input output internals by
unfold test
dsimp only [test,drunfold,seval,Batteries.AssocList.toList,bagged,Function.uncurry,Module.mapIdent,List.toAssocList,List.foldl,Batteries.AssocList.find?,Option.pure_def,Option.bind_eq_bind,Option.bind_some,Module.renamePorts,Batteries.AssocList.mapKey,InternalPort.map,toString,Nat.repr,Nat.toDigits,Nat.toDigitsCore,Nat.digitChar,List.asString,Option.bind,Batteries.AssocList.mapVal,Batteries.AssocList.eraseAll,Batteries.AssocList.eraseAllP,beq_self_eq_true,Option.getD,cond,beq_self_eq_true, beq_iff_eq, InternalPort.mk.injEq, String.reduceEq, and_false, imp_self,BEq.beq]
simp (config := {decide := true,maxSteps := 10000000}) only [seval,InternalPort.mk.injEq, and_false, decide_False, decide_True, and_true]
conv in Module.connect'' _ _ => rw [Module.connect''_dep_rw]; rfl
conv in _ :: Module.connect'' _ _ :: _ => arg 2; rw [Module.connect''_dep_rw]; rfl
unfold Module.connect''
dsimp


#print test2

-- TODO: Remove join here
Expand All @@ -81,40 +79,37 @@ def tagged_ooo_h : ExprHigh String :=
deq [mod="io"];

tagger [mod="tag"];
bagged [mod="bag"];
join [mod="join"];
bagged [mod="baggedModule"];

-- Match tag and input
-- Top-level inputs: The second input to join which is unbound
tagger -> join [out = "out0", inp = "inp1"];
enq -> join [out = "enq", inp = "inp0"];

-- Feed the pair to the bag
join -> bagged [out = "out0", inp = "enq"];
tagger -> bagged [out = "out0", inp = "enqT"];
enq -> bagged [inp = "enq"];

-- Output of the bag complete inside the tagger
bagged -> tagger [out = "deq", inp = "inp0"];

-- Top-level outputs: Second output of the tagger, the untagged value which is unbound
tagger -> deq [out = "out1", inp = "deq"];
tagger -> deq [out = "out1"];
]

def test3 TagT [h: DecidableEq TagT] T (m: Σ S, StringModule S) :=
tagged_ooo_h.build_module [("m", m), ("tag", ⟨_,(NatModule.tag_complete_spec TagT T).stringify⟩),("bag", ⟨_,StringModule.bagS (T × TagT)⟩), ("join", ⟨_,(NatModule.join T TagT).stringify⟩)].toAssocList
def test3 TagT [h: DecidableEq TagT] T S input output internals :=
tagged_ooo_h.build_module [("baggedModule", (test2 TagT T S input output internals)), ("tag", ⟨_,(NatModule.tag_complete_spec TagT T).stringify⟩),("bag", ⟨_,StringModule.bagS (T × TagT)⟩), ("join", ⟨_,(NatModule.join T TagT).stringify⟩)].toAssocList

#reallyReduce test3

def test4 TagT [h: DecidableEq TagT] (T : Type) (m: Σ S, StringModule S)
: (T : Type) × Module String T := by precomputeTac test3 TagT T m by
dsimp only [test3,drunfold,seval,Batteries.AssocList.toList,bagged,Function.uncurry,Module.mapIdent,List.toAssocList,List.foldl,Batteries.AssocList.find?,Option.pure_def,Option.bind_eq_bind,Option.bind_some,Module.renamePorts,Batteries.AssocList.mapKey,InternalPort.map,toString,Nat.repr,Nat.toDigits,Nat.toDigitsCore,Nat.digitChar,List.asString,Option.bind,Batteries.AssocList.mapVal,Batteries.AssocList.eraseAll,Batteries.AssocList.eraseP,beq_self_eq_true,Option.getD,cond,beq_self_eq_true, beq_iff_eq, InternalPort.mk.injEq, String.reduceEq, and_false, imp_self,BEq.beq]

def test4 (TagT T S : Type) [h:DecidableEq TagT] (input output : (T : Type) × (S → T → S → Prop))
(internals : List (S → S → Prop))
: (T : Type) × Module String T := by precomputeTac @test3 TagT h T S input output internals by
dsimp only [test3,test2,drunfold,seval,Batteries.AssocList.toList,bagged,Function.uncurry,Module.mapIdent,List.toAssocList,List.foldl,Batteries.AssocList.find?,Option.pure_def,Option.bind_eq_bind,Option.bind_some,Module.renamePorts,Batteries.AssocList.mapKey,InternalPort.map,toString,Nat.repr,Nat.toDigits,Nat.toDigitsCore,Nat.digitChar,List.asString,Option.bind,Batteries.AssocList.mapVal,Batteries.AssocList.eraseAll,Batteries.AssocList.eraseP,beq_self_eq_true,Option.getD,cond,beq_self_eq_true, beq_iff_eq, InternalPort.mk.injEq, String.reduceEq, and_false, imp_self,BEq.beq]
simp (config := {decide := true,maxSteps := 10000000,ground := true,autoUnfold := true}) only [seval,InternalPort.mk.injEq, and_false, decide_False, decide_True, and_true]
set_option pp.piBinderTypes true in set_option pp.letVarTypes true in set_option pp.structureInstances false in set_option pp.fieldNotation false in set_option pp.funBinderTypes true in set_option pp.explicit true in set_option pp.deepTerms true in set_option pp.maxSteps 1000000000 in trace_state
conv in Module.connect'' _ _ => rw [Module.connect''_dep_rw]; rfl
conv in _ :: Module.connect'' _ _ :: _ => arg 2; rw [Module.connect''_dep_rw]; rfl
conv in _ :: Module.connect'' _ _ :: _ => arg 2; arg 2; rw [Module.connect''_dep_rw]; rfl
-- conv in _ :: Module.connect'' _ _ :: _ => arg 2; arg 2; rw [Module.connect''_dep_rw]; rfl
unfold Module.connect''
dsimp


end BranchMerge

end DataflowRewriter

0 comments on commit dd01af2

Please sign in to comment.