[ fix ] Seq1#68
Conversation
|
@stefan-hoeck Would appreciate a review on the fixes to |
| export | ||
| data Seq1 : (s : Type) -> (e : Type) -> Type where | ||
| MkSeq1 : Ref s (FingerTree (Elem e)) | ||
| MkSeq1 : Ref s (Seq e) |
There was a problem hiding this comment.
Just a minor thing, but would using FingerTree directly here not make the rest of the code simpler. In the utility function that follow, there is usually an extra unwrapping step followed by a rewrapping, which - in my opinion - makes the code harder to read.
| let tr # t := ref1 Empty t | ||
| in (MkSeq1 tr) # t | ||
| let seq # t := ref1 (MkSeq Empty) t | ||
| in (MkSeq1 seq) # t |
There was a problem hiding this comment.
I'd suggest to not use parens here. They are not needed and hamper readability. Same in many other functions.
| let tr' # t := read1 tr t | ||
| in casswap1 tr (reverseTree id tr') t | ||
| reverse (MkSeq1 seq) t = | ||
| casupdate1 seq (\(MkSeq tr) => (MkSeq (reverseTree id tr), ())) t |
There was a problem hiding this comment.
Use casmod1 instead of casupdate1 here.
| let tr' # t := read1 tr t | ||
| in casswap1 tr (MkElem a `consTree` tr') t | ||
| (a `cons` (MkSeq1 seq)) t = | ||
| casupdate1 seq (\(MkSeq tr) => (MkSeq (MkElem a `consTree` tr), ())) t |
There was a problem hiding this comment.
Whenever the return type of a a CAS-loop is Unit, use casmod1 instead of casupdate1.
| in case viewLTree tr of | ||
| Just (MkElem a, _) => | ||
| Just a # t | ||
| Nothing => | ||
| Nothing # t | ||
|
|
There was a problem hiding this comment.
I'd suggest to use map here.
There was a problem hiding this comment.
I'm confused as to what map will do here for implementing head?
| tail (MkSeq1 seq) t = | ||
| casupdate1 seq | ||
| (\(MkSeq tr) => | ||
| case viewLTree tr of | ||
| Just (MkElem _, tr') => | ||
| (MkSeq tr', MkSeq1 seq) | ||
| Nothing => | ||
| (MkSeq tr, MkSeq1 seq) | ||
| ) t |
There was a problem hiding this comment.
If the goal of this function is in-place mutation, there is no need for a return value and it should probably just be F1' s. If the goal is to return the tail of the internal sequence, it should by typed and implemented similar to head. Currently, head and tail are somewhat at odds.
| viewr (MkSeq1 seq) t = | ||
| casupdate1 seq | ||
| (\(MkSeq tr) => | ||
| case viewRTree tr of | ||
| Just (tr', MkElem a) => | ||
| (MkSeq tr', Just (MkSeq1 seq, a)) | ||
| Nothing => | ||
| (MkSeq tr, Nothing) | ||
| ) t |
There was a problem hiding this comment.
Again, it is not clear why this should return a pair of values.
There was a problem hiding this comment.
viewl and viewr want to return a pair of values as these functions serve as "views", they allow inspection of either the first or last element, and pairs either the Seq1 without the first element (viewl), or Seq1 without the last element (viewr).
| seq'' # t | ||
| Nothing => | ||
| empty t | ||
| init (MkSeq1 seq) t = |
There was a problem hiding this comment.
init and last are again at odds, similar to head and tail.
There was a problem hiding this comment.
I think the idea is that head and last are inverses, as are init and tail.
head and last are non-mutating, and init and tail are mutating.
|
I added some opinionated comments. Thread-safety looks OK, but should ideally be tested for all functions not only one. The semantics of some of the functions is not always clear: See the comment for Mere mutation functions should probably always be of type |
Thank you for your thorough review. I've addressed all comments, and have made quite a few changes based on them. I think this is in a good spot for a re-review. |
2 participants
This PR fixes the
Seq1implementation by utilizingcasupdate1to ensure thread-safe operations.Closes #63