From 860344f9c504d3c86d679ea9ef43e306e26a964e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 13:44:46 -0700 Subject: [PATCH 01/12] refactor: Factor out `FrontendM` driver --- Pantograph/Compile/Elab.lean | 2 +- Pantograph/Compile/Frontend.lean | 16 +++++++++++----- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/Pantograph/Compile/Elab.lean b/Pantograph/Compile/Elab.lean index 79833f3..2ded0f1 100644 --- a/Pantograph/Compile/Elab.lean +++ b/Pantograph/Compile/Elab.lean @@ -1,4 +1,4 @@ - +/- Adapted from https://github.com/semorrison/lean-training-data -/ import Lean.Elab.Import import Lean.Elab.Command import Lean.Elab.InfoTree diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Compile/Frontend.lean index 3dbad85..640f5fa 100644 --- a/Pantograph/Compile/Frontend.lean +++ b/Pantograph/Compile/Frontend.lean @@ -29,6 +29,9 @@ end Lean.PersistentArray namespace Pantograph.Compile + +abbrev FrontendM := Elab.Frontend.FrontendM + structure CompilationStep where fileName : String fileMap : FileMap @@ -44,7 +47,7 @@ structure CompilationStep where Process one command, returning a `CompilationStep` and `done : Bool`, indicating whether this was the last command. -/ -def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do +def processOneCommand: FrontendM (CompilationStep × Bool) := do let s := (← get).commandState let before := s.env let done ← Elab.Frontend.processCommand @@ -57,30 +60,33 @@ def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do let ⟨_, fileName, fileMap⟩ := (← read).inputCtx return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done) -partial def processFile : Elab.Frontend.FrontendM (List CompilationStep) := do +partial def collectCompilationSteps : FrontendM (List CompilationStep) := do let (cmd, done) ← processOneCommand if done then return [cmd] else - return cmd :: (← processFile) + return cmd :: (← collectCompilationSteps) def findSourcePath (module : Name) : IO System.FilePath := do return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean" -def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do +def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do let file ← IO.FS.readFile (← findSourcePath module) let inputCtx := Parser.mkInputContext file module.toString let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← Elab.processHeader header opts messages inputCtx let commandState := Elab.Command.mkState env messages opts - processFile.run { inputCtx } + m.run { inputCtx } |>.run' { commandState := { commandState with infoState.enabled := true }, parserState, cmdPos := parserState.pos } +def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := + runFrontendMInFile module opts collectCompilationSteps + end Pantograph.Compile -- 2.44.1 From 8e3241c02ab65660169cdcb436883e27bd81e2b6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 15:02:43 -0700 Subject: [PATCH 02/12] refactor: Move all frontend functions to `Frontend` --- Main.lean | 2 +- Pantograph.lean | 2 +- Pantograph/Compile.lean | 25 ---------------- Pantograph/Compile/Parse.lean | 14 --------- Pantograph/Condensed.lean | 1 - Pantograph/Frontend.lean | 4 +++ .../Frontend.lean => Frontend/Basic.lean} | 30 +++++++++++++------ Pantograph/{Compile => Frontend}/Elab.lean | 20 +++++++++++-- Pantograph/Goal.lean | 18 ----------- Pantograph/Library.lean | 20 +++++++++++-- Pantograph/Protocol.lean | 5 ++-- Pantograph/Serial.lean | 7 +++++ Repl.lean | 23 +++++++------- Test/Integration.lean | 4 +-- 14 files changed, 86 insertions(+), 89 deletions(-) delete mode 100644 Pantograph/Compile.lean delete mode 100644 Pantograph/Compile/Parse.lean create mode 100644 Pantograph/Frontend.lean rename Pantograph/{Compile/Frontend.lean => Frontend/Basic.lean} (78%) rename Pantograph/{Compile => Frontend}/Elab.lean (86%) diff --git a/Main.lean b/Main.lean index eb5240d..2959a64 100644 --- a/Main.lean +++ b/Main.lean @@ -7,7 +7,7 @@ import Pantograph import Repl -- Main IO functions -open Pantograph +open Pantograph.Repl /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ def parseCommand (s: String): Except String Protocol.Command := do diff --git a/Pantograph.lean b/Pantograph.lean index 09327e8..292efb9 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,6 +1,6 @@ -import Pantograph.Compile import Pantograph.Condensed import Pantograph.Environment +import Pantograph.Frontend import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol diff --git a/Pantograph/Compile.lean b/Pantograph/Compile.lean deleted file mode 100644 index 83b463f..0000000 --- a/Pantograph/Compile.lean +++ /dev/null @@ -1,25 +0,0 @@ -/- Adapted from lean-training-data by semorrison -/ -import Pantograph.Protocol -import Pantograph.Compile.Frontend -import Pantograph.Compile.Elab -import Pantograph.Compile.Parse - -open Lean - -namespace Pantograph.Compile - -def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do - let infoTrees := steps.bind (·.trees) - let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ - | info@(.ofTacticInfo _) => info.isOriginal - | _ => false - let tactics := tacticInfoTrees.bind collectTactics - tactics.mapM λ invocation => do - let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty - let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty - let tactic ← invocation.ctx.runMetaM {} do - let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ - return t.pretty - return { goalBefore, goalAfter, tactic } - -end Pantograph.Compile diff --git a/Pantograph/Compile/Parse.lean b/Pantograph/Compile/Parse.lean deleted file mode 100644 index 72eb620..0000000 --- a/Pantograph/Compile/Parse.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Lean - -open Lean - -namespace Pantograph.Compile - -def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do - return Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := s) - (fileName := "") - -end Pantograph.Compile diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index c47f882..125b69c 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -2,7 +2,6 @@ import Lean import Pantograph.Goal import Pantograph.Expr -import Pantograph.Protocol open Lean diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean new file mode 100644 index 0000000..ffeeec5 --- /dev/null +++ b/Pantograph/Frontend.lean @@ -0,0 +1,4 @@ +/- Adapted from lean-training-data by semorrison -/ +import Pantograph.Protocol +import Pantograph.Frontend.Basic +import Pantograph.Frontend.Elab diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Frontend/Basic.lean similarity index 78% rename from Pantograph/Compile/Frontend.lean rename to Pantograph/Frontend/Basic.lean index 640f5fa..55f8e93 100644 --- a/Pantograph/Compile/Frontend.lean +++ b/Pantograph/Frontend/Basic.lean @@ -27,8 +27,7 @@ protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α : end Lean.PersistentArray -namespace Pantograph.Compile - +namespace Pantograph.Frontend abbrev FrontendM := Elab.Frontend.FrontendM @@ -47,6 +46,7 @@ structure CompilationStep where Process one command, returning a `CompilationStep` and `done : Bool`, indicating whether this was the last command. -/ +@[export pantograph_frontend_process_one_command_m] def processOneCommand: FrontendM (CompilationStep × Bool) := do let s := (← get).commandState let before := s.env @@ -67,26 +67,38 @@ partial def collectCompilationSteps : FrontendM (List CompilationStep) := do else return cmd :: (← collectCompilationSteps) - def findSourcePath (module : Name) : IO System.FilePath := do return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean" -def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do +@[export pantograph_create_frontend_context_state_from_file_m] +unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options := {}) + : IO (Elab.Frontend.Context × Elab.Frontend.State) := do let file ← IO.FS.readFile (← findSourcePath module) let inputCtx := Parser.mkInputContext file module.toString let (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← Elab.processHeader header opts messages inputCtx let commandState := Elab.Command.mkState env messages opts - m.run { inputCtx } - |>.run' { + let context: Elab.Frontend.Context := { inputCtx } + let state: Elab.Frontend.State := { commandState := { commandState with infoState.enabled := true }, parserState, cmdPos := parserState.pos } + return (context, state) -def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := - runFrontendMInFile module opts collectCompilationSteps +partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do + let (cmd, done) ← processOneCommand + let result ← f cmd + if done then + return [result] + else + return result :: (← mapCompilationSteps f) + +def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do + let (context, state) ← createFrontendContextStateFromFile module opts + m.run context |>.run' state -end Pantograph.Compile + +end Pantograph.Frontend diff --git a/Pantograph/Compile/Elab.lean b/Pantograph/Frontend/Elab.lean similarity index 86% rename from Pantograph/Compile/Elab.lean rename to Pantograph/Frontend/Elab.lean index 2ded0f1..e29d8f9 100644 --- a/Pantograph/Compile/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -3,7 +3,8 @@ import Lean.Elab.Import import Lean.Elab.Command import Lean.Elab.InfoTree -import Pantograph.Compile.Frontend +import Pantograph.Protocol +import Pantograph.Frontend.Basic open Lean @@ -75,7 +76,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : end Lean.Elab.InfoTree -namespace Pantograph.Compile +namespace Pantograph.Frontend -- Info tree filtering functions @@ -142,5 +143,18 @@ def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := def collectTactics (t : Elab.InfoTree) : List TacticInvocation := collectTacticNodes t |>.filter fun i => i.info.isSubstantive +@[export pantograph_frontend_collect_tactics_from_compilation_step_m] +def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do + let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ + | info@(.ofTacticInfo _) => info.isOriginal + | _ => false + let tactics := tacticInfoTrees.bind collectTactics + tactics.mapM λ invocation => do + let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty + let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty + let tactic ← invocation.ctx.runMetaM {} do + let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ + return t.pretty + return { goalBefore, goalAfter, tactic } -end Pantograph.Compile +end Pantograph.Frontend diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index f248923..b4a6fc7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -3,9 +3,7 @@ Functions for handling metavariables All the functions starting with `try` resume their inner monadic state. -/ -import Pantograph.Protocol import Pantograph.Tactic -import Pantograph.Compile.Parse import Lean @@ -385,20 +383,4 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) catch exception => return .failure #[← exception.toMessageData.toString] - -protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let recursor ← match (← Compile.parseTermM recursor) with - | .ok syn => pure syn - | .error error => return .parseError error - state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor) -protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let eq ← match (← Compile.parseTermM eq) with - | .ok syn => pure syn - | .error error => return .parseError error - state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) - end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 2f31042..23a2046 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -159,7 +159,7 @@ def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticRes runTermElabM <| state.tryAssign goal expr @[export pantograph_goal_have_m] protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do - let type ← match (← Compile.parseTermM type) with + let type ← match (← parseTermM type) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do @@ -167,12 +167,28 @@ protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: S state.tryTacticM goal $ Tactic.evalHave binderName.toName type @[export pantograph_goal_try_define_m] protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do - let expr ← match (← Compile.parseTermM expr) with + let expr ← match (← parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do state.restoreElabM state.tryTacticM goal (Tactic.evalDefine binderName.toName expr) +@[export pantograph_goal_try_motivated_apply_m] +protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let recursor ← match (← parseTermM recursor) with + | .ok syn => pure syn + | .error error => return .parseError error + state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor) +@[export pantograph_goal_try_no_confuse_m] +protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let eq ← match (← parseTermM eq) with + | .ok syn => pure syn + | .error error => return .parseError error + state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goal binderName type diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 223fcfe..74da216 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -286,8 +286,6 @@ structure GoalDiag where /-- Executes the Lean compiler on a single file -/ structure CompileUnit where module: String - -- If set to true, query the string boundaries of compilation units - compilationUnits: Bool := false -- If set to true, collect tactic invocations invocations: Bool := false deriving Lean.FromJson @@ -297,7 +295,8 @@ structure InvokedTactic where tactic: String deriving Lean.ToJson structure CompileUnitResult where - units?: Option $ List (Nat × Nat) + -- String boundaries of compilation units + units: List (Nat × Nat) invocations?: Option $ List InvokedTactic deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 93dfb95..3a9efa4 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -26,6 +26,13 @@ def parseTerm (env: Environment) (s: String): Except String Syntax := (input := s) (fileName := "") +def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do + return Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := "") + /-- Parse a syntax object. May generate additional metavariables! -/ def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do try diff --git a/Repl.lean b/Repl.lean index ef77d56..cd5bfe7 100644 --- a/Repl.lean +++ b/Repl.lean @@ -1,7 +1,7 @@ import Lean.Data.HashMap import Pantograph -namespace Pantograph +namespace Pantograph.Repl structure Context where imports: List String @@ -204,17 +204,20 @@ def execute (command: Protocol.Command): MainM Lean.Json := do compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do let module := args.module.toName try - let steps ← Compile.processSource module - let units? := if args.compilationUnits then - .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) + let li ← Frontend.runFrontendMInFile module {} <| Frontend.mapCompilationSteps λ step => do + let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) + let tacticInvocations ← if args.invocations then + Frontend.collectTacticsFromCompilationStep step + else + pure [] + return (unitBoundary, tacticInvocations) + let units := li.map λ (unit, _) => unit + let invocations? := if args.invocations then + .some $ li.bind λ (_, invocations) => invocations else .none - let invocations? ← if args.invocations then - pure $ .some (← Compile.collectTacticsFromCompilation steps) - else - pure .none - return .ok { units?, invocations? } + return .ok { units, invocations? } catch e => return .error $ errorI "compile" (← e.toMessageData.toString) -end Pantograph +end Pantograph.Repl diff --git a/Test/Integration.lean b/Test/Integration.lean index b82962b..e9eec76 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -6,13 +6,13 @@ import Repl import Test.Common namespace Pantograph.Test.Integration -open Pantograph +open Pantograph.Repl def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json)) (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do let payload := Lean.Json.mkObj payload let name := name?.getD s!"{cmd} {payload.compress}" - let result ← execute { cmd, payload } + let result ← Repl.execute { cmd, payload } return LSpec.test name (toString result = toString (Lean.toJson expected)) abbrev Test := List (MainM LSpec.TestSeq) -- 2.44.1 From 08fb53c0209a27fcfce95d738ab896e92b382625 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 10:18:20 -0700 Subject: [PATCH 03/12] test: Frontend process testing --- Pantograph/Frontend/Basic.lean | 55 +++++++++++++++++++--------------- Pantograph/Protocol.lean | 12 +++++--- Repl.lean | 23 ++++++++++---- Test/Integration.lean | 33 ++++++++++++++++++++ 4 files changed, 90 insertions(+), 33 deletions(-) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 55f8e93..79d3ea1 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -60,24 +60,45 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do let ⟨_, fileName, fileMap⟩ := (← read).inputCtx return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done) -partial def collectCompilationSteps : FrontendM (List CompilationStep) := do +partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do let (cmd, done) ← processOneCommand if done then - return [cmd] + if cmd.src.isEmpty then + return [] + else + return [← f cmd] else - return cmd :: (← collectCompilationSteps) + return (← f cmd) :: (← mapCompilationSteps f) + +@[export pantograph_frontend_find_source_path_m] def findSourcePath (module : Name) : IO System.FilePath := do return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean" -@[export pantograph_create_frontend_context_state_from_file_m] -unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options := {}) - : IO (Elab.Frontend.Context × Elab.Frontend.State) := do - let file ← IO.FS.readFile (← findSourcePath module) - let inputCtx := Parser.mkInputContext file module.toString +/-- +Use with +```lean +let m: FrontendM α := ... +let (context, state) ← createContextStateFromFile ... +m.run context |>.run' state +``` +-/ +@[export pantograph_frontend_create_context_state_from_file_m] +def createContextStateFromFile + (file : String) -- Content of the file + (fileName : String := "") + (env? : Option Lean.Environment := .none) -- If set to true, assume there's no header. + (opts : Options := {}) + : IO (Elab.Frontend.Context × Elab.Frontend.State) := unsafe do + --let file ← IO.FS.readFile (← findSourcePath module) + let inputCtx := Parser.mkInputContext file fileName - let (header, parserState, messages) ← Parser.parseHeader inputCtx - let (env, messages) ← Elab.processHeader header opts messages inputCtx + let (env, parserState, messages) ← match env? with + | .some env => pure (env, {}, .empty) + | .none => + let (header, parserState, messages) ← Parser.parseHeader inputCtx + let (env, messages) ← Elab.processHeader header opts messages inputCtx + pure (env, parserState, messages) let commandState := Elab.Command.mkState env messages opts let context: Elab.Frontend.Context := { inputCtx } let state: Elab.Frontend.State := { @@ -87,18 +108,4 @@ unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options := } return (context, state) -partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do - let (cmd, done) ← processOneCommand - let result ← f cmd - if done then - return [result] - else - return result :: (← mapCompilationSteps f) - -def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do - let (context, state) ← createFrontendContextStateFromFile module opts - m.run context |>.run' state - - - end Pantograph.Frontend diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 74da216..12a75a2 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -284,20 +284,24 @@ structure GoalDiag where /-- Executes the Lean compiler on a single file -/ -structure CompileUnit where - module: String +structure FrontendProcess where + -- One of these two must be supplied: Either supply the file name or the content. + fileName?: Option String := .none + file?: Option String := .none -- If set to true, collect tactic invocations invocations: Bool := false + -- If set to true, collect `sorry`s + sorrys: Bool := false deriving Lean.FromJson structure InvokedTactic where goalBefore: String goalAfter: String tactic: String deriving Lean.ToJson -structure CompileUnitResult where +structure FrontendProcessResult where -- String boundaries of compilation units units: List (Nat × Nat) - invocations?: Option $ List InvokedTactic + invocations?: Option (List InvokedTactic) := .none deriving Lean.ToJson abbrev CR α := Except InteractionError α diff --git a/Repl.lean b/Repl.lean index cd5bfe7..2f92eb8 100644 --- a/Repl.lean +++ b/Repl.lean @@ -46,7 +46,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "goal.continue" => run goal_continue | "goal.delete" => run goal_delete | "goal.print" => run goal_print - | "compile.unit" => run compile_unit + | "frontend.process" => run frontend_process | cmd => let error: Protocol.InteractionError := errorCommand s!"Unknown command {cmd}" @@ -201,16 +201,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}" let result ← runMetaInMainM <| goalPrint goalState state.options return .ok result - compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do - let module := args.module.toName + frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do try - let li ← Frontend.runFrontendMInFile module {} <| Frontend.mapCompilationSteps λ step => do + let (fileName, file) ← match args.fileName?, args.file? with + | .some fileName, .none => do + let file ← IO.FS.readFile fileName + pure (fileName, file) + | .none, .some file => + pure ("", file) + | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied" + let env?: Option Lean.Environment ← if args.fileName?.isSome then + pure .none + else do + let env ← Lean.MonadEnv.getEnv + pure <| .some env + let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {} + let m := Frontend.mapCompilationSteps λ step => do let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) let tacticInvocations ← if args.invocations then Frontend.collectTacticsFromCompilationStep step else pure [] return (unitBoundary, tacticInvocations) + let li ← m.run context |>.run' state let units := li.map λ (unit, _) => unit let invocations? := if args.invocations then .some $ li.bind λ (_, invocations) => invocations @@ -218,6 +231,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do .none return .ok { units, invocations? } catch e => - return .error $ errorI "compile" (← e.toMessageData.toString) + return .error $ errorI "frontend" (← e.toMessageData.toString) end Pantograph.Repl diff --git a/Test/Integration.lean b/Test/Integration.lean index e9eec76..3681d4e 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -161,6 +161,38 @@ def test_env_add_inspect : Test := Protocol.EnvInspectResult) ] +example : ∀ (p: Prop), p → p := by + intro p h + exact h + +def test_frontend_process : Test := + [ + let file := "example : ∀ (p: Prop), p → p := by\n intro p h\n exact h" + let goal1 := "p : Prop\nh : p\n⊢ p" + step "frontend.process" + [ + ("file", .str file), + ("invocations", .bool true), + ("sorrys", .bool false), + ] + ({ + units := [(0, file.utf8ByteSize)], + invocations? := .some [ + { + goalBefore := "⊢ ∀ (p : Prop), p → p", + goalAfter := goal1, + tactic := "intro p h", + }, + { + goalBefore := goal1 , + goalAfter := "", + tactic := "exact h", + }, + ] + }: Protocol.FrontendProcessResult), + ] + + def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do -- Setup the environment for execution let context: Context := { @@ -182,6 +214,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := ("Manual Mode", test_automatic_mode false), ("Automatic Mode", test_automatic_mode true), ("env.add env.inspect", test_env_add_inspect), + ("frontend.process", test_frontend_process), ] tests.map (fun (name, test) => (name, runTest env test)) -- 2.44.1 From 4f5950ed7878f17de50d9b535b3bd030f1965af8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 12:26:46 -0700 Subject: [PATCH 04/12] feat: Convert holes to goals --- Pantograph/Frontend/Elab.lean | 29 ++++++++++++++++++++-- Pantograph/Goal.lean | 11 +++++++++ Pantograph/Protocol.lean | 1 + Repl.lean | 45 +++++++++++++++++++++++------------ Test/Integration.lean | 33 ++++++++++++++++++++++++- 5 files changed, 101 insertions(+), 18 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index e29d8f9..8deac23 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -5,6 +5,7 @@ import Lean.Elab.InfoTree import Pantograph.Protocol import Pantograph.Frontend.Basic +import Pantograph.Goal open Lean @@ -132,7 +133,7 @@ partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pre /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, each equipped with its relevant `ContextInfo`, and any children info trees. -/ -def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := +private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := let infos := findAllInfo t none fun i => match i with | .ofTacticInfo _ => true | _ => false @@ -153,8 +154,32 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty let tactic ← invocation.ctx.runMetaM {} do - let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ + let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ return t.pretty return { goalBefore, goalAfter, tactic } +private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.TermInfo := + let infos := findAllInfo t none fun i => match i with + | .ofTermInfo { expectedType?, expr, stx, .. } => + expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry + | _ => false + infos.filterMap fun p => match p with + | (.ofTermInfo i, _, _) => .some i + | _ => none + +@[export pantograph_frontend_collect_sorrys_m] +def collectSorrys (step: CompilationStep) : List Elab.TermInfo := + step.trees.bind collectSorrysInTree + +@[export pantograph_frontend_sorrys_to_goal_state] +def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do + assert! !sorrys.isEmpty + let goals ← sorrys.mapM λ termInfo => Meta.withLCtx termInfo.lctx #[] do + let type := termInfo.expectedType?.get! + let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type + return mvar.mvarId! + GoalState.createFromMVars goals (root := { name := .anonymous }) + + + end Pantograph.Frontend diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b4a6fc7..79e3004 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -46,6 +46,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do savedState, parentMVar? := .none, } +@[export pantograph_goal_state_create_from_mvars_m] +protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do + let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState + let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {} + return { + root, + savedState, + parentMVar? := .none, + } @[export pantograph_goal_state_is_conv] protected def GoalState.isConv (state: GoalState): Bool := state.convMVar?.isSome @@ -143,6 +152,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except @[export pantograph_goal_state_root_expr] protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do + if goalState.root.name == .anonymous then + .none let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) if expr.hasExprMVar then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 12a75a2..26cae09 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -302,6 +302,7 @@ structure FrontendProcessResult where -- String boundaries of compilation units units: List (Nat × Nat) invocations?: Option (List InvokedTactic) := .none + goalStates?: Option (List (Nat × Array Goal)) := .none deriving Lean.ToJson abbrev CR α := Except InteractionError α diff --git a/Repl.lean b/Repl.lean index 2f92eb8..1277e73 100644 --- a/Repl.lean +++ b/Repl.lean @@ -54,6 +54,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do where errorCommand := errorI "command" errorIndex := errorI "index" + newGoalState (goalState: GoalState) : MainM Nat := do + let state ← get + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return stateId -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -95,7 +103,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do return .ok (← get).options goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do - let state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) @@ -108,11 +115,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match expr? with | .error error => return .error error | .ok goalState => - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } + let stateId ← newGoalState goalState return .ok { stateId, root := goalState.root.name.toString } goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get @@ -151,11 +154,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals" pure result | false, _ => pure nextGoalState - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert state.nextId nextGoalState, - nextId := state.nextId + 1, - } + let nextStateId ← newGoalState nextGoalState let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' return .ok { nextStateId? := .some nextStateId, @@ -202,6 +201,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let result ← runMetaInMainM <| goalPrint goalState state.options return .ok result frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do + let options := (← get).options try let (fileName, file) ← match args.fileName?, args.file? with | .some fileName, .none => do @@ -222,14 +222,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Frontend.collectTacticsFromCompilationStep step else pure [] - return (unitBoundary, tacticInvocations) + let sorrys := if args.sorrys then + Frontend.collectSorrys step + else + [] + return (unitBoundary, tacticInvocations, sorrys) let li ← m.run context |>.run' state - let units := li.map λ (unit, _) => unit + let units := li.map λ (unit, _, _) => unit let invocations? := if args.invocations then - .some $ li.bind λ (_, invocations) => invocations + .some $ li.bind λ (_, invocations, _) => invocations else .none - return .ok { units, invocations? } + let goalStates? ← if args.sorrys then do + let stateIds ← li.filterMapM λ (_, _, sorrys) => do + if sorrys.isEmpty then + return .none + let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys + let stateId ← newGoalState goalState + let goals ← goalSerialize goalState options + return .some (stateId, goals) + pure $ .some stateIds + else + pure .none + return .ok { units, invocations?, goalStates? } catch e => return .error $ errorI "frontend" (← e.toMessageData.toString) diff --git a/Test/Integration.lean b/Test/Integration.lean index 3681d4e..4a8e418 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -192,6 +192,36 @@ def test_frontend_process : Test := }: Protocol.FrontendProcessResult), ] +example : 1 + 2 = 3 := rfl +example (p: Prop): p → p := by simp + +def test_frontend_process_sorry : Test := + let solved := "example : 1 + 2 = 3 := rfl\n" + let withSorry := "example (p: Prop): p → p := sorry" + [ + let file := s!"{solved}{withSorry}" + let goal1: Protocol.Goal := { + name := "_uniq.1", + target := { pp? := .some "p → p" }, + vars := #[{ name := "_uniq.168", userName := "p", type? := .some { pp? := .some "Prop" }}], + } + step "frontend.process" + [ + ("file", .str file), + ("invocations", .bool false), + ("sorrys", .bool true), + ] + ({ + units := [ + (0, solved.utf8ByteSize), + (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize), + ], + goalStates? := [ + (0, #[goal1]), + ] + }: Protocol.FrontendProcessResult), + ] + def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do -- Setup the environment for execution @@ -214,7 +244,8 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := ("Manual Mode", test_automatic_mode false), ("Automatic Mode", test_automatic_mode true), ("env.add env.inspect", test_env_add_inspect), - ("frontend.process", test_frontend_process), + ("frontend.process invocation", test_frontend_process), + ("frontend.process sorry", test_frontend_process_sorry), ] tests.map (fun (name, test) => (name, runTest env test)) -- 2.44.1 From 762a139e7800bc08bc27c2f6a9aa3ba8365fcf44 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 12:30:32 -0700 Subject: [PATCH 05/12] feat: Export frontend functions --- Pantograph/Frontend/Basic.lean | 1 + Pantograph/Frontend/Elab.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 79d3ea1..933424c 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -8,6 +8,7 @@ namespace Lean.FileMap /-- Extract the range of a `Syntax` expressed as lines and columns. -/ -- Extracted from the private declaration `Lean.Elab.formatStxRange`, -- in `Lean.Elab.InfoTree.Main`. +@[export pantograph_frontend_stx_range] protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position := let pos := stx.getPos?.getD 0 let endPos := stx.getTailPos?.getD pos diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 8deac23..2ff9a2e 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -88,6 +88,7 @@ structure TacticInvocation where namespace TacticInvocation /-- Return the range of the tactic, as a pair of file positions. -/ +@[export pantograph_frontend_tactic_invocation_range] protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx /-- Pretty print a tactic. -/ -- 2.44.1 From 9f0de0957e54dbeaa94d06bbf0f4c5620429f817 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 12:39:32 -0700 Subject: [PATCH 06/12] doc: Update documentation for frontend command --- README.md | 74 ++++++++++++++++++++++++++++++------------------------- 1 file changed, 41 insertions(+), 33 deletions(-) diff --git a/README.md b/README.md index 8bda1ef..27af323 100644 --- a/README.md +++ b/README.md @@ -9,30 +9,17 @@ examine the symbol list of a Lean project for machine learning. ## Installation -For Nix based workflow, see below. +For Nix users, run +``` sh +nix build .#{sharedLib,executable} +``` +to build either the shared library or executable. Install `elan` and `lake`, and run ``` sh lake build ``` -This builds the executable in `.lake/build/bin/pantograph`. - -To use Pantograph in a project environment, setup the `LEAN_PATH` environment -variable so it contains the library path of lean libraries. The libraries must -be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, -the environment might be setup like this: - -``` sh -LIB="../lib" -LIB_MATHLIB="$LIB/mathlib4/lake-packages" -export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" - -LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ -``` -The `$LEAN_PATH` executable of any project can be extracted by -``` sh -lake env printenv LEAN_PATH -``` +This builds the executable in `.lake/build/bin/pantograph-repl`. ## Executable Usage @@ -90,10 +77,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va only the values of definitions are printed. * `options.set { key: value, ... }`: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - + One particular option for interest for machine learning researchers is the automatic mode. `options.set { "automaticMode": true }`. This makes Pantograph act like - LeanDojo, with no resumption necessary to manage your goals. + gym, with no resumption necessary to manage your goals. * `options.print`: Display the current set of options * `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol @@ -113,6 +100,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state +* `frontend.process { ["fileName": ",] ["file": ], invocations: + , sorrys: }`: Executes the Lean frontend on a file, collecting + either the tactic invocations (`"invocations": true`) or the sorrys into goal + states (`"sorrys": true`) ### Errors @@ -129,6 +120,25 @@ Common error forms: input of another is broken. For example, attempting to query a symbol not existing in the library or indexing into a non-existent proof state. +### Project Environment + +To use Pantograph in a project environment, setup the `LEAN_PATH` environment +variable so it contains the library path of lean libraries. The libraries must +be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, +the environment might be setup like this: + +``` sh +LIB="../lib" +LIB_MATHLIB="$LIB/mathlib4/lake-packages" +export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" + +LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ +``` +The `$LEAN_PATH` executable of any project can be extracted by +``` sh +lake env printenv LEAN_PATH +``` + ### Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: @@ -142,13 +152,22 @@ ulimit -s unlimited with `Pantograph` which mirrors the REPL commands above. It is recommended to call Pantograph via this FFI since it provides a tremendous speed up. +The executable can be used as-is, but linking against the shared library +requires the presence of `lean-all`. + +Inject any project path via the `pantograph_init_search` function. + ## Developing A Lean development shell is provided in the Nix flake. ### Testing -The tests are based on `LSpec`. To run tests, +The tests are based on `LSpec`. To run tests, use either +``` sh +nix flake check +``` +or ``` sh lake test ``` @@ -157,14 +176,3 @@ You can run an individual test by specifying a prefix ``` sh lake test -- "Tactic/No Confuse" ``` - -## Nix based workflow - -The included Nix flake provides build targets for `sharedLib` and `executable`. -The executable can be used as-is, but linking against the shared library -requires the presence of `lean-all`. - -To run tests: -``` sh -nix flake check -``` -- 2.44.1 From fe8b259e4f09817bf4b2df269d87e836d10155cf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 17:37:59 -0700 Subject: [PATCH 07/12] feat: Set root when there's just one mvar --- Pantograph/Frontend/Elab.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 2ff9a2e..4d6afe4 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -179,7 +179,11 @@ def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do let type := termInfo.expectedType?.get! let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type return mvar.mvarId! - GoalState.createFromMVars goals (root := { name := .anonymous }) + let root := match goals with + | [] => panic! "This function cannot be called on an empty list" + | [g] => g + | _ => { name := .anonymous } + GoalState.createFromMVars goals root -- 2.44.1 From bec84f857bd4f80064213fa5646bef4699191290 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 18:43:34 -0700 Subject: [PATCH 08/12] fix: repl build failure --- Main.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/Main.lean b/Main.lean index 2959a64..b866711 100644 --- a/Main.lean +++ b/Main.lean @@ -1,16 +1,15 @@ import Lean.Data.Json import Lean.Environment -import Pantograph.Version -import Pantograph.Library import Pantograph import Repl -- Main IO functions open Pantograph.Repl +open Pantograph.Protocol /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ -def parseCommand (s: String): Except String Protocol.Command := do +def parseCommand (s: String): Except String Command := do let s := s.trim match s.get? 0 with | .some '{' => -- Parse in Json mode @@ -30,7 +29,7 @@ partial def loop : MainM Unit := do if command.trim.length = 0 then return () match parseCommand command with | .error error => - let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError) + let error := Lean.toJson ({ error := "command", desc := error }: InteractionError) -- Using `Lean.Json.compress` here to prevent newline IO.println error.compress | .ok command => @@ -46,15 +45,15 @@ unsafe def main (args: List String): IO Unit := do -- NOTE: A more sophisticated scheme of command line argument handling is needed. -- Separate imports and options if args == ["--version"] then do - println! s!"{version}" + println! s!"{Pantograph.version}" return - initSearch "" + Pantograph.initSearch "" let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) - |>.toArray |> createCoreContext + |>.toArray |> Pantograph.createCoreContext let imports:= args.filter (λ s => ¬ (s.startsWith "--")) - let coreState ← createCoreState imports.toArray + let coreState ← Pantograph.createCoreState imports.toArray let context: Context := { imports } -- 2.44.1 From 18cd1d038819fbb9f8985648aaf3554049822b5e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Oct 2024 22:22:20 -0700 Subject: [PATCH 09/12] fix: Extracting sorrys from sketches --- Pantograph/Frontend/Elab.lean | 96 +++++++++++++++++++++++++++++++---- Test/Frontend.lean | 55 ++++++++++++++++++++ Test/Main.lean | 2 + 3 files changed, 142 insertions(+), 11 deletions(-) create mode 100644 Test/Frontend.lean diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 4d6afe4..ec86df3 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -159,26 +159,100 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc return t.pretty return { goalBefore, goalAfter, tactic } -private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.TermInfo := +private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.Info := let infos := findAllInfo t none fun i => match i with | .ofTermInfo { expectedType?, expr, stx, .. } => - expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry + expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry + | .ofTacticInfo { stx, .. } => + -- The `sorry` term is distinct from the `sorry` tactic + stx.isOfKind `Lean.Parser.Tactic.tacticSorry | _ => false - infos.filterMap fun p => match p with - | (.ofTermInfo i, _, _) => .some i - | _ => none + infos.map fun (i, _, _) => i +-- NOTE: Plural deliberately not spelled "sorries" @[export pantograph_frontend_collect_sorrys_m] -def collectSorrys (step: CompilationStep) : List Elab.TermInfo := +def collectSorrys (step: CompilationStep) : List Elab.Info := step.trees.bind collectSorrysInTree -@[export pantograph_frontend_sorrys_to_goal_state] -def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do - assert! !sorrys.isEmpty - let goals ← sorrys.mapM λ termInfo => Meta.withLCtx termInfo.lctx #[] do + +namespace MetaTranslate + +structure Context where + sourceMCtx : MetavarContext := {} + sourceLCtx : LocalContext := {} + +/- +Monadic state for translating a frozen meta state. The underlying `MetaM` +operates in the "target" context and state. +-/ +abbrev MetaTranslateM := ReaderT Context MetaM + +def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx +def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx + +private def translateExpr (expr: Expr) : MetaTranslateM Expr := do + let (expr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) expr + return expr + +def translateLocalDecl (frozenLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do + let fvarId ← mkFreshFVarId + match frozenLocalDecl with + | .cdecl index _ userName type bi kind => + return .cdecl index fvarId userName type bi kind + | .ldecl index _ userName type value nonDep kind => + return .ldecl index fvarId userName type value nonDep kind + +def translateMVarId (mvarId: MVarId) : MetaTranslateM MVarId := do + let shadowDecl := (← getSourceMCtx).findDecl? mvarId |>.get! + let target ← translateExpr shadowDecl.type + let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := shadowDecl.lctx }) do + let lctx ← MonadLCtx.getLCtx + let lctx ← (← getSourceLCtx).foldlM (λ lctx frozenLocalDecl => do + let localDecl ← translateLocalDecl frozenLocalDecl + let lctx := lctx.addDecl localDecl + pure lctx + ) lctx + withTheReader Meta.Context (fun ctx => { ctx with lctx }) do + Meta.mkFreshExprSyntheticOpaqueMVar target + return mvar.mvarId! + +def translateTermInfo (termInfo: Elab.TermInfo) : MetaM MVarId := do + let trM : MetaTranslateM MVarId := do let type := termInfo.expectedType?.get! - let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type + let lctx ← getSourceLCtx + let mvar ← withTheReader Meta.Context (fun ctx => { ctx with lctx }) do + Meta.mkFreshExprSyntheticOpaqueMVar type return mvar.mvarId! + trM.run { sourceLCtx := termInfo.lctx } + + +def translateTacticInfoBefore (tacticInfo: Elab.TacticInfo) : MetaM (List MVarId) := do + let trM : MetaTranslateM (List MVarId) := do + tacticInfo.goalsBefore.mapM translateMVarId + trM.run { sourceMCtx := tacticInfo.mctxBefore } + + +end MetaTranslate + +export MetaTranslate (MetaTranslateM) + +/-- +Since we cannot directly merge `MetavarContext`s, we have to get creative. This +function duplicates frozen mvars in term and tactic info nodes, and add them to +the current `MetavarContext`. +-/ +@[export pantograph_frontend_sorrys_to_goal_state] +def sorrysToGoalState (sorrys : List Elab.Info) : MetaM GoalState := do + assert! !sorrys.isEmpty + let goals ← sorrys.mapM λ info => Meta.withLCtx info.lctx #[] do + match info with + | .ofTermInfo termInfo => do + let mvarId ← MetaTranslate.translateTermInfo termInfo + return [mvarId] + | .ofTacticInfo tacticInfo => do + MetaTranslate.translateTacticInfoBefore tacticInfo + | _ => panic! "Invalid info" + let goals := goals.bind id let root := match goals with | [] => panic! "This function cannot be called on an empty list" | [g] => g diff --git a/Test/Frontend.lean b/Test/Frontend.lean new file mode 100644 index 0000000..ac347e6 --- /dev/null +++ b/Test/Frontend.lean @@ -0,0 +1,55 @@ +import LSpec +import Pantograph +import Repl +import Test.Common + +open Lean Pantograph +namespace Pantograph.Test.Frontend + +def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do + let filename := "" + let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} + let m := Frontend.mapCompilationSteps λ step => do + return Frontend.collectSorrys step + let li ← m.run context |>.run' state + let goalStates ← li.filterMapM λ sorrys => do + if sorrys.isEmpty then + return .none + let goalState ← Frontend.sorrysToGoalState sorrys + return .some goalState + return goalStates + +def test_multiple_sorries_in_proof : TestT MetaM Unit := do + let sketch := " +theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by + have h_nat_add_succ: ∀ n m : Nat, n = m := sorry + sorry + " + let goalStates ← (collectSorrysFromSource sketch).run' {} + let [goalState] := goalStates | panic! "Illegal number of states" + addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})) = #[ + { + name := "_uniq.1", + target := { pp? := "∀ (n m : Nat), n = m" }, + vars := #[ + ] + }, + { + name := "_uniq.4", + target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" }, + vars := #[{ + name := "_uniq.3", + userName := "h_nat_add_succ", + type? := .some { pp? := "∀ (n m : Nat), n = m" }, + }], + } + ]) + + +def suite (env : Environment): List (String × IO LSpec.TestSeq) := + let tests := [ + ("multiple_sorrys_in_proof", test_multiple_sorries_in_proof), + ] + tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test)) + +end Pantograph.Test.Frontend diff --git a/Test/Main.lean b/Test/Main.lean index 6da6640..0fde5fa 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,5 +1,6 @@ import LSpec import Test.Environment +import Test.Frontend import Test.Integration import Test.Library import Test.Metavar @@ -44,6 +45,7 @@ def main (args: List String) := do let suites: List (String × List (String × IO LSpec.TestSeq)) := [ ("Environment", Environment.suite), + ("Frontend", Frontend.suite env_default), ("Integration", Integration.suite env_default), ("Library", Library.suite env_default), ("Metavar", Metavar.suite env_default), -- 2.44.1 From 143cd289bbc4ea93f0889cf05737c3b6f90a51df Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 3 Oct 2024 01:29:46 -0700 Subject: [PATCH 10/12] fix: Extraction of sorry's from nested tactics --- Pantograph/Frontend/Elab.lean | 135 ++++++++++++++++++++++++---------- Test/Frontend.lean | 96 ++++++++++++++++++++++-- Test/Integration.lean | 4 +- 3 files changed, 187 insertions(+), 48 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index ec86df3..2e0c14e 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -124,12 +124,12 @@ protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format := end TacticInvocation /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ -partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) : +partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) : List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) := match t with - | .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred + | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred | .node i children => - (if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred) + (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) | _ => [] /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, @@ -159,7 +159,11 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc return t.pretty return { goalBefore, goalAfter, tactic } -private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.Info := +structure InfoWithContext where + info: Elab.Info + context?: Option Elab.ContextInfo := .none + +private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext := let infos := findAllInfo t none fun i => match i with | .ofTermInfo { expectedType?, expr, stx, .. } => expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry @@ -167,11 +171,11 @@ private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.Info := -- The `sorry` term is distinct from the `sorry` tactic stx.isOfKind `Lean.Parser.Tactic.tacticSorry | _ => false - infos.map fun (i, _, _) => i + infos.map fun (info, context?, _) => { info, context? } -- NOTE: Plural deliberately not spelled "sorries" @[export pantograph_frontend_collect_sorrys_m] -def collectSorrys (step: CompilationStep) : List Elab.Info := +def collectSorrys (step: CompilationStep) : List InfoWithContext := step.trees.bind collectSorrysInTree @@ -181,55 +185,106 @@ structure Context where sourceMCtx : MetavarContext := {} sourceLCtx : LocalContext := {} +structure State where + -- Stores mapping from old to new mvar/fvars + mvarMap: HashMap MVarId MVarId := {} + fvarMap: HashMap FVarId FVarId := {} + /- Monadic state for translating a frozen meta state. The underlying `MetaM` operates in the "target" context and state. -/ -abbrev MetaTranslateM := ReaderT Context MetaM +abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx +def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do + let state ← get + set { state with fvarMap := state.fvarMap.insert src dst } +def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do + let state ← get + set { state with mvarMap := state.mvarMap.insert src dst } -private def translateExpr (expr: Expr) : MetaTranslateM Expr := do - let (expr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) expr - return expr +def resetFVarMap : MetaTranslateM Unit := do + let state ← get + set { state with fvarMap := {} } -def translateLocalDecl (frozenLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do +private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do + let (srcExpr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) srcExpr + --IO.println s!"Transform src: {srcExpr}" + let result ← Core.transform srcExpr λ e => do + let state ← get + match e with + | .fvar fvarId => + let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}" + return .done $ .fvar fvarId' + | .mvar mvarId => do + match state.mvarMap.find? mvarId with + | .some mvarId' => do + return .done $ .mvar mvarId' + | .none => do + --let t := (← getSourceMCtx).findDecl? mvarId |>.get!.type + --let t' ← translateExpr t + let mvar' ← Meta.mkFreshExprMVar .none + addTranslatedMVar mvarId mvar'.mvarId! + return .done mvar' + | _ => return .continue + try + Meta.check result + catch ex => + panic! s!"Check failed: {← ex.toMessageData.toString}" + return result + +def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do let fvarId ← mkFreshFVarId - match frozenLocalDecl with - | .cdecl index _ userName type bi kind => - return .cdecl index fvarId userName type bi kind - | .ldecl index _ userName type value nonDep kind => - return .ldecl index fvarId userName type value nonDep kind + addTranslatedFVar srcLocalDecl.fvarId fvarId + match srcLocalDecl with + | .cdecl index _ userName type bi kind => do + --IO.println s!"[CD] {userName} {toString type}" + return .cdecl index fvarId userName (← translateExpr type) bi kind + | .ldecl index _ userName type value nonDep kind => do + --IO.println s!"[LD] {toString type} := {toString value}" + return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind -def translateMVarId (mvarId: MVarId) : MetaTranslateM MVarId := do - let shadowDecl := (← getSourceMCtx).findDecl? mvarId |>.get! - let target ← translateExpr shadowDecl.type - let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := shadowDecl.lctx }) do - let lctx ← MonadLCtx.getLCtx - let lctx ← (← getSourceLCtx).foldlM (λ lctx frozenLocalDecl => do - let localDecl ← translateLocalDecl frozenLocalDecl - let lctx := lctx.addDecl localDecl - pure lctx - ) lctx - withTheReader Meta.Context (fun ctx => { ctx with lctx }) do - Meta.mkFreshExprSyntheticOpaqueMVar target +def translateLCtx : MetaTranslateM LocalContext := do + resetFVarMap + (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do + let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl + pure $ lctx.addDecl localDecl + ) (← MonadLCtx.getLCtx) + + +def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do + let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get! + let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do + let lctx' ← translateLCtx + Meta.withLCtx lctx' #[] do + let target' ← translateExpr srcDecl.type + Meta.mkFreshExprSyntheticOpaqueMVar target' + addTranslatedMVar srcMVarId mvar.mvarId! return mvar.mvarId! -def translateTermInfo (termInfo: Elab.TermInfo) : MetaM MVarId := do +def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo) + : MetaM MVarId := do let trM : MetaTranslateM MVarId := do let type := termInfo.expectedType?.get! - let lctx ← getSourceLCtx - let mvar ← withTheReader Meta.Context (fun ctx => { ctx with lctx }) do - Meta.mkFreshExprSyntheticOpaqueMVar type + let lctx' ← translateLCtx + let mvar ← Meta.withLCtx lctx' #[] do + let type' ← translateExpr type + Meta.mkFreshExprSyntheticOpaqueMVar type' return mvar.mvarId! - trM.run { sourceLCtx := termInfo.lctx } + trM.run { + sourceMCtx := context?.map (·.mctx) |>.getD {}, + sourceLCtx := termInfo.lctx } |>.run' {} -def translateTacticInfoBefore (tacticInfo: Elab.TacticInfo) : MetaM (List MVarId) := do +def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo) + : MetaM (List MVarId) := do let trM : MetaTranslateM (List MVarId) := do tacticInfo.goalsBefore.mapM translateMVarId - trM.run { sourceMCtx := tacticInfo.mctxBefore } + trM.run { + sourceMCtx := tacticInfo.mctxBefore + } |>.run' {} end MetaTranslate @@ -242,15 +297,15 @@ function duplicates frozen mvars in term and tactic info nodes, and add them to the current `MetavarContext`. -/ @[export pantograph_frontend_sorrys_to_goal_state] -def sorrysToGoalState (sorrys : List Elab.Info) : MetaM GoalState := do +def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do assert! !sorrys.isEmpty - let goals ← sorrys.mapM λ info => Meta.withLCtx info.lctx #[] do - match info with + let goals ← sorrys.mapM λ i => do + match i.info with | .ofTermInfo termInfo => do - let mvarId ← MetaTranslate.translateTermInfo termInfo + let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context? return [mvarId] | .ofTacticInfo tacticInfo => do - MetaTranslate.translateTacticInfoBefore tacticInfo + MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context? | _ => panic! "Invalid info" let goals := goals.bind id let root := match goals with diff --git a/Test/Frontend.lean b/Test/Frontend.lean index ac347e6..c186503 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -19,7 +19,7 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do return .some goalState return goalStates -def test_multiple_sorries_in_proof : TestT MetaM Unit := do +def test_multiple_sorrys_in_proof : TestT MetaM Unit := do let sketch := " theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by have h_nat_add_succ: ∀ n m : Nat, n = m := sorry @@ -27,28 +27,112 @@ theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + " let goalStates ← (collectSorrysFromSource sketch).run' {} let [goalState] := goalStates | panic! "Illegal number of states" - addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})) = #[ + addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ { - name := "_uniq.1", target := { pp? := "∀ (n m : Nat), n = m" }, vars := #[ ] }, { - name := "_uniq.4", target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" }, vars := #[{ - name := "_uniq.3", userName := "h_nat_add_succ", type? := .some { pp? := "∀ (n m : Nat), n = m" }, }], } ]) +def test_sorry_in_middle: TestT MetaM Unit := do + let sketch := " +example : ∀ (n m: Nat), n + m = m + n := by + intros n m + sorry + " + let goalStates ← (collectSorrysFromSource sketch).run' {} + let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}" + addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ + { + target := { pp? := "n + m = m + n" }, + vars := #[{ + userName := "n", + type? := .some { pp? := "Nat" }, + }, { + userName := "m", + type? := .some { pp? := "Nat" }, + } + ], + } + ]) + +def test_sorry_in_induction : TestT MetaM Unit := do + let sketch := " +example : ∀ (n m: Nat), n + m = m + n := by + intros n m + induction n with + | zero => + have h1 : 0 + m = m := sorry + sorry + | succ n ih => + have h2 : n + m = m := sorry + sorry + " + let goalStates ← (collectSorrysFromSource sketch).run' {} + let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}" + addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ + { + target := { pp? := "0 + m = m" }, + vars := #[{ + userName := "m", + type? := .some { pp? := "Nat" }, + }] + }, + { + target := { pp? := "0 + m = m + 0" }, + vars := #[{ + userName := "m", + type? := .some { pp? := "Nat" }, + }, { + userName := "h1", + type? := .some { pp? := "0 + m = m" }, + }] + }, + { + target := { pp? := "n + m = m" }, + vars := #[{ + userName := "m", + type? := .some { pp? := "Nat" }, + }, { + userName := "n", + type? := .some { pp? := "Nat" }, + }, { + userName := "ih", + type? := .some { pp? := "n + m = m + n" }, + }] + }, + { + target := { pp? := "n + 1 + m = m + (n + 1)" }, + vars := #[{ + userName := "m", + type? := .some { pp? := "Nat" }, + }, { + userName := "n", + type? := .some { pp? := "Nat" }, + }, { + userName := "ih", + type? := .some { pp? := "n + m = m + n" }, + }, { + userName := "h2", + type? := .some { pp? := "n + m = m" }, + }] + } + ]) + def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests := [ - ("multiple_sorrys_in_proof", test_multiple_sorries_in_proof), + ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof), + ("sorry_in_middle", test_sorry_in_middle), + ("sorry_in_induction", test_sorry_in_induction), ] tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test)) diff --git a/Test/Integration.lean b/Test/Integration.lean index 4a8e418..b3d49fe 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -201,9 +201,9 @@ def test_frontend_process_sorry : Test := [ let file := s!"{solved}{withSorry}" let goal1: Protocol.Goal := { - name := "_uniq.1", + name := "_uniq.6", target := { pp? := .some "p → p" }, - vars := #[{ name := "_uniq.168", userName := "p", type? := .some { pp? := .some "Prop" }}], + vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}], } step "frontend.process" [ -- 2.44.1 From 530a1a1a97273314bd7b01c542ce686a366aa0b9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 3 Oct 2024 11:35:54 -0700 Subject: [PATCH 11/12] fix: Extracting `sorry`s from coupled goals --- Pantograph/Expr.lean | 87 ++++++++--------- Pantograph/Frontend.lean | 2 +- Pantograph/Frontend/Elab.lean | 118 +--------------------- Pantograph/Frontend/MetaTranslate.lean | 129 +++++++++++++++++++++++++ Test/Frontend.lean | 49 ++++++++-- 5 files changed, 221 insertions(+), 164 deletions(-) create mode 100644 Pantograph/Frontend/MetaTranslate.lean diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index f989575..ad064a7 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -60,53 +60,54 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do -- nested mvars. mvarId.setKind .syntheticOpaque - let lctx ← MonadLCtx.getLCtx - if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then - let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with - | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name] - | .none => acc) [] - panic! s!"Local context variable violation: {violations}" + mvarId.withContext do + let lctx ← MonadLCtx.getLCtx + if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then + let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with + | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name] + | .none => acc) [] + panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}" - if let .some assign ← getExprMVarAssignment? mvarId then - --IO.println s!"{padding}├A ?{mvarId.name}" - assert! !(← mvarId.isDelayedAssigned) - return .visit (mkAppN assign args) - else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then - --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList - --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]" + if let .some assign ← getExprMVarAssignment? mvarId then + --IO.println s!"{padding}├A ?{mvarId.name}" + assert! !(← mvarId.isDelayedAssigned) + return .visit (mkAppN assign args) + else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList + --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]" - if args.size < fvars.size then - throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" - --if !args.isEmpty then - --IO.println s!"{padding}├── Arguments Begin" - let args ← args.mapM self - --if !args.isEmpty then - --IO.println s!"{padding}├── Arguments End" - if !(← mvarIdPending.isAssignedOrDelayedAssigned) then - --IO.println s!"{padding}├T1" - let result := mkAppN f args + if args.size < fvars.size then + throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" + --if !args.isEmpty then + --IO.println s!"{padding}├── Arguments Begin" + let args ← args.mapM self + --if !args.isEmpty then + --IO.println s!"{padding}├── Arguments End" + if !(← mvarIdPending.isAssignedOrDelayedAssigned) then + --IO.println s!"{padding}├T1" + let result := mkAppN f args + return .done result + + let pending ← mvarIdPending.withContext do + let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1) + --IO.println s!"{padding}├Pre: {inner}" + pure <| (← inner.abstractM fvars).instantiateRev args + + -- Tail arguments + let result := mkAppRange pending fvars.size args.size args + --IO.println s!"{padding}├MD {result}" return .done result + else + assert! !(← mvarId.isAssigned) + assert! !(← mvarId.isDelayedAssigned) + --if !args.isEmpty then + -- IO.println s!"{padding}├── Arguments Begin" + let args ← args.mapM self + --if !args.isEmpty then + -- IO.println s!"{padding}├── Arguments End" - let pending ← mvarIdPending.withContext do - let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1) - --IO.println s!"{padding}├Pre: {inner}" - pure <| (← inner.abstractM fvars).instantiateRev args - - -- Tail arguments - let result := mkAppRange pending fvars.size args.size args - --IO.println s!"{padding}├MD {result}" - return .done result - else - assert! !(← mvarId.isAssigned) - assert! !(← mvarId.isDelayedAssigned) - --if !args.isEmpty then - -- IO.println s!"{padding}├── Arguments Begin" - let args ← args.mapM self - --if !args.isEmpty then - -- IO.println s!"{padding}├── Arguments End" - - --IO.println s!"{padding}├M ?{mvarId.name}" - return .done (mkAppN f args)) + --IO.println s!"{padding}├M ?{mvarId.name}" + return .done (mkAppN f args)) --IO.println s!"{padding}└Result {result}" return result where diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean index ffeeec5..fd91823 100644 --- a/Pantograph/Frontend.lean +++ b/Pantograph/Frontend.lean @@ -1,4 +1,4 @@ /- Adapted from lean-training-data by semorrison -/ -import Pantograph.Protocol import Pantograph.Frontend.Basic import Pantograph.Frontend.Elab +import Pantograph.Frontend.MetaTranslate diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 2e0c14e..2036aea 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -3,9 +3,10 @@ import Lean.Elab.Import import Lean.Elab.Command import Lean.Elab.InfoTree -import Pantograph.Protocol import Pantograph.Frontend.Basic +import Pantograph.Frontend.MetaTranslate import Pantograph.Goal +import Pantograph.Protocol open Lean @@ -179,117 +180,6 @@ def collectSorrys (step: CompilationStep) : List InfoWithContext := step.trees.bind collectSorrysInTree -namespace MetaTranslate - -structure Context where - sourceMCtx : MetavarContext := {} - sourceLCtx : LocalContext := {} - -structure State where - -- Stores mapping from old to new mvar/fvars - mvarMap: HashMap MVarId MVarId := {} - fvarMap: HashMap FVarId FVarId := {} - -/- -Monadic state for translating a frozen meta state. The underlying `MetaM` -operates in the "target" context and state. --/ -abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM - -def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx -def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx -def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do - let state ← get - set { state with fvarMap := state.fvarMap.insert src dst } -def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do - let state ← get - set { state with mvarMap := state.mvarMap.insert src dst } - -def resetFVarMap : MetaTranslateM Unit := do - let state ← get - set { state with fvarMap := {} } - -private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do - let (srcExpr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) srcExpr - --IO.println s!"Transform src: {srcExpr}" - let result ← Core.transform srcExpr λ e => do - let state ← get - match e with - | .fvar fvarId => - let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}" - return .done $ .fvar fvarId' - | .mvar mvarId => do - match state.mvarMap.find? mvarId with - | .some mvarId' => do - return .done $ .mvar mvarId' - | .none => do - --let t := (← getSourceMCtx).findDecl? mvarId |>.get!.type - --let t' ← translateExpr t - let mvar' ← Meta.mkFreshExprMVar .none - addTranslatedMVar mvarId mvar'.mvarId! - return .done mvar' - | _ => return .continue - try - Meta.check result - catch ex => - panic! s!"Check failed: {← ex.toMessageData.toString}" - return result - -def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do - let fvarId ← mkFreshFVarId - addTranslatedFVar srcLocalDecl.fvarId fvarId - match srcLocalDecl with - | .cdecl index _ userName type bi kind => do - --IO.println s!"[CD] {userName} {toString type}" - return .cdecl index fvarId userName (← translateExpr type) bi kind - | .ldecl index _ userName type value nonDep kind => do - --IO.println s!"[LD] {toString type} := {toString value}" - return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind - -def translateLCtx : MetaTranslateM LocalContext := do - resetFVarMap - (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do - let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl - pure $ lctx.addDecl localDecl - ) (← MonadLCtx.getLCtx) - - -def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do - let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get! - let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do - let lctx' ← translateLCtx - Meta.withLCtx lctx' #[] do - let target' ← translateExpr srcDecl.type - Meta.mkFreshExprSyntheticOpaqueMVar target' - addTranslatedMVar srcMVarId mvar.mvarId! - return mvar.mvarId! - -def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo) - : MetaM MVarId := do - let trM : MetaTranslateM MVarId := do - let type := termInfo.expectedType?.get! - let lctx' ← translateLCtx - let mvar ← Meta.withLCtx lctx' #[] do - let type' ← translateExpr type - Meta.mkFreshExprSyntheticOpaqueMVar type' - return mvar.mvarId! - trM.run { - sourceMCtx := context?.map (·.mctx) |>.getD {}, - sourceLCtx := termInfo.lctx } |>.run' {} - - -def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo) - : MetaM (List MVarId) := do - let trM : MetaTranslateM (List MVarId) := do - tacticInfo.goalsBefore.mapM translateMVarId - trM.run { - sourceMCtx := tacticInfo.mctxBefore - } |>.run' {} - - -end MetaTranslate - -export MetaTranslate (MetaTranslateM) /-- Since we cannot directly merge `MetavarContext`s, we have to get creative. This @@ -299,7 +189,7 @@ the current `MetavarContext`. @[export pantograph_frontend_sorrys_to_goal_state] def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do assert! !sorrys.isEmpty - let goals ← sorrys.mapM λ i => do + let goalsM := sorrys.mapM λ i => do match i.info with | .ofTermInfo termInfo => do let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context? @@ -307,7 +197,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do | .ofTacticInfo tacticInfo => do MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context? | _ => panic! "Invalid info" - let goals := goals.bind id + let goals := (← goalsM.run {} |>.run' {}).bind id let root := match goals with | [] => panic! "This function cannot be called on an empty list" | [g] => g diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean new file mode 100644 index 0000000..82f8dfc --- /dev/null +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -0,0 +1,129 @@ +import Lean.Meta + +open Lean + +namespace Pantograph.Frontend + +namespace MetaTranslate + +structure Context where + sourceMCtx : MetavarContext := {} + sourceLCtx : LocalContext := {} + +abbrev FVarMap := HashMap FVarId FVarId + +structure State where + -- Stores mapping from old to new mvar/fvars + mvarMap: HashMap MVarId MVarId := {} + fvarMap: HashMap FVarId FVarId := {} + +/- +Monadic state for translating a frozen meta state. The underlying `MetaM` +operates in the "target" context and state. +-/ +abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM + +def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx +def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx +def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do + modifyGet λ state => ((), { state with fvarMap := state.fvarMap.insert src dst }) +def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do + modifyGet λ state => ((), { state with mvarMap := state.mvarMap.insert src dst }) + +def saveFVarMap : MetaTranslateM FVarMap := do + return (← get).fvarMap +def restoreFVarMap (map: FVarMap) : MetaTranslateM Unit := do + modifyGet λ state => ((), { state with fvarMap := map }) +def resetFVarMap : MetaTranslateM Unit := do + modifyGet λ state => ((), { state with fvarMap := {} }) + +mutual +private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do + let sourceMCtx ← getSourceMCtx + let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr + --IO.println s!"Transform src: {srcExpr}" + let result ← Core.transform srcExpr λ e => do + let state ← get + match e with + | .fvar fvarId => + let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}" + assert! (← getLCtx).contains fvarId' + return .done $ .fvar fvarId' + | .mvar mvarId => do + assert! !(sourceMCtx.dAssignment.contains mvarId) + assert! !(sourceMCtx.eAssignment.contains mvarId) + match state.mvarMap.find? mvarId with + | .some mvarId' => do + return .done $ .mvar mvarId' + | .none => do + -- Entering another LCtx, must save the current one + let fvarMap ← saveFVarMap + let mvarId' ← translateMVarId mvarId + restoreFVarMap fvarMap + return .done $ .mvar mvarId' + | _ => return .continue + Meta.check result + return result + +partial def translateLocalInstance (srcInstance: LocalInstance) : MetaTranslateM LocalInstance := do + return { + className := srcInstance.className, + fvar := ← translateExpr srcInstance.fvar + } +partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do + let fvarId ← mkFreshFVarId + addTranslatedFVar srcLocalDecl.fvarId fvarId + match srcLocalDecl with + | .cdecl index _ userName type bi kind => do + --IO.println s!"[CD] {userName} {toString type}" + return .cdecl index fvarId userName (← translateExpr type) bi kind + | .ldecl index _ userName type value nonDep kind => do + --IO.println s!"[LD] {toString type} := {toString value}" + return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind + +partial def translateLCtx : MetaTranslateM LocalContext := do + resetFVarMap + (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do + let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl + pure $ lctx.addDecl localDecl + ) (← MonadLCtx.getLCtx) + +partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do + if let .some mvarId' := (← get).mvarMap.find? srcMVarId then + return mvarId' + let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get! + let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do + let lctx' ← translateLCtx + let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance + Meta.withLCtx lctx' localInstances' do + let target' ← translateExpr srcDecl.type + Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName + addTranslatedMVar srcMVarId mvar.mvarId! + return mvar.mvarId! +end + +def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo) + : MetaTranslateM MVarId := do + withTheReader Context (λ ctx => { ctx with + sourceMCtx := context?.map (·.mctx) |>.getD {}, + sourceLCtx := termInfo.lctx, + }) do + let type := termInfo.expectedType?.get! + let lctx' ← translateLCtx + let mvar ← Meta.withLCtx lctx' #[] do + let type' ← translateExpr type + Meta.mkFreshExprSyntheticOpaqueMVar type' + return mvar.mvarId! + + +def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo) + : MetaTranslateM (List MVarId) := do + withTheReader Context (λ ctx => { ctx with sourceMCtx := tacticInfo.mctxBefore }) do + tacticInfo.goalsBefore.mapM translateMVarId + + +end MetaTranslate + +export MetaTranslate (MetaTranslateM) + +end Pantograph.Frontend diff --git a/Test/Frontend.lean b/Test/Frontend.lean index c186503..b09ef81 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -26,8 +26,8 @@ theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + sorry " let goalStates ← (collectSorrysFromSource sketch).run' {} - let [goalState] := goalStates | panic! "Illegal number of states" - addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ + let [goalState] := goalStates | panic! "Incorrect number of states" + addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ { target := { pp? := "∀ (n m : Nat), n = m" }, vars := #[ @@ -49,8 +49,8 @@ example : ∀ (n m: Nat), n + m = m + n := by sorry " let goalStates ← (collectSorrysFromSource sketch).run' {} - let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}" - addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ + let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" + addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ { target := { pp? := "n + m = m + n" }, vars := #[{ @@ -77,8 +77,8 @@ example : ∀ (n m: Nat), n + m = m + n := by sorry " let goalStates ← (collectSorrysFromSource sketch).run' {} - let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}" - addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ + let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" + addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ { target := { pp? := "0 + m = m" }, vars := #[{ @@ -87,6 +87,7 @@ example : ∀ (n m: Nat), n + m = m + n := by }] }, { + userName? := .some "zero", target := { pp? := "0 + m = m + 0" }, vars := #[{ userName := "m", @@ -110,6 +111,7 @@ example : ∀ (n m: Nat), n + m = m + n := by }] }, { + userName? := .some "succ", target := { pp? := "n + 1 + m = m + (n + 1)" }, vars := #[{ userName := "m", @@ -127,12 +129,47 @@ example : ∀ (n m: Nat), n + m = m + n := by } ]) +def test_sorry_in_coupled: TestT MetaM Unit := do + let sketch := " +example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by + intro y + apply Exists.intro + case h => sorry + case w => sorry + " + let goalStates ← (collectSorrysFromSource sketch).run' {} + let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" + addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[ + { + target := { pp? := "y + 1 = ?w" }, + vars := #[{ + userName := "y", + type? := .some { pp? := "Nat" }, + } + ], + }, + { + userName? := .some "w", + target := { pp? := "Nat" }, + vars := #[{ + userName := "y✝", + isInaccessible := true, + type? := .some { pp? := "Nat" }, + }, { + userName := "y", + type? := .some { pp? := "Nat" }, + } + ], + } + ]) + def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof), ("sorry_in_middle", test_sorry_in_middle), ("sorry_in_induction", test_sorry_in_induction), + ("sorry_in_coupled", test_sorry_in_coupled), ] tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test)) -- 2.44.1 From a03eeddc9bea63caf91b20bdbbbd4cf9e5133b79 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 3 Oct 2024 11:46:09 -0700 Subject: [PATCH 12/12] fix: Variable duplication in nested translation --- Pantograph/Frontend/MetaTranslate.lean | 22 +++++++++++++--------- Test/Frontend.lean | 4 ---- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean index 82f8dfc..1a12029 100644 --- a/Pantograph/Frontend/MetaTranslate.lean +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -83,21 +83,25 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD partial def translateLCtx : MetaTranslateM LocalContext := do resetFVarMap + let lctx ← MonadLCtx.getLCtx + assert! lctx.isEmpty (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do - let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl + let localDecl ← Meta.withLCtx lctx #[] do + translateLocalDecl srcLocalDecl pure $ lctx.addDecl localDecl - ) (← MonadLCtx.getLCtx) + ) lctx partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do if let .some mvarId' := (← get).mvarMap.find? srcMVarId then return mvarId' - let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get! - let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do - let lctx' ← translateLCtx - let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance - Meta.withLCtx lctx' localInstances' do - let target' ← translateExpr srcDecl.type - Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName + let mvar ← Meta.withLCtx .empty #[] do + let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get! + withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do + let lctx' ← translateLCtx + let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance + Meta.withLCtx lctx' localInstances' do + let target' ← translateExpr srcDecl.type + Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName addTranslatedMVar srcMVarId mvar.mvarId! return mvar.mvarId! end diff --git a/Test/Frontend.lean b/Test/Frontend.lean index b09ef81..68d961b 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -152,10 +152,6 @@ example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by userName? := .some "w", target := { pp? := "Nat" }, vars := #[{ - userName := "y✝", - isInaccessible := true, - type? := .some { pp? := "Nat" }, - }, { userName := "y", type? := .some { pp? := "Nat" }, } -- 2.44.1