Skip to content
Closed
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
122 changes: 122 additions & 0 deletions src/v3/compiler/src/eval_substrate_reify.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
//! E6-G1.a — evaluator-owned substrate `Dag` reification for [`crate::evaluator::evaluate_body`].
//!
//! User `data … : Dag = …` literals remain class-5 blocked; this module bridges compiled
//! [`crate::dag::Dag`] graphs into the five-variant [`crate::evaluator::Value`] carrier without
//! routing the API through [`crate::lens_apply::apply_lens_declaration`] (compatibility seam only).
//!
//! **Program scope:** [`reify_compiled_dag_as_substrate_value`] names whole-`Dag` authority: it
//! reflects **every** behavior in `program.nodes()` in graph order — no `source_file` filter and
//! no inheritance of [`crate::lens_apply::reflect_program_dag_nodes_in_file`] narrowing.
//!
//! **Variant payload fields:** [`eval_constructor_variant_payload_fields`] is the public
//! reification-facing entry to the same [`crate::lower`] query used by the body evaluator when
//! lowering `FieldValue::Variant` into [`Value::VariantValue`].
//!
//! **Declaration references:** `runtime.dag` locks [`Value`] to five variants and does not carry
//! `DeclarationId` as a first-class inhabitant. [`field_value_to_eval_value`] therefore encodes
//! [`FieldValue::Reference`] as [`LiteralBits::Int`] holding [`DeclarationId::raw`] (sign-extended
//! to `i64`). This is an explicit host-bridge contract for reflected substrate facts (e.g.
//! [`TransformTarget::Callable`], [`BranchPattern::ResolvedVariant`]); user programs must not rely
//! on mathematical `Int` semantics for those handles until the substrate value model grows a typed
//! declaration reference.

use crate::dag::{Dag, DeclarationId, FieldValue, LiteralBits};
use crate::evaluator::{NamedField, Value};
use crate::lens_apply::{empty_substrate_list_value, reflect_program_nodes_whole_dag, LensApplyError};

/// Resolves variant-constructor payload field labels for eager reification into
/// [`Value::VariantValue`], delegating to [`crate::lower::eval_constructor_variant_payload_fields`].
pub fn eval_constructor_variant_payload_fields(
dag: &Dag,
callee_decl: DeclarationId,
) -> Option<Vec<(String, DeclarationId)>> {
crate::lower::eval_constructor_variant_payload_fields(dag, callee_decl)
}

/// Convert structural [`FieldValue`] (from whole-dag reflection) into [`Value`].
///
/// See the module note on [`FieldValue::Reference`] encoding.
pub fn field_value_to_eval_value(dag: &Dag, fv: &FieldValue) -> Result<Value, LensApplyError> {
match fv {
FieldValue::Literal(bits) => Ok(Value::LiteralValue(bits.clone())),
FieldValue::Reference(id) => Ok(Value::LiteralValue(LiteralBits::Int(id.raw() as i64))),
FieldValue::List(_) => Err(LensApplyError::SubstrateReflect(
"FieldValue::List is not reified; reflection uses Cons spines",
)),
FieldValue::Map(_) => Err(LensApplyError::SubstrateReflect(
"FieldValue::Map is not reified into evaluator Value (E6-G1.a)",
)),
FieldValue::Record(rec) => {
let mut fields = Vec::with_capacity(rec.len());
for (label, child) in rec {
fields.push(NamedField {
label: label.clone(),
value: field_value_to_eval_value(dag, child)?,
});
}
Ok(Value::RecordValue(fields))
}
FieldValue::Variant {
constructor,
payload,
} => {
let field_defs = eval_constructor_variant_payload_fields(dag, *constructor)
.ok_or(LensApplyError::SubstrateReflect(
"variant constructor payload fields missing",
))?;
if field_defs.len() != payload.len() {
return Err(LensApplyError::SubstrateReflect(
"variant payload arity mismatch for eval reification",
));
}
let converted: Vec<Value> = payload
.iter()
.map(|p| field_value_to_eval_value(dag, p))
.collect::<Result<_, _>>()?;
let inner = if field_defs.len() == 1 && field_defs[0].0 == "_0" {
converted.into_iter().next().expect("length checked")
} else {
Value::RecordValue(
field_defs
.into_iter()
.zip(converted)
.map(|((label, _), value)| NamedField { label, value })
.collect(),
)
};
Ok(Value::VariantValue {
tag: *constructor,
payload: Box::new(inner),
})
}
}
}

/// Build a substrate-typed `Dag` [`Value`] carrying **all** behaviors from `program.nodes()`.
///
/// `declarations`, `ports`, and `clusters` are empty lists (class-5 blocks structural `Dag` data
/// literals; those fields are not required by the G1.a static fold ratchet).
pub fn reify_compiled_dag_as_substrate_value(program: &Dag) -> Result<Value, LensApplyError> {
let empty_fv = empty_substrate_list_value(program)?;
let empty_val = field_value_to_eval_value(program, &empty_fv)?;
let nodes_fv = reflect_program_nodes_whole_dag(program)?;
let nodes_val = field_value_to_eval_value(program, &nodes_fv)?;
Ok(Value::RecordValue(vec![
NamedField {
label: "declarations".to_string(),
value: empty_val.clone(),
},
NamedField {
label: "nodes".to_string(),
value: nodes_val,
},
NamedField {
label: "ports".to_string(),
value: empty_val.clone(),
},
NamedField {
label: "clusters".to_string(),
value: empty_val,
},
]))
}
9 changes: 9 additions & 0 deletions src/v3/compiler/src/lens_apply.rs
Original file line number Diff line number Diff line change
Expand Up @@ -317,6 +317,15 @@ pub fn reflect_program_dag_nodes_in_file(
Ok(FieldValue::Record(vec![("nodes".to_string(), nodes)]))
}

/// Whole-`program.nodes()` reflection in graph order using `program` as id-space (no `source_file`
/// filter).
///
/// E6-G1.a: evaluator-owned [`crate::eval_substrate_reify`] uses this for Dag [`Value`] carriers.
/// Contrast [`reflect_program_dag_nodes_in_file`], which narrows by compilation unit.
pub fn reflect_program_nodes_whole_dag(program: &Dag) -> Result<FieldValue, LensApplyError> {
substrate_reflection::reflect_behavior_list(program, program.nodes()).map_err(Into::into)
}

/// PR-E (Evaluator): apply a lens declaration over
/// [`reflect_program_dag_nodes_in_file`] output (substrate-shaped `FieldValue` program spine).
///
Expand Down
1 change: 1 addition & 0 deletions src/v3/compiler/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2718,6 +2718,7 @@ mod int_literal_ranges;
/// T-LensAPI D1: bounded lens interpreter over substrate-shaped [`FieldValue`]
/// (see module docs in `lens_apply.rs`).
pub mod lens_apply;
pub mod eval_substrate_reify;
pub mod lens_testgen;

/// Effect-enumeration lens. Authority lives in
Expand Down
2 changes: 2 additions & 0 deletions src/v3/compiler/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,8 @@ mod canonical_lens_bridge_ratchet_test;
mod cementing_lens_registry_dispatch_test;
#[path = "integration/e_i_lane_induction_preflight_test.rs"]
mod e_i_lane_induction_preflight_test;
#[path = "integration/e6_g1a_static_lens_fold_test.rs"]
mod e6_g1a_static_lens_fold_test;
#[path = "integration/extdeps_rust_primitives_loader_test.rs"]
mod extdeps_rust_primitives_loader_test;
#[path = "integration/four_fixture_regression_test.rs"]
Expand Down
135 changes: 135 additions & 0 deletions src/v3/compiler/tests/integration/e6_g1a_static_lens_fold_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,135 @@
//! **Layer:** integration
//!
//! E6-G1.a — static top-level `Lens<C>` fold through the public body evaluator (Evaluator E3).
//!
//! Authority: `docs/briefs/r3-pr-e6-g1a-static-lens-fold-worker.md` (slice boundary + acceptance
//! gates). User `data … : Dag = …` literals remain class-5 blocked; the ratchet reifies a
//! substrate `Dag` [`v3_compiler::evaluator::Value`] via
//! [`v3_compiler::eval_substrate_reify::reify_compiled_dag_as_substrate_value`] (whole-program
//! `program.nodes()` order; no `source_file` filter). The fixture uses `std.list.fold`; the std
//! `fold` arrow remains an `ArrowBody::Unparsed` scaffold in the bootstrap dag, so the body
//! evaluator runs it through a small Rust intrinsic that mirrors the `list.dag` catamorphism.

use crate::common::cached_compile_to_dag;
use v3_compiler::dag::{ArrowBody, Behavior, TypeConnective};
use v3_compiler::eval_substrate_reify::reify_compiled_dag_as_substrate_value;
use v3_compiler::evaluator::{
evaluate_body, EvalFrame, EvalStateStack, EvalStrategy, InputEvaluationOrder, Value,
};

const G1A_SOURCE: &str = r#"
import std.list { List, empty, fold }
import std.substrate { Dag, Behavior, LoopBound }
import v3.std.dimensions { Witness, OptionalDiagnostic, DimensionReport }
import v3.std.diagnostics { Diagnostic }
import v3.std.lens { Lens }

fn tc1_empty_witnesses() -> List<Witness<Int>> = empty()
fn tc1_empty_violations() -> List<Diagnostic> = empty()

fn lens_read(d: Dag, b: Behavior) -> Witness<Int> { Inhabits(1) }
fn int_add(a: Int, b: Int) -> Int = a + b
fn int_max(a: Int, b: Int) -> Int = if a > b then a else b
fn lens_iterate(c: Int, bound: LoopBound) -> Int = c
fn lens_validate(d: Dag, c: Int) -> OptionalDiagnostic { NoDiagnostic }

data tc1_static_lens: Lens<Int> = {
name: "tc1_static",
read: lens_read,
sequential: { op: int_add, identity: 0 },
branch: int_max,
iterate: lens_iterate,
validate: lens_validate
}

fn tc1_composed(d: Dag) -> Int =
fold(
d.nodes,
tc1_static_lens.sequential.identity,
|acc, b|
match tc1_static_lens.read(d, b) {
Inhabits(c) => int_add(acc, c)
Violates { reason: r, at: beh } => acc
}
)

fn tc1_static_dimension_fold(d: Dag) -> DimensionReport<Int> =
match tc1_static_lens.validate(d, tc1_composed(d)) {
NoDiagnostic =>
DimensionOk {
dimension_name: "tc1_static",
composed: tc1_composed(d),
witnesses: tc1_empty_witnesses()
}
SomeDiagnostic { value: _diag } =>
DimensionFail {
dimension_name: "tc1_static",
violations: tc1_empty_violations(),
witnesses: tc1_empty_witnesses()
}
}

fn tc1_static_dimension_fold_eta(d: Dag) -> DimensionReport<Int> =
match tc1_static_lens.validate(d, 0 + tc1_composed(d)) {
NoDiagnostic =>
DimensionOk {
dimension_name: "tc1_static",
composed: 0 + tc1_composed(d),
witnesses: tc1_empty_witnesses()
}
SomeDiagnostic { value: _diag } =>
DimensionFail {
dimension_name: "tc1_static",
violations: tc1_empty_violations(),
witnesses: tc1_empty_witnesses()
}
}
"#;

const G1A_FILE: &str = "tc1_g1a_static_lens_fold.v3";

fn eval_dimension_report_fn(dag: &v3_compiler::dag::Dag, fn_name: &str, d_arg: Value) -> Value {
let decl = dag
.declaration_by_name(fn_name)
.unwrap_or_else(|| panic!("missing `{fn_name}`"));
let TypeConnective::Arrow { body, .. } = &decl.connective else {
panic!("`{fn_name}` must be an arrow");
};
let ArrowBody::UserDefined(bind_id) = body else {
panic!("`{fn_name}` must have a UserDefined body");
};
let bind_node_id = bind_id.node_id();
let Behavior::Bind(bind) = dag.node(bind_node_id) else {
panic!("bind node");
};
assert_eq!(bind.params.len(), 1, "`{fn_name}` expects one Dag parameter");
let d_port = bind.params[0];
let frame = EvalFrame::from_bindings([(d_port, d_arg)]).expect("frame");
let mut state = EvalStateStack::with_root_frame(frame);
let strategy = EvalStrategy::ApplicativeOrder {
input_order: InputEvaluationOrder::LeftFirst,
};
evaluate_body(dag, bind_node_id, &mut state, strategy)
.unwrap_or_else(|e| panic!("evaluate `{fn_name}`: {e:?}"))
}

#[test]
fn e6_g1a_static_lens_fold_executes_tc1_dimension_report_pair() {
let dag = cached_compile_to_dag(G1A_SOURCE, G1A_FILE);
assert!(
dag.diagnostics().is_empty(),
"G1.a fixture should compile cleanly: {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
);

let d_value = reify_compiled_dag_as_substrate_value(&dag)
.expect("reify substrate Dag Value for evaluator");

let left = eval_dimension_report_fn(&dag, "tc1_static_dimension_fold", d_value.clone());
let right = eval_dimension_report_fn(&dag, "tc1_static_dimension_fold_eta", d_value);

assert_eq!(
left, right,
"Pattern-A TC1 static pair: eta-expanded fold body must agree with direct fold"
);
}