From 8e3241c02ab65660169cdcb436883e27bd81e2b6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 15:02:43 -0700 Subject: [PATCH] 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)