meta_language/
language_support.rs

1//! Versioned capability and translation declarations for the four-language surface.
2
3/// Schema revision for parser, emitter, and translation contracts.
4pub const LANGUAGE_REPRESENTATION_SCHEMA_VERSION: u32 = 2;
5
6/// Honest capability level for a representation layer.
7#[derive(Clone, Copy, Debug, PartialEq, Eq)]
8pub enum RepresentationLevel {
9    /// Original information is retained exactly.
10    Preserved,
11    /// A concrete lexical/syntactic structure is available.
12    ConcreteSyntax,
13    /// Surface structure was parsed into language-specific semantic facts.
14    Parsed,
15    /// References are connected to project-aware symbol identities.
16    Resolved,
17    /// Expanded or elaborated structures and their provenance are available.
18    Elaborated,
19    /// Source is retained but its meaning requires a project extension or plugin.
20    Opaque,
21    /// The language does not define this representation layer.
22    NotApplicable,
23    /// The runtime does not provide this semantic layer.
24    Unavailable,
25}
26
27/// Immutable support declaration for a registered language frontend and emitter.
28#[derive(Clone, Copy, Debug, PartialEq, Eq)]
29pub struct LanguageSupport {
30    /// Contract schema revision.
31    pub schema_version: u32,
32    /// Canonical language name.
33    pub name: &'static str,
34    /// Case-insensitive parser aliases.
35    pub aliases: &'static [&'static str],
36    /// Exact target language release.
37    pub version: &'static str,
38    /// Language edition or surface dialect.
39    pub edition: &'static str,
40    /// Registered file extensions.
41    pub extensions: &'static [&'static str],
42    /// Original-source preservation level.
43    pub source_bytes: RepresentationLevel,
44    /// Parser structure level.
45    pub concrete_syntax: RepresentationLevel,
46    /// Name/scope resolution level.
47    pub binding_resolution: RepresentationLevel,
48    /// Type or proof elaboration level.
49    pub type_elaboration: RepresentationLevel,
50    /// Handling of macros, notation, attributes, and plugins.
51    pub dynamic_extensions: RepresentationLevel,
52    /// Proof/tactic representation level.
53    pub proof_syntax: RepresentationLevel,
54    /// Registered emitter description.
55    pub emitter: &'static str,
56}
57
58const fn support(
59    name: &'static str,
60    aliases: &'static [&'static str],
61    version: &'static str,
62    edition: &'static str,
63    extensions: &'static [&'static str],
64    proof_syntax: RepresentationLevel,
65) -> LanguageSupport {
66    LanguageSupport {
67        schema_version: LANGUAGE_REPRESENTATION_SCHEMA_VERSION,
68        name,
69        aliases,
70        version,
71        edition,
72        extensions,
73        source_bytes: RepresentationLevel::Preserved,
74        concrete_syntax: RepresentationLevel::ConcreteSyntax,
75        binding_resolution: RepresentationLevel::Parsed,
76        type_elaboration: RepresentationLevel::Unavailable,
77        dynamic_extensions: RepresentationLevel::Parsed,
78        proof_syntax,
79        emitter: "ordered source-token emitter",
80    }
81}
82
83/// The four built-in parser/emitter capability declarations.
84pub const FOUR_LANGUAGE_SUPPORT: [LanguageSupport; 4] = [
85    support(
86        "JavaScript",
87        &["javascript", "js", "ecmascript"],
88        "ECMAScript 2026",
89        "ECMA-262, 17th edition",
90        &[".js", ".mjs", ".cjs"],
91        RepresentationLevel::NotApplicable,
92    ),
93    support(
94        "Rust",
95        &["rust", "rs"],
96        "Rust 1.99.0",
97        "2024",
98        &[".rs"],
99        RepresentationLevel::NotApplicable,
100    ),
101    support(
102        "Lean",
103        &["lean", "lean4"],
104        "Lean 4.34.1",
105        "Lean 4",
106        &[".lean"],
107        RepresentationLevel::Parsed,
108    ),
109    support(
110        "Rocq",
111        &["rocq", "coq"],
112        "Rocq 9.3",
113        "Vernacular",
114        &[".v"],
115        RepresentationLevel::Parsed,
116    ),
117];
118
119/// Returns the capability declaration for a canonical name or alias.
120#[must_use]
121pub fn language_support(language: &str) -> Option<&'static LanguageSupport> {
122    FOUR_LANGUAGE_SUPPORT.iter().find(|support| {
123        support
124            .aliases
125            .iter()
126            .any(|alias| alias.eq_ignore_ascii_case(language))
127    })
128}
129
130/// Translation-hook result when no semantics-preserving implementation is registered.
131#[derive(Clone, Copy, Debug, PartialEq, Eq)]
132pub enum TranslationSupport {
133    /// A reversible target-native source envelope preserves the full program.
134    PortableEncoding,
135    /// A recognized source form has an executable target implementation.
136    SemanticSubset,
137    /// A portable-core program is translated to a native target program with a recorded contract.
138    SemanticTranslation,
139}
140
141/// One directed source-to-target translation contract.
142#[derive(Clone, Debug, PartialEq, Eq)]
143pub struct TranslationContract {
144    /// Contract schema revision.
145    pub schema_version: u32,
146    /// Canonical source language.
147    pub source: &'static str,
148    /// Canonical target language.
149    pub target: &'static str,
150    /// Current support state.
151    pub support: TranslationSupport,
152    /// Observable behavior currently represented.
153    pub observation: &'static str,
154    /// Runtime required to validate target artifacts.
155    pub required_runtime: &'static str,
156    /// Registered non-native encoding, if any.
157    pub encoding: &'static str,
158    /// Assumptions made by the translation.
159    pub assumptions: &'static [&'static str],
160    /// Precise reason translation cannot proceed.
161    pub obligation: Option<String>,
162}
163
164/// Returns all 12 directed hooks among JavaScript, Rust, Lean, and Rocq.
165#[must_use]
166pub fn translation_contracts() -> Vec<TranslationContract> {
167    FOUR_LANGUAGE_SUPPORT
168        .iter()
169        .flat_map(|source| {
170            FOUR_LANGUAGE_SUPPORT
171                .iter()
172                .filter(move |target| target.name != source.name)
173                .map(move |target| contract(source, target))
174        })
175        .collect()
176}
177
178/// Returns one directed translation hook, excluding same-language emission.
179#[must_use]
180pub fn translation_contract(
181    source_language: &str,
182    target_language: &str,
183) -> Option<TranslationContract> {
184    let source = language_support(source_language)?;
185    let target = language_support(target_language)?;
186    (source.name != target.name).then(|| contract(source, target))
187}
188
189fn contract(source: &LanguageSupport, target: &LanguageSupport) -> TranslationContract {
190    TranslationContract {
191        schema_version: LANGUAGE_REPRESENTATION_SCHEMA_VERSION,
192        source: source.name,
193        target: target.name,
194        support: TranslationSupport::PortableEncoding,
195        observation: "exact source bytes after decoding; target behavior is not preserved",
196        required_runtime: runtime_for(target.name),
197        encoding: "meta-language portable source envelope v1 (UTF-8 hexadecimal payload)",
198        assumptions: &["the source-language runtime is required to execute decoded source"],
199        obligation: Some(
200            "semantic translation is not implemented for arbitrary source programs".to_string(),
201        ),
202    }
203}
204
205fn runtime_for(language: &str) -> &'static str {
206    match language {
207        "Lean" => "Lean 4.34.1 kernel and project environment",
208        "Rocq" => "Rocq 9.3 kernel and project environment",
209        "Rust" => "Rust 1.99.0, edition 2024",
210        _ => "ECMAScript 2026 host",
211    }
212}
meta_language/language_support.rs

meta_language/
language_support.rs
