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
73 changes: 73 additions & 0 deletions src/v2/tests/src/fn_as_value_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -139,3 +139,76 @@ fn use_bad() -> Int { apply_rec(x: Rec { v: 7 }, g: fn(r) { r.nope }) }
"r.nope on instantiated Rec (T=Rec) must fail closed (diagnostic or eval error), not silently succeed"
);
}

// ── Generic FreeMonoid fold callback instantiation (R2 §4a) ─────────────
// fold_list/fold_list_right cons|snoc callbacks must bind T from xs: FreeMonoid<T>
// so the second lambda param is concrete (field access / arithmetic type-checks).

#[test]
fn fold_list_generic_cons_callback_binds_element_type() {
let src = r#"module test.fold_gi
type Rec { v: Int }
type FreeMonoid<T> = Empty | Cons { head: T, tail: FreeMonoid<T> }
fn fold_list<T, A>(xs: FreeMonoid<T>, empty: A, cons: fn(A, T) -> A) -> A {
match xs {
Empty => empty
Cons { head: h, tail: t } => fold_list(xs: t, empty: cons(empty: empty, h: h), cons: cons)
}
}
fn sum_ints() -> Int {
fold_list(xs: [1, 2, 3], empty: 0, cons: fn(acc, h) { acc + h })
}
fn field_access() -> Int {
let xs = [Rec { v: 1 }, Rec { v: 2 }]
fold_list(xs: xs, empty: 0, cons: fn(acc, r) { acc + r.v })
}
"#;
let sources = resolve_imports_transitively("test.dag", src);
let resolved = compile_to_resolved(Rc::new(sources));
assert_resolved_no_hard_errors(&resolved);
let graph = resolved
.graph
.as_ref()
.expect("graph after successful resolve");
match v2_interpreter::run(graph, resolved.source_indices.clone(), "sum_ints") {
Ok(Value::Int(6)) => {}
other => panic!("expected Int(6) from fold_list sum, got {other:?}"),
}
match v2_interpreter::run(graph, resolved.source_indices.clone(), "field_access") {
Ok(Value::Int(3)) => {}
other => {
panic!("expected Int(3) (T=Rec from xs, cons r: Rec, r.v field access), got {other:?}")
}
}
}

#[test]
fn fold_list_right_generic_snoc_callback_binds_element_type() {
let src = r#"module test.fold_right_gi
type Rec { v: Int }
type FreeMonoid<T> = Empty | Cons { head: T, tail: FreeMonoid<T> }
fn fold_list_right<T, A>(xs: FreeMonoid<T>, empty: A, snoc: fn(A, T) -> A) -> A {
match xs {
Empty => empty
Cons { head: h, tail: t } => snoc(fold_list_right(xs: t, empty: empty, snoc: snoc), h)
}
}
fn field_access() -> Int {
let xs = [Rec { v: 4 }, Rec { v: 5 }]
fold_list_right(xs: xs, empty: 0, snoc: fn(acc, r) { acc + r.v })
}
"#;
let sources = resolve_imports_transitively("test.dag", src);
let resolved = compile_to_resolved(Rc::new(sources));
assert_resolved_no_hard_errors(&resolved);
let graph = resolved
.graph
.as_ref()
.expect("graph after successful resolve");
match v2_interpreter::run(graph, resolved.source_indices.clone(), "field_access") {
Ok(Value::Int(9)) => {}
other => {
panic!("expected Int(9) (T=Rec from xs, snoc r: Rec, r.v field access), got {other:?}")
}
}
}
89 changes: 89 additions & 0 deletions src/v2/tests/src/fold_list_generic_instantiation_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
//! v2 R2 generic instantiation — fold_list/fold_list_right cons|snoc callbacks bind T
//! from xs: FreeMonoid<T> (dep-graph-2026-06-12 §4a / tidy-stag-172).
//!
//! Executes the v4 witness through the real v2 compile+interpret pipeline (same path as
//! `gunbc run --source-root src/v4` claim runners).

use std::rc::Rc;
use std::sync::OnceLock;

use v2_compiler::v2_compiler_compile::{compile_to_resolved, ResolvedPipelineResult, SourceFile};
use v2_compiler::v2_interpreter::{self, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

const CERT_ENTRY: &str = "src/v4/test/claim/manual/fold_list_generic_instantiation.dag";
const WITNESS_FN: &str = "fold_list_generic_instantiation_holds";

fn v4_source_roots() -> Vec<std::path::PathBuf> {
vec![workspace_root().join("src/v4")]
}

fn cert_source_pairs() -> &'static Vec<(String, String)> {
static CACHE: OnceLock<Vec<(String, String)>> = OnceLock::new();
CACHE.get_or_init(|| {
let entry_content = std::fs::read_to_string(workspace_root().join(CERT_ENTRY))
.unwrap_or_else(|e| panic!("read {CERT_ENTRY}: {e}"));
resolve_imports_transitively_with_source_roots(
CERT_ENTRY,
&entry_content,
&v4_source_roots(),
)
.iter()
.map(|s| (s.path.clone(), s.content.clone()))
.collect()
})
}

fn cert_sources() -> Vec<Rc<SourceFile>> {
cert_source_pairs()
.iter()
.map(|(path, content)| {
Rc::new(SourceFile {
path: path.clone(),
content: content.clone(),
})
})
.collect()
}

fn assert_resolved_ok(resolved: &ResolvedPipelineResult) {
let msgs: Vec<String> = resolved
.diagnostics
.iter()
.map(|d| v2_compiler::v2_std_core::diagnostic_to_message(d.diagnostic.clone()))
.filter(|m| !m.starts_with("complexity: "))
.collect();
assert!(
msgs.is_empty() && resolved.graph.is_some(),
"expected resolved graph for {CERT_ENTRY}, got diagnostics {msgs:?} (graph present: {})",
resolved.graph.is_some()
);
}

#[test]
fn v4_fold_list_generic_instantiation_holds() {
let resolved = compile_to_resolved(Rc::new(cert_sources()));
assert_resolved_ok(&resolved);
let graph = resolved
.graph
.as_ref()
.expect("graph after successful resolve");
match v2_interpreter::run(graph, resolved.source_indices.clone(), WITNESS_FN) {
Ok(Value::Bool(true)) => {}
other => panic!(
"expected Bool(true) from {WITNESS_FN} (fold_list cons/snoc bind T from xs), got {other:?}"
),
}
}

#[test]
fn v4_name_resolve_compiles_with_fold_list_dissolution() {
const ENTRY: &str = "src/v4/compiler/03_name_resolve.dag";
let entry_content = std::fs::read_to_string(workspace_root().join(ENTRY))
.unwrap_or_else(|e| panic!("read {ENTRY}: {e}"));
let sources =
resolve_imports_transitively_with_source_roots(ENTRY, &entry_content, &v4_source_roots());
let resolved = compile_to_resolved(Rc::new(sources));
assert_resolved_ok(&resolved);
}
2 changes: 2 additions & 0 deletions src/v2/tests/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ mod effects;
#[cfg(test)]
mod fn_as_value_test;
#[cfg(test)]
mod fold_list_generic_instantiation_test;
#[cfg(test)]
mod generator_match_arm_test;
#[cfg(test)]
mod infer_semantics;
Expand Down
54 changes: 22 additions & 32 deletions src/v4/compiler/03_name_resolve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ import v4.extdeps.languages.dag {
dag_surface_module_header_metadata_edge,
qualified_name_from_module_node
}
import v4.std.algebra { Cons, Empty, FreeMonoid }
import v4.std.algebra { Cons, Empty, FreeMonoid, fold_list }
import v4.std.collection { Absent, Map, Present, empty_map, map_get, map_insert, optional_absent, optional_present }
import v4.std.diagnostic {
Accepted,
Expand Down Expand Up @@ -168,29 +168,26 @@ fn admit_export_symbol(
}


// 🟡 gated — fold_list bootstrap-limitation interim — feature: fold-list-generic-qualified-name — hand-rolls Empty/Cons accumulation over FreeMonoid<QualifiedName>; dissolve-on-arrival: v2 bootstrap fixes FreeMonoid<T> generic type inference for user-defined T.
fn module_root_name_find_fold(
names: FreeMonoid<QualifiedName>,
name: QualifiedName,
acc: ModuleRootNameFindState
) -> ModuleRootNameFindState {
match names {
Empty => acc
Cons { head: candidate, tail: rest } =>
module_root_name_find_fold(
names: rest,
name: name,
acc: if qualified_name_eq(a: candidate, b: name) {
match acc {
ModuleRootNameNotFound => ModuleRootNameFoundOnce
ModuleRootNameFoundOnce => ModuleRootNameFoundDuplicate
ModuleRootNameFoundDuplicate => ModuleRootNameFoundDuplicate
}
} else {
acc
fold_list(
xs: names,
empty: acc,
cons: fn(st, candidate) {
if qualified_name_eq(a: candidate, b: name) {
match st {
ModuleRootNameNotFound => ModuleRootNameFoundOnce
ModuleRootNameFoundOnce => ModuleRootNameFoundDuplicate
ModuleRootNameFoundDuplicate => ModuleRootNameFoundDuplicate
}
)
}
} else {
st
}
}
)
}


Expand Down Expand Up @@ -433,20 +430,13 @@ fn admit_imports(
imports: FreeMonoid<Import>,
state: AdmissionState
) -> AdmissionState {
// 🟡 gated — fold_list bootstrap-limitation interim — feature: fold-list-generic-import — hand-rolls Empty/Cons accumulation over FreeMonoid<Import>; dissolve-on-arrival: v2 bootstrap fixes FreeMonoid<T> generic type inference for user-defined T.
match imports {
Empty => state
Cons { head: import_edge, tail: rest } =>
admit_imports(
roots: roots,
imports: rest,
state: admit_import_entry(
roots: roots,
import_edge: import_edge,
state: state
)
)
}
fold_list(
xs: imports,
empty: state,
cons: fn(acc, import_edge) {
admit_import_entry(roots: roots, import_edge: import_edge, state: acc)
}
)
}


Expand Down
27 changes: 27 additions & 0 deletions src/v4/test/claim/manual/fold_list_generic_instantiation.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// Manual execution cert: v2 R2 generic instantiation binds fold_list cons/snoc
// callback element type T from xs: FreeMonoid<T> (dep-graph-2026-06-12 §4a).
module test.claim.fold_list_generic_instantiation

import v4.std.algebra { Cons, Empty, fold_list, fold_list_right }

type Rec { v: Int }

fn fold_list_sum_ints() -> Int {
fold_list(xs: [1, 2, 3], empty: 0, cons: fn(acc, h) { acc + h })
}

fn fold_list_field_access() -> Int {
let xs = [Rec { v: 1 }, Rec { v: 2 }]
fold_list(xs: xs, empty: 0, cons: fn(acc, r) { acc + r.v })
}

fn fold_list_right_field_access() -> Int {
let xs = [Rec { v: 4 }, Rec { v: 5 }]
fold_list_right(xs: xs, empty: 0, snoc: fn(acc, r) { acc + r.v })
}

fn fold_list_generic_instantiation_holds() -> Bool {
fold_list_sum_ints() == 6
&& fold_list_field_access() == 3
&& fold_list_right_field_access() == 9
}
Loading