Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
0d16578
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
3b1e525
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
803e41c
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
c367634
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
5fec077
fix(no_dual_representation_test): address review — audit all fns, unr…
Jul 1, 2026
b2e3b3f
fix(no_dual_representation_test): generic eq-site extraction, delete …
Jul 1, 2026
25780ca
refactor(no_dual_representation_test): Node facts via fn_arrow_decl, …
Jul 1, 2026
e0fe110
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
9c475e1
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
bf27fba
fix(no_dual_representation_test): unify literal fingerprint authority
Jul 1, 2026
19c07ca
fix(data_index): remove unsupported // comments breaking parse
Jul 1, 2026
a224c86
Merge remote-tracking branch 'origin/main' into session/swift-carp-820
Jul 1, 2026
b1bfd45
docs(no_dual_representation_test): name #5364 dissolution for data_in…
Jul 1, 2026
db11f26
Merge remote-tracking branch 'origin/main' into session/swift-carp-820
Jul 1, 2026
8ff447f
style(coproduct_reflection): cargo fmt data_init_literal_fingerprint …
Jul 1, 2026
5c79c09
fix(data_index): fingerprint data-init literals from source lexeme
Jul 1, 2026
dd26703
WIP: Rebuild the no-dual-representation-test lens PURELY in v2/.dag (…
Jul 1, 2026
cb068a7
docs(no_dual_representation_test): document residue lens scope nits
Jul 1, 2026
981ecea
Merge remote-tracking branch 'origin/main' into session/swift-carp-820
Jul 1, 2026
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
88 changes: 87 additions & 1 deletion src/v1/stage0/src/coproduct_reflection.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use crate::v1_interpreter::{
};
use crate::v1_std_core::{
authored_name_at, expr_var_name_at, field_node_type_expr, inferred_to_node, param_node_name_at,
Connective, ExprData, NewlineIndex, Node, VarBindingKind,
source_text_at, Connective, ExprData, NewlineIndex, Node, VarBindingKind,
};

pub(crate) const NULLARY_PAYLOAD_TYPE_NAME: &str = "coproduct_nullary_payload";
Expand Down Expand Up @@ -1197,6 +1197,92 @@ pub fn eval_fn_arrow_decl_facts_live(
Ok(crate::v1_interpreter::list_value(rows))
}

fn literal_source_lexeme(
node: &Rc<Node>,
si: &Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> Option<String> {
let index = si.get(&node.span.file)?;
let text = source_text_at(index.clone(), node.span.clone());
if text.is_empty() {
None
} else {
Some(text)
}
}

fn data_init_literal_fingerprint(
body: &Rc<Node>,
si: &Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> Option<String> {
// Encoding must match `v2.std.data_index` (`literal_fingerprint_*_lexeme`).
let lexeme = literal_source_lexeme(body, si)?;
match body.expr_data.as_ref() {
ExprData::ExprLiteral { value, .. } => match value.as_ref() {
crate::std_syntax::LiteralValue::LitInt { .. }
| crate::std_syntax::LiteralValue::LitFloat { .. } => Some(format!("num:{lexeme}")),
crate::std_syntax::LiteralValue::LitBool { .. } => Some(format!("bool:{lexeme}")),
// Str uses decoded content, not source lexeme: witness RHS is a skeleton atom
// name (bare content), so this matches `literal_fingerprint_str_content` when the
// initializer is a plain quoted literal without escapes.
crate::std_syntax::LiteralValue::LitStr { value: s, .. } => {
Some(format!("str:\"{s}\""))
}
_ => None,
},
_ => None,
}
}

// Corpus-wide data-init reflection: sibling of `eval_fn_arrow_decl_facts_live` and
// `eval_concept_decl_facts_live`. Yields one `DataInitDecl` per `ItemKind::DataItem` whose
// initializer is a literal, carrying `literal_fp` for literal-mirror detection in
// `v2.lens.no_dual_representation_test`. Host SOURCE half; dissolves with
// `fn_arrow_decl_facts_live` / `concept_decl_facts_live` on the same gunbc#5364
// corpus-as-node accessor widen trigger named in `v2.lens.wiring_liveness`'s
// construction_justification. Fingerprint encoding spec: `v2.std.data_index`
// (`literal_fingerprint_*_lexeme`); this host block is a transient SOURCE projection on
// the gunbc#5364 corpus-accessor widen — not an independent authority.
pub fn eval_data_init_decl_facts_live(
ctx: &InterpContext,
_args: &[(Option<String>, Value)],
) -> InterpResult<Value> {
let si = ctx.source_indices();
let mut rows: Vec<Value> = Vec::new();
for module in ctx.modules.iter() {
for item in module.items.iter() {
let name = authored_name_at(si.clone(), item.clone());
if name.is_empty() {
continue;
}
let info = module
.item_registry
.get(&name)
.or_else(|| module.item_registry.get(&item.name));
let Some(info) = info else { continue };
if info.kind != ItemKind::DataItem {
continue;
}
let Some(body) = item.body.as_ref() else {
continue;
};
let Some(literal_fp) = data_init_literal_fingerprint(body, &si) else {
continue;
};
let qualified_name = logical_qualified_name(&info.module_name, &name);
rows.push(Value::Record {
type_name: ctx.sym("DataInitDecl"),
fields: Rc::new(sorted_fields(vec![
(ctx.sym("qualified_name"), Value::Str(qualified_name)),
(ctx.sym("module"), Value::Str(info.module_name.clone())),
(ctx.sym("name"), Value::Str(name.clone())),
(ctx.sym("literal_fp"), Value::Str(literal_fp)),
])),
});
}
}
Ok(crate::v1_interpreter::list_value(rows))
}

fn variant_is_nullary(variant: &Rc<Node>) -> bool {
variant.children.is_empty()
}
Expand Down
24 changes: 24 additions & 0 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2139,6 +2139,8 @@ pub(crate) const STD_CONCEPT_INDEX_BRIDGE_FNS: &[&str] = &["concept_decl_facts_l

pub(crate) const STD_FN_INDEX_BRIDGE_FNS: &[&str] = &["fn_arrow_decl_facts_live"];

pub(crate) const STD_DATA_INDEX_BRIDGE_FNS: &[&str] = &["data_init_decl_facts_live"];

pub fn std_node_bridge_fn_names() -> &'static [&'static str] {
STD_NODE_BRIDGE_FNS
}
Expand All @@ -2155,6 +2157,10 @@ pub fn std_fn_index_bridge_fn_names() -> &'static [&'static str] {
STD_FN_INDEX_BRIDGE_FNS
}

pub fn std_data_index_bridge_fn_names() -> &'static [&'static str] {
STD_DATA_INDEX_BRIDGE_FNS
}

pub fn std_qualified_name_bridge_fn_names() -> &'static [&'static str] {
STD_QUALIFIED_NAME_BRIDGE_FNS
}
Expand Down Expand Up @@ -2195,6 +2201,15 @@ fn is_v4_std_fn_index_bridge_call(ctx: &InterpContext, func_name: &str) -> bool
.is_some_and(|info| info.module_name == "v2.std.fn_index")
}

fn is_v4_std_data_index_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
if !STD_DATA_INDEX_BRIDGE_FNS.contains(&func_name) {
return false;
}
ctx.item_registry
.get(func_name)
.is_some_and(|info| info.module_name == "v2.std.data_index")
}

fn is_v4_std_lexing_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
if !STD_LEXING_BRIDGE_FNS.contains(&func_name) {
return false;
Expand Down Expand Up @@ -2290,6 +2305,15 @@ fn eval_call(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResul
};
}

if is_v4_std_data_index_bridge_call(ctx, &func_name) {
return match func_name.as_str() {
"data_init_decl_facts_live" => {
crate::coproduct_reflection::eval_data_init_decl_facts_live(ctx, &args)
}
_ => unreachable!("data_index bridge fn set mismatch"),
};
}

match func_name.as_str() {
"fold_list" => return eval_fold_list_native(&args, env, ctx),
"fold_list_right" => return eval_fold_list_right_native(&args, env, ctx),
Expand Down
10 changes: 10 additions & 0 deletions src/v1/tests/src/coproduct_reflection_conformance_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,12 @@ fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() {
"eval_call intercept must wire v2.std.fn_index bridge `{name}`"
);
}
for name in v1_interpreter::std_data_index_bridge_fn_names() {
assert!(
source.contains(&format!("\"{name}\" =>")),
"eval_call intercept must wire v2.std.data_index bridge `{name}`"
);
}
assert!(
source.contains("is_v4_std_node_bridge_call"),
"eval_call must gate v2.std.node bridge dispatch"
Expand All @@ -97,6 +103,10 @@ fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() {
source.contains("is_v4_std_fn_index_bridge_call"),
"eval_call must gate v2.std.fn_index bridge dispatch"
);
assert!(
source.contains("is_v4_std_data_index_bridge_call"),
"eval_call must gate v2.std.data_index bridge dispatch"
);
}

#[test]
Expand Down
53 changes: 53 additions & 0 deletions src/v2/lens/no_dual_representation_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
module v2.lens.no_dual_representation_test

import gunbc.ci_layer_roots { witness_layer_roots }
import std.disposition { RealizationDispatch }
import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
import v2.lens.module_graph { module_declaration_facts_live }
import v2.lens.no_dual_representation_test.scan {
DualRepModuleRef,
DualRepModuleScan,
dual_rep_clean_holds_for_scans,
dual_rep_module_scans_from_fn_index,
dual_rep_test_file_count_from_scans,
dual_rep_violation_count_from_scans,
empty_dual_rep_module_refs
}
import v2.std.algebra { fold_list, list_snoc_item }
import v2.std.collection { List }
import v2.std.logic { Bool }

fn module_refs_from_declaration_facts(pool_roots: List<String>) -> List<DualRepModuleRef> {
fold_list(
xs: module_declaration_facts_live(pool_roots: pool_roots),
empty: empty_dual_rep_module_refs,
cons: fn(acc, decl) {
list_snoc_item(
xs: acc,
item: DualRepModuleRef { module: decl.module, path: decl.path }
)
}
)
}

fn dual_rep_live_module_scans() -> List<DualRepModuleScan> {
dual_rep_module_scans_from_fn_index(
modules: module_refs_from_declaration_facts(pool_roots: witness_layer_roots)
)
}

fn no_dual_representation_test_live_count() -> Int {
dual_rep_violation_count_from_scans(scans: dual_rep_live_module_scans())
}

fn no_dual_representation_test_live_file_count() -> Int {
dual_rep_test_file_count_from_scans(scans: dual_rep_live_module_scans())
}

fn no_dual_representation_test_clean_holds() -> Bool {
dual_rep_clean_holds_for_scans(scans: dual_rep_live_module_scans())
}

data construction_justification: ConstructionJustification = ConstructionJustification {
class: WallAfterGrounding { dissolves_to: RealizationDispatch }
}
Loading
Loading