use 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.empty def 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 ""]`. /// /// 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`) 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`; 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 -1 pub 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, .. }` (`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 { }` -- syntax as data. Mirrors the Rust reference's /// `Term::Quote { term: Box }` (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 ` — 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 := ` — 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` /// (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, }