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
24 changes: 24 additions & 0 deletions dag/test/claim/qualified_pattern_head_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
module test.claim.qualified_pattern_head_witness_test

import gunbc.compile_diagnostic_census { CompileDiagnosticCensus, CensusObserved, CensusNotRunnable, census_blocking_rows }

data qualified_pattern_head_note: String = "A QUALIFIED PATTERN HEAD MUST BIND WHAT THE BARE SPELLING BINDS. Two spellings of one pattern name the same declaration, so they must bind the same node; only the authored string differs. MECHANISM: lookup_variant_in_type forks on whether the head contains a dot. The bare branch answers from the SCRUTINEE, which carries the instantiation. The dotted branch answered from the SYMBOL INDEX, which returns the coproduct's DECLARATION -- uninstantiated -- so the payload bound to the declaration's type PARAMETER instead of the scrutinee's type ARGUMENT. THE FIX PRESERVES ADMISSION: the index lookup still runs first and still decides whether the head names a variant of this coproduct at all; only the bound node's source changes once admission succeeds, and the fallback arm reproduces the previous answer. WHY THE CENSUS GRAIN AND NOT AN EMIT CHECK, which is the part worth reading. The subject here is a BINDING fact, and a binding fact is decided at typecheck. The first revision of this witness asked it through compile_dag_rust_emit_check, which parses, resolves, typechecks, EMITS RUST, and then -- per compile_dag_diagnostic_census_row_note -- collapses the whole result to a Bool, discarding WHICH judgment fired. So it measured emission for a proposition about resolution, and the enrolled claim duly cost 58579ms CPU against a 5000ms budget with 1.21GB RSS growth while its bare control passed. compile_dag_diagnostic_census reports the causal judgment directly as typed rows, which makes this witness narrower in subject, MORE discriminating (it names the diagnostic instead of collapsing to false), and cheaper for a principled reason rather than a convenient one -- emission is downstream of the fact being tested, so removing it removes work, not evidence. THE COST OBSERVATION IS NOT REPAIRED BY THIS CHANGE AND IS NOT CLAIMED TO BE; it is carried forward as a separate finding in the pull request that lands this, with its ruled-out causes and its next discriminator. MEASURED, all four cells, one fixture, both probe sources carrying IDENTICAL imports so the only difference is the two pattern heads -- pre-fix binary: qualified census OBSERVED[1] InternalError | no field 'root' on type 'T' | blocking=true | n=1, bare census OBSERVED[0]; post-fix binary: qualified OBSERVED[0], bare OBSERVED[0]. The earlier revision's arms differed in their import lists as well as in the head spelling, which made them a controlled experiment for the semantic discriminator and not for anything else; that is fixed here and was fixed before this grain change. A NON-GENERIC coproduct cannot discriminate this at all -- declaration and instantiation coincide there -- which is why the fixture is generic. CensusNotRunnable is a FAILURE with its own cause, never the expected red: could-not-measure and measured-nothing are different states and only one of them is evidence. dissolve-on: never -- permanent regression control for the spelling-identity law in pattern position."

data qualpat_qualified_probe_source: String = "module qualpat_qual_probe_mod\n\nimport test.fixture.qualpat_provider \{ QualpatResult, QualpatPayload, QualpatOk, QualpatErr \}\n\nfn qualpat_qual_read(r: QualpatResult<QualpatPayload>) -> String \{\n match r \{\n test.fixture.qualpat_provider.QualpatOk \{ value: v \} => v.root\n test.fixture.qualpat_provider.QualpatErr \{ code: _ \} => \"\"\n \}\n\}\n"

data qualpat_bare_probe_source: String = "module qualpat_bare_probe_mod\n\nimport test.fixture.qualpat_provider \{ QualpatResult, QualpatPayload, QualpatOk, QualpatErr \}\n\nfn qualpat_bare_read(r: QualpatResult<QualpatPayload>) -> String \{\n match r \{\n QualpatOk \{ value: v \} => v.root\n QualpatErr \{ code: _ \} => \"\"\n \}\n\}\n"

fn qualpat_probe_has_no_blocking_diagnostic(source: String) -> Bool {
match compile_dag_diagnostic_census(source) {
CensusObserved { rows: rows } => count(census_blocking_rows(rows: rows)) == 0
CensusNotRunnable { cause: _ } => false
}
}

test fn qualified_pattern_head_binds_the_instantiation() -> Bool {
qualpat_probe_has_no_blocking_diagnostic(source: qualpat_qualified_probe_source)
}

test fn bare_pattern_head_is_unchanged() -> Bool {
qualpat_probe_has_no_blocking_diagnostic(source: qualpat_bare_probe_source)
}
11 changes: 11 additions & 0 deletions dag/test/fixture/qualpat_provider.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module test.fixture.qualpat_provider

data qualpat_provider_fixture_note: String = "Provider fixture for test.claim.qualified_pattern_head_witness_test: one GENERIC coproduct and one concrete record to instantiate it with, which is the smallest pair that can distinguish a pattern head bound from the DECLARATION (payload type is the parameter T) from one bound from the SCRUTINEE (payload type is the argument). A non-generic coproduct cannot discriminate at all, because declaration and instantiation coincide there. Self-contained by construction: compile_dag_rust_emit_check assembles its source set by following imports, so a fixture that reaches into a THIRD module makes the harness refuse the closure and the control arm goes red for a reason that has nothing to do with the subject. The names are deliberately unlike anything in the seed, so a homonym in the bare-name registry cannot satisfy the assertions by accident."

type QualpatPayload {
root: String
}

type QualpatResult<T>
= QualpatOk { value: T }
| QualpatErr { code: Int }
20 changes: 19 additions & 1 deletion src/v1/04_patterns.dag
Original file line number Diff line number Diff line change
Expand Up @@ -262,6 +262,20 @@ fn variant_not_found_result(scrut: Node, variant_name: String, module_name: Stri
)
}

// A qualified pattern head must bind what the bare spelling binds. The dotted
// branch answers from the SYMBOL INDEX, which returns the coproduct's
// DECLARATION -- uninstantiated -- while the bare branch answers from the
// scrutinee, which carries the instantiation. So a bare `Ok { value: r }` bound
// r to the scrutinee's type ARGUMENT and the qualified spelling of the same
// pattern bound it to the declaration's type PARAMETER, so every field read off
// r reported no such field on type 'T'. Measured on a two-function probe whose
// only difference is the spelling of the head.
//
// The index lookup still runs first and still decides ADMISSION: a head naming
// a variant of some other coproduct misses there exactly as before. What changes
// is where the bound NODE comes from once admission succeeds -- the scrutinee
// when it carries that variant, the declaration otherwise, which is the
// pre-existing answer for a scrutinee that does not.
fn lookup_variant_in_type(scrut: PatternSubject, variant_name: String, module_name: String, env: TypeEnv, field_binding_count: Int) -> NodeLookupResult {
match scrut {
PatternLookupBlocked =>
Expand All @@ -275,7 +289,11 @@ fn lookup_variant_in_type(scrut: PatternSubject, variant_name: String, module_na
Present { value: resolved } =>
if (resolved.connective == Disj) {
match find_child_named(n: resolved, name: qualified_last_segment(name: variant_name), source_indices: source_indices) {
Present { value: variant_child } => node_lookup_resolved(node: variant_child)
Present { value: variant_child } =>
match find_child_named(n: expand_scrut_type_for_variant_lookup(scrut_node: scrut_node, env: env), name: qualified_last_segment(name: variant_name), source_indices: source_indices) {
Present { value: scrut_child } => node_lookup_resolved(node: scrut_child)
Absent => node_lookup_resolved(node: variant_child)
}
Absent =>
variant_not_found_result(scrut: scrut_node, variant_name: variant_name, module_name: module_name, source_indices: source_indices)
}
Expand Down
12 changes: 11 additions & 1 deletion src/v1/stage0/src/v1_compiler_infer_patterns.rs
Original file line number Diff line number Diff line change
Expand Up @@ -582,7 +582,17 @@ pub fn lookup_variant_in_type(
qualified_last_segment(variant_name.clone()),
source_indices.clone(),
) {
Some(variant_child) => node_lookup_resolved(variant_child.clone()),
Some(variant_child) => match find_child_named(
expand_scrut_type_for_variant_lookup(
scrut_node.clone(),
env.clone(),
),
qualified_last_segment(variant_name.clone()),
source_indices.clone(),
) {
Some(scrut_child) => node_lookup_resolved(scrut_child.clone()),
None => node_lookup_resolved(variant_child.clone()),
},
None => variant_not_found_result(
scrut_node.clone(),
variant_name.clone(),
Expand Down
Loading