diff --git a/CLAUDE.md b/CLAUDE.md index 955e475..dd81bc6 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -357,12 +357,13 @@ Tests in `tests/named_path_test.rs`. Full ISO context + roadmap in `docs/interna ### Null semantics -`Value::Null` is a first-class variant. Properties that are absent from a node/edge map are treated as null at query time, and explicit nulls round-trip through the on-disk format. +`Value::Null` is a first-class variant, and the 3VL *unknown* truth value **is** the null value (ISO: no separate `Unknown`). A missing property/record key on a bound element reads as `Success(Value::Null)` — FPPC rule `Ra` "ok null" — so 3VL sees a null (lenient), while a genuine type error stays a `Failure`. Explicit nulls round-trip through the on-disk format. -- **3VL in `cmp_values`** (`runtime/mod.rs`): null on either side yields `false`, so a predicate involving null is dropped from the result. Used by both the LTJ filter loop (`NodeAttrCmp`) and the standard scan (`filter_node`/`filter_edge`). +- **Residual `WHERE` / general expressions** (`engine.rs` `run_expr` / `eval_binop`): classic 3VL. Arithmetic / comparison / `IN` propagate null (any null operand → null); `AND`/`OR` use the SQL truth tables (`false` absorbing for `AND`, `true` for `OR`; else null); `NOT null → null`; `null AS T → null` for any (nullable-by-default) target. A genuine **type error** (non-bool in boolean position, failed non-null cast, div-by-zero) is a `Failure` and **empties the path** — dropped in `WHERE`, null cell in `RETURN` — regardless of essential/inessential position (the strict subset of ISO `UA004`; we never short-circuit-suppress an inessential error). The typechecker's `cod` override for `OR`/`AND` (result `Bool` unless *both* operands meet ⊥ against `Bool`) keeps the static emptiness judgment an under-approximation. Known ISO gap: an *essential* type error and a `NOT NULL`-site null should raise a hard data exception (`22G12`/`22G03`); froGQL empties instead (FPPC "type errors yield empty outputs") — tracked as a future *ISO data-exceptions* workstream in `docs/internals/iso-gql-gaps.md`. +- **3VL in `cmp_values`** (`runtime/mod.rs`): null on either side yields `false`, so a *pushed-down* predicate involving null is dropped from the result. Used by the LTJ filter loop (`NodeAttrCmp`) and the standard scan (`filter_node`/`filter_edge`); the residual-`WHERE` path above yields `null` (which likewise drops the row via `get_bool`), so the two agree on the keep/drop decision. - **Aggregate null elimination** (`engine.rs` `collect_aggregate_values`): both `ExprResult::Failure` and `Success(Value::Null)` are dropped before the reducer runs. Empty aggregates emit `Value::Null`. - **Wire format**: `PropValue::Null` carries tag byte 6 (no payload). Nested nulls inside lists / records survive the round-trip. Top-level nulls are encoded as key absence — the property is omitted from the on-disk record. -- **Surface syntax**: the lexer accepts `null` / `NULL`. The parser emits `Expr::Const(Value::Null)`. The typechecker maps the literal to `SimpleType::Star` so `WHERE x = null` does not collapse the surrounding type derivation. `IS NULL` and `IS NOT NULL` (parsed via `try_is_null` lookahead) produce an `Expr::IsNull { operand, negated }` that returns `Value::Bool` regardless of operand type; missing-attribute and unbound-variable failures are treated as null. +- **Surface syntax**: the lexer accepts `null` / `NULL`. The parser emits `Expr::Const(Value::Null)`. The typechecker maps the literal to `SimpleType::Star` so `WHERE x = null` does not collapse the surrounding type derivation. `IS NULL` and `IS NOT NULL` (parsed via `try_is_null` lookahead) produce an `Expr::IsNull { operand, negated }` that returns `Value::Bool` regardless of operand type; a missing attribute reads as `Value::Null` (so `IS NULL` matches it), and an unbound-variable `Failure` is likewise treated as null for the test. ### CSV loader diff --git a/src/runtime/engine.rs b/src/runtime/engine.rs index b5e05c4..bba6c37 100644 --- a/src/runtime/engine.rs +++ b/src/runtime/engine.rs @@ -3179,7 +3179,11 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> { }; match props.get(attr) { Some(v) => ExprResult::Success(v.clone()), - None => ExprResult::Failure(format!("attribute '{attr}' not found")), + // FPPC rule (Ra): reading an absent property on a bound element is + // `ok null`, not a stuck/error state. Missing key -> null so 3VL in + // the connectives/comparisons sees a value, not a Failure (which is + // reserved for genuine errors that must empty the path). + None => ExprResult::Success(Value::Null), } } @@ -3248,10 +3252,20 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> { } Expr::FieldAccess { base, field } => match self.run_expr(mu, base) { - ExprResult::Success(Value::Record(m)) => match m.get(field) { - Some(v) => ExprResult::Success(v.clone()), - None => ExprResult::Failure(format!("field '{field}' not found")), - }, + // Missing record key -> null. Records/nested field access are a + // froGQL extension beyond FPPC's flat property model; this + // follows ISO §20.11 for an OPEN, + // nullable-by-default site. (A closed type would reject the key + // at prep time; a NOT NULL site would raise 22G12 — both are the + // tracked closed-schema / material-type gaps.) + ExprResult::Success(Value::Record(m)) => { + ExprResult::Success(m.get(field).cloned().unwrap_or(Value::Null)) + } + // Field access on a null base -> null (ISO §20.11: reading + // through a null source yields null when the destination is + // nullable — froGQL's default; mirrors FPPC Ra's null-bound + // variable case). + ExprResult::Success(Value::Null) => ExprResult::Success(Value::Null), ExprResult::Success(other) => { ExprResult::Failure(format!("field access on non-record value: {other}")) } @@ -3272,6 +3286,14 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> { BinOp::As => { let l = self.run_expr(mu, left); match (&l, right.as_ref()) { + // null inhabits every type: `null AS T` is null, + // regardless of target. A *failed* cast of a non-null + // value stays a Failure (error) below — the runtime + // relaxation lets null reach the 3VL logic without + // turning genuine cast errors into null. + (ExprResult::Success(Value::Null), Expr::Type(_)) => { + ExprResult::Success(Value::Null) + } (ExprResult::Success(val), Expr::Type(ty)) => { if Expr::value_is_type(val, ty) { ExprResult::Success(val.clone()) @@ -3320,10 +3342,16 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> { UnOp::Neg => match val { Value::Int(n) => ExprResult::Success(Value::Int(-n)), Value::Float(x) => ExprResult::Success(Value::Float(-x)), + // 3VL: -null = null. + Value::Null => ExprResult::Success(Value::Null), _ => ExprResult::Failure("neg requires int or float".into()), }, UnOp::Not => match val { Value::Bool(b) => ExprResult::Success(Value::Bool(!b)), + // 3VL: NOT null = null. NOT has no short-circuit; a + // bottom (error) operand still propagates as Failure + // via the arm below. + Value::Null => ExprResult::Success(Value::Null), _ => ExprResult::Failure("not requires bool".into()), }, }, @@ -4001,6 +4029,26 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> { } } match op { + // Classic 3VL: arithmetic and comparison operators propagate null — + // any null operand yields null (unknown). Errors do NOT reach here: + // the operand-cast wrapper propagates a Failure before eval_binop, + // so only genuine values (including null) arrive. Logical AND/OR are + // handled below (null is absorbing-aware, not blanket-propagated). + BinOp::Add + | BinOp::Sub + | BinOp::Mul + | BinOp::Div + | BinOp::Mod + | BinOp::Gt + | BinOp::Lt + | BinOp::Ge + | BinOp::Le + | BinOp::Eq + | BinOp::Ne + if lv.is_null() || rv.is_null() => + { + ExprResult::Success(Value::Null) + } BinOp::Add => match as_num_pair(lv, rv) { Some((Value::Int(a), Value::Int(b))) => ExprResult::Success(Value::Int(a + b)), Some((Value::Float(a), Value::Float(b))) => { @@ -4068,20 +4116,50 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> { } _ => ExprResult::Failure("<= requires numeric operands".into()), }, + // Non-null Eq/Ne are structural (the null cases were handled by the + // 3VL guard above: `null = x` / `x = null` -> null). BinOp::Eq => ExprResult::Success(Value::Bool(lv == rv)), BinOp::Ne => ExprResult::Success(Value::Bool(lv != rv)), + // 3VL membership: `null IN xs` -> null; found -> true; not found but + // the list carries a null -> null (unknown); else false. BinOp::In => match rv { Value::List(items) => { - ExprResult::Success(Value::Bool(items.iter().any(|x| x == lv))) + if lv.is_null() { + ExprResult::Success(Value::Null) + } else if items.iter().any(|x| x == lv) { + ExprResult::Success(Value::Bool(true)) + } else if items.iter().any(Value::is_null) { + ExprResult::Success(Value::Null) + } else { + ExprResult::Success(Value::Bool(false)) + } } + Value::Null => ExprResult::Success(Value::Null), _ => ExprResult::Failure("'in' requires a list on the right".into()), }, + // Classic 3VL for the short-circuit connectives. `false` is + // absorbing for AND, `true` for OR (so `false AND null = false`, + // `true OR null = true`); otherwise a null operand yields null. + // A non-bool, non-null operand is an error (a Failure never reaches + // here — the wrapper empties the path first). BinOp::And => match (lv, rv) { - (Value::Bool(a), Value::Bool(b)) => ExprResult::Success(Value::Bool(*a && *b)), + (Value::Bool(false), _) | (_, Value::Bool(false)) => { + ExprResult::Success(Value::Bool(false)) + } + (Value::Bool(true), Value::Bool(true)) => ExprResult::Success(Value::Bool(true)), + (Value::Bool(true) | Value::Null, Value::Bool(true) | Value::Null) => { + ExprResult::Success(Value::Null) + } _ => ExprResult::Failure("and requires bools".into()), }, BinOp::Or => match (lv, rv) { - (Value::Bool(a), Value::Bool(b)) => ExprResult::Success(Value::Bool(*a || *b)), + (Value::Bool(true), _) | (_, Value::Bool(true)) => { + ExprResult::Success(Value::Bool(true)) + } + (Value::Bool(false), Value::Bool(false)) => ExprResult::Success(Value::Bool(false)), + (Value::Bool(false) | Value::Null, Value::Bool(false) | Value::Null) => { + ExprResult::Success(Value::Null) + } _ => ExprResult::Failure("or requires bools".into()), }, _ => ExprResult::Failure(format!("unexpected op {op} in eval_binop")), diff --git a/src/typing/checker.rs b/src/typing/checker.rs index 22ff420..911539b 100644 --- a/src/typing/checker.rs +++ b/src/typing/checker.rs @@ -740,9 +740,23 @@ impl Typechecker { let t2 = self.check_expr(right, env); let (expected_t1, expected_t2, result_t) = op.delta(&t1, &t2); - if SimpleType::meet(&t1, &expected_t1) != SimpleType::Zero - && SimpleType::meet(&t2, &expected_t2) != SimpleType::Zero - { + let ok1 = SimpleType::meet(&t1, &expected_t1) != SimpleType::Zero; + let ok2 = SimpleType::meet(&t2, &expected_t2) != SimpleType::Zero; + + // c̃od override for the short-circuit connectives (OR/AND): + // degrade to ⊥ only when BOTH operands are incompatible with + // the expected type. A single ⊥/null operand beside a valid + // Bool still types as Bool (e.g. `⊥ OR B : B`) — a deliberate + // under-approximation so a dynamically-valid branch is not + // falsely pruned as empty. Non-short-circuit ops (arithmetic, + // comparisons) keep the default: any ⊥ operand degrades. + let defined = if matches!(op, BinOp::And | BinOp::Or) { + ok1 || ok2 + } else { + ok1 && ok2 + }; + + if defined { result_t } else { self.warnings.push(format!( diff --git a/tests/three_valued_logic_test.rs b/tests/three_valued_logic_test.rs new file mode 100644 index 0000000..46d587d --- /dev/null +++ b/tests/three_valued_logic_test.rs @@ -0,0 +1,485 @@ +//! SQL/GQL three-valued logic (3VL) end-to-end, per the froGQL amendment to +//! FPPC approved by M. Toro: +//! +//! - `cod` degrades to bottom for the short-circuit connectives OR/AND only +//! when BOTH operands are bottom (a bottom/null operand beside a valid Bool +//! stays Bool). +//! - `null AS T` -> null for any target; any *other* failed cast is an error. +//! - binary/unary operators follow classic 3VL, propagating nulls. +//! +//! Plus the FPPC `Ra` read-site rule: a missing property/field reads as `ok +//! null`, so 3VL sees a null value (lenient) while genuine errors stay Failure +//! (which empties the path). +//! +//! Error-vs-null at a connective (a type error beside a dominating boolean): +//! confirmed by both the FPPC oracle (DGG monotonicity, Thm 6.8) and the ISO +//! oracle (`UA004`). A genuine type error empties the path regardless of +//! essential/inessential position — we take the strict, portable subset: +//! suppressing an inessential error is *permitted* by ISO but never *required*, +//! and never relied upon. A *null* operand stays lenient (3VL); only a genuine +//! error empties. + +use frogql::compile_query; +use frogql::model::graph::MemoryGraphStore; +use frogql::model::value::Value; +use frogql::runtime::engine::Runtime; +use frogql::runtime::result::QueryResult; + +// --------------------------------------------------------------------------- +// Harness +// --------------------------------------------------------------------------- + +fn run(g: &MemoryGraphStore, q: &str) -> Vec> { + let rt = Runtime::new(g); + let query = compile_query(q).expect("compile failed"); + match rt.run_query(&query, 0) { + QueryResult::Projected(rs) => rs, + other => panic!("expected projected rows for {q:?}, got {other:?}"), + } +} + +/// One bare node (`s = "a"`, a non-numeric string) so `RETURN ` gives one row. +fn one_node() -> MemoryGraphStore { + let json = r#"{"nodes":[{"id":"n1","labels":["N"],"props":{"s":"a"}}],"edges":[]}"#; + MemoryGraphStore::from_json_str(json).unwrap() +} + +/// Single-cell value of `RETURN () AS b` over one node. +fn scalar(expr: &str) -> Value { + let g = one_node(); + let rows = run(&g, &format!("MATCH (x:N) RETURN ({expr}) AS b")); + assert_eq!(rows.len(), 1, "expected one row for {expr:?}, got {rows:?}"); + rows.into_iter().next().unwrap().into_iter().next().unwrap() +} + +/// Three users; Carol has no `email` (missing property -> null). +fn users() -> MemoryGraphStore { + let json = r#"{ + "nodes": [ + {"id":"u1","labels":["User"],"props":{"name":"Alice","email":"a@x.test"}}, + {"id":"u2","labels":["User"],"props":{"name":"Bob","email":"b@x.test"}}, + {"id":"u3","labels":["User"],"props":{"name":"Carol"}} + ], + "edges": [] + }"#; + MemoryGraphStore::from_json_str(json).unwrap() +} + +/// active = true / false / missing. +fn active_graph() -> MemoryGraphStore { + let json = r#"{ + "nodes": [ + {"id":"a","labels":["N"],"props":{"name":"A","active":true}}, + {"id":"b","labels":["N"],"props":{"name":"B","active":false}}, + {"id":"c","labels":["N"],"props":{"name":"C"}} + ], + "edges": [] + }"#; + MemoryGraphStore::from_json_str(json).unwrap() +} + +fn names(g: &MemoryGraphStore, q: &str) -> Vec { + let mut ns: Vec = run(g, q) + .into_iter() + .map(|r| match &r[0] { + Value::Str(s) => s.clone(), + other => panic!("expected Str name, got {other:?}"), + }) + .collect(); + ns.sort(); + ns +} + +// --------------------------------------------------------------------------- +// Logical connectives — classic 3VL truth tables (literal null) +// --------------------------------------------------------------------------- + +#[test] +fn test_or_truth_table() { + assert_eq!(scalar("true OR null"), Value::Bool(true)); + assert_eq!(scalar("null OR true"), Value::Bool(true)); + assert_eq!(scalar("false OR null"), Value::Null); + assert_eq!(scalar("null OR false"), Value::Null); + assert_eq!(scalar("null OR null"), Value::Null); + assert_eq!(scalar("true OR false"), Value::Bool(true)); + assert_eq!(scalar("false OR false"), Value::Bool(false)); +} + +#[test] +fn test_and_truth_table() { + assert_eq!(scalar("false AND null"), Value::Bool(false)); + assert_eq!(scalar("null AND false"), Value::Bool(false)); + assert_eq!(scalar("true AND null"), Value::Null); + assert_eq!(scalar("null AND true"), Value::Null); + assert_eq!(scalar("null AND null"), Value::Null); + assert_eq!(scalar("true AND true"), Value::Bool(true)); + assert_eq!(scalar("true AND false"), Value::Bool(false)); +} + +#[test] +fn test_not_truth_table() { + assert_eq!(scalar("NOT null"), Value::Null); + assert_eq!(scalar("NOT true"), Value::Bool(false)); + assert_eq!(scalar("NOT false"), Value::Bool(true)); +} + +// --------------------------------------------------------------------------- +// Read-site nulls (FPPC Ra): a missing property is null, not an error — so it +// stays lenient under the connectives. This is the headline fix. +// --------------------------------------------------------------------------- + +#[test] +fn test_missing_property_reads_as_null() { + let g = users(); + let rows = run(&g, "MATCH (x:User) WHERE x.name = 'Carol' RETURN x.email"); + assert_eq!(rows, vec![vec![Value::Null]]); +} + +#[test] +fn test_missing_or_true_keeps_all_rows() { + // `status` is absent on every user -> null -> `null OR true = true` -> all + // rows. This is the canonical headline case (`WHERE x.status OR true`). + let g = users(); + assert_eq!( + names(&g, "MATCH (x:User) WHERE x.status OR true RETURN x.name"), + vec!["Alice", "Bob", "Carol"], + ); +} + +#[test] +fn test_bool_property_or_true_keeps_all_rows() { + // `active` is a real boolean, present (true/false) or missing (-> null); + // `x.active OR true` is true for all three. + let g = active_graph(); + assert_eq!( + names(&g, "MATCH (x:N) WHERE x.active OR true RETURN x.name"), + vec!["A", "B", "C"], + ); +} + +#[test] +fn test_nonbool_value_beside_true_still_empties() { + // A *present* non-bool value (a string) in boolean position is a type + // error, not a null. It empties even beside a dominating `true` (ISO + // permits suppressing this inessential error but never requires it — we + // don't). Only the missing (null) row survives via `null OR true`. + let g = users(); // Alice/Bob email = string; Carol email missing (null) + assert_eq!( + names(&g, "MATCH (x:User) WHERE x.email OR true RETURN x.name"), + vec!["Carol"], + ); +} + +#[test] +fn test_missing_property_is_unknown_in_or() { + // `false OR x.active`: active=true -> true, false -> false, missing -> null. + let g = active_graph(); + let mut rows = run(&g, "MATCH (x:N) RETURN x.name, (false OR x.active) AS b"); + rows.sort_by(|l, r| format!("{:?}", l[0]).cmp(&format!("{:?}", r[0]))); + assert_eq!( + rows, + vec![ + vec![Value::Str("A".into()), Value::Bool(true)], + vec![Value::Str("B".into()), Value::Bool(false)], + vec![Value::Str("C".into()), Value::Null], + ] + ); +} + +#[test] +fn test_missing_and_false_short_circuits() { + // false AND x.active = false on every row (false is absorbing). + let g = active_graph(); + let rows = run(&g, "MATCH (x:N) RETURN (false AND x.active) AS b"); + assert_eq!(rows.len(), 3); + assert!(rows.iter().all(|r| r == &vec![Value::Bool(false)])); +} + +// --------------------------------------------------------------------------- +// Comparison / equality — 3VL (null propagates) +// --------------------------------------------------------------------------- + +#[test] +fn test_null_comparisons_are_null() { + assert_eq!(scalar("null = null"), Value::Null); + assert_eq!(scalar("null = 5"), Value::Null); + assert_eq!(scalar("5 = null"), Value::Null); + assert_eq!(scalar("null <> null"), Value::Null); + assert_eq!(scalar("null < 5"), Value::Null); + assert_eq!(scalar("5 > null"), Value::Null); +} + +#[test] +fn test_non_null_comparisons_unaffected() { + assert_eq!(scalar("1 = 1"), Value::Bool(true)); + assert_eq!(scalar("1 = 2"), Value::Bool(false)); + assert_eq!(scalar("2 > 1"), Value::Bool(true)); + assert_eq!(scalar("'a' = 'a'"), Value::Bool(true)); +} + +#[test] +fn test_eq_null_drops_rows_but_is_null_keeps() { + // `= null` is never true -> empty; `IS NULL` is the way to match. + let g = users(); + assert!(run(&g, "MATCH (x:User) WHERE x.email = null RETURN x.name").is_empty()); + assert!(run(&g, "MATCH (x:User) WHERE x.email <> null RETURN x.name").is_empty()); + assert_eq!( + names(&g, "MATCH (x:User) WHERE x.email IS NULL RETURN x.name"), + vec!["Carol"], + ); + assert_eq!( + names(&g, "MATCH (x:User) WHERE x.email IS NOT NULL RETURN x.name"), + vec!["Alice", "Bob"], + ); +} + +#[test] +fn test_where_not_drops_unknown() { + // NOT (unknown) = unknown -> Carol (missing email) is dropped, not kept. + let g = users(); + assert_eq!( + names( + &g, + "MATCH (x:User) WHERE NOT (x.email = 'nobody@x.test') RETURN x.name", + ), + vec!["Alice", "Bob"], + ); +} + +// --------------------------------------------------------------------------- +// Arithmetic — 3VL null propagation +// --------------------------------------------------------------------------- + +#[test] +fn test_arithmetic_null_propagates() { + assert_eq!(scalar("null + 1"), Value::Null); + assert_eq!(scalar("1 + null"), Value::Null); + assert_eq!(scalar("null - null"), Value::Null); + assert_eq!(scalar("null * 3"), Value::Null); + assert_eq!(scalar("10 / null"), Value::Null); + assert_eq!(scalar("-null"), Value::Null); +} + +// --------------------------------------------------------------------------- +// IN — 3VL membership +// --------------------------------------------------------------------------- + +#[test] +fn test_in_three_valued() { + assert_eq!(scalar("2 IN [1, 2, 3]"), Value::Bool(true)); + assert_eq!(scalar("9 IN [1, 2, 3]"), Value::Bool(false)); + // null on the left -> unknown + assert_eq!(scalar("null IN [1, 2, 3]"), Value::Null); + // not found, but the list carries a null -> unknown + assert_eq!(scalar("9 IN [1, null, 3]"), Value::Null); + // found -> true even if the list also carries a null + assert_eq!(scalar("1 IN [1, null, 3]"), Value::Bool(true)); + // right side null -> unknown + assert_eq!(scalar("1 IN null"), Value::Null); +} + +// --------------------------------------------------------------------------- +// Cast (`as`) — null passes; genuine failures are errors, not null +// --------------------------------------------------------------------------- + +#[test] +fn test_null_cast_passes_through() { + assert_eq!(scalar("null AS INTEGER"), Value::Null); + assert_eq!(scalar("null AS FLOAT"), Value::Null); + assert_eq!(scalar("null AS STRING"), Value::Null); + assert_eq!(scalar("null AS BOOL"), Value::Null); +} + +#[test] +fn test_cast_convert_valid() { + // CAST() conversion still works for real (non-null) values. + let n = r#"{"nodes":[{"id":"n1","labels":["N"],"props":{"s":"7"}}],"edges":[]}"#; + let g = MemoryGraphStore::from_json_str(n).unwrap(); + assert_eq!( + run(&g, "MATCH (x:N) RETURN CAST(x.s AS INTEGER) AS i"), + vec![vec![Value::Int(7)]], + ); +} + +#[test] +fn test_null_field_access_and_missing_key() { + // Record with an `addr` sub-record missing `zip`; and one node with no addr. + let json = r#"{ + "nodes": [ + {"id":"a","labels":["N"],"props":{"name":"A","addr":{"city":"X"}}}, + {"id":"b","labels":["N"],"props":{"name":"B"}} + ], + "edges": [] + }"#; + let g = MemoryGraphStore::from_json_str(json).unwrap(); + // missing sub-key -> null; missing base record -> null.field -> null. + let mut rows = run(&g, "MATCH (x:N) RETURN x.name, x.addr.zip AS z"); + rows.sort_by(|l, r| format!("{:?}", l[0]).cmp(&format!("{:?}", r[0]))); + assert_eq!( + rows, + vec![ + vec![Value::Str("A".into()), Value::Null], + vec![Value::Str("B".into()), Value::Null], + ] + ); +} + +#[test] +fn test_null_base_field_access_is_null_not_error() { + // Field access on a NULL base (`x.addr.zip` where node B has no `addr`, so + // `x.addr` is null) must yield null (lenient), NOT a Failure. A projection + // can't distinguish the two (both render as a null cell), so we test it in a + // connective where null and error diverge: `null.field OR true` keeps the + // row (null OR true = true); a Failure would empty it. + let json = r#"{"nodes":[{"id":"b","labels":["N"],"props":{"name":"B"}}],"edges":[]}"#; + let g = MemoryGraphStore::from_json_str(json).unwrap(); + assert_eq!( + names(&g, "MATCH (x:N) WHERE x.addr.zip OR true RETURN x.name"), + vec!["B"], + ); + // Contrast: field access on a non-record, non-null base is a genuine error, + // so `x.name.zip OR true` (name is a string) empties. + assert!(run(&g, "MATCH (x:N) WHERE x.name.zip OR true RETURN x.name").is_empty()); +} + +// --------------------------------------------------------------------------- +// Error vs null at a connective. A genuine type error (failed cast / non-bool +// value) empties the path regardless of essential/inessential position — the +// strict, portable subset (ISO UA004 permits suppressing an inessential error +// but never requires it; FPPC DGG Thm 6.8 confirms static `B` imposes no +// runtime success obligation). A *null* operand stays lenient. +// --------------------------------------------------------------------------- + +#[test] +fn test_failed_cast_beside_true_empties() { + // `'a' AS INTEGER` is a genuine cast error (NOT null): inessential beside + // `OR true`, but we still empty (we never rely on suppression). + let g = one_node(); // s = "a" + assert!(run(&g, "MATCH (x:N) WHERE (x.s AS INTEGER) OR true RETURN x.s").is_empty()); +} + +#[test] +fn test_nonbool_literal_error_vs_null_operand() { + // `1` cannot be a boolean operand: `1 OR true` -> error -> empties. + let g = one_node(); + assert!(run(&g, "MATCH (x:N) WHERE 1 OR true RETURN x.s").is_empty()); + // Contrast: a *null* operand is lenient — `null OR true` keeps the row. + assert_eq!( + run(&g, "MATCH (x:N) WHERE null OR true RETURN x.s").len(), + 1 + ); +} + +#[test] +fn test_error_empties_essential_and_inessential_alike() { + // We treat a type error identically whether the boolean makes it + // inessential (`_ OR true`, `false AND _`) or essential (`_ OR false`, + // `true AND _`): all empty. (ISO mandates the essential ones; the + // inessential ones we take the strict/portable option.) + let g = one_node(); // s = "a" (a non-numeric string) + for q in [ + "WHERE (x.s AS INTEGER) OR true", // inessential + "WHERE (x.s AS INTEGER) OR false", // essential + "WHERE (x.s AS INTEGER) AND false", // inessential + "WHERE (x.s AS INTEGER) AND true", // essential + ] { + assert!( + run(&g, &format!("MATCH (x:N) {q} RETURN x.s")).is_empty(), + "expected empty for {q:?}", + ); + } +} + +#[test] +fn test_cast_error_in_projection_is_null_cell() { + // In a projection the error surfaces as a null cell (row kept) — the engine + // never crashes on a type error. + let g = one_node(); + assert_eq!( + run(&g, "MATCH (x:N) RETURN CAST(x.s AS INTEGER) AS i"), + vec![vec![Value::Null]], + ); +} + +// --------------------------------------------------------------------------- +// Soundness of the vacuity under-approximation. We relaxed the *runtime* (null +// propagation across all binops) but only the *typechecker* for OR/AND (the cod +// override). These tests guard the one thing that asymmetry could break: the +// typechecker declaring a query `guaranteed_empty` while the runtime returns +// rows. That must never happen (static-empty must imply runtime-empty). +// --------------------------------------------------------------------------- + +fn ge_and_rows(g: &MemoryGraphStore, q: &str) -> (bool, usize) { + let res = frogql::compile_query_with_diagnostics(q).expect("compile"); + let rows = match Runtime::new(g).run_query(&res.query, 0) { + QueryResult::Projected(r) => r.len(), + QueryResult::Raw(ir) => ir.rows.len(), + }; + (res.guaranteed_empty, rows) +} + +#[test] +fn test_static_empty_implies_runtime_empty() { + // Every predicate here types to bottom (via literal/type mismatch across the + // binops we changed: arithmetic, comparison, IN, AND/OR). Wherever the + // checker says `guaranteed_empty`, the runtime must return zero rows. + let g = active_graph(); + for q in [ + "MATCH (x:N) WHERE 1 RETURN x.name", // non-bool predicate + "MATCH (x:N) WHERE 1 AND 2 RETURN x.name", // Int AND Int (both bottom) + "MATCH (x:N) WHERE 1 OR 2 RETURN x.name", // Int OR Int (both bottom) + "MATCH (x:N) WHERE 'a' = 1 RETURN x.name", // incompatible comparison + "MATCH (x:N) WHERE 'a' < 1 RETURN x.name", // incompatible ordering + "MATCH (x:N) WHERE x.name + 1 RETURN x.name", // arithmetic in bool position + "MATCH (x:N) WHERE 5 IN 3 RETURN x.name", // IN non-list + ] { + let (ge, rows) = ge_and_rows(&g, q); + if ge { + assert_eq!( + rows, 0, + "UNSOUND: {q:?} is guaranteed_empty but returned {rows} rows" + ); + } + } +} + +#[test] +fn test_cod_override_keeps_vacuity_sound_under_closed_schema() { + use frogql::typing::descriptor_type::DescriptorType; + use frogql::typing::label_type::LabelType; + use frogql::typing::property_type::PropertyType; + use frogql::typing::simple_type::SimpleType; + use frogql::typing::variable_type::{Schema, VariableType}; + use std::collections::BTreeMap; + + // Closed type N { n: Int } — so an unknown property `status` types to bottom. + let mut props = BTreeMap::new(); + props.insert("n".to_string(), SimpleType::Z); + let schema = Schema::from_parts( + vec![VariableType::Node(DescriptorType::new( + LabelType::Label("N".into()), + PropertyType::Closed(props), + ))], + vec![], + ); + + // `x.status OR true`: `x.status` is bottom (unknown on a closed type). WITHOUT + // the OR cod override this would prune as guaranteed_empty; the runtime reads + // x.status as null, so `null OR true = true` keeps every row — that mismatch + // would be unsound. The override types it Bool, so it is NOT pruned. + let res = frogql::compile_query_with_diagnostics_with( + &schema, + "MATCH (x:N) WHERE x.status OR true RETURN x.name", + ) + .expect("compile"); + assert!( + !res.guaranteed_empty, + "cod override must keep `bottom OR true` non-empty to stay sound", + ); + let g = active_graph(); + let rows = match Runtime::new(&g).run_query(&res.query, 0) { + QueryResult::Projected(r) => r.len(), + _ => 0, + }; + assert_eq!(rows, 3, "runtime keeps all rows: null OR true = true"); +}