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))