From cf949794dc8e42474963b3aa87aced09c9fab492 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Fri, 22 May 2026 10:06:44 -0400 Subject: [PATCH] Fix pip install; ManagedProject falls back to git dep when not in a dev checkout ManagedProject assumed _LEANPY_ROOT always pointed at the repo root with lakefile.lean present. When installed via pip, that path resolves to site-packages and lake build fails. The managed project now detects whether the Lean source tree is local (editable install or checkout) and switches to a git-based Lake require otherwise, keyed to the package version tag. LEANPY_GIT_REV overrides the rev if needed. Moved all in-function imports to toplevel. The one circular dependency (core.py needs _register_inductive from solver.py, solver.py imports from core.py) is broken by extracting _inductive_reg.py as a small bridge module. Removed unused imports and variables flagged by ruff. --- lean_py/_parse.py | 59 ++++++-- lean_py/_runtime.py | 91 +++++++++--- lean_py/base_types.py | 2 +- lean_py/exceptions.py | 5 +- lean_py/kernel.py | 72 +++++---- lean_py/lean_types.py | 19 +-- lean_py/library.py | 65 ++++---- lean_py/marshal.py | 280 +++++++++++++++++++++++++---------- lean_py/project.py | 75 ++++++---- lean_py/registry.py | 18 ++- lean_py/utils.py | 4 +- lean_py/z3/_inductive_reg.py | 34 +++++ lean_py/z3/core.py | 3 +- lean_py/z3/solver.py | 41 +---- 14 files changed, 517 insertions(+), 251 deletions(-) create mode 100644 lean_py/z3/_inductive_reg.py diff --git a/lean_py/_parse.py b/lean_py/_parse.py index 20a5f03..fcc3a41 100644 --- a/lean_py/_parse.py +++ b/lean_py/_parse.py @@ -17,6 +17,7 @@ # Data model # ============================================================================ + @dataclass class StructField: name: str @@ -64,6 +65,7 @@ class HeaderModel: # Header location # ============================================================================ + def find_lean_header() -> Path: """Locate lean.h via the active Lean toolchain. @@ -76,9 +78,7 @@ def find_lean_header() -> Path: `lean-toolchain` file, for callers who don't have `lean` on PATH. """ try: - prefix = subprocess.check_output( - ["lean", "--print-prefix"], text=True - ).strip() + prefix = subprocess.check_output(["lean", "--print-prefix"], text=True).strip() header = Path(prefix) / "include" / "lean" / "lean.h" if header.exists(): return header @@ -89,7 +89,15 @@ def find_lean_header() -> Path: if toolchain_file.exists(): toolchain = toolchain_file.read_text().strip() toolchain_dir = toolchain.replace("/", "--").replace(":", "---") - header = Path.home() / ".elan" / "toolchains" / toolchain_dir / "include" / "lean" / "lean.h" + header = ( + Path.home() + / ".elan" + / "toolchains" + / toolchain_dir + / "include" + / "lean" + / "lean.h" + ) if header.exists(): return header @@ -102,6 +110,7 @@ def find_lean_header() -> Path: # Extraction # ============================================================================ + def extract_defines(header_path: Path) -> dict[str, int]: """Extract integer #define constants from raw header.""" text = header_path.read_text() @@ -122,7 +131,8 @@ def _preprocess(header_path: Path) -> Path: # -D flags strip GCC/Clang constructs that pycparser can't handle result = subprocess.run( [ - "cc", "-E", + "cc", + "-E", "-D__STDC_VERSION__=201112L", "-DNDEBUG", "-D__attribute__(x)=", @@ -143,7 +153,8 @@ def _preprocess(header_path: Path) -> Path: f"-I{include_dir}", str(header_path), ], - capture_output=True, text=True, + capture_output=True, + text=True, ) if result.returncode != 0: raise RuntimeError(f"C preprocessor failed: {result.stderr}") @@ -182,6 +193,7 @@ def _preprocess(header_path: Path) -> Path: # AST helpers # ============================================================================ + def _type_to_str(node) -> str: if node is None: return "void" @@ -223,7 +235,9 @@ def _extract_struct(node: c_ast.Struct) -> StructDef | None: bitfield = None if decl.bitsize and isinstance(decl.bitsize, c_ast.Constant): bitfield = int(decl.bitsize.value) - fields.append(StructField(name=fname, c_type=ftype, is_pointer=is_ptr, bitfield=bitfield)) + fields.append( + StructField(name=fname, c_type=ftype, is_pointer=is_ptr, bitfield=bitfield) + ) return StructDef(name=node.name or "", fields=fields) @@ -258,7 +272,9 @@ def _extract_export_names(header_path: Path) -> set[str]: def _extract_inline_names(header_path: Path) -> set[str]: text = header_path.read_text() - pattern = re.compile(r"static\s+inline\s+(?:LEAN_ALWAYS_INLINE\s+)?[\w\s*]+\s+(\w+)\s*\(") + pattern = re.compile( + r"static\s+inline\s+(?:LEAN_ALWAYS_INLINE\s+)?[\w\s*]+\s+(\w+)\s*\(" + ) return {m.group(1) for m in pattern.finditer(text)} @@ -266,7 +282,10 @@ def _extract_inline_names(header_path: Path) -> set[str]: # Classification # ============================================================================ -def _classify(ast: c_ast.FileAST, defines: dict[str, int], header_path: Path) -> HeaderModel: + +def _classify( + ast: c_ast.FileAST, defines: dict[str, int], header_path: Path +) -> HeaderModel: model = HeaderModel() model.constants = defines @@ -275,14 +294,18 @@ def _classify(ast: c_ast.FileAST, defines: dict[str, int], header_path: Path) -> for node in ast.ext: if isinstance(node, c_ast.Typedef): - if isinstance(node.type, c_ast.TypeDecl) and isinstance(node.type.type, c_ast.Struct): + if isinstance(node.type, c_ast.TypeDecl) and isinstance( + node.type.type, c_ast.Struct + ): struct = _extract_struct(node.type.type) if struct: struct.name = node.name model.structs.append(struct) continue typedef_type = _decl_type_to_str(node.type) - model.typedefs.append(TypedefDef(name=node.name, underlying_type=typedef_type)) + model.typedefs.append( + TypedefDef(name=node.name, underlying_type=typedef_type) + ) elif isinstance(node, c_ast.Decl): if isinstance(node.type, c_ast.FuncDecl): @@ -290,7 +313,12 @@ def _classify(ast: c_ast.FileAST, defines: dict[str, int], header_path: Path) -> ret_type = _decl_type_to_str(func_decl.type) params, is_variadic = _extract_func_params(func_decl) fname = node.name or "" - func = FuncDecl(name=fname, return_type=ret_type, params=params, is_variadic=is_variadic) + func = FuncDecl( + name=fname, + return_type=ret_type, + params=params, + is_variadic=is_variadic, + ) if fname in export_names: model.exported_functions.append(func) elif fname in inline_names: @@ -303,7 +331,12 @@ def _classify(ast: c_ast.FileAST, defines: dict[str, int], header_path: Path) -> ret_type = _decl_type_to_str(func_decl.type) params, is_variadic = _extract_func_params(func_decl) fname = decl.name or "" - func = FuncDecl(name=fname, return_type=ret_type, params=params, is_variadic=is_variadic) + func = FuncDecl( + name=fname, + return_type=ret_type, + params=params, + is_variadic=is_variadic, + ) if fname in inline_names: model.inline_functions.append(func) elif fname in export_names: diff --git a/lean_py/_runtime.py b/lean_py/_runtime.py index 3f67ff2..51b0179 100644 --- a/lean_py/_runtime.py +++ b/lean_py/_runtime.py @@ -9,13 +9,31 @@ import ctypes import functools from ctypes import ( - POINTER, Structure, c_bool, c_char, c_char_p, c_double, c_float, - c_int, c_int8, c_int16, c_int32, c_int64, c_long, c_size_t, - c_ssize_t, c_uint, c_uint8, c_uint16, c_uint32, c_uint64, c_void_p, + POINTER, + Structure, + c_bool, + c_char, + c_char_p, + c_double, + c_float, + c_int, + c_int8, + c_int16, + c_int32, + c_int64, + c_long, + c_size_t, + c_ssize_t, + c_uint, + c_uint8, + c_uint16, + c_uint32, + c_uint64, + c_void_p, ) from typing import Any -from lean_py._parse import HeaderModel, StructDef, FuncDecl, get_header_model +from lean_py._parse import HeaderModel, StructDef, get_header_model from lean_py.utils import all_lean_runtime_libs, find_lean_dynlib @@ -82,8 +100,14 @@ def _resolve_type(c_type: str, structs: dict[str, type]) -> Any: return _TYPE_MAP[c_type] # lean_object pointer types - if c_type in ("lean_object *", "lean_obj_arg", "b_lean_obj_arg", - "u_lean_obj_arg", "lean_obj_res", "b_lean_obj_res"): + if c_type in ( + "lean_object *", + "lean_obj_arg", + "b_lean_obj_arg", + "u_lean_obj_arg", + "lean_obj_res", + "b_lean_obj_res", + ): return structs.get("_LeanObjectPtr", c_void_p) if c_type == "lean_object * *": @@ -91,8 +115,12 @@ def _resolve_type(c_type: str, structs: dict[str, type]) -> Any: return POINTER(obj_ptr) # Known opaque pointer types - if c_type in ("lean_external_class *", "lean_external_finalize_proc", - "lean_external_foreach_proc", "lean_task_imp *"): + if c_type in ( + "lean_external_class *", + "lean_external_finalize_proc", + "lean_external_foreach_proc", + "lean_task_imp *", + ): return c_void_p # Pointer types @@ -121,6 +149,7 @@ def _resolve_type(c_type: str, structs: dict[str, type]) -> Any: # Dynamic struct creation # ============================================================================ + def _build_structs(model: HeaderModel) -> dict[str, type]: """Dynamically create ctypes Structure classes from the model.""" structs: dict[str, type] = {} @@ -168,9 +197,9 @@ def _make_struct(sdef: StructDef, known: dict[str, type]) -> type: # Dynamic FFI class creation # ============================================================================ + def _build_ffi_class(model: HeaderModel, structs: dict[str, type]) -> type: """Dynamically create the LeanFFI class with all bindings.""" - LeanObjectPtr = structs["_LeanObjectPtr"] constants = model.constants def __init__(self): @@ -216,8 +245,9 @@ def __init__(self): # init code can run with the flag still true (which is required # by Lean's `initialize` blocks), then flip it after. try: - self.lean_io_mark_end_initialization = \ + self.lean_io_mark_end_initialization = ( self.lib.lean_io_mark_end_initialization + ) self.lean_io_mark_end_initialization.argtypes = [] self.lean_io_mark_end_initialization.restype = None except AttributeError: @@ -261,7 +291,9 @@ def _bind_exported(self, lib): try: cfunc = getattr(lib, func.name) if func.params: - cfunc.argtypes = [_resolve_type(p.c_type, structs) for p in func.params] + cfunc.argtypes = [ + _resolve_type(p.c_type, structs) for p in func.params + ] restype = _resolve_type(func.return_type, structs) if restype is not None: cfunc.restype = restype @@ -446,7 +478,9 @@ def lean_ctor_get(self, o, i): # pointer that aliases into the Lean ctor's m_objs memory. If the # ctor is later freed (lean_dec), an aliased pointer would become # stale when the Lean allocator reuses the memory. - elem_addr = ctypes.addressof(ctor.contents) + offset + i * ctypes.sizeof(LeanObjectPtr) + elem_addr = ( + ctypes.addressof(ctor.contents) + offset + i * ctypes.sizeof(LeanObjectPtr) + ) raw_val = c_void_p.from_address(elem_addr).value or 0 return ctypes.cast(c_void_p(raw_val), LeanObjectPtr) @@ -538,7 +572,9 @@ def lean_alloc_ctor(self, tag, num_objs, scalar_sz): def lean_alloc_array(self, size, capacity): fn = self._find_leanpy_helper("leanpy_alloc_array") if fn is None: - raise RuntimeError("leanpy_alloc_array not found — leanpy_native not linked") + raise RuntimeError( + "leanpy_alloc_array not found — leanpy_native not linked" + ) fn.argtypes = [c_size_t, c_size_t] fn.restype = LeanObjectPtr return fn(size, capacity) @@ -557,7 +593,8 @@ def lean_box_uint64(self, v): # Use the exported lean_box_uint64 if present. fn = getattr(self.lib, "lean_box_uint64", None) if fn is not None: - fn.argtypes = [c_uint64]; fn.restype = LeanObjectPtr + fn.argtypes = [c_uint64] + fn.restype = LeanObjectPtr return fn(v) # Fallback: scalar tagged pointer (only valid for small values). return self.lean_box(v) @@ -565,7 +602,8 @@ def lean_box_uint64(self, v): def lean_unbox_uint64(self, o): fn = getattr(self.lib, "lean_unbox_uint64", None) if fn is not None: - fn.argtypes = [LeanObjectPtr]; fn.restype = c_uint64 + fn.argtypes = [LeanObjectPtr] + fn.restype = c_uint64 return fn(o) return self.lean_unbox(o) @@ -591,7 +629,8 @@ def lean_unsigned_to_nat(self, n): fn = getattr(self.lib, "lean_unsigned_to_nat", None) if fn is None: return self.lean_box(n) - fn.argtypes = [c_uint]; fn.restype = LeanObjectPtr + fn.argtypes = [c_uint] + fn.restype = LeanObjectPtr return fn(n) def lean_uint64_to_nat(self, n): @@ -602,9 +641,12 @@ def lean_uint64_to_nat(self, n): return self.lean_box(n) big = getattr(self.lib, "lean_big_uint64_to_nat", None) if big is not None: - big.argtypes = [c_uint64]; big.restype = LeanObjectPtr + big.argtypes = [c_uint64] + big.restype = LeanObjectPtr return big(c_uint64(n).value) - raise RuntimeError(f"Cannot convert uint64 {n} to Nat: lean_big_uint64_to_nat not found") + raise RuntimeError( + f"Cannot convert uint64 {n} to Nat: lean_big_uint64_to_nat not found" + ) def lean_uint64_of_nat(self, p): # Inline: small scalar fast-path; large path via lean_uint64_of_big_nat. @@ -613,7 +655,8 @@ def lean_uint64_of_nat(self, p): fn = getattr(self.lib, "lean_uint64_of_big_nat", None) if fn is None: raise RuntimeError("lean_uint64_of_big_nat not found and Nat is not scalar") - fn.argtypes = [LeanObjectPtr]; fn.restype = c_uint64 + fn.argtypes = [LeanObjectPtr] + fn.restype = c_uint64 return int(fn(p)) def lean_int64_to_int(self, n): @@ -621,7 +664,8 @@ def lean_int64_to_int(self, n): # to the static-inline `lean_int64_to_int` exactly. fn = self._find_leanpy_helper("leanpy_int64_to_int") if fn is not None: - fn.argtypes = [c_int64]; fn.restype = LeanObjectPtr + fn.argtypes = [c_int64] + fn.restype = LeanObjectPtr return fn(n) # Fallback (mirrors `lean.h`): encode int32-range as a scalar. if -(1 << 31) <= n <= (1 << 31) - 1: @@ -629,13 +673,15 @@ def lean_int64_to_int(self, n): big = getattr(self.lib, "lean_big_int64_to_int", None) if big is None: return self.lean_box(n & ((1 << 63) - 1)) - big.argtypes = [c_int64]; big.restype = LeanObjectPtr + big.argtypes = [c_int64] + big.restype = LeanObjectPtr return big(n) def lean_int64_of_int(self, p): fn = self._find_leanpy_helper("leanpy_int64_of_int") if fn is not None: - fn.argtypes = [LeanObjectPtr]; fn.restype = c_int64 + fn.argtypes = [LeanObjectPtr] + fn.restype = c_int64 return int(fn(p)) if self.lean_is_scalar(p): return int(self.lean_scalar_to_int(p)) @@ -658,7 +704,6 @@ def lean_scalar_to_int(self, p): def _add_helper_methods(class_dict: dict, structs: dict): """Add convenience helper methods.""" - LeanObjectPtr = structs["_LeanObjectPtr"] def mk_string(self, s): """Create a Lean string from a Python string.""" diff --git a/lean_py/base_types.py b/lean_py/base_types.py index d966889..f5e9d5f 100644 --- a/lean_py/base_types.py +++ b/lean_py/base_types.py @@ -7,7 +7,7 @@ from __future__ import annotations -from ctypes import POINTER, _Pointer +from ctypes import _Pointer from lean_py._runtime import get_structs, get_constants diff --git a/lean_py/exceptions.py b/lean_py/exceptions.py index 7b5776d..4bc7b14 100644 --- a/lean_py/exceptions.py +++ b/lean_py/exceptions.py @@ -39,8 +39,7 @@ class LeanError(RuntimeError): __slots__ = ("kind", "message", "context") - def __init__(self, kind: str, message: str, - context: dict | None = None) -> None: + def __init__(self, kind: str, message: str, context: dict | None = None) -> None: self.kind = kind self.message = message self.context = context or {} @@ -97,7 +96,7 @@ def parse_io_error_message(raw: str) -> tuple[str, str]: return "", raw if not typename[0].isupper(): return "", raw - return typename, raw[sep + 2:] + return typename, raw[sep + 2 :] __all__ = [ diff --git a/lean_py/kernel.py b/lean_py/kernel.py index 069caaf..e3f42e4 100644 --- a/lean_py/kernel.py +++ b/lean_py/kernel.py @@ -52,8 +52,7 @@ def ok(self) -> bool: return self.status == "success" @classmethod - def parse(cls, encoded: str, kernel: "Kernel", - raw_state: Any) -> "TacticResult": + def parse(cls, encoded: str, kernel: "Kernel", raw_state: Any) -> "TacticResult": """Parse the multi-line encoding produced by Lean's ``encodeTacticResult``.""" if not encoded: @@ -97,28 +96,33 @@ def pretty(self) -> str: return self._kernel._lib.leanpy_kernel_goal_pretty(self._handle) def try_tactic(self, tactic: str) -> TacticResult: - encoded, next_state = \ - self._kernel._lib.leanpy_kernel_goal_try_tactic(self._handle, tactic) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_tactic( + self._handle, tactic + ) return TacticResult.parse(encoded, self._kernel, next_state) def try_assign(self, expr: str) -> TacticResult: - encoded, next_state = \ - self._kernel._lib.leanpy_kernel_goal_try_assign(self._handle, expr) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_assign( + self._handle, expr + ) return TacticResult.parse(encoded, self._kernel, next_state) def conv_enter(self) -> TacticResult: - encoded, next_state = \ - self._kernel._lib.leanpy_kernel_goal_conv_enter(self._handle) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_conv_enter( + self._handle + ) return TacticResult.parse(encoded, self._kernel, next_state) def calc_enter(self) -> TacticResult: - encoded, next_state = \ - self._kernel._lib.leanpy_kernel_goal_calc_enter(self._handle) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_calc_enter( + self._handle + ) return TacticResult.parse(encoded, self._kernel, next_state) def fragment_exit(self) -> TacticResult: - encoded, next_state = \ - self._kernel._lib.leanpy_kernel_goal_fragment_exit(self._handle) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_fragment_exit( + self._handle + ) return TacticResult.parse(encoded, self._kernel, next_state) # ---- prograde tactics -------------------------------------------------- @@ -126,21 +130,27 @@ def fragment_exit(self) -> TacticResult: def try_have(self, binder_name: str, type_str: str) -> TacticResult: """Equivalent to ``have : := ?``.""" encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_have( - self._handle, binder_name, type_str, + self._handle, + binder_name, + type_str, ) return TacticResult.parse(encoded, self._kernel, next_state) def try_let(self, binder_name: str, type_str: str) -> TacticResult: """Equivalent to ``let : := ?``.""" encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_let( - self._handle, binder_name, type_str, + self._handle, + binder_name, + type_str, ) return TacticResult.parse(encoded, self._kernel, next_state) def try_define(self, binder_name: str, expr_str: str) -> TacticResult: """Equivalent to ``let := ``.""" encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_define( - self._handle, binder_name, expr_str, + self._handle, + binder_name, + expr_str, ) return TacticResult.parse(encoded, self._kernel, next_state) @@ -148,7 +158,8 @@ def try_draft(self, expr_str: str) -> TacticResult: """Substitute the goal with an expression that may contain sorrys, leaving the sorrys as fresh subgoals.""" encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_draft( - self._handle, expr_str, + self._handle, + expr_str, ) return TacticResult.parse(encoded, self._kernel, next_state) @@ -158,7 +169,9 @@ def goal_names(self) -> list[str]: return list(self._kernel._lib.leanpy_kernel_goal_state_goal_names(self._handle)) def parent_names(self) -> list[str]: - return list(self._kernel._lib.leanpy_kernel_goal_state_parent_names(self._handle)) + return list( + self._kernel._lib.leanpy_kernel_goal_state_parent_names(self._handle) + ) def root_name(self) -> str: return self._kernel._lib.leanpy_kernel_goal_state_root_name(self._handle) @@ -186,7 +199,8 @@ def pickle(self, path: str) -> None: def resume(self, goal_names: list[str]) -> "GoalState": next_state, err = self._kernel._lib.leanpy_kernel_goal_resume( - self._handle, goal_names, + self._handle, + goal_names, ) if err: raise RuntimeError(f"resume failed: {err}") @@ -194,7 +208,8 @@ def resume(self, goal_names: list[str]) -> "GoalState": def continue_with(self, branch: "GoalState") -> "GoalState": next_state, err = self._kernel._lib.leanpy_kernel_goal_continue( - self._handle, branch._handle, + self._handle, + branch._handle, ) if err: raise RuntimeError(f"continue failed: {err}") @@ -203,21 +218,28 @@ def continue_with(self, branch: "GoalState") -> "GoalState": def replay(self, src: "GoalState", src_prime: "GoalState") -> "GoalState": """Merge differential ``src → src_prime`` onto ``self`` (the dst).""" next_state, err = self._kernel._lib.leanpy_kernel_goal_replay( - self._handle, src._handle, src_prime._handle, + self._handle, + src._handle, + src_prime._handle, ) if err: raise RuntimeError(f"replay failed: {err}") return GoalState(self._kernel, next_state) - def subsume(self, goal_name: str, candidate_names: list[str] - ) -> tuple[str, "GoalState | None", str]: + def subsume( + self, goal_name: str, candidate_names: list[str] + ) -> tuple[str, "GoalState | None", str]: """Try to discharge ``goal_name`` using one of ``candidate_names``. Returns (``"none"|"subsumed"|"cycle"|"error"``, optional new state, - optional name of the candidate that subsumed). """ + optional name of the candidate that subsumed).""" label, next_state, sub_name = self._kernel._lib.leanpy_kernel_goal_subsume( - self._handle, goal_name, candidate_names, + self._handle, + goal_name, + candidate_names, + ) + next_gs = ( + GoalState(self._kernel, next_state) if next_state is not None else None ) - next_gs = GoalState(self._kernel, next_state) if next_state is not None else None return label, next_gs, sub_name def __repr__(self) -> str: diff --git a/lean_py/lean_types.py b/lean_py/lean_types.py index 8989fe5..063325b 100644 --- a/lean_py/lean_types.py +++ b/lean_py/lean_types.py @@ -19,13 +19,13 @@ class LeanValue: 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() + self.ffi: LeanFFI = get_lean_ffi() def __del__(self): """Automatically decrement reference when Python object is garbage collected.""" @@ -40,14 +40,14 @@ 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') + return ctypes.string_at(m_data_start, string_obj.m_size - 1).decode("utf-8") def __str__(self): return self.to_python_string() @@ -68,8 +68,10 @@ 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}") - + 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) @@ -99,7 +101,7 @@ def is_error(self): def get_or_raise(self): """ Get the value if Ok, or raise an exception if Error. - + Raises: RuntimeError: If the result is an Error """ @@ -115,4 +117,3 @@ def get_or_raise(self): # 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 d50209b..aea7fce 100644 --- a/lean_py/library.py +++ b/lean_py/library.py @@ -28,6 +28,7 @@ from pathlib import Path from typing import Any, Callable +from lean_py._runtime import get_structs from lean_py.base_types import LeanObject from lean_py.lean_ffi import get_lean_ffi from lean_py.marshal import LeanInductiveValue, Marshaller, TypeWrapper, _CtorMeta @@ -46,7 +47,9 @@ def _list_init_symbols(dylib: Path) -> list[str]: try: out = subprocess.run( ["nm", "-gj", str(dylib)], - capture_output=True, text=True, check=True, + capture_output=True, + text=True, + check=True, ).stdout except (FileNotFoundError, subprocess.CalledProcessError): return [] @@ -56,8 +59,11 @@ def _list_init_symbols(dylib: Path) -> list[str]: # macOS prefixes exported symbols with `_`; strip that. if sym.startswith("_"): sym = sym[1:] - if sym.startswith("initialize_") and "Lean_" not in sym \ - and "LeanPy_" not in sym: + if ( + sym.startswith("initialize_") + and "Lean_" not in sym + and "LeanPy_" not in sym + ): candidates.append(sym) return candidates @@ -77,7 +83,9 @@ def _ensure_rpath(dylib: Path) -> None: try: out = subprocess.run( ["otool", "-L", str(dylib)], - capture_output=True, text=True, check=True, + capture_output=True, + text=True, + check=True, ).stdout except (FileNotFoundError, subprocess.CalledProcessError): return @@ -88,14 +96,15 @@ def _ensure_rpath(dylib: Path) -> None: continue # Form: "@rpath/libFoo.dylib (compatibility version ...)" ref = line.split(" ", 1)[0] - leaf = ref[len("@rpath/"):] + leaf = ref[len("@rpath/") :] candidate = libdir / leaf if not candidate.exists(): continue try: subprocess.run( ["install_name_tool", "-change", ref, str(candidate), str(dylib)], - check=True, capture_output=True, + check=True, + capture_output=True, ) except (FileNotFoundError, subprocess.CalledProcessError): pass @@ -135,14 +144,14 @@ def __init__(self, ti: TypeInfo, marshaller: Marshaller): match_args = tuple(f"_{i}" for i in range(n_fields)) attrs = { - '_ctor_name': ctor.name, - '_type_name': ti.name, - '_tag': ctor.tag, - '__match_args__': match_args, + "_ctor_name": ctor.name, + "_type_name": ti.name, + "_tag": ctor.tag, + "__match_args__": match_args, # Backward compat for nullary ctors used as values: - 'ctor': ctor.name, - 'tag': ctor.tag, - 'fields': (), + "ctor": ctor.name, + "tag": ctor.tag, + "fields": (), } cls = _CtorMeta(ctor.name, (), attrs) setattr(self, ctor.name, cls) @@ -231,14 +240,11 @@ def _ctype_for_call(ct): # If the return is a pointer, we need to cast it back to LeanObjectPtr # before handing it to the unmarshaller. - from lean_py._runtime import get_structs LObjPtr = get_structs()["_LeanObjectPtr"] - return_is_pointer = ( - isinstance(rwrap.ctype, type) - and issubclass(rwrap.ctype, ctypes._Pointer) + return_is_pointer = isinstance(rwrap.ctype, type) and issubclass( + rwrap.ctype, ctypes._Pointer ) - from lean_py.lean_ffi import get_lean_ffi _ffi = get_lean_ffi() def _wrapper(*args): @@ -322,9 +328,9 @@ def _find(name: str) -> Path | None: if not build_root.is_dir(): return None patterns = [ - f"lib{name}{ext}", # old layout - f"lib*_{name}{ext}", # new: lib_. - f"lib{name}_*{ext}", # mirror + f"lib{name}{ext}", # old layout + f"lib*_{name}{ext}", # new: lib_. + f"lib{name}_*{ext}", # mirror ] # Quick path: standard lib_dir, exact name. primary = lib_dir / f"lib{name}{ext}" @@ -354,8 +360,9 @@ def _diagnostic() -> str: # Some Lake versions don't honour `defaultFacets = ["shared"]` # in lakefile.toml; ask for the shared facet explicitly. try: - run_command(["lake", "build", f"{library_name}:shared"], - cwd=lake_path) + run_command( + ["lake", "build", f"{library_name}:shared"], cwd=lake_path + ) except Exception: pass found = _find(library_name) @@ -370,9 +377,9 @@ def _diagnostic() -> str: shared = [] if build_root.is_dir(): shared = [ - p for p in build_root.rglob(f"lib*{ext}") - if p.suffix == ext - and not p.name.endswith((".hash", ".trace", ".rsp")) + p + for p in build_root.rglob(f"lib*{ext}") + if p.suffix == ext and not p.name.endswith((".hash", ".trace", ".rsp")) ] if not shared: raise FileNotFoundError( @@ -418,9 +425,11 @@ def __init__(self, dylib_path: str | os.PathLike, library_name: str): self._types: dict[str, _InductiveType] = {} for ti in self.registry.types: - wrapper = _StructureType(ti, self.marshaller) \ - if len(ti.ctors) == 1 \ + wrapper = ( + _StructureType(ti, self.marshaller) + if len(ti.ctors) == 1 else _InductiveType(ti, self.marshaller) + ) short = ti.name.split(".")[-1] self._types[short] = wrapper setattr(self, short, wrapper) diff --git a/lean_py/marshal.py b/lean_py/marshal.py index 2f8e39f..67ecc10 100644 --- a/lean_py/marshal.py +++ b/lean_py/marshal.py @@ -24,13 +24,23 @@ import ctypes import struct as _struct from ctypes import ( - POINTER, c_char_p, c_double, c_int8, c_int16, c_int32, c_int64, - c_size_t, c_uint8, c_uint16, c_uint32, c_uint64, c_void_p, + c_double, + c_int8, + c_int16, + c_int32, + c_int64, + c_size_t, + c_uint8, + c_uint16, + c_uint32, + c_uint64, + c_void_p, ) from typing import Any, Callable from lean_py._runtime import _ptr_as_int, get_lean_ffi, get_structs -from lean_py.registry import CtorInfo, FuncInfo, LibraryRegistry, TypeInfo, TypeRepr +from lean_py.exceptions import LeanError, LeanPyCallbackError, parse_io_error_message +from lean_py.registry import CtorInfo, LibraryRegistry, TypeInfo, TypeRepr # ============================================================================ @@ -122,8 +132,13 @@ class TypeWrapper: """ __slots__ = ( - "repr", "from_lean", "to_lean", "ctype", - "ctor_scalar_size", "from_ctor_scalar", "to_ctor_scalar", + "repr", + "from_lean", + "to_lean", + "ctype", + "ctor_scalar_size", + "from_ctor_scalar", + "to_ctor_scalar", ) def __init__( @@ -162,6 +177,7 @@ def _is_enum_tag_only(ti: TypeInfo) -> bool: # Wrapper for a registered user inductive (`derive_python`) # ---------------------------------------------------------------------------- + class _CtorMeta(type): """Metaclass for constructor pattern-match classes. @@ -172,26 +188,34 @@ class _CtorMeta(type): """ def __call__(cls, *args): - n_fields = len(cls.__match_args__) if hasattr(cls, '__match_args__') else 0 + n_fields = len(cls.__match_args__) if hasattr(cls, "__match_args__") else 0 if len(args) != n_fields: raise TypeError( f"{cls._type_name}.{cls._ctor_name} expects {n_fields} args, " - f"got {len(args)}") + f"got {len(args)}" + ) # Convert zero-arg _CtorMeta sentinels to LeanInductiveValue so that # all tree nodes are uniformly LeanInductiveValue for pattern matching. converted = tuple( LeanInductiveValue(a._type_name, a._ctor_name, a._tag, ()) - if type(a) is _CtorMeta else a + if type(a) is _CtorMeta + else a for a in args ) return LeanInductiveValue(cls._type_name, cls._ctor_name, cls._tag, converted) def __instancecheck__(cls, instance): if isinstance(instance, LeanInductiveValue): - return instance.ctor == cls._ctor_name and instance._type_name == cls._type_name + return ( + instance.ctor == cls._ctor_name + and instance._type_name == cls._type_name + ) if type(instance) is _CtorMeta: # Allow isinstance(Color.red, Color.red) — both are _CtorMeta classes - return instance._ctor_name == cls._ctor_name and instance._type_name == cls._type_name + return ( + instance._ctor_name == cls._ctor_name + and instance._type_name == cls._type_name + ) return False def __repr__(cls): @@ -199,11 +223,16 @@ def __repr__(cls): def __eq__(cls, other): if isinstance(other, LeanInductiveValue): - return (other._type_name == cls._type_name - and other.ctor == cls._ctor_name - and other.fields == ()) + return ( + other._type_name == cls._type_name + and other.ctor == cls._ctor_name + and other.fields == () + ) if isinstance(other, _CtorMeta): - return cls._type_name == other._type_name and cls._ctor_name == other._ctor_name + return ( + cls._type_name == other._type_name + and cls._ctor_name == other._ctor_name + ) return NotImplemented def __hash__(cls): @@ -244,23 +273,30 @@ def __getattr__(self, name: str) -> Any: if idx < len(self.fields): return self.fields[idx] raise AttributeError( - f"field index {idx} out of range (have {len(self.fields)} fields)") + f"field index {idx} out of range (have {len(self.fields)} fields)" + ) raise AttributeError(name) def __repr__(self) -> str: if not self.fields: return f"{self._type_name}.{self.ctor}" - return f"{self._type_name}.{self.ctor}({', '.join(repr(f) for f in self.fields)})" + return ( + f"{self._type_name}.{self.ctor}({', '.join(repr(f) for f in self.fields)})" + ) def __eq__(self, other: object) -> bool: if isinstance(other, LeanInductiveValue): return (self._type_name, self.tag, self.fields) == ( - other._type_name, other.tag, other.fields, + other._type_name, + other.tag, + other.fields, ) if type(other) is _CtorMeta: - return (self._type_name == other._type_name # type: ignore[attr-defined] - and self.ctor == other._ctor_name # type: ignore[attr-defined] - and self.fields == ()) + return ( + self._type_name == other._type_name # type: ignore[attr-defined] + and self.ctor == other._ctor_name # type: ignore[attr-defined] + and self.fields == () + ) return NotImplemented def __hash__(self) -> int: @@ -313,51 +349,64 @@ def _call(fn, obj_args, ObjPtr): # -- Lean.Name ---------------------------------------------------------- _nmks = _sym("lean_name_mk_string") if _nmks: + def _name_str(ffi, ObjPtr, ch): return _call(_nmks, ch, ObjPtr) + ctors[("Lean.Name", "str")] = _name_str _nmkn = _sym("lean_name_mk_numeral") if _nmkn: + def _name_num(ffi, ObjPtr, ch): return _call(_nmkn, ch, ObjPtr) + ctors[("Lean.Name", "num")] = _name_num # -- Lean.Level --------------------------------------------------------- - _lvl = {n: _sym(n) for n in [ - "lean_level_mk_zero", "lean_level_mk_succ", "lean_level_mk_max", - "lean_level_mk_imax", "lean_level_mk_param", "lean_level_mk_mvar", - ]} + _lvl = { + n: _sym(n) + for n in [ + "lean_level_mk_zero", + "lean_level_mk_succ", + "lean_level_mk_max", + "lean_level_mk_imax", + "lean_level_mk_param", + "lean_level_mk_mvar", + ] + } for cname, sym, nargs in [ ("zero", "lean_level_mk_zero", 0), ("succ", "lean_level_mk_succ", 1), - ("max", "lean_level_mk_max", 2), + ("max", "lean_level_mk_max", 2), ("imax", "lean_level_mk_imax", 2), - ("param","lean_level_mk_param",1), + ("param", "lean_level_mk_param", 1), ("mvar", "lean_level_mk_mvar", 1), ]: fn = _lvl.get(sym) if fn: + def _mk(ffi, ObjPtr, ch, _fn=fn, _n=nargs): return _call(_fn, ch[:_n], ObjPtr) + ctors[("Lean.Level", cname)] = _mk # -- Lean.Expr ---------------------------------------------------------- # BinderInfo / Bool trailing args are passed as uint8 (the unboxed # scalar value), NOT as lean_object*. _expr = { - "bvar": (_sym("lean_expr_mk_bvar"), 1, False), - "fvar": (_sym("lean_expr_mk_fvar"), 1, False), - "mvar": (_sym("lean_expr_mk_mvar"), 1, False), - "sort": (_sym("lean_expr_mk_sort"), 1, False), - "const": (_sym("lean_expr_mk_const"), 2, False), - "app": (_sym("lean_expr_mk_app"), 2, False), - "lam": (_sym("lean_expr_mk_lambda"), 4, True), - "forallE": (_sym("lean_expr_mk_forall"), 4, True), - "letE": (_sym("lean_expr_mk_let"), 5, True), - "lit": (_sym("lean_expr_mk_lit"), 1, False), - "mdata": (_sym("lean_expr_mk_mdata"), 2, False), - "proj": (_sym("lean_expr_mk_proj"), 3, False), + "bvar": (_sym("lean_expr_mk_bvar"), 1, False), + "fvar": (_sym("lean_expr_mk_fvar"), 1, False), + "mvar": (_sym("lean_expr_mk_mvar"), 1, False), + "sort": (_sym("lean_expr_mk_sort"), 1, False), + "const": (_sym("lean_expr_mk_const"), 2, False), + "app": (_sym("lean_expr_mk_app"), 2, False), + "lam": (_sym("lean_expr_mk_lambda"), 4, True), + "forallE": (_sym("lean_expr_mk_forall"), 4, True), + "letE": (_sym("lean_expr_mk_let"), 5, True), + "lit": (_sym("lean_expr_mk_lit"), 1, False), + "mdata": (_sym("lean_expr_mk_mdata"), 2, False), + "proj": (_sym("lean_expr_mk_proj"), 3, False), } for cname, (fn, nargs, scalar_tail) in _expr.items(): if fn is None: @@ -368,14 +417,16 @@ def _mk(ffi, ObjPtr, ch, _fn=fn, _n=nargs, _st=scalar_tail): # type: ignore[mis for i, c in enumerate(ch[:_n]): if _st and i == _n - 1: # Trailing BinderInfo / Bool — unbox to uint8. - c_args.append(ffi.lean_unbox(c) if ffi.lean_is_scalar(c) - else _ptr_as_int(c)) + c_args.append( + ffi.lean_unbox(c) if ffi.lean_is_scalar(c) else _ptr_as_int(c) + ) else: c_args.append(_ptr_as_int(c)) _fn.restype = c_void_p _fn.argtypes = [c_void_p] * len(c_args) raw = _fn(*c_args) return ctypes.cast(c_void_p(raw), ObjPtr) + ctors[("Lean.Expr", cname)] = _mk return ctors @@ -583,7 +634,9 @@ def _encode_inductive(self, ti: TypeInfo, value: Any) -> Any: # -- public -------------------------------------------------------------- - def decode_lean_obj(self, type_name: str, lean_obj: "LeanObj") -> LeanInductiveValue: + def decode_lean_obj( + self, type_name: str, lean_obj: "LeanObj" + ) -> LeanInductiveValue: """Decode a ``LeanObj`` (raw ``lean_object*``) as a registered inductive. This is the entry point for Path B (tactic): Lean wraps an ``Expr`` @@ -615,19 +668,29 @@ def _build_wrapper(self, t: TypeRepr) -> TypeWrapper: # Unit is encoded as the boxed scalar 0 (the `()` ctor). def from_lean(p): return None + def to_lean(_): return ffi.lean_box(0) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "bool": + def from_lean(p): return _ctor_tag(ffi, p) == 1 + def to_lean(b): return ffi.lean_box(1 if b else 0) - return TypeWrapper(t, from_lean, to_lean, c_uint8, - ctor_scalar_size=1, - from_ctor_scalar=lambda raw: raw == 1, - to_ctor_scalar=lambda b: 1 if b else 0) + + return TypeWrapper( + t, + from_lean, + to_lean, + c_uint8, + ctor_scalar_size=1, + from_ctor_scalar=lambda raw: raw == 1, + to_ctor_scalar=lambda b: 1 if b else 0, + ) if k == "nat": # Small values are boxed scalars; use lean_uint64_of_nat at the FFI level. @@ -635,14 +698,20 @@ def from_lean(p): v = ffi.lean_uint64_of_nat(p) ffi.lean_dec(p) return v + def to_lean(n): if n < 0: raise ValueError("Nat must be ≥ 0") - return ffi.lean_unsigned_to_nat(ctypes.c_uint(n & 0xFFFFFFFF).value) \ - if n < (1 << 32) else ffi.lean_uint64_to_nat(ctypes.c_uint64(n).value) + return ( + ffi.lean_unsigned_to_nat(ctypes.c_uint(n & 0xFFFFFFFF).value) + if n < (1 << 32) + else ffi.lean_uint64_to_nat(ctypes.c_uint64(n).value) + ) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "int": + def from_lean(p): # Use lean_scalar_to_int / lean_int_to_int64 round-trip. if ffi.lean_is_scalar(p): @@ -651,33 +720,48 @@ def from_lean(p): v = ffi.lean_int64_of_int(p) ffi.lean_dec(p) return v + def to_lean(n): return ffi.lean_int64_to_int(ctypes.c_int64(n).value) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "string": + def from_lean(p): s = self._lean_string_to_py(p) ffi.lean_dec(p) return s + def to_lean(s): return self._py_to_lean_string(s) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "float": + def from_lean(p): # IEEE doubles are passed by value, not pointer; this path is # only used when float appears in a generic context (boxed). v = ffi.lean_unbox_float(p) ffi.lean_dec(p) return v + def to_lean(f): return ffi.lean_box_float(c_double(f).value) + return TypeWrapper( - t, from_lean, to_lean, c_double, + t, + from_lean, + to_lean, + c_double, ctor_scalar_size=8, - from_ctor_scalar=lambda raw: _struct.unpack('d', _struct.pack('Q', raw))[0], - to_ctor_scalar=lambda f: _struct.unpack('Q', _struct.pack('d', float(f)))[0], + from_ctor_scalar=lambda raw: _struct.unpack( + "d", _struct.pack("Q", raw) + )[0], + to_ctor_scalar=lambda f: _struct.unpack( + "Q", _struct.pack("d", float(f)) + )[0], ) if k == "uint": @@ -685,7 +769,10 @@ def to_lean(f): byte_sz = bits // 8 ct = {8: c_uint8, 16: c_uint16, 32: c_uint32, 64: c_uint64}[bits] return TypeWrapper( - t, lambda v: int(v), lambda v: ct(int(v)).value, ct, + t, + lambda v: int(v), + lambda v: ct(int(v)).value, + ct, ctor_scalar_size=byte_sz, from_ctor_scalar=lambda raw: int(raw), to_ctor_scalar=lambda v, _ct=ct: _ct(int(v)).value, # type: ignore[misc,return-value] @@ -697,10 +784,15 @@ def to_lean(f): ct = {8: c_int8, 16: c_int16, 32: c_int32, 64: c_int64}[bits] uct = {8: c_uint8, 16: c_uint16, 32: c_uint32, 64: c_uint64}[bits] return TypeWrapper( - t, lambda v: int(v), lambda v: ct(int(v)).value, ct, + t, + lambda v: int(v), + lambda v: ct(int(v)).value, + ct, ctor_scalar_size=byte_sz, from_ctor_scalar=lambda raw, _ct=ct: int(_ct(raw).value), # type: ignore[misc,return-value] - to_ctor_scalar=lambda v, _uct=uct, _ct=ct: _uct(_ct(int(v)).value).value, # type: ignore[misc,return-value] + to_ctor_scalar=lambda v, _uct=uct, _ct=ct: ( # type: ignore[misc] + _uct(_ct(int(v)).value).value + ), # type: ignore[return-value] ) if k == "char": @@ -711,12 +803,17 @@ def from_lean(p): return chr(n) ffi.lean_dec(p) raise RuntimeError("Char value was not scalar") + def to_lean(c): if isinstance(c, str) and len(c) == 1: c = ord(c) return ffi.lean_box(int(c)) + return TypeWrapper( - t, from_lean, to_lean, c_uint32, + t, + from_lean, + to_lean, + c_uint32, ctor_scalar_size=4, from_ctor_scalar=lambda raw: chr(raw), to_ctor_scalar=lambda c: ord(c) if isinstance(c, str) else int(c), @@ -724,16 +821,20 @@ def to_lean(c): if k == "array": inner = self.wrapper_for(t.elem) # type: ignore[arg-type] + def from_lean(p): xs = self._lean_array_to_py(p, inner) ffi.lean_dec(p) return xs + def to_lean(xs): return self._py_to_lean_array(xs, inner) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "list": inner = self.wrapper_for(t.elem) # type: ignore[arg-type] + def from_lean(p): # List α: ctor 0 is `nil`, ctor 1 is `cons head tail`. out = [] @@ -748,6 +849,7 @@ def from_lean(p): cur = _ctor_get(ffi, cur, 1) ffi.lean_dec(p) return out + def to_lean(xs): items = list(xs) # Build right-to-left. @@ -758,10 +860,12 @@ def to_lean(xs): ffi.lean_ctor_set(cell, 1, acc) acc = cell return acc + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "option": inner = self.wrapper_for(t.elem) # type: ignore[arg-type] + def from_lean(p): tag = _ctor_tag(ffi, p) if tag == 0: @@ -772,34 +876,42 @@ def from_lean(p): v = inner.from_lean(inner_ptr) ffi.lean_dec(p) return v + def to_lean(v): if v is None: return ffi.lean_box(0) cell = ffi.lean_alloc_ctor(1, 1, 0) ffi.lean_ctor_set(cell, 0, inner.to_lean(v)) return cell + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "prod": wa = self.wrapper_for(t.a) # type: ignore[arg-type] wb = self.wrapper_for(t.b) # type: ignore[arg-type] + def from_lean(p): a_ptr = _ctor_get(ffi, p, 0) b_ptr = _ctor_get(ffi, p, 1) - ffi.lean_inc(a_ptr); ffi.lean_inc(b_ptr) - a = wa.from_lean(a_ptr); b = wb.from_lean(b_ptr) + ffi.lean_inc(a_ptr) + ffi.lean_inc(b_ptr) + a = wa.from_lean(a_ptr) + b = wb.from_lean(b_ptr) ffi.lean_dec(p) return (a, b) + def to_lean(pr): a, b = pr cell = ffi.lean_alloc_ctor(0, 2, 0) ffi.lean_ctor_set(cell, 0, wa.to_lean(a)) ffi.lean_ctor_set(cell, 1, wb.to_lean(b)) return cell + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "io": inner = self.wrapper_for(t.elem) # type: ignore[arg-type] + # IO is encoded as Except IO.Error α (where the second field # is the new RealWorld state). On Ok, m_objs[0] holds the # value (owned by the IO ctor); we inc to take ownership and @@ -808,9 +920,9 @@ def from_lean(p): tag = _ctor_tag(ffi, p) if tag == 0: val_ptr = _ctor_get(ffi, p, 0) - ffi.lean_inc(val_ptr) # +1 (now we share ownership) - ffi.lean_dec(p) # drop the IO ctor → val_ptr's - # shared ownership stays at 1 + ffi.lean_inc(val_ptr) # +1 (now we share ownership) + ffi.lean_dec(p) # drop the IO ctor → val_ptr's + # shared ownership stays at 1 return inner.from_lean(val_ptr) # consumes val_ptr # error case: decode the IO.Error ctor and raise a typed # exception (LeanError or LeanPyCallbackError). @@ -819,12 +931,14 @@ def from_lean(p): exc = self._build_io_exception(err_ptr) ffi.lean_dec(p) raise exc + def to_lean(v): # Wrap a value as an IO Ok result. cell = ffi.lean_alloc_ctor(0, 2, 0) ffi.lean_ctor_set(cell, 0, inner.to_lean(v)) ffi.lean_ctor_set(cell, 1, ffi.lean_box(0)) return cell + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "named": @@ -840,6 +954,7 @@ def to_lean(v): scalar_sz, ct = 2, c_uint16 else: scalar_sz, ct = 4, c_uint32 + def from_lean(tag, _ti=ti): # type: ignore[misc] if isinstance(tag, int): n = tag @@ -851,6 +966,7 @@ def from_lean(tag, _ti=ti): # type: ignore[misc] if ctor is None: raise RuntimeError(f"unknown {_ti.name} tag {n}") return LeanInductiveValue(_ti.name, ctor.name, n, ()) + def to_lean(v): if isinstance(v, LeanInductiveValue): return ffi.lean_box(v.tag) @@ -859,11 +975,13 @@ def to_lean(v): if isinstance(v, int): return ffi.lean_box(v) raise TypeError(f"cannot encode {v!r} as enum {ti.name}") + def _from_scalar(raw, _ti=ti): ctor = next((c for c in _ti.ctors if c.tag == raw), None) if ctor is None: raise RuntimeError(f"unknown {_ti.name} tag {raw}") return LeanInductiveValue(_ti.name, ctor.name, raw, ()) + def _to_scalar(v): if isinstance(v, LeanInductiveValue): return v.tag @@ -872,18 +990,25 @@ def _to_scalar(v): if isinstance(v, int): return v raise TypeError(f"cannot encode {v!r} as enum scalar") + return TypeWrapper( - t, from_lean, to_lean, ct, + t, + from_lean, + to_lean, + ct, ctor_scalar_size=scalar_sz, from_ctor_scalar=_from_scalar, to_ctor_scalar=_to_scalar, ) + def from_lean(p): v = self._decode_inductive(ti, p) ffi.lean_dec(p) return v + def to_lean(v): return self._encode_inductive(ti, v) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) if k == "pyobject": @@ -962,6 +1087,7 @@ def to_lean(v): "supported; convert via LeanPy.Python.Py.ofString / etc. on " "the Lean side, or pass through a LeanObj handle" ) + return TypeWrapper(t, from_lean, to_lean, ObjPtr) def _opaque_wrapper(self, t: TypeRepr) -> TypeWrapper: @@ -979,8 +1105,10 @@ def _opaque_wrapper(self, t: TypeRepr) -> TypeWrapper: """ ObjPtr = self._lean_object_ptr ffi = self.ffi + def from_lean(p): return LeanObj(p, owned=True) + def to_lean(v): if isinstance(v, LeanObj): p = v.ptr @@ -988,6 +1116,7 @@ def to_lean(v): ffi.lean_inc(p) return p return v + return TypeWrapper(t, from_lean, to_lean, ObjPtr) # Lean's `IO.Error` inductive (Init/System/IOError.lean), Lean 4.25.x: @@ -1000,16 +1129,16 @@ def to_lean(v): # non-userError variants that's typically the filename, so # `_format` shows it via `context["raw_field0"]`. _IO_ERROR_TAGS = { - 0: "alreadyExists", - 1: "otherError", - 2: "resourceBusy", - 3: "resourceVanished", - 4: "unsupportedOperation", - 5: "hardwareFault", - 6: "unsatisfiedConstraints", - 7: "illegalOperation", - 8: "protocolError", - 9: "timeExpired", + 0: "alreadyExists", + 1: "otherError", + 2: "resourceBusy", + 3: "resourceVanished", + 4: "unsupportedOperation", + 5: "hardwareFault", + 6: "unsatisfiedConstraints", + 7: "illegalOperation", + 8: "protocolError", + 9: "timeExpired", 10: "interrupted", 11: "noFileOrDirectory", 12: "invalidArgument", @@ -1042,10 +1171,6 @@ def _build_io_exception(self, ptr: Any) -> "Exception": Python exception type is visible. Other ctors map to `LeanError` with the appropriate `kind`. """ - from lean_py.exceptions import ( - LeanError, LeanPyCallbackError, parse_io_error_message, - ) - try: tag = _ctor_tag(self.ffi, ptr) except Exception: @@ -1068,8 +1193,11 @@ def _build_io_exception(self, ptr: Any) -> "Exception": # Other ctors carry varying field shapes. Capture field0 as the # primary descriptor and leave a structured `context` so callers # can still access it. - return LeanError(kind, field0 or f"<{kind} (no message)>", - context={"raw_field0": field0} if field0 else None) + return LeanError( + kind, + field0 or f"<{kind} (no message)>", + context={"raw_field0": field0} if field0 else None, + ) def _format_io_error(self, ptr: Any) -> str: """Legacy stringification — preserved for callers that just want diff --git a/lean_py/project.py b/lean_py/project.py index 6cb4dbd..cfd0e99 100644 --- a/lean_py/project.py +++ b/lean_py/project.py @@ -16,20 +16,22 @@ import hashlib import os import shutil +from importlib.metadata import version as pkg_version from pathlib import Path -from typing import TYPE_CHECKING +from lean_py.kernel import Kernel +from lean_py.library import LeanLibrary from lean_py.utils import lean_toolchain_version, run_command -if TYPE_CHECKING: - from lean_py.kernel import Kernel - from lean_py.library import LeanLibrary - _LEANPY_ROOT = Path(__file__).resolve().parent.parent -_CACHE_ROOT = Path(os.environ.get( - "LEANPY_MANAGED_DIR", - Path.home() / ".lean_py" / "managed", -)) +_LEANPY_GIT = "https://github.com/BasisResearch/lean.py" +_IS_DEV = (_LEANPY_ROOT / "lakefile.lean").exists() +_CACHE_ROOT = Path( + os.environ.get( + "LEANPY_MANAGED_DIR", + Path.home() / ".lean_py" / "managed", + ) +) # Well-known Lake packages: name -> (git, import_name, link_obj) # The rev is auto-matched to the active lean-toolchain version. @@ -66,8 +68,19 @@ def _dep_rev(version: str) -> str: return version +def _leanpy_version() -> str: + """Return the installed lean_py package version.""" + return pkg_version("lean_py") + + +def _leanpy_git_rev() -> str: + """Git rev for the LeanPy Lake dependency when pip-installed.""" + return os.environ.get("LEANPY_GIT_REV", f"v{_leanpy_version()}") + + def _cache_key(lean_version: str, deps: tuple[str, ...]) -> str: - blob = f"{lean_version}|{','.join(sorted(deps))}|{_LEANPY_ROOT}" + src_id = str(_LEANPY_ROOT) if _IS_DEV else f"git:{_leanpy_git_rev()}" + blob = f"{lean_version}|{','.join(sorted(deps))}|{src_id}" return hashlib.sha256(blob.encode()).hexdigest()[:16] @@ -101,18 +114,15 @@ def build(self) -> None: def library(self) -> LeanLibrary: """Build and return a :class:`LeanLibrary` for this project.""" - from lean_py.library import LeanLibrary - return LeanLibrary.from_lake(self._dir, "Managed", build=True) def kernel(self) -> Kernel: """Build and return a :class:`Kernel` backed by this project.""" - from lean_py.kernel import Kernel - lib = self.library() k = Kernel(lib) sp = run_command( - ["lake", "env", "printenv", "LEAN_PATH"], cwd=str(self._dir), + ["lake", "env", "printenv", "LEAN_PATH"], + cwd=str(self._dir), ) k.init_search(sp) k.load(["Init", "LeanPy.Z3"]) @@ -127,7 +137,8 @@ def clean(self) -> None: if self._dir.exists(): shutil.rmtree(self._dir) key = next( - (k for k, v in self._instances.items() if v is self), None, + (k for k, v in self._instances.items() if v is self), + None, ) if key: del self._instances[key] @@ -169,7 +180,13 @@ def _generate_lakefile( "", "[[require]]", 'name = "LeanPy"', - f'path = "{_LEANPY_ROOT}"', + ] + if _IS_DEV: + lines.append(f'path = "{_LEANPY_ROOT}"') + else: + lines.append(f'git = "{_LEANPY_GIT}"') + lines.append(f'rev = "{_leanpy_git_rev()}"') + lines += [ "", ] @@ -193,17 +210,19 @@ def _generate_lakefile( _, _, link_obj = _KNOWN_DEPS[dep] link_objs.append(f'"{link_obj}"') - lines.extend([ - "[[lean_lib]]", - 'name = "Managed"', - "moreLinkObjs = [" + ", ".join(link_objs) + "]", - "precompileModules = true", - 'defaultFacets = ["shared"]', - "moreLinkArgs = [", - ' "-Wl,-headerpad_max_install_names",', - "]", - "", - ]) + lines.extend( + [ + "[[lean_lib]]", + 'name = "Managed"', + "moreLinkObjs = [" + ", ".join(link_objs) + "]", + "precompileModules = true", + 'defaultFacets = ["shared"]', + "moreLinkArgs = [", + ' "-Wl,-headerpad_max_install_names",', + "]", + "", + ] + ) return "\n".join(lines) diff --git a/lean_py/registry.py b/lean_py/registry.py index 356bec8..64a9f61 100644 --- a/lean_py/registry.py +++ b/lean_py/registry.py @@ -31,6 +31,7 @@ class TypeRepr: - ``"pyobject"`` — the ``LeanPy.Python.Py`` opaque wrapper. - ``"opaque"`` — any type that lean-py cannot introspect. """ + kind: str # Optional fields, depending on kind bits: int | None = None @@ -64,8 +65,17 @@ def __repr__(self) -> str: def short(self) -> str: """A compact pseudo-Lean rendering for diagnostics.""" k = self.kind - if k in ("unit", "bool", "nat", "int", "float", "float32", "char", - "string", "pyobject"): + if k in ( + "unit", + "bool", + "nat", + "int", + "float", + "float32", + "char", + "string", + "pyobject", + ): return k.capitalize() if k != "string" else "String" if k == "uint": return f"UInt{self.bits}" @@ -95,6 +105,7 @@ class CtorInfo: tag: Runtime integer tag (index in constructor order, starting at 0). fields: Tuple of :class:`TypeRepr` describing each positional field. """ + name: str tag: int fields: tuple[TypeRepr, ...] @@ -118,6 +129,7 @@ class TypeInfo: isEnum: True if all constructors are nullary (enum-like). ctors: Constructors in declaration order. """ + name: str isStructure: bool isEnum: bool @@ -143,6 +155,7 @@ class FuncInfo: params: Positional parameter types in declaration order. returnType: Return type (may be wrapped in ``IO``). """ + declName: str exportName: str params: tuple[TypeRepr, ...] @@ -168,6 +181,7 @@ class LibraryRegistry: funcs: All ``@[python]``-annotated functions. types: All types registered via ``derive_python``. """ + funcs: tuple[FuncInfo, ...] = field(default_factory=tuple) types: tuple[TypeInfo, ...] = field(default_factory=tuple) diff --git a/lean_py/utils.py b/lean_py/utils.py index 2f55a5a..a35786e 100644 --- a/lean_py/utils.py +++ b/lean_py/utils.py @@ -14,9 +14,7 @@ def run_command(args: list[str], **kwargs) -> str: res = subprocess.run(args, capture_output=True, **kwargs) if res.returncode != 0: stderr = res.stderr.decode(errors="replace") if res.stderr else "" - raise RuntimeError( - f"Command {args} exited with {res.returncode}: {stderr}" - ) + raise RuntimeError(f"Command {args} exited with {res.returncode}: {stderr}") return res.stdout.decode().strip() diff --git a/lean_py/z3/_inductive_reg.py b/lean_py/z3/_inductive_reg.py new file mode 100644 index 0000000..bb3c765 --- /dev/null +++ b/lean_py/z3/_inductive_reg.py @@ -0,0 +1,34 @@ +"""Registration of Python datatypes as Lean inductives. + +Separated from solver.py to break a circular import: core.py needs +_register_inductive, and solver.py imports from core.py. +""" + +from __future__ import annotations + +from typing import Any + +from lean_py.z3._ast import InductiveASTSort + + +def _register_inductive(name: str, ctors: list[tuple[str, Any]]) -> None: + """Register a Lean inductive type in the kernel environment.""" + from lean_py.z3.solver import _get_kernel, _marshal_sort + + k = _get_kernel() + lib = k._lib + + lean_ctors = [] + for ctor_name, fields in ctors: + lean_fields = [] + for f_name, f_sort in fields: + if hasattr(f_sort, "_ast_sort"): + sort = _marshal_sort(lib, f_sort._ast_sort) + else: + # Self-referential: f_sort is a _DatatypeBuilder + sort = _marshal_sort(lib, InductiveASTSort(f_sort._name)) + lean_fields.append(lib.Z3CtorField(f_name, sort)) + lean_ctors.append(lib.Z3CtorDesc(ctor_name, lean_fields)) + + desc = lib.Z3InductiveDesc(name, lean_ctors) + lib.z3_add_inductive(desc) diff --git a/lean_py/z3/core.py b/lean_py/z3/core.py index d4bb236..f70f208 100644 --- a/lean_py/z3/core.py +++ b/lean_py/z3/core.py @@ -18,6 +18,7 @@ from fractions import Fraction from typing import Any, Sequence +from lean_py.z3._inductive_reg import _register_inductive from lean_py.z3._ast import ( ASTNode, ASTSort, @@ -1214,8 +1215,6 @@ def declare( self._ctors.append((ctor_name, tuple(fields))) def create(self) -> DatatypeSortRef: - from lean_py.z3.solver import _register_inductive - _register_inductive(self._name, self._ctors) sort = DatatypeSortRef(InductiveASTSort(self._name), self._name, self._ctors) diff --git a/lean_py/z3/solver.py b/lean_py/z3/solver.py index eaaa0a6..0bb25d1 100644 --- a/lean_py/z3/solver.py +++ b/lean_py/z3/solver.py @@ -18,8 +18,10 @@ from __future__ import annotations -from typing import TYPE_CHECKING, Any +from typing import Any +from lean_py.kernel import Kernel +from lean_py.project import ManagedProject from lean_py.z3._ast import ( ASTNode, ASTSort, @@ -94,15 +96,11 @@ FuncDeclRef, Implies, Not, - _DatatypeBuilder, _ast_repr, ) from lean_py.z3.smt2 import parse_smt2_file as _parse_smt2_file_impl from lean_py.z3.smt2 import parse_smt2_string as _parse_smt2_string_impl -if TYPE_CHECKING: - from lean_py.kernel import Kernel - # --------------------------------------------------------------------------- # CheckSatResult # --------------------------------------------------------------------------- @@ -151,9 +149,6 @@ def _get_kernel() -> Kernel: global _kernel if _kernel is not None: return _kernel - # Lazy init via ManagedProject - from lean_py.project import ManagedProject - mp = ManagedProject.get() _kernel = mp.kernel() return _kernel @@ -399,36 +394,6 @@ def _var_sort_key(var: tuple[str, ASTSort]) -> tuple[int, str]: return (2, name) -# --------------------------------------------------------------------------- -# Inductive type registration -# --------------------------------------------------------------------------- - - -def _register_inductive(name: str, ctors: list) -> None: - """Register a Lean inductive type in the kernel environment.""" - k = _get_kernel() - lib = k._lib - - lean_ctors = [] - for ctor_name, fields in ctors: - lean_fields = [] - for f_name, f_sort in fields: - if isinstance(f_sort, _DatatypeBuilder): - lean_fields.append( - lib.Z3CtorField( - f_name, _marshal_sort(lib, InductiveASTSort(f_sort._name)) - ) - ) - else: - lean_fields.append( - lib.Z3CtorField(f_name, _marshal_sort(lib, f_sort._ast_sort)) - ) - lean_ctors.append(lib.Z3CtorDesc(ctor_name, lean_fields)) - - desc = lib.Z3InductiveDesc(name, lean_ctors) - lib.z3_add_inductive(desc) - - # --------------------------------------------------------------------------- # Core prove function # ---------------------------------------------------------------------------