Skip to content

Commit 1c148db

Browse files
committed
IxVM kernel: route list_lookup through list_drop
`list_lookup(list, idx)` previously walked the list inline (Cons + match + recurse). Replacing the body with `head(load(list_drop(list, idx)))` lets `list_drop`'s memo dedup sublist pointers — content-addressed intermediates collapse across all lookups that pass through them. `lake exe check`: * Nat.add_comm: 54_670_728 → 54_350_107 FFT (-0.6%) * `_private....utf8DecodeChar?.helper₃`: 38_696_601_688 → 37_793_682_359 FFT (-2.3%)
1 parent 1141f2d commit 1c148db

1 file changed

Lines changed: 2 additions & 5 deletions

File tree

Ix/IxVM/Core.lean

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -52,11 +52,8 @@ def core := ⟦
5252
}
5353

5454
fn list_lookup‹T›(list: List‹T›, idx: G) -> T {
55-
let ListNode.Cons(v, rest) = load(list);
56-
match idx {
57-
0 => v,
58-
_ => list_lookup(rest, idx - 1),
59-
}
55+
let ListNode.Cons(v, _) = load(list_drop(list, idx));
56+
v
6057
}
6158

6259
fn list_lookup_u64‹T›(list: List‹T›, idx: U64) -> T {

0 commit comments

Comments
 (0)