feat: Simp, made simple #98
Conversation
YaelDillies
force-pushed
the
how-to-write-a-simproc
branch
from
5ed721a to
2feca6c
Compare
This PR adds the first blog post in a series of three to introduce the concept of simprocs and explain how to write them. The second blog post can be found here: #98 Co-authored-by : Yaël Dillies <[email protected]>
|
Part 1 references this post, so maybe it can also be updated to have working links pointing here too. |
posts/simp-made-simple.md
Outdated
| ``` | ||
| Note: The above snippet is a simplification and the constructors as shown actually belong to `Lean.TransformStep`, which `Lean.Meta.Simp.DStep` is an `abbrev` of. | ||
|
|
||
| <span style="color:red">**(Yaël): Why is there a mismatch in docstrings between `Step.continue` and `DStep.continue`? [Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Simp.2EStep.2Econtinue.20vs.20Simp.2EDStep.2Econtinue/with/509056271)**</span> |
There was a problem hiding this comment.
Do you want to remove this?
YaelDillies
force-pushed
the
how-to-write-a-simproc
branch
2 times, most recently
from
ed3714e to
04f3d50
Compare
Co-authored-by: Paul Lezeau <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Bhavik Mehta <[email protected]>
Co-authored-by: Bhavik Mehta <[email protected]>
YaelDillies
force-pushed
the
how-to-write-a-simproc
branch
from
04f3d50 to
f7aa206
Compare
Co-authored-by: blizzard_inc <[email protected]>
posts/simp-made-simple.md
Outdated
| ``` | ||
|
|
||
| `simp` does not consume bare elements of type `Simproc`. | ||
| Instead, a simproc is an element of type `Simproc` annotated with tbe extra data mentioned in the overview subsection, like whether the simproc is `pre` or `post`. |
There was a problem hiding this comment.
The section on Step is great, and contains a lot of detail. These latter sections seem somewhat rushed and the ending of the blogpost feels abrupt to me.
For example, this sentence about annotations with extra data... could that be accompanied by a code block that shows exactly what is going on?
And would it make sense to give the exact definition of the simpM monad, and add a bit more detail on it?
Maybe you could even end with a little cliff hanger about what will happen in the final blogpost?
There was a problem hiding this comment.
Sounds good! I'm planning on spending some extra time adding stuff about SimpM to the post this coming month.
There was a problem hiding this comment.
🏓 @Paul-Lez and @YaelDillies, it would be great to get this out! :-)
There was a problem hiding this comment.
@kim-em this is now ready to review if you fancy taking a look;)
If you're very busy, I think the first part is probably more ready/polished than the second one!
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Paul Lezeau <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Paul-Lez
force-pushed
the
how-to-write-a-simproc
branch
from
206fa34 to
3ac5a4c
Compare
| - `continue`. | ||
| It turns out that both `Nat.reduceDvd` and `reduceIte` also use the `continue` constructor. | ||
| Indeed, both these simprocs rely on the fact that some part of the expression | ||
| considered is simplifiable (e.g. the condition in the `if` statement). | ||
| When this is not the case, the `continue` constructor signals to `simp` that it should | ||
| *not* attempt to simplify the expression again using the same simproc to prevent | ||
| the simplification procedure from looping around. | ||
| More generally, `continue` is used in most simprocs as the "default" output | ||
| produced when the simproc was not able to make any simplification. |
There was a problem hiding this comment.
I don't completely understand this explanation, it seems like there are two things being mixed up here. Step indicates what to do when the simproc is done, right? But here "some part of the expression considered is simplifiable (e.g. the condition in the if statement)." refers to simplifying before the logic of the simproc itself. And then you describe when not to use .continue instead of when you do want to use it. Also because the .visit/.continue distinction is only relevant for pre-simprocs, which is mentioned above, but not here.
If we want to rework this completely, I would do something like: open the list with .continue since .continue none is the default. Then say something like:
...
.continueindicates that the simproc is done with this expression and its subexpressions. As a result,simpwill not not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping around.
|
|
||
| In the case where the two expressions `e` and `e'` are definitionally equal, | ||
| one can actually describe a simplification step using a simple structure, | ||
| namely `DStep` (where the "d" stands for "definitional"). |
There was a problem hiding this comment.
DSimprocs are mentioned only later on. So it is weird to discuss DStep here, it will make the reader wonder how they can return a DStep instead of a Step from a simproc.
| 3) The second monad transformer application: `ReaderT Simp.Context $ StateRefT Simp.State MetaM`. | ||
| The `SimpM` monad should also be able to access the "context" that `simp` is running in, e.g. which simp theorems it has access to and so on. This is captured by the type `Simp.Context`. | ||
| Here, the situation is not quite the same as when we were adding a `Simp.State` state to `MetaM`: while we will often want to change the state during the `simp` call, the context should always be the same (in programmer lingo: _immutable_) | ||
| Thus, we use a different monad transformer called `ReaderT`, which is almost identical to `StateT`, but outputs a new monad that can only read the type passed as parameter. |
There was a problem hiding this comment.
Mildly pedantic, but ReaderT can change the value in the calls it makes (e.g. ReaderT.adapt as equivalent to modify for a Reader). In programming language nerd terms, State(Ref)T gives you a global variable, and ReaderT gives you dynamic scoping.
(Does simp in practice use that though?)
10 participants
This is the second part of #97.
Co-authored-by: Paul Lezeau [email protected]