Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090use lang::types { Attribute, Decl, Def, Identifier, InductConstructor, Inductive, Infix, Instance, InstanceKey, LocalScope, LocalVar, Module, ModulePath, ModuleRegistry, NamePath, NameRef, Param, QualifiedName, Scope, ScopeData, ScopeDef, ScopeError, ScopeInstance, Similar, Term, TypeConstraint, Visibility, binder_binder, many, named, package_private, param_many, priv_, pub_, sort_n, unnamed,}use lang::scope { LocalTypeBinding, add_constraint_dict_params, bind_term_vars, build_scope_from_decls, build_scope_from_modules, find_constraint_bound_carrier_any, infer_carrier_type, list_append, lookup_binding, mk, npath_eq, placeholder_carrier, resolve_def_in_scope_by_name, scope_data_add_def, scope_data_add_inductive, scope_data_add_instance, scope_data_empty, scope_find_inductive, scope_find_inductive_by_constructor, scope_find_local, scope_globals, scope_push_local, scope_resolve_instance, scope_resolve_name, term_to_slug,}use llvm::strmap {str_map_empty, str_map_insert}// --- Build scope from empty decl_list ---#[test]def test_build_empty_scope : Bool := let empty_id_list : List Identifier := List.empty in let empty_path : ModulePath := ModulePath.mp empty_id_list in let no_decls : List Decl := List.empty in let empty_scope : ScopeData := build_scope_from_decls empty_path no_decls in true// --- Build scope with a def declaration ---#[test]def test_build_with_def : Bool := let name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let empty_constraints : List TypeConstraint := List.empty in let empty_attrs : List Attribute := List.empty in let def_decl : Def := Def.mk name Term.hole Term.hole empty_constraints empty_attrs Visibility.package_private List.empty in let decl_list : List Decl := List.cons (Decl.def_d def_decl) List.empty in let sd : ScopeData := build_scope_from_decls mod_path decl_list in true// --- Build scope with an inductive declaration ---#[test]def test_build_with_inductive : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Bool") List.empty) in let empty_params : List Param := List.empty in let true_cn : InductConstructor := InductConstructor.mk (NamePath.npath (List.cons (Identifier.id "true") List.empty)) empty_params (sort_n 1) in let false_cn : InductConstructor := InductConstructor.mk (NamePath.npath (List.cons (Identifier.id "false") List.empty)) empty_params (sort_n 1) in let cns : List InductConstructor := List.cons true_cn (List.cons false_cn List.empty) in let empty_attrs : List Attribute := List.empty in let ind : Inductive := Inductive.mk type_name empty_params (sort_n 1) cns empty_attrs Visibility.package_private in let decl_list : List Decl := List.cons (Decl.inductive_d ind) List.empty in let sd : ScopeData := build_scope_from_decls mod_path decl_list in true// --- scope_globals extracts ScopeData from Scope ---#[test]def test_scope_globals : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let sd : ScopeData := scope_data_empty in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let g : ScopeData := scope_globals s in true// --- scope_find_inductive finds an inductive by name ---#[test]def test_scope_find_inductive_found : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Bool") List.empty) in let empty_params : List Param := List.empty in let true_cn : InductConstructor := InductConstructor.mk (NamePath.npath (List.cons (Identifier.id "true") List.empty)) empty_params (sort_n 1) in let cns : List InductConstructor := List.cons true_cn List.empty in let empty_attrs : List Attribute := List.empty in let ind : Inductive := Inductive.mk type_name empty_params (sort_n 1) cns empty_attrs Visibility.package_private in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_inductive` on // top of `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_inductive scope_data_empty ind in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let result : Result ScopeError Inductive := scope_find_inductive type_name s in match result { ok found => true, err _ => false }// --- scope_find_inductive returns error when not found ---#[test]def test_scope_find_inductive_not_found : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let lookup_name : NamePath := NamePath.npath (List.cons (Identifier.id "NoSuch") List.empty) in let sd : ScopeData := scope_data_empty in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let result : Result ScopeError Inductive := scope_find_inductive lookup_name s in match result { ok _ => false, err _ => true }// --- scope_push_local creates a new LocalScope ---#[test]def test_scope_push_local : Bool := let lv : LocalVar := { name := Identifier.id "x", typ := Term.hole, multiplicity := Multiplicity.many, } in let empty_parent : Option LocalScope := Option.none in let ls : LocalScope := { vars := List.empty, parent := empty_parent, } in let pushed : LocalScope := scope_push_local lv ls in true// --- scope_find_local finds a variable in LocalScope ---#[test]def test_scope_find_local_found : Bool := let lv : LocalVar := { name := Identifier.id "x", typ := sort_n 1, multiplicity := Multiplicity.many, } in let empty_parent : Option LocalScope := Option.none in let ls : LocalScope := { vars := List.cons lv List.empty, parent := empty_parent, } in let result : Option LocalVar := scope_find_local (Identifier.id "x") ls in match result { Option.some found => true, Option.none => false }// --- scope_find_local searches parent chain ---#[test]def test_scope_find_local_parent : Bool := let lv1 : LocalVar := { name := Identifier.id "x", typ := sort_n 1, multiplicity := Multiplicity.many, } in let lv2 : LocalVar := { name := Identifier.id "y", typ := sort_n 1, multiplicity := Multiplicity.many, } in let empty_parent : Option LocalScope := Option.none in let parent : LocalScope := { vars := List.cons lv1 List.empty, parent := empty_parent, } in let some_parent : Option LocalScope := Option.some parent in let child : LocalScope := { vars := List.cons lv2 List.empty, parent := some_parent, } in let result : Option LocalVar := scope_find_local (Identifier.id "x") child in match result { Option.some found => true, Option.none => false }// --- scope_find_local returns none when not found ---#[test]def test_scope_find_local_not_found : Bool := let empty_parent : Option LocalScope := Option.none in let ls : LocalScope := { vars := List.empty, parent := empty_parent, } in let result : Option LocalVar := scope_find_local (Identifier.id "x") ls in match result { Option.some _ => false, Option.none => true }// --- scope_resolve_name finds a def in ScopeData ---#[test]def test_scope_resolve_name_found : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in let def_entry : ScopeDef := { name := def_name, module := mod_path, sig := Term.hole, body := Term.hole, vis := Visibility.package_private, } in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_def` on top of // `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_def scope_data_empty def_entry in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let nref : NameRef := NameRef.nnp def_name in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent, } in let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in match result { ok found => true, err _ => false }// --- scope_resolve_name returns error when not found ---#[test]def test_scope_resolve_name_not_found : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let sd : ScopeData := scope_data_empty in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let nref : NameRef := NameRef.nnp (NamePath.npath (List.cons (Identifier.id "no_such") List.empty)) in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent, } in let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in match result { ok _ => false, err _ => true }// --- Builtin Type resolves ---#[test]def test_builtin_type_resolves : Bool := let empty_id_list : List Identifier := List.empty in let empty_path : ModulePath := ModulePath.mp empty_id_list in let no_decls : List Decl := List.empty in let sd : ScopeData := build_scope_from_decls empty_path no_decls in let s : Scope := { module_id := empty_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Type") List.empty) in let result : Result ScopeError ScopeDef := resolve_def_in_scope_by_name type_name s in match result { ok found => true, err _ => false }// --- Builtin Type inductive is found ---#[test]def test_builtin_type_inductive : Bool := let empty_id_list : List Identifier := List.empty in let empty_path : ModulePath := ModulePath.mp empty_id_list in let no_decls : List Decl := List.empty in let sd : ScopeData := build_scope_from_decls empty_path no_decls in let s : Scope := { module_id := empty_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Type") List.empty) in let result : Result ScopeError Inductive := scope_find_inductive type_name s in match result { ok found => true, err _ => false }// --- build_scope_from_modules with empty modules ---#[test]def test_build_from_modules_empty : Bool := let empty_id_list : List Identifier := List.empty in let empty_path : ModulePath := ModulePath.mp empty_id_list in let empty_modules : ModuleRegistry := { modules := List.empty, } in let sd : ScopeData := build_scope_from_modules empty_path empty_modules in true// --- build_scope_from_modules with one module ---#[test]def test_build_from_modules_one_def : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in let def_entry : ScopeDef := { name := def_name, module := mod_path, sig := Term.hole, body := Term.hole, vis := Visibility.package_private, } in let empty_instances : List ScopeInstance := List.empty in let empty_infixes : List Infix := List.empty in let empty_inductives : List Inductive := List.empty in let defs : List ScopeDef := List.cons def_entry List.empty in let m : Module := { path := mod_path, inductives := empty_inductives, defs := defs, infixs := empty_infixes, instances := empty_instances, } in let loaded : ModuleRegistry := { modules := List.cons m List.empty, } in let sd : ScopeData := build_scope_from_modules mod_path loaded in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let nref : NameRef := NameRef.nnp def_name in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent, } in let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in match result { ok found => true, err _ => false }// --- priv visibility ---/// `priv` is module-private: the declaring module sees it, no one else/// does. Built as a pair of tests over the same two-module fixture so the/// only difference between them is WHICH module is being scoped.def priv_fixture (vis : Visibility) : ModuleRegistry := let owner : ModulePath := ModulePath.mp [Identifier.id "Owner"] in let def_name : NamePath := NamePath.npath [Identifier.id "secret"] in let def_entry : ScopeDef := { name := def_name, module := owner, sig := Term.hole, body := Term.hole, vis := vis, } in let m : Module := { path := owner, inductives := ([] : List Inductive), defs := List.cons def_entry List.empty, infixs := ([] : List Infix), instances := ([] : List ScopeInstance), } in { modules := List.cons m List.empty }def priv_fixture_resolves_from (vis : Visibility) (consumer : ModulePath) : Bool := let sd : ScopeData := build_scope_from_modules consumer (priv_fixture vis) in let s : Scope := { module_id := consumer, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let locals : LocalScope := { vars := List.empty, parent := (Option.none : Option LocalScope) } in let nref : NameRef := NameRef.nnp (NamePath.npath [Identifier.id "secret"]) in match scope_resolve_name nref s locals { ok _ => true, err _ => false }#[test]def test_priv_def_is_visible_in_its_own_module : Bool := priv_fixture_resolves_from Visibility.priv_ (ModulePath.mp [Identifier.id "Owner"])#[test]def test_priv_def_is_hidden_from_other_modules : Bool := not (priv_fixture_resolves_from Visibility.priv_ (ModulePath.mp [Identifier.id "Other"]))/// The default (package-private) still crosses module boundaries -- only/// `priv` is enforced today, and the mote boundary is a later step.#[test]def test_package_private_def_still_crosses_modules : Bool := priv_fixture_resolves_from Visibility.package_private (ModulePath.mp [Identifier.id "Other"])#[test]def test_pub_def_crosses_modules : Bool := priv_fixture_resolves_from Visibility.pub_ (ModulePath.mp [Identifier.id "Other"])// --- scope_resolve_instance found ---#[test]def test_scope_resolve_instance_found : Bool := let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Monad") List.empty) in let inst_name : Identifier := Identifier.id "maybeMonad" in let empty_constraints : List TypeConstraint := List.empty in let empty_args : List Term := List.empty in let ins : Instance := Instance.mk inst_name cls_name empty_constraints empty_args Visibility.package_private List.empty List.empty in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_instance` on // top of `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_instance scope_data_empty ins in let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let empty_params : List Param := List.empty in let key : InstanceKey := { cls := cls_name, constraints := empty_constraints, args := empty_params, } in let result : Result ScopeError Instance := scope_resolve_instance cls_name key s in match result { ok found => true, err _ => false }// --- scope_resolve_instance not found ---#[test]def test_scope_resolve_instance_not_found : Bool := let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Monad") List.empty) in let sd : ScopeData := scope_data_empty in let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let empty_params : List Param := List.empty in let empty_constraints : List TypeConstraint := List.empty in let key : InstanceKey := { cls := cls_name, constraints := empty_constraints, args := empty_params, } in let result : Result ScopeError Instance := scope_resolve_instance cls_name key s in match result { ok _ => false, err _ => true }// --- list_append appends two lists ---#[test]def test_list_append_empty : Bool := let empty : List I64 := List.empty in let result : List I64 := list_append empty empty in true// --- list_append with non-empty list ---#[test]def test_list_append_non_empty : Bool := let xs : List I64 := List.cons (1 : I64) (List.cons (2 : I64) List.empty) in let ys : List I64 := List.cons (3 : I64) (List.cons (4 : I64) List.empty) in let result : List I64 := list_append xs ys in true// --- scope_resolve_instance matches by class name ---#[test]def test_scope_resolve_instance_matches_class : Bool := let cls_name1 : NamePath := NamePath.npath (List.cons (Identifier.id "Show") List.empty) in let cls_name2 : NamePath := NamePath.npath (List.cons (Identifier.id "Monad") List.empty) in let inst_show : Instance := Instance.mk (Identifier.id "showBool") cls_name1 List.empty List.empty Visibility.package_private List.empty List.empty in let inst_monad : Instance := Instance.mk (Identifier.id "maybeMonad") cls_name2 List.empty List.empty Visibility.package_private List.empty List.empty in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_instance` on // top of `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_instance (scope_data_add_instance scope_data_empty inst_show) inst_monad in let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let empty_params : List Param := List.empty in let key : InstanceKey := { cls := cls_name2, constraints := List.empty, args := empty_params, } in let result : Result ScopeError Instance := scope_resolve_instance cls_name2 key s in match result { ok ins => match ins { mk name cls _ _ _ _ _ => Similar.similar name (Identifier.id "maybeMonad") }, err _ => false }// --- build_scope_from_decls resolves a def through scope_resolve_name ---#[test]def test_build_scope_then_resolve_def : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "add") List.empty) in let def_decl : Def := Def.mk def_name Term.hole Term.hole List.empty List.empty Visibility.package_private List.empty in let decl_list : List Decl := List.cons (Decl.def_d def_decl) List.empty in let sd : ScopeData := build_scope_from_decls mod_path decl_list in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let nref : NameRef := NameRef.nnp def_name in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent, } in let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in match result { ok d => true, err _ => false }// --- build_scope_from_decls resolves an inductive constructor ---#[test]def test_build_scope_then_resolve_constructor : Bool := let mod_id : Identifier := Identifier.id "Test" in let mod_path : ModulePath := ModulePath.mp (List.cons mod_id List.empty) in let type_name : NamePath := NamePath.npath (List.cons (Identifier.id "Bool") List.empty) in let true_name : NamePath := NamePath.npath (List.cons (Identifier.id "true") List.empty) in let empty_params : List Param := List.empty in let true_cn : InductConstructor := InductConstructor.mk true_name empty_params (sort_n 1) in let cns : List InductConstructor := List.cons true_cn List.empty in let empty_attrs : List Attribute := List.empty in let ind : Inductive := Inductive.mk type_name empty_params (sort_n 1) cns empty_attrs Visibility.package_private in let decl_list : List Decl := List.cons (Decl.inductive_d ind) List.empty in let sd : ScopeData := build_scope_from_decls mod_path decl_list in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in let nref : NameRef := NameRef.nnp true_name in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent, } in let result : Result ScopeError ScopeDef := scope_resolve_name nref s locals in match result { ok d => match d { mk name _ _ _ _ => Similar.similar name true_name }, err _ => false }// --- instance_key_matches compares type args ---#[test]def test_instance_key_matches_type_args : Bool := let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Show") List.empty) in let i64_typ : Term := sort_n 1 in let bool_typ : Term := sort_n 1 in let show_i64 : Instance := Instance.mk (Identifier.id "showI64") cls_name List.empty (List.cons i64_typ List.empty) Visibility.package_private List.empty List.empty in let show_bool : Instance := Instance.mk (Identifier.id "showBool") cls_name List.empty (List.cons bool_typ List.empty) Visibility.package_private List.empty List.empty in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_instance` on // top of `scope_data_empty` rather than a hand-written literal. // Insertion order reversed vs. the original hand-written list // (`show_bool` first, `show_i64` last) — `scope_data_add_instance` // prepends to its class's instance list, so this preserves the // original `[show_i64, show_bool]` order: `show_i64`/`show_bool` // here deliberately share the same level-1 sort arg (see above), // so `first_matching_instance`'s scan needs this exact order to // still return `show_i64` first, matching this test's intent. let sd : ScopeData := scope_data_add_instance (scope_data_add_instance scope_data_empty show_bool) show_i64 in let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in // Key requesting Show I64 — should find show_i64 instance let key_i64 : InstanceKey := { cls := cls_name, constraints := List.empty, args := List.cons (param_many (Identifier.id "A") i64_typ) List.empty, } in match scope_resolve_instance cls_name key_i64 s { ok found => match found { mk name _ _ _ _ _ _ => Similar.similar name (Identifier.id "showI64"), }, err _ => false, }#[test]def test_instance_key_matches_wrong_type_args : Bool := let cls_name : NamePath := NamePath.npath (List.cons (Identifier.id "Show") List.empty) in let i64_typ : Term := sort_n 1 in let string_typ : Term := sort_n 2 in // different from type_1 let show_i64 : Instance := Instance.mk (Identifier.id "showI64") cls_name List.empty (List.cons i64_typ List.empty) Visibility.package_private List.empty List.empty in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_instance` on // top of `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_instance scope_data_empty show_i64 in let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in // Key requesting Show String — should NOT find show_i64 let key_string : InstanceKey := { cls := cls_name, constraints := List.empty, args := List.cons (param_many (Identifier.id "A") string_typ) List.empty, } in match scope_resolve_instance cls_name key_string s { ok _ => false, err _ => true, }// --- scope_find_inductive_by_constructor finds inductive by constructor name ---#[test]def test_find_inductive_by_constructor_found : Bool := let ind_name : NamePath := NamePath.npath (List.cons (Identifier.id "Maybe") List.empty) in let some_np : NamePath := NamePath.npath (List.cons (Identifier.id "some") List.empty) in let none_np : NamePath := NamePath.npath (List.cons (Identifier.id "none") List.empty) in let some_cn : InductConstructor := InductConstructor.mk some_np List.empty (sort_n 1) in let none_cn : InductConstructor := InductConstructor.mk none_np List.empty (sort_n 1) in let cns : List InductConstructor := List.cons some_cn (List.cons none_cn List.empty) in let ind : Inductive := Inductive.mk ind_name List.empty (sort_n 1) cns List.empty Visibility.package_private in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_inductive` on // top of `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_inductive scope_data_empty ind in let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in // Look up by "some" constructor — should find Maybe match scope_find_inductive_by_constructor some_np s { Option.some found => match found { mk name _ _ _ _ _ => npath_eq name ind_name, }, Option.none => false, }#[test]def test_find_inductive_by_constructor_not_found : Bool := let ind_name : NamePath := NamePath.npath (List.cons (Identifier.id "Maybe") List.empty) in let some_np : NamePath := NamePath.npath (List.cons (Identifier.id "some") List.empty) in let some_cn : InductConstructor := InductConstructor.mk some_np List.empty (sort_n 1) in let ind : Inductive := Inductive.mk ind_name List.empty (sort_n 1) [some_cn] List.empty Visibility.package_private in // `def_refs` is a `std.map` `HashMap` (see `lang/scope.mo`'s own `use // std.map {}` doc comment) — built via `scope_data_add_inductive` on // top of `scope_data_empty` rather than a hand-written literal. let sd : ScopeData := scope_data_add_inductive scope_data_empty ind in let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "Test") List.empty) in let s : Scope := { module_id := mod_path, scope := sd, parent := Option.none, incomplete_match_ok := false, } in // Look up by "nope" constructor — should NOT find let nope_np : NamePath := NamePath.npath (List.cons (Identifier.id "nope") List.empty) in match scope_find_inductive_by_constructor nope_np s { Option.some _ => false, Option.none => true, }// --- dict-param placeholder regression (gap 7) ---/// A constrained def whose body calls its own constraint's class method/// (`Add.add a b` -- the `instance [Add A] HAdd A A A` -> `HAdd_A_A_A_add`/// shape) qualifies for a leading dictionary parameter. That parameter's/// own `typ` annotation MUST be `Term.hole` (which `type_check` always/// succeeds on, returning `expected_type`), never a bound `Term.var 0`:/// `check_def_with_scope` checks a def's body against `Term.hole`, so/// `type_check_lam`'s non-`pi` branch re-checks each lambda's own written/// param type against the current `local_types` stack -- and the/// outermost dict lambda is checked with that stack EMPTY, so a/// `Term.var 0` placeholder reported a spurious out-of-range `bound_var`/// (the `HAdd_A_A_A_add` self-hosted-check gap). Mirrors the Rust/// reference's own dictionary/projected-method placeholder/// (`CoreTerm::Hole`, `core_check_module`).#[test]def test_dict_param_type_is_hole : Bool := let add_cls : NamePath := NamePath.npath (List.cons (Identifier.id "Add") List.empty) in let constraint : TypeConstraint := TypeConstraint.mk add_cls (List.cons (Identifier.id "A") List.empty) in let constraints : List TypeConstraint := List.cons constraint List.empty in // The body's `Add.add` reference is what `qualifying_dict_constraints` // needs (`def_references_class` scans for a `var` whose name starts // with `"Add."`) to qualify the constraint for a leading dict param. let add_add_ref : Term := Term.var (-1) (DebugName.named (Identifier.id "Add.add")) in let body : Term := Term.app add_add_ref (Term.var (-1) (DebugName.named (Identifier.id "a"))) in let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "HAdd_A_A_A_add") List.empty) in let empty_attrs : List Attribute := List.empty in let df : Def := Def.mk def_name Term.hole body constraints empty_attrs Visibility.package_private List.empty in match add_constraint_dict_params df { Def.mk {typ := _new_typ, term := new_term, ..} => match new_term { Term.lam _dbg param_typ _body => match param_typ { Term.hole => true, _ => false, }, _ => false, }, }// --- Module-qualified references (`NameRef.nqn`) ---//// These are the first tests anywhere to exercise `nqn`. The parser builds// one, but `lower_parse.mo` renders it to a flat `DebugName` string and// every checker call site rebuilt it as a bare `nid` -- so// `resolve_name_in_scope`'s `nqn` arm was unreachable and a qualified// reference always reported `unknown variable`./// A `nqn` resolves by matching (module, name) as a PAIR: a def declared/// bare (`process_id` in `std::process`) carries no prefix in its own/// registered name, so the flattened-key lookup misses and the by-module/// fallback is what has to answer.#[test]def test_scope_resolve_qualified_name : Bool := let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "std") (List.cons (Identifier.id "process") List.empty)) in let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "process_id") List.empty) in let def_entry : ScopeDef := { name := def_name, module := mod_path, sig := Term.hole, body := Term.hole, vis := Visibility.package_private, } in let sd : ScopeData := scope_data_add_def scope_data_empty def_entry in let s : Scope := { module_id := ModulePath.mp (List.cons (Identifier.id "Main") List.empty), scope := sd, parent := Option.none, incomplete_match_ok := false, } in let qn : QualifiedName := { qmod := mod_path, qname := def_name } in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent } in match scope_resolve_name (NameRef.nqn qn) s locals { ok found => true, err _ => false }/// The MODULE half must be load-bearing: a qualified reference naming the/// right def in the WRONG module must not resolve, or the qualifier is/// decoration and a typo silently becomes a working reference.#[test]def test_scope_qualified_wrong_module_does_not_resolve : Bool := let mod_path : ModulePath := ModulePath.mp (List.cons (Identifier.id "std") (List.cons (Identifier.id "process") List.empty)) in let def_name : NamePath := NamePath.npath (List.cons (Identifier.id "process_id") List.empty) in let def_entry : ScopeDef := { name := def_name, module := mod_path, sig := Term.hole, body := Term.hole, vis := Visibility.package_private, } in let sd : ScopeData := scope_data_add_def scope_data_empty def_entry in let s : Scope := { module_id := ModulePath.mp (List.cons (Identifier.id "Main") List.empty), scope := sd, parent := Option.none, incomplete_match_ok := false, } in let wrong : ModulePath := ModulePath.mp (List.cons (Identifier.id "std") (List.cons (Identifier.id "nosuch") List.empty)) in let qn : QualifiedName := { qmod := wrong, qname := def_name } in let empty_parent : Option LocalScope := Option.none in let locals : LocalScope := { vars := List.empty, parent := empty_parent } in match scope_resolve_name (NameRef.nqn qn) s locals { ok _ => false, err _ => true }// --- A placeholder is a WEAK carrier, never a dropped one ---//// `infer_carrier_type`'s `Term.var` arm reads a local's declared type out of// the env. An un-annotated binding's desugared binder holds a placeholder --// a hole, or the bare sort W1.1's lowering made of an un-annotated lambda// parameter -- and a placeholder names no head -- so `term_matches_carrier`// cannot fail against one and it matches EVERY instance, which makes it// worse than useless whenever it outranks a real carrier.//// It is still handed on, because it is sometimes the ONLY evidence a call// has. MEASURED: refusing it here (answering `Option.none` in that arm)// turned `init/src/foldable_tests.mo`'s `Foldable.foldr (fn x acc => x + acc)// 0 [] == 0` into `no instance found for `Foldable.foldr`` -- the// un-annotated lambda's placeholder-typed binder is the only carrier// candidate the empty `[]` leaves behind, so with it dropped nothing matched// `instance Foldable List`. The PRECEDENCE problem is what// `demote_uninformative_carriers` solves at the call sites, by moving a// placeholder behind every real carrier instead of removing it -- see// `placeholder_carrier`'s own doc comment in `lang/scope.mo`.#[test]def test_placeholder_carrier_sorts_and_holes : Bool := placeholder_carrier (sort_n 1) && placeholder_carrier (sort_n 0) && placeholder_carrier Term.hole#[test]def test_placeholder_carrier_named_types : Bool := Bool.not (placeholder_carrier (Term.var 0 (DebugName.named (Identifier.id "I64")))) && Bool.not (placeholder_carrier (Term.app (Term.var 0 (DebugName.named (Identifier.id "List"))) (Term.var 0 (DebugName.named (Identifier.id "I64")))))/// The env an un-annotated `let` leaves behind, for one name.def placeholder_env (nm : Identifier) (ty : Term) : List LocalTypeBinding := List.cons (LocalTypeBinding.mk nm ty) List.emptydef local_var (nm : Identifier) : Term := Term.var 0 (DebugName.named nm)/// A placeholder-typed local is still OFFERED as a carrier -- dropping it/// would lose the `Foldable.foldr ... []` resolution above.#[test]def test_placeholder_local_yields_a_carrier : Bool := match infer_carrier_type (placeholder_env (Identifier.id "filtered") (sort_n 1)) List.empty str_map_empty List.empty (local_var (Identifier.id "filtered")) { Option.some _ => true, Option.none => false, }/// Control: a local whose declared type names something still offers itself/// as a carrier, with its arguments intact.#[test]def test_named_local_still_yields_a_carrier : Bool := match infer_carrier_type (placeholder_env (Identifier.id "xs") (Term.var 0 (DebugName.named (Identifier.id "I64")))) List.empty str_map_empty List.empty (local_var (Identifier.id "xs")) { Option.some c => match c { Term.var _ dbg => match dbg { DebugName.named nm => Similar.similar nm (Identifier.id "I64"), DebugName.unnamed => false, }, _ => false, }, Option.none => false, }// --- The constraint's own variable resolves at the BOUND carrier ---//// `resolve_ordinary_constrained_call` has no instance head of its own, so it// passes `bindings = List.empty` to `constraint_carriers`, which then answers// `[carrier]` -- the WHOLE carrier. Resolving `[BEq A]` at the whole carrier// `List I64` re-matches `instance [BEq A] BEq (List A)`, and a dict name is// mangled from the INSTANCE's declared args, so the element slot of a// `List I64` comparison received `__Dict_BEq_List_A` and the driver read a// raw `I64` in `monad_get_tag`. That is the B3 SIGSEGV in// `std/src/list_tests3a.mo`. `find_constraint_bound_carrier_any` resolves the// constraint at the carrier the matched instance's own head BINDS that// variable to instead (`A := I64`, so `__Dict_BEq_I64`).def var_named (nm : String) : Term := Term.var 0 (DebugName.named (Identifier.id nm))def list_of (t : Term) : Term := Term.app (var_named "List") tdef only_instance (ins : Instance) : List Instance := List.cons ins List.emptydef beq_cls : NamePath := NamePath.npath (List.cons (Identifier.id "BEq") List.empty)/// `instance [BEq A] BEq (List A)`, in the shape the parser produces it.def beq_list_instance : Instance := Instance.mk (Identifier.id "BEq_List_A") beq_cls (List.cons (TypeConstraint.mk beq_cls (List.cons (Identifier.id "A") List.empty)) List.empty) (List.cons (list_of (var_named "A")) List.empty) Visibility.package_private [param_many (Identifier.id "A") (sort_n 1)] List.empty/// `instance [Show A] Show A` -- a candidate that binds `A` back to `A` is/// no progress at all, so nothing may be read from it.def show_a_instance : Instance := Instance.mk (Identifier.id "Show_A") (NamePath.npath (List.cons (Identifier.id "Show") List.empty)) (List.cons (TypeConstraint.mk (NamePath.npath (List.cons (Identifier.id "Show") List.empty)) (List.cons (Identifier.id "A") List.empty)) List.empty) (List.cons (var_named "A") List.empty) Visibility.package_private [param_many (Identifier.id "A") (sort_n 1)] List.emptydef bound_carrier_slug (ins : Instance) (cls : NamePath) (vars : List Identifier) (c : Term) : String := match find_constraint_bound_carrier_any (only_instance ins) cls vars (List.cons c List.empty) { Option.some p => match p { Pair.pair bound _matched => term_to_slug bound, }, Option.none => "<none>", }/// The measured B3 shape: `List I64` against `instance [BEq A] BEq (List A)`/// binds `A := I64`, so the constraint resolves at `I64`, NOT at the whole/// `List I64` that mentions it.#[test]def test_constraint_bound_carrier_is_the_bound_element : Bool := String.beq (bound_carrier_slug beq_list_instance beq_cls (List.cons (Identifier.id "A") List.empty) (list_of (var_named "I64"))) "I64"/// A candidate that binds the constraint's variable BACK to itself makes no/// progress, so it is skipped rather than resolved at.#[test]def test_constraint_bound_carrier_skips_no_progress : Bool := String.beq (bound_carrier_slug show_a_instance (NamePath.npath (List.cons (Identifier.id "Show") List.empty)) (List.cons (Identifier.id "A") List.empty) (var_named "A")) "<none>"/// A candidate that matches no instance at all yields nothing.#[test]def test_constraint_bound_carrier_requires_a_match : Bool := String.beq (bound_carrier_slug beq_list_instance beq_cls (List.cons (Identifier.id "A") List.empty) (var_named "I64")) "<none>"/// ...and so does a constraint with no candidate to read from.#[test]def test_constraint_bound_carrier_needs_a_candidate : Bool := match find_constraint_bound_carrier_any (only_instance beq_list_instance) beq_cls (List.cons (Identifier.id "A") List.empty) List.empty { Option.some _ => false, Option.none => true, }// --- The def-type table is `forall`-wrapped, so a HEAD read off it must// --- unquantify first.//// `collect_def_types` registers every def type `elaborate_def`-wrapped// (`registered_def_type`), which is what gives the callee-signature// channel the `Forall` binders it reads. The arm of `infer_carrier_type`// that reads a bare HEAD off that same value (`type_head_name_local`) sees// nothing in a `forall`, so it answered NO carrier where the raw type// answered one. MEASURED: the promoted `FromListLiteral_List_empty` -- the// callee that arm's own comment names as its load-bearing case -- left the// enclosing `Foldable.foldr (fn x acc => x + acc) 0 []` with nothing to// infer `Foldable`'s own carrier from, and it reported `no instance found`.// The bare empty-list literal was the only casualty: an ascription, a typed// `let`, `List.empty`, a non-empty literal and a bare `none` all take other// arms./// The shape this table holds for a def that quantifies over its own/// variable -- what `registered_def_type` guarantees.def quantified_def_typ : Term := Term.pi (binder_binder (Identifier.id "A")) Term.hole (list_of (var_named "A"))/// The carrier `infer_carrier_type` reads off a 0-arg def REFERENCE/// (`empty`, what `[]` desugars to), as a slug.def def_ref_carrier_slug (typ : Term) : String := match infer_carrier_type List.empty List.empty (str_map_insert "empty" typ str_map_empty) List.empty (var_named "empty") { Option.some c => term_to_slug c, Option.none => "<none>", }#[test]def test_def_ref_carrier_reads_through_a_quantified_type : Bool := String.beq (def_ref_carrier_slug quantified_def_typ) "List"#[test]def test_def_ref_carrier_reads_a_bare_type_too : Bool := String.beq (def_ref_carrier_slug (list_of (var_named "A"))) "List"// --- bind_term_vars: an applied shape pairs with the applied carrier ---/// `StateT I64 Id I64` fully applied -- the carrier the `instance [Monad/// M] Monad (StateT S M)` call site in `init/src/transformers_tests.mo`/// dispatches at.def statet_applied : Term := Term.app (Term.app (Term.app (var_named "StateT") (var_named "I64")) (var_named "Id")) (var_named "I64")/// The same, asymmetric, so a pin can tell LEADING from TRAILING pairing:/// the element type differs from the parameters'.def statet_asym : Term := Term.app (Term.app (Term.app (var_named "StateT") (var_named "I64")) (var_named "Id")) (var_named "U8")/// The binding `bind_term_vars` records for `nm`, as a slug.def bound_slug (wildcards : List Identifier) (shape : Term) (actual : Term) (nm : String) : String := match lookup_binding (bind_term_vars wildcards shape actual List.empty) (Identifier.id nm) { Option.some t => term_to_slug t, Option.none => "<none>", }/// MEASURED (`transformers_tests.mo`, driver exited -1): the instance's own/// arg is a PARTIAL application of the carrier's head, so its variables/// align with the carrier's FIRST args. Pairing the spines from the/// outside bound `M := I64` (the ELEMENT type), which sent `[Monad M]`'s/// dictionary lookup to `I64` -- where only prelude's wildcard-headed/// bridge matches, so the promoted `StateT` method got the bridge's/// dictionary and died on entry. `spine_matches` (the match side) was/// already left-aligned; this is the binding side.#[test]def test_bind_term_vars_left_aligns_a_partial_application : Bool := let shape := Term.app (Term.app (var_named "StateT") (var_named "S")) (var_named "M") in let wildcards : List Identifier := [Identifier.id "S", Identifier.id "M"] in String.beq (bound_slug wildcards shape statet_applied "S") "I64" && String.beq (bound_slug wildcards shape statet_applied "M") "Id"/// A hole HEAD names a type constructor -- the carrier's head applied to/// the params the shape's own arg does not name -- so its arg pairs with/// the carrier's LAST. Both halves are pinned (the head loses `U8`, the/// arg gains it), which is what a leading/trailing mix-up breaks.#[test]def test_bind_term_vars_binds_a_hole_head_to_the_carrier_prefix_and_its_arg_to_the_tail : Bool := let shape := Term.app (var_named "M") (var_named "A") in let wildcards : List Identifier := [Identifier.id "M", Identifier.id "A"] in String.beq (bound_slug wildcards shape statet_asym "M") "StateT_I64_Id" && String.beq (bound_slug wildcards shape statet_asym "A") "U8"/// The bridge's own shape: two hole args, one carrier param between them/// and the head (`M I I` against `StateT I64 Id U8`). `I` is recorded/// twice; the later record wins (`lookup_binding` scans the prepended/// list front-first), so the pin's `U8` also says the pair ran to the end.#[test]def test_bind_term_vars_walks_a_hole_heads_args_along_the_carrier_tail : Bool := let shape := Term.app (Term.app (var_named "M") (var_named "I")) (var_named "I") in let wildcards : List Identifier := [Identifier.id "M", Identifier.id "I"] in String.beq (bound_slug wildcards shape statet_asym "M") "StateT_I64" && String.beq (bound_slug wildcards shape statet_asym "I") "U8"/// The equal-arity case is unchanged either way -- `instance [BEq A] BEq/// (List A)` against `List I64`.#[test]def test_bind_term_vars_aligns_equal_arity_spines : Bool := String.beq (bound_slug [Identifier.id "A"] (list_of (var_named "A")) (list_of (var_named "I64")) "A") "I64"