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.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451145214531454145514561457145814591460146114621463146414651466146714681469147014711472147314741475147614771478147914801481148214831484148514861487148814891490149114921493149414951496149714981499150015011502150315041505150615071508150915101511151215131514151515161517151815191520152115221523152415251526152715281529153015311532153315341535153615371538153915401541154215431544154515461547154815491550155115521553155415551556155715581559156015611562156315641565156615671568156915701571157215731574157515761577157815791580158115821583158415851586158715881589159015911592159315941595159615971598159916001601160216031604160516061607160816091610161116121613161416151616161716181619162016211622162316241625162616271628162916301631163216331634163516361637163816391640164116421643164416451646164716481649165016511652165316541655165616571658165916601661166216631664166516661667166816691670167116721673167416751676167716781679168016811682168316841685168616871688168916901691169216931694169516961697169816991700170117021703170417051706170717081709171017111712171317141715171617171718171917201721172217231724172517261727172817291730173117321733173417351736173717381739174017411742174317441745174617471748174917501751175217531754175517561757175817591760176117621763176417651766176717681769177017711772177317741775177617771778177917801781178217831784178517861787178817891790179117921793179417951796179717981799180018011802180318041805180618071808180918101811181218131814181518161817181818191820182118221823182418251826182718281829183018311832183318341835183618371838183918401841184218431844184518461847184818491850185118521853185418551856185718581859186018611862186318641865186618671868186918701871187218731874187518761877187818791880188118821883188418851886188718881889189018911892189318941895189618971898189919001901190219031904190519061907190819091910191119121913191419151916191719181919192019211922192319241925192619271928192919301931193219331934193519361937193819391940194119421943194419451946194719481949195019511952195319541955195619571958195919601961196219631964196519661967196819691970197119721973197419751976197719781979198019811982198319841985198619871988198919901991199219931994199519961997199819992000200120022003200420052006200720082009201020112012201320142015201620172018201920202021202220232024202520262027202820292030203120322033203420352036203720382039204020412042204320442045204620472048204920502051205220532054205520562057205820592060206120622063206420652066206720682069207020712072207320742075207620772078207920802081208220832084208520862087208820892090209120922093209420952096209720982099210021012102210321042105210621072108210921102111211221132114211521162117211821192120212121222123212421252126212721282129213021312132213321342135213621372138213921402141214221432144214521462147214821492150215121522153215421552156215721582159216021612162216321642165216621672168216921702171217221732174217521762177217821792180218121822183218421852186218721882189219021912192219321942195219621972198219922002201220222032204220522062207220822092210221122122213221422152216221722182219222022212222222322242225222622272228222922302231223222332234223522362237223822392240224122422243224422452246224722482249225022512252225322542255225622572258225922602261226222632264226522662267226822692270227122722273227422752276227722782279228022812282228322842285228622872288228922902291229222932294229522962297229822992300230123022303230423052306230723082309231023112312231323142315231623172318231923202321232223232324232523262327232823292330233123322333233423352336233723382339234023412342234323442345234623472348234923502351235223532354235523562357235823592360236123622363236423652366236723682369237023712372237323742375237623772378237923802381238223832384238523862387238823892390239123922393239423952396239723982399240024012402240324042405240624072408240924102411241224132414241524162417241824192420242124222423242424252426242724282429243024312432243324342435243624372438243924402441244224432444244524462447244824492450245124522453245424552456245724582459246024612462246324642465246624672468246924702471247224732474247524762477247824792480248124822483248424852486248724882489249024912492249324942495249624972498249925002501250225032504250525062507250825092510251125122513251425152516251725182519252025212522252325242525252625272528252925302531253225332534253525362537253825392540254125422543254425452546254725482549255025512552255325542555255625572558255925602561256225632564256525662567256825692570257125722573257425752576257725782579258025812582258325842585258625872588258925902591259225932594259525962597259825992600260126022603260426052606260726082609261026112612261326142615261626172618261926202621262226232624262526262627262826292630263126322633263426352636263726382639264026412642264326442645264626472648264926502651265226532654265526562657265826592660266126622663266426652666266726682669267026712672267326742675267626772678267926802681268226832684268526862687268826892690269126922693269426952696269726982699270027012702270327042705270627072708270927102711271227132714271527162717271827192720272127222723272427252726272727282729273027312732273327342735273627372738273927402741274227432744274527462747274827492750275127522753275427552756275727582759276027612762276327642765276627672768276927702771277227732774277527762777277827792780278127822783278427852786278727882789279027912792279327942795279627972798279928002801280228032804280528062807280828092810281128122813281428152816281728182819282028212822282328242825282628272828282928302831283228332834283528362837283828392840284128422843284428452846284728482849285028512852285328542855285628572858285928602861286228632864286528662867286828692870287128722873287428752876287728782879288028812882288328842885288628872888288928902891289228932894289528962897289828992900290129022903290429052906290729082909291029112912291329142915291629172918291929202921292229232924292529262927292829292930293129322933293429352936293729382939294029412942294329442945294629472948294929502951295229532954295529562957295829592960296129622963296429652966296729682969297029712972297329742975297629772978297929802981298229832984298529862987298829892990299129922993299429952996299729982999300030013002300330043005300630073008300930103011301230133014301530163017301830193020302130223023302430253026302730283029303030313032303330343035303630373038303930403041304230433044304530463047304830493050305130523053305430553056305730583059306030613062use std::show {Show}// `ScopeData.def_refs` below is a `std.map` `HashMap ModulePath ScopeDef`.// This import is required here (not just at `scope_data_empty`'s own// call sites in `lang/scope.mo`) — a real, isolated evaluator// limitation: a nullary class method like `Map.empty` (no argument// whose runtime constructor tag the interpreter could otherwise// dispatch on, unlike `Map.insert`/`Map.lookup`) fails at runtime with// `unresolved global: Map.empty` unless `std.map`'s `Map` instances are// also in scope in the module that DECLARES the struct field's type,// even when every call site already imports `std.map` itself. Listing// the names is what puts them in scope here; it used to be left empty// out of caution about naming `std.map`'s exports — see// std/map_tests.mo's note for why that caution is gone.use std::map {HashMap, HashMap.empty_buckets, map}use std::list {List.intercalate, List.length}pub type Identifier { id String}/// Compare two identifiers for equality (by string value).def id_eq (a : Identifier) (b : Identifier) : Bool := match a { Identifier.id as => match b { Identifier.id bs => String.beq as bs, }, }instance BEq Identifier { def beq (a b : Identifier) : Bool := id_eq a b}/// Check if an identifier is in a list of identifiers.def id_member (id : Identifier) (ids : List Identifier) : Bool := match ids { List.cons hd rest => if id_eq id hd then true else id_member id rest, List.empty => false, }/// Union two lists of identifiers (deduplicated, left-biased order).def union_ids (a : List Identifier) (b : List Identifier) : List Identifier := match a { List.cons hd rest => if id_member hd b then union_ids rest b else List.cons hd (union_ids rest b), List.empty => b, }/// An argument to a `#[name arg1 arg2 ...]` attribute. Mirrors the Rust/// reference's `AttrArg` (core/src/term.rs) exactly, including the/// `named`/`group` shapes (`{name := value}` / `[item, ...]`) even/// though no real corpus attribute uses either yet — the combinator/// cost of supporting them now is near-zero and avoids a later/// breaking retype of `Attribute.args` once one does.type AttrArg { ident (id: Identifier), str (value: String), num (value: I64), named (name: Identifier) (value: AttrArg), group (items: List AttrArg),}/// A single `#[name arg1 arg2 ...]` declaration/param annotation, e.g./// `#[derive BEq BOrd Debug Lens]` — one `Attribute` with FOUR bare-/// `ident` args (confirmed against the reference grammar: attribute/// args are whitespace-separated and flattened onto the one attribute,/// not four stacked attributes). Deliberately has no `source_location`/// field (unlike the Rust reference's `Attribute`, whose own/// `PartialEq` ignores that field anyway) — no sibling decl-level type/// here (`Def`, `Inductive`, ...) carries source-location data, and/// nothing downstream would read it.pub struct Attribute { name: Identifier, args: List AttrArg,}/// The empty attribute list, under both names the corpus already uses/// for it. Declared here, beside `Attribute` itself, because each was/// previously declared TWICE -- `empty_attrs` in/// `lang/typecheck/macro_queue.mo` and `lang/codegen/emit.mo`,/// `no_attrs` in `lang/codegen/test_driver.mo` and/// `lang/typecheck/meta_reflect.mo` -- so each was two definitions of/// one LLVM symbol, of which the emitted binary silently kept one./// Both spellings are kept rather than picking a winner: the two names/// read differently at their call sites (`no_attrs` for a synthesized/// decl that HAS no attributes, `empty_attrs` for an accumulator's/// zero) and unifying them is a rename sweep with no correctness value.def empty_attrs : List Attribute := List.emptydef no_attrs : List Attribute := List.empty/// Structural equality by name and args.def attr_eq (a : Attribute) (b : Attribute) : Bool := match a { Attribute.mk an aargs => match b { Attribute.mk bn bargs => id_eq an bn && attr_args_eq aargs bargs, } }def attr_args_eq (a : List AttrArg) (b : List AttrArg) : Bool := match a { List.empty => match b { List.empty => true, List.cons _ _ => false }, List.cons ah arest => match b { List.empty => false, List.cons bh brest => attr_arg_eq ah bh && attr_args_eq arest brest, }, }def attr_arg_eq (a : AttrArg) (b : AttrArg) : Bool := match a { AttrArg.ident ai => match b { AttrArg.ident bi => id_eq ai bi, _ => false }, AttrArg.str av => match b { AttrArg.str bv => String.beq av bv, _ => false }, AttrArg.num av => match b { AttrArg.num bv => I64.beq av bv, _ => false }, AttrArg.named an av => match b { AttrArg.named bn bv => id_eq an bn && attr_arg_eq av bv, _ => false }, AttrArg.group aitems => match b { AttrArg.group bitems => attr_args_eq aitems bitems, _ => false }, }instance BEq Attribute { def beq (a b : Attribute) : Bool := attr_eq a b}/// Whether `attrs` contains an attribute named `name`, e.g./// `has_attr (Identifier.id "derive_cli") ind_attrs`. Mirrors the Rust/// reference's `Inductive::has_attr`/`Def::has_test_attr`/// (core/src/term.rs).def has_attr (name : Identifier) (attrs : List Attribute) : Bool := match attrs { List.cons hd rest => match hd { Attribute.mk n _ => if id_eq n name then true else has_attr name rest }, List.empty => false, }/// The ARGUMENTS of the first attribute named `name` -- `has_attr`'s/// args-reading sibling (`has_attr` matches `Attribute.mk n _` and/// drops them). `Option.none` when no attribute of that name is/// present, which is distinct from `Option.some List.empty` for an/// argument-less attribute like `#[partial]`.////// Exists for `#[decreasing x]` (`lang/termination.mo`), the/// one corpus attribute whose args carry meaning: the parser already/// produces `AttrArg.ident` for it (`attr_arg_parser`,/// lang/parser.mo), so what was missing was only a way to read them/// back out.def attr_args (name : Identifier) (attrs : List Attribute) : Option (List AttrArg) := match attrs { List.cons hd rest => match hd { Attribute.mk n args => if id_eq n name then Option.some args else attr_args name rest, }, List.empty => Option.none, }/// Whether a def opts out of the match-coverage check/// (`validate_match_coverage`, `lang/typecheck/infer.mo`) via/// `#[allow_incomplete_match "<reason>"]`.////// The STRING argument is required: a bare `#[allow_incomplete_match]` is/// deliberately NOT an exemption. Unlike `has_termination_exemption` --/// whose argument-less `#[decreasing]` is accepted, because there the/// argument only records WHICH parameter shrinks -- there is nothing here/// to record but the reason, and an unexplained exemption is exactly the/// blanket this attribute exists not to be.def has_incomplete_match_exemption (attrs : List Attribute) : Bool := match attr_args (Identifier.id "allow_incomplete_match") attrs { Option.some args => match_args_carry_a_string args, Option.none => false, }def match_args_carry_a_string (args : List AttrArg) : Bool := match args { List.cons hd _ => match hd { AttrArg.str _ => true, _ => false }, List.empty => false, }#[test]def test_attr_args_returns_the_named_attributes_args : Bool := let attrs : List Attribute := [ Attribute.mk (Identifier.id "native") [AttrArg.ident (Identifier.id "i64_add")], Attribute.mk (Identifier.id "decreasing") [AttrArg.ident (Identifier.id "n")], ] in match attr_args (Identifier.id "decreasing") attrs { Option.some args => match args { List.cons a more => List.length more == 0 && match a { AttrArg.ident id => id_eq id (Identifier.id "n") }, List.empty => false, }, Option.none => false, }#[test]def test_attr_args_missing_is_none_but_argless_is_some_empty : Bool := // `#[partial]` has no arguments at all, which is a DIFFERENT answer // from `#[absent]` not being there -- that distinction is the whole // reason this exists alongside `has_attr`. let attrs : List Attribute := [Attribute.mk (Identifier.id "partial") List.empty] in match attr_args (Identifier.id "partial") attrs { Option.some args => List.length args == 0, Option.none => false, } && match attr_args (Identifier.id "absent") attrs { Option.some _ => false, Option.none => true, }type Operator { operator String}pub type ModulePath { mp (List Identifier)}/// A term-level dotted name path (`Foo.bar.baz`) — a DECL name or a/// legacy dotted reference. Distinct from `ModulePath` (a FILE path,/// `use`d with `::`) since the qualified-names split; see/// plans/implementations/qualified-names.md. Constructor `npath`/// (`mp` is taken by `ModulePath.mp`).pub type NamePath { npath (List Identifier)}/// A module-qualified term reference (`std::list::List.cons`) — the/// `::`-separated module half names a real loaded module, the/// `.`-separated name half a decl inside it. Rendered with the module/// segments `::`-joined, so the string is disjoint from any `NamePath`/// rendering (`:` can't occur in an identifier).pub struct QualifiedName { qmod : ModulePath, qname : NamePath,}pub def show_identifier (id : Identifier) : String := match id { Identifier.id s => s,}/// A `Char`'s source text -- its UTF-8 bytes back as a `String`./// `Char` is `of_bytes (List U8)` (`init/prelude.mo`) and carries one/// codepoint's worth of them, so this is total and round-trips whatever/// `char_literal` (`lang/parser/string.mo`) sliced out.def char_to_string (c : Char) : String := match c { Char.of_bytes bytes => String.from_list bytes,}def show_operator (op : Operator) : String := match op { Operator.operator s => s,}pub def show_module_path (mp : ModulePath) : String := match mp { ModulePath.mp ids => join_identifiers ids,}/// A `NamePath` rendered `.`-joined (`Foo.bar`). The RENDERING matches/// `show_module_path`'s — the two types differ in role (name vs file/// path), not in this one spelling — while `use` module paths render/// `::`-joined in source (`module_path_to_string`, lang/parser.mo).pub def show_name_path (np : NamePath) : String := match np { NamePath.npath ids => join_identifiers ids,}/// `std::list::List.cons` — module half `::`-joined, then `::`, then/// name half `.`-joined. Matches the Rust host's `Display` for/// `QualifiedName` (core/src/term.rs) so DebugName strings stay/// compiler-consistent.pub def show_qualified_name (qn : QualifiedName) : String := String.concat (module_path_to_string_colon qn.qmod) (String.concat "::" (show_name_path qn.qname))/// A module path spelled the way SOURCE spells it: `::`-joined/// (`std::process`). This is the right rendering for anything a user/// reads -- diagnostics, verbose progress lines, `use` decls -- because/// `::` is what they wrote. `show_module_path`'s dot-joined form is the/// INTERNAL spelling (symbol names, map keys) and should not surface.////// Distinct from the general `module_path_to_string` (lang/parser.mo)/// only to avoid a circular parser->types import; the two agree.pub def module_path_to_string_colon (mp : ModulePath) : String := match mp { ModulePath.mp ids => List.intercalate "::" (List.map show_identifier ids),}/// Join a module path's segments with `.` (`[Foo, bar]` -> `Foo.bar`)./// For the LLVM symbol-name form (`Foo__bar`) see/// `lang/codegen/emit.mo`'s `mangle_identifiers`.def join_identifiers (ids : List Identifier) : String := List.intercalate "." (List.map show_identifier ids)instance Show ModulePath { def show (mp : ModulePath) : String := show_module_path mp}/// The `NamePath` twin of the `ModulePath` instance above -- mirrors the/// Rust host's own `impl Display for NamePath` (core/src/term.rs). The/// two render identically (`.`-joined); the instances exist separately/// because the two types are no longer interchangeable.instance Show NamePath { def show (np : NamePath) : String := show_name_path np}/// Identifiers can't contain ".", so the dotted-string-join used by/// show_identifier/show_module_path is collision-free as an ordering key.instance BOrd Identifier { def lt (a b : Identifier) : Bool := BOrd.lt (show_identifier a) (show_identifier b) def gt (a b : Identifier) : Bool := BOrd.gt (show_identifier a) (show_identifier b)}instance BOrd ModulePath { def lt (a b : ModulePath) : Bool := BOrd.lt (show_module_path a) (show_module_path b) def gt (a b : ModulePath) : Bool := BOrd.gt (show_module_path a) (show_module_path b)}/// Same "collision-free as a string key" property `BOrd`'s own/// delegation above already relies on — hash the dotted-string join/// rather than writing a separate combining hash over the segment list./// Needed for `lang/scope.mo`'s `ScopeData.def_refs` to use/// `std.map`'s `HashMap ModulePath ScopeDef` (see/// `bench/scope_lookup.mo` for why: at realistic sizes, `HashMap`/// clearly outperforms both `List`+linear-scan and `BTreeMap` for/// scope's lookup-heavy access pattern).instance Hashable Identifier { def hash (a : Identifier) : U64 := String.hash (show_identifier a)}instance Hashable ModulePath { def hash (mp : ModulePath) : U64 := String.hash (show_module_path mp)}instance Hashable NamePath { def hash (np : NamePath) : U64 := String.hash (show_name_path np)}pub type NameRef { nid (Identifier), /// A dotted name path (`Foo.bar`) — legacy flat spelling or a /// constructor-owner style name. nnp (NamePath), /// An explicit module-qualified reference (`std::list::List.cons`). nqn (QualifiedName), nop (Operator),}type Multiplicity { zero, many, linear, affine,}pub struct Location { offset : I64, line : I64, column : I64,}pub struct SourceRange { start : Location, end : Location, path : Option String,}pub struct LocatedSpan { fragment : String, location : Location,}// Canonical Param uses de Bruijn Term; `ParseParam` is the parser's.pub type Param { mk (name: Identifier) (type_: Term) (mult: Multiplicity) (default: Option Term) (attrs: List Attribute)}/// Create a canonical Param with multiplicity=Many, no default value, and/// no attributes.def parse_param_many (name: Identifier) (type_: ParseTerm) : ParseParam := let none : Option ParseTerm := Option.none in let no_attrs : List Attribute := List.empty in ParseParam.mk name type_ Multiplicity.many none no_attrs/// Like `parse_param_many` but with an explicit multiplicity — for/// `!`/`?`/`%` prefixes on def/lambda params.def parse_param_with_mult (name: Identifier) (type_: ParseTerm) (mult: Multiplicity) : ParseParam := let none : Option ParseTerm := Option.none in let no_attrs : List Attribute := List.empty in ParseParam.mk name type_ mult none no_attrs/// Canonical sibling of `parse_param_many`, for code that already holds/// a lowered `Term`.#[partial]def param_many (name: Identifier) (type_: Term) : Param := let none : Option Term := Option.none in let no_attrs : List Attribute := List.empty in Param.mk name type_ Multiplicity.many none no_attrs/// Create a canonical Param with explicit multiplicity, no default/// value, and no attributes.pub def mk_param (name: Identifier) (type_: Term) (mult: Multiplicity) : Param := let none : Option Term := Option.none in let no_attrs : List Attribute := List.empty in Param.mk name type_ mult none no_attrs/// Create a canonical Param with multiplicity=Many, no default value,/// and explicit attrs — the one constructor/def-param path that/// actually needs a non-empty `attrs` list (e.g. `#[arg]`).pub def param_with_attrs (name: Identifier) (type_: Term) (attrs: List Attribute) : Param := let none : Option Term := Option.none in Param.mk name type_ Multiplicity.many none attrs// Canonical MatchCase uses de Bruijn Term; `ParseMatchCase` is the parser's.//// `field_pattern` mirrors the Rust reference's `MatchCase.field_pattern`// (core/src/term.rs, `plans/implementations/struct-field-destructuring.md`):// `Option.some` only pre-elaboration, when this case was parsed as a// `{ x, y } => ...`/`ConsName { x, y } => ...` field-pattern rather than// the ordinary positional form (`ConsName x y => ...`). `args`/`body` for// a field-pattern case are indexed in the pattern's WRITTEN field order// at PARSE time (`match_case_arrow`'s own `lambda_extend_ctx` call,// `lang/parser.mo` -- this file's canonical `Term` is de Bruijn from the// parser onward, unlike the Rust reference's separate parse-then-lower// split, so there is no later "lowering" pass to defer this to the way// the reference's own `CoreMatchCase.field_pattern` doc comment// describes). `lang/typecheck/infer.mo`'s `type_check_match_case`// resolves this once the scrutinee's real constructor is known,// retargeting `args`/`body` onto the constructor's true declared order// (`lang/typecheck/subst.mo`'s `term_permute`, mirroring the reference's// own `core_term::permute_binders`) and clearing this back to// `Option.none` -- every OTHER consumer (`lang/lower_core_ir.mo`,// `lang/codegen/emit.mo`, `lang/pretty.mo`'s runtime-facing paths) only// ever sees `Option.none` here.type MatchCase { mc (name: Identifier) (args: List Identifier) (body: Term) (field_pattern: Option FieldPattern)}/// One `{ field, other := binder, .. }` pattern -- mirrors the Rust/// reference's `FieldPattern` (core/src/term.rs). `fields` is/// `(field_name, binder)` in the order written; `binder` equals/// `field_name` when punned (`{ x }`). `rest` is `true` when a trailing/// `..` is present (unlisted fields are discarded, not brought into/// scope).pub type FieldPattern { mk (fields: List FieldPatternEntry) (rest: Bool)}/// One `field` or `field := binder` entry inside a `FieldPattern` --/// a dedicated named-pair type (mirroring `StructLitField`'s own/// `name`/`value` shape) rather than a generic `Pair`, so this file/// doesn't need a cross-module dependency on `init/prelude.mo`'s `Pair`/// for its own canonical AST.pub type FieldPatternEntry { mk (field: Identifier) (binder: Identifier)}/// Nested bare-form field-pattern `Match` chain desugaring a dotted-path/// field access (`p.first`, `vzero.x`) into ordinary struct-field/// destructuring -- mirrors the Rust reference's/// `lower_core.rs::lower_field_access_chain`.////// Lives here, beside the two types it builds, because it has two callers/// that must not drift: the parser's `lower_path_ids` (a subject that IS a/// local binder) and the checker's `try_global_field_access`/// (`lang/src/typecheck/infer.mo`, a subject that is a top-level def, the/// case `lower_path_ids` cannot settle at parse time). `lang::types` is the/// lowest module both already depend on.////// The binder list is `[field]` inline rather than via/// `field_pattern_binder_names`: the pattern built here has exactly one/// entry whose binder IS `field`, so calling that helper would only add a/// dependency back on `lang/parser.mo`, which the parser's copy of this/// module exists without.#[partial]pub def field_access_chain (scrutinee : Term) (fields : List Identifier) : Term := match fields { List.empty => scrutinee, List.cons field rest => let value : Term := field_access_chain (Term.var 0 (DebugName.named field)) rest in let entry : FieldPatternEntry := FieldPatternEntry.mk field field in let fp : FieldPattern := FieldPattern.mk (List.cons entry List.empty) true in let binders : List Identifier := List.cons field List.empty in let case_ : MatchCase := MatchCase.mc (Identifier.id "") binders value (Option.some fp) in Term.lit (Literal.match_ scrutinee (List.cons case_ List.empty)), }/// A single `def` parameter as parsed: either an ordinary explicit param/// (unchanged), or a destructured one (`({ x, y } : T)`,/// `plans/implementations/struct-field-destructuring.md`'s Phase 8) --/// paired with the `FieldPattern` a wrapping `match` needs to actually/// bind `x`/`y` from the fixed-name `Param` this variant also carries./// Mirrors the Rust reference's own `ParsedParam` (`core/src/parser.rs`)/// exactly, adapted to a fixed binder name (`__struct_param`) instead of/// a gensym -- `lang/` has no gensym facility (see `motes/clap/src/args.mo`'s own/// header comment for the established precedent of a fixed, prefixed/// name standing in for one here). Kept as a thin wrapper (rather than/// adding a pattern slot to `Param` itself) so every OTHER `Param`/// consumer needs no changes at all -- a `destructured` entry's own/// `Param` is an ordinary, real binder by the time it reaches any of/// them; only the `def` parameter chain in `lang/parser.mo` ever/// inspects the `FieldPattern` half, to wrap the body in one extra/// `match` per `destructured` param before building the final `Term.lam`/// chain./// A parameter as WRITTEN, before lowering -- parse-stage, so it holds/// `ParseParam`. Used only by `lang/parser.mo`.type ParsedParam { plain (param: ParseParam), destructured (param: ParseParam) (fp: FieldPattern),}type NumSuffix { i8, i16, i32, i64, u8, u16, u32, u64, f32, f64,}// Canonical Literal uses de Bruijn Term; `ParseLiteral` is the parser's.type Literal { str (value: String), /// A `'c'` literal. Carries a real `Char` -- one Unicode codepoint, /// mirroring the Rust reference's `Literal::Char(char)` and feeding /// `IrLit.ir_char` (`lang/core_ir.mo`), which has always wanted a /// `Char`, unchanged. NOT the source text: `Char`'s own declared /// shape (`init/prelude.mo`, `of_bytes (List U8)`) holds the /// codepoint's UTF-8 bytes, and the parser slices exactly one /// codepoint (`utf8_char_width`) before building it. char (value: Char), num (value: I64) (suffix: NumSuffix), /// A literal written with a decimal point (`3.0`, `3.14f32`). Kept as /// the exact source text rather than a numeric value: self-hosted /// Monad code has no native bridge to parse a decimal string into an /// actual float bit pattern (unlike the Rust reference's /// `Literal::Float { value: F64Wrap, .. }`, core/src/term.rs), so /// `text` is the only representation available here — sufficient for /// round-tripping through `show_term`/parsing back, though genuine /// float codegen (`lang/codegen/emit.mo` has no float `LLVMValue` /// variant at all yet) remains a separate, unstarted piece of work. flt (text: String) (suffix: NumSuffix), if_ (one: Term) (two: Term) (three: Term), match_ (value: Term) (cases: List MatchCase), /// DEPRECATED: never constructed on purpose. Both typechecking /// (`type_check_struct_lit`, `lang/typecheck/infer.mo`) and codegen /// (`desugar_struct_lits_decls`, `lang/codegen/emit.mo`) rewrite an /// annotated struct literal to a real `Term.con` before use; this /// variant survives only when best-effort elaboration fails, and /// every survivor is rejected fail-fast by /// `validate_no_undesugared_struct_lits` (compile path) or /// `lower_literal`'s `le_struct_lit_survived` (eval path). New code /// should not add consumers for it. /// A struct-literal expression (`{ field := value, ... }`), /// optionally self-annotated with which struct it builds /// (`{ field := value, ... : StructName }`) — lets the checker /// resolve the struct name directly without needing an ambient /// expected type from context (a struct literal doesn't always have /// one, e.g. passed to a generic function). Mirrors the Rust /// reference's `CoreLit::StructLit` (core/src/core_term.rs). struct_lit (fields: List StructLitField) (type_name: Option Term), /// DEPRECATED: never constructed on purpose. Both typechecking /// (`type_check_struct_update`, `lang/typecheck/infer.mo`) and /// codegen (`desugar_struct_lits_decls`, `lang/codegen/emit.mo`) /// rewrite a struct update away before use; this variant survives /// only when best-effort elaboration fails, and every survivor is /// rejected fail-fast by `validate_no_undesugared_struct_lits` /// (compile path) or `lower_literal`'s `le_struct_lit_survived` /// (eval path). New code should not add consumers for it. /// `{ base with field := value, ... }` — a copy of `base` (an /// existing struct VALUE, not a type name) with the listed fields /// replaced. `base` is a resolved `Term` (typically `Term.var`) here /// rather than a bare `Identifier`, unlike the Rust reference's own /// SOURCE-level `term::Literal::StructUpdate` — this checker has no /// separate parse-then-lower stage the way the reference's /// `Literal` (pre-lowering) vs `CoreLit` (post-lowering, /// `base: Box<CoreTerm>`) split does, so the parser resolves `base` /// directly, matching every other variable reference elsewhere in /// this file (`Term.var`/`variable`). Mirrors the Rust reference's /// `CoreLit::StructUpdate`. struct_update (base: Term) (fields: List StructLitField),}/// A single `name := value` field inside a struct-literal EXPRESSION/// (`{ x := 1, y := 2 }`) — as distinct from `StructField`'s/// DECLARATION shape (`x : T := default`). Mirrors one entry of the/// Rust reference's `CoreLit::StructLit`'s `fields: Map<Identifier,/// CoreTerm>`; order here doesn't matter (fields are matched by name)/// — the struct's own declared field order (from its registered/// `Param` list, see `build_scope_struct`) is what determines the/// final constructor-argument order once `type_check_lit` resolves/// this into a `Term.con`.pub type StructLitField { mk (name: Identifier) (value: Term)}pub type Con { mk (name: Identifier) (typ_name: NamePath) (num_args: I64) (args: List (Option Term))}pub type Native { mk (native_name: Identifier) (num_args: I64) (args: List (Option Term))}// ─── Cubical primitives ────────────────────────────────────────────────//// The cubical fragment (`plans/type-system/univalence.md`) needs a handful// of irreducible primitives -- the interval, its De Morgan operations, and// later `PathP`/`transp`/`hcomp`/`Glue`. They are irreducible in the sense// that no cubical type theory builds them from anything simpler, so unlike// `match`/`if` they cannot be encoded away.//// They live behind ONE `Term` variant carrying ONE struct, which is the// shape `Term.lit (Literal)`, `Term.con (Con)` and `Term.ntv (Native)`// already use. The alternative -- one flat `Term` variant per primitive --// would take `similar_term_go` below from a 10x10 hand-expanded cross// product to 21x21 -- a missed pair is a compile error since Phase 1// (strict-exhaustiveness.md), but 231 lines of it.// With this shape every generic walker grows exactly one arm, over `args`.//// `args` is positional and its length is the primitive's arity;// `cubical_arity` below is the table, and `type_check_cubical`// (`lang/typecheck/cubical.mo`) is what enforces it -- the same division of// labour as `Con`'s `num_args` and `type_check_con`.//// NOTE none of these is a BINDER. A path abstraction is an ordinary// `Term.lam` whose parameter type is `I`, so a dimension variable is an// ordinary de Bruijn term variable and every `args` entry sits at the same// binder depth as the node itself. That is what spares// `term_shift`/`term_subst`/`term_permute` and// `term_map_children_at_depth` from needing a second index space.pub type CubicalPrim { /// The interval type `I`. Not a `Sort`, and deliberately NOT an /// inductive: a two-constructor `I` would make `match` on a dimension /// admissible, which destroys univalence. interval, /// The two endpoints, `i0 : I` and `i1 : I`. i0, i1, /// De Morgan interval operations: `ineg i`, `imeet i j`, `ijoin i j`. /// Spelled as names rather than `~`/`/\`/`\/` because `op_chars` /// (`lang/parser/core.mo`) is maximal-munch, so adding an operator /// character retokenizes the compiler's own source. ineg, imeet, ijoin, /// The heterogeneous path former `PathP A a b`, over a line /// `A : I -> Sort l` (Stage 2, plans/type-system/univalence.md). /// The one primitive whose arguments are NOT dimensions: a line of /// types and the two endpoint values. A path abstraction is an /// ordinary `Term.lam` with an `I`-typed binder, so this primitive is /// never a binder either. pathp, /// Transport along a line of types: `transp A a : A i1` for /// `A : I -> Sort l` and `a : A i0` (Stage 3, /// plans/type-system/univalence.md). `transp` rather than CCHM's /// `comp` so the stage can land before the face lattice exists -- /// it takes no cofibration. Like `pathp`, its arguments are not /// dimensions. transp, /// The two cofibration generators `face_eq0 i` / `face_eq1 i` -- /// the constraints `i = 0` / `i = 1` -- and the truth predicate /// `is_one φ : Sort 1` (Stage 4). Cofibrations are INTERVAL terms: /// `∧`/`∨` are the existing `imeet`/`ijoin` and `0`/`1` the /// endpoints, so these three are the only new formers the face /// lattice needs. A partial element over `φ` is then an ordinary /// function `is_one φ -> A` -- Agda's encoding, no new syntax. Note /// `is_one`'s result is a SORT: it is a former of types, like /// `pathp`, and unlike everything else in this list its arguments /// are still dimensions. face_eq0, face_eq1, is_one, /// Kan composition: `hcomp A φ u u0 : A` for a type `A`, a /// cofibration `φ`, a system `u : I -> is_one φ -> A`, and a base /// `u0 : A` (Stage 5, plans/type-system/univalence.md). The /// arguments are not dimensions (`A` and the two elements) and not /// all of the same shape, which is why this prim gets its own /// typing rule rather than the generic `check_cubical_args_then`. /// /// The BOUNDARY law is CCHM's: on `φ` the composite IS the system's /// top, `hcomp A φ u u0 ≡ u i1`. Note what that does NOT say: `u0` /// is the system's BOTTOM (`u i0 = u0` on `φ`), so `hcomp A i1 u u0` /// is `u i1`, never `u0`. Only one of the two decided cases is /// therefore reducible here. When `face_decide` refutes `φ` the /// system constrains nothing and `whnf_hcomp` answers the base /// (`hcomp A i0 u u0 ≡ u0`, the empty box's composition); when /// `face_decide` satisfies `φ` the right answer is `u i1`, which /// needs a witness of `is_one i1` that this syntax has no canonical /// term for -- so it stays STUCK, deliberately, exactly as Stage 4 /// leaves `ijoin`-of-opposite-faces stuck. `whnf_hcomp` /// (`lang/typecheck/whnf.mo`) is the reducer and states the /// asymmetry at the rule. hcomp,}/// One cubical primitive applied to `args`, whose length is its arity.pub struct Cubical { prim : CubicalPrim, args : List Term,}// Optional debug name carried by de Bruijn variables and binders.// Names are never used for identity or equality — de Bruijn indices// determine identity. DebugName exists solely for error messages// and pretty-printing during debugging.pub type DebugName { named (id: Identifier), unnamed,}/// Free-variable sentinel de Bruijn index: `>= 0` means bound, `-1`/// means free/unresolved. The parser emits it for every not-yet-/// resolved `Term.var`, and `lang.scope`/`lang.typecheck` compare/// against it to decide whether a variable still needs resolving.////// Declared here, in the module that owns `Term`/`DebugName`, because/// it is part of that representation's contract rather than any one/// pass's private constant. It previously existed as five byte-/// identical copies (`lang/parser.mo`, `lang/elaborate.mo`,/// `lang/lower_core_ir.mo`, `lang/typecheck/infer.mo`,/// `lang/typecheck/meta_reflect.mo`); since codegen mangles a top-/// level def to its BARE name, those five were five definitions of/// one LLVM symbol `@sentinel`, of which the emitted binary silently/// kept one -- see `validate_no_colliding_def_symbols`/// (`lang/codegen/emit.mo`), which now rejects that shape outright.def sentinel : I64 := -1/// Visibility of a declaration. Mirrors the Rust reference's/// `core::term::Visibility` exactly: `priv` is enforced immediately/// (module boundaries already exist), `pub` vs. the default/// `package_private` is a no-op until a package system exists. Applies to/// `def`/`type`/`class`/`struct`/`instance`/`infix` — NOT `use` (which/// gets its own separate `public: Bool` field directly on `Decl.use_d`,/// since `priv use` isn't a real form) or `open` (no visibility concept/// at all).type Visibility { pub_, priv_, package_private,}/// Structural equality on `Visibility`. Hand-rolled rather than derived:/// `types.mo` has no `BEq` instances at all (it is below the class/// machinery in the dependency order).def visibility_beq (a : Visibility) (b : Visibility) : Bool := match a { Visibility.pub_ => match b { Visibility.pub_ => true, _ => false }, Visibility.priv_ => match b { Visibility.priv_ => true, _ => false }, Visibility.package_private => match b { Visibility.package_private => true, _ => false } }// --- ParseTerm: the parser's own output, before de Bruijn resolution --//// The stage this compiler did not have. `Literal.struct_update`'s own doc// comment (above) names the gap exactly: "this checker has no separate// parse-then-lower stage the way the reference's `Literal`// (pre-lowering) vs `CoreLit` (post-lowering) split does, so the parser// resolves `base` directly".//// Two things distinguish a `ParseTerm` from the canonical `Term` below://// - **Named, not de Bruijn.** A variable is a `NameRef`, exactly as// written. The parser no longer computes de Bruijn indices inline// (`var_term`/`find_index`, `lang/parser.mo`) and no longer threads a// `ctx : List Identifier` through its grammar; binder structure is// recovered during lowering, where `lam`/`forall`/`pi`/`match_` arms// say what they bind.// - **Located.** Every node carries the source range it was parsed// from, which is the only place that information is cheaply// available.//// The span lives on the wrapper struct rather than being repeated on// each variant, so a walk matches `.kind` once and a constructor sets// `span` once. `Term` itself is deliberately NOT given locations: it is// walked by `elaborate.mo`, `typecheck/subst.mo`, `traverse.mo`'s// `term_map_children`, `infer.mo` and `emit.mo`, and it sits on the// measured hot path (AGENTS.md item 27). Lowering emits positions into a// side table instead.//// Replaces the `TermV0`/`ParamV0`/`MatchCaseV0`/`LiteralV0` family, which// was a vestige: incomplete (no `quote_`, `var_macro`, `struct_lit`,// `struct_update`), carrying a `ctx (loc) (term)` variant that was an// abandoned attempt at exactly this feature, and reached only by// `path_variable` building a `TermV0.var` that `variable_try_path_got`// destructured straight back into a `Term`./// Where a `ParseTerm` came from, recorded as the LENGTH OF THE REMAINING/// INPUT at the start and end of the construct.////// Not an absolute offset, because no parser def sees the whole file --/// each one is handed only the unconsumed remainder, and the whole file/// exists nowhere in the grammar at all -- only `build_loc_table`, which/// runs after the parse, ever holds it. Both/// numbers here are available locally and for free: `String.length input`/// before a parser runs and `String.length rem` after it succeeds, each/// an O(1) read on the `SharedStr` window the remainder actually is./// Recording an absolute offset instead would mean threading the file/// (or its length) through all ~235 grammar defs -- re-adding exactly/// the threading that dropping the de Bruijn `ctx` removes.////// Converted to a real `SourceRange` only at the top level, where the/// file IS known: `offset = total_length - start_rem`, then/// `lang/parser/position.mo`'s divide-and-conquer scan for line/column./// Note the ordering is inverted from an offset -- a LARGER `start_rem`/// means EARLIER in the file.pub struct ParseSpan { start_rem : I64, end_rem : I64,}/// The span of a construct whose position has not been recorded. Distinct/// from a zero-length span at end-of-input (`0`/`0`), which is a real/// position.def parse_span_unknown : ParseSpan := { start_rem := -1, end_rem := -1 }#[partial]def parse_span_is_unknown (sp : ParseSpan) : Bool := I64.beq sp.start_rem -1pub struct ParseTerm { span : ParseSpan, kind : ParseTermKind,}/// Build a `ParseTerm` whose position has not been recorded yet.#[partial]def pt_ (k : ParseTermKind) : ParseTerm := { span := parse_span_unknown, kind := k }/// Build a located `ParseTerm` from the input it started at and the/// remainder it left, which is the shape every parser already has in/// hand at the point it succeeds.#[partial]def pt_at (input : String) (rem : String) (k : ParseTermKind) : ParseTerm := { span := { start_rem := String.length input, end_rem := String.length rem }, kind := k }/// Span a compound term from the start of its LEFTMOST sub-term to/// `rem`. The grammar builds application chains and infix climbs/// bottom-up, so by the time the combined term exists the text where it/// began is long since consumed -- but the left operand still carries/// its own span, and that start IS the compound's start. This is why/// `expr_climb` needs no extra threading to locate a whole expression.////// If the left operand has no recorded span (a synthesized sub-term),/// the compound has none either: a span running from an unknown start/// to a real end is not a position, and half a location is worse than/// none.#[partial]def pt_from (left : ParseTerm) (rem : String) (k : ParseTermKind) : ParseTerm := if parse_span_is_unknown left.span then pt_ k else { span := { start_rem := left.span.start_rem, end_rem := String.length rem }, kind := k }// Same-arity constructors for each kind, so converting a grammar site is// a token rename (`Term.app` -> `pt_app`) rather than a wrap that would// have to re-parenthesise the arguments.//// These leave the span UNRECORDED, and most grammar sites are right to// use them: a construct is located once, at `atom_term`/`decl_parser`// (see their doc comments in `lang/parser.mo`), where the text it starts// at is actually in hand. The sites that keep an unknown span are the// ones with no source extent to record at all -- a `pt_hole` standing in// for an omitted type annotation, the cons cells `build_list_literal`// synthesises from a `[a, b, c]` that has only one position, the// `pt_pi` chain `build_param_pi_chain` folds out of a parameter list.// `parse_span_is_unknown` is how a consumer tells "not written in the// source" from a real position.#[partial]def pt_var (n : NameRef) : ParseTerm := pt_ (ParseTermKind.var n)#[partial]def pt_var_macro (n : NameRef) : ParseTerm := pt_ (ParseTermKind.var_macro n)#[partial]def pt_lam (name : Identifier) (typ : ParseTerm) (body : ParseTerm) : ParseTerm := pt_ (ParseTermKind.lam name typ body)#[partial]def pt_pi (name : Option Identifier) (arg : ParseTerm) (ret : ParseTerm) : ParseTerm := pt_ (ParseTermKind.pi name arg ret)#[partial]def pt_app (f : ParseTerm) (a : ParseTerm) : ParseTerm := pt_ (ParseTermKind.app f a)#[partial]def pt_lit (l : ParseLiteral) : ParseTerm := pt_ (ParseTermKind.lit l)/// Every sort form -- `Prop`, `Type`, `Sort n`, `Sort u` -- arrives here as a/// `SortLevel`. Before W1.4 there was also a `pt_type_ (u : I64)` for the/// concrete levels; it and `ParseTermKind.type_` are gone, so `concrete` is/// just one more level shape rather than a constructor of its own.#[partial]def pt_sort (l : SortLevel) : ParseTerm := pt_ (ParseTermKind.sort l)#[partial]def pt_quote_ (t : ParseTerm) : ParseTerm := pt_ (ParseTermKind.quote_ t)#[partial]def pt_do (stmts : List DoStmt) : ParseTerm := pt_ (ParseTermKind.do_ stmts)def pt_hole : ParseTerm := pt_ ParseTermKind.hole// --- The declaration half of the parse stage -------------------------//// Each mirrors its canonical twin with every `Term` replaced by// `ParseTerm`, and mirrors its SHAPE too (a `type` with `mk` where the// canonical one is a `type`, a `struct` where it is a struct) so that// converting a grammar construction site is a rename rather than a// rewrite.//// These exist because lowering cannot sit at the decl boundary. An// earlier attempt assumed it could -- that `Decl`/`Def` keep holding// `Term` and the change stays inside the expression parsers -- and it// does not: `DoStmt`, `Param`, `StructField`, `InductConstructor`,// `ClassDef`, `Def` and `Inductive` all embed `Term` and sit BETWEEN// expressions and declarations. `DoStmt` is the clearest case: it// holds a term per statement and its binder context accumulates across// statements, so there is no point at which one can be lowered without// already having the `ctx` threading this whole change exists to remove.//// Not mirrored, checked rather than assumed: `TypeConstraint` (only a// `ModulePath` and `Identifier`s), `Attribute`/`AttrArg` (no `Term`// anywhere), `Operator`, `UseFilter`, `OpenFilter`, `Visibility`.pub struct ParseParam { name : Identifier, type_ : ParseTerm, mult : Multiplicity, default : Option ParseTerm, attrs : List Attribute,}pub struct ParseStructField { name : Identifier, typ : ParseTerm, default : Option ParseTerm, mult : Multiplicity,}pub struct ParseInductConstructor { name : NamePath, params : List ParseParam, typ : ParseTerm,}pub struct ParseClassDef { name : Identifier, typ : ParseTerm, default : Option ParseTerm,}pub struct ParseDef { name: NamePath, typ: ParseTerm, term: ParseTerm, constraints: List TypeConstraint, attrs: List Attribute, vis: Visibility, params: List ParseParam}pub struct ParseInductive { name : NamePath, params : List ParseParam, typ : ParseTerm, constructors : List ParseInductConstructor, attrs : List Attribute, vis : Visibility,}pub struct ParseClass { name : Identifier, params : List ParseParam, constraints : List TypeConstraint, methods : List ParseClassDef, vis : Visibility,}pub struct ParseInstance { name : Identifier, cls : NamePath, constraints : List TypeConstraint, args : List ParseTerm, vis : Visibility, implicit_params : List ParseParam, defs : List ParseDef,}pub struct ParseStruct { name : Identifier, fields : List ParseStructField, /// `#[...]` attributes stacked above the `struct` keyword — the same /// slot `ParseInductive` has carried since `#[derive_cli]` had to /// survive `type` (see `lang/parser.mo`'s `type_try_attrs`). Needed /// for `#[derive BEq BOrd Debug Lens] struct Point {...}` /// (`examples/derive.mo`), which the bridge in /// `lang/typecheck/macro_queue.mo` reads back off the lowered /// `Struct`. attrs : List Attribute, vis : Visibility,}/// A declaration plus the span it was parsed from.////// The span is what collapsed the two parallel top-level parsers into/// one. A second parser (`decls_skip_with_locs`) used to re-derive each/// declaration's position by threading the whole file alongside the/// shrinking input; positions became a projection over the span recorded/// here instead -- at the top level the total length IS available, so/// `offset = total_length - span.start_rem`, then/// `lang/parser/position.mo`'s scan for line/column. Same arithmetic,/// one parser instead of two, and no way for the two to disagree about/// where a declaration starts.pub struct ParseDecl { span : ParseSpan, kind : ParseDeclKind,}pub type ParseDeclKind { def_d (ParseDef), inductive_d (ParseInductive), struct_d (ParseStruct), class_d (ParseClass), instance_d (ParseInstance), infix_d (op: Operator) (path: NamePath) (vis: Visibility), use_d (path: ModulePath) (filter: UseFilter) (public: Bool), open_d (path: NamePath) (filter: OpenFilter), scoped_open_d (path: NamePath) (filter: OpenFilter) (decl: ParseDecl), def_macro_d (ParseDef), decl_gen_d (name: NamePath) (params: List ParseParam) (decl_list: List ParseDecl) (attrs: List Attribute), macro_call_d (name: Identifier) (args: List ParseTerm), /// `#![mote { ... }]` — the file-level INNER attribute, carried until /// lowering as `Decl.mote_d`. Appended LAST deliberately: these are /// constructor-named variants, so nothing is positional, but a /// variant's TAG is its declaration order and appending is what /// guarantees no existing tag moves. mote_d (attr: Attribute),}/// Build a `ParseDecl` whose position has not been recorded yet.#[partial]def pd_ (k : ParseDeclKind) : ParseDecl := { span := parse_span_unknown, kind := k }/// Build a located `ParseDecl` from the input it started at and the/// remainder it left.#[partial]def pd_at (input : String) (rem : String) (k : ParseDeclKind) : ParseDecl := { span := { start_rem := String.length input, end_rem := String.length rem }, kind := k }// Same-arity constructors per declaration kind, for the same reason the// `pt_*` family exists: a grammar site converts by renaming// `Decl.def_d` -> `pd_def_d` rather than by a wrap that would have to// re-parenthesise its argument. As with `pt_*`, the span is recorded at// the choke point (`decl_parser`) rather than here -- every one of these// twenty sites sits somewhere in the middle of the declaration it// builds, and none of them can see where it began.#[partial]def pd_def_d (d : ParseDef) : ParseDecl := pd_ (ParseDeclKind.def_d d)#[partial]def pd_inductive_d (i : ParseInductive) : ParseDecl := pd_ (ParseDeclKind.inductive_d i)#[partial]def pd_struct_d (s : ParseStruct) : ParseDecl := pd_ (ParseDeclKind.struct_d s)#[partial]def pd_class_d (c : ParseClass) : ParseDecl := pd_ (ParseDeclKind.class_d c)#[partial]def pd_instance_d (i : ParseInstance) : ParseDecl := pd_ (ParseDeclKind.instance_d i)#[partial]def pd_infix_d (op : Operator) (path : NamePath) (vis : Visibility) : ParseDecl := pd_ (ParseDeclKind.infix_d op path vis)#[partial]def pd_use_d (path : ModulePath) (filter : UseFilter) (public : Bool) : ParseDecl := pd_ (ParseDeclKind.use_d path filter public)#[partial]def pd_open_d (path : NamePath) (filter : OpenFilter) : ParseDecl := pd_ (ParseDeclKind.open_d path filter)#[partial]def pd_scoped_open_d (path : NamePath) (filter : OpenFilter) (inner : ParseDecl) : ParseDecl := pd_ (ParseDeclKind.scoped_open_d path filter inner)#[partial]def pd_def_macro_d (d : ParseDef) : ParseDecl := pd_ (ParseDeclKind.def_macro_d d)#[partial]def pd_decl_gen_d (name : NamePath) (params : List ParseParam) (decl_list : List ParseDecl) (attrs : List Attribute) : ParseDecl := pd_ (ParseDeclKind.decl_gen_d name params decl_list attrs)#[partial]def pd_macro_call_d (name : Identifier) (args : List ParseTerm) : ParseDecl := pd_ (ParseDeclKind.macro_call_d name args)/// `#![mote { ... }]`. Takes the already-parsed `Attribute` (the `#![]`/// spelling is the parser's business, not this constructor's) so it can/// reuse `attribute_open` rather than duplicating the whole/// name/args/close chain for a one-character difference.#[partial]def pd_mote_d (attr : Attribute) : ParseDecl := pd_ (ParseDeclKind.mote_d attr)pub type ParseTermKind { var (name: NameRef), /// Term-position `name!`. Kept a separate variant rather than a /// tagged `var` for the same reason `Term.var_macro` is (see its own /// doc comment): macro names resolve in a separate namespace. var_macro (name: NameRef), lam (name: Identifier) (typ: ParseTerm) (body: ParseTerm), forall (name: Identifier) (typ: ParseTerm) (body: ParseTerm), /// `arg_name` is `some` for a written dependent arrow /// (`(n : T) -> body`, which binds `n` over `body`) AND, since R2a', /// for each parameter `build_param_pi_chain` folds out of a `def`'s /// parameter list — a declared signature is dependent whenever it /// says it is. It is `none` only for the genuinely non-dependent /// chains `build_pi_chain` folds (class-method parameter types, which /// carry no names at all). Mirrors the Rust reference's `Term::Pi { arg_name: /// Option<Name>, .. }` (`core/src/term.rs`), whose `lower_core.rs` /// arm likewise pushes `arg_name` into scope only when it is `Some`. /// /// The distinction is load-bearing, not cosmetic: `Term.pi` has no /// field to carry a binder name, so a name dropped here is gone for /// good and every use of it inside `ret` resolves to `sentinel`. /// This branch shipped exactly that regression once. pi (arg_name: Option Identifier) (arg: ParseTerm) (ret: ParseTerm), app (fun: ParseTerm) (arg: ParseTerm), lit (value: ParseLiteral), // `forall`, `ntv` and `con` were spelled here to mirror the old // `Term`; no syntax produces one: there is no `forall` keyword in the // grammar, // natives arrive through an attribute rather than a term, and the // parser has never built a `Term.con` (constructor applications are // ordinary `app`s of a `var` until the type checker resolves them). // `Term.forall` itself is gone -- R2b folded it into `Term.pi` -- but // this parse-tree variant stays because deleting it would mean // touching the lowering arms for no gain. They carry no `pt_*` smart // constructor for that reason -- only the lowering arms and // exhaustive matches name them. ntv (native: ParseNative), con (c: ParseCon), /// A sort, as a `SortLevel` -- which covers a concrete numeral exactly as /// well as a level VARIABLE or a computed `max`/`succ`. The sole sort /// spelling: a sibling `type_ (universe: I64)` used to carry the concrete /// levels, which meant every level could be written two ways and every /// match site had to absorb both shapes. sort (level: SortLevel), quote_ (term: ParseTerm), /// A `do { }` block, kept as STATEMENTS rather than desugared during /// parsing. Do-notation is syntax, so it belongs in the parse AST; /// Preserved as syntax and desugared by `lower_parse_do` once the /// binder context is known. The grammar used to desugar inline, /// which is only possible while it also threads `ctx`. do_ (stmts: List DoStmt), hole,}pub struct ParseMatchCase { name : Identifier, args : List Identifier, body : ParseTerm, field_pattern : Option FieldPattern,}type ParseLiteral { str (value: String), /// Parse-level sibling of `Literal.char` -- same `Char` payload, see /// its doc comment there. char (value: Char), num (value: I64) (suffix: NumSuffix), flt (text: String) (suffix: NumSuffix), if_ (one: ParseTerm) (two: ParseTerm) (three: ParseTerm), match_ (value: ParseTerm) (cases: List ParseMatchCase), struct_lit (fields: List ParseStructLitField) (type_name: Option ParseTerm), /// `base` is a `ParseTerm` here for the same reason it is a `Term` /// in `Literal` -- it is an expression, not a name -- but at THIS /// stage it is still the unresolved one the source wrote. struct_update (base: ParseTerm) (fields: List ParseStructLitField),}pub struct ParseStructLitField { name : Identifier, value : ParseTerm,}pub type ParseCon { mk (name: Identifier) (typ_name: NamePath) (num_args: I64) (args: List (Option ParseTerm))}pub type ParseNative { mk (native_name: Identifier) (num_args: I64) (args: List (Option ParseTerm))}// The universe level of a sort. `Prop`/`Type`/`Sort n` are `concrete n`; a// level variable is `var name`; `max`/`succ` are the structure that makes a// Pi's universe and cumulativity computable without solving anything.//// NAME-KEYED, not de Bruijn. A level variable can only be introduced at a// def boundary, so it is free by construction -- the same discipline// `solve_typevars`/`subst_typevars_term` (`lang/typecheck/infer.mo`) already// use for type variables. Keeping it free is what spares// `term_shift`/`term_subst`/`term_permute`/`term_map_children_at_depth` any// change at all: there is no second index space to carry, and no second// depth counter to keep in step (the trap `lang/typecheck/whnf.mo` records// for its many-at-once binder shift).pub type SortLevel { concrete (level: I64), var (name: Identifier), max (left: SortLevel) (right: SortLevel), succ (inner: SortLevel),}/// How a binder BEHAVES — everything about a binder that is not its name.////// This type exists so that a binder's name and its behaviour travel as one/// unit rather than as two parameters. They always co-occur (`pi` and `lam`/// are the only binders, and every binder has both), so carrying them/// separately would mean two fields that are only ever written together.pub type BinderInfo { /// `(x : T) -> U` — an ordinary explicit parameter. Every `lam`'s /// binder, and the only kind `pi` had before R2. explicit, /// A quantified type variable, whose domain is a real type — /// `{A : Type} -> …`. This is what a `Term.forall` became when R2b folded /// it into `pi`; `binder_binder` above is its sole constructor. binder, /// A universe-LEVEL binder, whose domain is a level rather than a type. /// This was `forall`'s marker, recognised before R2b by /// `is_level_binder_kind` testing whether the binder's `kind` term was a /// sort at level 0 — a shape test on a term standing in for a property of /// the binder. That test is now the tag it was always describing (see /// `binder_is_level` below), which is what removes the hazard the old /// comment recorded: the marker was only collision-free because the /// grammar has no `forall` keyword. level,}/// A binder: what it is called, and how it behaves.////// `name` is a `DebugName`, which is error-message metadata and NEVER/// identity — de Bruijn indices determine identity, and this field changes/// no index. `BinderInfo` is what the checker actually discriminates on.pub struct Binder { name : DebugName, info : BinderInfo,}/// A binder from a `DebugName` the caller already holds, under the/// behaviour `lam` always wants. `binder_anon` and `binder_named` below/// are its two shorthand spellings -- they cover the construction site/// that has no name to give and the one that has an `Identifier` -- and/// this is the one for a `DebugName` in hand, which is what a `Term.lam`/// carries and why R2c needed it.pub def binder_explicit (d : DebugName) : Binder := { name := d, info := BinderInfo.explicit,}/// The binder an anonymous construction site wants: nothing for the error/// message, an ordinary explicit parameter. A named def rather than an/// inline literal because a bare struct literal in argument position is a/// known miscompile, and because one spelling makes the hundred-odd call/// sites that have no name to give read identically.////// `pub`, with `Binder`/`BinderInfo` above it, because `proofs/` is a/// separate mote and builds anonymous `Term.pi`s in/// `proofs/src/checker/sort_props.mo`. That mote's `harness.mo` records/// keeping `lang`'s export surface at zero as a deliberate constraint;/// this is the third deliberate widening (after `DebugName` for W1.2 and/// `level_const` for W1.4), and the alternative -- spelling the struct/// literal at each site -- is the miscompile trap the line above names.pub def binder_anon : Binder := { name := DebugName.unnamed, info := BinderInfo.explicit,}/// The binder a NAMED arrow carries — `(n : T) -> body` puts `n` in scope/// over `body`. Same construction discipline as `binder_anon` above, and/// for the same reason.////// This is the half of R2 that makes a declared dependent signature mean/// something. `build_param_pi_chain` folds a `def`'s parameter list into a/// pi chain, and before R2a' it had no name to pass, so every parameter/// type and the return type were lowered at the SAME depth while/// `type_check_pi` checked the codomain under `List.cons arg local_types`/// and `term_map_children_at_depth` walked `ret` at depth 1. Threading the/// name moves the producer onto the consumers' side: a mention of an/// earlier parameter now binds instead of resolving to `sentinel`.pub def binder_named (n : Identifier) : Binder := { name := DebugName.named n, info := BinderInfo.explicit,}/// The binder `wrap_forall` (`lang/elaborate.mo`) puts on a quantified type/// variable — `forall`'s term-level flavour, `{A : Type} -> …`. Built here/// rather than at the wrap site for the same reason as the two above, and/// because R2b's fold needs exactly one place that says what a former/// `forall` lowers to.////// The `Term` side of that fold is the `dom`: `wrap_forall` writes/// `Term.sort (SortLevel.concrete 1)`, which is `Type`, and that is right —/// the binder's domain really is the type its variable ranges over. Only the/// *discriminator* moved, from "is the kind a sort at level 0?" to this tag.pub def binder_binder (n : Identifier) : Binder := { name := DebugName.named n, info := BinderInfo.binder,}/// The binder `wrap_level_forall` puts on a universe level — `Sort u` in a/// signature, bound by the enclosing def. Same discipline as `binder_binder`/// above; `wrap_level_forall` writes `Term.sort (SortLevel.concrete 0)` as the/// domain, which is the marker the old `is_level_binder_kind` read.pub def binder_level (n : Identifier) : Binder := { name := DebugName.named n, info := BinderInfo.level,}/// Every `BinderInfo`, as a number. Same purpose as `cubical_prim_tag`: the/// type is payload-free, so equality IS tag equality, and a spelled-out 3×3/// cross product is nine places to get the answer wrong for the same result./// Read by `binder_info_eq` and by the `Similar` instance below it.pub def binder_info_tag (i : BinderInfo) : I64 := match i { BinderInfo.explicit => 0, BinderInfo.binder => 1, BinderInfo.level => 2,}pub def binder_info_eq (a : BinderInfo) (b : BinderInfo) : Bool := I64.beq (binder_info_tag a) (binder_info_tag b)/// What a binder's behaviour is, for a caller holding a whole `Binder`./// A named def rather than a field read because reading a struct field/// inside a recursive walk defeats the termination checker where a/// pattern binder does not (AGENTS.md).pub def binder_info_of (b : Binder) : BinderInfo := match b { { name := _n, info := i } => i }/// Is this an ordinary arrow's binder -- `(x : T) -> U`?////// The question a walker asks when it has to decide whether a `pi` is a/// REAL function type or one of the two former `forall` flavours. It was/// never asked before R2b: `forall` and `pi` were different constructors,/// so a walker that cared told them apart by shape. Now they share an arm/// and `info` is the only thing that separates them, which is why this/// exists as a named predicate rather than a field read at each site.pub def binder_is_explicit (b : Binder) : Bool := binder_info_eq (binder_info_of b) BinderInfo.explicit/// Is this a LEVEL binder rather than a type-variable binder?////// This was a SHAPE test on the binder's `kind` term until R2b: a/// `Term.forall` carried `wrap_level_forall`'s marker/// (`Term.sort (SortLevel.concrete 0)`) as its kind, where `wrap_forall`/// used level 1, so "is a sort at level 0" was the whole discriminator --/// a property of the binder read off a term standing in for it. The fold/// deleted the kind term and made the property the tag it always was./// That is also why this lives here now: the old test walked a `Term` and/// so had to sit beside `term_map_children` in `lang/typecheck/levels.mo`;/// a tag comparison has no such dependency.////// The collision the old test reasoned about is gone rather than/// mitigated: no term is a binder's `info`, so nothing a program writes/// can be mistaken for a level marker.pub def binder_is_level (b : Binder) : Bool := binder_info_eq (binder_info_of b) BinderInfo.level/// What a binder is called, for a caller holding a whole `Binder`./// Companion to `binder_info_of` and a named def for the same reason:/// `b.name` by field access inside a recursive walk loses the/// termination proof.pub def binder_name (b : Binder) : DebugName := match b { { name := n, info := _i } => n }// The canonical de Bruijn term IR — what everything after the parser// works on. `ParseTerm` above is lowered into this.//// De Bruijn convention: index 0 = most recently bound variable.// Free variables use sentinel index (I64.max) and are resolved// by the type checker or module resolver.pub type Term { var (idx: I64) (dbg: DebugName), /// The lambda, and the ONLY binder over a term. Its binder is an /// ANNOTATION, exactly as `pi`'s below is, and its `info` is ALWAYS /// `explicit` -- a lambda's argument is written, never implicit -- so /// nothing discriminates on it. R2c gave it the `Binder` `pi` already /// had, for uniformity; `binder_is_explicit` answering `true` for a /// lambda is the contract that buys. lam (b: Binder) (typ: Term) (body: Term), /// A function type, and the ONLY binder over a type. `forall` used to sit /// beside it as a second spelling; R2b folded it in, so `b`'s `info` is /// now what tells a quantified type variable (`binder`), a universe level /// (`level`) and an ordinary arrow (`explicit`) apart, and `arg` carries a /// former `forall`'s `kind` unchanged (a `Term.sort`, which is exactly the /// domain its variable ranges over). /// /// The binder is an ANNOTATION, exactly as `lam`'s `dbg` is: the name never /// affects an index, because the parser already binds it before `Term` /// exists (`lower_parse.mo`'s `pi_ret_ctx` extends the lowering context by /// the arrow's own binder when the source named one), and /// `term_map_children_at_depth` already walks `ret` at depth 1. R2a stopped /// `pi` from DROPPING the name it was given; R2a' made the grammar actually /// give it one for a `def`'s parameter list (`binder_named` above). pi (b : Binder) (arg : Term) (ret: Term), app (fun: Term) (arg: Term), lit (value: Literal), ntv (native: Native), con (c: Con), hole, /// `quote { <term> }` -- syntax as data. Mirrors the Rust reference's /// `Term::Quote { term: Box<Term> }` (core/src/term.rs). Named /// `quote_`, not `quote` -- `quote` is a reserved keyword in the /// self-hosted grammar's own identifier parser too (same reason /// `type_`/`if_`/`match_` above are suffixed, not bare). Parsing/ /// representation only in this codebase so far -- no expansion pass /// exists yet to resolve `unquote`/`,(expr)` inside the quoted body /// (see plans/bootstrapping/self-hosted-compiler.md); `unquote` /// itself needs no special grammar at all, since it's just an /// ordinary identifier at parse time (recognized as magic only at /// expansion time, mirroring the reference exactly). quote_ (term: Term), /// Term-position `name!` (`foo!`, `foo! 1 2`). Structurally /// identical to `Term.var` (`idx`/`dbg`) -- `idx` is always /// `sentinel` in practice, since macro names are resolved in a /// separate namespace at expansion time, never via de Bruijn lookup /// against a local `ctx` the way an ordinary bound variable is. /// A separate sibling variant, not a tagged `Term.var`, because /// self-hosted has no `NameRef` at the canonical term level to add /// a `Macro` case to the way the Rust reference's /// `Term::Var{name: NameRef::Macro(_)}` does (a qualified/dotted /// name here is just one joined `Identifier` string, not a /// structured `NameRef`) -- see /// plans/bootstrapping/self-hosted-compiler.md for the alternatives /// considered and rejected (baking `!` into the identifier string; /// a 3rd `DebugName` variant, ruled out as live-regression-risky /// since `DebugName` is matched exhaustively in several real /// hot-path files). var_macro (idx: I64) (dbg: DebugName), /// A source position attached to the term it wraps. Mirrors the Rust /// reference's `Term::Ctx { loc, module, term }` (`core/src/term.rs`), /// minus the module -- DWARF needs a point, and the file is known at /// emission. /// /// A WRAPPER rather than a field on each variant: a field changes all /// twelve constructor arities, and every positional match on them /// breaks at RUNTIME with `expected N constructor fields, got N+1`, /// no location, across ~2262 occurrence sites. A wrapper leaves every /// existing pattern working. /// /// It is also NOT a side table, which would be the cheaper-looking /// option: `Term` has no node identity to key one by. `var.idx` is /// positional and rewritten by `term_shift`/`term_permute`, and /// `DebugName` is documented as explicitly not identity and is /// rewritten by `resolve_infix_term`, `qualify_modules` and /// `infer.mo`'s mangling. Nothing stable exists to point at. /// /// **Semantically transparent.** A wrapper may change what the /// compiler ANNOTATES and must never change what it DECIDES, so every /// site that inspects a term's SHAPE peels first (`term_peel`), and /// every site that rebuilds preserves (`Term.ctx loc (f inner)`). /// `tools/debug_transparency_oracle.sh` is what enforces this: strip /// `!dbg` from a `--debug` build and it must be byte-identical to the /// non-debug build. /// /// Constructed on EVERY path, not only under `compile --debug`. The /// located entry point is the one production parse site: /// `parse_all_decls` (`lang/src/module.mo`) is written against /// `decls_parser_located`, so `check`, `test`, `compile` and `pretty` /// all see wrappers, and the corpus exercises transparency /// continuously rather than only in a debug build. (Corrected /// 2026-09-29: this said the opposite -- "constructed ONLY by the /// located parser entry point, so `check`, `test` and a non-debug /// `compile` never see one" -- and believing it is exactly what makes /// a reader conclude a new tool must switch the check path to the /// located parser. It must not; it is already there.) Not every node /// carries one: `kind_wants_loc` (`lang/src/parser/lower_parse.mo`) /// excludes the kinds whose position is not worth recording, and a /// located def's BODY carries one by construction /// (`lang/src/codegen/ctx.mo`). ctx (loc: Location) (term: Term), /// A sort, at a level that may be a plain numeral or a level expression /// (`var`/`max`/`succ`). The ONLY sort spelling at the canonical term /// level: `Term.type_ n` was deleted in favour of it, so there is no /// longer anything to reconcile. `sort_level_of` below is how a /// shape-inspecting site asks "is this a sort, and at what level". /// /// Declared last, which no longer means anything. It was put here because /// "adding a variant leaves every existing constructor tag where it is" -- /// an argument that was already wrong (a tag is assigned per compile from /// declaration order, `build_constructor_tag_map` in `codegen/ctors.mo`, /// and every consumer looks one up by NAME), and that this deletion /// disproves: no numeric tag is read, assigned, compared or serialized /// anywhere. A FIELD would still be wrong -- see `ctx` above for the /// arity breakage that causes. sort (level: SortLevel), /// A cubical primitive application -- see `CubicalPrim`/`Cubical` above. /// One variant rather than one per primitive, for the reason recorded /// there: `similar_term_go` is a hand-expanded cross product over this /// type's variants and nothing checks it for exhaustiveness. cubical (c: Cubical),}/// Strip location wrappers, exposing the term a shape test wants.////// Call this at the ENTRY of anything that matches on a term's shape --/// `flatten_call_spine`, `class_method_ref`, `collect_db_params`,/// `term_has_struct_lit` -- rather than adding a `ctx` arm to each. A/// shape probe that forgets does not fail loudly; it silently stops/// matching, and the call it was meant to resolve quietly does not.#[partial]pub def term_peel (t : Term) : Term := match t { Term.ctx _loc inner => term_peel inner, _ => t,}/// The OUTERMOST recorded position of a term, if it carries one: the/// wrapper chain is only ever entered from outside, so the first `ctx`/// met is returned and any inner one is dropped. (This said "innermost"/// until 2026-09-29, which was simply wrong.)#[partial]pub def term_loc (t : Term) : Option Location := match t { Term.ctx loc _inner => Option.some loc, _ => Option.none,}/// Canonical TypeError uses de Bruijn Term. TypeErrorV0 is the legacy V0 variant.pub type TypeError { mismatch (expected: Term) (actual: Term), unknown_var (name: NameRef), unknown_type (name: NameRef), unknown_constructor (name: NameRef), not_a_function (term: Term), not_a_type (term: Term), infinite_type (term: Term), custom (msg: String),}/// Canonical EvalError uses de Bruijn Term. EvalErrorV0 is the legacy V0 variant.type EvalError { undefined_var (name: NameRef), not_a_function (term: Term), match_failure (term: Term), custom (msg: String),}pub type TypeConstraint { mk (cls: NamePath) (vars: List Identifier)}/// Canonical Def uses de Bruijn Term. DefV0 is the legacy V0 variant.pub struct Def { name: NamePath, typ: Term, term: Term, constraints: List TypeConstraint, attrs: List Attribute, vis: Visibility, params: List Param}pub def Def.name (d : Def) : NamePath := d.name// Canonical InductConstructor uses de Bruijn Term. InductConstructorV0 is the legacy V0 variant.pub type InductConstructor { mk (name: NamePath) (params: List Param) (typ: Term)}// Canonical Inductive uses de Bruijn Term. InductiveV0 is the legacy V0 variant.pub type Inductive { mk (name: NamePath) (params: List Param) (typ: Term) (constructors: List InductConstructor) (attrs: List Attribute) (vis: Visibility)}// Canonical ClassDef uses de Bruijn Term. ClassDefV0 is the legacy V0 variant.pub type ClassDef { mk (name: Identifier) (typ: Term) (default: Option Term)}// Canonical Class uses de Bruijn Term. ClassV0 is the legacy V0 variant.pub type Class { mk (name: Identifier) (params: List Param) (constraints: List TypeConstraint) (methods: List ClassDef) (vis: Visibility)}// Canonical StructField uses de Bruijn Term. StructFieldV0 is the legacy V0 variant.pub type StructField { /// `mult` mirrors the Rust reference's `StructField.mult` /// (core/src/term.rs): `!name : T` (Linear, must be consumed exactly /// once), `?name : T` (Affine, at most once), `%name : T` (Zero / /// Erased), or no prefix at all (Many, the default — the common /// case). See examples/structs.mo's `Buffer.data` for a live `!` use. mk (name: Identifier) (typ: Term) (default: Option Term) (mult: Multiplicity)}// Canonical Struct uses de Bruijn Term. StructV0 is the legacy V0 variant.pub type Struct { /// `attrs` mirrors `Inductive`'s own slot: the `#[...]` attributes /// written above the declaration, preserved through lowering so the /// macro-expansion pass can still see a `#[derive ...]`/ /// `#[derive_cli]` request at the point where decl-gen macros are /// resolved (`lang/typecheck/macro_queue.mo`) — the attribute itself /// is not a term or a type, so nothing else could carry it. mk (name: Identifier) (fields: List StructField) (attrs: List Attribute) (vis: Visibility)}/// A single item inside a `use Module { ... }` brace filter. Mirrors the/// Rust host's `UseItem` (core/src/term.rs).type UseItem { use_name (name: Identifier), use_rename (name: Identifier) (alias: Identifier), use_glob, use_sub (name: Identifier) (items: List UseItem), use_sub_rename (name: Identifier) (alias: Identifier) (items: List UseItem),}/// What names a `use` declaration imports. Bare `use Module` (no braces)/// is deprecated but still parses. Mirrors Rust's `UseFilter`.type UseFilter { use_bare, use_items (items: List UseItem),}/// What names an `open` declaration makes unqualified. Mirrors Rust's/// `OpenFilter`.type OpenFilter { open_all, open_only (names: List Identifier),}// Canonical Decl uses de Bruijn Term. DeclV0 is the legacy variant.pub type Decl { def_d (Def), inductive_d (Inductive), struct_d (Struct), class_d (Class), instance_d (Instance), infix_d (op: Operator) (path: NamePath) (vis: Visibility), use_d (path: ModulePath) (filter: UseFilter) (public: Bool), open_d (path: NamePath) (filter: OpenFilter), /// `open ModulePath [{filter}] in <decl>` — the module is opened only /// for the scope of the wrapped declaration (def/type/struct/class/ /// instance). Mirrors Rust's `Decl::ScopedOpen`. scoped_open_d (path: NamePath) (filter: OpenFilter) (decl: Decl), /// `defmacro name params := <term>` — mirrors the Rust reference's /// `Decl::DefMacro(Def)` (core/src/term.rs): literally reuses `Def` /// (`typ` forced to `Term.hole`, `term` wrapped in one lambda per /// param when `params` is non-empty via the existing `lam_params` /// helper, lang/parser.mo — no new lambda-building logic needed). /// Parsing/representation only — nothing expands or invokes this /// yet (see plans/bootstrapping/self-hosted-compiler.md). def_macro_d (Def), /// `defmacro name params := decls { ... }` — the sibling /// declaration-generating form. Mirrors the Rust reference's /// `Decl::DeclGen(DeclGenDef)`, but with `DeclGenDef`'s fields /// inlined directly here (matching this type's own `infix_d`/ /// `scoped_open_d` convention of inline fields over a separate /// wrapper struct) rather than introduced as its own named type. /// `decl_list` is the literal, unexpanded list of declarations parsed /// out of the `decls { ... }` body. decl_gen_d (name: NamePath) (params: List Param) (decl_list: List Decl) (attrs: List Attribute), /// Declaration-position `name! arg1 arg2 ...` (e.g. `derive_beq! /// Point`, `reflect_type_info! T some_meta`). `name` is a bare /// `Identifier`, NOT a `ModulePath` — differs from `defmacro`'s own /// name shape, mirroring the Rust reference's `Decl::MacroCall` /// exactly (core/src/term.rs). `args` are whitespace-separated /// terms, not a comma/paren-delimited call. macro_call_d (name: Identifier) (args: List Term), /// `#![mote { name := "x", deps := [init, std] }]` — a file-level /// INNER attribute declaring this file's mote inline, so a module /// with no `mote.toml` above it is a mote rather than "script mode" /// (`Mote.discover`'s own `Option.none`). This is what takes /// `examples/` out of the untracked state the plan's item G records, /// and what makes `validate_module_deps` apply to it. /// /// Valid ONLY as the first declaration of a file, and the diagnostic /// for a misplaced one comes from `validate_mote_attr_position` /// (lang/module.mo) rather than from the parser — see that def's /// comment for why the parser is the wrong place to reject it. /// /// Appended LAST for the same reason as `ParseDeclKind.mote_d`. mote_d (attr: Attribute),}def Decl.to_name (d : Decl) : NamePath := match d { def_d def_ => Def.name def_, _ => NamePath.npath [] }// Canonical Instance uses de Bruijn Term. InstanceV0 is the legacy V0 variant.pub type Instance { /// `implicit_params` holds any `{Name : Type}` binders written right /// after `instance` (before the optional `[constraints]` and the class /// name), e.g. `instance {A : Type} Show A { ... }`. Mirrors the Rust /// reference's `Instance.params` (core/src/term.rs) — load-bearing for /// instance resolution there (substitution-based matching against a /// lookup key's args), not just documentation. Empty for the common /// case of a fully-concrete instance like `instance Show Bool { ... }`. /// /// `defs` holds the instance's own concrete method `Def`s (`def m := /// ...` entries inside the `instance ... { }` body) — mirrors the /// Rust reference's `Instance.impls_map: Map<Identifier, Def>` /// (core/src/term.rs), and mirrors this very module's own `Class` /// type, which already retains its method defs the same way /// (`Class.mk`'s `methods` field). Until this field existed, /// `instance_parser`/`instance_close` (lang/parser.mo) fully parsed /// an instance's own methods and then discarded them outright — /// `resolve_class_method`/`derive_instance_key` /// (lang/typecheck/infer.mo) could find a matching `Instance` but /// never its concrete implementation, always falling back to the /// class method's own abstract signature. See /// plans/bootstrapping/self-hosted-compiler.md's dictionary-passing /// plan (Phase 1) for the full context. mk (name: Identifier) (cls: NamePath) (constraints: List TypeConstraint) (args: List Term) (vis: Visibility) (implicit_params: List Param) (defs: List Def)}// --- Do-notation ---//// `do { ... }` is SYNTAX, not a term: nothing survives lowering, which// desugars it into `Monad.bind`/`Monad.pure` applications. So `DoStmt`// holds `ParseTerm` and belongs to the parse stage -- there is no// canonical `Term`-carrying twin, and the desugaring itself lives in// `lang/parser/lower_parse.mo` (`lower_parse_do`) rather than here,// because it has to interleave with de Bruijn resolution: each binder a// statement introduces is in scope for the statements that FOLLOW it, so// desugaring and context accumulation are one traversal, not two.//// `bind_s`/`let_s` carry the statement's own declared type (`hole` when// unannotated, e.g. `let x <- expr;`/`let x := expr;`) -- without it the// desugaring had no way to give the bound variable a real type even when// the source explicitly wrote one (`let x : T <- expr;`), which broke// downstream typecheck precision for that binding (e.g. match-case// validation on a do-block-bound value whose real type WAS written down,// just never threaded through -- see plans/bootstrapping/// self-hosted-compiler.md's changelog for the cli/src/main.mo `main` repro// this was found from).type DoStmt { bind_s (name: Identifier) (typ: ParseTerm) (expr: ParseTerm), let_s (name: Identifier) (typ: ParseTerm) (expr: ParseTerm), ret_s (expr: ParseTerm), expr_s (expr: ParseTerm),}def list_rev_loop {A : Type} (xs : List A) (acc : List A) : List A := match xs { List.cons x rest => list_rev_loop rest (List.cons x acc), List.empty => acc }def list_reverse {A : Type} (xs : List A) : List A := list_rev_loop xs List.empty// --- Similar class for structural comparison ---class Similar A { def similar (a : A) (b : A) : Bool}instance Similar Identifier { def similar (a : Identifier) (b : Identifier) : Bool := match a { id s1 => match b { id s2 => String.beq s1 s2 } }}instance Similar Operator { def similar (a : Operator) (b : Operator) : Bool := match a { operator s1 => match b { operator s2 => String.beq s1 s2 } }}// List helpers (avoid generic constrained instance due to solver limitation)def id_list_similar (a : List Identifier) (b : List Identifier) : Bool := match a { List.cons x xs => match b { List.cons y ys => Similar.similar x y && id_list_similar xs ys, List.empty => false, _ => false }, List.empty => match b { List.empty => true, List.cons _ _ => false, _ => false }, _ => false }def mc_list_similar (a : List MatchCase) (b : List MatchCase) : Bool := match a { List.cons x xs => match b { List.cons y ys => Similar.similar x y && mc_list_similar xs ys, List.empty => false }, List.empty => match b { List.empty => true, List.cons _ _ => false } }def param_list_similar (a : List Param) (b : List Param) : Bool := match a { List.cons x xs => match b { List.cons y ys => Similar.similar x y && param_list_similar xs ys, List.empty => false }, List.empty => match b { List.cons y ys => false, List.empty => true } }def opt_db_term_similar (a : Option Term) (b : Option Term) : Bool := match a { Option.some x => match b { Option.some y => Similar.similar x y, Option.none => false }, Option.none => match b { Option.none => true, Option.some _ => false } }def opt_db_term_list_similar (a : List (Option Term)) (b : List (Option Term)) : Bool := match a { List.cons x xs => match b { List.cons y ys => opt_db_term_similar x y && opt_db_term_list_similar xs ys, List.empty => false }, List.empty => match b { List.empty => true, List.cons _ _ => false } }instance Similar ModulePath { def similar (a : ModulePath) (b : ModulePath) : Bool := match a { ModulePath.mp ids1 => match b { ModulePath.mp ids2 => id_list_similar ids1 ids2, _ => false }, _ => false }}/// `Similar ModulePath`'s twin, for the positions the qualified-names/// split moved to the def-name role (`Infix.name`, `ScopeDef.name`,/// `Inductive.name` ...). Delegates to `name_path_similar` below so the/// segment-wise rule has one home.instance Similar NamePath { def similar (a : NamePath) (b : NamePath) : Bool := name_path_similar a b}instance Similar NameRef { def similar (a : NameRef) (b : NameRef) : Bool := match a { NameRef.nid id1 => match b { NameRef.nid id2 => Similar.similar id1 id2, NameRef.nnp _ => false, NameRef.nqn _ => false, NameRef.nop _ => false }, NameRef.nnp np1 => match b { NameRef.nnp np2 => name_path_similar np1 np2, NameRef.nid _ => false, NameRef.nqn _ => false, NameRef.nop _ => false }, NameRef.nqn qn1 => match b { NameRef.nqn qn2 => Similar.similar qn1.qmod qn2.qmod && name_path_similar qn1.qname qn2.qname, NameRef.nid _ => false, NameRef.nnp _ => false, NameRef.nop _ => false }, NameRef.nop op1 => match b { NameRef.nop op2 => Similar.similar op1 op2, NameRef.nid _ => false, NameRef.nnp _ => false, NameRef.nqn _ => false } }}/// Segment-wise `Similar` over a `NamePath` — the `NameRef.nnp`/`nqn`/// arms above delegate here rather than keying `ScopeData`'s maps on the/// rendered string (the string comparison `BOrd ModulePath` relies on/// would conflate nothing here, but segment-wise keeps `Similar`/// structural like `id_list_similar`).pub def name_path_similar (a : NamePath) (b : NamePath) : Bool := match a { NamePath.npath ids1 => match b { NamePath.npath ids2 => id_list_similar ids1 ids2 } }instance Similar NumSuffix { def similar (a : NumSuffix) (b : NumSuffix) : Bool := match a { i8 => match b { i8 => true, i16 => false, i32 => false, i64 => false, u8 => false, u16 => false, u32 => false, u64 => false, f32 => false, f64 => false }, i16 => match b { i8 => false, i16 => true, i32 => false, i64 => false, u8 => false, u16 => false, u32 => false, u64 => false, f32 => false, f64 => false }, i32 => match b { i8 => false, i16 => false, i32 => true, i64 => false, u8 => false, u16 => false, u32 => false, u64 => false, f32 => false, f64 => false }, i64 => match b { i8 => false, i16 => false, i32 => false, i64 => true, u8 => false, u16 => false, u32 => false, u64 => false, f32 => false, f64 => false }, u8 => match b { i8 => false, i16 => false, i32 => false, i64 => false, u8 => true, u16 => false, u32 => false, u64 => false, f32 => false, f64 => false }, u16 => match b { i8 => false, i16 => false, i32 => false, i64 => false, u8 => false, u16 => true, u32 => false, u64 => false, f32 => false, f64 => false }, u32 => match b { i8 => false, i16 => false, i32 => false, i64 => false, u8 => false, u16 => false, u32 => true, u64 => false, f32 => false, f64 => false }, u64 => match b { i8 => false, i16 => false, i32 => false, i64 => false, u8 => false, u16 => false, u32 => false, u64 => true, f32 => false, f64 => false }, f32 => match b { i8 => false, i16 => false, i32 => false, i64 => false, u8 => false, u16 => false, u32 => false, u64 => false, f32 => true, f64 => false }, f64 => match b { i8 => false, i16 => false, i32 => false, i64 => false, u8 => false, u16 => false, u32 => false, u64 => false, f32 => false, f64 => true } }}instance Similar Con { def similar (a : Con) (b : Con) : Bool := match a { mk name1 typ1 nargs1 args1 => match b { mk name2 typ2 nargs2 args2 => Similar.similar name1 name2 && Similar.similar typ1 typ2 && I64.beq nargs1 nargs2 && opt_db_term_list_similar args1 args2 } }}instance Similar Native { def similar (a : Native) (b : Native) : Bool := match a { mk name1 nargs1 args1 => match b { mk name2 nargs2 args2 => Similar.similar name1 name2 && I64.beq nargs1 nargs2 && opt_db_term_list_similar args1 args2 } }}instance Similar MatchCase { def similar (a : MatchCase) (b : MatchCase) : Bool := match a { mc name1 args1 body1 => match b { mc name2 args2 body2 => Similar.similar name1 name2 && id_list_similar args1 args2 && Similar.similar body1 body2 } }}instance Similar Multiplicity { def similar (a : Multiplicity) (b : Multiplicity) : Bool := match a { zero => match b { zero => true, many => false, linear => false, affine => false }, many => match b { zero => false, many => true, linear => false, affine => false }, linear => match b { zero => false, many => false, linear => true, affine => false }, affine => match b { zero => false, many => false, linear => false, affine => true } }}instance Similar Param { def similar (a : Param) (b : Param) : Bool := match a { mk name1 typ1 mult1 def1 _attrs1 => match b { mk name2 typ2 mult2 def2 _attrs2 => Similar.similar name1 name2 && Similar.similar typ1 typ2 && Similar.similar mult1 mult2 && opt_db_term_similar def1 def2 } }}instance Similar Location { def similar (a : Location) (b : Location) : Bool := match a { mk off1 line1 col1 => match b { mk off2 line2 col2 => I64.beq off1 off2 && I64.beq line1 line2 && I64.beq col1 col2 } }}def opt_str_similar (a : Option String) (b : Option String) : Bool := match a { Option.some x => match b { Option.some y => String.beq x y, Option.none => false }, Option.none => match b { Option.none => true, Option.some _ => false } }instance Similar SourceRange { def similar (a : SourceRange) (b : SourceRange) : Bool := match a { mk start1 end1 path1 => match b { mk start2 end2 path2 => Similar.similar start1 start2 && Similar.similar end1 end2 && opt_str_similar path1 path2 } }}instance Similar Literal { def similar (a : Literal) (b : Literal) : Bool := match a { str s1 => match b { str s2 => String.beq s1 s2, num _ _ => false, if_ _ _ _ => false, match_ _ _ => false }, num v1 s1 => match b { num v2 s2 => I64.beq v1 v2 && Similar.similar s1 s2, str _ => false, if_ _ _ _ => false, match_ _ _ => false }, if_ o1 t1 th1 => match b { if_ o2 t2 th2 => Similar.similar o1 o2 && Similar.similar t1 t2 && Similar.similar th1 th2, str _ => false, num _ _ => false, match_ _ _ => false }, match_ v1 cs1 => match b { match_ v2 cs2 => Similar.similar v1 v2 && mc_list_similar cs1 cs2, str _ => false, num _ _ => false, if_ _ _ _ => false } }}// --- Similar instances for de Bruijn types (Phase 0) ---instance Similar BinderInfo { /// Dense tag comparison, not a cross product -- the `cubical_prim_eq` /// pattern, and for the same reason. def similar (a : BinderInfo) (b : BinderInfo) : Bool := binder_info_eq a b}/// The NAME is deliberately not compared. `Binder`'s own doc comment says the/// name is error-message metadata and NEVER identity; two binders differing/// only in what an error message would call them are the same binder. `info`/// is the half the checker discriminates on, so it is the half this compares.////// That distinction became load-bearing with R2b. Before the fold every/// `pi`'s binder was `binder_anon`, so ignoring it was free. After, a level/// binder at level 0 and an explicit `(x : Prop)` binder have the SAME domain/// (`Term.sort (SortLevel.concrete 0)`) and can have the same codomain — so a/// `similar_term_go` that ignored `info` would call `forall u. C` and/// `(x : Prop) -> C` convertible, and `pi_arity` counts one of those as a value/// parameter and not the other.instance Similar Binder { def similar (a : Binder) (b : Binder) : Bool := binder_info_eq (binder_info_of a) (binder_info_of b)}instance Similar DebugName { def similar (a : DebugName) (b : DebugName) : Bool := match a { named id1 => match b { named id2 => Similar.similar id1 id2, unnamed => false }, unnamed => match b { unnamed => true, named _ => false } }}// ─── Sort levels ────────────────────────────────────────────────────//// Elementary operations only. The normalizing comparison and the// substitution machinery land with `lang/typecheck/levels.mo` (W1.5); these// live here rather than there because `Similar Term` below needs level// equality, and a `levels` module would have to import this one -- a cycle./// The larger of two `I64`s. `I64.max` is not a function in this tree (the/// sentinel comment that mentions it means `I64`'s maximum value), so the/// two-line version is spelled out.def level_i64_max (a: I64) (b: I64) : I64 := if I64.gt a b then a else b/// The concrete value of a level, when it has one.////// `succ`/`max` of concrete levels ARE evaluated -- `succ (concrete 1)` is/// `2`. That is load-bearing rather than tidy: `type_check_sort_full` infers/// the type of a sort at level `l` as the sort at `succ l`, so a Pi's/// universe or a cumulativity check routinely meets a `succ` that has to/// count as a number.////// A level variable answers `Option.none`, and so does any `succ`/`max`/// containing one. An unresolved level is deliberately NOT given a number --/// the comparisons below all refuse it, which is the sound direction (an/// unresolved level costs completeness, never soundness), and W1.5's/// normalizing comparison is what resolves these structurally.pub def level_const (l: SortLevel) : Option I64 := match l { SortLevel.concrete n => Option.some n, SortLevel.var _ => Option.none, SortLevel.succ inner => match level_const inner { Option.some n => Option.some (n + 1), Option.none => Option.none, }, SortLevel.max left right => match level_const left { Option.some a => match level_const right { Option.some b => Option.some (level_i64_max a b), Option.none => Option.none, }, Option.none => Option.none, },}/// Level equality, for `Similar`. Concrete-valued levels compare by value, so/// a `succ`/`max` that happens to be concrete still matches a literal. A/// variable equals only the same name; anything partially unresolved is NOT/// equal, again refusing rather than guessing.def level_eq (l: SortLevel) (r: SortLevel) : Bool := match level_const l { Option.some a => match level_const r { Option.some b => I64.beq a b, Option.none => false, }, Option.none => match l { SortLevel.var n1 => match r { SortLevel.var n2 => Similar.similar n1 n2, _ => false, }, _ => false, },}/// `l <= r` -- cumulativity.////// Two ways to hold. A level is `<=` ITSELF whatever it evaluates to, so/// `level_eq` settles the reflexive case first: `u <= u` is true under every/// valuation of `u`, and it is not a guess. Without it `unify` was not/// reflexive on sorts -- `unify_sort` (`lang/typecheck/unify.mo`) routes both/// spellings here before the structural `Similar.similar` fallback ever runs,/// so `Sort u` failed to unify with `Sort u` and a universe-polymorphic/// signature could not be compared against itself.////// Otherwise both sides must be concrete, and an unresolved level answers/// FALSE (see `level_const`) -- the sound direction, which costs/// completeness and never soundness. Two DIFFERENT variables still do not/// unify; W1.5's normalizing comparison is what resolves those structurally.////// `level_lt` is unaffected by the reflexive arm, which is the point of/// spelling it `level_le (succ l) r`: `level_eq (succ u) u` is false (they/// are not the same level), so `Sort u : Sort u` stays rejected.def level_le (l: SortLevel) (r: SortLevel) : Bool := if level_eq l r then true else match level_const l { Option.some a => match level_const r { Option.some b => not (I64.gt a b), Option.none => false, }, Option.none => false, }/// `l < r` -- the sort rule, and exactly `succ l <= r`. Spelling it this way/// is not a shortcut: it is what makes `Sort n : Sort n` false by the same/// relation that makes `Sort n : Sort (n+1)` true, which is the shape the/// check had before W1.0's fix and the reason that fix was a one-line/// deletion rather than a special case.def level_lt (l: SortLevel) (r: SortLevel) : Bool := level_le (SortLevel.succ l) r/// `Sort n : Sort n` is Type-in-Type and must stay rejected -- the one/// thing `level_le`'s reflexive arm must NOT have loosened. `level_lt`/// is `level_le (succ l) r`, and `succ u` is not the same level as `u`,/// so the arm does not fire here.#[test]def test_level_lt_is_not_reflexive_on_a_level_var : Bool := let u : SortLevel := SortLevel.var (Identifier.id "u") in Bool.not (level_lt u u)/// ...while `level_le` IS reflexive on the same variable. Asserted/// beside the test above because the two are one relation: a fix that/// made `level_le` reflexive by making `level_const` invent a number for/// a variable would pass this and fail that one.#[test]def test_level_le_is_reflexive_on_a_level_var : Bool := let u : SortLevel := SortLevel.var (Identifier.id "u") in level_le u u/// And a variable is still not `<=` a DIFFERENT variable: nothing has/// determined the ordering, so refusing is the sound answer.#[test]def test_level_le_refuses_two_distinct_level_vars : Bool := Bool.not (level_le (SortLevel.var (Identifier.id "u")) (SortLevel.var (Identifier.id "v")))/// The sort level of a term, if that term is a sort.#[partial]def sort_level_of (t: Term) : Option SortLevel := match term_peel t { Term.sort level => Option.some level, _ => Option.none,}/// A sort reads back its own level. The old spelling this used to be/// compared against is gone, so what is left to pin is that the sole/// constructor is reachable at all -- a `sort_level_of` that stopped/// matching `Term.sort` would answer `none` for every sort in the compiler/// and collapse `level_of_type`, `binder_is_level` and `unify_sort` with it.#[test]def test_sort_level_of_reads_the_only_spelling : Bool := match sort_level_of (sort_n 3) { Option.some l => level_eq l (SortLevel.concrete 3), Option.none => false, }/// A sort at a concrete level, in the one remaining spelling.////// A FIXTURE SHORTHAND, not a layer. Every hand-written sort in the test/// suite used to say `Term.type_ n`; this is what that becomes, so ~640 sites/// do not each spell out `Term.sort (SortLevel.concrete n)`. Production code/// writes the constructor directly.////// It is also what keeps `SortLevel` out of sixteen test files: a call site/// writes `sort_n 3` and never names the level type at all. Nothing about the/// level rules depends on the difference -- `level_const`/`sort_level_of` fold/// a `concrete` built either way to the same answer.////// Deliberately NOT `pub`: `proofs/` writes the explicit constructor instead,/// so a test convenience never becomes part of `lang`'s public surface.def sort_n (n : I64) : Term := Term.sort (SortLevel.concrete n)/// The sort level of a term known to be a TYPE, for a caller that must answer/// with a level rather than an `Option`.////// The default is `concrete 1` -- exactly what the callers answered/// unconditionally before, so any component that is not a known sort keeps/// its old contribution. A component whose type IS a sort/// contributes that sort's level, which is the standard rule: the sort of/// `Pi A B` is the max of the sorts of `A` and `B`.def level_of_type (t: Term) : SortLevel := match sort_level_of t { Option.some l => l, Option.none => SortLevel.concrete 1,}// ─── Level variables: the substitution half (W1.3) ────────────────────//// The comparison helpers above all REFUSE an unresolved level. These// three are what resolve one, and they are the whole reason levels are// name-keyed rather than de Bruijn: a level variable can only be bound// at a def boundary, so it is free by construction, and there is no// second index space for `term_shift`/`term_subst`/`term_permute` to// maintain./// Every free level variable in a level, in first-seen order.def free_level_vars_of (l: SortLevel) : List Identifier := match l { SortLevel.concrete _ => List.empty, SortLevel.var name => List.cons name List.empty, SortLevel.succ inner => free_level_vars_of inner, SortLevel.max left right => union_ids (free_level_vars_of left) (free_level_vars_of right),}/// Substitute level variables inside a LEVEL. Unmentioned variables are/// left alone rather than defaulted, so a partial solution stays partial/// -- the same non-committal discipline `solve_typevars` follows.def level_subst (l: SortLevel) (binds: List (Pair Identifier SortLevel)) : SortLevel := match l { SortLevel.concrete n => SortLevel.concrete n, SortLevel.var name => match level_lookup name binds { Option.some replacement => replacement, Option.none => SortLevel.var name, }, SortLevel.succ inner => SortLevel.succ (level_subst inner binds), SortLevel.max left right => SortLevel.max (level_subst left binds) (level_subst right binds),}/// First binding for `name`, or none. A plain assoc walk: a level/// substitution holds one entry per generalized binder, so this is/// never long enough to want a map.def level_lookup (name: Identifier) (binds: List (Pair Identifier SortLevel)) : Option SortLevel := match binds { List.cons entry rest => match entry { Pair.pair key val => if Similar.similar key name then Option.some val else level_lookup name rest, }, List.empty => Option.none, }// ─── Cubical constructors and arity ────────────────────────────────────/// Build a cubical term. Binds an annotated local before wrapping because a/// BARE struct literal in argument position miscompiles through the/// self-hosted backend (AGENTS.md); this is the established shape for it.pub def cub (prim : CubicalPrim) (args : List Term) : Term := let c : Cubical := { prim := prim, args := args } in Term.cubical c/// The interval type `I`.pub def cub_interval : Term := cub CubicalPrim.interval List.empty/// `i0 : I`.pub def cub_i0 : Term := cub CubicalPrim.i0 List.empty/// `i1 : I`.pub def cub_i1 : Term := cub CubicalPrim.i1 List.empty/// `ineg i` -- interval negation.pub def cub_ineg (i : Term) : Term := cub CubicalPrim.ineg [i]/// `imeet i j` -- the De Morgan meet.pub def cub_imeet (i : Term) (j : Term) : Term := cub CubicalPrim.imeet [i, j]/// `ijoin i j` -- the De Morgan join.pub def cub_ijoin (i : Term) (j : Term) : Term := cub CubicalPrim.ijoin [i, j]/// `PathP A a b` -- a path over the line `A` from `a` to `b`. The line is/// checked to be `I -> Sort l` and the endpoints to live at `A i0`/`A i1`/// by `type_check_pathp` (`lang/src/typecheck/infer.mo`).pub def cub_pathp (a_line : Term) (a_left : Term) (a_right : Term) : Term := cub CubicalPrim.pathp [a_line, a_left, a_right]/// `transp A a` -- the element `a : A i0` transported to `A i1`. The/// line is checked to be `I -> Sort l` and the element to live at/// `A i0` by `type_check_transp` (`lang/src/typecheck/infer.mo`); the/// constant-family reduction to the element itself lives in/// `whnf_transp` (`lang/src/typecheck/whnf.mo`).pub def cub_transp (a_line : Term) (a_elem : Term) : Term := cub CubicalPrim.transp [a_line, a_elem]/// `face_eq0 i` -- the cofibration `i = 0`. Reduces to `i1` exactly at/// `i0` and to `i0` at `i1` (`whnf_face`,/// `lang/src/typecheck/whnf.mo`); `face_eq0 (ineg i)` is `face_eq1 i`.pub def cub_face_eq0 (i : Term) : Term := cub CubicalPrim.face_eq0 [i]/// `face_eq1 i` -- the cofibration `i = 1`. Reduces to `i1` exactly at/// `i1` and to `i0` at `i0`; `face_eq1 (ineg i)` is `face_eq0 i`.pub def cub_face_eq1 (i : Term) : Term := cub CubicalPrim.face_eq1 [i]/// `is_one φ` -- the proposition that the cofibration `φ` is `i1`. A/// former of types (result `Sort 1`); its proofs are what a partial/// element (`is_one φ -> A`) consumes, and `hcomp` below is the one/// consumer of a whole system. Both `is_one` and the `hcomp` it feeds/// stay rigid -- nothing in the checker fabricates a proof of/// `is_one φ`, which is exactly why `hcomp`'s satisfied-face case has no/// reduction (see `CubicalPrim.hcomp`).pub def cub_is_one (i : Term) : Term := cub CubicalPrim.is_one [i]/// `hcomp A φ u u0` -- Kan composition. `whnf_hcomp`/// (`lang/src/typecheck/whnf.mo`) answers `u0` when the cofibration is/// REFUTED and stays stuck when it is satisfied; see `CubicalPrim.hcomp`/// for why the satisfied case has no rule here.pub def cub_hcomp (a_typ : Term) (a_face : Term) (a_sys : Term) (a_base : Term) : Term := cub CubicalPrim.hcomp [a_typ, a_face, a_sys, a_base]/// How many arguments a primitive takes. `args` is positional and this is/// the only statement of its expected length; `type_check_cubical` is what/// rejects a mismatch, exactly as `type_check_con` does for `Con.num_args`./// Keeping it as a total function over `CubicalPrim` rather than a field on/// `Cubical` means a new primitive cannot be added without answering it.pub def cubical_arity (prim : CubicalPrim) : I64 := match prim { CubicalPrim.interval => 0, CubicalPrim.i0 => 0, CubicalPrim.i1 => 0, CubicalPrim.ineg => 1, CubicalPrim.imeet => 2, CubicalPrim.ijoin => 2, CubicalPrim.pathp => 3, CubicalPrim.transp => 2, CubicalPrim.face_eq0 => 1, CubicalPrim.face_eq1 => 1, CubicalPrim.is_one => 1, CubicalPrim.hcomp => 4,}/// Is this primitive one of the two interval ENDPOINTS? The reducer and the/// path-application rule both ask, and asking through one predicate keeps/// the two from drifting.pub def cubical_is_endpoint (prim : CubicalPrim) : Bool := match prim { CubicalPrim.i0 => true, CubicalPrim.i1 => true, CubicalPrim.interval => false, CubicalPrim.ineg => false, CubicalPrim.imeet => false, CubicalPrim.ijoin => false, CubicalPrim.pathp => false, CubicalPrim.transp => false, CubicalPrim.face_eq0 => false, CubicalPrim.face_eq1 => false, CubicalPrim.is_one => false, CubicalPrim.hcomp => false,}/// A dense tag per primitive. Total over `CubicalPrim`, so a primitive added/// later cannot be left without one.////// Equality goes through this rather than through a hand-expanded 6x6 cross/// product of constructor pairs. The cross product is what `similar_term_go`/// below does for `Term`, where it is forced -- those variants carry payloads/// that have to be compared arm by arm. `CubicalPrim` carries none, so the/// only thing a cross product would add here is 36 places to omit a pair,/// and an omitted pair answers "different" for two equal primitives. One/// comparison over six literals is checkable by reading it.pub def cubical_prim_tag (prim : CubicalPrim) : I64 := match prim { CubicalPrim.interval => 0, CubicalPrim.i0 => 1, CubicalPrim.i1 => 2, CubicalPrim.ineg => 3, CubicalPrim.imeet => 4, CubicalPrim.ijoin => 5, CubicalPrim.pathp => 6, CubicalPrim.transp => 7, CubicalPrim.face_eq0 => 8, CubicalPrim.face_eq1 => 9, CubicalPrim.is_one => 10, CubicalPrim.hcomp => 11,}pub def cubical_prim_eq (a : CubicalPrim) (b : CubicalPrim) : Bool := I64.beq (cubical_prim_tag a) (cubical_prim_tag b)/// The primitive's surface name. One table, shared by the printer/// (`lang/pretty.mo`) and the checker's diagnostics, so the two cannot drift.pub def cubical_prim_name (prim : CubicalPrim) : String := match prim { CubicalPrim.interval => "I", CubicalPrim.i0 => "i0", CubicalPrim.i1 => "i1", CubicalPrim.ineg => "ineg", CubicalPrim.imeet => "imeet", CubicalPrim.ijoin => "ijoin", CubicalPrim.pathp => "PathP", CubicalPrim.transp => "transp", CubicalPrim.face_eq0 => "face_eq0", CubicalPrim.face_eq1 => "face_eq1", CubicalPrim.is_one => "is_one", CubicalPrim.hcomp => "hcomp",}/// Every primitive, in `cubical_prim_tag` order. Exists as one list so the/// decoder below can be derived from `cubical_marker_key` by scanning,/// not keyed by a second copy of the same strings.pub def cubical_prims_all : List CubicalPrim := List.cons CubicalPrim.interval (List.cons CubicalPrim.i0 (List.cons CubicalPrim.i1 (List.cons CubicalPrim.ineg (List.cons CubicalPrim.imeet (List.cons CubicalPrim.ijoin (List.cons CubicalPrim.pathp (List.cons CubicalPrim.transp (List.cons CubicalPrim.face_eq0 (List.cons CubicalPrim.face_eq1 (List.cons CubicalPrim.is_one (List.cons CubicalPrim.hcomp List.empty)))))))))))/// The string a `#[cubical "..."]` MARKER names a primitive by -- the/// marker key, which is NOT the surface name `cubical_prim_name` returns:/// the interval's surface name is `I` (what a user writes, what the/// printer shows) but its marker is `interval`, because the marker names/// the PRIMITIVE, and the def the marker sits on already carries its own/// name on the same line. Distinct tables by exactly that one entry;/// total over `CubicalPrim` so a primitive added later cannot be left/// without a marker key silently.pub def cubical_marker_key (prim : CubicalPrim) : String := match prim { CubicalPrim.interval => "interval", CubicalPrim.i0 => "i0", CubicalPrim.i1 => "i1", CubicalPrim.ineg => "ineg", CubicalPrim.imeet => "imeet", CubicalPrim.ijoin => "ijoin", CubicalPrim.pathp => "pathp", CubicalPrim.transp => "transp", CubicalPrim.face_eq0 => "face_eq0", CubicalPrim.face_eq1 => "face_eq1", CubicalPrim.is_one => "is_one", CubicalPrim.hcomp => "hcomp",}/// Decode a `#[cubical "..."]` marker's string back to the primitive it/// names -- the inverse of `cubical_marker_key`, derived from that same/// table by scanning `cubical_prims_all`, so a primitive added with a/// marker key cannot leave the decoder behind (an if-chain keyed by its/// own copy of the strings could). `Option`, not a panic: the marker is/// authored in user source, so an unknown string must answer "binds/// nothing" and the def then stays an ordinary def -- the same answer as/// no marker at all.pub def cubical_prim_of_name (s : String) : Option CubicalPrim := cubical_prim_of_name_scan cubical_prims_all s#[partial]def cubical_prim_of_name_scan (ps : List CubicalPrim) (s : String) : Option CubicalPrim := match ps { List.empty => Option.none, List.cons p rest => if String.beq (cubical_marker_key p) s then Option.some p else cubical_prim_of_name_scan rest s, }/// Read a cubical term's primitive, past any location wrapper.pub def cubical_prim_of (t : Term) : Option CubicalPrim := match term_peel t { Term.cubical c => Option.some c.prim, _ => Option.none,}instance Similar Term { /// Peels BOTH sides before comparing, so a location wrapper never /// makes two otherwise-identical terms compare unequal. Without this, /// `--debug` would change what the type checker decides, not just what /// it annotates -- and `term_matches_carrier` (`lang/scope.mo`) reaches /// here on instance-carrier matching, so the effect would be a /// silently unresolved instance. /// /// A pre-existing gap it does NOT fix: the inner matches below omit /// `quote_` and `var_macro`, so comparing either is a /// non-exhaustive-match crash waiting on a caller that constructs one. /// `term_peel` does not strip those two, so routing through one entry /// point that peels only keeps that gap at one place instead of eleven. /// /// `Term.sort` had to be added to EVERY inner match below, not just to a /// new outer arm: a sort compared against a non-sort lands in the other /// arm's inner match, and an unlisted variant there is a runtime /// non-exhaustive-match crash, not a type error. Two sorts are similar /// when their levels are -- `level_eq`, which folds a concrete level back /// to the `I64.beq` this comparison always was. def similar (a : Term) (b : Term) : Bool := similar_term_go (term_peel a) (term_peel b)}#[partial]def similar_term_go (a : Term) (b : Term) : Bool := match a { var i1 d1 => match b { var i2 d2 => I64.beq i1 i2 && Similar.similar d1 d2, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, con _ => false, hole => false, sort _ => false, cubical _ => false }, // R2c: `d1`/`d2` are `Binder`s now, so this compares `info` and // NOT the name, where it compared names before -- the arm's text // never changed, the type under it did. The one widening R2c // makes; `test_lam_similarity_ignores_the_name` pins it. lam d1 t1 bd1 => match b { lam d2 t2 bd2 => Similar.similar d1 d2 && Similar.similar t1 t2 && Similar.similar bd1 bd2, var _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, con _ => false, hole => false, sort _ => false, cubical _ => false }, // The two binders are compared, and the domain and codomain with // them. Comparing `b1`/`b2` is not decoration: it is what keeps a // level binder at level 0 -- whose domain is `Term.sort (concrete // 0)`, i.e. `Prop` -- from being similar to an explicit // `(x : Prop) -> …`. See `Similar Binder` for the full reason. pi b1 a1 r1 => match b { pi b2 a2 r2 => Similar.similar b1 b2 && Similar.similar a1 a2 && Similar.similar r1 r2, var _ _ => false, lam _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, con _ => false, hole => false, sort _ => false, cubical _ => false }, app f1 a1 => match b { app f2 a2 => Similar.similar f1 f2 && Similar.similar a1 a2, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, lit _ => false, ntv _ => false, con _ => false, hole => false, sort _ => false, cubical _ => false }, lit v1 => match b { lit v2 => Similar.similar v1 v2, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, ntv _ => false, con _ => false, hole => false, sort _ => false, cubical _ => false }, ntv n1 => match b { ntv n2 => Similar.similar n1 n2, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, con _ => false, hole => false, sort _ => false, cubical _ => false }, con c1 => match b { con c2 => Similar.similar c1 c2, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, hole => false, sort _ => false, cubical _ => false }, sort l1 => match b { sort l2 => level_eq l1 l2, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, con _ => false, hole => false, cubical _ => false }, hole => match b { hole => true, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, con _ => false, sort _ => false, cubical _ => false }, cubical c1 => match b { cubical c2 => similar_cubical c1 c2, var _ _ => false, lam _ _ _ => false, pi _ _ _ => false, app _ _ => false, lit _ => false, ntv _ => false, con _ => false, hole => false, sort _ => false } }/// Two cubical terms are similar when they name the same primitive and/// their argument lists are pointwise similar. `args` carries the arity, so/// a length mismatch is a difference rather than a crash.def similar_cubical (a : Cubical) (b : Cubical) : Bool := if cubical_prim_eq a.prim b.prim then similar_terms_pointwise a.args b.args else false#[partial]def similar_terms_pointwise (xs : List Term) (ys : List Term) : Bool := match xs { List.empty => List.is_empty ys, List.cons x xrest => match ys { List.empty => false, List.cons y yrest => if Similar.similar x y then similar_terms_pointwise xrest yrest else false, },}/// Two sorts are similar exactly when their levels are -- the property that/// replaced "similar across the two spellings". A `similar` answering `false`/// for two equal sorts would make `term_matches_carrier` (`lang/scope.mo`)/// reject a matching instance carrier: the silently-unresolved-instance/// failure the `Similar Term` instance's own doc warns about.#[test]def test_similar_matches_sorts_by_level : Bool := Similar.similar (sort_n 2) (sort_n 2) && Bool.not (Similar.similar (sort_n 2) (sort_n 3))// ─── Term construction tests (Phase 0) ─────────────────────────────#[test]def test_term_var : Bool := let v : Term := Term.var 0 (DebugName.named (Identifier.id "x")) in true#[test]def test_term_lam : Bool := let body : Term := Term.var 0 (DebugName.unnamed) in let l : Term := Term.lam binder_anon body body in true/// R2c's contract, and the whole of what a walker merging `lam` and `pi`/// arms is allowed to assume: a lambda's binder is ALWAYS `explicit`,/// whether it was given a name or not. Mutating `binder_explicit` to any/// other `BinderInfo` -- or `binder_anon`/`binder_named` off it -- fails/// this and nothing else, because nothing else in the corpus reads a/// lambda's `info`.#[test]def test_lam_binder_is_always_explicit : Bool := let n : Binder := binder_named (Identifier.id "x") in let named_lam : Term := Term.lam n Term.hole Term.hole in let anon_lam : Term := Term.lam binder_anon Term.hole Term.hole in let d_lam : Term := Term.lam (binder_explicit DebugName.unnamed) Term.hole Term.hole in let named_ok : Bool := match named_lam { Term.lam b _ _ => binder_is_explicit b, _ => false, } in let anon_ok : Bool := match anon_lam { Term.lam b _ _ => binder_is_explicit b, _ => false, } in let d_ok : Bool := match d_lam { Term.lam b _ _ => binder_is_explicit b, _ => false, } in named_ok && anon_ok && d_ok/// The other half of R2c: the name a lambda is built with survives as/// `name`, which is what the printer reads (`test_show_lam_named` in/// `pretty_tests.mo` pins the printed consequence). `binder_explicit` is/// the lift every `DebugName`-carrying call site goes through, so a/// mutation that drops `d` on the floor fails here first.#[test]def test_lam_binder_keeps_its_name : Bool := let d : DebugName := DebugName.named (Identifier.id "x") in let l : Term := Term.lam (binder_explicit d) Term.hole Term.hole in match l { Term.lam b _ _ => match binder_name b { DebugName.named id => show_identifier id == "x", DebugName.unnamed => false, }, _ => false, }/// R2c's one semantic consequence, and it is a widening. `similar_term_go`'s/// `lam` arm compared `Similar DebugName` and now compares `Similar Binder`,/// so two lambdas whose binders differ only in name are similar -- exactly as/// the `pi` pin below has it. Only a binder the body never mentions is/// affected, because a `var` carries its own name and the body is still/// compared. Mutating that arm to compare `binder_name` restores the old/// rejection and fails the first conjunct.#[test]def test_lam_similarity_ignores_the_name : Bool := let body : Term := Term.var 0 DebugName.unnamed in let x_lam : Term := Term.lam (binder_named (Identifier.id "x")) Term.hole body in let y_lam : Term := Term.lam (binder_named (Identifier.id "y")) Term.hole body in let renamed : Term := Term.var 0 (DebugName.named (Identifier.id "y")) in let z_lam : Term := Term.lam (binder_named (Identifier.id "x")) Term.hole renamed in Similar.similar x_lam y_lam && Bool.not (Similar.similar x_lam z_lam)/// A level binder is not similar to an explicit binder even when their/// domains coincide -- and they CAN coincide, which is why this pin exists./// `wrap_level_forall` gives a level binder `Term.sort (SortLevel.concrete 0)`/// as its domain, and `Prop` lowers to exactly that term, so `forall u. C` and/// `(x : Prop) -> C` agree on the domain AND the codomain and differ only in/// `BinderInfo`. Before R2b the two were different constructors and `similar`/// answered `false` for free; the fold is what makes `info` load-bearing.////// Mutating `Similar Binder` to constant `true` -- or reverting/// `similar_term_go`'s `pi` arm to ignoring its binders, which is what it did/// before R2b -- makes this fail, and nothing else in the corpus does: every/// other consumer that must tell the two apart tests `info` directly rather/// than going through `Similar`.#[test]def test_level_binder_is_not_similar_to_a_prop_binder : Bool := let prop : Term := Term.sort (SortLevel.concrete 0) in let cod : Term := Term.sort (SortLevel.concrete 1) in let level_pi : Term := Term.pi (binder_level (Identifier.id "u")) prop cod in let explicit_pi : Term := Term.pi (binder_named (Identifier.id "x")) prop cod in let other_name : Term := Term.pi (binder_level (Identifier.id "v")) prop cod in Bool.not (Similar.similar level_pi explicit_pi) && Similar.similar level_pi other_name/// The three tags are pairwise distinct, and each predicate reads exactly/// one of them. A `binder_is_explicit` that answered `true` for a level/// binder would make every walker that guards on it treat a generalization/// as a function type -- which is the whole Class-2 hazard R2b creates, in/// one line.#[test]def test_binder_predicates_read_their_own_tag : Bool := let ex : Binder := binder_anon in let ty : Binder := binder_binder (Identifier.id "A") in let lv : Binder := binder_level (Identifier.id "u") in binder_is_explicit ex && Bool.not (binder_is_explicit ty) && Bool.not (binder_is_explicit lv) && binder_is_level lv && Bool.not (binder_is_level ex) && Bool.not (binder_is_level ty) && Bool.not (binder_is_explicit ty) && Bool.not (binder_is_level ex)#[test]def test_term_pi : Bool := let arg : Term := Term.sort (SortLevel.concrete 1) in let ret : Term := Term.sort (SortLevel.concrete 1) in let p : Term := Term.pi binder_anon arg ret in true#[test]def test_term_dep_pi : Bool := // Dependent pi: pi Nat (var 0 "n") — ret references arg at index 0 let arg : Term := Term.sort (SortLevel.concrete 0) in let ret : Term := Term.var 0 (DebugName.named (Identifier.id "n")) in let p : Term := Term.pi binder_anon arg ret in true#[test]def test_term_app : Bool := let f : Term := Term.var 0 (DebugName.unnamed) in let a : Term := Term.var 1 (DebugName.unnamed) in let app : Term := Term.app f a in true#[test]def test_term_lit : Bool := let l : Term := Term.lit (Literal.str "hello") in true#[test]def test_term_ntv : Bool := // Work around Native.mk forall-inference bug with List.empty // by using a non-empty list of args let none_opt : Option Term := Option.none in let args : List (Option Term) := List.cons none_opt List.empty in let ntv_val : Native := Native.mk (Identifier.id "foo") 0 args in let n : Term := Term.ntv ntv_val in true#[test]def test_term_con : Bool := // Work around Con.mk/NamePath.npath forall-inference bugs with List.empty // by using non-empty lists let none_opt : Option Term := Option.none in let args : List (Option Term) := List.cons none_opt List.empty in let mod_path : NamePath := NamePath.npath (List.cons (Identifier.id "Test") List.empty) in let con_val : Con := Con.mk (Identifier.id "Bar") mod_path 0 args in let c : Term := Term.con con_val in true#[test]def test_term_type : Bool := let t : Term := Term.sort (SortLevel.concrete 0) in true#[test]def test_term_hole : Bool := let h : Term := Term.hole in true// --- Phase 2: Scope types ---// Infix operator binding. Maps an operator symbol to a definition path.pub struct Infix { operator : Operator, name : NamePath,}// Instance lookup key.pub struct InstanceKey { cls : NamePath, constraints : List TypeConstraint, args : List Param,}// A resolved definition entry in scope.//// `vis` is the declaration's own visibility, carried here so scope// construction can act on it: a `priv` def is dropped when the module// being scoped is not the one that declared it (`build_scope_from_one_// module`, lang/src/scope.mo). Constructors and class methods inherit the// visibility of the type or class they belong to, which is why they are// built with the parent's `vis` rather than one of their own.pub struct ScopeDef { name : NamePath, module : ModulePath, sig : Term, body : Term, vis : Visibility,}// A class method entry in scope.pub struct ScopeClassDef { class_name : NamePath, full_name : NamePath, name : Identifier, sig : Term,}// Instance entries grouped by class name.pub struct ScopeInstance { class_name : NamePath, instances : List Instance,}// Conflicting name resolution entry.pub struct ScopeConflict { name : NamePath, candidates : List NamePath,}// Local variable in the scope chain.pub struct LocalVar { name : Identifier, typ : Term, multiplicity : Multiplicity,}// All resolved entries for a single scope level.//// `def_params`: a def's own DECLARED parameter list (`List Param`), in// order -- see `plans/implementations/named-field-construction.md`'s// Phase 6. DECLARED, not recovered: `build_scope_def` registers// `Def.params` straight off the decl and only falls back to walking the// `Term.lam` chain when the decl carries none. Deliberately a SEPARATE side-table from `def_refs`, not a// change to `ScopeDef.sig`/`.body`: that field's `Term.hole` sentinel// (set unconditionally by `build_scope_def`) is load-bearing for dozens// of existing call sites across the checker, which changing would risk// wide-reaching regressions -- named-call resolution only ever needs a// def's param NAMES (to match a call's own field names), TYPES (to// check each field's value against) and DEFAULTS (to stand in for an// omitted field), never its full body/signature, so this side-table is// both safer and sufficient. Has a `:=` default// (`Map.empty`) so every EXISTING `{ def_refs := .., .. }` struct-literal// construction site continues to build correctly unchanged (the checker// fills a missing field from its own declared default, same as any other// struct literal) -- only POSITIONAL `mk`/pattern-match destructuring// sites need updating for the new arity.pub struct ScopeData { def_refs : HashMap String ScopeDef, class_defs : List ScopeClassDef, instances : List ScopeInstance, // `HashMap`, not `List` -- mirrors `def_refs` (see bench/scope_lookup.mo): // every consumer looks this up by name (`scope_find_inductive`), never // iterates it, so a linear scan over every inductive in the merged // scope (~218+ corpus-wide) on every match-case/struct-literal check // was pure waste. `classes`, the sibling field just below, stays a // `List` (by-name lookup is now `scope_find_class`, lower corpus // cardinality than inductives, no measured need for a HashMap yet). inductives : HashMap String Inductive, // Full `Class` values (params/constraints/ordered methods), not a // synthetic zero-method `Inductive` stand-in -- `build_scope_class` // used to throw the real `Class` away and register a `dummy_ind` // instead, which is why `resolve_class_method`'s own class lookup // (`lang/typecheck/infer.mo`) could never actually resolve a class's // own declared params/methods. `scope_find_class`/`scope_data_classes` // (below) are the real by-name reader this field never had before. classes : List Class, infixes : List Infix, conflicts : List ScopeConflict, // `HashMap.map HashMap.empty_buckets` directly, not `Map.empty`: the // latter is a CLASS method (`instance [Hashable K, BOrd K] Map // HashMap`, `std/map.mo`) needing type-directed dispatch that a // struct field's default-value expression doesn't get the same way // an ordinary call site does (confirmed: `Map.empty` here fails at // evaluation with "unresolved global: Map.empty") -- `HashMap.map`/ // `.empty_buckets` are ordinary functions, no dispatch needed. def_params : HashMap String (List Param) := HashMap.map HashMap.empty_buckets, // A def's own DECLARED return type (the final non-`Pi`/`Forall` type // at the end of its signature's own Pi-chain, `Def.typ` -- NOT its // body's inferred type, and NOT `ScopeDef.sig`, which stays // unconditionally `Term.hole` by its own load-bearing design, see // `build_scope_def`'s doc comment). Lets `find_inductive_for_cases` // (`lang/typecheck/infer.mo`) resolve a match's scrutinee type when // it's a bare call to a known def (`match fresh_temp c { ... }`) -- // pure INFER-mode type-checking a call otherwise can't recover a // return type at all (`ScopeDef.sig` is hole), so it fell through to // an ambiguous constructor-NAME-only scan across every inductive in // scope; every `struct`'s auto-generated constructor is named `mk` // (`build_scope_struct`), so that scan is ambiguous between ANY two // structs the moment either is matched directly on a call result -- // confirmed to silently return the WRONG field's value, not just // fail loudly. Mirrors `def_params`'s own precedent exactly (added // for the analogous "recover param types without touching the // load-bearing `sig`/`body` hole sentinel" need). def_return_types : HashMap String Term := HashMap.map HashMap.empty_buckets, // A def's own FULL declared signature (`Def.typ` itself, e.g. // `forall V. Pi (xs : List V) (Option V)` for `def get_first {V : // Type} ...`) -- unlike `def_return_types` just above (the Pi-chain // STRIPPED final return type) this keeps the implicit-binder and // parameter types too, so a call site can check each argument // against the parameter's real declared type and solve the // signature's type variables from the arguments' actual types. // Same side-table pattern (and same never-touch-the-load-bearing- // `sig`-hole rule) as `def_params`/`def_return_types`; populated by // `build_scope_def`, consumed by `type_check_app`'s signature-driven // path (`lang/typecheck/infer.mo`). def_sigs : HashMap String Term := HashMap.map HashMap.empty_buckets, // A def's own BODY (`Def.term`), kept for DELTA REDUCTION -- // unfolding a global reference during conversion checking // (`lang/typecheck/whnf.mo`). Without it there is no name -> body // lookup reachable from inference at all: `build_scope_def` stores // `Term.hole` in `ScopeDef.body` unconditionally, and that sentinel // is load-bearing for dozens of call sites, so this follows the // same side-table pattern as `def_params`/`def_return_types`/ // `def_sigs` above rather than filling the hole in. // // Note what is stored is the body as `build_scope_def` sees it -- // PRE-elaboration, and still `Term.lam`-chain shaped for a def with // parameters, which is exactly what beta reduction then consumes // one argument at a time. def_bodies : HashMap String Term := HashMap.map HashMap.empty_buckets, // A def marked `#[cubical "..."]` (`proofs/src/cubical.mo`) bound to // the `CubicalPrim` the marker names -- the name-binding half of the // cubical design (the checker rewrite is in `lang/typecheck/infer.mo`: // `type_check_free_var` for bare primitives, `type_check_app`'s // cubical probe for applications). The MARKER, not the bare spelling, // binds, so a user's own `def I : Type` stays an ordinary def. // Keyed by the resolved `ScopeDef.name` exactly like `def_bodies` // above, and for the same reason: the lookup happens after // `scope_resolve_name`, under the qualified name it returns. cubical_prims : HashMap String CubicalPrim := HashMap.map HashMap.empty_buckets,}// A scope node in the linked list.pub struct Scope { module_id : ModulePath, scope : ScopeData, parent : Option Scope, // Read by `validate_match_coverage` (`lang/typecheck/infer.mo`), set by // `lang/module.mo`'s def-body sites from `has_incomplete_match_exemption`; // `false` means "checked", the safe default. // // Spell it at EVERY `Scope` literal -- all 69 in the tree do. Leaving it // to the default sends the Rust host into an unbounded missing-field fill // (`desugar_struct_literals`, `core/src/core_check.rs`) that OOMs the // whole-corpus check, so the pre-commit hook can never pass. incomplete_match_ok : Bool := false,}// Compiled or loaded module entry.pub struct Module { path : ModulePath, inductives : List Inductive, defs : List ScopeDef, infixs : List Infix, instances : List ScopeInstance,}// One module's own declarations, tagged with the module that OWNS them.//// The pipeline used to flatten every loaded module's decls into one// `List Decl` and hand the result a SINGLE `ModulePath` -- the target's --// so `build_scope_def` (`lang/scope.mo`) stamped every dependency def// with the CONSUMER's module. `find_def_by_module_and_name` matches a// qualified reference on name AND module, so a cross-module qualified// reference could never resolve. Carrying the owner alongside the decls// is what lets `build_scope_from_groups` register each def under its real// module instead.pub struct DeclGroup { path : ModulePath, decls : List Decl,}// A flat registry of loaded modules, keyed positionally by the list.//// Named `ModuleRegistry`, NOT `LoadedModules`, deliberately: `lang/// module.mo` declares its own, DIFFERENT `LoadedModules`// (`{main_module : ModuleInfo, all_modules : List ModuleInfo}`) which is// the one the real pipeline uses (`load_file_modules` ->// `elaborate_loaded_modules` -> codegen). Since this compiler's global// name table is not module-scoped, two same-named top-level types across// files silently collide -- whichever registers last wins for every// caller project-wide. `cli/src/main.mo` imported BOTH (one from// `lang.types`, one from `lang.module`), so the collision was live.// Renaming this one -- the narrower of the two, reached only by// `build_scope_from_modules` -- resolves it. See AGENTS.md item 18 for// the broader ~862-name duplicate-name sweep this is one instance of.pub struct ModuleRegistry { modules : List Module,}// Scope for local bindings (let expressions, case arms, lambda vars).pub struct LocalScope { vars : List LocalVar, parent : Option LocalScope,}// Error type for scope resolution failures.type ScopeError { name_not_found (name : NameRef), ambiguous_name (name : NameRef) (candidates : List NamePath), inductive_not_found (name : NamePath), instance_not_found (key : InstanceKey), class_not_found (name : NamePath), linear_used_twice (name : Identifier), affine_used_multiple (name : Identifier),}/// Returns true if the Result is ok, false if err.def result_is_ok {E A : Type} (r : Result E A) : Bool := match r { Result.ok _ => true, Result.err _ => false, }