Module emit_rust 

The Rust emitter: writes a checked program as Rust with its translation contract.

Naturals and integers are ml::Big, an unbounded integer the translation carries in its own prelude, so no value is ever narrowed; machine integers stay Rust machine integers with checked arithmetic, which panics exactly where the source aborts; a JavaScript Number is an f64, printed by ml_number::js_number exactly as JavaScript prints it. Data types are enums whose data-typed fields are boxed. Every value is owned: a variable is cloned where it is consumed. Theorems cannot be proved in Rust: each becomes an executable property, checked over a bounded domain by --ml-check-theorems, while the proof stays discharged by the source kernel.

Mirrors js/src/translation/emit-rust.js.

Functions

emit_rust

Emits a checked program as Rust.