From 576a4ec2c5a8ce8ced830c606fa313e019f88e3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Sep 2022 21:24:04 +0200 Subject: [PATCH] test: basic compiler tests for findJoinPoints --- tests/lean/CompilerFindJoinPoints.lean | 19 +++++++++++++++++++ .../CompilerFindJoinPoints.lean.expected.out | 5 +++++ 2 files changed, 24 insertions(+) create mode 100644 tests/lean/CompilerFindJoinPoints.lean create mode 100644 tests/lean/CompilerFindJoinPoints.lean.expected.out 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