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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483/// Constructor tags and arities.////// A constructor's runtime tag and field count are keyed in their OWN/// namespace, not the def-symbol one: `MatchCase` carries only a bare/// `Identifier` (the parser parses `Slim.mk` and discards the/// qualifier), so dispatch can never supply more than a bare name.////// Tags are therefore keyed three ways at one build site: the composite/// `bare#arity`, the owner-qualified `Type.ctor` alias, and the bare/// name -- the last carrying a `-1` ambiguity sentinel when two types/// claim it at different arities. Keying by bare name ALONE is what/// once put 283 constructors on one tag at seven arities and sized/// allocations wrongly; the builtin tiers are checked for a matching/// arity for the same reason.use llvm::strmap {str_map_empty, str_map_insert, str_map_lookup}use std::list {List.length}use lib::types {InductConstructor, Inductive, Struct}use lib::codegen::ctx {CodegenCtx, ctx_lookup_ctor_arity, ctx_lookup_ctor_tag}use lib::codegen::symbols {extract_base_name, name_path_to_str, symbol_identifier}use lib::codegen::util {}use std::map {HashMap}/// The builtin constructors' tags, keyed by BOTH their qualified/// ("RawIO.io", "IO.mk") and base ("io") name forms -- built once, looked/// up via `str_map_lookup` instead of a hand-rolled `if/else-if` chain./// The values are FIXED rather than per-program, because `runtime.c`/// allocates some of them directly and a C function cannot consult the/// per-program numbering. 17/18 are that file's `MONAD_FIBER_TAG` //// `MONAD_SCOPE_TAG` handle kinds, so no constructor may be minted onto/// them; 16 is `Array.mk` and 19 is `IO.mk`.#[partial]def builtin_ctor_tags : HashMap String I64 := let m := str_map_empty in let m := str_map_insert "RawIO.io" 7 m in let m := str_map_insert "IO.mk" 19 m in let m := str_map_insert "Unit.unit" 0 m in let m := str_map_insert "Bool.true" 1 m in let m := str_map_insert "Bool.false" 2 m in let m := str_map_insert "Option.none" 3 m in let m := str_map_insert "Option.some" 4 m in let m := str_map_insert "List.empty" 5 m in let m := str_map_insert "List.cons" 6 m in let m := str_map_insert "unit" 0 m in let m := str_map_insert "true" 1 m in let m := str_map_insert "false" 2 m in let m := str_map_insert "none" 3 m in let m := str_map_insert "some" 4 m in let m := str_map_insert "empty" 5 m in let m := str_map_insert "cons" 6 m in let m := str_map_insert "io" 7 m in let m := str_map_insert "trivial" 8 m in let m := str_map_insert "refl" 9 m in let m := str_map_insert "ok" 10 m in let m := str_map_insert "err" 11 m in let m := str_map_insert "zero" 12 m in let m := str_map_insert "succ" 13 m in let m := str_map_insert "nil" 14 m in let m := str_map_insert "pair" 15 m in // `std/array.mo`'s `Array.mk`/`ArrayBuilder.mk`. A builtin tag, // even though the type is declared in `std/` rather than `init/`, // because `runtime.c`'s `monad_array_*` ALLOCATE one directly and // a C function cannot consult the per-program constructor // numbering. The two share a tag deliberately: they are the same // representation (`std/array.mo`'s own doc comment), and // `array_freeze` converts between them by copying, never by // re-tagging. // // NOTE the arity subtlety: unlike every other entry here, an // `Array`'s field count is its LENGTH, not a fixed number, so // `builtin_ctor_arities` records 0 -- the arity a bare, unapplied // `Array.mk` really has. Only the natives allocate longer ones. let m := str_map_insert "Array.mk" 16 m in let m := str_map_insert "ArrayBuilder.mk" 16 m in m/// Field counts for the same builtin constructors `builtin_ctor_tags`/// enumerates -- needed by `constructor_arity` (see its own doc comment/// for why: a bare, unapplied reference to an arity>0 constructor, e.g./// `List.map Option.some xs`, needs to know it must box a real closure,/// not just allocate a 0-field object).#[partial]def builtin_ctor_arities : HashMap String I64 := let m := str_map_empty in let m := str_map_insert "RawIO.io" 1 m in let m := str_map_insert "IO.mk" 1 m in let m := str_map_insert "Unit.unit" 0 m in let m := str_map_insert "Bool.true" 0 m in let m := str_map_insert "Bool.false" 0 m in let m := str_map_insert "Option.none" 0 m in let m := str_map_insert "Option.some" 1 m in let m := str_map_insert "List.empty" 0 m in let m := str_map_insert "List.cons" 2 m in let m := str_map_insert "unit" 0 m in let m := str_map_insert "true" 0 m in let m := str_map_insert "false" 0 m in let m := str_map_insert "none" 0 m in let m := str_map_insert "some" 1 m in let m := str_map_insert "empty" 0 m in let m := str_map_insert "cons" 2 m in let m := str_map_insert "io" 1 m in let m := str_map_insert "trivial" 0 m in let m := str_map_insert "refl" 0 m in let m := str_map_insert "ok" 1 m in let m := str_map_insert "err" 1 m in let m := str_map_insert "zero" 0 m in let m := str_map_insert "succ" 1 m in let m := str_map_insert "nil" 0 m in let m := str_map_insert "pair" 2 m in // See `builtin_ctor_tags`' note: 0 is the arity of a bare // `Array.mk`, which is also the empty array. A populated one's // field count comes from `alloc_constructor`, not from here. let m := str_map_insert "Array.mk" 0 m in let m := str_map_insert "ArrayBuilder.mk" 0 m in m/// Falls back to `c`'s own dynamically-built `ctor_tags` table/// (`build_constructor_tag_map`) for anything not in `builtin_ctor_tags`/// -- every user-defined inductive's constructor, and any BUILTIN/// constructor referenced by its full dotted name in a shape/// `builtin_ctor_tags` doesn't happen to enumerate. The ctx tiers try/// the name AS WRITTEN first ("Box.mk" -- the map carries an/// owner-qualified alias per constructor) and then its bare name --/// which for a bare name claimed at several arities is the -1/// ambiguity sentinel, answered as 0 by `bare_ctor_tag`. Callers that/// know the constructor's field count should use `constructor_tag_at`/// instead: its composite bare#arity key distinguishes the differing-/// arity colliders this bare-name path cannot.#[partial]def constructor_tag (c : CodegenCtx) (name : String) : I64 := let base_name := extract_base_name name in match str_map_lookup name builtin_ctor_tags { Option.some tag => tag, Option.none => match str_map_lookup base_name builtin_ctor_tags { Option.some tag => tag, Option.none => match ctx_lookup_ctor_tag c name { Option.some tag => tag, Option.none => bare_ctor_tag c base_name, }, }, }/// Same 3-tier lookup shape as `constructor_tag` just above (hardcoded/// builtin table, by full name then base name, then `c`'s own/// dynamically-built table -- name as written, then bare), for a/// constructor's FIELD COUNT instead of its tag. Needed by/// `compile_db_term_ir`'s `Term.var` case (a bare, unapplied/// constructor reference in VALUE position, e.g. `List.map Identifier.id/// ids` or `List.map Option.some xs`): that case used to/// unconditionally allocate a 0-field object regardless of the/// constructor's REAL declared arity, correct only for a genuinely/// nullary constructor -- confirmed as a real gap via a live self-/// compiled binary's own SIGSEGV (jumping to a garbage function pointer/// inside `List.map`'s `apply_closure1`, traced to `ids_to_module_path`'s/// own `List.map Identifier.id ids`, a 1-field constructor referenced/// bare). The ctx tiers key `ctor_arities` by the owner-qualified/// alias first ("Box.mk" -- how such a reference is actually written)/// and the bare name second; a bare name claimed at several arities/// records its FIRST-encountered arity there -- an arbitrary but/// deterministic answer for a shape that is genuinely unresolvable/// without the owning type (write the reference qualified and the/// alias tier answers exactly). Falls back to 0 (matching/// `constructor_tag`'s own "unknown -> 0" fallback) if the name isn't/// found anywhere -- a name that isn't even a known constructor never/// reaches this function to begin with (`is_constructor_var` already/// gated the caller).#[partial]def constructor_arity (c : CodegenCtx) (name : String) : I64 := let base_name := extract_base_name name in match str_map_lookup name builtin_ctor_arities { Option.some arity => arity, Option.none => // The owner-qualified ctx alias ("CompileResult.ok") is tried // BEFORE the bare-name builtin tier, for the same reason // `constructor_tag_at` reorders its own tiers: a user // constructor sharing a builtin's bare name would otherwise // report the BUILTIN's field count and allocate the wrong // size. The full-name builtin tier above still wins for a // genuine "Result.ok". match ctx_lookup_ctor_arity c name { Option.some arity => arity, Option.none => match str_map_lookup base_name builtin_ctor_arities { Option.some arity => arity, Option.none => match ctx_lookup_ctor_arity c base_name { Option.some arity => arity, Option.none => 0, }, }, }, }/// Struct `mk`s, as claims -- the missing half of `collect_ctor_claims`.////// A struct has exactly one implicit constructor, named `mk`, whose/// field count is the struct's own. The claim's keys are rendered the/// same way the inductive path renders them (`symbol_identifier` is the/// same rendering a reference is looked up under, `collect_ctor_claims`/// uses `name_path_to_str` on a one-segment path) so the qualified key/// matches a source-written `Point.mk` exactly.////// These claims reach ONLY the arity map (`build_constructor_arity_map_/// with_structs`), never the tag map: a struct literal allocates with/// `constructor_tag_at c "mk" arity`, whose composite key is absent for a/// struct and falls through to the bare-name tier -- the same tag a/// `Point.mk` reference gets, so the two agree without a tag of their/// own (see `constructor_tag_at`'s own note that struct `mk`s stay out/// of the tag map).#[partial]def collect_struct_ctor_claims (structs : List Struct) (acc : List CtorClaim) : List CtorClaim := match structs { List.empty => acc, List.cons s rest => match s { Struct.mk name fields _attrs _vis => let claim : CtorClaim := { bare := "mk", arity := List.length fields, qualified := String.concat (symbol_identifier name) ".mk", } in collect_struct_ctor_claims rest (List.cons claim acc), },}/// Check if a variable name is a known constructor./// Handles both simple names ("unit", "true") and qualified names ("Unit.unit", "RawIO.io", "IO.mk"),/// falling back to `c`'s own dynamically-built `ctor_tags` table/// (`build_constructor_tag_map`) for anything not in `builtin_ctor_tags`/// -- see `constructor_tag`'s own doc comment. A bare name claimed at/// several arities still has a ctx-table entry (the -1 ambiguity/// sentinel, see `constructor_tag_at`) -- presence alone answers this/// question.////// The last tier is the ARITY table, which is the only table that knows/// about structs at all (`collect_struct_ctor_claims`' own doc comment):/// a struct's `mk` carries no tag-map entry, so `Point.mk` -- the shape/// a decl-gen macro emits for a struct (std/derive.mo's `lens_setter`)/// -- answered `false` here and compiled as a call to a nonexistent/// function (`llc: use of undefined value '@Point.mk'`). It is looked up/// as WRITTEN rather than by base name on purpose: bare `mk` is claimed/// by hundreds of types at seven arities, so only the owner-qualified/// form identifies one unambiguously -- which is also how such a/// reference is always written.#[partial]def is_constructor_var (c : CodegenCtx) (name : String) : Bool := let base_name := extract_base_name name in match str_map_lookup base_name builtin_ctor_tags { Option.some _ => true, Option.none => match ctx_lookup_ctor_tag c base_name { Option.some _ => true, Option.none => match ctx_lookup_ctor_arity c name { Option.some _ => true, Option.none => false, }, }, }/// The composite tag-map key: a constructor's BARE name plus its/// declared field count, joined by `#` ("mk#7", "present#2"). `#` never/// appears in an identifier, so the composite key can never collide/// with a qualified "Type.ctor" alias or a bare name. This is the key/// that makes same-bare-name constructors at DIFFERING arities/// distinguishable at runtime -- see `build_constructor_tag_map`.def ctor_composite_key (name : String) (arity : I64) : String := String.concat name (String.concat "#" (I64.to_string arity))/// The ctx-table's bare entry, answered as a tag. A bare constructor/// name claimed at exactly ONE arity has a real tag here; one claimed at/// several arities gets the -1 ambiguity sentinel instead (see/// `constructor_tag_at`), which this answers as 0 -- the same "unknown"/// answer a missing entry gets, and unreachable for real shapes, since/// every caller that knows its arity goes through the composite key/// first.#[partial]def bare_ctor_tag (c : CodegenCtx) (bare : String) : I64 := match ctx_lookup_ctor_tag c bare { Option.some tag => if I64.gt tag (-1) then tag else 0, Option.none => 0, }/// One constructor "claim" collected from the declared `Inductive`s:/// the constructor's BARE rendered name (how match dispatch will refer/// to it), its declared FIELD COUNT (how the composite key/// disambiguates colliders), and its owner-QUALIFIED name/// ("TypeName.ctorName" -- how a value-position reference is written).pub struct CtorClaim { bare : String, arity : I64, qualified : String,}/// Collect every declared constructor's claim, in declaration order./// `Inductive.name` is the OWNING type's path -- the qualifier every/// `mk`-shaped bare name needs to become unique.#[partial]def collect_ctor_claims (owner : String) (ctors : List InductConstructor) (acc : List CtorClaim) : List CtorClaim := match ctors { List.empty => acc, List.cons c rest => match c { InductConstructor.mk name params _typ => let claim : CtorClaim := { bare := name_path_to_str name, arity := List.length params, qualified := String.concat owner (String.concat "." (name_path_to_str name)), } in collect_ctor_claims owner rest (List.cons claim acc), },}#[partial]def collect_ctor_claims_inds (inds : List Inductive) (acc : List CtorClaim) : List CtorClaim := match inds { List.empty => acc, List.cons ind rest => match ind { Inductive.mk name _params _typ constructors _attrs _vis => collect_ctor_claims_inds rest (collect_ctor_claims (name_path_to_str name) constructors acc), },}/// The per-bare-name arity scan every map build starts with: the FIRST/// arity each bare name was claimed at, and whether it was later/// claimed at a DIFFERENT arity too (the ambiguity marker -- a bare/// name with several arities cannot answer an arity-unknown lookup and/// gets the -1 sentinel in the tag map).pub struct BareArityScan { first : HashMap String I64, multi : HashMap String Bool,}#[partial]def scan_ctor_bare_arities (claims : List CtorClaim) (st : BareArityScan) : BareArityScan := match claims { List.empty => st, List.cons cl rest => match cl { CtorClaim.mk bare arity _qualified => let st2 := match str_map_lookup bare st.first { Option.some first => if arity == first then st else { st with multi := str_map_insert bare true st.multi }, Option.none => { st with first := str_map_insert bare arity st.first }, } in scan_ctor_bare_arities rest st2, },}pub struct CtorTagBuildState { next_tag : I64, tags : HashMap String I64,}/// Assign one fresh, globally-unique tag per DISTINCT bare#arity pair,/// first-encounter order. Duplicate claims (the same pair again, a/// module loaded twice, another type with the same-named same-arity/// constructor) reuse the tag -- same-layout claimants are/// interchangeable at runtime by construction, since alloc and match/// both key by (name, arity).#[partial]def assign_ctor_pair_tags (claims : List CtorClaim) (st : CtorTagBuildState) : CtorTagBuildState := match claims { List.empty => st, List.cons cl rest => match cl { CtorClaim.mk bare arity _qualified => let comp := ctor_composite_key bare arity in let st2 := match str_map_lookup comp st.tags { Option.some _ => st, Option.none => { st with tags := str_map_insert comp st.next_tag st.tags, next_tag := st.next_tag + 1 }, } in assign_ctor_pair_tags rest st2, },}/// Add the two alias keys every claim also gets, on top of the/// composite keys: the owner-qualified name ("Box.mk" -> Box's own/// tag -- the tier a value-position reference written qualified hits)/// and the bare name (real tag when the name is claimed at one single/// arity, the -1 ambiguity sentinel when claimed at several -- so/// `is_constructor_var` still sees presence, while arity-unknown tag/// lookups degrade to 0 rather than silently answering one claimant).#[partial]def add_ctor_alias_tags (claims : List CtorClaim) (scan : BareArityScan) (tags : HashMap String I64) : HashMap String I64 := match claims { List.empty => tags, List.cons cl rest => match cl { CtorClaim.mk bare arity qualified => let comp := ctor_composite_key bare arity in let tag := match str_map_lookup comp tags { Option.some t => t, Option.none => 0, } in let bare_entry := match str_map_lookup bare scan.multi { Option.some amb => if amb then (-1) else tag, Option.none => tag, } in add_ctor_alias_tags rest scan (str_map_insert bare bare_entry (str_map_insert qualified tag tags)), },}/// Builds `ctor_tags` for every constructor of every declared/// `Inductive` in the whole program, keyed THREE ways:////// - `bare#arity` (the composite key -- `constructor_tag_at`'s ctx/// tier): one fresh tag per distinct pair, so constructors sharing/// a bare name at differing arities -- the 283-way `mk` collision/// that cost the v29 rung-3 ladder rung -- get DIFFERENT tags and/// can never be confused at alloc or match dispatch;/// - `TypeName.ctorName` (the owner-qualified alias --/// `constructor_tag`/`constructor_arity`'s ctx tier): the shape a/// value-position reference is actually written in;/// - the bare name alone (last-resort tier): real tag when claimed/// at one arity, -1 sentinel when ambiguous.////// Starts at 16 -- the number this has always started at. The fixed/// builtin range it was chosen to clear (`constructor_tag`'s 0-15) has/// since grown to reach 16 (`Array.mk`) and 19 (`IO.mk`), so a dynamic/// tag can now coincide with a builtin's; those tiers are consulted/// BEFORE this map, so a coincidence is reachable only through a/// composite-key miss./// Matching a bare name with its arity at every alloc/dispatch site is/// what makes the composite key sufficient without threading the/// scrutinee's static type into match compilation (`MatchCase` carries/// only the bare Identifier -- the parser accepts and drops the/// qualifier -- but it also carries the case's own binder list, which/// IS the arity; see `build_match_chain`)./// See `implementations/2026-08-29-user-defined-constructor-codegen-gap.md`/// for the map's original single-key design.#[partial]def build_constructor_tag_map (inds : List Inductive) : HashMap String I64 := let claims := List.reverse (collect_ctor_claims_inds inds List.empty) in let scan := scan_ctor_bare_arities claims { first := str_map_empty, multi := str_map_empty } in let assigned := assign_ctor_pair_tags claims { next_tag := 16, tags := str_map_empty } in add_ctor_alias_tags claims scan assigned.tags/// Mirrors `build_constructor_tag_map`'s qualified/bare alias keying/// (built from the same claim scan) but records each constructor's/// FIELD COUNT instead of its tag -- see `constructor_arity`'s own doc/// comment for why this is needed. A bare name claimed at several/// arities records its FIRST-encountered arity under the bare key --/// arbitrary but deterministic; write such references qualified.#[partial]def build_constructor_arity_map (inds : List Inductive) : HashMap String I64 := build_constructor_arity_map_with_structs inds List.empty/// `build_constructor_arity_map` with a program's structs folded in --/// the arity table is the ONE constructor table structs appear in (see/// `collect_struct_ctor_claims`), and it is what makes `is_constructor_var`/// answer true for a value-position `Point.mk` and/// `constructor_arity` answer the struct's field count for it.////// The inductive claims stay FIRST in declaration order, so the bare-name/// tier's "first claim wins" answer (see this function's own doc/// comment) is unchanged for every name an inductive also claims: a/// struct's `mk` can only answer a bare `mk` lookup in a program where/// no inductive claims that name at all.#[partial]pub def build_constructor_arity_map_with_structs (inds : List Inductive) (structs : List Struct) : HashMap String I64 := let claims := List.reverse (List.append (collect_ctor_claims_inds inds List.empty) (collect_struct_ctor_claims structs List.empty)) in let scan := scan_ctor_bare_arities claims { first := str_map_empty, multi := str_map_empty } in add_ctor_arity_keys claims scan str_map_empty#[partial]def add_ctor_arity_keys (claims : List CtorClaim) (scan : BareArityScan) (acc : HashMap String I64) : HashMap String I64 := match claims { List.empty => acc, List.cons cl rest => match cl { CtorClaim.mk bare arity qualified => let bare_entry := match str_map_lookup bare scan.multi { Option.some amb => if amb then match str_map_lookup bare scan.first { Option.some first => first, Option.none => arity, } else arity, Option.none => arity, } in add_ctor_arity_keys rest scan (str_map_insert bare bare_entry (str_map_insert qualified arity acc)), },}