diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 81575ed3..bc2dff1e 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -5,10 +5,42 @@ Authors: Scott Morrison -/ import Lean.Elab.Frontend -open Lean Elab +open Lean Elab Language namespace Lean.Elab.IO +partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext) + (parserState : Parser.ModuleParserState) (commandState : Command.State) + (old? : Option IncrementalState) : + BaseIO (List (IncrementalState × Option InfoTree)) := do + let task ← Language.Lean.processCommands inputCtx parserState commandState + (old?.map fun old => (old.inputCtx, old.initialSnap)) + return go task.get task #[] +where + go initialSnap t commands := + let snap := t.get + let commands := commands.push snap + -- Opting into reuse also enables incremental reporting, so make sure to collect messages from + -- all snapshots + let messages := toSnapshotTree initialSnap + |>.getAll.map (·.diagnostics.msgLog) + |>.foldl (· ++ ·) {} + -- In contrast to messages, we should collect info trees only from the top-level command + -- snapshots as they subsume any info trees reported incrementally by their children. + let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray' + let result : (IncrementalState × Option InfoTree) := + ({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees } + , parserState := snap.parserState + , cmdPos := snap.parserState.pos + , commands := commands.map (·.stx) + , inputCtx := inputCtx + , initialSnap := initialSnap + }, snap.elabSnap.infoTreeSnap.get.infoTree?) + if let some next := snap.nextCmdSnap? then + result :: go initialSnap next.task commands + else + [result] + /-- Wrapper for `IO.processCommands` that enables info states, and returns * the new command state @@ -17,41 +49,36 @@ Wrapper for `IO.processCommands` that enables info states, and returns -/ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) - (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do + (commandState : Command.State) (incrementalState? : Option IncrementalState := none) + : IO (List (IncrementalState × Option InfoTree) × List Message) := do let commandState := { commandState with infoState.enabled := true } - let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState - pure (s, s.messages.toList, s.infoState.trees.toList) + let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState? + pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {}) /-- Process some text input, with or without an existing command state. -If there is no existing environment, we parse the input for headers (e.g. import statements), -and create a new environment. -Otherwise, we add to the existing environment. Returns: -1. The header-only command state (only useful when cmdState? is none) -2. The resulting command state after processing the entire input -3. List of messages -4. List of info trees +1. The resulting command state after processing the entire input +2. List of messages +3. List of info trees along with Command.State from the incremental processing -/ def processInput (input : String) (cmdState? : Option Command.State) (opts : Options := {}) (fileName : Option String := none) : - IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do + IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do Lean.initSearchPath (← Lean.findSysroot) enableInitializersExecution let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName - match cmdState? with | none => do -- Split the processing into two phases to prevent self-reference in proofs in tactic mode let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← processHeader header opts messages inputCtx let headerOnlyState := Command.mkState env messages opts - let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState - return (headerOnlyState, cmdState, messages, trees) - + let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState + return (headerOnlyState, incStates) | some cmdStateBefore => do let parserState : Parser.ModuleParserState := {} - let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore - return (cmdStateBefore, cmdStateAfter, messages, trees) + let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore + return (cmdStateBefore, incStates) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ebec4c56..fa44e2a8 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -47,7 +47,7 @@ deriving ToJson, FromJson structure Pos where line : Nat column : Nat -deriving ToJson, FromJson +deriving ToJson, FromJson, BEq, Hashable /-- Severity of a message. -/ inductive Severity diff --git a/REPL/Main.lean b/REPL/Main.lean index b05583f7..078c44b5 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op fun ⟨ctx, g, pos, endPos⟩ => do let (goal, proofState) ← match g with | .tactic g => do - let lctx ← ctx.runMetaM {} do - match ctx.mctx.findDecl? g with - | some decl => return decl.lctx - | none => throwError "unknown metavariable '{g}'" - let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals? + let s ← ProofSnapshot.create ctx none env? [g] rootGoals? pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term lctx (some t) => do let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t] @@ -115,6 +111,16 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goal pos endPos proofStateId +def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) +(rootGoals? : Option (List MVarId)) +: M m (List Sorry) := + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let s ← sorries infoTree?.toList prevEnv rootGoals? + let restSorries ← sorriesCmd rest state.commandState.env rootGoals? + return s ++ restSorries + def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try Lean.PrettyPrinter.ppTactic ⟨stx⟩ @@ -130,6 +136,14 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact let proofStateId ← proofState.mapM recordProofSnapshot return Tactic.of goals tactic pos endPos proofStateId ns +def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let ts ← tactics infoTree?.toList prevEnv + let restTactics ← tacticsCmd rest state.commandState.env + return ts ++ restTactics + def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do @@ -138,6 +152,14 @@ def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment let proofStateId ← proofState.mapM recordProofSnapshot return Sorry.of goals pos pos proofStateId +def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : + M m (List Sorry) := do + match treeList with + | [] => pure [] + | (state, infoTree?) :: rest => do + let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv + let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env + return sorries ++ restSorries private def collectFVarsAux : Expr → NameSet | .fvar fvarId => NameSet.empty.insert fvarId.name @@ -197,7 +219,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do unless (← Meta.isDefEq pft expectedType) do return s!"Error: proof has type {pft} but root goal has type {expectedType}" - let pf ← abstractAllLambdaFVars pf + let pf ← abstractAllLambdaFVars pf >>= instantiateMVars let pft ← Meta.inferType pf >>= instantiateMVars if pf.hasExprMVar then @@ -302,19 +324,19 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do if notFound then return .inr ⟨"Unknown environment."⟩ let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState - let (initialCmdState, cmdState, messages, trees) ← try + let (initialCmdState, incStates, messages) ← try IO.processInput s.cmd initialCmdState? catch ex => return .inr ⟨ex.toString⟩ + + let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState let messages ← messages.mapM fun m => Message.of m - -- For debugging purposes, sometimes we print out the trees here: - -- trees.forM fun t => do IO.println (← t.format) - let sorries ← sorries trees initialCmdState.env none + let sorries ← sorriesCmd incStates initialCmdState.env none let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env)) + | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env)) | _ => pure sorries let tactics ← match s.allTactics with - | some true => tactics trees initialCmdState.env + | some true => tacticsCmd incStates initialCmdState.env | _ => pure [] let cmdSnapshot := { cmdState @@ -324,6 +346,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do snap? := none, cancelTk? := none } } let env ← recordCommandSnapshot cmdSnapshot + let trees := cmdState.infoState.trees.toList + -- For debugging purposes, sometimes we print out the trees here: + -- trees.forM fun t => do IO.println (← t.format) let jsonTrees := match s.infotree with | some "full" => trees | some "tactics" => trees.flatMap InfoTree.retainTacticInfo diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index f6936245..d87981e6 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := /-- Pretty print the current goals in the `ProofSnapshot`. -/ def ppGoals (p : ProofSnapshot) : IO (List Format) := Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·) + /-- Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals. - For convenience, we also allow a list of `Expr`s, and these are appended to the goals as fresh metavariables with the given types. -/ -def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) +def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment) (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := []) : IO ProofSnapshot := do - ctx.runMetaM (lctx?.getD {}) do - let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) - let s ← getThe Core.State - let s := match env? with - | none => s - | some env => { s with env } - pure <| - { coreState := s - coreContext := ← readThe Core.Context - metaState := ← getThe Meta.State - metaContext := ← readThe Meta.Context - termState := {} - termContext := {} - tacticState := { goals } - tacticContext := { elaborator := .anonymous } - rootGoals := match rootGoals? with - | none => goals - | some gs => gs } + -- Get the local context from the goals if not provided. + let lctx ← match lctx? with + | none => match goals with + | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx + | [] => match rootGoals? with + | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx + | _ => pure {} + | some lctx => pure lctx + + ctx.runMetaM lctx do + -- update local instances, which is necessary when `types` is non-empty + Meta.withLocalInstances (lctx.decls.toList.filterMap id) do + let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) + let s ← getThe Core.State + let s := match prevEnv? with + | none => s + | some env => { s with env } + pure <| + { coreState := s + coreContext := ← readThe Core.Context + metaState := ← getThe Meta.State + metaContext := ← readThe Meta.Context + termState := {} + termContext := {} + tacticState := { goals } + tacticContext := { elaborator := .anonymous } + rootGoals := match rootGoals? with + | none => goals + | some gs => gs } open Lean.Core in /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/ diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out new file mode 100644 index 00000000..e22d70ba --- /dev/null +++ b/test/in_command_dependency.expected.out @@ -0,0 +1,45 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 26}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}, + {"severity": "info", + "pos": {"line": 2, "column": 22}, + "endPos": {"line": 2, "column": 28}, + "data": "Try this:\n [apply] exact x"}], + "env": 0} + +{"sorries": + [{"proofState": 1, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 26}}, + {"proofState": 2, + "pos": {"line": 2, "column": 19}, + "goal": "⊢ False", + "endPos": {"line": 2, "column": 24}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}, + {"severity": "warning", + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"proofStatus": "Completed", + "proofState": 3, + "messages": + [{"severity": "info", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "Try this:\n [apply] exact x"}], + "goals": []} + diff --git a/test/in_command_dependency.in b/test/in_command_dependency.in new file mode 100644 index 00000000..78c0b6a9 --- /dev/null +++ b/test/in_command_dependency.in @@ -0,0 +1,6 @@ +{"cmd": "theorem x : False := sorry\nexample : False := by exact?"} + +{"cmd": "theorem x : False := sorry\nexample : False := sorry"} + +{"proofState": 2, "tactic": "exact?"} + diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out new file mode 100644 index 00000000..5a93d082 --- /dev/null +++ b/test/local_instance_proof.expected.out @@ -0,0 +1,62 @@ +{"env": 0} + +{"env": 1} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 42}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 47}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 2} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + +{"sorries": + [{"proofState": 2, + "pos": {"line": 1, "column": 45}, + "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 50}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 3} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"env": 4} + +{"sorries": + [{"proofState": 4, + "pos": {"line": 1, "column": 17}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 22}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 5} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + +{"sorries": + [{"proofState": 6, + "pos": {"line": 1, "column": 20}, + "goal": "α : Type\ns : Inhabited α\n⊢ α", + "endPos": {"line": 1, "column": 25}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 9}, + "data": "declaration uses 'sorry'"}], + "env": 6} + +{"proofStatus": "Completed", "proofState": 7, "goals": []} + diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in new file mode 100644 index 00000000..eeefd5ef --- /dev/null +++ b/test/local_instance_proof.in @@ -0,0 +1,21 @@ +{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 0} + +{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0} + +{"tactic": "exact test α", "proofState": 2} + +{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0} + +{"cmd": "def test2 : α := sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 4} + +{"cmd": "def test2 : α := by sorry", "env": 4} + +{"tactic": "exact test α", "proofState": 6}