diff --git a/LeanPy/native/python_bridge.c b/LeanPy/native/python_bridge.c index c1b4651..08534cd 100644 --- a/LeanPy/native/python_bridge.c +++ b/LeanPy/native/python_bridge.c @@ -442,29 +442,38 @@ LEAN_EXPORT lean_obj_res lean_py_is_initialized(lean_obj_arg unit, lean_obj_arg } \ } while (0) -/* Acquire the GIL for the duration of a Python C API call. The macro - * declares a `_gil_state` variable and releases it on `WITH_GIL_END`. */ -#define WITH_GIL_BEGIN() \ - PyGILState_STATE _gil_state = p_PyGILState_Ensure(); -#define WITH_GIL_END() \ - p_PyGILState_Release(_gil_state); +/* Acquire the GIL for the duration of a Python C API call, releasing it + * automatically on scope exit so every return path is covered. `WITH_GIL()` + * is placed once at the top of each entry point that touches the CPython + * C API. PyGILState_Ensure is reentrant: when the calling thread already + * holds the GIL — the common case, since `LeanLibrary` loads the bridge via + * ctypes `PyDLL` — this is a cheap no-op. It becomes load-bearing when the + * bridge is entered *without* the GIL held: a foreign thread created by + * Lean, a free-threaded build, or a `CDLL`-loaded library. */ +static inline void _leanpy_gil_release(PyGILState_STATE *st) { + p_PyGILState_Release(*st); +} +#define WITH_GIL() \ + PyGILState_STATE _gil_state \ + __attribute__((cleanup(_leanpy_gil_release))) \ + = p_PyGILState_Ensure() /* ------------------------------------------------------------------ */ /* Singletons */ /* ------------------------------------------------------------------ */ LEAN_EXPORT lean_obj_res lean_py_none(lean_obj_arg unit, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); p_Py_IncRef(p_Py_None); return lean_io_result_mk_ok(wrap_pyobject(p_Py_None)); } LEAN_EXPORT lean_obj_res lean_py_true(lean_obj_arg unit, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); p_Py_IncRef(p_Py_True); return lean_io_result_mk_ok(wrap_pyobject(p_Py_True)); } LEAN_EXPORT lean_obj_res lean_py_false(lean_obj_arg unit, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); p_Py_IncRef(p_Py_False); return lean_io_result_mk_ok(wrap_pyobject(p_Py_False)); } @@ -474,7 +483,7 @@ LEAN_EXPORT lean_obj_res lean_py_false(lean_obj_arg unit, lean_obj_arg world) { /* ------------------------------------------------------------------ */ LEAN_EXPORT lean_obj_res lean_py_of_bool(uint8_t b, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return ok_owned_or_err(p_PyBool_FromLong(b ? 1 : 0)); } @@ -482,7 +491,7 @@ LEAN_EXPORT lean_obj_res lean_py_of_bool(uint8_t b, lean_obj_arg world) { * support the int64 range and error otherwise; this is what 99% of API * surface needs. Callers needing arbitrary precision can stringify. */ LEAN_EXPORT lean_obj_res lean_py_of_int64(b_lean_obj_arg n, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); long long v; if (lean_is_scalar(n)) { v = (long long) lean_scalar_to_int64(n); @@ -494,26 +503,26 @@ LEAN_EXPORT lean_obj_res lean_py_of_int64(b_lean_obj_arg n, lean_obj_arg world) } LEAN_EXPORT lean_obj_res lean_py_of_float(double f, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return ok_owned_or_err(p_PyFloat_FromDouble(f)); } LEAN_EXPORT lean_obj_res lean_py_of_string(b_lean_obj_arg s, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); const char *cs = lean_string_cstr(s); size_t n = lean_string_size(s) - 1; /* size includes terminating NUL */ return ok_owned_or_err(p_PyUnicode_DecodeUTF8(cs, (Py_ssize_t)n, NULL)); } LEAN_EXPORT lean_obj_res lean_py_of_bytes(b_lean_obj_arg ba, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); Py_ssize_t n = (Py_ssize_t) lean_sarray_size(ba); const char *p = (const char *) lean_sarray_cptr(ba); return ok_owned_or_err(p_PyBytes_FromStringAndSize(p, n)); } LEAN_EXPORT lean_obj_res lean_py_of_list(b_lean_obj_arg arr, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); size_t n = lean_array_size(arr); PyObject *list = p_PyList_New((Py_ssize_t)n); if (!list) return raise_py_error(); @@ -527,7 +536,7 @@ LEAN_EXPORT lean_obj_res lean_py_of_list(b_lean_obj_arg arr, lean_obj_arg world) } LEAN_EXPORT lean_obj_res lean_py_of_tuple(b_lean_obj_arg arr, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); size_t n = lean_array_size(arr); PyObject *tup = p_PyTuple_New((Py_ssize_t)n); if (!tup) return raise_py_error(); @@ -541,7 +550,7 @@ LEAN_EXPORT lean_obj_res lean_py_of_tuple(b_lean_obj_arg arr, lean_obj_arg world } LEAN_EXPORT lean_obj_res lean_py_of_dict(b_lean_obj_arg arr, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); PyObject *d = p_PyDict_New(); if (!d) return raise_py_error(); size_t n = lean_array_size(arr); @@ -565,21 +574,21 @@ LEAN_EXPORT lean_obj_res lean_py_of_dict(b_lean_obj_arg arr, lean_obj_arg world) /* ------------------------------------------------------------------ */ LEAN_EXPORT lean_obj_res lean_py_to_bool(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); int r = p_PyObject_IsTrue(unwrap_pyobject(p)); if (r < 0) return raise_py_error(); return lean_io_result_mk_ok(lean_box(r ? 1 : 0)); } LEAN_EXPORT lean_obj_res lean_py_to_int64(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); long long v = p_PyLong_AsLongLong(unwrap_pyobject(p)); if (v == -1 && p_PyErr_Occurred()) return raise_py_error(); return lean_io_result_mk_ok(lean_int64_to_int((int64_t) v)); } LEAN_EXPORT lean_obj_res lean_py_to_float(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); double d = p_PyFloat_AsDouble(unwrap_pyobject(p)); if (d == -1.0 && p_PyErr_Occurred()) return raise_py_error(); return lean_io_result_mk_ok(lean_box_float(d)); @@ -598,22 +607,22 @@ static lean_object *py_obj_to_lean_string(PyObject *s) { } LEAN_EXPORT lean_obj_res lean_py_to_string(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return py_obj_to_lean_string(p_PyObject_Str(unwrap_pyobject(p))); } LEAN_EXPORT lean_obj_res lean_py_repr(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return py_obj_to_lean_string(p_PyObject_Repr(unwrap_pyobject(p))); } LEAN_EXPORT lean_obj_res lean_py_str(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return py_obj_to_lean_string(p_PyObject_Str(unwrap_pyobject(p))); } LEAN_EXPORT lean_obj_res lean_py_type_name(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); PyObject *ty = p_PyObject_Type(unwrap_pyobject(p)); if (!ty) return raise_py_error(); PyObject *nm = p_PyObject_GetAttrString(ty, "__name__"); @@ -626,51 +635,51 @@ LEAN_EXPORT lean_obj_res lean_py_type_name(b_lean_obj_arg p, lean_obj_arg world) /* ------------------------------------------------------------------ */ LEAN_EXPORT lean_obj_res lean_py_getattr(b_lean_obj_arg p, b_lean_obj_arg name, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return ok_owned_or_err(p_PyObject_GetAttrString(unwrap_pyobject(p), lean_string_cstr(name))); } LEAN_EXPORT lean_obj_res lean_py_setattr(b_lean_obj_arg p, b_lean_obj_arg name, b_lean_obj_arg v, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); int r = p_PyObject_SetAttrString(unwrap_pyobject(p), lean_string_cstr(name), unwrap_pyobject(v)); if (r != 0) return raise_py_error(); return lean_io_result_mk_ok(lean_box(0)); } LEAN_EXPORT lean_obj_res lean_py_hasattr(b_lean_obj_arg p, b_lean_obj_arg name, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); int r = p_PyObject_HasAttrString(unwrap_pyobject(p), lean_string_cstr(name)); return lean_io_result_mk_ok(lean_box(r ? 1 : 0)); } LEAN_EXPORT lean_obj_res lean_py_getitem(b_lean_obj_arg p, b_lean_obj_arg k, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return ok_owned_or_err(p_PyObject_GetItem(unwrap_pyobject(p), unwrap_pyobject(k))); } LEAN_EXPORT lean_obj_res lean_py_setitem(b_lean_obj_arg p, b_lean_obj_arg k, b_lean_obj_arg v, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); int r = p_PyObject_SetItem(unwrap_pyobject(p), unwrap_pyobject(k), unwrap_pyobject(v)); if (r != 0) return raise_py_error(); return lean_io_result_mk_ok(lean_box(0)); } LEAN_EXPORT lean_obj_res lean_py_length(b_lean_obj_arg p, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); Py_ssize_t r = p_PyObject_Length(unwrap_pyobject(p)); if (r < 0) return raise_py_error(); return lean_io_result_mk_ok(lean_int64_to_int((int64_t) r)); } LEAN_EXPORT lean_obj_res lean_py_eq(b_lean_obj_arg a, b_lean_obj_arg b, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); int r = p_PyObject_RichCompareBool(unwrap_pyobject(a), unwrap_pyobject(b), Py_EQ); if (r < 0) return raise_py_error(); return lean_io_result_mk_ok(lean_box(r ? 1 : 0)); } LEAN_EXPORT lean_obj_res lean_py_is(b_lean_obj_arg a, b_lean_obj_arg b, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return lean_io_result_mk_ok(lean_box(unwrap_pyobject(a) == unwrap_pyobject(b) ? 1 : 0)); } @@ -679,7 +688,7 @@ LEAN_EXPORT lean_obj_res lean_py_is(b_lean_obj_arg a, b_lean_obj_arg b, lean_obj /* ------------------------------------------------------------------ */ LEAN_EXPORT lean_obj_res lean_py_call(b_lean_obj_arg f, b_lean_obj_arg args, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); size_t n = lean_array_size(args); PyObject *tup = p_PyTuple_New((Py_ssize_t)n); if (!tup) return raise_py_error(); @@ -694,7 +703,7 @@ LEAN_EXPORT lean_obj_res lean_py_call(b_lean_obj_arg f, b_lean_obj_arg args, lea } LEAN_EXPORT lean_obj_res lean_py_call_kw(b_lean_obj_arg f, b_lean_obj_arg args, b_lean_obj_arg kwargs, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); size_t n = lean_array_size(args); PyObject *tup = p_PyTuple_New((Py_ssize_t)n); if (!tup) return raise_py_error(); @@ -726,7 +735,7 @@ LEAN_EXPORT lean_obj_res lean_py_call_kw(b_lean_obj_arg f, b_lean_obj_arg args, /* ------------------------------------------------------------------ */ LEAN_EXPORT lean_obj_res lean_py_import(b_lean_obj_arg name, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return ok_owned_or_err(p_PyImport_ImportModule(lean_string_cstr(name))); } @@ -737,7 +746,7 @@ static PyObject *get_main_globals(void) { } LEAN_EXPORT lean_obj_res lean_py_eval(b_lean_obj_arg src, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); PyObject *g = get_main_globals(); if (!g) return raise_py_error(); PyObject *r = p_PyRun_StringFlags(lean_string_cstr(src), Py_eval_input, g, g, NULL); @@ -745,7 +754,7 @@ LEAN_EXPORT lean_obj_res lean_py_eval(b_lean_obj_arg src, lean_obj_arg world) { } LEAN_EXPORT lean_obj_res lean_py_exec(b_lean_obj_arg src, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); PyObject *g = get_main_globals(); if (!g) return raise_py_error(); PyObject *r = p_PyRun_StringFlags(lean_string_cstr(src), Py_file_input, g, g, NULL); @@ -760,7 +769,7 @@ LEAN_EXPORT lean_obj_res lean_py_exec(b_lean_obj_arg src, lean_obj_arg world) { #define BINOP(name, fn) \ LEAN_EXPORT lean_obj_res name(b_lean_obj_arg a, b_lean_obj_arg b, lean_obj_arg world) { \ - (void)world; ENSURE_INIT(); \ + (void)world; ENSURE_INIT(); WITH_GIL(); \ return ok_owned_or_err(fn(unwrap_pyobject(a), unwrap_pyobject(b))); \ } @@ -770,13 +779,13 @@ BINOP(lean_py_mul, p_PyNumber_Multiply) BINOP(lean_py_div, p_PyNumber_TrueDivide) LEAN_EXPORT lean_obj_res lean_py_pow(b_lean_obj_arg a, b_lean_obj_arg b, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); /* PyNumber_Power borrows all three arguments; no IncRef needed. */ return ok_owned_or_err(p_PyNumber_Power(unwrap_pyobject(a), unwrap_pyobject(b), p_Py_None)); } LEAN_EXPORT lean_obj_res lean_py_neg(b_lean_obj_arg a, lean_obj_arg world) { - (void)world; ENSURE_INIT(); + (void)world; ENSURE_INIT(); WITH_GIL(); return ok_owned_or_err(p_PyNumber_Negative(unwrap_pyobject(a))); } @@ -846,8 +855,7 @@ static void format_lean_io_error(lean_object *err, char *buf, size_t bufsz) { snprintf(buf, bufsz, "Lean error (no payload)"); return; } - /* Most IO.Error variants have a String at field 0. userError is - * tag 18, payload (msg : String). */ + /* Most IO.Error variants (e.g. userError) carry a String at field 0. */ if (lean_is_scalar(err)) { snprintf(buf, bufsz, "Lean IO.Error (tag %u, no payload)", (unsigned)lean_unbox(err)); @@ -856,7 +864,7 @@ static void format_lean_io_error(lean_object *err, char *buf, size_t bufsz) { unsigned tag = lean_ptr_tag(err); /* lean_ctor_get returns a borrowed pointer */ lean_object *fld = lean_ctor_get(err, 0); - if (fld && !lean_is_scalar(fld) && lean_ptr_tag(fld) == 249 /* string tag */) { + if (fld && !lean_is_scalar(fld) && lean_is_string(fld)) { snprintf(buf, bufsz, "%s", lean_string_cstr(fld)); return; } @@ -1175,7 +1183,7 @@ static PyObject *get_lean_obj_handle_type(void) { */ LEAN_EXPORT lean_obj_res lean_py_of_lean_obj(b_lean_obj_arg obj, lean_obj_arg world) { (void)world; - ENSURE_INIT(); + ENSURE_INIT(); WITH_GIL(); PyObject *type = get_lean_obj_handle_type(); if (!type) return raise_io_error("LeanPy: failed to create LeanObjHandle type"); @@ -1200,7 +1208,7 @@ LEAN_EXPORT lean_obj_res lean_py_of_lean_obj(b_lean_obj_arg obj, lean_obj_arg wo */ LEAN_EXPORT lean_obj_res lean_py_to_lean_obj(b_lean_obj_arg py_ext, lean_obj_arg world) { (void)world; - ENSURE_INIT(); + ENSURE_INIT(); WITH_GIL(); if (!lean_is_external(py_ext)) { /* Return none */ diff --git a/README.md b/README.md index 710e0e6..cfae63f 100644 --- a/README.md +++ b/README.md @@ -333,6 +333,80 @@ objects: lib.makeList123(None) # [1, 2, 3] (not an opaque handle) ``` +## Type stubs + +A `LeanLibrary` exposes its functions and types dynamically, so editors and +type-checkers see only `Any`. Generate a `.pyi` stub from the same registry +that drives marshalling — one source of truth for runtime conversion *and* +static types: + +```bash +python -m lean_py.stubgen path/to/project MyLib -o MyLib.pyi +``` + +or at runtime: + +```python +lib = LeanLibrary.from_lake("path/to/project", "MyLib", build=True) +lib.write_stub("MyLib.pyi") +``` + +The stub declares a `MyLibLibrary(LeanLibrary)` subclass with typed methods +(`def add(self, a0: int, a1: int, /) -> int: ...`) and one class per derived +type, including per-constructor classes for pattern matching. Annotate the +`from_lake` result to opt in: + +```python +from MyLib import MyLibLibrary # the generated stub +lib: MyLibLibrary = LeanLibrary.from_lake("path/to/project", "MyLib") # type: ignore[assignment] +lib.add(3, 4) # checked: (int, int) -> int +``` + +Parameter *names* are not in the registry yet, so parameters are positional +(`a0, a1, ...`), matching the runtime wrappers, which reject keyword arguments. + +The stub annotations come from the same `TypeRepr` that drives marshalling, so +they can't drift from runtime behaviour. That representation also backs an +optional runtime check — one description, static hints and value validation +alike: + +```python +from lean_py import set_argument_typechecking + +set_argument_typechecking(True) +lib.add(3, "four") # TypeError: add arg 1: expected `Int` (int), got str 'four' +``` + +It is off by default (the marshaller is deliberately lenient); enable it while +developing for clearer errors before values cross the FFI boundary. + +## Distribution: self-contained wheels + +By default a `LeanLibrary` discovers the Lean runtime from the active toolchain +(`lean --print-prefix`), so every user needs elan installed. To ship a library +that installs with **no toolchain**, bundle the dylib together with its Lean +runtime dependency closure into a wheel: + +```bash +python -m lean_py.packaging build path/to/project MyLib --version 0.1.0 -o dist/ +``` + +The bundler vendors the dylib, the Lean runtime shared libraries, and `lean.h` +into the wheel, and rewrites their install names / RPATHs so they resolve each +other via `@loader_path` (macOS) or `$ORIGIN` (Linux). The wheel ships a loader: + +```python +from mylib import load # the bundled package +lib = load() # a ready LeanLibrary, no elan required +lib.myFunction(42) +``` + +Because lean.py binds through **ctypes** rather than a CPython C-extension, the +wheel is ABI-independent and tagged `py3-none-` — the only +platform-specific content is the vendored dylibs. (This is the analogue of +nerodia's `abi3` wheels; lean.py needs no Python-ABI tag at all.) Bundling +requires `install_name_tool`/`codesign` on macOS or `patchelf` on Linux. + ## Exceptions Errors carry type information across the boundary: @@ -372,10 +446,10 @@ cd tests/lean && lake build TestLib:shared && cd ../.. uv run pytest tests -v ``` -125 tests covering: FFI primitives, all marshalled types, typed -exceptions, bidirectional introspection, kernel facade (goal state, -tactics, environment, elaboration, frontend, serialisation), Python-in-Lean -demos, and refcount stress tests. +1300+ tests across 17 files covering: FFI primitives, all marshalled +types, typed exceptions, bidirectional introspection, kernel facade (goal +state, tactics, environment, elaboration, frontend, serialisation), +Python-in-Lean demos, the z3py-compatible layer, and refcount stress tests. ## How it works diff --git a/lean_py/__init__.py b/lean_py/__init__.py index 04d3431..b259cad 100644 --- a/lean_py/__init__.py +++ b/lean_py/__init__.py @@ -22,7 +22,7 @@ from lean_py.exceptions import LeanError, LeanPyCallbackError from lean_py.kernel import GoalState, Kernel, TacticResult -from lean_py.library import LeanLibrary, Library +from lean_py.library import LeanLibrary, Library, set_argument_typechecking from lean_py.marshal import LeanInductiveValue, LeanObj, Marshaller from lean_py.registry import ( CtorInfo, @@ -31,6 +31,7 @@ TypeInfo, TypeRepr, ) +from lean_py.stubgen import generate_stub __all__ = [ "LeanLibrary", @@ -48,4 +49,6 @@ "Kernel", "GoalState", "TacticResult", + "generate_stub", + "set_argument_typechecking", ] diff --git a/lean_py/_parse.py b/lean_py/_parse.py index 770143b..c5d2cc3 100644 --- a/lean_py/_parse.py +++ b/lean_py/_parse.py @@ -1,6 +1,7 @@ """Parse lean.h and extract declarations for runtime binding.""" import hashlib +import os import pickle import re import subprocess @@ -75,7 +76,16 @@ def find_lean_header() -> Path: install picked the toolchain. 2. Fall back to constructing the elan path from the project's `lean-toolchain` file, for callers who don't have `lean` on PATH. + + A ``LEANPY_BUNDLE_DIR`` bundle ships its own ``lean.h`` so a + wheel-installed library can build its ctypes bindings without a toolchain. """ + bundle = os.environ.get("LEANPY_BUNDLE_DIR") + if bundle: + for cand in (Path(bundle) / "lean.h", Path(bundle) / "include" / "lean" / "lean.h"): + if cand.exists(): + return cand + try: prefix = subprocess.check_output(["lean", "--print-prefix"], text=True).strip() header = Path(prefix) / "include" / "lean" / "lean.h" diff --git a/lean_py/_runtime.py b/lean_py/_runtime.py index 27b792a..93f7d9b 100644 --- a/lean_py/_runtime.py +++ b/lean_py/_runtime.py @@ -699,32 +699,11 @@ def mk_string(self, s): s = s.encode("utf-8") return self.lean_mk_string(s) - def inc_ref(self, obj): - """Increment reference counter.""" - if self.lean_is_st(obj): - obj.contents.m_rc += 1 - - def dec_ref(self, obj): - """Decrement reference counter.""" - if self.lean_is_st(obj): - obj.contents.m_rc -= 1 - if obj.contents.m_rc == 0: - self.lean_free_object(obj) - elif obj.contents.m_rc != 0: - self.lean_dec_ref_cold(obj) - - def io_result_is_ok(self, res) -> bool: - """Check if an IO result is Ok (tag == 0).""" - return res.contents.m_tag == 0 - def io_result_show_error(self, res): """Display an IO error result.""" self.lean_io_result_show_error(res) class_dict["mk_string"] = mk_string - class_dict["inc_ref"] = inc_ref - class_dict["dec_ref"] = dec_ref - class_dict["io_result_is_ok"] = io_result_is_ok class_dict["io_result_show_error"] = io_result_show_error diff --git a/lean_py/lean_types.py b/lean_py/lean_types.py deleted file mode 100644 index 32a5717..0000000 --- a/lean_py/lean_types.py +++ /dev/null @@ -1,118 +0,0 @@ -""" -Higher level types wrapping Lean objects. -""" - - -# ============================================================================ -# Higher-level Python Type Wrappers -# ============================================================================ - -import ctypes -from ctypes import POINTER, addressof - -from lean_py.base_types import LeanArrayObject, LeanStringObject -from lean_py.lean_ffi import LeanFFI, get_lean_ffi - - -class LeanValue: - """Base class for Python-friendly Lean value wrappers.""" - - def __init__(self, ptr): - """ - Initialize with a Lean object pointer. - - Args: - ptr: Pointer to Lean object - ffi: LeanFFI instance for managing the value - """ - self.ptr = ptr - self.ffi: LeanFFI = get_lean_ffi() - - def __del__(self): - """Automatically decrement reference when Python object is garbage collected.""" - if self.ptr: - self.ffi.dec_ref(self.ptr) - - -class LeanString(LeanValue): - """Python wrapper for Lean strings.""" - - def to_python_string(self): - """Convert to Python string.""" - if self.ptr is None: - return "" - - string_obj = ctypes.cast(self.ptr, POINTER(LeanStringObject)).contents - if string_obj.m_size == 0: - return "" - m_data_start = addressof(string_obj) + LeanStringObject.m_data.offset - - # m_data is a pointer to char, get the raw bytes - return ctypes.string_at(m_data_start, string_obj.m_size - 1).decode("utf-8") - - def __str__(self): - return self.to_python_string() - - def __repr__(self): - return f"LeanString({self.to_python_string()!r})" - - -class LeanArray(LeanValue): - """Python wrapper for Lean arrays.""" - - def size(self): - """Get the size of the array.""" - array_obj = ctypes.cast(self.ptr, POINTER(LeanArrayObject)).contents - return array_obj.m_size - - def get(self, index): - """Get element at index.""" - array_obj = ctypes.cast(self.ptr, POINTER(LeanArrayObject)).contents - if index < 0 or index >= array_obj.m_size: - raise IndexError(f"Index {index} out of bounds for array of size {array_obj.m_size}") - - elem_ptr = array_obj.m_data[index] - self.ffi.inc_ref(elem_ptr) - return LeanValue(elem_ptr) - - def to_python_list(self): - """Convert to Python list.""" - return [self.get(i) for i in range(self.size())] - - def __len__(self): - return self.size() - - def __getitem__(self, index): - return self.get(index) - - -class LeanIOResult(LeanValue): - """Python wrapper for Lean IO results.""" - - def is_ok(self): - """Check if result is Ok.""" - return self.ffi.io_result_is_ok(self.ptr) - - def is_error(self): - """Check if result is Error.""" - return not self.is_ok() - - def get_or_raise(self): - """ - Get the value if Ok, or raise an exception if Error. - - Raises: - RuntimeError: If the result is an Error - """ - if self.is_ok(): - # For Ok, the value is in the second field of the Result - result_obj = ctypes.cast(self.ptr, POINTER(LeanArrayObject)).contents - if result_obj.m_size > 0: - val_ptr = result_obj.m_data[0] - self.ffi.inc_ref(val_ptr) - return LeanValue(val_ptr) - return LeanValue(self.ffi.lean_box(0)) - else: - # For Error, display and raise - self.ffi.io_result_show_error(self.ptr) - raise RuntimeError("Lean IO error occurred") diff --git a/lean_py/library.py b/lean_py/library.py index de29755..22419fb 100644 --- a/lean_py/library.py +++ b/lean_py/library.py @@ -76,6 +76,12 @@ def _ensure_rpath(dylib: Path) -> None: """ if sys.platform != "darwin": return + from lean_py.utils import bundle_dir + + if bundle_dir() is not None: + # A bundled dylib is already relocated to `@loader_path`; leave it be + # (and avoid a toolchain lookup that would fail without elan). + return libdir = lean_lib_dir() try: out = subprocess.run( @@ -181,6 +187,24 @@ def __call__(self, *args, **kwargs) -> LeanInductiveValue: return LeanInductiveValue(self._ti.name, self._ctor.name, self._ctor.tag, tuple(args)) +# Optional runtime validation of arguments against their Lean `TypeRepr`. +# Off by default (the marshaller is intentionally lenient); enable it for +# clearer errors during development. See `set_argument_typechecking`. +_argument_typechecking = False + + +def set_argument_typechecking(enabled: bool) -> None: + """Enable/disable runtime validation of arguments to `@[python]` functions. + + When enabled, each argument is checked against the same `TypeRepr` that + drives marshalling (:meth:`lean_py.registry.TypeRepr.check`), raising a + clear ``TypeError`` before the value crosses the FFI boundary. Applies to + functions bound after — and calls made while — it is enabled. + """ + global _argument_typechecking + _argument_typechecking = bool(enabled) + + # ============================================================================ # Generated function wrappers # ============================================================================ @@ -237,9 +261,16 @@ def _ctype_for_call(ct): _ffi = get_lean_ffi() + params = finfo.params + def _wrapper(*args): if len(args) != len(pwraps): raise TypeError(f"{finfo.exportName}: expected {len(pwraps)} args, got {len(args)}") + if _argument_typechecking: + # Validate against the same TypeRepr that drives marshalling, + # for a clear error before the value reaches the FFI boundary. + for i, (p, a) in enumerate(zip(params, args)): + p.check(a, name=f"{finfo.declName.split('.')[-1]} arg {i}") cargs = [] for w, a in zip(pwraps, args): v = w.to_lean(a) @@ -504,9 +535,9 @@ def _initialize_lean_module(self) -> None: result = init_fn(1, ctypes.cast(c_void_p(1), POINTER(LeanObject))) if result.contents.m_tag != 0: self.ffi.io_result_show_error(result) - self.ffi.dec_ref(result) + self.ffi.lean_dec(result) raise RuntimeError(f"{init_name} failed") - self.ffi.dec_ref(result) + self.ffi.lean_dec(result) # The user library's `initialize_*` block has now run all its # `initialize` declarations. Flip the runtime's global init # flag so subsequent calls (e.g. frontend operations that @@ -539,7 +570,7 @@ def _call_string_export(self, name: str) -> str: raw = cstr.value if isinstance(cstr, ctypes.c_char_p) else cstr return (raw or b"").decode("utf-8") finally: - self.ffi.dec_ref(result_ptr) + self.ffi.lean_dec(result_ptr) # -- public ----------------------------------------------------------- @@ -550,6 +581,21 @@ def __getitem__(self, key: str) -> Any: return self._types[key] raise KeyError(key) + def generate_stub(self) -> str: + """Return a ``.pyi`` type stub describing this library's surface.""" + from lean_py.stubgen import generate_stub_for_library + + return generate_stub_for_library(self) + + def write_stub(self, path: str | os.PathLike | None = None) -> str: + """Write a ``.pyi`` stub for this library and return the path written. + + Defaults to ``.pyi`` in the current directory. + """ + out = Path(path) if path is not None else Path(f"{self.name}.pyi") + out.write_text(self.generate_stub(), encoding="utf-8") + return str(out) + def __repr__(self) -> str: return f"" diff --git a/lean_py/packaging.py b/lean_py/packaging.py new file mode 100644 index 0000000..c6fe1d6 --- /dev/null +++ b/lean_py/packaging.py @@ -0,0 +1,373 @@ +"""Bundle a compiled Lean library into a self-contained, installable wheel. + +A `LeanLibrary` normally loads the Lake-built dylib and discovers the Lean +runtime shared libraries from the active toolchain (`lean --print-prefix`). +That requires every user to have `elan` and the matching toolchain installed. + +This module vendors the dylib together with its Lean runtime dependency closure +into one directory, rewrites their install names / RPATHs so they resolve each +other via ``@loader_path`` (macOS) or ``$ORIGIN`` (Linux), and packages the +result as a wheel with a tiny loader. Installing that wheel needs no toolchain. + +Note on wheel tags: lean.py binds through **ctypes**, not a CPython C +extension, so the wheel is ABI-independent — it is tagged ``py3-none-`` +(pure-Python loader plus platform-specific data dylibs), not ``abi3``. The +platform-specific part is the vendored dylibs, not a compiled extension. + + python -m lean_py.packaging build path/to/project MyLib --version 0.1.0 -o dist/ + +or programmatically:: + + from lean_py.packaging import build_wheel + build_wheel("path/to/project", "MyLib", version="0.1.0", out_dir="dist") +""" + +from __future__ import annotations + +import base64 +import hashlib +import os +import shutil +import subprocess +import sys +import sysconfig +import zipfile +from dataclasses import dataclass, field +from pathlib import Path + +from lean_py.utils import all_lean_runtime_libs, find_lean_dynlib, shared_lib_extension + +_LIBS_SUBDIR = "_lean_libs" + + +# --------------------------------------------------------------------------- +# Native-library relocation +# --------------------------------------------------------------------------- + + +def _run(args: list[str]) -> None: + res = subprocess.run(args, capture_output=True, text=True) + if res.returncode != 0: + raise RuntimeError( + f"command failed ({res.returncode}): {' '.join(args)}\n{res.stderr.strip()}" + ) + + +def _make_writable(path: Path) -> None: + """Toolchain dylibs are often read-only; relocation needs write access.""" + mode = path.stat().st_mode + os.chmod(path, mode | 0o200) + + +def _otool_deps(lib: Path) -> list[str]: + """The install-name dependencies of a Mach-O dylib (excluding its own id).""" + out = subprocess.run( + ["otool", "-L", str(lib)], check=True, capture_output=True, text=True + ).stdout + lines = out.splitlines()[1:] # first line is the file name + deps = [] + for line in lines: + line = line.strip() + if not line: + continue + deps.append(line.split(" ", 1)[0]) + # The first dependency line is the library's own id; drop it. + return deps[1:] if deps else deps + + +def _try_run(args: list[str]) -> bool: + """Run a relocation command, tolerating "load commands don't fit" errors + on toolchain libraries that were linked without header padding.""" + try: + _run(args) + return True + except RuntimeError: + return False + + +def _relocate_macos(dest: Path, leaves: set[str]) -> None: + """Point every bundled dylib at its siblings without lengthening install + names past the Mach-O header padding. + + The Lean runtime libs are linked without ``-headerpad``, so we must not + grow their load commands: ids are left untouched, ``@rpath/leaf`` deps are + resolved by adding a single (small) ``@loader_path`` RPATH, and only + absolute toolchain paths (always longer than ``@loader_path/leaf``) are + rewritten in place. install_name_tool invalidates the signature, so we + re-sign ad-hoc afterwards (arm64 dyld rejects unsigned modified Mach-O). + """ + for lib in sorted(dest.glob(f"*{shared_lib_extension()}")): + needs_rpath = False + for dep in _otool_deps(lib): + leaf = Path(dep).name + if leaf not in leaves or dep.startswith("@loader_path/"): + continue + if dep.startswith("/"): + # Absolute toolchain path: rewrite to @loader_path (fits). + _run(["install_name_tool", "-change", dep, f"@loader_path/{leaf}", str(lib)]) + else: + # @rpath/leaf (or similar): resolve via an @loader_path RPATH. + needs_rpath = True + if needs_rpath: + _try_run(["install_name_tool", "-add_rpath", "@loader_path", str(lib)]) + # Re-sign ad-hoc so the modified Mach-O loads on arm64. + _try_run(["codesign", "--force", "--sign", "-", str(lib)]) + + # Fail loudly if any absolute toolchain reference survived — that would + # break a toolchain-less install. + for lib in sorted(dest.glob(f"*{shared_lib_extension()}")): + for dep in _otool_deps(lib): + if dep.startswith("/") and Path(dep).name in leaves: + raise RuntimeError( + f"{lib.name} still references {dep} by absolute path after " + f"relocation; the bundle would not load standalone." + ) + + +def _relocate_linux(dest: Path) -> None: + """Point every bundled .so at its siblings via an ``$ORIGIN`` RPATH.""" + patchelf = shutil.which("patchelf") + if not patchelf: + raise RuntimeError( + "patchelf is required to bundle a Lean library on Linux " + "(install it via your package manager)." + ) + for lib in sorted(dest.glob(f"*{shared_lib_extension()}")): + _run([patchelf, "--set-rpath", "$ORIGIN", "--force-rpath", str(lib)]) + + +def relocate_bundle(dest: Path) -> None: + """Make every native library in ``dest`` reference its siblings relatively.""" + leaves = {p.name for p in dest.glob(f"*{shared_lib_extension()}")} + if sys.platform == "darwin": + _relocate_macos(dest, leaves) + elif sys.platform.startswith("linux"): + _relocate_linux(dest) + else: + raise RuntimeError(f"bundling is not supported on {sys.platform}") + + +@dataclass +class Bundle: + """A relocated, self-contained set of native libraries.""" + + dir: Path + main_lib: Path # the user's library dylib inside the bundle + library_name: str + runtime_libs: list[Path] = field(default_factory=list) + + +def bundle_native_libs(main_dylib: Path, library_name: str, dest: Path) -> Bundle: + """Copy ``main_dylib`` plus the Lean runtime closure into ``dest`` and + relocate them to load standalone. Returns the resulting :class:`Bundle`.""" + main_dylib = Path(main_dylib).resolve() + if not main_dylib.exists(): + raise FileNotFoundError(main_dylib) + dest.mkdir(parents=True, exist_ok=True) + + # The Lean runtime closure the loader preloads today; proven-sufficient set. + runtime = list(all_lean_runtime_libs()) + lean_shared = find_lean_dynlib() + if lean_shared not in runtime and lean_shared.exists(): + runtime.append(lean_shared) + + copied_runtime: list[Path] = [] + for lib in runtime: + target = dest / lib.name + if not target.exists(): + shutil.copy2(lib, target) + _make_writable(target) + copied_runtime.append(target) + + main_target = dest / main_dylib.name + shutil.copy2(main_dylib, main_target) + _make_writable(main_target) + + # Ship lean.h so a toolchain-less install can build its ctypes bindings. + from lean_py._parse import find_lean_header + + try: + header = find_lean_header() + shutil.copy2(header, dest / "lean.h") + except FileNotFoundError: + pass + + relocate_bundle(dest) + return Bundle( + dir=dest, + main_lib=main_target, + library_name=library_name, + runtime_libs=copied_runtime, + ) + + +# --------------------------------------------------------------------------- +# Wheel assembly +# --------------------------------------------------------------------------- + +_LOADER_TEMPLATE = '''\ +"""Auto-generated loader for the vendored Lean library ``{name}``. + +Import and call :func:`load` to get a ready-to-use ``LeanLibrary`` backed by +the bundled Lean runtime — no elan / toolchain required. +""" + +import os +from pathlib import Path + +_HERE = Path(__file__).resolve().parent +_LIBS = _HERE / "{libs_subdir}" +_MAIN = _LIBS / "{main_leaf}" + +# Point toolchain discovery at the vendored runtime before importing lean_py. +os.environ.setdefault("LEANPY_BUNDLE_DIR", str(_LIBS)) + +from lean_py.library import LeanLibrary # noqa: E402 +from lean_py.utils import add_lean_lib_to_dyld_path # noqa: E402 + +_cached: "LeanLibrary | None" = None + + +def load() -> LeanLibrary: + """Load the vendored ``{name}`` library (cached per process).""" + global _cached + if _cached is None: + add_lean_lib_to_dyld_path() + _cached = LeanLibrary(str(_MAIN), "{name}") + return _cached +''' + + +def _platform_tag() -> str: + """A PEP 425 platform tag derived from the current interpreter.""" + return sysconfig.get_platform().replace("-", "_").replace(".", "_") + + +def _record_line(arc: str, data: bytes) -> str: + digest = base64.urlsafe_b64encode(hashlib.sha256(data).digest()).rstrip(b"=") + return f"{arc},sha256={digest.decode()},{len(data)}" + + +def build_wheel( + project_dir: str | os.PathLike, + library_name: str, + *, + version: str = "0.0.0", + out_dir: str | os.PathLike = "dist", + package_name: str | None = None, + build: bool = True, + dist_name: str | None = None, +) -> Path: + """Build a self-contained wheel for the Lean library ``library_name``. + + ``package_name`` is the importable Python package the wheel installs + (default: ``library_name`` lower-cased). ``dist_name`` is the distribution + name on PyPI (default: same as the package). Returns the wheel path. + """ + from lean_py.library import LeanLibrary + + project = Path(project_dir).resolve() + # Loading resolves (and optionally builds) the dylib and gives us its path. + lib = LeanLibrary.from_lake(project, library_name, build=build) + main_dylib = Path(lib.path) + + pkg = (package_name or library_name).replace("-", "_").lower() + dist = (dist_name or pkg).replace("_", "-") + out = Path(out_dir) + out.mkdir(parents=True, exist_ok=True) + + staging = out / f"_build_{pkg}" + if staging.exists(): + shutil.rmtree(staging) + pkg_dir = staging / pkg + libs_dir = pkg_dir / _LIBS_SUBDIR + libs_dir.mkdir(parents=True) + + bundle = bundle_native_libs(main_dylib, library_name, libs_dir) + + (pkg_dir / "__init__.py").write_text( + _LOADER_TEMPLATE.format( + name=library_name, libs_subdir=_LIBS_SUBDIR, main_leaf=bundle.main_lib.name + ), + encoding="utf-8", + ) + (pkg_dir / "py.typed").write_text("", encoding="utf-8") + + tag = f"py3-none-{_platform_tag()}" + wheel_name = f"{dist.replace('-', '_')}-{version}-{tag}.whl" + wheel_path = out / wheel_name + distinfo = f"{dist.replace('-', '_')}-{version}.dist-info" + + metadata = ( + "Metadata-Version: 2.1\n" + f"Name: {dist}\n" + f"Version: {version}\n" + "Summary: Self-contained Lean library bundled by lean_py.\n" + "Requires-Dist: lean_py\n" + ) + wheel_meta = ( + f"Wheel-Version: 1.0\nGenerator: lean_py.packaging\nRoot-Is-Purelib: false\nTag: {tag}\n" + ) + + # Assemble the zip and a RECORD. + records: list[str] = [] + if wheel_path.exists(): + wheel_path.unlink() + with zipfile.ZipFile(wheel_path, "w", zipfile.ZIP_DEFLATED) as zf: + for path in sorted(staging.rglob("*")): + if path.is_dir(): + continue + arc = str(path.relative_to(staging)) + data = path.read_bytes() + zf.writestr(arc, data) + records.append(_record_line(arc, data)) + for arc, text in ( + (f"{distinfo}/METADATA", metadata), + (f"{distinfo}/WHEEL", wheel_meta), + ): + data = text.encode() + zf.writestr(arc, data) + records.append(_record_line(arc, data)) + record_arc = f"{distinfo}/RECORD" + records.append(f"{record_arc},,") + zf.writestr(record_arc, "\n".join(records) + "\n") + + shutil.rmtree(staging, ignore_errors=True) + return wheel_path + + +def _main(argv: list[str] | None = None) -> int: + import argparse + + parser = argparse.ArgumentParser( + prog="python -m lean_py.packaging", + description="Bundle a Lean library into a self-contained wheel.", + ) + sub = parser.add_subparsers(dest="cmd", required=True) + + b = sub.add_parser("build", help="Build a self-contained wheel.") + b.add_argument("project_dir") + b.add_argument("library_name") + b.add_argument("--version", default="0.0.0") + b.add_argument("-o", "--out-dir", default="dist") + b.add_argument("--package-name", default=None) + b.add_argument("--dist-name", default=None) + b.add_argument("--no-build", action="store_true") + + args = parser.parse_args(argv) + if args.cmd == "build": + wheel = build_wheel( + args.project_dir, + args.library_name, + version=args.version, + out_dir=args.out_dir, + package_name=args.package_name, + dist_name=args.dist_name, + build=not args.no_build, + ) + print(f"Wrote {wheel}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(_main()) diff --git a/lean_py/registry.py b/lean_py/registry.py index 2a2b764..6566433 100644 --- a/lean_py/registry.py +++ b/lean_py/registry.py @@ -9,10 +9,19 @@ from __future__ import annotations import json +import keyword from dataclasses import dataclass, field from typing import Any +def py_ident(name: str) -> str: + """A short Lean name made into a valid, non-keyword Python identifier.""" + short = name.split(".")[-1] + if not short.isidentifier() or keyword.iskeyword(short): + return short + "_" + return short + + @dataclass(frozen=True) class TypeRepr: """Structural description of a Lean type as it appears in the registry. @@ -95,6 +104,136 @@ def short(self) -> str: return self.name or "?" return f"<{k}>" + # -- unified type interpretation ------------------------------------------ + # + # A ``TypeRepr`` is the single source of truth for a Lean type's Python + # face. From it we derive both the *static* annotation (used by the stub + # generator) and a *runtime* predicate over Python values (used for + # argument validation). This mirrors nerodia's ``Typing = Py.Raw → Prop``, + # where one description drives static hints and runtime checks alike — + # adapted to lean.py's registry-driven design. + + def python_annotation(self, known_types: set[str] | None = None, named_prefix: str = "") -> str: + """Render this type as a Python type-annotation string. + + ``known_types`` is the set of derived-type short names the caller has + classes for; a ``named`` reference resolves to ``named_prefix + short`` + when known, else ``Any``. When ``known_types`` is ``None``, every named + type is assumed present (used for diagnostics). + """ + + def rec(x: TypeRepr | None) -> str: + return x.python_annotation(known_types, named_prefix) if x else "Any" + + k = self.kind + if k == "unit": + return "None" + if k == "bool": + return "bool" + if k in ("nat", "int", "uint", "sint"): + return "int" + if k == "char": + return "str" + if k in ("float", "float32"): + return "float" + if k == "string": + return "str" + if k == "pyobject": + return "Any" + if k in ("array", "list"): + return f"list[{rec(self.elem)}]" if self.elem else "list[Any]" + if k == "option": + return f"{rec(self.elem)} | None" if self.elem else "Any | None" + if k == "prod": + return f"tuple[{rec(self.a)}, {rec(self.b)}]" + if k == "sum": + return f"{rec(self.a)} | {rec(self.b)}" + if k == "io": + return rec(self.elem) if self.elem else "None" + if k == "except": + return rec(self.a) if self.a else "Any" + if k in ("named", "opaque"): + short = py_ident(self.name) if self.name else "" + if not short: + return "Any" + if known_types is None or short in known_types: + return f"{named_prefix}{short}" + return "Any" + return "Any" + + def matches(self, value: Any) -> bool: + """Return True if ``value`` is a plausible Python value for this type. + + The runtime half of the unified interpretation: a structural predicate + used to validate arguments before marshalling. Scalars and containers + are checked precisely; ``named`` types are checked by identity when the + value is a Lean inductive value and accepted leniently otherwise (the + marshaller also accepts tuple/constructor spellings).""" + k = self.kind + if k == "unit": + return value is None + if k == "bool": + return isinstance(value, bool) + if k == "nat": + return isinstance(value, int) and not isinstance(value, bool) and value >= 0 + if k in ("int", "sint"): + return isinstance(value, int) and not isinstance(value, bool) + if k == "uint": + return isinstance(value, int) and not isinstance(value, bool) and value >= 0 + if k in ("float", "float32"): + return isinstance(value, (int, float)) and not isinstance(value, bool) + if k == "char": + return isinstance(value, str) and len(value) == 1 + if k == "string": + return isinstance(value, str) + if k == "pyobject": + return True + if k in ("array", "list"): + if not isinstance(value, (list, tuple)): + return False + return self.elem is None or all(self.elem.matches(v) for v in value) + if k == "option": + return value is None or (self.elem is not None and self.elem.matches(value)) + if k == "prod": + return ( + isinstance(value, tuple) + and len(value) == 2 + and self.a is not None + and self.a.matches(value[0]) + and self.b is not None + and self.b.matches(value[1]) + ) + if k == "sum": + return (self.a is not None and self.a.matches(value)) or ( + self.b is not None and self.b.matches(value) + ) + if k == "io": + return self.elem is None or self.elem.matches(value) + if k == "except": + return self.a is None or self.a.matches(value) + if k in ("named", "opaque"): + return self._matches_named(value) + return True + + def _matches_named(self, value: Any) -> bool: + # A Lean inductive value/constructor carries its own type name; if so, + # require it to match. Anything else (tuple spellings, opaque handles) + # is accepted leniently. + type_name = getattr(value, "_type_name", None) + if type_name is None: + type_name = getattr(type(value), "_type_name", None) + if type_name is None: + return True + return self.name is None or py_ident(type_name) == py_ident(self.name) + + def check(self, value: Any, name: str = "value") -> None: + """Raise ``TypeError`` if ``value`` does not match this type.""" + if not self.matches(value): + raise TypeError( + f"{name}: expected a value of Lean type `{self.short()}` " + f"(Python {self.python_annotation()}), got {type(value).__name__} {value!r}" + ) + @dataclass(frozen=True) class CtorInfo: diff --git a/lean_py/stubgen.py b/lean_py/stubgen.py new file mode 100644 index 0000000..48561d7 --- /dev/null +++ b/lean_py/stubgen.py @@ -0,0 +1,229 @@ +"""Generate ``.pyi`` type stubs for a Lean library's Python surface. + +A :class:`~lean_py.library.LeanLibrary` exposes its ``@[python]`` functions and +``derive_python`` types as dynamic attributes, so editors and type-checkers see +only ``Any``. This module turns the runtime registry (the same +``TypeRepr``/``FuncInfo``/``TypeInfo`` data that drives marshalling) into a +static stub, so the marshaller and the type hints share one source of truth. + +Usage:: + + from lean_py import LeanLibrary + lib = LeanLibrary.from_lake("path/to/project", "MyLib", build=True) + lib.write_stub("MyLib.pyi") # or + print(generate_stub(lib.registry, "MyLib")) + +or from the command line:: + + python -m lean_py.stubgen path/to/project MyLib -o MyLib.pyi + +The generated stub declares a ``Library`` subclass of ``LeanLibrary`` with +typed methods and typed constructor attributes, plus one class per derived +type. Annotate the ``from_lake`` result with it to get completion and checks:: + + lib: MyLibLibrary = LeanLibrary.from_lake(...) # type: ignore[assignment] +""" + +from __future__ import annotations + +from typing import TYPE_CHECKING + +from lean_py.registry import ( + LibraryRegistry, + TypeInfo, + TypeRepr, + py_ident, +) + +if TYPE_CHECKING: + from lean_py.library import LeanLibrary + + +_HEADER = ( + "# Auto-generated by `python -m lean_py.stubgen`. Do not edit by hand.\n" + "# Regenerate after changing the Lean library's `@[python]` surface.\n" +) + + +# `_safe_ident` sanitises an already-short name; `py_ident` does the same but +# also strips a dotted prefix. Type/constructor/function names use `py_ident`. +def _safe_ident(name: str) -> str: + return py_ident(name) + + +def _annotation(t: TypeRepr, known_types: set[str], named_prefix: str = "") -> str: + """Render a ``TypeRepr`` as a Python annotation string. + + Delegates to :meth:`TypeRepr.python_annotation` — the canonical mapping that + also backs runtime argument validation — so the static hints and the + runtime predicate can never drift. + + ``known_types`` is the set of short class names the stub defines; a ``named`` + reference resolves to ``named_prefix + short`` when known, else ``Any``. The + prefix lets the library class reference module-scope type classes through + aliases without its constructor attributes shadowing them. + """ + return t.python_annotation(known_types, named_prefix) + + +def _params(fields: tuple[TypeRepr, ...], known_types: set[str], named_prefix: str = "") -> str: + """Positional-only parameter list. The registry carries types but not + names, so parameters are named ``a0, a1, ...`` and marked positional-only + (``/``), matching the runtime wrappers, which reject keyword arguments.""" + if not fields: + return "" + parts = [f"a{i}: {_annotation(f, known_types, named_prefix)}" for i, f in enumerate(fields)] + return ", ".join(parts) + ", /" + + +# Prefix for the module-level aliases the library class uses to reference type +# classes without its constructor attributes shadowing them. +_ALIAS = "_ty_" + + +def _emit_type(ti: TypeInfo, known_types: set[str]) -> list[str]: + """Emit a module-scope class for a derived type. + + Type classes live at module scope so their fields can reference sibling and + recursive types by their natural names (Python class bodies are not + enclosing scopes, so nested classes could not see each other). + + Single-constructor structures are callable directly (``Point(x, y)``), so + the class gets an ``__init__``. Multi-constructor inductives expose each + constructor as a nested callable class (``Shape.circle(r)``), matching the + ``_InductiveType`` namespace built at load time. + """ + lines: list[str] = [] + cls_name = _safe_ident(ti.name) + doc = f'"""Lean type ``{ti.name}``. Values are ``LeanInductiveValue``s."""' + + if len(ti.ctors) == 1 and not ti.isEnum: + ctor = ti.ctors[0] + params = _params(ctor.fields, known_types) + lines.append(f"class {cls_name}(LeanInductiveValue):") + lines.append(f" {doc}") + lines.append(f" def __init__(self{', ' + params if params else ''}) -> None: ...") + return lines + + lines.append(f"class {cls_name}:") + lines.append(f" {doc}") + for ctor in ti.ctors: + ctor_name = _safe_ident(ctor.name) + if ctor.fields: + params = _params(ctor.fields, known_types) + lines.append(f" class {ctor_name}(LeanInductiveValue):") + lines.append(f" def __init__(self, {params}) -> None: ...") + else: + # Nullary constructor: usable as a value (`Color.red`) and in + # `isinstance`/pattern matching. + lines.append(f" class {ctor_name}(LeanInductiveValue): ...") + return lines + + +def generate_stub(registry: LibraryRegistry, library_name: str) -> str: + """Return the text of a ``.pyi`` stub for ``registry``.""" + type_names = [_safe_ident(ti.name) for ti in registry.types] + known_types = set(type_names) + + out: list[str] = [_HEADER] + out.append("from typing import Any") + out.append("") + out.append("from lean_py.library import LeanLibrary") + out.append("from lean_py.marshal import LeanInductiveValue") + out.append("") + out.append("") + + # Module-scope type classes (natural names, resolvable everywhere). + for ti in registry.types: + out.extend(_emit_type(ti, known_types)) + out.append("") + out.append("") + + # Aliases so the library class can name types without its constructor + # attributes (`Point: type[_ty_Point]`) shadowing the classes. + if type_names: + for tname in type_names: + out.append(f"{_ALIAS}{tname} = {tname}") + out.append("") + out.append("") + + cls_name = _safe_ident(library_name) + "Library" + out.append(f"class {cls_name}(LeanLibrary):") + out.append(f' """Typed view of the ``{library_name}`` Lean library.') + out.append("") + out.append(" Annotate the ``from_lake`` result with this class to get") + out.append(" completion and type-checking for the library's surface::") + out.append("") + out.append(f" lib: {cls_name} = LeanLibrary.from_lake(...) # type: ignore[assignment]") + out.append(' """') + out.append("") + + body: list[str] = [] + + # Constructor attributes: `lib.Point`, `lib.Shape`, ... typed via aliases. + for tname in type_names: + body.append(f" {tname}: type[{_ALIAS}{tname}]") + + # Functions. Deduplicate by the short name we actually attribute onto the + # instance (`declName`'s last segment), preferring the first occurrence. + seen: set[str] = set() + for fi in registry.funcs: + name = _safe_ident(fi.declName) + if name in seen: + continue + seen.add(name) + params = _params(fi.params, known_types, named_prefix=_ALIAS) + ret = _annotation(fi.returnType, known_types, named_prefix=_ALIAS) + sig = f"self{', ' + params if params else ''}" + body.append(f" def {name}({sig}) -> {ret}: ...") + + if not any(line.strip() for line in body): + body.append(" pass") + out.extend(body) + out.append("") + + return "\n".join(out) + + +def generate_stub_for_library(lib: LeanLibrary) -> str: + """Convenience wrapper: build a stub from a loaded library.""" + return generate_stub(lib.registry, lib.name) + + +def _main(argv: list[str] | None = None) -> int: + import argparse + + from lean_py.library import LeanLibrary + + parser = argparse.ArgumentParser( + prog="python -m lean_py.stubgen", + description="Generate a .pyi stub for a Lean library's Python surface.", + ) + parser.add_argument("lake_dir", help="Path to the Lake project directory.") + parser.add_argument("library_name", help="Lean library name (e.g. MyLib).") + parser.add_argument( + "-o", + "--output", + default=None, + help="Output path (default: .pyi in the current dir).", + ) + parser.add_argument( + "--no-build", + action="store_true", + help="Do not run `lake build` before loading the library.", + ) + args = parser.parse_args(argv) + + lib = LeanLibrary.from_lake(args.lake_dir, args.library_name, build=not args.no_build) + stub = generate_stub_for_library(lib) + out_path = args.output or f"{args.library_name}.pyi" + with open(out_path, "w", encoding="utf-8") as fh: + fh.write(stub) + print( + f"Wrote {out_path} ({len(lib.registry.funcs)} functions, {len(lib.registry.types)} types)." + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(_main()) diff --git a/lean_py/utils.py b/lean_py/utils.py index a35786e..1849683 100644 --- a/lean_py/utils.py +++ b/lean_py/utils.py @@ -44,8 +44,22 @@ def lean_prefix() -> Path: return Path(run_command(["lean", "--print-prefix"])) +def bundle_dir() -> Path | None: + """Directory of a self-contained library bundle, if one is active. + + When ``LEANPY_BUNDLE_DIR`` is set (e.g. by a wheel-installed library's + loader), the Lean runtime shared libraries and the user dylib have been + vendored and relocated there, so we can resolve everything without an + installed toolchain. See :mod:`lean_py.packaging`. + """ + d = os.environ.get("LEANPY_BUNDLE_DIR") + return Path(d) if d else None + + def lean_lib_dir() -> Path: """Where Lean's own shared libraries live.""" + if b := bundle_dir(): + return b return lean_prefix() / "lib" / "lean" @@ -75,6 +89,9 @@ def find_lean_dynlib() -> Path: lib = lean_lib_dir() / f"libleanshared{ext}" if lib.exists(): return lib + if bundle_dir(): + # In a bundle we must not fall through to a toolchain lookup. + raise RuntimeError(f"libleanshared{ext} not found in bundle {lean_lib_dir()}") # Fallback: scan LEAN_PATH (less reliable, retained for back-compat). try: out = run_command(["lake", "env", "printenv", "LEAN_PATH"]) diff --git a/tests/test_ffi.py b/tests/test_ffi.py index 38cffa0..e6a5d47 100644 --- a/tests/test_ffi.py +++ b/tests/test_ffi.py @@ -1,7 +1,16 @@ import ctypes from lean_py.lean_ffi import LeanFFI, get_lean_ffi -from lean_py.lean_types import LeanString + + +def _lean_string_to_py(ffi, ptr) -> str: + """Decode a Lean string object into a Python str via the safe ffi path.""" + size = ffi.lean_string_size(ptr) + if size <= 1: + return "" + cstr = ffi.lean_string_cstr(ptr) + raw = cstr.value if isinstance(cstr, ctypes.c_char_p) else cstr + return (raw or b"").decode("utf-8") def test_ffi_can_be_created(): @@ -17,5 +26,7 @@ def test_ffi_has_initialised(): def test_lean_string_wrap(): ffi = get_lean_ffi() kiran_str = ffi.mk_string("kiran") - obj = LeanString(kiran_str) - assert str(obj) == "kiran" + try: + assert _lean_string_to_py(ffi, kiran_str) == "kiran" + finally: + ffi.lean_dec(kiran_str) diff --git a/tests/test_packaging.py b/tests/test_packaging.py new file mode 100644 index 0000000..898cfcb --- /dev/null +++ b/tests/test_packaging.py @@ -0,0 +1,131 @@ +"""Tests for the self-contained bundler / wheel builder (`lean_py.packaging`). + +The key guarantee: a bundled library loads and runs with **no Lean toolchain** +on PATH (no elan, no `DYLD_LIBRARY_PATH`). We prove it by relocating the dylib +closure and then loading it from a subprocess whose environment has the +toolchain stripped out. +""" + +import subprocess +import sys +import zipfile +from pathlib import Path + +import pytest + +from lean_py.library import LeanLibrary +from lean_py.packaging import build_wheel, bundle_native_libs + +TESTLEAN = Path(__file__).parent / "lean" + +pytestmark = pytest.mark.skipif( + not (sys.platform == "darwin" or sys.platform.startswith("linux")), + reason="bundling is only supported on macOS and Linux", +) + + +def _toolchainless_env(bundle_dir: Path) -> dict: + """A subprocess env with the Lean toolchain removed, pointing only at the + vendored bundle.""" + import os + + env = dict(os.environ) + # Drop elan / toolchain dirs from PATH. + env["PATH"] = ":".join(p for p in env.get("PATH", "").split(":") if ".elan" not in p and p) + for var in ("DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH", "LEANPY_LIBLEAN"): + env.pop(var, None) + env["LEANPY_BUNDLE_DIR"] = str(bundle_dir) + return env + + +def test_bundle_loads_and_runs_without_toolchain(tmp_path): + lib = LeanLibrary.from_lake(TESTLEAN, "TestLib", build=True) + bundle = bundle_native_libs(Path(lib.path), "TestLib", tmp_path / "_lean_libs") + + # lean.h and libleanshared must be vendored for a toolchain-less load. + assert (bundle.dir / "lean.h").exists() + assert list(bundle.dir.glob("libleanshared*")) + + prog = f""" +from lean_py.library import LeanLibrary +from lean_py.utils import add_lean_lib_to_dyld_path +add_lean_lib_to_dyld_path() +lib = LeanLibrary(r"{bundle.main_lib}", "TestLib") +assert lib.bar(21) == 22, lib.bar(21) +assert lib.sumList([1, 2, 3, 4, 5]) == 15, lib.sumList([1, 2, 3, 4, 5]) +print("STANDALONE_OK") +""" + res = subprocess.run( + [sys.executable, "-c", prog], + env=_toolchainless_env(bundle.dir), + capture_output=True, + text=True, + ) + assert "STANDALONE_OK" in res.stdout, ( + f"standalone load failed\nstdout:\n{res.stdout}\nstderr:\n{res.stderr}" + ) + + +def test_build_wheel_structure(tmp_path): + wheel = build_wheel( + TESTLEAN, + "TestLib", + version="0.1.0", + out_dir=tmp_path, + package_name="testlib_bundled", + build=True, + ) + assert wheel.exists() + assert wheel.suffix == ".whl" + assert wheel.name.startswith("testlib_bundled-0.1.0-py3-none-") + + with zipfile.ZipFile(wheel) as zf: + names = zf.namelist() + # Loader package + vendored libs + metadata. + assert "testlib_bundled/__init__.py" in names + assert any(n.endswith("lean.h") for n in names) + assert any("_lean_libs/libleanshared" in n for n in names) + assert any(n.endswith(".dist-info/WHEEL") for n in names) + assert any(n.endswith(".dist-info/RECORD") for n in names) + + +def test_installed_wheel_loads_without_toolchain(tmp_path): + """Extract the built wheel into a throwaway dir and load it through the + generated loader, with the toolchain stripped from the environment. + + (Extraction rather than ``pip install`` because the loader package + its + ``_lean_libs`` land at import-root either way, and uv venvs often ship no + pip.)""" + import os + + wheel = build_wheel( + TESTLEAN, + "TestLib", + version="0.1.0", + out_dir=tmp_path, + package_name="testlib_bundled", + build=True, + ) + target = tmp_path / "site" + with zipfile.ZipFile(wheel) as zf: + zf.extractall(target) + + libs_dir = target / "testlib_bundled" / "_lean_libs" + prog = """ +from testlib_bundled import load +lib = load() +assert lib.bar(41) == 42, lib.bar(41) +assert lib.powInt(2, 10) == 1024, lib.powInt(2, 10) +print("WHEEL_OK") +""" + env = _toolchainless_env(libs_dir) + env["PYTHONPATH"] = str(target) + os.pathsep + env.get("PYTHONPATH", "") + res = subprocess.run( + [sys.executable, "-c", prog], + env=env, + capture_output=True, + text=True, + ) + assert "WHEEL_OK" in res.stdout, ( + f"installed-wheel load failed\nstdout:\n{res.stdout}\nstderr:\n{res.stderr}" + ) diff --git a/tests/test_python_in_lean_threads.py b/tests/test_python_in_lean_threads.py new file mode 100644 index 0000000..927c239 --- /dev/null +++ b/tests/test_python_in_lean_threads.py @@ -0,0 +1,50 @@ +"""Concurrency hardening tests for the Python-in-Lean bridge. + +The C bridge (`LeanPy/native/python_bridge.c`) acquires the GIL defensively +via `WITH_GIL()` around every entry point that touches the CPython C API. +`LeanLibrary` also loads the bridge with ctypes `PyDLL`, so the GIL is held +across the Lean call in the common path. These tests hammer the Python-in-Lean +entry points from many Python threads at once to guard against a regression +that drops the GIL handling (which would surface as a crash, deadlock, or +corrupted refcounts under load). +""" + +from concurrent.futures import ThreadPoolExecutor + +import pytest + + +def test_python_eval_int_concurrent(example_lib): + """Many threads evaluating Python expressions through Lean concurrently.""" + + def work(i: int) -> int: + return example_lib.pythonEvalInt(f"{i} * {i}") + + n = 200 + with ThreadPoolExecutor(max_workers=16) as pool: + results = list(pool.map(work, range(n))) + assert results == [i * i for i in range(n)] + + +def test_python_call_and_str_concurrent(example_lib): + """Mix of C-API entry points (call, eval, str) hit from many threads.""" + + def work(i: int): + assert example_lib.pythonCall1Int("operator", "neg", i) == -i + assert example_lib.pythonEvalStr(f"str({i}) + '!'") == f"{i}!" + return True + + with ThreadPoolExecutor(max_workers=16) as pool: + assert all(pool.map(work, range(200))) + + +def test_python_eval_errors_concurrent(example_lib): + """Errors raised inside Lean callbacks stay isolated across threads.""" + + def work(i: int) -> bool: + with pytest.raises(RuntimeError): + example_lib.pythonEvalInt("undefined_name") + return True + + with ThreadPoolExecutor(max_workers=8) as pool: + assert all(pool.map(work, range(64))) diff --git a/tests/test_stubgen.py b/tests/test_stubgen.py new file mode 100644 index 0000000..ffd4a4e --- /dev/null +++ b/tests/test_stubgen.py @@ -0,0 +1,140 @@ +"""Tests for the `.pyi` stub generator (`lean_py.stubgen`).""" + +import ast + +from lean_py.registry import ( + CtorInfo, + FuncInfo, + LibraryRegistry, + TypeInfo, + TypeRepr, +) +from lean_py.stubgen import _annotation, generate_stub + + +def _t(kind, **kw): + return TypeRepr(kind=kind, **kw) + + +# --- pure type-mapping unit tests (no Lean build required) ---------------- + + +def test_annotation_scalars(): + known: set[str] = set() + assert _annotation(_t("unit"), known) == "None" + assert _annotation(_t("bool"), known) == "bool" + assert _annotation(_t("nat"), known) == "int" + assert _annotation(_t("int"), known) == "int" + assert _annotation(_t("uint", bits=8), known) == "int" + assert _annotation(_t("float"), known) == "float" + assert _annotation(_t("float32"), known) == "float" + assert _annotation(_t("char"), known) == "str" + assert _annotation(_t("string"), known) == "str" + assert _annotation(_t("pyobject"), known) == "Any" + + +def test_annotation_containers(): + known: set[str] = set() + assert _annotation(_t("list", elem=_t("int")), known) == "list[int]" + assert _annotation(_t("array", elem=_t("string")), known) == "list[str]" + assert _annotation(_t("option", elem=_t("bool")), known) == "bool | None" + assert _annotation(_t("prod", a=_t("int"), b=_t("string")), known) == "tuple[int, str]" + assert _annotation(_t("sum", a=_t("int"), b=_t("bool")), known) == "int | bool" + + +def test_annotation_io_and_except_unwrap(): + known: set[str] = set() + assert _annotation(_t("io", elem=_t("int")), known) == "int" + assert _annotation(_t("io", elem=_t("unit")), known) == "None" + assert _annotation(_t("except", e=_t("string"), a=_t("bool")), known) == "bool" + + +def test_annotation_named_resolution(): + # A named type that the stub defines resolves to its class; otherwise Any. + assert _annotation(_t("named", name="My.Point"), {"Point"}) == "Point" + assert _annotation(_t("named", name="Lean.Expr"), set()) == "Any" + assert _annotation(_t("opaque", name="Foo.Bar"), set()) == "Any" + + +# --- end-to-end generation over a synthetic registry ---------------------- + + +def _sample_registry() -> LibraryRegistry: + point = TypeInfo( + name="Demo.Point", + isStructure=True, + isEnum=False, + ctors=(CtorInfo(name="mk", tag=0, fields=(_t("int"), _t("int"))),), + ) + color = TypeInfo( + name="Demo.Color", + isStructure=False, + isEnum=True, + ctors=( + CtorInfo(name="red", tag=0, fields=()), + CtorInfo(name="green", tag=1, fields=()), + ), + ) + shape = TypeInfo( + name="Demo.Shape", + isStructure=False, + isEnum=False, + ctors=( + CtorInfo(name="circle", tag=0, fields=(_t("float"),)), + CtorInfo(name="rect", tag=1, fields=(_t("float"), _t("float"))), + ), + ) + add = FuncInfo( + declName="Demo.add", + exportName="demo_add", + params=(_t("int"), _t("int")), + returnType=_t("int"), + ) + origin = FuncInfo( + declName="Demo.origin", + exportName="demo_origin", + params=(_t("unit"),), + returnType=_t("io", elem=_t("named", name="Demo.Point")), + ) + return LibraryRegistry(funcs=(add, origin), types=(point, color, shape)) + + +def test_generate_stub_is_valid_python(): + stub = generate_stub(_sample_registry(), "Demo") + ast.parse(stub) # raises on syntax error + + +def test_generate_stub_contents(): + stub = generate_stub(_sample_registry(), "Demo") + # Structure: callable directly. + assert "class Point(LeanInductiveValue):" in stub + assert "def __init__(self, a0: int, a1: int, /) -> None: ..." in stub + # Enum + inductive constructors. + assert "class Color:" in stub + assert "class red(LeanInductiveValue): ..." in stub + assert "class circle(LeanInductiveValue):" in stub + # Library class with typed methods and named-type resolution (via alias). + assert "class DemoLibrary(LeanLibrary):" in stub + assert "def add(self, a0: int, a1: int, /) -> int: ..." in stub + assert "def origin(self, a0: None, /) -> _ty_Point: ..." in stub + # Type classes live at module scope (column 0) so recursive/sibling refs + # resolve; the library class references them through aliases. + assert "\nclass Point(LeanInductiveValue):" in stub + assert "_ty_Point = Point" in stub + assert "Point: type[_ty_Point]" in stub + + +def test_generate_stub_empty_registry(): + stub = generate_stub(LibraryRegistry(), "Empty") + ast.parse(stub) + assert "class EmptyLibrary(LeanLibrary):" in stub + assert " pass" in stub + + +def test_write_stub_roundtrip(tmp_path): + from lean_py import stubgen # noqa: F401 — ensure importable + + stub = generate_stub(_sample_registry(), "Demo") + out = tmp_path / "Demo.pyi" + out.write_text(stub) + ast.parse(out.read_text()) diff --git a/tests/test_typerepr.py b/tests/test_typerepr.py new file mode 100644 index 0000000..72982e1 --- /dev/null +++ b/tests/test_typerepr.py @@ -0,0 +1,103 @@ +"""Tests for the unified `TypeRepr` interpretation: one representation drives +the static annotation *and* the runtime value predicate.""" + +import pytest + +from lean_py.registry import TypeRepr + + +def _t(kind, **kw): + return TypeRepr(kind=kind, **kw) + + +# --- static annotation (shared with the stub generator) ------------------- + + +def test_python_annotation_matches_stub_mapping(): + assert _t("unit").python_annotation() == "None" + assert _t("nat").python_annotation() == "int" + assert _t("char").python_annotation() == "str" + assert _t("list", elem=_t("int")).python_annotation() == "list[int]" + assert _t("option", elem=_t("string")).python_annotation() == "str | None" + assert _t("prod", a=_t("int"), b=_t("bool")).python_annotation() == "tuple[int, bool]" + assert _t("io", elem=_t("unit")).python_annotation() == "None" + # named resolution honours known_types + prefix. + named = _t("named", name="My.Point") + assert named.python_annotation({"Point"}, "_ty_") == "_ty_Point" + assert named.python_annotation(set()) == "Any" + assert named.python_annotation() == "Point" # None => assume present + + +# --- runtime predicate ---------------------------------------------------- + + +def test_matches_scalars(): + assert _t("unit").matches(None) + assert not _t("unit").matches(0) + assert _t("bool").matches(True) + assert not _t("bool").matches(1) # bool is not an int here + assert _t("int").matches(5) + assert not _t("int").matches(True) # and int is not a bool + assert _t("nat").matches(0) + assert not _t("nat").matches(-1) + assert _t("float").matches(3) + assert _t("float").matches(3.5) + assert _t("char").matches("a") + assert not _t("char").matches("ab") + assert _t("string").matches("hello") + assert not _t("string").matches(5) + assert _t("pyobject").matches(object()) # accepts anything + + +def test_matches_containers(): + assert _t("list", elem=_t("int")).matches([1, 2, 3]) + assert not _t("list", elem=_t("int")).matches([1, "x"]) + assert not _t("list", elem=_t("int")).matches(5) + assert _t("option", elem=_t("int")).matches(None) + assert _t("option", elem=_t("int")).matches(7) + assert not _t("option", elem=_t("int")).matches("x") + prod = _t("prod", a=_t("int"), b=_t("string")) + assert prod.matches((1, "a")) + assert not prod.matches((1, 2)) + assert not prod.matches((1,)) + + +def test_matches_named_by_identity(): + class FakeInductive: + _type_name = "Demo.Shape" + + shape = _t("named", name="Demo.Shape") + point = _t("named", name="Demo.Point") + assert shape.matches(FakeInductive()) + assert not point.matches(FakeInductive()) + # A value with no Lean identity is accepted leniently (tuple spellings etc). + assert shape.matches(("circle", 5)) + + +def test_check_raises_with_helpful_message(): + with pytest.raises(TypeError) as exc: + _t("int").check("not an int", name="x") + msg = str(exc.value) + assert "x" in msg and "Int" in msg and "str" in msg + # No error on a match. + _t("int").check(5, name="x") + + +# --- opt-in end-to-end validation through a real library ------------------ + + +def test_argument_typechecking_toggle(example_lib): + from lean_py import set_argument_typechecking + + # bar : Int -> Int + assert example_lib.bar(21) == 22 + set_argument_typechecking(True) + try: + with pytest.raises(TypeError): + example_lib.bar("not an int") + # A valid call still works with checking on. + assert example_lib.bar(41) == 42 + finally: + set_argument_typechecking(False) + # With checking off again, the marshaller's own error path handles it. + assert example_lib.bar(1) == 2