The C API (lungo.h)

lungo.h is the interface of the prebuilt runtime library (liblungo). It is included in every runtime package (include/lungo.h) and every generated package. Its C ABI has a version, LUNGO_ABI_VERSION, currently 2; generated code calls the function lungo_abi_v<N> (lungo_abi_v2), which only a runtime of that ABI defines, so it cannot link with a runtime of another ABI.

The header has three parts: the value API, for C and Objective-C programs using a generated C package; the program API and the boundary, for generated code and the support libraries; and the runtime’s primitives (lungo_<symbol> for every Lean @[extern] symbol the runtime implements), for generated code.

Values

A lungo_value * is a Lean value as a tree of plain data. The API returns owned values, freed with lungo_value_free; constructors of composite values take ownership of their parts; accessors return pointers borrowed from their argument. A value owns the handles and host functions in it: freeing it releases them, lungo_value_clone duplicates them.

lungo_value_kind(v) is the value’s kind; lungo_value_equal(a, b) compares values (opaque values and functions are equal when they are the same handle or host function); strings the API returns are freed with lungo_string_free.

Misusing the API (a null pointer, reading a value of another kind, an index out of range) terminates the process with a message naming the function. Invalid data (a string that is not UTF-8, digits that are not a number) is reported by a NULL result.

Types

A lungo_type * is a type expression: lungo_type_simple(LUNGO_NAT) (and the other kinds without parts), lungo_type_option(t), lungo_type_list(t), lungo_type_array(t), lungo_type_prod(a, b), lungo_type_except(e, a), lungo_type_function(params, n, result), and the named types of a program from its generated descriptors. Constructors borrow their arguments; types are freed with lungo_type_free. Polymorphic functions take the types of their type arguments; function values need their type to be called.

Calls and errors

A generated function returns a status:

lungo_error_kind(e), lungo_error_message(e) (for display; the value itself for a string error value) and lungo_error_value(e) read an error; lungo_error_free(e) frees it.

Host functions

A host function has the type lungo_function:

int32_t f(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result, lungo_error **error);

It returns LUNGO_OK with its result (owned by the runtime afterwards), or LUNGO_FAILED with an error: lungo_error_io(message) for an IO extern (Lean’s IO.userError; a copy of an error received from Lean, lungo_error_clone(e), raises that error), or lungo_error_from_value(v) for an EIO extern. An error of a host function whose Lean type is neither is fatal to the program. Host functions may be called on any thread. The drop function given with one frees its context once no value or Lean closure refers to it.

The first host function created makes the C API the process’s host; a process has one host, so the C API’s host functions cannot be combined with another language’s support library.

A generated C package implements each operation of the program’s facilities with a host function given to <id>_implement_<facility>_<operation>(f, ctx, drop), before the program initializes. The program’s first use checks that every operation has one, and otherwise ends the process (lungo_panic_facility_missing), naming the facility, the operation and its Lean declaration.

Async programs

A generated function for an export returning Lungo.Async.Program Op α takes a lungo_step * in place of the result, and stores the program’s first step in it:

typedef struct lungo_step {
    uint8_t kind;           /* LUNGO_STEP_DONE or LUNGO_STEP_CALL */
    lungo_value *value;     /* owned: the program's value, or the operation it asks */
    uint64_t resumption;    /* LUNGO_STEP_CALL: what answers the operation */
} lungo_step;

A LUNGO_STEP_DONE step holds the program’s value. A LUNGO_STEP_CALL step holds the operation the host is asked to perform, a value of Op read with its generated accessors, and a resumption. The host performs the operation, in its own time and on any thread, and answers it:

A resumption is used exactly once: resuming or cancelling consumes it, so the program’s continuation never runs twice, and a resumption used again is reported as LUNGO_STALE, never undefined. A program the host neither resumes nor cancels stays in memory until the process ends; a process may end with programs waiting.

Assurance

const char *<id>_assurance_json(void) returns the program’s assurance document, the text of the package’s assurance.json, NUL-terminated and static.

Program API and boundary

These parts are used by generated code and the support libraries; they are documented in lungo.h itself:

• objects: lungo_obj, boxing, reference counting fast paths (inline) and slow paths, allocation, closures and application;
• constants and initializers (lungo_lazy_obj, lungo_init_obj, …), the program’s initialization and lungo_run_main;
• the boundary of the wire format: lungo_types_load, the call context (lungo_call_*, with lungo_call_write_async for an async program’s first step), the resumption of async programs (lungo_async_resume, lungo_async_cancel, lungo_async_outstanding), host calls (lungo_hostcall_*), lungo_closure_call, lungo_set_host, handles (lungo_handle_clone, lungo_handle_release) and buffers (lungo_buffer_alloc, lungo_buffer_free);
• lungo_invoke and lungo_host_function_new, through which generated C packages implement their API on the value API;
• lungo_check_layout(lean_type, provider, expected, actual), with which a package using another package’s type (extern types) refuses, before its first call, a provider generated for another layout of the type.