2023-10-15 12:31:22 -07:00
|
|
|
|
import Pantograph.Goal
|
2023-10-15 17:15:23 -07:00
|
|
|
|
import Pantograph.Protocol
|
|
|
|
|
import Pantograph.Serial
|
|
|
|
|
import Pantograph.Symbol
|
2023-11-07 12:09:54 -08:00
|
|
|
|
import Lean.Data.HashMap
|
2023-08-13 21:19:06 -07:00
|
|
|
|
|
|
|
|
|
namespace Pantograph
|
|
|
|
|
|
|
|
|
|
structure Context where
|
2023-08-14 17:07:53 -07:00
|
|
|
|
imports: List String
|
2023-08-13 21:19:06 -07:00
|
|
|
|
|
|
|
|
|
/-- Stores state of the REPL -/
|
|
|
|
|
structure State where
|
2023-10-15 17:15:23 -07:00
|
|
|
|
options: Protocol.Options := {}
|
2023-11-07 12:09:54 -08:00
|
|
|
|
nextId: Nat := 0
|
|
|
|
|
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
|
2023-08-13 21:19:06 -07:00
|
|
|
|
|
2023-10-15 17:15:23 -07:00
|
|
|
|
/-- Main state monad for executing commands -/
|
2023-12-12 18:39:02 -08:00
|
|
|
|
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
|
2023-10-15 17:15:23 -07:00
|
|
|
|
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
|
|
|
|
|
-- certain monadic features in `MainM`
|
|
|
|
|
abbrev CR α := Except Protocol.InteractionError α
|
2023-08-13 21:19:06 -07:00
|
|
|
|
|
2023-12-12 18:39:02 -08:00
|
|
|
|
def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
|
|
|
|
|
metaM.run'
|
|
|
|
|
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
|
2023-12-08 16:17:16 -08:00
|
|
|
|
termElabM.run' (ctx := {
|
|
|
|
|
declName? := .none,
|
|
|
|
|
errToSorry := false,
|
2023-12-12 18:39:02 -08:00
|
|
|
|
}) |>.run'
|
2023-12-08 16:17:16 -08:00
|
|
|
|
|
2023-10-15 17:15:23 -07:00
|
|
|
|
def execute (command: Protocol.Command): MainM Lean.Json := do
|
2023-08-15 15:40:54 -07:00
|
|
|
|
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
|
2023-08-13 21:19:06 -07:00
|
|
|
|
match Lean.fromJson? command.payload with
|
2023-08-15 15:40:54 -07:00
|
|
|
|
| .ok args => do
|
|
|
|
|
match (← comm args) with
|
|
|
|
|
| .ok result => return Lean.toJson result
|
|
|
|
|
| .error ierror => return Lean.toJson ierror
|
2023-08-24 22:51:40 -07:00
|
|
|
|
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
|
2023-08-15 15:40:54 -07:00
|
|
|
|
match command.cmd with
|
2023-11-06 12:20:08 -08:00
|
|
|
|
| "reset" => run reset
|
|
|
|
|
| "stat" => run stat
|
|
|
|
|
| "expr.echo" => run expr_echo
|
|
|
|
|
| "lib.catalog" => run lib_catalog
|
|
|
|
|
| "lib.inspect" => run lib_inspect
|
|
|
|
|
| "options.set" => run options_set
|
|
|
|
|
| "options.print" => run options_print
|
|
|
|
|
| "goal.start" => run goal_start
|
|
|
|
|
| "goal.tactic" => run goal_tactic
|
|
|
|
|
| "goal.continue" => run goal_continue
|
|
|
|
|
| "goal.delete" => run goal_delete
|
2023-10-27 15:41:12 -07:00
|
|
|
|
| "goal.print" => run goal_print
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| cmd =>
|
2023-10-15 17:15:23 -07:00
|
|
|
|
let error: Protocol.InteractionError :=
|
2023-08-24 22:51:40 -07:00
|
|
|
|
errorCommand s!"Unknown command {cmd}"
|
2023-08-13 21:19:06 -07:00
|
|
|
|
return Lean.toJson error
|
|
|
|
|
where
|
2023-10-15 17:15:23 -07:00
|
|
|
|
errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
|
2023-08-24 22:51:40 -07:00
|
|
|
|
errorCommand := errorI "command"
|
2023-08-13 21:19:06 -07:00
|
|
|
|
errorIndex := errorI "index"
|
2023-08-14 17:07:53 -07:00
|
|
|
|
-- Command Functions
|
2023-10-15 17:15:23 -07:00
|
|
|
|
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
|
2023-08-14 17:07:53 -07:00
|
|
|
|
let state ← get
|
2023-08-27 19:58:52 -07:00
|
|
|
|
let nGoals := state.goalStates.size
|
2023-11-07 13:07:50 -08:00
|
|
|
|
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
|
2023-08-27 19:58:52 -07:00
|
|
|
|
return .ok { nGoals }
|
2023-10-15 17:15:23 -07:00
|
|
|
|
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
2023-08-27 19:58:52 -07:00
|
|
|
|
let state ← get
|
|
|
|
|
let nGoals := state.goalStates.size
|
|
|
|
|
return .ok { nGoals }
|
2023-10-15 17:15:23 -07:00
|
|
|
|
lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do
|
2023-08-13 21:19:06 -07:00
|
|
|
|
let env ← Lean.MonadEnv.getEnv
|
|
|
|
|
let names := env.constants.fold (init := #[]) (λ acc name info =>
|
|
|
|
|
match to_filtered_symbol name info with
|
|
|
|
|
| .some x => acc.push x
|
|
|
|
|
| .none => acc)
|
2023-08-15 15:40:54 -07:00
|
|
|
|
return .ok { symbols := names }
|
2023-10-15 17:15:23 -07:00
|
|
|
|
lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
|
2023-08-14 17:07:53 -07:00
|
|
|
|
let state ← get
|
2023-08-13 21:19:06 -07:00
|
|
|
|
let env ← Lean.MonadEnv.getEnv
|
2023-11-06 10:45:11 -08:00
|
|
|
|
let name := args.name.toName
|
2023-08-13 21:19:06 -07:00
|
|
|
|
let info? := env.find? name
|
|
|
|
|
match info? with
|
2023-08-15 15:40:54 -07:00
|
|
|
|
| none => return .error $ errorIndex s!"Symbol not found {args.name}"
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| some info =>
|
|
|
|
|
let module? := env.getModuleIdxFor? name >>=
|
|
|
|
|
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
|
2023-08-14 17:07:53 -07:00
|
|
|
|
let value? := match args.value?, info with
|
|
|
|
|
| .some true, _ => info.value?
|
|
|
|
|
| .some false, _ => .none
|
|
|
|
|
| .none, .defnInfo _ => info.value?
|
|
|
|
|
| .none, _ => .none
|
2023-08-15 15:40:54 -07:00
|
|
|
|
return .ok {
|
2023-12-12 18:39:02 -08:00
|
|
|
|
type := ← (serialize_expression state.options info.type).run',
|
|
|
|
|
value? := ← value?.mapM (λ v => serialize_expression state.options v |>.run'),
|
2023-12-05 20:20:08 -08:00
|
|
|
|
publicName? := Lean.privateToUserName? name |>.map (·.toString),
|
2023-12-06 15:05:04 -08:00
|
|
|
|
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
|
2023-11-25 15:07:56 -08:00
|
|
|
|
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
|
|
|
|
|
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
|
2023-08-13 21:19:06 -07:00
|
|
|
|
module? := module?
|
2023-08-15 15:40:54 -07:00
|
|
|
|
}
|
2023-10-15 17:15:23 -07:00
|
|
|
|
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
2023-08-14 21:43:40 -07:00
|
|
|
|
let state ← get
|
2023-08-13 21:19:06 -07:00
|
|
|
|
let env ← Lean.MonadEnv.getEnv
|
|
|
|
|
match syntax_from_str env args.expr with
|
2023-08-15 15:40:54 -07:00
|
|
|
|
| .error str => return .error $ errorI "parsing" str
|
2023-12-12 18:39:02 -08:00
|
|
|
|
| .ok syn => runTermElabM do
|
|
|
|
|
match ← syntax_to_expr syn with
|
2023-08-15 15:40:54 -07:00
|
|
|
|
| .error str => return .error $ errorI "elab" str
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| .ok expr => do
|
|
|
|
|
try
|
2023-08-14 21:43:40 -07:00
|
|
|
|
let type ← Lean.Meta.inferType expr
|
2023-08-15 15:40:54 -07:00
|
|
|
|
return .ok {
|
2023-08-14 21:43:40 -07:00
|
|
|
|
type := (← serialize_expression (options := state.options) type),
|
|
|
|
|
expr := (← serialize_expression (options := state.options) expr)
|
2023-08-15 15:40:54 -07:00
|
|
|
|
}
|
2023-08-13 21:19:06 -07:00
|
|
|
|
catch exception =>
|
2023-08-15 15:40:54 -07:00
|
|
|
|
return .error $ errorI "typing" (← exception.toMessageData.toString)
|
2023-10-15 17:15:23 -07:00
|
|
|
|
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
|
2023-08-16 19:25:32 -07:00
|
|
|
|
let state ← get
|
|
|
|
|
let options := state.options
|
|
|
|
|
set { state with
|
|
|
|
|
options := {
|
|
|
|
|
-- FIXME: This should be replaced with something more elegant
|
|
|
|
|
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
|
|
|
|
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
|
|
|
|
printExprAST := args.printExprAST?.getD options.printExprAST,
|
2023-10-26 22:47:42 -07:00
|
|
|
|
noRepeat := args.noRepeat?.getD options.noRepeat,
|
2023-08-16 19:25:32 -07:00
|
|
|
|
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
|
|
|
|
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
return .ok { }
|
2023-10-15 17:15:23 -07:00
|
|
|
|
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
|
2023-08-16 19:25:32 -07:00
|
|
|
|
return .ok (← get).options
|
2023-10-15 17:15:23 -07:00
|
|
|
|
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
|
2023-08-13 21:19:06 -07:00
|
|
|
|
let state ← get
|
|
|
|
|
let env ← Lean.MonadEnv.getEnv
|
2023-12-08 17:31:25 -08:00
|
|
|
|
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| .some expr, .none =>
|
|
|
|
|
(match syntax_from_str env expr with
|
|
|
|
|
| .error str => return .error <| errorI "parsing" str
|
|
|
|
|
| .ok syn => do
|
2023-12-08 17:31:25 -08:00
|
|
|
|
(match ← syntax_to_expr syn with
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| .error str => return .error <| errorI "elab" str
|
2023-12-08 17:31:25 -08:00
|
|
|
|
| .ok expr => return .ok (← GoalState.create expr)))
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| .none, .some copyFrom =>
|
2023-11-06 10:45:11 -08:00
|
|
|
|
(match env.find? <| copyFrom.toName with
|
2023-08-13 21:19:06 -07:00
|
|
|
|
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
|
2023-12-08 17:31:25 -08:00
|
|
|
|
| .some cInfo => return .ok (← GoalState.create cInfo.type))
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| _, _ =>
|
|
|
|
|
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
|
2023-08-13 21:19:06 -07:00
|
|
|
|
match expr? with
|
2023-08-15 15:40:54 -07:00
|
|
|
|
| .error error => return .error error
|
2023-12-08 17:31:25 -08:00
|
|
|
|
| .ok goalState =>
|
2023-11-07 12:09:54 -08:00
|
|
|
|
let stateId := state.nextId
|
|
|
|
|
set { state with
|
|
|
|
|
goalStates := state.goalStates.insert stateId goalState,
|
|
|
|
|
nextId := state.nextId + 1
|
|
|
|
|
}
|
2023-11-06 11:51:31 -08:00
|
|
|
|
return .ok { stateId, root := goalState.root.name.toString }
|
2023-10-15 17:15:23 -07:00
|
|
|
|
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
|
2023-08-13 21:19:06 -07:00
|
|
|
|
let state ← get
|
2023-11-07 12:09:54 -08:00
|
|
|
|
match state.goalStates.find? args.stateId with
|
2023-10-15 17:15:23 -07:00
|
|
|
|
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| .some goalState => do
|
|
|
|
|
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
|
|
|
|
|
| .some tactic, .none => do
|
2023-12-08 16:17:16 -08:00
|
|
|
|
pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| .none, .some expr => do
|
2023-12-08 16:17:16 -08:00
|
|
|
|
pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr))
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
|
|
|
|
|
match nextGoalState? with
|
|
|
|
|
| .error error => return .error error
|
|
|
|
|
| .ok (.success nextGoalState) =>
|
2023-11-07 12:09:54 -08:00
|
|
|
|
let nextStateId := state.nextId
|
2023-11-07 13:07:50 -08:00
|
|
|
|
set { state with
|
|
|
|
|
goalStates := state.goalStates.insert state.nextId nextGoalState,
|
|
|
|
|
nextId := state.nextId + 1,
|
|
|
|
|
}
|
2023-12-12 18:39:02 -08:00
|
|
|
|
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
|
2023-10-15 17:15:23 -07:00
|
|
|
|
return .ok {
|
|
|
|
|
nextStateId? := .some nextStateId,
|
2023-10-26 22:47:42 -07:00
|
|
|
|
goals? := .some goals,
|
2023-10-15 17:15:23 -07:00
|
|
|
|
}
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| .ok (.parseError message) =>
|
2023-10-15 17:15:23 -07:00
|
|
|
|
return .ok { parseError? := .some message }
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| .ok (.indexError goalId) =>
|
2023-10-15 17:15:23 -07:00
|
|
|
|
return .error $ errorIndex s!"Invalid goal id index {goalId}"
|
2023-10-27 15:32:59 -07:00
|
|
|
|
| .ok (.failure messages) =>
|
2023-08-15 15:40:54 -07:00
|
|
|
|
return .ok { tacticErrors? := .some messages }
|
2023-11-04 15:51:09 -07:00
|
|
|
|
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
|
|
|
|
|
let state ← get
|
2023-11-07 12:09:54 -08:00
|
|
|
|
match state.goalStates.find? args.target with
|
2023-11-04 15:51:09 -07:00
|
|
|
|
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
|
|
|
|
|
| .some target => do
|
|
|
|
|
let nextState? ← match args.branch?, args.goals? with
|
|
|
|
|
| .some branchId, .none => do
|
2023-11-07 12:09:54 -08:00
|
|
|
|
match state.goalStates.find? branchId with
|
2023-11-04 15:51:09 -07:00
|
|
|
|
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
|
|
|
|
|
| .some branch => pure $ target.continue branch
|
|
|
|
|
| .none, .some goals =>
|
2023-11-06 10:45:11 -08:00
|
|
|
|
let goals := goals.map (λ name => { name := name.toName })
|
2023-11-04 15:51:09 -07:00
|
|
|
|
pure $ target.resume goals
|
|
|
|
|
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
|
|
|
|
|
match nextState? with
|
2023-11-09 22:24:17 -08:00
|
|
|
|
| .error error => return .error <| errorI "structure" error
|
2023-11-04 15:51:09 -07:00
|
|
|
|
| .ok nextGoalState =>
|
2023-11-07 12:09:54 -08:00
|
|
|
|
let nextStateId := state.nextId
|
|
|
|
|
set { state with
|
|
|
|
|
goalStates := state.goalStates.insert nextStateId nextGoalState,
|
|
|
|
|
nextId := state.nextId + 1
|
|
|
|
|
}
|
2023-12-12 18:39:02 -08:00
|
|
|
|
let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
|
2023-11-04 15:51:09 -07:00
|
|
|
|
return .ok {
|
2023-11-09 22:24:17 -08:00
|
|
|
|
nextStateId,
|
|
|
|
|
goals,
|
2023-11-04 15:51:09 -07:00
|
|
|
|
}
|
2023-10-15 17:15:23 -07:00
|
|
|
|
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
|
2023-08-30 19:16:33 -07:00
|
|
|
|
let state ← get
|
2023-11-07 12:09:54 -08:00
|
|
|
|
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
|
2023-08-30 19:16:33 -07:00
|
|
|
|
set { state with goalStates }
|
|
|
|
|
return .ok {}
|
2023-10-27 15:41:12 -07:00
|
|
|
|
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
|
|
|
|
|
let state ← get
|
2023-11-07 12:09:54 -08:00
|
|
|
|
match state.goalStates.find? args.stateId with
|
2023-10-27 15:41:12 -07:00
|
|
|
|
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
2023-12-12 18:39:02 -08:00
|
|
|
|
| .some goalState => runMetaM <| do
|
2023-12-08 17:31:25 -08:00
|
|
|
|
goalState.restoreMetaM
|
2023-10-27 15:41:12 -07:00
|
|
|
|
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
|
|
|
|
|
return .ok {
|
|
|
|
|
root?,
|
|
|
|
|
}
|
2023-08-13 21:19:06 -07:00
|
|
|
|
|
|
|
|
|
end Pantograph
|