Skip to content

feat(3vl): SQL three-valued logic for AND/OR/NOT + null cast pass-through #63

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Felipe705x wants to merge 4 commits into from
Closed

feat(3vl): SQL three-valued logic for AND/OR/NOT + null cast pass-through #63

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1628b47
feat(3vl): three-valued logic for AND/OR/NOT at runtime
Felipe705x Jun 29, 2026
ade7352
feat(3vl): pass null through the `as` cast (null AS T -> null)
Felipe705x Jun 29, 2026
8e36fe6
feat(3vl): typechecker short-circuit override for AND/OR
Felipe705x Jun 29, 2026
f508fab
test(3vl): three-valued-logic suite for the boolean connectives
Felipe705x Jun 29, 2026
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
94 changes: 92 additions & 2 deletions src/runtime/engine.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3272,6 +3272,15 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> {
BinOp::As => {
let l = self.run_expr(mu, left);
match (&l, right.as_ref()) {
// 3VL: null inhabits every type — `null AS T` is null,
// regardless of target. This also lets a null operand
// pass the implicit argument cast in the wrapper below
// and reach the 3VL logic (the runtime `△(bop)`
// relaxation), without changing the `IS`/`TYPED`
// predicate (which uses `value_is_type` directly).
(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())
Expand All @@ -3283,6 +3292,69 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> {
_ => ExprResult::Failure("invalid 'as' operands".into()),
}
}
// Logical connectives follow SQL three-valued logic (3VL) and
// short-circuit. They are handled here, *outside* the generic
// operator wrapper below, so a `Null`/`Failure` operand reaches
// the 3VL table instead of being rejected by the implicit
// argument cast. `Failure` (a missing attribute, an unbound
// variable, a type error) is treated as the unknown/null input,
// matching how `IsNull`/`Coalesce`/aggregates already read it.
BinOp::Or => {
let l = self.run_expr(mu, left);
// true OR _ = true (short-circuit; rhs not evaluated).
if matches!(l, ExprResult::Success(Value::Bool(true))) {
return ExprResult::Success(Value::Bool(true));
}
let r = self.run_expr(mu, right);
match (&l, &r) {
// _ OR true = true
(_, ExprResult::Success(Value::Bool(true))) => {
ExprResult::Success(Value::Bool(true))
}
// false OR false = false
(
ExprResult::Success(Value::Bool(false)),
ExprResult::Success(Value::Bool(false)),
) => ExprResult::Success(Value::Bool(false)),
// false OR null, null OR false, null OR null = null.
(
ExprResult::Success(Value::Bool(false) | Value::Null)
| ExprResult::Failure(_),
ExprResult::Success(Value::Bool(false) | Value::Null)
| ExprResult::Failure(_),
) => ExprResult::Success(Value::Null),
// A concrete non-bool operand (e.g. Int) is a real error.
_ => ExprResult::Failure("or requires bools".into()),
}
}
BinOp::And => {
let l = self.run_expr(mu, left);
// false AND _ = false (short-circuit; rhs not evaluated).
if matches!(l, ExprResult::Success(Value::Bool(false))) {
return ExprResult::Success(Value::Bool(false));
}
let r = self.run_expr(mu, right);
match (&l, &r) {
// _ AND false = false
(_, ExprResult::Success(Value::Bool(false))) => {
ExprResult::Success(Value::Bool(false))
}
// true AND true = true
(
ExprResult::Success(Value::Bool(true)),
ExprResult::Success(Value::Bool(true)),
) => ExprResult::Success(Value::Bool(true)),
// true AND null, null AND true, null AND null = null.
(
ExprResult::Success(Value::Bool(true) | Value::Null)
| ExprResult::Failure(_),
ExprResult::Success(Value::Bool(true) | Value::Null)
| ExprResult::Failure(_),
) => ExprResult::Success(Value::Null),
// A concrete non-bool operand (e.g. Int) is a real error.
_ => ExprResult::Failure("and requires bools".into()),
}
}
_ => {
let (ty_l, _, _) = op.delta(&SimpleType::Star, &SimpleType::Star);
let cast_left = Expr::Binop {
Expand Down Expand Up @@ -3324,6 +3396,9 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> {
},
UnOp::Not => match val {
Value::Bool(b) => ExprResult::Success(Value::Bool(!b)),
// 3VL: NOT null = null (a Failure operand already
// propagates to null below).
Value::Null => ExprResult::Success(Value::Null),
_ => ExprResult::Failure("not requires bool".into()),
},
},
Expand Down Expand Up @@ -4076,12 +4151,27 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> {
}
_ => ExprResult::Failure("'in' requires a list on the right".into()),
},
// NOTE: `And`/`Or` are normally intercepted in `run_expr` (3VL +
// short-circuit) and do not reach here. These arms are kept
// consistent with that 3VL table for any direct caller.
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")),
Expand Down
21 changes: 21 additions & 0 deletions src/typing/checker.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -738,6 +738,27 @@ impl Typechecker {
}

let t2 = self.check_expr(right, env);

// Logical connectives short-circuit under 3VL, so we override
// the default `c̃od` propagation for them: the result is `B`
// unless BOTH operands are incompatible with `B` (a ⊥/Null
// operand beside a valid Bool still yields a Bool, e.g.
// `true OR ⊥`). Only when both sides meet ⊥ against `B` do we
// degrade to ⊥.
if matches!(op, BinOp::And | BinOp::Or) {
let both_bottom = SimpleType::meet(&t1, &SimpleType::B) == SimpleType::Zero
&& SimpleType::meet(&t2, &SimpleType::B) == SimpleType::Zero;
return if both_bottom {
self.warnings.push(format!(
"Binop {:?} between types {} and {} is not defined",
op, t1, t2
));
SimpleType::Zero
} else {
SimpleType::B
};
}

let (expected_t1, expected_t2, result_t) = op.delta(&t1, &t2);

if SimpleType::meet(&t1, &expected_t1) != SimpleType::Zero
Expand Down
Loading
Loading