Skip to content
19 changes: 17 additions & 2 deletions src/v3/grounding_coercion_fold/src/fold.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
//!
//! ## Design authority (`docs/design-emission-model.md`)
//!
//! Worked **Examples 1–7** in that doc are behavioral targets. **Examples 1, 2, 5, and 6** are
//! Worked examples in that doc are behavioral targets. **Examples 1, 2, 5, 6, and 8** are
//! implemented for the [`LanguageSpecProjection::ScratchIntExamples`](crate::types::LanguageSpecProjection::ScratchIntExamples)
//! checkpoint path only; other examples and `Undeclared` remain
//! [`EmissionDiagnostic::FoldNotImplemented`](crate::diagnostic::EmissionDiagnostic::FoldNotImplemented).
Expand Down Expand Up @@ -39,13 +39,25 @@ fn fold_design_doc_example_6_no_inhabitant() -> Result<TargetInhabitance, Emissi
Err(EmissionDiagnostic::NoInhabitant)
}

fn fold_design_doc_example_8_rust() -> Result<TargetInhabitance, EmissionDiagnostic> {
Ok(TargetInhabitance::RustI32)
}

fn fold_design_doc_example_8_python() -> Result<TargetInhabitance, EmissionDiagnostic> {
Ok(TargetInhabitance::PythonInt)
}

fn fold_design_doc_example_8_go() -> Result<TargetInhabitance, EmissionDiagnostic> {
Ok(TargetInhabitance::GoInt32)
}

/// Structural fold: program + lifetime analysis + LanguageSpec projection →
/// per-binding target inhabitances, **or** a single typed diagnostic.
///
/// - [`LanguageSpecProjection::Undeclared`](crate::types::LanguageSpecProjection::Undeclared): fail-closed
/// [`EmissionDiagnostic::FoldNotImplemented`](crate::diagnostic::EmissionDiagnostic::FoldNotImplemented).
/// - [`LanguageSpecProjection::ScratchIntExamples`](crate::types::LanguageSpecProjection::ScratchIntExamples): runs
/// design-doc Int Examples 1, 2, 5, and 6 for a single synthetic binding [`BindingId`](v3_grounding_lifetime::BindingId)`(0)`.
/// design-doc Int Examples 1, 2, 5, 6, and 8 for a single synthetic binding [`BindingId`](v3_grounding_lifetime::BindingId)`(0)`.
/// **Checkpoint:** ignores `_dag` by design; on the scratch path, `lifetime_facts` must be
/// empty in debug builds until this body reads real facts. Do not widen this arm to multiple
/// bindings or real program facts without landing the declared projection / dissolution path
Expand Down Expand Up @@ -79,6 +91,9 @@ pub fn fold_program_to_target(
IntScratchExample::DesignDocExample6NoInhabitant => {
fold_design_doc_example_6_no_inhabitant()?
}
IntScratchExample::DesignDocExample8Rust => fold_design_doc_example_8_rust()?,
IntScratchExample::DesignDocExample8Python => fold_design_doc_example_8_python()?,
IntScratchExample::DesignDocExample8Go => fold_design_doc_example_8_go()?,
};
Ok(BTreeMap::from([(binding, inhabitance)]))
}
Expand Down
48 changes: 39 additions & 9 deletions src/v3/grounding_coercion_fold/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
//! and **§Example 2** (`Int(0..2^32)` / `Semiring` exact-bound → [`TargetInhabitance::RustU32`](types::TargetInhabitance::RustU32))
//! plus **§Example 5** (same bound without algebra annotation → `UnderRefined("algebra")`)
//! and **§Example 6** (`Int(0..2^65)` → [`EmissionDiagnostic::NoInhabitant`](diagnostic::EmissionDiagnostic::NoInhabitant))
//! and **§Example 8** (`Int(-2^31..2^31)` → Rust `i32`, Python `int`, Go `int32`)
//! for a single synthetic binding — checkpoint until a real LanguageSpec projection replaces
//! the scratch carrier (manager #1133 / #1286).
//!
Expand All @@ -39,6 +40,18 @@ mod tests {

use super::*;

fn assert_single_binding_inhabitance(example: IntScratchExample, expected: TargetInhabitance) {
let dag = Dag::new();
let lifetime: LifetimeAnalysisReport = Default::default();
let spec = LanguageSpecProjection::ScratchIntExamples(example);
let got = fold_program_to_target(&dag, &lifetime, &spec).expect("ok");
assert_eq!(got.len(), 1);
assert_eq!(
got.get(&v3_grounding_lifetime::BindingId(0)),
Some(&expected)
);
}

#[test]
fn fold_undeclared_projection_stays_fold_not_implemented() {
let dag = Dag::new();
Expand Down Expand Up @@ -66,16 +79,9 @@ mod tests {

#[test]
fn design_doc_example_2_bounded_int_emits_rust_u32() {
let dag = Dag::new();
let lifetime: LifetimeAnalysisReport = Default::default();
let spec = LanguageSpecProjection::ScratchIntExamples(
assert_single_binding_inhabitance(
IntScratchExample::DesignDocExample2BoundedU32,
);
let got = fold_program_to_target(&dag, &lifetime, &spec).expect("ok");
assert_eq!(got.len(), 1);
assert_eq!(
got.get(&v3_grounding_lifetime::BindingId(0)),
Some(&TargetInhabitance::RustU32)
TargetInhabitance::RustU32,
);
}

Expand Down Expand Up @@ -105,4 +111,28 @@ mod tests {
let err = fold_program_to_target(&dag, &lifetime, &spec).expect_err("no inhabitant");
assert_eq!(err, EmissionDiagnostic::NoInhabitant);
}

#[test]
fn fold_dag_int_refined_cross_target_consistent_rust() {
assert_single_binding_inhabitance(
IntScratchExample::DesignDocExample8Rust,
TargetInhabitance::RustI32,
);
}

#[test]
fn fold_dag_int_refined_cross_target_consistent_python() {
assert_single_binding_inhabitance(
IntScratchExample::DesignDocExample8Python,
TargetInhabitance::PythonInt,
);
}

#[test]
fn fold_dag_int_refined_cross_target_consistent_go() {
assert_single_binding_inhabitance(
IntScratchExample::DesignDocExample8Go,
TargetInhabitance::GoInt32,
);
}
}
22 changes: 17 additions & 5 deletions src/v3/grounding_coercion_fold/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,15 +33,27 @@ pub enum IntScratchExample {
DesignDocExample5AmbiguousAlgebra,
/// Example 6 — `Int(0..2^65)` exceeds the Rust Int128 family.
DesignDocExample6NoInhabitant,
/// Example 8 — Rust target for `Int(-2^31..2^31)`.
///
/// Kept as three flat variants rather than adding a scratch target coproduct: this matches
/// the existing per-example driver shape and keeps the transitional selector simple until
/// the declared LanguageSpec projection replaces it.
DesignDocExample8Rust,
/// Example 8 — Python target for `Int(-2^31..2^31)`.
DesignDocExample8Python,
/// Example 8 — Go target for `Int(-2^31..2^31)`.
DesignDocExample8Go,
}

/// Unique target inhabitance for a binding (Examples 1–2 surface only).
/// Unique target inhabitance for a binding (scratch Int example surface only).
///
/// Practice 4 (`docs/modeling-discipline.md`): single-variant placeholder — N \< 2, so no 🟢/🟡/🔴
/// coproduct checkpoint until a second inhabitant is introduced. When a second variant lands,
/// classify this enum explicitly (substrate vs Rust mirror / dissolution) — do not grow ad hoc
/// without the same checkpoint discipline as the projection carriers.
/// Practice 4 (`docs/modeling-discipline.md`): **🟡 YELLOW** — lane-local output mirror for
/// hardcoded scratch examples. It retires with `ScratchIntExamples` when the declared
/// LanguageSpec projection can compute target inhabitance structurally.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum TargetInhabitance {
RustU32,
RustI32,
PythonInt,
GoInt32,
}
Loading