[polyml] ArraySlice.copy is inefficient

I've just committed the change I suggested. Give it a try and let me know how it works. Regards, David

On 20/06/2013 12:27, Peter Lammich wrote:

Hi Matt. Thanks for the quick answer.

What's about

...

...

2) Can ArraySlice.copy be patched to use System_move_words after
   a check that the arrays are actually not the same?

This would only be a minor change.

Is the patch below safe?

fun copy {src = Slice{array=s, start=srcStart, length=srcLen}, dst, di: int} = if di < 0 orelse di+srcLen > Array.length dst then raise General.Subscript

•    else if s <> dst then
  

•     System_move_words(RunCall.unsafeCast s, srcStart+1, RunCall.unsafeCast dst, di+1, srcLen)
     else (* We can't use System_move_words because of the potential overlap problem. *)
     let
         fun copyUp n =
         if n = srcLen then ()
         else (Array.update(dst, n+di, Array.sub(s, n+srcStart)); copyUp(n+1))
  
         and copyDown n =
         if n < 0 then ()
         else (Array.update(dst, n+di, Array.sub(s, n+srcStart)); copyDown(n-1))
     in
         if di > srcStart then copyDown(srcLen-1) else copyUp 0
     end
  
  

Best, Peter