Skip to content

Commit 60aaab3

Browse files
Merge pull request #51 from Matthew-Mosior/rrbvector1-map-refactor
[ refactor ] RRBVector1 mmap
2 parents cacceb2 + fa21e84 commit 60aaab3

File tree

2 files changed

+26
-28
lines changed

2 files changed

+26
-28
lines changed

src/Data/RRBVector1/Sized.idr

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -763,17 +763,16 @@ viewr v@(Root _ tree) t =
763763

764764
private
765765
mapTree : {n : Nat}
766-
-> (a -> b)
766+
-> (a -> a)
767767
-> (arr : MArray s n (Tree1 s a))
768-
-> F1 s (MArray s n (Tree1 s b))
768+
-> F1 s (MArray s n (Tree1 s a))
769769
mapTree f arr t =
770-
let tmt # t := unsafeMArray1 n t
771-
in go 0 n tmt t
770+
go 0 n arr t
772771
where
773772
go : (m, x : Nat)
774-
-> (arr' : MArray s n (Tree1 s b))
773+
-> (arr' : MArray s n (Tree1 s a))
775774
-> {auto v : Ix x n}
776-
-> F1 s (MArray s n (Tree1 s b))
775+
-> F1 s (MArray s n (Tree1 s a))
777776
go m Z arr' t =
778777
arr' # t
779778
go m (S j) arr' t =
@@ -802,17 +801,17 @@ mapTree f arr t =
802801
Nothing =>
803802
(assert_total $ idris_crash "Data.RRBVector.mapTree.go: can't convert Nat to Fin") # t
804803
Just m' =>
805-
let arr''' # t := mmap f arr'' t
806-
arr'''' := Leaf {lsize=l} (l ** arr''')
807-
() # t := set arr' m' arr'''' t
804+
let () # t := mupdate f arr'' t
805+
arr''' := Leaf {lsize=l} (l ** arr'')
806+
() # t := set arr' m' arr''' t
808807
in go (S m) j arr' t
809808
810809
||| Apply the function to every element. O(n)
811810
export
812811
map : {n : Nat}
813-
-> (a -> b)
812+
-> (a -> a)
814813
-> RRBVector1 s n a
815-
-> F1 s (n' ** RRBVector1 s n' b)
814+
-> F1 s (n' ** RRBVector1 s n' a)
816815
map _ Empty t =
817816
(0 ** Empty) # t
818817
map f (Root sh (Balanced (b ** arr))) t =
@@ -824,9 +823,9 @@ map f (Root sh (Unbalanced (u ** arr) sizes)) t =
824823
arr'' := Unbalanced (u ** arr') sizes
825824
in (n ** Root sh arr'') # t
826825
map f (Root sh (Leaf (l ** arr))) t =
827-
let arr' # t := mmap f arr t
828-
arr'' := Leaf {lsize=l} (l ** arr')
829-
in (n ** Root sh arr'') # t
826+
let () # t := mupdate f arr t
827+
arr' := Leaf {lsize=l} (l ** arr)
828+
in (n ** Root sh arr') # t
830829
831830
--------------------------------------------------------------------------------
832831
-- Concatenation

src/Data/RRBVector1/Unsized.idr

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -749,17 +749,16 @@ viewr v@(Root size _ tree) t =
749749

750750
private
751751
mapTree : {n : Nat}
752-
-> (a -> b)
752+
-> (a -> a)
753753
-> (arr : MArray s n (Tree1 s a))
754-
-> F1 s (MArray s n (Tree1 s b))
754+
-> F1 s (MArray s n (Tree1 s a))
755755
mapTree f arr t =
756-
let tmt # t := unsafeMArray1 n t
757-
in go 0 n tmt t
756+
go 0 n arr t
758757
where
759758
go : (m, x : Nat)
760-
-> (arr' : MArray s n (Tree1 s b))
759+
-> (arr' : MArray s n (Tree1 s a))
761760
-> {auto v : Ix x n}
762-
-> F1 s (MArray s n (Tree1 s b))
761+
-> F1 s (MArray s n (Tree1 s a))
763762
go m Z arr' t =
764763
arr' # t
765764
go m (S j) arr' t =
@@ -788,16 +787,16 @@ mapTree f arr t =
788787
Nothing =>
789788
(assert_total $ idris_crash "Data.RRBVector.mapTree.go: can't convert Nat to Fin") # t
790789
Just m' =>
791-
let arr''' # t := mmap f arr'' t
792-
arr'''' := Leaf {lsize=l} (l ** arr''')
793-
() # t := set arr' m' arr'''' t
790+
let () # t := mupdate f arr'' t
791+
arr''' := Leaf {lsize=l} (l ** arr'')
792+
() # t := set arr' m' arr''' t
794793
in go (S m) j arr' t
795794
796795
||| Apply the function to every element. O(n)
797796
export
798-
map : (a -> b)
797+
map : (a -> a)
799798
-> RRBVector1 s a
800-
-> F1 s (RRBVector1 s b)
799+
-> F1 s (RRBVector1 s a)
801800
map _ Empty t =
802801
empty t
803802
map f (Root size sh (Balanced (b ** arr))) t =
@@ -809,9 +808,9 @@ map f (Root size sh (Unbalanced (u ** arr) sizes)) t =
809808
arr'' := Unbalanced (u ** arr') sizes
810809
in (Root size sh arr'') # t
811810
map f (Root size sh (Leaf (l ** arr))) t =
812-
let arr' # t := mmap f arr t
813-
arr'' := Leaf {lsize=l} (l ** arr')
814-
in (Root size sh arr'') # t
811+
let () # t := mupdate f arr t
812+
arr' := Leaf {lsize=l} (l ** arr)
813+
in (Root size sh arr') # t
815814
816815
--------------------------------------------------------------------------------
817816
-- Concatenation

0 commit comments

Comments
 (0)