From 91b7a570c2bd1c9e1cab894ded866e885f28946a Mon Sep 17 00:00:00 2001 From: Brandt Bucher Date: Thu, 22 May 2025 10:42:29 -0400 Subject: [PATCH] [ty] Implement Python's floor division semantics for `Literal` `int`s (#18249) Division works differently in Python than in Rust. If the result is negative and there is a remainder, the division rounds down (instead of towards zero). The remainder needs to be adjusted to compensate so that `(lhs // rhs) * rhs + (lhs % rhs) == lhs`. Fixes astral-sh/ty#481. --- .../resources/mdtest/binary/integers.md | 28 ++++++++++++++++ crates/ty_python_semantic/src/types/infer.rs | 32 +++++++++++++------ 2 files changed, 50 insertions(+), 10 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/binary/integers.md b/crates/ty_python_semantic/resources/mdtest/binary/integers.md index d7e920ed0e..95561a295e 100644 --- a/crates/ty_python_semantic/resources/mdtest/binary/integers.md +++ b/crates/ty_python_semantic/resources/mdtest/binary/integers.md @@ -72,6 +72,34 @@ reveal_type(2 ** (-1)) # revealed: float reveal_type((-1) ** (-1)) # revealed: float ``` +## Division and Modulus + +Division works differently in Python than in Rust. If the result is negative and there is a +remainder, the division rounds down (instead of towards zero). The remainder needs to be adjusted to +compensate so that `(lhs // rhs) * rhs + (lhs % rhs) == lhs`: + +```py +reveal_type(256 % 129) # revealed: Literal[127] +reveal_type(-256 % 129) # revealed: Literal[2] +reveal_type(256 % -129) # revealed: Literal[-2] +reveal_type(-256 % -129) # revealed: Literal[-127] + +reveal_type(129 % 16) # revealed: Literal[1] +reveal_type(-129 % 16) # revealed: Literal[15] +reveal_type(129 % -16) # revealed: Literal[-15] +reveal_type(-129 % -16) # revealed: Literal[-1] + +reveal_type(10 // 8) # revealed: Literal[1] +reveal_type(-10 // 8) # revealed: Literal[-2] +reveal_type(10 // -8) # revealed: Literal[-2] +reveal_type(-10 // -8) # revealed: Literal[1] + +reveal_type(10 // 6) # revealed: Literal[1] +reveal_type(-10 // 6) # revealed: Literal[-2] +reveal_type(10 // -6) # revealed: Literal[-2] +reveal_type(-10 // -6) # revealed: Literal[1] +``` + ## Division by Zero This error is really outside the current Python type system, because e.g. `int.__truediv__` and diff --git a/crates/ty_python_semantic/src/types/infer.rs b/crates/ty_python_semantic/src/types/infer.rs index 46c383eaa7..01668d6af7 100644 --- a/crates/ty_python_semantic/src/types/infer.rs +++ b/crates/ty_python_semantic/src/types/infer.rs @@ -6108,17 +6108,29 @@ impl<'db> TypeInferenceBuilder<'db> { Some(KnownClass::Float.to_instance(self.db())) } - (Type::IntLiteral(n), Type::IntLiteral(m), ast::Operator::FloorDiv) => Some( - n.checked_div(m) - .map(Type::IntLiteral) - .unwrap_or_else(|| KnownClass::Int.to_instance(self.db())), - ), + (Type::IntLiteral(n), Type::IntLiteral(m), ast::Operator::FloorDiv) => Some({ + let mut q = n.checked_div(m); + let r = n.checked_rem(m); + // Division works differently in Python than in Rust. If the result is negative and + // there is a remainder, the division rounds down (instead of towards zero): + if n.is_negative() != m.is_negative() && r.unwrap_or(0) != 0 { + q = q.map(|q| q - 1); + } + q.map(Type::IntLiteral) + .unwrap_or_else(|| KnownClass::Int.to_instance(self.db())) + }), - (Type::IntLiteral(n), Type::IntLiteral(m), ast::Operator::Mod) => Some( - n.checked_rem(m) - .map(Type::IntLiteral) - .unwrap_or_else(|| KnownClass::Int.to_instance(self.db())), - ), + (Type::IntLiteral(n), Type::IntLiteral(m), ast::Operator::Mod) => Some({ + let mut r = n.checked_rem(m); + // Division works differently in Python than in Rust. If the result is negative and + // there is a remainder, the division rounds down (instead of towards zero). Adjust + // the remainder to compensate so that q * m + r == n: + if n.is_negative() != m.is_negative() && r.unwrap_or(0) != 0 { + r = r.map(|x| x + m); + } + r.map(Type::IntLiteral) + .unwrap_or_else(|| KnownClass::Int.to_instance(self.db())) + }), (Type::IntLiteral(n), Type::IntLiteral(m), ast::Operator::Pow) => Some({ if m < 0 {