From 9447d29e379d26c61db5e1903f351f14510dda34 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Oct 2023 17:15:23 -0700 Subject: [PATCH] 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" }) ]