test(frontend): Add scope `open` test

This commit is contained in:
Leni Aniva 2025-03-09 23:29:33 -07:00
parent 1dceb5428e
commit 0cfd73e44e
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 20 additions and 2 deletions

View File

@ -40,6 +40,7 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
abbrev FrontendM := Elab.Frontend.FrontendM
structure CompilationStep where
scope : Elab.Command.Scope
fileName : String
fileMap : FileMap
src : Substring
@ -74,7 +75,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
let msgs := s'.messages.toList.drop s.messages.toList.length
let trees := s'.infoState.trees.drop s.infoState.trees.size
let ⟨_, fileName, fileMap⟩ := (← read).inputCtx
return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done)
partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
let (cmd, done) ← processOneCommand

View File

@ -1,11 +1,27 @@
import LSpec
import Pantograph
import Repl
import Test.Common
import LSpec
open Lean Pantograph
namespace Pantograph.Test.Frontend
def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do
let filename := "<anonymous>"
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
let m := Frontend.mapCompilationSteps f
m.run context |>.run' state
def test_open : TestT MetaM Unit := do
let sketch := "
open Nat
example : ∀ (n m: Nat), n + m = m + n := by
apply add_comm
"
let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString)
checkEq "errors" errors [[]]
def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
: MetaM (List GoalState) := do
let filename := "<anonymous>"
@ -233,6 +249,7 @@ theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get
def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
let tests := [
("open", test_open),
("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
("sorry_in_middle", test_sorry_in_middle),
("sorry_in_induction", test_sorry_in_induction),