L’API C (lungo.h)

lungo.h è l’interfaccia della libreria del runtime precompilato (liblungo). È inclusa in ogni pacchetto del runtime (include/lungo.h) e in ogni pacchetto generato. La sua ABI C ha una versione, LUNGO_ABI_VERSION, attualmente 2; il codice generato chiama la funzione lungo_abi_v<N> (lungo_abi_v2), che solo un runtime di quell’ABI definisce, quindi non può collegarsi a un runtime di un’altra ABI.

L’header ha tre parti: l’API dei valori, per i programmi C e Objective-C che usano un pacchetto C generato; l’API del programma e il confine, per il codice generato e le librerie di supporto; e le primitive del runtime (lungo_<symbol> per ogni simbolo Lean @[extern] implementato dal runtime), per il codice generato.

Valori

Un lungo_value * è un valore Lean come albero di dati semplici. L’API restituisce valori posseduti, da liberare con lungo_value_free; i costruttori dei valori composti prendono possesso delle loro parti; gli accessori restituiscono puntatori presi in prestito dal loro argomento. Un valore possiede gli handle e le funzioni dell’host che contiene: liberarlo li rilascia, lungo_value_clone li duplica.

lungo_value_kind(v) è il genere del valore; lungo_value_equal(a, b) confronta valori (i valori opachi e le funzioni sono uguali quando sono lo stesso handle o la stessa funzione dell’host); le stringhe restituite dall’API si liberano con lungo_string_free.

Un uso scorretto dell’API (un puntatore nullo, la lettura di un valore di un altro genere, un indice fuori intervallo) termina il processo con un messaggio che indica la funzione. I dati non validi (una stringa che non è UTF-8, cifre che non formano un numero) vengono segnalati da un risultato NULL.

Tipi

Un lungo_type * è un’espressione di tipo: lungo_type_simple(LUNGO_NAT) (e gli altri generi senza parti), 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), e i tipi con nome di un programma a partire dai suoi descrittori generati. I costruttori prendono in prestito i loro argomenti; i tipi si liberano con lungo_type_free. Le funzioni polimorfe ricevono i tipi dei loro argomenti di tipo; i valori funzione hanno bisogno del proprio tipo per essere chiamati.

Chiamate ed errori

Una funzione generata restituisce uno stato:

lungo_error_kind(e), lungo_error_message(e) (per la visualizzazione; il valore stesso per un valore di errore stringa) e lungo_error_value(e) leggono un errore; lungo_error_free(e) lo libera.

Funzioni dell’host

Una funzione dell’host ha il tipo lungo_function:

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

Restituisce LUNGO_OK con il suo risultato (posseduto dal runtime da quel momento), oppure LUNGO_FAILED con un errore: lungo_error_io(message) per un extern IO (l’IO.userError di Lean; una copia di un errore ricevuto da Lean, lungo_error_clone(e), solleva quell’errore), oppure lungo_error_from_value(v) per un extern EIO. Un errore di una funzione dell’host il cui tipo Lean non è né l’uno né l’altro è fatale per il programma. Le funzioni dell’host possono essere chiamate su qualsiasi thread. La funzione drop fornita insieme a una di esse ne libera il contesto quando nessun valore o chiusura Lean vi fa più riferimento.

La prima funzione dell’host creata rende l’API C l’host del processo; un processo ha un solo host, quindi le funzioni dell’host dell’API C non possono essere combinate con la libreria di supporto di un altro linguaggio.

Un pacchetto C generato implementa ogni operazione delle facility del programma con una funzione dell’host passata a <id>_implement_<facility>_<operation>(f, ctx, drop), prima che il programma si inizializzi. Il primo uso del programma controlla che ogni operazione ne abbia una, e altrimenti termina il processo (lungo_panic_facility_missing), indicando la facility, l’operazione e la sua dichiarazione Lean.

Programmi asincroni

Una funzione generata per un export che restituisce Lungo.Async.Program Op α prende un lungo_step * al posto del risultato, e vi memorizza il primo passo del programma:

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;

Un passo LUNGO_STEP_DONE contiene il valore del programma. Un passo LUNGO_STEP_CALL contiene l’operazione che si chiede all’host di compiere, un valore di Op da leggere con i suoi accessori generati, e una ripresa (resumption). L’host compie l’operazione, nei suoi tempi e su qualsiasi thread, e risponde:

Una ripresa si usa esattamente una volta: riprenderla o annullarla la consuma, così la continuazione del programma non viene mai eseguita due volte, e una ripresa usata di nuovo viene riportata come LUNGO_STALE, mai indefinita. Un programma che l’host non riprende né annulla resta in memoria fino alla fine del processo; un processo può terminare con programmi in attesa.

Garanzia

const char *<id>_assurance_json(void) restituisce il documento di garanzia del programma, il testo dell’assurance.json del pacchetto, terminato da NUL e statico.

API del programma e confine

Queste parti sono usate dal codice generato e dalle librerie di supporto; sono documentate in lungo.h stesso:

• oggetti: lungo_obj, boxing, percorsi rapidi (inline) e lenti del conteggio dei riferimenti, allocazione, chiusure e applicazione;
• costanti e inizializzatori (lungo_lazy_obj, lungo_init_obj, …), l’inizializzazione del programma e lungo_run_main;
• il confine del formato di trasmissione: lungo_types_load, il contesto della chiamata (lungo_call_*, con lungo_call_write_async per il primo passo di un programma asincrono), la ripresa dei programmi asincroni (lungo_async_resume, lungo_async_cancel, lungo_async_outstanding), le chiamate all’host (lungo_hostcall_*), lungo_closure_call, lungo_set_host, gli handle (lungo_handle_clone, lungo_handle_release) e i buffer (lungo_buffer_alloc, lungo_buffer_free);
• lungo_invoke e lungo_host_function_new, tramite cui i pacchetti C generati implementano la loro API sull’API dei valori;
• lungo_check_layout(lean_type, provider, expected, actual), con cui un pacchetto che usa il tipo di un altro pacchetto (tipi extern) rifiuta, prima della sua prima chiamata, un fornitore generato per un altro layout del tipo.