hax_rust_engine/backends/
lean.rs

1//! The Lean backend
2//!
3//! This module defines the trait implementations to export the rust ast to
4//! Pretty::Doc type, which can in turn be exported to string (or, eventually,
5//! source maps).
6
7use std::collections::HashSet;
8use std::sync::LazyLock;
9
10use super::prelude::*;
11use crate::{
12    ast::identifiers::global_id::view::{ConstructorKind, PathSegment, TypeDefKind},
13    resugarings::BinOp,
14};
15
16mod binops {
17    pub use crate::names::rust_primitives::hax::machine_int::{add, div, mul, rem, shr, sub};
18    pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
19}
20
21/// The Lean printer
22#[derive(Default)]
23pub struct LeanPrinter;
24impl_doc_allocator_for!(LeanPrinter);
25
26const INDENT: isize = 2;
27
28static RESERVED_KEYWORDS: LazyLock<HashSet<String>> = LazyLock::new(|| {
29    HashSet::from_iter(
30        [
31            "end",
32            "def",
33            "abbrev",
34            "theorem",
35            "example",
36            "inductive",
37            "structure",
38            "from",
39        ]
40        .iter()
41        .map(|s| s.to_string()),
42    )
43});
44
45impl RenderView for LeanPrinter {
46    fn separator(&self) -> &str {
47        "."
48    }
49    fn render_path_segment(&self, chunk: &PathSegment) -> Vec<String> {
50        fn uppercase_first(s: &str) -> String {
51            let mut c = s.chars();
52            match c.next() {
53                None => String::new(),
54                Some(first) => first.to_uppercase().collect::<String>() + c.as_str(),
55            }
56        }
57        // Returning None indicates that the default rendering should be used
58        (match chunk.kind() {
59            AnyKind::Mod => {
60                let mut chunks = default::render_path_segment(self, chunk);
61                for c in &mut chunks {
62                    *c = uppercase_first(c);
63                }
64                Some(chunks)
65            }
66            AnyKind::Constructor(ConstructorKind::Constructor { ty })
67                if matches!(ty.kind(), TypeDefKind::Struct) =>
68            {
69                Some(vec![
70                    self.render_path_segment_payload(chunk.payload())
71                        .to_string(),
72                    "mk".to_string(),
73                ])
74            }
75            AnyKind::Field { named: _, parent } => match parent.kind() {
76                ConstructorKind::Constructor { ty }
77                    if matches!(&ty.kind(), TypeDefKind::Struct) =>
78                {
79                    chunk.parent().map(|parent| {
80                        vec![
81                            self.escape(
82                                self.render_path_segment_payload(parent.payload())
83                                    .to_string(),
84                            ),
85                            self.escape(
86                                self.render_path_segment_payload(chunk.payload())
87                                    .to_string(),
88                            ),
89                        ]
90                    })
91                }
92                _ => None,
93            },
94            _ => None,
95        })
96        .unwrap_or(default::render_path_segment(self, chunk))
97    }
98}
99
100impl Printer for LeanPrinter {
101    fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
102        vec![Box::new(BinOp::new(&[
103            binops::add,
104            binops::sub,
105            binops::mul,
106            binops::rem,
107            binops::div,
108            binops::shr,
109            binops::logical_op_and,
110            binops::logical_op_or,
111        ]))]
112    }
113}
114
115/// The Lean backend
116pub struct LeanBackend;
117
118impl Backend for LeanBackend {
119    type Printer = LeanPrinter;
120
121    fn module_path(&self, module: &Module) -> camino::Utf8PathBuf {
122        camino::Utf8PathBuf::from_iter(self.printer().render_strings(&module.ident.view()))
123            .with_extension("lean")
124    }
125}
126
127impl LeanPrinter {
128    /// A filter for items blacklisted by the Lean backend : returns false if
129    /// the item is definitely not printable, but might return true on
130    /// unsupported items
131    pub fn printable_item(item: &Item) -> bool {
132        match &item.kind {
133            // Anonymous consts
134            ItemKind::Fn {
135                name,
136                generics: _,
137                body: _,
138                params: _,
139                safety: _,
140            } if name.is_anonymous_const() => false,
141            // Other unprintable items
142            ItemKind::Error(_) | ItemKind::NotImplementedYet | ItemKind::Use { .. } => false,
143            // Printable items
144            ItemKind::Fn { .. }
145            | ItemKind::TyAlias { .. }
146            | ItemKind::Type { .. }
147            | ItemKind::Trait { .. }
148            | ItemKind::Impl { .. }
149            | ItemKind::Alias { .. }
150            | ItemKind::Resugared(_)
151            | ItemKind::Quote { .. } => true,
152        }
153    }
154
155    /// Render a global id using the Rendering strategy of the Lean printer. Works for both concrete
156    /// and projector ids. TODO: https://github.com/cryspen/hax/issues/1660
157    pub fn render_id(&self, id: &GlobalId) -> String {
158        self.render_string(&id.view())
159    }
160
161    /// Escapes local identifiers (prefixing reserved keywords with an underscore).
162    /// TODO: This should be treated directly in the name rendering engine, see
163    /// https://github.com/cryspen/hax/issues/1630
164    pub fn escape(&self, id: String) -> String {
165        let id = id.replace([' ', '<', '>'], "_");
166        if id.is_empty() {
167            "_ERROR_EMPTY_ID_".to_string()
168        } else if RESERVED_KEYWORDS.contains(&id) || id.starts_with(|c: char| c.is_ascii_digit()) {
169            format!("_{id}")
170        } else {
171            id
172        }
173    }
174
175    /// Renders a single symbol, used for anonymous implementations of typeclasses
176    pub fn render_symbol(&self, symbol: Symbol) -> String {
177        self.escape(symbol.to_string())
178    }
179
180    /// Renders the last, most local part of an id. Used for named arguments of constructors.
181    pub fn render_last(&self, id: &GlobalId) -> String {
182        let id = self
183            .render(&id.view())
184            .path
185            .last()
186            // TODO: Should be ensured by the rendering engine; see
187            // https://github.com/cryspen/hax/issues/1660
188            .expect("Segments should always be non-empty")
189            .clone();
190        self.escape(id)
191    }
192}
193
194/// Render parameters, adding a line after each parameter
195impl<'a, A: 'a + Clone> Pretty<'a, LeanPrinter, A> for &Vec<Param> {
196    fn pretty(self, allocator: &'a LeanPrinter) -> DocBuilder<'a, LeanPrinter, A> {
197        allocator.params(self)
198    }
199}
200
201#[prepend_associated_functions_with(install_pretty_helpers!(self: Self))]
202const _: () = {
203    // Boilerplate: define local macros to disambiguate otherwise `std` macros.
204    #[allow(unused)]
205    macro_rules! todo {($($tt:tt)*) => {disambiguated_todo!($($tt)*)};}
206
207    // Insert a new line in a doc (pretty)
208    macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
209
210    // Concatenate docs (pretty )
211    macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};}
212
213    // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `ASBS...CS`
214    macro_rules! zip_right {
215        ($a:expr, $sep:expr) => {
216            docs![concat!($a.into_iter().map(|a| docs![a, $sep]))]
217        };
218    }
219
220    // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `SASB...SC`
221    macro_rules! zip_left {
222        ($sep:expr, $a:expr) => {
223            docs![concat!($a.into_iter().map(|a| docs![$sep, a]))]
224        };
225    }
226
227    // Methods for handling arguments of variants (or struct constructor)
228    impl LeanPrinter {
229        /// Prints arguments a variant or constructor of struct, using named or unamed arguments based
230        /// on the `is_record` flag. Used for both expressions and patterns
231        pub fn arguments<'a, 'b, A: 'a + Clone, D>(
232            &'a self,
233            fields: &'b [(GlobalId, D)],
234            is_record: &bool,
235        ) -> DocBuilder<'a, Self, A>
236        where
237            &'b D: Pretty<'a, Self, A>,
238        {
239            if *is_record {
240                self.named_arguments(fields)
241            } else {
242                self.positional_arguments(fields)
243            }
244        }
245
246        /// Prints named arguments (record) of a variant or constructor of struct
247        fn named_arguments<'a, 'b, A: 'a + Clone, D>(
248            &'a self,
249            fields: &'b [(GlobalId, D)],
250        ) -> DocBuilder<'a, Self, A>
251        where
252            &'b D: Pretty<'a, Self, A>,
253        {
254            macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
255            docs![intersperse!(
256                fields.iter().map(|(id, e)| {
257                    docs![self.render_last(id), reflow!(" := "), e]
258                        .parens()
259                        .group()
260                }),
261                line!()
262            )]
263            .group()
264        }
265
266        /// Prints positional arguments (tuple) of a variant or constructor of struct
267        fn positional_arguments<'a, 'b, A: 'a + Clone, D>(
268            &'a self,
269            fields: &'b [(GlobalId, D)],
270        ) -> DocBuilder<'a, Self, A>
271        where
272            &'b D: Pretty<'a, Self, A>,
273        {
274            macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
275            docs![intersperse!(fields.iter().map(|(_, e)| e), line!())].group()
276        }
277
278        /// Prints parameters of functions (items, trait items, impl items)
279        fn params<'a, 'b, A: 'a + Clone>(
280            &'a self,
281            params: &'b Vec<Param>,
282        ) -> DocBuilder<'a, Self, A> {
283            zip_right!(params, line!())
284        }
285
286        /// Renders expressions with an explicit ascription `(e : Result ty)`. Used for the body of closure, for
287        /// numeric literals, etc.
288        fn expr_typed_result<'a, 'b, A: 'a + Clone>(
289            &'a self,
290            expr: &'b Expr,
291        ) -> DocBuilder<'a, Self, A> {
292            docs![
293                expr,
294                reflow!(" : "),
295                docs!["Result", line!(), &expr.ty].group()
296            ]
297            .group()
298        }
299
300        fn pat_typed<'a, 'b, A: 'a + Clone>(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
301            docs![pat.kind(), reflow!(" :"), line!(), &pat.ty]
302                .parens()
303                .group()
304        }
305    }
306
307    impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter {
308        const NAME: &'static str = "Lean";
309
310        fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> {
311            let items = &module.items;
312            docs![
313                intersperse!(
314                    "
315-- Experimental lean backend for Hax
316-- The Hax prelude library can be found in hax/proof-libs/lean
317import Hax
318import Std.Tactic.Do
319import Std.Do.Triple
320import Std.Tactic.Do.Syntax
321open Std.Do
322open Std.Tactic
323
324set_option mvcgen.warning false
325set_option linter.unusedVariables false
326
327
328"
329                    .lines(),
330                    hardline!(),
331                ),
332                intersperse!(
333                    items
334                        .iter()
335                        .filter(|item| LeanPrinter::printable_item(item)),
336                    docs![hardline!(), hardline!()]
337                )
338            ]
339        }
340
341        fn global_id(&'a self, global_id: &'b GlobalId) -> DocBuilder<'a, Self, A> {
342            docs![self.render_id(global_id)]
343        }
344
345        /// Render generics, adding a space after each parameter
346        fn generics(
347            &'a self,
348            Generics {
349                params,
350                constraints,
351            }: &'b Generics,
352        ) -> DocBuilder<'a, Self, A> {
353            // TODO : The lean backend should not ignore constraints on generic params, see
354            // https://github.com/cryspen/hax/issues/1636
355            docs![
356                zip_right!(params, line!()),
357                zip_right!(
358                    constraints
359                        .iter()
360                        .map(|constraint| docs![constraint].brackets()),
361                    line!()
362                ),
363            ]
364            .group()
365        }
366
367        fn generic_constraint(
368            &'a self,
369            generic_constraint: &'b GenericConstraint,
370        ) -> DocBuilder<'a, Self, A> {
371            match generic_constraint {
372                GenericConstraint::Type(impl_ident) => docs![impl_ident],
373                _ => todo!("-- unsupported constraint"),
374            }
375        }
376
377        fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> {
378            match generic_param.kind() {
379                GenericParamKind::Type => docs![&generic_param.ident, reflow!(" : Type")]
380                    .parens()
381                    .group(),
382                GenericParamKind::Lifetime => unreachable!(),
383                GenericParamKind::Const { .. } => {
384                    todo!("-- Unsupported const param")
385                }
386            }
387        }
388
389        fn expr(&'a self, Expr { kind, ty, meta: _ }: &'b Expr) -> DocBuilder<'a, Self, A> {
390            match &**kind {
391                ExprKind::Literal(int_lit @ Literal::Int { .. }) => {
392                    docs![int_lit, reflow!(" : "), ty].parens().group()
393                }
394                ExprKind::If {
395                    condition,
396                    then,
397                    else_,
398                } => {
399                    if let Some(else_branch) = else_ {
400                        // TODO: have a proper monadic resugaring, see
401                        // https://github.com/cryspen/hax/issues/1620
402                        docs![
403                            docs!["← if", line!(), condition, reflow!(" then do")].group(),
404                            docs![line!(), then].nest(INDENT),
405                            line!(),
406                            reflow!("else do"),
407                            docs![line!(), else_branch].nest(INDENT)
408                        ]
409                        .parens()
410                        .group()
411                    } else {
412                        // The Hax engine should ensure that there is always an else branch
413                        unreachable!()
414                    }
415                }
416                ExprKind::App {
417                    head,
418                    args,
419                    generic_args,
420                    bounds_impls: _,
421                    trait_: _,
422                } => {
423                    // TODO: have a proper monadic resugaring, see https://github.com/cryspen/hax/issues/1620
424                    let monadic_lift = if let ExprKind::GlobalId(head_id) = head.kind()
425                        && (head_id.is_constructor() || head_id.is_projector())
426                    {
427                        None
428                    } else {
429                        Some("← ")
430                    };
431                    let generic_args = (!generic_args.is_empty()).then_some(
432                        docs![line!(), self.intersperse(generic_args, line!())]
433                            .nest(INDENT)
434                            .group(),
435                    );
436                    let args = (!args.is_empty()).then_some(
437                        docs![line!(), intersperse!(args, line!())]
438                            .nest(INDENT)
439                            .group(),
440                    );
441                    docs![monadic_lift, head, generic_args, args]
442                        .nest(INDENT)
443                        .parens()
444                        .group()
445                }
446                ExprKind::Literal(literal) => docs![literal],
447                ExprKind::Array(exprs) => docs![
448                    "#v[",
449                    intersperse!(exprs, docs![",", line!()])
450                        .nest(INDENT)
451                        .group()
452                        .align(),
453                    "]"
454                ]
455                .group(),
456                ExprKind::Construct {
457                    constructor,
458                    is_record,
459                    is_struct: _,
460                    fields,
461                    base,
462                } => {
463                    if fields.is_empty() && base.is_none() {
464                        docs![constructor]
465                    } else if base.is_some() {
466                        // TODO : support base expressions. see https://github.com/cryspen/hax/issues/1637
467                        todo!("-- Unsupported base expressions for structs.")
468                    } else {
469                        docs![constructor, line!(), self.arguments(fields, is_record)]
470                            .nest(INDENT)
471                            .parens()
472                            .group()
473                    }
474                }
475                ExprKind::Let { lhs, rhs, body } => {
476                    docs![
477                        docs![
478                            docs![
479                                "let",
480                                line!(),
481                                // TODO: Remove this pattern-matching. See
482                                // https://github.com/cryspen/hax/issues/1620
483                                match *lhs.kind.clone() {
484                                    PatKind::Binding {
485                                        mutable: false,
486                                        var,
487                                        mode: BindingMode::ByValue,
488                                        sub_pat: None,
489                                    } => docs![&var, reflow!(" : "), &lhs.ty],
490                                    _ => docs![lhs],
491                                },
492                            ]
493                            .group(),
494                            " ←",
495                            softline!(),
496                            docs!["pure", line!(), rhs].parens().group(),
497                            ";"
498                        ]
499                        .nest(INDENT)
500                        .group(),
501                        line!(),
502                        body,
503                    ]
504                }
505                ExprKind::GlobalId(global_id) => docs![global_id],
506                ExprKind::LocalId(local_id) => docs![local_id],
507                ExprKind::Ascription { e, ty } => docs![
508                    // TODO: This insertion should be done by a monadic phase (or resugaring). See
509                    // https://github.com/cryspen/hax/issues/1620
510                    match *e.kind {
511                        ExprKind::Literal(_) | ExprKind::Construct { .. } => None,
512                        _ => Some("← "),
513                    },
514                    e,
515                    reflow!(" : "),
516                    ty
517                ]
518                .parens()
519                .group(),
520                ExprKind::Closure {
521                    params,
522                    body,
523                    captures: _,
524                } => docs![
525                    reflow!("fun "),
526                    intersperse!(params, line!()).group(),
527                    reflow!(" => "),
528                    // TODO: have a proper monadic resugaring, see https://github.com/cryspen/hax/issues/1620
529                    docs!["do", line!(), self.expr_typed_result(body)]
530                        .nest(INDENT)
531                        .parens()
532                        .group()
533                ]
534                .parens()
535                .group()
536                .nest(INDENT),
537                ExprKind::Resugared(resugared_expr_kind) => match resugared_expr_kind {
538                    ResugaredExprKind::BinOp {
539                        op,
540                        lhs,
541                        rhs,
542                        generic_args: _,
543                        bounds_impls: _,
544                        trait_: _,
545                    } => {
546                        let symbol = match *op {
547                            binops::add => "+?",
548                            binops::sub => "-?",
549                            binops::mul => "*?",
550                            binops::div => "/?",
551                            binops::rem => "%?",
552                            binops::shr => ">>>?",
553                            binops::logical_op_and => "&&?",
554                            binops::logical_op_or => "||?",
555                            _ => unreachable!(),
556                        };
557
558                        // TODO: This monad lifting should be handled by a phase/resugaring, see
559                        // https://github.com/cryspen/hax/issues/1620
560                        docs!["← ", lhs, line!(), docs![symbol, softline!(), rhs].group()]
561                            .group()
562                            .nest(INDENT)
563                            .parens()
564                    }
565                    ResugaredExprKind::Tuple { .. } => {
566                        unreachable!("This printer doesn't use the tuple resugaring")
567                    }
568                },
569                ExprKind::Match { scrutinee, arms } => docs![
570                    docs![
571                        "match",
572                        docs![line!(), scrutinee].nest(INDENT),
573                        line!(),
574                        "with"
575                    ]
576                    .group(),
577                    docs![line!(), intersperse!(arms, line!())]
578                        .group()
579                        .nest(INDENT),
580                ]
581                .parens()
582                .group(),
583                _ => todo!(),
584            }
585        }
586
587        fn arm(&'a self, arm: &'b Arm) -> DocBuilder<'a, Self, A> {
588            if let Some(_guard) = &arm.guard {
589                todo!()
590            } else {
591                docs![
592                    reflow!("| "),
593                    &*arm.pat.kind,
594                    line!(),
595                    docs!["=> do", line!(), &arm.body].nest(INDENT).group()
596                ]
597                .nest(INDENT)
598                .group()
599            }
600        }
601
602        fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
603            docs![pat.kind()]
604        }
605
606        fn pat_kind(&'a self, pat_kind: &'b PatKind) -> DocBuilder<'a, Self, A> {
607            match pat_kind {
608                PatKind::Wild => docs!["_"],
609                PatKind::Ascription { pat, ty: _ } => docs![&*pat.kind],
610                PatKind::Binding {
611                    mutable,
612                    var,
613                    mode,
614                    sub_pat,
615                } => match (mutable, mode, sub_pat) {
616                    (false, BindingMode::ByValue, None) => docs![var],
617                    _ => panic!(),
618                },
619                PatKind::Or { sub_pats } => docs![intersperse!(sub_pats, reflow!(" | "))].group(),
620                PatKind::Array { args: _ } => todo!(),
621                PatKind::Deref { sub_pat: _ } => todo!(),
622                PatKind::Constant { lit: _ } => todo!(),
623                PatKind::Construct {
624                    constructor,
625                    is_record,
626                    is_struct,
627                    fields,
628                } => {
629                    if *is_struct {
630                        if !*is_record {
631                            // Tuple-like structure, using positional arguments
632                            docs![
633                                "⟨",
634                                intersperse!(
635                                    fields.iter().map(|field| { docs![&field.1] }),
636                                    docs![",", line!()]
637                                )
638                                .align()
639                                .group(),
640                                "⟩"
641                            ]
642                            .align()
643                            .group()
644                        } else {
645                            // Structure-like structure, using named arguments
646                            docs![intersperse!(
647                                fields.iter().map(|(id, pat)| {
648                                    docs![self.render_last(id), reflow!(" := "), pat].group()
649                                }),
650                                docs![",", line!()]
651                            )]
652                            .align()
653                            .braces()
654                            .group()
655                        }
656                    } else {
657                        // Variant
658                        docs![
659                            constructor,
660                            line!(),
661                            self.arguments(fields, is_record).align()
662                        ]
663                        .parens()
664                        .group()
665                        .nest(INDENT)
666                    }
667                }
668                PatKind::Resugared(_resugared_pat_kind) => todo!(),
669                PatKind::Error(_error_node) => todo!(),
670            }
671        }
672
673        fn ty(&'a self, ty: &'b Ty) -> DocBuilder<'a, Self, A> {
674            match ty.kind() {
675                TyKind::Primitive(primitive_ty) => docs![primitive_ty],
676                TyKind::App { head, args } => {
677                    if args.is_empty() {
678                        docs![head]
679                    } else {
680                        docs![head, zip_left!(line!(), args)]
681                            .parens()
682                            .group()
683                            .nest(INDENT)
684                    }
685                }
686                TyKind::Arrow { inputs, output } => docs![
687                    zip_right!(inputs, docs![line!(), reflow!("-> ")]),
688                    "Result ",
689                    output
690                ]
691                .group(),
692                TyKind::Param(local_id) => docs![local_id],
693                TyKind::Slice(ty) => docs!["RustSlice", line!(), ty].parens().group(),
694                TyKind::Array { ty, length } => docs!["RustArray", line!(), ty, line!(), &**length]
695                    .parens()
696                    .group(),
697                TyKind::AssociatedType { impl_, item } => {
698                    let kind = impl_.kind();
699                    match &kind {
700                        ImplExprKind::Self_ => docs![self.render_last(item)],
701                        _ => todo!(), // Support only local associated types
702                    }
703                }
704                _ => todo!("sorry \n-- unsupported type\n"),
705            }
706        }
707
708        fn literal(&'a self, literal: &'b Literal) -> DocBuilder<'a, Self, A> {
709            docs![match literal {
710                Literal::String(symbol) => format!("\"{symbol}\""),
711                Literal::Char(c) => format!("'{c}'"),
712                Literal::Bool(b) => format!("{b}"),
713                Literal::Int {
714                    value,
715                    negative,
716                    kind: _,
717                } => format!("{}{value}", if *negative { "-" } else { "" }),
718                Literal::Float {
719                    value: _,
720                    negative: _,
721                    kind: _,
722                } => todo!(),
723            }]
724        }
725
726        fn local_id(&'a self, local_id: &'b LocalId) -> DocBuilder<'a, Self, A> {
727            // TODO: should be done by name rendering, see https://github.com/cryspen/hax/issues/1630
728            docs![self.escape(local_id.0.to_string())]
729        }
730
731        fn spanned_ty(&'a self, spanned_ty: &'b SpannedTy) -> DocBuilder<'a, Self, A> {
732            docs![&spanned_ty.ty]
733        }
734
735        fn primitive_ty(&'a self, primitive_ty: &'b PrimitiveTy) -> DocBuilder<'a, Self, A> {
736            match primitive_ty {
737                PrimitiveTy::Bool => docs!["Bool"],
738                PrimitiveTy::Int(int_kind) => docs![int_kind],
739                PrimitiveTy::Float(_float_kind) => todo!(),
740                PrimitiveTy::Char => docs!["Char"],
741                PrimitiveTy::Str => docs!["String"],
742            }
743        }
744
745        fn int_kind(&'a self, int_kind: &'b IntKind) -> DocBuilder<'a, Self, A> {
746            docs![match (&int_kind.signedness, &int_kind.size) {
747                (Signedness::Signed, IntSize::S8) => "i8",
748                (Signedness::Signed, IntSize::S16) => "i16",
749                (Signedness::Signed, IntSize::S32) => "i32",
750                (Signedness::Signed, IntSize::S64) => "i64",
751                (Signedness::Signed, IntSize::S128) => "i128",
752                (Signedness::Signed, IntSize::SSize) => "isize",
753                (Signedness::Unsigned, IntSize::S8) => "u8",
754                (Signedness::Unsigned, IntSize::S16) => "u16",
755                (Signedness::Unsigned, IntSize::S32) => "u32",
756                (Signedness::Unsigned, IntSize::S64) => "u64",
757                (Signedness::Unsigned, IntSize::S128) => "u128",
758                (Signedness::Unsigned, IntSize::SSize) => "usize",
759            }]
760        }
761
762        fn generic_value(&'a self, generic_value: &'b GenericValue) -> DocBuilder<'a, Self, A> {
763            match generic_value {
764                GenericValue::Ty(ty) => docs![ty],
765                GenericValue::Expr(expr) => docs![expr],
766                GenericValue::Lifetime => todo!(),
767            }
768        }
769
770        fn quote_content(&'a self, quote_content: &'b QuoteContent) -> DocBuilder<'a, Self, A> {
771            match quote_content {
772                QuoteContent::Verbatim(s) => {
773                    intersperse!(s.lines().map(|x| x.to_string()), hardline!())
774                }
775                QuoteContent::Expr(expr) => docs![expr],
776                QuoteContent::Pattern(pat) => docs![pat],
777                QuoteContent::Ty(ty) => docs![ty],
778            }
779        }
780
781        fn quote(&'a self, quote: &'b Quote) -> DocBuilder<'a, Self, A> {
782            concat![&quote.0]
783        }
784
785        fn param(&'a self, param: &'b Param) -> DocBuilder<'a, Self, A> {
786            self.pat_typed(&param.pat)
787        }
788
789        fn item(
790            &'a self,
791            item @ Item {
792                ident,
793                kind,
794                meta: _,
795            }: &'b Item,
796        ) -> DocBuilder<'a, Self, A> {
797            if !LeanPrinter::printable_item(item) {
798                return nil!();
799            };
800            match kind {
801                ItemKind::Fn {
802                    name,
803                    generics,
804                    body,
805                    params,
806                    safety: _,
807                } => match &*body.kind {
808                    // TODO: Literal consts. This should be done by a resugaring, see
809                    // https://github.com/cryspen/hax/issues/1614
810                    ExprKind::Literal(l) if params.is_empty() => {
811                        docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group()
812                    }
813                    _ => docs![
814                        docs![
815                            docs!["def", line!(), name].group(),
816                            line!(),
817                            generics,
818                            params,
819                            docs![": Result", line!(), &body.ty].group(),
820                            line!(),
821                            ":= do"
822                        ]
823                        .group(),
824                        line!(),
825                        body
826                    ]
827                    .group()
828                    .nest(INDENT),
829                },
830                ItemKind::TyAlias {
831                    name,
832                    generics: _,
833                    ty,
834                } => docs!["abbrev ", name, reflow!(" := "), ty].group(),
835                ItemKind::Use {
836                    path: _,
837                    is_external: _,
838                    rename: _,
839                } => nil!(),
840                ItemKind::Quote { quote, origin: _ } => docs![quote],
841                ItemKind::NotImplementedYet => {
842                    docs!["example : Unit := sorry /- unsupported by the Hax engine -/"]
843                }
844                ItemKind::Type {
845                    name,
846                    generics,
847                    variants,
848                    is_struct,
849                } => {
850                    // TODO: use a resugaring, see https://github.com/cryspen/hax/issues/1668
851                    if *is_struct {
852                        // Structures
853                        let Some(variant) = variants.first() else {
854                            // Structures always have a constructor (even empty ones)
855                            unreachable!()
856                        };
857                        let args = if !variant.is_record {
858                            // Tuple-like structure, using positional arguments
859                            intersperse!(
860                                variant.arguments.iter().enumerate().map(|(i, (_, ty, _))| {
861                                    docs![format!("_{i} :"), line!(), ty].group().nest(INDENT)
862                                }),
863                                hardline!()
864                            )
865                        } else {
866                            // Structure-like structure, using named arguments
867                            intersperse!(
868                                variant.arguments.iter().map(|(id, ty, _)| {
869                                    docs![self.render_last(id), reflow!(" : "), ty]
870                                        .group()
871                                        .nest(INDENT)
872                                }),
873                                hardline!()
874                            )
875                        };
876                        docs![
877                            docs![reflow!("structure "), name, line!(), generics, "where"].group(),
878                            docs![hardline!(), args],
879                        ]
880                        .nest(INDENT)
881                        .group()
882                    } else {
883                        // Enums
884                        let applied_name: DocBuilder<'a, Self, A> =
885                            docs![name, line!(), generics].group();
886                        docs![
887                            docs!["inductive ", name, line!(), generics, ": Type"].group(),
888                            hardline!(),
889                            concat!(variants.iter().map(|variant| docs![
890                                "| ",
891                                docs![variant, applied_name.clone()].group().nest(INDENT),
892                                hardline!()
893                            ])),
894                        ]
895                    }
896                }
897                ItemKind::Trait {
898                    name,
899                    generics,
900                    items,
901                } => {
902                    // Type parameters are also parameters of the class, but constraints are fields of the class
903                    docs![
904                        docs![
905                            docs![reflow!("class "), name],
906                            (!generics.params.is_empty()).then_some(docs![
907                                line!(),
908                                intersperse!(&generics.params, line!()).group()
909                            ]),
910                            line!(),
911                            "where"
912                        ]
913                        .group(),
914                        hardline!(),
915                        (!generics.constraints.is_empty()).then_some(docs![zip_right!(
916                            generics
917                                .constraints
918                                .iter()
919                                .map(|constraint: &GenericConstraint| {
920                                    match constraint {
921                                        GenericConstraint::Type(tc_constraint) => docs![
922                                            format!("_constr_{}", tc_constraint.name),
923                                            " :",
924                                            line!(),
925                                            constraint
926                                        ]
927                                        .group()
928                                        .brackets(),
929                                        _ => {
930                                            todo!("unsupported type constraint in trait definition")
931                                        }
932                                    }
933                                }),
934                            hardline!()
935                        )]),
936                        intersperse!(
937                            items.iter().filter(|item| {
938                                // TODO: should be treated directly by name rendering, see :
939                                // https://github.com/cryspen/hax/issues/1646
940                                !(item.ident.is_precondition() || item.ident.is_postcondition())
941                            }),
942                            hardline!()
943                        )
944                    ]
945                    .nest(INDENT)
946                }
947                ItemKind::Impl {
948                    generics,
949                    self_ty: _,
950                    of_trait: (trait_, args),
951                    items,
952                    parent_bounds: _,
953                    safety: _,
954                } => docs![
955                    docs![
956                        docs![reflow!("instance "), ident, line!(), generics, ":"].group(),
957                        line!(),
958                        docs![trait_, concat!(args.iter().map(|gv| docs![line!(), gv]))].group(),
959                        line!(),
960                        "where",
961                    ]
962                    .group()
963                    .nest(INDENT),
964                    docs![
965                        hardline!(),
966                        intersperse!(
967                            items.iter().filter(|item| {
968                                // TODO: should be treated directly by name rendering, see :
969                                // https://github.com/cryspen/hax/issues/1646
970                                !(item.ident.is_precondition() || item.ident.is_postcondition())
971                            }),
972                            hardline!()
973                        )
974                    ]
975                    .nest(INDENT),
976                ],
977                _ => todo!("-- unsupported item"),
978            }
979        }
980
981        fn trait_item(
982            &'a self,
983            TraitItem {
984                meta: _,
985                kind,
986                generics,
987                ident,
988            }: &'b TraitItem,
989        ) -> DocBuilder<'a, Self, A> {
990            let name = self.render_last(ident);
991            docs![match kind {
992                TraitItemKind::Fn(ty) => {
993                    docs![name, softline!(), generics, ":", line!(), ty]
994                        .group()
995                        .nest(INDENT)
996                }
997                TraitItemKind::Type(constraints) => {
998                    docs![
999                        name.clone(),
1000                        reflow!(" : Type"),
1001                        concat!(constraints.iter().map(|c| docs![
1002                                hardline!(),
1003                                docs![format!("_constr_{}", c.name),
1004                                reflow!(" :"),
1005                                line!(),
1006                                &c.goal
1007                            ]
1008                                .group()
1009                                .nest(INDENT)
1010                            .brackets()]))
1011                    ]
1012                }
1013                _ => todo!("-- unsupported trait item"),
1014            }]
1015        }
1016
1017        fn impl_item(
1018            &'a self,
1019            ImplItem {
1020                meta: _,
1021                generics,
1022                kind,
1023                ident,
1024            }: &'b ImplItem,
1025        ) -> DocBuilder<'a, Self, A> {
1026            let name = self.render_last(ident);
1027            match kind {
1028                ImplItemKind::Type {
1029                    ty,
1030                    parent_bounds: _,
1031                } => docs![name, reflow!(" := "), ty],
1032                ImplItemKind::Fn { body, params } => docs![
1033                    docs![
1034                        name,
1035                        softline!(),
1036                        generics,
1037                        zip_right!(params, line!()).group(),
1038                        ":= do",
1039                    ]
1040                    .group(),
1041                    line!(),
1042                    body
1043                ]
1044                .group()
1045                .nest(INDENT),
1046                ImplItemKind::Resugared(_) => todo!(),
1047            }
1048        }
1049
1050        fn impl_ident(
1051            &'a self,
1052            ImplIdent { goal, name: _ }: &'b ImplIdent,
1053        ) -> DocBuilder<'a, Self, A> {
1054            docs![goal]
1055        }
1056
1057        fn trait_goal(
1058            &'a self,
1059            TraitGoal { trait_, args }: &'b TraitGoal,
1060        ) -> DocBuilder<'a, Self, A> {
1061            docs![trait_, concat!(args.iter().map(|arg| docs![line!(), arg]))]
1062                .parens()
1063                .nest(INDENT)
1064                .group()
1065        }
1066
1067        fn variant(
1068            &'a self,
1069            Variant {
1070                name,
1071                arguments,
1072                is_record,
1073                attributes: _,
1074            }: &'b Variant,
1075        ) -> DocBuilder<'a, Self, A> {
1076            docs![
1077                self.render_last(name),
1078                softline!(),
1079                // args
1080                if *is_record {
1081                    // Use named the arguments, keeping only the head of the identifier
1082                    docs![
1083                        intersperse!(
1084                            arguments.iter().map(|(id, ty, _)| {
1085                                docs![self.render_last(id), reflow!(" : "), ty]
1086                                    .parens()
1087                                    .group()
1088                            }),
1089                            line!()
1090                        )
1091                        .align()
1092                        .nest(INDENT),
1093                        line!(),
1094                        reflow!(": "),
1095                    ]
1096                    .group()
1097                } else {
1098                    // Use anonymous arguments
1099                    docs![
1100                        reflow!(": "),
1101                        concat!(
1102                            arguments
1103                                .iter()
1104                                .map(|(_, ty, _)| { docs![ty, reflow!(" -> ")] })
1105                        )
1106                    ]
1107                }
1108            ]
1109            .group()
1110            .nest(INDENT)
1111        }
1112    }
1113};
hax_rust_engine/backends/lean.rs

hax_rust_engine/backends/
lean.rs
