Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions dag/gunbc/bare_name_fork_lens.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module gunbc.bare_name_fork_lens

import std.types { Bool, Int, String }
import v2.std.decl_index { DeclFact, ItemKind, FnItem, FuncItem, TypeItem, DataItem, ServiceItem, OtherItem, decl_facts }
import v2.std.decl_index { DeclFact, ItemKind, FnItem, TypeItem, DataItem, ServiceItem, OtherItem, decl_facts }
import std.materialization_ladder { string_list_contains }

// WHAT THIS ANSWERS, AND WHY A COMPILE CANNOT.
Expand Down Expand Up @@ -39,7 +39,6 @@ import std.materialization_ladder { string_list_contains }
fn item_kind_text(kind: ItemKind) -> String {
match kind {
FnItem => "fn"
FuncItem => "fn"
TypeItem => "type"
DataItem => "data"
ServiceItem => "service"
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/claim_batch_function_preflight_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ data claim_batch_function_preflight_seed_growth_justification: SeedGrowthJustifi
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.claim_batch", decl_name: "validate_explicit_functions", field: WholeDeclaration }
],
reason: "WHY RUST IS STILL NEEDED: claim_batch is a seed-host CLI and its argv is consumed before any .dag evaluation frame exists. validate_explicit_functions adds no declaration vocabulary and no selection policy: it asks module_path_index.parse_dag_file, the canonical tokenizer/parser path, for the entry's constructed Node items and retains exactly ItemKind.FnItem or ItemKind.FuncItem, the same callable partition used by the interpreter. A parse failure refuses; it never becomes an empty declaration set. The function exists only to place the evaluator's existing no-such-function refusal before whole-corpus preparation.",
reason: "WHY RUST IS STILL NEEDED: claim_batch is a seed-host CLI and its argv is consumed before any .dag evaluation frame exists. validate_explicit_functions adds no declaration vocabulary and no selection policy: it asks module_path_index.parse_dag_file, the canonical tokenizer/parser path, for the entry's constructed Node items and retains exactly ItemKind.FnItem, the same callable partition used by the interpreter. A parse failure refuses; it never becomes an empty declaration set. The function exists only to place the evaluator's existing no-such-function refusal before whole-corpus preparation.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete validate_explicit_functions and this row when claim_batch argv ingestion is modeled in .dag and function selections are constructed as declaration identities before the seed host receives an execution plan.",
current_boundary: "Only explicit --function/--functions rows are checked, immediately after path argv validation and before the bare-reference warm. Discovery-produced rows retain their existing producer-owned identity path. A declared callable proceeds unchanged; a missing name or an entry that cannot be parsed exits 2 before any corpus preparation."
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/instruments/multi_module_compile_fixture.dag
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ import gunbc.compile_diagnostic_census { CompileDiagnosticCensusRow }
// SIGNATURE SHAPE IS OBSERVABLE AS A STRUCTURED RUST PROJECTION OVER THE RESOLVED
// REGISTRY, not as contents-by-path and not as a read of emitted bytes. On
// FixtureCompileCompleted the field resolved_rust_functions carries List<ResolvedRustFnSignature>
// — per FnItem/FuncItem in item_registry: source owner_module + declaration_name and the
// — per FnItem in item_registry: source owner_module + declaration_name and the
// ordered parameter name list derived from that registry row (emit_ident / service_var_name
// transforms applied). Witnesses assert over that list; raw text is not offered as an assertion
// surface. Discriminating RED: test.claim.resolved_rust_fn_projection_witness.
Expand All @@ -90,7 +90,7 @@ type MultiModuleCompileFixture {
entry: NonEmptyStr
}

// THE STRUCTURED PROJECTION WITNESSES ASSERT OVER. Per resolved FnItem/FuncItem on each
// THE STRUCTURED PROJECTION WITNESSES ASSERT OVER. Per resolved FnItem on each
// TypedModule.item_registry (NOT the bare-name-merged ResolvedGraph.item_registry): source
// identity (owning module + declaration name) and the PARAMETER NAME LIST taken from ItemInfo
// with the same per-arm name transforms emit_func_params applies today (emit_ident for authored
Expand Down
97 changes: 97 additions & 0 deletions dag/test/claim/effectful_item_kind_collapse_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
module test.claim.effectful_item_kind_collapse_witness_test

import std.types { String, Bool, Int }
import v2.std.optional { Present, Absent }
import gunbc.compile_diagnostic_census { CompileDiagnosticCensus, CensusObserved, CensusNotRunnable, census_blocking_rows, census_total_count }
import gunbc.guarantee_probe_corpus { census_blocking_count_for_class }

// ENROLLED EVIDENCE for the FuncItem -> FnItem collapse (DESIGN section 3: one concept, one
// name) and for the two facts that collapse made observable. `ItemKind.FuncItem` was the node
// model's shadow of the deleted `func` spelling; its only distinguishing content was that the
// registry projection (`v1.compiler.infer` build_item_info) hardcoded is_self_recursive and
// has_non_tail_self_call false for every effectful item, and that the zero-parameter branch of
// infer_item -- the branch a `func` with no parameters landed in -- rebuilt the typed node with
// `uses: []`, extended no scope with the declared resources, and hardcoded the same two fields.
// After the collapse one arm builds every function's ItemInfo and one branch of infer_item types
// every function with a body, so the typed node and the registry answer the same question the
// same way. Neither of those facts is visible from a green over the existing corpus: no corpus
// module both declares a zero-parameter effectful function that reads its resource and is emitted
// to Rust, and no corpus module carries an effectful self-call. These fixtures are the
// constructed RED / control pairs, per DESIGN section 4b(4).
//
// THE ZERO-PARAMETER PAIR. `zpe_reads_resource` declares `uses net` and returns `net.id`, so the
// resource must be BOUND in the body's scope for the compile to carry no blocking diagnostic, and
// the emitted Rust signature must carry the resource parameter (`net: &`), which emit_func_params
// renders from the typed node's `uses` and from nothing else. Before this change the first arm
// refused (`net` unbound: the zero-parameter branch extended no scope) and the second emitted a
// signature with no resource parameter while the registry said the item was effectful -- two
// contradictory observations of one declaration. MUTATION BAR: restore `uses: []` on the
// zero-parameter typed node and both arms go RED; restore the scope omission alone and the first
// goes RED.
//
// THE RECURSION PAIR. emit_func_def renders every effectful declaration as `async fn` and never
// consults is_tco_eligible or is_self_recursive, so an effectful self-call reached the target
// verbatim and rustc refused it (E0733) AFTER `gunbc compile` had reported success. That is the
// fabricated-plausible-output failure of DESIGN section 5, and it was unreachable by any refusal
// keyed on the registry, because the registry said every effectful item was non-recursive.
// `EffectfulSelfRecursionUnrealized` is now raised at the Rust emitter boundary from the SAME
// registry read the pure path's TCO decision consumes. Both the tail and the non-tail shape are
// refused: the effectful path realizes neither. MUTATION BAR: restore `is_self_recursive: false`
// in build_item_info (in v1_compiler_infer.rs -- these fixtures are compiled by the SEED BINARY,
// so the mutation must be made in the mirror, exactly as
// generic_effectful_declaration_wall_witness_test records) and both refusal arms go RED while the
// control stays green; delete the diagnostics fold in emit_rust and the same happens.
//
// THE CONTROL is the same shape with the self-call replaced by a call to a pure helper, which is
// the realization the diagnostic text recommends: it compiles clean and emits. A refusal that
// fired on every effectful declaration would pass both refusal arms and FAIL this one.
//
// COVERAGE BOUND. These arms reach the emitted TEXT and the diagnostic census; none invokes
// rustc. The E0733 claim above is rustc's documented rule, cited as the reason the refusal
// exists, not measured here.

data zpe_reads_resource_source: String = "module zpe_reads_resource\n\ntype ZpeNet \{\n id: Int\n}\n\nfn zpe_read() -> Int\n uses net: ZpeNet\n\{\n net.id\n}\n"

data efr_tail_source: String = "module efr_tail\n\ntype EfrNet \{\n id: Int\n}\n\nfn efr_count_down(n: Int) -> Int\n uses net: EfrNet\n\{\n if n == 0 \{ net.id } else \{ efr_count_down(n: n - 1) }\n}\n"

data efr_non_tail_source: String = "module efr_non_tail\n\ntype EfrNet \{\n id: Int\n}\n\nfn efr_sum_down(n: Int) -> Int\n uses net: EfrNet\n\{\n if n == 0 \{ net.id } else \{ n + efr_sum_down(n: n - 1) }\n}\n"

data efr_control_source: String = "module efr_control\n\ntype EfrNet \{\n id: Int\n}\n\nfn efr_pure_sum(n: Int) -> Int \{\n if n == 0 \{ 0 } else \{ n + efr_pure_sum(n: n - 1) }\n}\n\nfn efr_effectful_total(n: Int) -> Int\n uses net: EfrNet\n\{\n net.id + efr_pure_sum(n: n)\n}\n"

// NOT-RUNNABLE IS NOT ZERO: -1 satisfies neither the == 0 control nor the == 1 refusal.
fn eik_blocking_count(source: String, wanted: String) -> Int {
match census_blocking_count_for_class(census: compile_dag_diagnostic_census(source), wanted: wanted) {
Present { value: n } => n
Absent => 0 - 1
}
}

// TOTAL over every blocking class is exact here because each fixture imports nothing, so its
// closure is itself (see generic_effectful_declaration_wall_witness_test for why that matters).
fn eik_total_blocking(source: String) -> Int {
match compile_dag_diagnostic_census(source) {
CensusObserved { rows: rows } => census_total_count(rows: census_blocking_rows(rows: rows))
CensusNotRunnable { cause: _ } => 0 - 1
}
}

test fn a_zero_parameter_effectful_declaration_binds_its_resource() -> Bool {
eik_total_blocking(source: zpe_reads_resource_source) == 0
}

test fn a_zero_parameter_effectful_declaration_emits_its_resource_parameter() -> Bool {
compile_dag_rust_emit_check(zpe_reads_resource_source, "src/zpe_reads_resource.rs", ["net: &"], [])
}

test fn an_effectful_tail_self_call_is_refused_at_the_rust_emitter() -> Bool {
eik_blocking_count(source: efr_tail_source, wanted: "EffectfulSelfRecursionUnrealized") == 1
}

test fn an_effectful_non_tail_self_call_is_refused_at_the_rust_emitter() -> Bool {
eik_blocking_count(source: efr_non_tail_source, wanted: "EffectfulSelfRecursionUnrealized") == 1
}

test fn an_effectful_declaration_calling_a_pure_recursive_helper_is_admitted() -> Bool {
eik_total_blocking(source: efr_control_source) == 0
&& compile_dag_rust_emit_check(efr_control_source, "src/efr_control.rs", ["net: &"], ["compile_error!"])
}
4 changes: 4 additions & 0 deletions src/v1/00_core.dag
Original file line number Diff line number Diff line change
Expand Up @@ -429,6 +429,7 @@ type CompilerDiagnostic
| DataReferenceVisibilityBudgetExceeded { name: String, span: SourceSpan }
| ParameterDefaultFormNotAdmitted { parameter: String, admitted: List<String>, span: SourceSpan }
| AmbiguousAnonymousRecordLiteral { candidates: List<String>, span: SourceSpan }
| EffectfulSelfRecursionUnrealized { name: String, span: SourceSpan }
| ModuleFilenameCollision { filename: String, modules: List<String>, span: SourceSpan }
| EffectSummaryIncompleteAtFunctionValue { caller: String, span: SourceSpan }
| EffectSummaryIncompleteAtLocalBinding { caller: String, name: String, span: SourceSpan }
Expand Down Expand Up @@ -650,6 +651,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
DataReferenceVisibilityBudgetExceeded { name: _, span: s } => s
ParameterDefaultFormNotAdmitted { parameter: _, admitted: _, span: s } => s
AmbiguousAnonymousRecordLiteral { candidates: _, span: s } => s
EffectfulSelfRecursionUnrealized { name: _, span: s } => s
ModuleFilenameCollision { filename: _, modules: _, span: s } => s
EffectSummaryIncompleteAtFunctionValue { caller: _, span: s } => s
EffectSummaryIncompleteAtLocalBinding { caller: _, name: _, span: s } => s
Expand Down Expand Up @@ -749,6 +751,7 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
ParameterDefaultFormNotAdmitted { parameter: p, admitted: forms, span: _ } =>
concat("default value for parameter '", p, "' is not an admitted form (admitted: ", join(forms, separator: ", "), ")")
AmbiguousAnonymousRecordLiteral { candidates: cs, span: _ } => concat("ambiguous anonymous record literal shape matches ", to_string(value: cs |> count), " structs: ", join(cs, separator: ", "), " — add a nominal type")
EffectfulSelfRecursionUnrealized { name: n, span: _ } => concat("effectful declaration '", n, "' calls itself: the Rust realization renders an effectful declaration as `async fn`, and rustc refuses recursion in an async fn without boxing (E0733), which no emitter performs. Realize the recursion as a loop, or move the self-call into a pure helper.")
ModuleFilenameCollision { filename: f, modules: ms, span: _ } => concat("module filename collision: ", to_string(value: ms |> count), " modules render one emitted file name '", f, "': ", join(ms, separator: ", "), " — module_to_filename maps '.' to '_', so these names are indistinguishable at the emitted path; rename one module segment")
EffectSummaryIncompleteAtFunctionValue { caller: c, span: _ } => concat("effect summary incomplete: ", c, " calls through a function value, whose callee is chosen at runtime, so its effects are unknown rather than empty — the caller's summary is a lower bound, not the answer")
EffectSummaryIncompleteAtLocalBinding { caller: c, name: n, span: _ } => concat(concat(concat(concat("effect summary incomplete: ", c), " calls the local binding '"), n), "', whose effects this pass cannot join through the registry, so the caller's summary is a lower bound rather than the answer")
Expand Down Expand Up @@ -880,6 +883,7 @@ fn diagnostic_disposition(d: CompilerDiagnostic) -> DiagnosticDisposition {
DataReferenceVisibilityBudgetExceeded { name: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
ParameterDefaultFormNotAdmitted { parameter: _, admitted: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
AmbiguousAnonymousRecordLiteral { candidates: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
EffectfulSelfRecursionUnrealized { name: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
ModuleFilenameCollision { filename: _, modules: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
EffectSummaryIncompleteAtFunctionValue { caller: _, span: _ } => DiagnosticDisposition { severity: SeverityNonError, gate: GateAdvisoryTypecheck }
EffectSummaryIncompleteAtLocalBinding { caller: _, name: _, span: _ } => DiagnosticDisposition { severity: SeverityNonError, gate: GateAdvisoryTypecheck }
Expand Down
49 changes: 2 additions & 47 deletions src/v1/04_infer.dag
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ import v1.compiler.infer_emit_info {
add_emit_item_summary, derive_variant_to_enum, close_fn_fields
}
import v1.compiler.infer_items {
ItemKind, FnItem, FuncItem, TypeItem, DataItem, ServiceItem, OtherItem,
ItemKind, FnItem, TypeItem, DataItem, ServiceItem, OtherItem,
ItemInfo, TypedModule, TypedGraph, ResolvedGraph, ModuleInterface, leaf_owner_modules_from_registry,
ModuleTypecheckProgress, ItemsChecked, AbandonedBeforeItems,
inferred_to_outputs, item_kind
Expand Down Expand Up @@ -11271,7 +11271,7 @@ fn infer_item(item: Node, scope: InferScope) -> TypedItemResult {
diagnostics: concat(transport_diags, props_diags)
}
}
else if item.body != none && item.params |> count > 0 {
else if item.body != none && (item.params |> count > 0 || item.inferred != none) {
let fn_scope = build_params_scope(scope: scope, params: item.params)
let fn_scope = fold(item.uses, init: fn_scope, f: (s, u) =>
extend_scope(scope: s, name: resource_use_name_at(n: u, source_indices: scope.type_env.source_indices), resolved: resource_use_resource(n: u), provenance: SubValueUnknown)
Expand Down Expand Up @@ -11317,39 +11317,6 @@ fn infer_item(item: Node, scope: InferScope) -> TypedItemResult {
diagnostics: concat(transport_diags, props_diags, concat(body_diags, return_conformance_diags))
}
}
else if item.body != none && item.params |> count == 0 && item.inferred != none {
let fn_decl_name = authored_name_at(source_indices: scope.type_env.source_indices, node: item)
let fn_scope = InferScope {
type_env: scope.type_env,
func_env: scope.func_env,
locals: scope.locals,
body_locals: scope.body_locals,
match_bound_names: scope.match_bound_names,
module_name: scope.module_name,
service_registry: scope.service_registry,
item_registry: scope.item_registry,
caller_decl_name: fn_decl_name,
lambda_param_provenance: scope.lambda_param_provenance
}
let body_result = infer_expr(texpr: item.body.value, scope: fn_scope, expected: Present { value: resolved_type(n: item) })
let body_typed = body_result.typed
let body_diags = concat(
body_result.diagnostics,
concat(
declared_type_conformance_diags(declared: declared_return_type_node(item: item), produced: resolved_type(n: body_typed), span: item.body.value.span, scope: scope),
explicit_return_conformance_diags(declared: declared_return_type_node(item: item), body_typed: body_typed, scope: scope))
)
TypedItemResult {
item: Node {
occurrence_identity: item.occurrence_identity, name: item.name, span: item.span, ident_span: item.ident_span, children: [], params: [],
inferred: item.inferred, return_cardinality: item.return_cardinality, uses: [], body: Present { value: body_typed },
connective: NoConnective, transport: typed_transport,
properties: typed_properties, type_annotation: typed_anno,
is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, module_item_kind: item.module_item_kind, expr_data: NoExprData
},
diagnostics: concat(transport_diags, props_diags, body_diags)
}
}
else if item.body != none && item.params |> count == 0 {
let data_expected = if item.type_annotation != none { Present { value: item.type_annotation.value } } else { none }
let val_result = infer_expr(texpr: item.body.value, scope: scope, expected: data_expected)
Expand Down Expand Up @@ -11866,7 +11833,6 @@ fn interface_cache_from_module(cache: TypeEnvCache) -> TypeEnvCache {
fn export_kind_of_item_kind(kind: ItemKind) -> ExportKind? {
match kind {
FnItem => Present { value: ExportFn }
FuncItem => Present { value: ExportFn }
TypeItem => Present { value: ExportType }
DataItem => Present { value: ExportData }
ServiceItem => Present { value: ExportService }
Expand Down Expand Up @@ -13251,17 +13217,6 @@ fn build_item_info(item: Node, source_indices: Map<String, NewlineIndex>, module
let res_names = item.uses |> map(u => resource_use_name_at(n: u, source_indices: source_indices))
let item_name_str = authored_name_at(source_indices: source_indices, node: item)
match kind {
FuncItem =>
ItemInfo {
name: item_name_str,
module_name: module_name,
kind: kind,
service_names: if item.body == none { [] } else { collect_typed_service_calls(texpr: item.body.value, source_indices: source_indices) },
resource_names: res_names,
params: item.params,
is_self_recursive: false,
has_non_tail_self_call: false
}
FnItem =>
ItemInfo {
name: item_name_str,
Expand Down
4 changes: 1 addition & 3 deletions src/v1/04_items.dag
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ import v1.compiler.infer_emit_info {
}


type ItemKind = FnItem | FuncItem | TypeItem | DataItem | ServiceItem | OtherItem
type ItemKind = FnItem | TypeItem | DataItem | ServiceItem | OtherItem

type ItemInfo {
name: String
Expand Down Expand Up @@ -243,8 +243,6 @@ fn item_kind(item: Node) -> ItemKind {
TypeItem
} else if item.transport != none {
ServiceItem
} else if item.body != none && item.uses |> count > 0 {
FuncItem
} else if item.body != none && item.params |> count > 0 {
FnItem
} else if item.body != none && item.type_annotation != none {
Expand Down
Loading
Loading