refactor: composition pipeline and qpf body parsing #19
Conversation
|
I also added some refactors for Replace in the same pr here, will be looking for more TODOs as well |
There was a problem hiding this comment.
The diff is quite noisy and hard to review.
Generally, when doing big refactors, it's best to not move around and change code at the same time.
In this case, could you first submit a PR that takes the current code, and just copies it exactly into separate functions. That will have a large diff, but it should be relatively easy to confirm it's just moving code around and nothing semantically changed.
Then, in a second PR, make the semantic changes. That way, this second diff will be much more focussed, and it will be easier to see the relevant changes
| def Vector.mapM | ||
| {m : Type u → Type v} | ||
| {α : Type w} | ||
| {β : Type u} | ||
| [Monad m] | ||
| (l : Vector α n) | ||
| (f : α → m β) : m $ Vector β n := | ||
| match l with | ||
| | ⟨.cons hd tl, b⟩ => do | ||
| let v ← f hd | ||
| let x ← Vector.mapM ⟨tl, by rfl⟩ f | ||
| pure ⟨v :: x.val, by { | ||
| rw [List.length_cons] at b | ||
| rw [List.length_cons, x.property] | ||
| exact b | ||
| }⟩ | ||
| | ⟨.nil, h⟩ => pure ⟨[], by exact h⟩ |
There was a problem hiding this comment.
If Vector.mmap exists upstream, let's use that one
A general note on style:
- We generally prefer putting variables on fewer lines, rather than getting a very tall definition
- The type (and binders) should be indented one level more than the body of the definition
- There's no need for
{ ... }around the multiline proof,byis white-space sensitive rflis also a term, there is (usually!) no need to use the tactic version (as inby rfl)
| def Vector.mapM | |
| {m : Type u → Type v} | |
| {α : Type w} | |
| {β : Type u} | |
| [Monad m] | |
| (l : Vector α n) | |
| (f : α → m β) : m $ Vector β n := | |
| match l with | |
| | ⟨.cons hd tl, b⟩ => do | |
| let v ← f hd | |
| let x ← Vector.mapM ⟨tl, by rfl⟩ f | |
| pure ⟨v :: x.val, by { | |
| rw [List.length_cons] at b | |
| rw [List.length_cons, x.property] | |
| exact b | |
| }⟩ | |
| | ⟨.nil, h⟩ => pure ⟨[], by exact h⟩ | |
| def Vector.mapM {m : Type u → Type v} | |
| {α : Type w} {β : Type u} [Monad m] | |
| (l : Vector α n) (f : α → m β) : m $ Vector β n := | |
| match l with | |
| | ⟨.cons hd tl, b⟩ => do | |
| let v ← f hd | |
| let x ← Vector.mapM ⟨tl, rfl⟩ f | |
| pure ⟨v :: x.val, by simpa [List.length_cons, x.property] using b⟩ | |
| | ⟨.nil, h⟩ => pure ⟨[], by exact h⟩ |
|
|
||
| private def CtorArgs.reset : ReplaceM m Unit := do | ||
| let r ← StateT.get | ||
| let n := r.vars.size | ||
| let ctor: CtorArgs := ⟨#[], (Array.range n).map fun _ => #[]⟩ | ||
| StateT.set ⟨r.expr, r.vars, ctor⟩ | ||
| StateT.set { r with ctor } |
There was a problem hiding this comment.
This seems like an unrelated change, please put that in it's own PR.
If you put the trivial stuff separately, I can quickly review and merge that, removing noise from the current diff
Have to discuss if the changes made to
is_trivialare logically equivalent. Lots of use of bullet should be rewritten, this should probably be done together in the review to see the best way to write them. In some cases, there are bullet free versions below the line. Some changes to pattern matching, it might be worth modifying Comp.parseApp as well to allow for reuse of match results if this results in more readable code.