Skip to content
Merged
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
52 changes: 52 additions & 0 deletions interactive/src/corgi/logic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ use corgi::{ArithOp, BinOp as CBinOp, Builder, CmpOp, Graph, Kind, NumOp, Op, Pr
/// single sample can't reveal (it shows only one tag), so the scan is over every row, recursing
/// column-wise to cover nested variants too.
pub fn infer_shape_cols(rows: &[DValue]) -> Shape {
assert_uniform(rows);
let Some(first) = rows.first() else { return Shape::Unit };
match first {
DValue::Int(_) => Shape::Prim(64),
Expand Down Expand Up @@ -80,6 +81,33 @@ pub fn infer_shape_cols(rows: &[DValue]) -> Shape {
}
}

/// The uniformity contract, enforced LOUDLY at the ingest boundary: corgi columns are SoA
/// and carry ONE shape, while DDIR rows are dynamically typed. Without this check a mixed
/// column either truncated silently (rows wider than row 0 lost their extra fields — silent
/// wrong answers) or panicked with a bare `index out of bounds` — both worse than saying why.
/// Nested levels are covered by `infer_shape_cols`' recursion (each recursive call re-checks).
fn assert_uniform(rows: &[DValue]) {
let Some(first) = rows.first() else { return };
fn kind(r: &DValue) -> (&'static str, usize) {
match r {
DValue::Int(_) => ("Int", 0),
DValue::Tuple(xs) => ("Tuple", xs.len()),
DValue::List(_) => ("List", 0),
DValue::Variant(..) => ("Variant", 0),
}
}
let k0 = kind(first);
for (i, r) in rows.iter().enumerate().skip(1) {
let ki = kind(r);
assert!(
ki == k0,
"corgi transcode: heterogeneous column — row 0 is {}/{} but row {} is {}/{}: \
the corgi backend requires shape-uniform columns (pad rows to one arity, or use --backend=vec)",
k0.0, k0.1, i, ki.0, ki.1
);
}
}

/// AoS rows -> SoA corgi columns, directed by `shape`.
pub fn transcode(rows: &[DValue], shape: &Shape) -> CValue {
match shape {
Expand Down Expand Up @@ -218,6 +246,22 @@ pub fn shape_of_place(t: &Term, env_shapes: &[Shape]) -> Shape {
}
}

/// TOTAL best-effort shape of a `Proj` operand: resolve the `Var`/`Bound`/`Proj` spine
/// through KNOWN shapes only; `None` means "can't tell" (never a panic), and the caller
/// keeps the old lowering. The non-panicking cousin of [`shape_of_place`].
fn place_shape_opt(t: &Term, env_shapes: &[Shape]) -> Option<Shape> {
match t {
Term::Var(i) => env_shapes.get(*i).cloned(),
Term::Bound(k) => env_shapes.get(env_shapes.len().checked_sub(1 + *k)?).cloned(),
Term::Proj(inner, i) => match place_shape_opt(inner, env_shapes)? {
Shape::Prod(fs) => fs.get(*i).cloned(),
Shape::List(e) => Some(*e),
_ => None,
},
_ => None,
}
}

/// Best-effort structural `Shape` of a (non-place) compiled `Term`, used to decide cross-shape
/// `Eq`/`Ne`: DDIR compares `Value`s structurally, so e.g. `Tuple != Int` is *always* true (the
/// variants differ) — but corgi's `CmpOp::Rel` requires matching shapes. When the operand shapes
Expand Down Expand Up @@ -392,6 +436,14 @@ pub fn compile(term: &Term, b: &mut Builder<NumOp>, env: &[usize], env_shapes: &
}
}
Term::Proj(t, i) => {
// Shape-directed: `Op::Field` is PRODUCT elimination only. On a `List` operand,
// DDIR's Proj means indexing (`ir::eval` ir.rs:112), which has no columnar
// lowering here yet (corgi's Get tier) — decline, and rows handle it. The check
// is the TOTAL place resolver (never panics); an unresolved operand compiles as
// before (`Field`, with corgi's runtime shape check behind it).
if matches!(place_shape_opt(t, env_shapes), Some(Shape::List(_))) {
return None;
}
let id = compile(t, b, env, env_shapes, anchor)?;
Some(b.add(Op::Field(*i), vec![id]))
}
Expand Down
Loading