diff --git a/src/Examples.thy b/src/Examples.thy index 7d50921..3b42376 100644 --- a/src/Examples.thy +++ b/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 diff --git a/src/Model.thy b/src/Model.thy index 10c3c8c..0d018ff 100644 --- a/src/Model.thy +++ b/src/Model.thy @@ -57,7 +57,7 @@ fun fold_binary :: "operator \ expression \ expression \ fun fold_cond :: "expression \ expression \ expression \ 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 \ expression" where "optimise (Binary op a b) = fold_binary op (optimise a) (optimise b)" diff --git a/tests/native.py b/tests/native.py index 5e34c94..7de6b68 100644 --- a/tests/native.py +++ 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)]