Basics¶
Three small functions show fixed-width integer markers, a purity contract,
and a per-function optimization level. Run it with python and it is
ordinary Python. Run it with ppy run and the same three functions compile
through LLVM, after the checker has verified two contracts.
Run it¶
Fixed-width markers¶
A Python int is unbounded, so a native x * x on a plain int has to be
guarded: on overflow it falls back to CPython's arbitrary precision.
ppy.i64 is a contract that the value fits 64 bits. The checker holds
callers to it (a value that provably leaves the range is E1401), so the
native multiply needs no guard.
@ppy.opt(3) raises the optimization level for this one function. The
project default is 2.
The purity contract¶
@ppy.pure says the function has no observable effect: no I/O, no global
writes, no mutation of its arguments. The checker proves it across calls:
sum_of_squares is pure because square is. A violation is an error
(E1601), not a warning.
collatz_steps keeps a plain int. Its loop runs natively with an overflow
guard per operation, and a value that outgrows a word takes the fallback and
still gets the correct answer.
What it prints¶
python basics.ppy, ppy basics.ppy, ppy run basics.ppy
Read on: Directives and markers ยท Arbitrary precision
basics.ppy is hand-written; there is no .py source and no conversion step.
01_basics/basics.ppy¶
import ppy
from ppy import i64
@ppy.pure
@ppy.opt(3)
def square(x: i64) -> i64:
return x * x
@ppy.pure
def sum_of_squares(n: i64) -> i64:
total: i64 = 0
for value in range(n):
total += square(value)
return total
@ppy.pure
def collatz_steps(n: int) -> int:
steps: int = 0
while n != 1:
if n % 2 == 0:
n = n // 2
else:
n = 3 * n + 1
steps += 1
return steps
def main() -> None:
print(square(7), sum_of_squares(10), collatz_steps(27))
if __name__ == "__main__":
main()
Source: examples/01_basics.