Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680/// Key-value map type class. Types implementing Map provide ordered/// key-value storage with insertion, lookup, and deletion.////// `:= HashMap` -- a declared default carrier, matching/// `class FromListLiteral (L : Type -> Type := List)`'s own convention/// -- so a NULLARY call like `Map.empty` (no args to infer a carrier/// from at all) can still resolve via/// `resolve_class_method_call_d4_default_carrier` (`lang/scope.mo`)/// instead of giving up. Confirmed via `bootstrap compile cli/src/main.mo/// monad`: `lang/module.mo`'s `module_scope_cache_empty`'s own struct-/// literal field `entries := Map.empty` (declared field type `HashMap/// ModulePath ScopeData`, `ModuleScopeCache`) hit exactly this -- that/// caller has since been deleted as dead code, but the gap it found is/// real and this default is what closes it --/// `HashMap` is already this codebase's own preferred `Map` instance/// (see `filter_reachable_decls`'s own doc comment on why), so it's the/// correct default here too.pub class Map (M: (K : Type) -> (V : Type) -> Type := HashMap) { def empty : M K V def insert (key: K) (val: V) (m: M K V) : M K V def lookup (key: K) (m: M K V) : Option V def delete (key: K) (m: M K V) : M K V}/// Balanced binary search tree (AVL) key-value map.pub type BTreeMap K V { empty, node (key: K) (val: V) (left: BTreeMap K V) (right: BTreeMap K V) (height: I64)}def BTreeMap.beq [BEq K, BEq V] (a b : BTreeMap K V) : Bool := BTreeMap.fold (fn r ka va => r && Map.lookup ka b == some va ) true apub instance [BEq K, BEq V] BEq BTreeMap K V { def beq (a b : BTreeMap K V) : Bool := BTreeMap.beq a b}/// Eliminator: apply a function if the tree is a node, otherwise return default.def BTreeMap.with_node (m: BTreeMap K V) (f: K -> V -> BTreeMap K V -> BTreeMap K V -> I64 -> A) (default: A) : A := match m { BTreeMap.node k v l r h => f k v l r h, BTreeMap.empty => default }/// Return the height of a tree. Empty tree has height 0.def BTreeMap.height_of (m: BTreeMap K V) : I64 := BTreeMap.with_node m (fn k v l r h => h) 0/// Create a node, computing the height from children.def BTreeMap.create_node {K V : Type} (key: K) (val: V) (left: BTreeMap K V) (right: BTreeMap K V) : BTreeMap K V := let lh := BTreeMap.height_of left in let rh := BTreeMap.height_of right in if I64.gt lh rh then BTreeMap.node key val left right (lh + 1) else BTreeMap.node key val left right (rh + 1)/// Balance a key-value pair with left and right children./// Detects AVL imbalance and applies rotations inline.def BTreeMap.balance {K V : Type} (key: K) (val: V) (left: BTreeMap K V) (right: BTreeMap K V) : BTreeMap K V := let lh := BTreeMap.height_of left in let rh := BTreeMap.height_of right in if I64.gt lh (rh + 1) then BTreeMap.balance_left_heavy key val left right else if I64.gt rh (lh + 1) then BTreeMap.balance_right_heavy key val left right else BTreeMap.create_node key val left right/// Handle left-heavy imbalance: check children heights and apply LL or LR rotation.def BTreeMap.balance_left_heavy {K V : Type} (key: K) (val: V) (left: BTreeMap K V) (right: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node left (fn lk lv ll lr _ => let llh := BTreeMap.height_of ll in let lrh := BTreeMap.height_of lr in if I64.gt lrh llh then BTreeMap.rotate_lr key val lk lv ll lr right else BTreeMap.rotate_ll key val lk lv ll lr right) (BTreeMap.create_node key val left right)/// Left-right double rotation.def BTreeMap.rotate_lr {K V : Type} (root_key: K) (root_val: V) (l_key: K) (l_val: V) (ll: BTreeMap K V) (lr: BTreeMap K V) (right: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node lr (fn lrk lrv lrl lrr _ => let new_left := BTreeMap.create_node l_key l_val ll lrl in BTreeMap.create_node lrk lrv new_left (BTreeMap.create_node root_key root_val lrr right)) (BTreeMap.create_node root_key root_val (BTreeMap.create_node l_key l_val ll BTreeMap.empty) right)/// Left-left single rotation.def BTreeMap.rotate_ll {K V : Type} (root_key: K) (root_val: V) (l_key: K) (l_val: V) (ll: BTreeMap K V) (lr: BTreeMap K V) (right: BTreeMap K V) : BTreeMap K V := BTreeMap.create_node l_key l_val ll (BTreeMap.create_node root_key root_val lr right)/// Handle right-heavy imbalance: check children heights and apply RR or RL rotation.def BTreeMap.balance_right_heavy {K V : Type} (key: K) (val: V) (left: BTreeMap K V) (right: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node right (fn rk rv rl rr _ => let rlh := BTreeMap.height_of rl in let rrh := BTreeMap.height_of rr in if I64.gt rlh rrh then BTreeMap.rotate_rl key val left rk rv rl rr else BTreeMap.rotate_rr key val left rk rv rl rr) (BTreeMap.create_node key val left right)/// Right-left double rotation.def BTreeMap.rotate_rl {K V : Type} (root_key: K) (root_val: V) (left: BTreeMap K V) (r_key: K) (r_val: V) (rl: BTreeMap K V) (rr: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node rl (fn rlk rlv rll rlr _ => let new_right := BTreeMap.create_node r_key r_val rlr rr in BTreeMap.create_node rlk rlv (BTreeMap.create_node root_key root_val left rll) new_right) (BTreeMap.create_node root_key root_val left (BTreeMap.create_node r_key r_val BTreeMap.empty rr))/// Right-right single rotation.def BTreeMap.rotate_rr {K V : Type} (root_key: K) (root_val: V) (left: BTreeMap K V) (r_key: K) (r_val: V) (rl: BTreeMap K V) (rr: BTreeMap K V) : BTreeMap K V := BTreeMap.create_node r_key r_val (BTreeMap.create_node root_key root_val left rl) rr/// Find the leftmost (minimum) node in the tree.#[terminating]def BTreeMap.min_node (m: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node m (fn k v left right h => BTreeMap.with_node left (fn lk lv ll lr lh => BTreeMap.min_node left) m) BTreeMap.empty/// Fold over the map in ascending key order.def BTreeMap.fold (f: A -> K -> V -> A) (init: A) (m: BTreeMap K V) : A := match m { BTreeMap.empty => init, BTreeMap.node k v left right _ => let left_result := BTreeMap.fold f init left in let current_result := f left_result k v in BTreeMap.fold f current_result right }/// Convert the map to a list of (key, value) pairs in ascending key order.pub def BTreeMap.to_list {K V : Type} (m: BTreeMap K V) : List (Pair K V) := BTreeMap.to_list_asc m (List.empty : List (Pair K V))def BTreeMap.to_list_asc (m: BTreeMap K V) (acc: List (Pair K V)) : List (Pair K V) := match m { BTreeMap.empty => acc, BTreeMap.node k v left right _ => let acc1 := BTreeMap.to_list_asc right acc in let acc2 := List.cons (Pair.pair k v) acc1 in BTreeMap.to_list_asc left acc2 }/// Recursive insert helper. Takes comparison functions explicitly to avoid/// needing type class constraints on recursive self-calls./// NOTE: this function is ready for use but requires compiler support for/// evaluating class method references (BOrd.lt/BOrd.gt) passed as arguments/// from constrained instance bodies.#[terminating]def BTreeMap.insert_loop {K V : Type} (lt: K -> K -> Bool) (gt: K -> K -> Bool) (key: K) (val: V) (m: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node m (fn k v left right h => let insert_left : BTreeMap K V := BTreeMap.insert_loop lt gt key val left in let insert_right : BTreeMap K V := BTreeMap.insert_loop lt gt key val right in if lt key k then BTreeMap.balance k v insert_left right else if gt key k then BTreeMap.balance k v left insert_right else BTreeMap.node key val left right h) (BTreeMap.node key val BTreeMap.empty BTreeMap.empty 1)/// Recursive lookup helper.#[terminating]def BTreeMap.lookup_loop {K V : Type} (lt: K -> K -> Bool) (gt: K -> K -> Bool) (key: K) (m: BTreeMap K V) : Option V := match m { BTreeMap.empty => Option.none, BTreeMap.node k v left right _ => if lt key k then BTreeMap.lookup_loop lt gt key left else if gt key k then BTreeMap.lookup_loop lt gt key right else Option.some v }/// Recursive delete helper.#[terminating]def BTreeMap.delete_loop {K V : Type} (lt: K -> K -> Bool) (gt: K -> K -> Bool) (key: K) (m: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node m (fn k v left right h => let delete_left : BTreeMap K V := BTreeMap.delete_loop lt gt key left in let delete_right : BTreeMap K V := BTreeMap.delete_loop lt gt key right in if lt key k then BTreeMap.balance k v delete_left right else if gt key k then BTreeMap.balance k v left delete_right else BTreeMap.with_node left (fn lk lv ll lr lh => BTreeMap.with_node right (fn rk rv rl rr rh => BTreeMap.with_node (BTreeMap.min_node right) (fn mk mv _ _ _ => BTreeMap.balance mk mv left (BTreeMap.delete_loop lt gt mk right)) right) left) right) BTreeMap.empty/// Instance: BTreeMap implements the Map type class.pub instance [BOrd K] Map BTreeMap { def empty : BTreeMap K V := BTreeMap.empty // `with_node`'s callback params are explicitly typed (`left`/`right : // BTreeMap K V`) -- needed so `lang.scope`'s syntactic dictionary- // passing pass (`resolve_class_call_term`'s `Term.lam` case, the same // one that already registers any OTHER typed lambda/let param) can // see `left`/`right`'s own carrier when resolving the SELF-RECURSIVE // `Map.insert key val left`/`right` calls below. Confirmed load- // bearing via `examples/json.mo`'s `Map.insert` on a real `BTreeMap` // compiling to a hard "no instance found" failure without this. Typed // `fn` params inside a function-call argument position (this // `with_node` call) needed a separate self-hosted-parser fix first // (`lambda_dispatch`/`lambda_typed_params`, `lang/parser.mo`) -- // before that, this exact annotation broke self-hosted parsing // outright. #[terminating] def insert (key: K) (val: V) (m: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node m (fn (k : K) (v : V) (left : BTreeMap K V) (right : BTreeMap K V) (h : I64) => let insert_left : BTreeMap K V := Map.insert key val left in let insert_right : BTreeMap K V := Map.insert key val right in if BOrd.lt key k then BTreeMap.balance k v insert_left right else if BOrd.gt key k then BTreeMap.balance k v left insert_right else BTreeMap.node key val left right h) (BTreeMap.node key val BTreeMap.empty BTreeMap.empty 1) #[terminating] def lookup (key: K) (m: BTreeMap K V) : Option V := match m { BTreeMap.empty => Option.none, BTreeMap.node k v left right _ => if BOrd.lt key k then Map.lookup key left else if BOrd.gt key k then Map.lookup key right else Option.some v } // Same rationale as `insert`'s own doc comment above -- `left`/`right` // need real declared types for the self-recursive `Map.delete` calls // (both directly below and nested inside the `else` branch's own // `with_node` calls, which still see this outer `right` in scope) to // resolve their own `Map` instance dispatch. #[terminating] def delete (key: K) (m: BTreeMap K V) : BTreeMap K V := BTreeMap.with_node m (fn (k : K) (v : V) (left : BTreeMap K V) (right : BTreeMap K V) (h : I64) => let delete_left : BTreeMap K V := Map.delete key left in let delete_right : BTreeMap K V := Map.delete key right in if BOrd.lt key k then BTreeMap.balance k v delete_left right else if BOrd.gt key k then BTreeMap.balance k v left delete_right else BTreeMap.with_node left (fn lk lv ll lr lh => BTreeMap.with_node right (fn rk rv rl rr rh => BTreeMap.with_node (BTreeMap.min_node right) (fn mk mv _ _ _ => BTreeMap.balance mk mv left (Map.delete mk right)) right) left) right) BTreeMap.empty}/// ─── HashMap ────────────────────────────────────────────────/// Compute bucket index (0-255) from a hash value.////// 256, not 16. The table is two LEVELS of the same 16-way dispatch/// (`Bucket16` below), so widening cost no new dispatch code -- and the/// old 16 was badly under-provisioned for how this codebase actually/// uses `HashMap`: the compiler keeps ~4,200 def names and ~2,700/// reachability entries in one map, which at 16 buckets is ~260 entries/// per bucket, and `bucket_lookup_eq` scans a bucket LINEARLY. That made/// every lookup ~130 key comparisons on the hottest paths in the/// backend. At 256 the same maps sit at ~16 per bucket.pub def HashMap.bucket_of (hash: U64) : U64 := U64.mod hash 256u64/// One level of 16-way dispatch, generic in what a slot holds.////// Generic in `P` specifically so it can nest: a `HashMap`'s table is/// `Bucket16 (Bucket16 (List (Pair K V)))`, which is 256 buckets built/// from ONE 16-arm dispatch written once, rather than a 256-field/// constructor and two 256-arm chains.pub type Bucket16 P { buckets ( b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 : P)}/// Hash map type: 256-bucket chaining hash table, as 16x16.pub type HashMap K V { map (Bucket16 (Bucket16 (List (Pair K V))))}/// Every slot, in index order -- the basis for the whole-table folds/// (`to_list`, `is_empty`) that used to be written out 16 ways.def Bucket16.to_list {P : Type} (b : Bucket16 P) : List P := match b { Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 => [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15] }/// All 16 slots set to the same value.def Bucket16.replicate {P : Type} (e : P) : Bucket16 P := Bucket16.buckets e e e e e e e e e e e e e e e e/// Slot-wise combine of two levels -- what `merge_buckets` is.def Bucket16.map2 {P : Type} (f : P -> P -> P) (x : Bucket16 P) (y : Bucket16 P) : Bucket16 P := match x { Bucket16.buckets a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 => match y { Bucket16.buckets c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 => Bucket16.buckets (f a0 c0) (f a1 c1) (f a2 c2) (f a3 c3) (f a4 c4) (f a5 c5) (f a6 c6) (f a7 c7) (f a8 c8) (f a9 c9) (f a10 c10) (f a11 c11) (f a12 c12) (f a13 c13) (f a14 c14) (f a15 c15) } }/// 16 empty buckets.pub def HashMap.empty_buckets {K V : Type} : Bucket16 (Bucket16 (List (Pair K V))) := Bucket16.replicate (Bucket16.replicate (List.empty : List (Pair K V)))/// One 16-way step per level. The index is a flat 0-255 so that every/// caller -- `str_map_*` (`lang/codegen/util.mo`), `modpath_map_*` and/// `alias_map_*` (`lang/scope.mo`) -- keeps working unchanged against/// `bucket_of`/`get_bucket`/`set_bucket`; the two-level shape is an/// implementation detail of this file.def Bucket16.get {P : Type} (b : Bucket16 P) (idx : U64) : P := match b { Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 => if U64.beq 0u64 idx then b0 else if U64.beq 1u64 idx then b1 else if U64.beq 2u64 idx then b2 else if U64.beq 3u64 idx then b3 else if U64.beq 4u64 idx then b4 else if U64.beq 5u64 idx then b5 else if U64.beq 6u64 idx then b6 else if U64.beq 7u64 idx then b7 else if U64.beq 8u64 idx then b8 else if U64.beq 9u64 idx then b9 else if U64.beq 10u64 idx then b10 else if U64.beq 11u64 idx then b11 else if U64.beq 12u64 idx then b12 else if U64.beq 13u64 idx then b13 else if U64.beq 14u64 idx then b14 else b15 }def Bucket16.set {P : Type} (b : Bucket16 P) (idx : U64) (v : P) : Bucket16 P := match b { Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 => if U64.beq 0u64 idx then Bucket16.buckets v b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 1u64 idx then Bucket16.buckets b0 v b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 2u64 idx then Bucket16.buckets b0 b1 v b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 3u64 idx then Bucket16.buckets b0 b1 b2 v b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 4u64 idx then Bucket16.buckets b0 b1 b2 b3 v b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 5u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 v b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 6u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 v b7 b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 7u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 v b8 b9 b10 b11 b12 b13 b14 b15 else if U64.beq 8u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 v b9 b10 b11 b12 b13 b14 b15 else if U64.beq 9u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 v b10 b11 b12 b13 b14 b15 else if U64.beq 10u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 v b11 b12 b13 b14 b15 else if U64.beq 11u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 v b12 b13 b14 b15 else if U64.beq 12u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 v b13 b14 b15 else if U64.beq 13u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 v b14 b15 else if U64.beq 14u64 idx then Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 v b15 else Bucket16.buckets b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 v }pub def HashMap.get_bucket {K V : Type} (b: Bucket16 (Bucket16 (List (Pair K V)))) (idx: U64) : List (Pair K V) := Bucket16.get (Bucket16.get b (U64.div idx 16u64)) (U64.mod idx 16u64)pub def HashMap.set_bucket {K V : Type} (b: Bucket16 (Bucket16 (List (Pair K V)))) (idx: U64) (new_val: List (Pair K V)) : Bucket16 (Bucket16 (List (Pair K V))) := let hi : U64 := U64.div idx 16u64 in let lo : U64 := U64.mod idx 16u64 in Bucket16.set b hi (Bucket16.set (Bucket16.get b hi) lo new_val)/// Instance: HashMap implements the Map type class using hashing + ordering-based equality./// NOTE: uses BOrd K instead of BEq K due to evaluator instance resolution limitation./// The evaluator's resolve_class_method_instance picks the first registered instance/// (BOrd I64 is correctly first for I64 keys, but BEq Bool is first for BEq, producing/// wrong instance when abstract K is concrete I64 at runtime).pub instance [Hashable K, BOrd K] Map HashMap { def empty : HashMap K V := HashMap.map HashMap.empty_buckets #[terminating] def insert (key: K) (val: V) (m: HashMap K V) : HashMap K V := match m { HashMap.map buckets => let idx : U64 := HashMap.bucket_of (Hashable.hash key) in let bucket : List (Pair K V) := HashMap.get_bucket buckets idx in let new_bucket : List (Pair K V) := HashMap.bucket_insert BOrd.lt BOrd.gt key val bucket in HashMap.map (HashMap.set_bucket buckets idx new_bucket) } #[terminating] def lookup (key: K) (m: HashMap K V) : Option V := match m { HashMap.map buckets => let idx : U64 := HashMap.bucket_of (Hashable.hash key) in let bucket : List (Pair K V) := HashMap.get_bucket buckets idx in HashMap.bucket_lookup BOrd.lt BOrd.gt key bucket } #[terminating] def delete (key: K) (m: HashMap K V) : HashMap K V := match m { HashMap.map buckets => let idx : U64 := HashMap.bucket_of (Hashable.hash key) in let bucket : List (Pair K V) := HashMap.get_bucket buckets idx in let new_bucket : List (Pair K V) := HashMap.bucket_delete BOrd.lt BOrd.gt key bucket in HashMap.map (HashMap.set_bucket buckets idx new_bucket) }}def HashMap.bucket_insert {K V : Type} (lt: K -> K -> Bool) (gt: K -> K -> Bool) (key: K) (val: V) (bucket: List (Pair K V)) : List (Pair K V) := match bucket { List.empty => List.cons (Pair.pair key val) List.empty, List.cons pair rest => match pair { Pair.pair k v => if Bool.not (lt key k) && Bool.not (gt key k) then List.cons (Pair.pair key val) rest else List.cons pair (HashMap.bucket_insert lt gt key val rest) } }/// Equality-predicate variants of `bucket_insert`/`bucket_lookup`.////// The lt/gt versions above use `!lt(k1,k2) && !gt(k1,k2)` purely as an/// EQUALITY test -- the chain is not kept sorted (insert appends at the/// end; only an existing equal key is replaced in place), so ordering is/// never relied on. That costs TWO comparator calls per chain step, and/// for a key whose comparator renders a string (`lang/scope.mo`'s/// `modpath_lt`/`modpath_gt` both call `show_module_path`, which rebuilds/// the path via `List.map` + `intercalate`) that is four string/// constructions per step. These variants take a single `eq` instead.#[terminating]def HashMap.bucket_insert_eq {K V : Type} (eq: K -> K -> Bool) (key: K) (val: V) (bucket: List (Pair K V)) : List (Pair K V) := match bucket { List.empty => List.cons (Pair.pair key val) List.empty, List.cons pair rest => match pair { Pair.pair k v => if eq key k then List.cons (Pair.pair key val) rest else List.cons pair (HashMap.bucket_insert_eq eq key val rest) } }#[terminating]def HashMap.bucket_lookup_eq {K V : Type} (eq: K -> K -> Bool) (key: K) (bucket: List (Pair K V)) : Option V := match bucket { List.empty => Option.none, List.cons pair rest => match pair { Pair.pair k v => if eq key k then Option.some v else HashMap.bucket_lookup_eq eq key rest } }/// `bucket_lookup_eq`/`bucket_insert_eq` specialised to `String` keys,/// calling `String.beq` directly instead of taking it as a parameter.////// Passing a comparator is what a compiled binary pays dearly for. A/// `gdb` backtrace from a self-compile stuck in Stage 0c showed every/// single map probe going/// `str_map_lookup -> alloc_closure -> GC_malloc_kind -> GC_clear_stack`/// to build the `String.beq` closure, then reaching the comparison/// itself through `apply_closure2 -> apply_closure_dispatch ->/// String.beq_closure_shim` -- one GC allocation and an indirect call/// per bucket entry, for a function whose identity is known statically./// The Rust host pays none of this, which is most of why that pass ran/// ~20x worse compiled than interpreted rather than the usual ~4x.////// `String` because that is what every hot map in the compiler is keyed/// by: `llvm/src/strmap.mo`'s `str_map_*` (re-exported by/// `lang/codegen/util.mo`, where they used to live) and `lang/scope.mo`'s/// `alias_map_*`.#[terminating]pub def HashMap.bucket_lookup_str {V : Type} (key: String) (bucket: List (Pair String V)) : Option V := match bucket { List.empty => Option.none, List.cons pair rest => match pair { Pair.pair k v => if String.beq key k then Option.some v else HashMap.bucket_lookup_str key rest } }#[terminating]pub def HashMap.bucket_insert_str {V : Type} (key: String) (val: V) (bucket: List (Pair String V)) : List (Pair String V) := match bucket { List.empty => List.cons (Pair.pair key val) List.empty, List.cons pair rest => match pair { Pair.pair k v => if String.beq key k then List.cons (Pair.pair key val) rest else List.cons pair (HashMap.bucket_insert_str key val rest) } }/// Look up a key in a single bucket.#[terminating]def HashMap.bucket_lookup {K V : Type} (lt: K -> K -> Bool) (gt: K -> K -> Bool) (key: K) (bucket: List (Pair K V)) : Option V := match bucket { List.empty => Option.none, List.cons pair rest => match pair { Pair.pair k v => if Bool.not (lt key k) && Bool.not (gt key k) then Option.some v else HashMap.bucket_lookup lt gt key rest } }/// Delete a key from a single bucket.#[terminating]def HashMap.bucket_delete {K V : Type} (lt: K -> K -> Bool) (gt: K -> K -> Bool) (key: K) (bucket: List (Pair K V)) : List (Pair K V) := match bucket { List.empty => List.empty, List.cons pair rest => match pair { Pair.pair k v => if Bool.not (lt key k) && Bool.not (gt key k) then rest else List.cons pair (HashMap.bucket_delete lt gt key rest) } }/// Concatenate two `List (Pair K V)`s — a local helper rather than/// reaching for the prelude's own `List.append` (curried differently,/// per `lang/scope.mo`'s/`lang/module.mo`'s own local `list_append`/// helpers and their doc comments).#[terminating]def HashMap.concat_lists {K V : Type} (a : List (Pair K V)) (b : List (Pair K V)) : List (Pair K V) := match a { List.empty => b, List.cons x rest => List.cons x (HashMap.concat_lists rest b) }#[terminating]def HashMap.concat_all {K V : Type} (lists : List (List (Pair K V))) : List (Pair K V) := match lists { List.empty => List.empty, List.cons hd rest => HashMap.concat_lists hd (HashMap.concat_all rest) }/// Convert the map to a list of (key, value) pairs — unlike/// `BTreeMap.to_list`, in NO particular order (buckets are visited/// 0..15, each bucket's own chain in insertion order, which has no/// relationship to key order for a hash table).pub def HashMap.to_list {K V : Type} (m: HashMap K V) : List (Pair K V) := match m { HashMap.map outer => HashMap.concat_inners (Bucket16.to_list outer) }/// Flatten one outer level: each slot is itself 16 buckets.def HashMap.concat_inners {K V : Type} (inners : List (Bucket16 (List (Pair K V)))) : List (Pair K V) := match inners { List.empty => List.empty, List.cons inner rest => HashMap.concat_lists (HashMap.concat_all (Bucket16.to_list inner)) (HashMap.concat_inners rest) }/// Emptiness without walking entries. Recursive over the two levels/// rather than two 8-wide `&&` chains: the chain-length rule that shaped/// the old `buckets_all_empty_lo`/`_hi` pair does not scale to 256, and/// the recursion short-circuits on the first non-empty bucket anyway./// Kept cheap because `lang/module.mo`'s `merge_scope_data` uses it to/// skip a `to_list`-then-reinsert merge entirely.def HashMap.lists_all_empty {K V : Type} (ls : List (List (Pair K V))) : Bool := match ls { List.empty => true, List.cons l rest => if List.is_empty l then HashMap.lists_all_empty rest else false }def HashMap.inners_all_empty {K V : Type} (inners : List (Bucket16 (List (Pair K V)))) : Bool := match inners { List.empty => true, List.cons inner rest => if HashMap.lists_all_empty (Bucket16.to_list inner) then HashMap.inners_all_empty rest else false }pub def HashMap.is_empty {K V : Type} (m: HashMap K V) : Bool := match m { HashMap.map outer => HashMap.inners_all_empty (Bucket16.to_list outer) }/// NOTE: a generic `HashMap.insert_all [Hashable K, BOrd K] (pairs: List/// (Pair K V)) (acc: HashMap K V) : HashMap K V` (fold-inserting `pairs`/// into `acc`, the natural building block for a `HashMap.merge`) was/// tried here and removed — it doesn't work. This is a *broader* form of/// the limitation `HashMap`'s own `instance` block already documents for/// `Map.insert` specifically: from a standalone `[Constraint]`-annotated/// function (as opposed to directly inside an `instance ... { }` body),/// EVERY class-method call misbehaves, not just generic `Map` dispatch —/// confirmed empirically by bisection:/// - Calling generic `Map.insert k v acc` from such a function raises/// `unresolved global: Map.insert` at runtime./// - Calling `HashMap`'s own concrete bucket primitives instead/// (`Hashable.hash k`, `BOrd.lt`/`BOrd.gt` — the exact calls the/// `Map HashMap` instance's own `insert` body makes, and the/// workaround that fixed the above) still fails, but differently:/// a function no more complex than `match acc { HashMap.map _ =>/// true }` plus one `Hashable.hash k` call in the same body returns/// an under-applied `Closure` instead of its declared `Bool`, i.e./// the call site ends up with fewer arguments than the compiled/// function expects — apparently from however constraint/// dictionaries get threaded through the class-method calls, not/// from `match` itself (a `[Constraint]`-annotated function that/// never calls a class method, e.g. `qux` in the bisection, matches/// `acc` against `HashMap.map _` with no issue)./// - The exact same code, monomorphic (no `[Constraint]` list, all/// types concrete — e.g. specialized to a single key type instead of/// generic `K`) works with no issue, calling ordinary `Map.insert`//// `Map.lookup` exactly like `bench/scope_lookup.mo`'s/// `hashmap_build`/`hashmap_lookup_range` already do successfully./// Net: this evaluator's class-method dispatch is reliable inside/// `instance` bodies and inside monomorphic call sites, not inside/// generic `[Constraint]`-annotated helper functions. Callers needing a/// `HashMap` fold/merge should write a monomorphic version specialized/// to their concrete key/value types (see `lang/scope.mo`'s/// `merge_def_refs`) rather than a generic one here.////// `HashMap.merge_buckets` just below takes a different, better/// approach for the actual real-world need (`lang/module.mo`'s/// `merge_scope_data`, merging `ScopeData.def_refs`) — it needs no/// `[Constraint]` list at all, so it sidesteps this whole limitation/// rather than working around it./// Merge two `HashMap`s bucket-by-bucket, WITHOUT re-hashing any key —/// safe specifically because both sides already used the SAME hash/// function to place their entries, so a key that landed in bucket `i`/// on one side always lands in bucket `i` on the other too. `m1`'s/// entries come FIRST in each merged bucket's list, so `m1` wins over/// `m2` on a duplicate key (matches `HashMap.bucket_lookup`'s own/// head-first linear scan — same "first argument wins" precedence/// `merge_scope_data`/`list_append`'s own callers already rely on)./// Needs no `[Hashable K, BOrd K]` constraint (unlike a `to_list`+/// refold merge through `Map.insert`) since it never calls/// `Hashable.hash`/`BOrd.lt`/`BOrd.gt` — just 16 `List.append` calls,/// one per bucket, however many entries each side holds. Measurably/// cheaper than the `to_list`+refold pattern this replaces in/// `lang/module.mo`'s `merge_scope_data` (that pattern rebuilds the/// WHOLE combined map via one `Map.insert`-equivalent call per entry,/// re-walking/reallocating a bucket on every single insert; this does a/// fixed 16 bucket-pair appends regardless of N) — see AGENTS.md's/// performance section for the measured before/after.pub def HashMap.merge_buckets {K V : Type} (m1: HashMap K V) (m2: HashMap K V) : HashMap K V := match m1 { HashMap.map a => match m2 { HashMap.map b => HashMap.map (Bucket16.map2 (Bucket16.map2 List.append) a b) } }