diff --git a/tests/lean/CompilerFindJoinPoints.lean b/tests/lean/CompilerFindJoinPoints.lean new file mode 100644 index 0000000000..af4129a0cf --- /dev/null +++ b/tests/lean/CompilerFindJoinPoints.lean @@ -0,0 +1,19 @@ +import Lean.Compiler.Main +import Lean.Compiler.LCNF.Testing +import Lean.Elab.Do + +open Lean +open Lean.Compiler.LCNF + +-- Run compilation twice to avoid the output caused by the inliner +#eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] + +@[cpass] +def findJoinPointFixTest : PassInstaller := Testing.assertIsAtFixPoint `findJoinPoints + +@[cpass] +def cseSizeTest : PassInstaller := + Testing.assertReducesOrPreservesSize `findJoinPoints `findJoinPointsSizeLeq "findJoinPoints increased size of declaration" + +set_option trace.Compiler.test true in +#eval Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo] diff --git a/tests/lean/CompilerFindJoinPoints.lean.expected.out b/tests/lean/CompilerFindJoinPoints.lean.expected.out new file mode 100644 index 0000000000..1644479746 --- /dev/null +++ b/tests/lean/CompilerFindJoinPoints.lean.expected.out @@ -0,0 +1,5 @@ + +[Compiler.test] Starting condition test findJoinPointsSizeLeq for findJoinPoints +[Compiler.test] Condition test findJoinPointsSizeLeq for findJoinPoints successful +[Compiler.test] Running fixpoint test for findJoinPoints +[Compiler.test] Fixpoint test for findJoinPoints successful