@@ -174,6 +174,42 @@ let setPA = lam pa. lam n. lam y.
174174 else pa
175175end
176176
177+ -- `updatePA pa n f ` updates value (random access ) at index `n ` in
178+ -- `pa ` using function `f `. Note that the input `pa ` is not
179+ -- affected . The updated pure array is the result value . The
180+ -- complexity of the function is O(log n ) with a low constant factor
181+ recursive
182+ let updatePA : all a . PA a - > Int - > (a - > a ) - > PA a = lam pa . lam n . lam f .
183+ match pa with PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 ) then
184+ let n2 = modi n l in
185+ let i2 = divi n l in
186+ (switch i2
187+ case 0 then PANode (i ,l ,updatePA x0 n2 f ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
188+ case 1 then PANode (i ,l ,x0 ,updatePA x1 n2 f ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
189+ case 2 then PANode (i ,l ,x0 ,x1 ,updatePA x2 n2 f ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
190+ case 3 then PANode (i ,l ,x0 ,x1 ,x2 ,updatePA x3 n2 f ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
191+ case 4 then PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,updatePA x4 n2 f ,x5 ,x6 ,x7 ,x8 ,x9 )
192+ case 5 then PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,x4 ,updatePA x5 n2 f ,x6 ,x7 ,x8 ,x9 )
193+ case 6 then PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,updatePA x6 n2 f ,x7 ,x8 ,x9 )
194+ case 7 then PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,updatePA x7 n2 f ,x8 ,x9 )
195+ case 8 then PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,updatePA x8 n2 f ,x9 )
196+ case _ then PANode (i ,l ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,updatePA x9 n2 f ) end )
197+ else
198+ match pa with PAData (k ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 ) then
199+ (switch n
200+ case 0 then PAData (k ,f x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
201+ case 1 then PAData (k ,x0 ,f x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
202+ case 2 then PAData (k ,x0 ,x1 ,f x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
203+ case 3 then PAData (k ,x0 ,x1 ,x2 ,f x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
204+ case 4 then PAData (k ,x0 ,x1 ,x2 ,x3 ,f x4 ,x5 ,x6 ,x7 ,x8 ,x9 )
205+ case 5 then PAData (k ,x0 ,x1 ,x2 ,x3 ,x4 ,f x5 ,x6 ,x7 ,x8 ,x9 )
206+ case 6 then PAData (k ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,f x6 ,x7 ,x8 ,x9 )
207+ case 7 then PAData (k ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,f x7 ,x8 ,x9 )
208+ case 8 then PAData (k ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,f x8 ,x9 )
209+ case _ then PAData (k ,x0 ,x1 ,x2 ,x3 ,x4 ,x5 ,x6 ,x7 ,x8 ,f x9 ) end )
210+ else pa
211+ end
212+
177213
178214-- Helper for `makePA `
179215recursive
@@ -279,4 +315,3 @@ utest
279315 in
280316 maintest 0
281317with true
282-
0 commit comments