Come chiamare funzioni Rust da Lean

Questa guida mostra come permettere al codice Lean di chiamare una funzione della tua applicazione Rust: dichiararla in Lean come operazione di una facility, implementarla in Rust e mappare l’una sull’altra.

Dichiara la funzione in Lean

Una facility è ciò che l’applicazione fornisce, registrata con @[lungo_facility]; le sue operazioni sono costanti opache con il simbolo che il lato Rust implementerà, marcate @[lungo_operation]. Gli attributi vengono dalla libreria Lean di lungo, che il progetto Lake richiede:

import Lungo

namespace Host

/-- The services the application provides. -/
@[lungo_facility "app.services"]
structure Services

/-- Looks a key up in the host's table. -/
@[extern "host_lookup", lungo_operation Services]
opaque hostLookup (key : @& String) : Option Nat

/-- Appends a line to the host's log. -/
@[extern "host_log", lungo_operation Services]
opaque hostLog (line : String) : IO Unit

end Host

Il tipo del risultato ha bisogno di un’istanza Inhabited (Lean ne richiede una per opaque). @& indica un parametro che Lean presta anziché trasferire; la funzione Rust riceve in ogni caso un valore Rust posseduto. Ciò che le dimostrazioni del programma richiedono all’implementazione, e non possono controllare, si dichiara come assunzione della facility (vedi come dichiarare facility e assunzioni).

Usala da Lean come qualsiasi altra funzione:

def resolve (k : String) : IO Nat := do
  match Host.hostLookup k with
  | some v => Host.hostLog s!"{k} => {v}"; return v
  | none => throw (IO.userError s!"unknown key: {k}")

Implementala in Rust

Scrivi una funzione i cui parametri e il cui risultato sono le forme Rust dei tipi Lean (vedi I tipi Lean in Rust). IO α diventa Result<A, lungo::IoError>:

pub mod host {
    use lungo::{IoError, Nat};

    pub fn lookup(key: String) -> Option<Nat> {
        match key.as_str() {
            "alpha" => Some(Nat::from(1u64)),
            _ => None,
        }
    }

    pub fn log(line: String) -> Result<(), IoError> {
        if line.is_empty() {
            return Err(IoError::user("empty log line"));
        }
        eprintln!("{line}");
        Ok(())
    }
}

Un Err restituito da una funzione IO viene sollevato in Lean come quell’IO.Error. La funzione di un’operazione il cui tipo Lean è puro deve comportarsi da funzione pura, rispondendo allo stesso modo agli stessi argomenti: Lean può calcolare una tale chiamata una volta sola e conservarne il valore.

Mappa i simboli

In build.rs, mappa ogni simbolo sul percorso Rust della sua implementazione, visto dalla radice del crate:

fn main() -> lungo_build::Result<()> {
    lungo_build::configure()
        .rust_extern("host_lookup", "crate::host::lookup")
        .rust_extern("host_log", "crate::host::log")
        .compile_lean("lean")
}

(con il comando lungo, le stesse mappature sono la tabella [rust.rust-externs] di lungo.toml).

Compila. Se un’operazione non ha un’implementazione, la build fallisce con LNG0401, indicando la dichiarazione e la firma Rust di cui ha bisogno; così anche un extern che non è operazione di alcuna facility, con il suggerimento di marcarlo @[lungo_operation]. Mappare un simbolo che non è di un’operazione fallisce con LNG0706, e una mappatura per un simbolo che nessuno usa con LNG0405.

Passa funzioni attraverso il confine

Un parametro funzione di Lean arriva in Rust come LeanClosure, che Rust può chiamare:

@[extern "host_transform", lungo_operation Services]
opaque hostTransform (f : Nat → Nat) (xs : List Nat) : List Nat

use lungo::{LeanClosure, List, Nat};

pub fn transform(f: LeanClosure<fn(Nat) -> Nat>, xs: List<Nat>) -> List<Nat> {
    xs.into_iter().map(|x| f.call(x)).collect()
}

Nella direzione opposta, Rust passa le proprie funzioni alle funzioni Lean generate con LeanClosure::from_fn(|n: Nat| …).

In modalità LeanOracle

Le stesse mappature funzionano in modalità LeanOracle per gli extern dichiarati @[extern "symbol"]: l’adattatore generato viene esportato con quel simbolo C. Le altre forme di extern falliscono con LNG0407.

Le operazioni a cui l’applicazione risponde in modo asincrono sono invece una facility asincrona, i cui export diventano async fn che ricevono un handler (vedi come chiamare operazioni asincrone dell’host).

Un esempio completo è compiler-tests/host in lungo-rs.