Merge pull request 'feat: Specify type in echo' (#55) from expr/echo into dev

Reviewed-on: #55
This commit is contained in:
Leni Aniva 2024-03-31 16:45:43 -07:00
commit 2511573a82
13 changed files with 94 additions and 45 deletions

View File

@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get
exprEcho args.expr state.options
exprEcho args.expr args.type? state.options
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get
let options := state.options
@ -93,11 +93,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
| .some expr, .none => goalStartExpr expr
| .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@ -152,7 +148,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .some branchId, .none => do
match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .some branch => pure $ goalContinue target branch
| .none, .some goals =>
pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"

View File

@ -98,13 +98,13 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
let type ← match syntax_from_str env args.type with
let type ← match parseTerm env args.type with
| .ok syn => do
match ← syntax_to_expr syn with
match ← elabTerm syn with
| .error e => return .error e
| .ok expr => pure expr
| .error e => return .error e
let value ← match syntax_from_str env args.value with
let value ← match parseTerm env args.value with
| .ok syn => do
try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)

View File

@ -109,21 +109,34 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem }
/-- This must be a TermElabM since the parsed expr contains extra information -/
def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv
let syn ← match syntax_from_str env s with
let syn ← match parseTerm env type with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← syntax_to_expr syn with
match ← elabType syn with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr
/-- This must be a TermElabM since the parsed expr contains extra information -/
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv
let expectedType? ← match ← expectedType?.mapM parseElabType with
| .none => pure $ .none
| .some (.ok t) => pure $ .some t
| .some (.error e) => return .error e
let syn ← match parseTerm env expr with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← elabTerm syn expectedType? with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr
@[export pantograph_expr_echo_m]
def exprEcho (expr: String) (options: @&Protocol.Options):
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
let expr ← match ← parseElabExpr expr expectedType? with
| .error e => return .error e
| .ok expr => pure expr
try
@ -139,7 +152,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
@[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
let expr ← match ← parseElabType expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr

View File

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

View File

@ -21,23 +21,22 @@ def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
--- Input Functions ---
/-- Read syntax object from string -/
def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
def parseTerm (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory
(env := env)
(catName := `term)
(input := s)
(fileName := "<stdin>")
/-- Parse a syntax object. May generate additional metavariables! -/
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try
let expr ← Elab.Term.elabType syn
return .ok expr
catch ex => return .error (← ex.toMessageData.toString)
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
return .ok expr
catch ex => return .error (← ex.toMessageData.toString)

View File

@ -72,7 +72,7 @@ where the application of `assumption` should lead to a failure.
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
- `expr.echo {"expr": <expr>, "type": <optional expected type>}`: Determine the type of an expression and round-trip it
- `env.catalog`: Display a list of all safe Lean symbols in the current environment
- `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default

View File

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

View File

@ -73,22 +73,22 @@ def test_malformed_command : IO LSpec.TestSeq :=
]
def test_tactic : IO LSpec.TestSeq :=
let goal1: Protocol.Goal := {
name := "_uniq.10",
name := "_uniq.11",
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.13",
name := "_uniq.14",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [
subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p q → q p")]
(Lean.toJson ({stateId := 0, root := "_uniq.8"}:
(Lean.toJson ({stateId := 0, root := "_uniq.9"}:
Protocol.GoalStartResult)),
subroutine_step "goal.tactic"
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
@ -100,7 +100,7 @@ def test_tactic : IO LSpec.TestSeq :=
subroutine_step "goal.print"
[("stateId", .num 1)]
(Lean.toJson ({
parent? := .some { pp? := .some "fun x => ?m.11 x" },
parent? := .some { pp? := .some "fun x => ?m.12 x" },
}:
Protocol.GoalPrintResult)),
subroutine_step "goal.tactic"

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

View File

@ -17,12 +17,12 @@ def addTest (test: LSpec.TestSeq): TestM Unit := do
def test_instantiate_mvar: TestM Unit := do
let env ← Lean.MonadEnv.getEnv
let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
let syn ← match syntax_from_str env value with
let syn ← match parseTerm env value with
| .ok s => pure $ s
| .error e => do
addTest $ assertUnreachable e
return ()
let expr ← match ← syntax_to_expr syn with
let expr ← match ← elabTerm syn with
| .ok expr => pure $ expr
| .error e => do
addTest $ assertUnreachable e
@ -36,14 +36,14 @@ def test_instantiate_mvar: TestM Unit := do
def startProof (expr: String): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
let syn? := syntax_from_str env expr
let syn? := parseTerm env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← syntax_to_expr_type syn
let expr? ← elabType syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>

View File

@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
| .none =>
return Option.none
| .expr expr =>
let syn? := syntax_from_str env expr
let syn? := parseTerm env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← syntax_to_expr_type syn
let expr? ← elabType syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>

View File

@ -55,8 +55,8 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
]
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
let env ← MonadEnv.getEnv
let s := syntax_from_str env source |>.toOption |>.get!
let expr := (← syntax_to_expr s) |>.toOption |>.get!
let s := parseTerm env source |>.toOption |>.get!
let expr := (← elabTerm s) |>.toOption |>.get!
let test := LSpec.check source ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
@ -67,8 +67,8 @@ def test_instance (env: Environment): IO LSpec.TestSeq := do
let metaM: MetaM LSpec.TestSeq := do
let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
let s := syntax_from_str env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
let s := parseTerm env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
return LSpec.TestSeq.done
runMetaMSeq env metaM