From 03342a3647e2bf7e9d1ff5f1e29c2b2b7be6275e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 27 Sep 2026 16:30:20 +0000 Subject: [PATCH 1/7] 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 2/7] 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 0fb011ffc455a61052238361bdd6cd302a24b051 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 28 Sep 2026 13:38:22 +0000 Subject: [PATCH 3/7] 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 4/7] 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 5/7] 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 6/7] 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 7/7] 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