Skip to main content

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::OnceLock;
9
10use super::prelude::*;
11use crate::{
12    ast::{
13        identifiers::global_id::view::{ConstructorKind, PathSegment, TypeDefKind},
14        span::Span,
15    },
16    attributes::hax_proof_attributes,
17    names::rust_primitives::hax::{
18        cast_op,
19        explicit_monadic::{lift, pure},
20    },
21    phase::*,
22};
23use camino::Utf8PathBuf;
24use hax_lib_macros_types::ProofMethod;
25use hax_types::engine_api::File;
26
27mod binops {
28    pub use crate::names::core::cmp::PartialEq;
29    pub use crate::names::core::ops::bit::*;
30    pub use crate::names::core::ops::index::*;
31    pub use crate::names::rust_primitives::arithmetic::neg;
32    pub use crate::names::rust_primitives::hax::machine_int::*;
33    pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
34}
35
36const LIFT: GlobalId = lift;
37const PURE: GlobalId = pure;
38const CAST_OP: GlobalId = cast_op;
39
40/// The Lean printer
41#[setup_printer_struct]
42#[derive(Default, Clone)]
43pub struct LeanPrinter {
44    current_namespace: Option<GlobalId>,
45}
46
47const INDENT: isize = 2;
48
49const HEADER: &str = "
50-- Experimental lean backend for Hax
51-- The Hax prelude library can be found in hax/proof-libs/lean
52import Hax
53import Std.Tactic.Do
54import Std.Do.Triple
55import Std.Tactic.Do.Syntax
56open Std.Do
57open Std.Tactic
58
59set_option mvcgen.warning false
60set_option linter.unusedVariables false
61
62
63";
64
65impl RenderView for LeanPrinter {
66    fn reserved_keywords() -> &'static HashSet<String> {
67        static SET: OnceLock<HashSet<String>> = OnceLock::new();
68        SET.get_or_init(|| {
69            [
70                // reserved for Lean:
71                "end",
72                "def",
73                "abbrev",
74                "theorem",
75                "example",
76                "inductive",
77                "structure",
78                "from",
79                // reserved for hax encoding:
80                "associatedTypes",
81                "AssociatedTypes",
82            ]
83            .into_iter()
84            .map(|s| s.to_string())
85            .collect()
86        })
87    }
88
89    fn should_escape(id: &str) -> bool {
90        Self::is_reserved_keyword(id)
91            || id.starts_with(|c: char| c.is_ascii_digit())
92            || id.starts_with("trait_constr_")
93    }
94
95    fn separator(&self) -> &str {
96        "."
97    }
98
99    fn relativize_module_path<'a>(&self, module_path: &'a [PathSegment]) -> &'a [PathSegment] {
100        if let Some(namespace) = self.current_namespace
101            && namespace.view().segments() == module_path
102        {
103            &[]
104        } else {
105            module_path
106        }
107    }
108
109    fn render_path_segment(&self, chunk: &PathSegment) -> Vec<String> {
110        // Returning None indicates that the default rendering should be used
111        (match chunk.kind() {
112            AnyKind::Constructor(ConstructorKind::Constructor { ty })
113                if matches!(ty.kind(), TypeDefKind::Struct) =>
114            {
115                Some(vec![
116                    Self::escape(&self.render_path_segment_payload(chunk.payload())),
117                    "mk".to_string(),
118                ])
119            }
120            AnyKind::Field { named: _, parent } => match parent.kind() {
121                ConstructorKind::Constructor { ty }
122                    if matches!(&ty.kind(), TypeDefKind::Struct) =>
123                {
124                    chunk.parent().map(|parent| {
125                        vec![
126                            Self::escape(&self.render_path_segment_payload(parent.payload())),
127                            Self::escape(&self.render_path_segment_payload(chunk.payload())),
128                        ]
129                    })
130                }
131                _ => None,
132            },
133            _ => None,
134        })
135        .unwrap_or(default::render_path_segment(self, chunk))
136    }
137}
138
139impl Printer for LeanPrinter {}
140
141/// The Lean backend
142pub struct LeanBackend;
143
144impl Backend for LeanBackend {
145    type Printer = LeanPrinter;
146
147    fn module_path(&self, module: &Module) -> Utf8PathBuf {
148        let krate = module.ident.krate();
149        Utf8PathBuf::from(krate).with_extension("lean")
150    }
151
152    fn phases(&self) -> Vec<PhaseKind> {
153        use crate::phase::{PhaseKind::*, legacy::LegacyOCamlPhase::*};
154        vec![
155            RejectRawOrMutPointer.into(),
156            RejectImplTypeMethod.into(),
157            RewriteLocalSelf.into(),
158            TransformHaxLibInline.into(),
159            Specialize.into(),
160            DropSizedTrait.into(),
161            SimplifyQuestionMarks.into(),
162            AndMutDefsite.into(),
163            ReconstructAsserts.into(),
164            ReconstructForLoops.into(),
165            ReconstructWhileLoops.into(),
166            DirectAndMut.into(),
167            RejectArbitraryLhs.into(),
168            DropBlocks.into(),
169            DropMatchGuards.into(),
170            DropReferences.into(),
171            TrivializeAssignLhs.into(),
172            HoistSideEffects.into(),
173            HoistDisjunctivePatterns.into(),
174            SimplifyMatchReturn.into(),
175            LocalMutation.into(),
176            RewriteControlFlow.into(),
177            DropReturnBreakContinue.into(),
178            FunctionalizeLoops.into(),
179            RejectQuestionMark.into(),
180            TraitsSpecs.into(),
181            SimplifyHoisting.into(),
182            NewtypeAsRefinement.into(),
183            ReorderFields.into(),
184            SortItems.into(),
185            FilterUnprintableItems,
186            ExplicitMonadic,
187        ]
188    }
189
190    fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
191        vec![
192            Box::new(RecursiveFunctions),
193            Box::new(FunctionsToConstants),
194            Box::new(LetPure),
195            Box::new(RecordEllipsis),
196        ]
197    }
198
199    fn items_to_module(&self, items: Vec<Item>) -> Vec<Module> {
200        let mut modules: Vec<Module> = Vec::new();
201
202        for item in items {
203            let module_ident = item.ident.mod_only_closest_parent();
204
205            if let Some(last_module) = modules.last_mut()
206                && last_module.ident == module_ident
207            {
208                last_module.items.push(item);
209            } else {
210                modules.push(Module {
211                    ident: module_ident,
212                    items: vec![item],
213                    meta: Metadata {
214                        span: Span::dummy(),
215                        attributes: vec![],
216                    },
217                });
218            }
219        }
220        modules
221    }
222
223    fn modules_to_files(&self, modules: Vec<Module>, mut printer: Self::Printer) -> Vec<File> {
224        if modules.is_empty() {
225            return vec![];
226        }
227        let path = self.module_path(modules.first().unwrap()).to_string();
228        let contents = modules
229            .into_iter()
230            .map(|module: Module| {
231                let (c, _) = printer.print(module);
232                c
233            })
234            .collect::<Vec<String>>()
235            .join("\n");
236        vec![File {
237            path,
238            contents: format!("{}{}", HEADER, contents),
239            sourcemap: None,
240        }]
241    }
242}
243
244impl LeanPrinter {
245    /// Checks if we are extracting core models to be able to use different namespeacing when
246    /// referring to core.
247    pub fn is_hax_core_models_extraction_mode(&self) -> bool {
248        std::env::var("HAX_CORE_MODELS_EXTRACTION_MODE")
249            .map(|v| v == "on")
250            .unwrap_or(false)
251    }
252
253    /// Render a global id using the Rendering strategy of the Lean printer. Works for both concrete
254    /// and projector ids. TODO: https://github.com/cryspen/hax/issues/1660
255    pub fn render_id(&self, id: &GlobalId) -> String {
256        let id = if !self.is_hax_core_models_extraction_mode() && id.krate() == "core" {
257            id.rename_krate("core_models")
258        } else {
259            *id
260        };
261        self.render_string(&id.view())
262    }
263
264    /// Renders the last, most local part of an id. Used for named arguments of constructors.
265    pub fn render_last(&self, id: &GlobalId) -> String {
266        self.render(&id.view())
267            .path
268            .last()
269            // TODO: Should be ensured by the rendering engine; see
270            // https://github.com/cryspen/hax/issues/1660
271            .expect("Segments should always be non-empty")
272            .clone()
273    }
274
275    /// Inject an identifier in before-last position while rendering
276    /// TODO: use `DefIdInner::kind` for this instead (https://github.com/cryspen/hax/issues/1877)
277    pub fn render_with_injection(&self, id: &GlobalId, injection: &String) -> String {
278        let rendered = self.render(&id.view());
279        let (last, butlast) = rendered
280            .path
281            .split_last()
282            // TODO: Should be ensured by the rendering engine; see
283            // https://github.com/cryspen/hax/issues/1660
284            .expect("Segments should always be non-empty");
285        let path: Vec<String> = butlast
286            .iter()
287            .chain(std::iter::once(injection))
288            .chain(std::iter::once(last))
289            .map(String::clone)
290            .collect();
291        self.rendered_to_string(Rendered {
292            module: rendered.module,
293            path,
294        })
295    }
296
297    /// Escape a string for use in Lean string literals.
298    /// Handles newlines, quotes, backslashes, and other special characters.
299    fn escape_string(&self, s: &str) -> String {
300        let mut result = String::with_capacity(s.len());
301        for c in s.chars() {
302            match c {
303                '"' => result.push_str("\\\""),
304                '\'' => result.push_str("\\'"),
305                '\\' => result.push_str("\\\\"),
306                '\n' => result.push_str("\\n"),
307                '\r' => result.push_str("\\r"),
308                '\t' => result.push_str("\\t"),
309                c if c.is_ascii_control() => {
310                    result.push_str(&format!("\\x{:02x}", c as u8));
311                }
312                c => result.push(c),
313            }
314        }
315        result
316    }
317}
318
319/// Render parameters, adding a line after each parameter
320impl<A: 'static + Clone> ToDocument<LeanPrinter, A> for Vec<Param> {
321    fn to_document(&self, printer: &LeanPrinter) -> DocBuilder<A> {
322        printer.params(self)
323    }
324}
325
326#[prepend_associated_functions_with(install_pretty_helpers!(self: Self))]
327const _: () = {
328    // Emits a CLI error with a github issue number, and prints "sorry" in the lean output
329    macro_rules! emit_error {($($tt:tt)*) => {disambiguated_todo!($($tt)*)};}
330
331    // Insert a new line in a doc (pretty)
332    macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
333
334    // Concatenate docs (pretty )
335    macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};}
336
337    // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `ASBS...CS`
338    macro_rules! zip_right {
339        ($a:expr, $sep:expr) => {
340            docs![concat!($a.into_iter().map(|a| docs![a, $sep]))]
341        };
342    }
343
344    // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `SASB...SC`
345    macro_rules! zip_left {
346        ($sep:expr, $a:expr) => {
347            docs![concat!($a.into_iter().map(|a| docs![$sep, a]))]
348        };
349    }
350
351    // Prints a one-line comment
352    macro_rules! comment {
353        ($e:expr) => {
354            docs!["-- ", $e]
355        };
356    }
357
358    // Extra methods, specific to the LeanPrinter
359    impl LeanPrinter {
360        /// Prints arguments a variant or constructor of struct, using named or unamed arguments based
361        /// on the `is_record` flag. Used for both expressions and patterns
362        pub fn arguments<A: 'static + Clone, D>(
363            &self,
364            fields: &[(GlobalId, D)],
365            is_record: &bool,
366        ) -> DocBuilder<A>
367        where
368            D: ToDocument<Self, A>,
369        {
370            if *is_record {
371                self.named_arguments(fields)
372            } else {
373                self.positional_arguments(fields)
374            }
375        }
376
377        /// Prints fields of structures (when in braced notation)
378        fn struct_fields<A: 'static + Clone, D>(&self, fields: &[(GlobalId, D)]) -> DocBuilder<A>
379        where
380            D: ToDocument<Self, A>,
381        {
382            docs![intersperse!(
383                fields
384                    .iter()
385                    .map(|(id, e)| { docs![self.render_last(id), reflow!(" := "), e].group() }),
386                docs![",", line!()]
387            )]
388            .group()
389        }
390        /// Prints named arguments (record) of a variant or constructor of struct
391        fn named_arguments<A: 'static + Clone, D>(&self, fields: &[(GlobalId, D)]) -> DocBuilder<A>
392        where
393            D: ToDocument<Self, A>,
394        {
395            docs![zip_left!(
396                line!(),
397                fields.iter().map(|(id, e)| {
398                    docs![self.render_last(id), reflow!(" := "), e]
399                        .parens()
400                        .group()
401                })
402            )]
403            .group()
404        }
405
406        /// Prints positional arguments (tuple) of a variant or constructor of struct
407        fn positional_arguments<A: 'static + Clone, D>(
408            &self,
409            fields: &[(GlobalId, D)],
410        ) -> DocBuilder<A>
411        where
412            D: ToDocument<Self, A>,
413        {
414            docs![zip_left!(line!(), fields.iter().map(|(_, e)| e))].group()
415        }
416
417        /// Prints parameters of functions (items, trait items, impl items)
418        fn params<A: 'static + Clone>(&self, params: &Vec<Param>) -> DocBuilder<A> {
419            zip_left!(line!(), params)
420        }
421
422        /// Print parameters as function arguments
423        fn params_as_args<A: 'static + Clone>(&self, params: &[Param]) -> DocBuilder<A> {
424            zip_left!(
425                line!(),
426                params.iter().map(|param| {
427                    let Ty(ty_kind) = &param.ty;
428                    // We need to print arguments of type `Tuple0` as `⟨⟩` instead of `_`
429                    // https://github.com/cryspen/hax/issues/1856
430                    if let TyKind::App { head, .. } = **ty_kind
431                        && let Some(global_id::TupleId::Type { length: 0 }) = head.expect_tuple()
432                    {
433                        docs!["⟨⟩"]
434                    } else {
435                        docs![param]
436                    }
437                })
438            )
439        }
440
441        /// Renders expressions with an explicit ascription `(e : RustM ty)`. Used for the body of closure, for
442        /// numeric literals, etc.
443        fn expr_typed_result<A: 'static + Clone>(&self, expr: &Expr) -> DocBuilder<A> {
444            docs![
445                expr,
446                softline!(),
447                ":",
448                line!(),
449                docs!["RustM", line!(), &expr.ty].group()
450            ]
451            .group()
452        }
453
454        fn pat_typed<A: 'static + Clone>(&self, pat: &Pat) -> DocBuilder<A> {
455            docs![pat, reflow!(" :"), line!(), &pat.ty].parens().group()
456        }
457
458        fn do_block<A: 'static + Clone, D: ToDocument<Self, A>>(&self, body: D) -> DocBuilder<A> {
459            docs!["do", line!(), body].group()
460        }
461
462        /// Produces a name for a constraint on an trait-level constraint, or an associated
463        /// type. The name is obtained by combining the type it applies to and the name of the
464        /// constraint (and should be unique)
465        fn constraint_name(&self, type_name: &String, constraint: &ImplIdent) -> String {
466            format!("trait_constr_{}_{}", type_name, constraint.name)
467        }
468
469        /// Renders a named argument for associated types with equality constraints
470        /// (aka projections). If there are no equality constraints, returns None.
471        fn associated_type_projections<A: 'static + Clone>(
472            &self,
473            impl_ident: &ImplIdent,
474            projections: Vec<DocBuilder<A>>,
475        ) -> Option<DocBuilder<A>> {
476            (!projections.is_empty()).then_some(
477                docs![
478                    "(associatedTypes := {",
479                    line!(),
480                    docs![
481                        "show",
482                        line!(),
483                        impl_ident.goal.trait_,
484                        ".AssociatedTypes",
485                        zip_left!(line!(), impl_ident.goal.args.iter()),
486                    ]
487                    .group()
488                    .nest(INDENT),
489                    line!(),
490                    reflow!("by infer_instance"),
491                    line!(),
492                    docs![
493                        "with",
494                        line!(),
495                        intersperse!(projections, docs![",", line!()]),
496                    ]
497                    .group()
498                    .nest(INDENT),
499                    "})"
500                ]
501                .group()
502                .nest(INDENT),
503            )
504        }
505
506        /// Turns an expression of type `RustM T` into one of type `T` (out of the monad), providing
507        /// reflexivity as a proof witness.
508        fn monad_extract<A: 'static + Clone>(&self, expr: &Expr) -> DocBuilder<A> {
509            if let ExprKind::App { head, args, .. } = expr.kind()
510                && let ExprKind::GlobalId(PURE) = head.kind()
511                && let [pure_expr] = &args[..]
512                && let ExprKind::Literal(_) | ExprKind::GlobalId(_) | ExprKind::LocalId(_) =
513                    pure_expr.kind()
514            {
515                // Pure values are displayed directly. Note that constructors, while pure, may
516                // contain sub-expressions that are not, so they must be wrapped in a do-block
517                docs![pure_expr]
518            } else {
519                // All other expressions are wrapped in a do-block, and extracted out of the monad
520                docs![
521                    "RustM.of_isOk",
522                    line!(),
523                    self.do_block(expr).parens(),
524                    line!(),
525                    "(by rfl)"
526                ]
527                .group()
528                .nest(INDENT)
529            }
530        }
531
532        /// Print trait items, adding trait-level params as extra arguments
533        fn trait_item_with_trait_params<A: 'static + Clone>(
534            &self,
535            trait_generics: &[GenericParam],
536            TraitItem {
537                meta: _,
538                kind,
539                generics: item_generics,
540                ident,
541            }: &TraitItem,
542        ) -> DocBuilder<A> {
543            {
544                let name = self.render_last(ident);
545                let trait_generics = zip_left!(
546                    softline!(),
547                    trait_generics
548                        .iter()
549                        .map(|GenericParam { ident, .. }| docs![ident].parens())
550                );
551                docs![match kind {
552                    TraitItemKind::Fn(ty) => {
553                        docs![
554                            name,
555                            trait_generics,
556                            self.generics(item_generics, &self.render_last(ident)),
557                            softline!(),
558                            ":",
559                            line!(),
560                            ty
561                        ]
562                        .group()
563                        .nest(INDENT)
564                    }
565                    TraitItemKind::Type(_) => {
566                        docs![name, softline!(), ":", line!(), "Type"]
567                            .group()
568                            .nest(INDENT)
569                    }
570                    TraitItemKind::Default { params, body } => docs![
571                        docs![
572                            name,
573                            trait_generics,
574                            self.generics(item_generics, &self.render_last(ident)),
575                            zip_left!(line!(), params).group(),
576                            softline!(),
577                            ":",
578                            if params.is_empty() {
579                                docs![body.ty, softline!(), reflow!(":=")]
580                            } else {
581                                docs!["RustM", softline!(), body.ty, softline!(), reflow!(":= do")]
582                                    .group()
583                            }
584                        ]
585                        .group(),
586                        line!(),
587                        if params.is_empty() {
588                            self.monad_extract(body)
589                        } else {
590                            docs![body]
591                        },
592                    ]
593                    .group()
594                    .nest(INDENT),
595                    TraitItemKind::Resugared(_) => {
596                        unreachable!("This backend has no resugaring for trait items")
597                    }
598                    TraitItemKind::Error(e) => docs![e],
599                }]
600            }
601        }
602
603        // Print generics, using `name` as a prefix for constraint names
604        fn generics<A: 'static + Clone>(
605            &self,
606            generics: &Generics,
607            name: &String,
608        ) -> DocBuilder<A> {
609            docs![
610                zip_left!(line!(), &generics.params),
611                zip_left!(
612                    line!(),
613                    generics.type_class_constraints().map(|impl_ident| {
614                        let projections = generics
615                            .equality_constraints()
616                            .filter(|p| !matches!(&*p.impl_.kind, ImplExprKind::LocalBound { id } if *id != impl_ident.name ))
617                            .map(|p| {
618                                if let ImplExprKind::LocalBound { .. } = &*p.impl_.kind {
619                                    docs![p]
620                                } else if let ImplExprKind::Parent { .. } = &*p.impl_.kind {
621                                    emit_error!(issue 1923, "Unsupported equality constraints on associated types of parent trait")
622                                } else {
623                                    emit_error!(issue 1924, "Unsupported variant of associated type projection")
624                                }
625                            })
626                            .collect::<Vec<_>>();
627                        docs![
628                            docs![
629                                self.constraint_name(&format!("{}_associated_type", name), impl_ident),
630                                reflow!(" : "),
631                                impl_ident.goal.trait_,
632                                ".AssociatedTypes",
633                                concat!(
634                                    impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
635                                )
636                            ]
637                            .brackets()
638                            .group()
639                            .nest(INDENT),
640                            line!(),
641                            docs![
642                                self.constraint_name(name, impl_ident),
643                                reflow!(" : "),
644                                impl_ident.goal.trait_,
645                                concat!(
646                                    impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
647                                ),
648                                line!(),
649                                self.associated_type_projections(impl_ident, projections)
650                            ]
651                            .brackets()
652                            .nest(INDENT)
653                            .group()
654                        ]
655                        .group()
656                    })
657                ),
658            ]
659            .group()
660        }
661
662        /// Print spec of an item
663        fn spec<A: 'static + Clone>(
664            &self,
665            item: &Item,
666            name: &GlobalId,
667            generics: &Generics,
668            params: &Vec<Param>,
669        ) -> DocBuilder<A> {
670            let linked_items = HasLinkedItemGraph::linked_item_graph(self);
671            let spec = linked_items.fn_like_linked_expressions(item, item.self_id());
672            if !linked_items.has_spec(item) {
673                nil!()
674            } else {
675                match hax_proof_attributes(item) {
676                    Err(message) => emit_error!("{message}"),
677                    Ok(proof_attributes) => {
678                        let (tactic, specset) = match proof_attributes.proof_method {
679                            Some(ProofMethod::Grind) => ("grind", "int"),
680                            Some(ProofMethod::BvDecide) | None => ("bv_decide", "bv"),
681                        };
682                        let pure_requires_proof = proof_attributes
683                            .pure_requires_proof
684                            .unwrap_or(format!("by hax_construct_pure <;> {tactic}"));
685                        let pure_ensures_proof = proof_attributes
686                            .pure_ensures_proof
687                            .unwrap_or(format!("by hax_construct_pure <;> {tactic}"));
688                        let proof = proof_attributes.proof.map(|s| docs![s]).unwrap_or(docs![
689                            "by hax_mvcgen [",
690                            name,
691                            "] <;> ",
692                            tactic
693                        ]);
694                        {
695                            docs![
696                                hardline!(),
697                                hardline!(),
698                                docs!["set_option hax_mvcgen.specset \"", specset, "\" in"],
699                                hardline!(),
700                                "@[hax_spec]",
701                                hardline!(),
702                                docs![
703                                    docs![
704                                        "def",
705                                        line!(),
706                                        name,
707                                        ".spec",
708                                        self.generics(generics, &self.render_last(name)),
709                                        params,
710                                        softline!(),
711                                        ":"
712                                    ]
713                                    .group()
714                                    .nest(INDENT),
715                                    line!(),
716                                    docs![
717                                        "Spec",
718                                        line!(),
719                                        docs![
720                                            "requires",
721                                            softline!(),
722                                            ":= do",
723                                            line!(),
724                                            spec.precondition
725                                                .map_or(reflow!("pure True"), |p| docs![p])
726                                        ]
727                                        .parens()
728                                        .group()
729                                        .nest(INDENT),
730                                        line!(),
731                                        docs![
732                                            "ensures := ",
733                                            spec.postcondition.map_or(
734                                                reflow!("fun _ => pure True"),
735                                                |p| docs![
736                                                    "fun",
737                                                    line!(),
738                                                    p.result_binder,
739                                                    softline!(),
740                                                    "=> do",
741                                                    line!(),
742                                                    p.body,
743                                                ]
744                                                .group()
745                                                .nest(INDENT)
746                                            ),
747                                        ]
748                                        .parens()
749                                        .group()
750                                        .nest(INDENT),
751                                        line!(),
752                                        docs![
753                                            name,
754                                            zip_left!(line!(), &generics.params),
755                                            self.params_as_args(params)
756                                        ]
757                                        .parens()
758                                        .group()
759                                        .nest(INDENT)
760                                    ]
761                                    .group()
762                                    .nest(INDENT),
763                                    softline!(),
764                                    ":=",
765                                ]
766                                .group()
767                                .nest(2 * INDENT),
768                                softline!(),
769                                docs![
770                                    hardline!(),
771                                    docs!["pureRequires :=", softline!(), pure_requires_proof],
772                                    hardline!(),
773                                    docs!["pureEnsures :=", softline!(), pure_ensures_proof],
774                                    hardline!(),
775                                    docs!["contract :=", softline!(), proof]
776                                        .group()
777                                        .nest(INDENT),
778                                    hardline!(),
779                                ]
780                                .nest(INDENT)
781                                .braces(),
782                            ]
783                        }
784                    }
785                }
786            }
787        }
788    }
789
790    impl<A: 'static + Clone> ToDocument<LeanPrinter, A> for (Vec<GenericParam>, &TraitItem) {
791        fn to_document(&self, printer: &LeanPrinter) -> DocBuilder<A> {
792            printer.trait_item_with_trait_params(&self.0, self.1)
793        }
794    }
795
796    impl<A: 'static + Clone> PrettyAst<A> for LeanPrinter {
797        const NAME: &'static str = "Lean";
798
799        /// Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [`todo_document!`].
800        fn todo_document(&self, message: &str, issue_id: Option<u32>) -> DocBuilder<A> {
801            <Self as PrettyAst<A>>::emit_diagnostic(
802                self,
803                hax_types::diagnostics::Kind::Unimplemented {
804                    issue_id,
805                    details: Some(message.into()),
806                },
807            );
808            text!("sorry")
809        }
810
811        fn module(&self, module: &Module) -> DocBuilder<A> {
812            let current_namespace = module.ident;
813            let new_printer = LeanPrinter {
814                current_namespace: Some(current_namespace),
815                ..self.clone()
816            };
817            let items = &module.items;
818            docs![
819                "namespace ",
820                current_namespace,
821                hardline!(),
822                hardline!(),
823                intersperse!(
824                    items.iter().map(|item| { item.to_document(&new_printer) }),
825                    docs![hardline!(), hardline!()]
826                ),
827                hardline!(),
828                hardline!(),
829                "end ",
830                current_namespace,
831                hardline!(),
832                hardline!(),
833            ]
834        }
835
836        fn global_id(&self, global_id: &GlobalId) -> DocBuilder<A> {
837            docs![self.render_id(global_id)]
838        }
839
840        fn generics(&self, generics: &Generics) -> DocBuilder<A> {
841            self.generics(generics, &String::new())
842        }
843
844        fn generic_constraint(&self, _: &GenericConstraint) -> DocBuilder<A> {
845            unreachable!(
846                "Generic constraints are rendered inline because they must contain associated type projections."
847            )
848        }
849
850        fn generic_param(&self, generic_param: &GenericParam) -> DocBuilder<A> {
851            match generic_param.kind() {
852                GenericParamKind::Type => docs![&generic_param.ident, reflow!(" : Type")]
853                    .parens()
854                    .group(),
855                GenericParamKind::Lifetime => unreachable_by_invariant!(Drop_references),
856                GenericParamKind::Const { ty } => docs![&generic_param.ident, reflow!(" : "), ty]
857                    .parens()
858                    .group(),
859            }
860        }
861
862        fn generic_value(&self, generic_value: &GenericValue) -> DocBuilder<A> {
863            match generic_value {
864                GenericValue::Ty(ty) => docs![ty],
865                GenericValue::Expr(expr) => docs![expr].parens(),
866                GenericValue::Lifetime => unreachable_by_invariant!(Drop_references),
867            }
868        }
869
870        fn expr(&self, Expr { kind, ty, meta: _ }: &Expr) -> DocBuilder<A> {
871            match &**kind {
872                ExprKind::If {
873                    condition,
874                    then,
875                    else_,
876                } => {
877                    if let Some(else_branch) = else_ {
878                        docs![
879                            docs!["if", line!(), condition, reflow!(" then do")].group(),
880                            docs![line!(), then].nest(INDENT),
881                            line!(),
882                            reflow!("else do"),
883                            docs![line!(), else_branch].nest(INDENT)
884                        ]
885                        .group()
886                    } else {
887                        unreachable_by_invariant!(Local_mutation)
888                    }
889                }
890                ExprKind::App {
891                    head,
892                    args,
893                    generic_args,
894                    bounds_impls: _,
895                    trait_,
896                } => {
897                    match (&args[..], &generic_args[..], head.kind()) {
898                        ([arg], [], ExprKind::GlobalId(LIFT)) => docs![reflow!("← "), arg].parens(),
899                        ([arg], [], ExprKind::GlobalId(PURE)) => {
900                            docs![reflow!("pure "), arg].parens()
901                        }
902                        ([arg], [], ExprKind::GlobalId(CAST_OP)) => docs![
903                            // Add type annotation for `cast_op`:
904                            docs![head, line!(), arg],
905                            softline!(),
906                            ":",
907                            line!(),
908                            "RustM",
909                            softline!(),
910                            ty
911                        ]
912                        .parens()
913                        .group()
914                        .nest(INDENT),
915                        // TODO: Replace this match pattern with an `if let` guard when the feature stabilizes
916                        // Tracking PR: https://github.com/rust-lang/rust/pull/141295
917                        (
918                            [arg],
919                            [],
920                            ExprKind::GlobalId(op @ (binops::neg | binops::not | binops::Not::not)),
921                        ) if arg.ty == Ty::bool() || arg.ty.is_int() => {
922                            let symbol = match *op {
923                                binops::neg => "-?",
924                                binops::not => "~?",
925                                binops::Not::not => "!?",
926                                _ => unreachable!(),
927                            };
928                            docs![symbol, softline!(), arg].parens()
929                        }
930                        ([lhs, rhs], [], ExprKind::GlobalId(binops::Index::index)) => {
931                            docs![lhs, "[", line_!(), rhs, line_!(), "]_?"]
932                                .nest(INDENT)
933                                .group()
934                        }
935                        // TODO: Replace this match pattern with an `if let` guard when the feature stabilizes
936                        // Tracking PR: https://github.com/rust-lang/rust/pull/141295
937                        (
938                            [lhs, rhs],
939                            [],
940                            ExprKind::GlobalId(
941                                op @ (binops::add
942                                | binops::sub
943                                | binops::mul
944                                | binops::div
945                                | binops::rem
946                                | binops::shr
947                                | binops::shl
948                                | binops::bitand
949                                | binops::BitAnd::bitand
950                                | binops::bitor
951                                | binops::BitOr::bitor
952                                | binops::bitxor
953                                | binops::BitXor::bitxor
954                                | binops::logical_op_and
955                                | binops::logical_op_or
956                                | binops::eq
957                                | binops::PartialEq::eq
958                                | binops::lt
959                                | binops::le
960                                | binops::gt
961                                | binops::ge
962                                | binops::ne
963                                | binops::PartialEq::ne),
964                            ),
965                        ) if (lhs.ty == Ty::bool() && rhs.ty == Ty::bool())
966                            || (rhs.ty.is_int() && lhs.ty.is_int()) =>
967                        {
968                            let symbol = match *op {
969                                binops::add => "+?",
970                                binops::sub => "-?",
971                                binops::mul => "*?",
972                                binops::div => "/?",
973                                binops::rem => "%?",
974                                binops::shr => ">>>?",
975                                binops::shl => "<<<?",
976                                binops::bitand => "&&&?",
977                                binops::BitAnd::bitand => "&&?",
978                                binops::bitor => "|||?",
979                                binops::BitOr::bitor => "||?",
980                                binops::bitxor => "^^^?",
981                                binops::BitXor::bitxor => "^^?",
982                                binops::logical_op_and => "&&?",
983                                binops::logical_op_or => "||?",
984                                binops::eq => "==?",
985                                binops::PartialEq::eq => "==?",
986                                binops::lt => "<?",
987                                binops::le => "<=?",
988                                binops::gt => ">?",
989                                binops::ge => ">=?",
990                                binops::ne => "!=?",
991                                binops::PartialEq::ne => "!=?",
992                                _ => unreachable!(),
993                            };
994                            docs![lhs, line!(), docs![symbol, softline!(), rhs].group()]
995                                .group()
996                                .nest(INDENT)
997                                .parens()
998                        }
999                        _ => {
1000                            // Fallback for any application
1001                            docs![
1002                                head,
1003                                trait_
1004                                    .as_ref()
1005                                    .map(|(impl_expr, _)| zip_left!(line!(), &impl_expr.goal.args)),
1006                                zip_left!(line!(), generic_args).group(),
1007                                zip_left!(line!(), args).group(),
1008                            ]
1009                            .parens()
1010                            .nest(INDENT)
1011                            .group()
1012                        }
1013                    }
1014                }
1015                ExprKind::Literal(numeric_lit @ (Literal::Float { .. } | Literal::Int { .. })) => {
1016                    docs![numeric_lit, reflow!(" : "), ty].parens().group()
1017                }
1018                ExprKind::Literal(literal) => docs![literal],
1019                ExprKind::Array(exprs) => docs![
1020                    "RustArray.ofVec #v[",
1021                    intersperse!(exprs, docs![",", line!()])
1022                        .nest(INDENT)
1023                        .group()
1024                        .align(),
1025                    "]"
1026                ]
1027                .parens()
1028                .group(),
1029                ExprKind::Construct {
1030                    constructor,
1031                    is_record,
1032                    is_struct,
1033                    fields,
1034                    base,
1035                } => {
1036                    if fields.is_empty() && base.is_none() {
1037                        docs![constructor]
1038                    } else if let Some(base) = base {
1039                        if !(*is_record && *is_struct) {
1040                            unreachable!(
1041                                "Constructors with base expressions are necessarily structs with record-like arguments"
1042                            )
1043                        }
1044                        docs![base, line!(), reflow!("with "), self.struct_fields(fields)]
1045                            .braces()
1046                            .group()
1047                    } else {
1048                        docs![constructor, self.arguments(fields, is_record)]
1049                            .nest(INDENT)
1050                            .parens()
1051                            .group()
1052                    }
1053                }
1054                ExprKind::Let { lhs, rhs, body }
1055                | ExprKind::Resugared(ResugaredExprKind::LetPure { lhs, rhs, body }) => {
1056                    let binder = if matches!(**kind, ExprKind::Let { .. }) {
1057                        " ←"
1058                    } else {
1059                        " :="
1060                    };
1061                    docs![
1062                        docs![
1063                            docs![
1064                                "let",
1065                                line!(),
1066                                // TODO: Improve treatment of patterns in general. see
1067                                // https://github.com/cryspen/hax/issues/1712
1068                                match *lhs.kind.clone() {
1069                                    PatKind::Ascription { .. } =>
1070                                        docs![lhs, reflow!(" : "), &lhs.ty],
1071                                    PatKind::Binding {
1072                                        mutable: false,
1073                                        var,
1074                                        mode: BindingMode::ByValue,
1075                                        sub_pat: None,
1076                                    } => docs![&var, reflow!(" : "), &lhs.ty],
1077                                    _ => docs![lhs],
1078                                },
1079                            ]
1080                            .group(),
1081                            binder,
1082                            line!(),
1083                            rhs,
1084                            ";"
1085                        ]
1086                        .nest(INDENT)
1087                        .group(),
1088                        line!(),
1089                        body,
1090                    ]
1091                }
1092                ExprKind::GlobalId(global_id) => docs![global_id],
1093                ExprKind::LocalId(local_id) => docs![local_id],
1094                ExprKind::Ascription { e, ty } => docs![e, reflow!(" : "), ty].parens().group(),
1095                ExprKind::Closure {
1096                    params,
1097                    body,
1098                    captures: _,
1099                } => docs![
1100                    docs![
1101                        reflow!("fun"),
1102                        zip_left!(line!(), params),
1103                        softline!(),
1104                        "=>"
1105                    ]
1106                    .group(),
1107                    line!(),
1108                    self.do_block(self.expr_typed_result(body)).parens()
1109                ]
1110                .parens()
1111                .group()
1112                .nest(INDENT),
1113
1114                ExprKind::Resugared(ResugaredExprKind::Tuple { .. }) => {
1115                    unreachable!("This printer doesn't use the tuple resugaring")
1116                }
1117                ExprKind::Match { scrutinee, arms } => docs![
1118                    docs![
1119                        "match",
1120                        docs![line!(), scrutinee].nest(INDENT),
1121                        line!(),
1122                        "with"
1123                    ]
1124                    .group(),
1125                    docs![line!(), intersperse!(arms, line!())]
1126                        .group()
1127                        .nest(INDENT),
1128                ]
1129                .group(),
1130
1131                ExprKind::Borrow { .. } => {
1132                    unreachable_by_invariant!(Drop_references)
1133                }
1134                ExprKind::AddressOf { .. } => unreachable_by_invariant!(Reject_raw_or_mut_pointer),
1135                ExprKind::Assign { .. } => unreachable_by_invariant!(Local_mutation),
1136                ExprKind::Loop { .. } => unreachable_by_invariant!(Functionalize_loops),
1137                ExprKind::Break { .. } | ExprKind::Return { .. } | ExprKind::Continue { .. } => {
1138                    unreachable_by_invariant!(Drop_break_continue_return)
1139                }
1140                ExprKind::Block { .. } => unreachable_by_invariant!(Drop_blocks),
1141                ExprKind::Quote { contents } => docs![contents],
1142                ExprKind::Error(error_node) => docs![error_node],
1143            }
1144        }
1145
1146        fn arm(&self, arm: &Arm) -> DocBuilder<A> {
1147            if let Some(_guard) = &arm.guard {
1148                unreachable_by_invariant!(Drop_match_guards)
1149            } else {
1150                docs![
1151                    reflow!("| "),
1152                    &arm.pat,
1153                    softline!(),
1154                    "=>",
1155                    softline!(),
1156                    "do",
1157                    line!(),
1158                    &arm.body
1159                ]
1160                .nest(INDENT)
1161                .group()
1162            }
1163        }
1164
1165        fn pat(&self, pat: &Pat) -> DocBuilder<A> {
1166            match &*pat.kind {
1167                PatKind::Wild => docs!["_"],
1168                PatKind::Ascription { pat, ty: _ } => docs![pat],
1169                PatKind::Binding {
1170                    mutable,
1171                    var,
1172                    mode,
1173                    sub_pat,
1174                } => match (mutable, mode, sub_pat) {
1175                    (true, _, _) => unreachable_by_invariant!(Local_mutation),
1176                    (false, BindingMode::ByRef(_), _) => unreachable_by_invariant!(Drop_references),
1177                    (false, BindingMode::ByValue, None) => docs![var],
1178                    (false, BindingMode::ByValue, Some(pat)) => {
1179                        docs![var, "@", softline_!(), pat].group()
1180                    }
1181                },
1182                PatKind::Or { sub_pats } => docs![intersperse!(sub_pats, reflow!(" | "))].group(),
1183                PatKind::Array { .. } => {
1184                    emit_error!(issue 1712, "Unsupported pattern-matching on arrays")
1185                }
1186                PatKind::Deref { .. } => unreachable_by_invariant!(Drop_references),
1187                PatKind::Constant {
1188                    lit: Literal::Float { .. },
1189                } => {
1190                    emit_error!(issue 1788, "Unsupported pattern-matching on floats")
1191                }
1192                PatKind::Constant { lit } => docs![lit],
1193                PatKind::Construct {
1194                    constructor,
1195                    is_record,
1196                    is_struct,
1197                    fields,
1198                } => {
1199                    if *is_struct {
1200                        if !*is_record {
1201                            // Tuple-like structure, using positional arguments
1202                            docs![
1203                                "⟨",
1204                                intersperse!(
1205                                    fields.iter().map(|field| { docs![&field.1] }),
1206                                    docs![",", line!()]
1207                                )
1208                                .align()
1209                                .group(),
1210                                "⟩"
1211                            ]
1212                            .align()
1213                            .group()
1214                        } else {
1215                            // Record-like structure, using named arguments
1216                            docs![intersperse!(
1217                                fields.iter().map(|(id, pat)| {
1218                                    docs![self.render_last(id), reflow!(" :="), line!(), pat]
1219                                        .group()
1220                                }),
1221                                docs![",", line!()]
1222                            )]
1223                            .align()
1224                            .braces()
1225                            .group()
1226                        }
1227                    } else {
1228                        // Variant
1229                        docs![
1230                            constructor,
1231                            line!(),
1232                            self.arguments(fields, is_record).align()
1233                        ]
1234                        .parens()
1235                        .group()
1236                        .nest(INDENT)
1237                    }
1238                }
1239                PatKind::Resugared(ResugaredPatKind::ConstructWithEllipsis {
1240                    constructor,
1241                    is_struct,
1242                    fields,
1243                }) => {
1244                    if *is_struct {
1245                        // Struct: render as `{f1 := pat, f2 := pat, ..}` or `_`
1246                        if fields.is_empty() {
1247                            docs!["_"]
1248                        } else {
1249                            docs![intersperse!(
1250                                fields
1251                                    .iter()
1252                                    .map(|(id, pat)| {
1253                                        docs![self.render_last(id), reflow!(" :="), line!(), pat]
1254                                            .group()
1255                                    })
1256                                    .chain(std::iter::once(docs![".."])),
1257                                docs![",", line!()]
1258                            )]
1259                            .align()
1260                            .braces()
1261                            .group()
1262                        }
1263                    } else {
1264                        // Enum variant with named fields: (f1 := pat) (f2 := pat) ..
1265                        let record_part = if fields.is_empty() {
1266                            docs!["_"]
1267                        } else {
1268                            docs![intersperse!(
1269                                fields.iter().map(|(id, pat)| {
1270                                    docs![self.render_last(id), reflow!(" :="), line!(), pat]
1271                                        .group()
1272                                        .parens()
1273                                }),
1274                                line!()
1275                            )]
1276                            .align()
1277                            .group()
1278                        };
1279                        docs![constructor, line!(), record_part, " .."]
1280                            .parens()
1281                            .group()
1282                            .nest(INDENT)
1283                    }
1284                }
1285                PatKind::Error(_) => {
1286                    // TODO : Should be made unreachable by https://github.com/cryspen/hax/pull/1672
1287                    text!("sorry")
1288                }
1289            }
1290        }
1291
1292        fn ty(&self, ty: &Ty) -> DocBuilder<A> {
1293            match ty.kind() {
1294                TyKind::Primitive(primitive_ty) => docs![primitive_ty],
1295                TyKind::App { head, args } => {
1296                    if args.is_empty() {
1297                        docs![head]
1298                    } else {
1299                        docs![head, zip_left!(line!(), args)]
1300                            .parens()
1301                            .group()
1302                            .nest(INDENT)
1303                    }
1304                }
1305                TyKind::Arrow { inputs, output } => docs![
1306                    zip_right!(inputs, docs![softline!(), "->", line!()]),
1307                    "RustM",
1308                    softline!(),
1309                    output
1310                ]
1311                .parens()
1312                .group(),
1313                TyKind::Param(local_id) => docs![local_id],
1314                TyKind::Slice(ty) => docs!["RustSlice", line!(), ty].parens().group(),
1315                TyKind::Array { ty, length } => docs!["RustArray", line!(), ty, line!(), {
1316                    if let ExprKind::Literal(int_lit @ Literal::Int { .. }) = length.kind() {
1317                        docs![int_lit]
1318                    } else if let ExprKind::LocalId(local_id) = length.kind() {
1319                        docs![local_id]
1320                    } else {
1321                        unreachable!(
1322                            "Only arrays with integer literal or const param size are supported"
1323                        )
1324                    }
1325                }]
1326                .parens()
1327                .group(),
1328                TyKind::AssociatedType { impl_, item } => {
1329                    let kind = impl_.kind();
1330                    match &kind {
1331                        ImplExprKind::Self_ => docs!["associatedTypes.", self.render_last(item)],
1332                        ImplExprKind::Parent { ident, .. }
1333                        | ImplExprKind::Projection { ident, .. } => {
1334                            docs![item, zip_left!(line!(), ident.goal.args.iter())]
1335                                .parens()
1336                                .group()
1337                                .nest(INDENT)
1338                        }
1339                        ImplExprKind::LocalBound { .. } => {
1340                            docs![item, zip_left!(line!(), impl_.goal.args.iter())]
1341                                .parens()
1342                                .group()
1343                                .nest(INDENT)
1344                        }
1345                        _ => {
1346                            emit_error!(issue 1922, "Unsupported variant of associated type")
1347                        }
1348                    }
1349                }
1350                TyKind::Ref { .. } => unreachable_by_invariant!(Drop_references),
1351                TyKind::RawPointer => unreachable_by_invariant!(Reject_raw_or_mut_pointer),
1352                TyKind::Opaque(_) => emit_error!(issue 1714, "Unsupported opaque type definitions"),
1353                TyKind::Dyn(_) => emit_error!(issue 1708, "Unsupported `dyn` traits"),
1354                TyKind::Resugared(resugared_ty_kind) => match resugared_ty_kind {
1355                    ResugaredTyKind::Tuple(_) => {
1356                        unreachable!("This backend does not use tuple resugaring (yet)")
1357                    }
1358                },
1359                TyKind::Error(e) => docs![e],
1360            }
1361        }
1362
1363        fn literal(&self, literal: &Literal) -> DocBuilder<A> {
1364            docs![match literal {
1365                Literal::String(symbol) => format!("\"{}\"", self.escape_string(symbol)),
1366                Literal::Char(c) => format!("'{c}'"),
1367                Literal::Bool(b) => format!("{b}"),
1368                Literal::Int {
1369                    value,
1370                    negative,
1371                    kind: _,
1372                } => format!("{}{value}", if *negative { "-" } else { "" }),
1373                Literal::Float {
1374                    value,
1375                    negative,
1376                    kind: _,
1377                } => format!("{}{value}", if *negative { "-" } else { "" }),
1378            }]
1379        }
1380
1381        fn local_id(&self, local_id: &LocalId) -> DocBuilder<A> {
1382            // TODO: should be done by name rendering, see https://github.com/cryspen/hax/issues/1630
1383            docs![Self::escape(&local_id.0)]
1384        }
1385
1386        fn spanned_ty(&self, spanned_ty: &SpannedTy) -> DocBuilder<A> {
1387            docs![&spanned_ty.ty]
1388        }
1389
1390        fn primitive_ty(&self, primitive_ty: &PrimitiveTy) -> DocBuilder<A> {
1391            match primitive_ty {
1392                PrimitiveTy::Bool => docs!["Bool"],
1393                PrimitiveTy::Int(int_kind) => docs![int_kind],
1394                PrimitiveTy::Float(float_kind) => docs![float_kind],
1395                PrimitiveTy::Char => docs!["Char"],
1396                PrimitiveTy::Str => docs!["String"],
1397            }
1398        }
1399
1400        fn int_kind(&self, int_kind: &IntKind) -> DocBuilder<A> {
1401            docs![match (&int_kind.signedness, &int_kind.size) {
1402                (Signedness::Signed, IntSize::S8) => "i8",
1403                (Signedness::Signed, IntSize::S16) => "i16",
1404                (Signedness::Signed, IntSize::S32) => "i32",
1405                (Signedness::Signed, IntSize::S64) => "i64",
1406                (Signedness::Signed, IntSize::S128) => "i128",
1407                (Signedness::Signed, IntSize::SSize) => "isize",
1408                (Signedness::Unsigned, IntSize::S8) => "u8",
1409                (Signedness::Unsigned, IntSize::S16) => "u16",
1410                (Signedness::Unsigned, IntSize::S32) => "u32",
1411                (Signedness::Unsigned, IntSize::S64) => "u64",
1412                (Signedness::Unsigned, IntSize::S128) => "u128",
1413                (Signedness::Unsigned, IntSize::SSize) => "usize",
1414            }]
1415        }
1416
1417        fn float_kind(&self, float_kind: &FloatKind) -> DocBuilder<A> {
1418            docs![match float_kind {
1419                FloatKind::F32 => "f32",
1420                FloatKind::F64 => "f64",
1421                _ => emit_error!(issue 1787, "The only supported float types are `f32` and `f64`."),
1422            }]
1423        }
1424
1425        fn quote_content(&self, quote_content: &QuoteContent) -> DocBuilder<A> {
1426            match quote_content {
1427                QuoteContent::Verbatim(s) => {
1428                    intersperse!(s.lines().map(|x| x.to_string()), hardline!())
1429                }
1430                QuoteContent::Expr(expr) => docs![expr],
1431                QuoteContent::Pattern(pat) => docs![pat],
1432                QuoteContent::Ty(ty) => docs![ty],
1433            }
1434        }
1435
1436        fn quote(&self, quote: &Quote) -> DocBuilder<A> {
1437            concat![&quote.0]
1438        }
1439
1440        fn param(&self, param: &Param) -> DocBuilder<A> {
1441            if matches!(
1442                *param.pat.kind,
1443                PatKind::Wild | PatKind::Ascription { .. } | PatKind::Binding { sub_pat: None, .. }
1444            ) {
1445                self.pat_typed(&param.pat)
1446            } else {
1447                emit_error!(issue 1791, "Function parameters must not contain patterns")
1448            }
1449        }
1450
1451        fn item(&self, item @ Item { ident, kind, meta }: &Item) -> DocBuilder<A> {
1452            let body = match kind {
1453                ItemKind::Fn {
1454                    name,
1455                    generics,
1456                    body,
1457                    params,
1458                    safety: _,
1459                } => {
1460                    let opaque = item.is_opaque();
1461                    let linked_items = HasLinkedItemGraph::linked_item_graph(self);
1462                    docs![
1463                        if opaque || linked_items.has_spec(item) {
1464                            nil!()
1465                        } else {
1466                            // Function should be unfolded by `mvcgen`
1467                            docs!["@[spec]", hardline!()]
1468                        },
1469                        docs![
1470                            docs![
1471                                docs![
1472                                    docs![if opaque { "opaque" } else { "def" }, line!(), name]
1473                                        .group(),
1474                                    self.generics(generics, &self.render_last(name)),
1475                                    params,
1476                                    softline!(),
1477                                    ":"
1478                                ]
1479                                .group(),
1480                                line!(),
1481                                docs![
1482                                    "RustM",
1483                                    line!(),
1484                                    &body.ty,
1485                                    if opaque {
1486                                        nil!()
1487                                    } else {
1488                                        docs![line!(), ":= do"]
1489                                    }
1490                                ]
1491                                .group(),
1492                            ]
1493                            .group()
1494                            .nest(INDENT),
1495                            if opaque { nil!() } else { docs![line!(), body] }
1496                        ]
1497                        .group()
1498                        .nest(INDENT),
1499                        if opaque {
1500                            nil!()
1501                        } else {
1502                            docs![&self.spec(item, name, generics, params)]
1503                        }
1504                    ]
1505                }
1506                ItemKind::TyAlias { name, generics, ty } => docs![
1507                    "abbrev ",
1508                    name,
1509                    self.generics(generics, &self.render_last(name)),
1510                    softline!(),
1511                    ":",
1512                    line!(),
1513                    "Type",
1514                    softline!(),
1515                    ":=",
1516                    line!(),
1517                    ty
1518                ]
1519                .nest(INDENT)
1520                .group(),
1521                ItemKind::RustModule | ItemKind::Use { .. } => nil!(),
1522                ItemKind::Quote { quote, origin: _ } => docs![quote],
1523                ItemKind::NotImplementedYet => {
1524                    emit_error!(issue 1706, "Item unsupported by the Hax engine (unimplemented yet)")
1525                }
1526                ItemKind::Type {
1527                    name,
1528                    generics,
1529                    variants,
1530                    is_struct,
1531                } => {
1532                    if item.is_opaque() {
1533                        docs![
1534                            reflow!("opaque "),
1535                            name,
1536                            self.generics(generics, &self.render_last(name)),
1537                            softline!(),
1538                            ":",
1539                            line!(),
1540                            "Type"
1541                        ]
1542                        .group()
1543                        .nest(INDENT)
1544                    }
1545                    // TODO: use a resugaring, see https://github.com/cryspen/hax/issues/1668
1546                    else if *is_struct {
1547                        // Structures
1548                        let Some(variant) = variants.first() else {
1549                            unreachable!(
1550                                "Structures should always have a constructor (even empty ones)"
1551                            )
1552                        };
1553                        let args = if variant.arguments.is_empty() {
1554                            comment!["no fields"]
1555                        } else if !variant.is_record {
1556                            // Tuple-like structure, using positional arguments
1557                            intersperse!(
1558                                variant.arguments.iter().enumerate().map(|(i, (_, ty, _))| {
1559                                    docs![format!("_{i} :"), line!(), ty].group().nest(INDENT)
1560                                }),
1561                                hardline!()
1562                            )
1563                        } else {
1564                            // Structure-like structure, using named arguments
1565                            intersperse!(
1566                                variant.arguments.iter().map(|(id, ty, _)| {
1567                                    docs![self.render_last(id), reflow!(" : "), ty]
1568                                        .group()
1569                                        .nest(INDENT)
1570                                }),
1571                                hardline!()
1572                            )
1573                        };
1574                        docs![
1575                            docs![
1576                                reflow!("structure "),
1577                                name,
1578                                self.generics(generics, &self.render_last(name)),
1579                                line!(),
1580                                "where"
1581                            ]
1582                            .group(),
1583                            docs![hardline!(), args],
1584                        ]
1585                        .nest(INDENT)
1586                        .group()
1587                    } else {
1588                        // Enums
1589                        let applied_name: DocBuilder<A> = if generics.params.is_empty()
1590                            && generics.constraints.is_empty()
1591                        {
1592                            docs![name]
1593                        } else {
1594                            docs![name, self.generics(generics, &self.render_last(name))].group()
1595                        };
1596                        docs![
1597                            docs![
1598                                "inductive ",
1599                                name,
1600                                self.generics(generics, &self.render_last(name)),
1601                                softline!(),
1602                                ":",
1603                                line!(),
1604                                "Type"
1605                            ]
1606                            .group(),
1607                            hardline!(),
1608                            intersperse!(
1609                                variants.iter().map(|variant| docs![
1610                                    "| ",
1611                                    variant,
1612                                    applied_name.clone()
1613                                ]
1614                                .group()
1615                                .nest(INDENT)),
1616                                hardline!()
1617                            ),
1618                        ]
1619                    }
1620                }
1621                ItemKind::Trait {
1622                    name,
1623                    generics,
1624                    items,
1625                    safety: _,
1626                } => {
1627                    let generic_types = generics.type_class_constraints().collect::<Vec<_>>();
1628                    if generic_types.len() < generics.constraints.len() {
1629                        emit_error!(issue 1921, "Unsupported equality constraints on associated types")
1630                    }
1631                    docs![
1632                        // A trait is encoded as two Lean type classes: one holding the associated types,
1633                        // and one holding all other fields.
1634                        // This is the type class holding the associated types:
1635                        docs![
1636                            docs![
1637                                docs![reflow!("class "), name, ".AssociatedTypes"],
1638                                zip_left!(line!(), &generics.params).group(),
1639                                line!(),
1640                                "where"
1641                            ]
1642                            .group(),
1643                            zip_left!(
1644                                hardline!(),
1645                                generic_types.iter().map(|impl_ident| docs![
1646                                    self.constraint_name(&self.render_last(name), impl_ident),
1647                                    " :",
1648                                    line!(),
1649                                    &impl_ident.goal.trait_,
1650                                    ".AssociatedTypes",
1651                                    line!(),
1652                                    intersperse!(&impl_ident.goal.args, line!())
1653                                ]
1654                                .group()
1655                                .brackets())
1656                            ),
1657                            zip_left!(
1658                                hardline!(),
1659                                items
1660                                    .iter()
1661                                    .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1662                                    .map(|item| docs![(generics.params.clone(), item)])
1663                            ),
1664                        ]
1665                        .nest(INDENT),
1666                        // We add the `[instance]` attribute to the contained constraints to make
1667                        // them available for type inference:
1668                        zip_left!(
1669                            docs![hardline!(), hardline!()],
1670                            generic_types.iter().map(|impl_ident| docs![
1671                                "attribute [instance_reducible, instance]",
1672                                line!(),
1673                                name,
1674                                ".AssociatedTypes.",
1675                                self.constraint_name(&self.render_last(name), impl_ident),
1676                            ]
1677                            .group()
1678                            .nest(INDENT))
1679                        ),
1680                        zip_left!(
1681                            docs![hardline!(), hardline!()],
1682                            items
1683                                .iter()
1684                                .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1685                                .map(|item| docs![
1686                                    "attribute [reducible]",
1687                                    line!(),
1688                                    self.render_with_injection(
1689                                        &item.ident,
1690                                        &"AssociatedTypes".to_string()
1691                                    )
1692                                ]
1693                                .group()
1694                                .nest(INDENT))
1695                        ),
1696                        // When referencing associated types, we would like to refer to them as
1697                        // `TraitName.TypeName` instead of `TraitName.AssociatedTypes.TypeName`:
1698                        zip_left!(
1699                            docs![hardline!(), hardline!()],
1700                            items
1701                                .iter()
1702                                .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1703                                .map(|item| {
1704                                    docs![
1705                                        "abbrev ",
1706                                        name,
1707                                        ".",
1708                                        self.render_last(&item.ident),
1709                                        " :=",
1710                                        line!(),
1711                                        name,
1712                                        ".AssociatedTypes",
1713                                        ".",
1714                                        self.render_last(&item.ident),
1715                                    ]
1716                                    .nest(INDENT)
1717                                })
1718                        ),
1719                        hardline!(),
1720                        hardline!(),
1721                        // This is the type class holding all other fields:
1722                        docs![
1723                            docs![
1724                                docs![reflow!("class "), name],
1725                                docs![
1726                                    // Type parameters are also parameters of the class, but constraints are fields of the class
1727                                    docs![zip_left!(line!(), &generics.params)].group(),
1728                                    line!(),
1729                                    // The collection of associated types is an extra parameter so that we can encode
1730                                    // equality constraints on associated types.
1731                                    docs![
1732                                        reflow!("associatedTypes :"),
1733                                        softline!(),
1734                                        "outParam",
1735                                        softline!(),
1736                                        docs![
1737                                            name,
1738                                            ".AssociatedTypes",
1739                                            softline!(),
1740                                            intersperse!(&generics.params, softline!()),
1741                                        ]
1742                                        .parens()
1743                                        .nest(INDENT)
1744                                    ]
1745                                    .brackets()
1746                                    .nest(INDENT)
1747                                ]
1748                                .group(),
1749                                line!(),
1750                                "where"
1751                            ]
1752                            .group(),
1753                            // Lean's `extends` does not work for us because one cannot implement
1754                            // different functions of the same name on the super- and on the
1755                            // subclass. So we treat supertraits like any other constraint:
1756                            zip_left!(
1757                                hardline!(),
1758                                generic_types.iter().map(|impl_ident| docs![
1759                                    self.constraint_name(&self.render_last(name), impl_ident),
1760                                    softline!(),
1761                                    ":",
1762                                    line!(),
1763                                    impl_ident.goal.trait_,
1764                                    zip_left!(line!(), impl_ident.goal.args.iter())
1765                                ]
1766                                .group()
1767                                .brackets())
1768                            ),
1769                            // We also add constraints on associated types here:
1770                            concat!(
1771                                items
1772                                    .iter()
1773                                    .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1774                                    .map(|item| docs![
1775                                        self.generics(
1776                                            &item.generics,
1777                                            &self.render_last(&item.ident)
1778                                        )
1779                                    ])
1780                            ),
1781                            // Finally the regular trait items:
1782                            zip_left!(
1783                                hardline!(),
1784                                items.iter().filter(|item| {!(
1785                                    // TODO: should be treated directly by name rendering, see :
1786                                    // https://github.com/cryspen/hax/issues/1646
1787                                    item.ident.is_precondition() || item.ident.is_postcondition() ||
1788                                    // Associated types are encoded in a separate type class.
1789                                    matches!(item.kind, TraitItemKind::Type(_))
1790                                )}).map(|item| docs![(generics.params.clone(), item)] )
1791                            ),
1792                        ]
1793                        .nest(INDENT),
1794                        // We add the `[instance]` attribute to the contained constraints to make
1795                        // them available for type inference:
1796                        zip_left!(
1797                            docs![hardline!(), hardline!()],
1798                            generic_types.iter().map(|impl_ident| docs![
1799                                "attribute [instance_reducible, instance]",
1800                                line!(),
1801                                name,
1802                                ".",
1803                                self.constraint_name(&self.render_last(name), impl_ident),
1804                            ]
1805                            .group()
1806                            .nest(INDENT))
1807                        ),
1808                    ]
1809                }
1810                ItemKind::Impl {
1811                    generics,
1812                    self_ty: _,
1813                    of_trait: (trait_, args),
1814                    items,
1815                    parent_bounds: _,
1816                } => {
1817                    let opaque = item.is_opaque();
1818                    docs![
1819                        // An impl is encoded as two Lean instances:
1820                        // One for the associated types...
1821                        docs![
1822                            docs![
1823                                if opaque {
1824                                    reflow!("@[instance] opaque ")
1825                                } else {
1826                                    reflow!("@[reducible] instance ")
1827                                },
1828                                ident,
1829                                ".AssociatedTypes",
1830                                self.generics(generics, &self.render_last(ident)),
1831                                softline!(),
1832                                ":"
1833                            ]
1834                            .group(),
1835                            line!(),
1836                            docs![trait_, ".AssociatedTypes", zip_left!(line!(), args)].group(),
1837                            if opaque {
1838                                docs![
1839                                    softline!(),
1840                                    ":=",
1841                                    line!(),
1842                                    reflow!("by constructor <;> exact Inhabited.default")
1843                                ]
1844                            } else {
1845                                docs![line!(), "where"]
1846                            },
1847                        ]
1848                        .group()
1849                        .nest(INDENT),
1850                        if opaque {
1851                            nil!()
1852                        } else {
1853                            docs![zip_left!(
1854                                hardline!(),
1855                                items.iter().filter(|item| {
1856                                    matches!(item.kind, ImplItemKind::Type { .. })
1857                                })
1858                            )]
1859                            .nest(INDENT)
1860                        },
1861                        hardline!(),
1862                        hardline!(),
1863                        // ...and one for all other fields:
1864                        docs![
1865                            docs![
1866                                if opaque {
1867                                    reflow!("@[instance] opaque ")
1868                                } else {
1869                                    reflow!("instance ")
1870                                },
1871                                ident,
1872                                self.generics(generics, &self.render_last(ident)),
1873                                softline!(),
1874                                ":"
1875                            ]
1876                            .group(),
1877                            line!(),
1878                            docs![trait_, zip_left!(line!(), args.iter())].group(),
1879                            if opaque {
1880                                docs![
1881                                    softline!(),
1882                                    ":=",
1883                                    line!(),
1884                                    reflow!("by constructor <;> exact Inhabited.default")
1885                                ]
1886                            } else {
1887                                docs![line!(), "where"]
1888                            },
1889                        ]
1890                        .group()
1891                        .nest(INDENT),
1892                        if opaque {
1893                            nil!()
1894                        } else {
1895                            docs![zip_left!(
1896                                hardline!(),
1897                                items.iter().filter(|item| {
1898                                    !(
1899                                        // TODO: should be treated directly by name rendering, see :
1900                                        // https://github.com/cryspen/hax/issues/1646
1901                                        item.ident.is_precondition() || item.ident.is_postcondition() ||
1902                                        // Associated types are encoded into a separate type class
1903                                        matches!(item.kind, ImplItemKind::Type { .. })
1904                                    )
1905                                })
1906                            )]
1907                            .nest(INDENT)
1908                        },
1909                    ]
1910                }
1911                ItemKind::Resugared(resugared_item_kind) => match resugared_item_kind {
1912                    ResugaredItemKind::Constant {
1913                        name,
1914                        body,
1915                        generics,
1916                    } => docs![
1917                        docs![
1918                            docs![
1919                                docs!["def", line!(), name].group(),
1920                                self.generics(generics, &self.render_last(ident)),
1921                                softline!(),
1922                                ":",
1923                            ]
1924                            .group(),
1925                            line!(),
1926                            &body.ty,
1927                            line!(),
1928                            ":="
1929                        ]
1930                        .group(),
1931                        line!(),
1932                        self.monad_extract(body),
1933                    ]
1934                    .group()
1935                    .nest(INDENT),
1936                    ResugaredItemKind::RecursiveFn {
1937                        name,
1938                        generics,
1939                        body,
1940                        params,
1941                        safety,
1942                    } => {
1943                        // Render the item with an appended `partial_fixpoint`:
1944                        let item = Item {
1945                            ident: item.ident,
1946                            kind: ItemKind::Fn {
1947                                name: *name,
1948                                generics: generics.clone(),
1949                                body: body.clone(),
1950                                params: params.clone(),
1951                                safety: safety.clone(),
1952                            },
1953                            meta: item.meta.clone(),
1954                        };
1955                        return docs![item, hardline!(), "partial_fixpoint"];
1956                    }
1957                },
1958                ItemKind::Alias { .. } => {
1959                    // aliases are introduced when creating bundles. Those should not appear in
1960                    // Lean, as items can be named correctly in any file.
1961                    emit_error!(issue 1658, "Unsupported alias item")
1962                }
1963                ItemKind::Error(e) => docs![e],
1964            };
1965            docs![meta, body]
1966        }
1967
1968        fn impl_item(
1969            &self,
1970            ImplItem {
1971                meta: _,
1972                generics,
1973                kind,
1974                ident,
1975            }: &ImplItem,
1976        ) -> DocBuilder<A> {
1977            let name = self.render_last(ident);
1978            match kind {
1979                ImplItemKind::Type {
1980                    ty,
1981                    parent_bounds: _,
1982                } => docs![name, reflow!(" := "), ty],
1983                ImplItemKind::Fn { body, params } => docs![
1984                    docs![
1985                        name,
1986                        softline!(),
1987                        ":=",
1988                        line!(),
1989                        docs![
1990                            "fun",
1991                            self.generics(generics, &self.render_last(ident)),
1992                            zip_left!(line!(), params).group(),
1993                            softline!(),
1994                            "=>",
1995                            softline!(),
1996                            "do"
1997                        ]
1998                        .group()
1999                        .nest(INDENT)
2000                    ]
2001                    .group(),
2002                    line!(),
2003                    body
2004                ]
2005                .group()
2006                .nest(INDENT),
2007                ImplItemKind::Resugared(ResugaredImplItemKind::Constant { body }) => {
2008                    docs![
2009                        name,
2010                        softline!(),
2011                        ":=",
2012                        softline!(),
2013                        self.monad_extract(body)
2014                    ]
2015                }
2016                ImplItemKind::Error(err) => docs!(err),
2017            }
2018        }
2019
2020        fn impl_ident(&self, ImplIdent { .. }: &ImplIdent) -> DocBuilder<A> {
2021            unreachable!(
2022                "`ImplIdent`s are rendered inline because we have multiple variants of how they must be rendered."
2023            )
2024        }
2025
2026        fn trait_goal(&self, TraitGoal { .. }: &TraitGoal) -> DocBuilder<A> {
2027            unreachable!(
2028                "`TraitGoal`s are rendered inline because we have multiple variants of how they must be rendered."
2029            )
2030        }
2031
2032        fn variant(
2033            &self,
2034            Variant {
2035                name,
2036                arguments,
2037                is_record,
2038                attributes,
2039            }: &Variant,
2040        ) -> DocBuilder<A> {
2041            docs![
2042                concat!(attributes),
2043                self.render_last(name),
2044                softline!(),
2045                // args
2046                if *is_record {
2047                    // Use named the arguments, keeping only the head of the identifier
2048                    docs![
2049                        intersperse!(
2050                            arguments.iter().map(|(id, ty, _)| {
2051                                docs![self.render_last(id), reflow!(" : "), ty]
2052                                    .parens()
2053                                    .group()
2054                            }),
2055                            line!()
2056                        )
2057                        .align()
2058                        .nest(INDENT),
2059                        line!(),
2060                        reflow!(": "),
2061                    ]
2062                    .group()
2063                } else {
2064                    // Use anonymous arguments
2065                    docs![
2066                        reflow!(": "),
2067                        concat!(
2068                            arguments
2069                                .iter()
2070                                .map(|(_, ty, _)| { docs![ty, reflow!(" -> ")] })
2071                        )
2072                    ]
2073                }
2074            ]
2075            .group()
2076            .nest(INDENT)
2077        }
2078
2079        fn symbol(&self, symbol: &Symbol) -> DocBuilder<A> {
2080            docs![Self::escape(symbol)]
2081        }
2082
2083        fn metadata(
2084            &self,
2085            Metadata {
2086                span: _,
2087                attributes,
2088            }: &Metadata,
2089        ) -> DocBuilder<A> {
2090            concat!(attributes)
2091        }
2092
2093        fn lhs(&self, _lhs: &Lhs) -> DocBuilder<A> {
2094            unreachable_by_invariant!(Local_mutation)
2095        }
2096
2097        fn safety_kind(&self, _safety_kind: &SafetyKind) -> DocBuilder<A> {
2098            nil!()
2099        }
2100
2101        fn binding_mode(&self, _binding_mode: &BindingMode) -> DocBuilder<A> {
2102            unreachable!("This backend handle binding modes directly inside patterns")
2103        }
2104
2105        fn region(&self, _region: &Region) -> DocBuilder<A> {
2106            unreachable_by_invariant!(Drop_references)
2107        }
2108
2109        fn dyn_trait_goal(&self, _dyn_trait_goal: &DynTraitGoal) -> DocBuilder<A> {
2110            emit_error!(issue 1708, "`dyn` traits are unsupported")
2111        }
2112
2113        fn attribute(&self, Attribute { kind, span: _ }: &Attribute) -> DocBuilder<A> {
2114            match kind {
2115                AttributeKind::Tool { .. } | AttributeKind::Hax { .. } => {
2116                    nil!()
2117                }
2118                AttributeKind::DocComment {
2119                    kind: DocCommentKind::Line,
2120                    body,
2121                } => comment!(body.clone()).append(hardline!()),
2122                AttributeKind::DocComment {
2123                    kind: DocCommentKind::Block,
2124                    body,
2125                } => docs![
2126                    "/--",
2127                    line!(),
2128                    intersperse!(body.lines().map(|line| line.to_string()), line!()),
2129                    line!(),
2130                    "-/"
2131                ]
2132                .nest(INDENT)
2133                .group()
2134                .append(hardline!()),
2135            }
2136        }
2137
2138        fn borrow_kind(&self, _borrow_kind: &BorrowKind) -> DocBuilder<A> {
2139            unreachable_by_invariant!(Drop_references)
2140        }
2141
2142        fn guard(&self, _guard: &Guard) -> DocBuilder<A> {
2143            unreachable_by_invariant!(Drop_match_guards)
2144        }
2145
2146        fn projection_predicate(
2147            &self,
2148            projection_predicate: &ProjectionPredicate,
2149        ) -> DocBuilder<A> {
2150            docs![
2151                self.render_last(&projection_predicate.assoc_item),
2152                softline!(),
2153                ":=",
2154                line!(),
2155                projection_predicate.ty,
2156            ]
2157            .group()
2158            .nest(INDENT)
2159        }
2160
2161        fn error_node(&self, _error_node: &ErrorNode) -> DocBuilder<A> {
2162            // TODO : Should be made unreachable by https://github.com/cryspen/hax/pull/1672
2163            text!("sorry")
2164        }
2165
2166        // Impl expressions
2167
2168        fn impl_expr(&self, _impl_expr: &ImplExpr) -> DocBuilder<A> {
2169            emit_error!(issue 1716, "Explicit impl expressions are unsupported")
2170        }
2171    }
2172};