meta_language/translation/
rocq.rs

1//! The Rocq frontend for the portable core.
2//!
3//! It reads the vernacular subset the core can represent faithfully:
4//! modules, inductive types, `Definition`, `Fixpoint` and measure-based
5//! `Function` declarations over `nat`, `N`, `Z`, `bool` and `string`,
6//! theorems with their tactic structure, and a program
7//! `Definition main : list string` whose elements are the lines the program
8//! prints. Everything else is rejected with a precise obligation.
9//!
10//! Mirrors `js/src/translation/rocq.js`.
11
12use std::collections::HashMap;
13
14use super::diagnostics::{Result, TranslationError, type_error, unsupported};
15use super::lexer::{Source, Token, TokenCursor, TokenKind, describe, is_js_space, tokenize_source};
16use super::surface::{
17    BinaryOp, Flavor, Rounding, SBinder, SComparison, SCtor, SData, SEffect, SExpr, SField, SFn,
18    SItem, SMain, SModule, SNode, SParam, SPattern, SPatternNode, SProgram, SProof, SProp,
19    SPropNode, SRow, SRule, SSplit, SSplitCase, SStep, STheorem, ShowStyle, UnaryOp,
20};
21use super::types::{BOOL, INT, NAT, STRING, Type, UNIT};
22use super::{Language, Span};
23
24mod portable;
25mod proofs;
26mod terms;
27mod vernacular;
28use self::portable::{
29    check_portable, collect_forall_types, pattern_value, scope_prop, walk_output, with_scope,
30};
31
32const THEOREM_KEYWORDS: &[&str] = &[
33    "Theorem",
34    "Lemma",
35    "Example",
36    "Fact",
37    "Remark",
38    "Corollary",
39    "Proposition",
40];
41const UNSUPPORTED_COMMANDS: &[&str] = &[
42    "Section",
43    "Variable",
44    "Variables",
45    "Hypothesis",
46    "Context",
47    "Record",
48    "Structure",
49    "Class",
50    "Instance",
51    "CoInductive",
52    "CoFixpoint",
53    "Axiom",
54    "Parameter",
55    "Notation",
56    "Infix",
57    "Ltac",
58    "Program",
59    "Let",
60    "Arguments",
61    "Hint",
62    "Set",
63    "Unset",
64    "Global",
65    "Local",
66    "Module Type",
67    "Include",
68    "Export",
69    "Canonical",
70    "Coercion",
71    "Scheme",
72    "Equations",
73    "Declare",
74];
75const EXPRESSION_STOP: &[&str] = &["then", "else", "with", "end", "in", "as", "return"];
76const EVAL_STRATEGIES: &[&str] = &[
77    "vm_compute",
78    "compute",
79    "cbv",
80    "lazy",
81    "native_compute",
82    "cbn",
83    "simpl",
84];
85
86fn builtin_type(name: &str) -> Option<Type> {
87    match name {
88        "nat" | "N" => Some(NAT),
89        "Z" => Some(INT),
90        "bool" => Some(BOOL),
91        "string" => Some(STRING),
92        "unit" => Some(UNIT),
93        _ => None,
94    }
95}
96
97/// Rocq types with no portable counterpart.
98const OUTSIDE_CORE_TYPES: &[&str] = &[
99    "list",
100    "option",
101    "prod",
102    "sum",
103    "positive",
104    "ascii",
105    "Type",
106    "Set",
107    "Prop",
108    "sig",
109    "sigT",
110    "Q",
111    "R",
112    "vector",
113    "int",
114    "uint",
115    "float",
116    "PrimInt63.int",
117    "Uint63.int",
118];
119
120// Library functions of the portable core, by Rocq name. Rounding follows
121// the Stdlib definition: `Z.div`/`Z.modulo` floor, `Z.quot`/`Z.rem` truncate,
122// and the natural-number divisions are total with `x / 0 = 0`.
123fn binary_function(name: &str) -> Option<(BinaryOp, Option<Rounding>)> {
124    Some(match name {
125        "N.add" | "Z.add" | "Nat.add" | "plus" => (BinaryOp::Add, None),
126        "N.sub" | "Z.sub" | "Nat.sub" | "minus" => (BinaryOp::Sub, None),
127        "N.mul" | "Z.mul" | "Nat.mul" | "mult" => (BinaryOp::Mul, None),
128        "N.div" | "Nat.div" => (BinaryOp::Div, None),
129        "Z.div" => (BinaryOp::Div, Some(Rounding::Floor)),
130        "N.modulo" | "Nat.modulo" => (BinaryOp::Rem, None),
131        "Z.modulo" => (BinaryOp::Rem, Some(Rounding::Floor)),
132        "Z.quot" => (BinaryOp::Div, Some(Rounding::Trunc)),
133        "Z.rem" => (BinaryOp::Rem, Some(Rounding::Trunc)),
134        "N.eqb" | "Z.eqb" | "Nat.eqb" | "String.eqb" | "Bool.eqb" | "eqb" => (BinaryOp::Eq, None),
135        "N.ltb" | "Z.ltb" | "Nat.ltb" => (BinaryOp::Lt, None),
136        "N.leb" | "Z.leb" | "Nat.leb" => (BinaryOp::Le, None),
137        "Z.gtb" => (BinaryOp::Gt, None),
138        "Z.geb" => (BinaryOp::Ge, None),
139        "andb" => (BinaryOp::And, None),
140        "orb" => (BinaryOp::Or, None),
141        "String.append" => (BinaryOp::Concat, None),
142        _ => return None,
143    })
144}
145
146const NAT_TO_INT: &[&str] = &["Z.of_N", "Z.of_nat"];
147const INT_TO_NAT: &[&str] = &["Z.to_N", "Z.to_nat"];
148const NAT_IDENTITY: &[&str] = &["N.of_nat", "N.to_nat", "Nat.of_N"];
149const PREDECESSOR: &[&str] = &["N.pred", "Nat.pred", "pred", "Z.pred"];
150const SUCCESSOR: &[&str] = &["N.succ", "Nat.succ", "S", "Z.succ"];
151// `NilEmpty.string_of_uint (N.to_uint n)` and `NilZero.string_of_int
152// (Z.to_int z)` are the Stdlib's decimal renderings, the same text as the
153// other languages' number printing.
154const DECIMAL_STRINGS: &[(&str, &[&str])] = &[
155    ("NilEmpty.string_of_uint", &["N.to_uint", "Nat.to_uint"]),
156    (
157        "DecimalString.NilEmpty.string_of_uint",
158        &["N.to_uint", "Nat.to_uint"],
159    ),
160    ("NilZero.string_of_int", &["Z.to_int"]),
161    ("DecimalString.NilZero.string_of_int", &["Z.to_int"]),
162];
163
164/// `/^(?:N|Z|Nat|String|Pos|List|Bool|Ascii)\./`: the Stdlib modules whose
165/// other functions are outside the portable core.
166fn outside_core(name: &str) -> bool {
167    ["N", "Z", "Nat", "String", "Pos", "List", "Bool", "Ascii"]
168        .iter()
169        .any(|module| {
170            name.strip_prefix(module)
171                .is_some_and(|rest| rest.starts_with('.'))
172        })
173}
174
175/// `/^(?:N|Z|Nat)\.to_u?int$/`: the decimal conversions `DECIMAL_STRINGS` consume.
176fn decimal_conversion(name: &str) -> bool {
177    matches!(
178        name,
179        "N.to_int" | "N.to_uint" | "Z.to_int" | "Z.to_uint" | "Nat.to_int" | "Nat.to_uint"
180    )
181}
182
183/// The names `measureFn in {}` finds on `Object.prototype` (Node 24).
184fn object_prototype_key(name: &str) -> bool {
185    matches!(
186        name,
187        "constructor"
188            | "__defineGetter__"
189            | "__defineSetter__"
190            | "hasOwnProperty"
191            | "__lookupGetter__"
192            | "__lookupSetter__"
193            | "isPrototypeOf"
194            | "propertyIsEnumerable"
195            | "toString"
196            | "valueOf"
197            | "__proto__"
198            | "toLocaleString"
199    )
200}
201
202/// Levels 50 (`|| + -`) and 40 (`&& * / mod`) of the notation table.
203fn notation(level: u32, token: &Token) -> Option<BinaryOp> {
204    if token.kind != TokenKind::Punct && token.value != "mod" {
205        return None;
206    }
207    match (level, token.value.as_str()) {
208        (50, "||") => Some(BinaryOp::Or),
209        (50, "+") => Some(BinaryOp::Add),
210        (50, "-") => Some(BinaryOp::Sub),
211        (40, "&&") => Some(BinaryOp::And),
212        (40, "*") => Some(BinaryOp::Mul),
213        (40, "/") => Some(BinaryOp::Div),
214        (40, "mod") => Some(BinaryOp::Rem),
215        _ => None,
216    }
217}
218
219fn boolean_relation(value: &str) -> Option<BinaryOp> {
220    match value {
221        "=?" => Some(BinaryOp::Eq),
222        "<?" => Some(BinaryOp::Lt),
223        "<=?" => Some(BinaryOp::Le),
224        _ => None,
225    }
226}
227
228fn prop_relation(value: &str, comparison: SComparison) -> Option<SPropNode> {
229    Some(match value {
230        "=" => SPropNode::Eq(comparison),
231        "<>" => SPropNode::Ne(comparison),
232        "<" => SPropNode::Lt(comparison),
233        "<=" => SPropNode::Le(comparison),
234        ">" => SPropNode::Gt(comparison),
235        ">=" => SPropNode::Ge(comparison),
236        _ => return None,
237    })
238}
239
240fn is_prop_relation(value: &str) -> bool {
241    matches!(value, "=" | "<>" | "<" | "<=" | ">" | ">=")
242}
243
244fn scope_type(scope: &str) -> Option<Type> {
245    match scope {
246        "N" | "nat" => Some(NAT),
247        "Z" => Some(INT),
248        _ => None,
249    }
250}
251
252/// Reads a Rocq program.
253///
254/// # Errors
255/// On syntax errors and on constructs outside the portable core.
256pub fn parse_rocq(source: &str) -> Result<SProgram> {
257    let source = Source::new(source);
258    let tokens = tokenize_source(&source, Language::Rocq)?.tokens;
259    RocqParser {
260        cursor: TokenCursor::new(tokens, Language::Rocq),
261        source,
262    }
263    .file()
264}
265
266/// A `Definition`, `Fixpoint` or `Function`: a function, or the program output.
267enum Definition {
268    Fn(Box<SFn>),
269    Main(SMain, Span),
270}
271
272#[derive(Clone, Copy, PartialEq, Eq)]
273enum Annotation {
274    Struct,
275    Measure,
276}
277
278/// A run of adjacent `-`, `+` or `*` tokens.
279struct Bullet {
280    text: String,
281    length: usize,
282    depth: usize,
283}
284
285/// Whether a proof block has reached its end.
286type Done<'a> = &'a dyn Fn(&RocqParser) -> bool;
287
288/// Rocq names each proof variable's type as written, which proof steps consult.
289type ProofTypes = HashMap<String, String>;
290
291struct RocqParser {
292    cursor: TokenCursor,
293    source: Source,
294}
295
296impl RocqParser {
297    fn fail(message: &str, token: &Token) -> TranslationError {
298        TranslationError::syntax(
299            format!("{message} but found {}", describe(token)),
300            Some(token.span()),
301        )
302    }
303
304    fn fail_here(&self, message: &str) -> TranslationError {
305        Self::fail(message, self.cursor.peek())
306    }
307
308    fn peek(&self) -> &Token {
309        self.cursor.peek()
310    }
311
312    fn is(&self, value: &str) -> bool {
313        self.cursor.is(value)
314    }
315
316    /// `cursor.expect`, where an empty context (a JavaScript falsy string) is none.
317    fn expect(&mut self, value: &str, context: &str) -> Result<Token> {
318        self.cursor.expect(value, context_of(context))
319    }
320
321    fn identifier(&mut self, context: &str) -> Result<Token> {
322        self.cursor.identifier(context_of(context))
323    }
324
325    /// The `.` that ends a sentence.
326    fn end_sentence(&mut self, context: &str) -> Result<()> {
327        self.expect(".", context).map(drop)
328    }
329}
330
331/// A JavaScript context string: the empty string counts as none.
332fn context_of(context: &str) -> Option<&str> {
333    (!context.is_empty()).then_some(context)
334}
335
336/// The arguments of a library function of fixed arity.
337fn arity<const N: usize>(name: &str, args: Vec<SExpr>, range: Span) -> Result<[SExpr; N]> {
338    let count = args.len();
339    <[SExpr; N]>::try_from(args).map_err(|_| {
340        if count < N {
341            unsupported(
342                "partial application",
343                &format!("{name} expects {N} arguments"),
344                Some(range),
345            )
346        } else {
347            type_error(
348                format!("{name} expects {N} arguments but got {count}"),
349                Some(range),
350            )
351        }
352    })
353}
354
355/// A proposition connective, which carries no span.
356const fn connective(node: SPropNode) -> SProp {
357    SProp { node, span: None }
358}
359
360fn unreachable_relation(value: &str) -> SPropNode {
361    unreachable!("{value} is a proposition relation")
362}
363
364fn binary(op: BinaryOp, left: SExpr, right: SExpr, token: &Token) -> SExpr {
365    let binary_span = joined(&left, &right, token);
366    SExpr::new(
367        SNode::Binary {
368            op,
369            left: Box::new(left),
370            right: Box::new(right),
371            rounding: None,
372        },
373        Some(binary_span),
374    )
375}
376
377/// `String.prototype.trim` of `source.slice(start, end)`.
378fn js_trim(source: &Source, start: usize, end: usize) -> String {
379    let units = source.units();
380    let end = end.min(units.len());
381    let mut first = start.min(end);
382    let mut last = end;
383    while first < last && is_js_space(units[first]) {
384        first += 1;
385    }
386    while last > first && is_js_space(units[last - 1]) {
387        last -= 1;
388    }
389    source.slice(first, last)
390}
391
392fn joined(left: &SExpr, right: &SExpr, token: &Token) -> Span {
393    Span {
394        start: left.span.map_or(token.start, |span| span.start),
395        end: right.span.map_or(token.end, |span| span.end),
396    }
397}
398
399/// From the start of `from` to the start of `to` (or the end of `from`, when
400/// `to` is the end of input or precedes it).
401fn span(from: &Token, to: &Token) -> Span {
402    let end = if to.kind == TokenKind::Eof {
403        from.end
404    } else {
405        to.start
406    };
407    Span {
408        start: from.start,
409        end: from.end.max(end),
410    }
411}
meta_language/translation/rocq.rs

meta_language/translation/
rocq.rs
