feat: Specify type in echo #55

Merged
aniva merged 5 commits from expr/echo into dev 2024-03-31 16:45:44 -07:00
5 changed files with 47 additions and 7 deletions
Showing only changes of commit 2130bcf357 - Show all commits

View File

@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
Environment.addDecl args Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get let state ← get
exprEcho args.expr args.type state.options exprEcho args.expr args.type? state.options
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get let state ← get
let options := state.options let options := state.options

View File

@ -98,7 +98,7 @@ structure StatResult where
-- Return the type of an expression -- Return the type of an expression
structure ExprEcho where structure ExprEcho where
expr: String expr: String
type: Option String type?: Option String
deriving Lean.FromJson deriving Lean.FromJson
structure ExprEchoResult where structure ExprEchoResult where
expr: Expression expr: Expression

View File

@ -24,6 +24,9 @@ def Goal.devolatilize (goal: Goal): Goal :=
deriving instance DecidableEq, Repr for Expression deriving instance DecidableEq, Repr for Expression
deriving instance DecidableEq, Repr for Variable deriving instance DecidableEq, Repr for Variable
deriving instance DecidableEq, Repr for Goal deriving instance DecidableEq, Repr for Goal
deriving instance DecidableEq, Repr for ExprEchoResult
deriving instance DecidableEq, Repr for InteractionError
deriving instance DecidableEq, Repr for Option
end Protocol end Protocol
def TacticResult.toString : TacticResult → String def TacticResult.toString : TacticResult → String
@ -38,8 +41,8 @@ def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message fa
open Lean open Lean
def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
let coreContext: Core.Context ← createCoreContext #[] let coreContext: Core.Context ← createCoreContext options
match ← (coreM.run' coreContext { env := env }).toBaseIO with match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception => | .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "") return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")

35
Test/Library.lean Normal file
View File

@ -0,0 +1,35 @@
import LSpec
import Lean
import Pantograph.Library
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Library
def test_expr_echo: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let inner: CoreM LSpec.TestSeq := do
let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
let tests := LSpec.TestSeq.done
let echoResult ← exprEcho prop_and_proof (options := {})
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
}))
let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := {})
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "(p : Prop) ×' p" }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩" }
}))
return tests
runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
def suite: IO LSpec.TestSeq := do
return LSpec.group "Library" $
(LSpec.group "ExprEcho" (← test_expr_echo))
end Pantograph.Test.Library

View File

@ -1,7 +1,8 @@
import LSpec import LSpec
import Test.Environment import Test.Environment
import Test.Metavar
import Test.Integration import Test.Integration
import Test.Library
import Test.Metavar
import Test.Proofs import Test.Proofs
import Test.Serial import Test.Serial
@ -11,11 +12,12 @@ def main := do
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
let suites := [ let suites := [
Metavar.suite, Environment.suite,
Integration.suite, Integration.suite,
Library.suite,
Metavar.suite,
Proofs.suite, Proofs.suite,
Serial.suite, Serial.suite,
Environment.suite
] ]
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
LSpec.lspecIO $ all LSpec.lspecIO $ all