Work on simplifying the rewriter for proofs

DataflowRewriter/Module.lean

@@ -691,7 +691,7 @@ theorem refines_refines' :
   rcases href with ⟨mm, R, href⟩
   refine ⟨mm, fun x y => imod.indistinguishable smod x y ∧ R x y, ?_, ?_⟩
   · assumption
-  · simp (config := {contextual := true})
+  · simp +contextual
 
 theorem refines'_refines :
   imod ⊑' smod →

DataflowRewriter/Rewriter.lean

@@ -118,10 +118,11 @@ language does not remember any names.
 
   -- We then rename all internal signals in the new expression with the fresh
   -- names.
-  let e_renamed_sub' := e_sub'.renameMapped int_mapping'
+  let e_renamed_output_sub := e_sub_output.renamePorts int_mapping'
+  let e_renamed_input_sub := e_sub_input.renamePorts int_mapping'
 
   -- Finally we do the actual replacement.
-  return g_lower.replace e_sub e_renamed_sub' |>.higherS fresh_prefix
+  return g_lower.replace e_renamed_input_sub e_renamed_output_sub |>.higherS fresh_prefix
 
 /--
 Abstract a subgraph into a separate node.  One can imagine that the node type is
@@ -143,7 +144,7 @@ proofs that are already present in the framework should be enough.
   comes in the second phase. -/
   let portMapping := e_sub.build_interface.toIdentityPortMapping' -- abstraction.typ
   let abstracted := g_lower.abstract e_sub portMapping abstraction.typ
-  let e_sub' := e_sub.renameMapped portMapping.inverse
+  let e_sub' := e_sub.renamePorts portMapping.inverse
   -- let portMapping := e_sub.build_interface.toIdentityPortMapping -- abstraction.typ
   -- let abstracted := g_lower.abstract e_sub portMapping abstraction.typ
   -- let e_sub' := e_sub
@@ -164,7 +165,7 @@ are still fresh in the graph.
     <| g_lower.findBase concretisation.typ
   -- return g_lower.concretise (concretisation.expr.renameMapped base) base concretisation.typ
   --        |>.higherS fresh_prefix
-  let e_sub := concretisation.expr.renameMapped base
+  let e_sub := concretisation.expr.renamePorts base
   return g_lower.concretise e_sub base concretisation.typ |>.higherS fresh_prefix
 
 @[drunfold] def Rewrite.run (fresh_prefix : String) (g : ExprHigh String) (rewrite : Rewrite String)

DataflowRewriter/Rewrites/BranchMuxToMerge.lean

@@ -199,7 +199,7 @@ def lhs' : ExprHigh String := [graph|
     branch [type = "TaggedBranch"];
     m_left1 [type = "mod_left1"];
     m_left2 [type = "mod_left2"];
-    m_right [type = "mod_right"];
+    m_right [type = "mod_right2"];
     mux [type = "TaggedMux"];
     fork [type = "TaggedFork"];
     bag [type = "Bag"];

lake-manifest.json

@@ -1,95 +1,105 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/VCA-EPFL/leanses",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6c99a8cfb3315f13cfcf55acf1b633fba45bc3dd",
+   "rev": "3894c72cbd6f4baba45c79678e75503123a51756",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing-2024-11-11",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/VCA-EPFL/leanses",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "292be522616364e3315c48ebf22977f131ccbfd9",
    "name": "leanses",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b8b985f203e1f2f590e3ce46b50d722cc2ba8692",
-   "name": "batteries",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41",
-   "name": "Qq",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
-   "name": "aesop",
+   "rev": "5ee6767b2157766c8aa451bb93d1434436e593a2",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cd20dae87c48495f0220663014dff11671597fcf",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.43-pre",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "10001e92eb91fd0d186f10b8a396a98836c97f2a",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
-   "name": "importGraph",
+   "rev": "2adf619a966509c4e2fe129787f4b1e89601ce64",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
-   "name": "LeanSearchClient",
+   "rev": "433429762eb5e9efb6420292b1a4be97b47cd75b",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "5c179825b962cca3ba1fae66444dea32a12de3f2",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-10-10",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "«dataflow-rewriter»",
  "lakeDir": ".lake"}

lakefile.toml

@@ -22,7 +22,7 @@ rev = "main"
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-10-10"
+rev = "nightly-testing-2024-11-11"
 
 [[lean_lib]]
 name = "DataflowRewriter"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-10
+leanprover/lean4:nightly-2024-11-11