Come chiamare codice dell’host da Lean

Questa guida mostra come il codice Lean chiama una funzione dell’applicazione, nel linguaggio del pacchetto generato. Per Rust, vedi come chiamare funzioni Rust da Lean; per operazioni a cui l’applicazione risponde in modo asincrono, vedi come chiamare operazioni asincrone dell’host.

Dichiara una facility in Lean

Ciò che l’host fornisce è una facility: una dichiarazione registrata con @[lungo_facility], le cui operazioni sono dichiarazioni @[extern] marcate @[lungo_operation]. Il progetto richiede la libreria Lean di lungo per gli attributi.

import Lungo

namespace Store

/-- The application's store. -/
@[lungo_facility "store.data"]
structure Data

/-- The application's log. -/
@[lungo_facility "store.journal"]
structure Journal

/-- Looks a key up in the application's store. -/
@[extern "store_lookup", lungo_operation Data]
opaque lookup (key : @& String) : Option Nat

/-- Appends a line to the application's log. -/
@[extern "store_log", lungo_operation Journal]
opaque log (line : String) : IO Unit

def total (keys : List String) : IO Nat := do
  let mut sum := 0
  for k in keys do
    match lookup k with
    | some v => log s!"{k} = {v}"; sum := sum + v
    | none => throw (IO.userError s!"unknown key {k}")
  return sum

end Store

L’identificatore della facility (store.data) la nomina in ogni pacchetto, e il suo ultimo segmento la nomina in ciascun linguaggio (Data, set_data, data). Un extern che non è operazione di alcuna facility e che né il runtime né il programma implementano è un errore (LNG0401); lo è anche un’operazione che il runtime o un @[export] Lean implementano già (LNG0706).

Ciò che Lean non può controllare dell’host, può assumerlo: una proposizione @[lungo_assumption Data] dice che cosa deve soddisfare l’implementazione dell’host, e i claim che vi si appoggiano lo dichiarano in ogni pacchetto (vedi come dichiarare facility e assunzioni).

Implementala

Il pacchetto generato ha, per ogni facility, un’interfaccia (o un protocollo) con un metodo per operazione, con il nome della dichiarazione Lean e i suoi tipi, e una funzione che la installa. Un’operazione IO fallisce con l’errore di IO del linguaggio (qualsiasi altro errore diventa IO.userError con il suo messaggio); un’operazione che non è IO né EIO non deve fallire: un suo fallimento termina il programma. Un’operazione il cui tipo Lean è puro deve anche comportarsi da funzione pura, rispondendo allo stesso modo agli stessi argomenti: Lean può calcolare lookup "a" una volta sola e conservarne il valore.

Installa ogni facility prima della prima chiamata del programma. Una chiamata precedente fallisce indicando la facility e una sua operazione: Go restituisce un *lungo.MissingFacilityError, Python solleva lungo_py.MissingFacilityError, Swift lancia LungoMissingFacility, il load di TypeScript rifiuta con MissingFacilityError e un programma C termina con un messaggio.

Go

type data struct{ values map[string]*big.Int }

func (d *data) Lookup(key string) (lungo.Option[*big.Int], error) {
	v, ok := d.values[key]
	return lungo.Option[*big.Int]{Value: v, Valid: ok}, nil
}

type journal struct{}

func (journal) Log(line string) error {
	log.Println(line)
	return nil
}

store.SetData(&data{values: map[string]*big.Int{"a": big.NewInt(1)}})
store.SetJournal(journal{})

Python

class Data:
    def lookup(self, key: str):
        return {"a": 1}.get(key)

class Journal:
    def log(self, line: str) -> None:
        print(line)

store.set_data(Data())
store.set_journal(Journal())

Swift

final class Table: StoreData {
    func lookup(_ key: String) throws -> LungoNat? { key == "a" ? 1 : nil }
}

final class Console: StoreJournal {
    func log(_ line: String) throws { print(line) }
}

setData(Table())
setJournal(Console())

TypeScript

const p = await load({
  facilities: {
    data: { lookup: (key) => (key === "a" ? 1n : null) },
    journal: { log: (line) => console.log(line) },
  },
});

C

static int32_t lookup(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result, lungo_error **error) {
    size_t len;
    const char *key = lungo_value_get_string(args[0], &len);
    *result = len == 1 && key[0] == 'a' ? lungo_value_some(lungo_value_nat(1)) : lungo_value_none();
    return LUNGO_OK;
}

static int32_t log_line(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result, lungo_error **error) {
    size_t len;
    const char *line = lungo_value_get_string(args[0], &len);
    printf("%.*s\n", (int)len, line);
    *result = lungo_value_unit();
    return LUNGO_OK;
}

store_implement_data_lookup(lookup, NULL, NULL);
store_implement_journal_log(log_line, NULL, NULL);

Vedi di che cosa ha bisogno il programma

lungo assurance elenca, per ogni export, le facility di cui ha bisogno e le assunzioni che i suoi claim fanno su di esse; ogni pacchetto porta le stesse informazioni nel suo documento di garanzia (vedi il documento di garanzia).

Passa funzioni in entrambe le direzioni

Un parametro Lean di tipo funzione accetta una funzione del linguaggio dell’host, che Lean può chiamare un numero qualsiasi di volte, su qualsiasi thread, finché la trattiene; una funzione Lean restituita all’host è una funzione che l’host chiama. Entrambe attraversano il confine come descritto nel formato di trasmissione; non serve dichiarare nulla.