From 42133f9b7469bdf93c1b5f17edcb640d50baaefb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Oct 2023 17:31:36 -0700 Subject: [PATCH 01/10] 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 From 8c93d30ab76763f2c2a9011d5f77436bcd10144d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Oct 2023 12:31:22 -0700 Subject: [PATCH 02/10] Rename tactic to goal and restructure --- Makefile | 7 +++++-- Pantograph.lean | 2 +- Pantograph/{Tactic.lean => Goal.lean} | 11 ++++++++--- Pantograph/Serial.lean | 10 +--------- Test/Holes.lean | 2 +- Test/Proofs.lean | 8 ++++---- 6 files changed, 20 insertions(+), 20 deletions(-) rename Pantograph/{Tactic.lean => Goal.lean} (87%) diff --git a/Makefile b/Makefile index edee774..39350b6 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ TEST_EXE := build/bin/test TEST_SOURCE := $(wildcard Test/*.lean) $(LIB) $(EXE): $(SOURCE) - lake build + lake build pantograph $(TEST_EXE): $(LIB) $(TEST_SOURCE) lake build test @@ -14,4 +14,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE) test: $(TEST_EXE) lake env $(TEST_EXE) -.PHONY: test +clean: + lake clean + +.PHONY: test clean diff --git a/Pantograph.lean b/Pantograph.lean index 3e53859..c5d56a1 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,7 +1,7 @@ import Pantograph.Commands import Pantograph.Serial import Pantograph.Symbols -import Pantograph.Tactic +import Pantograph.Goal import Pantograph.SemihashMap namespace Pantograph diff --git a/Pantograph/Tactic.lean b/Pantograph/Goal.lean similarity index 87% rename from Pantograph/Tactic.lean rename to Pantograph/Goal.lean index a736064..ea81c36 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Goal.lean @@ -31,12 +31,15 @@ structure GoalState where abbrev M := Elab.TermElabM def GoalState.create (expr: Expr): M GoalState := do + -- Immediately synthesise all metavariables if we need to leave the elaboration context. + -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 + --Elab.Term.synthesizeSyntheticMVarsNoPostponing let expr ← instantiateMVars expr - let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic)) + let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)) let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} return { - savedState := savedState, + savedState, mvarId := goal.mvarId! } @@ -52,7 +55,9 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin let errors ← (messages.map Message.data).mapM fun md => md.toString return .error errors else - return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals) + let unsolved ← Elab.Tactic.getUnsolvedGoals + -- The order of evaluation is important here + return .ok (← MonadBacktrack.saveState, unsolved) catch exception => return .error #[← exception.toMessageData.toString] match Parser.runParserCategory diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 924c77b..27251b6 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -28,19 +28,11 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax := def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do try let expr ← Elab.Term.elabType syn - -- Immediately synthesise all metavariables if we need to leave the elaboration context. - -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 - --Elab.Term.synthesizeSyntheticMVarsNoPostponing - let expr ← instantiateMVars expr return .ok expr catch ex => return .error (← ex.toMessageData.toString) def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do try let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none) - -- Immediately synthesise all metavariables if we need to leave the elaboration context. - -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 - --Elab.Term.synthesizeSyntheticMVarsNoPostponing - let expr ← instantiateMVars expr return .ok expr catch ex => return .error (← ex.toMessageData.toString) @@ -249,7 +241,7 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe caseName? := match mvarDecl.userName with | Name.anonymous => .none | name => .some <| toString name, - isConversion := "| " == (Meta.getGoalPrefix mvarDecl) + isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), vars := vars.reverse.toArray } diff --git a/Test/Holes.lean b/Test/Holes.lean index 8935ea9..64f2e2c 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Tactic +import Pantograph.Goal import Pantograph.Serial namespace Pantograph.Test.Holes diff --git a/Test/Proofs.lean b/Test/Proofs.lean index c9daf84..3aaea0f 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Tactic +import Pantograph.Goal import Pantograph.Serial namespace Pantograph.Test.Proofs @@ -39,7 +39,7 @@ def start_proof (start: Start): TestM (Option GoalState) := do IO.println error return Option.none | .ok syn => - let expr? ← syntax_to_expr syn + let expr? ← syntax_to_expr_type syn add_test $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => @@ -213,7 +213,7 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq : let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options let coreContext: Lean.Core.Context := { - currNamespace := str_to_name "Aniva", + currNamespace := Name.append .anonymous "Aniva", openDecls := [], -- No 'open' directives needed fileName := "", fileMap := { source := "", positions := #[0], lines := #[1] } @@ -232,7 +232,7 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq : /-- 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 })) + (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}]) (opts := {}) (trustLevel := 1) let tests := [ From 9447d29e379d26c61db5e1903f351f14510dda34 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Oct 2023 17:15:23 -0700 Subject: [PATCH 03/10] Store states instead of goals 1. Rename {Commands, Protocol}, and {Symbols, Symbol} 2. Store the root mvarId in the proof state along with goal indices 3. Add diagnostics function which prints out the state 4. Bump version to 0.2.6 (breaking change) Documentations pending --- Main.lean | 6 +- Pantograph.lean | 78 +++-- Pantograph/Goal.lean | 156 ++++++--- Pantograph/{Commands.lean => Protocol.lean} | 34 +- Pantograph/Serial.lean | 16 +- Pantograph/{Symbols.lean => Symbol.lean} | 4 +- Pantograph/Version.lean | 2 +- Test/Integration.lean | 16 +- Test/Main.lean | 4 +- Test/Proofs.lean | 347 +++++++++++--------- Test/Serial.lean | 6 +- 11 files changed, 378 insertions(+), 291 deletions(-) rename Pantograph/{Commands.lean => Protocol.lean} (84%) rename Pantograph/{Symbols.lean => Symbol.lean} (94%) diff --git a/Main.lean b/Main.lean index 8fd617b..d7f936e 100644 --- a/Main.lean +++ b/Main.lean @@ -8,7 +8,7 @@ import Pantograph open Pantograph /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ -def parse_command (s: String): Except String Commands.Command := do +def parseCommand (s: String): Except String Protocol.Command := do let s := s.trim match s.get? 0 with | .some '{' => -- Parse in Json mode @@ -26,9 +26,9 @@ unsafe def loop : MainM Unit := do let state ← get let command ← (← IO.getStdin).getLine if command.trim.length = 0 then return () - match parse_command command with + match parseCommand command with | .error error => - let error := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError) + let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError) -- Using `Lean.Json.compress` here to prevent newline IO.println error.compress | .ok command => diff --git a/Pantograph.lean b/Pantograph.lean index c5d56a1..0e74e81 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,8 +1,8 @@ -import Pantograph.Commands -import Pantograph.Serial -import Pantograph.Symbols import Pantograph.Goal +import Pantograph.Protocol import Pantograph.SemihashMap +import Pantograph.Serial +import Pantograph.Symbol namespace Pantograph @@ -11,16 +11,16 @@ structure Context where /-- Stores state of the REPL -/ structure State where - options: Commands.Options := {} + options: Protocol.Options := {} goalStates: SemihashMap GoalState := SemihashMap.empty --- State monad +/-- Main state monad for executing commands -/ abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) --- For some reason writing `CommandM α := MainM (Except ... α)` disables certain --- monadic features in `MainM` -abbrev CR α := Except Commands.InteractionError α +-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables +-- certain monadic features in `MainM` +abbrev CR α := Except Protocol.InteractionError α -def execute (command: Commands.Command): MainM Lean.Json := do +def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with | .ok args => do @@ -40,31 +40,31 @@ def execute (command: Commands.Command): MainM Lean.Json := do | "goal.tactic" => run goal_tactic | "goal.delete" => run goal_delete | cmd => - let error: Commands.InteractionError := + let error: Protocol.InteractionError := errorCommand s!"Unknown command {cmd}" return Lean.toJson error where - errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc } + errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } errorCommand := errorI "command" errorIndex := errorI "index" -- Command Functions - reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do + reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get let nGoals := state.goalStates.size set { state with goalStates := SemihashMap.empty } return .ok { nGoals } - stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do + stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do let state ← get let nGoals := state.goalStates.size return .ok { nGoals } - lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do + lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => match to_filtered_symbol name info with | .some x => acc.push x | .none => acc) return .ok { symbols := names } - lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do + lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do let state ← get let env ← Lean.MonadEnv.getEnv let name := str_to_name args.name @@ -84,7 +84,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do value? := ← value?.mapM (λ v => serialize_expression state.options v), module? := module? } - expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do + expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get let env ← Lean.MonadEnv.getEnv match syntax_from_str env args.expr with @@ -101,7 +101,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do } catch exception => return .error $ errorI "typing" (← exception.toMessageData.toString) - options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do + options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options set { state with @@ -116,9 +116,9 @@ def execute (command: Commands.Command): MainM Lean.Json := do } } return .ok { } - options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do + options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do return .ok (← get).options - goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do + goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do let state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with @@ -140,34 +140,32 @@ def execute (command: Commands.Command): MainM Lean.Json := do | .error error => return .error error | .ok expr => let goalState ← GoalState.create expr - let (goalStates, goalId) := state.goalStates.insert goalState + let (goalStates, stateId) := state.goalStates.insert goalState set { state with goalStates } - return .ok { goalId } - goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do + return .ok { stateId } + goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get - match state.goalStates.get? args.goalId with - | .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}" + match state.goalStates.get? args.stateId with + | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => - let result ← GoalState.execute goalState args.tactic |>.run state.options + let result ← GoalState.execute goalState args.goalId args.tactic |>.run state.options match result with - | .success goals => - if goals.isEmpty then - return .ok {} - else - -- Append all goals - let (goalStates, goalIds, sGoals) := Array.foldl (λ acc itr => - let (map, indices, serializedGoals) := acc - let (goalState, sGoal) := itr - let (map, index) := map.insert goalState - (map, index :: indices, sGoal :: serializedGoals) - ) (state.goalStates, [], []) goals - set { state with goalStates } - return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray } + | .success nextGoalState goals => + let (goalStates, nextStateId) := state.goalStates.insert nextGoalState + set { state with goalStates } + return .ok { + nextStateId? := .some nextStateId, + goals? := .some goals + } + | .parseError message => + return .ok { parseError? := .some message } + | .indexError goalId => + return .error $ errorIndex s!"Invalid goal id index {goalId}" | .failure messages => return .ok { tacticErrors? := .some messages } - goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do + goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do let state ← get - let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates + let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates set { state with goalStates } return .ok {} diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ea81c36..64c0a6e 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -1,19 +1,8 @@ import Lean -import Pantograph.Symbols +import Pantograph.Symbol import Pantograph.Serial - -/- -The proof state manipulation system - -A proof state is launched by providing -1. Environment: `Environment` -2. Expression: `Expr` -The expression becomes the first meta variable in the saved tactic state -`Elab.Tactic.SavedState`. -From this point on, any proof which extends -`Elab.Term.Context` and --/ +import Pantograph.Protocol def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := { @@ -25,25 +14,32 @@ namespace Pantograph open Lean structure GoalState where - mvarId: MVarId savedState : Elab.Tactic.SavedState + -- The root hole which is the search target + root: MVarId + -- New metavariables acquired in this state + newMVars: SSet MVarId + abbrev M := Elab.TermElabM -def GoalState.create (expr: Expr): M GoalState := do - -- Immediately synthesise all metavariables if we need to leave the elaboration context. +protected def GoalState.create (expr: Expr): M GoalState := do + -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 + --Elab.Term.synthesizeSyntheticMVarsNoPostponing - let expr ← instantiateMVars expr + --let expr ← instantiateMVars expr let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)) let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} return { savedState, - mvarId := goal.mvarId! + root := goal.mvarId!, + newMVars := SSet.empty, } +protected def GoalState.goals (goalState: GoalState): List MVarId := goalState.savedState.tactic.goals -def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) : +def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do state.restore @@ -56,52 +52,108 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin return .error errors else let unsolved ← Elab.Tactic.getUnsolvedGoals - -- The order of evaluation is important here + -- The order of evaluation is important here, since `getUnsolvedGoals` prunes the goals set return .ok (← MonadBacktrack.saveState, unsolved) catch exception => return .error #[← exception.toMessageData.toString] - match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `tactic) - (input := tactic) - (fileName := "") with - | Except.error err => return .error #[err] - | Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic + tacticM tactic { elaborator := .anonymous } |>.run' state.tactic /-- Response for executing a tactic -/ inductive TacticResult where -- Goes to next state - | success (goals: Array (GoalState × Commands.Goal)) - -- Fails with messages + | success (state: GoalState) (goals: Array Protocol.Goal) + -- Tactic failed with messages | failure (messages: Array String) - -namespace TacticResult - -def is_success: TacticResult → Bool - | .success _ => true - | .failure _ => false - -end TacticResult + -- Could not parse tactic + | parseError (message: String) + -- The goal index is out of bounds + | indexError (goalId: Nat) /-- Execute tactic on given state -/ -def GoalState.execute (goal: GoalState) (tactic: String): - Commands.OptionsT M TacticResult := do +protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String): + Protocol.OptionsT M TacticResult := do + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure $ goal + | .none => return .indexError goalId + let tactic ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `tactic) + (input := tactic) + (fileName := "") with + | .ok stx => pure $ stx + | .error error => return .parseError error let options ← read - match (← execute_tactic (state := goal.savedState) (goal := goal.mvarId) (tactic := tactic)) with + match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with | .error errors => return .failure errors - | .ok (nextState, nextGoals) => - if nextGoals.isEmpty then - return .success #[] + | .ok (nextSavedState, nextGoals) => + assert! nextSavedState.tactic.goals.length == nextGoals.length + -- Assert that the definition of metavariables are the same + let nextMCtx := nextSavedState.term.meta.meta.mctx + let prevMCtx := state.savedState.term.meta.meta.mctx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars := (← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return mvarId :: acc + ) []).toSSet + let nextState: GoalState := { + savedState := nextSavedState + root := state.root, + newMVars, + } + nextSavedState.term.restore + let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal + let goals ← nextGoals.mapM fun nextGoal => do + match (← MonadMCtx.getMCtx).findDecl? nextGoal with + | .some mvarDecl => + let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) + return serializedGoal + | .none => throwError s!"Parent mvar id does not exist {nextGoal.name}" + return .success nextState goals.toArray + +-- Diagnostics functions + +/-- Print the metavariables in a readable format -/ +protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): Elab.TermElabM Unit := do + let savedState := goalState.savedState + savedState.term.restore + let goals := savedState.tactic.goals + let mctx ← getMCtx + goals.forM (fun mvarId => do + let pref := "⊢" + match mctx.decls.find? mvarId with + | .some decl => printMVar pref mvarId decl + | .none => IO.println s!"{pref}{mvarId.name}: ??" + ) + let goals := goals.toSSet + mctx.decls.forM (fun mvarId decl => do + if goals.contains mvarId then + pure () + else if mvarId == goalState.root then + printMVar (pref := ">") mvarId decl + else if ¬(goalState.newMVars.contains mvarId) then + printMVar (pref := " ") mvarId decl + else if options.printNonVisible then + printMVar (pref := "~") mvarId decl else - let nextGoals: List GoalState := nextGoals.map fun mvarId => { mvarId, savedState := nextState } - let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal.mvarId - let goals ← nextGoals.mapM fun nextGoal => do - match (← MonadMCtx.getMCtx).findDecl? nextGoal.mvarId with - | .some mvarDecl => - let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) - return (nextGoal, serializedGoal) - | .none => throwError nextGoal.mvarId - return .success goals.toArray + IO.println s!" {mvarId.name}{userNameToString decl.userName}" + ) + where + printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do + if options.printContext then + decl.lctx.fvarIdToDecl.forM printFVar + IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {← serialize_expression_ast decl.type}" + if options.printValue then + if let Option.some value := (← getMCtx).eAssignment.find? mvarId then + IO.println s!" = {← Meta.ppExpr value}" + printFVar (fvarId: FVarId) (decl: LocalDecl): Elab.TermElabM Unit := do + IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}" + userNameToString : Name → String + | .anonymous => "" + | other => s!"[{other}]" end Pantograph diff --git a/Pantograph/Commands.lean b/Pantograph/Protocol.lean similarity index 84% rename from Pantograph/Commands.lean rename to Pantograph/Protocol.lean index 72194b0..390c49f 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Protocol.lean @@ -6,7 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL. -/ import Lean.Data.Json -namespace Pantograph.Commands +namespace Pantograph.Protocol /-- Main Option structure, placed here to avoid name collision -/ @@ -132,32 +132,42 @@ abbrev OptionsPrintResult := Options structure GoalStart where -- Only one of the fields below may be populated. - expr: Option String -- Proof expression - copyFrom: Option String -- Theorem name + expr: Option String -- Directly parse in an expression + copyFrom: Option String -- Copy the type from a theorem in the environment deriving Lean.FromJson structure GoalStartResult where - goalId: Nat := 0 -- Proof tree id + stateId: Nat := 0 deriving Lean.ToJson structure GoalTactic where -- Identifiers for tree, state, and goal - goalId: Nat + stateId: Nat + goalId: Nat := 0 tactic: String deriving Lean.FromJson structure GoalTacticResult where - -- Existence of this field shows success + -- The next goal state id. Existence of this field shows success + nextStateId?: Option Nat := .none + -- If the array is empty, it shows the goals have been fully resolved. goals?: Option (Array Goal) := .none - -- Next proof state id, if successful - goalIds?: Option (Array Nat) := .none - -- Existence of this field shows failure + + -- Existence of this field shows tactic execution failure tacticErrors?: Option (Array String) := .none + + -- Existence of this field shows the tactic parsing has failed + parseError?: Option String := .none deriving Lean.ToJson --- Remove a bunch of goals. +-- Remove goal states structure GoalDelete where - goalIds: List Nat + stateIds: List Nat deriving Lean.FromJson structure GoalDeleteResult where deriving Lean.ToJson +structure GoalPrint where + printContext: Bool := true + printValue: Bool := true + printNonVisible: Bool := true -end Pantograph.Commands + +end Pantograph.Protocol diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 27251b6..46f1262 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -3,7 +3,7 @@ All serialisation functions -/ import Lean -import Pantograph.Commands +import Pantograph.Protocol namespace Pantograph open Lean @@ -39,7 +39,7 @@ def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do --- Output Functions --- -def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do +def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do Meta.forallTelescope expr fun arr body => do let binders ← arr.mapM fun fvar => do return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType))) @@ -108,7 +108,7 @@ def serialize_expression_ast (expr: Expr): MetaM String := do -- Lean these are handled using a `#` prefix. return s!"{deBruijnIndex}" | .fvar fvarId => - let name := (← fvarId.getDecl).userName + let name := name_to_ast fvarId.name return s!"(:fv {name})" | .mvar mvarId => let name := name_to_ast mvarId.name @@ -166,7 +166,7 @@ def serialize_expression_ast (expr: Expr): MetaM String := do | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" -def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do +def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp := toString (← Meta.ppExpr e) let pp?: Option String := match options.printExprPretty with | true => .some pp @@ -181,8 +181,8 @@ def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.E } /-- Adapted from ppGoal -/ -def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) - : MetaM Commands.Goal := do +def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) + : MetaM Protocol.Goal := do -- Options for printing; See Meta.ppGoal for details let showLetValues := true let ppAuxDecls := options.printAuxDecls @@ -190,7 +190,7 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe let lctx := mvarDecl.lctx let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } Meta.withLCtx lctx mvarDecl.localInstances do - let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do + let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do match localDecl with | .cdecl _ _ varName _ _ _ => let varName := varName.simpMacroScopes @@ -201,7 +201,7 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe return { name := toString varName, } - let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do + let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with | .cdecl _ _ varName type _ _ => let varName := varName.simpMacroScopes diff --git a/Pantograph/Symbols.lean b/Pantograph/Symbol.lean similarity index 94% rename from Pantograph/Symbols.lean rename to Pantograph/Symbol.lean index 641a276..81d7deb 100644 --- a/Pantograph/Symbols.lean +++ b/Pantograph/Symbol.lean @@ -1,10 +1,8 @@ -/- - - Manages the visibility status of symbols - -/ import Lean.Declaration namespace Pantograph +/-- Converts a symbol of the form `aa.bb.cc` to a name -/ def str_to_name (s: String): Lean.Name := (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index f450292..ec93fa9 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,5 @@ namespace Pantograph -def version := "0.2.5" +def version := "0.2.6" end Pantograph diff --git a/Test/Integration.lean b/Test/Integration.lean index 5dbb80a..b7a5e62 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -47,26 +47,26 @@ def test_option_modify : IO LSpec.TestSeq := let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n" let sexp? := Option.some "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))" let module? := Option.some "Init.Data.Nat.Basic" - let options: Commands.Options := {} + let options: Protocol.Options := {} subroutine_runner [ subroutine_step "lib.inspect" [("name", .str "Nat.add_one")] (Lean.toJson ({ type := { pp? }, module? }: - Commands.LibInspectResult)), + Protocol.LibInspectResult)), subroutine_step "options.set" [("printExprAST", .bool true)] (Lean.toJson ({ }: - Commands.OptionsSetResult)), + Protocol.OptionsSetResult)), subroutine_step "lib.inspect" [("name", .str "Nat.add_one")] (Lean.toJson ({ type := { pp?, sexp? }, module? }: - Commands.LibInspectResult)), + Protocol.LibInspectResult)), subroutine_step "options.print" [] (Lean.toJson ({ options with printExprAST := true }: - Commands.OptionsPrintResult)) + Protocol.OptionsPrintResult)) ] def test_malformed_command : IO LSpec.TestSeq := let invalid := "invalid" @@ -75,12 +75,12 @@ def test_malformed_command : IO LSpec.TestSeq := [("name", .str "Nat.add_one")] (Lean.toJson ({ error := "command", desc := s!"Unknown command {invalid}"}: - Commands.InteractionError)), + Protocol.InteractionError)), subroutine_named_step "JSON Deserialization" "expr.echo" [(invalid, .str "Random garbage data")] (Lean.toJson ({ - error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}: - Commands.InteractionError)) + error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}: + Protocol.InteractionError)) ] def suite: IO LSpec.TestSeq := do diff --git a/Test/Main.lean b/Test/Main.lean index cb7c055..5b9a24a 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,5 +1,5 @@ import LSpec -import Test.Holes +--import Test.Holes import Test.Integration import Test.Proofs import Test.Serial @@ -11,7 +11,7 @@ unsafe def main := do Lean.initSearchPath (← Lean.findSysroot) let suites := [ - Holes.suite, + --Holes.suite, Integration.suite, Proofs.suite, Serial.suite diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 3aaea0f..05331ed 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -1,7 +1,21 @@ +/- +Tests pertaining to goals with no interdependencies +-/ import LSpec import Pantograph.Goal import Pantograph.Serial +namespace Pantograph + +def TacticResult.toString : TacticResult → String + | .success _ goals => s!".success ({goals.size} goals)" + | .failure messages => + let messages := "\n".intercalate messages.toList + s!".failure {messages}" + | .parseError error => s!".parseError {error}" + | .indexError index => s!".indexError {index}" +end Pantograph + namespace Pantograph.Test.Proofs open Pantograph open Lean @@ -10,21 +24,21 @@ inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M) +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) -deriving instance DecidableEq, Repr for Commands.Expression -deriving instance DecidableEq, Repr for Commands.Variable -deriving instance DecidableEq, Repr for Commands.Goal +deriving instance DecidableEq, Repr for Protocol.Expression +deriving instance DecidableEq, Repr for Protocol.Variable +deriving instance DecidableEq, Repr for Protocol.Goal -def add_test (test: LSpec.TestSeq): TestM Unit := do +def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test -def start_proof (start: Start): TestM (Option GoalState) := do +def startProof (start: Start): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv match start with | .copy name => let cInfo? := str_to_name name |> env.find? - add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome + addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome match cInfo? with | .some cInfo => let goal ← GoalState.create (expr := cInfo.type) @@ -33,14 +47,14 @@ def start_proof (start: Start): TestM (Option GoalState) := do return Option.none | .expr expr => let syn? := syntax_from_str env expr - add_test $ LSpec.check s!"Parsing {expr}" (syn?.isOk) + 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 - add_test $ LSpec.check s!"Elaborating" expr?.isOk + addTest $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => IO.println error @@ -49,9 +63,9 @@ def start_proof (start: Start): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal -def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false +def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false -def build_goal (nameType: List (String × String)) (target: String): Commands.Goal := +def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goal := { target := { pp? := .some target}, vars := (nameType.map fun x => ({ @@ -60,8 +74,8 @@ def build_goal (nameType: List (String × String)) (target: String): Commands.Go 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 := +-- Like `buildGoal` but allow certain variables to be elided. +def buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal := { target := { pp? := .some target}, vars := (nameType.map fun x => ({ @@ -70,146 +84,7 @@ def build_goal_selective (nameType: List (String × Option String)) (target: Str isInaccessible? := x.snd.map (λ _ => false) })).toArray } - - --- Individual test cases -example: ∀ (a b: Nat), a + b = b + a := by - intro n m - rw [Nat.add_comm] -def proof_nat_add_comm: TestM Unit := do - let goal? ← start_proof (.copy "Nat.add_comm") - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then - let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" - add_test $ LSpec.check "intro n m" (sGoal = sGoal1e) - - if let .failure #[message] ← goal.execute "assumption" then - add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") - else - add_test $ assert_unreachable "assumption" - - if let .success #[] ← goal.execute "rw [Nat.add_comm]" then - return () - else - add_test $ assert_unreachable "rw [Nat.add_comm]" - else - add_test $ assert_unreachable "intro n m" -def proof_nat_add_comm_manual: TestM Unit := do - let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a") - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then - let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" - add_test $ LSpec.check "intro n m" (sGoal = sGoal1e) - - if let .failure #[message] ← goal.execute "assumption" then - add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") - else - add_test $ assert_unreachable "assumption" - - if let .success #[] ← goal.execute "rw [Nat.add_comm]" then - return () - else - add_test $ assert_unreachable "rw [Nat.add_comm]" - else - add_test $ assert_unreachable "intro n m" - - --- Two ways to write the same theorem -example: ∀ (p q: Prop), p ∨ q → q ∨ p := by - intro p q h - cases h - apply Or.inr - assumption - apply Or.inl - assumption -example: ∀ (p q: Prop), p ∨ q → q ∨ p := by - intro p q h - cases h - . apply Or.inr - assumption - . apply Or.inl - assumption -def proof_or_comm: TestM Unit := do - let typeProp: Commands.Expression := { pp? := .some "Prop" } - let branchGoal (caseName name: String): Commands.Goal := { - caseName? := .some caseName, - target := { pp? := .some "q ∨ p" }, - vars := #[ - { name := "p", type? := .some typeProp, isInaccessible? := .some false }, - { name := "q", type? := .some typeProp, isInaccessible? := .some false }, - { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } - ] - } - let goal? ← start_proof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - if let .success #[(goal, sGoal)] ← goal.execute "intro p q h" then - let sGoal1e := build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p" - add_test $ LSpec.check "intro p q h" (sGoal = sGoal1e) - - if let .success #[(goal1, sGoal1), (goal2, sGoal2)] ← goal.execute "cases h" then - add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p") - if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then - if let .success #[] ← goal.execute "assumption" then - return () - else - add_test $ assert_unreachable "assumption" - else - add_test $ assert_unreachable "apply Or.inr" - - - add_test $ LSpec.check "cases h/2" (sGoal2 = branchGoal "inr" "q") - if let .success #[(goal, _)] ← goal2.execute "apply Or.inl" then - if let .success #[] ← goal.execute "assumption" then - return () - else - add_test $ assert_unreachable "assumption" - else - add_test $ assert_unreachable "apply Or.inl" - - else - add_test $ assert_unreachable "cases h" - else - add_test $ assert_unreachable "intro p q h" - -example (w x y z : Nat) (p : Nat → Prop) - (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by - simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at * - assumption -def proof_arith_1: TestM Unit := do - let goal? ← start_proof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - if let .success #[(goal, _)] ← goal.execute "intros" then - if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then - if let .success #[] ← goal.execute "assumption" then - return () - else - add_test $ assert_unreachable "assumption" - else - add_test $ assert_unreachable "simp ..." - else - add_test $ assert_unreachable "intros" - -def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do - let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a") - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - if let .success #[(goal, sGoal)] ← goal.execute "intro n" then - let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" - add_test $ LSpec.check "intro n" (sGoal = sGoal1e) - - if let .success #[(_, sGoal)] ← goal.execute "intro m" then - let sGoal2e: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n" - add_test $ LSpec.check "intro m" (sGoal = sGoal2e) - else - add_test $ assert_unreachable "intro m" - else - add_test $ assert_unreachable "intro n" - -def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do +def proofRunner (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 := { @@ -229,6 +104,160 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq : | .ok (_, a) => return a + +-- Individual test cases +example: ∀ (a b: Nat), a + b = b + a := by + intro n m + rw [Nat.add_comm] +def proof_nat_add_comm (manual: Bool): TestM Unit := do + let state? ← startProof <| match manual with + | false => .copy "Nat.add_comm" + | true => .expr "∀ (a b: Nat), a + b = b + a" + addTest $ LSpec.check "Start goal" state?.isSome + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let (state1, goal1) ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "intro n m" (goal1 = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") + + match ← state1.execute (goalId := 0) (tactic := "assumption") with + | .failure #[message] => + addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") + | other => do + addTest $ assertUnreachable $ other.toString + + let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with + | .success state #[] => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + return () + + +-- Two ways to write the same theorem +example: ∀ (p q: Prop), p ∨ q → q ∨ p := by + intro p q h + cases h + apply Or.inr + assumption + apply Or.inl + assumption +example: ∀ (p q: Prop), p ∨ q → q ∨ p := by + intro p q h + cases h + . apply Or.inr + assumption + . apply Or.inl + assumption +def proof_or_comm: TestM Unit := do + let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let (state1, goal1) ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "p q h" (goal1 = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p") + let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with + | .success state #[goal1, goal2] => pure (state, goal1, goal2) + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "cases h/1" (goal1 = branchGoal "inl" "p") + addTest $ LSpec.check "cases h/2" (goal2 = branchGoal "inr" "q") + + let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with + | .success state #[] => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + IO.println "===== 1 =====" + state1.print + IO.println "===== 2 =====" + state2.print + IO.println "===== 4_1 =====" + state4_1.print + let (state3_2, _goal) ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + IO.println "===== 3_2 =====" + state3_2.print + let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with + | .success state #[] => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + IO.println "===== 4_2 =====" + state4_2.print + + return () + where + typeProp: Protocol.Expression := { pp? := .some "Prop" } + branchGoal (caseName name: String): Protocol.Goal := { + caseName? := .some caseName, + target := { pp? := .some "q ∨ p" }, + vars := #[ + { name := "p", type? := .some typeProp, isInaccessible? := .some false }, + { name := "q", type? := .some typeProp, isInaccessible? := .some false }, + { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } + ] + } + +--example (w x y z : Nat) (p : Nat → Prop) +-- (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by +-- simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at * +-- assumption +--def proof_arith_1: TestM Unit := do +-- let goal? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") +-- addTest $ LSpec.check "Start goal" goal?.isSome +-- if let .some goal := goal? then +-- if let .success #[(goal, _)] ← goal.execute "intros" then +-- if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then +-- if let .success #[] ← goal.execute "assumption" then +-- return () +-- else +-- addTest $ assertUnreachable "assumption" +-- else +-- addTest $ assertUnreachable "simp ..." +-- else +-- addTest $ assertUnreachable "intros" +-- +--def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do +-- let goal? ← startProof (.expr "∀ (a b: Nat), a + b = b + a") +-- addTest $ LSpec.check "Start goal" goal?.isSome +-- if let .some goal := goal? then +-- if let .success #[(goal, sGoal)] ← goal.execute "intro n" then +-- let sGoal1e: Protocol.Goal :=buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" +-- addTest $ LSpec.check "intro n" (sGoal = sGoal1e) +-- +-- if let .success #[(_, sGoal)] ← goal.execute "intro m" then +-- let sGoal2e: Protocol.Goal :=buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n" +-- addTest $ LSpec.check "intro m" (sGoal = sGoal2e) +-- else +-- addTest $ assertUnreachable "intro m" +-- else +-- addTest $ assertUnreachable "intro n" + /-- 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 @@ -236,15 +265,15 @@ def suite: IO LSpec.TestSeq := do (opts := {}) (trustLevel := 1) let tests := [ - ("Nat.add_comm", proof_nat_add_comm), - ("nat.add_comm manual", proof_nat_add_comm_manual), - ("Or.comm", proof_or_comm), - ("arithmetic 1", proof_arith_1), - ("delta variable", proof_delta_variable) + ("Nat.add_comm", proof_nat_add_comm false), + ("Nat.add_comm manual", proof_nat_add_comm true), + ("Or.comm", proof_or_comm) + --("arithmetic 1", proof_arith_1), + --("delta variable", proof_delta_variable) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests - let tests ← proof_runner env tests + let tests ← proofRunner env tests return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done return LSpec.group "Proofs" tests diff --git a/Test/Serial.lean b/Test/Serial.lean index e135c0c..30d6f60 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -1,19 +1,19 @@ import LSpec import Pantograph.Serial -import Pantograph.Symbols +import Pantograph.Symbol namespace Pantograph.Test.Serial open Pantograph open Lean -deriving instance Repr, DecidableEq for Commands.BoundExpression +deriving instance Repr, DecidableEq for Protocol.BoundExpression def test_str_to_name: LSpec.TestSeq := LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run") def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do - let entries: List (String × Commands.BoundExpression) := [ + let entries: List (String × Protocol.BoundExpression) := [ ("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), ("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" }) ] From 0a0f0304a8d1bb234bac8a10ed047da985038712 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 25 Oct 2023 16:03:45 -0700 Subject: [PATCH 04/10] feat: Add proof continue and root extraction --- Pantograph/Goal.lean | 72 ++++++++++++++++------ Pantograph/Protocol.lean | 3 +- Pantograph/Serial.lean | 126 ++++++++++++++++++++------------------- Test/Proofs.lean | 30 ++++++---- 4 files changed, 142 insertions(+), 89 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 64c0a6e..3f42abe 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -31,14 +31,20 @@ protected def GoalState.create (expr: Expr): M GoalState := do --let expr ← instantiateMVars expr let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)) let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState - let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} + let root := goal.mvarId! + let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]} return { savedState, - root := goal.mvarId!, - newMVars := SSet.empty, + root, + newMVars := SSet.insert .empty root, } protected def GoalState.goals (goalState: GoalState): List MVarId := goalState.savedState.tactic.goals +private def GoalState.mctx (state: GoalState): MetavarContext := + state.savedState.term.meta.meta.mctx +private def GoalState.mvars (state: GoalState): SSet MVarId := + state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k + def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do @@ -93,13 +99,13 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String let prevMCtx := state.savedState.term.meta.meta.mctx -- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars. - let newMVars := (← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then assert! prevMVarDecl.type == mvarDecl.type return acc else - return mvarId :: acc - ) []).toSSet + return acc.insert mvarId + ) SSet.empty let nextState: GoalState := { savedState := nextSavedState root := state.root, @@ -115,38 +121,70 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String | .none => throwError s!"Parent mvar id does not exist {nextGoal.name}" return .success nextState goals.toArray +/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ +protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState := + if target.root != graftee.root then + .error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}" + -- Ensure goals are not dangling + else if ¬ (target.goals.all (λ goal => graftee.mvars.contains goal)) then + .error s!"Some goals in target are not present in the graftee" + else + -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. + let unassigned := target.goals.filter (λ goal => + let mctx := graftee.mctx + ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) + .ok { + savedState := { + term := graftee.savedState.term, + tactic := { goals := unassigned }, + }, + root := target.root, + newMVars := graftee.newMVars, + } + +protected def GoalState.rootExpr (goalState: GoalState): Option Expr := + goalState.mctx.eAssignment.find? goalState.root |>.filter (λ e => ¬ e.hasMVar) + -- Diagnostics functions /-- Print the metavariables in a readable format -/ -protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): Elab.TermElabM Unit := do +protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): M Unit := do let savedState := goalState.savedState savedState.term.restore let goals := savedState.tactic.goals let mctx ← getMCtx + let root := goalState.root + -- Print the root + match mctx.decls.find? root with + | .some decl => printMVar ">" root decl + | .none => IO.println s!">{root.name}: ??" goals.forM (fun mvarId => do - let pref := "⊢" - match mctx.decls.find? mvarId with - | .some decl => printMVar pref mvarId decl - | .none => IO.println s!"{pref}{mvarId.name}: ??" + if mvarId != root then + match mctx.decls.find? mvarId with + | .some decl => printMVar "⊢" mvarId decl + | .none => IO.println s!"⊢{mvarId.name}: ??" ) let goals := goals.toSSet mctx.decls.forM (fun mvarId decl => do - if goals.contains mvarId then + if goals.contains mvarId || mvarId == root then pure () + -- Always print the root goal else if mvarId == goalState.root then printMVar (pref := ">") mvarId decl - else if ¬(goalState.newMVars.contains mvarId) then - printMVar (pref := " ") mvarId decl + -- Print the remainig ones that users don't see in Lean else if options.printNonVisible then - printMVar (pref := "~") mvarId decl + let pref := if goalState.newMVars.contains mvarId then "~" else " " + printMVar pref mvarId decl else - IO.println s!" {mvarId.name}{userNameToString decl.userName}" + pure () + --IO.println s!" {mvarId.name}{userNameToString decl.userName}" ) where printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do if options.printContext then decl.lctx.fvarIdToDecl.forM printFVar - IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {← serialize_expression_ast decl.type}" + let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) + IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" if options.printValue then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then IO.println s!" = {← Meta.ppExpr value}" diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 390c49f..49103d7 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -167,7 +167,8 @@ structure GoalDeleteResult where structure GoalPrint where printContext: Bool := true printValue: Bool := true - printNonVisible: Bool := true + printNewMVars: Bool := false + printNonVisible: Bool := false end Pantograph.Protocol diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 46f1262..a5acd7f 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -45,9 +45,11 @@ def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType))) return { binders, target := toString (← Meta.ppExpr body) } -private def name_to_ast: Lean.Name → String - | .anonymous - | .num _ _ => ":anon" +private def name_to_ast (name: Lean.Name) (sanitize: Bool := true): String := match name with + | .anonymous => ":anon" + | .num n i => match sanitize with + | false => s!"{toString n} {i}" + | true => ":anon" | n@(.str _ _) => toString n private def level_depth: Level → Nat @@ -100,71 +102,73 @@ def serialize_sort_level_ast (level: Level): String := /-- Completely serializes an expression tree. Json not used due to compactness -/ -def serialize_expression_ast (expr: Expr): MetaM String := do - match expr with - | .bvar deBruijnIndex => - -- This is very common so the index alone is shown. Literals are handled below. - -- The raw de Bruijn index should never appear in an unbound setting. In - -- Lean these are handled using a `#` prefix. - return s!"{deBruijnIndex}" - | .fvar fvarId => - let name := name_to_ast fvarId.name - return s!"(:fv {name})" - | .mvar mvarId => - let name := name_to_ast mvarId.name - return s!"(:mv {name})" - | .sort level => - let level := serialize_sort_level_ast level - return s!"(:sort {level})" - | .const declName _ => - -- The universe level of the const expression is elided since it should be - -- inferrable from surrounding expression - return s!"(:c {declName})" - | .app fn arg => - let fn' ← serialize_expression_ast fn - let arg' ← serialize_expression_ast arg - return s!"({fn'} {arg'})" - | .lam binderName binderType body binderInfo => - let binderName' := name_to_ast binderName - let binderType' ← serialize_expression_ast binderType - let body' ← serialize_expression_ast body - let binderInfo' := binder_info_to_ast binderInfo - return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" - | .forallE binderName binderType body binderInfo => - let binderName' := name_to_ast binderName - let binderType' ← serialize_expression_ast binderType - let body' ← serialize_expression_ast body - let binderInfo' := binder_info_to_ast binderInfo - return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" - | .letE name type value body _ => - -- Dependent boolean flag diacarded - let name' := name_to_ast name - let type' ← serialize_expression_ast type - let value' ← serialize_expression_ast value - let body' ← serialize_expression_ast body - return s!"(:let {name'} {type'} {value'} {body'})" - | .lit v => - -- To not burden the downstream parser who needs to handle this, the literal - -- is wrapped in a :lit sexp. - let v' := match v with - | .natVal val => toString val - | .strVal val => s!"\"{val}\"" - return s!"(:lit {v'})" - | .mdata _ expr => - -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter - -- It may become necessary to incorporate the metadata. - return (← serialize_expression_ast expr) - | .proj typeName idx struct => - let struct' ← serialize_expression_ast struct - return s!"(:proj {typeName} {idx} {struct'})" - +def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do + return self expr where + self (e: Expr): String := + match e with + | .bvar deBruijnIndex => + -- This is very common so the index alone is shown. Literals are handled below. + -- The raw de Bruijn index should never appear in an unbound setting. In + -- Lean these are handled using a `#` prefix. + s!"{deBruijnIndex}" + | .fvar fvarId => + let name := of_name fvarId.name + s!"(:fv {name})" + | .mvar mvarId => + let name := of_name mvarId.name + s!"(:mv {name})" + | .sort level => + let level := serialize_sort_level_ast level + s!"(:sort {level})" + | .const declName _ => + -- The universe level of the const expression is elided since it should be + -- inferrable from surrounding expression + s!"(:c {declName})" + | .app fn arg => + let fn' := self fn + let arg' := self arg + s!"({fn'} {arg'})" + | .lam binderName binderType body binderInfo => + let binderName' := of_name binderName + let binderType' := self binderType + let body' := self body + let binderInfo' := binder_info_to_ast binderInfo + s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" + | .forallE binderName binderType body binderInfo => + let binderName' := of_name binderName + let binderType' := self binderType + let body' := self body + let binderInfo' := binder_info_to_ast binderInfo + s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" + | .letE name type value body _ => + -- Dependent boolean flag diacarded + let name' := name_to_ast name + let type' := self type + let value' := self value + let body' := self body + s!"(:let {name'} {type'} {value'} {body'})" + | .lit v => + -- To not burden the downstream parser who needs to handle this, the literal + -- is wrapped in a :lit sexp. + let v' := match v with + | .natVal val => toString val + | .strVal val => s!"\"{val}\"" + s!"(:lit {v'})" + | .mdata _ inner => + -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter + -- It may become necessary to incorporate the metadata. + self inner + | .proj typeName idx struct => + let struct' := self struct + s!"(:proj {typeName} {idx} {struct'})" -- Elides all unhygenic names binder_info_to_ast : Lean.BinderInfo → String | .default => "" | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" + of_name (name: Name) := name_to_ast name sanitize def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp := toString (← Meta.ppExpr e) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 05331ed..ac9c78c 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -189,26 +189,36 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - IO.println "===== 1 =====" - state1.print - IO.println "===== 2 =====" - state2.print - IO.println "===== 4_1 =====" - state4_1.print let (state3_2, _goal) ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with | .success state #[goal] => pure (state, goal) | other => do addTest $ assertUnreachable $ other.toString return () - IO.println "===== 3_2 =====" - state3_2.print let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with | .success state #[] => pure state | other => do addTest $ assertUnreachable $ other.toString return () - IO.println "===== 4_2 =====" - state4_2.print + + -- Ensure the proof can continue from `state4_2`. + let state2b ← match state2.continue state4_2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.test "state2b" (state2b.goals == [state2.goals.get! 0]) + let (state3_1, _goal) ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with + | .success state #[] => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + IO.println "===== 4_1 =====" + state4_1.print ({ printNonVisible := false }) return () where From 0ecfa9fc261b53c2e046004ea4c82bf09254826e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 25 Oct 2023 22:18:59 -0700 Subject: [PATCH 05/10] feat: Display user name in Goal structure 1. Modify `serialize_expression_ast` so its no longer a monad 2. Test existence of root expression --- Pantograph/Goal.lean | 9 +++++++-- Pantograph/Protocol.lean | 5 ++++- Pantograph/Serial.lean | 42 ++++++++++++++++++++++------------------ Test/Common.lean | 19 ++++++++++++++++++ Test/Proofs.lean | 25 ++++++++++++------------ Test/Serial.lean | 4 ++-- 6 files changed, 68 insertions(+), 36 deletions(-) create mode 100644 Test/Common.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3f42abe..4e57134 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -143,7 +143,12 @@ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Excep } protected def GoalState.rootExpr (goalState: GoalState): Option Expr := - goalState.mctx.eAssignment.find? goalState.root |>.filter (λ e => ¬ e.hasMVar) + let expr := goalState.mctx.eAssignment.find! goalState.root + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + if expr.hasMVar then + .none + else + .some expr -- Diagnostics functions @@ -183,7 +188,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrin printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do if options.printContext then decl.lctx.fvarIdToDecl.forM printFVar - let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) + let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" if options.printValue then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 49103d7..a6bae29 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -43,7 +43,10 @@ structure Expression where deriving Lean.ToJson structure Variable where - name: String + /-- The internal name used in raw expressions -/ + name: String := "" + /-- The name displayed to the user -/ + userName: String /-- Does the name contain a dagger -/ isInaccessible?: Option Bool := .none type?: Option Expression := .none diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a5acd7f..99f95ef 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -102,8 +102,8 @@ def serialize_sort_level_ast (level: Level): String := /-- Completely serializes an expression tree. Json not used due to compactness -/ -def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do - return self expr +def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String := + self expr where self (e: Expr): String := match e with @@ -175,7 +175,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E let pp?: Option String := match options.printExprPretty with | true => .some pp | false => .none - let sexp: String := (← serialize_expression_ast e) + let sexp: String := serialize_expression_ast e let sexp?: Option String := match options.printExprAST with | true => .some sexp | false => .none @@ -196,27 +196,30 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe Meta.withLCtx lctx mvarDecl.localInstances do let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do match localDecl with - | .cdecl _ _ varName _ _ _ => - let varName := varName.simpMacroScopes + | .cdecl _ fvarId userName _ _ _ => + let userName := userName.simpMacroScopes return { - name := toString varName, + name := of_name fvarId.name, + userName:= of_name userName.simpMacroScopes, } - | .ldecl _ _ varName _ _ _ _ => do + | .ldecl _ fvarId userName _ _ _ _ => do return { - name := toString varName, + name := of_name fvarId.name, + userName := toString userName.simpMacroScopes, } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with - | .cdecl _ _ varName type _ _ => - let varName := varName.simpMacroScopes + | .cdecl _ fvarId userName type _ _ => + let userName := userName.simpMacroScopes let type ← instantiateMVars type return { - name := toString varName, - isInaccessible? := .some varName.isInaccessibleUserName + name := of_name fvarId.name, + userName:= of_name userName, + isInaccessible? := .some userName.isInaccessibleUserName type? := .some (← serialize_expression options type) } - | .ldecl _ _ varName type val _ _ => do - let varName := varName.simpMacroScopes + | .ldecl _ fvarId userName type val _ _ => do + let userName := userName.simpMacroScopes let type ← instantiateMVars type let value? ← if showLetValues then let val ← instantiateMVars val @@ -224,8 +227,9 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe else pure $ .none return { - name := toString varName, - isInaccessible? := .some varName.isInaccessibleUserName + name := of_name fvarId.name, + userName:= of_name userName, + isInaccessible? := .some userName.isInaccessibleUserName type? := .some (← serialize_expression options type) value? := value? } @@ -242,13 +246,13 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe | false => ppVar localDecl return var::acc return { - caseName? := match mvarDecl.userName with - | Name.anonymous => .none - | name => .some <| toString name, + caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), vars := vars.reverse.toArray } + where + of_name (n: Name) := name_to_ast n (sanitize := false) diff --git a/Test/Common.lean b/Test/Common.lean new file mode 100644 index 0000000..3e52932 --- /dev/null +++ b/Test/Common.lean @@ -0,0 +1,19 @@ +import Pantograph.Protocol + +namespace Pantograph + +namespace Protocol +/-- Set internal names to "" -/ +def Goal.devolatilize (goal: Goal): Goal := + { + goal with + vars := goal.vars.map removeInternalAux, + } + where removeInternalAux (v: Variable): Variable := + { + v with + name := "" + } +end Protocol + +end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ac9c78c..d609dd4 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -4,6 +4,7 @@ Tests pertaining to goals with no interdependencies import LSpec import Pantograph.Goal import Pantograph.Serial +import Test.Common namespace Pantograph @@ -69,7 +70,7 @@ def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goa { target := { pp? := .some target}, vars := (nameType.map fun x => ({ - name := x.fst, + userName := x.fst, type? := .some { pp? := .some x.snd }, isInaccessible? := .some false })).toArray @@ -79,7 +80,7 @@ def buildGoalSelective (nameType: List (String × Option String)) (target: Strin { target := { pp? := .some target}, vars := (nameType.map fun x => ({ - name := x.fst, + userName := x.fst, type? := x.snd.map (λ type => { pp? := type }), isInaccessible? := x.snd.map (λ _ => false) })).toArray @@ -104,7 +105,6 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := | .ok (_, a) => return a - -- Individual test cases example: ∀ (a b: Nat), a + b = b + a := by intro n m @@ -125,7 +125,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "intro n m" (goal1 = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") + addTest $ LSpec.check "intro n m" (goal1.devolatilize = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") match ← state1.execute (goalId := 0) (tactic := "assumption") with | .failure #[message] => @@ -170,14 +170,14 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "p q h" (goal1 = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p") + addTest $ LSpec.check "p q h" (goal1.devolatilize = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p") let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with | .success state #[goal1, goal2] => pure (state, goal1, goal2) | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "cases h/1" (goal1 = branchGoal "inl" "p") - addTest $ LSpec.check "cases h/2" (goal2 = branchGoal "inr" "q") + addTest $ LSpec.check "cases h/1" (goal1.devolatilize = branchGoal "inl" "p") + addTest $ LSpec.check "cases h/2" (goal2.devolatilize = branchGoal "inr" "q") let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state #[goal] => pure (state, goal) @@ -200,6 +200,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "4_2 root" state4_2.rootExpr.isNone -- Ensure the proof can continue from `state4_2`. let state2b ← match state2.continue state4_2 with | .error msg => do @@ -217,8 +218,8 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - IO.println "===== 4_1 =====" - state4_1.print ({ printNonVisible := false }) + state4_1.print + addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome return () where @@ -227,9 +228,9 @@ def proof_or_comm: TestM Unit := do caseName? := .some caseName, target := { pp? := .some "q ∨ p" }, vars := #[ - { name := "p", type? := .some typeProp, isInaccessible? := .some false }, - { name := "q", type? := .some typeProp, isInaccessible? := .some false }, - { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } + { userName := "p", type? := .some typeProp, isInaccessible? := .some false }, + { userName := "q", type? := .some typeProp, isInaccessible? := .some false }, + { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } ] } diff --git a/Test/Serial.lean b/Test/Serial.lean index 30d6f60..9a42992 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv let expr := str_to_name symbol |> env.find? |>.get! |>.type - let test := LSpec.check symbol ((← serialize_expression_ast expr) = target) - return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' + let test := LSpec.check symbol ((serialize_expression_ast expr) = target) + return LSpec.TestSeq.append suites test) LSpec.TestSeq.done let coreM := metaM.run' let coreContext: Core.Context := { currNamespace := Lean.Name.str .anonymous "Aniva" From 4ffd226cace5610d9a0cbc46dcf611c09c26ab20 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 26 Oct 2023 11:22:02 -0700 Subject: [PATCH 06/10] test: m-coupled goals --- Pantograph/Goal.lean | 8 +++-- Test/Proofs.lean | 85 ++++++++++++++++++++++++++++++++------------ 2 files changed, 69 insertions(+), 24 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 4e57134..884b8a0 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -38,9 +38,13 @@ protected def GoalState.create (expr: Expr): M GoalState := do root, newMVars := SSet.insert .empty root, } -protected def GoalState.goals (goalState: GoalState): List MVarId := goalState.savedState.tactic.goals +protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals -private def GoalState.mctx (state: GoalState): MetavarContext := +protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do + state.savedState.term.restore + m + +protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k diff --git a/Test/Proofs.lean b/Test/Proofs.lean index d609dd4..a3d26fe 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -141,6 +141,37 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do return () +example (w x y z : Nat) (p : Nat → Prop) + (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by + simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at * + assumption +def proof_arith: TestM Unit := do + let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let (state1, goal) ← match ← state0.execute (goalId := 0) (tactic := "intros") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "1 root" state1.rootExpr.isNone + let (state2, goal) ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with + | .success state #[goal] => pure (state, goal) + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "2 root" state2.rootExpr.isNone + let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with + | .success state #[] => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "3 root" state3.rootExpr.isSome + return () -- Two ways to write the same theorem example: ∀ (p q: Prop), p ∨ q → q ∨ p := by @@ -218,7 +249,6 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - state4_1.print addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome return () @@ -234,25 +264,35 @@ def proof_or_comm: TestM Unit := do ] } ---example (w x y z : Nat) (p : Nat → Prop) --- (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by --- simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at * --- assumption ---def proof_arith_1: TestM Unit := do --- let goal? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") --- addTest $ LSpec.check "Start goal" goal?.isSome --- if let .some goal := goal? then --- if let .success #[(goal, _)] ← goal.execute "intros" then --- if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then --- if let .success #[] ← goal.execute "assumption" then --- return () --- else --- addTest $ assertUnreachable "assumption" --- else --- addTest $ assertUnreachable "simp ..." --- else --- addTest $ assertUnreachable "intros" --- +/-- M-coupled goals -/ +def proof_m_couple: TestM Unit := do + let state? ← startProof (.expr "(2: Nat) ≤ 5") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let (state1, goalL, goalR, goalM) ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + | .success state #[goalL, goalR, goalM] => pure (state, goalL, goalR, goalM) + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "2 ≤ ?m" (goalL.target.pp? = .some "2 ≤ ?m") + addTest $ LSpec.test "?m ≤ 5" (goalR.target.pp? = .some "?m ≤ 5") + addTest $ LSpec.test "Nat" (goalM.target.pp? = .some "Nat") + -- Set m to 3 + let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with + | .success state #[] => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state1b ← match state1.continue state2 with + | .ok state => pure state + | .error error => do + addTest $ assertUnreachable $ error + return () + state1b.print --def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do -- let goal? ← startProof (.expr "∀ (a b: Nat), a + b = b + a") -- addTest $ LSpec.check "Start goal" goal?.isSome @@ -278,8 +318,9 @@ def suite: IO LSpec.TestSeq := do let tests := [ ("Nat.add_comm", proof_nat_add_comm false), ("Nat.add_comm manual", proof_nat_add_comm true), - ("Or.comm", proof_or_comm) - --("arithmetic 1", proof_arith_1), + ("arithmetic", proof_arith), + ("Or.comm", proof_or_comm), + ("2 < 5", proof_m_couple) --("delta variable", proof_delta_variable) ] let tests ← tests.foldlM (fun acc tests => do From e98fb77f3361546c0dc838c38698715887368889 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 26 Oct 2023 22:47:42 -0700 Subject: [PATCH 07/10] refactor: Separate goal printing and processing Added a test for delta proof variables --- Pantograph.lean | 10 +-- Pantograph/Goal.lean | 75 +++---------------- Pantograph/Protocol.lean | 9 ++- Pantograph/Serial.lean | 72 ++++++++++++++++-- Test/Proofs.lean | 158 +++++++++++++++++++++++---------------- 5 files changed, 181 insertions(+), 143 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 0e74e81..29f9bd5 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -110,7 +110,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, printExprPretty := args.printExprPretty?.getD options.printExprPretty, printExprAST := args.printExprAST?.getD options.printExprAST, - proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta, + noRepeat := args.noRepeat?.getD options.noRepeat, printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps } @@ -148,14 +148,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match state.goalStates.get? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => - let result ← GoalState.execute goalState args.goalId args.tactic |>.run state.options - match result with - | .success nextGoalState goals => + match ← GoalState.execute goalState args.goalId args.tactic with + | .success nextGoalState => let (goalStates, nextStateId) := state.goalStates.insert nextGoalState set { state with goalStates } + let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) return .ok { nextStateId? := .some nextStateId, - goals? := .some goals + goals? := .some goals, } | .parseError message => return .ok { parseError? := .some message } diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 884b8a0..1f3f71a 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -1,8 +1,6 @@ import Lean import Pantograph.Symbol -import Pantograph.Serial -import Pantograph.Protocol def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := { @@ -21,6 +19,9 @@ structure GoalState where -- New metavariables acquired in this state newMVars: SSet MVarId + -- The id of the goal in the parent + parentGoalId: Nat := 0 + abbrev M := Elab.TermElabM protected def GoalState.create (expr: Expr): M GoalState := do @@ -49,6 +50,7 @@ protected def GoalState.mctx (state: GoalState): MetavarContext := private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k +/-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do @@ -71,7 +73,7 @@ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax /-- Response for executing a tactic -/ inductive TacticResult where -- Goes to next state - | success (state: GoalState) (goals: Array Protocol.Goal) + | success (state: GoalState) -- Tactic failed with messages | failure (messages: Array String) -- Could not parse tactic @@ -81,7 +83,7 @@ inductive TacticResult where /-- Execute tactic on given state -/ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String): - Protocol.OptionsT M TacticResult := do + M TacticResult := do let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure $ goal | .none => return .indexError goalId @@ -92,7 +94,6 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String (fileName := "") with | .ok stx => pure $ stx | .error error => return .parseError error - let options ← read match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with | .error errors => return .failure errors @@ -110,20 +111,12 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String else return acc.insert mvarId ) SSet.empty - let nextState: GoalState := { + return .success { savedState := nextSavedState root := state.root, newMVars, + parentGoalId := goalId, } - nextSavedState.term.restore - let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal - let goals ← nextGoals.mapM fun nextGoal => do - match (← MonadMCtx.getMCtx).findDecl? nextGoal with - | .some mvarDecl => - let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) - return serializedGoal - | .none => throwError s!"Parent mvar id does not exist {nextGoal.name}" - return .success nextState goals.toArray /-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState := @@ -150,57 +143,11 @@ protected def GoalState.rootExpr (goalState: GoalState): Option Expr := let expr := goalState.mctx.eAssignment.find! goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) if expr.hasMVar then + -- Must not assert that the goal state is empty here. We could be in a branch goal. + --assert! ¬goalState.goals.isEmpty .none else + assert! goalState.goals.isEmpty .some expr --- Diagnostics functions - -/-- Print the metavariables in a readable format -/ -protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): M Unit := do - let savedState := goalState.savedState - savedState.term.restore - let goals := savedState.tactic.goals - let mctx ← getMCtx - let root := goalState.root - -- Print the root - match mctx.decls.find? root with - | .some decl => printMVar ">" root decl - | .none => IO.println s!">{root.name}: ??" - goals.forM (fun mvarId => do - if mvarId != root then - match mctx.decls.find? mvarId with - | .some decl => printMVar "⊢" mvarId decl - | .none => IO.println s!"⊢{mvarId.name}: ??" - ) - let goals := goals.toSSet - mctx.decls.forM (fun mvarId decl => do - if goals.contains mvarId || mvarId == root then - pure () - -- Always print the root goal - else if mvarId == goalState.root then - printMVar (pref := ">") mvarId decl - -- Print the remainig ones that users don't see in Lean - else if options.printNonVisible then - let pref := if goalState.newMVars.contains mvarId then "~" else " " - printMVar pref mvarId decl - else - pure () - --IO.println s!" {mvarId.name}{userNameToString decl.userName}" - ) - where - printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do - if options.printContext then - decl.lctx.fvarIdToDecl.forM printFVar - let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) - IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" - if options.printValue then - if let Option.some value := (← getMCtx).eAssignment.find? mvarId then - IO.println s!" = {← Meta.ppExpr value}" - printFVar (fvarId: FVarId) (decl: LocalDecl): Elab.TermElabM Unit := do - IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}" - userNameToString : Name → String - | .anonymous => "" - | other => s!"[{other}]" - end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index a6bae29..1c05227 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -18,9 +18,10 @@ structure Options where printExprPretty: Bool := true -- When enabled, print the raw AST of expressions printExprAST: Bool := false - -- When enabled, the types and values of persistent variables in a proof goal - -- are not shown unless they are new to the proof step. Reduces overhead - proofVariableDelta: Bool := false + -- When enabled, the types and values of persistent variables in a goal + -- are not shown unless they are new to the proof step. Reduces overhead. + -- NOTE: that this assumes the type and assignment of variables can never change. + noRepeat: Bool := false -- See `pp.auxDecls` printAuxDecls: Bool := false -- See `pp.implementationDetailHyps` @@ -123,7 +124,7 @@ structure OptionsSet where printJsonPretty?: Option Bool printExprPretty?: Option Bool printExprAST?: Option Bool - proofVariableDelta?: Option Bool + noRepeat?: Option Bool printAuxDecls?: Option Bool printImplementationDetailHyps?: Option Bool deriving Lean.FromJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 99f95ef..87552eb 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -4,6 +4,7 @@ All serialisation functions import Lean import Pantograph.Protocol +import Pantograph.Goal namespace Pantograph open Lean @@ -173,12 +174,12 @@ def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String := def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp := toString (← Meta.ppExpr e) let pp?: Option String := match options.printExprPretty with - | true => .some pp - | false => .none + | true => .some pp + | false => .none let sexp: String := serialize_expression_ast e let sexp?: Option String := match options.printExprAST with - | true => .some sexp - | false => .none + | true => .some sexp + | false => .none return { pp?, sexp? @@ -239,7 +240,7 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe if skip then return acc else - let nameOnly := options.proofVariableDelta && (parentDecl?.map + let nameOnly := options.noRepeat && (parentDecl?.map (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false) let var ← match nameOnly with | true => ppVarNameOnly localDecl @@ -254,6 +255,67 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe where of_name (n: Name) := name_to_ast n (sanitize := false) +protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do + let goals := state.goals.toArray + state.savedState.term.meta.restore + let parentDecl? := parent.bind (λ parentState => + let parentGoal := parentState.goals.get! state.parentGoalId + parentState.mctx.findDecl? parentGoal) + goals.mapM fun goal => do + if options.noRepeat then + let key := if parentDecl?.isSome then "is some" else "is none" + IO.println s!"goal: {goal.name}, {key}" + match state.mctx.findDecl? goal with + | .some mvarDecl => + let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) + pure serializedGoal + | .none => throwError s!"Metavariable does not exist in context {goal.name}" +/-- Print the metavariables in a readable format -/ +protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): MetaM Unit := do + let savedState := goalState.savedState + savedState.term.meta.restore + let goals := savedState.tactic.goals + let mctx ← getMCtx + let root := goalState.root + -- Print the root + match mctx.decls.find? root with + | .some decl => printMVar ">" root decl + | .none => IO.println s!">{root.name}: ??" + goals.forM (fun mvarId => do + if mvarId != root then + match mctx.decls.find? mvarId with + | .some decl => printMVar "⊢" mvarId decl + | .none => IO.println s!"⊢{mvarId.name}: ??" + ) + let goals := goals.toSSet + mctx.decls.forM (fun mvarId decl => do + if goals.contains mvarId || mvarId == root then + pure () + -- Always print the root goal + else if mvarId == goalState.root then + printMVar (pref := ">") mvarId decl + -- Print the remainig ones that users don't see in Lean + else if options.printNonVisible then + let pref := if goalState.newMVars.contains mvarId then "~" else " " + printMVar pref mvarId decl + else + pure () + --IO.println s!" {mvarId.name}{userNameToString decl.userName}" + ) + where + printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do + if options.printContext then + decl.lctx.fvarIdToDecl.forM printFVar + let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) + IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" + if options.printValue then + if let Option.some value := (← getMCtx).eAssignment.find? mvarId then + IO.println s!" = {← Meta.ppExpr value}" + printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do + IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}" + userNameToString : Name → String + | .anonymous => "" + | other => s!"[{other}]" end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a3d26fe..79f0f38 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -9,7 +9,7 @@ import Test.Common namespace Pantograph def TacticResult.toString : TacticResult → String - | .success _ goals => s!".success ({goals.size} goals)" + | .success state => s!".success ({state.goals.length} goals)" | .failure messages => let messages := "\n".intercalate messages.toList s!".failure {messages}" @@ -75,16 +75,6 @@ def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goa isInaccessible? := .some false })).toArray } --- Like `buildGoal` but allow certain variables to be elided. -def buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal := - { - target := { pp? := .some target}, - vars := (nameType.map fun x => ({ - userName := x.fst, - type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := x.snd.map (λ _ => false) - })).toArray - } def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options @@ -120,12 +110,13 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let (state1, goal1) ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with - | .success state #[goal] => pure (state, goal) + let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "intro n m" (goal1.devolatilize = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") + addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"]) match ← state1.execute (goalId := 0) (tactic := "assumption") with | .failure #[message] => @@ -134,12 +125,49 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do addTest $ assertUnreachable $ other.toString let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with - | .success state #[] => pure state + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty return () +def proof_delta_variable: TestM Unit := do + let options: Protocol.Options := { noRepeat := true } + let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a" + addTest $ LSpec.check "Start goal" state?.isSome + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) = + #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"]) + let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) = + #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"]) + return () + where +-- Like `buildGoal` but allow certain variables to be elided. + buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal := + { + target := { pp? := .some target}, + vars := (nameType.map fun x => ({ + userName := x.fst, + type? := x.snd.map (λ type => { pp? := type }), + isInaccessible? := x.snd.map (λ _ => false) + })).toArray + } example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by @@ -153,23 +181,26 @@ def proof_arith: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let (state1, goal) ← match ← state0.execute (goalId := 0) (tactic := "intros") with - | .success state #[goal] => pure (state, goal) + let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "1 root" state1.rootExpr.isNone - let (state2, goal) ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with - | .success state #[goal] => pure (state, goal) + addTest $ LSpec.check "intros" (state1.goals.length = 1) + addTest $ LSpec.test "1 root" state1.rootExpr.isNone + let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "simp ..." (state2.goals.length = 1) addTest $ LSpec.check "2 root" state2.rootExpr.isNone let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with - | .success state #[] => pure state + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.test "assumption" state3.goals.isEmpty addTest $ LSpec.check "3 root" state3.rootExpr.isSome return () @@ -196,59 +227,66 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let (state1, goal1) ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with - | .success state #[goal] => pure (state, goal) + let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "p q h" (goal1.devolatilize = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p") - let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with - | .success state #[goal1, goal2] => pure (state, goal1, goal2) + addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) + let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "cases h/1" (goal1.devolatilize = branchGoal "inl" "p") - addTest $ LSpec.check "cases h/2" (goal2.devolatilize = branchGoal "inr" "q") + addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[branchGoal "inl" "p", branchGoal "inr" "q"]) - let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with - | .success state #[goal] => pure (state, goal) + let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with - | .success state #[] => pure state + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - let (state3_2, _goal) ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with - | .success state #[goal] => pure (state, goal) + addTest $ LSpec.check "· assumption" state4_1.goals.isEmpty + addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isNone + let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1) let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with - | .success state #[] => pure state + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - - addTest $ LSpec.check "4_2 root" state4_2.rootExpr.isNone + addTest $ LSpec.check "· assumption" state4_2.goals.isEmpty + addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr.isNone -- Ensure the proof can continue from `state4_2`. let state2b ← match state2.continue state4_2 with | .error msg => do addTest $ assertUnreachable $ msg return () | .ok state => pure state - addTest $ LSpec.test "state2b" (state2b.goals == [state2.goals.get! 0]) - let (state3_1, _goal) ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with - | .success state #[goal] => pure (state, goal) + addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0]) + let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with - | .success state #[] => pure state + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "· assumption" state4_1.goals.isEmpty addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome return () @@ -273,41 +311,30 @@ def proof_m_couple: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let (state1, goalL, goalR, goalM) ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with - | .success state #[goalL, goalR, goalM] => pure (state, goalL, goalR, goalM) + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.test "2 ≤ ?m" (goalL.target.pp? = .some "2 ≤ ?m") - addTest $ LSpec.test "?m ≤ 5" (goalR.target.pp? = .some "?m ≤ 5") - addTest $ LSpec.test "Nat" (goalM.target.pp? = .some "Nat") + addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone -- Set m to 3 let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with - | .success state #[] => pure state + | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.test "(1b root)" state2.rootExpr.isNone let state1b ← match state1.continue state2 with - | .ok state => pure state - | .error error => do - addTest $ assertUnreachable $ error + | .error msg => do + addTest $ assertUnreachable $ msg return () - state1b.print ---def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do --- let goal? ← startProof (.expr "∀ (a b: Nat), a + b = b + a") --- addTest $ LSpec.check "Start goal" goal?.isSome --- if let .some goal := goal? then --- if let .success #[(goal, sGoal)] ← goal.execute "intro n" then --- let sGoal1e: Protocol.Goal :=buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" --- addTest $ LSpec.check "intro n" (sGoal = sGoal1e) --- --- if let .success #[(_, sGoal)] ← goal.execute "intro m" then --- let sGoal2e: Protocol.Goal :=buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n" --- addTest $ LSpec.check "intro m" (sGoal = sGoal2e) --- else --- addTest $ assertUnreachable "intro m" --- else --- addTest $ assertUnreachable "intro n" + | .ok state => pure state + addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ 3", .some "3 ≤ 5"]) + addTest $ LSpec.test "(2 root)" state1b.rootExpr.isNone + return () /-- Tests the most basic form of proofs whose goals do not relate to each other -/ def suite: IO LSpec.TestSeq := do @@ -318,6 +345,7 @@ def suite: IO LSpec.TestSeq := do let tests := [ ("Nat.add_comm", proof_nat_add_comm false), ("Nat.add_comm manual", proof_nat_add_comm true), + ("Nat.add_comm delta", proof_delta_variable), ("arithmetic", proof_arith), ("Or.comm", proof_or_comm), ("2 < 5", proof_m_couple) From b381d89ff93f5fa94ccc161ce70f5f22e3ac2dcb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 27 Oct 2023 15:15:22 -0700 Subject: [PATCH 08/10] feat: Assigning a goal with an expression --- Pantograph/Goal.lean | 67 +++++++++++++++++++++++++++++++++++----- Pantograph/Protocol.lean | 3 +- Pantograph/Serial.lean | 5 +-- Test/Proofs.lean | 61 +++++++++++++++++++++++++++++------- 4 files changed, 112 insertions(+), 24 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 1f3f71a..3be34ad 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -47,13 +47,15 @@ protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx +protected def GoalState.env (state: GoalState): Environment := + state.savedState.term.meta.core.env private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : - M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do - let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do + M (Except (Array String) Elab.Tactic.SavedState):= do + let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do state.restore Elab.Tactic.setGoals [goal] try @@ -63,9 +65,7 @@ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax let errors ← (messages.map Message.data).mapM fun md => md.toString return .error errors else - let unsolved ← Elab.Tactic.getUnsolvedGoals - -- The order of evaluation is important here, since `getUnsolvedGoals` prunes the goals set - return .ok (← MonadBacktrack.saveState, unsolved) + return .ok (← MonadBacktrack.saveState) catch exception => return .error #[← exception.toMessageData.toString] tacticM tactic { elaborator := .anonymous } |>.run' state.tactic @@ -97,8 +97,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with | .error errors => return .failure errors - | .ok (nextSavedState, nextGoals) => - assert! nextSavedState.tactic.goals.length == nextGoals.length + | .ok nextSavedState => -- Assert that the definition of metavariables are the same let nextMCtx := nextSavedState.term.meta.meta.mctx let prevMCtx := state.savedState.term.meta.meta.mctx @@ -112,12 +111,64 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String return acc.insert mvarId ) SSet.empty return .success { + state with savedState := nextSavedState - root := state.root, newMVars, parentGoalId := goalId, } +protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let expr ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := expr) + (fileName := "") with + | .ok syn => pure syn + | .error error => return .parseError error + let tacticM: Elab.Tactic.TacticM TacticResult := do + state.savedState.restore + Elab.Tactic.setGoals [goal] + try + let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none) + -- Attempt to unify the expression + let goalType ← goal.getType + let exprType ← Meta.inferType expr + if !(← Meta.isDefEq goalType exprType) then + return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)] + goal.checkNotAssigned `GoalState.tryAssign + goal.assign expr + if (← getThe Core.State).messages.hasErrors then + let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray + let errors ← (messages.map Message.data).mapM fun md => md.toString + return .failure errors + else + let prevMCtx := state.savedState.term.meta.meta.mctx + let nextMCtx ← getMCtx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return mvarId :: acc + ) [] + -- The new goals are the newMVars that lack an assignment + Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned))) + let nextSavedState ← MonadBacktrack.saveState + return .success { + state with + savedState := nextSavedState, + newMVars := newMVars.toSSet, + parentGoalId := goalId, + } + catch exception => + return .failure #[← exception.toMessageData.toString] + tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + /-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState := if target.root != graftee.root then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 1c05227..b0e7744 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -172,7 +172,8 @@ structure GoalPrint where printContext: Bool := true printValue: Bool := true printNewMVars: Bool := false - printNonVisible: Bool := false + -- Print all mvars + printAll: Bool := false end Pantograph.Protocol diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 87552eb..1a07444 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -262,9 +262,6 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt let parentGoal := parentState.goals.get! state.parentGoalId parentState.mctx.findDecl? parentGoal) goals.mapM fun goal => do - if options.noRepeat then - let key := if parentDecl?.isSome then "is some" else "is none" - IO.println s!"goal: {goal.name}, {key}" match state.mctx.findDecl? goal with | .some mvarDecl => let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) @@ -296,7 +293,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrin else if mvarId == goalState.root then printMVar (pref := ">") mvarId decl -- Print the remainig ones that users don't see in Lean - else if options.printNonVisible then + else if options.printAll then let pref := if goalState.newMVars.contains mvarId then "~" else " " printMVar pref mvarId decl else diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 79f0f38..809cf50 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -66,8 +66,9 @@ def startProof (start: Start): TestM (Option GoalState) := do def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false -def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goal := +def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal := { + caseName?, target := { pp? := .some target}, vars := (nameType.map fun x => ({ userName := x.fst, @@ -187,21 +188,21 @@ def proof_arith: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "intros" (state1.goals.length = 1) - addTest $ LSpec.test "1 root" state1.rootExpr.isNone + addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "simp ..." (state2.goals.length = 1) - addTest $ LSpec.check "2 root" state2.rootExpr.isNone + addTest $ LSpec.check "(2 root)" state2.rootExpr.isNone let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.test "assumption" state3.goals.isEmpty - addTest $ LSpec.check "3 root" state3.rootExpr.isSome + addTest $ LSpec.check "(3 root)" state3.rootExpr.isSome return () -- Two ways to write the same theorem @@ -253,7 +254,7 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "· assumption" state4_1.goals.isEmpty + addTest $ LSpec.check " assumption" state4_1.goals.isEmpty addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isNone let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state @@ -266,7 +267,7 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "· assumption" state4_2.goals.isEmpty + addTest $ LSpec.check " assumption" state4_2.goals.isEmpty addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr.isNone -- Ensure the proof can continue from `state4_2`. let state2b ← match state2.continue state4_2 with @@ -286,8 +287,8 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "· assumption" state4_1.goals.isEmpty - addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome + addTest $ LSpec.check " assumption" state4_1.goals.isEmpty + addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isSome return () where @@ -336,7 +337,45 @@ def proof_m_couple: TestM Unit := do addTest $ LSpec.test "(2 root)" state1b.rootExpr.isNone return () -/-- Tests the most basic form of proofs whose goals do not relate to each other -/ +def proof_proposition_generation: TestM Unit := do + let state? ← startProof (.expr "Σ' p:Prop, p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + buildGoal [] "?fst" (caseName? := .some "snd"), + buildGoal [] "Prop" (caseName? := .some "fst") + ]) + addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone + + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) + addTest $ LSpec.test "(2 root)" state2.rootExpr.isNone + + let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = + #[]) + addTest $ LSpec.test "(3 root)" state3.rootExpr.isSome + return () + def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}]) @@ -348,8 +387,8 @@ def suite: IO LSpec.TestSeq := do ("Nat.add_comm delta", proof_delta_variable), ("arithmetic", proof_arith), ("Or.comm", proof_or_comm), - ("2 < 5", proof_m_couple) - --("delta variable", proof_delta_variable) + ("2 < 5", proof_m_couple), + ("Proposition Generation", proof_proposition_generation) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests From 82f5494718b6b9383512451baf2ef80833c503f0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 27 Oct 2023 15:32:59 -0700 Subject: [PATCH 09/10] feat: Add REPL command for assigning an expression --- Pantograph.lean | 24 +++++++++++++++--------- Pantograph/Protocol.lean | 4 +++- Test/Integration.lean | 21 ++++++++++++++++++++- 3 files changed, 38 insertions(+), 11 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 29f9bd5..dd25e9f 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -133,9 +133,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do (match env.find? <| str_to_name copyFrom with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .some cInfo => return .ok cInfo.type) - | .none, .none => - return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied" - | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}") + | _, _ => + return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") match expr? with | .error error => return .error error | .ok expr => @@ -147,9 +146,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get match state.goalStates.get? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" - | .some goalState => - match ← GoalState.execute goalState args.goalId args.tactic with - | .success nextGoalState => + | .some goalState => do + let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with + | .some tactic, .none => do + pure ( Except.ok (← GoalState.execute goalState args.goalId tactic)) + | .none, .some expr => do + pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr)) + | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") + match nextGoalState? with + | .error error => return .error error + | .ok (.success nextGoalState) => let (goalStates, nextStateId) := state.goalStates.insert nextGoalState set { state with goalStates } let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) @@ -157,11 +163,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do nextStateId? := .some nextStateId, goals? := .some goals, } - | .parseError message => + | .ok (.parseError message) => return .ok { parseError? := .some message } - | .indexError goalId => + | .ok (.indexError goalId) => return .error $ errorIndex s!"Invalid goal id index {goalId}" - | .failure messages => + | .ok (.failure messages) => return .ok { tacticErrors? := .some messages } goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do let state ← get diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index b0e7744..62700c4 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -146,7 +146,9 @@ structure GoalTactic where -- Identifiers for tree, state, and goal stateId: Nat goalId: Nat := 0 - tactic: String + -- One of the fields here must be filled + tactic?: Option String := .none + expr?: Option String := .none deriving Lean.FromJson structure GoalTacticResult where -- The next goal state id. Existence of this field shows success diff --git a/Test/Integration.lean b/Test/Integration.lean index b7a5e62..39f145e 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -82,12 +82,31 @@ def test_malformed_command : IO LSpec.TestSeq := error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}: Protocol.InteractionError)) ] +def test_tactic : IO LSpec.TestSeq := + let goal: Protocol.Goal := { + target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, + vars := #[{ name := "_uniq 9", userName := "x", 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}: + Protocol.GoalStartResult)), + subroutine_step "goal.tactic" + [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] + (Lean.toJson ({ + nextStateId? := .some 1, + goals? := #[goal], + }: + Protocol.GoalTacticResult)) + ] def suite: IO LSpec.TestSeq := do return LSpec.group "Integration" $ (LSpec.group "Option modify" (← test_option_modify)) ++ - (LSpec.group "Malformed command" (← test_malformed_command)) + (LSpec.group "Malformed command" (← test_malformed_command)) ++ + (LSpec.group "Tactic" (← test_tactic)) end Pantograph.Test.Integration From 427d819349ed5ece7e0904f5485323452ab48b09 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 27 Oct 2023 15:41:12 -0700 Subject: [PATCH 10/10] feat: Add REPL function for root expression --- Pantograph.lean | 10 ++++++++++ Pantograph/Goal.lean | 2 +- Pantograph/Protocol.lean | 9 +++++++++ Pantograph/Serial.lean | 2 +- README.md | 5 +++-- Test/Proofs.lean | 24 ++++++++++++------------ 6 files changed, 36 insertions(+), 16 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index dd25e9f..00782d5 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -39,6 +39,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "goal.start" => run goal_start | "goal.tactic" => run goal_tactic | "goal.delete" => run goal_delete + | "goal.print" => run goal_print | cmd => let error: Protocol.InteractionError := errorCommand s!"Unknown command {cmd}" @@ -174,5 +175,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates set { state with goalStates } return .ok {} + goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do + let state ← get + match state.goalStates.get? args.stateId with + | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" + | .some goalState => do + let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) + return .ok { + root?, + } end Pantograph diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3be34ad..78a4194 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -190,7 +190,7 @@ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Excep newMVars := graftee.newMVars, } -protected def GoalState.rootExpr (goalState: GoalState): Option Expr := +protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := let expr := goalState.mctx.eAssignment.find! goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) if expr.hasMVar then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 62700c4..e379782 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -171,6 +171,15 @@ structure GoalDeleteResult where deriving Lean.ToJson structure GoalPrint where + stateId: Nat + deriving Lean.FromJson +structure GoalPrintResult where + -- The root expression + root?: Option Expression + deriving Lean.ToJson + +-- Diagnostic Options, not available in REPL +structure GoalDiag where printContext: Bool := true printValue: Bool := true printNewMVars: Bool := false diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 1a07444..62321bd 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -269,7 +269,7 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt | .none => throwError s!"Metavariable does not exist in context {goal.name}" /-- Print the metavariables in a readable format -/ -protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): MetaM Unit := do +protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do let savedState := goalState.savedState savedState.term.meta.restore let goals := savedState.tactic.goals diff --git a/README.md b/README.md index 442b57d..0c19a3a 100644 --- a/README.md +++ b/README.md @@ -76,8 +76,9 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va have to be set via command line arguments.), for options, see `Pantograph/Commands.lean` - `options.print`: Display the current set of options - `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol -- `goal.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given goal -- `goal.remove {"goalIds": []}"`: Remove a bunch of stored goals. +- `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": ]}`: Execute a tactic string on a given goal +- `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. +- `goal.print {"stateId": }"`: Print a goal state - `stat`: Display resource usage ## Errors diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 809cf50..a726627 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -188,21 +188,21 @@ def proof_arith: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "intros" (state1.goals.length = 1) - addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "simp ..." (state2.goals.length = 1) - addTest $ LSpec.check "(2 root)" state2.rootExpr.isNone + addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.test "assumption" state3.goals.isEmpty - addTest $ LSpec.check "(3 root)" state3.rootExpr.isSome + addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome return () -- Two ways to write the same theorem @@ -255,7 +255,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty - addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isNone + addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state | other => do @@ -268,7 +268,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_2.goals.isEmpty - addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr.isNone + addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone -- Ensure the proof can continue from `state4_2`. let state2b ← match state2.continue state4_2 with | .error msg => do @@ -288,7 +288,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty - addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isSome + addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome return () where @@ -319,14 +319,14 @@ def proof_m_couple: TestM Unit := do return () addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) - addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone -- Set m to 3 let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.test "(1b root)" state2.rootExpr.isNone + addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone let state1b ← match state1.continue state2 with | .error msg => do addTest $ assertUnreachable $ msg @@ -334,7 +334,7 @@ def proof_m_couple: TestM Unit := do | .ok state => pure state addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ 3", .some "3 ≤ 5"]) - addTest $ LSpec.test "(2 root)" state1b.rootExpr.isNone + addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone return () def proof_proposition_generation: TestM Unit := do @@ -355,7 +355,7 @@ def proof_proposition_generation: TestM Unit := do buildGoal [] "?fst" (caseName? := .some "snd"), buildGoal [] "Prop" (caseName? := .some "fst") ]) - addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with | .success state => pure state @@ -364,7 +364,7 @@ def proof_proposition_generation: TestM Unit := do return () addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) - addTest $ LSpec.test "(2 root)" state2.rootExpr.isNone + addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with | .success state => pure state @@ -373,7 +373,7 @@ def proof_proposition_generation: TestM Unit := do return () addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = #[]) - addTest $ LSpec.test "(3 root)" state3.rootExpr.isSome + addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome return () def suite: IO LSpec.TestSeq := do