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 744c9ee286
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 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 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
@ -93,11 +93,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => do | .some expr, .none => goalStartExpr expr
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
| .none, .some copyFrom => | .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with (match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .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 | .some branchId, .none => do
match state.goalStates.find? branchId with match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch | .some branch => pure $ goalContinue target branch
| .none, .some goals => | .none, .some goals =>
pure $ goalResume target goals pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" | _, _ => 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 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do 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 | .ok syn => do
match ← syntax_to_expr syn with match ← elabTerm syn with
| .error e => return .error e | .error e => return .error e
| .ok expr => pure expr | .ok expr => pure expr
| .error e => return .error e | .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 | .ok syn => do
try try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) 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) := Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem } Environment.addDecl { name, type, value, isTheorem }
/-- This must be a TermElabM since the parsed expr contains extra information -/ def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv 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 | .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn | .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 | .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr | .ok expr => return .ok expr
@[export pantograph_expr_echo_m] @[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 Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
let termElabM: Lean.Elab.TermElabM _ := 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 | .error e => return .error e
| .ok expr => pure expr | .ok expr => pure expr
try try
@ -139,7 +152,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
@[export pantograph_goal_start_expr_m] @[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with let expr ← match ← parseElabType expr with
| .error e => return .error e | .error e => return .error e
| .ok expr => pure $ expr | .ok expr => pure $ expr
return .ok $ ← GoalState.create expr return .ok $ ← GoalState.create expr

View File

@ -98,6 +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
deriving Lean.FromJson deriving Lean.FromJson
structure ExprEchoResult where structure ExprEchoResult where
expr: Expression expr: Expression

View File

@ -21,23 +21,22 @@ def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
--- Input Functions --- --- Input Functions ---
/-- Read syntax object from string -/ /-- 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 Parser.runParserCategory
(env := env) (env := env)
(catName := `term) (catName := `term)
(input := s) (input := s)
(fileName := "<stdin>") (fileName := "<stdin>")
/-- Parse a syntax object. May generate additional metavariables! -/ /-- 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 try
let expr ← Elab.Term.elabType syn let expr ← Elab.Term.elabType syn
return .ok expr return .ok expr
catch ex => return .error (← ex.toMessageData.toString) 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 try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none) let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
return .ok expr return .ok expr
catch ex => return .error (← ex.toMessageData.toString) 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. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees - `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.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 - `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 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 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}" = "")

View File

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

View File

@ -17,12 +17,12 @@ def addTest (test: LSpec.TestSeq): TestM Unit := do
def test_instantiate_mvar: TestM Unit := do def test_instantiate_mvar: TestM Unit := do
let env ← Lean.MonadEnv.getEnv 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 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 | .ok s => pure $ s
| .error e => do | .error e => do
addTest $ assertUnreachable e addTest $ assertUnreachable e
return () return ()
let expr ← match ← syntax_to_expr syn with let expr ← match ← elabTerm syn with
| .ok expr => pure $ expr | .ok expr => pure $ expr
| .error e => do | .error e => do
addTest $ assertUnreachable e addTest $ assertUnreachable e
@ -36,14 +36,14 @@ def test_instantiate_mvar: TestM Unit := do
def startProof (expr: String): TestM (Option GoalState) := do def startProof (expr: String): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv 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) addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with match syn? with
| .error error => | .error error =>
IO.println error IO.println error
return Option.none return Option.none
| .ok syn => | .ok syn =>
let expr? ← syntax_to_expr_type syn let expr? ← elabType syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with match expr? with
| .error error => | .error error =>

View File

@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
| .none => | .none =>
return Option.none return Option.none
| .expr expr => | .expr expr =>
let syn? := syntax_from_str env expr let syn? := parseTerm env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk) addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with match syn? with
| .error error => | .error error =>
IO.println error IO.println error
return Option.none return Option.none
| .ok syn => | .ok syn =>
let expr? ← syntax_to_expr_type syn let expr? ← elabType syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with match expr? with
| .error error => | .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 termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let s := syntax_from_str env source |>.toOption |>.get! let s := parseTerm env source |>.toOption |>.get!
let expr := (← syntax_to_expr s) |>.toOption |>.get! let expr := (← elabTerm s) |>.toOption |>.get!
let test := LSpec.check source ((← serialize_expression_ast expr) = target) let test := LSpec.check source ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let metaM := termElabM.run' (ctx := defaultTermElabMContext) 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 metaM: MetaM LSpec.TestSeq := do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y" 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 s := parseTerm env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get! let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
return LSpec.TestSeq.done return LSpec.TestSeq.done
runMetaMSeq env metaM runMetaMSeq env metaM