meta_language/translation/
mod.rs

1//! Translation between JavaScript, Rust, Lean and Rocq through a checked
2//! portable core.
3//!
4//! Each frontend reads a source program into the surface AST,
5//! the checker resolves names, types and the exact operator semantics, and
6//! each emitter writes a target program together with its mapping, the
7//! encodings it chose and the assumptions it relies on.
8//!
9//! Mirrors `js/src/translation/`; both runtimes produce the same surface
10//! trees, checked programs, target texts and contracts.
11
12use serde::{Deserialize, Serialize};
13
14pub mod aborts;
15pub mod check;
16pub mod decimal;
17pub mod diagnostics;
18pub mod emit_common;
19pub mod emit_javascript;
20pub mod emit_lean;
21pub mod emit_rocq;
22pub mod emit_rust;
23mod frontend_rules;
24pub mod ir;
25pub mod javascript;
26pub mod js_number;
27pub mod lean;
28pub mod lean_root_names;
29pub mod lexer;
30pub mod output;
31pub mod proof;
32pub mod rocq;
33pub mod rust;
34pub mod surface;
35pub mod types;
36
37/// A source range in UTF-16 code units, as JavaScript string offsets count.
38#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
39pub struct Span {
40    pub start: usize,
41    pub end: usize,
42}
43
44impl Span {
45    #[must_use]
46    pub const fn new(start: usize, end: usize) -> Self {
47        Self { start, end }
48    }
49}
50
51/// The four languages of the translation matrix.
52#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
53pub enum Language {
54    JavaScript,
55    Rust,
56    Lean,
57    Rocq,
58}
59
60impl Language {
61    pub const ALL: [Self; 4] = [Self::JavaScript, Self::Rust, Self::Lean, Self::Rocq];
62
63    #[must_use]
64    pub const fn as_str(self) -> &'static str {
65        match self {
66            Self::JavaScript => "JavaScript",
67            Self::Rust => "Rust",
68            Self::Lean => "Lean",
69            Self::Rocq => "Rocq",
70        }
71    }
72
73    #[must_use]
74    pub fn parse(name: &str) -> Option<Self> {
75        Self::ALL
76            .into_iter()
77            .find(|language| language.as_str() == name)
78    }
79}
meta_language/translation/mod.rs

meta_language/translation/
mod.rs
