From 42133f9b7469bdf93c1b5f17edcb640d50baaefb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Oct 2023 17:31:36 -0700 Subject: [PATCH] Add holes test stub Move tests into their own namespaces --- Test/Holes.lean | 101 ++++++++++++++++++++++++++++++++++++++++++ Test/Integration.lean | 6 +-- Test/Main.lean | 8 ++-- Test/Proofs.lean | 8 ++-- Test/Serial.lean | 8 ++-- 5 files changed, 117 insertions(+), 14 deletions(-) create mode 100644 Test/Holes.lean diff --git a/Test/Holes.lean b/Test/Holes.lean new file mode 100644 index 0000000..8935ea9 --- /dev/null +++ b/Test/Holes.lean @@ -0,0 +1,101 @@ +import LSpec +import Pantograph.Tactic +import Pantograph.Serial + +namespace Pantograph.Test.Holes +open Pantograph +open Lean + +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M) + +deriving instance DecidableEq, Repr for Commands.Expression +deriving instance DecidableEq, Repr for Commands.Variable +deriving instance DecidableEq, Repr for Commands.Goal + +def add_test (test: LSpec.TestSeq): TestM Unit := do + set $ (← get) ++ test + +def start_goal (hole: String): TestM (Option GoalState) := do + let env ← Lean.MonadEnv.getEnv + let syn? := syntax_from_str env hole + add_test $ LSpec.check s!"Parsing {hole}" (syn?.isOk) + match syn? with + | .error error => + IO.println error + return Option.none + | .ok syn => + let expr? ← syntax_to_expr syn + add_test $ LSpec.check s!"Elaborating" expr?.isOk + match expr? with + | .error error => + IO.println error + return Option.none + | .ok expr => + let goal ← GoalState.create (expr := expr) + return Option.some goal + +def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false + +def build_goal (nameType: List (String × String)) (target: String): Commands.Goal := + { + target := { pp? := .some target}, + vars := (nameType.map fun x => ({ + name := x.fst, + type? := .some { pp? := .some x.snd }, + isInaccessible? := .some false + })).toArray + } +-- Like `build_goal` but allow certain variables to be elided. +def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal := + { + target := { pp? := .some target}, + vars := (nameType.map fun x => ({ + name := x.fst, + type? := x.snd.map (λ type => { pp? := type }), + isInaccessible? := x.snd.map (λ _ => false) + })).toArray + } + +def construct_sigma: TestM Unit := do + let goal? ← start_goal "∀ (n m: Nat), n + m = m + n" + add_test $ LSpec.check "Start goal" goal?.isSome + if let .some goal := goal? then + return () + + +def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do + let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options + + let coreContext: Lean.Core.Context := { + currNamespace := str_to_name "Aniva", + openDecls := [], -- No 'open' directives needed + fileName := "", + fileMap := { source := "", positions := #[0], lines := #[1] } + } + let metaM := termElabM.run' (ctx := { + declName? := some "_pantograph", + errToSorry := false + }) + let coreM := metaM.run' + match ← (coreM.run' coreContext { env := env }).toBaseIO with + | .error exception => + return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "") + | .ok (_, a) => + return a + +def suite: IO LSpec.TestSeq := do + let env: Lean.Environment ← Lean.importModules + (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) + (opts := {}) + (trustLevel := 1) + let tests := [ + ("Σ'", construct_sigma) + ] + let tests ← tests.foldlM (fun acc tests => do + let (name, tests) := tests + let tests ← proof_runner env tests + return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done + + return LSpec.group "Holes" tests + +end Pantograph.Test.Holes diff --git a/Test/Integration.lean b/Test/Integration.lean index 6caaf90..5dbb80a 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -2,7 +2,7 @@ -/ import LSpec import Pantograph -namespace Pantograph.Test +namespace Pantograph.Test.Integration open Pantograph def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json)) @@ -83,11 +83,11 @@ def test_malformed_command : IO LSpec.TestSeq := Commands.InteractionError)) ] -def test_integration: IO LSpec.TestSeq := do +def suite: IO LSpec.TestSeq := do return LSpec.group "Integration" $ (LSpec.group "Option modify" (← test_option_modify)) ++ (LSpec.group "Malformed command" (← test_malformed_command)) -end Pantograph.Test +end Pantograph.Test.Integration diff --git a/Test/Main.lean b/Test/Main.lean index 84d686d..cb7c055 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,4 +1,5 @@ import LSpec +import Test.Holes import Test.Integration import Test.Proofs import Test.Serial @@ -10,9 +11,10 @@ unsafe def main := do Lean.initSearchPath (← Lean.findSysroot) let suites := [ - test_integration, - test_proofs, - test_serial + Holes.suite, + Integration.suite, + Proofs.suite, + Serial.suite ] let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done LSpec.lspecIO $ all diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a6d08e7..c9daf84 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -2,7 +2,7 @@ import LSpec import Pantograph.Tactic import Pantograph.Serial -namespace Pantograph.Test +namespace Pantograph.Test.Proofs open Pantograph open Lean @@ -229,7 +229,8 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq : | .ok (_, a) => return a -def test_proofs : IO LSpec.TestSeq := do +/-- Tests the most basic form of proofs whose goals do not relate to each other -/ +def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (opts := {}) @@ -248,5 +249,4 @@ def test_proofs : IO LSpec.TestSeq := do return LSpec.group "Proofs" tests -end Pantograph.Test - +end Pantograph.Test.Proofs diff --git a/Test/Serial.lean b/Test/Serial.lean index 058ba04..e135c0c 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -2,7 +2,7 @@ import LSpec import Pantograph.Serial import Pantograph.Symbols -namespace Pantograph.Test +namespace Pantograph.Test.Serial open Pantograph open Lean @@ -62,15 +62,15 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do | .ok a => return a -def test_serial: IO LSpec.TestSeq := do +def suite: IO LSpec.TestSeq := do let env: Environment ← importModules (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (opts := {}) (trustLevel := 1) - return LSpec.group "Serialisation" $ + return LSpec.group "Serialization" $ (LSpec.group "str_to_name" test_str_to_name) ++ (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++ (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) -end Pantograph.Test +end Pantograph.Test.Serial