The kernel facade. Wraps a :class:`LeanLibrary` whose Lean source has imported ``LeanPy.Kernel`` and exposed the standard ``@[python]`` surface. Example: .. code-block:: python from lean_py import LeanLibrary from lean_py.kernel import Kernel lib = LeanLi
| 237 | |
| 238 | |
| 239 | class Kernel: |
| 240 | """The kernel facade. |
| 241 | |
| 242 | Wraps a :class:`LeanLibrary` whose Lean source has imported |
| 243 | ``LeanPy.Kernel`` and exposed the standard ``@[python]`` surface. |
| 244 | |
| 245 | Example: |
| 246 | |
| 247 | .. code-block:: python |
| 248 | |
| 249 | from lean_py import LeanLibrary |
| 250 | from lean_py.kernel import Kernel |
| 251 | |
| 252 | lib = LeanLibrary.from_lake("path/to/project", "MyLib") |
| 253 | k = Kernel(lib) |
| 254 | k.init_search("") |
| 255 | k.load(["Init"]) |
| 256 | s = k.goal_create("∀ n : Nat, n + 0 = n") |
| 257 | print(s.pretty()) |
| 258 | """ |
| 259 | |
| 260 | def __init__(self, lib: Any) -> None: |
| 261 | self._lib = lib |
| 262 | |
| 263 | # -- env lifecycle --------------------------------------------------- |
| 264 | |
| 265 | def init_search(self, sp: str = "") -> None: |
| 266 | self._lib.leanpy_kernel_init_search(sp) |
| 267 | |
| 268 | def load(self, modules: Iterable[str]) -> None: |
| 269 | self._lib.leanpy_kernel_load_env(list(modules)) |
| 270 | |
| 271 | def is_loaded(self) -> bool: |
| 272 | return self._lib.leanpy_kernel_is_loaded(None) |
| 273 | |
| 274 | def clear(self) -> None: |
| 275 | self._lib.leanpy_kernel_clear_env(None) |
| 276 | |
| 277 | # -- env introspection ---------------------------------------------- |
| 278 | |
| 279 | def decl_count(self) -> int: |
| 280 | return int(self._lib.leanpy_kernel_decl_count(None)) |
| 281 | |
| 282 | def all_decls(self) -> list[str]: |
| 283 | s = self._lib.leanpy_kernel_all_decls(None) |
| 284 | return s.split("\n") if s else [] |
| 285 | |
| 286 | def catalog(self) -> list[str]: |
| 287 | s = self._lib.leanpy_kernel_catalog(None) |
| 288 | return s.split("\n") if s else [] |
| 289 | |
| 290 | def search(self, needle: str) -> list[str]: |
| 291 | s = self._lib.leanpy_kernel_search(needle) |
| 292 | return s.split("\n") if s else [] |
| 293 | |
| 294 | def decl_exists(self, name: str) -> bool: |
| 295 | return self._lib.leanpy_kernel_decl_exists(name) |
| 296 |