meta_language/translation/
emit_javascript.rs

1//! The JavaScript emitter: writes a checked program as a strict ES module
2//! with its translation contract.
3//!
4//! Every portable integer is a `BigInt`, so naturals and integers stay unbounded
5//! and machine integers are range-checked exactly as Rust checks them; a Number
6//! stays a Number. Data values are plain objects whose `$` property names the
7//! constructor. Modules become object literals referenced by qualified names.
8//! Theorems cannot be proved in JavaScript: each becomes an executable
9//! property, checked over a bounded domain by `--ml-check-theorems`, while the
10//! proof obligation stays discharged by the source language's kernel.
11//!
12//! Mirrors `js/src/translation/emit-javascript.js`.
13
14use std::collections::BTreeSet;
15
16use super::Language;
17use super::aborts::{cast_message, overflow_message, zero_divisor_message};
18use super::diagnostics::{Result, TranslationError, type_error, unsupported};
19use super::emit_common::{EmitOptions, EmitState, Emitted};
20use super::ir::{
21    Binder, ByZero, Case, Ctor, Decl, Effect, Expr, FnDecl, LitValue, Main, Node, Param, Pattern,
22    Program, Prop, Semantics, TheoremDecl, rename_function, rename_main, rename_theorem, tail_loop,
23};
24use super::lexer::json_string;
25use super::surface::{BinaryOp, Flavor, Rounding, UnaryOp};
26use super::types::{Type, fixed_bounds};
27
28mod arrays;
29mod helpers;
30mod math;
31mod names;
32use self::helpers::Helper;
33use self::names::{KEYWORDS, field_key, ident};
34
35fn indent(text: &str, depth: usize) -> String {
36    let pad = "  ".repeat(depth);
37    text.split('\n')
38        .map(|line| {
39            if line.is_empty() {
40                String::new()
41            } else {
42                format!("{pad}{line}")
43            }
44        })
45        .collect::<Vec<_>>()
46        .join("\n")
47}
48
49/// Top-level members are method-shaped (`name(…) {`); at the root they become function declarations.
50fn declare_function(text: &str) -> String {
51    let name = text
52        .find(|character: char| {
53            !(character.is_ascii_alphanumeric() || character == '_' || character == '$')
54        })
55        .unwrap_or(text.len());
56    if name > 0 && text[name..].starts_with('(') {
57        format!("function {text}")
58    } else {
59        text.to_owned()
60    }
61}
62
63/// The error JavaScript throws on a node the checker never produces.
64fn malformed(message: String) -> TranslationError {
65    type_error(message, None)
66}
67
68fn ctor_object(ctor: &Ctor, args: &[String]) -> String {
69    let fields: Vec<String> = ctor
70        .fields
71        .iter()
72        .enumerate()
73        .map(|(index, field)| {
74            let arg = args.get(index).map_or("undefined", String::as_str);
75            format!("{}: {arg}", field_key(&field.name))
76        })
77        .collect();
78    let fields = if fields.is_empty() {
79        String::new()
80    } else {
81        format!(", {}", fields.join(", "))
82    };
83    format!(
84        "Object.freeze({{ $: '{}'{fields} }})",
85        ctor.name.replace('\'', "\\'")
86    )
87}
88
89/// Emits a checked program as JavaScript.
90///
91/// # Errors
92/// On constructs the target cannot express faithfully.
93pub fn emit_javascript(program: &Program) -> Result<Emitted> {
94    let state = EmitState::new(
95        program,
96        Language::JavaScript,
97        ident,
98        KEYWORDS,
99        EmitOptions {
100            modules_share_term_space: true,
101            type_space: true,
102            ..EmitOptions::default()
103        },
104    );
105    JavaScriptEmitter {
106        program,
107        state,
108        helpers: BTreeSet::new(),
109        temporaries: 0,
110        theorem_checks: Vec::new(),
111        uses_float: false,
112        loop_params: None,
113    }
114    .file()
115}
116
117/// Declarations grouped by module, in source order.
118#[derive(Default)]
119struct ModuleTree<'p> {
120    items: Vec<&'p Decl>,
121    modules: Vec<(String, Self)>,
122}
123
124#[derive(Clone)]
125struct TheoremCheck {
126    reference: String,
127    binders: Vec<Binder>,
128    source: String,
129}
130
131struct JavaScriptEmitter<'p> {
132    program: &'p Program,
133    state: EmitState<'p>,
134    helpers: BTreeSet<Helper>,
135    temporaries: usize,
136    theorem_checks: Vec<TheoremCheck>,
137    uses_float: bool,
138    /// The lifted loop being emitted as a loop, and its parameters, which
139    /// each call to it assigns before the next iteration.
140    loop_params: Option<(String, Vec<String>)>,
141}
142
143impl<'p> JavaScriptEmitter<'p> {
144    fn file(mut self) -> Result<Emitted> {
145        let program = self.program;
146        let mut tree = ModuleTree::default();
147        for entry in &program.declarations {
148            let mut node = &mut tree;
149            for segment in entry.module_path() {
150                let index = if let Some(index) =
151                    node.modules.iter().position(|(name, _)| name == segment)
152                {
153                    index
154                } else {
155                    node.modules.push((segment.clone(), ModuleTree::default()));
156                    node.modules.len() - 1
157                };
158                node = &mut node.modules[index].1;
159            }
160            node.items.push(entry);
161        }
162        let mut blocks = Vec::new();
163        for entry in &tree.items {
164            if let Some(text) = self.declaration(entry)? {
165                blocks.push(declare_function(&text));
166            }
167        }
168        for (segment, node) in &tree.modules {
169            let path = [segment.clone()];
170            let name = self.module_name(&path);
171            let object = self.module_object(node, &path)?;
172            blocks.push(format!("const {name} = {object};"));
173        }
174        let main = match &program.main {
175            Some(main) => Some(self.main(main)?),
176            None => None,
177        };
178        let theorems = !self.theorem_checks.is_empty();
179        if theorems {
180            self.helpers.insert(Helper::Domains);
181            self.helpers.insert(Helper::Forall);
182        }
183        let mut entry = Vec::new();
184        if theorems {
185            entry.push(self.theorem_runner()?);
186        }
187        entry.extend(main.clone());
188        if theorems {
189            entry.push(
190                "if (process.argv.includes('--ml-check-theorems')) ml_checkTheorems();\nelse main();"
191                    .to_owned(),
192            );
193        } else if main.is_some() {
194            entry.push("main();".to_owned());
195        }
196        let mut lines = vec![
197            format!(
198                "// Translated from {} by meta-language: portable core, JavaScript target.",
199                program.source_language.as_str()
200            ),
201            "'use strict';".to_owned(),
202            String::new(),
203        ];
204        let preludes: Vec<String> = self
205            .helpers
206            .iter()
207            .map(|helper| helper.text().to_owned())
208            .collect();
209        for prelude in &preludes {
210            lines.push(prelude.clone());
211            lines.push(String::new());
212        }
213        let definitions = blocks.clone();
214        for block in blocks.into_iter().chain(entry) {
215            lines.push(block);
216            lines.push(String::new());
217        }
218        self.state.encode("numbers", "every natural, integer and machine integer is a BigInt; machine-integer results are range-checked and throw RangeError where Rust would panic");
219        if self.uses_float {
220            self.state.encode("floats", "a Number is a JavaScript Number, an IEEE-754 double, with its own arithmetic, comparisons and String conversion");
221        }
222        let mut emitted = self
223            .state
224            .finish(lines.join("\n"), main.map(|_| "main".to_owned()));
225        emitted.preludes = preludes;
226        emitted.definitions = definitions;
227        Ok(emitted)
228    }
229
230    fn module_name(&self, path: &[String]) -> String {
231        self.state
232            .module_name(path)
233            .unwrap_or("undefined")
234            .to_owned()
235    }
236
237    fn module_object(&mut self, node: &ModuleTree<'p>, path: &[String]) -> Result<String> {
238        let mut members = Vec::new();
239        for entry in &node.items {
240            if let Some(text) = self.declaration(entry)? {
241                members.push(indent(&format!("{text},"), 1));
242            }
243        }
244        for (segment, child) in &node.modules {
245            let mut child_path = path.to_vec();
246            child_path.push(segment.clone());
247            let name = self.module_name(&child_path);
248            let object = self.module_object(child, &child_path)?;
249            members.push(indent(&format!("{name}: {object},"), 1));
250        }
251        Ok(format!("{{\n{}\n}}", members.join("\n")))
252    }
253
254    fn declaration(&mut self, entry: &Decl) -> Result<Option<String>> {
255        match entry {
256            Decl::Data(data) => {
257                let name = self.state.local_name(&data.full_name).to_owned();
258                self.state.map(entry, &name);
259                self.state.encode("data", "a data value is a frozen object whose $ property names its constructor and whose other properties are its fields");
260                Ok(None)
261            }
262            Decl::Fn(function) => self.function(entry, function).map(Some),
263            Decl::Theorem(theorem) => self.theorem(entry, theorem).map(Some),
264        }
265    }
266
267    fn function(&mut self, entry: &Decl, function: &FnDecl) -> Result<String> {
268        let (params, body) = rename_function(function, &ident, &self.state.local_reserved());
269        if params.iter().any(|param| param.ty.is_float()) || function.ret.is_float() {
270            self.uses_float = true;
271        }
272        let name = self.state.local_name(&function.full_name).to_owned();
273        self.state.map(entry, &name);
274        let mut lines: Vec<String> = params
275            .iter()
276            .filter_map(|param| self.parameter_guard(param))
277            .collect();
278        if tail_loop(function) {
279            // A lifted loop runs as a loop: each iteration assigns the parameters their next values.
280            let names = params.iter().map(|param| param.name.clone()).collect();
281            self.loop_params = Some((function.full_name.clone(), names));
282            let statements = self.statements(&body);
283            self.loop_params = None;
284            lines.push("for (;;) {".to_owned());
285            lines.push(indent(&statements?.join("\n"), 1));
286            lines.push("}".to_owned());
287        } else {
288            lines.extend(self.statements(&body)?);
289        }
290        let names: Vec<&str> = params.iter().map(|param| param.name.as_str()).collect();
291        Ok(format!(
292            "{name}({}) {{\n{}\n}}",
293            names.join(", "),
294            indent(&lines.join("\n"), 1)
295        ))
296    }
297
298    /// Machine-integer parameters are range-checked, as the Rust type guarantees.
299    fn parameter_guard(&mut self, param: &Param) -> Option<String> {
300        let Type::Fixed { bits, signed } = param.ty else {
301            return None;
302        };
303        self.helpers.insert(Helper::Fixed);
304        let (min, max) = fixed_bounds(bits, signed);
305        Some(format!(
306            "ml_fixed({name}, {min}n, {max}n, {message});",
307            name = param.name,
308            message = json_string(&format!(
309                "{} argument {} out of range",
310                param.ty.key(),
311                param.name
312            ))
313        ))
314    }
315
316    fn theorem(&mut self, entry: &Decl, theorem: &TheoremDecl) -> Result<String> {
317        let (binders, prop, _) = rename_theorem(theorem, &ident, &self.state.local_reserved());
318        let name = self.state.local_name(&theorem.full_name).to_owned();
319        self.state.map(entry, &name);
320        self.state
321            .theorem(&theorem.full_name, &name, binders.is_empty(), true);
322        self.theorem_checks.push(TheoremCheck {
323            reference: self.state.reference(&theorem.full_name, "."),
324            binders: binders.clone(),
325            source: theorem.full_name.clone(),
326        });
327        let names: Vec<&str> = binders.iter().map(|binder| binder.name.as_str()).collect();
328        Ok(format!(
329            "{name}({}) {{\n  return {};\n}}",
330            names.join(", "),
331            self.prop(&prop)?
332        ))
333    }
334
335    fn theorem_runner(&mut self) -> Result<String> {
336        self.state.encode("theorem-properties", "each theorem is an executable property; --ml-check-theorems evaluates it on every input of a bounded domain, and its proof remains checked by the source kernel");
337        let mut checks = Vec::new();
338        for check in self.theorem_checks.clone() {
339            let mut domains = Vec::new();
340            for binder in &check.binders {
341                domains.push(self.domain(&binder.ty, 3)?);
342            }
343            let TheoremCheck {
344                reference, source, ..
345            } = check;
346            let call = if domains.is_empty() {
347                format!("{reference}()")
348            } else {
349                format!(
350                    "ml_product([{}]).every((args) => {reference}(...args))",
351                    domains.join(", ")
352                )
353            };
354            checks.push(format!("  if (!({call})) throw new Error('theorem {source} fails on a bounded input');\n  console.log('theorem {source}: holds on the bounded domain');"));
355        }
356        Ok(format!(
357            "function ml_checkTheorems() {{\n{}\n}}",
358            checks.join("\n")
359        ))
360    }
361
362    /// Values of a type up to a constructor depth, as JavaScript source.
363    fn domain(&mut self, ty: &Type, depth: i64) -> Result<String> {
364        self.helpers.insert(Helper::Domains);
365        let values = match ty {
366            Type::Nat => if depth >= 3 { "ml_nat" } else { "ml_small_nat" }.to_owned(),
367            Type::Int => if depth >= 3 { "ml_int" } else { "ml_small_int" }.to_owned(),
368            Type::Fixed { signed, .. } => if *signed {
369                "ml_small_int"
370            } else {
371                "ml_small_nat"
372            }
373            .to_owned(),
374            Type::Bool => "[false, true]".to_owned(),
375            Type::String => "['', 'a', 'ab']".to_owned(),
376            Type::Unit => "[null]".to_owned(),
377            Type::Data { name } => self.data_domain(name, depth)?,
378            other => {
379                return Err(malformed(format!(
380                    "no JavaScript domain for {}",
381                    other.kind()
382                )));
383            }
384        };
385        Ok(values)
386    }
387
388    fn data_domain(&mut self, name: &str, depth: i64) -> Result<String> {
389        let entry = self.program.data(name);
390        let mut values = Vec::new();
391        for ctor in &entry.ctors {
392            let recursive = ctor
393                .fields
394                .iter()
395                .any(|field| matches!(field.ty, Type::Data { .. }));
396            if recursive && depth <= 1 {
397                continue;
398            }
399            let mut fields = Vec::new();
400            for field in &ctor.fields {
401                let field_depth = if matches!(field.ty, Type::Data { .. }) {
402                    depth - 1
403                } else {
404                    1
405                };
406                fields.push(self.domain(&field.ty, field_depth)?);
407            }
408            if fields.is_empty() {
409                values.push(format!("[{}]", ctor_object(ctor, &[])));
410            } else {
411                let args: Vec<String> = (0..ctor.fields.len())
412                    .map(|index| format!("args[{index}]"))
413                    .collect();
414                values.push(format!(
415                    "ml_product([{}]).map((args) => {})",
416                    fields.join(", "),
417                    ctor_object(ctor, &args)
418                ));
419            }
420        }
421        if values.is_empty() {
422            return Ok("[]".to_owned());
423        }
424        let spread: Vec<String> = values.iter().map(|value| format!("...{value}")).collect();
425        Ok(format!("[{}]", spread.join(", ")))
426    }
427
428    fn prop(&mut self, prop: &Prop) -> Result<String> {
429        Ok(match prop {
430            Prop::Forall { binders, body } => {
431                let mut inner = self.prop(body)?;
432                for binder in binders.iter().rev() {
433                    let domain = self.domain(&binder.ty, 3)?;
434                    inner = format!("ml_forall({domain}, ({}) => {inner})", binder.name);
435                }
436                inner
437            }
438            Prop::And { left, right } => {
439                format!("({} && {})", self.prop(left)?, self.prop(right)?)
440            }
441            Prop::Or { left, right } => {
442                format!("({} || {})", self.prop(left)?, self.prop(right)?)
443            }
444            Prop::Implies { left, right } => {
445                format!("(!{} || {})", self.prop(left)?, self.prop(right)?)
446            }
447            Prop::Not { arg } => format!("!{}", self.prop(arg)?),
448            Prop::Bool { expr } => self.expr(expr)?,
449            Prop::Eq(comparison) | Prop::Ne(comparison) => {
450                let left = self.expr(&comparison.left)?;
451                let right = self.expr(&comparison.right)?;
452                let structured = matches!(comparison.left.ty, Type::Data { .. } | Type::Unit);
453                let equal = if structured {
454                    self.helpers.insert(Helper::Equal);
455                    format!("ml_equal({left}, {right})")
456                } else if comparison.same_value {
457                    format!("Object.is({left}, {right})")
458                } else {
459                    format!("({left} === {right})")
460                };
461                if matches!(prop, Prop::Eq(_)) {
462                    equal
463                } else {
464                    format!("!{equal}")
465                }
466            }
467            Prop::Lt(comparison)
468            | Prop::Le(comparison)
469            | Prop::Gt(comparison)
470            | Prop::Ge(comparison) => {
471                let operator = match prop {
472                    Prop::Lt(_) => "<",
473                    Prop::Le(_) => "<=",
474                    Prop::Gt(_) => ">",
475                    _ => ">=",
476                };
477                format!(
478                    "({} {operator} {})",
479                    self.expr(&comparison.left)?,
480                    self.expr(&comparison.right)?
481                )
482            }
483        })
484    }
485
486    /// A function body as statements that return its value.
487    fn statements(&mut self, e: &Expr) -> Result<Vec<String>> {
488        match &e.node {
489            Node::Let { name, value, body } => {
490                let mut lines = vec![format!("const {name} = {};", self.expr(value)?)];
491                lines.extend(self.statements(body)?);
492                Ok(lines)
493            }
494            Node::Print { text, body } => {
495                let mut lines = vec![format!("console.log({});", self.expr(text)?)];
496                lines.extend(self.statements(body)?);
497                Ok(lines)
498            }
499            Node::If {
500                cond,
501                then,
502                otherwise,
503            } => {
504                let cond = self.expr(cond)?;
505                let then = self.statements(then)?.join("\n");
506                let otherwise = self.statements(otherwise)?.join("\n");
507                Ok(vec![
508                    format!("if ({cond}) {{"),
509                    indent(&then, 1),
510                    "} else {".to_owned(),
511                    indent(&otherwise, 1),
512                    "}".to_owned(),
513                ])
514            }
515            Node::Match { scrutinee, cases } => self.match_statements(scrutinee, cases),
516            Node::Abort { message } => {
517                self.helpers.insert(Helper::Abort);
518                Ok(vec![format!("return ml_abort({});", json_string(message))])
519            }
520            Node::Call { func, args }
521                if self
522                    .loop_params
523                    .as_ref()
524                    .is_some_and(|(name, _)| name == func) =>
525            {
526                let mut texts = Vec::with_capacity(args.len());
527                for arg in args {
528                    texts.push(self.expr(arg)?);
529                }
530                let names = self
531                    .loop_params
532                    .as_ref()
533                    .map(|(_, names)| names.as_slice())
534                    .unwrap_or_default();
535                let mut lines = match names {
536                    [] => Vec::new(),
537                    [name] => vec![format!("{name} = {};", texts[0])],
538                    _ => vec![format!("[{}] = [{}];", names.join(", "), texts.join(", "))],
539                };
540                lines.push("continue;".to_owned());
541                Ok(lines)
542            }
543            _ => Ok(vec![format!("return {};", self.expr(e)?)]),
544        }
545    }
546
547    /// The body of the first wildcard or binding case, with the binding declared.
548    fn fallback_body(&mut self, fallback: Option<&Case>, subject: &str) -> Result<Vec<String>> {
549        // A checked match is exhaustive, so a missing case always has a fallback.
550        let kase = fallback.ok_or_else(|| {
551            malformed("Cannot read properties of undefined (reading 'pattern')".to_owned())
552        })?;
553        let mut lines = Vec::new();
554        if let Pattern::Bind { name } = &kase.pattern {
555            lines.push(format!("const {name} = {subject};"));
556        }
557        lines.extend(self.statements(&kase.body)?);
558        Ok(lines)
559    }
560
561    fn match_statements(&mut self, scrutinee: &Expr, cases: &[Case]) -> Result<Vec<String>> {
562        let mut lines = Vec::new();
563        let subject = if let Some(name) = scrutinee.var_name() {
564            name.to_owned()
565        } else {
566            self.temporaries += 1;
567            let subject = format!("ml_subject{}", self.temporaries);
568            lines.push(format!("const {subject} = {};", self.expr(scrutinee)?));
569            subject
570        };
571        let fallback = cases
572            .iter()
573            .find(|kase| matches!(kase.pattern, Pattern::Wild | Pattern::Bind { .. }));
574        let Type::Data { name: data } = &scrutinee.ty else {
575            let zero = cases
576                .iter()
577                .find(|kase| matches!(kase.pattern, Pattern::NatZero));
578            let succ = cases
579                .iter()
580                .find(|kase| matches!(kase.pattern, Pattern::NatSucc { .. }));
581            let zero_lines = match zero {
582                Some(kase) => self.statements(&kase.body)?,
583                None => self.fallback_body(fallback, &subject)?,
584            };
585            let succ_lines = match succ {
586                Some(Case {
587                    pattern: Pattern::NatSucc { name },
588                    body,
589                }) => {
590                    let mut lines = vec![format!("const {name} = {subject} - 1n;")];
591                    lines.extend(self.statements(body)?);
592                    lines
593                }
594                _ => self.fallback_body(fallback, &subject)?,
595            };
596            lines.extend([
597                format!("if ({subject} === 0n) {{"),
598                indent(&zero_lines.join("\n"), 1),
599                "} else {".to_owned(),
600                indent(&succ_lines.join("\n"), 1),
601                "}".to_owned(),
602            ]);
603            return Ok(lines);
604        };
605        let entry = self.program.data(data);
606        lines.push(format!("switch ({subject}.$) {{"));
607        for kase in cases {
608            let Pattern::Ctor { ctor, binds, .. } = &kase.pattern else {
609                continue;
610            };
611            let ctor = entry
612                .ctors
613                .iter()
614                .find(|candidate| candidate.name == *ctor)
615                .unwrap_or_else(|| panic!("{data} has no constructor {ctor}"));
616            let mut body: Vec<String> = binds
617                .iter()
618                .enumerate()
619                .filter_map(|(index, bind)| {
620                    bind.as_ref().map(|bind| {
621                        format!(
622                            "const {bind} = {subject}.{};",
623                            field_key(&ctor.fields[index].name)
624                        )
625                    })
626                })
627                .collect();
628            lines.push(format!("  case '{}': {{", ctor.name.replace('\'', "\\'")));
629            body.extend(self.statements(&kase.body)?);
630            lines.push(indent(&body.join("\n"), 2));
631            lines.push("  }".to_owned());
632        }
633        lines.push("  default: {".to_owned());
634        if fallback.is_some() {
635            let body = self.fallback_body(fallback, &subject)?;
636            lines.push(indent(&body.join("\n"), 2));
637        } else {
638            lines.push(format!(
639                "    throw new TypeError(`unexpected constructor ${{{subject}.$}}`);"
640            ));
641        }
642        lines.push("  }".to_owned());
643        lines.push("}".to_owned());
644        Ok(lines)
645    }
646
647    fn expr(&mut self, e: &Expr) -> Result<String> {
648        if e.ty.is_float() {
649            self.uses_float = true;
650        }
651        match &e.node {
652            Node::Lit { value } => literal(&e.ty, value),
653            Node::Unit => Ok("null".to_owned()),
654            Node::Var { name } => Ok(name.clone()),
655            Node::Print { text, body } => Ok(format!(
656                "(console.log({}), {})",
657                self.expr(text)?,
658                self.expr(body)?
659            )),
660            Node::OutNil | Node::OutCons { .. } => {
661                unreachable!("only the Lean and Rocq emitters thread output")
662            }
663            Node::Call { func, args } => {
664                let target = self.state.reference(func, ".");
665                let args = self.exprs(args)?;
666                Ok(format!("{target}({})", args.join(", ")))
667            }
668            Node::Ctor { data, ctor, args } => {
669                let entry = self.program.data(data);
670                let ctor = entry
671                    .ctors
672                    .iter()
673                    .find(|candidate| candidate.name == *ctor)
674                    .unwrap_or_else(|| panic!("{data} has no constructor {ctor}"));
675                let args = self.exprs(args)?;
676                Ok(ctor_object(ctor, &args))
677            }
678            Node::Unary { op, arg, .. } => {
679                let arg = self.expr(arg)?;
680                Ok(match op {
681                    UnaryOp::Not => format!("!{arg}"),
682                    UnaryOp::Neg => self.checked(negate(&arg), &e.ty, "neg"),
683                })
684            }
685            Node::Binary { .. } => self.binary(e),
686            Node::If {
687                cond,
688                then,
689                otherwise,
690            } => Ok(format!(
691                "({} ? {} : {})",
692                self.expr(cond)?,
693                self.expr(then)?,
694                self.expr(otherwise)?
695            )),
696            Node::Let { .. } | Node::Match { .. } => Ok(format!(
697                "(() => {{\n{}\n}})()",
698                indent(&self.statements(e)?.join("\n"), 1)
699            )),
700            Node::ToString { arg, console } => {
701                if *console && arg.ty.is_float() {
702                    self.helpers.insert(Helper::ShowNumber);
703                    Ok(format!("ml_showNumber({})", self.expr(arg)?))
704                } else if matches!(arg.ty, Type::String) {
705                    self.expr(arg)
706                } else {
707                    self.text_of(arg)
708                }
709            }
710            Node::Cast {
711                arg,
712                flavor,
713                message,
714                ..
715            } => self.cast(arg, *flavor, message.as_deref()),
716            Node::Abort { message } => {
717                self.helpers.insert(Helper::Abort);
718                Ok(format!("ml_abort({})", json_string(message)))
719            }
720            Node::Array { .. } | Node::Append { .. } | Node::Index { .. } | Node::Length { .. } => {
721                self.array_expr(e)
722            }
723            Node::Math { .. } => self.math(e),
724        }
725    }
726
727    pub(super) fn exprs(&mut self, list: &[Expr]) -> Result<Vec<String>> {
728        list.iter().map(|arg| self.expr(arg)).collect()
729    }
730
731    fn text_of(&mut self, arg: &Expr) -> Result<String> {
732        if matches!(arg.ty, Type::Data { .. } | Type::Unit) {
733            return Err(unsupported(
734                "output of structured values",
735                &format!("a {} value has no portable textual form", arg.ty.kind()),
736                arg.span,
737            ));
738        }
739        Ok(format!("String({})", self.expr(arg)?))
740    }
741
742    /// A machine-integer result out of range panics as Rust does.
743    fn checked(&mut self, text: String, ty: &Type, op: &str) -> String {
744        let Type::Fixed { bits, signed } = *ty else {
745            return text;
746        };
747        self.helpers.insert(Helper::Fixed);
748        let (min, max) = fixed_bounds(bits, signed);
749        format!(
750            "ml_fixed({text}, {min}n, {max}n, {})",
751            json_string(overflow_message(op))
752        )
753    }
754
755    fn binary(&mut self, e: &Expr) -> Result<String> {
756        let Node::Binary {
757            op,
758            left,
759            right,
760            semantics,
761            rounding,
762            by_zero,
763            ..
764        } = &e.node
765        else {
766            unreachable!("binary called on a {} node", e.kind());
767        };
768        let left = self.expr(left)?;
769        let right = self.expr(right)?;
770        let comparison = |operator: &str| format!("({left} {operator} {right})");
771        Ok(match op {
772            BinaryOp::And => comparison("&&"),
773            BinaryOp::Or => comparison("||"),
774            BinaryOp::Concat => comparison("+"),
775            BinaryOp::Eq => comparison("==="),
776            BinaryOp::Ne => comparison("!=="),
777            BinaryOp::Lt => comparison("<"),
778            BinaryOp::Le => comparison("<="),
779            BinaryOp::Gt => comparison(">"),
780            BinaryOp::Ge => comparison(">="),
781            BinaryOp::Add => self.checked(comparison("+"), &e.ty, "add"),
782            BinaryOp::Mul => self.checked(comparison("*"), &e.ty, "mul"),
783            BinaryOp::Sub => {
784                if *semantics == Some(Semantics::Truncated) {
785                    self.helpers.insert(Helper::NatSub);
786                    format!("ml_natSub({left}, {right})")
787                } else {
788                    self.checked(comparison("-"), &e.ty, "sub")
789                }
790            }
791            BinaryOp::Div | BinaryOp::Rem if *semantics == Some(Semantics::Ieee) => {
792                comparison(if *op == BinaryOp::Div { "/" } else { "%" })
793            }
794            BinaryOp::Div | BinaryOp::Rem => {
795                self.helpers.insert(Helper::Divide);
796                let rounding = match rounding {
797                    Some(Rounding::Trunc) => "trunc",
798                    Some(Rounding::Euclid) => "euclid",
799                    Some(Rounding::Floor) => "floor",
800                    None => "undefined",
801                };
802                let zero = if *by_zero == Some(ByZero::Abort) {
803                    json_string(zero_divisor_message(op.name(), &e.ty))
804                } else {
805                    "null".to_owned()
806                };
807                let remainder = *op == BinaryOp::Rem;
808                let Type::Fixed { bits, signed } = e.ty else {
809                    return Ok(format!(
810                        "ml_divide({left}, {right}, '{rounding}', {zero}, {remainder})"
811                    ));
812                };
813                let (min, max) = fixed_bounds(bits, signed);
814                format!(
815                    "ml_divide({left}, {right}, '{rounding}', {zero}, {remainder}, [{min}n, {max}n, {}])",
816                    json_string(overflow_message(op.name()))
817                )
818            }
819            BinaryOp::Plus => return Err(malformed("no JavaScript operator plus".to_owned())),
820        })
821    }
822
823    fn cast(&mut self, arg: &Expr, flavor: Flavor, message: Option<&str>) -> Result<String> {
824        let arg = self.expr(arg)?;
825        Ok(match flavor {
826            Flavor::Exact => arg,
827            Flavor::Clamp => format!("((value) => (value < 0n ? 0n : value))({arg})"),
828            Flavor::Checked => {
829                self.helpers.insert(Helper::ToNatChecked);
830                format!(
831                    "ml_toNatChecked({arg}, {})",
832                    json_string(cast_message(message))
833                )
834            }
835        })
836    }
837
838    fn main(&mut self, main: &Main) -> Result<String> {
839        let effects = rename_main(main, &ident, &self.state.local_reserved());
840        let mut lines = Vec::new();
841        let mut assertion = 0;
842        for effect in &effects {
843            match effect {
844                Effect::Print { expr, .. } => {
845                    lines.push(format!("console.log({});", self.expr(expr)?));
846                }
847                Effect::Let { name, value, .. } => {
848                    lines.push(format!("const {name} = {};", self.expr(value)?));
849                }
850                Effect::Assert { prop, .. } => {
851                    assertion += 1;
852                    self.helpers.insert(Helper::Assert);
853                    let label = format!("assertion {assertion}");
854                    lines.push(format!(
855                        "ml_assert({}, {});",
856                        self.prop(prop)?,
857                        json_string(&label)
858                    ));
859                    self.state.assertion_theorem(&label, effect);
860                }
861                Effect::Output { .. } | Effect::Unwrap { .. } => {
862                    unreachable!("only the Lean and Rocq emitters thread output")
863                }
864            }
865        }
866        if main.sequential_async {
867            self.state.encode(
868                "sequential-async",
869                "an async function is the function its body computes and await is its call: every call of one is awaited where it is made, so nothing runs concurrently and the output is the same, in the same order",
870            );
871        }
872        self.state.encode(
873            "program-output",
874            "main prints the lines the source program prints, in order, with console.log",
875        );
876        Ok(format!(
877            "function main() {{\n{}\n}}",
878            indent(&lines.join("\n"), 1)
879        ))
880    }
881}
882
883/// `-x`, parenthesised so that `-(-x)` does not read as a decrement.
884fn negate(text: &str) -> String {
885    if text.starts_with('-') {
886        format!("-({text})")
887    } else {
888        format!("-{text}")
889    }
890}
891
892fn literal(ty: &Type, value: &LitValue) -> Result<String> {
893    let text = value.text();
894    match ty {
895        Type::Nat | Type::Int | Type::Fixed { .. } => Ok(if text.starts_with('-') {
896            format!("({text}n)")
897        } else {
898            format!("{text}n")
899        }),
900        Type::Float => Ok(if text.starts_with('-') {
901            format!("({text})")
902        } else {
903            text
904        }),
905        Type::Bool => Ok(text),
906        Type::String => Ok(json_string(&text)),
907        other => Err(malformed(format!(
908            "no JavaScript literal for {}",
909            other.kind()
910        ))),
911    }
912}
meta_language/translation/emit_javascript.rs

meta_language/translation/
emit_javascript.rs
