meta_language/translation/
lean.rs

1//! The Lean 4 frontend for the portable core.
2//!
3//! It reads the layout-sensitive subset that the core can represent
4//! faithfully: namespaces, inductive types, definitions (including
5//! equation-compiler style), `match`, `if`, `let`, theorems with their tactic
6//! structure, and a `main : IO Unit` of `IO.println` effects. Everything else
7//! is rejected with a precise obligation.
8//!
9//! Mirrors `js/src/translation/lean.js`.
10
11use super::diagnostics::{Result, TranslationError, type_error, unsupported};
12use super::lexer::{Source, Token, TokenCursor, TokenKind, describe, is_js_space, tokenize_source};
13use super::surface::{
14    BinaryOp, SBinder, SComparison, SCtor, SData, SEffect, SExpr, SField, SFn, SItem, SMain,
15    SModule, SNode, SParam, SPattern, SPatternNode, SProgram, SProp, SPropNode, ShowStyle,
16};
17use super::types::{BOOL, INT, NAT, STRING, Type, UNIT};
18use super::{Language, Span};
19
20mod expressions;
21mod proofs;
22
23const ITEM_KEYWORDS: [&str; 28] = [
24    "namespace",
25    "end",
26    "inductive",
27    "def",
28    "theorem",
29    "lemma",
30    "structure",
31    "class",
32    "instance",
33    "abbrev",
34    "open",
35    "section",
36    "variable",
37    "universe",
38    "import",
39    "mutual",
40    "partial",
41    "private",
42    "protected",
43    "noncomputable",
44    "set_option",
45    "example",
46    "axiom",
47    "opaque",
48    "macro",
49    "syntax",
50    "notation",
51    "attribute",
52];
53
54fn is_item_keyword(value: &str) -> bool {
55    ITEM_KEYWORDS.contains(&value)
56}
57
58fn builtin_type(name: &str) -> Option<Type> {
59    match name {
60        "Nat" => Some(NAT),
61        "Int" => Some(INT),
62        "Bool" => Some(BOOL),
63        "String" => Some(STRING),
64        "Unit" => Some(UNIT),
65        _ => None,
66    }
67}
68
69/// Lean types the portable core has no counterpart for.
70fn is_unsupported_type(name: &str) -> bool {
71    let fixed = name
72        .strip_prefix('U')
73        .unwrap_or(name)
74        .strip_prefix("Int")
75        .is_some_and(|bits| matches!(bits, "8" | "16" | "32" | "64"));
76    fixed
77        || matches!(
78            name,
79            "USize" | "Float" | "Char" | "List" | "Array" | "Option" | "Prop" | "Type" | "Sort"
80        )
81}
82
83struct Level {
84    ops: &'static [&'static str],
85    prec: u32,
86    op: Option<BinaryOp>,
87    right: bool,
88}
89
90const BINARY: [Level; 6] = [
91    Level {
92        ops: &["||"],
93        prec: 30,
94        op: Some(BinaryOp::Or),
95        right: false,
96    },
97    Level {
98        ops: &["&&"],
99        prec: 35,
100        op: Some(BinaryOp::And),
101        right: false,
102    },
103    Level {
104        ops: &["==", "!=", "=", "≠", "<", "<=", "≤", ">", ">=", "≥"],
105        prec: 50,
106        op: None,
107        right: false,
108    },
109    Level {
110        ops: &["++"],
111        prec: 65,
112        op: Some(BinaryOp::Concat),
113        right: true,
114    },
115    Level {
116        ops: &["+", "-"],
117        prec: 65,
118        op: None,
119        right: false,
120    },
121    Level {
122        ops: &["*", "/", "%"],
123        prec: 70,
124        op: None,
125        right: false,
126    },
127];
128
129fn operator_name(op: &str) -> Option<BinaryOp> {
130    Some(match op {
131        "==" | "=" => BinaryOp::Eq,
132        "!=" | "≠" => BinaryOp::Ne,
133        "<" => BinaryOp::Lt,
134        "<=" | "≤" => BinaryOp::Le,
135        ">" => BinaryOp::Gt,
136        ">=" | "≥" => BinaryOp::Ge,
137        "+" => BinaryOp::Add,
138        "-" => BinaryOp::Sub,
139        "*" => BinaryOp::Mul,
140        "/" => BinaryOp::Div,
141        "%" => BinaryOp::Rem,
142        _ => return None,
143    })
144}
145
146type Relation = fn(SComparison) -> SPropNode;
147
148fn prop_relation(op: &str) -> Option<Relation> {
149    Some(match op {
150        "=" => SPropNode::Eq,
151        "≠" => SPropNode::Ne,
152        "<" => SPropNode::Lt,
153        "≤" | "<=" => SPropNode::Le,
154        ">" => SPropNode::Gt,
155        "≥" | ">=" => SPropNode::Ge,
156        _ => return None,
157    })
158}
159
160/// Reads a Lean program.
161///
162/// # Errors
163/// On syntax errors and on constructs outside the portable core.
164pub fn parse_lean(source: &str) -> Result<SProgram> {
165    let source = Source::new(source);
166    let mut tokens = tokenize_source(&source, Language::Lean)?.tokens;
167    annotate_layout(&mut tokens, source.units());
168    LeanParser::new(tokens, &source).file()
169}
170
171/// Fills in each token's line, column and whether it starts its line.
172pub fn annotate_layout(tokens: &mut [Token], source: &[u16]) {
173    let mut line = 0;
174    let mut line_start = 0;
175    let mut cursor = 0;
176    let mut previous_line = None;
177    for token in tokens {
178        while cursor < token.start {
179            if source.get(cursor) == Some(&u16::from(b'\n')) {
180                line += 1;
181                line_start = cursor + 1;
182            }
183            cursor += 1;
184        }
185        token.line = line;
186        token.col = token.start - line_start;
187        token.first = previous_line != Some(line);
188        previous_line = Some(line);
189    }
190}
191
192/// The range from `from` up to the start of `to` (the end of input adds nothing).
193#[must_use]
194pub fn span(from: &Token, to: &Token) -> Span {
195    let reach = if to.kind == TokenKind::Eof {
196        from.end
197    } else {
198        to.start
199    };
200    Span::new(from.start, from.end.max(reach))
201}
202
203/// A token's column, comparable with the `-1` that no column reaches.
204fn column(token: &Token) -> i64 {
205    i64::try_from(token.col).unwrap_or(i64::MAX)
206}
207
208fn syntax_at(message: String, token: &Token) -> TranslationError {
209    TranslationError::syntax(message, Some(token.span()))
210}
211
212/// `source.slice(start, end).trim()` as JavaScript trims.
213fn js_trimmed(units: &[u16]) -> String {
214    let start = units
215        .iter()
216        .position(|&unit| !is_js_space(unit))
217        .unwrap_or(units.len());
218    let end = units
219        .iter()
220        .rposition(|&unit| !is_js_space(unit))
221        .map_or(start, |index| index + 1);
222    String::from_utf16_lossy(&units[start..end.max(start)])
223}
224
225const fn expr(node: SNode, at: Span) -> SExpr {
226    SExpr::new(node, Some(at))
227}
228
229const fn pattern(node: SPatternNode, at: Option<Span>) -> SPattern {
230    SPattern { node, span: at }
231}
232
233/// A qualified pattern head: `Tree.node`, or `.node` resolved against the scrutinee.
234struct PatternHead {
235    path: Vec<String>,
236    dot: bool,
237}
238
239enum Definition {
240    Fn(Box<SFn>),
241    Main(SMain, Span),
242}
243
244struct LeanParser<'a> {
245    cursor: TokenCursor,
246    source: &'a Source,
247    bounds: Vec<i64>,
248}
249
250impl<'a> LeanParser<'a> {
251    fn new(tokens: Vec<Token>, source: &'a Source) -> Self {
252        Self {
253            cursor: TokenCursor::new(tokens, Language::Lean),
254            source,
255            bounds: vec![-1],
256        }
257    }
258
259    fn bound(&self) -> i64 {
260        self.bounds.last().copied().unwrap_or(-1)
261    }
262
263    fn with_bound<T>(
264        &mut self,
265        column: i64,
266        parse: impl FnOnce(&mut Self) -> Result<T>,
267    ) -> Result<T> {
268        self.bounds.push(column);
269        let result = parse(self);
270        self.bounds.pop();
271        result
272    }
273
274    /// True when the token closes the current layout block.
275    fn blocked(&self, token: &Token) -> bool {
276        if token.kind == TokenKind::Eof {
277            return true;
278        }
279        if token.col == 0
280            && token.first
281            && token.kind == TokenKind::Identifier
282            && is_item_keyword(&token.value)
283        {
284            return true;
285        }
286        token.first && column(token) <= self.bound()
287    }
288
289    fn blocked_next(&self) -> bool {
290        self.blocked(self.cursor.peek())
291    }
292
293    /// Alternatives may sit at the column of the construct that opens them.
294    fn outdented(&self, at: i64) -> bool {
295        let token = self.cursor.peek();
296        token.kind == TokenKind::Eof || (token.first && column(token) < at)
297    }
298
299    fn fail(&self, message: &str) -> TranslationError {
300        Self::fail_at(message, self.cursor.peek())
301    }
302
303    fn fail_at(message: &str, token: &Token) -> TranslationError {
304        syntax_at(format!("{message} but found {}", describe(token)), token)
305    }
306
307    fn peek(&self) -> Token {
308        self.cursor.peek().clone()
309    }
310
311    fn span_to_next(&self, from: &Token) -> Span {
312        span(from, self.cursor.peek())
313    }
314
315    fn file(mut self) -> Result<SProgram> {
316        let mut items = Vec::new();
317        let mut main = None;
318        self.items(&mut main, &mut items, &[])?;
319        Ok(SProgram {
320            language: Language::Lean,
321            items,
322            main,
323        })
324    }
325
326    fn items(
327        &mut self,
328        main: &mut Option<SMain>,
329        items: &mut Vec<SItem>,
330        path: &[String],
331    ) -> Result<()> {
332        while !self.cursor.at_end() {
333            let token = self.peek();
334            if self.cursor.is("end") {
335                let Some(open) = path.last() else {
336                    return Err(self.fail("unmatched end"));
337                };
338                self.cursor.advance();
339                let name = self.qualified_name()?.join(".");
340                if name != *open {
341                    return Err(syntax_at(
342                        format!("end {name} closes namespace {open}"),
343                        &token,
344                    ));
345                }
346                return Ok(());
347            }
348            if self.cursor.is("namespace") {
349                self.cursor.advance();
350                let mut segments = self.qualified_name()?;
351                let module_span = self.span_to_next(&token);
352                if segments.len() != 1 {
353                    return Err(unsupported(
354                        "dotted namespace",
355                        "use one namespace per level",
356                        Some(span(&token, &token)),
357                    ));
358                }
359                let name = segments.remove(0);
360                let mut module = SModule {
361                    name: name.clone(),
362                    items: Vec::new(),
363                    span: Some(module_span),
364                };
365                let mut inner = path.to_vec();
366                inner.push(name);
367                self.items(main, &mut module.items, &inner)?;
368                items.push(SItem::Module(module));
369                continue;
370            }
371            if self.cursor.is("inductive") {
372                items.push(SItem::Data(self.inductive()?));
373                continue;
374            }
375            if self.cursor.is("def") {
376                match self.definition(path)? {
377                    Definition::Main(program_main, at) => {
378                        if !path.is_empty() {
379                            return Err(unsupported(
380                                "namespaced main",
381                                "main must be declared at the top level",
382                                Some(at),
383                            ));
384                        }
385                        if main.is_some() {
386                            return Err(type_error("duplicate main", Some(at)));
387                        }
388                        *main = Some(program_main);
389                    }
390                    Definition::Fn(item) => items.push(SItem::Fn(*item)),
391                }
392                continue;
393            }
394            if self.cursor.is("theorem") {
395                items.push(SItem::Theorem(self.theorem()?));
396                continue;
397            }
398            if token.kind == TokenKind::Identifier && is_item_keyword(&token.value) {
399                return Err(unsupported(
400                    &format!("Lean {} declaration", token.value),
401                    "outside the portable core",
402                    Some(span(&token, &token)),
403                ));
404            }
405            return Err(self.fail("expected a declaration"));
406        }
407        if let Some(open) = path.last() {
408            return Err(syntax_at(
409                format!("namespace {open} is not closed"),
410                self.cursor.peek(),
411            ));
412        }
413        Ok(())
414    }
415
416    fn qualified_name(&mut self) -> Result<Vec<String>> {
417        let token = self.cursor.identifier(Some("name"))?;
418        Ok(token.value.split('.').map(str::to_owned).collect())
419    }
420
421    fn inductive(&mut self) -> Result<SData> {
422        let start = self.cursor.advance();
423        let name = self.cursor.identifier(Some("inductive"))?.value;
424        if name.contains('.') {
425            return Err(unsupported(
426                "qualified inductive name",
427                "declare inductives inside their namespace",
428                Some(span(&start, &start)),
429            ));
430        }
431        if !self.cursor.is("where") {
432            if self.cursor.is("(") || self.cursor.is("{") {
433                return Err(unsupported(
434                    "parameterised inductive",
435                    "type parameters are outside the portable core",
436                    Some(self.span_to_next(&start)),
437                ));
438            }
439            self.cursor.expect("where", Some("inductive"))?;
440        }
441        self.cursor.advance();
442        let mut ctors = Vec::new();
443        while self.cursor.is("|") {
444            let bar = self.cursor.advance();
445            let ctor_name = self.cursor.identifier(Some("constructor"))?.value;
446            let mut fields = Vec::new();
447            while self.cursor.is("(") {
448                fields.extend(self.binder_group()?.into_iter().map(|(name, ty)| SField {
449                    name: Some(name),
450                    ty,
451                    rocq_type: None,
452                    span: None,
453                }));
454            }
455            if self.cursor.eat(":").is_some() {
456                let mut types = self.arrow_type()?;
457                let result = types.pop();
458                let constructs_self = matches!(
459                    &result,
460                    Some(Type::Named { path, .. }) if path.join(".") == name
461                );
462                if !constructs_self {
463                    return Err(unsupported(
464                        "indexed constructor",
465                        &format!("{ctor_name} must construct {name}"),
466                        Some(self.span_to_next(&bar)),
467                    ));
468                }
469                fields.extend(types.into_iter().map(|ty| SField {
470                    name: None,
471                    ty,
472                    rocq_type: None,
473                    span: None,
474                }));
475            }
476            ctors.push(SCtor {
477                name: ctor_name,
478                fields,
479            });
480        }
481        if self.cursor.is("deriving") {
482            self.cursor.advance();
483            self.cursor.identifier(Some("deriving"))?;
484            while self.cursor.eat(",").is_some() {
485                self.cursor.identifier(Some("deriving"))?;
486            }
487        }
488        Ok(SData {
489            name,
490            ctors,
491            span: Some(self.span_to_next(&start)),
492            generated: false,
493        })
494    }
495
496    fn binder_group(&mut self) -> Result<Vec<(String, Type)>> {
497        let open = self.cursor.expect("(", Some("binder"))?;
498        let mut names = Vec::new();
499        while self.cursor.is_kind(TokenKind::Identifier) {
500            names.push(self.cursor.advance().value);
501        }
502        if names.is_empty() {
503            return Err(self.fail("expected binder names"));
504        }
505        self.cursor.expect(":", Some("binder"))?;
506        let ty = self.ty()?;
507        self.cursor.expect(")", Some("binder"))?;
508        if self.cursor.is("{") || self.cursor.is("[") {
509            return Err(unsupported(
510                "implicit binder",
511                "implicit and instance binders are outside the portable core",
512                Some(self.span_to_next(&open)),
513            ));
514        }
515        Ok(names.into_iter().map(|name| (name, ty.clone())).collect())
516    }
517
518    fn binders(&mut self) -> Result<Vec<(String, Type)>> {
519        let mut result = Vec::new();
520        while self.cursor.is("(") || self.cursor.is("{") || self.cursor.is("[") {
521            if !self.cursor.is("(") {
522                let token = self.cursor.peek();
523                return Err(unsupported(
524                    "implicit binder",
525                    "implicit and instance binders are outside the portable core",
526                    Some(span(token, token)),
527                ));
528            }
529            result.extend(self.binder_group()?);
530        }
531        Ok(result)
532    }
533
534    fn arrow_type(&mut self) -> Result<Vec<Type>> {
535        let mut types = vec![self.ty()?];
536        while self.cursor.eat("→").is_some() || self.cursor.eat("->").is_some() {
537            types.push(self.ty()?);
538        }
539        Ok(types)
540    }
541
542    fn ty(&mut self) -> Result<Type> {
543        let token = self.peek();
544        if self.cursor.eat("(").is_some() {
545            let mut types = self.arrow_type()?;
546            self.cursor.expect(")", Some("type"))?;
547            if types.len() != 1 {
548                return Err(unsupported(
549                    "function type",
550                    "higher-order values are outside the portable core",
551                    Some(span(&token, &token)),
552                ));
553            }
554            return Ok(types.remove(0));
555        }
556        let name = self.cursor.identifier(Some("type"))?.value;
557        if let Some(builtin) = builtin_type(&name) {
558            return Ok(builtin);
559        }
560        if is_unsupported_type(&name) {
561            return Err(unsupported(
562                &format!("Lean type {name}"),
563                "outside the portable core",
564                Some(span(&token, &token)),
565            ));
566        }
567        let next = self.cursor.peek();
568        if !self.blocked(next)
569            && next.kind == TokenKind::Identifier
570            && !["where", ":=", "with", "deriving"].contains(&next.value.as_str())
571        {
572            return Err(unsupported(
573                "type application",
574                &format!("{name} {} is outside the portable core", next.value),
575                Some(span(&token, next)),
576            ));
577        }
578        Ok(Type::Named {
579            path: name.split('.').map(str::to_owned).collect(),
580            span: Some(span(&token, &token)),
581        })
582    }
583
584    fn definition(&mut self, path: &[String]) -> Result<Definition> {
585        let start = self.cursor.advance();
586        let name_token = self.cursor.identifier(Some("def"))?;
587        let name = name_token.value.clone();
588        if name.contains('.') {
589            return Err(unsupported(
590                "qualified definition name",
591                "declare definitions inside their namespace",
592                Some(span(&name_token, &name_token)),
593            ));
594        }
595        let params: Vec<SParam> = self
596            .binders()?
597            .into_iter()
598            .map(|(name, ty)| param(name, ty))
599            .collect();
600        self.cursor.expect(":", Some("def"))?;
601        if name == "main" && path.is_empty() && self.cursor.is("IO") {
602            return self.main(&start);
603        }
604        let mut types = self.arrow_type()?;
605        let ret = types.pop();
606        let extra: Vec<SParam> = types
607            .into_iter()
608            .enumerate()
609            .map(|(index, ty)| param(format!("ml_arg{index}"), ty))
610            .collect();
611        if self.cursor.eat(":=").is_some() {
612            if !extra.is_empty() {
613                return Err(unsupported(
614                    "function-valued definition body",
615                    "use binders or equations for arrow types",
616                    Some(self.span_to_next(&start)),
617                ));
618            }
619            let body = self.with_bound(0, Self::expr)?;
620            self.end_decl(&start, "termination_by")?;
621            return Ok(Definition::Fn(Box::new(SFn {
622                name,
623                params,
624                ret,
625                body,
626                span: Some(self.span_to_next(&start)),
627                generated: false,
628            })));
629        }
630        if !self.cursor.is("|") {
631            return Err(self.fail("expected := or equations"));
632        }
633        if extra.is_empty() {
634            return Err(unsupported(
635                "equations without arrow arguments",
636                "use match",
637                Some(self.span_to_next(&start)),
638            ));
639        }
640        let rows = self.alternatives(extra.len())?;
641        let body = expr(
642            SNode::Match {
643                scrutinees: extra.iter().map(|param| SExpr::name(&param.name)).collect(),
644                rows,
645            },
646            self.span_to_next(&start),
647        );
648        self.end_decl(&start, "termination_by")?;
649        Ok(Definition::Fn(Box::new(SFn {
650            name,
651            params: params.into_iter().chain(extra).collect(),
652            ret,
653            body,
654            span: Some(self.span_to_next(&start)),
655            generated: false,
656        })))
657    }
658
659    fn end_decl(&self, start: &Token, keyword: &str) -> Result<()> {
660        if self.cursor.is(keyword) || self.cursor.is("decreasing_by") {
661            return Err(unsupported(
662                &format!("Lean {}", self.cursor.peek().value),
663                "explicit termination arguments are outside the portable core",
664                Some(self.span_to_next(start)),
665            ));
666        }
667        if !self.blocked_next() {
668            return Err(self.fail("expected the end of the declaration"));
669        }
670        Ok(())
671    }
672
673    fn main(&mut self, start: &Token) -> Result<Definition> {
674        self.cursor.expect("IO", Some("main"))?;
675        self.cursor.expect("Unit", Some("main"))?;
676        self.cursor.expect(":=", Some("main"))?;
677        self.cursor.expect("do", Some("main"))?;
678        let mut effects = Vec::new();
679        let first = self.peek();
680        let effect_column = if first.first { column(&first) } else { -1 };
681        if effect_column <= 0 {
682            return Err(unsupported(
683                "inline do block",
684                "write one effect per line",
685                Some(span(&first, &first)),
686            ));
687        }
688        while !self.cursor.at_end()
689            && column(self.cursor.peek()) == effect_column
690            && self.cursor.peek().first
691        {
692            let before = self.cursor.index;
693            effects.push(self.with_bound(effect_column, Self::effect)?);
694            if self.cursor.index == before {
695                return Err(self.fail("expected an effect"));
696            }
697        }
698        self.end_decl(start, "where")?;
699        let at = self.span_to_next(start);
700        Ok(Definition::Main(
701            SMain {
702                effects,
703                span: Some(at),
704                sequential_async: false,
705            },
706            at,
707        ))
708    }
709
710    fn effect(&mut self) -> Result<SEffect> {
711        let token = self.peek();
712        if self.cursor.is("IO.println") {
713            self.cursor.advance();
714            let expr = self.atom()?;
715            return Ok(SEffect::Print {
716                expr,
717                style: ShowStyle::Lean,
718                span: Some(self.span_to_next(&token)),
719            });
720        }
721        if self.cursor.is("let") {
722            self.cursor.advance();
723            let name = self.cursor.identifier(Some("let"))?.value;
724            let ty = if self.cursor.eat(":").is_some() {
725                Some(self.ty()?)
726            } else {
727                None
728            };
729            self.cursor.expect(":=", Some("let"))?;
730            let value = self.expr()?;
731            return Ok(SEffect::Let {
732                name,
733                ty,
734                value,
735                constant: false,
736                span: Some(self.span_to_next(&token)),
737            });
738        }
739        Err(unsupported(
740            "Lean do element",
741            &format!("{} is outside the portable effect model", describe(&token)),
742            Some(span(&token, &token)),
743        ))
744    }
745}
746
747/// A head applied to arguments, or the head alone when there are none.
748fn plain_application(head: SExpr, args: Vec<SExpr>, range: Span) -> Result<SExpr> {
749    if args.is_empty() {
750        return Ok(head);
751    }
752    if !matches!(head.node, SNode::Name { .. } | SNode::DotCtor { .. }) {
753        return Err(unsupported(
754            "higher-order application",
755            "only named functions can be applied",
756            Some(range),
757        ));
758    }
759    Ok(expr(
760        SNode::App {
761            func: Box::new(head),
762            args,
763        },
764        range,
765    ))
766}
767
768const fn connective(node: SPropNode) -> SProp {
769    SProp { node, span: None }
770}
771
772fn bind_or_ctor(head: PatternHead, token: &Token) -> SPattern {
773    let name = head.path.into_iter().next().unwrap_or_default();
774    pattern(SPatternNode::BindOrCtor { name }, Some(span(token, token)))
775}
776
777const fn param(name: String, ty: Type) -> SParam {
778    SParam {
779        name,
780        default_value: None,
781        ty: Some(ty),
782        span: None,
783        guard: None,
784        rocq_type: None,
785    }
786}
787
788const fn binder(name: String, ty: Type) -> SBinder {
789    SBinder {
790        name,
791        ty: Some(ty),
792        rocq_type: None,
793        span: None,
794    }
795}
meta_language/translation/lean.rs

meta_language/translation/
lean.rs
