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 hax_lib_macros_types::AttrPayload;
8use std::collections::HashSet;
9use std::sync::LazyLock;
10
11use super::prelude::*;
12use crate::{
13    ast::identifiers::global_id::view::{ConstructorKind, PathSegment, TypeDefKind},
14    attributes::hax_attributes,
15    names::rust_primitives::hax::explicit_monadic::{lift, pure},
16    phase::*,
17};
18
19mod binops {
20    pub use crate::names::core::ops::index::*;
21    pub use crate::names::rust_primitives::hax::machine_int::*;
22    pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
23}
24
25const LIFT: GlobalId = lift;
26const PURE: GlobalId = pure;
27
28/// The Lean printer
29#[setup_printer_struct]
30#[derive(Default, Clone)]
31pub struct LeanPrinter;
32
33const INDENT: isize = 2;
34
35static RESERVED_KEYWORDS: LazyLock<HashSet<String>> = LazyLock::new(|| {
36    HashSet::from_iter(
37        [
38            // reserved for Lean:
39            "end",
40            "def",
41            "abbrev",
42            "theorem",
43            "example",
44            "inductive",
45            "structure",
46            "from",
47            // reserved for hax encoding:
48            "associatedTypes",
49            "AssociatedTypes",
50        ]
51        .iter()
52        .map(|s| s.to_string()),
53    )
54});
55
56impl RenderView for LeanPrinter {
57    fn separator(&self) -> &str {
58        "."
59    }
60    fn render_path_segment(&self, chunk: &PathSegment) -> Vec<String> {
61        fn uppercase_first(s: &str) -> String {
62            let mut c = s.chars();
63            match c.next() {
64                None => String::new(),
65                Some(first) => first.to_uppercase().collect::<String>() + c.as_str(),
66            }
67        }
68        // Returning None indicates that the default rendering should be used
69        (match chunk.kind() {
70            AnyKind::Mod => {
71                let mut chunks = default::render_path_segment(self, chunk);
72                for c in &mut chunks {
73                    *c = uppercase_first(c);
74                }
75                Some(chunks)
76            }
77            AnyKind::Constructor(ConstructorKind::Constructor { ty })
78                if matches!(ty.kind(), TypeDefKind::Struct) =>
79            {
80                Some(vec![
81                    self.render_path_segment_payload(chunk.payload())
82                        .to_string(),
83                    "mk".to_string(),
84                ])
85            }
86            AnyKind::Field { named: _, parent } => match parent.kind() {
87                ConstructorKind::Constructor { ty }
88                    if matches!(&ty.kind(), TypeDefKind::Struct) =>
89                {
90                    chunk.parent().map(|parent| {
91                        vec![
92                            self.escape(
93                                self.render_path_segment_payload(parent.payload())
94                                    .to_string(),
95                            ),
96                            self.escape(
97                                self.render_path_segment_payload(chunk.payload())
98                                    .to_string(),
99                            ),
100                        ]
101                    })
102                }
103                _ => None,
104            },
105            _ => None,
106        })
107        .unwrap_or(default::render_path_segment(self, chunk))
108    }
109}
110
111impl Printer for LeanPrinter {
112    fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
113        vec![
114            Box::new(BinOp::new(&[
115                binops::add,
116                binops::sub,
117                binops::mul,
118                binops::rem,
119                binops::div,
120                binops::shr,
121                binops::shl,
122                binops::bitand,
123                binops::bitxor,
124                binops::logical_op_and,
125                binops::logical_op_or,
126                binops::Index::index,
127            ])),
128            Box::new(FunctionsToConstants),
129            Box::new(LetPure),
130        ]
131    }
132}
133
134/// The Lean backend
135pub struct LeanBackend;
136
137impl Backend for LeanBackend {
138    type Printer = LeanPrinter;
139
140    fn module_path(&self, module: &Module) -> camino::Utf8PathBuf {
141        camino::Utf8PathBuf::from_iter(LeanPrinter::default().render_strings(&module.ident.view()))
142            .with_extension("lean")
143    }
144
145    fn phases(&self) -> Vec<Box<dyn Phase>> {
146        vec![Box::new(ExplicitMonadic)]
147    }
148}
149
150impl LeanPrinter {
151    /// A filter for items blacklisted by the Lean backend : returns false if
152    /// the item is definitely not printable, but might return true on
153    /// unsupported items
154    pub fn printable_item(item: &Item) -> bool {
155        match &item.kind {
156            // Other unprintable items
157            ItemKind::Error(_) | ItemKind::NotImplementedYet | ItemKind::Use { .. } => false,
158            // Printable items
159            ItemKind::Fn { .. }
160            | ItemKind::TyAlias { .. }
161            | ItemKind::Type { .. }
162            | ItemKind::Trait { .. }
163            | ItemKind::Impl { .. }
164            | ItemKind::Alias { .. }
165            | ItemKind::Resugared(_)
166            | ItemKind::Quote { .. } => true,
167        }
168    }
169
170    /// Render a global id using the Rendering strategy of the Lean printer. Works for both concrete
171    /// and projector ids. TODO: https://github.com/cryspen/hax/issues/1660
172    pub fn render_id(&self, id: &GlobalId) -> String {
173        self.render_string(&id.view())
174    }
175
176    /// Escapes local identifiers (prefixing reserved keywords with an underscore).
177    /// TODO: This should be treated directly in the name rendering engine, see
178    /// https://github.com/cryspen/hax/issues/1630
179    pub fn escape(&self, id: String) -> String {
180        let id = id.replace([' ', '<', '>'], "_");
181        if id.is_empty() {
182            "_ERROR_EMPTY_ID_".to_string()
183        } else if RESERVED_KEYWORDS.contains(&id)
184            || id.starts_with("trait_constr_")
185            || id.starts_with(|c: char| c.is_ascii_digit())
186        {
187            format!("_{id}")
188        } else {
189            id
190        }
191    }
192
193    /// Renders the last, most local part of an id. Used for named arguments of constructors.
194    pub fn render_last(&self, id: &GlobalId) -> String {
195        let id = self
196            .render(&id.view())
197            .path
198            .last()
199            // TODO: Should be ensured by the rendering engine; see
200            // https://github.com/cryspen/hax/issues/1660
201            .expect("Segments should always be non-empty")
202            .clone();
203        self.escape(id)
204    }
205}
206
207/// Render parameters, adding a line after each parameter
208impl<A: 'static + Clone> ToDocument<LeanPrinter, A> for Vec<Param> {
209    fn to_document(&self, printer: &LeanPrinter) -> DocBuilder<A> {
210        printer.params(self)
211    }
212}
213
214#[prepend_associated_functions_with(install_pretty_helpers!(self: Self))]
215const _: () = {
216    // Emits a CLI error with a github issue number, and prints "sorry" in the lean output
217    macro_rules! emit_error {($($tt:tt)*) => {disambiguated_todo!($($tt)*)};}
218
219    // Insert a new line in a doc (pretty)
220    macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
221
222    // Concatenate docs (pretty )
223    macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};}
224
225    // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `ASBS...CS`
226    macro_rules! zip_right {
227        ($a:expr, $sep:expr) => {
228            docs![concat!($a.into_iter().map(|a| docs![a, $sep]))]
229        };
230    }
231
232    // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `SASB...SC`
233    macro_rules! zip_left {
234        ($sep:expr, $a:expr) => {
235            docs![concat!($a.into_iter().map(|a| docs![$sep, a]))]
236        };
237    }
238
239    // Prints a one-line comment
240    macro_rules! comment {
241        ($e:expr) => {
242            docs!["-- ", $e]
243        };
244    }
245
246    // Extra methods, specific to the LeanPrinter
247    impl LeanPrinter {
248        /// Prints arguments a variant or constructor of struct, using named or unamed arguments based
249        /// on the `is_record` flag. Used for both expressions and patterns
250        pub fn arguments<A: 'static + Clone, D>(
251            &self,
252            fields: &[(GlobalId, D)],
253            is_record: &bool,
254        ) -> DocBuilder<A>
255        where
256            D: ToDocument<Self, A>,
257        {
258            if *is_record {
259                self.named_arguments(fields)
260            } else {
261                self.positional_arguments(fields)
262            }
263        }
264
265        /// Prints fields of structures (when in braced notation)
266        fn struct_fields<A: 'static + Clone, D>(&self, fields: &[(GlobalId, D)]) -> DocBuilder<A>
267        where
268            D: ToDocument<Self, A>,
269        {
270            docs![intersperse!(
271                fields
272                    .iter()
273                    .map(|(id, e)| { docs![self.render_last(id), reflow!(" := "), e].group() }),
274                docs![",", line!()]
275            )]
276            .group()
277        }
278        /// Prints named arguments (record) of a variant or constructor of struct
279        fn named_arguments<A: 'static + Clone, D>(&self, fields: &[(GlobalId, D)]) -> DocBuilder<A>
280        where
281            D: ToDocument<Self, A>,
282        {
283            docs![intersperse!(
284                fields.iter().map(|(id, e)| {
285                    docs![self.render_last(id), reflow!(" := "), e]
286                        .parens()
287                        .group()
288                }),
289                line!()
290            )]
291            .group()
292        }
293
294        /// Prints positional arguments (tuple) of a variant or constructor of struct
295        fn positional_arguments<A: 'static + Clone, D>(
296            &self,
297            fields: &[(GlobalId, D)],
298        ) -> DocBuilder<A>
299        where
300            D: ToDocument<Self, A>,
301        {
302            docs![intersperse!(fields.iter().map(|(_, e)| e), line!())].group()
303        }
304
305        /// Prints parameters of functions (items, trait items, impl items)
306        fn params<A: 'static + Clone>(&self, params: &Vec<Param>) -> DocBuilder<A> {
307            zip_right!(params, line!())
308        }
309
310        /// Renders expressions with an explicit ascription `(e : RustM ty)`. Used for the body of closure, for
311        /// numeric literals, etc.
312        fn expr_typed_result<A: 'static + Clone>(&self, expr: &Expr) -> DocBuilder<A> {
313            docs![
314                expr,
315                reflow!(" : "),
316                docs!["RustM", line!(), &expr.ty].group()
317            ]
318            .group()
319        }
320
321        fn pat_typed<A: 'static + Clone>(&self, pat: &Pat) -> DocBuilder<A> {
322            docs![pat, reflow!(" :"), line!(), &pat.ty].parens().group()
323        }
324
325        fn do_block<A: 'static + Clone, D: ToDocument<Self, A>>(&self, body: D) -> DocBuilder<A> {
326            docs!["do", line!(), body].group()
327        }
328
329        /// Produces a name for a constraint on an trait-level constraint, or an associated
330        /// type. The name is obtained by combining the type it applies to and the name of the
331        /// constraint (and should be unique)
332        fn constraint_name(&self, type_name: &String, constraint: &ImplIdent) -> String {
333            format!("trait_constr_{}_{}", type_name, constraint.name)
334        }
335
336        /// Renders a named argument for associated types with equality constraints
337        /// (aka projections). If there are no equality constraints, returns None.
338        fn associated_type_projections<A: 'static + Clone>(
339            &self,
340            impl_ident: &ImplIdent,
341            projections: Vec<DocBuilder<A>>,
342        ) -> Option<DocBuilder<A>> {
343            (!projections.is_empty()).then_some(
344                docs![
345                    "(associatedTypes := {",
346                    line!(),
347                    docs![
348                        "show",
349                        line!(),
350                        impl_ident.goal.trait_,
351                        ".AssociatedTypes",
352                        concat!(impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])),
353                    ]
354                    .group()
355                    .nest(INDENT),
356                    line!(),
357                    reflow!("by infer_instance"),
358                    line!(),
359                    docs![
360                        "with",
361                        line!(),
362                        intersperse!(projections, docs![",", line!()]),
363                    ]
364                    .group()
365                    .nest(INDENT),
366                    "})"
367                ]
368                .group()
369                .nest(INDENT),
370            )
371        }
372
373        /// Turns an expression of type `RustM T` into one of type `T` (out of the monad), providing
374        /// reflexivity as a proof witness.
375        fn monad_extract<A: 'static + Clone>(&self, expr: &Expr) -> DocBuilder<A> {
376            match *expr.kind() {
377                ExprKind::Literal(_) | ExprKind::GlobalId(_) | ExprKind::LocalId(_) => {
378                    // Pure values are displayed directly. Note that constructors, while pure, may
379                    // contain sub-expressions that are not, so they must be wrapped in a do-block
380                    docs![expr]
381                }
382                _ => {
383                    // All other expressions are wrapped in a do-block, and extracted out of the monad
384                    docs![
385                        "RustM.of_isOk",
386                        line!(),
387                        self.do_block(expr).parens(),
388                        line!(),
389                        "(by rfl)"
390                    ]
391                    .group()
392                    .nest(INDENT)
393                }
394            }
395        }
396
397        /// Print trait items, adding trait-level params as extra arguments
398        fn trait_item_with_trait_params<A: 'static + Clone>(
399            &self,
400            trait_generics: &[GenericParam],
401            TraitItem {
402                meta: _,
403                kind,
404                generics: item_generics,
405                ident,
406            }: &TraitItem,
407        ) -> DocBuilder<A> {
408            {
409                let name = self.render_last(ident);
410                let trait_generics = intersperse!(
411                    trait_generics
412                        .iter()
413                        .map(|GenericParam { ident, .. }| ident),
414                    softline!()
415                )
416                .parens()
417                .group()
418                .append(line!());
419                docs![match kind {
420                    TraitItemKind::Fn(ty) => {
421                        docs![
422                            name,
423                            softline!(),
424                            trait_generics,
425                            item_generics,
426                            ":",
427                            line!(),
428                            ty
429                        ]
430                        .group()
431                        .nest(INDENT)
432                    }
433                    TraitItemKind::Type(_) => {
434                        docs![name.clone(), softline!(), ":", line!(), "Type"]
435                            .group()
436                            .nest(INDENT)
437                    }
438                    TraitItemKind::Default { params, body } => docs![
439                        docs![
440                            name,
441                            softline!(),
442                            trait_generics,
443                            item_generics,
444                            zip_right!(params, line!()).group(),
445                            docs![": RustM ", body.ty].group(),
446                            line!(),
447                            ":= do",
448                        ]
449                        .group(),
450                        line!(),
451                        body,
452                    ]
453                    .group()
454                    .nest(INDENT),
455                    TraitItemKind::Resugared(_) => {
456                        unreachable!("This backend has no resugaring for trait items")
457                    }
458                }]
459            }
460        }
461
462        /// Print spec of an item
463        fn spec<A: 'static + Clone>(
464            &self,
465            item: &Item,
466            name: &GlobalId,
467            generics: &Generics,
468            params: &Vec<Param>,
469        ) -> DocBuilder<A> {
470            let spec = HasLinkedItemGraph::linked_item_graph(self)
471                .fn_like_linked_expressions(item, item.self_id());
472            if spec.precondition.is_none() && spec.postcondition.is_none() {
473                nil!()
474            } else {
475                let proofs: Vec<&String> = hax_attributes(&item.meta.attributes)
476                    .flat_map(|attr| match attr {
477                        AttrPayload::Proof(proof) => Some(proof),
478                        _ => None,
479                    })
480                    .collect();
481                if proofs.len() > 1 {
482                    emit_error!("Only one proof attribute per item is allowed.");
483                }
484                docs![
485                    hardline!(),
486                    hardline!(),
487                    "@[spec]",
488                    hardline!(),
489                    docs![
490                        docs![
491                            "def",
492                            line!(),
493                            name,
494                            ".spec",
495                            line!(),
496                            generics,
497                            params,
498                            softline!(),
499                            ":"
500                        ]
501                        .group()
502                        .nest(INDENT),
503                        line!(),
504                        docs![
505                            "Spec",
506                            line!(),
507                            docs![
508                                "requires",
509                                softline!(),
510                                ":= do",
511                                line!(),
512                                spec.precondition.map_or(reflow!("pure True"), |p| docs![p])
513                            ]
514                            .parens()
515                            .group()
516                            .nest(INDENT),
517                            line!(),
518                            docs![
519                                "ensures := ",
520                                spec.postcondition
521                                    .map_or(reflow!("fun _ => pure True"), |p| docs![
522                                        "fun",
523                                        line!(),
524                                        p.result_binder,
525                                        softline!(),
526                                        "=> do",
527                                        line!(),
528                                        p.body,
529                                    ]
530                                    .group()
531                                    .nest(INDENT)),
532                            ]
533                            .parens()
534                            .group()
535                            .nest(INDENT),
536                            line!(),
537                            docs![name, line!(), generics, params]
538                                .parens()
539                                .group()
540                                .nest(INDENT)
541                        ]
542                        .group()
543                        .nest(INDENT),
544                        softline!(),
545                        ":=",
546                    ]
547                    .group()
548                    .nest(2 * INDENT),
549                    softline!(),
550                    docs![
551                        hardline!(),
552                        "pureRequires := by constructor; mvcgen <;> try grind",
553                        hardline!(),
554                        "pureEnsures := by constructor; intros; mvcgen <;> try grind",
555                        hardline!(),
556                        docs![
557                            "contract :=",
558                            line!(),
559                            if proofs.is_empty() {
560                                docs!["by mvcgen[", name, "] <;> try grind"]
561                            } else {
562                                docs![intersperse!(proofs, nil!())]
563                            }
564                        ]
565                        .group()
566                        .nest(INDENT),
567                        hardline!(),
568                    ]
569                    .nest(INDENT)
570                    .braces(),
571                ]
572            }
573        }
574    }
575
576    impl<A: 'static + Clone> ToDocument<LeanPrinter, A> for (Vec<GenericParam>, &TraitItem) {
577        fn to_document(&self, printer: &LeanPrinter) -> DocBuilder<A> {
578            printer.trait_item_with_trait_params(&self.0, self.1)
579        }
580    }
581
582    impl<A: 'static + Clone> PrettyAst<A> for LeanPrinter {
583        const NAME: &'static str = "Lean";
584
585        /// Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [`todo_document!`].
586        fn todo_document(&self, message: &str, issue_id: Option<u32>) -> DocBuilder<A> {
587            <Self as PrettyAst<A>>::emit_diagnostic(
588                self,
589                hax_types::diagnostics::Kind::Unimplemented {
590                    issue_id,
591                    details: Some(message.into()),
592                },
593            );
594            text!("sorry")
595        }
596
597        fn module(&self, module: &Module) -> DocBuilder<A> {
598            let items = &module.items;
599            docs![
600                intersperse!(
601                    "
602-- Experimental lean backend for Hax
603-- The Hax prelude library can be found in hax/proof-libs/lean
604import Hax
605import Std.Tactic.Do
606import Std.Do.Triple
607import Std.Tactic.Do.Syntax
608open Std.Do
609open Std.Tactic
610
611set_option mvcgen.warning false
612set_option linter.unusedVariables false
613
614
615"
616                    .lines(),
617                    hardline!(),
618                ),
619                intersperse!(
620                    items
621                        .iter()
622                        .filter(|item| LeanPrinter::printable_item(item)),
623                    docs![hardline!(), hardline!()]
624                )
625            ]
626        }
627
628        fn global_id(&self, global_id: &GlobalId) -> DocBuilder<A> {
629            docs![self.render_id(global_id)]
630        }
631
632        /// Render generics, adding a space after each parameter
633        fn generics(&self, generics: &Generics) -> DocBuilder<A> {
634            docs![
635                zip_right!(&generics.params, line!()),
636                zip_right!(
637                    generics.type_constraints().map(|impl_ident| {
638                        let projections = generics
639                            .projection_constraints()
640                            .filter(|p| !matches!(&*p.impl_.kind, ImplExprKind::LocalBound { id } if *id != impl_ident.name ))
641                            .map(|p| {
642                                if let ImplExprKind::LocalBound { .. } = &*p.impl_.kind {
643                                    docs![p]
644                                } else {
645                                    emit_error!(issue 1710, "Unsupported variant of associated type projection")
646                                }
647                            })
648                            .collect::<Vec<_>>();
649                        docs![
650                            docs![
651                                impl_ident.goal.trait_,
652                                ".AssociatedTypes",
653                                concat!(
654                                    impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
655                                )
656                            ]
657                            .brackets()
658                            .group()
659                            .nest(INDENT),
660                            line!(),
661                            docs![
662                                impl_ident.goal.trait_,
663                                concat!(
664                                    impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
665                                ),
666                                line!(),
667                                self.associated_type_projections(impl_ident, projections)
668                            ]
669                            .brackets()
670                            .nest(INDENT)
671                            .group()
672                        ]
673                        .group()
674                    }),
675                    line!()
676                ),
677            ]
678            .group()
679        }
680
681        fn generic_constraint(&self, _: &GenericConstraint) -> DocBuilder<A> {
682            unreachable!(
683                "Generic constraints are rendered inline because they must contain associated type projections."
684            )
685        }
686
687        fn generic_param(&self, generic_param: &GenericParam) -> DocBuilder<A> {
688            match generic_param.kind() {
689                GenericParamKind::Type => docs![&generic_param.ident, reflow!(" : Type")]
690                    .parens()
691                    .group(),
692                GenericParamKind::Lifetime => unreachable_by_invariant!(Drop_references),
693                GenericParamKind::Const { ty } => docs![&generic_param.ident, reflow!(" : "), ty]
694                    .parens()
695                    .group(),
696            }
697        }
698
699        fn generic_value(&self, generic_value: &GenericValue) -> DocBuilder<A> {
700            match generic_value {
701                GenericValue::Ty(ty) => docs![ty],
702                GenericValue::Expr(expr) => docs![self.monad_extract(expr)].parens(),
703                GenericValue::Lifetime => unreachable_by_invariant!(Drop_references),
704            }
705        }
706
707        fn expr(&self, Expr { kind, ty, meta: _ }: &Expr) -> DocBuilder<A> {
708            match &**kind {
709                ExprKind::If {
710                    condition,
711                    then,
712                    else_,
713                } => {
714                    if let Some(else_branch) = else_ {
715                        docs![
716                            docs!["if", line!(), condition, reflow!(" then")].group(),
717                            docs![line!(), then].nest(INDENT),
718                            line!(),
719                            "else",
720                            docs![line!(), else_branch].nest(INDENT)
721                        ]
722                        .group()
723                    } else {
724                        unreachable_by_invariant!(Local_mutation)
725                    }
726                }
727                ExprKind::App {
728                    head,
729                    args,
730                    generic_args,
731                    bounds_impls: _,
732                    trait_,
733                } => {
734                    match (&args[..], &generic_args[..], head.kind()) {
735                        ([arg], [], ExprKind::GlobalId(LIFT)) => docs![reflow!("← "), arg].parens(),
736                        ([arg], [], ExprKind::GlobalId(PURE)) => {
737                            docs![reflow!("pure "), arg].parens()
738                        }
739                        _ => {
740                            // Fallback for any application
741                            docs![
742                                head,
743                                trait_
744                                    .as_ref()
745                                    .map(|(impl_expr, _)| zip_left!(line!(), &impl_expr.goal.args)),
746                                zip_left!(line!(), generic_args).group(),
747                                zip_left!(line!(), args).group(),
748                            ]
749                            .parens()
750                            .nest(INDENT)
751                            .group()
752                        }
753                    }
754                }
755                ExprKind::Literal(numeric_lit @ (Literal::Float { .. } | Literal::Int { .. })) => {
756                    docs![numeric_lit, reflow!(" : "), ty].parens().group()
757                }
758                ExprKind::Literal(literal) => docs![literal],
759                ExprKind::Array(exprs) => docs![
760                    "#v[",
761                    intersperse!(exprs, docs![",", line!()])
762                        .nest(INDENT)
763                        .group()
764                        .align(),
765                    "]"
766                ]
767                .group(),
768                ExprKind::Construct {
769                    constructor,
770                    is_record,
771                    is_struct,
772                    fields,
773                    base,
774                } => {
775                    if fields.is_empty() && base.is_none() {
776                        docs![constructor]
777                    } else if let Some(base) = base {
778                        if !(*is_record && *is_struct) {
779                            unreachable!(
780                                "Constructors with base expressions are necessarily structs with record-like arguments"
781                            )
782                        }
783                        docs![base, line!(), reflow!("with "), self.struct_fields(fields)]
784                            .braces()
785                            .group()
786                    } else {
787                        docs![constructor, line!(), self.arguments(fields, is_record)]
788                            .nest(INDENT)
789                            .parens()
790                            .group()
791                    }
792                }
793                ExprKind::Let { lhs, rhs, body }
794                | ExprKind::Resugared(ResugaredExprKind::LetPure { lhs, rhs, body }) => {
795                    let binder = if matches!(**kind, ExprKind::Let { .. }) {
796                        " ←"
797                    } else {
798                        " :="
799                    };
800                    docs![
801                        docs![
802                            docs![
803                                "let",
804                                line!(),
805                                // TODO: Improve treatment of patterns in general. see
806                                // https://github.com/cryspen/hax/issues/1712
807                                match *lhs.kind.clone() {
808                                    PatKind::Ascription { .. } =>
809                                        docs![lhs, reflow!(" : "), &lhs.ty],
810                                    PatKind::Binding {
811                                        mutable: false,
812                                        var,
813                                        mode: BindingMode::ByValue,
814                                        sub_pat: None,
815                                    } => docs![&var, reflow!(" : "), &lhs.ty],
816                                    _ => docs![lhs],
817                                },
818                            ]
819                            .group(),
820                            binder,
821                            line!(),
822                            rhs,
823                            ";"
824                        ]
825                        .nest(INDENT)
826                        .group(),
827                        line!(),
828                        body,
829                    ]
830                }
831                ExprKind::GlobalId(global_id) => docs![global_id],
832                ExprKind::LocalId(local_id) => docs![local_id],
833                ExprKind::Ascription { e, ty } => docs![e, reflow!(" : "), ty].parens().group(),
834                ExprKind::Closure {
835                    params,
836                    body,
837                    captures: _,
838                } => docs![
839                    reflow!("fun "),
840                    intersperse!(params, line!()).group(),
841                    reflow!(" => "),
842                    self.do_block(self.expr_typed_result(body)).parens()
843                ]
844                .parens()
845                .group()
846                .nest(INDENT),
847
848                ExprKind::Resugared(ResugaredExprKind::BinOp { op, lhs, rhs, .. }) => {
849                    // TODO : refactor this, moving this code directly in the `App` node (see
850                    // https://github.com/cryspen/hax/issues/1705)
851                    if *op == binops::Index::index {
852                        return docs![lhs, "[", line_!(), rhs, line_!(), "]_?"]
853                            .nest(INDENT)
854                            .group();
855                    }
856                    let symbol = match *op {
857                        binops::add => "+?",
858                        binops::sub => "-?",
859                        binops::mul => "*?",
860                        binops::div => "/?",
861                        binops::rem => "%?",
862                        binops::shr => ">>>?",
863                        binops::shl => "<<<?",
864                        binops::bitand => "&&&?",
865                        binops::bitxor => "^^^?",
866                        binops::logical_op_and => "&&?",
867                        binops::logical_op_or => "||?",
868                        _ => unreachable!(),
869                    };
870                    docs![lhs, line!(), docs![symbol, softline!(), rhs].group()]
871                        .group()
872                        .nest(INDENT)
873                        .parens()
874                }
875                ExprKind::Resugared(ResugaredExprKind::Tuple { .. }) => {
876                    unreachable!("This printer doesn't use the tuple resugaring")
877                }
878                ExprKind::Match { scrutinee, arms } => docs![
879                    docs![
880                        "match",
881                        docs![line!(), scrutinee].nest(INDENT),
882                        line!(),
883                        "with"
884                    ]
885                    .group(),
886                    docs![line!(), intersperse!(arms, line!())]
887                        .group()
888                        .nest(INDENT),
889                ]
890                .group(),
891
892                ExprKind::Borrow { .. } | ExprKind::Deref(_) => {
893                    unreachable_by_invariant!(Drop_references)
894                }
895                ExprKind::AddressOf { .. } => unreachable_by_invariant!(Reject_raw_or_mut_pointer),
896                ExprKind::Assign { .. } => unreachable_by_invariant!(Local_mutation),
897                ExprKind::Loop { .. } => unreachable_by_invariant!(Functionalize_loops),
898                ExprKind::Break { .. } | ExprKind::Return { .. } | ExprKind::Continue { .. } => {
899                    unreachable_by_invariant!(Drop_break_continue_return)
900                }
901                ExprKind::Block { .. } => unreachable_by_invariant!(Drop_blocks),
902                ExprKind::Quote { contents } => docs![contents],
903                ExprKind::Error(error_node) => docs![error_node],
904            }
905        }
906
907        fn arm(&self, arm: &Arm) -> DocBuilder<A> {
908            if let Some(_guard) = &arm.guard {
909                unreachable_by_invariant!(Drop_match_guards)
910            } else {
911                docs![
912                    reflow!("| "),
913                    &arm.pat,
914                    line!(),
915                    docs!["=>", line!(), &arm.body].nest(INDENT).group()
916                ]
917                .nest(INDENT)
918                .group()
919            }
920        }
921
922        fn pat(&self, pat: &Pat) -> DocBuilder<A> {
923            match &*pat.kind {
924                PatKind::Wild => docs!["_"],
925                PatKind::Ascription { pat, ty: _ } => docs![pat],
926                PatKind::Binding {
927                    mutable,
928                    var,
929                    mode,
930                    sub_pat,
931                } => match (mutable, mode, sub_pat) {
932                    (true, _, _) => unreachable_by_invariant!(Local_mutation),
933                    (false, BindingMode::ByRef(_), _) => unreachable_by_invariant!(Drop_references),
934                    (false, BindingMode::ByValue, None) => docs![var],
935                    (false, BindingMode::ByValue, Some(pat)) => {
936                        docs![var, "@", softline_!(), pat].group()
937                    }
938                },
939                PatKind::Or { sub_pats } => docs![intersperse!(sub_pats, reflow!(" | "))].group(),
940                PatKind::Array { .. } => {
941                    emit_error!(issue 1712, "Unsupported pattern-matching on arrays")
942                }
943                PatKind::Deref { .. } => unreachable_by_invariant!(Drop_references),
944                PatKind::Constant {
945                    lit: Literal::Float { .. },
946                } => {
947                    emit_error!(issue 1788, "Unsupported pattern-matching on floats")
948                }
949                PatKind::Constant { lit } => docs![lit],
950                PatKind::Construct {
951                    constructor,
952                    is_record,
953                    is_struct,
954                    fields,
955                } => {
956                    if *is_struct {
957                        if !*is_record {
958                            // Tuple-like structure, using positional arguments
959                            docs![
960                                "⟨",
961                                intersperse!(
962                                    fields.iter().map(|field| { docs![&field.1] }),
963                                    docs![",", line!()]
964                                )
965                                .align()
966                                .group(),
967                                "⟩"
968                            ]
969                            .align()
970                            .group()
971                        } else {
972                            // Structure-like structure, using named arguments
973                            docs![intersperse!(
974                                fields.iter().map(|(id, pat)| {
975                                    docs![self.render_last(id), reflow!(" := "), pat].group()
976                                }),
977                                docs![",", line!()]
978                            )]
979                            .align()
980                            .braces()
981                            .group()
982                        }
983                    } else {
984                        // Variant
985                        docs![
986                            constructor,
987                            line!(),
988                            self.arguments(fields, is_record).align()
989                        ]
990                        .parens()
991                        .group()
992                        .nest(INDENT)
993                    }
994                }
995                PatKind::Resugared(_) => {
996                    unreachable!("This backend does not use resugarings on patterns")
997                }
998                PatKind::Error(_) => {
999                    // TODO : Should be made unreachable by https://github.com/cryspen/hax/pull/1672
1000                    text!("sorry")
1001                }
1002            }
1003        }
1004
1005        fn ty(&self, ty: &Ty) -> DocBuilder<A> {
1006            match ty.kind() {
1007                TyKind::Primitive(primitive_ty) => docs![primitive_ty],
1008                TyKind::App { head, args } => {
1009                    if args.is_empty() {
1010                        docs![head]
1011                    } else {
1012                        docs![head, zip_left!(line!(), args)]
1013                            .parens()
1014                            .group()
1015                            .nest(INDENT)
1016                    }
1017                }
1018                TyKind::Arrow { inputs, output } => docs![
1019                    zip_right!(inputs, docs![line!(), reflow!("-> ")]),
1020                    "RustM ",
1021                    output
1022                ]
1023                .parens()
1024                .group(),
1025                TyKind::Param(local_id) => docs![local_id],
1026                TyKind::Slice(ty) => docs!["RustSlice", line!(), ty].parens().group(),
1027                TyKind::Array { ty, length } => docs!["RustArray", line!(), ty, line!(), {
1028                    if let ExprKind::Literal(int_lit @ Literal::Int { .. }) = length.kind() {
1029                        docs![int_lit]
1030                    } else if let ExprKind::LocalId(local_id) = length.kind() {
1031                        docs![local_id]
1032                    } else {
1033                        unreachable!(
1034                            "Only arrays with integer literal or const param size are supported"
1035                        )
1036                    }
1037                }]
1038                .parens()
1039                .group(),
1040                TyKind::AssociatedType { impl_, item } => {
1041                    let kind = impl_.kind();
1042                    match &kind {
1043                        ImplExprKind::Self_ => docs!["associatedTypes.", self.render_last(item)],
1044                        ImplExprKind::LocalBound { .. } => docs![
1045                            item,
1046                            concat!(impl_.goal.args.iter().map(|arg| docs![line!(), arg])),
1047                        ]
1048                        .parens()
1049                        .group()
1050                        .nest(INDENT),
1051                        _ => {
1052                            emit_error!(issue 1710, "Unsupported variant of associated type")
1053                        }
1054                    }
1055                }
1056                TyKind::Ref { .. } => unreachable_by_invariant!(Drop_references),
1057                TyKind::RawPointer => unreachable_by_invariant!(Reject_raw_or_mut_pointer),
1058                TyKind::Opaque(_) => emit_error!(issue 1714, "Unsupported opaque type definitions"),
1059                TyKind::Dyn(_) => emit_error!(issue 1708, "Unsupported `dyn` traits"),
1060                TyKind::Resugared(resugared_ty_kind) => match resugared_ty_kind {
1061                    ResugaredTyKind::Tuple(_) => {
1062                        unreachable!("This backend does not use tuple resugaring (yet)")
1063                    }
1064                },
1065                TyKind::Error(e) => docs![e],
1066            }
1067        }
1068
1069        fn literal(&self, literal: &Literal) -> DocBuilder<A> {
1070            docs![match literal {
1071                Literal::String(symbol) => format!("\"{symbol}\""),
1072                Literal::Char(c) => format!("'{c}'"),
1073                Literal::Bool(b) => format!("{b}"),
1074                Literal::Int {
1075                    value,
1076                    negative,
1077                    kind: _,
1078                } => format!("{}{value}", if *negative { "-" } else { "" }),
1079                Literal::Float {
1080                    value,
1081                    negative,
1082                    kind: _,
1083                } => format!("{}{value}", if *negative { "-" } else { "" }),
1084            }]
1085        }
1086
1087        fn local_id(&self, local_id: &LocalId) -> DocBuilder<A> {
1088            // TODO: should be done by name rendering, see https://github.com/cryspen/hax/issues/1630
1089            docs![self.escape(local_id.0.to_string())]
1090        }
1091
1092        fn spanned_ty(&self, spanned_ty: &SpannedTy) -> DocBuilder<A> {
1093            docs![&spanned_ty.ty]
1094        }
1095
1096        fn primitive_ty(&self, primitive_ty: &PrimitiveTy) -> DocBuilder<A> {
1097            match primitive_ty {
1098                PrimitiveTy::Bool => docs!["Bool"],
1099                PrimitiveTy::Int(int_kind) => docs![int_kind],
1100                PrimitiveTy::Float(float_kind) => docs![float_kind],
1101                PrimitiveTy::Char => docs!["Char"],
1102                PrimitiveTy::Str => docs!["String"],
1103            }
1104        }
1105
1106        fn int_kind(&self, int_kind: &IntKind) -> DocBuilder<A> {
1107            docs![match (&int_kind.signedness, &int_kind.size) {
1108                (Signedness::Signed, IntSize::S8) => "i8",
1109                (Signedness::Signed, IntSize::S16) => "i16",
1110                (Signedness::Signed, IntSize::S32) => "i32",
1111                (Signedness::Signed, IntSize::S64) => "i64",
1112                (Signedness::Signed, IntSize::S128) => "i128",
1113                (Signedness::Signed, IntSize::SSize) => "isize",
1114                (Signedness::Unsigned, IntSize::S8) => "u8",
1115                (Signedness::Unsigned, IntSize::S16) => "u16",
1116                (Signedness::Unsigned, IntSize::S32) => "u32",
1117                (Signedness::Unsigned, IntSize::S64) => "u64",
1118                (Signedness::Unsigned, IntSize::S128) => "u128",
1119                (Signedness::Unsigned, IntSize::SSize) => "usize",
1120            }]
1121        }
1122
1123        fn float_kind(&self, float_kind: &FloatKind) -> DocBuilder<A> {
1124            docs![match float_kind {
1125                FloatKind::F32 => "f32",
1126                FloatKind::F64 => "f64",
1127                _ => emit_error!(issue 1787, "The only supported float types are `f32` and `f64`."),
1128            }]
1129        }
1130
1131        fn quote_content(&self, quote_content: &QuoteContent) -> DocBuilder<A> {
1132            match quote_content {
1133                QuoteContent::Verbatim(s) => {
1134                    intersperse!(s.lines().map(|x| x.to_string()), hardline!())
1135                }
1136                QuoteContent::Expr(expr) => docs![expr],
1137                QuoteContent::Pattern(pat) => docs![pat],
1138                QuoteContent::Ty(ty) => docs![ty],
1139            }
1140        }
1141
1142        fn quote(&self, quote: &Quote) -> DocBuilder<A> {
1143            concat![&quote.0]
1144        }
1145
1146        fn param(&self, param: &Param) -> DocBuilder<A> {
1147            if matches!(
1148                *param.pat.kind,
1149                PatKind::Wild | PatKind::Ascription { .. } | PatKind::Binding { sub_pat: None, .. }
1150            ) {
1151                self.pat_typed(&param.pat)
1152            } else {
1153                emit_error!(issue 1791, "Function parameters must not contain patterns")
1154            }
1155        }
1156
1157        fn item(&self, item @ Item { ident, kind, meta }: &Item) -> DocBuilder<A> {
1158            let body = match kind {
1159                ItemKind::Fn {
1160                    name,
1161                    generics,
1162                    body,
1163                    params,
1164                    safety: _,
1165                } => {
1166                    let opaque = item.is_opaque();
1167                    docs![
1168                        docs![
1169                            docs![
1170                                docs![if opaque { "opaque" } else { "def" }, line!(), name].group(),
1171                                line!(),
1172                                generics,
1173                                params,
1174                                docs![": RustM", line!(), &body.ty].group(),
1175                                line!(),
1176                                if opaque { nil!() } else { docs![":= do"] }
1177                            ]
1178                            .group(),
1179                            if opaque { nil!() } else { docs![line!(), body] }
1180                        ]
1181                        .group()
1182                        .nest(INDENT),
1183                        if opaque {
1184                            nil!()
1185                        } else {
1186                            docs![&self.spec(item, name, generics, params)]
1187                        }
1188                    ]
1189                }
1190                ItemKind::TyAlias { name, generics, ty } => docs![
1191                    "abbrev ",
1192                    name,
1193                    line!(),
1194                    generics,
1195                    reflow!(": Type :="),
1196                    line!(),
1197                    ty
1198                ]
1199                .nest(INDENT)
1200                .group(),
1201                ItemKind::Use {
1202                    path: _,
1203                    is_external: _,
1204                    rename: _,
1205                } => nil!(),
1206                ItemKind::Quote { quote, origin: _ } => docs![quote],
1207                ItemKind::NotImplementedYet => {
1208                    emit_error!(issue 1706, "Item unsupported by the Hax engine (unimplemented yet)")
1209                }
1210                ItemKind::Type {
1211                    name,
1212                    generics,
1213                    variants,
1214                    is_struct,
1215                } => {
1216                    // TODO: use a resugaring, see https://github.com/cryspen/hax/issues/1668
1217                    if *is_struct {
1218                        // Structures
1219                        let Some(variant) = variants.first() else {
1220                            unreachable!(
1221                                "Structures should always have a constructor (even empty ones)"
1222                            )
1223                        };
1224                        let args = if !variant.is_record {
1225                            // Tuple-like structure, using positional arguments
1226                            intersperse!(
1227                                variant.arguments.iter().enumerate().map(|(i, (_, ty, _))| {
1228                                    docs![format!("_{i} :"), line!(), ty].group().nest(INDENT)
1229                                }),
1230                                hardline!()
1231                            )
1232                        } else {
1233                            // Structure-like structure, using named arguments
1234                            intersperse!(
1235                                variant.arguments.iter().map(|(id, ty, _)| {
1236                                    docs![self.render_last(id), reflow!(" : "), ty]
1237                                        .group()
1238                                        .nest(INDENT)
1239                                }),
1240                                hardline!()
1241                            )
1242                        };
1243                        docs![
1244                            docs![reflow!("structure "), name, line!(), generics, "where"].group(),
1245                            docs![hardline!(), args],
1246                        ]
1247                        .nest(INDENT)
1248                        .group()
1249                    } else {
1250                        // Enums
1251                        let applied_name: DocBuilder<A> =
1252                            if generics.params.is_empty() && generics.constraints.is_empty() {
1253                                docs![name]
1254                            } else {
1255                                docs![name, line!(), generics].group()
1256                            };
1257                        docs![
1258                            docs!["inductive ", name, line!(), generics, ": Type"].group(),
1259                            hardline!(),
1260                            concat!(variants.iter().map(|variant| docs![
1261                                "| ",
1262                                docs![variant, applied_name.clone()].group().nest(INDENT),
1263                                hardline!()
1264                            ])),
1265                        ]
1266                    }
1267                }
1268                ItemKind::Trait {
1269                    name,
1270                    generics,
1271                    items,
1272                } => {
1273                    let generic_types = generics.type_constraints().collect::<Vec<_>>();
1274                    if generic_types.len() < generics.constraints.len() {
1275                        emit_error!(issue 1710, "Unsupported equality constraints on associated types")
1276                    }
1277                    docs![
1278                        // A trait is encoded as two Lean type classes: one holding the associated types,
1279                        // and one holding all other fields.
1280                        // This is the type class holding the associated types:
1281                        docs![
1282                            docs![
1283                                docs![reflow!("class "), name, ".AssociatedTypes"],
1284                                (!generics.params.is_empty()).then_some(docs![
1285                                    softline!(),
1286                                    intersperse!(&generics.params, softline!()).group()
1287                                ]),
1288                                softline!(),
1289                                "where"
1290                            ]
1291                            .group(),
1292                            zip_left!(
1293                                hardline!(),
1294                                generic_types.iter().map(|impl_ident| docs![
1295                                    self.constraint_name(&self.render_last(name), impl_ident),
1296                                    " :",
1297                                    line!(),
1298                                    &impl_ident.goal.trait_,
1299                                    ".AssociatedTypes",
1300                                    line!(),
1301                                    intersperse!(&impl_ident.goal.args, line!())
1302                                ]
1303                                .group()
1304                                .brackets())
1305                            ),
1306                            zip_left!(
1307                                hardline!(),
1308                                items
1309                                    .iter()
1310                                    .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1311                                    .map(|item| docs![(generics.params.clone(), item)])
1312                            ),
1313                        ]
1314                        .nest(INDENT),
1315                        // We add the `[instance]` attribute to the contained constraints to make
1316                        // them available for type inference:
1317                        zip_left!(
1318                            docs![hardline!(), hardline!()],
1319                            generic_types.iter().map(|impl_ident| docs![
1320                                "attribute [instance]",
1321                                line!(),
1322                                name,
1323                                ".AssociatedTypes.",
1324                                self.constraint_name(&self.render_last(name), impl_ident),
1325                            ]
1326                            .group()
1327                            .nest(INDENT))
1328                        ),
1329                        // When referencing associated types, we would like to refer to them as
1330                        // `TraitName.TypeName` instead of `TraitName.AssociatedTypes.TypeName`:
1331                        zip_left!(
1332                            docs![hardline!(), hardline!()],
1333                            items
1334                                .iter()
1335                                .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1336                                .map(|item| {
1337                                    docs![
1338                                        "abbrev ",
1339                                        name,
1340                                        ".",
1341                                        self.render_last(&item.ident),
1342                                        " :=",
1343                                        line!(),
1344                                        name,
1345                                        ".AssociatedTypes",
1346                                        ".",
1347                                        self.render_last(&item.ident),
1348                                    ]
1349                                    .nest(INDENT)
1350                                })
1351                        ),
1352                        hardline!(),
1353                        hardline!(),
1354                        // This is the type class holding all other fields:
1355                        docs![
1356                            docs![
1357                                docs![reflow!("class "), name],
1358                                line!(),
1359                                docs![
1360                                    // Type parameters are also parameters of the class, but constraints are fields of the class
1361                                    intersperse!(&generics.params, line!()),
1362                                    line!(),
1363                                    // The collection of associated types is an extra parameter so that we can encode
1364                                    // equality constraints on associated types.
1365                                    docs![
1366                                        reflow!("associatedTypes :"),
1367                                        softline!(),
1368                                        "outParam",
1369                                        softline!(),
1370                                        docs![
1371                                            name,
1372                                            ".AssociatedTypes",
1373                                            softline!(),
1374                                            intersperse!(&generics.params, softline!()),
1375                                        ]
1376                                        .parens()
1377                                        .nest(INDENT)
1378                                    ]
1379                                    .brackets()
1380                                    .nest(INDENT)
1381                                ]
1382                                .group(),
1383                                line!(),
1384                                "where"
1385                            ]
1386                            .group(),
1387                            // Lean's `extends` does not work for us because one cannot implement
1388                            // different functions of the same name on the super- and on the
1389                            // subclass. So we treat supertraits like any other constraint:
1390                            zip_left!(
1391                                hardline!(),
1392                                generic_types.iter().map(|impl_ident| docs![
1393                                    self.constraint_name(&self.render_last(name), impl_ident),
1394                                    " :",
1395                                    line!(),
1396                                    impl_ident.goal.trait_,
1397                                    concat!(
1398                                        impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
1399                                    )
1400                                ]
1401                                .group()
1402                                .brackets())
1403                            ),
1404                            zip_left!(
1405                                hardline!(),
1406                                items.iter().filter(|item| {!(
1407                                    // TODO: should be treated directly by name rendering, see :
1408                                    // https://github.com/cryspen/hax/issues/1646
1409                                    item.ident.is_precondition() || item.ident.is_postcondition() ||
1410                                    // Associated types are encoded in a separate type class.
1411                                    matches!(item.kind, TraitItemKind::Type(_))
1412                                )}).map(|item| docs![(generics.params.clone(), item)] )
1413                            ),
1414                        ]
1415                        .nest(INDENT),
1416                        // We add the `[instance]` attribute to the contained constraints to make
1417                        // them available for type inference:
1418                        zip_left!(
1419                            docs![hardline!(), hardline!()],
1420                            generic_types.iter().map(|impl_ident| docs![
1421                                "attribute [instance]",
1422                                line!(),
1423                                name,
1424                                ".",
1425                                self.constraint_name(&self.render_last(name), impl_ident),
1426                            ]
1427                            .group()
1428                            .nest(INDENT))
1429                        ),
1430                    ]
1431                }
1432                ItemKind::Impl {
1433                    generics,
1434                    self_ty: _,
1435                    of_trait: (trait_, args),
1436                    items,
1437                    parent_bounds: _,
1438                    safety: _,
1439                } => docs![
1440                    // An impl is encoded as two Lean instances:
1441                    // One for the associated types...
1442                    docs![
1443                        docs![
1444                            reflow!("instance "),
1445                            ident,
1446                            ".AssociatedTypes",
1447                            line!(),
1448                            generics,
1449                            ":"
1450                        ]
1451                        .group(),
1452                        line!(),
1453                        docs![
1454                            trait_,
1455                            ".AssociatedTypes",
1456                            concat!(args.iter().map(|gv| docs![line!(), gv]))
1457                        ]
1458                        .group(),
1459                        line!(),
1460                        "where",
1461                    ]
1462                    .group()
1463                    .nest(INDENT),
1464                    docs![zip_left!(
1465                        hardline!(),
1466                        items
1467                            .iter()
1468                            .filter(|item| { matches!(item.kind, ImplItemKind::Type { .. }) })
1469                    )]
1470                    .nest(INDENT),
1471                    hardline!(),
1472                    hardline!(),
1473                    // ...and one for all other fields:
1474                    docs![
1475                        docs![reflow!("instance "), ident, line!(), generics, ":"].group(),
1476                        line!(),
1477                        docs![trait_, concat!(args.iter().map(|gv| docs![line!(), gv]))].group(),
1478                        line!(),
1479                        "where",
1480                    ]
1481                    .group()
1482                    .nest(INDENT),
1483                    docs![zip_left!(
1484                        hardline!(),
1485                        items.iter().filter(|item| {
1486                            !(
1487                                // TODO: should be treated directly by name rendering, see :
1488                                // https://github.com/cryspen/hax/issues/1646
1489                                item.ident.is_precondition() || item.ident.is_postcondition() ||
1490                                // Associated types are encoded into a separate type class
1491                                matches!(item.kind, ImplItemKind::Type { .. })
1492                            )
1493                        })
1494                    )]
1495                    .nest(INDENT),
1496                ],
1497                ItemKind::Resugared(resugared_item_kind) => match resugared_item_kind {
1498                    ResugaredItemKind::Constant {
1499                        name,
1500                        body,
1501                        generics,
1502                    } => docs![
1503                        docs![
1504                            docs!["def", line!(), name].group(),
1505                            line!(),
1506                            generics,
1507                            docs![":", line!(), &body.ty].group(),
1508                            line!(),
1509                            ":="
1510                        ]
1511                        .group(),
1512                        line!(),
1513                        self.monad_extract(body),
1514                    ]
1515                    .group()
1516                    .nest(INDENT),
1517                },
1518                ItemKind::Alias { .. } => {
1519                    // aliases are introduced when creating bundles. Those should not appear in
1520                    // Lean, as items can be named correctly in any file.
1521                    emit_error!(issue 1658, "Unsupported alias item")
1522                }
1523                ItemKind::Error(e) => docs![e],
1524            };
1525            docs![meta, body]
1526        }
1527
1528        fn impl_item(
1529            &self,
1530            ImplItem {
1531                meta: _,
1532                generics,
1533                kind,
1534                ident,
1535            }: &ImplItem,
1536        ) -> DocBuilder<A> {
1537            let name = self.render_last(ident);
1538            match kind {
1539                ImplItemKind::Type {
1540                    ty,
1541                    parent_bounds: _,
1542                } => docs![name, reflow!(" := "), ty],
1543                ImplItemKind::Fn { body, params } => docs![
1544                    docs![
1545                        name,
1546                        softline!(),
1547                        ":=",
1548                        line!(),
1549                        docs![
1550                            "fun",
1551                            line!(),
1552                            generics,
1553                            zip_right!(params, line!()).group(),
1554                            "=>",
1555                            softline!(),
1556                            "do"
1557                        ]
1558                        .group()
1559                        .nest(INDENT)
1560                    ]
1561                    .group(),
1562                    line!(),
1563                    body
1564                ]
1565                .group()
1566                .nest(INDENT),
1567                ImplItemKind::Resugared(_) => {
1568                    unreachable!("This backend has no resugaring for impl items")
1569                }
1570            }
1571        }
1572
1573        fn impl_ident(&self, ImplIdent { .. }: &ImplIdent) -> DocBuilder<A> {
1574            unreachable!(
1575                "`ImplIdent`s are rendered inline because we have multiple variants of how they must be rendered."
1576            )
1577        }
1578
1579        fn trait_goal(&self, TraitGoal { .. }: &TraitGoal) -> DocBuilder<A> {
1580            unreachable!(
1581                "`TraitGoal`s are rendered inline because we have multiple variants of how they must be rendered."
1582            )
1583        }
1584
1585        fn variant(
1586            &self,
1587            Variant {
1588                name,
1589                arguments,
1590                is_record,
1591                attributes,
1592            }: &Variant,
1593        ) -> DocBuilder<A> {
1594            docs![
1595                concat!(attributes),
1596                self.render_last(name),
1597                softline!(),
1598                // args
1599                if *is_record {
1600                    // Use named the arguments, keeping only the head of the identifier
1601                    docs![
1602                        intersperse!(
1603                            arguments.iter().map(|(id, ty, _)| {
1604                                docs![self.render_last(id), reflow!(" : "), ty]
1605                                    .parens()
1606                                    .group()
1607                            }),
1608                            line!()
1609                        )
1610                        .align()
1611                        .nest(INDENT),
1612                        line!(),
1613                        reflow!(": "),
1614                    ]
1615                    .group()
1616                } else {
1617                    // Use anonymous arguments
1618                    docs![
1619                        reflow!(": "),
1620                        concat!(
1621                            arguments
1622                                .iter()
1623                                .map(|(_, ty, _)| { docs![ty, reflow!(" -> ")] })
1624                        )
1625                    ]
1626                }
1627            ]
1628            .group()
1629            .nest(INDENT)
1630        }
1631
1632        fn symbol(&self, symbol: &Symbol) -> DocBuilder<A> {
1633            docs![self.escape(symbol.to_string())]
1634        }
1635
1636        fn metadata(
1637            &self,
1638            Metadata {
1639                span: _,
1640                attributes,
1641            }: &Metadata,
1642        ) -> DocBuilder<A> {
1643            concat!(attributes)
1644        }
1645
1646        fn lhs(&self, _lhs: &Lhs) -> DocBuilder<A> {
1647            unreachable_by_invariant!(Local_mutation)
1648        }
1649
1650        fn safety_kind(&self, _safety_kind: &SafetyKind) -> DocBuilder<A> {
1651            nil!()
1652        }
1653
1654        fn binding_mode(&self, _binding_mode: &BindingMode) -> DocBuilder<A> {
1655            unreachable!("This backend handle binding modes directly inside patterns")
1656        }
1657
1658        fn region(&self, _region: &Region) -> DocBuilder<A> {
1659            unreachable_by_invariant!(Drop_references)
1660        }
1661
1662        fn dyn_trait_goal(&self, _dyn_trait_goal: &DynTraitGoal) -> DocBuilder<A> {
1663            emit_error!(issue 1708, "`dyn` traits are unsupported")
1664        }
1665
1666        fn attribute(&self, Attribute { kind, span: _ }: &Attribute) -> DocBuilder<A> {
1667            match kind {
1668                AttributeKind::Tool { .. } | AttributeKind::Hax { .. } => {
1669                    nil!()
1670                }
1671                AttributeKind::DocComment {
1672                    kind: DocCommentKind::Line,
1673                    body,
1674                } => comment!(body.clone()).append(hardline!()),
1675                AttributeKind::DocComment {
1676                    kind: DocCommentKind::Block,
1677                    body,
1678                } => docs![
1679                    "/--",
1680                    line!(),
1681                    intersperse!(body.lines().map(|line| line.to_string()), line!()),
1682                    line!(),
1683                    "-/"
1684                ]
1685                .nest(INDENT)
1686                .group()
1687                .append(hardline!()),
1688            }
1689        }
1690
1691        fn borrow_kind(&self, _borrow_kind: &BorrowKind) -> DocBuilder<A> {
1692            unreachable_by_invariant!(Drop_references)
1693        }
1694
1695        fn guard(&self, _guard: &Guard) -> DocBuilder<A> {
1696            unreachable_by_invariant!(Drop_match_guards)
1697        }
1698
1699        fn projection_predicate(
1700            &self,
1701            projection_predicate: &ProjectionPredicate,
1702        ) -> DocBuilder<A> {
1703            docs![
1704                self.render_last(&projection_predicate.assoc_item),
1705                softline!(),
1706                ":=",
1707                line!(),
1708                projection_predicate.ty,
1709            ]
1710            .group()
1711            .nest(INDENT)
1712        }
1713
1714        fn error_node(&self, _error_node: &ErrorNode) -> DocBuilder<A> {
1715            // TODO : Should be made unreachable by https://github.com/cryspen/hax/pull/1672
1716            text!("sorry")
1717        }
1718
1719        // Impl expressions
1720
1721        fn impl_expr(&self, _impl_expr: &ImplExpr) -> DocBuilder<A> {
1722            emit_error!(issue 1716, "Explicit impl expressions are unsupported")
1723        }
1724    }
1725};
hax_rust_engine/backends/lean.rs

hax_rust_engine/backends/
lean.rs
