Destructive Updates

Stream: lean4

[Tomaz Gomes]

Hi there! Is the following code linear? The comment above setD says that the update is done destructively if the reference counter is one, but I am having some trouble to understand if this is the case here or not... thanks!

def invertPermutation : List Nat → MetaM (List Nat) := fun p => do
  let size := p.length
  let p: Array Nat := ⟨p⟩
  let mut answer: Array Nat := ⟨List.replicate size 0⟩
  for i in [ : size] do
    answer := answer.setD (p.get! i) i
  return answer.toList

[Joachim Breitner]

Based on my (so far preliminary) understanding of the system: yes, it should be!

[Joachim Breitner]

I wonder if there is a way to assert that inside the code, so that one wouldn't have to guess.
Maybe a throwIfNotExclusive function?
Or a getStableName and throwIfStableNamesDiffer to check that answer points to the same location in memory throughout.
@Sebastian Ullrich , have you had any thoughts in that directions?

[Marc Huisinga]

You can also use dbgTraceIfShared for debugging:

def invertPermutation : List Nat → List Nat := fun p => Id.run do
  let size := p.length
  let p: Array Nat := ⟨p⟩
  let mut answer: Array Nat := ⟨List.replicate size 0⟩
  for i in [ : size] do
    answer := dbgTraceIfShared "answer" answer
    answer := answer.setD (p.get! i) i
  return answer.toList

-- [0, 0, 1]
#eval invertPermutation [1, 2, 3]

def invertPermutation2 : List Nat → List Nat := fun p => Id.run do
  let size := p.length
  let p: Array Nat := ⟨p⟩
  let mut answer: Array Nat := ⟨List.replicate size 0⟩
  let sharedAnswer := answer
  for i in [ : size] do
    answer := dbgTraceIfShared "answer" answer
    answer := answer.setD (p.get! i) i
  return answer.toList ++ sharedAnswer.toList

-- shared RC answer
-- [0, 0, 1, 0, 0, 0]
#eval invertPermutation2 [1, 2, 3]