From 65ac0d5c5821bd4a5e65a7d7ff57eee9ba690249 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 31 Mar 2024 15:55:08 -0700 Subject: [PATCH 1/5] feat: Specify type in echo --- Pantograph.lean | 2 +- Pantograph/Environment.lean | 6 +++--- Pantograph/Library.lean | 25 +++++++++++++++++++------ Pantograph/Protocol.lean | 1 + Pantograph/Serial.lean | 9 ++++----- Test/Metavar.lean | 8 ++++---- Test/Proofs.lean | 4 ++-- Test/Serial.lean | 8 ++++---- 8 files changed, 38 insertions(+), 25 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index bcf8395..075a7f6 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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 diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 19c3249..f00e857 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -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) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index f44fcad..d2bc8a0 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -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 typeParse (typeParse: 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 typeParse 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 exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do + let env ← Lean.MonadEnv.getEnv + let expectedType? ← match ← expectedType?.mapM typeParse with + | .none => pure $ .none + | .some (.ok t) => pure $ .some t + | .some (.error e) => return .error e + let syn ← match parseTerm env exprStr 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 ← exprParse expr expectedType? with | .error e => return .error e | .ok expr => pure expr try diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index cd42ab8..7a2b341 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index f829611..2eb09c6 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -25,23 +25,22 @@ def instantiateAll (e: Lean.Expr) : Lean.MetaM 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 := "") - /-- 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) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 9820dde..9595b35 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -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 => diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 833c02e..133eee0 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -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 => diff --git a/Test/Serial.lean b/Test/Serial.lean index c2810c8..f186bbb 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -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 From 52d3283b5c472d7a61b39797bd83567951d21c13 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 31 Mar 2024 16:06:30 -0700 Subject: [PATCH 2/5] refactor: Use library goalStartExpr function --- Pantograph.lean | 6 +----- Pantograph/Library.lean | 2 +- Test/Integration.lean | 14 +++++++------- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 075a7f6..18f8e27 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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}" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index d2bc8a0..56b8edb 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -152,7 +152,7 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (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 ← typeParse expr with | .error e => return .error e | .ok expr => pure $ expr return .ok $ ← GoalState.create expr diff --git a/Test/Integration.lean b/Test/Integration.lean index 92c5007..5f2523b 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -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" From 7283c5c9709aa9fc1439c1125f5fe0faab430ebc Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 31 Mar 2024 16:11:41 -0700 Subject: [PATCH 3/5] refactor: Use library functions when possible --- Pantograph.lean | 2 +- Pantograph/Library.lean | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 18f8e27..1def945 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -148,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" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 56b8edb..d5652de 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -109,9 +109,9 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := Environment.addDecl { name, type, value, isTheorem } -def typeParse (typeParse: 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 parseTerm env typeParse with + let syn ← match parseTerm env type with | .error str => return .error $ errorI "parsing" str | .ok syn => pure syn match ← elabType syn with @@ -119,13 +119,13 @@ def typeParse (typeParse: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) : | .ok expr => return .ok expr /-- This must be a TermElabM since the parsed expr contains extra information -/ -def exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do +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 typeParse with + 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 exprStr with + let syn ← match parseTerm env expr with | .error str => return .error $ errorI "parsing" str | .ok syn => pure syn match ← elabTerm syn expectedType? with @@ -136,7 +136,7 @@ def exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.El 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 expectedType? with + let expr ← match ← parseElabExpr expr expectedType? with | .error e => return .error e | .ok expr => pure expr try @@ -152,7 +152,7 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (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 ← typeParse expr with + let expr ← match ← parseElabType expr with | .error e => return .error e | .ok expr => pure $ expr return .ok $ ← GoalState.create expr From 840d2acbd8885c0066adc2138fcc88372e6c4ee5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 31 Mar 2024 16:12:23 -0700 Subject: [PATCH 4/5] docs: Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index cde0807..26bf788 100644 --- a/README.md +++ b/README.md @@ -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": }`: Determine the type of an expression and round-trip it +- `expr.echo {"expr": , "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": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default From 2130bcf3576912c7a4f6750dab8958d5a2dd2551 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 31 Mar 2024 16:43:30 -0700 Subject: [PATCH 5/5] test: Library test --- Pantograph.lean | 2 +- Pantograph/Protocol.lean | 2 +- Test/Common.lean | 7 +++++-- Test/Library.lean | 35 +++++++++++++++++++++++++++++++++++ Test/Main.lean | 8 +++++--- 5 files changed, 47 insertions(+), 7 deletions(-) create mode 100644 Test/Library.lean diff --git a/Pantograph.lean b/Pantograph.lean index 1def945..97f03f4 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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 args.type 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 diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 7a2b341..6ee3354 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -98,7 +98,7 @@ structure StatResult where -- Return the type of an expression structure ExprEcho where expr: String - type: Option String + type?: Option String deriving Lean.FromJson structure ExprEchoResult where expr: Expression diff --git a/Test/Common.lean b/Test/Common.lean index 2e7149d..378dce8 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -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}" = "") diff --git a/Test/Library.lean b/Test/Library.lean new file mode 100644 index 0000000..265335a --- /dev/null +++ b/Test/Library.lean @@ -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 diff --git a/Test/Main.lean b/Test/Main.lean index d24f45f..6baffad 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -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