Try to use simp instead of reduce

DataflowRewriter/Examples/BranchMerge.lean

@@ -53,12 +53,13 @@ section BranchMerge
   def test  TagT T (m: Σ S, StringModule S) :=
    bagged.build_module [("m", m), ("bag", ⟨_,Module.bagS (T × TagT)⟩), ("join", ⟨_,(Module.join T TagT).stringify⟩)].toAssocList
 
-  -- seal List.get List.remove in
-  -- #reallyReduce fun S TagT T input output internals =>
-  --   test TagT T ⟨S, ({ inputs := [(⟨ .top, "inp"⟩ , input)].toAssocList,
-  --                      outputs := [(⟨ .top, "out"⟩ , output)].toAssocList,
-  --                      internals := internals })⟩
-
+example y : (fun S TagT T input output internals =>
+  test TagT T ⟨S, ({ inputs := [(⟨ .top, "inp"⟩ , input)].toAssocList,
+                     outputs := [(⟨ .top, "out"⟩ , output)].toAssocList,
+                     internals := internals })⟩) = y := by
+  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.erase,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]
+  -- nearly there
+  sorry
 
 @[drunfold]
 def tagged_ooo_h : ExprHigh String :=

DataflowRewriter/ExprHigh.lean

@@ -175,7 +175,6 @@ declare_syntax_cat dot_attr
 syntax str : dot_value
 syntax num : dot_value
 syntax ident : dot_value
-syntax ("t" <|> "f") : dot_value
 
 syntax ident " = " dot_value : dot_attr
 syntax (dot_attr),* : dot_attr_list
@@ -199,14 +198,16 @@ def findStx (n : Name) (stx : Array Syntax) : Option Nat := do
       out := some (TSyntax.mk pair[2][0]).getNat
   out
 
+#check true
+
 open Lean in
 def findStxBool (n : Name) (stx : Array Syntax) : Option Bool := do
   let mut out := none
   for pair in stx do
     if pair[0].getId = n then
       out := match pair[2] with
-             | `(dot_value| true) => .some .true
-             | `(dot_value| false) => .some .false
+             | `(dot_value| true) => .some true
+             | `(dot_value| false) => .some false
              | _ => .none
   out
 

DataflowRewriter/Simp.lean

@@ -8,3 +8,35 @@ import Lean
 
 register_simp_attr dmod
 register_simp_attr drunfold
+
+-- def fromExpr? (e : Expr) : SimpM (Option String) := do
+--   return getStringValue? et
+
+open Lean Meta Simp
+
+-- simproc ↓ decideDecidable (Bool.rec _ _ c) := fun e => do
+--   let_expr f@Bool.rec _ a b c ← e | return .continue
+--   let r ← simp c
+--   return .done r
+
+-- @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM DStep := do
+--   unless e.isAppOfArity declName arity do return .continue
+--   let some n ← Expr.fromExpr? e.appFn!.appArg! | return .continue
+--   let some m ← fromExpr? e.appArg! | return .continue
+--   return .done <| toExpr (op n m)
+
+
+-- structure A where
+--   a : String
+--   b : String
+-- deriving DecidableEq
+
+-- example b : (match ({ a := "", b := "b" } : A) == { a := "", b := "c" } with
+--              | true => 1
+--              | false => 2) = b := by
+--   -- simp
+--   have : (({ a := "", b := "b" } : A) == { a := "", b := "c" }) = false := by decide
+--   unfold _example.match_1
+--   simp [_example.match_1]
+
+--   sorry