Module translation 

Translation between JavaScript, Rust, Lean and Rocq through a checked portable core.

Each frontend reads a source program into the surface AST, the checker resolves names, types and the exact operator semantics, and each emitter writes a target program together with its mapping, the encodings it chose and the assumptions it relies on.

Mirrors js/src/translation/; both runtimes produce the same surface trees, checked programs, target texts and contracts.

Modules

aborts

The message a source program aborts with, in the words of the source language, so every target aborts where the source does with the message the source prints.

check

The portable-core checker.

decimal

Arbitrary-precision integer literals as decimal strings.

diagnostics

Errors raised by the portable-core translator.

emit_common

State shared by the emitters.

emit_javascript

The JavaScript emitter: writes a checked program as a strict ES module with its translation contract.

emit_lean

The Lean 4 emitter.

emit_rocq

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

emit_rust

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

ir

The checked portable core: every expression carries its type and every operator its source semantics. Emitters consume it; the renaming passes give each target unique, legal local names.

javascript

JavaScript frontend for the portable core.

js_number

ECMAScript Number::toString for binary64.

lean

The Lean 4 frontend for the portable core.

lean_root_names

Generated by js/scripts/build-lean-root-names.mjs from Lean 4.34.1; do not edit.

lexer

Tokenizer shared by the portable-core translation frontends.

output

Output and aborts as values, for the targets whose programs are pure.

proof

Portable proof plans.

rocq

The Rocq frontend for the portable core.

rust

The Rust frontend: reads a Rust program into the surface AST.

surface

The surface AST the four frontends produce and the checker consumes.

types

Portable-core types.

Structs

Span

A source range in UTF-16 code units, as JavaScript string offsets count.

Enums

Language

The four languages of the translation matrix.