perf(optimiser): collapse conditionals with identical branches

src/Examples.thy

@@ -47,6 +47,10 @@ lemma dead_branch:
   "optimise (Cond (Literal 0) (Input X) (Input Y)) = Input Y"
   by eval
 
+lemma equal_branches:
+  "optimise (Cond (Input T) (Input X) (Input X)) = Input X"
+  by eval
+
 lemma literal_code:
   "executable (Literal 42) = [72,184,42,0,0,0,0,0,0,0,80,88,195]"
   by eval

src/Model.thy

@@ -57,7 +57,7 @@ fun fold_binary :: "operator \<Rightarrow> expression \<Rightarrow> expression \
 
 fun fold_cond :: "expression \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
   "fold_cond (Literal c) a b = (if c = 0 then b else a)"
-| "fold_cond c a b = Cond c a b"
+| "fold_cond c a b = (if a = b then a else Cond c a b)"
 
 fun optimise :: "expression \<Rightarrow> expression" where
   "optimise (Binary op a b) = fold_binary op (optimise a) (optimise b)"

tests/native.py

@@ -68,6 +68,7 @@ def main():
     cases += [(op, "x", 0) for op in ("+", "-", "or", "xor", "shl", "shr")]
     cases += [("*", "x", 1), ("*", 1, "x"), ("and", "x", MASK)]
     cases += [("*", "x", 0), ("and", "x", 0), ("shl", 0, "y"), ("shr", 0, "y"), ("or", "x", MASK)]
+    cases += [("if", "x", ("+", "y", "t"), ("+", "y", "t"))]
     cases += [("let", "a", ("+", "x", 3), ("+", "y", ("let", "b", "t", ("*", "a", "b")))),
               ("let", "x", "y", ("if", "t", ("+", "x", 1), ("-", "x", 1)))]
     cases += [generate(rng, 5, ["x", "y", "t"]) for _ in range(117)]