structure update performance issue

[leodemoura]

Consider the following variants of a cache function

import Lean

set_option trace.compiler.ir.result true

open Lean

structure State where
  keys    : Array Expr
  results : Array Expr

abbrev M := StateM State

def cache1 (i : Nat) (key : Expr) (result : Expr) : M Expr := do
  modify fun ⟨keys, results⟩ => { keys := keys.set! i key, results := results.set! i result }
  pure result

def cache2 (i : Nat) (key : Expr) (result : Expr) : M Expr := do
  modify fun s => { s with keys := s.keys.set! i key, results := s.results.set! i result }
  pure result

def cache3 (i : Nat) (key : Expr) (result : Expr) : M Expr := do
  modify fun s => { keys := s.keys.set! i key, results := s.results.set! i result }
  pure result

def cache4 (i : Nat) (key : Expr) (result : Expr) : M Expr := do
  modify fun s => { s with keys := s.keys.set! i key }
  modify fun s => { s with results := s.results.set! i result }
  pure result

Only cache1 is performing destructive array updates. This behavior is consistent with the algorithm described in the "Counting immutable beans" paper. Only cache1 is "matching" on the State structure. However, I think we used to have special support for structure updates. I might have broken it when we moved to the new frontend. This issue produced a performance problem fixed by https://github.com/leanprover/lean4/commit/4908eaf39603704e5d576439d420cab248ad68c0