Function lean_py_to_lean_obj

LeanPy/native/python_bridge.c:1201–1235

* lean_py_to_lean_obj: extract a lean_object* from a Python LeanObjHandle. * Returns Option α: some(obj) if the Python object is a LeanObjHandle, * none otherwise. * * @[extern "lean_py_to_lean_obj"] * opaque Py.toLeanObj (py : @& Py) : IO (Option α) */

}

/*
 * lean_py_to_lean_obj: extract a lean_object* from a Python LeanObjHandle.
 * Returns Option α:  some(obj) if the Python object is a LeanObjHandle,
 * none otherwise.
 *
 * @[extern "lean_py_to_lean_obj"]
 * opaque Py.toLeanObj (py : @& Py) : IO (Option α)
 */
LEAN_EXPORT lean_obj_res lean_py_to_lean_obj(b_lean_obj_arg py_ext, lean_obj_arg world) {
    (void)world;
    ENSURE_INIT(); WITH_GIL();

    if (!lean_is_external(py_ext)) {
        /* Return none */
        return lean_io_result_mk_ok(lean_box(0));
    }

    PyObject *pyobj = unwrap_pyobject(py_ext);
    if (!pyobj) {
        return lean_io_result_mk_ok(lean_box(0));
    }

    /* Check if pyobj is an instance of LeanObjHandle.
       Cast to LeanObjHandle* to read ob_type (PyObject is opaque). */
    PyObject *handle_type = get_lean_obj_handle_type();
    LeanObjHandle *candidate = (LeanObjHandle *)pyobj;
    if (!handle_type || candidate->ob_type != handle_type) {
        return lean_io_result_mk_ok(lean_box(0));  /* none */
    }

    LeanObjHandle *h = (LeanObjHandle *)pyobj;
    lean_object *result = h->ptr;
    if (!result) {
        return lean_io_result_mk_ok(lean_box(0));  /* none */
    }

    lean_inc(result);  /* caller gets their own ref */