Come condividere tipi tra progetti Lean

Questa guida mostra come usare i tipi generati per un pacchetto Lake nel pacchetto generato per un altro pacchetto che lo richiede, così che i valori passino dall’uno all’altro senza conversioni.

Supponi che il pacchetto Lake drawing richieda il pacchetto geometry. Generati separatamente, ciascuno ha il proprio tipo per la structure Lean Geometry.Point, e un Point dell’uno non può essere passato a una funzione dell’altro. Indicare alla generazione di drawing quale tipo fornisce Geometry.Point (un tipo extern) le fa usare quello di geometry.

In Rust

Compila ogni pacchetto in build.rs, e indica alla build di drawing quale tipo Rust fornisce ciascun tipo Lean di geometry che usa:

fn main() -> lungo_build::Result<()> {
    lungo_build::compile_lean("lean/geometry")?;
    lungo_build::configure()
        .extern_type("Geometry.Point", "crate::geometry::Point")
        .extern_type("Geometry.Shape", "crate::geometry::Shape")
        .compile_lean("lean/drawing")
}

I percorsi Rust sono visti dalla radice del crate; ogni modulo prende il nome dal suo pacchetto Lake:

pub mod geometry {
    lungo::include_lean!("geometry");
}

pub mod drawing {
    lungo::include_lean!("drawing");
}

Ora le funzioni di drawing accettano e restituiscono i tipi di geometry:

use my_crate::{drawing, geometry::Point};
use lungo::Int;

let a = Point { x: Int::from(-4), y: Int::from(2) };
let b = Point { x: Int::from(8), y: Int::from(6) };
let mid: Point = drawing::midpoint(a, b);

Un tipo i cui valori può costruire solo il codice Lean (uno con una dimostrazione tra i suoi campi) è opaco: il modulo di geometry vi si riferisce come lungo::LeanValue<crate::geometry::__opaque::<Name>>, ed è quello il percorso da indicare.

Negli altri linguaggi

La tabella di ciascun linguaggio in lungo.toml indica il tipo dell’altro pacchetto per un tipo Lean (vedi tipi extern):

# lungo.toml di drawing
project = "lean/drawing"

[go]
out = "drawing"

[go.extern-types."Geometry.Point"]
package = "example.com/app/geometry"   # il pacchetto Go generato per geometry
name = "Point"

package è ciò che il linguaggio importa (un percorso di import Go, un modulo Python, un modulo Swift, uno specificatore di modulo JavaScript, un header C) e name il tipo come lo ha chiamato il generatore di geometry. I valori creati da un programma passano all’altro così come sono: tramite handle per i tipi opachi, poiché entrambi girano sull’unico runtime del processo. In TypeScript ogni programma gira in una propria istanza WebAssembly, quindi lì si possono condividere solo i tipi i cui valori sono dati semplici; un tipo opaco viene rifiutato.

Che cosa lo rende sicuro

Il codice compilato di drawing legge i valori di geometry secondo il layout per cui è stato compilato. Entrambi devono provenire dalla stessa definizione del tipo, e di ogni tipo raggiunto dai suoi campi. Ogni tipo generato porta un’impronta del layout, e drawing controlla quella di geometry prima che qualcosa venga eseguito: in Rust non compila con un’altra (il tipo fornito implementa lungo::LeanLayout, cosa che un tipo generato da lungo fa già), e negli altri linguaggi il pacchetto si rifiuta di caricarsi, indicando il tipo e il pacchetto che lo fornisce. La soluzione è rigenerarli entrambi dalla stessa definizione Lean.

I tipi di drawing che contengono un tipo extern Rust derivano solo Clone e Debug, poiché lungo non sa quali altri trait implementi il tipo extern; aggiungi altre derivazioni con type_attribute. Una mappatura per un tipo Lean che nessuna dichiarazione esportata usa fallisce con LNG0107.

In lungo-rs, compiler-tests/shaping compila due moduli Rust di questo tipo, e compiler-tests/extern condivide tipi tra due programmi in ogni linguaggio.