make repl more extensible

[Qiu233]

All tests passed.

The 4 commits include in order:

clean

Collect the action functions from Main.lean to their own source files, along with their related message and response definitions.

polymorphism

• Define typeclass MonadREPL and related instances to provide the REPL effects, that is, command&proof snapshots manipulation.
• Define M := StateRefT State IO and its MonadREPL instance.

The main advantage is StateRefT being much more performant than StateT. The trade-off is M being specialized to IO, otherwise we would add many confusing STWorld stuff in the signature of effectful functions.
This makes sense since some existing actions really specialize (hard-coded) to IO and thus provide no polymorphism. Why not get it straight?

For the originally polymorphic functions with [Monad m] [MonadLiftT IO m], we add [MonadREPL m] to qualify m and return m a directly rather than wrap it in M m a. Under this setting, users can still make their own monad, implement MonadREPL for it, and call the polymorphic functions on it.

error handling

• Define ResultT m := ExceptT Error m
• Define local instance [ToJson e] [toJson a] : ToJson (Except e a)

Compared to the present manual error handling with sum-type, the new scheme will enable early-return and much more readable error handling in effectful actions.

Remark: The catch construct provided by Lean 4 supports dispatch by explicit exception type. Thus, we can still handle catch ex : IO.Error in ResultT m whenever [MonadLiftT IO m] is satisfied.

frameworking

Define two attributes repl_request and repl_request_handler to decouple request definition and handling from the main dispatch loop.
This design is completely based on compile-time code generation, thus is statically safe, and induces no runtime overhead.

The following is the definition and handler of Command:

@[repl_request]
structure Command extends CommandOptions where
  env : Option Nat
  cmd : String
deriving ToJson, FromJson

@[repl_request_handler Command]
def runCommand (s : Command) : ResultT M CommandResponse := do
  ...

The new command #mkInput Input in Main.lean generates the definition of type Input as well as its FromJson Input instance. The instance handles the try-chain so we don't need to put them manually in parse.

The main loop will then use an effectful macro make_repl_dispatch% input to parse a value of type Input, call the corresponding handler, and return (monadically) the result json. The generated code is designed to be compatible in any monadic environment, and can be made pure in Id monad.