refactor(repl): Tactic into goal section

This commit is contained in:
Leni Aniva 2025-06-26 12:11:27 -07:00
parent 7fba24d57a
commit 4d9e229707
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 14 additions and 10 deletions

View File

@ -97,16 +97,7 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
} }
runCoreM $ termElabM.run' context state |>.run' runCoreM $ termElabM.run' context state |>.run'
section Frontend section Goal
structure CompilationUnit where
-- Environment immediately before the unit
env : Environment
boundary : Nat × Nat
invocations : List Protocol.InvokedTactic
sorrys : List Frontend.InfoWithContext
messages : Array String
newConstants : List Name
def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
let state ← getMainState let state ← getMainState
@ -175,6 +166,19 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult :=
| .ok (.failure messages) => | .ok (.failure messages) =>
return { messages? := .some messages } return { messages? := .some messages }
end Goal
section Frontend
structure CompilationUnit where
-- Environment immediately before the unit
env : Environment
boundary : Nat × Nat
invocations : List Protocol.InvokedTactic
sorrys : List Frontend.InfoWithContext
messages : Array String
newConstants : List Name
def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
let options := (← getMainState).options let options := (← getMainState).options
let (fileName, file) ← match args.fileName?, args.file? with let (fileName, file) ← match args.fileName?, args.file? with