max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: basic compiler tests for findJoinPoints

Browse source
This commit is contained in:
Henrik Böving 2022-09-07 21:24:04 +02:00 • committed by Leonardo de Moura
parent f912349a29
commit 576a4ec2c5
2 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
tests/lean/CompilerFindJoinPoints.lean Normal file
View file

@ -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]

5
tests/lean/CompilerFindJoinPoints.lean.expected.out Normal file
View file

@ -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