diff --git a/dag/gunbc/explicit_witness_admission.dag b/dag/gunbc/explicit_witness_admission.dag index 6e8fdd61f70..54028199a1f 100644 --- a/dag/gunbc/explicit_witness_admission.dag +++ b/dag/gunbc/explicit_witness_admission.dag @@ -193,6 +193,62 @@ fn known_red_pre_verdict_probe( data known_red_class_note: String = "WHAT A KNOWN-RED ADMISSION IS: a witness red on main for a feature gap owned by a named lane. It is a RED CONTROL for that lane, not a broken test — deleting it would discard the discriminating input, while leaving it in per-PR discovery would red every wide PR on a debt that PR did not create. Greening is the counted un-quarantine event of std.witness_admission: the row deletes in the SAME change that lands the fix, which promotes the unchanged witness to ordinary DiscoverySelection as a permanent regression control (DESIGN 4b(4) — the climb deletes the quarantine machinery, never the evidence). A DISSOLVE_ON MUST NAME A FACT THAT IS FALSE TODAY AND BECOMES TRUE EXACTLY WHEN THE FIX LANDS, and this requirement is here because two rows failed it in one night. A trigger keyed on a condition already satisfied is not a trigger, it is a deletion licence with a date on it: whoever next reads it dissolves a quarantine standing in for a defect that is still live, and the row reads as dissolved-per-its-own-terms while the wall it substituted for does not exist. RECEIPT 1, another lane's: the #8592 row's trigger read 'the mirrors are regenerated so the compiled harness CONTAINS declared_arg_types_for_method' — that symbol has been present in v1_compiler_infer_lookup.rs all along, so the trigger was satisfiable from the moment it was written, while the defect it quarantines is live (on main the function still takes no TypeEnv, which is precisely the bug). RECEIPT 2, MY OWN, AND IT IS THE MORE INSTRUCTIVE ONE BECAUSE THE DELETION WAS STILL CORRECT: the min-length row's trigger read 'the compiled harness contains the wall'. Measured, where_refinement_predicates_covered has 2 occurrences in that mirror on main and always did, so a reader checking 'the wall' would have dissolved the row at any point in the preceding weeks. It dissolved correctly only because the author happened to grep where_predicate_guaranteed_min_length, which was 0 on main and 2 after the regen. THE TRIGGER DID NOT ENCODE WHICH FACT DECIDED IT; the right answer came from the reader, not the row. So: name the symbol, signature or behaviour whose ABSENCE is the gap — a new parameter, a specific new function, a named repro passing — never a category word like 'the wall' or 'the fix', and never a symbol that predates the change. The test a reviewer applies: run the trigger's check against main TODAY, and if it passes, the trigger is defective and the row is unprotected. The roster must not grow silently: a new admission carries a reason naming the diagnosis and owner plus a dissolve_on, both refused empty by NonEmptyStr, and a row whose witness runs green locally is stale and deletes. Local recipe per row: claim_batch --source-root dag --source-root src/v2 --entry --functions -- AND FOR AN ExecutionWitnessKind ROW, --wet AS WELL, WITHOUT WHICH THE RECIPE CANNOT DO WHAT THE ROW ASKS OF IT. claim_batch is hermetic by default, so a wet row invoked by the recipe as written above never reaches its subject: measured 2026-08-26 on self_host_logic_behavioral_receipt_holds, it returns FAIL in 87 seconds with 'hermetic route has no arm for Dir: the claim never reached its subject, so this is a route gap and not a verdict', naming three undeclared dispatches (Filesystem.Read, git.Inspect.Toplevel, shell.Mktemp.Dir). The refusal is well-modeled and says plainly that it is not a verdict; the defect was in the recipe, which every wet dissolution condition below cites as the way its row greens. A row whose only recorded closing move cannot close it is the shape DESIGN records for a gate whose sole green is the forbidden action -- here arrived at from the other side, with no green reachable at all. CorpusWitnessKind rows run on the hermetic falsifier probe batch; ExecutionWitnessKind rows run on the falsifier wet quarantine batch." data explicit_witness_admissions: List = [ + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_headless_literal_equals_the_headed_introduction_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "map arm control under Map (the headless map literal elaborates to exactly the headed introduction), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.", + dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection") + ), + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_a_duplicate_key_refuses_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "map arm control under Map (a repeated key refuses resolve_anonymous_map_duplicate_key at its second occurrence), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.", + dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection") + ), + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_an_escaped_and_a_raw_key_are_one_key_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "map arm control under Map (an escaped key and its raw scalar collide under the decoded-text key law), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.", + dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection") + ), + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_distinct_keys_are_accepted_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "map arm control under Map (distinct keys elaborate), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.", + dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection") + ), + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_infer_refuses_an_elaborated_value_mismatch_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "map arm control under Map (infer refuses an elaborated map whose value does not inhabit V), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.", + dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection") + ), + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_an_elaborated_map_infers_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "map arm control: a well-typed elaborated map infers. RED beyond the map arm: measured with gunbc#12760 merged, infer refuses infer_grounding_not_derived located (NodeLocus) at the MapIntroductionEntry { .. } construct, identically for the HEADED spelling and under Map. The discriminating specimen ml_a_same_module_generic_entry_construct_infers_holds (generic record declared in the same module) refuses the same way, so this is neither cross-module declaration reading (#12726 PR2) nor the v2 Bool fork. Owner: smart-newt-725 (record construct typing, #12763 lineage), per quiet-gull-780.", + dissolution: unbound_dissolution(description: "infer grounds a construct of a generic record whose type arguments come only from its expected type (callee parameter or list element): this witness greens and the row deletes in that change") + ), + known_red_probe( + entry: "src/v2/test/claim/body_lowering/map_literal_test.dag", + f: "ml_a_same_module_generic_entry_construct_infers_holds", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "the discriminating specimen for ml_an_elaborated_map_infers_holds: LocalEntry and local_from_entries declared beside the data decl, so no cross-module declaration is read; infer refuses infer_grounding_not_derived at the LocalEntry { .. } construct (measured with gunbc#12760 merged; without it, unbound String refuses first). Owner: smart-newt-725.", + dissolution: unbound_dissolution(description: "infer grounds a construct of a generic record whose type arguments come only from its expected type (callee parameter or list element): this witness greens and the row deletes in that change") + ), known_red_probe( entry: "dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag", f: "w_a_branded_product_refinement_at_an_unrelated_product_formal_still_refuses", diff --git a/dag/gunbc/recurring_failure_mode/expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering.dag b/dag/gunbc/recurring_failure_mode/expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering.dag index b90e358013b..d610a3ba452 100644 --- a/dag/gunbc/recurring_failure_mode/expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering.dag +++ b/dag/gunbc/recurring_failure_mode/expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering.dag @@ -14,6 +14,7 @@ data expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body "DISTINGUISHING FACTS. Not `lowering_accessor_collapses_a_sequence_operand`, which keeps the LEFT element of an operand; here the block is kept and the enclosing expression is lost. Not gunbc#11911, a parse-order defect; here the parse accepts. Not `match_arms_after_the_second_are_dropped_at_v2_body_lowering`, which loses arms INSIDE a match; this loses what is AROUND it.", "RUNG FOUND AT: below the floor (silent wrongness). CEILING: structurally guaranteed. An expression lowers to its own operator, construct or application over every constituent, or refuses at the constituent it could not read. A control form is lowered as the whole value only where it IS the value. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: v2 body lowering has no reader that answers a value by searching its subtree for a control form, so an enclosing expression the fold left unlowered refuses instead of being replaced. Owner: bright-boar-848's fold queue (quiet-seal-543, 2026-09-25). The fall-back reader is that lane's subject. Pinned drops, each holding while the drop happens and redding when the repair lands, in `v2.test.claim.namespace_xl0.reference_conservation_accepted_drops`: `a_binary_operand_beside_a_match_is_reported_dropped_holds`, `a_binary_operand_beside_an_if_is_reported_dropped_holds`, `a_record_field_beside_a_match_valued_field_is_reported_dropped_holds`, `a_call_argument_beside_a_match_valued_argument_is_reported_dropped_holds`. The census's clean control, `v2.test.claim.namespace_xl0.reference_conservation` `the_clean_control_conserves_every_authored_atom_holds`, is the neighbour that conserves.", "CLIMBED, THE TRIGGER CAPABILITY MET (bright-boar-848, XL-2). Two links, both in `v2.compiler.body_lowering_fold`. (1) `body_lower_find_control_form_optional` no longer searches a value's subtree: it descends only through what does not change the expression -- a production to its captured child, a sequence whose right side is an empty tail, a lone opening or closing delimiter -- so a control form is lowered as the whole value only where it IS the value, and an enclosing operator, call or record goes whole to the binary/postfix route. (2) That route then exposed the second link: `body_lower_primary_expr` ran its raw-syntax strategy readers over a capture the bottom-up fold had ALREADY lowered (a Match or Branch) and one answered it with its first child, so `t && match w {..}` became `t && w`. Measured by calling `body_lower_value_read` at each production level of the operand: correct at the match_expr node, collapsed from its primary parent up. A primary whose capture is core substrate is now that node, the rule `body_lower_postfix_lowered_primary_optional` already states one level up. The four pinned drops flip to conservation controls (accepted AND the enclosing constituent not dropped), red against the base fold and green after. The label and let-binder atoms that stay absent in the same fixtures are the separately declared NamedArgumentLabel and StatementLetBinder drops. RUNG NOW: structurally guaranteed for the enclosing expression.", + "THE LEFT-OPERAND HALF IS STILL OPEN, and it is valid dag the corpus writes: a block-headed expression as the LEFT operand of a binary operator (`match w {..} && t`, `match w {..} || t`) at expression start. Measured occurrence count 179 (a scan of dag/ and src/v2 for a statement-initial `match .. {` whose closing brace is followed by a `&&`/`||` line); all sit under dag/test, which the native route does not admit into its population, so the native census shows none of them. The seed parser accepts the form and v2 refuses it, so the two parsers disagree on the same source. LOCATED SPECIMEN (gunbc#12758): v2.test.claim.body_lowering.map_literal `ml_the_key_law_names_both_occurrences_holds` is `match map_introduction_duplicate_key(..) { .. } && match .. { .. }`; claim_batch (seed) runs it PASS, and the v2 native route file-refuses src/v2/test/claim/body_lowering/map_literal_test.dag with parse_g0_tokens_remain (WholeFile). Bisected by feeding each top-level declaration to the v2 parser alone: only that declaration refuses. The specimen keeps its spelling as the witness; it is not rewritten around the gap. NEXT-RUNG TRIGGER: the v2 grammar admits a block-headed primary as the left operand of a binary operator, and this specimen's file clears parse on the native route.", ], evidence: [ diff --git a/dag/std/algebra.dag b/dag/std/algebra.dag index 3bb78e5658f..73e19cd5883 100644 --- a/dag/std/algebra.dag +++ b/dag/std/algebra.dag @@ -237,6 +237,30 @@ type FinitelySupportedFunction { size: fn() -> Int } +// THE MAP-LITERAL INTRODUCTION: the declaration a map literal `{ "k": v, .. }` elaborates to, as +// `FreeMonoid` is the one a list literal elaborates to (v2.std.map_introduction carries its head +// path and constructor; docs/plans/map-literal-introduction-design.md). It is NOT a second +// constructor of the carrier: it is the carrier's own insert (the `map_insert` row of +// `finitely_supported_function_templates`) folded over its own empty (the `empty_map` row), in +// authored order. It lives HERE, below `std.types`, because `std.types`' own map literals elaborate +// to it; a home that imports `std.types` (v2.std.collection) would close an import cycle. +// +// The fold's last-write-wins is unobservable on every accepted program: the one writer that builds +// this call (v2.compiler.resolve, the map arm) refuses a repeated key BEFORE it builds it +// (v2.std.map_introduction map_introduction_duplicate_key). A caller that bypasses that writer and +// calls this directly with a repeated key gets insert's semantics, which is what it asked for. +// The result is spelled `Map`, the kernel container spelling this module already uses bare +// (kernel_algebra_profile_value), because the seed types `empty_map()` only under a keyed-collection +// expectation; it names this carrier (std.types Map = FinitelySupportedFunction). +type MapIntroductionEntry { + key: K + value: V +} + +fn map_from_entries(entries: FreeMonoid>) -> Map { + entries |> fold(init: empty_map(), f: (acc, entry) => map_insert(acc, entry.key, entry.value)) +} + // MOVED HERE from `v2.std.collection` by the change that split `PartialFunction`. They are the // total corner of the family above, and leaving them in a different module from their own axis is // where a fork starts. `TotalPolicy` travels with `TotalMap` rather than staying behind: it is the diff --git a/src/v1/stage0/src/std_algebra.rs b/src/v1/stage0/src/std_algebra.rs index 7552cd847b6..2216f510249 100644 --- a/src/v1/stage0/src/std_algebra.rs +++ b/src/v1/stage0/src/std_algebra.rs @@ -305,6 +305,24 @@ pub struct FinitelySupportedFunction { pub _phantom: std::marker::PhantomData<(K, V)>, } +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct MapIntroductionEntry { + pub key: K, + pub value: V, + pub _phantom: std::marker::PhantomData<(K, V)>, +} + +pub fn map_from_entries( + entries: Rc>>>, +) -> Rc> { + entries.iter().cloned().fold( + v1_rt::rc_empty_map::<_, _>(), + |acc: _, entry: Rc>| { + v1_rt::rc_map_insert(acc, entry.key.clone(), entry.value.clone()) + }, + ) +} + #[derive(Clone)] pub struct TotalMap { pub lookup: Rc V>, diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 3cbf4006820..01290d8558e 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -14,6 +14,8 @@ import v2.std.declaration_marker { import std.disposition { Disposition, Scaffold, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } import v2.extdeps.languages.dag { + dag_kernel_string_type_spelling, + dag_string_literal_value_optional, dag_kernel_type_binding_optional, dag_kernel_type_declaration_binding_optional, dag_node_is_float_literal_atom, @@ -27,7 +29,7 @@ import v2.extdeps.languages.dag { qualified_name_from_module_node } import std.algebra { Cons, Empty, FreeMonoid, list_append, list_snoc_item } -import v2.std.algebra { any, fold_list, length } +import v2.std.algebra { any, fold_list, length, skip } import v2.std.collection { Map, PointwisePower, @@ -131,10 +133,16 @@ import v2.std.node { construct_tag_marker, Instantiation, symbol_eq, + symbol_lexeme, + labeled_named_is, well_formed, } import v2.std.type_binder { GenericTypeDecl, PlainTypeDecl, type_decl_view, edge_is_cast_target, edge_is_type_annotation, edge_is_type_params, type_binder_first_mislabelled, type_binder_labels_conform, type_param_names } import v2.std.node_query { + NamedChildAmbiguous, + NamedChildFound, + NamedChildMissing, + named_child_lookup, construct_field_edges, construct_tag_reading, ConstructTagAuthored, @@ -148,6 +156,19 @@ import v2.std.node_query { } import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId } import v2.std.list_introduction { list_introduction_elements_optional, list_introduction_head_path } +import v2.std.map_introduction { + MapIntroductionEntryNodes, + MapIntroductionKeyRepeated, + MapIntroductionKeysDistinct, + MapLiteralEntriesMalformed, + MapLiteralEntriesNone, + MapLiteralEntriesPresent, + map_literal_entries, + map_literal_entries_label, + lower_map_introduction, + map_introduction_duplicate_key, + map_introduction_expected_head_is_map +} // RESOLVE'S OUTPUT IS THE RESOLVED ROOT AND THE INDEX IT WAS RESOLVED AGAINST, one record. A later // stage that needs a reference's declaration asks the SAME authority resolution asked @@ -1826,9 +1847,19 @@ fn resolve_expected_edge(ctx: ResolveContext, e: Edge, x: ResolveExpectation) -> fn resolve_elided_construct_walk(ctx: ResolveContext, n: Node, x: ResolveExpectation) -> ResolveNodeWalk { match resolve_expected_head_path(ctx: ctx, x: x) { - ExpectedHeadAbsent => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_record_expected_type_not_record) + ExpectedHeadAbsent => + if resolve_elided_construct_is_map_literal(n: n) { + resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_expected_type_not_map) + } else { + resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_record_expected_type_not_record) + } ExpectedHeadAliasCycle => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_record_alias_cycle) ExpectedHeadAt { path: path } => + if map_introduction_expected_head_is_map(path: path) { + resolve_map_literal_walk(ctx: ctx, n: n, x: x) + } else if resolve_elided_construct_is_map_literal(n: n) { + resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_expected_type_not_map) + } else { match symbol_index_declared_payload_at(index: ctx.namespace.symbol_index, qualified_path: path) { Present { value: RecordTypePayload } => match construct_tag_optional_edge_target(n: n) { @@ -1845,9 +1876,220 @@ fn resolve_elided_construct_walk(ctx: ResolveContext, n: Node, x: ResolveExpecta } _ => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_record_expected_type_not_record) } + } + } +} + +// THE MAP ARM OF THE ONE ELABORATION WRITER (docs/plans/map-literal-introduction-design.md). A +// headless brace whose authored expected head is, by declaration identity, a Map +// (v2.std.map_introduction map_introduction_expected_head_is_map) elaborates to the one +// introduction v2.std.map_introduction lower_map_introduction builds, or refuses located: +// +// - the expectation must be a closed `Map` instantiation, peeled syntactically; else +// resolve_anonymous_map_expected_type_not_closed at the literal; +// - every item must be string-keyed; a name-keyed brace under a Map head refuses +// resolve_anonymous_map_name_key at its first item; +// - K must be the type a string literal denotes: the kernel text binding an unimported String +// takes (v2.extdeps.languages.dag dag_kernel_type_binding_optional), never a declaration (a K resolving to any declaration -- the structural v2.std.text String +// included -- is a text crossing no route declares here); else +// resolve_anonymous_map_key_kind_mismatch at the first key; +// - no key may repeat, judged by the key type's equality -- for string literals, decoded text +// (the decoder gunbc#12759 lands; until then no key has text and the arm refuses at it) -- through the ONE key law, +// v2.std.map_introduction map_introduction_duplicate_key; a repeat refuses +// resolve_anonymous_map_duplicate_key at its SECOND occurrence. Never last-wins. +// +// Each value is walked under V (the fifth position rule beside #12711's four), so a nested headless +// value elaborates through this same writer; each key is walked as the ordinary child it is. +// Nothing is unified here, and infer still checks every value against V afterwards. +fn resolve_elided_construct_is_map_literal(n: Node) -> Bool { + match map_literal_entries(n: n) { + MapLiteralEntriesNone => false + MapLiteralEntriesPresent { pairs: _ } => true + MapLiteralEntriesMalformed => true + } +} + + +fn resolve_map_literal_walk(ctx: ResolveContext, n: Node, x: ResolveExpectation) -> ResolveNodeWalk { + let type_args = node_positional_child_targets(node: x.expected) + match list_at_optional(xs: type_args, index: 1) { + Absent => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_expected_type_not_closed) + Present { value: key_type } => + match list_at_optional(xs: type_args, index: 2) { + Absent => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_expected_type_not_closed) + Present { value: value_type } => + match resolve_map_first_name_keyed_item(items: skip(xs: n.children, n: 1)) { + Present { value: offending } => resolve_anonymous_record_refused(n: offending, reason: ^resolve_anonymous_map_name_key) + Absent => + match resolve_map_literal_pairs(n: n) { + ResolveMapPairMalformed { at: p } => resolve_anonymous_record_refused(n: p, reason: ^resolve_anonymous_map_entry_malformed) + ResolveMapPairsRead { entries: entries } => + if resolve_map_key_type_is_string_literal_type(ctx: ctx, position: x.position, t: key_type) { + resolve_map_literal_entries(ctx: ctx, n: n, entries: entries, value_x: ResolveExpectation { expected: value_type, position: x.position, at_use_site: x.at_use_site }) + } else { + match list_at_optional(xs: entries, index: 0) { + Present { value: first } => resolve_anonymous_record_refused(n: first.key, reason: ^resolve_anonymous_map_key_kind_mismatch) + Absent => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_key_kind_mismatch) + } + } + } + } + } + } +} + +fn resolve_map_first_name_keyed_item(items: List) -> Optional { + fold(items, init: optional_absent(), f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => if labeled_named_is(x: e, label_of: edge_label_of, wanted: map_literal_entries_label()) { optional_absent() } else { optional_present(value: e.target) } + } + }) +} + +fn resolve_map_key_type_is_string_literal_type(ctx: ResolveContext, position: QualifiedName, t: Node) -> Bool { + match t.kind { + TypeNode { connective: Atom { identity: id } } => + match symbol_index_lexical_lookup(index: ctx.namespace.symbol_index, position: position, name: id) { + LexicalUnbound => + dag_kernel_string_type_spelling(sym: id) && match dag_kernel_type_binding_optional(sym: id) { + Present { value: _ } => true + Absent => false + } + _ => false + } + _ => false + } +} + +// A pair is a tag-elided construct carrying `key` and `value` (body lowering +// body_lower_map_literal_entry_edge); these read them back. +fn resolve_map_entry_field(entry: Node, field: Symbol) -> Optional { + match named_child_lookup(root: entry, name: field) { + NamedChildFound { target: t } => optional_present(value: t) + NamedChildMissing => optional_absent() + NamedChildAmbiguous => optional_absent() + } +} + +// A KEY'S TEXT, OR NONE, read through the ONE string decoder: a string literal lowers to a terminal +// carrying its decoded text (gunbc#12759, v2.extdeps.languages.dag dag_string_literal_value_optional; +// a malformed escape already refused at lowering). A key without that payload has no text, and the +// arm refuses at it rather than compare it -- payload-less keys would all compare equal. +fn resolve_map_key_text_optional(key: Node) -> Optional { + dag_string_literal_value_optional(node: key) +} + +// THE PAIRS, READ TOTALLY. A pair is a tag-elided construct carrying `key` and `value` (body lowering +// body_lower_map_literal_entry_edge). Either every pair carries both, and the entries come back typed +// (key, value, source), or the first pair that does not is named -- never substituted: DESIGN 5 forbids +// a fabricated default, so a missing field is a located refusal +// (resolve_anonymous_map_entry_malformed), however unlikely lowering is to produce one. +type ResolveMapPairs + = ResolveMapPairsRead { entries: List } + | ResolveMapPairMalformed { at: Node } + +fn resolve_map_pairs(pairs: List) -> ResolveMapPairs { + fold(pairs, init: ResolveMapPairsRead { entries: [] }, f: fn(acc, p) { + match acc { + ResolveMapPairMalformed { at: _ } => acc + ResolveMapPairsRead { entries: es } => + match resolve_map_entry_field(entry: p, field: ^key) { + Absent => ResolveMapPairMalformed { at: p } + Present { value: k } => + match resolve_map_entry_field(entry: p, field: ^value) { + Absent => ResolveMapPairMalformed { at: p } + Present { value: v } => + ResolveMapPairsRead { entries: list_snoc_item(xs: es, item: MapIntroductionEntryNodes { key: k, value: v, source: p }) } + } + } + } + }) +} + +fn resolve_map_pair_targets(items: List) -> List { + fold(items, init: [], f: fn(acc, e) { list_snoc_item(xs: acc, item: e.target) }) +} + +// The literal's pairs, read through v2.std.map_introduction map_literal_entries: `{}` has none, and a +// malformed entries carrier refuses at the literal rather than reading as empty. +fn resolve_map_literal_pairs(n: Node) -> ResolveMapPairs { + match map_literal_entries(n: n) { + MapLiteralEntriesNone => ResolveMapPairsRead { entries: [] } + MapLiteralEntriesMalformed => ResolveMapPairMalformed { at: n } + MapLiteralEntriesPresent { pairs: pairs } => resolve_map_pairs(pairs: pairs) + } +} + +// THE KEYS' TEXTS, READ TOTALLY: one text per entry, in order, or the first key with no text, named. +type ResolveMapKeyTexts + = ResolveMapKeyTextsRead { texts: List } + | ResolveMapKeyTextless { at: Node } + +fn resolve_map_key_texts(entries: List) -> ResolveMapKeyTexts { + fold(entries, init: ResolveMapKeyTextsRead { texts: [] }, f: fn(acc, e) { + match acc { + ResolveMapKeyTextless { at: _ } => acc + ResolveMapKeyTextsRead { texts: ts } => + match resolve_map_key_text_optional(key: e.key) { + Present { value: t } => ResolveMapKeyTextsRead { texts: list_snoc_item(xs: ts, item: t) } + Absent => ResolveMapKeyTextless { at: e.key } + } + } + }) +} + +// The key law sees one text per entry, so its indices are entry indices. +// The pairs are walked under a Transform carrier (positional edges only) that never leaves this +// arm; the resolved pairs are read again through resolve_map_pairs, never defaulted. +fn resolve_map_literal_entries(ctx: ResolveContext, n: Node, entries: List, value_x: ResolveExpectation) -> ResolveNodeWalk { + match resolve_map_key_texts(entries: entries) { + ResolveMapKeyTextless { at: key } => resolve_anonymous_record_refused(n: key, reason: ^resolve_anonymous_map_key_text_unavailable) + ResolveMapKeyTextsRead { texts: texts } => + match map_introduction_duplicate_key(keys: texts) { + MapIntroductionKeyRepeated { first_index: _, second_index: second } => + match list_at_optional(xs: entries, index: second) { + Present { value: e } => resolve_anonymous_record_refused(n: e.key, reason: ^resolve_anonymous_map_duplicate_key) + Absent => resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_duplicate_key) + } + MapIntroductionKeysDistinct => + let walked = fold(entries, init: child_walk_init(), f: fn(acc, e) { + child_walk_step(w: acc, e: Edge { label: Positional, target: e.source }, r: resolve_map_entry_walk(ctx: ctx, entry: e.source, value_x: value_x)) + }) + let carrier = node_with_occurrence_id(kind: ComputationNode { behavior: Transform }, children: [], occurrence_id: n.occurrence_id) + match child_walk_node(w: walked, n: carrier) { + ResolveWalkRefused { first: f, rest: r, observation: o } => ResolveWalkRefused { first: f, rest: r, observation: o } + ResolveWalkAccepted { value: resolved, diagnostics: d } => + match resolve_map_pairs(pairs: resolve_map_pair_targets(items: resolved.children)) { + ResolveMapPairMalformed { at: p } => resolve_anonymous_record_refused(n: p, reason: ^resolve_anonymous_map_entry_malformed) + ResolveMapPairsRead { entries: resolved_entries } => + ResolveWalkAccepted { value: lower_map_introduction(entries: resolved_entries, source: n), diagnostics: d } + } + } + } } } +// One entry: its key walked as an ordinary child, its value under V. The pair keeps its elided tag +// edge untouched; it never leaves this arm. +fn resolve_map_entry_walk(ctx: ResolveContext, entry: Node, value_x: ResolveExpectation) -> ResolveNodeWalk { + child_walk_node(n: entry, w: fold(entry.children, init: child_walk_init(), f: fn(acc, e) { + if acc.ordinal == 0 { + child_walk_step(w: acc, e: e, r: ResolveWalkAccepted { value: e.target, diagnostics: None }) + } else { + match e.label { + Named { name: nm } => + if symbol_eq(a: nm, b: ^value) { + child_walk_step(w: acc, e: e, r: resolve_expected_edge(ctx: ctx, e: e, x: value_x)) + } else { + child_walk_step(w: acc, e: e, r: resolve_child_edge(ctx: ctx, e: e)) + } + Positional => child_walk_step(w: acc, e: e, r: resolve_child_edge(ctx: ctx, e: e)) + } + } + })) +} + fn construct_tag_optional_edge_target(n: Node) -> Optional { match list_at_optional(xs: n.children, index: 0) { Present { value: e } => optional_present(value: e.target) @@ -2072,7 +2314,11 @@ fn resolve_node_walk( TypeNode { connective: Conj } => match construct_tag_reading(n: n) { ConstructTagElided => - resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_record_no_expected_type) + if resolve_elided_construct_is_map_literal(n: n) { + resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_map_no_expected_type) + } else { + resolve_anonymous_record_refused(n: n, reason: ^resolve_anonymous_record_no_expected_type) + } ConstructTagAuthored { reference: reference } => resolve_construct_walk(ctx: ctx, n: n, reference: reference, field: fn(e, record) { resolve_record_field_edge(ctx: ctx, e: e, record: record) diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 1443168256f..64b06b486ed 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -77,6 +77,7 @@ import v2.std.compilers.body_lowering { lower_unary_prefix } import v2.std.list_introduction { lower_list_introduction } +import v2.std.map_introduction { map_literal_entries_label, map_literal_entry_label } import v2.std.arrow_signature { anonymous_signature_arrow, declared_signature, signature_order_edge } import v2.std.compilers.sugar { SugarSequencePair, sugar_sequence_pair_optional } import v2.std.grammar { GrammarExpr, GrammarExprFold, fold_grammar_expr } @@ -107,6 +108,8 @@ import v2.std.symbol_index { } import v2.std.node { Arrow, + edge_label_of, + labeled_named_is, is_positional, Atom, Branch, @@ -136,8 +139,10 @@ import v2.std.type_binder { cast_target_edge, type_alias_wrapper, type_decl_wrap import v2.std.node_query { node_positional_child_targets, construct_node, + construct_node_elided, construct_tag_elided_reference, construct_tag_reading, + construct_tag_reading_of_target, ConstructTagAuthored, ConstructTagElided, NotAConstruct, @@ -7932,7 +7937,7 @@ fn body_lower_field_init_edge(item: Node) -> Outcome { d: body_lower_diagnostic(reason: ^body_lowering_reason_field_init_unlowered, n: item) ) if body_lower_field_init_is_string_keyed(item: captured) { - refuse + body_lower_map_literal_entry_edge_from_item(captured: captured, item: item, refuse: refuse) } else { match sugar_sequence_pair_optional(node: captured) { Absent => refuse @@ -7957,6 +7962,101 @@ fn body_lower_field_init_edge(item: Node) -> Outcome { } } +// A STRING-KEYED ITEM `"k": v` (a map literal's entry), recognised by the grammar's own production +// (body_lower_field_init_is_string_keyed, the one reader). Its key is lowered as the VALUE any string +// literal lowers to, never read as a field name, so the key's kind survives to resolve +// (docs/plans/map-literal-introduction-design.md). +fn body_lower_map_literal_entry_edge_from_item(captured: Node, item: Node, refuse: Outcome) -> Outcome { + match sugar_sequence_pair_optional(node: parse_production_captured_child_optional_or_self(node: captured)) { + Absent => refuse + Present { value: pair } => + match body_lower_value_read(value: pair.left) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: key, diagnostics: _ } => body_lower_map_literal_entry_edge(key: key, after_key: pair.right, item: item, refuse: refuse) + } + } +} + +fn parse_production_captured_child_optional_or_self(node: Node) -> Node { + match parse_production_captured_child_optional(node: body_lower_deep_unwrap_optional(node: node)) { + Present { value: c } => c + Absent => node + } +} + +// The entry edge: v2.std.map_introduction map_literal_entry_label, targeting a tag-elided construct +// carrying `key` and `value`. Only resolve's map arm reads it. +fn body_lower_map_literal_entry_edge(key: Node, after_key: Node, item: Node, refuse: Outcome) -> Outcome { + match sugar_sequence_pair_optional(node: after_key) { + Absent => refuse + Present { value: after_colon } => + match body_lower_value_read(value: after_colon.right) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: value, diagnostics: d } => + outcome_with_diagnostics( + value: Edge { + label: Named { name: map_literal_entry_label() }, + target: construct_node_elided( + field_edges: [ + Edge { label: Named { name: ^key }, target: key }, + Edge { label: Named { name: ^value }, target: value } + ], + source: item + ) + }, + diagnostics: d + ) + } + } +} + +// A brace already known to be all string keys (body_lower_brace_key_kinds_refusal_optional ran +// first) carries its pairs on ONE edge, a list literal of them in authored order; any other brace +// is returned as it is. +fn body_lower_map_literal_entries_collapsed(edges: List, source: Node) -> List { + let pairs = fold(edges, init: [], f: fn(acc, e) { + if labeled_named_is(x: e, label_of: edge_label_of, wanted: map_literal_entry_label()) { list_snoc_item(xs: acc, item: e.target) } else { acc } + }) + match pairs { + Empty => edges + Cons { head: _, tail: _ } => + [Edge { label: Named { name: map_literal_entries_label() }, target: lower_list_introduction(elements: pairs, source: source) }] + } +} + +// ONE KIND OF KEY PER BRACE, AND STRING KEYS ONLY WITHOUT A HEAD. Lowering does not choose record or +// map, but it can see a brace no choice could type: a constructor head over string keys +// (`R { "k": v }`), or a headless brace mixing name keys and string keys. Each refuses at the first +// item of the offending kind. +fn body_lower_brace_key_kinds_refusal_optional(reference: Node, edges: List) -> Optional { + let headless = match construct_tag_reading_of_target(target: reference) { + ConstructTagElided => true + ConstructTagAuthored { reference: _ } => false + NotAConstruct => false + } + let first_entry = fold(edges, init: optional_absent(), f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => if labeled_named_is(x: e, label_of: edge_label_of, wanted: map_literal_entry_label()) { optional_present(value: e) } else { optional_absent() } + } + }) + let first_field = fold(edges, init: optional_absent(), f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => if labeled_named_is(x: e, label_of: edge_label_of, wanted: map_literal_entry_label()) { optional_absent() } else { optional_present(value: e) } + } + }) + match first_entry { + Absent => optional_absent() + Present { value: entry } => + if headless { + first_field + } else { + optional_present(value: entry) + } + } +} + // The field items of a brace record body, `{ field_init, .. }`. One reader for both heads: a bare // name's brace suffix (primary_expr) and a dotted chain's final brace suffix // (dag_grammar_postfix_dot_suffix_expr takes the same ident suffix), so the qualified and the @@ -8010,10 +8110,15 @@ fn body_lower_record_construct(reference: Node, items: List, source: Node) }) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: edges, diagnostics: d } => + match body_lower_brace_key_kinds_refusal_optional(reference: reference, edges: edges) { + Present { value: offending } => + outcome_rejected(d: body_lower_diagnostic(reason: ^body_lowering_reason_brace_key_kind_mismatch, n: offending.target)) + Absent => Accepted { - value: construct_node(reference: reference, field_edges: edges, source: source), + value: construct_node(reference: reference, field_edges: body_lower_map_literal_entries_collapsed(edges: edges, source: source), source: source), diagnostics: d } + } } } @@ -8055,8 +8160,8 @@ fn body_lower_record_literal_tag_optional(captured: Node) -> Optional Outcome> { match body_lower_record_brace_items_optional(brace: captured) { Absent => outcome_accepted(value: optional_absent()) diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 07edabdb9c9..6985f4d5807 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -3712,6 +3712,15 @@ fn dag_kernel_type_binding_optional(sym: Symbol) -> Optional { } } +// THE KERNEL SPELLING OF THE TYPE A STRING LITERAL DENOTES: host text, the kernel `String` +// (DESIGN section 4, Ruling 3; ruling neat-boar-16: an unimported String denotes the kernel text +// binding, never std.string_type). It is admitted as a key type only where the kernel table above +// binds it, which it does not yet (the deep-bee-18 lane adds it); a `String` that resolves to a +// declaration is a different type. Consumed by v2.compiler.resolve's map arm (the key-kind rule). +fn dag_kernel_string_type_spelling(sym: Symbol) -> Bool { + symbol_lexeme(sym: sym) == "String" +} + // THE DECLARATIONS A KERNEL TYPE SPELLING DENOTES. A kernel spelling that resolves, through an // import or another module's declaration, to a declaration in this table takes its canonical // binding. Resolving to any other declaration is refused rather than captured diff --git a/src/v2/std/map_introduction.dag b/src/v2/std/map_introduction.dag new file mode 100644 index 00000000000..c0cc9575d69 --- /dev/null +++ b/src/v2/std/map_introduction.dag @@ -0,0 +1,160 @@ +module v2.std.map_introduction + +import std.algebra { list_snoc_item } +import std.types { Map, String } +import v2.std.collection { List, empty_map, map_insert, map_lookup } +import v2.std.optional { Absent, Optional, Present, optional_absent } +import v2.std.integer { Int } +import v2.std.list_introduction { list_introduction_elements_optional, list_introduction_head_path } +import v2.std.logic { Bool } +import v2.std.node { ComputationNode, Edge, Named, Node, Positional, Symbol, Transform, node_with_occurrence_id } +import v2.std.node_query { NamedChildAmbiguous, NamedChildFound, NamedChildMissing, construct_node, named_child_lookup } +import v2.std.qualified_name { QualifiedName, declaration_reference_node } + +// THE MAP-LITERAL INTRODUCTION, ONE AUTHORITY FOR ITS PATHS, ITS CONSTRUCTOR AND ITS KEY LAW +// (docs/plans/map-literal-introduction-design.md). A map literal `{ "k": v, .. }` under an authored +// `Map` is elaborated by v2.compiler.resolve's map arm into ONE ordinary call, +// +// std.algebra.map_from_entries(entries: [std.algebra.MapIntroductionEntry { key: "k", value: v }, ..]) +// +// whose head names the std.algebra declaration exactly as v2.std.list_introduction names +// std.algebra.FreeMonoid. It is a call, not a head with entries as positional children, so infer, +// eval and emit type, evaluate and realize it through the routes they already have for calls, list +// literals and constructs -- no reader arm is added downstream, which is why this module carries no +// reader. The declaration lives in std.algebra, below std.types, because std.types' own map +// literals elaborate to it (an import cycle otherwise). + +// A STRING-KEYED BRACE, as body lowering records it. Each item is first an edge labelled +// map_literal_entry_label targeting a tag-elided `{ key, value }` construct; once the brace is +// known to be all string keys, lowering collapses those items into ONE edge labelled +// map_literal_entries_label whose target is a list literal of the pairs -- one edge, because a +// construct's named edges must be distinct (v2.std.node well_formed). Lowering records the key's +// KIND and chooses nothing; resolve's map arm reads the list. +fn map_literal_entry_label() -> Symbol { + ^map_literal_entry +} + +fn map_literal_entries_label() -> Symbol { + ^map_literal_entries +} + +// THE AUTHORED PAIRS OF A STRING-KEYED BRACE, read totally through the one named-child lookup +// (v2.std.node_query named_child_lookup): no entries edge, exactly one carrying a list literal of +// pairs, or a malformed carrier (two entries edges, or one that is not a list literal) -- which the +// map arm refuses rather than reading as empty. +type MapLiteralEntries + = MapLiteralEntriesNone + | MapLiteralEntriesPresent { pairs: List } + | MapLiteralEntriesMalformed + +fn map_literal_entries(n: Node) -> MapLiteralEntries { + match named_child_lookup(root: n, name: map_literal_entries_label()) { + NamedChildMissing => MapLiteralEntriesNone + NamedChildAmbiguous => MapLiteralEntriesMalformed + NamedChildFound { target: t } => + match list_introduction_elements_optional(node: t) { + Present { value: pairs } => MapLiteralEntriesPresent { pairs: pairs } + Absent => MapLiteralEntriesMalformed + } + } +} + +fn map_introduction_head_path() -> QualifiedName { + [^std, ^algebra, ^map_from_entries] +} + +fn map_introduction_entry_path() -> QualifiedName { + [^std, ^algebra, ^MapIntroductionEntry] +} + +// THE EXPECTED HEADS A MAP LITERAL ELABORATES UNDER, BY DECLARATION IDENTITY: the std.types alias a +// source writes and the carrier it names. Matching a resolved path against this list is identity, +// not alias unfolding; any other head is not a map expectation. +fn map_introduction_expected_head_is_map(path: QualifiedName) -> Bool { + path == [^std, ^types, ^Map] || path == [^std, ^algebra, ^FinitelySupportedFunction] +} + +// THE KEY LAW: the first repeated key, in authored order, as a VALUE -- never a hole, never +// last-wins. `keys` are the entries' keys already reduced to the key type's declared equality (for +// string-literal keys, the decoded text that gunbc#12759's decoder supplies), +// so equal elements are equal keys. One pass over a map from key to its first index: linear. +type MapIntroductionKeys + = MapIntroductionKeysDistinct + | MapIntroductionKeyRepeated { first_index: Int, second_index: Int } + +type MapIntroductionKeyScan { + index: Int + seen: Map + verdict: MapIntroductionKeys +} + +fn map_introduction_duplicate_key(keys: List) -> MapIntroductionKeys { + fold(keys, init: MapIntroductionKeyScan { index: 0, seen: empty_map(), verdict: MapIntroductionKeysDistinct }, f: fn(acc, key) { + match acc.verdict { + MapIntroductionKeyRepeated { first_index: _, second_index: _ } => acc + MapIntroductionKeysDistinct => + match map_lookup(m: acc.seen, key: key) { + Present { value: first } => + MapIntroductionKeyScan { + index: acc.index + 1, + seen: acc.seen, + verdict: MapIntroductionKeyRepeated { first_index: first, second_index: acc.index } + } + Absent => + MapIntroductionKeyScan { + index: acc.index + 1, + seen: map_insert(m: acc.seen, key: key, value: acc.index), + verdict: MapIntroductionKeysDistinct + } + } + } + }).verdict +} + +// One authored entry, its key and value already resolved. +type MapIntroductionEntryNodes { + key: Node + value: Node + source: Node +} + +// The entries argument: the list introduction in its RESOLVED form, its head the declaration +// reference to v2.std.list_introduction's path (the form resolve leaves an authored `[..]` in and +// infer mints for FreeMonoid), since this node is built inside resolve's output. +fn map_introduction_resolved_list(elements: List, source: Node) -> Node { + node_with_occurrence_id( + kind: ComputationNode { behavior: Transform }, + children: fold( + elements, + init: [Edge { label: Positional, target: declaration_reference_node(qn: list_introduction_head_path(), occurrence_id: source.occurrence_id) }], + f: fn(acc, element) { list_snoc_item(xs: acc, item: Edge { label: Positional, target: element }) } + ), + occurrence_id: source.occurrence_id + ) +} + +// THE CONSTRUCTOR: the call above, with the head and entry tag written as declaration references +// (the resolved form), located at the literal. +fn lower_map_introduction(entries: List, source: Node) -> Node { + let entry_nodes = fold(entries, init: [], f: fn(acc, e) { + list_snoc_item( + xs: acc, + item: construct_node( + reference: declaration_reference_node(qn: map_introduction_entry_path(), occurrence_id: e.source.occurrence_id), + field_edges: [ + Edge { label: Named { name: ^key }, target: e.key }, + Edge { label: Named { name: ^value }, target: e.value } + ], + source: e.source + ) + ) + }) + node_with_occurrence_id( + kind: ComputationNode { behavior: Transform }, + children: [ + Edge { label: Positional, target: declaration_reference_node(qn: map_introduction_head_path(), occurrence_id: source.occurrence_id) }, + Edge { label: Named { name: ^entries }, target: map_introduction_resolved_list(elements: entry_nodes, source: source) } + ], + occurrence_id: source.occurrence_id + ) +} diff --git a/src/v2/test/claim/body_lowering/map_literal_test.dag b/src/v2/test/claim/body_lowering/map_literal_test.dag new file mode 100644 index 00000000000..4ba57fe546a --- /dev/null +++ b/src/v2/test/claim/body_lowering/map_literal_test.dag @@ -0,0 +1,313 @@ +module v2.test.claim.body_lowering.map_literal + +import v2.compiler.resolve { ResolvedTree } +import v2.compiler.infer { infer } +import v2.compiler.name_resolve { + Admission, + ResolutionSubject, + resolution_context, + resolve_with_admission_context_policy +} +import v2.std.cross_tree.resolution { source_root_index_empty } +import v2.std.resolution_policy { default_name_resolution_policy } +import v2.compiler.normalized_tree { NormalizedTree } +import v2.compiler.program_assembly { module_roots_from_source_root_ingest } +import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest } +import v2.extdeps.languages.dag { dag_language_model } +import v2.std.artifact { Artifact, SourceFile } +import v2.std.cross_tree.import_model { DagTree } +import v2.std.diagnostic { Accepted, Outcome, Rejected, diagnostics_fatal_reason } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.optional { Absent, Present } +import v2.std.node { Hash, Node, Symbol, content_hash, node_subtree_nodes } +import v2.std.node_query { node_positional_child_targets } +import v2.std.qualified_name { declaration_reference_path_optional, qualified_name_from_dotted_string } +import v2.std.map_introduction { MapIntroductionKeyRepeated, MapIntroductionKeysDistinct, map_introduction_duplicate_key, map_introduction_head_path } +import v2.std.algebra { length } +import v2.std.text { String } +import v2.std.collection { List, list_at_optional } +import std.algebra { Cons, Empty, FreeMonoid, list_snoc_item } +import extdeps.communication.medium { Lossless, Medium } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A MAP LITERAL ELABORATES FROM ITS AUTHORED Map, OR REFUSES LOCATED. +// +// The subject is the map arm of v2.compiler.resolve's one elaboration writer +// (docs/plans/map-literal-introduction-design.md): lowering writes a headless string-keyed brace +// with one map_literal_entries edge, and resolve elaborates it to the one introduction +// v2.std.map_introduction lower_map_introduction builds, or refuses. The oracle is CONTENT EQUALITY +// WITH THE HEADED SPELLING, `map_from_entries(entries: [MapIntroductionEntry { .. }, ..])`, resolved +// through the ordinary call route. +// +// THE SOURCES ARE SUPPLIED AND THE ROUTE IS REAL (tokenize, parse, normalize with body lowering, +// resolve, and infer for control 7). The providers stand in for std.types and std.algebra with +// exactly the declarations the arm matches by identity -- the Map head, its carrier, the entry +// record and the introduction -- because a fixture ingest carries only the modules it is given. The +// real std.types is the inhabitance claim, and it is the native-route census on the PR, not this +// module. +data ml_types_source: String = "module std.types\n\nimport std.algebra { FinitelySupportedFunction }\n\ntype Map = FinitelySupportedFunction\n" + +data ml_algebra_source: String = "module std.algebra\n\ntype FreeMonoid\n = Empty\n | Cons { head: T, tail: FreeMonoid }\n\ntype FinitelySupportedFunction {\n size: Int\n}\n\ntype MapIntroductionEntry {\n key: K\n value: V\n}\n\nfn map_from_entries(entries: FreeMonoid>) -> FinitelySupportedFunction {\n FinitelySupportedFunction { size: 0 }\n}\n" + +// K = String is the KERNEL text binding (ruling, neat-boar-16 via gentle-koi-724): an unimported +// String, not a declaration. It does not bind on the v2 route yet, so every claim below that +// elaborates under Map is an EXPECTED-RED row in gunbc.explicit_witness_admission, owned by +// the deep-bee-18 lane; the name-key and call-argument controls use K = Int and hold today. +data ml_headed_source: String = "module v2.test.ml_headed\n\nimport std.types { Map }\nimport std.algebra { MapIntroductionEntry, map_from_entries }\n\ndata ml_x: Map = map_from_entries(entries: [MapIntroductionEntry { key: \"a\", value: true }, MapIntroductionEntry { key: \"b\", value: false }])\n" + +data ml_headless_source: String = "module v2.test.ml_headless\n\nimport std.types { Map }\n\ndata ml_x: Map = { \"a\": true, \"b\": false }\n" + +// Distinct under the key law although they differ only in case. +data ml_distinct_source: String = "module v2.test.ml_distinct\n\nimport std.types { Map }\n\ndata ml_d: Map = { \"a\": true, \"A\": false }\n" + +data ml_duplicate_source: String = "module v2.test.ml_duplicate\n\nimport std.types { Map }\n\ndata ml_dup: Map = { \"a\": true, \"b\": true, \"a\": false }\n" + +// The same key spelled two ways: the escape `\n` and a raw line feed. Equal by decoded text, so a +// duplicate; a spelling comparison would admit both and let the second silently win. +data ml_escape_duplicate_source: String = "module v2.test.ml_escape_duplicate\n\nimport std.types { Map }\n\ndata ml_esc: Map = { \"a\\nb\": true, \"a\nb\": false }\n" + +data ml_key_kind_source: String = "module v2.test.ml_key_kind\n\nimport std.types { Map }\n\ndata ml_k: Map = { \"k\": true }\n" + +data ml_name_key_source: String = "module v2.test.ml_name_key\n\nimport std.types { Map }\n\ndata ml_n: Map = { k: true }\n" + +data ml_call_argument_source: String = "module v2.test.ml_call_argument\n\nimport std.types { Map }\n\nfn ml_take(m: Map) -> Bool { true }\n\nfn ml_call() -> Bool { ml_take(m: { \"a\": true }) }\n" + +// The discriminating specimen for the infer gap: a generic record and its introduction declared in +// the data declaration's OWN module, so no cross-module declaration is read. It refuses exactly as +// the map introduction does, which places the gap in grounding a generic record construct. +data ml_samemod_source: String = "module v2.test.ml_samemod\n\nimport std.types { Map }\nimport std.algebra { FreeMonoid, FinitelySupportedFunction }\n\ntype LocalEntry {\n key: K\n value: V\n}\n\nfn local_from_entries(entries: FreeMonoid>) -> FinitelySupportedFunction {\n FinitelySupportedFunction { size: 0 }\n}\n\ndata ml_x: Map = local_from_entries(entries: [LocalEntry { key: \"a\", value: 1 }])\n" + +data ml_value_mismatch_source: String = "module v2.test.ml_value_mismatch\n\nimport std.types { Map }\n\ndata ml_bad: Map = { \"a\": 3 }\n" + +// An Int key where K = String: never a map entry, so never admitted. +data ml_int_key_source: String = "module v2.test.ml_int_key\n\nimport std.types { Map }\n\ndata ml_i: Map = { 1: true }\n" + +data ml_int_key_ingest: SourceRootIngest = [ + ml_read(source: ml_types_source, id: ^ml_ik_types_read, unit: ^ml_ik_types_cu, path: "src/v2/test/fixture/map_literal/ik_types.dag"), + ml_read(source: ml_algebra_source, id: ^ml_ik_algebra_read, unit: ^ml_ik_algebra_cu, path: "src/v2/test/fixture/map_literal/ik_algebra.dag"), + ml_read(source: ml_int_key_source, id: ^ml_int_key_read, unit: ^ml_int_key_cu, path: "src/v2/test/fixture/map_literal/int_key.dag") +] + +// Lowering's refusal is its own ingest: a module that fails body lowering fails the whole ingest. +data ml_mixed_source: String = "module v2.test.ml_mixed\n\nimport std.types { Map }\n\ndata ml_m: Map = { \"a\": true, b: false }\n" + +fn ml_read(source: String, id: Symbol, unit: Symbol, path: String) -> DagSourceReadWitness { + DagSourceReadWitness { + source: Medium { carried: source, fidelity: Lossless }, + artifact: Artifact { kind: SourceFile, id: id, file_path: path }, + compilation_unit: unit, + source_root: DagTree + } +} + +data ml_ingest: SourceRootIngest = [ + ml_read(source: ml_types_source, id: ^ml_types_read, unit: ^ml_types_cu, path: "src/v2/test/fixture/map_literal/types.dag"), + ml_read(source: ml_algebra_source, id: ^ml_algebra_read, unit: ^ml_algebra_cu, path: "src/v2/test/fixture/map_literal/algebra.dag"), + ml_read(source: ml_headed_source, id: ^ml_headed_read, unit: ^ml_headed_cu, path: "src/v2/test/fixture/map_literal/headed.dag"), + ml_read(source: ml_headless_source, id: ^ml_headless_read, unit: ^ml_headless_cu, path: "src/v2/test/fixture/map_literal/headless.dag"), + ml_read(source: ml_distinct_source, id: ^ml_distinct_read, unit: ^ml_distinct_cu, path: "src/v2/test/fixture/map_literal/distinct.dag"), + ml_read(source: ml_duplicate_source, id: ^ml_duplicate_read, unit: ^ml_duplicate_cu, path: "src/v2/test/fixture/map_literal/duplicate.dag"), + ml_read(source: ml_escape_duplicate_source, id: ^ml_escape_duplicate_read, unit: ^ml_escape_duplicate_cu, path: "src/v2/test/fixture/map_literal/escape_duplicate.dag"), + ml_read(source: ml_key_kind_source, id: ^ml_key_kind_read, unit: ^ml_key_kind_cu, path: "src/v2/test/fixture/map_literal/key_kind.dag"), + ml_read(source: ml_name_key_source, id: ^ml_name_key_read, unit: ^ml_name_key_cu, path: "src/v2/test/fixture/map_literal/name_key.dag"), + ml_read(source: ml_call_argument_source, id: ^ml_call_argument_read, unit: ^ml_call_argument_cu, path: "src/v2/test/fixture/map_literal/call_argument.dag"), + ml_read(source: ml_samemod_source, id: ^ml_samemod_read, unit: ^ml_samemod_cu, path: "src/v2/test/fixture/map_literal/samemod.dag"), + ml_read(source: ml_value_mismatch_source, id: ^ml_value_mismatch_read, unit: ^ml_value_mismatch_cu, path: "src/v2/test/fixture/map_literal/value_mismatch.dag") +] + +data ml_mixed_ingest: SourceRootIngest = [ + ml_read(source: ml_mixed_source, id: ^ml_mixed_read, unit: ^ml_mixed_cu, path: "src/v2/test/fixture/map_literal/mixed.dag") +] + +// THE FRONT END RUNS ONCE, NOT ONCE PER CLAIM. The fixture ingest and each subject's resolve are +// nullary pure producers, served across witnesses from v2.workflow.floor_pure_producer_share +// floor_cross_claim_pure_producers_warm (the rows beside #12740's anonymous_record producers); every +// claim below only inspects a produced value (DESIGN section 3: a witness discriminates at one +// interface, and the front end is not its subject). +fn ml_fixture_normalized() -> Outcome> { + module_roots_from_source_root_ingest(ingest: ml_ingest, lm: dag_language_model()) +} + +fn ml_resolve_subject(subject: String) -> Outcome { + match ml_fixture_normalized() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: roots, diagnostics: _ } => + resolve_with_admission_context_policy( + context: resolution_context(lm: dag_language_model(), roots: roots), + admission: Admission { + subject: ResolutionSubject { name: qualified_name_from_dotted_string(dotted: subject) }, + imports: Empty + }, + index: source_root_index_empty(), + active_roots: Empty, + policy: default_name_resolution_policy() + ) + } +} + +fn ml_resolved_headed() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_headed") } +fn ml_resolved_headless() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_headless") } +fn ml_resolved_duplicate() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_duplicate") } +fn ml_resolved_escape_duplicate() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_escape_duplicate") } +fn ml_resolved_distinct() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_distinct") } +fn ml_resolved_key_kind() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_key_kind") } +fn ml_resolved_name_key() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_name_key") } +fn ml_resolved_call_argument() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_call_argument") } +fn ml_resolved_value_mismatch() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_value_mismatch") } +fn ml_resolved_samemod() -> Outcome { ml_resolve_subject(subject: "v2.test.ml_samemod") } + +fn ml_infer_verdict_headless() -> Bool { ml_infers(o: ml_resolved_headless()) } +fn ml_infer_verdict_value_mismatch() -> Bool { ml_infers(o: ml_resolved_value_mismatch()) } +fn ml_infer_verdict_samemod() -> Bool { ml_infers(o: ml_resolved_samemod()) } + +fn ml_int_key_verdict_refused() -> Bool { + match module_roots_from_source_root_ingest(ingest: ml_int_key_ingest, lm: dag_language_model()) { + Rejected { diagnostics: _ } => true + Accepted { value: roots, diagnostics: _ } => + match resolve_with_admission_context_policy( + context: resolution_context(lm: dag_language_model(), roots: roots), + admission: Admission { subject: ResolutionSubject { name: qualified_name_from_dotted_string(dotted: "v2.test.ml_int_key") }, imports: Empty }, + index: source_root_index_empty(), + active_roots: Empty, + policy: default_name_resolution_policy() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } + } +} + +fn ml_mixed_normalized() -> Outcome> { + module_roots_from_source_root_ingest(ingest: ml_mixed_ingest, lm: dag_language_model()) +} + +// Every node under the root that is a call headed by the introduction, in tree order. +fn ml_introductions(root: Node) -> List { + fold(node_subtree_nodes(root: root), init: Empty, f: fn(acc, n) { + match list_at_optional(xs: node_positional_child_targets(node: n), index: 0) { + Present { value: head } => + match declaration_reference_path_optional(node: head) { + Present { value: path } => if path == map_introduction_head_path() { list_snoc_item(xs: acc, item: n) } else { acc } + Absent => acc + } + Absent => acc + } + }) +} + +fn ml_introduction_hashes(o: Outcome) -> List { + match o { + Rejected { diagnostics: _ } => Empty + Accepted { value: t, diagnostics: _ } => + fold(ml_introductions(root: t.root), init: Empty, f: fn(acc, n) { list_snoc_item(xs: acc, item: content_hash(n: n)) }) + } +} + +fn ml_refuses_with(o: Outcome, reason: Symbol) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == reason + } +} + +fn ml_accepts(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +// Control 1: the headless literal elaborates to exactly the introduction the headed call spells -- +// one of it, equal by content. +test fn ml_headless_literal_equals_the_headed_introduction_holds() -> Bool { + let headed = ml_introduction_hashes(o: ml_resolved_headed()) + (length(xs: headed) == 1) && (headed == ml_introduction_hashes(o: ml_resolved_headless())) +} + +// Control 2: a repeated key refuses at resolve, never last-wins. +test fn ml_a_duplicate_key_refuses_holds() -> Bool { + ml_refuses_with(o: ml_resolved_duplicate(), reason: ^resolve_anonymous_map_duplicate_key) +} + +// Control 2b: the key law compares DECODED text, so an escape and the scalar it stands for collide. +test fn ml_an_escaped_and_a_raw_key_are_one_key_holds() -> Bool { + ml_refuses_with(o: ml_resolved_escape_duplicate(), reason: ^resolve_anonymous_map_duplicate_key) +} + +// Control 3: distinct keys are accepted and elaborate. +test fn ml_distinct_keys_are_accepted_holds() -> Bool { + length(xs: ml_introduction_hashes(o: ml_resolved_distinct())) == 1 +} + +// The key law itself, as a value: the FIRST repeat, with both occurrences. The mutation this +// discriminates is a law that always answers Distinct -- the fold's last-wins absorbing the repeat -- +// under which this and control 2 go red together. +test fn ml_the_key_law_names_both_occurrences_holds() -> Bool { + match map_introduction_duplicate_key(keys: ["a", "b", "a", "b"]) { + MapIntroductionKeyRepeated { first_index: f, second_index: s } => (f == 0) && (s == 2) + MapIntroductionKeysDistinct => false + } + && match map_introduction_duplicate_key(keys: ["a", "b"]) { + MapIntroductionKeysDistinct => true + MapIntroductionKeyRepeated { first_index: _, second_index: _ } => false + } +} + +// Control 5: K is not the type a string literal denotes, so the key refuses where it is written. +test fn ml_a_key_of_the_wrong_kind_refuses_holds() -> Bool { + ml_refuses_with(o: ml_resolved_key_kind(), reason: ^resolve_anonymous_map_key_kind_mismatch) +} + +test fn ml_a_name_keyed_brace_under_a_map_refuses_holds() -> Bool { + ml_refuses_with(o: ml_resolved_name_key(), reason: ^resolve_anonymous_map_name_key) +} + +// Control 8: the expectation does not leak into a call argument. +test fn ml_a_call_argument_has_no_expected_type_holds() -> Bool { + ml_refuses_with(o: ml_resolved_call_argument(), reason: ^resolve_anonymous_map_no_expected_type) +} + +// Control 7: resolve's choice is not proof. The Int value elaborates (resolve accepts it) and +// infer then refuses it against V = Bool. +test fn ml_infer_refuses_an_elaborated_value_mismatch_holds() -> Bool { + ml_accepts(o: ml_resolved_value_mismatch()) && (ml_infer_verdict_value_mismatch() == false) +} + +// Control 7's positive half: a well-typed elaborated map infers. Measured with #12760 merged: this +// is red for the HEADED spelling too (map_from_entries(entries: [MapIntroductionEntry { .. }]) under +// Map does not infer), so the gap is infer's, not the arm's; its row says so. +test fn ml_an_elaborated_map_infers_holds() -> Bool { + ml_infer_verdict_headless() +} + +// The same-module specimen infers (see ml_samemod_source). +test fn ml_a_same_module_generic_entry_construct_infers_holds() -> Bool { + ml_infer_verdict_samemod() +} + +fn ml_infers(o: Outcome) -> Bool { + match o { + Rejected { diagnostics: _ } => false + Accepted { value: t, diagnostics: _ } => + match infer(tree: t) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } + } +} + +// An Int key under Map is refused somewhere on the route -- at lowering or at resolve -- +// and never elaborates. Were String collapsed onto Int, this is the claim that would go red. +test fn ml_an_int_key_under_a_string_map_refuses_holds() -> Bool { + ml_int_key_verdict_refused() +} + +// Lowering refuses a brace no key-kind choice could type, at the first item of the minority kind. +test fn ml_a_mixed_key_brace_refuses_at_lowering_holds() -> Bool { + match ml_mixed_normalized() { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^body_lowering_reason_brace_key_kind_mismatch + } +} diff --git a/src/v2/workflow/compile_door_cause_ownership.dag b/src/v2/workflow/compile_door_cause_ownership.dag index 8d48e11fd11..aed6189d8ad 100644 --- a/src/v2/workflow/compile_door_cause_ownership.dag +++ b/src/v2/workflow/compile_door_cause_ownership.dag @@ -280,7 +280,61 @@ data known_frontier_causes: List = [ cause: ^resolve_anonymous_record_expected_type_not_record, grain: FatalGrain, lane: SharedSelfHostCriticalPath, - flip_trigger: "a headless record literal whose authored expected type does not resolve, by syntactic peel and the existing lexical lookup, to a single record (v2.std.symbol_index RecordTypePayload): a coproduct with several constructors, a primitive, a type binder, an optional, or a head reached only through alias unfolding resolve does not do. Refused rather than guessed (docs/plans/anonymous-record-literal-design.md, review condition 1). Flips per site when the source writes the constructor head; a Map head is the map arm (gunbc#12734), which takes that population when it lands" + flip_trigger: "a headless record literal whose authored expected type does not resolve, by syntactic peel and the existing lexical lookup, to a single record (v2.std.symbol_index RecordTypePayload): a coproduct with several constructors, a primitive, a type binder, an optional, or a head reached only through alias unfolding resolve does not do. Refused rather than guessed (docs/plans/anonymous-record-literal-design.md, review condition 1). Flips per site when the source writes the constructor head. A Map head is not in this population: it takes the map arm (resolve_anonymous_map_*)" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_no_expected_type, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a headless string-keyed map literal reached by an edge no authored annotation types (a call argument, an unannotated let, a match-arm body), so v2.compiler.resolve's map arm has no Map to elaborate from and refuses rather than guess (docs/plans/map-literal-introduction-design.md). Not a frontier: each occurrence flips when its source writes an annotation" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_expected_type_not_map, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a headless map literal whose authored expected type does not resolve, by declaration identity, to a Map head (v2.std.map_introduction map_introduction_expected_head_is_map): a record, a coproduct, a binder, or a head reached only by alias unfolding resolve does not do. Refused, never guessed; flips per site when the source writes a Map annotation" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_expected_type_not_closed, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a headless map literal under a Map head that is not syntactically a closed Map instantiation, so K and V cannot be peeled without inference. Refused at the literal; flips per site when the annotation writes both type arguments" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_name_key, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a headless brace of NAME keys under an authored Map head: a record literal where a map was declared. Refused at its first item; flips when the source writes string keys or the declared type is corrected" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_key_kind_mismatch, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a map literal whose declared key type K is not the type a string literal denotes (the unbound kernel String, v2.extdeps.languages.dag dag_kernel_string_type_spelling), so a literal key would cross into K with no declared route (DESIGN section 4). Refused at the first key; flips when K is the kernel String or a declared unfold route is written" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_key_text_unavailable, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a map literal key that carries no string-literal lexeme, so the key law has no text to compare: in v2 today every string literal lowers to one class-stamped atom with no payload (gunbc.recurring_failure_mode string_literal_lowers_to_one_class_stamped_atom). Refused at the key rather than compared, since comparing payload-less keys would call every pair a duplicate. A frontier: flips to zero when string literals lower to lexeme-stamped terminals (sleek-owl-120, gunbc#12759)" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_entry_malformed, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a map literal pair that does not carry both its key and its value field, refused at the pair by v2.compiler.resolve's map arm rather than substituting a node for the missing field (DESIGN 5). Body lowering always writes both, so this names a lowering defect if it ever fires; not a frontier, and expected to stay at zero" + }, + CauseOwnership { + cause: ^resolve_anonymous_map_duplicate_key, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a map literal whose keys repeat under the key type's equality (decoded text, via the decoder gunbc#12759 lands), judged by the one key law v2.std.map_introduction map_introduction_duplicate_key and refused at the SECOND occurrence, never last-wins. Not a frontier: each occurrence is a source defect and flips when the repeated entry is removed" + }, + CauseOwnership { + cause: ^body_lowering_reason_brace_key_kind_mismatch, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a brace no key-kind choice could type: a constructor head over string keys, or a headless brace mixing name keys and string keys. Refused at lowering at the first item of the offending kind (docs/plans/map-literal-introduction-design.md); flips per site when the source writes one kind" }, CauseOwnership { cause: ^resolve_anonymous_record_alias_cycle, diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 59fe3a1f371..fc210094f4d 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -1142,6 +1142,22 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.body_lowering.anonymous_record.ar_infer_verdict_value_mismatch_headed", "v2.test.claim.body_lowering.anonymous_record.ar_key_bare_subject", "v2.test.claim.body_lowering.anonymous_record.ar_key_quoted_subject", + "v2.test.claim.body_lowering.map_literal.ml_fixture_normalized", + "v2.test.claim.body_lowering.map_literal.ml_resolved_headed", + "v2.test.claim.body_lowering.map_literal.ml_resolved_headless", + "v2.test.claim.body_lowering.map_literal.ml_resolved_duplicate", + "v2.test.claim.body_lowering.map_literal.ml_resolved_escape_duplicate", + "v2.test.claim.body_lowering.map_literal.ml_resolved_distinct", + "v2.test.claim.body_lowering.map_literal.ml_resolved_key_kind", + "v2.test.claim.body_lowering.map_literal.ml_resolved_name_key", + "v2.test.claim.body_lowering.map_literal.ml_resolved_call_argument", + "v2.test.claim.body_lowering.map_literal.ml_resolved_value_mismatch", + "v2.test.claim.body_lowering.map_literal.ml_resolved_samemod", + "v2.test.claim.body_lowering.map_literal.ml_infer_verdict_headless", + "v2.test.claim.body_lowering.map_literal.ml_infer_verdict_value_mismatch", + "v2.test.claim.body_lowering.map_literal.ml_infer_verdict_samemod", + "v2.test.claim.body_lowering.map_literal.ml_int_key_verdict_refused", + "v2.test.claim.body_lowering.map_literal.ml_mixed_normalized", "v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test.rcf_fixture_normalized", "v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test.rcf_resolved_bad", "v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test.rcf_resolved_good",