meta_language/translation/
emit_rocq.rs

1//! The Rocq emitter: writes a checked program as Rocq with its translation contract.
2//!
3//! Naturals become binary `N` and integers `Z`, so programs run at their
4//! source sizes (unary `nat` cannot hold 20!). Structural recursion over data
5//! is a `Fixpoint`; recursion that decreases a natural is a `Function` with
6//! the measure `N.to_nat`, whose obligations `lia` discharges and whose
7//! equation lemma the reconstructed proofs rewrite with. A JavaScript Number
8//! is a primitive `float`, which the kernel computes with, so assertions about
9//! Numbers are still theorems closed by computation.
10//!
11//! Mirrors `js/src/translation/emit-rocq.js`.
12
13use std::collections::{HashMap, HashSet};
14use std::fmt::Write as _;
15use std::rc::Rc;
16
17use super::Language;
18use super::diagnostics::{ErrorKind, Result, TranslationError, unsupported};
19use super::emit_common::{
20    CtorStyle, EmitOptions, EmitState, Emitted, mutual_groups, order_declarations, unthreaded,
21};
22use super::ir::{
23    ByZero, Case, DataDecl, Decl, Effect, Expr, FnDecl, Hints, LitValue, Main, Node, Param,
24    Pattern, Plan, Program, Prop, Semantics, TheoremDecl, rename_function, rename_main,
25    rename_theorem,
26};
27use super::output::thread_output;
28use super::proof::prop_functions;
29use super::surface::{BinaryOp, Flavor, Rounding, UnaryOp};
30use super::types::Type;
31
32mod arrays;
33mod expressions;
34mod floats;
35mod math;
36mod mutual;
37mod proofs;
38
39use self::arrays::{FLOAT_INDEX, LIST_AT};
40pub use self::floats::FLOAT_PRELUDE;
41use self::floats::{FLOAT_REM, FLOAT_SAME, JS_CONSOLE, JS_NUMBER};
42use self::math::MATH;
43use self::mutual::Mutual;
44
45const KEYWORDS: &[&str] = &[
46    "as",
47    "at",
48    "cofix",
49    "else",
50    "end",
51    "exists",
52    "exists2",
53    "fix",
54    "for",
55    "forall",
56    "fun",
57    "if",
58    "IF",
59    "in",
60    "let",
61    "match",
62    "mod",
63    "Prop",
64    "return",
65    "Set",
66    "SProp",
67    "then",
68    "Type",
69    "using",
70    "where",
71    "with",
72    "struct",
73    "measure",
74    "wf",
75    "Definition",
76    "Fixpoint",
77    "Function",
78    "Theorem",
79    "Lemma",
80    "Proof",
81    "Qed",
82    "Defined",
83    "Module",
84    "End",
85    "Inductive",
86    "Import",
87    "Require",
88    "From",
89    "Open",
90    "Scope",
91    "Eval",
92    "Compute",
93    "Check",
94    "Print",
95    // Standard-library names the emitted code uses unqualified.
96    "N",
97    "Z",
98    "String",
99    "EmptyString",
100    "negb",
101    "andb",
102    "orb",
103    "true",
104    "false",
105    "bool",
106    "string",
107    "list",
108    "nil",
109    "cons",
110    "unit",
111    "tt",
112    "nat",
113    "O",
114    "S",
115    "Bool",
116    "Ascii",
117    "main",
118    "lia",
119    "nia",
120    "float",
121    "PrimFloat",
122    // Imported constructors: a pattern variable with one of these names would match the constructor instead.
123    "left",
124    "right",
125    "inleft",
126    "inright",
127    "Some",
128    "None",
129    "pair",
130    "inl",
131    "inr",
132    "exist",
133    "existT",
134    "I",
135    "conj",
136    "or_introl",
137    "or_intror",
138    "ex_intro",
139    "eq_refl",
140    "Eq",
141    "Lt",
142    "Gt",
143    "CompEq",
144    "CompLt",
145    "CompGt",
146    "xI",
147    "xO",
148    "xH",
149    "N0",
150    "Npos",
151    "Z0",
152    "Zpos",
153    "Zneg",
154    "ReflectT",
155    "ReflectF",
156    "identity_refl",
157];
158
159/// The `Require` lines every emitted file starts with.
160pub const ROCQ_PRELUDE: &[&str] =
161    &["From Stdlib Require Import NArith ZArith Lia Recdef String List Ascii."];
162
163const DIGITS: &str = r"Fixpoint ml_digits (fuel : nat) (n : N) (acc : string) : string :=
164  match fuel with
165  | O => acc
166  | S rest =>
167      let acc' := String (ascii_of_N (48 + N.modulo n 10)) acc in
168      if N.ltb n 10 then acc' else ml_digits rest (N.div n 10) acc'
169  end.
170Definition ml_N_to_string (n : N) : string := ml_digits (S (N.size_nat n)) n EmptyString.";
171
172const Z_TO_STRING: &str = r#"Definition ml_Z_to_string (z : Z) : string :=
173  if Z.ltb z 0 then String.append "-" (ml_N_to_string (Z.to_N (Z.opp z))) else ml_N_to_string (Z.to_N z)."#;
174
175const BOOL_TO_STRING: &str =
176    r#"Definition ml_bool_to_string (b : bool) : string := if b then "true" else "false"."#;
177
178const EUCLID: &str = r"(* Euclidean division, the rounding of Lean's Int / and %: the remainder is never negative. *)
179Definition ml_Z_ediv (a b : Z) : Z := Z.mul (Z.sgn b) (Z.div a (Z.abs b)).
180Definition ml_Z_emod (a b : Z) : Z := Z.modulo a (Z.abs b).";
181
182const TACTICS: &str = r"Ltac ml_N_norm := repeat first
183  [ rewrite N.pred_succ
184  | rewrite (proj2 (N.eqb_neq (N.succ _) 0) (N.neq_succ_0 _))
185  | rewrite N.eqb_refl ].
186Ltac ml_obligation := intros; repeat match goal with H : N.eqb _ _ = false |- _ => apply N.eqb_neq in H end; lia.
187Ltac ml_close := first [reflexivity | lia | nia | congruence].";
188
189// A closed assertion computes to connectives over literal (in)equalities:
190// prove the goal, or refute a hypothesis, one connective at a time.
191const DECIDE: &str = r#"Ltac ml_prove := first
192  [ reflexivity | discriminate | exact I | lia
193  | split; ml_prove
194  | left; ml_prove
195  | right; ml_prove
196  | let H := fresh "H" in intro H; first [ml_prove | ml_refute H] ]
197with ml_refute H := first
198  [ discriminate H | exact H | lia
199  | let A := fresh "H" in let B := fresh "H" in destruct H as [A B]; first [ml_refute A | ml_refute B]
200  | let A := fresh "H" in let B := fresh "H" in destruct H as [A | B]; [ml_refute A | ml_refute B]
201  | apply H; ml_prove ].
202Ltac ml_decide := vm_compute; ml_prove."#;
203
204const FIX: &str = "(* The least fixed point of a one-step unfolding F, unfolded lazily: level k
205   nests 2^k calls of F before it would reach the fallback. *)
206Fixpoint ml_fix {A B : Type} (k : nat) (F : (A -> B) -> A -> B) (fallback : A -> B) : A -> B :=
207  match k with
208  | O => F fallback
209  | S k => fun a => ml_fix k F (ml_fix k F fallback) a
210  end.";
211
212const EMIT: &str = "(* The lines a step of main prints, before the lines the rest of main prints
213   and the message of the abort that stops it, if one does. *)
214Definition ml_emit (lines : list string) (rest : list string * option string) : list string * option string :=
215  (app lines (fst rest), snd rest).";
216
217/// A helper definition the emitted program may need, in the order they are written out.
218#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
219enum Helper {
220    Digits,
221    ZToString,
222    BoolToString,
223    Euclid,
224    JsNumber,
225    JsConsole,
226    FloatSame,
227    FloatRem,
228    Math,
229    ListAt,
230    FloatIndex,
231    Fix,
232    Tactics,
233    Decide,
234    Emit,
235}
236
237impl Helper {
238    const ALL: [Self; 15] = [
239        Self::Digits,
240        Self::ZToString,
241        Self::BoolToString,
242        Self::Euclid,
243        Self::JsNumber,
244        Self::JsConsole,
245        Self::FloatSame,
246        Self::FloatRem,
247        Self::Math,
248        Self::ListAt,
249        Self::FloatIndex,
250        Self::Fix,
251        Self::Tactics,
252        Self::Decide,
253        Self::Emit,
254    ];
255
256    const fn text(self) -> &'static str {
257        match self {
258            Self::Digits => DIGITS,
259            Self::ZToString => Z_TO_STRING,
260            Self::BoolToString => BOOL_TO_STRING,
261            Self::Euclid => EUCLID,
262            Self::JsNumber => JS_NUMBER,
263            Self::JsConsole => JS_CONSOLE,
264            Self::FloatSame => FLOAT_SAME,
265            Self::FloatRem => FLOAT_REM,
266            Self::Math => MATH,
267            Self::ListAt => LIST_AT,
268            Self::FloatIndex => FLOAT_INDEX,
269            Self::Fix => FIX,
270            Self::Tactics => TACTICS,
271            Self::Decide => DECIDE,
272            Self::Emit => EMIT,
273        }
274    }
275}
276
277fn ident(name: &str) -> String {
278    let mut result: String = name
279        .chars()
280        .map(|c| {
281            if c.is_ascii_alphanumeric() || c == '_' || c == '\'' {
282                c
283            } else {
284                '_'
285            }
286        })
287        .collect();
288    if result.starts_with(|c: char| c.is_ascii_digit() || c == '\'') {
289        result = format!("x{result}");
290    }
291    if KEYWORDS.contains(&result.as_str()) {
292        result.push('_');
293    }
294    result
295}
296
297/// Rocq derives these from inductives and Functions in the same namespace.
298fn generated(name: &str) -> Vec<String> {
299    [
300        "_ind",
301        "_rect",
302        "_rec",
303        "_sind",
304        "_equation",
305        "_tcc",
306        "_terminate",
307        "_F",
308        "_graph",
309        "_complete",
310        "_correct",
311        "_ind_",
312        "_rect_",
313    ]
314    .iter()
315    .map(|suffix| format!("{name}{suffix}"))
316    .chain(std::iter::once(format!("R_{name}")))
317    .collect()
318}
319
320/// An error the JavaScript emitter raises with a plain `Error`: the checker never produces its input.
321fn internal(message: String) -> TranslationError {
322    TranslationError::new(ErrorKind::Type, message, None)
323}
324
325/// Emits a checked program as Rocq.
326///
327/// # Errors
328/// On constructs the target cannot express faithfully.
329pub fn emit_rocq(source: &Program) -> Result<Emitted> {
330    let program = &*thread_output(source)?;
331    let state = EmitState::new(
332        program,
333        Language::Rocq,
334        ident,
335        KEYWORDS,
336        EmitOptions {
337            ctor_style: CtorStyle::Module,
338            generated: Some(generated),
339            ..EmitOptions::default()
340        },
341    );
342    RocqEmitter {
343        program,
344        state,
345        helpers: HashSet::from([Helper::Tactics]),
346        nat_functions: HashMap::new(),
347        current: None,
348        uses_float: false,
349    }
350    .file()
351}
352
353/// The function being emitted, so its recursive calls use its local name.
354struct Current {
355    full_name: String,
356    name: String,
357    recursive: bool,
358    /// Recursive with no termination argument: self-calls go through `ml_fix`.
359    general: bool,
360    /// Recursive on a natural through more than one threaded self-call: self-calls spend `ml_fuel`.
361    fuel: bool,
362    /// A member of a mutually recursive group: calls of the group go through `ml_rec`.
363    mutual: Option<Rc<Mutual>>,
364}
365
366struct RocqEmitter<'p> {
367    program: &'p Program,
368    state: EmitState<'p>,
369    helpers: HashSet<Helper>,
370    /// Functions recursive on a natural: the decreasing parameter and the arity.
371    nat_functions: HashMap<String, (usize, usize)>,
372    current: Option<Current>,
373    uses_float: bool,
374}
375
376impl RocqEmitter<'_> {
377    fn file(mut self) -> Result<Emitted> {
378        let program = self.program;
379        let mut blocks: Vec<String> = Vec::new();
380        let order = order_declarations(program, true)?;
381        let mut open_modules: Vec<String> = Vec::new();
382        let groups = mutual_groups(program);
383        for entry in order {
384            self.move_to(&mut open_modules, entry.module_path(), &mut blocks);
385            blocks.push(match (entry, groups.get(entry.full_name())) {
386                (_, Some(group)) if std::ptr::eq(group[0], entry) => self.mutual(group)?,
387                (_, Some(_)) => continue,
388                (Decl::Data(data), None) => self.data(entry, data)?,
389                (Decl::Fn(function), None) => self.function(entry, function)?,
390                (Decl::Theorem(theorem), None) => self.theorem(entry, theorem)?,
391            });
392        }
393        self.move_to(&mut open_modules, &[], &mut blocks);
394        let main_text = match &program.main {
395            Some(main) => Some(self.main(main)?),
396            None => None,
397        };
398        let helper_text = Helper::ALL.into_iter().filter(|helper| {
399            self.helpers.contains(helper)
400                || (*helper == Helper::Digits
401                    && (self.helpers.contains(&Helper::ZToString)
402                        || self.helpers.contains(&Helper::JsNumber)))
403        });
404        let mut lines: Vec<String> = vec![format!(
405            "(* Translated from {} by meta-language: portable core, Rocq target. *)",
406            program.source_language.as_str()
407        )];
408        let prelude = if self.uses_float {
409            FLOAT_PRELUDE
410        } else {
411            ROCQ_PRELUDE
412        };
413        lines.extend(prelude.iter().map(|line| (*line).to_owned()));
414        lines.push(String::new());
415        for helper in helper_text {
416            lines.push(helper.text().to_owned());
417            lines.push(String::new());
418        }
419        for block in blocks {
420            lines.push(block);
421            lines.push(String::new());
422        }
423        let entry = main_text.as_ref().map(|_| "main".to_owned());
424        if let Some(main_text) = main_text {
425            lines.push(main_text);
426            lines.push(String::new());
427            lines.push("Eval vm_compute in main.".to_owned());
428            lines.push(String::new());
429        }
430        Ok(self.state.finish(lines.join("\n"), entry))
431    }
432
433    /// Closes and opens `Module` blocks until `path` is the open module.
434    fn move_to(&self, open_modules: &mut Vec<String>, path: &[String], blocks: &mut Vec<String>) {
435        let common = open_modules
436            .iter()
437            .zip(path)
438            .take_while(|(open, wanted)| open == wanted)
439            .count();
440        while open_modules.len() > common {
441            blocks.push(format!("End {}.", self.module_name(open_modules)));
442            open_modules.pop();
443        }
444        while open_modules.len() < path.len() {
445            open_modules.push(path[open_modules.len()].clone());
446            blocks.push(format!("Module {}.", self.module_name(open_modules)));
447        }
448    }
449
450    fn module_name(&self, path: &[String]) -> &str {
451        self.state.module_name(path).unwrap_or("undefined")
452    }
453
454    fn ty(&mut self, ty: &Type) -> Result<String> {
455        Ok(match ty {
456            Type::Nat => "N".to_owned(),
457            Type::Int => "Z".to_owned(),
458            Type::Fixed { signed, .. } => {
459                self.state
460                    .machine_integer(ty, if *signed { "Z" } else { "N" });
461                if *signed { "Z" } else { "N" }.to_owned()
462            }
463            Type::Float => {
464                self.floats();
465                "float".to_owned()
466            }
467            Type::Bool => "bool".to_owned(),
468            Type::String => "string".to_owned(),
469            Type::Unit => "unit".to_owned(),
470            Type::Output => "list string".to_owned(),
471            Type::Data { name } => self.state.reference(name, "."),
472            Type::Array { element } => {
473                self.state.encode(
474                    "arrays",
475                    "a JavaScript array, which the portable core never mutates, is a Rocq list; a read walks it to the index",
476                );
477                format!("(list {})", self.ty(element)?)
478            }
479            other => return Err(internal(format!("no Rocq type for {}", other.kind()))),
480        })
481    }
482
483    fn data(&mut self, entry: &Decl, data: &DataDecl) -> Result<String> {
484        fn lists(ty: &Type) -> bool {
485            ty.element()
486                .is_some_and(|element| matches!(element, Type::Data { .. }) || lists(element))
487        }
488        let name = self.state.local_name(&data.full_name).to_owned();
489        let mut lines = vec![format!("Inductive {name} : Type :=")];
490        for ctor in &data.ctors {
491            let mut fields = String::new();
492            for field in &ctor.fields {
493                fields.push_str(&self.ty(&field.ty)?);
494                fields.push_str(" -> ");
495            }
496            let local = self.state.ctor_local(&data.full_name, &ctor.name);
497            lines.push(format!("| {local} : {fields}{name}"));
498        }
499        self.state.map(entry, &name);
500        // A type nested through list has no registered All scheme, which Rocq would warn of on every definition.
501        let nested = data
502            .ctors
503            .iter()
504            .any(|ctor| ctor.fields.iter().any(|field| lists(&field.ty)));
505        if nested {
506            lines.insert(0, "#[warnings=\"-register-all\"]".to_owned());
507        }
508        Ok(lines.join("\n") + ".")
509    }
510
511    /// Recursion that decreases a natural by one each call, in a function whose
512    /// output or abort is threaded, is a structural fixpoint over a fuel one more
513    /// than the natural: every call spends one fuel and decreases the natural, so
514    /// the fuel never runs out before the natural reaches zero.
515    #[allow(clippy::too_many_arguments)]
516    fn fuel_recursion(
517        &mut self,
518        name: &str,
519        params: &[Param],
520        binders: &str,
521        result: &str,
522        text: &str,
523        decreasing: &str,
524        ret: &Type,
525    ) -> Result<String> {
526        self.state.encode(
527            "nat-fuel-recursion",
528            "a threaded function that decreases a natural through more than one call is a fixpoint over a fuel of one more than the natural, which every call spends as it decreases the natural, so the fuel outlasts every run",
529        );
530        let args: Vec<&str> = params.iter().map(|param| param.name.as_str()).collect();
531        Ok(format!(
532            "Definition {name}{binders} : {result} :=\n  (fix ml_go (ml_fuel : nat){binders} {{struct ml_fuel}} : {result} :=\n    match ml_fuel with\n    | O => {}\n    | S ml_fuel => {text}\n    end) (S (N.to_nat {decreasing})) {}.",
533            self.inhabitant(ret)?,
534            args.join(" ")
535        ))
536    }
537
538    /// Recursion with no termination argument Rocq could check is `ml_fix`
539    /// applied to the function's one-step unfolding: the parameters travel as
540    /// one tuple, a self-call is a call of `ml_rec`, and a run nested deeper
541    /// than 2^64 calls, which no machine reaches, would fall back to an inhabitant.
542    fn general_recursion(
543        &mut self,
544        name: &str,
545        params: &[Param],
546        binders: &str,
547        result: &str,
548        text: &str,
549        ret: &Type,
550    ) -> Result<String> {
551        self.helpers.insert(Helper::Fix);
552        self.state.encode(
553            "general-recursion",
554            "recursion without a termination argument Rocq could check is ml_fix over the function's one-step unfolding, which unfolds lazily to 2^64 nested calls: every run that terminates computes the same value, and Rocq accepts it as a plain Definition",
555        );
556        let mut domain = Vec::new();
557        for param in params {
558            domain.push(self.ty(&param.ty)?);
559        }
560        let domain = if domain.is_empty() {
561            "unit".to_owned()
562        } else {
563            domain.join(" * ")
564        };
565        let names: Vec<&str> = params.iter().map(|param| param.name.as_str()).collect();
566        let tuple = format!("({})", names.join(", "));
567        let (input, unpack, args) = match names.as_slice() {
568            [] => ("_", String::new(), "tt"),
569            [only] => (*only, String::new(), *only),
570            _ => (
571                "ml_args",
572                format!("let '{tuple} := ml_args in "),
573                tuple.as_str(),
574            ),
575        };
576        Ok(format!(
577            "Definition {name}{binders} : {result} :=\n  ml_fix 64 (fun (ml_rec : {domain} -> {result}) ({input} : {domain}) =>\n    {unpack}{text})\n    (fun _ => {}) {args}.",
578            self.inhabitant(ret)?
579        ))
580    }
581
582    fn function(&mut self, entry: &Decl, function: &FnDecl) -> Result<String> {
583        let (params, body) = rename_function(function, &ident, &self.state.local_reserved());
584        let name = self.state.local_name(&function.full_name).to_owned();
585        self.state.map(entry, &name);
586        let general = function.recursive && function.decreasing.is_none() && !function.mutual;
587        // A threaded function calling itself more than once matches on one call's pair around the next, whose equation Function cannot generate.
588        let fuel = !general
589            && function.recursive
590            && !function.mutual
591            && !function
592                .decreasing
593                .and_then(|index| params.get(index))
594                .is_some_and(|param| matches!(param.ty, Type::Data { .. }))
595            && matches!(&function.ret, Type::Data { name: ret } if matches!(self.program.declaration(ret), Some(Decl::Data(data)) if data.output))
596            && self_calls(&body, &function.full_name) > 1;
597        self.current = Some(Current {
598            full_name: function.full_name.clone(),
599            name: name.clone(),
600            recursive: function.recursive,
601            general,
602            fuel,
603            mutual: None,
604        });
605        let mut binders = String::new();
606        for param in &params {
607            let ty = self.ty(&param.ty)?;
608            let _ = write!(binders, " ({} : {ty})", param.name);
609        }
610        let result = self.ty(&function.ret)?;
611        let text = self.expr(&body)?;
612        self.current = None;
613        if !function.recursive {
614            return Ok(format!(
615                "Definition {name}{binders} : {result} :=\n  {text}."
616            ));
617        }
618        let Some(index) = function.decreasing else {
619            return self.general_recursion(&name, &params, &binders, &result, &text, &function.ret);
620        };
621        let decreasing = &params[index];
622        if matches!(decreasing.ty, Type::Data { .. }) {
623            return Ok(format!(
624                "Fixpoint {name}{binders} {{struct {}}} : {result} :=\n  {text}.",
625                decreasing.name
626            ));
627        }
628        if fuel {
629            return self.fuel_recursion(
630                &name,
631                &params,
632                &binders,
633                &result,
634                &text,
635                &decreasing.name,
636                &function.ret,
637            );
638        }
639        self.nat_functions
640            .insert(function.full_name.clone(), (index, params.len()));
641        self.state.encode(
642            "nat-recursion",
643            "recursion that decreases a natural is a Rocq Function with measure N.to_nat; lia discharges the decrease obligations",
644        );
645        Ok(format!(
646            "Function {name}{binders} {{measure N.to_nat {}}} : {result} :=\n  {text}.\nProof. all: ml_obligation. Defined.",
647            decreasing.name
648        ))
649    }
650}
651
652/// The operator's name as the checked program spells it.
653const fn op_name(op: BinaryOp) -> &'static str {
654    match op {
655        BinaryOp::Add => "add",
656        BinaryOp::Sub => "sub",
657        BinaryOp::Mul => "mul",
658        BinaryOp::Div => "div",
659        BinaryOp::Rem => "rem",
660        BinaryOp::Eq => "eq",
661        BinaryOp::Ne => "ne",
662        BinaryOp::Lt => "lt",
663        BinaryOp::Le => "le",
664        BinaryOp::Gt => "gt",
665        BinaryOp::Ge => "ge",
666        BinaryOp::And => "and",
667        BinaryOp::Or => "or",
668        BinaryOp::Concat => "concat",
669        BinaryOp::Plus => "plus",
670    }
671}
672
673/// How many times a function body calls the function itself.
674fn self_calls(node: &Expr, name: &str) -> usize {
675    let own = usize::from(matches!(&node.node, Node::Call { func, .. } if func == name));
676    own + node
677        .children()
678        .into_iter()
679        .map(|child| self_calls(child, name))
680        .sum::<usize>()
681}
682
683fn collect_hint_functions(plan: &Plan) -> Vec<&String> {
684    match plan {
685        Plan::Close { hints } => hints.unfold.iter().collect(),
686        Plan::Induction(split) | Plan::Cases(split) => split
687            .cases
688            .iter()
689            .flat_map(|kase| collect_hint_functions(&kase.plan))
690            .collect(),
691    }
692}
meta_language/translation/emit_rocq.rs

meta_language/translation/
emit_rocq.rs
