Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
e985c22
Close gate 61 function-valued data receipt
briansrls May 14, 2026
6fe9583
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
820b75a
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
18493ee
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
f81222d
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
88b3a75
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
6f04ef0
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
b0b4ce5
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
bc66bef
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
887b888
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
04a8681
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
08db2a3
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
5f97570
Use canonical DimensionReport in gate 61 receipt
briansrls May 14, 2026
2b40770
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
147c923
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
5149df4
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
d79acde
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
d330028
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
de92d90
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
38d26c3
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
98bb48e
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
c9f7619
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
7934119
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 2026
55d0b88
Merge remote-tracking branch 'origin/main' into session/gentle-eagle-11
briansrls May 14, 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
16 changes: 16 additions & 0 deletions src/v3/compiler/tests/fixtures/r3_class_2_function_valued_data.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,21 @@
// R3 Class 2 gap representative: function-valued data is first-class.

import std.list { List, Empty, Cons }
import v3.std.dimensions { DimensionReport, Witness }

data add_one: fn(Int) -> Int = |x| x + 1

fn gate61_empty_int_witnesses() -> List<Witness<Int>> = Empty

fn gate61_int_witnesses(c: Int) -> List<Witness<Int>> =
Cons { head: Inhabits(c), tail: gate61_empty_int_witnesses() }

data report_int: fn(Int) -> DimensionReport<Int> =
|x| DimensionOk {
dimension_name: "function-valued-data",
composed: x,
witnesses: gate61_int_witnesses(x)
}

fn test_function_valued_data() -> Int = add_one(41)
fn test_function_valued_dimension_report() -> DimensionReport<Int> = report_int(42)
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,14 @@ fn substrate_gap_function_valued_data_executes_through_evaluator() {
.collect();
assert_eq!(
user_defined_arrow_names,
vec!["add_one", "test_function_valued_data"],
vec![
"add_one",
"gate61_empty_int_witnesses",
"gate61_int_witnesses",
"report_int",
"test_function_valued_data",
"test_function_valued_dimension_report",
],
"only the named data callable and named caller should carry executable Arrow bodies"
);
assert!(
Expand All @@ -207,6 +214,80 @@ fn substrate_gap_function_valued_data_executes_through_evaluator() {
assert_eq!(value, Value::LiteralValue(literal_bits_int(42)));
}

#[test]
fn substrate_gap_function_valued_data_produces_dimension_report() {
let dag = cached_compile_to_dag(SOURCE, FILE);
assert!(
dag.diagnostics().is_empty(),
"representative must compile without diagnostics: {:?}",
dag.diagnostics()
);

let report_int = dag
.declaration_by_name("report_int")
.expect("function-valued DimensionReport data")
.id;
let report_int_decl = dag.declaration(report_int);
assert!(
report_int_decl.value_body.is_none(),
"`report_int` must lower as executable function-valued data"
);
assert!(
matches!(
&report_int_decl.connective,
TypeConnective::Arrow {
body: ArrowBody::UserDefined(_),
..
}
),
"`report_int` must carry a UserDefined Arrow body"
);
assert!(
dag.nodes().iter().any(|node| {
matches!(
node,
Behavior::Transform(t)
if matches!(&t.target, TransformTarget::Callable(target) if *target == report_int)
)
}),
"`report_int(42)` must lower to TransformTarget::Callable(report_int)"
);

let entry = bind_node_id_for_fn(&dag, "test_function_valued_dimension_report");
let mut state = EvalStateStack::with_root_frame(EvalFrame::empty());
let strategy = EvalStrategy::ApplicativeOrder {
input_order: InputEvaluationOrder::LeftFirst,
};
let value = evaluate_body(&dag, entry, &mut state, strategy)
.expect("function-valued data should produce DimensionReport through evaluator");

let Value::VariantValue { tag, payload } = value else {
panic!("expected DimensionReport::DimensionOk VariantValue");
};
let variant_label = dag.declarations().iter().find_map(|decl| {
let TypeConnective::Disj { variants } = &decl.connective else {
return None;
};
variants
.iter()
.find(|variant| variant.ty == tag)
.map(|variant| variant.label.as_str())
});
assert_eq!(
variant_label,
Some("DimensionOk"),
"E6-G0d must materialize the canonical DimensionOk variant constructor"
);
let Value::RecordValue(fields) = *payload else {
panic!("DimensionOk payload must be a RecordValue");
};
let composed = fields
.iter()
.find(|field| field.label == "composed")
.expect("DimensionOk.composed field");
assert_eq!(composed.value, Value::LiteralValue(literal_bits_int(42)));
}

#[test]
fn function_valued_data_recursion_fails_closed() {
let dag = cached_compile_any(
Expand Down
Loading