Pacchetti generati

lungo generate --<language>_out=DIR scrive un pacchetto che contiene il programma (come C, oppure per TypeScript come WebAssembly) e la sua API nel linguaggio. Si compila con gli strumenti del linguaggio stesso e gira sul runtime di lungo, che prende dalla release di lungo (o da una distribuzione locale) esattamente alla versione che lo ha generato. L’output Rust è descritto in codice generato e in I tipi Lean in Rust.

Di seguito, l’id del programma è il suo nome come identificatore C (polyglot per un pacchetto Lake polyglot).

Nomi

Una dichiarazione esportata prende il nome dal suffisso più corto del suo nome Lean con cui non termina nessun’altra dichiarazione del suo genere: Geometry.Shape.area è area, a meno che un’altra funzione termini anch’essa con area, nel qual caso entrambe mantengono un componente in più (shape_area, other_area). Il suffisso viene convertito secondo le convenzioni del linguaggio (snake_case in C e Python, UpperCamelCase per Go e per tutti i tipi, lowerCamelCase per i membri Swift e TypeScript) ed escapato dove è una parola chiave.

Una funzione il cui nome risulta uguale a quello di un tipo (o di un costruttore, o di un descrittore) mantiene un componente in più, come fanno due funzioni che terminano allo stesso modo; il tipo mantiene il proprio nome. In Go, dove entrambi sono UpperCamelCase in un solo package, Gate.acquire accanto al tipo Acquire è GateAcquire. Due funzioni che otterrebbero comunque lo stesso nome (foo e Foo), o due tipi, sono un errore (LNG0107) che le indica entrambe: rinominane una in Lean.

Tipi Lean

I numeri vengono controllati quando entrano in Lean: un Nat negativo, un int32 Go fuori dall’intervallo di un UInt16, una stringa che non è Unicode valido, un valore nil di un tipo induttivo vengono rifiutati (vedi errori), mai troncati. Un Option i cui valori possono essere a loro volta None/null (Option (Option α), Option Unit) è Some(value) (Python, TypeScript) dove è some. Una structure che contiene sé stessa per valore (tramite opzioni, coppie o altre structure) è un puntatore in Go e una classe final in Swift. I valori a cui Lean non può dare un tipo del linguaggio (azioni IO memorizzate come dati, un Type, un valore di un tipo che il programma non descrive) sono opachi: handle che mantengono vivo il valore Lean finché non vengono chiusi o raccolti.

Tipi opachi

Un tipo induttivo i cui valori può costruire solo il codice Lean (per esempio uno con una dimostrazione tra i suoi campi, come una structure fatta di un valore e della dimostrazione che è ben formato) è opaco: i suoi valori attraversano il confine come handle, che le funzioni del programma creano e leggono. Resta comunque un tipo a sé: Wf in Go è struct{ lungo.Opaque }, una sottoclasse di lungo_py.Opaque in Python, una struct in Swift, una sottoclasse di Opaque in TypeScript, così il valore di un tipo opaco non può essere passato dove se ne aspetta un altro. I parametri di tipo di un tipo opaco non fanno parte del suo tipo nel binding. I tipi che non sono induttivi, o che hanno indici, sono semplici valori opachi.

Impronte del layout

Ogni tipo con nome registra l’impronta del suo layout: <Name>Fingerprint (Go), <Class>.__lungo_fingerprint__ (Python), <Type>.lungoFingerprint (Swift), leanTypes["<Lean name>"].fingerprint (TypeScript), <ID>_<TYPE>_FINGERPRINT (C), e lungo::LeanLayout::FINGERPRINT in Rust. Un pacchetto che usa il tipo di un altro come tipo extern la controlla prima di essere eseguito.

Una funzione polimorfa riceve per prima cosa un descrittore di tipo per ogni parametro di tipo: Size(lungo.NatType, tree) (Go), size(lungo_py.NAT, tree) (Python), size(Lungo.nat, tree) (Swift), p.size(L.NAT, tree) (TypeScript), polyglot_size(nat_type, tree, &result, &error) (C). Ogni tipo con nome ha una funzione descrittore (TreeType(a), tree_type(a), Tree.lungoType(a), treeType(a), polyglot_tree_type(a)).

Errori

Una funzione il cui risultato è Unit non restituisce nulla (solo il suo errore) in Go, Swift e TypeScript.

Facility

Gli extern che l’host implementa sono le operazioni delle facility del programma, che il suo codice Lean dichiara (@[lungo_facility "ns.name"], @[lungo_operation C]; vedi come chiamare codice dell’host da Lean). Ogni facility è un tipo del linguaggio, che prende il nome dall’ultimo componente del suo identificatore (polyglot.scaler è Scaler), con un metodo per operazione, e l’host installa un’implementazione di ciascuna:

Ogni facility dichiarata dai moduli collegati del programma va installata, che una data chiamata la raggiunga o no, così un programma fallisce alla sua prima chiamata invece che nel mezzo di una. Il commento di documentazione di una facility indica le assunzioni che i claim del programma fanno sull’implementazione dell’host; il programma non può verificarle. Un metodo il cui tipo Lean è puro deve rispondere allo stesso modo agli stessi argomenti: Lean può valutare una chiamata una sola volta e conservarne il valore.

Export asincroni

Un export che restituisce Lungo.Async.Program Op α chiede all’host, mentre viene eseguito, di compiere operazioni della facility asincrona su Op, e attende ogni risposta. È una funzione asincrona del linguaggio che prende per primo un handler: un oggetto con un metodo per ogni costruttore di Op, che prende i campi del costruttore e restituisce (o risolve con) la risposta.

Un programma a cui si rinuncia viene rilasciato dal runtime, e la chiamata fallisce con l’errore del metodo (o con l’annullamento). lungo.Outstanding() (Go), lungo_py.outstanding() (Python), lungoOutstanding() (Swift), p.outstanding() (TypeScript, per programma) e lungo_async_outstanding() (C) contano i programmi in attesa di una risposta: zero quando ogni chiamata è terminata. Un processo può terminare con programmi in attesa.

Garanzia

Ogni pacchetto contiene il documento di garanzia del programma, assurance.json, lo stesso file per ogni linguaggio, e lo legge con i tipi del linguaggio:

Ogni lettore rifiuta un documento di un’altra versione dello schema, o con un campo che non conosce o che manca, a qualunque profondità (dettagli).

Thread

Il programma può essere chiamato da un numero qualsiasi di thread contemporaneamente (goroutine Go, thread Python, task e code Swift, thread C); le chiamate rilasciano il GIL di Python. Le funzioni dell’host possono essere chiamate su qualsiasi thread, compresi i thread su cui girano i task di Lean. WebAssembly ha un solo thread: i task di Lean vengono eseguiti quando vengono creati, e il programma non può usare processi figli, socket, segnali o timer (LNG0408).

Un processo ha un solo runtime di lungo e un solo host: la libreria di supporto del suo linguaggio. Le funzioni dell’host dell’API C dei valori e la libreria di supporto di un altro linguaggio non possono essere usate nello stesso processo.

C

CMakeLists.txt          the library <id> (target <id>::<id>) and the runtime
include/<id>.h          the API
src/<id>.c
program/                the program: lungo.h, <id>_program.h, <id>_program.c,
                        <id>_boundary.c, modules/*.c

Il progetto CMake scarica l’archivio del runtime della release di lungo per il target, ne controlla il digest SHA-256 (URL_HASH) e collega la sua libreria statica (lungo::runtime). Con -D<ID>_FETCH_LUNGO=OFF usa invece un runtime installato (find_package(lungo <version> EXACT); CMAKE_PREFIX_PATH o lungo_DIR lo individuano); -D<ID>_LUNGO_TARGET=<triple> sceglie l’archivio quando il target non può essere dedotto. Includilo con add_subdirectory.

Ogni valore è un lungo_value * dell’API C. L’API aggiunge, per ogni tipo, il suo descrittore (<id>_<type>_type(...)), una funzione costruttore per ogni costruttore (<id>_<type>_<ctor>(fields…), che prende possesso dei campi), una macro con l’indice di ogni costruttore (<ID>_<TYPE>_<CTOR>) e un accessore per campo (<id>_<type>_<field>(v), oppure <id>_<type>_<ctor>_<field>(v) per i tipi con più costruttori); per ogni funzione int32_t <id>_<function>(type arguments…, arguments…, lungo_value **result, lungo_error **error) (un export asincrono prende lungo_step *step invece di result); <id>_implement_<facility>_<operation>(f, ctx, drop); <id>_assurance_json(); <id>_initialize() e <id>_run_main(argc, argv). Objective-C usa la stessa API (vedi Swift).

Go

<id>.go                 the package (cgo)
*.c, *.h                the program; module files are module_<stem>_lean.c

Il pacchetto importa github.com/machinefabric/lungo-go e richiede esattamente la versione del modulo della release di lungo che lo ha generato (const _ = lungo.EnforceVersion<version> non compila con un’altra). Il modulo contiene il runtime per linux/amd64, linux/arm64, darwin/amd64, darwin/arm64 e windows/amd64 e lo collega una sola volta per binario. Compila con cgo abilitato e un compilatore C (su Windows, GCC di MinGW-w64). Il nome del pacchetto è l’id del programma (opzione package).

Le funzioni restituiscono (T, error); i tipi sono tipi Go, ciascuno con una funzione descrittore (PointType(), TreeType[A](typeA)); Set<Facility>(impl) installa ogni facility; gli export asincroni prendono un context.Context e un handler; Assurance() è il documento di garanzia; RunMain(args) (int, error) esegue main.

Python

pyproject.toml          scikit-build-core; requires lungo-py
CMakeLists.txt          builds the program as the shared library of the package
program/
src/<package>/__init__.py, py.typed

pip install DIR compila una wheel (py3-none-<platform>: il programma è una libreria condivisa caricata con ctypes, non un’estensione CPython, quindi una sola wheel serve ogni Python 3). Dipende esattamente dal lungo-py della release, che contiene il runtime. Le funzioni sono funzioni del modulo (gli export asincroni sono async def); i tipi sono dataclass immutabili; set_<facility>(impl) installa ogni facility; ASSURANCE è il documento di garanzia; run_main(args) esegue main.

Swift

Package.swift           depends on lungo-swift at exactly the release's version
Sources/<Module>Program/  the program and the C API (include/<id>.h: for C and Objective-C)
Sources/<Module>/<Module>.swift

Il pacchetto ha due prodotti: <Module> (l’API Swift) e <Module>Program (l’API C, che Objective-C importa con @import <Module>Program;). lungo-swift fornisce LungoKit e il runtime come XCFramework (macOS 12 e successivi, iOS 15 e successivi, il simulatore iOS). Le funzioni sono funzioni del modulo che lanciano (throw; gli export asincroni sono async throws); i tipi sono struct e indirect enum; set<Facility>(_:) installa ogni facility; assurance è il documento di garanzia; runMain(_:) esegue main.

TypeScript

package.json            depends on lungo-ts at exactly the release's version
index.js, index.d.ts    ES module and its declarations
program.wasm            the program and the runtime, for wasm32-wasip1

lungo generate collega program.wasm con il wasi-sdk fissato. await load(options) lo istanzia (su Node.js 20 e successivi con node:wasi; nei browser con BrowserWasi di lungo-ts, o con qualsiasi WASI passato come options.wasi) e restituisce un oggetto i cui metodi sono le funzioni del programma (gli export asincroni restituiscono promise); options.facilities implementa le facility, e ASSURANCE è il documento di garanzia. I programmi che usano primitive che mancano a WebAssembly non possono essere generati (LNG0408).

Pacchetti incorporati

Una libreria che è già un pacchetto nel suo linguaggio (una distribuzione Python, un pacchetto npm, un pacchetto Swift o un progetto CMake) incorpora il programma al suo interno con l’opzione del generatore embed, invece di dipendere da un pacchetto proprio del programma. lungo possiede la directory di output e la sostituisce per intero, quindi è una directory dell’host, mai la sua radice. Il manifest dell’host fornisce ciò che avrebbe fornito quello generato: