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
5 changes: 4 additions & 1 deletion dag/std/algebra.dag
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,10 @@ type AbelianGroup<T> {

type GroupCompletion<M>

type FieldOfFractions<R>
type FieldOfFractions<R> {
num: R
denom: R
}

type Semiring<T> {
add: fn(T, T) -> T
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module test.retirement.field_of_fractions_construction_retained


data field_of_fractions_construction_retention: TestModuleRetirement = TestModuleRetirement {
module: "field_of_fractions_construction_test.rs",
disposition: RetainedNonMigratable {
reason: "This witness guards the eval_record_lit construction-side NON-collapse for FieldOfFractions \{ num, denom \} (§7.2 model grounding): a plain-record construction with native Value::Int fields must stay a boxed Value::Record carrying both fields untouched — the deliberate negative-space counterpart to GroupCompletion's collapse (#7197), since FieldOfFractions has no native Rust scalar checkpoint to collapse into (an f64 collapse would be lossy/dishonest; Real/ApproximateField already exists for that). The assertions pattern-match on the host interpreter's internal Value enum (Value::Record vs any native scalar) to catch a regression that special-cases FieldOfFractions into a native collapse — that representation-strategy distinction has no observable surface from within a .dag program (the language has no reflection over Value's native-vs-boxed shape), so it cannot migrate to an exact-stem test dag floor witness. Retained until src/v1 deletes at v2 self-host; not migration debt and not a delete candidate."
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module test.retirement.field_of_fractions_single_declaration_retained


data field_of_fractions_single_declaration_retention: TestModuleRetirement = TestModuleRetirement {
module: "field_of_fractions_single_declaration_test.rs",
disposition: RetainedNonMigratable {
reason: "This witness guards the §7.2 FieldOfFractions de-fork non-regression: a corpus-wide filesystem walk over dag/ and src/v2/ must find exactly one top-level `type FieldOfFractions` declaration, at dag/std/algebra.dag — a second declaration anywhere else is a §3 fork that desynchronizes from the single authority. The scan reads host filesystem shape (per-file declaration heads), not an interpreter-observable .dag surface, so it cannot migrate to an exact-stem test dag floor witness. Retained until src/v1 deletes at v2 self-host; not migration debt and not a delete candidate."
}
}
8 changes: 6 additions & 2 deletions src/v1/stage0/src/std_algebra.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,8 +64,12 @@ pub struct AbelianGroup<T> {
#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct GroupCompletion<M>(pub std::marker::PhantomData<M>);

#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct FieldOfFractions<R>(pub std::marker::PhantomData<R>);
#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
pub struct FieldOfFractions<R> {
pub num: R,
pub denom: R,
pub _phantom: std::marker::PhantomData<R>,
}

#[derive(Clone)]
pub struct Semiring<T> {
Expand Down
88 changes: 88 additions & 0 deletions src/v1/tests/src/field_of_fractions_construction_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
use std::rc::Rc;

use v1_compiler::cli_run;
use v1_compiler::v1_compiler_compile::{compile_to_resolved, ResolvedPipelineResult};
use v1_compiler::v1_interpreter::{self, ExecutionMode, Value};

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

// Discriminating witness for the §7.2 FieldOfFractions model grounding (sharp-bee-290
// sign-off): `FieldOfFractions<R> = { num: R, denom: R }` is now a real 2-field record at
// its single authority (dag/std/algebra.dag). Unlike GroupCompletion (#7197), this is
// deliberately negative-space: FieldOfFractions has no native Rust scalar checkpoint to
// collapse into (Rational has no lossless native representation — an f64 collapse would be
// dishonest, per the design doc), so `eval_record_lit` must NOT special-case it. A plain
// `FieldOfFractions { num, denom }` construction with native `Value::Int` fields must stay
// a boxed `Value::Record` carrying both fields untouched. A regression that special-cases
// FieldOfFractions into any native collapse (silently lossy or otherwise) fails this
// witness; a regression that leaves the type hollow (no `num`/`denom` fields at all) fails
// to resolve at all, which this witness's `assert_resolved` also guards.
const RECEIPTS_SOURCE: &str = r#"
module test.field_of_fractions_construction

import std.algebra { FieldOfFractions }

fn one_half() -> FieldOfFractions<Int> { FieldOfFractions { num: 1, denom: 2 } }
fn three_quarters() -> FieldOfFractions<Int> { FieldOfFractions { num: 3, denom: 4 } }
"#;

fn assert_resolved(resolved: &ResolvedPipelineResult) {
let msgs: Vec<String> = resolved
.diagnostics
.iter()
.map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone()))
.filter(|m| !m.starts_with("complexity: ") && !m.starts_with("unlisted import use "))
.collect();
assert!(
msgs.is_empty() && resolved.graph.is_some(),
"receipts source should resolve cleanly, got {:?} (graph present: {})",
msgs,
resolved.graph.is_some(),
);
}

fn with_receipts_ctx<R>(body: impl FnOnce(&v1_interpreter::InterpContext) -> R) -> R {
let ws = workspace_root();
let roots = [ws.join("src/v2"), ws.join("dag")];
let sources =
resolve_imports_transitively_with_source_roots("test.dag", RECEIPTS_SOURCE, &roots);
let resolved = compile_to_resolved(Rc::new(sources.into()));
assert_resolved(&resolved);
let graph = resolved.graph.as_ref().expect("graph");
let ctx =
cli_run::make_eval_context(graph, resolved.source_indices.clone(), ExecutionMode::Wet);
body(&ctx)
}

#[test]
fn field_of_fractions_pair_stays_boxed_record_not_native_collapse() {
with_receipts_ctx(|ctx| {
for (f, expected_num, expected_denom) in
[("one_half", 1i64, 2i64), ("three_quarters", 3i64, 4i64)]
{
match v1_interpreter::run_in_context(ctx, f, false) {
Ok(Value::Record { type_name, fields }) => {
assert!(
ctx.sym_eq(type_name, "FieldOfFractions"),
"{f}: expected type_name FieldOfFractions, got {}",
ctx.resolve(type_name)
);
match ctx.field(&fields, "num") {
Some(Value::Int(n)) if *n == expected_num => {}
other => panic!("{f}: num field mismatch, got {other:?}"),
}
match ctx.field(&fields, "denom") {
Some(Value::Int(n)) if *n == expected_denom => {}
other => panic!("{f}: denom field mismatch, got {other:?}"),
}
}
other => panic!(
"{f}: expected a boxed Value::Record{{num, denom}} — FieldOfFractions has \
no native Rust scalar to collapse into, so a regression that special-cases \
it into any native Value variant (Int, Float, or otherwise) surfaces here; \
got {other:?}"
),
}
}
});
}
87 changes: 87 additions & 0 deletions src/v1/tests/src/field_of_fractions_single_declaration_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
//! De-fork non-regression witness for the §7.2 FieldOfFractions model grounding.
//!
//! Unlike GroupCompletion (#7197), FieldOfFractions had no existing §3 fork at the time the
//! model landed — this witness guards against a FUTURE fork appearing (a second independent
//! `type FieldOfFractions` declaration anywhere in the corpus, which would duplicate the
//! single authority at dag/std/algebra.dag and desynchronize from it). Reads corpus SHAPE
//! (a per-file top-level `type FieldOfFractions` declaration head), not contents.

fn workspace_root() -> std::path::PathBuf {
std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
.join("../../..")
.canonicalize()
.expect("workspace root")
}

fn collect_dag_files(dir: &std::path::Path, out: &mut Vec<std::path::PathBuf>) {
let mut entries: Vec<_> = match std::fs::read_dir(dir) {
Ok(e) => e.filter_map(|x| x.ok()).collect(),
Err(_) => return,
};
entries.sort_by_key(|e| e.file_name());
for e in entries {
let p = e.path();
if p.is_dir() {
collect_dag_files(&p, out);
} else if p.extension().map(|x| x == "dag").unwrap_or(false) {
out.push(p);
}
}
}

fn declares_field_of_fractions(content: &str) -> bool {
content.lines().any(|line| {
let t = line.trim_start();
t.starts_with("type FieldOfFractions") || t.starts_with("type FieldOfFractions<")
})
}

#[test]
fn field_of_fractions_has_exactly_one_declaration_corpuswide() {
let ws = workspace_root();
let mut files = Vec::new();
for dir in ["dag", "src/v2"] {
collect_dag_files(&ws.join(dir), &mut files);
}
assert!(
!files.is_empty(),
"no .dag sources found under dag/ or src/v2/"
);

let declaring: Vec<String> = files
.into_iter()
.filter_map(|p| {
let content = std::fs::read_to_string(&p).ok()?;
if declares_field_of_fractions(&content) {
Some(
p.strip_prefix(&ws)
.unwrap_or(&p)
.to_string_lossy()
.into_owned(),
)
} else {
None
}
})
.collect();

assert_eq!(
declaring,
vec!["dag/std/algebra.dag".to_string()],
"FieldOfFractions must have exactly one declaration at its single authority \
(dag/std/algebra.dag) — a second declaration anywhere else in the corpus is a §3 \
fork; found: {declaring:?}"
);
}

// Red control: the scanner itself must actually detect a declaration when one exists,
// not just report zero unconditionally.
#[test]
fn declares_field_of_fractions_detects_a_real_declaration() {
assert!(declares_field_of_fractions(
"module std.algebra\n\ntype FieldOfFractions<R> {\n num: R\n denom: R\n}\n"
));
assert!(!declares_field_of_fractions(
"module std.algebra\n\ntype GroupCompletion<M> {\n pos: M\n neg: M\n}\n"
));
}
4 changes: 4 additions & 0 deletions src/v1/tests/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,10 @@ mod faithful_string_element_char_witness_test;
#[cfg(test)]
mod field_import_surface_generic_arg_test;
#[cfg(test)]
mod field_of_fractions_construction_test;
#[cfg(test)]
mod field_of_fractions_single_declaration_test;
#[cfg(test)]
mod floor_drain_retention_test;
#[cfg(test)]
mod fn_as_value_test;
Expand Down
Loading