From aca776f3dae424c3c1ae94b2e4f23510754b9703 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 10:10:26 +0000 Subject: [PATCH 01/15] v2: coercion admits a refinement-to-declared-carrier cast as Widened A cast from a refinement to its DECLARED carrier (x as Int from x: Pos, type Pos = Int where positive) is admitted as Widened: the declaration's carrier edge composed with the existing exact-structural find_witness. No preservation rule is added (ruling: neat-boar-16). - v2.compiler.infer refinement_declaration: reference -> declaration {path, carrier, where_clause} by the reference's own path down the containment spine; one reader for this cast and the literal-into- refinement producer (shape agreed with quick-crab-850 / deep-bee-18). - v2.std.coercion coercion_cast_crossing takes source_declared_carrier and stays tree-free; a non-carrier target refuses with the original operand mismatch. One step only: Pos2 = Pos where .. widens to Pos, not Int. - body lowering lowers a where-refined head as a type (it rode as the raw parse sequence nothing resolved), so the carrier is resolved and an undeclared carrier now refuses unbound. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../as_cast_has_no_lowered_form.dag | 6 +- src/v2/compiler/04_infer.dag | 98 +++++++++++++++-- src/v2/compiler/body_lowering_fold.dag | 35 ++++-- src/v2/std/coercion.dag | 95 +++++++++++++--- src/v2/test/claim/body_cast_node_test.dag | 102 +++++++++++++++--- .../claim/declaration_graft_assemble_test.dag | 23 +++- 6 files changed, 301 insertions(+), 58 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag b/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag index 1582d1d89f2..fc879f3f57a 100644 --- a/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag +++ b/dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag @@ -14,7 +14,7 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode { "RUNG FOUND AT: mitigated on the operator route; below the floor on the value route (the cast's type was dropped, so `x as Q` was Accepted with `Q` declared nowhere). CEILING: structurally guaranteed -- a cast lowers to a value carrying its operand and its target type, or refuses.", "RUNG NOW: mitigated on EVERY route. `v2.compiler.body_lowering_fold` `body_lower_postfix_expr` refuses a postfix chain carrying an as-suffix with `body_lowering_reason_type_annotation_not_carried` located at the authored target type -- the one reason for a type the lowering cannot carry, shared with the let annotation -- and `body_lower_arm_operand_resolved_optional` declines a cast so a let value or an arm reaches that refusal instead of answering the operand. A declared target refuses too: nothing is carried, so nothing is accepted. As an operator operand the cast now refuses with the same reason, because the postfix is folded before the operator reader sees it. CENSUS: the v2-route identity census over the 321-path population (`v2.compiler.reference_conservation_census` `reference_conservation_stratified_sample_paths` plus six) re-derived by `reference_conservation_census_for_paths` over each arm (pair 620ecb0a50f / 4c9f8d326d3): the modules that newly refuse are data rows casting a literal to a refinement and fn bodies casting to String, each refusing whole, and each returns when the trigger below lands.", "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY (the one the refusal above was retired by): a TYPED CAST NODE -- `e as T` lowers to Transform[coerce, e] with `v2.std.type_binder` `` -> T beside its positional children, and that node is SUFFICIENT FOR: resolve binding T in type role through the shared type-role frame (an undeclared T refusing at T); infer admitting the crossing through `v2.std.coercion` (not `std.coercion` `dag_cast_rules`, which is v1's side of `coercion_two_algebras_answer_one_question_stall`) or refusing typed; and translate and eval realizing it or refusing typed -- on every route, for every cast the refusal now stops.", - "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its carrier (`x as Int` from `x: Pos`) REFUSES, loud and typed at the operand, until `v2.std.coercion` admits a refinement-to-declared-carrier crossing as Widened from the type declaration (its existing widening fold needs per-domain integer value sets); it previously admitted only because an unscoped parameter walk bound x to an unrelated `fn positive(x: Int)`. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.", + "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its DECLARED carrier (`x as Int` from `x: Pos`, `type Pos = Int where positive`) is ADMITTED as Widened: `v2.compiler.infer` `refinement_declaration` reads the carrier from the declaration the reference's path reaches, and `v2.std.coercion` `coercion_cast_crossing` composes that carrier edge with the same exact-structural find_witness -- no preservation rule is added and no predicate is evaluated. Only the declared carrier widens, one step: `x as Bool` from x: Pos, `x as Neg` between two refinements of Int, and `x as Int` from `x: Pos2` (`type Pos2 = Pos where ..`, whose carrier is Pos) all REFUSE at the operand. Residue on that arm: the lowered cast's operator names `CoercionCrossing` by the exact rule (`v2.std.compilers.target_model` `canonical_operation_op_coerce`), fixed at lowering, so a Widened crossing is realized under that identity; both are representation-preserving (`OperandUnchanged`), so no emitted program differs. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.", ], evidence: [ @@ -36,7 +36,9 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode { DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_loop_passes_the_resolver_gate", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_foreign_label_on_a_transform_refuses", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_into_a_refinement_refuses_at_infer", field: WholeDeclaration }, - DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_refuses_until_carrier_widening", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_between_sibling_refinements_refuses", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_identity_cast_into_a_refinement_admits", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "an_as_cast_operand_resolves", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "a_parenthesised_call_operand_resolves", field: WholeDeclaration }, diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index e303f64f807..cdc4617461d 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -2,7 +2,7 @@ module v2.compiler.infer import std.occurrence_identity { OccurrenceSynthetic } import std.kind { Kind, kind_node, roster_member_kind } -import v2.std.algebra { any, Empty, TailAbsent, TailFound, length, list_tail, zip_map } +import v2.std.algebra { any, Empty, TailAbsent, TailFound, fold_list, length, list_tail, zip_map } import std.algebra { Cons, list_snoc_item } import v2.std.bounded_lattice_completeness { infer_bounded_lattice_consumer_gate, @@ -55,7 +55,7 @@ import v2.std.optional { optional_absent, optional_present } -import v2.std.qualified_name { declaration_reference_node, declaration_reference_path_optional } +import v2.std.qualified_name { QualifiedName, declaration_reference_node, declaration_reference_path_optional } import v2.std.compilers.body_lowering { list_introduction_elements_optional, list_introduction_head_path } import v2.std.exact_structural_equality_zip_fold_predicate { exact_structural_equality_zip_fold } import v2.std.constraints { @@ -970,6 +970,78 @@ fn infer_parameter_type_in_scope(tree: Node, reference: Node, binding: Symbol) - } } +// A REFINEMENT DECLARATION, READ FROM A TYPE REFERENCE. `type Pos = Int where positive` is lowered +// (v2.compiler.body_lowering_fold body_lower_type_variant, the head lowered as a type) to +// `Pos: Conj { : Int, +// : clause }` and grafted onto the containment spine at its qualified path +// (v2.compiler.namespace_graft namespace_graft_fold_spine). A resolved reference to it carries that +// path (v2.std.qualified_name declaration_reference_path_optional), so the declaration is reached by +// walking the path's own segments down the spine, never by searching the tree for a matching shape. +// ONE READER, TWO CONSUMERS: v2.std.coercion's declared-carrier widening projects .carrier, and the +// literal-into-refinement cast projects .where_clause into resolve's predicate bindings. Absent when +// the reference is not a declaration reference, the path does not reach a declaration, or the +// declaration carries no where clause (it is then not a refinement, and has no carrier to widen to). +// When the symbol index reaches infer's carriers, the spine walk becomes a lookup in it +// (v2.std.symbol_index symbol_index_entry_at) and this reader keeps its signature. +type RefinementDeclaration { + path: QualifiedName + carrier: Node + where_clause: Node +} + +fn refinement_declaration_spine_step(n: Node, segment: Symbol) -> Optional { + match find_named_child(root: n, name: segment) { + Accepted { value: next, diagnostics: _ } => Present { value: next } + Rejected { diagnostics: _ } => + match find_named_child(root: n, name: ^grammar_production_captured_node_projection) { + Accepted { value: captured, diagnostics: _ } => refinement_declaration_spine_step(n: captured, segment: segment) + Rejected { diagnostics: _ } => Absent + } + } +} + +fn refinement_declaration_at_path(tree: Node, path: QualifiedName) -> Optional { + fold_list(xs: path, empty: Present { value: tree }, cons: fn(at, segment) { + match at { + Present { value: n } => refinement_declaration_spine_step(n: n, segment: segment) + Absent => Absent + } + }) +} + +fn refinement_declaration(tree: Node, reference: Node) -> Optional { + match declaration_reference_path_optional(node: reference) { + Absent => Absent + Present { value: path } => + match refinement_declaration_at_path(tree: tree, path: path) { + Absent => Absent + Present { value: decl } => + match find_named_child(root: decl, name: ^dag_surface_where_refinement_clause) { + Rejected { diagnostics: _ } => Absent + Accepted { value: clause, diagnostics: _ } => + match find_named_child(root: decl, name: ^dag_surface_type_expr) { + Rejected { diagnostics: _ } => Absent + Accepted { value: head, diagnostics: _ } => + Present { + value: RefinementDeclaration { + path: path, + carrier: head, + where_clause: clause + } + } + } + } + } + } +} + +fn refinement_declared_carrier(tree: Node, source_type: Node) -> Optional { + match refinement_declaration(tree: tree, reference: source_type) { + Present { value: d } => Present { value: d.carrier } + Absent => Absent + } +} + // The literal and arrow-domain arms below derive a real type for the operand; the remaining arm // falls through to the operand's own inferred facts. When those facts are the GroundingNotDerived // frontier there is no operand type, and this now refuses (Violates) instead of returning the @@ -2423,7 +2495,7 @@ fn infer_gather_application_row_on_entries( // not derived leaves the check unjudged and the Bind on the counted frontier, as an unannotated Bind // is: the check is neither admitted nor skipped silently. -fn infer_bind_annotation_check(node: Node, entries: List) -> Outcome { +fn infer_bind_annotation_check(node: Node, entries: List, tree: Node) -> Outcome { match type_annotation_optional(n: node) { Absent => outcome_accepted(true) Present { value: annotation } => @@ -2436,7 +2508,12 @@ fn infer_bind_annotation_check(node: Node, entries: List) -> match bound_facts.grounding { GroundingNotDerived { node: _ } => outcome_accepted(true) DerivedGrounding { grounding: g } => - match coercion_cast_crossing(source: g, source_type: g.witness.structural.evidence, target: annotation) { + match coercion_cast_crossing( + source: g, + source_type: g.witness.structural.evidence, + source_declared_carrier: refinement_declared_carrier(tree: tree, source_type: g.witness.structural.evidence), + target: annotation + ) { Accepted { value: _, diagnostics: d } => Accepted { value: true, diagnostics: d } Rejected { diagnostics: r } => Rejected { diagnostics: infer_bind_annotation_refusal(annotation: annotation, cause: r) } @@ -2471,7 +2548,7 @@ fn infer_gather_bind_annotation_row_on_entries( partials: List, tree: Node, ) -> InferGatherFoldAcc { - match infer_bind_annotation_check(node: node, entries: entries) { + match infer_bind_annotation_check(node: node, entries: entries, tree: tree) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2504,7 +2581,7 @@ fn infer_transform_derived_optional( if infer_transform_is_binary_infix_int_add_shape(node: node) { optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, tree: tree)) } else { - infer_transform_cast_optional(node: node, entries: entries) + infer_transform_cast_optional(node: node, entries: entries, tree: tree) } } @@ -2521,7 +2598,7 @@ fn infer_transform_is_cast(node: Node) -> Bool { } } -fn infer_transform_cast_optional(node: Node, entries: List) -> Optional> { +fn infer_transform_cast_optional(node: Node, entries: List, tree: Node) -> Optional> { if !infer_transform_is_cast(node: node) { optional_absent() } else { @@ -2538,7 +2615,12 @@ fn infer_transform_cast_optional(node: Node, entries: List) GroundingNotDerived { node: _ } => optional_absent() DerivedGrounding { grounding: g } => optional_present(value: bind_outcome( - o: coercion_cast_crossing(source: g, source_type: g.witness.structural.evidence, target: target), + o: coercion_cast_crossing( + source: g, + source_type: g.witness.structural.evidence, + source_declared_carrier: refinement_declared_carrier(tree: tree, source_type: g.witness.structural.evidence), + target: target + ), f: fn(crossed) { match infer_descent_witness_for_node(n: node) { Violates { diagnostic: d } => Rejected { diagnostics: diagnostics_singleton(d: d) } diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 1357261152f..80d15df7977 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -951,6 +951,12 @@ fn body_lower_fielded_type_variant(shell: Node, head: Node, payload_shell: Node) } } +// A WHERE-REFINED HEAD IS A TYPE, LOWERED BY THE ONE TYPE-EXPRESSION LOWERING signatures and cast +// targets use (body_lower_type_expr_lowered_optional), so resolve binds the carrier in type role like +// any other type and v2.compiler.infer refinement_declaration reads a resolved carrier. It was carried +// as the raw parse sequence, whose `Int` atom no stage resolved, so the declaration named its carrier +// in a vocabulary nothing else spoke (a cast target `Int` is the kernel binding, the carrier was the +// spelling). A head the lowering cannot read refuses at the head, as an unreadable annotation does. // A variant shell is seq(type_expr, seq(optional(where), optional(payload))). A bare head is left // as parsed: whether `type T = U` names an alias or a one-variant sum is decided where the // alternatives are counted (v2.std.compilers.sugar sugar_fold_coproduct_pipe_chain, the seed's @@ -986,17 +992,24 @@ fn body_lower_type_variant(shell: Node) -> Outcome { Absent => outcome_accepted(value: shell) Present { value: suffix_id } => if suffix_id == ^dag_surface_where_refinement_clause { - outcome_accepted( - value: node_with_occurrence_id( - kind: TypeNode { connective: Conj }, - children: body_lower_type_variant_children_with_where( - base: pair.left, - where_clause: suffixes.left, - fields: suffixes.right - ), - occurrence_id: shell.occurrence_id - ) - ) + match body_lower_type_expr_lowered_optional(node: pair.left) { + Absent => + outcome_rejected( + d: body_lower_diagnostic(reason: ^body_lowering_reason_type_annotation_not_carried, n: pair.left) + ) + Present { value: carrier } => + outcome_accepted( + value: node_with_occurrence_id( + kind: TypeNode { connective: Conj }, + children: body_lower_type_variant_children_with_where( + base: carrier, + where_clause: suffixes.left, + fields: suffixes.right + ), + occurrence_id: shell.occurrence_id + ) + ) + } } else { outcome_accepted(value: shell) } diff --git a/src/v2/std/coercion.dag b/src/v2/std/coercion.dag index ff05a1dcf8b..4ccc4d2ed81 100644 --- a/src/v2/std/coercion.dag +++ b/src/v2/std/coercion.dag @@ -34,6 +34,7 @@ import v2.std.find_witness { UniqueOnly, find_witness, } +import v2.std.optional { Absent, Optional, Present } import v2.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed } import v2.std.refinement_widening_predicate { refinement_widening_is_strict_coarsening } import v2.std.witness { HomomorphismWitness, StructuralPropertyWitness } @@ -354,17 +355,27 @@ fn coercion_fold_exact_structural( // fold's own question with the candidate set fixed by the author -- the singleton {target}, so the // multiplicity is UniqueOnly and no target-selection policy applies -- answered by the same // procedure (find_witness under exact structural equality) and refused with the same typed -// mismatch (coercion_wrap_find_witness_rejection). Only an Identity or Exact crossing is admitted. +// mismatch (coercion_wrap_find_witness_rejection). Exact on the source's own type is Identity or +// Exact. // A TARGET THAT NAMES A REFINEMENT (`NonEmptyStr = String where non_empty`) is structurally equal // only to an operand whose derived type is that same refinement: v2.compiler.infer grounds a // parameter by its enclosing Arrow's declared type, so the identity cast `x as Pos` from `x: Pos` is -// admitted, and a literal cast into Pos refuses (its predicate is not decided here). A cast from a -// refinement to its carrier (`x as Int` from `x: Pos`) also refuses: v2.std.coercion models -// refinement crossings only with a value-set predicate supplied per domain -// (coercion_fold_refinement_widening), so no crossing is admitted by name or by a declared carrier -// alone. This is v2.compiler.infer's authority for `e as T`; the -// name-keyed std.coercion dag_cast_rules is not consulted -// (gunbc.guarantee_stall coercion_two_algebras_answer_one_question_stall). +// admitted, and a literal cast into Pos refuses (its predicate is not decided here). +// A CAST FROM A REFINEMENT TO ITS DECLARED CARRIER (`x as Int` from `x: Pos`, `type Pos = Int where +// positive`) is Widened, and it is TWO FACTS COMPOSED, not a rule: the declaration's own carrier edge +// (every Pos value is an Int by declaration, so no predicate is evaluated and no value set is needed) +// and then the SAME exact-structural find_witness from that carrier to the target. The caller reads +// the carrier from the declaration (v2.compiler.infer refinement_declaration) and hands it in as +// source_declared_carrier, so this module stays tree-free. It is not a second widening algebra beside +// v2.std.refinement_widening_predicate: that rule answers value-set containment between two domains; +// this one judges nothing but structural equality, which find_witness already owns, so no +// preservation rule is added. ONE STEP ONLY: the carrier of `type Pos2 = Pos where q` is Pos, so +// `x as Pos` from `x: Pos2` is Widened and `x as Int` REFUSES -- the carrier edge is not walked to a +// fixed point (a walk would need its own termination argument over the declaration graph, and one +// step is the whole of what the declaration states). A target that is not the declared carrier +// refuses with the ORIGINAL mismatch located at the operand, so the widening arm never changes what a +// refusal says. This is v2.compiler.infer's authority for `e as T`; the name-keyed std.coercion +// dag_cast_rules is not consulted (gunbc.guarantee_stall coercion_two_algebras_answer_one_question_stall). fn coercion_cast_target_singleton(target: Node) -> CandidateSet { CandidateSet { candidates: [target], @@ -372,10 +383,8 @@ fn coercion_cast_target_singleton(target: Node) -> CandidateSet { } } -// source is the operand's grounding (its node is the operand, where a refusal is located) and -// source_type the type that grounding established. -fn coercion_cast_crossing(source: CanonicalGrounding, source_type: Node, target: Node) -> Outcome { - match find_witness( +fn coercion_cast_exact_witness(source_type: Node, target: Node) -> Outcome { + find_witness( source_facts: source_type, candidates: coercion_cast_target_singleton(target: target), predicate: PreservationPredicate { @@ -383,7 +392,57 @@ fn coercion_cast_crossing(source: CanonicalGrounding, source_type: Node, target: preservation_rule: ^preservation_rule_exact_structural_equality_zip_fold }, multiplicity_policy: UniqueOnly - ) { + ) +} + +fn coercion_cast_refused(source: CanonicalGrounding, upstream: NonEmptyDiagnostics) -> Outcome { + match coercion_wrap_find_witness_rejection(source: source, upstream: upstream) { + Accepted { value: wrapped, diagnostics: _ } => Rejected { diagnostics: wrapped } + Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r } + } +} + +// The Widened arm, reached only after the exact crossing on the source's own type refused; its own +// refusal is discarded for the original one, which is the mismatch the author wrote. +fn coercion_cast_to_declared_carrier( + source: CanonicalGrounding, + source_declared_carrier: Optional, + target: Node, + exact_refusal: NonEmptyDiagnostics, +) -> Outcome { + match source_declared_carrier { + Absent => coercion_cast_refused(source: source, upstream: exact_refusal) + Present { value: carrier } => + match coercion_cast_exact_witness(source_type: carrier, target: target) { + Accepted { value: fw, diagnostics: fw_d } => + Accepted { + value: CoercionResult { + target: fw.candidate, + quality: Widened, + witness: CoercionWitness { + homomorphism: HomomorphismWitness { + rule: ^homomorphism_rule_refinement_declared_carrier, + evidence: coercion_homomorphism_evidence(source: source, fw: fw) + } + } + }, + diagnostics: fw_d + } + Rejected { diagnostics: _ } => coercion_cast_refused(source: source, upstream: exact_refusal) + } + } +} + +// source is the operand's grounding (its node is the operand, where a refusal is located), +// source_type the type that grounding established, and source_declared_carrier the carrier its +// refinement declaration states (Absent when source_type is not a refinement). +fn coercion_cast_crossing( + source: CanonicalGrounding, + source_type: Node, + source_declared_carrier: Optional, + target: Node, +) -> Outcome { + match coercion_cast_exact_witness(source_type: source_type, target: target) { Accepted { value: fw, diagnostics: fw_d } => Accepted { value: CoercionResult { @@ -399,10 +458,12 @@ fn coercion_cast_crossing(source: CanonicalGrounding, source_type: Node, target: diagnostics: fw_d } Rejected { diagnostics: r } => - match coercion_wrap_find_witness_rejection(source: source, upstream: r) { - Accepted { value: wrapped, diagnostics: _ } => Rejected { diagnostics: wrapped } - Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r } - } + coercion_cast_to_declared_carrier( + source: source, + source_declared_carrier: source_declared_carrier, + target: target, + exact_refusal: r + ) } } diff --git a/src/v2/test/claim/body_cast_node_test.dag b/src/v2/test/claim/body_cast_node_test.dag index afb7058f290..7fb14262268 100644 --- a/src/v2/test/claim/body_cast_node_test.dag +++ b/src/v2/test/claim/body_cast_node_test.dag @@ -1,16 +1,17 @@ module v2.test.claim.body_cast_node import std.algebra { Cons, Empty, list_snoc_item } -import v2.std.coercion { NoTargetCandidate } +import v2.std.coercion { CoercionQuality, NoTargetCandidate, Widened, coercion_cast_crossing } import std.occurrence_identity { OccurrenceSynthetic } import v2.test.claim.type_param_binder_frame { tpb_accepts, tpb_assemble, tpb_refuses_with } import v2.compiler.emit { emit } import v2.compiler.eval { eval, inputs_root_only } -import v2.compiler.infer { InferredFacts, InferredTree, infer } +import v2.compiler.infer { InferredFacts, InferredTree, infer, refinement_declaration } import v2.extdeps.languages.dag { dag_arrow_domain_conj_node, dag_arrow_with_body_node, dag_int_literal_node_from_lexeme, dag_type_atom_node } import v2.extdeps.languages.rust_test { rust_binop_target_model_staging } import v2.extdeps.runtimes.v2_evaluator { v2_evaluator_interpretation } -import v2.test.lens_common.infer_fixture { claim_inferred_facts_from_nodes } +import v2.test.lens_common.infer_fixture { claim_canonical_grounding, claim_inferred_facts_from_nodes } +import v2.std.qualified_name { QualifiedName, declaration_reference_node } import v2.std.cardinality { termination_proof_witness_for_node } import v2.std.compilers.target_model { canonical_operation_op_coerce, target_model_canonical_operation_wire_node } import v2.std.collection { List } @@ -117,6 +118,53 @@ fn bcn_out_of_refinement() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Int {\n x as Int\n}\n") } +fn bcn_refinement_of_refinement_as_int() -> Outcome { + tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Pos2 = Pos where positive\n\nfn f(x: Pos2) -> Int {\n x as Int\n}\n") +} + +fn bcn_refinement_of_refinement_as_its_carrier() -> Outcome { + tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Pos2 = Pos where positive\n\nfn f(x: Pos2) -> Pos {\n x as Pos\n}\n") +} + +fn bcn_sibling_refinement_cast() -> Outcome { + tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Neg = Int where positive\n\nfn f(x: Pos) -> Neg {\n x as Neg\n}\n") +} + +fn bcn_is_widened(q: Optional) -> Bool { + match q { + Present { value: Widened } => true + Present { value: _ } => false + Absent => false + } +} + +// The crossing's quality, from the real assembled tree: the refinement declaration the reference's +// path reaches, and the tree's one cast target. Absent when the tree refuses, the reader finds no +// refinement, the tree does not carry exactly one cast, or the crossing refuses. +fn bcn_crossing_quality(o: Outcome, reference_path: QualifiedName) -> Optional { + match o { + Rejected { diagnostics: _ } => Absent + Accepted { value: root, diagnostics: _ } => + match bcn_cast_targets(n: root) { + Cons { head: target, tail: Empty } => + match refinement_declaration(tree: root, reference: declaration_reference_node(qn: reference_path, occurrence_id: OccurrenceSynthetic)) { + Absent => Absent + Present { value: decl } => + match coercion_cast_crossing( + source: claim_canonical_grounding(type_symbol: ^bcn_refinement_operand, algebra_symbol: ^bcn_refinement_operand), + source_type: declaration_reference_node(qn: reference_path, occurrence_id: OccurrenceSynthetic), + source_declared_carrier: Present { value: decl.carrier }, + target: target + ) { + Accepted { value: crossed, diagnostics: _ } => Present { value: crossed.quality } + Rejected { diagnostics: _ } => Absent + } + } + _ => Absent + } + } +} + fn bcn_refinement_param_as_bool() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Bool {\n x as Bool\n}\n") } @@ -437,17 +485,7 @@ fn bcn_refused_with_mismatch(o: Outcome) -> Bool { } } -// (15) THE CAST OUT OF A REFINEMENT REFUSES, STATED. A parameter is now bound by its ENCLOSING -// Arrow (v2.compiler.infer infer_parameter_type_in_scope), so `x` in `fn f(x: Pos)` grounds as the -// Pos declaration-reference, and Pos is not structurally Int: coercion_cast_crossing refuses with -// its typed mismatch. RED BEFORE: on main at 21f4d0c this row ADMITTED, by the wrong route -- the -// unscoped parameter walk bound f's `x` to the unrelated `fn positive(x: Int)`, and the crossing was -// Int to Int. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: v2.std.coercion admitting a cast from a -// refinement to its DECLARED carrier as Widened, decided from the type declaration; the existing -// coercion_fold_refinement_widening cannot carry it because its predicate needs per-domain integer -// value sets (v2.std.refinement_widening_predicate refinement_widening_value_sets_hold). When that -// lands this row flips to an accepting control asserting the Widened quality. The partner `x as Bool` -// refuses under both groundings. +// A refusal located at the cast's OPERAND (not at the `as` keyword), with coercion's typed mismatch. fn bcn_refused_with_mismatch_at_operand(o: Outcome) -> Bool { match o { Accepted { value: _, diagnostics: _ } => false @@ -465,9 +503,40 @@ fn bcn_operand_mismatch(x: Diagnostic) -> Bool { } } -test fn bcn_cast_out_of_a_refinement_refuses_until_carrier_widening() -> Bool { +// (15) THE CAST OUT OF A REFINEMENT TO ITS DECLARED CARRIER IS ADMITTED, WIDENED. `x as Int` from +// `x: Pos` (`type Pos = Int where positive`): infer admits it on the production route, and the +// crossing's quality is Widened -- read by v2.compiler.infer refinement_declaration from the SAME +// assembled tree (the declaration reached by the reference's own path) and judged by +// v2.std.coercion coercion_cast_crossing against the SAME tree's cast target. RED BEFORE (main at +// 980761c838): infer refused NoTargetCandidate at the operand, because coercion judged only exact +// structural equality and Pos is not structurally Int. The route is asserted, not only the verdict: +// the quality is Widened, not Exact, so an admission through some other rule cannot green this row. +test fn bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens() -> Bool { + match bcn_out_of_refinement_inferred() { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: _ } => + bcn_is_widened(q: bcn_crossing_quality(o: bcn_out_of_refinement(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos, tail: Empty } })) + } +} + +// (15b) THE WIDENING IS THE DECLARED CARRIER ONLY. `x as Bool` from x: Pos refuses (Bool is not Pos's +// carrier). ONE STEP, PINNED: `type Pos2 = Pos where positive` declares Pos as its carrier, so `x as +// Pos` from x: Pos2 is Widened and `x as Int` REFUSES at the operand -- the carrier edge is not walked +// to a fixed point (v2.std.coercion states why). +test fn bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses() -> Bool { bcn_refused_with_mismatch(o: bcn_refinement_param_as_bool_inferred()) - && bcn_refused_with_mismatch_at_operand(o: bcn_out_of_refinement_inferred()) + && bcn_refused_with_mismatch_at_operand(o: bcn_infers(o: bcn_refinement_of_refinement_as_int())) + && match bcn_infers(o: bcn_refinement_of_refinement_as_its_carrier()) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } + && bcn_is_widened(q: bcn_crossing_quality(o: bcn_refinement_of_refinement_as_its_carrier(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos2, tail: Empty } })) +} + +// (15c) A SIBLING REFINEMENT OVER THE SAME CARRIER IS NOT A CARRIER. `x as Neg` from x: Pos, where +// both are `Int where ...`: sharing a carrier admits nothing, so the cast refuses at the operand. +test fn bcn_cast_between_sibling_refinements_refuses() -> Bool { + bcn_refused_with_mismatch_at_operand(o: bcn_infers(o: bcn_sibling_refinement_cast())) } // (16) THE IDENTITY CAST INTO A REFINEMENT IS ADMITTED BY THE EXACT RULE. `x as Pos` from `x: Pos`: @@ -511,3 +580,4 @@ test fn bcn_a_foreign_label_on_a_transform_refuses() -> Bool { ] )) } + diff --git a/src/v2/test/claim/declaration_graft_assemble_test.dag b/src/v2/test/claim/declaration_graft_assemble_test.dag index 9017de0a047..57f07684421 100644 --- a/src/v2/test/claim/declaration_graft_assemble_test.dag +++ b/src/v2/test/claim/declaration_graft_assemble_test.dag @@ -120,13 +120,14 @@ fn declaration_graft_atom_present(root: Node, lexeme: String) -> Bool { // fn-only, type-only, where-alias-only) are the containment-spine controls (gunbc#11694) // and stay separate, as do the three record sources (once refusing; now the Named controls of // the record spelling, see the bottom of this module). -data src_combined: String = "module p\n\nimport v2.std.logic { Bool }\n\ntype Flag = On | Off\ntype Name = String where brand(\"Name\")\nfn f(x: Int) -> Int { x }\nfn dag_user(x: Int) -> Int { x }\nfn g(q: Flag) -> Flag { q }\nfn h() -> Flag { On }\nfn flip(q: Flag) -> Flag { match q { On => Off } }\nfn b() -> Bool { true }\n" -data src_alias_spelled_as_emitted_id: String = "module p\n\ntype dag_surface_type_expr = String where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" -data src_alias_spelled_as_production_name: String = "module p\n\ntype dag_production_type_decl = String where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" +data src_combined: String = "module p\n\nimport v2.std.logic { Bool }\n\ntype Flag = On | Off\ntype Name = Int where brand(\"Name\")\nfn f(x: Int) -> Int { x }\nfn dag_user(x: Int) -> Int { x }\nfn g(q: Flag) -> Flag { q }\nfn h() -> Flag { On }\nfn flip(q: Flag) -> Flag { match q { On => Off } }\nfn b() -> Bool { true }\n" +data src_alias_spelled_as_emitted_id: String = "module p\n\ntype dag_surface_type_expr = Int where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" +data src_alias_spelled_as_production_name: String = "module p\n\ntype dag_production_type_decl = Int where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" data src_empty: String = "module p\n" data src_fn_only: String = "module p\n\nfn f(x: Int) -> Int { x }\n" data src_type_only: String = "module p\n\ntype Flag = On | Off\n" -data src_where_alias_only: String = "module p\n\ntype Name = String where brand(\"Name\")\n" +data src_where_alias_only: String = "module p\n\ntype Name = Int where brand(\"Name\")\n" +data src_where_alias_undeclared_carrier: String = "module p\n\ntype Name = Undeclared where brand(\"Name\")\n" data src_record_construct: String = "module p\n\ntype Rec { n: Int }\nfn mk() -> Rec { Rec { n: 1 } }\n" data src_record_type_only: String = "module p\n\ntype Rec { n: Int }\n" data src_flag_and_rec: String = "module p\n\ntype Flag = On | Off\ntype Rec { n: Int }\n" @@ -185,6 +186,20 @@ test fn declaration_graft_where_alias_accepts() -> Bool { declaration_graft_accepts(out: declaration_graft_where_alias_only_assembled()) } +// A WHERE-ALIAS'S CARRIER IS A RESOLVED TYPE. Body lowering lowers the refined head as a type +// (v2.compiler.body_lowering_fold body_lower_type_variant), so resolve binds it and a carrier nothing +// declares refuses unbound. RED BEFORE: the head rode as the raw parse sequence no stage resolved, so +// `Undeclared where ..` ASSEMBLED -- the declaration named its carrier in a vocabulary nothing checked +// (and this module's own fixtures carried an unimported `String` that way; they now carry Int). +test fn declaration_graft_where_alias_over_an_undeclared_carrier_refuses() -> Bool { + match declaration_graft_assemble_for(src: src_where_alias_undeclared_carrier) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => + (d.head.reason == ^resolve_reason_unbound_symbol) + || fold(d.tail, init: false, f: fn(acc, x) { acc || (x.reason == ^resolve_reason_unbound_symbol) }) + } +} + test fn declaration_graft_combined_accepts() -> Bool { declaration_graft_accepts(out: declaration_graft_combined_assembled()) } From 415fdb7bc2cbbb13b0fac32654912b98ac43c900 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 10:42:13 +0000 Subject: [PATCH 02/15] infer: RefinementDeclaration drops unconsumed path; where_clause named as a declared frontier (review 71764) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index cdc4617461d..3602d02d271 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -977,14 +977,18 @@ fn infer_parameter_type_in_scope(tree: Node, reference: Node, binding: Symbol) - // (v2.compiler.namespace_graft namespace_graft_fold_spine). A resolved reference to it carries that // path (v2.std.qualified_name declaration_reference_path_optional), so the declaration is reached by // walking the path's own segments down the spine, never by searching the tree for a matching shape. -// ONE READER, TWO CONSUMERS: v2.std.coercion's declared-carrier widening projects .carrier, and the -// literal-into-refinement cast projects .where_clause into resolve's predicate bindings. Absent when +// CONSUMERS. .carrier is consumed in this change: refinement_declared_carrier hands it to +// v2.std.coercion coercion_cast_crossing, the declared-carrier widening. .where_clause is a DECLARED +// FRONTIER, not yet consumed: its consumer is the literal-into-refinement cast arm of work item +// adhoc-032c89dc-138 (deep-bee-18), which projects it into resolve's where-predicate bindings. That arm +// lands with the next-rung trigger of gunbc.recurring_failure_mode as_cast_has_no_lowered_form +// (v2.std.coercion deciding a refinement's predicate on the cast operand), and it reads the clause +// here rather than finding the declaration a second time. Absent when // the reference is not a declaration reference, the path does not reach a declaration, or the // declaration carries no where clause (it is then not a refinement, and has no carrier to widen to). // When the symbol index reaches infer's carriers, the spine walk becomes a lookup in it // (v2.std.symbol_index symbol_index_entry_at) and this reader keeps its signature. type RefinementDeclaration { - path: QualifiedName carrier: Node where_clause: Node } @@ -1024,7 +1028,6 @@ fn refinement_declaration(tree: Node, reference: Node) -> Optional Present { value: RefinementDeclaration { - path: path, carrier: head, where_clause: clause } From 59e14d6443bed15a15fbff77df80f32fbf518660 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 11:47:36 +0000 Subject: [PATCH 03/15] body_cast_node: 15b/15c supply values at coercion's interface; drop the over-budget assembly rows Floor refused three new witnesses over the 72300 eval-step new-witness budget (no claim failed). The refusal logic lives in v2.std.coercion, so 15b/15c now supply the reference, declared carrier and target there (2652 / 2015 steps); row 15 stays the inhabitance claim on the production route. The undeclared-carrier assembly row is dropped: row 15 is the lowering change's discriminating red (an unlowered head cannot widen). Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/test/claim/body_cast_node_test.dag | 72 ++++++++++++------- .../claim/declaration_graft_assemble_test.dag | 15 ---- 2 files changed, 45 insertions(+), 42 deletions(-) diff --git a/src/v2/test/claim/body_cast_node_test.dag b/src/v2/test/claim/body_cast_node_test.dag index 7fb14262268..dbbb9947452 100644 --- a/src/v2/test/claim/body_cast_node_test.dag +++ b/src/v2/test/claim/body_cast_node_test.dag @@ -1,7 +1,7 @@ module v2.test.claim.body_cast_node import std.algebra { Cons, Empty, list_snoc_item } -import v2.std.coercion { CoercionQuality, NoTargetCandidate, Widened, coercion_cast_crossing } +import v2.std.coercion { CoercionQuality, CoercionResult, NoTargetCandidate, Widened, coercion_cast_crossing } import std.occurrence_identity { OccurrenceSynthetic } import v2.test.claim.type_param_binder_frame { tpb_accepts, tpb_assemble, tpb_refuses_with } import v2.compiler.emit { emit } @@ -118,18 +118,6 @@ fn bcn_out_of_refinement() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Int {\n x as Int\n}\n") } -fn bcn_refinement_of_refinement_as_int() -> Outcome { - tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Pos2 = Pos where positive\n\nfn f(x: Pos2) -> Int {\n x as Int\n}\n") -} - -fn bcn_refinement_of_refinement_as_its_carrier() -> Outcome { - tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Pos2 = Pos where positive\n\nfn f(x: Pos2) -> Pos {\n x as Pos\n}\n") -} - -fn bcn_sibling_refinement_cast() -> Outcome { - tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ntype Neg = Int where positive\n\nfn f(x: Pos) -> Neg {\n x as Neg\n}\n") -} - fn bcn_is_widened(q: Optional) -> Bool { match q { Present { value: Widened } => true @@ -519,24 +507,54 @@ test fn bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens() -> Bool { } } -// (15b) THE WIDENING IS THE DECLARED CARRIER ONLY. `x as Bool` from x: Pos refuses (Bool is not Pos's -// carrier). ONE STEP, PINNED: `type Pos2 = Pos where positive` declares Pos as its carrier, so `x as -// Pos` from x: Pos2 is Widened and `x as Int` REFUSES at the operand -- the carrier edge is not walked -// to a fixed point (v2.std.coercion states why). +// (15b)/(15c) ONLY THE DECLARED CARRIER WIDENS -- at v2.std.coercion's interface, with SUPPLIED +// values (DESIGN section 3, a witness discriminates at one interface): the source is a refinement's +// declaration reference, its declared carrier the node refinement_declaration returns, the target the +// cast's. Row (15) is the inhabitance claim that pairs them: on the production route the reader +// returns the kernel Int atom as Pos's carrier and it meets the tree's own cast target, so the Int +// atom supplied here is the shape the real producer emits. Row (16)'s partner keeps `x as Bool` from +// x: Pos refusing on the production route. +fn bcn_int_type() -> Node { dag_type_atom_node(identity: ^dag_binding_type_int) } +fn bcn_bool_type() -> Node { dag_type_atom_node(identity: ^dag_binding_type_bool) } +fn bcn_ref(leaf: Symbol) -> Node { + declaration_reference_node(qn: Cons { head: ^p, tail: Cons { head: leaf, tail: Empty } }, occurrence_id: OccurrenceSynthetic) +} +fn bcn_supplied_crossing(source_leaf: Symbol, carrier: Node, target: Node) -> Outcome { + coercion_cast_crossing( + source: claim_canonical_grounding(type_symbol: ^bcn_refinement_operand, algebra_symbol: ^bcn_refinement_operand), + source_type: bcn_ref(leaf: source_leaf), + source_declared_carrier: Present { value: carrier }, + target: target + ) +} +fn bcn_supplied_refuses(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => bcn_has_reason(d: d, reason: discriminant(v: NoTargetCandidate)) + } +} +fn bcn_supplied_quality(o: Outcome) -> Optional { + match o { + Accepted { value: crossed, diagnostics: _ } => Present { value: crossed.quality } + Rejected { diagnostics: _ } => Absent + } +} + +// (15b) A TARGET THAT IS NOT THE DECLARED CARRIER REFUSES, AND THE CARRIER EDGE IS ONE STEP. +// `x as Bool` from x: Pos (carrier Int) refuses. `type Pos2 = Pos where ..` declares Pos as its +// carrier, so `x as Pos` from x: Pos2 is Widened and `x as Int` REFUSES -- the edge is not walked to +// a fixed point (v2.std.coercion states why). RED if the widening arm admitted any target, or walked +// the carrier chain. test fn bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses() -> Bool { - bcn_refused_with_mismatch(o: bcn_refinement_param_as_bool_inferred()) - && bcn_refused_with_mismatch_at_operand(o: bcn_infers(o: bcn_refinement_of_refinement_as_int())) - && match bcn_infers(o: bcn_refinement_of_refinement_as_its_carrier()) { - Accepted { value: _, diagnostics: _ } => true - Rejected { diagnostics: _ } => false - } - && bcn_is_widened(q: bcn_crossing_quality(o: bcn_refinement_of_refinement_as_its_carrier(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos2, tail: Empty } })) + bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos, carrier: bcn_int_type(), target: bcn_bool_type())) + && bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos2, carrier: bcn_ref(leaf: ^Pos), target: bcn_int_type())) + && bcn_is_widened(q: bcn_supplied_quality(o: bcn_supplied_crossing(source_leaf: ^Pos2, carrier: bcn_ref(leaf: ^Pos), target: bcn_ref(leaf: ^Pos)))) } -// (15c) A SIBLING REFINEMENT OVER THE SAME CARRIER IS NOT A CARRIER. `x as Neg` from x: Pos, where -// both are `Int where ...`: sharing a carrier admits nothing, so the cast refuses at the operand. +// (15c) A SIBLING REFINEMENT OVER THE SAME CARRIER IS NOT A CARRIER: `x as Neg` from x: Pos, both +// `Int where ..`, refuses. RED if sharing a carrier admitted a crossing between refinements. test fn bcn_cast_between_sibling_refinements_refuses() -> Bool { - bcn_refused_with_mismatch_at_operand(o: bcn_infers(o: bcn_sibling_refinement_cast())) + bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos, carrier: bcn_int_type(), target: bcn_ref(leaf: ^Neg))) } // (16) THE IDENTITY CAST INTO A REFINEMENT IS ADMITTED BY THE EXACT RULE. `x as Pos` from `x: Pos`: diff --git a/src/v2/test/claim/declaration_graft_assemble_test.dag b/src/v2/test/claim/declaration_graft_assemble_test.dag index 57f07684421..2e114e341e6 100644 --- a/src/v2/test/claim/declaration_graft_assemble_test.dag +++ b/src/v2/test/claim/declaration_graft_assemble_test.dag @@ -127,7 +127,6 @@ data src_empty: String = "module p\n" data src_fn_only: String = "module p\n\nfn f(x: Int) -> Int { x }\n" data src_type_only: String = "module p\n\ntype Flag = On | Off\n" data src_where_alias_only: String = "module p\n\ntype Name = Int where brand(\"Name\")\n" -data src_where_alias_undeclared_carrier: String = "module p\n\ntype Name = Undeclared where brand(\"Name\")\n" data src_record_construct: String = "module p\n\ntype Rec { n: Int }\nfn mk() -> Rec { Rec { n: 1 } }\n" data src_record_type_only: String = "module p\n\ntype Rec { n: Int }\n" data src_flag_and_rec: String = "module p\n\ntype Flag = On | Off\ntype Rec { n: Int }\n" @@ -186,20 +185,6 @@ test fn declaration_graft_where_alias_accepts() -> Bool { declaration_graft_accepts(out: declaration_graft_where_alias_only_assembled()) } -// A WHERE-ALIAS'S CARRIER IS A RESOLVED TYPE. Body lowering lowers the refined head as a type -// (v2.compiler.body_lowering_fold body_lower_type_variant), so resolve binds it and a carrier nothing -// declares refuses unbound. RED BEFORE: the head rode as the raw parse sequence no stage resolved, so -// `Undeclared where ..` ASSEMBLED -- the declaration named its carrier in a vocabulary nothing checked -// (and this module's own fixtures carried an unimported `String` that way; they now carry Int). -test fn declaration_graft_where_alias_over_an_undeclared_carrier_refuses() -> Bool { - match declaration_graft_assemble_for(src: src_where_alias_undeclared_carrier) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: d } => - (d.head.reason == ^resolve_reason_unbound_symbol) - || fold(d.tail, init: false, f: fn(acc, x) { acc || (x.reason == ^resolve_reason_unbound_symbol) }) - } -} - test fn declaration_graft_combined_accepts() -> Bool { declaration_graft_accepts(out: declaration_graft_combined_assembled()) } From 03342a3647e2bf7e9d1ff5f1e29c2b2b7be6275e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 16:30:20 +0000 Subject: [PATCH 04/15] v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted; cut every consumer root-first Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/00_compile.dag | 19 +++- src/v2/compiler/03_ingest.dag | 10 +- src/v2/compiler/03_name_resolve.dag | 25 +++-- src/v2/compiler/03_resolve.dag | 39 ++++++-- src/v2/compiler/04_infer.dag | 6 +- src/v2/compiler/ingested_fixture_arrows.dag | 7 +- src/v2/compiler/program_assembly.dag | 7 +- .../self_host/candidate_generation.dag | 3 +- .../candidate_generation_stage_verdicts.dag | 5 +- .../compiler/self_host/closure_emission.dag | 17 ++-- .../self_host/compiler_closure_emit.dag | 3 +- .../self_host/direct_rust_door_fixture.dag | 3 +- src/v2/compiler/source_authority.dag | 10 +- src/v2/compiler/staged_front_end.dag | 8 +- src/v2/test/claim/body_cast_node_test.dag | 47 ++++----- .../test/claim/body_let_annotation_test.dag | 20 ++-- .../arrow_body_form_witness_test.dag | 2 +- ...transform_binary_infix_witness_helpers.dag | 5 +- ...er_transform_binary_infix_witness_test.dag | 3 +- .../wave1_gate1_normalize_add_helpers.dag | 2 +- .../body_type_annotation_refusal_test.dag | 13 +-- .../compile_eval_thesis_proof_test.dag | 4 +- ...tion_argument_inhabitance_witness_test.dag | 25 ++--- .../data_decl_lowering_grounding_test.dag | 7 +- .../infer_atom_grounding_rules_test.dag | 5 +- .../infer_product_introduction_test.dag | 5 +- .../long/add_arrow_eval_by_execution_test.dag | 2 +- ...lassical_not_ingested_equals_eval_test.dag | 12 +-- ...ndidate_generation_stage_verdicts_test.dag | 3 +- .../self_host_candidate_generation_test.dag | 3 +- .../claim/infer_list_introduction_test.dag | 11 ++- .../claim/infer_self_grounding_wall_test.dag | 11 ++- ...bitant_neutralization_e2e_witness_test.dag | 5 +- .../parser_completeness_frontier_test.dag | 2 +- .../self_host_module_emit_derisk_test.dag | 4 +- .../test/claim/loop_infer_iteration_test.dag | 2 +- .../branch_infer_fail_open_audit_test.dag | 7 +- .../manual/branch_infer_if_then_else_test.dag | 5 +- .../test/claim/manual/branch_infer_test.dag | 2 +- ...language_add_python_to_typescript_test.dag | 5 +- ...unded_lattice_completeness_anchor_test.dag | 3 +- .../manual/infer_emit_compile_anchor.dag | 2 +- src/v2/test/claim/manual/infer_ground_add.dag | 7 +- .../test/claim/manual/ingest_bridge_test.dag | 5 +- .../manual/inhabitant_neutralization_test.dag | 9 +- .../match_infer_fail_open_audit_test.dag | 15 +-- .../one_member_cost_probe_test.dag | 4 +- .../test/claim/refinement_discharge_test.dag | 5 +- .../translate_underived_refusal_test.dag | 7 +- .../claim/type_param_binder_frame_test.dag | 96 ++++++++++--------- .../test/compiler/pipeline/stage_bridge.dag | 5 +- ...ecting_lens_blocks_before_compile_test.dag | 3 +- src/v2/test/lens_common/infer_fixture.dag | 10 ++ .../hollow_alias_nested_rejected_test.dag | 4 +- ...w_alias_vtc_empty_lenses_rejected_test.dag | 4 +- src/v2/workflow/dag_acceptance.dag | 5 +- src/v2/workflow/realization_attempt.dag | 10 +- 57 files changed, 334 insertions(+), 234 deletions(-) diff --git a/src/v2/compiler/00_compile.dag b/src/v2/compiler/00_compile.dag index 6137d4f2e13..fe68e4522f3 100644 --- a/src/v2/compiler/00_compile.dag +++ b/src/v2/compiler/00_compile.dag @@ -86,6 +86,7 @@ import v2.compiler.normalized_tree { NormalizedTree } import v2.compiler.parse { parse, prepare_grammar, PreparedGrammar } import v2.compiler.resolve { ObservationComplete, + ObservationIncomplete, ObservationCompleteness, ResolveNodeWalk, ResolveWalkAccepted, @@ -869,7 +870,7 @@ fn compile_inferred( } fn compile( - source: CoreNode, + source: ResolvedTree, mode: CompileMode ) -> Outcome { bind_outcome( @@ -928,7 +929,7 @@ fn validated_from_compile_output( // registration at this door, no wording here may claim it would be caught (DESIGN sections 4b(1), // 4b(2), 5). fn validate_then_compile( - source: CoreNode, + source: ResolvedTree, lenses: List, mode: CompileMode ) -> Outcome> { @@ -3120,6 +3121,9 @@ type NativeModuleResolveVerdict } | NativeModuleResolveAccepted { resolved: ResolvedTree } +// The walk ran under context.resolution's index (resolve_walk_with_admission_context_policy +// builds the subject namespace over it), so that index is minted beside the root. An +// accepted walk implies an accepted context; the Rejected arm states the refusal it would be. fn native_module_resolve_verdict( context: NativeTestContext, refusal_index: Map, @@ -3136,7 +3140,16 @@ fn native_module_resolve_verdict( ResolveWalkRefused { first: f, rest: r, observation: o } => NativeModuleResolveRefused { first: f, rest: r, observation: o } ResolveWalkAccepted { value: resolved, diagnostics: _ } => - NativeModuleResolveAccepted { resolved: resolved } + match context.resolution { + Accepted { value: shared, diagnostics: _ } => + NativeModuleResolveAccepted { resolved: ResolvedTree { root: resolved, symbol_index: shared.symbol_index } } + Rejected { diagnostics: r } => + NativeModuleResolveRefused { + first: r, + rest: [], + observation: ObservationIncomplete { reason: ^resolve_observation_context_refused } + } + } } } } diff --git a/src/v2/compiler/03_ingest.dag b/src/v2/compiler/03_ingest.dag index 1658e91eea2..2d25aeec2cd 100644 --- a/src/v2/compiler/03_ingest.dag +++ b/src/v2/compiler/03_ingest.dag @@ -1,5 +1,7 @@ module v2.compiler.ingest +import v2.compiler.resolve { ResolvedTree } +import v2.std.symbol_index { empty_symbol_index } import v2.compiler.refinement_discharge { infer_and_discharge } import std.algebra { Empty, list_append } import v2.std.collection { @@ -310,12 +312,15 @@ fn parse_tree_to_emitted_node(parse_tree: ParseTree, source_model: TargetModel) ) } +// The bridge infers the emitted node directly: it never passed through resolve, so it is +// supplied with an index that holds no declarations (a declaration lookup through it finds +// nothing and refuses, never fabricates one). fn parse_tree_to_target_model_bridge(parse_tree: ParseTree, source_model: TargetModel) -> Outcome { bind_outcome( o: parse_tree_to_emitted_node(parse_tree: parse_tree, source_model: source_model), f: fn(emitted) { bind_outcome( - o: infer_and_discharge(tree: emitted), + o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index() }), f: fn(inferred) { bind_outcome( o: coerce_grounded_node(source: emitted, tree: inferred, target: source_model), @@ -327,6 +332,7 @@ fn parse_tree_to_target_model_bridge(parse_tree: ParseTree, source_model: Target ) } +// Not resolved either (neutralized from the bridge's core): no declarations indexed. fn cross_language_compile( parse_tree: ParseTree, source_model: TargetModel, @@ -339,7 +345,7 @@ fn cross_language_compile( o: neutralize_core_for_target(core: core, target: target_model), f: fn(neutralized) { bind_outcome( - o: infer_and_discharge(tree: neutralized), + o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index() }), f: fn(inferred) { emit(tree: inferred, target: target_model) } diff --git a/src/v2/compiler/03_name_resolve.dag b/src/v2/compiler/03_name_resolve.dag index 6dc41c50b8c..901457715a4 100644 --- a/src/v2/compiler/03_name_resolve.dag +++ b/src/v2/compiler/03_name_resolve.dag @@ -14,7 +14,7 @@ import v2.compiler.resolve { ResolveNodeWalk, ResolveWalkRefused, ResolvedTree, - resolve_walk_outcome, + resolved_tree_outcome, resolve_walk_prefix_pending, resolve_walk_with_namespace_policy, try_edge_declared_binding @@ -772,6 +772,8 @@ fn resolve_with_admission_policy( ) } +// The admitted namespace is built over the context's own index (namespace_for_subject_in_context), +// so that index is the one this resolution consulted. A refused context resolved nothing. fn resolve_with_admission_context_policy( context: Outcome, admission: Admission, @@ -779,13 +781,20 @@ fn resolve_with_admission_context_policy( active_roots: FreeMonoid, policy: NameResolutionPolicy ) -> Outcome { - resolve_walk_outcome(w: resolve_walk_with_admission_context_policy( - context: context, - admission: admission, - index: index, - active_roots: active_roots, - policy: policy - )) + match context { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: shared, diagnostics: _ } => + resolved_tree_outcome( + w: resolve_walk_with_admission_context_policy( + context: context, + admission: admission, + index: index, + active_roots: active_roots, + policy: policy + ), + symbol_index: shared.symbol_index + ) + } } // THE SUBJECT'S WHOLE RESOLUTION OBSERVATION, every independent failure chain in walk order. The diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 45b1023f974..396474b6398 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -121,7 +121,20 @@ import v2.std.node_query { } import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId } -type ResolvedTree = Node +// 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 +// (v2.std.symbol_index symbol_index_lookup) instead of reconstructing it from the tree: the index is +// the Namespace.symbol_index the walk ran under, minted beside the root on the Accepted arm only, so +// a refusal carries no index and no stage can read one for a tree that did not resolve. +// CONSUMERS: .root is read by every stage after resolve (infer's gather reads it at its entry). +// .symbol_index is a DECLARED FRONTIER in this change: its consumer is gunbc#12407, which stacks on +// it -- v2.compiler.infer refinement_declaration asks symbol_index_lookup for a refinement +// declaration a cast operand's type references (the declared-carrier widening), replacing an +// infer-private walk over the tree. +type ResolvedTree { + root: Node + symbol_index: SymbolIndex +} // `test_code`, `declared_in` and `imported_origins` exist for one decision: whether a reference binds // to test code (owner ruling 2026-09-16/17). Root-scope bindings come from exactly two sources: the @@ -1083,6 +1096,15 @@ fn resolve_walk_outcome(w: ResolveNodeWalk) -> Outcome { } } +// The stage exit: the same projection, with the index resolution consulted minted beside the root. +fn resolved_tree_outcome(w: ResolveNodeWalk, symbol_index: SymbolIndex) -> Outcome { + match w { + ResolveWalkAccepted { value: v, diagnostics: d } => + Accepted { value: ResolvedTree { root: v, symbol_index: symbol_index }, diagnostics: d } + ResolveWalkRefused { first: f, rest: _, observation: _ } => Rejected { diagnostics: f } + } +} + // PENDING ADVISORIES STAY WITH THEIR OWN FATAL. A refused child's chains arrive intact; the walk // prefixes the advisories accepted siblings raised SINCE THE PREVIOUS REFUSAL onto the child's // first chain only, then resets them. So every advisory lands in at most one chain, the one whose @@ -1857,12 +1879,15 @@ fn resolve_with_namespace_policy( lm: LanguageModel, policy: NameResolutionPolicy ) -> Outcome { - resolve_walk_outcome(w: resolve_walk_with_namespace_policy( - tree: tree, - namespace: namespace, - lm: lm, - policy: policy - )) + resolved_tree_outcome( + w: resolve_walk_with_namespace_policy( + tree: tree, + namespace: namespace, + lm: lm, + policy: policy + ), + symbol_index: namespace.symbol_index + ) } fn resolve_walk_with_namespace_policy( diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index e303f64f807..263c4224ea9 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -3078,9 +3078,9 @@ fn infer_grounding_admits_infer_facts(grounding: CanonicalGrounding) -> Bool { } fn infer_entries_for_tree(tree: ResolvedTree) -> Outcome> { - let partials = partial_bounded_lattice_instances_in_tree(tree: tree) + let partials = partial_bounded_lattice_instances_in_tree(tree: tree.root) infer_gather_acc_to_outcome( - acc: fold_node(n: tree, algebra: infer_gather_fold_algebra(partials: partials, tree: tree)) + acc: fold_node(n: tree.root, algebra: infer_gather_fold_algebra(partials: partials, tree: tree.root)) ) } // INFER'S OUTPUT IS THE OBLIGATED FORM, never an InferredTree: v2.compiler.refinement_discharge @@ -3096,7 +3096,7 @@ fn infer(tree: ResolvedTree) -> Outcome { Accepted { value: facts_map, diagnostics: md } => Accepted { value: ObligatedInferredTree { - root: tree, + root: tree.root, facts: facts_map, obligations: Empty }, diff --git a/src/v2/compiler/ingested_fixture_arrows.dag b/src/v2/compiler/ingested_fixture_arrows.dag index 361884805ec..609906faae5 100644 --- a/src/v2/compiler/ingested_fixture_arrows.dag +++ b/src/v2/compiler/ingested_fixture_arrows.dag @@ -1,6 +1,7 @@ module v2.compiler.ingested_fixture_arrows import v2.compiler.staged_front_end { front_end_run_outcome, run_front_end } +import v2.compiler.resolve { ResolvedTree } import v2.std.optional { Absent, Optional, @@ -87,7 +88,7 @@ fn ingested_find_arrow_in_module(root: Node) -> Optional { // second route, and has no order of its own to drift from the one it projects — which is the whole // reason the front end moved rather than being copied (DESIGN section 3). -fn ingested_resolved_module_from_source(source: String, file: Symbol) -> Outcome { +fn ingested_resolved_module_from_source(source: String, file: Symbol) -> Outcome { front_end_run_outcome(run: run_front_end(source: source, file: file)) } @@ -95,7 +96,7 @@ fn ingested_arrow_from_source(source: String, file: Symbol) -> Outcome { bind_outcome( o: ingested_resolved_module_from_source(source: source, file: file), f: fn(resolved) { - match ingested_find_arrow_in_module(root: resolved) { + match ingested_find_arrow_in_module(root: resolved.root) { Present { value: arrow } => if well_formed(n: arrow) { outcome_accepted(value: arrow) @@ -111,7 +112,7 @@ fn ingested_arrow_from_source(source: String, file: Symbol) -> Outcome { outcome_rejected( d: ingested_fixture_diagnostic( reason: ^ingested_fixture_reason_arrow_missing, - n: resolved + n: resolved.root ) ) } diff --git a/src/v2/compiler/program_assembly.dag b/src/v2/compiler/program_assembly.dag index 718b99191db..ba5ada26f9e 100644 --- a/src/v2/compiler/program_assembly.dag +++ b/src/v2/compiler/program_assembly.dag @@ -22,6 +22,7 @@ import v2.compiler.parse { import v2.std.compilers.lexing { TokenStream, token_stream_remaining_count } import v2.std.integer { Int } import v2.compiler.normalize { normalize } +import v2.compiler.resolve { ResolvedTree } import v2.compiler.name_resolve { Admission, resolve_with_admission, @@ -525,7 +526,7 @@ fn assemble_program_from_module_roots( roots: FreeMonoid, admission: Admission, lm: LanguageModel -) -> Outcome { +) -> Outcome { bind_outcome( o: validate_module_roots(roots: roots), f: fn(validated_roots) { @@ -552,7 +553,7 @@ fn assemble_program_from_module_roots( // renderer degrades to "no file" instead of to a wrong file. type IngestAssembly { spans: SpanIndex, - program: Outcome + program: Outcome } fn assemble_program_from_ingest_located( @@ -586,7 +587,7 @@ fn assemble_program_from_ingest( ingest: SourceRootIngest, admission: Admission, lm: LanguageModel -) -> Outcome { +) -> Outcome { assemble_program_from_ingest_located( ingest: ingest, admission: admission, diff --git a/src/v2/compiler/self_host/candidate_generation.dag b/src/v2/compiler/self_host/candidate_generation.dag index b5051eca170..04234e75ff4 100644 --- a/src/v2/compiler/self_host/candidate_generation.dag +++ b/src/v2/compiler/self_host/candidate_generation.dag @@ -1,5 +1,6 @@ module v2.compiler.self_host.candidate_generation +import v2.compiler.resolve { ResolvedTree } import extdeps.communication.medium { Medium } import extdeps.filesystem.filesystem_io { Filesystem } import v2.compiler.emit { emit } @@ -142,7 +143,7 @@ fn generate_stage_candidate_from_ingest( } fn generate_translate_self_emit_candidate( - resolved_module: Node, + resolved_module: ResolvedTree, dag_target: TargetModel ) -> Outcome { bind_outcome( diff --git a/src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag b/src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag index 15e22d6e89c..c6afc65aab5 100644 --- a/src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag +++ b/src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag @@ -1,5 +1,6 @@ module v2.compiler.self_host.candidate_generation_stage_verdicts +import v2.compiler.resolve { ResolvedTree } import v2.compiler.infer { infer } import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } import v2.std.algebra { Cons, Empty, fold_list } @@ -77,7 +78,7 @@ fn diagnostics_carried_reasons(d: Diagnostics) -> List { } fn candidate_generation_composition_verdicts( - resolved_module: Node, + resolved_module: ResolvedTree, dag_target: TargetModel, infer_verdict: Symbol, infer_carried_reasons: List @@ -104,7 +105,7 @@ fn candidate_generation_composition_verdicts( } fn candidate_generation_stage_verdicts( - resolved_module: Node, + resolved_module: ResolvedTree, dag_target: TargetModel ) -> CandidateGenerationStageVerdicts { match infer(tree: resolved_module) { diff --git a/src/v2/compiler/self_host/closure_emission.dag b/src/v2/compiler/self_host/closure_emission.dag index 657ab49d6a8..fab196e05ac 100644 --- a/src/v2/compiler/self_host/closure_emission.dag +++ b/src/v2/compiler/self_host/closure_emission.dag @@ -37,7 +37,7 @@ import v2.compiler.reference_closure { reference_closure_neighbours, reference_derived_closure } -import v2.compiler.resolve { ResolveWalkAccepted, ResolveWalkRefused } +import v2.compiler.resolve { ResolvedTree, resolved_tree_outcome } import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest, @@ -327,20 +327,17 @@ fn closure_resolve_member( symbol_index: SymbolIndex, index: SourceRootIndex, active_roots: FreeMonoid -) -> Outcome { +) -> Outcome { bind_outcome( o: validate_module_roots(roots: Cons { head: tree, tail: Empty }), f: fn(validated) { - match resolve_walk_with_admission_context_policy( + resolved_tree_outcome(w: resolve_walk_with_admission_context_policy( context: outcome_accepted(value: ResolutionContext { lm: lm, roots: validated, symbol_index: symbol_index }), admission: Admission { subject: ResolutionSubject { name: member_module }, imports: Empty }, index: index, active_roots: active_roots, policy: default_name_resolution_policy() - ) { - ResolveWalkRefused { first: f, rest: _, observation: _ } => Rejected { diagnostics: f } - ResolveWalkAccepted { value: resolved, diagnostics: _ } => outcome_accepted(value: resolved) - } + ), symbol_index: symbol_index) } ) } @@ -373,7 +370,7 @@ fn closure_member_for_fold( ), f: fn(resolved) { outcome_accepted(value: ReferenceClosureMember { - resolved: resolved, + resolved: resolved.root, import_targets: fold_list(xs: tree.import_bindings, empty: Empty, cons: fn(acc, row) { list_snoc_item(xs: acc, item: row.target) }), @@ -431,7 +428,7 @@ fn closure_member_emission( ), f: fn(resolved) { match reference_closure_neighbours( - member: ReferenceClosureMember { resolved: resolved, import_targets: visit.member.import_targets, payload: true }, + member: ReferenceClosureMember { resolved: resolved.root, import_targets: visit.member.import_targets, payload: true }, roster: roster ) { ReferenceClosureTargetOwnerless { target: _, at: at } => @@ -452,7 +449,7 @@ fn closure_member_emission( } else { outcome_rejected(d: closure_emission_diagnostic( reason: ^closure_emission_member_reaches_outside_closure, - at: resolved + at: resolved.root )) } } diff --git a/src/v2/compiler/self_host/compiler_closure_emit.dag b/src/v2/compiler/self_host/compiler_closure_emit.dag index 05f5ba33564..5d779aa612d 100644 --- a/src/v2/compiler/self_host/compiler_closure_emit.dag +++ b/src/v2/compiler/self_host/compiler_closure_emit.dag @@ -4,6 +4,7 @@ import v2.compiler.refinement_discharge { infer_and_discharge } import std.dissolution { DissolutionCondition, unbound_dissolution } import std.types { NonEmptyStr } import v2.compiler.name_resolve { Admission } +import v2.compiler.resolve { ResolvedTree } import v2.compiler.program_assembly { assemble_program_from_ingest_located } import v2.compiler.program_partition { emit_for_target } import v2.compiler.source_authority { SourceRootIngest } @@ -137,7 +138,7 @@ fn emit_compiler_import_closure_from_ingest_located( } fn emit_compiler_import_closure_from_assembled( - program: Outcome, + program: Outcome, target: TargetModel ) -> Outcome { bind_outcome( diff --git a/src/v2/compiler/self_host/direct_rust_door_fixture.dag b/src/v2/compiler/self_host/direct_rust_door_fixture.dag index 9a586f2f8ce..297db5ddb0d 100644 --- a/src/v2/compiler/self_host/direct_rust_door_fixture.dag +++ b/src/v2/compiler/self_host/direct_rust_door_fixture.dag @@ -25,6 +25,7 @@ import v2.extdeps.languages.rust { rust_target_model } import v2.compiler.name_resolve { Admission, ResolutionSubject } +import v2.compiler.resolve { ResolvedTree } import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest } import std.algebra { Cons, Empty } import v2.std.artifact { Artifact, SourceFile } @@ -108,7 +109,7 @@ fn direct_rust_door_admission() -> Admission { // nullary and warm-enrolled in `v2.workflow.floor_pure_producer_share` // (floor_cross_claim_pure_producers_warm), which carries the measured recompute/sharing/serve // case; the required floor forces it during strict preparation, outside every per-claim budget. -fn direct_rust_door_specimen_resolved() -> Outcome { +fn direct_rust_door_specimen_resolved() -> Outcome { assemble_program_from_ingest( ingest: direct_rust_door_ingest(), admission: direct_rust_door_admission(), diff --git a/src/v2/compiler/source_authority.dag b/src/v2/compiler/source_authority.dag index 568b1231b25..98fd7e3fa30 100644 --- a/src/v2/compiler/source_authority.dag +++ b/src/v2/compiler/source_authority.dag @@ -1299,7 +1299,7 @@ fn semantic_ir_equal_witness( original: DagSemanticIr, reparsed: DagSemanticIr ) -> Witness { - if source_authority_node_equal(left: original.tree, right: reparsed.tree) { + if source_authority_node_equal(left: original.tree.root, right: reparsed.tree.root) { Holds { value: SemanticIrEqual { original: original, reparsed: reparsed } } } else { Violates { @@ -1423,13 +1423,13 @@ fn source_authority_round_trip_with_model( bind_outcome( o: target_serialize_source_from_model( target: canonical_source_target, - emitted: original_ir.tree + emitted: original_ir.tree.root ), f: fn(canonical_source) { bind_outcome( o: target_serialize_source_from_model( target: canonical_source_target, - emitted: original_ir.tree + emitted: original_ir.tree.root ), f: fn(canonical_source_again) { bind_outcome( @@ -1495,13 +1495,13 @@ fn canonical_dag_source_parse_print_law( bind_outcome( o: target_serialize_source_from_model( target: canonical_source_target, - emitted: original_ir.tree + emitted: original_ir.tree.root ), f: fn(canonical_source) { bind_outcome( o: target_serialize_source_from_model( target: canonical_source_target, - emitted: original_ir.tree + emitted: original_ir.tree.root ), f: fn(canonical_source_again) { bind_outcome( diff --git a/src/v2/compiler/staged_front_end.dag b/src/v2/compiler/staged_front_end.dag index c7d054d7f96..9e87db8126e 100644 --- a/src/v2/compiler/staged_front_end.dag +++ b/src/v2/compiler/staged_front_end.dag @@ -2,7 +2,7 @@ module v2.compiler.staged_front_end import v2.compiler.normalize { normalize } import v2.compiler.parse { parse_module } -import v2.compiler.resolve { resolve } +import v2.compiler.resolve { ResolvedTree, resolve } import v2.compiler.tokenize { tokenize } import v2.extdeps.languages.dag { dag_language_model } import std.algebra { list_snoc_item } @@ -71,7 +71,7 @@ type FrontEndStageStep } type FrontEndCompletion - = FrontEndResolvedModule { resolved: Node } + = FrontEndResolvedModule { resolved: ResolvedTree } | FrontEndRefused | FrontEndBoundReached { last: FrontEndStage } @@ -259,7 +259,7 @@ fn front_end_resolve_step( steps: front_end_passed( steps: steps, stage: FrontEndResolve, - receipt: ResolvedModule { node_count: node_subtree_count(n: resolved) }, + receipt: ResolvedModule { node_count: node_subtree_count(n: resolved.root) }, diagnostics: d ), completion: FrontEndResolvedModule { resolved: resolved } @@ -290,7 +290,7 @@ fn front_end_first_refusal(steps: List) -> Optional Outcome { +fn front_end_run_outcome(run: FrontEndRun) -> Outcome { match front_end_first_refusal(steps: run.steps) { Present { value: r } => Rejected { diff --git a/src/v2/test/claim/body_cast_node_test.dag b/src/v2/test/claim/body_cast_node_test.dag index afb7058f290..b6aaac609c0 100644 --- a/src/v2/test/claim/body_cast_node_test.dag +++ b/src/v2/test/claim/body_cast_node_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.body_cast_node +import v2.compiler.resolve { ResolvedTree } import std.algebra { Cons, Empty, list_snoc_item } import v2.std.coercion { NoTargetCandidate } import std.occurrence_identity { OccurrenceSynthetic } @@ -10,7 +11,7 @@ import v2.compiler.infer { InferredFacts, InferredTree, infer } import v2.extdeps.languages.dag { dag_arrow_domain_conj_node, dag_arrow_with_body_node, dag_int_literal_node_from_lexeme, dag_type_atom_node } import v2.extdeps.languages.rust_test { rust_binop_target_model_staging } import v2.extdeps.runtimes.v2_evaluator { v2_evaluator_interpretation } -import v2.test.lens_common.infer_fixture { claim_inferred_facts_from_nodes } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations, claim_inferred_facts_from_nodes } import v2.std.cardinality { termination_proof_witness_for_node } import v2.std.compilers.target_model { canonical_operation_op_coerce, target_model_canonical_operation_wire_node } import v2.std.collection { List } @@ -61,67 +62,67 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // body_lowering_reason_type_annotation_not_carried at `T` (the as-cast refusal), and before that // they were Accepted with `T` dropped: no cast node, so the count in bcn_one_cast_to_int was 0. -fn bcn_tail_cast() -> Outcome { +fn bcn_tail_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n x as Int\n}\n") } -fn bcn_let_value_cast() -> Outcome { +fn bcn_let_value_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let y = x as Int\n y\n}\n") } -fn bcn_call_argument_cast() -> Outcome { +fn bcn_call_argument_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn g(v: Int) -> Int { v }\n\nfn f(x: Int) -> Int {\n g(v: x as Int)\n}\n") } -fn bcn_if_arm_cast() -> Outcome { +fn bcn_if_arm_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn f(b: Bool, x: Int) -> Int {\n if b { x as Int } else { x }\n}\n") } -fn bcn_match_arm_cast() -> Outcome { +fn bcn_match_arm_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn f(b: Bool, x: Int) -> Int {\n match b {\n true => x as Int\n false => x\n }\n}\n") } -fn bcn_call_operand_cast() -> Outcome { +fn bcn_call_operand_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn g(v: Int) -> Int { v }\n\nfn f(x: Int) -> Int {\n g(v: x) as Int\n}\n") } -fn bcn_tail_undeclared() -> Outcome { +fn bcn_tail_undeclared() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n x as Q\n}\n") } -fn bcn_match_arm_undeclared() -> Outcome { +fn bcn_match_arm_undeclared() -> Outcome { tpb_assemble(src: "module p\n\nfn f(b: Bool, x: Int) -> Int {\n match b {\n true => x as Q\n false => x\n }\n}\n") } -fn bcn_generic_cast() -> Outcome { +fn bcn_generic_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T {\n x as T\n}\n") } -fn bcn_value_param_as_type() -> Outcome { +fn bcn_value_param_as_type() -> Outcome { tpb_assemble(src: "module p\n\nfn f(Q: Int) -> Int {\n Q as Q\n}\n") } -fn bcn_int_sum_as_int() -> Outcome { +fn bcn_int_sum_as_int() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n (x + x) as Int\n}\n") } -fn bcn_int_sum_as_bool() -> Outcome { +fn bcn_int_sum_as_bool() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Bool {\n (x + x) as Bool\n}\n") } -fn bcn_into_refinement() -> Outcome { +fn bcn_into_refinement() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\ndata d: Pos = 1 as Pos\n") } -fn bcn_out_of_refinement() -> Outcome { +fn bcn_out_of_refinement() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Int {\n x as Int\n}\n") } -fn bcn_refinement_param_as_bool() -> Outcome { +fn bcn_refinement_param_as_bool() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Bool {\n x as Bool\n}\n") } -fn bcn_refinement_identity_cast() -> Outcome { +fn bcn_refinement_identity_cast() -> Outcome { tpb_assemble(src: "module p\n\nfn positive(x: Int) -> Bool { true }\n\ntype Pos = Int where positive\n\nfn f(x: Pos) -> Pos {\n x as Pos\n}\n") } @@ -144,11 +145,11 @@ fn bcn_atom_identity(n: Node) -> Optional { // Accepted, with exactly one cast node whose target is a resolved atom: the lowering built the node // and resolve kept T. -fn bcn_one_cast(o: Outcome) -> Bool { +fn bcn_one_cast(o: Outcome) -> Bool { match o { Rejected { diagnostics: _ } => false Accepted { value: root, diagnostics: _ } => - match bcn_cast_targets(n: root) { + match bcn_cast_targets(n: root.root) { Cons { head: t, tail: Empty } => match bcn_atom_identity(n: t) { Present { value: _ } => true @@ -159,11 +160,11 @@ fn bcn_one_cast(o: Outcome) -> Bool { } } -fn bcn_cast_target_identity(o: Outcome) -> Optional { +fn bcn_cast_target_identity(o: Outcome) -> Optional { match o { Rejected { diagnostics: _ } => Absent Accepted { value: root, diagnostics: _ } => - match bcn_cast_targets(n: root) { + match bcn_cast_targets(n: root.root) { Cons { head: t, tail: Empty } => bcn_atom_identity(n: t) _ => Absent } @@ -180,7 +181,7 @@ fn bcn_atom_in(n: Node, id: Symbol) -> Bool { } // Refused with `reason`, located at a node spelling `id` and not at the fn or the `as` token. -fn bcn_refused_at(o: Outcome, reason: Symbol, id: Symbol) -> Bool { +fn bcn_refused_at(o: Outcome, reason: Symbol, id: Symbol) -> Bool { match o { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => @@ -250,7 +251,7 @@ fn bcn_has_reason(d: NonEmptyDiagnostics, reason: Symbol) -> Bool { diagnostics_list_has_reason(xs: Cons { head: d.head, tail: d.tail }, reason: reason) } -fn bcn_infers(o: Outcome) -> Outcome { +fn bcn_infers(o: Outcome) -> Outcome { match o { Rejected { diagnostics: d } => Rejected { diagnostics: d } Accepted { value: root, diagnostics: _ } => diff --git a/src/v2/test/claim/body_let_annotation_test.dag b/src/v2/test/claim/body_let_annotation_test.dag index 32a97fa0c33..0d93fd79ef6 100644 --- a/src/v2/test/claim/body_let_annotation_test.dag +++ b/src/v2/test/claim/body_let_annotation_test.dag @@ -1,5 +1,7 @@ module v2.test.claim.body_let_annotation +import v2.compiler.resolve { ResolvedTree } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import std.algebra { Cons, Empty } import v2.std.coercion { NoTargetCandidate } import v2.test.claim.type_param_binder_frame { tpb_accepts, tpb_assemble } @@ -45,19 +47,19 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // body_lowering_reason_type_annotation_not_carried at its annotation (gunbc.rung_drop // typed_statement_let_refuses_until_the_bind_annotation_carrier), so (1)-(5) were red. -fn bla_concrete() -> Outcome { +fn bla_concrete() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let y: Int = x\n y\n}\n") } -fn bla_generic() -> Outcome { +fn bla_generic() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T {\n let y: T = x\n y\n}\n") } -fn bla_type_param_as_value() -> Outcome { +fn bla_type_param_as_value() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T {\n let y: T = T\n y\n}\n") } -fn bla_value_param_as_type() -> Outcome { +fn bla_value_param_as_type() -> Outcome { tpb_assemble(src: "module p\n\nfn f(Q: Int) -> Int {\n let y: Q = Q\n y\n}\n") } @@ -65,11 +67,11 @@ fn bla_value_param_as_type() -> Outcome { // left on the frontier. A let-bound literal is not derived there, so it would leave the check // unjudged and admit both rows without discriminating anything. The infer outcomes below are // enrolled share points, so a claim reads the result and pays for none of the sum's derivation. -fn bla_int_sum_as_int() -> Outcome { +fn bla_int_sum_as_int() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let y: Int = x + x\n y\n}\n") } -fn bla_int_sum_as_bool() -> Outcome { +fn bla_int_sum_as_bool() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let y: Bool = x + x\n x\n}\n") } @@ -91,11 +93,11 @@ fn bla_atom_identity(n: Node) -> Optional { // The one annotation a tree carries, as its atom identity; Absent when refused, when no Bind carries // one, or when more than one does. -fn bla_annotation_identity(o: Outcome) -> Optional { +fn bla_annotation_identity(o: Outcome) -> Optional { match o { Rejected { diagnostics: _ } => Absent Accepted { value: root, diagnostics: _ } => - match bla_annotations(n: root) { + match bla_annotations(n: root.root) { Cons { head: t, tail: Empty } => bla_atom_identity(n: t) _ => Absent } @@ -168,7 +170,7 @@ test fn bla_value_binder_does_not_answer_the_annotation() -> Bool { } } -fn bla_infers(o: Outcome) -> Outcome { +fn bla_infers(o: Outcome) -> Outcome { match o { Rejected { diagnostics: d } => Rejected { diagnostics: d } Accepted { value: root, diagnostics: _ } => diff --git a/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag b/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag index 6c8a576d986..c7b6788c662 100644 --- a/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag +++ b/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag @@ -144,7 +144,7 @@ test fn arrow_body_form_eval_value_vertical_holds() -> Bool { ) && arrow_body_form_eval_nullary_int_holds(callee: zero_arrow, expected: 0) && arrow_body_form_eval_binary_int_holds( - callee: add_arrow, + callee: add_arrow.root, left_lex: "2", right_lex: "3", expected: 5 diff --git a/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag b/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag index ab7176af2bd..4531bce8f14 100644 --- a/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag +++ b/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag @@ -1,5 +1,6 @@ module v2.test.claim.body_lowering.infer_transform_binary_infix_witness_helpers +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import v2.compiler.infer { inferred_facts_grounding_derived, inferred_facts_witness_for_node } import v2.compiler.resolve { resolve } @@ -55,7 +56,7 @@ fn infer_transform_witness_resolved_add_arrow() -> Optional { Accepted { value: normalized, diagnostics: _ } => match resolve(tree: normalized, lm: dag_language_model()) { Accepted { value: resolved, diagnostics: _ } => - wave1_gate1_find_arrow_in_module(root: resolved) + wave1_gate1_find_arrow_in_module(root: resolved.root) Rejected { diagnostics: _ } => Absent } } @@ -80,7 +81,7 @@ fn infer_transform_add_vertical_discriminating_holds() -> Bool { match infer_transform_witness_add_body(arrow: arrow) { Absent => false Present { value: body } => - match infer_and_discharge(tree: arrow) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: arrow)) { Accepted { value: tree, diagnostics: _ } => match inferred_facts_witness_for_node(tree: tree, node: body) { Holds { value: body_facts } => diff --git a/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_test.dag b/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_test.dag index 90ef9ecb5eb..bfe05fee340 100644 --- a/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_test.dag +++ b/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.body_lowering.infer_transform_binary_infix_witness_test +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import v2.compiler.infer { inferred_facts_grounding_derived, inferred_facts_witness_for_node } import v2.std.diagnostic { Accepted, Rejected, diagnostics_has_reason } @@ -12,7 +13,7 @@ import v2.std.node { Symbol } test fn infer_transform_non_add_remains_frontier_holds() -> Bool { let body = infer_transform_subtract_fixture() - match infer_and_discharge(tree: body) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: body)) { Accepted { value: tree, diagnostics: d } => match inferred_facts_witness_for_node(tree: tree, node: body) { Holds { value: facts } => diff --git a/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag b/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag index d03fe6ad5fe..704fb14f3e8 100644 --- a/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag +++ b/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag @@ -98,7 +98,7 @@ fn wave1_gate1_resolved_add_arrow_transform_holds() -> Bool { Accepted { value: normalized, diagnostics: _ } => match resolve(tree: normalized, lm: dag_language_model()) { Accepted { value: resolved, diagnostics: _ } => - match wave1_gate1_find_arrow_in_module(root: resolved) { + match wave1_gate1_find_arrow_in_module(root: resolved.root) { Present { value: arrow } => match find_arrow_body_child(root: arrow) { Accepted { value: body, diagnostics: _ } => diff --git a/src/v2/test/claim/body_type_annotation_refusal_test.dag b/src/v2/test/claim/body_type_annotation_refusal_test.dag index e79fa1b9b23..6e2e363bf4a 100644 --- a/src/v2/test/claim/body_type_annotation_refusal_test.dag +++ b/src/v2/test/claim/body_type_annotation_refusal_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.body_type_annotation_refusal +import v2.compiler.resolve { ResolvedTree } import v2.test.claim.type_param_binder_frame { tpb_accepts, tpb_assemble, tpb_refuses_with } import v2.std.diagnostic { Accepted, NodeLocus, NonEmptyDiagnostics, Outcome, Rejected, diagnostics_fatal, diagnostics_fatal_reason } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -17,11 +18,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // declared nowhere. (2) is the unannotated control, green before and after, so the refusal is the // annotation's and not the let's. -fn btar_let_annotated() -> Outcome { +fn btar_let_annotated() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let y: Q = x\n y\n}\n") } -fn btar_let_plain() -> Outcome { +fn btar_let_plain() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let y = x\n y\n}\n") } @@ -51,7 +52,7 @@ fn btar_refusal_at_authored(d: NonEmptyDiagnostics, id: Symbol) -> Bool { } } -fn btar_refused_at_authored_q(o: Outcome) -> Bool { +fn btar_refused_at_authored_q(o: Outcome) -> Bool { match o { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => btar_refusal_at_authored(d: d, id: ^Q) @@ -77,15 +78,15 @@ test fn btar_let_annotation_refuses() -> Bool { } } -fn btar_fn_literal_annotated() -> Outcome { +fn btar_fn_literal_annotated() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let g = fn(y) -> Q { y }\n x\n}\n") } -fn btar_fn_literal_plain() -> Outcome { +fn btar_fn_literal_plain() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int {\n let g = fn(y) { y }\n x\n}\n") } -fn btar_if_arm_fn_literal() -> Outcome { +fn btar_if_arm_fn_literal() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Bool) -> Int { if x { fn(y) { zz } } else { 1 } }\n") } diff --git a/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag b/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag index 9dffdc65322..43c51f335ce 100644 --- a/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag +++ b/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag @@ -30,7 +30,7 @@ import v2.std.runtime { RuntimeValueNodeUnrepresentable, runtime_value_node_projection } -import v2.test.lens_common.infer_fixture { claim_inferred_facts_from_nodes } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations, claim_inferred_facts_from_nodes } import v2.std.witness { Holds } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -111,7 +111,7 @@ test fn compile_eval_bool_reaches_node_value_holds() -> Bool { test fn compile_eval_bool_via_compile_entry_refuses_underived_holds() -> Bool { match compile( - source: v2_eval_bool_literal_pin, + source: claim_resolved_tree_without_declarations(root: v2_eval_bool_literal_pin), mode: Eval { runtime: v2_eval_bool_literal_pin } ) { Rejected { diagnostics: d } => d.head.reason == ^infer_grounding_not_derived diff --git a/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag b/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag index c73babb7bc7..247d9321fef 100644 --- a/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag +++ b/src/v2/test/claim/compiler/infer_application_argument_inhabitance_witness_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.compiler.infer_application_argument_inhabitance_witness_test +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.infer { infer } import v2.std.inhabitance { inhabitance_cardinality_type, @@ -151,7 +152,7 @@ fn inhabitance_formal_unresolved_tree() -> Node { test fn infer_incompatible_argument_refuses_holds() -> Bool { match infer( - tree: inhabitance_call_tree(arg: dag_type_atom_node(identity: ^dag_token_kw_true)) + tree: claim_resolved_tree_without_declarations(root: inhabitance_call_tree(arg: dag_type_atom_node(identity: ^dag_token_kw_true))) ) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: nds } => @@ -163,7 +164,7 @@ test fn infer_incompatible_argument_refuses_holds() -> Bool { } test fn infer_compatible_argument_admits_holds() -> Bool { - match infer(tree: inhabitance_call_tree(arg: dag_int_literal_fixture_one())) { + match infer(tree: claim_resolved_tree_without_declarations(root: inhabitance_call_tree(arg: dag_int_literal_fixture_one()))) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } @@ -171,9 +172,9 @@ test fn infer_compatible_argument_admits_holds() -> Bool { test fn infer_argument_type_not_derived_is_counted_frontier_holds() -> Bool { match infer( - tree: inhabitance_call_tree( + tree: claim_resolved_tree_without_declarations(root: inhabitance_call_tree( arg: node_synthetic(kind: ComputationNode { behavior: Value }, children: []) - ) + )) ) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => @@ -185,7 +186,7 @@ test fn infer_argument_type_not_derived_is_counted_frontier_holds() -> Bool { } test fn infer_generic_formal_is_counted_frontier_holds() -> Bool { - match infer(tree: inhabitance_generic_formal_tree()) { + match infer(tree: claim_resolved_tree_without_declarations(root: inhabitance_generic_formal_tree())) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => diagnostics_has_reason( @@ -209,7 +210,7 @@ test fn inhabitance_cardinality_type_is_optional_carrier_holds() -> Bool { } test fn infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds() -> Bool { - match infer(tree: inhabitance_optional_formal_tree()) { + match infer(tree: claim_resolved_tree_without_declarations(root: inhabitance_optional_formal_tree())) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: nds } => diagnostics_has_reason( @@ -220,7 +221,7 @@ test fn infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds( } test fn infer_positional_surplus_refuses_holds() -> Bool { - match infer(tree: inhabitance_arity_unmodeled_tree()) { + match infer(tree: claim_resolved_tree_without_declarations(root: inhabitance_arity_unmodeled_tree())) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: nds } => diagnostics_has_reason( @@ -231,7 +232,7 @@ test fn infer_positional_surplus_refuses_holds() -> Bool { } test fn infer_atom_operator_is_counted_formal_unresolved_holds() -> Bool { - match infer(tree: inhabitance_formal_unresolved_tree()) { + match infer(tree: claim_resolved_tree_without_declarations(root: inhabitance_formal_unresolved_tree())) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => diagnostics_has_reason( @@ -303,10 +304,10 @@ fn inhabitance_declared_formal_tree(declared: Node, arg: Node) -> Node { test fn inhabitance_collection_produced_at_a_product_formal_is_counted_frontier_holds() -> Bool { match infer( - tree: inhabitance_declared_formal_tree( + tree: claim_resolved_tree_without_declarations(root: inhabitance_declared_formal_tree( declared: inhabitance_nominal_product_type_node(), arg: inhabitance_collection_type_node() - ) + )) ) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => @@ -319,10 +320,10 @@ test fn inhabitance_collection_produced_at_a_product_formal_is_counted_frontier_ test fn inhabitance_product_produced_at_a_collection_formal_is_counted_frontier_holds() -> Bool { match infer( - tree: inhabitance_declared_formal_tree( + tree: claim_resolved_tree_without_declarations(root: inhabitance_declared_formal_tree( declared: inhabitance_collection_type_node(), arg: inhabitance_nominal_product_type_node() - ) + )) ) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => diff --git a/src/v2/test/claim/execution/data_decl_lowering_grounding_test.dag b/src/v2/test/claim/execution/data_decl_lowering_grounding_test.dag index e73a1cd848c..9084c6becd6 100644 --- a/src/v2/test/claim/execution/data_decl_lowering_grounding_test.dag +++ b/src/v2/test/claim/execution/data_decl_lowering_grounding_test.dag @@ -1,5 +1,6 @@ module v2.test.execution.data_decl_lowering_grounding +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import extdeps.communication.medium { Lossless, Medium } import std.algebra { Cons, Empty } import std.occurrence_identity { OccurrenceSynthetic } @@ -169,7 +170,7 @@ fn ddl_fully_grounded(resolved: Outcome) -> Bool { match ddl_value_member(tree: tree) { Absent => false Present { value: member } => - match infer(tree: member) { + match infer(tree: claim_resolved_tree_without_declarations(root: member)) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: ds } => ddl_no_frontier_diagnostic(ds: ds) } @@ -269,7 +270,7 @@ test fn fn_brace_literal_body_grounds_fully_holds() -> Bool { } fn ddl_hand_grounding(tree: Node, n: Node) -> Int { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: _ } => 2 Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(n) { @@ -315,7 +316,7 @@ test fn malformed_literal_payload_stays_on_the_frontier_holds() -> Bool { // So this control reads the type back: the digit list is a FreeMonoid and its head a // DecimalDigit, in the integer authority's own nodes. fn ddl_resolved_type(tree: Node, n: Node) -> Optional { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: _ } => optional_absent() Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(n) { diff --git a/src/v2/test/claim/execution/infer_atom_grounding_rules_test.dag b/src/v2/test/claim/execution/infer_atom_grounding_rules_test.dag index b776fd35ca5..6384c968d3d 100644 --- a/src/v2/test/claim/execution/infer_atom_grounding_rules_test.dag +++ b/src/v2/test/claim/execution/infer_atom_grounding_rules_test.dag @@ -1,5 +1,6 @@ module v2.test.execution.infer_atom_grounding_rules +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.infer { DerivedGrounding, GroundingNotDerived, InferredTree } @@ -186,7 +187,7 @@ test fn atom_rules_leave_unbound_atom_on_the_frontier_holds() -> Bool { children: [], occurrence_id: OccurrenceSynthetic } - match infer_and_discharge(tree: unbound) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: unbound)) { Rejected { diagnostics: _ } => false Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(unbound) { @@ -201,7 +202,7 @@ test fn atom_rules_leave_unbound_atom_on_the_frontier_holds() -> Bool { } fn atom_grounding_standalone_evidence(n: Node) -> Optional { - match infer_and_discharge(tree: n) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: n)) { Rejected { diagnostics: _ } => Absent Accepted { value: inferred, diagnostics: _ } => atom_grounding_node_evidence(inferred: inferred, n: n) } diff --git a/src/v2/test/claim/execution/infer_product_introduction_test.dag b/src/v2/test/claim/execution/infer_product_introduction_test.dag index 98747dd18b1..46b8c330f38 100644 --- a/src/v2/test/claim/execution/infer_product_introduction_test.dag +++ b/src/v2/test/claim/execution/infer_product_introduction_test.dag @@ -1,5 +1,6 @@ module v2.test.execution.infer_product_introduction +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.infer { DerivedGrounding, GroundingNotDerived, InferredTree } @@ -200,7 +201,7 @@ test fn product_introduction_leaves_childless_conj_on_the_frontier_holds() -> Bo children: [], occurrence_id: OccurrenceSynthetic } - match infer_and_discharge(tree: childless) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: childless)) { Rejected { diagnostics: _ } => false Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(childless) { @@ -215,7 +216,7 @@ test fn product_introduction_leaves_childless_conj_on_the_frontier_holds() -> Bo } fn product_introduction_hand_tree_grounding(tree: Node, n: Node) -> Int { - match infer_and_discharge(tree: tree) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: _ } => 2 Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(n) { diff --git a/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag b/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag index 683a1ee6983..902b4e97880 100644 --- a/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag @@ -305,7 +305,7 @@ fn add_arrow_source_ingested_add_infers() -> Outcome { bind_outcome( o: resolve(tree: normalized, lm: lm), f: fn(resolved) { - outcome_accepted(value: add_arrow_eval_admitted_tree(root: resolved)) + outcome_accepted(value: add_arrow_eval_admitted_tree(root: resolved.root)) } ) } diff --git a/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag b/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag index ffaab45de7f..ce19bb24148 100644 --- a/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag +++ b/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag @@ -34,7 +34,7 @@ import v2.extdeps.languages.rust_test { rust_classical_not_ingested_target_model_staging, rust_match_target_model_staging } -import v2.test.lens_common.infer_fixture { claim_inferred_facts_from_nodes } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations, claim_inferred_facts_from_nodes } import v2.std.cardinality { RankingComponent, TerminationProof } import v2.std.collection { List, @@ -155,7 +155,7 @@ fn ingested_canonical_inferred_tree_from_arrow(arrow: Outcome) -> Outcome< bind_outcome( o: arrow, f: fn(a) { - infer_and_discharge(tree: a) + infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: a)) } ) } @@ -177,7 +177,7 @@ fn ingested_staging_inferred_tree_from_arrow(arrow: Outcome) -> Outcome Outcome Bool { test fn ingested_classical_not_real_infer_holds() -> Bool { match ingested_arrow_from_source(source: ingested_classical_not_source) { Accepted { value: arrow, diagnostics: _ } => - match infer(tree: arrow) { + match infer(tree: claim_resolved_tree_without_declarations(root: arrow)) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } @@ -676,7 +676,7 @@ fn ingested_classical_not_arrow_empty_domain_fixture() -> Node { } fn ingested_classical_not_param_scrutinee_domain_unresolved_infer_refuses(tree: Node) -> Bool { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: _ } => true } diff --git a/src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag b/src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag index eb5f2067359..b1e479c5a59 100644 --- a/src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag +++ b/src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag @@ -1,5 +1,6 @@ module v2.test.execution.self_host_candidate_generation_stage_verdicts +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import std.process { ExitSuccess, ProcessExit, exit_failure } import v2.compiler.self_host.candidate_generation_stage_verdicts { CandidateGenerationStageVerdicts, @@ -46,7 +47,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly fn add_slice_stage_verdicts() -> CandidateGenerationStageVerdicts { candidate_generation_stage_verdicts( - resolved_module: dag_add_emitted_root, + resolved_module: claim_resolved_tree_without_declarations(root: dag_add_emitted_root), dag_target: dag_add_target_model ) } diff --git a/src/v2/test/claim/execution/self_host_candidate_generation_test.dag b/src/v2/test/claim/execution/self_host_candidate_generation_test.dag index 8365267ac9d..5eeee2da069 100644 --- a/src/v2/test/claim/execution/self_host_candidate_generation_test.dag +++ b/src/v2/test/claim/execution/self_host_candidate_generation_test.dag @@ -1,5 +1,6 @@ module v2.test.execution.self_host_candidate_generation +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } @@ -130,7 +131,7 @@ fn witness_translate_diagnostic_reason_symbol_inverse() -> Bool { fn candidate_generation_dag_add_slice_accepts() -> Bool { match generate_translate_self_emit_candidate( - resolved_module: dag_add_emitted_root, + resolved_module: claim_resolved_tree_without_declarations(root: dag_add_emitted_root), dag_target: dag_add_target_model ) { Accepted { value: candidate, diagnostics: d } => diff --git a/src/v2/test/claim/infer_list_introduction_test.dag b/src/v2/test/claim/infer_list_introduction_test.dag index 6b50340131c..37bc3dd65af 100644 --- a/src/v2/test/claim/infer_list_introduction_test.dag +++ b/src/v2/test/claim/infer_list_introduction_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.infer_list_introduction +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.infer { infer, infer_branch_int_binding_type_node, inferred_facts_resolved_type } import v2.extdeps.languages.dag { dag_int_literal_fixture_one, dag_type_atom_node } @@ -100,7 +101,7 @@ fn ilt_freemonoid_argument(t: Node) -> Optional { // The literal's derived type, when infer accepts it with one. fn ilt_derived_type(tree: Node) -> Optional { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: _ } => optional_absent() Accepted { value: t, diagnostics: _ } => match t.facts.lookup(tree) { @@ -158,7 +159,7 @@ test fn a_list_of_equal_lists_infers_to_a_nested_freemonoid() -> Bool { // A STRUCTURAL MISMATCH refuses located AT the differing element: the second inner list (a // FreeMonoid beside a FreeMonoid), not the outer literal or the first element. test fn a_list_of_differently_typed_lists_refuses_at_the_differing_list() -> Bool { - match infer(tree: ilt_nested_mixed) { + match infer(tree: claim_resolved_tree_without_declarations(root: ilt_nested_mixed)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: r } => (diagnostics_fatal(d: r).reason == ^infer_list_element_type_mismatch) @@ -184,7 +185,7 @@ fn ilt_is_mismatch_at_true(d: Diagnostic) -> Bool { } test fn a_mixed_list_refuses_at_the_differing_element() -> Bool { - match infer(tree: ilt_mixed) { + match infer(tree: claim_resolved_tree_without_declarations(root: ilt_mixed)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: r } => ilt_is_mismatch_at_true(d: diagnostics_fatal(d: r)) } @@ -195,7 +196,7 @@ test fn a_mixed_list_refuses_at_the_differing_element() -> Bool { // It must still be ACCEPTED: a refusal would also "derive no type", so accepting Rejected here would // let one failure common to every list pass this claim while the other two went red. test fn an_empty_list_derives_no_type_here() -> Bool { - match infer(tree: ilt_empty) { + match infer(tree: claim_resolved_tree_without_declarations(root: ilt_empty)) { Rejected { diagnostics: _ } => false Accepted { value: tree, diagnostics: _ } => match tree.facts.lookup(ilt_empty) { @@ -223,7 +224,7 @@ fn ilt_diagnostic_text(d: Diagnostic) -> String { } fn ilt_outcome_text(tree: Node) -> String { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: r } => "rejected fatal=" + ilt_diagnostic_text(d: diagnostics_fatal(d: r)) + " head=" + ilt_diagnostic_text(d: r.head) Accepted { value: t, diagnostics: _ } => match t.facts.lookup(tree) { diff --git a/src/v2/test/claim/infer_self_grounding_wall_test.dag b/src/v2/test/claim/infer_self_grounding_wall_test.dag index 0c1f6a3988f..649c9a3a7ac 100644 --- a/src/v2/test/claim/infer_self_grounding_wall_test.dag +++ b/src/v2/test/claim/infer_self_grounding_wall_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.infer_self_grounding_wall +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import extdeps.filesystem.filesystem_io import std.occurrence_identity { OccurrenceSynthetic } @@ -185,7 +186,7 @@ fn wall_derived_grounding(node: Node) -> CanonicalGrounding { } fn wall_grounding_for_node_refused(root: Node) -> Bool { - match infer_and_discharge(tree: root) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: root)) { Rejected { diagnostics: _ } => false Accepted { value: tree, diagnostics: _ } => match canonical_grounding_for_node(tree: tree, node: root) { @@ -196,7 +197,7 @@ fn wall_grounding_for_node_refused(root: Node) -> Bool { } fn wall_resolved_type_refused(root: Node) -> Bool { - match infer_and_discharge(tree: root) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: root)) { Rejected { diagnostics: _ } => false Accepted { value: tree, diagnostics: _ } => match inferred_facts_witness_for_node(tree: tree, node: root) { @@ -211,7 +212,7 @@ fn wall_resolved_type_refused(root: Node) -> Bool { } fn wall_infer_counts_frontier(root: Node) -> Bool { - match infer(tree: root) { + match infer(tree: claim_resolved_tree_without_declarations(root: root)) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => match d { @@ -302,7 +303,7 @@ fn wall_frontier_observation_matches_infer(nes: NonEmptyDiagnostics, o: ProbeObs test fn wall_frontier_receipt_joins_corpus_identity() -> Bool { let root = wall_value_node() - match infer(tree: root) { + match infer(tree: claim_resolved_tree_without_declarations(root: root)) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => match d { @@ -347,7 +348,7 @@ test fn wall_frontier_receipt_joins_corpus_identity() -> Bool { test fn wall_frontier_derived_green_receipt_joins_corpus_identity() -> Bool { let root = dag_pick_if_body_fixture - match infer(tree: root) { + match infer(tree: claim_resolved_tree_without_declarations(root: root)) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: d } => match active_v2_infer_eval_probe_row(probe: v2_frontier_green_probe) { diff --git a/src/v2/test/claim/long/inhabitant_neutralization_e2e_witness_test.dag b/src/v2/test/claim/long/inhabitant_neutralization_e2e_witness_test.dag index 9d04a0b7b05..6b95bb7fce4 100644 --- a/src/v2/test/claim/long/inhabitant_neutralization_e2e_witness_test.dag +++ b/src/v2/test/claim/long/inhabitant_neutralization_e2e_witness_test.dag @@ -1,5 +1,6 @@ module v2.test.long.inhabitant_neutralization_e2e_witness +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import v2.compiler.emit { emit } import v2.compiler.ingest { cross_language_compile } @@ -88,7 +89,7 @@ test fn inhabitant_neutralization_python_to_go_translate_rejects() -> Bool { target: go_target_model() ) { Accepted { value: neutralized, diagnostics: _ } => - match infer_and_discharge(tree: neutralized) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: neutralized)) { Accepted { value: inferred, diagnostics: _ } => match translate(tree: inferred, target: go_target_model()) { Rejected { diagnostics: _ } => true @@ -106,7 +107,7 @@ test fn inhabitant_neutralization_python_to_go_emit_rejects() -> Bool { target: go_target_model() ) { Accepted { value: neutralized, diagnostics: _ } => - match infer_and_discharge(tree: neutralized) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: neutralized)) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: go_target_model()) { Rejected { diagnostics: _ } => true diff --git a/src/v2/test/claim/long/parser_completeness_frontier_test.dag b/src/v2/test/claim/long/parser_completeness_frontier_test.dag index 511a4a23d36..34ee0e404da 100644 --- a/src/v2/test/claim/long/parser_completeness_frontier_test.dag +++ b/src/v2/test/claim/long/parser_completeness_frontier_test.dag @@ -29,7 +29,7 @@ fn parser_frontier_admission() -> Admission { } } -fn parser_frontier_assemble_for(src: String) -> Outcome { +fn parser_frontier_assemble_for(src: String) -> Outcome { assemble_program_from_ingest( ingest: parser_frontier_ingest_for(src: src), admission: parser_frontier_admission(), diff --git a/src/v2/test/claim/long/self_host_module_emit_derisk_test.dag b/src/v2/test/claim/long/self_host_module_emit_derisk_test.dag index cb9fe49f6ec..6351a14afb8 100644 --- a/src/v2/test/claim/long/self_host_module_emit_derisk_test.dag +++ b/src/v2/test/claim/long/self_host_module_emit_derisk_test.dag @@ -1,5 +1,7 @@ module v2.test.long.self_host_module_emit_derisk +import v2.compiler.resolve { ResolvedTree } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import extdeps.communication.medium { Lossless, Medium } import v2.compiler.name_resolve { @@ -56,7 +58,7 @@ fn derisk_module_admission() -> Admission { } } -fn derisk_assemble_for(src: String) -> Outcome { +fn derisk_assemble_for(src: String) -> Outcome { assemble_program_from_ingest( ingest: derisk_ingest_for(src: src), admission: derisk_module_admission(), diff --git a/src/v2/test/claim/loop_infer_iteration_test.dag b/src/v2/test/claim/loop_infer_iteration_test.dag index e8e5a6707f5..f55c5048dc1 100644 --- a/src/v2/test/claim/loop_infer_iteration_test.dag +++ b/src/v2/test/claim/loop_infer_iteration_test.dag @@ -49,7 +49,7 @@ fn loop_infer_registered_measure() -> Node { } fn loop_infer_run(root: Node) -> Outcome { - infer_and_discharge(tree: root) + infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: root)) } fn loop_infer_loop_type_is_int(tree: InferredTree, body: Node) -> Bool { diff --git a/src/v2/test/claim/manual/branch_infer_fail_open_audit_test.dag b/src/v2/test/claim/manual/branch_infer_fail_open_audit_test.dag index 53a4490b0a7..e261d23793a 100644 --- a/src/v2/test/claim/manual/branch_infer_fail_open_audit_test.dag +++ b/src/v2/test/claim/manual/branch_infer_fail_open_audit_test.dag @@ -1,4 +1,5 @@ module v2.test.manual.branch_infer_fail_open_audit +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.infer { infer } import v2.extdeps.languages.dag { dag_pick_if_body_fixture, @@ -26,7 +27,7 @@ fn branch_infer_fail_open_audit_body() -> Node { } test fn branch_infer_fail_open_audit_rejects_holds() -> Bool { - match infer(tree: branch_infer_fail_open_audit_body()) { + match infer(tree: claim_resolved_tree_without_declarations(root: branch_infer_fail_open_audit_body())) { Accepted { value: _, diagnostics: d } => false Rejected { diagnostics: _ } => true } @@ -34,14 +35,14 @@ test fn branch_infer_fail_open_audit_rejects_holds() -> Bool { } fn branch_infer_fail_open_audit_silent_accept_holds() -> Bool { - match infer(tree: branch_infer_fail_open_audit_body()) { + match infer(tree: claim_resolved_tree_without_declarations(root: branch_infer_fail_open_audit_body())) { Accepted { value: _, diagnostics: d } => d == None Rejected { diagnostics: _ } => false } } test fn branch_infer_fail_open_audit_literal_arm_accepts_holds() -> Bool { - match infer(tree: dag_pick_if_body_fixture) { + match infer(tree: claim_resolved_tree_without_declarations(root: dag_pick_if_body_fixture)) { Accepted { value: _, diagnostics: d } => d == None Rejected { diagnostics: _ } => false } diff --git a/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag b/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag index cfe1729ee2b..2a798ccc7c5 100644 --- a/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag +++ b/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag @@ -1,5 +1,6 @@ module v2.test.manual.branch_infer_if_then_else +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.infer { infer, } @@ -35,7 +36,7 @@ fn branch_infer_arm_mismatch_body() -> Node { } test fn branch_infer_bool_cond_accepts_holds() -> Bool { - match infer(tree: dag_pick_if_body_fixture) { + match infer(tree: claim_resolved_tree_without_declarations(root: dag_pick_if_body_fixture)) { Accepted { value: _, diagnostics: d } => d == None Rejected { diagnostics: _ } => false } @@ -47,7 +48,7 @@ test fn branch_infer_bool_cond_accepts_holds() -> Bool { // remains covered by branch_infer_test using two genuinely derived operand types. test fn branch_infer_underived_arm_refuses_before_mismatch_holds() -> Bool { - match infer(tree: branch_infer_arm_mismatch_body()) { + match infer(tree: claim_resolved_tree_without_declarations(root: branch_infer_arm_mismatch_body())) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => d.head.reason == ^infer_grounding_not_derived } diff --git a/src/v2/test/claim/manual/branch_infer_test.dag b/src/v2/test/claim/manual/branch_infer_test.dag index a7d3a9ca4ed..5567b0a881d 100644 --- a/src/v2/test/claim/manual/branch_infer_test.dag +++ b/src/v2/test/claim/manual/branch_infer_test.dag @@ -65,7 +65,7 @@ fn branch_infer_cond_not_bool_body_node() -> Outcome { } fn branch_infer_resolved_tree(root: Node) -> ResolvedTree { - root + claim_resolved_tree_without_declarations(root: root) } fn branch_infer_positional_target(body: Node, index: Int) -> Node { diff --git a/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag b/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag index 72214a7d766..7f4e1fb7cda 100644 --- a/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag +++ b/src/v2/test/claim/manual/cross_language_add_python_to_typescript_test.dag @@ -1,5 +1,6 @@ module v2.test.manual.cross_language_add_python_to_typescript +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import v2.test.manual.python_grammar_claim { python_grammar_parse_fixture @@ -90,7 +91,7 @@ test fn parse_tree_to_target_model_bridge_realized() -> Bool { } test fn cross_language_emit_inhabitant_neutralization_fails_closed() -> Bool { - match infer_and_discharge(tree: python_emitted_add_fn_node()) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: python_emitted_add_fn_node())) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: ts_target_model()) { Rejected { diagnostics: _ } => true @@ -115,7 +116,7 @@ test fn cross_language_emit_inhabitant_neutralization_round_trip_holds() -> Bool target: ts_target_model() ) { Accepted { value: neutralized, diagnostics: _ } => - match infer_and_discharge(tree: neutralized) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: neutralized)) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: ts_target_model()) { Accepted { value: source, diagnostics: _ } => diff --git a/src/v2/test/claim/manual/infer_bounded_lattice_completeness_anchor_test.dag b/src/v2/test/claim/manual/infer_bounded_lattice_completeness_anchor_test.dag index da366cbb758..227e6771c51 100644 --- a/src/v2/test/claim/manual/infer_bounded_lattice_completeness_anchor_test.dag +++ b/src/v2/test/claim/manual/infer_bounded_lattice_completeness_anchor_test.dag @@ -1,5 +1,6 @@ module v2.test.manual.infer_bounded_lattice_completeness_anchor +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.infer { InferredTree } @@ -176,7 +177,7 @@ data anchor_consumer_gate_rejects_partial_reference: Outcome = infer_bound partials: [anchor_partial_bounded_lattice_instance] ) -data anchor_infer_rejects_consumer_tree: Outcome = infer_and_discharge(tree: anchor_module_with_partial_and_consumer) +data anchor_infer_rejects_consumer_tree: Outcome = infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: anchor_module_with_partial_and_consumer)) fn anchor_infer_consumer_tree_is_rejected() -> Bool { match anchor_infer_rejects_consumer_tree { diff --git a/src/v2/test/claim/manual/infer_emit_compile_anchor.dag b/src/v2/test/claim/manual/infer_emit_compile_anchor.dag index da2d49858c9..8a53f7941cb 100644 --- a/src/v2/test/claim/manual/infer_emit_compile_anchor.dag +++ b/src/v2/test/claim/manual/infer_emit_compile_anchor.dag @@ -43,7 +43,7 @@ data anchor_stub_inferred_tree: InferredTree = InferredTree { } fn anchor_infer_rejects() -> Outcome { - infer_and_discharge(tree: anchor_stub_empty_conj) + infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: anchor_stub_empty_conj)) } fn anchor_emit_rejects() -> Outcome> { diff --git a/src/v2/test/claim/manual/infer_ground_add.dag b/src/v2/test/claim/manual/infer_ground_add.dag index 12ba621e60f..236ff22093b 100644 --- a/src/v2/test/claim/manual/infer_ground_add.dag +++ b/src/v2/test/claim/manual/infer_ground_add.dag @@ -1,5 +1,6 @@ module v2.test.manual.infer_ground_add +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.eval { @@ -324,10 +325,10 @@ fn infer_descent_witness_receipt_run( } } -fn fixture_add_resolved_node() -> Node { - fixture_add_resolved_tree() -} fn fixture_add_resolved_tree() -> ResolvedTree { + claim_resolved_tree_without_declarations(root: fixture_add_resolved_node()) +} +fn fixture_add_resolved_node() -> Node { Node { kind: TypeNode { connective: Conj }, children: [ diff --git a/src/v2/test/claim/manual/ingest_bridge_test.dag b/src/v2/test/claim/manual/ingest_bridge_test.dag index 26f924fc96a..9f7ec970572 100644 --- a/src/v2/test/claim/manual/ingest_bridge_test.dag +++ b/src/v2/test/claim/manual/ingest_bridge_test.dag @@ -1,5 +1,6 @@ module v2.test.manual.ingest_bridge +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } @@ -229,7 +230,7 @@ test fn ingest_bridge_to_canonical_holds() -> Bool { test fn ingest_identity_coercion_accepts_source_present_in_authored_roster() -> Bool { let source = dag_fixture_emitted_add_fn - match infer_and_discharge(tree: source) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: source)) { Rejected { diagnostics: _ } => false Accepted { value: inferred, diagnostics: _ } => match canonical_grounding_for_node(tree: inferred, node: source) { @@ -253,7 +254,7 @@ test fn ingest_identity_coercion_accepts_source_present_in_authored_roster() -> test fn ingest_identity_coercion_refuses_source_absent_from_authored_roster() -> Bool { let source = ingest_unstamped_node() - match infer_and_discharge(tree: source) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: source)) { Rejected { diagnostics: _ } => false Accepted { value: inferred, diagnostics: _ } => match coerce_grounded_node( diff --git a/src/v2/test/claim/manual/inhabitant_neutralization_test.dag b/src/v2/test/claim/manual/inhabitant_neutralization_test.dag index e0a7078a001..85d252011a9 100644 --- a/src/v2/test/claim/manual/inhabitant_neutralization_test.dag +++ b/src/v2/test/claim/manual/inhabitant_neutralization_test.dag @@ -1,5 +1,6 @@ module v2.test.manual.inhabitant_neutralization +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import v2.compiler.emit { emit } import v2.compiler.ingest { cross_language_compile } @@ -146,7 +147,7 @@ fn inhabitant_neutralization_go_int64_to_ts_emit_round_trip_holds() -> Bool { target: ts_target_model() ) { Accepted { value: neutralized, diagnostics: _ } => - match infer_and_discharge(tree: neutralized) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: neutralized)) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: ts_target_model()) { Accepted { value: source, diagnostics: _ } => source.carried == ts_source_text @@ -191,7 +192,7 @@ test fn inhabitant_neutralization_emit_after_neutralize_round_trip_holds() -> Bo target: ts_target_model() ) { Accepted { value: neutralized, diagnostics: _ } => - match infer_and_discharge(tree: neutralized) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: neutralized)) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: ts_target_model()) { Accepted { value: source, diagnostics: _ } => source.carried == ts_source_text @@ -204,7 +205,7 @@ test fn inhabitant_neutralization_emit_after_neutralize_round_trip_holds() -> Bo } fn inhabitant_neutralization_raw_emit_still_fails_closed() -> Bool { - match infer_and_discharge(tree: python_emitted_add_fn_node()) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: python_emitted_add_fn_node())) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: ts_target_model()) { Rejected { diagnostics: _ } => true @@ -228,7 +229,7 @@ fn inhabitant_neutralization_same_flavor_python_emit_round_trip_holds() -> Bool target: python_target_model() ) { Accepted { value: neutralized, diagnostics: _ } => - match infer_and_discharge(tree: neutralized) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: neutralized)) { Accepted { value: inferred, diagnostics: _ } => match emit(tree: inferred, target: python_target_model()) { Accepted { value: source, diagnostics: _ } => source.carried == python_source_text diff --git a/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag b/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag index e83fd9f5012..94bd81fee8e 100644 --- a/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag +++ b/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag @@ -1,5 +1,6 @@ module v2.test.manual.match_infer_fail_open_audit +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.infer { infer } import v2.extdeps.languages.dag { @@ -78,7 +79,7 @@ fn match_infer_fail_open_audit_body() -> Node { } test fn match_infer_fail_open_audit_rejects_holds() -> Bool { - match infer(tree: match_infer_fail_open_audit_body()) { + match infer(tree: claim_resolved_tree_without_declarations(root: match_infer_fail_open_audit_body())) { Accepted { value: _, diagnostics: d } => false Rejected { diagnostics: _ } => true } @@ -105,7 +106,7 @@ fn match_infer_fail_open_audit_non_exhaustive_body() -> Node { } test fn match_infer_fail_open_audit_non_exhaustive_rejects_holds() -> Bool { - match infer(tree: match_infer_fail_open_audit_non_exhaustive_body()) { + match infer(tree: claim_resolved_tree_without_declarations(root: match_infer_fail_open_audit_non_exhaustive_body())) { Accepted { value: _, diagnostics: d } => false Rejected { diagnostics: _ } => true } @@ -146,7 +147,7 @@ fn match_infer_fail_open_audit_extra_arm_body() -> Node { } test fn match_infer_fail_open_audit_extra_arm_rejects_holds() -> Bool { - match infer(tree: match_infer_fail_open_audit_extra_arm_body()) { + match infer(tree: claim_resolved_tree_without_declarations(root: match_infer_fail_open_audit_extra_arm_body())) { Accepted { value: _, diagnostics: d } => false Rejected { diagnostics: _ } => true } @@ -185,14 +186,14 @@ fn classical_not_int_match_arrow_fixture() -> Node { } test fn complement_body_real_infer_refuses_unsupported_pattern_holds() -> Bool { - match infer(tree: dag_complement_body_fixture) { + match infer(tree: claim_resolved_tree_without_declarations(root: dag_complement_body_fixture)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: _ } => true } } test fn classical_not_int_match_arrow_real_infer_holds() -> Bool { - match infer(tree: classical_not_int_match_arrow_fixture()) { + match infer(tree: claim_resolved_tree_without_declarations(root: classical_not_int_match_arrow_fixture())) { Accepted { value: _, diagnostics: d } => diagnostics_contain_reason( d: d, @@ -230,7 +231,7 @@ fn classical_not_int_match_non_octet_arm_fixture() -> Node { } test fn classical_not_int_match_non_octet_arm_rejects_holds() -> Bool { - match infer(tree: classical_not_int_match_non_octet_arm_fixture()) { + match infer(tree: claim_resolved_tree_without_declarations(root: classical_not_int_match_non_octet_arm_fixture())) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: _ } => true } @@ -243,7 +244,7 @@ test fn classical_not_int_match_non_octet_arm_rejects_holds() -> Bool { // complement_arrow_real_infer_holds. test fn complement_arrow_real_infer_refuses_unsupported_pattern_holds() -> Bool { - match infer(tree: dag_complement_arrow_with_body_fixture) { + match infer(tree: claim_resolved_tree_without_declarations(root: dag_complement_arrow_with_body_fixture)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: _ } => true } diff --git a/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag b/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag index 5237c01b16c..f90f52e550f 100644 --- a/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag +++ b/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag @@ -104,7 +104,7 @@ fn probe_resolve(roots: FreeMonoid) -> Outcome { ) } -fn probe_resolved_export_identity(tree: ResolvedTree, wanted: Symbol) -> Bool { +fn probe_resolved_export_identity(tree: Node, wanted: Symbol) -> Bool { match tree.kind { TypeNode { connective: Atom { identity: id } } => id == wanted _ => @@ -119,7 +119,7 @@ test fn one_member_module_resolves_under_full_language_model() -> Bool { match probe_resolve(roots: roots) { Accepted { value: resolved, diagnostics: _ } => probe_resolved_export_identity( - tree: resolved, + tree: resolved.root, wanted: ^dag_c3_surface_sugar_service ) Rejected { diagnostics: _ } => false diff --git a/src/v2/test/claim/refinement_discharge_test.dag b/src/v2/test/claim/refinement_discharge_test.dag index fc89b849fc8..db6543a851d 100644 --- a/src/v2/test/claim/refinement_discharge_test.dag +++ b/src/v2/test/claim/refinement_discharge_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.refinement_discharge +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.infer { infer } import v2.compiler.inferred_tree { InferredTree, ObligatedInferredTree, RefinementObligation } import v2.compiler.refinement_discharge { discharge_refinement_obligations } @@ -58,7 +59,7 @@ fn rdt_false() -> Node { // infer's own output over the application, with ONE supplied obligation naming it. fn rdt_obligated(body: Node) -> Optional { let app = rdt_application(body: body) - match infer(tree: app) { + match infer(tree: claim_resolved_tree_without_declarations(root: app)) { Rejected { diagnostics: _ } => optional_absent() Accepted { value: t, diagnostics: _ } => optional_present(value: ObligatedInferredTree { @@ -115,7 +116,7 @@ test fn rdt_an_unevaluable_application_refuses_undischargeable_whatever_its_body // (2) ZERO OBLIGATIONS: the identity, and the cost path every module takes today. test fn rdt_zero_obligations_discharge_to_the_same_tree() -> Bool { - match infer(tree: rdt_application(body: rdt_true())) { + match infer(tree: claim_resolved_tree_without_declarations(root: rdt_application(body: rdt_true()))) { Rejected { diagnostics: _ } => false Accepted { value: t, diagnostics: _ } => match discharge_refinement_obligations(t: t) { diff --git a/src/v2/test/claim/translate_underived_refusal_test.dag b/src/v2/test/claim/translate_underived_refusal_test.dag index fe05e333a5c..d1fd69ca049 100644 --- a/src/v2/test/claim/translate_underived_refusal_test.dag +++ b/src/v2/test/claim/translate_underived_refusal_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.translate_underived_refusal +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } import v2.compiler.emit { emit } @@ -128,7 +129,7 @@ fn translate_underived_value_node() -> Node { } fn translate_underived_value_specimen_facts() -> Optional { - match infer_and_discharge(tree: translate_underived_value_specimen) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: translate_underived_value_specimen)) { Accepted { value: tree, diagnostics: _ } => tree.facts.lookup(translate_underived_value_specimen) Rejected { diagnostics: _ } => optional_absent() @@ -184,7 +185,7 @@ fn translate_bodyless_emission_root_with_poison_child_root() -> Node { } fn translate_bodyless_emission_root_facts_for(node: Node) -> Optional { - match infer_and_discharge(tree: python_emitted_add_fn_node()) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: python_emitted_add_fn_node())) { Accepted { value: tree, diagnostics: _ } => tree.facts.lookup(node) Rejected { diagnostics: _ } => optional_absent() } @@ -314,7 +315,7 @@ data translate_underived_grammar_match_target: TargetModel = TargetModel { } fn translate_refuses_underived_root_for_target(root: Node, target: TargetModel) -> Bool { - match infer_and_discharge(tree: root) { + match infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: root)) { Rejected { diagnostics: _ } => false Accepted { value: tree, diagnostics: _ } => match translate(tree: tree, target: target) { diff --git a/src/v2/test/claim/type_param_binder_frame_test.dag b/src/v2/test/claim/type_param_binder_frame_test.dag index 2a5c1b76dcd..810f8c1caf5 100644 --- a/src/v2/test/claim/type_param_binder_frame_test.dag +++ b/src/v2/test/claim/type_param_binder_frame_test.dag @@ -1,5 +1,7 @@ module v2.test.claim.type_param_binder_frame +import v2.compiler.resolve { ResolvedTree } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import extdeps.communication.medium { Lossless, Medium } import v2.compiler.name_resolve { Admission, ResolutionSubject } import v2.compiler.program_assembly { assemble_program_from_ingest } @@ -84,7 +86,7 @@ data tpb_artifact: Artifact = Artifact { file_path: "src/v2/pilot/type_param_binder_frame_pilot.dag" } -fn tpb_assemble(src: String) -> Outcome { +fn tpb_assemble(src: String) -> Outcome { assemble_program_from_ingest( ingest: Cons { head: DagSourceReadWitness { @@ -106,14 +108,14 @@ fn tpb_assemble(src: String) -> Outcome { // Each tpb_* specimen below is nullary and pure over an inline source -- Nodes and located // diagnostics, no closure -- and is enrolled in v2.workflow.floor_pure_producer_share, so // preparation runs the real route once per specimen and the rows read it. -fn tpb_accepts(o: Outcome) -> Bool { +fn tpb_accepts(o: Outcome) -> Bool { match o { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } } -fn tpb_refuses_with(o: Outcome, reason: Symbol) -> Bool { +fn tpb_refuses_with(o: Outcome, reason: Symbol) -> Bool { match o { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == reason @@ -121,11 +123,11 @@ fn tpb_refuses_with(o: Outcome, reason: Symbol) -> Bool { } // The declared type-parameter names of every Arrow in the resolved tree, in walk order. -fn tpb_type_param_rosters(o: Outcome) -> List> { +fn tpb_type_param_rosters(o: Outcome) -> List> { match o { Rejected { diagnostics: _ } => [] Accepted { value: n, diagnostics: _ } => - fold(node_subtree_nodes(root: n), init: [], f: fn(acc, m) { + fold(node_subtree_nodes(root: n.root), init: [], f: fn(acc, m) { match m.kind { TypeNode { connective: Arrow } => if count(type_param_names(n: m)) == 0 { acc } else { concat(acc, [type_param_names(n: m)]) } @@ -135,35 +137,35 @@ fn tpb_type_param_rosters(o: Outcome) -> List> { } } -fn tpb_identity() -> Outcome { +fn tpb_identity() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T { x }\n") } -fn tpb_colliding() -> Outcome { +fn tpb_colliding() -> Outcome { tpb_assemble(src: "module p\n\ntype T = Int\n\nfn f(x: T) -> T { x }\n") } -fn tpb_used_outside() -> Outcome { +fn tpb_used_outside() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T { x }\n\nfn h(y: T) -> Int { 1 }\n") } -fn tpb_same_name_twice() -> Outcome { +fn tpb_same_name_twice() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T { x }\n\nfn g(y: T) -> T { y }\n") } -fn tpb_sibling_binder_leak() -> Outcome { +fn tpb_sibling_binder_leak() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T { x }\n\nfn g(y: T) -> U { y }\n") } -fn tpb_two_params() -> Outcome { +fn tpb_two_params() -> Outcome { tpb_assemble(src: "module p\n\nfn first(a: A, b: B) -> A { a }\n") } -fn tpb_undeclared_type_name() -> Outcome { +fn tpb_undeclared_type_name() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: V) -> T { x }\n") } -fn tpb_non_generic() -> Outcome { +fn tpb_non_generic() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: Int) -> Int { x }\n") } @@ -213,7 +215,7 @@ test fn tpb_non_generic_fn_carries_no_type_params() -> Bool { tpb_accepts(o: tpb_non_generic()) && tpb_type_param_rosters(o: tpb_non_generic()) == [] } -fn tpb_type_param_as_value() -> Outcome { +fn tpb_type_param_as_value() -> Outcome { tpb_assemble(src: "module p\n\nfn f(x: T) -> T { T }\n") } @@ -292,10 +294,10 @@ test fn tpb_generic_arrow_is_well_formed() -> Bool { // (9) An argument at a type-variable formal instantiates it. RED ON MAIN: judged as the ordinary // declared type `T`, the Int argument refused application_argument_does_not_inhabit. test fn tpb_argument_at_a_type_variable_instantiates_it() -> Bool { - match infer(tree: tpb_apply( + match infer(tree: claim_resolved_tree_without_declarations(root: tpb_apply( arrow: tpb_generic_arrow(type_params: [^T], formals: [tpb_formal(name: ^x, declared: ^T)]), args: [dag_int_literal_fixture_one()] - )) { + ))) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } @@ -304,10 +306,10 @@ test fn tpb_argument_at_a_type_variable_instantiates_it() -> Bool { // (10) A type variable is ONE type per application: `f(x: T, y: T)` applied to an Int and a // Bool refuses at the second argument. Without it, (9) could be green by admitting anything. test fn tpb_second_occurrence_must_inhabit_the_instance() -> Bool { - match infer(tree: tpb_apply( + match infer(tree: claim_resolved_tree_without_declarations(root: tpb_apply( arrow: tpb_generic_arrow(type_params: [^T], formals: [tpb_formal(name: ^x, declared: ^T), tpb_formal(name: ^y, declared: ^T)]), args: [dag_int_literal_fixture_one(), tpb_true()] - )) { + ))) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => diagnostics_has_reason(d: Some { diagnostics: d }, reason: ^application_argument_does_not_inhabit) @@ -316,10 +318,10 @@ test fn tpb_second_occurrence_must_inhabit_the_instance() -> Bool { // (11) Distinct binders do not alias: `f(x: T, y: U)` admits an Int and a Bool. test fn tpb_distinct_type_variables_do_not_alias() -> Bool { - match infer(tree: tpb_apply( + match infer(tree: claim_resolved_tree_without_declarations(root: tpb_apply( arrow: tpb_generic_arrow(type_params: [^T, ^U], formals: [tpb_formal(name: ^x, declared: ^T), tpb_formal(name: ^y, declared: ^U)]), args: [dag_int_literal_fixture_one(), tpb_true()] - )) { + ))) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } @@ -328,10 +330,10 @@ test fn tpb_distinct_type_variables_do_not_alias() -> Bool { // (12) The type variable is the callee's OWN: an Arrow declaring no `T` still judges `x: T` as the // ordinary declared type, and the Int argument refuses. test fn tpb_undeclared_t_is_not_a_type_variable() -> Bool { - match infer(tree: tpb_apply( + match infer(tree: claim_resolved_tree_without_declarations(root: tpb_apply( arrow: tpb_generic_arrow(type_params: [^U], formals: [tpb_formal(name: ^x, declared: ^T)]), args: [dag_int_literal_fixture_one()] - )) { + ))) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => diagnostics_has_reason(d: Some { diagnostics: d }, reason: ^application_argument_does_not_inhabit) @@ -406,11 +408,11 @@ test fn tpb_emitter_refuses_a_generic_arrow() -> Bool { // The declared type-parameter names of every non-Arrow node in the resolved tree, in walk order: // on a type declaration, the member that carries them. -fn tpb_member_type_param_rosters(o: Outcome) -> List> { +fn tpb_member_type_param_rosters(o: Outcome) -> List> { match o { Rejected { diagnostics: _ } => [] Accepted { value: n, diagnostics: _ } => - fold(node_subtree_nodes(root: n), init: [], f: fn(acc, m) { + fold(node_subtree_nodes(root: n.root), init: [], f: fn(acc, m) { match m.kind { TypeNode { connective: Arrow } => acc _ => if count(type_param_names(n: m)) == 0 { acc } else { concat(acc, [type_param_names(n: m)]) } @@ -419,27 +421,27 @@ fn tpb_member_type_param_rosters(o: Outcome) -> List> { } } -fn tpb_type_decl_coproduct() -> Outcome { +fn tpb_type_decl_coproduct() -> Outcome { tpb_assemble(src: "module p\n\ntype Box = Full { value: T } | Empty\n") } -fn tpb_type_decl_coproduct_colliding() -> Outcome { +fn tpb_type_decl_coproduct_colliding() -> Outcome { tpb_assemble(src: "module p\n\ntype T = Int\n\ntype Box = Full { value: T } | Empty\n") } -fn tpb_type_decl_record() -> Outcome { +fn tpb_type_decl_record() -> Outcome { tpb_assemble(src: "module p\n\ntype R { f: T }\n") } -fn tpb_type_decl_record_two() -> Outcome { +fn tpb_type_decl_record_two() -> Outcome { tpb_assemble(src: "module p\n\ntype Pair { left: A, right: B }\n") } -fn tpb_type_decl_leak() -> Outcome { +fn tpb_type_decl_leak() -> Outcome { tpb_assemble(src: "module p\n\ntype Box = Full { value: T } | Empty\n\ntype S { g: T }\n") } -fn tpb_type_decl_non_generic() -> Outcome { +fn tpb_type_decl_non_generic() -> Outcome { tpb_assemble(src: "module p\n\ntype B = Full { value: Int } | Empty\n") } @@ -514,11 +516,11 @@ fn tpb_box_member_mixed() -> Node { ) } -fn tpb_type_decl_emit_twin() -> Outcome { +fn tpb_type_decl_emit_twin() -> Outcome { translate_type_expression_project(node: tpb_box_member(with_params: false), target: rust_target_model(), projection: rust_type_expression_projection()) } -fn tpb_type_decl_emit_generic() -> Outcome { +fn tpb_type_decl_emit_generic() -> Outcome { translate_type_expression_project(node: tpb_box_member(with_params: true), target: rust_target_model(), projection: rust_type_expression_projection()) } @@ -537,11 +539,11 @@ test fn tpb_translator_refuses_a_generic_type_decl_member() -> Bool { // The member of the first generic type declaration in the resolved tree: the first non-Arrow node // carrying type binders is its wrapper, read through the one typed unwrap. -fn tpb_generic_member(o: Outcome) -> List { +fn tpb_generic_member(o: Outcome) -> List { match o { Rejected { diagnostics: _ } => [] Accepted { value: n, diagnostics: _ } => - fold(node_subtree_nodes(root: n), init: [], f: fn(acc, m) { + fold(node_subtree_nodes(root: n.root), init: [], f: fn(acc, m) { match m.kind { TypeNode { connective: Arrow } => acc _ => @@ -623,44 +625,44 @@ test fn tpb_semantic_decl_emitter_refuses_a_generic_member() -> Bool { && tpb_semantic_emit_generic_reason() == ^translate_reason_generic_type_decl_not_rendered } -fn tpb_type_decl_generic_alias() -> Outcome { +fn tpb_type_decl_generic_alias() -> Outcome { tpb_assemble(src: "module p\n\ntype Id = T\n") } -fn tpb_type_decl_generic_alias_instantiation() -> Outcome { +fn tpb_type_decl_generic_alias_instantiation() -> Outcome { tpb_assemble(src: "module p\n\ntype Maybe = Some { v: A } | None\n\ntype Box = Maybe\n") } -fn tpb_type_decl_generic_alias_colliding() -> Outcome { +fn tpb_type_decl_generic_alias_colliding() -> Outcome { tpb_assemble(src: "module p\n\ntype T = Int\n\ntype Id = T\n") } -fn tpb_type_decl_generic_alias_undeclared() -> Outcome { +fn tpb_type_decl_generic_alias_undeclared() -> Outcome { tpb_assemble(src: "module p\n\ntype Id = Q\n") } -fn tpb_type_decl_generic_opaque() -> Outcome { +fn tpb_type_decl_generic_opaque() -> Outcome { tpb_assemble(src: "module p\n\ntype W\n") } -fn tpb_type_decl_generic_single_variant_after_separator() -> Outcome { +fn tpb_type_decl_generic_single_variant_after_separator() -> Outcome { tpb_assemble(src: "module p\n\ntype X =\n | Only\n") } -fn tpb_type_decl_plain_single_variant_after_separator() -> Outcome { +fn tpb_type_decl_plain_single_variant_after_separator() -> Outcome { tpb_assemble(src: "module p\n\ntype S =\n | Only\n") } -fn tpb_type_decl_plain_single_alias() -> Outcome { +fn tpb_type_decl_plain_single_alias() -> Outcome { tpb_assemble(src: "module p\n\ntype S = Int\n") } // Whether the resolved tree holds a Disj with exactly one arm, labelled `label`. -fn tpb_has_one_arm_disj(o: Outcome, label: Symbol) -> Bool { +fn tpb_has_one_arm_disj(o: Outcome, label: Symbol) -> Bool { match o { Rejected { diagnostics: _ } => false Accepted { value: n, diagnostics: _ } => - fold(node_subtree_nodes(root: n), init: false, f: fn(acc, m) { + fold(node_subtree_nodes(root: n.root), init: false, f: fn(acc, m) { acc || match m.kind { TypeNode { connective: Disj } => (count(m.children) == 1) && (tpb_arm_labels(members: [m]) == [label]) @@ -671,11 +673,11 @@ fn tpb_has_one_arm_disj(o: Outcome, label: Symbol) -> Bool { } // The v2.std.type_binder view of every generic declaration target in the resolved tree, as a tag. -fn tpb_generic_view_tags(o: Outcome) -> List { +fn tpb_generic_view_tags(o: Outcome) -> List { match o { Rejected { diagnostics: _ } => [] Accepted { value: n, diagnostics: _ } => - fold(node_subtree_nodes(root: n), init: [], f: fn(acc, m) { + fold(node_subtree_nodes(root: n.root), init: [], f: fn(acc, m) { match m.kind { TypeNode { connective: Arrow } => acc _ => @@ -790,7 +792,7 @@ test fn tpb_wrapper_with_no_view_arm_is_refused() -> Bool { && type_binder_labels_conform(root: type_alias_wrapper(binders: tpb_t_binders(), aliased: dag_type_atom_node(identity: ^T))) } -fn tpb_type_decl_nullary_tag() -> Outcome { +fn tpb_type_decl_nullary_tag() -> Outcome { tpb_assemble(src: "module p\n\ntype Tag = A | B\n") } diff --git a/src/v2/test/compiler/pipeline/stage_bridge.dag b/src/v2/test/compiler/pipeline/stage_bridge.dag index 251550c585e..ed668e38e2d 100644 --- a/src/v2/test/compiler/pipeline/stage_bridge.dag +++ b/src/v2/test/compiler/pipeline/stage_bridge.dag @@ -1,5 +1,6 @@ module v2.test.compiler.pipeline.stage_bridge +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import v2.compiler.normalized_tree { NormalizedTree } import v2.compiler.infer { InferredTree } @@ -128,8 +129,8 @@ fn pipeline_resolved_source(source: String, file: Symbol) -> Outcome { fn pipeline_inferred_arrow_from_resolved(resolved: Node) -> Outcome { match pipeline_find_arrow_in_module(root: resolved) { - Present { value: arrow } => infer_and_discharge(tree: arrow) - Absent => infer_and_discharge(tree: resolved) + Present { value: arrow } => infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: arrow)) + Absent => infer_and_discharge(tree: claim_resolved_tree_without_declarations(root: resolved)) } } diff --git a/src/v2/test/lens_application/rejecting_lens_blocks_before_compile_test.dag b/src/v2/test/lens_application/rejecting_lens_blocks_before_compile_test.dag index 055fe2f8168..bd5d7e3cf7d 100644 --- a/src/v2/test/lens_application/rejecting_lens_blocks_before_compile_test.dag +++ b/src/v2/test/lens_application/rejecting_lens_blocks_before_compile_test.dag @@ -1,5 +1,6 @@ module v2.test.lens_application.rejecting_lens_blocks_before_compile +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import std.occurrence_identity { OccurrenceSynthetic } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } import std.decl_ref { decl_ref } @@ -66,7 +67,7 @@ data rejecting_lens_kernel_ambient_source: Node = Node { test fn rejecting_lens_blocks_before_compile_claim_holds() -> Bool { match validate_then_compile( - source: rejecting_lens_kernel_ambient_source, + source: claim_resolved_tree_without_declarations(root: rejecting_lens_kernel_ambient_source), lenses: [rejecting_lens], mode: TranslateTo { target: rejecting_lens_target_model_stub } ) { diff --git a/src/v2/test/lens_common/infer_fixture.dag b/src/v2/test/lens_common/infer_fixture.dag index 3e27c51817d..4d0a9f887ca 100644 --- a/src/v2/test/lens_common/infer_fixture.dag +++ b/src/v2/test/lens_common/infer_fixture.dag @@ -1,6 +1,8 @@ module v2.test.lens_common.infer_fixture import std.occurrence_identity { OccurrenceSynthetic } +import v2.compiler.resolve { ResolvedTree } +import v2.std.symbol_index { empty_symbol_index } import v2.compiler.infer { DerivedGrounding, InferredFacts, InferredTree, infer_facts_lookup_miss_diagnostic } import v2.std.cardinality { RankingComponent, TerminationProof } import v2.std.collection { Map } @@ -12,6 +14,14 @@ import v2.std.node { Atom, Node, Symbol, TypeNode } import v2.std.optional { Present } import v2.std.witness { Holds, StructuralPropertyWitness, Witness, witness_from_optional } +// A HAND-BUILT TREE SUPPLIED AT INFER'S INTERFACE (DESIGN section 3: a witness supplies its input +// rather than executing the layers beneath it). infer takes resolve's output, which carries the index +// resolution consulted; a supplied tree was never resolved, so it carries an index holding NO +// declarations -- the name says so, and a declaration lookup through it finds nothing and refuses. +fn claim_resolved_tree_without_declarations(root: Node) -> ResolvedTree { + ResolvedTree { root: root, symbol_index: empty_symbol_index() } +} + fn claim_atom_node(s: Symbol) -> Node { Node { kind: TypeNode { connective: Atom { identity: s } }, diff --git a/src/v2/test/lens_fact_density/hollow_alias_nested_rejected_test.dag b/src/v2/test/lens_fact_density/hollow_alias_nested_rejected_test.dag index 313cb6850c8..ef22d862c53 100644 --- a/src/v2/test/lens_fact_density/hollow_alias_nested_rejected_test.dag +++ b/src/v2/test/lens_fact_density/hollow_alias_nested_rejected_test.dag @@ -9,7 +9,7 @@ import v2.compiler.compile { import v2.std.diagnostic { Accepted, Rejected } import v2.std.logic { Bool } import v2.std.node { Atom, Conj, Edge, Named, Node, Symbol, TypeNode } -import v2.test.lens_common.infer_fixture { claim_atom_node } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations, claim_atom_node } import v2.test.lens_application.empty_required_lenses_skip_gate { non_empty_diagnostics_contain_reason } @@ -35,7 +35,7 @@ data hollow_alias_nested_authority: Node = claim_atom_node(s: ^hollow_alias_nest test fn hollow_alias_nested_rejected_holds() -> Bool { match validate_then_compile( - source: hollow_alias_nested_root, + source: claim_resolved_tree_without_declarations(root: hollow_alias_nested_root), lenses: [], mode: Eval { runtime: hollow_alias_nested_root } ) { diff --git a/src/v2/test/lens_fact_density/hollow_alias_vtc_empty_lenses_rejected_test.dag b/src/v2/test/lens_fact_density/hollow_alias_vtc_empty_lenses_rejected_test.dag index f0e1faed9ad..b83d01fa0ad 100644 --- a/src/v2/test/lens_fact_density/hollow_alias_vtc_empty_lenses_rejected_test.dag +++ b/src/v2/test/lens_fact_density/hollow_alias_vtc_empty_lenses_rejected_test.dag @@ -9,7 +9,7 @@ import v2.compiler.compile { import v2.std.diagnostic { Accepted, Rejected } import v2.std.logic { Bool } import v2.std.node { Atom, Node, Symbol, TypeNode } -import v2.test.lens_common.infer_fixture { claim_atom_node } +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations, claim_atom_node } import v2.test.lens_application.empty_required_lenses_skip_gate { non_empty_diagnostics_contain_reason } @@ -24,7 +24,7 @@ data hollow_alias_el_authority: Node = claim_atom_node(s: ^hollow_alias_el_symbo test fn hollow_alias_vtc_empty_lenses_rejected_holds() -> Bool { match validate_then_compile( - source: hollow_alias_el_root, + source: claim_resolved_tree_without_declarations(root: hollow_alias_el_root), lenses: [], mode: Eval { runtime: hollow_alias_el_root } ) { diff --git a/src/v2/workflow/dag_acceptance.dag b/src/v2/workflow/dag_acceptance.dag index da6340baf8d..af649fb5f62 100644 --- a/src/v2/workflow/dag_acceptance.dag +++ b/src/v2/workflow/dag_acceptance.dag @@ -40,6 +40,7 @@ import v2.std.logic { Bool } import v2.std.node { Node, Symbol, node_subtree_count } import v2.std.optional { Absent, Optional, Present, optional_absent, optional_present } import v2.compiler.refinement_discharge { infer_and_discharge } +import v2.compiler.resolve { ResolvedTree } // STAGES MINT EVIDENCE, A CONTRACT MINTS ACCEPTANCE. Given a candidate .dag SOURCE STRING this // authority answers how far it got and why it stopped, as typed per-stage evidence adjudicated by a @@ -455,7 +456,7 @@ type TranslationOutputRow { type AcceptanceRunState { rows: List, - resolved: Optional, + resolved: Optional, inferred: Optional, translations: List, spent: Millisecond, @@ -584,7 +585,7 @@ fn front_end_declared_cost( // individually would be a second story about how the work is performed: they run inside one staged // fold, so a per-stage refusal after the fold ran would report a saving never made. -fn front_end_run_resolved(run: FrontEndRun) -> Optional { +fn front_end_run_resolved(run: FrontEndRun) -> Optional { match run.completion { FrontEndResolvedModule { resolved: n } => optional_present(value: n) FrontEndBoundReached { last: _ } => optional_absent() diff --git a/src/v2/workflow/realization_attempt.dag b/src/v2/workflow/realization_attempt.dag index ac81184cb80..cffc39a8e19 100644 --- a/src/v2/workflow/realization_attempt.dag +++ b/src/v2/workflow/realization_attempt.dag @@ -2,6 +2,7 @@ module v2.workflow.realization_attempt import v2.compiler.ingested_fixture_arrows { ingested_resolved_module_from_source } import v2.compiler.program_assembly { assemble_program_from_ingest } +import v2.compiler.resolve { ResolvedTree } import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest } import v2.compiler.name_resolve { Admission, ResolutionSubject, Import, ImportVisible } import v2.compiler.infer { InferredTree } @@ -154,7 +155,7 @@ fn attempt_entry_source(entry: String, source: String) -> EntryRealizationAttemp located: first_located_file(ds: ds) ) Accepted { value: resolved, diagnostics: _ } => { - let arrows = collect_arrows(root: resolved, acc: []) + let arrows = collect_arrows(root: resolved.root, acc: []) if length(xs: arrows) == 0 { attempt_refused(entry: entry, phase: PhaseTranslate, cause: ^realization_attempt_no_arrow_declarations) } else { @@ -273,8 +274,9 @@ fn phase_for_reason(reason: Symbol, fallback: RealizationPhase) -> RealizationPh } } -fn attempt_joined(program: Node, fn_name: Symbol, entry: String) -> EntryRealizationAttempt { - let joined = decl_edges_named(root: program, fn_name: fn_name, acc: []) +// decl is a subtree of the resolved program, resolved under the program's own index. +fn attempt_joined(program: ResolvedTree, fn_name: Symbol, entry: String) -> EntryRealizationAttempt { + let joined = decl_edges_named(root: program.root, fn_name: fn_name, acc: []) if length(xs: joined) == 0 { attempt_refused(entry: entry, phase: PhaseResolve, cause: ^realization_attempt_identity_absent) } else if length(xs: joined) > 1 { @@ -283,7 +285,7 @@ fn attempt_joined(program: Node, fn_name: Symbol, entry: String) -> EntryRealiza match list_at_optional(xs: joined, index: 0) { Absent => attempt_refused(entry: entry, phase: PhaseResolve, cause: ^realization_attempt_identity_absent) Present { value: decl } => - match infer_and_discharge(tree: decl) { + match infer_and_discharge(tree: ResolvedTree { root: decl, symbol_index: program.symbol_index }) { Rejected { diagnostics: ds } => attempt_refused_at(entry: entry, phase: PhaseInfer, cause: first_located_cause(ds: ds), located: first_located_file(ds: ds)) Accepted { value: inferred, diagnostics: _ } => From 95856efdaf9328db8ca299fe747232084b8328cb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 19:34:15 +0000 Subject: [PATCH 05/15] pick_ingested: the arrow extractor returns the arrow Node (my retype over-reached) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../pick_ingested_structural_lowering_test.dag | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag b/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag index fee53ce956c..ea85b998247 100644 --- a/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag +++ b/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag @@ -282,7 +282,7 @@ fn pick_ingested_resolved_module_from_source(source: String) -> Outcome Outcome { +fn pick_ingested_arrow_from_source(source: String) -> Outcome { bind_outcome( o: pick_ingested_resolved_module_from_source(source: source), f: fn(resolved) { @@ -409,7 +409,7 @@ test fn pick_ingested_pick_true_executes_holds() -> Bool { Accepted { value: arrow, diagnostics: _ } => pick_eval_run_passes( run: pick_eval_run( - callee: arrow.root, + callee: arrow, expected_lexeme: "1" ) ) @@ -422,7 +422,7 @@ test fn pick_ingested_pick_false_executes_holds() -> Bool { Accepted { value: arrow, diagnostics: _ } => pick_eval_run_passes( run: pick_eval_run( - callee: arrow.root, + callee: arrow, expected_lexeme: "2" ) ) @@ -435,7 +435,7 @@ test fn pick_ingested_swapped_arms_red_holds() -> Bool { Accepted { value: arrow, diagnostics: _ } => pick_eval_run_passes( run: pick_eval_run( - callee: arrow.root, + callee: arrow, expected_lexeme: "1" ) ) == false @@ -466,7 +466,7 @@ test fn pick2_ingested_pick_true_executes_holds() -> Bool { Accepted { value: arrow, diagnostics: _ } => pick_eval_run_passes( run: pick_eval_run( - callee: arrow.root, + callee: arrow, expected_lexeme: "3" ) ) @@ -479,7 +479,7 @@ test fn pick2_ingested_pick_false_executes_holds() -> Bool { Accepted { value: arrow, diagnostics: _ } => pick_eval_run_passes( run: pick_eval_run( - callee: arrow.root, + callee: arrow, expected_lexeme: "4" ) ) @@ -492,7 +492,7 @@ test fn pick2_ingested_swapped_arms_red_holds() -> Bool { Accepted { value: arrow, diagnostics: _ } => pick_eval_run_passes( run: pick_eval_run( - callee: arrow.root, + callee: arrow, expected_lexeme: "3" ) ) == false From 1c0fe0d9ce9f08985878287994d906d8e57b9c76 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 19:51:03 +0000 Subject: [PATCH 06/15] infer: drop the unused tree parameter from infer_bind_annotation_check (review 71857) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index e221e776770..967bbc5a22d 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -2475,7 +2475,7 @@ fn infer_gather_application_row_on_entries( // not derived leaves the check unjudged and the Bind on the counted frontier, as an unannotated Bind // is: the check is neither admitted nor skipped silently. -fn infer_bind_annotation_check(node: Node, entries: List, tree: Node, symbol_index: SymbolIndex) -> Outcome { +fn infer_bind_annotation_check(node: Node, entries: List, symbol_index: SymbolIndex) -> Outcome { match type_annotation_optional(n: node) { Absent => outcome_accepted(true) Present { value: annotation } => @@ -2528,7 +2528,7 @@ fn infer_gather_bind_annotation_row_on_entries( partials: List, tree: Node, symbol_index: SymbolIndex, ) -> InferGatherFoldAcc { - match infer_bind_annotation_check(node: node, entries: entries, tree: tree, symbol_index: symbol_index) { + match infer_bind_annotation_check(node: node, entries: entries, symbol_index: symbol_index) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, From f88aa3a3e5ed25ee5a199d1882828e9d0d1dd1c7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 20:21:50 +0000 Subject: [PATCH 07/15] infer: thread symbol_index through the gather step call the carrier merge brought in Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index c95f7c4f37c..1d1c0b1a581 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -3096,7 +3096,7 @@ fn infer_gather_fold_step( merged_entries: acc.entries, merged_pending: acc.pending, partials: partials, - tree: tree + tree: tree, symbol_index: symbol_index ) } else if child.failed { infer_gather_fold_acc_failed( From 86ac631119ff994b92fa8ccd7cc2c5a4ad94f2c6 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 21:11:43 +0000 Subject: [PATCH 08/15] infer: drop the unused tree parameter from infer_transform_cast_optional (review 71891) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 1d1c0b1a581..1f945f06c12 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -2675,7 +2675,7 @@ fn infer_transform_derived_optional( if infer_transform_is_binary_infix_int_add_shape(node: node) { optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, tree: tree)) } else { - infer_transform_cast_optional(node: node, entries: entries, tree: tree, symbol_index: symbol_index) + infer_transform_cast_optional(node: node, entries: entries, symbol_index: symbol_index) } } @@ -2692,7 +2692,7 @@ fn infer_transform_is_cast(node: Node) -> Bool { } } -fn infer_transform_cast_optional(node: Node, entries: List, tree: Node, symbol_index: SymbolIndex) -> Optional> { +fn infer_transform_cast_optional(node: Node, entries: List, symbol_index: SymbolIndex) -> Optional> { if !infer_transform_is_cast(node: node) { optional_absent() } else { From 6d321206a4c0962746c3914c44dfe1e8bd5a57d9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 28 Sep 2026 02:33:31 +0000 Subject: [PATCH 09/15] infer: thread ResolvedTree whole as 'resolved'; parameter scope search frozen as a declared frontier (neat-boar-16 ruling) Every infer function that took tree: Node (plus the separate symbol_index) now takes resolved: ResolvedTree and reads resolved.root / resolved.symbol_index. infer_parameter_scope_search stays FROZEN (no new callers or arms): a frame-bound parameter reference reaches infer as a bare canonical_atom with no path, so the index cannot key it; the trigger is on the carrier comment. infer_branch_operand_resolved_type no longer passes its operand as a fake tree: it states the literal-else-facts result that call always produced. Row 16 (positive(x: Int) beside f(x: Pos)) is the ruling's required control. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 154 ++++++++++++---------- src/v2/test/claim/body_cast_node_test.dag | 4 +- 2 files changed, 88 insertions(+), 70 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 1f945f06c12..dd25321a078 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -705,7 +705,7 @@ fn infer_product_facts_from_entries( } } -fn infer_node_facts(n: Node, partials: List, tree: Node) -> Outcome { +fn infer_node_facts(n: Node, partials: List, resolved: ResolvedTree) -> Outcome { match infer_bounded_lattice_consumer_gate(consumer: n, partials: partials) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: _, diagnostics: cd } => @@ -753,7 +753,7 @@ fn infer_node_facts(n: Node, partials: List, tree: Node) -> Outcome - match infer_parameter_type_in_scope(tree: tree, reference: n, binding: binding) { + match infer_parameter_type_in_scope(tree: resolved.root, reference: n, binding: binding) { Present { value: domain_ty } => inferred_facts_from_derived_type( node: n, @@ -954,7 +954,13 @@ fn infer_arrow_domain_type_for_binding(arrow: Node, binding: Symbol) -> Optional // occurrence identity) and each Arrow on the way back up binds it if its domain names it. // Consumers: infer_node_facts' parameter arm (the grounding every cast, add, application, branch, // match and loop operand reads) and infer_branch_operand_resolved_type_in_tree. -// interim: dissolve-on the SymbolIndex / ResolvedTree.bindings lookup, as before. +// FROZEN, A DECLARED FRONTIER (neat-boar-16 ruling): no new callers and no new arms. A declaration +// reference is answered by v2.std.symbol_index symbol_index_lookup on the ResolvedTree infer receives +// (refinement_declaration), but a frame-bound parameter reference reaches infer as a bare +// canonical_atom with no path (v2.compiler.resolve, the BoundInFrame arm), so this walk still scopes +// it. NEXT TRIGGER, NAMING THE CAPABILITY: resolve emits every frame-bound parameter reference as a +// declaration reference keyed in SymbolIndex, and eval + translate bind through it -- then this search +// and infer_parameter_type_in_scope are deleted. type InferParameterScopeSearch = ParameterReferenceNotHere | ParameterReferenceUnbound @@ -1051,7 +1057,7 @@ fn refinement_declared_carrier(index: SymbolIndex, source_type: Node) -> Optiona fn infer_branch_operand_resolved_type_in_tree( node: Node, facts: InferredFacts, - tree: Node, + resolved: ResolvedTree, ) -> Witness { match dag_canonical_literal_from_node(node: node) { Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } => @@ -1061,7 +1067,7 @@ fn infer_branch_operand_resolved_type_in_tree( Rejected { diagnostics: _ } => match infer_atom_binding_sym(node: node) { Present { value: binding } => - match infer_parameter_type_in_scope(tree: tree, reference: node, binding: binding) { + match infer_parameter_type_in_scope(tree: resolved.root, reference: node, binding: binding) { Present { value: domain_ty } => Holds { value: domain_ty } Absent => inferred_facts_resolved_type(facts: facts) } @@ -1070,8 +1076,18 @@ fn infer_branch_operand_resolved_type_in_tree( } } +// The operand's type with no enclosing tree: a literal's own type, else the operand's inferred facts. +// It has no parameter arm -- the previous spelling passed the operand as its own tree, where the +// scope search can never bind (the reference is the root), so this states that result directly +// rather than handing a node to a ResolvedTree position it never came from. fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Witness { - infer_branch_operand_resolved_type_in_tree(node: node, facts: facts, tree: node) + match dag_canonical_literal_from_node(node: node) { + Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } => + Holds { value: bool_node() } + Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } => + Holds { value: infer_branch_int_binding_type_node() } + Rejected { diagnostics: _ } => inferred_facts_resolved_type(facts: facts) + } } fn inferred_facts_from_derived_type( @@ -1443,7 +1459,7 @@ fn infer_match_bool( node: Node, partials: List, entries: List, - tree: Node, + resolved: ResolvedTree, ) -> Outcome { let positional_targets = node_positional_child_targets(node: node) if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { @@ -1467,7 +1483,7 @@ fn infer_match_bool( match infer_branch_operand_resolved_type_in_tree( node: scrutinee_target, facts: scrutinee_facts, - tree: tree + resolved: resolved ) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: scrutinee_type } => @@ -1641,15 +1657,15 @@ fn infer_unify_transform_operand_types( left_facts: InferredFacts, right_node: Node, right_facts: InferredFacts, - tree: Node, + resolved: ResolvedTree, ) -> Outcome { - match infer_branch_operand_resolved_type_in_tree(node: left_node, facts: left_facts, tree: tree) { + match infer_branch_operand_resolved_type_in_tree(node: left_node, facts: left_facts, resolved: resolved) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: left_type } => match infer_branch_operand_resolved_type_in_tree( node: right_node, facts: right_facts, - tree: tree + resolved: resolved ) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: right_type } => @@ -2023,7 +2039,7 @@ fn infer_transform_binary_infix( node: Node, partials: List, entries: List, - tree: Node, + resolved: ResolvedTree, ) -> Outcome { let positional_targets = node_positional_child_targets(node: node) if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { @@ -2056,7 +2072,7 @@ fn infer_transform_binary_infix( left_facts: left_facts, right_node: right_target, right_facts: right_facts, - tree: tree + resolved: resolved ) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: unified_type, diagnostics: ud } => @@ -2219,9 +2235,9 @@ fn infer_gather_match_row_on_entries( entries: List, pending: Diagnostics, partials: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { - match infer_match_bool(node: node, partials: partials, entries: entries, tree: tree) { + match infer_match_bool(node: node, partials: partials, entries: entries, resolved: resolved) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2314,9 +2330,9 @@ fn infer_gather_transform_frontier_on_entries( entries: List, pending: Diagnostics, partials: List, - tree: Node, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { - match infer_node_facts(n: node, partials: partials, tree: tree) { + match infer_node_facts(n: node, partials: partials, resolved: resolved) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2377,11 +2393,11 @@ fn infer_type_equal_ignoring_provenance(a: Node, b: Node) -> Bool { exact_structural_equality_zip_fold(source_facts: a, candidate: b) } -fn infer_list_element_type(element: Node, entries: List, tree: Node) -> Outcome { +fn infer_list_element_type(element: Node, entries: List, resolved: ResolvedTree) -> Outcome { match lookup_inferred_facts_in_entries(entries: entries, key: element) { Absent => outcome_rejected(infer_facts_lookup_miss_diagnostic(key: element)) Present { value: facts } => - match infer_branch_operand_resolved_type_in_tree(node: element, facts: facts, tree: tree) { + match infer_branch_operand_resolved_type_in_tree(node: element, facts: facts, resolved: resolved) { Violates { diagnostic: d } => outcome_rejected(d) Holds { value: t } => outcome_accepted(value: t) } @@ -2393,16 +2409,16 @@ fn infer_list_element_type(element: Node, entries: List, tre fn infer_list_elements_unified_type( elements: List, entries: List, - tree: Node + resolved: ResolvedTree ) -> Optional> { match elements { Empty => Absent Cons { head: first, tail: rest } => Present { - value: bind_outcome(o: infer_list_element_type(element: first, entries: entries, tree: tree), f: fn(t) { + value: bind_outcome(o: infer_list_element_type(element: first, entries: entries, resolved: resolved), f: fn(t) { fold(rest, init: outcome_accepted(value: t), f: fn(acc, element) { bind_outcome(o: acc, f: fn(unified) { - bind_outcome(o: infer_list_element_type(element: element, entries: entries, tree: tree), f: fn(et) { + bind_outcome(o: infer_list_element_type(element: element, entries: entries, resolved: resolved), f: fn(et) { if infer_type_equal_ignoring_provenance(a: unified, b: et) { outcome_accepted(value: unified) } else { @@ -2432,9 +2448,9 @@ fn infer_transform_freemonoid_introduction( node: Node, elements: List, entries: List, - tree: Node + resolved: ResolvedTree ) -> Optional> { - match infer_list_elements_unified_type(elements: elements, entries: entries, tree: tree) { + match infer_list_elements_unified_type(elements: elements, entries: entries, resolved: resolved) { Absent => Absent Present { value: unified } => Present { @@ -2458,15 +2474,15 @@ fn infer_gather_transform_row_on_entries( entries: List, pending: Diagnostics, partials: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { match list_introduction_elements_optional(node: node) { Absent => - infer_gather_application_row_on_entries(node: node, entries: entries, pending: pending, partials: partials, tree: tree, symbol_index: symbol_index) + infer_gather_application_row_on_entries(node: node, entries: entries, pending: pending, partials: partials, resolved: resolved) Present { value: elements } => - match infer_transform_freemonoid_introduction(node: node, elements: elements, entries: entries, tree: tree) { + match infer_transform_freemonoid_introduction(node: node, elements: elements, entries: entries, resolved: resolved) { Absent => - infer_gather_transform_frontier_on_entries(node: node, entries: entries, pending: pending, partials: partials, tree: tree) + infer_gather_transform_frontier_on_entries(node: node, entries: entries, pending: pending, partials: partials, resolved: resolved) Present { value: introduced } => match introduced { Rejected { diagnostics: r } => @@ -2513,7 +2529,7 @@ fn infer_gather_application_row_on_entries( entries: List, pending: Diagnostics, partials: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { match infer_application_argument_inhabitance(node: node, entries: entries) { Rejected { diagnostics: r } => @@ -2528,7 +2544,7 @@ fn infer_gather_application_row_on_entries( ) Accepted { value: _, diagnostics: id } => let merged_pending = diagnostics_merge(outer: pending, inner: id) - match infer_transform_derived_optional(node: node, partials: partials, entries: entries, tree: tree, symbol_index: symbol_index) { + match infer_transform_derived_optional(node: node, partials: partials, entries: entries, resolved: resolved) { Present { value: derived } => match derived { Rejected { diagnostics: r } => @@ -2575,7 +2591,7 @@ fn infer_gather_application_row_on_entries( entries: entries, pending: merged_pending, partials: partials, - tree: tree + resolved: resolved ) } } @@ -2589,7 +2605,7 @@ fn infer_gather_application_row_on_entries( // not derived leaves the check unjudged and the Bind on the counted frontier, as an unannotated Bind // is: the check is neither admitted nor skipped silently. -fn infer_bind_annotation_check(node: Node, entries: List, symbol_index: SymbolIndex) -> Outcome { +fn infer_bind_annotation_check(node: Node, entries: List, resolved: ResolvedTree) -> Outcome { match type_annotation_optional(n: node) { Absent => outcome_accepted(true) Present { value: annotation } => @@ -2605,7 +2621,7 @@ fn infer_bind_annotation_check(node: Node, entries: List, sy match coercion_cast_crossing( source: g, source_type: g.witness.structural.evidence, - source_declared_carrier: refinement_declared_carrier(index: symbol_index, source_type: g.witness.structural.evidence), + source_declared_carrier: refinement_declared_carrier(index: resolved.symbol_index, source_type: g.witness.structural.evidence), target: annotation ) { Accepted { value: _, diagnostics: d } => Accepted { value: true, diagnostics: d } @@ -2640,9 +2656,9 @@ fn infer_gather_bind_annotation_row_on_entries( entries: List, pending: Diagnostics, partials: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { - match infer_bind_annotation_check(node: node, entries: entries, symbol_index: symbol_index) { + match infer_bind_annotation_check(node: node, entries: entries, resolved: resolved) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -2659,7 +2675,7 @@ fn infer_gather_bind_annotation_row_on_entries( entries: entries, pending: diagnostics_merge(outer: pending, inner: d), partials: partials, - tree: tree + resolved: resolved ) } } @@ -2670,12 +2686,12 @@ fn infer_transform_derived_optional( node: Node, partials: List, entries: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> Optional> { if infer_transform_is_binary_infix_int_add_shape(node: node) { - optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, tree: tree)) + optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, resolved: resolved)) } else { - infer_transform_cast_optional(node: node, entries: entries, symbol_index: symbol_index) + infer_transform_cast_optional(node: node, entries: entries, resolved: resolved) } } @@ -2692,7 +2708,7 @@ fn infer_transform_is_cast(node: Node) -> Bool { } } -fn infer_transform_cast_optional(node: Node, entries: List, symbol_index: SymbolIndex) -> Optional> { +fn infer_transform_cast_optional(node: Node, entries: List, resolved: ResolvedTree) -> Optional> { if !infer_transform_is_cast(node: node) { optional_absent() } else { @@ -2712,7 +2728,7 @@ fn infer_transform_cast_optional(node: Node, entries: List, o: coercion_cast_crossing( source: g, source_type: g.witness.structural.evidence, - source_declared_carrier: refinement_declared_carrier(index: symbol_index, source_type: g.witness.structural.evidence), + source_declared_carrier: refinement_declared_carrier(index: resolved.symbol_index, source_type: g.witness.structural.evidence), target: target ), f: fn(crossed) { @@ -2740,13 +2756,13 @@ fn infer_transform_cast_optional(node: Node, entries: List, // added without deciding, at this site, whether it derives its type or joins the counted frontier // -- never defaulted into by omission (DESIGN §4 closed vocabulary, §5 unwritable-by-construction). -fn infer_gather_fold_not_derived(n: Node, partials: List, tree: Node) -> InferGatherFoldAcc { +fn infer_gather_fold_not_derived(n: Node, partials: List, resolved: ResolvedTree) -> InferGatherFoldAcc { infer_gather_transform_frontier_on_entries( node: n, entries: empty_inferred_facts_entry_list(), pending: None, partials: partials, - tree: tree + resolved: resolved ) } @@ -2758,7 +2774,7 @@ fn infer_gather_fold_not_derived(n: Node, partials: List, tree: Node) -> I // -- a grounding this fold does not derive -- and it takes that arm. Deriving the reference's type // FROM its declaration by path is the end-state the roster lookups above already name as their // dissolution, not this arm. -fn infer_gather_fold_init(n: Node, partials: List, tree: Node, symbol_index: SymbolIndex) -> InferGatherFoldAcc { +fn infer_gather_fold_init(n: Node, partials: List, resolved: ResolvedTree) -> InferGatherFoldAcc { match n.kind { ComputationNode { behavior: Branch } => infer_gather_fold_acc_ok( @@ -2793,7 +2809,7 @@ fn infer_gather_fold_init(n: Node, partials: List, tree: Node, symbol_inde await_transform_row: false, children_remaining: length(xs: n.children) ) - ComputationNode { behavior: Value } => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + ComputationNode { behavior: Value } => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) ComputationNode { behavior: Transform } => if length(xs: n.children) == 0 { infer_gather_transform_row_on_entries( @@ -2801,7 +2817,7 @@ fn infer_gather_fold_init(n: Node, partials: List, tree: Node, symbol_inde entries: empty_inferred_facts_entry_list(), pending: None, partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) } else { infer_gather_fold_acc_ok( @@ -2828,12 +2844,12 @@ fn infer_gather_fold_init(n: Node, partials: List, tree: Node, symbol_inde await_transform_row: false, children_remaining: length(xs: n.children) ) - Absent => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + Absent => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) } - TypeNode { connective: Atom { identity: _ } } => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + TypeNode { connective: Atom { identity: _ } } => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) TypeNode { connective: Conj } => match declaration_reference_path_optional(node: n) { - Present { value: _ } => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + Present { value: _ } => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) Absent => if infer_type_node_awaits_product_row(n: n) { infer_gather_fold_acc_ok( @@ -2847,10 +2863,10 @@ fn infer_gather_fold_init(n: Node, partials: List, tree: Node, symbol_inde children_remaining: length(xs: n.children) ) } else { - infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) } } - TypeNode { connective: Disj } => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + TypeNode { connective: Disj } => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) TypeNode { connective: Arrow } => if infer_type_node_awaits_product_row(n: n) { infer_gather_fold_acc_ok( @@ -2864,10 +2880,10 @@ fn infer_gather_fold_init(n: Node, partials: List, tree: Node, symbol_inde children_remaining: length(xs: n.children) ) } else { - infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) } - TypeNode { connective: Cardinality } => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) - TypeNode { connective: Instantiation } => infer_gather_fold_not_derived(n: n, partials: partials, tree: tree) + TypeNode { connective: Cardinality } => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) + TypeNode { connective: Instantiation } => infer_gather_fold_not_derived(n: n, partials: partials, resolved: resolved) } } @@ -3086,7 +3102,7 @@ fn infer_gather_fold_step( edge: Edge, child: InferGatherFoldAcc, partials: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { if acc.failed { acc @@ -3096,7 +3112,7 @@ fn infer_gather_fold_step( merged_entries: acc.entries, merged_pending: acc.pending, partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) } else if child.failed { infer_gather_fold_acc_failed( @@ -3129,7 +3145,7 @@ fn infer_gather_fold_step( merged_entries: list_snoc_item(xs: acc.entries, item: domain_entry), merged_pending: acc.pending, partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) } } else if infer_literal_edge_diagnostics_derived(parent: acc.node, edge: edge) { @@ -3150,7 +3166,7 @@ fn infer_gather_fold_step( merged_entries: concat_inferred_facts_entries(a: acc.entries, b: payload_entries), merged_pending: acc.pending, partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) } } else { @@ -3159,7 +3175,7 @@ fn infer_gather_fold_step( merged_entries: concat_inferred_facts_entries(a: acc.entries, b: child.entries), merged_pending: diagnostics_merge(outer: acc.pending, inner: child.pending), partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) } } @@ -3169,7 +3185,7 @@ fn infer_gather_fold_step_merged( merged_entries: List, merged_pending: Diagnostics, partials: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { let children_remaining = acc.children_remaining - 1 if acc.await_branch_row && children_remaining == 0 { @@ -3185,7 +3201,7 @@ fn infer_gather_fold_step_merged( entries: merged_entries, pending: merged_pending, partials: partials, - tree: tree + resolved: resolved ) } else if acc.await_loop_row && children_remaining == 0 { infer_gather_loop_row_on_entries( @@ -3200,10 +3216,10 @@ fn infer_gather_fold_step_merged( entries: merged_entries, pending: merged_pending, partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) } else if children_remaining == 0 { - infer_gather_settled_row(acc: acc, merged_entries: merged_entries, merged_pending: merged_pending, partials: partials, tree: tree, symbol_index: symbol_index) + infer_gather_settled_row(acc: acc, merged_entries: merged_entries, merged_pending: merged_pending, partials: partials, resolved: resolved) } else { infer_gather_fold_acc_ok( node: acc.node, @@ -3226,7 +3242,7 @@ fn infer_gather_settled_row( merged_entries: List, merged_pending: Diagnostics, partials: List, - tree: Node, symbol_index: SymbolIndex, + resolved: ResolvedTree, ) -> InferGatherFoldAcc { match type_annotation_optional(n: acc.node) { Present { value: _ } => @@ -3235,7 +3251,7 @@ fn infer_gather_settled_row( entries: merged_entries, pending: merged_pending, partials: partials, - tree: tree, symbol_index: symbol_index + resolved: resolved ) Absent => if infer_gather_acc_awaits_product_row(node: acc.node, entries: merged_entries) { @@ -3260,13 +3276,13 @@ fn infer_gather_settled_row( } } -fn infer_gather_fold_algebra(partials: List, tree: Node, symbol_index: SymbolIndex) -> NodeFold { +fn infer_gather_fold_algebra(partials: List, resolved: ResolvedTree) -> NodeFold { NodeFold { init: fn(n0) { - infer_gather_fold_init(n: n0, partials: partials, tree: tree, symbol_index: symbol_index) + infer_gather_fold_init(n: n0, partials: partials, resolved: resolved) }, step: fn(acc, e, child) { - infer_gather_fold_step(acc: acc, edge: e, child: child, partials: partials, tree: tree, symbol_index: symbol_index) + infer_gather_fold_step(acc: acc, edge: e, child: child, partials: partials, resolved: resolved) } } } @@ -3278,7 +3294,7 @@ fn infer_grounding_admits_infer_facts(grounding: CanonicalGrounding) -> Bool { fn infer_entries_for_tree(tree: ResolvedTree) -> Outcome> { let partials = partial_bounded_lattice_instances_in_tree(tree: tree.root) infer_gather_acc_to_outcome( - acc: fold_node(n: tree.root, algebra: infer_gather_fold_algebra(partials: partials, tree: tree.root, symbol_index: tree.symbol_index)) + acc: fold_node(n: tree.root, algebra: infer_gather_fold_algebra(partials: partials, resolved: tree)) ) } // INFER'S OUTPUT IS THE OBLIGATED FORM, never an InferredTree: v2.compiler.refinement_discharge diff --git a/src/v2/test/claim/body_cast_node_test.dag b/src/v2/test/claim/body_cast_node_test.dag index a18c9e29bf2..a2b792c5d71 100644 --- a/src/v2/test/claim/body_cast_node_test.dag +++ b/src/v2/test/claim/body_cast_node_test.dag @@ -579,7 +579,9 @@ test fn bcn_cast_between_sibling_refinements_refuses() -> Bool { bcn_supplied_refuses(o: bcn_supplied_crossing(source_leaf: ^Pos, carrier: bcn_int_type(), target: bcn_ref(leaf: ^Neg))) } -// (16) THE IDENTITY CAST INTO A REFINEMENT IS ADMITTED BY THE EXACT RULE. `x as Pos` from `x: Pos`: +// (16) THE IDENTITY CAST INTO A REFINEMENT IS ADMITTED BY THE EXACT RULE -- and the required control of +// neat-boar-16's ResolvedTree ruling: `fn positive(x: Int)` beside `fn f(x: Pos)`, where x in f must ground +// as Pos (the frozen parameter scope search), or this cast refuses. `x as Pos` from `x: Pos`: // infer grounds x as the Pos declaration-reference from f's own domain, and coercion_cast_crossing // finds the target structurally equal. The RED beside it: the same operand cast to Bool refuses // (row 15's partner), so this is a judged crossing, not the frontier passing it over. RED BEFORE From 0fb011ffc455a61052238361bdd6cd302a24b051 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 28 Sep 2026 13:38:22 +0000 Subject: [PATCH 10/15] Merge origin/main (#12379 landed); #12379's new hand-built infer inputs use the named no-declarations constructor Co-Authored-By: Claude Opus 5.5 (1M context) --- .../compiler/infer_arrow_elimination_witness_test.dag | 9 +++++---- src/v2/test/claim/refinement_discharge_test.dag | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/v2/test/claim/compiler/infer_arrow_elimination_witness_test.dag b/src/v2/test/claim/compiler/infer_arrow_elimination_witness_test.dag index d97889c2858..a9769336d3f 100644 --- a/src/v2/test/claim/compiler/infer_arrow_elimination_witness_test.dag +++ b/src/v2/test/claim/compiler/infer_arrow_elimination_witness_test.dag @@ -6,6 +6,7 @@ module v2.test.claim.compiler.infer_arrow_elimination_witness_test // infer, and the Bool control through the real evaluator: before this rule no application derived, // Int included, and eval refused both with eval_rejected_grounding_not_derived. +import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.infer { infer, inferred_facts_grounding_derived, inferred_facts_resolved_type } import v2.compiler.eval { eval, inputs_root_only } import v2.compiler.refinement_discharge { discharge_refinement_obligations } @@ -56,7 +57,7 @@ fn ae_false() -> Node { // The application's derived type, compared to the expected authority node. False when infer refuses, // the node carries no facts, or its grounding is not derived. fn ae_application_derives(tree: Node, expected: Node) -> Bool { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: _ } => false Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(tree) { @@ -72,7 +73,7 @@ fn ae_application_derives(tree: Node, expected: Node) -> Bool { } fn ae_refuses_body_return(tree: Node) -> Bool { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: nds } => diagnostics_has_reason( @@ -83,7 +84,7 @@ fn ae_refuses_body_return(tree: Node) -> Bool { } fn ae_eval(tree: Node) -> Outcome { - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: obligated, diagnostics: _ } => match discharge_refinement_obligations(t: obligated) { @@ -139,7 +140,7 @@ test fn infer_bare_arrow_with_mismatched_body_refuses_holds() -> Bool { // and the application is admitted on the frontier, never typed. test fn infer_undenoted_return_leaves_application_on_frontier_holds() -> Bool { let tree = ae_apply(returns: ^ae_undenoted_type, body: ae_true()) - match infer(tree: tree) { + match infer(tree: claim_resolved_tree_without_declarations(root: tree)) { Rejected { diagnostics: _ } => false Accepted { value: inferred, diagnostics: _ } => match inferred.facts.lookup(tree) { diff --git a/src/v2/test/claim/refinement_discharge_test.dag b/src/v2/test/claim/refinement_discharge_test.dag index bde956c52c3..1d1fd5c662c 100644 --- a/src/v2/test/claim/refinement_discharge_test.dag +++ b/src/v2/test/claim/refinement_discharge_test.dag @@ -138,7 +138,7 @@ fn rdt_unevaluable_application(body: Node) -> Node { fn rdt_discharged_unevaluable(body: Node) -> Optional> { let app = rdt_unevaluable_application(body: body) - match infer(tree: app) { + match infer(tree: claim_resolved_tree_without_declarations(root: app)) { Rejected { diagnostics: _ } => optional_absent() Accepted { value: t, diagnostics: _ } => optional_present(value: discharge_refinement_obligations(t: ObligatedInferredTree { From 2b8dc42e7d349d30b84e866c4cc5c41e04447511 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 29 Sep 2026 05:30:18 +0000 Subject: [PATCH 11/15] plain_type_decl_lowering (new from main): its assembly helpers carry ResolvedTree and walk .root Co-Authored-By: Claude Opus 5.5 (1M context) --- .../claim/body_lowering/plain_type_decl_lowering_test.dag | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/v2/test/claim/body_lowering/plain_type_decl_lowering_test.dag b/src/v2/test/claim/body_lowering/plain_type_decl_lowering_test.dag index 6a15437c628..4a418016aaa 100644 --- a/src/v2/test/claim/body_lowering/plain_type_decl_lowering_test.dag +++ b/src/v2/test/claim/body_lowering/plain_type_decl_lowering_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.body_lowering.plain_type_decl_lowering +import v2.compiler.resolve { ResolvedTree } import v2.compiler.symbol_index_fill { symbol_index_declared } import v2.std.diagnostic { Accepted, Outcome, Rejected } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -27,11 +28,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // separately, and nothing here asserts it or suppresses it. // The target the assembled tree declares under `name`: the first Named edge carrying that label. -fn ptd_declared_target(o: Outcome, name: Symbol) -> Optional { +fn ptd_declared_target(o: Outcome, name: Symbol) -> Optional { match o { Rejected { diagnostics: _ } => optional_absent() Accepted { value: root, diagnostics: _ } => - fold(node_subtree_nodes(root: root), init: optional_absent(), f: fn(acc, n) { + fold(node_subtree_nodes(root: root.root), init: optional_absent(), f: fn(acc, n) { match acc { Present { value: _ } => acc Absent => @@ -90,7 +91,7 @@ fn ptd_members_declared(t: Node) -> Bool { } } -fn ptd_verdict_of(o: Outcome, name: Symbol) -> PtdVerdict { +fn ptd_verdict_of(o: Outcome, name: Symbol) -> PtdVerdict { match ptd_declared_target(o: o, name: name) { Absent => PtdNotDeclared Present { value: t } => From c90dae33fee196472108ebcccb236afca9fb28c8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 29 Sep 2026 13:39:56 +0000 Subject: [PATCH 12/15] Merge origin/main; body_let_annotation (#12540's new rows) carries ResolvedTree Co-Authored-By: Claude Opus 5.5 (1M context) --- .../test/claim/body_let_annotation_test.dag | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/v2/test/claim/body_let_annotation_test.dag b/src/v2/test/claim/body_let_annotation_test.dag index 6fd8b10d7e5..7b67433dd84 100644 --- a/src/v2/test/claim/body_let_annotation_test.dag +++ b/src/v2/test/claim/body_let_annotation_test.dag @@ -273,11 +273,11 @@ test fn bla_infer_refuses_int_literal_ascribed_bool() -> Bool { // Each row asserts the ROUTE (the annotation is not the kernel binding, or resolve refused for this // reason) as well as the verdict. The controls are (5b), and the route row below: an undeclared // `Int` still binds the kernel type. -fn bla_declared_int_literal() -> Outcome { +fn bla_declared_int_literal() -> Outcome { tpb_assemble(src: "module p\n\ntype Int = | Mine\n\nfn f(x: Bool) -> Bool {\n let y: Int = 1\n x\n}\n") } -fn bla_declared_bool_literal() -> Outcome { +fn bla_declared_bool_literal() -> Outcome { tpb_assemble(src: "module p\n\ntype Bool = | Mine\n\nfn f(x: Int) -> Int {\n let y: Bool = true\n x\n}\n") } @@ -312,7 +312,7 @@ fn bla_source(src: String, artifact: Artifact, cu: Symbol) -> DagSourceReadWitne // Subject module p over peer modules, admitted with no admission-level imports: p's own `import` // lines are what bind the peers' names. -fn bla_assemble_with_peers(p_src: String, peers: List) -> Outcome { +fn bla_assemble_with_peers(p_src: String, peers: List) -> Outcome { assemble_program_from_ingest( ingest: Cons { head: bla_source(src: p_src, artifact: tpb_artifact, cu: ^type_param_binder_frame_cu), @@ -324,7 +324,7 @@ fn bla_assemble_with_peers(p_src: String, peers: List) -> } // p imports q's own `type Int = | Mine`. -fn bla_imported_int_literal() -> Outcome { +fn bla_imported_int_literal() -> Outcome { bla_assemble_with_peers( p_src: "module p\n\nimport q { Int }\n\nfn f(x: Bool) -> Bool {\n let y: Int = 1\n x\n}\n", peers: [bla_source(src: "module q\n\ntype Int = | Mine\n", artifact: bla_q_artifact, cu: ^body_let_annotation_q_cu)] @@ -332,7 +332,7 @@ fn bla_imported_int_literal() -> Outcome { } // p imports `Int` from two user modules: the name is ambiguous and neither is the kernel's. -fn bla_ambiguous_imported_int_literal() -> Outcome { +fn bla_ambiguous_imported_int_literal() -> Outcome { bla_assemble_with_peers( p_src: "module p\n\nimport q { Int }\nimport r { Int }\n\nfn f(x: Bool) -> Bool {\n let y: Int = 1\n x\n}\n", peers: [ @@ -345,7 +345,7 @@ fn bla_ambiguous_imported_int_literal() -> Outcome { // p imports `Int` from the two kernel declarations (v2.std.integer and std.integer, as // v2.extdeps.languages.dag dag_kernel_type_declaration_binding_optional lists them): ambiguous by // name, one kernel type by declaration. -fn bla_ambiguous_kernel_int_literal() -> Outcome { +fn bla_ambiguous_kernel_int_literal() -> Outcome { bla_assemble_with_peers( p_src: "module p\n\nimport v2.std.integer { Int }\nimport std.integer { Int }\n\nfn f(x: Bool) -> Bool {\n let y: Int = 1\n x\n}\n", peers: [ @@ -355,7 +355,7 @@ fn bla_ambiguous_kernel_int_literal() -> Outcome { ) } -fn bla_refuses_at_the_annotation(o: Outcome, inferred: Outcome) -> Bool { +fn bla_refuses_at_the_annotation(o: Outcome, inferred: Outcome) -> Bool { tpb_accepts(o: o) && match inferred { Accepted { value: _, diagnostics: _ } => false @@ -364,7 +364,7 @@ fn bla_refuses_at_the_annotation(o: Outcome, inferred: Outcome) -> B } } -fn bla_annotation_is(o: Outcome, id: Symbol) -> Bool { +fn bla_annotation_is(o: Outcome, id: Symbol) -> Bool { match bla_annotation_identity(o: o) { Present { value: s } => s == id Absent => false @@ -399,7 +399,7 @@ test fn bla_ambiguous_kernel_declarations_bind_the_kernel_type() -> Bool { // foreign declaration there while the admitted route above bound it (review 5342739525). Each row // asserts the resolve verdict and the annotation's route: the local Int/Bool bind the module's // declaration, and an undeclared Int still binds the kernel. -fn bla_single_tree_resolved(text: String) -> Outcome { +fn bla_single_tree_resolved(text: String) -> Outcome { match conservation_subject_of_text(path: "body_let_annotation_subject", text: text).normalized { Rejected { diagnostics: d } => Rejected { diagnostics: d } Accepted { value: t, diagnostics: _ } => @@ -417,15 +417,15 @@ fn bla_single_tree_admitted(text: String) -> Node { } } -fn bla_single_tree_declared_int() -> Outcome { +fn bla_single_tree_declared_int() -> Outcome { bla_single_tree_resolved(text: "module m.t\n\ntype Int = | Mine\n\nfn f(x: Bool) -> Bool {\n let y: Int = x\n x\n}\n") } -fn bla_single_tree_declared_bool() -> Outcome { +fn bla_single_tree_declared_bool() -> Outcome { bla_single_tree_resolved(text: "module m.t\n\ntype Bool = | Mine\n\nfn f(x: Int) -> Int {\n let y: Bool = x\n x\n}\n") } -fn bla_single_tree_undeclared_int() -> Outcome { +fn bla_single_tree_undeclared_int() -> Outcome { bla_single_tree_resolved(text: "module m.t\n\nfn f(x: Int) -> Int {\n let y: Int = x\n x\n}\n") } From 029efafd63d61a9e7c71fca253e13bb60ba33c59 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 29 Sep 2026 15:50:34 +0000 Subject: [PATCH 13/15] v2: lower the where-refined head as a type so resolve binds it; ResolvedTree.resolved_declarations (neat-boar-16 ruling) The head reached resolve as an unlowered dag_surface_qualified_name shell, which resolve preserves unchanged as module metadata, so a declaration's carrier was never resolved. It is now lowered through the one type-expression lowering; resolve binds it; an undeclared carrier refuses unbound. ResolvedTree gains resolved_declarations, the same module fold over the resolved root, alongside symbol_index (the index resolution consulted). The other declaration-body type positions are a declared frontier (gunbc.recurring_failure_mode declaration_body_type_shell_preserved_unresolved). Co-Authored-By: Claude Opus 5.5 (1M context) --- ...n_body_type_shell_preserved_unresolved.dag | 18 +++++++ src/v2/compiler/00_compile.dag | 3 +- src/v2/compiler/03_ingest.dag | 4 +- src/v2/compiler/03_resolve.dag | 27 +++++++++- src/v2/compiler/body_lowering_fold.dag | 38 ++++++++++---- .../claim/declaration_graft_assemble_test.dag | 52 +++++++++++++++++-- src/v2/test/lens_common/infer_fixture.dag | 2 +- src/v2/workflow/floor_pure_producer_share.dag | 7 ++- src/v2/workflow/realization_attempt.dag | 2 +- 9 files changed, 130 insertions(+), 23 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/declaration_body_type_shell_preserved_unresolved.dag diff --git a/dag/gunbc/recurring_failure_mode/declaration_body_type_shell_preserved_unresolved.dag b/dag/gunbc/recurring_failure_mode/declaration_body_type_shell_preserved_unresolved.dag new file mode 100644 index 00000000000..fb4279d7094 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/declaration_body_type_shell_preserved_unresolved.dag @@ -0,0 +1,18 @@ +module gunbc.recurring_failure_mode.declaration_body_type_shell_preserved_unresolved + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data declaration_body_type_shell_preserved_unresolved: RecurringFailureMode = RecurringFailureMode { + identity: "declaration_body_type_shell_preserved_unresolved" as NonEmptyStr, + receipts: [ + "INVALID STATE: a type reference inside a type DECLARATION's body reaches v2 resolve as an unlowered dag_surface_qualified_name parse shell, and resolve preserves that shell UNCHANGED as module metadata (`v2.extdeps.languages.dag` `dag_resolve_preserve_module_metadata_subtree`), so the declaration names its type in a vocabulary no stage resolved. HARM: a carrier nothing declares is accepted silently, and a consumer comparing the declaration's type with a resolved type sees two vocabularies for one type: the Widened refinement-to-carrier cast (gunbc#12407) refused `x as Int` from `x: Pos` once main lowered kernel spellings by declaration.", + "DISTINGUISHING FACT, MEASURED: on the resolved tree, a where-refined head that body lowering hands resolve as a plain type atom IS resolved (`Int` becomes the kernel binding); the same head left as the parse shell is not. So the boundary is LOWERING, not resolve: every declaration-body type position must be lowered before resolve, and resolve then binds it through its one producer, `v2.compiler.resolve` `resolved_reference_node` (a `std.decl_ref` `DeclarationRef`-carrying declaration reference for a corpus type, the kernel atom for a kernel spelling).", + "RUNG FOUND AT: silent on every declaration-body type position. RUNG NOW: structurally guaranteed for the where-refined head only: `v2.compiler.body_lowering_fold` `body_lower_type_variant` lowers it through `body_lower_type_expr_lowered_optional`, an unreadable head refuses at the head, and resolve binds it (RED: `v2.test.claim.declaration_graft_assemble` `declaration_graft_where_alias_over_an_undeclared_carrier_refuses`; control: `declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations`, read through `v2.compiler.resolve` `ResolvedTree` `resolved_declarations`). Step-0 census before the change: every where-refined head in the corpus is a plain type name, so none regressed. DECLARED FRONTIER: the alias right-hand side, record field types and variant payload types are the same defect and remain unresolved. CEILING: structurally guaranteed (a decidable, fully modeled class). NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: every declaration-body type position is lowered before resolve, so resolve binds each one and `resolved_declarations` carries it resolved. SIBLING: quiet-hawk-702's v1 cause 1b (gunbc#12612: v1 `Node.declaration`, written by v1 resolve for declaration-field references), the same identity type on the frozen v1 layer, not a second mechanism." + ], + evidence: [ + DeclarationRef { module_path: "v2.test.claim.declaration_graft_assemble", decl_name: "declaration_graft_where_alias_over_an_undeclared_carrier_refuses", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.declaration_graft_assemble", decl_name: "declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations", field: WholeDeclaration }, + ], +} diff --git a/src/v2/compiler/00_compile.dag b/src/v2/compiler/00_compile.dag index a8b6f386e40..8278dbad7d1 100644 --- a/src/v2/compiler/00_compile.dag +++ b/src/v2/compiler/00_compile.dag @@ -91,6 +91,7 @@ import v2.compiler.resolve { ResolveWalkAccepted, ResolveWalkRefused, resolve, + resolved_tree_of, ResolvedTree } import v2.compiler.tokenize { tokenize } @@ -3141,7 +3142,7 @@ fn native_module_resolve_verdict( ResolveWalkAccepted { value: resolved, diagnostics: _ } => match context.resolution { Accepted { value: shared, diagnostics: _ } => - NativeModuleResolveAccepted { resolved: ResolvedTree { root: resolved, symbol_index: shared.symbol_index } } + NativeModuleResolveAccepted { resolved: resolved_tree_of(root: resolved, symbol_index: shared.symbol_index) } Rejected { diagnostics: r } => NativeModuleResolveRefused { first: r, diff --git a/src/v2/compiler/03_ingest.dag b/src/v2/compiler/03_ingest.dag index 8b65216303f..73c7d151a45 100644 --- a/src/v2/compiler/03_ingest.dag +++ b/src/v2/compiler/03_ingest.dag @@ -318,7 +318,7 @@ fn parse_tree_to_target_model_bridge(parse_tree: ParseTree, source_model: Target o: parse_tree_to_emitted_node(parse_tree: parse_tree, source_model: source_model), f: fn(emitted) { bind_outcome( - o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index() }), + o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index() }), f: fn(inferred) { bind_outcome( o: coerce_grounded_node(source: emitted, tree: inferred, target: source_model), @@ -343,7 +343,7 @@ fn cross_language_compile( o: neutralize_core_for_target(core: core, target: target_model), f: fn(neutralized) { bind_outcome( - o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index() }), + o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index() }), f: fn(inferred) { emit(tree: inferred, target: target_model) } diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 398468ddb12..3f8b7b86682 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -74,6 +74,7 @@ import v2.std.resolution_policy { NamespaceOnlyY, default_name_resolution_policy } +import v2.compiler.symbol_index_fill { symbol_index_fill_module_declarations } import v2.std.symbol_index { LexicalAmbiguous, LexicalBindingCandidate, @@ -141,9 +142,33 @@ import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId } // it -- v2.compiler.infer refinement_declaration asks symbol_index_lookup for a refinement // declaration a cast operand's type references (the declared-carrier widening), replacing an // infer-private walk over the tree. +// TWO INDEXES OVER THE SAME DECLARATIONS AT DIFFERENT PHASES, NEVER ONE QUESTION TWICE. +// symbol_index is THE INDEX RESOLUTION CONSULTED: declarations as authored, before resolve, the table +// resolve looks references up in. resolved_declarations is DECLARATIONS WITH RESOLVED BODIES: the same +// module fold (v2.compiler.symbol_index_fill symbol_index_fill_module_declarations) run over the +// RESOLVED root, so a declaration's body carries the identities resolve bound in it -- a where-refined +// carrier `Int` is the kernel binding, a carrier naming a corpus type is its declaration reference. A +// reader that needs a body's resolved type reads resolved_declarations; nothing reads symbol_index for +// a body type (neat-boar-16 ruling), so the two never answer the same question. +// CONSUMERS: v2.compiler.infer refinement_declaration reads resolved_declarations (gunbc#12407, stacked +// on this change). symbol_index is read by no stage yet beyond resolve itself. type ResolvedTree { root: Node symbol_index: SymbolIndex + resolved_declarations: SymbolIndex +} + +// The resolved root's declarations, by the same module fold the pre-resolve index uses: the module's +// qualified name is read from the root's own header, so a declaration is keyed at its full path (p.Pos). +// A root whose module name cannot be read yields the empty index -- every lookup through it refuses. +fn resolved_declarations_of(root: Node) -> SymbolIndex { + symbol_index_fill_module_declarations(index: empty_symbol_index(), root: root, record_declarations: Empty) +} + +// THE ONE CONSTRUCTOR of an accepted resolution's carrier: the root, the index it was resolved +// against, and its declarations as resolved. +fn resolved_tree_of(root: Node, symbol_index: SymbolIndex) -> ResolvedTree { + ResolvedTree { root: root, symbol_index: symbol_index, resolved_declarations: resolved_declarations_of(root: root) } } // `test_code`, `declared_in` and `imported_origins` exist for one decision: whether a reference binds @@ -1249,7 +1274,7 @@ fn resolve_walk_outcome(w: ResolveNodeWalk) -> Outcome { fn resolved_tree_outcome(w: ResolveNodeWalk, symbol_index: SymbolIndex) -> Outcome { match w { ResolveWalkAccepted { value: v, diagnostics: d } => - Accepted { value: ResolvedTree { root: v, symbol_index: symbol_index }, diagnostics: d } + Accepted { value: resolved_tree_of(root: v, symbol_index: symbol_index), diagnostics: d } ResolveWalkRefused { first: f, rest: _, observation: _ } => Rejected { diagnostics: f } } } diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 58b47a6481d..65bfd3224a0 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -966,6 +966,15 @@ fn body_lower_fielded_type_variant(shell: Node, head: Node, payload_shell: Node) } } +// A WHERE-REFINED HEAD IS A TYPE, LOWERED BY THE ONE TYPE-EXPRESSION LOWERING that signatures and +// cast targets use (body_lower_type_expr_lowered_optional), so resolve binds the carrier in type role +// like any other type. Carried as the raw parse sequence, the head reached resolve as a +// dag_surface_qualified_name shell, which v2.compiler.resolve preserves UNCHANGED as module metadata +// (v2.extdeps.languages.dag dag_resolve_preserve_module_metadata_subtree): the declaration named its +// carrier in a vocabulary no stage resolved. A head the lowering cannot read refuses at the head, as an +// unreadable annotation does. The other declaration-body type positions (alias right-hand side, field +// and payload types) are the same defect and a declared frontier +// (gunbc.recurring_failure_mode declaration_body_type_shell_preserved_unresolved). // A variant shell is seq(type_expr, seq(optional(where), optional(payload))). A bare head is left // as parsed: whether `type T = U` names an alias or a one-variant sum is decided where the // alternatives are counted (v2.std.compilers.sugar sugar_fold_coproduct_pipe_chain, the seed's @@ -1001,17 +1010,24 @@ fn body_lower_type_variant(shell: Node) -> Outcome { Absent => outcome_accepted(value: shell) Present { value: suffix_id } => if suffix_id == ^dag_surface_where_refinement_clause { - outcome_accepted( - value: node_with_occurrence_id( - kind: TypeNode { connective: Conj }, - children: body_lower_type_variant_children_with_where( - base: pair.left, - where_clause: suffixes.left, - fields: suffixes.right - ), - occurrence_id: shell.occurrence_id - ) - ) + match body_lower_type_expr_lowered_optional(node: pair.left) { + Absent => + outcome_rejected( + d: body_lower_diagnostic(reason: ^body_lowering_reason_type_annotation_not_carried, n: pair.left) + ) + Present { value: carrier } => + outcome_accepted( + value: node_with_occurrence_id( + kind: TypeNode { connective: Conj }, + children: body_lower_type_variant_children_with_where( + base: carrier, + where_clause: suffixes.left, + fields: suffixes.right + ), + occurrence_id: shell.occurrence_id + ) + ) + } } else { outcome_accepted(value: shell) } diff --git a/src/v2/test/claim/declaration_graft_assemble_test.dag b/src/v2/test/claim/declaration_graft_assemble_test.dag index f68351787ce..ebf59397de9 100644 --- a/src/v2/test/claim/declaration_graft_assemble_test.dag +++ b/src/v2/test/claim/declaration_graft_assemble_test.dag @@ -1,6 +1,9 @@ module v2.test.claim.declaration_graft_assemble import v2.compiler.resolve { ResolvedTree } +import v2.std.symbol_index { symbol_index_lookup } +import v2.std.node_query { find_named_child } +import v2.std.optional { Absent, Present } import extdeps.communication.medium { Lossless, Medium } import v2.compiler.name_resolve { Admission, @@ -120,13 +123,14 @@ fn declaration_graft_atom_present(root: Node, lexeme: String) -> Bool { // fn-only, type-only, where-alias-only) are the containment-spine controls (gunbc#11694) // and stay separate, as do the three record sources (once refusing; now the Named controls of // the record spelling, see the bottom of this module). -data src_combined: String = "module p\n\nimport v2.std.logic { Bool }\n\ntype Flag = On | Off\ntype Name = String where brand(\"Name\")\nfn f(x: Int) -> Int { x }\nfn dag_user(x: Int) -> Int { x }\nfn g(q: Flag) -> Flag { q }\nfn h() -> Flag { On }\nfn flip(q: Flag) -> Flag { match q { On => Off } }\nfn b() -> Bool { true }\n" -data src_alias_spelled_as_emitted_id: String = "module p\n\ntype dag_surface_type_expr = String where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" -data src_alias_spelled_as_production_name: String = "module p\n\ntype dag_production_type_decl = String where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" +data src_combined: String = "module p\n\nimport v2.std.logic { Bool }\n\ntype Flag = On | Off\ntype Name = Int where brand(\"Name\")\nfn f(x: Int) -> Int { x }\nfn dag_user(x: Int) -> Int { x }\nfn g(q: Flag) -> Flag { q }\nfn h() -> Flag { On }\nfn flip(q: Flag) -> Flag { match q { On => Off } }\nfn b() -> Bool { true }\n" +data src_alias_spelled_as_emitted_id: String = "module p\n\ntype dag_surface_type_expr = Int where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" +data src_alias_spelled_as_production_name: String = "module p\n\ntype dag_production_type_decl = Int where brand(\"N\")\nfn f(x: Int) -> Int { x }\n" data src_empty: String = "module p\n" data src_fn_only: String = "module p\n\nfn f(x: Int) -> Int { x }\n" data src_type_only: String = "module p\n\ntype Flag = On | Off\n" -data src_where_alias_only: String = "module p\n\ntype Name = String where brand(\"Name\")\n" +data src_where_alias_only: String = "module p\n\ntype Name = Int where brand(\"Name\")\n" +data src_where_alias_undeclared_carrier: String = "module p\n\ntype Name = Undeclared where brand(\"Name\")\n" data src_record_construct: String = "module p\n\ntype Rec { n: Int }\nfn mk() -> Rec { Rec { n: 1 } }\n" data src_record_type_only: String = "module p\n\ntype Rec { n: Int }\n" data src_flag_and_rec: String = "module p\n\ntype Flag = On | Off\ntype Rec { n: Int }\n" @@ -138,6 +142,8 @@ fn declaration_graft_empty_assembled() -> Outcome { declaration_gr fn declaration_graft_fn_only_assembled() -> Outcome { declaration_graft_assemble_for(src: src_fn_only) } fn declaration_graft_type_only_assembled() -> Outcome { declaration_graft_assemble_for(src: src_type_only) } fn declaration_graft_where_alias_only_assembled() -> Outcome { declaration_graft_assemble_for(src: src_where_alias_only) } +// Rostered warm in v2.workflow.floor_pure_producer_share: one front end is more than one claim's budget. +fn declaration_graft_where_alias_undeclared_carrier_assembled() -> Outcome { declaration_graft_assemble_for(src: src_where_alias_undeclared_carrier) } fn declaration_graft_record_construct_assembled() -> Outcome { declaration_graft_assemble_for(src: src_record_construct) } fn declaration_graft_record_type_only_assembled() -> Outcome { declaration_graft_assemble_for(src: src_record_type_only) } fn declaration_graft_flag_and_rec_assembled() -> Outcome { declaration_graft_assemble_for(src: src_flag_and_rec) } @@ -185,6 +191,44 @@ test fn declaration_graft_where_alias_accepts() -> Bool { declaration_graft_accepts(out: declaration_graft_where_alias_only_assembled()) } +// A WHERE-ALIAS'S CARRIER IS A RESOLVED TYPE. Body lowering lowers the refined head as a type +// (v2.compiler.body_lowering_fold body_lower_type_variant), so resolve binds it and a carrier nothing +// declares refuses unbound, located at the carrier. RED BEFORE: the head reached resolve as an +// unlowered dag_surface_qualified_name shell, which resolve preserves unchanged as module metadata, +// so `Undeclared where ..` ASSEMBLED with its carrier never checked (and this module's fixtures +// carried an unimported `String` that way; they now carry Int). +// THE RESOLVED CARRIER IS READ FROM resolved_declarations (v2.compiler.resolve ResolvedTree): the +// where-alias's declaration, as resolved, holds its carrier as the kernel Int binding. RED if the head +// reached resolve unlowered (a preserved qualified-name shell) or were read from symbol_index, which +// holds the declaration as authored (the bare spelling Int). +test fn declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations() -> Bool { + match declaration_graft_where_alias_only_assembled() { + Rejected { diagnostics: _ } => false + Accepted { value: tree, diagnostics: _ } => + match symbol_index_lookup(index: tree.resolved_declarations, qualified_path: Cons { head: ^p, tail: Cons { head: ^Name, tail: Empty } }) { + Absent => false + Present { value: decl } => + match find_named_child(root: decl, name: ^dag_surface_type_expr) { + Accepted { value: carrier, diagnostics: _ } => + match carrier.kind { + TypeNode { connective: Atom { identity: id } } => id == ^dag_binding_type_int + _ => false + } + Rejected { diagnostics: _ } => false + } + } + } +} + +test fn declaration_graft_where_alias_over_an_undeclared_carrier_refuses() -> Bool { + match declaration_graft_where_alias_undeclared_carrier_assembled() { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => + (d.head.reason == ^resolve_reason_unbound_symbol) + || fold(d.tail, init: false, f: fn(acc, x) { acc || (x.reason == ^resolve_reason_unbound_symbol) }) + } +} + test fn declaration_graft_combined_accepts() -> Bool { declaration_graft_accepts(out: declaration_graft_combined_assembled()) } diff --git a/src/v2/test/lens_common/infer_fixture.dag b/src/v2/test/lens_common/infer_fixture.dag index 4d0a9f887ca..2383bdb3352 100644 --- a/src/v2/test/lens_common/infer_fixture.dag +++ b/src/v2/test/lens_common/infer_fixture.dag @@ -19,7 +19,7 @@ import v2.std.witness { Holds, StructuralPropertyWitness, Witness, witness_from_ // resolution consulted; a supplied tree was never resolved, so it carries an index holding NO // declarations -- the name says so, and a declaration lookup through it finds nothing and refuses. fn claim_resolved_tree_without_declarations(root: Node) -> ResolvedTree { - ResolvedTree { root: root, symbol_index: empty_symbol_index() } + ResolvedTree { root: root, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index() } } fn claim_atom_node(s: Symbol) -> Node { diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 91f15ff67c5..d98a3ec06bc 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -516,7 +516,9 @@ import v2.std.collection { List } // CLAIM-FORCED, by the same ceiling arithmetic as dag_prepared_grammar: an in-fold first // touch of this fill dies on the lane's margin and restarts per claim. The module is under // src/v2/extdeps, so it resolves in every required-floor subject. -// THE TEN declaration_graft_assemble PRODUCERS EARN THEIR ROWS ON THE FILL-THAT-CANNOT-LAND +// THE declaration_graft_assemble PRODUCERS EARN THEIR ROWS ON THE FILL-THAT-CANNOT-LAND (ten on the +// receipt below; an eleventh, declaration_graft_where_alias_undeclared_carrier_assembled, is the RED of +// the resolved where-head -- one assembly, on the same ground) // GROUND, AND SIX OF THEM ON THE SHARING GROUND AS WELL. Receipt, re-derivable: required-floor // run 35467726264 (gunbc#11574 head 1797ea43bd) reported fourteen of that file's claims // COMPLETED-OVER-COST-REQUIREMENT at 73,857-148,646 eval steps against the 72,300 new-witness @@ -1051,7 +1053,8 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.declaration_graft_assemble.declaration_graft_where_alias_only_assembled", "v2.test.claim.declaration_graft_assemble.declaration_graft_record_construct_assembled", "v2.test.claim.declaration_graft_assemble.declaration_graft_record_type_only_assembled", - "v2.test.claim.declaration_graft_assemble.declaration_graft_flag_and_rec_assembled" + "v2.test.claim.declaration_graft_assemble.declaration_graft_flag_and_rec_assembled", + "v2.test.claim.declaration_graft_assemble.declaration_graft_where_alias_undeclared_carrier_assembled" ] // grammar_relation_row_for_emitted HAS NOW BEEN MEASURED ON THE THIRD CONJUNCT, AND IT PASSES. diff --git a/src/v2/workflow/realization_attempt.dag b/src/v2/workflow/realization_attempt.dag index f3582fdb117..02e49bbe8db 100644 --- a/src/v2/workflow/realization_attempt.dag +++ b/src/v2/workflow/realization_attempt.dag @@ -284,7 +284,7 @@ fn attempt_joined(program: ResolvedTree, fn_name: Symbol, entry: String) -> Entr match list_at_optional(xs: joined, index: 0) { Absent => attempt_refused(entry: entry, phase: PhaseResolve, cause: ^realization_attempt_identity_absent) Present { value: decl } => - match infer_and_discharge(tree: ResolvedTree { root: decl, symbol_index: program.symbol_index }) { + match infer_and_discharge(tree: ResolvedTree { root: decl, symbol_index: program.symbol_index, resolved_declarations: program.resolved_declarations }) { Rejected { diagnostics: ds } => attempt_refused_at(entry: entry, phase: PhaseInfer, cause: first_located_cause(ds: ds), located: first_located_file(ds: ds)) Accepted { value: inferred, diagnostics: _ } => From f293dcb0d908fba152387706a9d3874ed6cb1c41 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 29 Sep 2026 16:27:33 +0000 Subject: [PATCH 14/15] resolve: ResolvedTree comment states symbol_index's consumers once (no later stage reads it; #12407 reads resolved_declarations) (review 72652) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/03_resolve.dag | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 3f8b7b86682..e7ce998eb95 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -138,10 +138,10 @@ import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId } // the Namespace.symbol_index the walk ran under, minted beside the root on the Accepted arm only, so // a refusal carries no index and no stage can read one for a tree that did not resolve. // CONSUMERS: .root is read by every stage after resolve (infer's gather reads it at its entry). -// .symbol_index is a DECLARED FRONTIER in this change: its consumer is gunbc#12407, which stacks on -// it -- v2.compiler.infer refinement_declaration asks symbol_index_lookup for a refinement -// declaration a cast operand's type references (the declared-carrier widening), replacing an -// infer-private walk over the tree. +// .symbol_index is the table resolve resolves against; no later stage reads it. A later stage that needs +// a declaration reads .resolved_declarations below: v2.compiler.infer refinement_declaration (gunbc#12407, +// stacked on this change) asks symbol_index_lookup there for the refinement declaration a cast +// operand's type references, replacing an infer-private walk over the tree. // TWO INDEXES OVER THE SAME DECLARATIONS AT DIFFERENT PHASES, NEVER ONE QUESTION TWICE. // symbol_index is THE INDEX RESOLUTION CONSULTED: declarations as authored, before resolve, the table // resolve looks references up in. resolved_declarations is DECLARATIONS WITH RESOLVED BODIES: the same @@ -150,8 +150,6 @@ import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId } // carrier `Int` is the kernel binding, a carrier naming a corpus type is its declaration reference. A // reader that needs a body's resolved type reads resolved_declarations; nothing reads symbol_index for // a body type (neat-boar-16 ruling), so the two never answer the same question. -// CONSUMERS: v2.compiler.infer refinement_declaration reads resolved_declarations (gunbc#12407, stacked -// on this change). symbol_index is read by no stage yet beyond resolve itself. type ResolvedTree { root: Node symbol_index: SymbolIndex From 2e0c19e21f3e2adb2030e1c4ecd30debb66388a1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 29 Sep 2026 16:52:12 +0000 Subject: [PATCH 15/15] body_cast_node: the Pos2 one-step row reads the resolved carrier only; infer's admission is row 15's subject (over the new-witness budget) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/test/claim/body_cast_node_test.dag | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/v2/test/claim/body_cast_node_test.dag b/src/v2/test/claim/body_cast_node_test.dag index 90ea7c36a57..8d1491f406a 100644 --- a/src/v2/test/claim/body_cast_node_test.dag +++ b/src/v2/test/claim/body_cast_node_test.dag @@ -554,8 +554,10 @@ test fn bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses() -> Bool { } // (15c2) A REFINEMENT OF A REFINEMENT WIDENS ONE STEP ON THE PRODUCTION ROUTE. `x as Pos` from -// `x: Pos2` (`type Pos2 = Pos where positive`): infer admits it, and the crossing's quality is Widened, -// read through resolved_declarations, where Pos2's carrier is the resolved reference to Pos. The +// `x: Pos2` (`type Pos2 = Pos where positive`): the crossing's quality is Widened, read through the +// production assembly's resolved_declarations, where Pos2's carrier is the resolved reference to Pos, +// against that tree's own cast target. infer's admission of a Widened cast end to end is row (15)'s +// subject; this row's is the resolved carrier, so infer is not re-run here (DESIGN section 3). The // assembly is a producer rostered warm in v2.workflow.floor_pure_producer_share. RED BEFORE // gunbc#12629: the carrier was the unresolved atom Pos and the cast refused. fn bcn_refinement_of_refinement_as_its_carrier() -> Outcome { @@ -563,11 +565,7 @@ fn bcn_refinement_of_refinement_as_its_carrier() -> Outcome { } test fn bcn_refinement_of_a_refinement_widens_one_step() -> Bool { - match bcn_infers(o: bcn_refinement_of_refinement_as_its_carrier()) { - Rejected { diagnostics: _ } => false - Accepted { value: _, diagnostics: _ } => - bcn_is_widened(q: bcn_crossing_quality(o: bcn_refinement_of_refinement_as_its_carrier(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos2, tail: Empty } })) - } + bcn_is_widened(q: bcn_crossing_quality(o: bcn_refinement_of_refinement_as_its_carrier(), reference_path: Cons { head: ^p, tail: Cons { head: ^Pos2, tail: Empty } })) } // (15d) A REFINEMENT LOOKUP MISS REFUSES. When v2.compiler.infer refinement_declaration finds no