We add helper classes with `outParam`.
@Kha This is similar to the `MonadExceptOf` modification.
Motivation: the new `StateRefT` (state monad implemented using
`IO.Ref`) makes is it quite cheap to have multiple states on the
stack. But, we need a mechanism for accessing the different states in
a convenient way.
Note that, I did not add a `MonadStateOf` class, but helper classes
such as `HasGet` which uses `outParam`. I will do the same for `MonadExcept`.
Summary:
- `get` gets the state on the top of the Monad stack
- `getThe σ` gets the state with type `σ`
- `modify f` modifies the state on the top of the Monad stack.
We use `modify fun s => { s with ... }` quite often, and we cannot
infer type of `s` here.
- `modifyThe σ f` allows us to select which state on the stack we are modifying.
- I didn't add `setThe`, since we usually can infer the state type at
`set s`. In the whole codebase, we have only one instance where this
is not true.
@Kha Please try to avoid importing `Lean.Meta`, it is huge, and any
change there was forcing a bunch of files to be recompiled since
`Parser.Extension` depends on `Parenthesizer`
@Kha Could you please double check these modifications.
I added a no-op for `checkRbpLt`. It is used at the `Sort` and `Type`
parsers.
As I described in previous commits, the `checkRBPGreater` comment and
implementation were misleading. It was actually succeeding when the
rbp was less than or equal to the given parameter. So, it was renamed
to `checkRbpLe`. So, is the depArrow parenthesizer ok? I did not check.
I updated the PPRoundtrip.lean.expected.out to make sure the tests
succeed, but we should revise it if there is a problem with the
modifications at Parenthesizer.lean
