`dbgTraceIfShared` を使って辞書がコピーされているか検証する例

この例は Zulip : Efficient hashmap counter from list から引用してきた。多少変えてある。

import Std

open Std (HashMap)

/-- リスト内の文字列をカウントする -/
def countFromList (xs : List String) : HashMap String Nat :=
  xs.foldl (init := HashMap.empty) fun hshMap str =>
    let cnt := hshMap[str]?.getD 0
    hshMap.insert str (cnt + 1)

#guard
  let actual := countFromList ["a", "a", "b", "c", "c", "c"] |>.toList
  let expected := [("c", 3), ("a", 2), ("b", 1)]
  actual = expected


namespace Ex1
  /- ## countFromList は、insert 処理を行うときに辞書をコピーしているか？ -/

  @[noinline]
  def insert (map : Std.HashMap String Nat) (x : String) (y : Nat) :=
    dbg_trace "insert called!"
    let map := dbgTraceIfShared "" map
    map.insert x y

  def countFromList (xs : List String) : HashMap String Nat :=
    xs.foldl (init := HashMap.empty) fun hshMap str =>
      let cnt := hshMap[str]?.getD 0
      insert hshMap str (cnt + 1)

  -- 最初の反復以外、コピーを行っていない！
  /--
    info: insert called!
    shared RC ⏎
    insert called!
    insert called!
    insert called!
    insert called!
    insert called!
    ---
    info: 2
  -/
  #guard_msgs (whitespace := lax) in
  #eval (countFromList ["a", "a", "b", "c", "c", "c"]) |>.getD "a" 0

end Ex1

Start with the supplied Lean snippet, especially Ex1.countFromList, dbgTraceIfShared, #guard_msgs, and #eval. Run the example and verify that its documented output shows sharing on the first insertion and no copying on later iterations. Done means the example is added in the repository's appropriate documentation location and remains reproducible.