diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 81575ed3..f8e70a59 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -19,8 +19,9 @@ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do let commandState := { commandState with infoState.enabled := true } + let oldMessages := commandState.messages.toList let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState - pure (s, s.messages.toList, s.infoState.trees.toList) + pure (s, oldMessages ++ s.messages.toList, s.infoState.trees.toList) /-- Process some text input, with or without an existing command state. diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 24db8402..4f1f2f70 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -6,6 +6,9 @@ Authors: Scott Morrison import Lean.Data.Json import Lean.Message import Lean.Elab.InfoTree.Main +import Lean.Meta.Basic +import Lean.Meta.CollectMVars +import REPL.Lean.InfoTree.ToJson open Lean Elab InfoTree @@ -19,6 +22,7 @@ structure CommandOptions where Anything else is ignored. -/ infotree : Option String + proofTrees : Option Bool := none /-- Run Lean commands. If `env = none`, starts a new session (in which you can use `import`). @@ -34,6 +38,11 @@ structure File extends CommandOptions where path : System.FilePath deriving FromJson +structure PruneSnapshots where + cmdFromId : Option Nat + proofFromId : Option Nat +deriving ToJson, FromJson + /-- Run a tactic in a proof state. -/ @@ -71,11 +80,29 @@ def Message.of (m : Lean.Message) : IO Message := do pure <| | .error => .error, data := (← m.data.toString).trim } +structure HypothesisInfo where + username : String + type : String + value : Option String + -- unique identifier for the hypothesis, fvarId + id : String + isProof : String + deriving Inhabited, ToJson, FromJson + +structure GoalInfo where + username : String + type : String + hyps : List HypothesisInfo + -- unique identifier for the goal, mvarId + id : MVarId + deriving Inhabited, ToJson, FromJson + /-- A Lean `sorry`. -/ structure Sorry where pos : Pos endPos : Pos goal : String + goalInfo: Option GoalInfo /-- The index of the proof state at the sorry. You can use the `ProofStep` instruction to run a tactic at this state. @@ -86,16 +113,20 @@ deriving FromJson instance : ToJson Sorry where toJson r := Json.mkObj <| .flatten [ [("goal", r.goal)], + match r.goalInfo with + | some goalInfo => [("goalInfo", toJson goalInfo)] + | none => [], [("proofState", toJson r.proofState)], if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [], if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [], ] /-- Construct the JSON representation of a Lean sorry. -/ -def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry := +def Sorry.of (goal : String) (goalInfo : Option GoalInfo) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry := { pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, goal, + goalInfo, proofState } structure Tactic where @@ -116,6 +147,83 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : proofState, usedConstants } +private def mayBeProof (expr : Expr) : MetaM String := do + let type : Expr ← Lean.Meta.inferType expr + if ← Meta.isProof expr then + return "proof" + if type.isSort then + return "universe" + else + return "data" + +def printGoalInfo (printCtx : ContextInfo) (id : MVarId) : IO GoalInfo := do + let some decl := printCtx.mctx.findDecl? id + | panic! "printGoalInfo: goal not found in the mctx" + -- to get tombstones in name ✝ for unreachable hypothesis + let lctx := decl.lctx |>.sanitizeNames.run' {options := {}} + let ppContext := printCtx.toPPContext lctx + + let hyps ← lctx.foldrM (init := []) (fun hypDecl acc => do + if hypDecl.isAuxDecl || hypDecl.isImplementationDetail then + return acc + + let type ← liftM (ppExprWithInfos ppContext hypDecl.type) + let value ← liftM (hypDecl.value?.mapM (ppExprWithInfos ppContext)) + let isProof : String ← printCtx.runMetaM decl.lctx (mayBeProof hypDecl.toExpr) + return ({ + username := hypDecl.userName.toString, + type := type.fmt.pretty, + value := value.map (·.fmt.pretty), + id := hypDecl.fvarId.name.toString, + isProof := isProof, + } : HypothesisInfo) :: acc) + return ⟨ decl.userName.toString, (← ppExprWithInfos ppContext decl.type).fmt.pretty, hyps, id⟩ + + +instance : BEq GoalInfo where + beq g1 g2 := g1.id == g2.id + +instance : Hashable GoalInfo where + hash g := hash g.id +structure MetavarDecl.Json where + mvarId : String + userName : String + type : String + mvarsInType : List MVarId + value : Option String +deriving ToJson, FromJson + +structure MetavarContext.Json where + decls : Array MetavarDecl.Json +deriving ToJson, FromJson + +def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO MetavarContext.Json := do + let mut decls := #[] + for (mvarId, decl) in mctx.decls do + let (_, typeMVars) ← ctx.runMetaM decl.lctx ((Meta.collectMVars decl.type).run {}) + decls := decls.push { + mvarId := toString mvarId.name + userName := toString decl.userName + type := (← ctx.ppExpr {} decl.type).pretty + mvarsInType := typeMVars.result.toList + -- value := (mctx.getExprAssignmentCore? mvarId).map toString + value := "N/A" + } + return { decls } + +structure ProofStepInfo where + tacticString : String + infoTree : Option Json + goalBefore : GoalInfo + goalsAfter : List GoalInfo + mctxBefore : Option MetavarContext.Json + mctxAfter : Option MetavarContext.Json + tacticDependsOn : List String + spawnedGoals : List GoalInfo + start : Option Lean.Position + finish : Option Lean.Position + deriving Inhabited, ToJson, FromJson + /-- A response to a Lean command. `env` can be used in later calls, to build on the stored environment. @@ -126,6 +234,7 @@ structure CommandResponse where sorries : List Sorry := [] tactics : List Tactic := [] infotree : Option Json := none + proofTreeEdges : Option (List (List ProofStepInfo)) := none deriving FromJson def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json) @@ -138,7 +247,10 @@ instance : ToJson CommandResponse where Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "tactics" r.tactics, - match r.infotree with | some j => [("infotree", j)] | none => [] + match r.infotree with | some j => [("infotree", j)] | none => [], + match r.proofTreeEdges with + | some edges => Json.nonemptyList "proofTreeEdges" edges + | none => [], ] /-- @@ -151,17 +263,23 @@ structure ProofStepResponse where messages : List Message := [] sorries : List Sorry := [] traces : List String + goalInfos: List GoalInfo := [] + mctxAfter : Option MetavarContext.Json proofStatus : String + stepVerification : String deriving ToJson, FromJson instance : ToJson ProofStepResponse where toJson r := Json.mkObj <| .flatten [ [("proofState", r.proofState)], [("goals", toJson r.goals)], + [("goalInfos", toJson r.goalInfos)], Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "traces" r.traces, - [("proofStatus", r.proofStatus)] + match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => [], + [("proofStatus", r.proofStatus)], + [("stepVerification", r.stepVerification)] ] /-- Json wrapper for an error. -/ diff --git a/REPL/Lean/InfoTree/ToJson.lean b/REPL/Lean/InfoTree/ToJson.lean index 6e3023c2..c7bc63b8 100644 --- a/REPL/Lean/InfoTree/ToJson.lean +++ b/REPL/Lean/InfoTree/ToJson.lean @@ -24,7 +24,7 @@ deriving ToJson structure Syntax.Json where pp : Option String - -- raw : String + raw : String range : Range deriving ToJson @@ -42,7 +42,7 @@ def _root_.Lean.Syntax.toJson (stx : Syntax) (ctx : ContextInfo) (lctx : LocalCo pp := match (← ctx.ppSyntax lctx stx).pretty with | "failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)" => none | pp => some pp - -- raw := toString stx + raw := toString stx range := stx.toRange ctx } structure TacticInfo.Json where @@ -58,7 +58,7 @@ def TacticInfo.toJson (i : TacticInfo) (ctx : ContextInfo) : IO TacticInfo.Json name := i.name? stx := { pp := Format.pretty (← i.pp ctx), - -- raw := toString i.info.stx, + raw := toString i.stx, range := i.stx.toRange ctx }, goalsBefore := (← i.goalState ctx).map Format.pretty, goalsAfter := (← i.goalStateAfter ctx).map Format.pretty } diff --git a/REPL/Main.lean b/REPL/Main.lean index b00b6833..df3c4799 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,7 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import REPL.PaperProof.BetterParser /-! # A REPL for Lean. @@ -94,6 +95,14 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do modify fun s => { s with proofStates := s.proofStates.push proofState } return id +/-- Delete all command snapshots with index >= id. -/ +def deleteCommandSnapshotsAfter (id : Nat) : M m Unit := do + modify fun s => { s with cmdStates := s.cmdStates.shrink id } + +/-- Delete all proof snapshots with index >= id. -/ +def deleteProofSnapshotsAfter (id : Nat) : M m Unit := do + modify fun s => { s with proofStates := s.proofStates.shrink id } + def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) : M m (List Sorry) := trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with @@ -113,7 +122,16 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term _ none => unreachable! let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goal pos endPos proofStateId + let goalInfo : Option GoalInfo ← match proofState with + | some proofState => do + match proofState.tacticState.goals[0]? with + | some goalId => do + -- TODO: this does not work when it's just `sorry` instead of `by sorry` - allow printGoalInfo to return none + let info ← printGoalInfo ctx goalId + pure (some info) + | none => pure none + | none => pure none + return Sorry.of goal goalInfo pos endPos proofStateId def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try @@ -130,13 +148,20 @@ 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 proofTrees (infoTrees : List InfoTree) : M m (List (List ProofStepInfo)) := do + infoTrees.mapM fun infoTree => do + let proofTree ← PaperProof.BetterParser infoTree + match proofTree with + | .some proofTree => return proofTree.steps + | .none => return [] + def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do let proofState := some (← ProofSnapshot.create ctx none env? goals goals) let goals := s!"{(← ctx.ppGoals goals)}".trim let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goals pos pos proofStateId + return Sorry.of goals none pos pos proofStateId private def collectFVarsAux : Expr → NameSet @@ -229,6 +254,307 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | _ => return "Incomplete: open goals remain" +def replaceWithPrint (f? : Expr → MetaM (Option Expr)) (e : Expr) : MetaM Expr := do + IO.println s!"Processing expression: {e}" + match ← f? e with + | some eNew => do + IO.println s!"Replaced with: {eNew}" + return eNew + | none => match e with + | .forallE _ d b _ => let d ← replaceWithPrint f? d; let b ← replaceWithPrint f? b; return e.updateForallE! d b + | .lam _ d b _ => let d ← replaceWithPrint f? d; let b ← replaceWithPrint f? b; return e.updateLambdaE! d b + | .mdata _ b => let b ← replaceWithPrint f? b; return e.updateMData! b + | .letE _ t v b _ => let t ← replaceWithPrint f? t; let v ← replaceWithPrint f? v; let b ← replaceWithPrint f? b; return e.updateLet! t v b + | .app f a => let f ← replaceWithPrint f? f; let a ← replaceWithPrint f? a; return e.updateApp! f a + | .proj _ _ b => let b ← replaceWithPrint f? b; return e.updateProj! b + | e => return e + +def replaceMVarsWithSorry (e : Expr) : MetaM Expr := do + match e with + | .mvar _ => do + let mvarType ← Meta.inferType e + let sorryTerm ← Meta.mkSorry mvarType false + return sorryTerm + | .forallE _ d b _ => let d ← replaceMVarsWithSorry d; let b ← replaceMVarsWithSorry b; return e.updateForallE! d b + | .lam _ d b _ => let d ← replaceMVarsWithSorry d; let b ← replaceMVarsWithSorry b; return e.updateLambdaE! d b + | .mdata _ b => let b ← replaceMVarsWithSorry b; return e.updateMData! b + | .letE _ t v b _ => let t ← replaceMVarsWithSorry t; let v ← replaceMVarsWithSorry v; let b ← replaceMVarsWithSorry b; return e.updateLet! t v b + | .app f a => let f ← replaceMVarsWithSorry f; let a ← replaceMVarsWithSorry a; return e.updateApp! f a + | .proj _ _ b => let b ← replaceMVarsWithSorry b; return e.updateProj! b + | e => return e + +def replaceMVarsWithSorryPrint (e : Expr) : MetaM Expr := do + let mkSorryForMVar (e : Expr) : MetaM (Option Expr) := do + if e.isMVar then + let mvarType ← Meta.inferType e + let sorryTerm ← Meta.mkSorry mvarType false + return some sorryTerm + else + return none + replaceWithPrint mkSorryForMVar e + + +/-- + Given a metavar‐context `mctx` and a metavariable `mvarId`, + first lookup its "core" assignment or delayed assignment, + then recursively replace any immediate `?m` occurrences in that Expr + by their own core/delayed assignments. + Returns `none` if no assignment of either kind is found. +-/ +partial def getFullAssignment (mctx : MetavarContext) (mvarId : MVarId) : Option Expr := + goMVar mvarId + where + -- goExpr: traverse an Expr, inlining any mvars via goMVar + goExpr (e : Expr) : Expr := + match e with + | .mvar mid => + match goMVar mid with + | some e' => e' + | none => e + | .forallE nm ty bd bi => .forallE nm (goExpr ty) (goExpr bd) bi + | .lam nm ty bd bi => .lam nm (goExpr ty) (goExpr bd) bi + | .app f a => .app (goExpr f) (goExpr a) + | .letE nm ty v bd bi => .letE nm (goExpr ty) (goExpr v) (goExpr bd) bi + | .mdata md b => .mdata md (goExpr b) + | .proj s i b => .proj s i (goExpr b) + | other => other + goMVar (mid : MVarId) : Option Expr := + match mctx.getExprAssignmentCore? mid with + | some e => some (goExpr e) + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => goMVar da.mvarIdPending + | none => none + +/-- + Given a metavar‐context `mctx` and a metavariable `mvarId`, + follow its core or delayed assignments recursively, + and collect the names of all metavariables reachable. + Returns a `NameSet` of metavariable names. +-/ +partial def getFullMvars (mctx : MetavarContext) (mvarId : MVarId) : NameSet := + goMVar mvarId NameSet.empty +where + /-- Handle a metavariable: inline its assignment if any, otherwise record it. -/ + goMVar (mid : MVarId) (acc : NameSet) : NameSet := + match mctx.getExprAssignmentCore? mid with + | some e => goExpr e acc + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => goMVar da.mvarIdPending acc + | none => acc.insert mid.name + + /-- Traverse an `Expr`, collecting any metavars it contains. -/ + goExpr : Expr → NameSet → NameSet + | Expr.mvar mid, acc => goMVar mid acc + | Expr.app f a, acc => goExpr a (goExpr f acc) + | Expr.lam _ ty body _, acc => goExpr body (goExpr ty acc) + | Expr.forallE _ ty bd _, acc => goExpr bd (goExpr ty acc) + | Expr.letE _ ty val bd _,acc => goExpr bd (goExpr val (goExpr ty acc)) + | Expr.mdata _ b, acc => goExpr b acc + | Expr.proj _ _ b, acc => goExpr b acc + | _, acc => acc + + +partial def getFullAssignmentIO (mctx : MetavarContext) (mvarId : MVarId) : IO (Option Expr) := + goMVar mvarId +where + /-- Traverse an Expr, inlining any mvars via goMVar, but first print it. -/ + goExpr (e : Expr) : IO Expr := do + IO.println s!"[goExpr] ▶ {e}" + match e with + | .mvar mid => + -- try to inline that mvar + match (← goMVar mid) with + | some e' => pure e' + | none => pure e + | .forallE nm ty bd bi => + pure $ .forallE nm (← goExpr ty) (← goExpr bd) bi + | .lam nm ty bd bi => + pure $ .lam nm (← goExpr ty) (← goExpr bd) bi + | .app f a => + pure $ .app (← goExpr f) (← goExpr a) + | .letE nm ty v bd bi => + pure $ .letE nm (← goExpr ty) (← goExpr v) (← goExpr bd) bi + | .mdata md b => + pure $ .mdata md (← goExpr b) + | .proj s i b => + pure $ .proj s i (← goExpr b) + | other => + pure other + + /-- Lookup the “core” or delayed assignment of a mvar, printing the mvar first. -/ + goMVar (mid : MVarId) : IO (Option Expr) := do + IO.println s!"[goMVar] ▶ {mid.name}" + match mctx.getExprAssignmentCore? mid with + | some e => + -- directly assigned: inline and return + some <$> goExpr e + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => + -- there’s a pending delayed assignment + goMVar da.mvarIdPending + | none => + -- not assigned at all + pure none + +partial def getFullAssignmentLambda (mctx : MetavarContext) (mvarId : MVarId) : MetaM (Option Expr) := + goMVar mvarId + where + goExpr (e : Expr) : MetaM Expr := do + match e with + | .mvar mid => + match (← goMVar mid) with + | some e' => pure e' + | none => pure e + | .forallE nm ty bd bi => + pure $ .forallE nm (← goExpr ty) (← goExpr bd) bi + | .lam nm ty bd bi => + pure $ .lam nm (← goExpr ty) (← goExpr bd) bi + | .app f a => + pure $ .app (← goExpr f) (← goExpr a) + | .letE nm ty v bd bi => + pure $ .letE nm (← goExpr ty) (← goExpr v) (← goExpr bd) bi + | .mdata md b => + pure $ .mdata md (← goExpr b) + | .proj s i b => + pure $ .proj s i (← goExpr b) + | other => + pure other + goMVar (mid : MVarId) : MetaM (Option Expr) := do + match mctx.getExprAssignmentCore? mid with + | some e => pure $ some (← goExpr e) + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => do + let e' ← goMVar da.mvarIdPending + match e' with + | some e' => + let e'' ← Meta.mkLambdaFVars da.fvars e' + return some e'' + | none => return none + | none => pure none + +/-- Does the expression `e` contain the metavariable `t`? -/ +private def findInExpr (t : MVarId) : Expr → Bool + | Expr.mvar mid => mid == t + | Expr.app f a => findInExpr t f || findInExpr t a + | Expr.lam _ ty bd _ => findInExpr t ty || findInExpr t bd + | Expr.forallE _ ty bd _ => findInExpr t ty || findInExpr t bd + | Expr.letE _ ty val bd _=> findInExpr t ty || findInExpr t val || findInExpr t bd + | Expr.proj _ _ e => findInExpr t e + | Expr.mdata _ e => findInExpr t e + | _ => false + +def checkAssignment (proofState : ProofSnapshot) (oldGoal : MVarId) (pf : Expr) : MetaM String := do + let occursCheck ← Lean.occursCheck oldGoal pf + if !occursCheck then + return s!"Error: Goal {oldGoal.name} assignment is circular" + + -- Check that all MVars in the proof are goals in new state + let mvars ← Meta.getMVars pf + + -- Loop through all unassigned metavariables recursively (note that delayed assigned ones are included). + for mvar in mvars do + let delayedAssigned ← mvar.isDelayedAssigned + -- We only care about the leaf metavariables, so we skip delayed assigned ones. + if delayedAssigned then + continue + + -- If the metavariable in the assignment is a new goal, it's fine. + if proofState.tacticState.goals.contains mvar then + continue + + return s!"Error: Goal {oldGoal.name} assignment contains unassigned metavariables" + + return "OK" + +/-- +Verifies that all goals from the old state are properly handled in the new state. +Returns either "OK" or an error message describing the first failing goal. +-/ +def verifyGoalAssignment (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : + M m String := do + match oldProofState? with + | none => return "OK" -- Nothing to verify + | some oldSt => do + let mut errorMsg := "" + for oldGoal in oldSt.tacticState.goals do + -- skip goals that are still open + if proofState.tacticState.goals.contains oldGoal then + continue + + -- run checks and build closed declaration inside the goal's local context + let (res, _) ← proofState.runMetaM do + -- switch to the local context of the goal + oldGoal.withContext do + match ← getExprMVarAssignment? oldGoal with + | none => return s!"Error: Goal {oldGoal.name} was not solved" + | some pfRaw => do + let pf ← instantiateMVars pfRaw + -- First check that the proof has the expected type + let pft ← Meta.inferType pf >>= instantiateMVars + let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars + unless (← Meta.isDefEq pft expectedType) do + return s!"Error: step assignment has type {pft} but goal has type {expectedType}" + + let chk ← checkAssignment proofState oldGoal pf + if chk != "OK" then return chk + + let pf ← instantiateMVars pfRaw + let pf ← replaceMVarsWithSorry pf + try + _ ← Lean.Meta.check pf + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + -- let pf ← instantiateMVars pfRaw + -- let pf ← abstractAllLambdaFVars pf + -- let pf ← instantiateMVars pf + -- -- let pf ← abstractAllLambdaFVars pf + -- let pf ← replaceMVarsWithSorry pf + -- -- let pf ← abstractAllLambdaFVars pf + + -- -- infer its type (it already includes the same Pi over locals) + -- let pftRaw ← Meta.inferType pf + -- let pftClosed ← instantiateMVars pftRaw + + -- -- collect universe levels + -- let usedLvls := + -- let l1 := collectLevelParams {} pftClosed + -- collectLevelParams l1 pf + + -- IO.println s!"pf: {pf}" + -- IO.println s!"pftClosed: {pftClosed}" + -- -- IO.println s!"usedLvls: {usedLvls.params.toList}" + + -- -- -- build the declaration + -- let freshName ← mkFreshId + -- let decl := Declaration.defnDecl { + -- name := freshName, + -- type := pftClosed, + -- value := pf, + -- levelParams := usedLvls.params.toList, + -- hints := ReducibilityHints.opaque, + -- safety := DefinitionSafety.safe + -- } + + -- -- add and check + -- try + -- -- TODO: isn't this memory leak + -- let _ ← addDecl decl + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + if res != "OK" then + errorMsg := res + break + + return if errorMsg == "" then "OK" else errorMsg + /-- Record a `ProofSnapshot` and generate a JSON response for it. -/ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) : M m ProofStepResponse := do @@ -245,14 +571,25 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) let sorries ← sorries trees none (some proofState.rootGoals) - let id ← recordProofSnapshot proofState + let proofStateId ← recordProofSnapshot proofState + let (ctx, _) ← proofState.runMetaM do return { ← CommandContextInfo.save with } + let goalInfos ← proofState.tacticState.goals.mapM (fun mvarId => do + let goalInfo ← printGoalInfo ctx mvarId + return goalInfo) + let mctxAfterJson ← MetavarContext.toJson proofState.metaState.mctx ctx return { - proofState := id + proofState := proofStateId goals := (← proofState.ppGoals).map fun s => s!"{s}" messages sorries traces - proofStatus := (← getProofStatus proofState) } + goalInfos + mctxAfter := mctxAfterJson + -- proofStatus := (← getProofStatus proofState) + proofStatus := "N/A" + stepVerification := (← verifyGoalAssignment proofState old?) + -- stepVerification := "N/A" + } /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do @@ -289,6 +626,21 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO (ProofStepResponse ⊕ let (proofState, _) ← ProofSnapshot.unpickle n.unpickleProofStateFrom cmdSnapshot? Sum.inl <$> createProofStepReponse proofState +def pruneSnapshots (n : PruneSnapshots) : M m String := do + match n.cmdFromId with + | some id => deleteCommandSnapshotsAfter id + | none => pure () + match n.proofFromId with + | some id => deleteProofSnapshotsAfter id + | none => pure () + return "OK" + +partial def removeChildren (t : InfoTree) : InfoTree := + match t with + | InfoTree.context ctx t' => InfoTree.context ctx (removeChildren t') + | InfoTree.node i _ => InfoTree.node i PersistentArray.empty + | InfoTree.hole _ => t + /-- Run a command, returning the id of the new environment, and any messages and sorries. -/ @@ -315,6 +667,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let tactics ← match s.allTactics with | some true => tactics trees initialCmdState.env | _ => pure [] + let proofTreeEdges ← match s.proofTrees with + | some true => some <$> proofTrees trees + | _ => pure none let cmdSnapshot := { cmdState cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD @@ -328,6 +683,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do | some "tactics" => trees.flatMap InfoTree.retainTacticInfo | some "original" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainOriginal | some "substantive" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainSubstantive + | some "no_children" => trees.map removeChildren | _ => [] let infotree ← if jsonTrees.isEmpty then pure none @@ -337,8 +693,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do { env, messages, sorries, - tactics - infotree } + tactics, + infotree, + proofTreeEdges } def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do try @@ -387,6 +744,7 @@ inductive Input | unpickleEnvironment : REPL.UnpickleEnvironment → Input | pickleProofSnapshot : REPL.PickleProofState → Input | unpickleProofSnapshot : REPL.UnpickleProofState → Input +| pruneSnapshots : REPL.PruneSnapshots → Input /-- Parse a user input string to an input command. -/ def parse (query : String) : IO Input := do @@ -408,6 +766,8 @@ def parse (query : String) : IO Input := do | .ok (r : REPL.Command) => return .command r | .error _ => match fromJson? j with | .ok (r : REPL.File) => return .file r + | .error _ => match fromJson? j with + | .ok (r : REPL.PruneSnapshots) => return .pruneSnapshots r | .error e => throw <| IO.userError <| toString <| toJson <| (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error) @@ -433,6 +793,7 @@ where loop : M IO Unit := do | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r) | .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r) | .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r) + | .pruneSnapshots r => return toJson (← pruneSnapshots r) printFlush "\n" -- easier to parse the output if there are blank lines loop diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean new file mode 100644 index 00000000..491dc0f9 --- /dev/null +++ b/REPL/PaperProof/BetterParser.lean @@ -0,0 +1,249 @@ +/- +MIT License + +Copyright (c) 2023 Anton Kovsharov + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. +-/ + +/- +Modified. +-/ + +import Lean +import Lean.Meta.Basic +import Lean.Meta.CollectMVars +import REPL.Lean.InfoTree.ToJson +import REPL.JSON + +open Lean Elab Server REPL + +namespace PaperProof + +def stepGoalsAfter (step : ProofStepInfo) : List GoalInfo := step.goalsAfter ++ step.spawnedGoals + +def noInEdgeGoals (allGoals : Std.HashSet GoalInfo) (steps : List ProofStepInfo) : Std.HashSet GoalInfo := + -- Some of the orphaned goals might be matched by tactics in sibling subtrees, e.g. for tacticSeq. + (steps.bind stepGoalsAfter).foldl Std.HashSet.erase allGoals + +/- + Instead of doing parsing of what user wrote (it wouldn't work for linarith etc), + let's do the following. + We have assigned something to our goal in mctxAfter. + All the fvars used in these assignments are what was actually used instead of what was in syntax. +-/ +def findHypsUsedByTactic (goalId: MVarId) (goalDecl : MetavarDecl) (mctxAfter : MetavarContext) : MetaM (List String) := do + let some expr := mctxAfter.eAssignment.find? goalId + | return [] + + -- Need to instantiate it to get all fvars + let fullExpr ← instantiateExprMVars expr + let fvarIds := (collectFVars {} fullExpr).fvarIds + let fvars := fvarIds.filterMap goalDecl.lctx.find? + let proofFvars ← fvars.filterM (Meta.isProof ·.toExpr) + -- let pretty := proofFvars.map (fun x => x.userName) + -- dbg_trace s!"Used {pretty}" + return proofFvars.map (fun x => x.fvarId.name.toString) |>.toList + +-- This is used to match goalsBefore with goalsAfter to see what was assigned to what +def findMVarsAssigned (goalId : MVarId) (mctxAfter : MetavarContext) : MetaM (List MVarId) := do + let some expr := mctxAfter.eAssignment.find? goalId + | return [] + let (_, s) ← (Meta.collectMVars expr).run {} + return s.result.toList + + +-- Returns unassigned goals from the provided list of goals +def getUnassignedGoals (goals : List MVarId) (mctx : MetavarContext) : IO (List MVarId) := do + goals.filterMapM fun id => do + if let none := mctx.findDecl? id then + return none + if mctx.eAssignment.contains id || + mctx.dAssignment.contains id then + return none + return some id + +structure Result where + steps : List ProofStepInfo + allGoals : Std.HashSet GoalInfo + +def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List String × GoalInfo × List GoalInfo)) := do + -- We want to filter out `focus` like tactics which don't do any assignments + -- therefore we check all goals on whether they were assigned during the tactic + let goalMVars := tInfo.goalsBefore ++ tInfo.goalsAfter + -- For printing purposes we always need to use the latest mctx assignments. For example in + -- have h := by calc + -- 3 ≤ 4 := by trivial + -- 4 ≤ 5 := by trivial + -- at mctxBefore type of `h` is `?m.260`, but by the time calc is elaborated at mctxAfter + -- it's known to be `3 ≤ 5` + let printCtx := {ctx with mctx := tInfo.mctxAfter} + let mut goalsBefore ← getUnassignedGoals goalMVars tInfo.mctxBefore + let mut goalsAfter ← getUnassignedGoals goalMVars tInfo.mctxAfter + let commonGoals := goalsBefore.filter fun g => goalsAfter.contains g + goalsBefore := goalsBefore.filter (!commonGoals.contains ·) + goalsAfter := goalsAfter.filter (!commonGoals.contains ·) + -- We need to match them into (goalBefore, goalsAfter) pairs according to assignment. + let mut result : List (List String × GoalInfo × List GoalInfo) := [] + for goalBefore in goalsBefore do + if let some goalDecl := tInfo.mctxBefore.findDecl? goalBefore then + let assignedMVars ← ctx.runMetaM goalDecl.lctx (findMVarsAssigned goalBefore tInfo.mctxAfter) + let tacticDependsOn ← ctx.runMetaM goalDecl.lctx + (findHypsUsedByTactic goalBefore goalDecl tInfo.mctxAfter) + + result := ( + tacticDependsOn, + ← printGoalInfo printCtx goalBefore, + ← goalsAfter.filter assignedMVars.contains |>.mapM (printGoalInfo printCtx) + ) :: result + return result + +-- TODO: solve rw_mod_cast + +open Parser.Tactic (optConfig rwRuleSeq location getConfigItems) + +def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo) : IO (List ProofStepInfo) := do + let range := stx.toRange ctx + let prettify (tStr : String) := + let res := tStr.trim.dropRightWhile (· == ',') + -- rw puts final rfl on the "]" token + if res == "]" then "rfl" else res + -- Each part of rw is a separate step none of them include the initial 'rw [' and final ']'. + -- So we add these to the first and last steps. + let extractRwStep (steps : List ProofStepInfo) (tactic : String) (atClause? : Option Syntax) : IO (List ProofStepInfo) := do + -- If atClause is present, call toJson on it and retrieve the `pp` field. + let atClauseStr? ← match atClause? with + | some atClause => do + let j ← atClause.toJson ctx (LocalContext.mkEmpty ()) + pure j.pp + | none => + pure none + + -- Turn the `Option String` into a (possibly-empty) string so we can insert it. + let maybeAtClause := atClauseStr?.getD "" -- getD "" returns `""` if `atClauseStr?` is `none` + -- rw puts final rfl on the "]" token + -- let rwSteps := (steps.filter (·.tacticString.trim.dropWhile (· == ' ') != "]")).map + -- fun a => { a with tacticString := s!"{tactic} [{prettify a.tacticString}]{maybeAtClause}" } + let rwSteps := steps.map + fun a => { a with tacticString := s!"{tactic} [{prettify a.tacticString}]{maybeAtClause}" } + + + match rwSteps with + | [] => + return [] + | [step] => + return [{ step with start := some range.start, finish := some range.finish }] + | steps => + let first := { steps.head! with start := some range.start } + let last := { steps.getLast! with finish := some range.finish } + let middle := steps.drop 1 |>.dropLast + return first :: middle ++ [last] + + match stx with + | `(tactic| rw [$_,*] $(at_clause)?) => + extractRwStep steps "rw" at_clause + | `(tactic| rewrite [$_,*] $(at_clause)?) => + extractRwStep steps "rewrite" at_clause + | `(tactic| rwa [$_,*] $(at_clause)?) => + let rwSteps ← extractRwStep steps "rw" at_clause + let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => + { + tacticString := "assumption", + infoTree := none, + goalBefore := g, + goalsAfter := [], + mctxBefore := none, + mctxAfter := none, + tacticDependsOn := [], + spawnedGoals := [], + start := none, + finish := none + } + return rwSteps ++ assumptionSteps + | _ => return steps + +-- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. +-- That's not completely right because it doesn't compare prefixes but +-- it's much shorter to write than correct version and serves the purpose. +def nameNumLt (n1 n2 : Name) : Bool := + match n1, n2 with + | .num _ n₁, .num _ n₂ => n₁ < n₂ + | .num _ _, _ => true + | _, _ => false + +partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree) (res : List (Option Result)) : IO Result := do + let res := res.filterMap id + let some ctx := i.updateContext? ctx + | panic! "unexpected context node" + let mut steps := res.map (fun r => r.steps) |>.join + let allSubGoals := Std.HashSet.empty.insertMany $ res.bind (·.allGoals.toList) + if let .ofTacticInfo tInfo := i then + -- shortcut if it's not a tactic user wrote + -- \n trim to avoid empty lines/comments until next tactic, + -- especially at the end of theorem it will capture comment for the next one + let some tacticString := tInfo.stx.getSubstring?.map (·.toString) + | return {steps, allGoals := allSubGoals} + + let infoTreeJson ← (InfoTree.node i PersistentArray.empty).toJson ctx + + steps ← prettifySteps tInfo.stx ctx steps + + let proofTreeEdges ← getGoalsChange ctx tInfo + let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join + let allGoals := allSubGoals.insertMany $ currentGoals + -- It's like tacticDependsOn but unnamed mvars instead of hyps. + -- Important to sort for have := calc for example, e.g. calc 3 < 4 ... 4 < 5 ... + let orphanedGoals := currentGoals.foldl Std.HashSet.erase (noInEdgeGoals allGoals steps) + |>.toArray.insertionSort (nameNumLt ·.id.name ·.id.name) |>.toList + + let mctxBeforeJson ← MetavarContext.toJson tInfo.mctxBefore ctx + let mctxAfterJson ← MetavarContext.toJson tInfo.mctxAfter ctx + + let isSimpRw := tInfo.stx.getKind.toString == "Mathlib.Tactic.tacticSimp_rw___" + + let newSteps := proofTreeEdges.filterMap fun ⟨ tacticDependsOn, goalBefore, goalsAfter ⟩ => + -- Leave only steps which are not handled in the subtree. + -- Additionally, simp_rw is not broken down since we are not able to properly transform it's rw steps. + if (steps.map (·.goalBefore) |>.elem goalBefore) && !isSimpRw then + none + else + let range := tInfo.stx.toRange ctx + some { + tacticString, + goalBefore, + goalsAfter, + mctxBefore := mctxBeforeJson, + mctxAfter := mctxAfterJson, + tacticDependsOn, + spawnedGoals := orphanedGoals, + start := range.start, + finish := range.finish, + infoTree := some infoTreeJson + } + + if isSimpRw then + return { steps := newSteps, allGoals } + else + return { steps := newSteps ++ steps, allGoals } + else + return { steps, allGoals := allSubGoals } + +partial def BetterParser (i : InfoTree) := i.visitM (postNode := postNode) + +end PaperProof diff --git a/lean-toolchain b/lean-toolchain index 9565de32..7aca1d8a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.19.0-rc2 +leanprover/lean4:v4.19.0