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 super::prelude::*;
8use crate::resugarings::BinOp;
9
10mod binops {
11    pub use crate::names::rust_primitives::hax::machine_int::{add, div, mul, rem, shr, sub};
12    pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
13}
14
15/// The Lean printer
16#[derive(Default)]
17pub struct LeanPrinter;
18impl_doc_allocator_for!(LeanPrinter);
19
20impl Printer for LeanPrinter {
21    fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
22        vec![Box::new(BinOp::new(&[
23            binops::add(),
24            binops::sub(),
25            binops::mul(),
26            binops::rem(),
27            binops::div(),
28            binops::shr(),
29            binops::logical_op_and(),
30            binops::logical_op_or(),
31        ]))]
32    }
33
34    const NAME: &str = "Lean";
35}
36
37const INDENT: isize = 2;
38
39/// The Lean backend
40pub struct LeanBackend;
41
42fn crate_name(items: &[Item]) -> String {
43    // We should have a proper treatment of empty modules, see
44    // https://github.com/cryspen/hax/issues/1617
45    let head_item = items.first().unwrap();
46    head_item.ident.krate()
47}
48
49impl Backend for LeanBackend {
50    type Printer = LeanPrinter;
51
52    fn module_path(&self, module: &Module) -> camino::Utf8PathBuf {
53        camino::Utf8PathBuf::from(format!("{}.lean", crate_name(&module.items)))
54    }
55}
56
57impl LeanPrinter {
58    /// A filter for items blacklisted by the Lean backend : returns false if
59    /// the item is definitely not printable, but might return true on
60    /// unsupported items
61    pub fn printable_item(item: &Item) -> bool {
62        match &item.kind {
63            // Anonymous consts
64            ItemKind::Fn {
65                name,
66                generics: _,
67                body: _,
68                params: _,
69                safety: _,
70            } if name.is_empty() => false,
71            // Other unprintable items
72            ItemKind::Error(_) | ItemKind::NotImplementedYet | ItemKind::Use { .. } => false,
73            // Printable items
74            ItemKind::Fn { .. }
75            | ItemKind::TyAlias { .. }
76            | ItemKind::Type { .. }
77            | ItemKind::Trait { .. }
78            | ItemKind::Impl { .. }
79            | ItemKind::Alias { .. }
80            | ItemKind::Resugared(_)
81            | ItemKind::Quote { .. } => true,
82        }
83    }
84}
85
86#[prepend_associated_functions_with(install_pretty_helpers!(self: Self))]
87const _: () = {
88    // Boilerplate: define local macros to disambiguate otherwise `std` macros.
89    #[allow(unused)]
90    macro_rules! todo {($($tt:tt)*) => {disambiguated_todo!($($tt)*)};}
91    #[allow(unused)]
92    macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
93    #[allow(unused)]
94    macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};}
95
96    impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter {
97        fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> {
98            let items = &module.items;
99            docs![
100                intersperse!(
101                    "
102-- Experimental lean backend for Hax
103-- The Hax prelude library can be found in hax/proof-libs/lean
104import Hax
105import Std.Tactic.Do
106import Std.Do.Triple
107import Std.Tactic.Do.Syntax
108open Std.Do
109open Std.Tactic
110
111set_option mvcgen.warning false
112set_option linter.unusedVariables false
113
114
115"
116                    .lines(),
117                    hardline!(),
118                ),
119                intersperse!(items, hardline!())
120            ]
121        }
122
123        fn global_id(&'a self, global_id: &'b GlobalId) -> DocBuilder<'a, Self, A> {
124            // This a temporary fix before a proper treatment of identifiers,
125            // see https://github.com/cryspen/hax/issues/1599
126            docs![global_id.to_debug_string()]
127        }
128
129        fn expr(&'a self, expr: &'b Expr) -> DocBuilder<'a, Self, A> {
130            docs![expr.kind()]
131        }
132
133        fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
134            docs![&*pat.kind, reflow!(" : "), &pat.ty].parens().group()
135        }
136
137        fn expr_kind(&'a self, expr_kind: &'b ExprKind) -> DocBuilder<'a, Self, A> {
138            match expr_kind {
139                ExprKind::If {
140                    condition,
141                    then,
142                    else_,
143                } => {
144                    if let Some(else_branch) = else_ {
145                        docs![
146                            docs!["if", line!(), condition].group(),
147                            line!(),
148                            docs!["then", line!(), then].group().nest(INDENT),
149                            line!(),
150                            docs!["else", line!(), else_branch].group().nest(INDENT)
151                        ]
152                        .group()
153                    } else {
154                        // The Hax engine should ensure that there is always an else branch
155                        unreachable!()
156                    }
157                }
158                ExprKind::App {
159                    head,
160                    args,
161                    generic_args,
162                    bounds_impls: _,
163                    trait_: _,
164                } => {
165                    let generic_args = (!generic_args.is_empty()).then_some(
166                        docs![
167                            line!(),
168                            self.intersperse(generic_args, line!()).nest(INDENT)
169                        ]
170                        .group(),
171                    );
172                    let args = (!args.is_empty()).then_some(
173                        docs![line!(), intersperse!(args, line!()).nest(INDENT)].group(),
174                    );
175                    docs!["← ", head, generic_args, args].parens().group()
176                }
177                ExprKind::Literal(literal) => docs![literal],
178                ExprKind::Array(exprs) => {
179                    docs!["#v[", intersperse!(exprs, reflow!(", ")).nest(INDENT)].group()
180                }
181                ExprKind::Construct {
182                    constructor,
183                    is_record: _,
184                    is_struct: _,
185                    fields,
186                    base: _,
187                } => {
188                    let record_args = (!fields.is_empty()).then_some(
189                        docs![
190                            line!(),
191                            intersperse!(
192                                fields.iter().map(|field: &(GlobalId, Expr)| docs![
193                                    &field.0,
194                                    reflow!(" := "),
195                                    &field.1
196                                ]
197                                .parens()
198                                .group()),
199                                line!()
200                            )
201                            .group()
202                        ]
203                        .group(),
204                    );
205                    docs!["constr_", constructor, record_args]
206                        .parens()
207                        .group()
208                        .nest(INDENT)
209                }
210                ExprKind::Let { lhs, rhs, body } => docs![
211                    "let ",
212                    lhs,
213                    " ←",
214                    softline!(),
215                    docs!["pure", line!(), rhs].group().nest(INDENT),
216                    ";",
217                    line!(),
218                    body,
219                ],
220                ExprKind::GlobalId(global_id) => docs![global_id],
221                ExprKind::LocalId(local_id) => docs![local_id],
222                ExprKind::Ascription { e, ty } => docs![
223                    // This insertion should be done by a monadic phase (or resugaring). See
224                    // https://github.com/cryspen/hax/issues/1620
225                    match *e.kind {
226                        ExprKind::Literal(_) | ExprKind::Construct { .. } => None,
227                        _ => Some("← "),
228                    },
229                    e,
230                    reflow!(" : "),
231                    ty
232                ]
233                .parens()
234                .group(),
235                ExprKind::Closure {
236                    params,
237                    body,
238                    captures: _,
239                } => docs![
240                    reflow!("fun "),
241                    intersperse!(params, softline!()).group(),
242                    reflow!(" => do "),
243                    body
244                ]
245                .parens()
246                .group()
247                .nest(INDENT),
248                ExprKind::Resugared(resugared_expr_kind) => match resugared_expr_kind {
249                    ResugaredExprKind::BinOp {
250                        op,
251                        lhs,
252                        rhs,
253                        generic_args: _,
254                        bounds_impls: _,
255                        trait_: _,
256                    } => {
257                        let symbol = if op == &binops::add() {
258                            "+?"
259                        } else if op == &binops::sub() {
260                            "-?"
261                        } else if op == &binops::mul() {
262                            "*?"
263                        } else if op == &binops::div() {
264                            "/?"
265                        } else if op == &binops::rem() {
266                            "%?"
267                        } else if op == &binops::shr() {
268                            ">>>?"
269                        } else if op == &binops::logical_op_and() {
270                            "&&"
271                        } else if op == &binops::logical_op_or() {
272                            "||"
273                        } else {
274                            unreachable!()
275                        };
276                        // This monad lifting should be handled by a phase/resugaring, see
277                        // https://github.com/cryspen/hax/issues/1620
278                        docs!["← ", lhs, softline!(), symbol, softline!(), rhs]
279                            .group()
280                            .parens()
281                    }
282                },
283                _ => todo!(),
284            }
285        }
286
287        fn pat_kind(&'a self, pat_kind: &'b PatKind) -> DocBuilder<'a, Self, A> {
288            match pat_kind {
289                PatKind::Wild => docs!["_"],
290                PatKind::Ascription { pat, ty: _ } => docs![pat],
291                PatKind::Binding {
292                    mutable,
293                    var,
294                    mode,
295                    sub_pat,
296                } => match (mutable, mode, sub_pat) {
297                    (false, BindingMode::ByValue, None) => docs![var],
298                    _ => panic!(),
299                },
300                _ => todo!(),
301            }
302        }
303
304        fn ty(&'a self, ty: &'b Ty) -> DocBuilder<'a, Self, A> {
305            docs![ty.kind()]
306        }
307
308        fn ty_kind(&'a self, ty_kind: &'b TyKind) -> DocBuilder<'a, Self, A> {
309            match ty_kind {
310                TyKind::Primitive(primitive_ty) => docs![primitive_ty],
311                TyKind::Tuple(items) => intersperse!(items, reflow![" * "]).parens().group(),
312                TyKind::App { head, args } => {
313                    if args.is_empty() {
314                        docs![head]
315                    } else {
316                        docs![head, softline!(), intersperse!(args, softline!())]
317                            .parens()
318                            .group()
319                    }
320                }
321                TyKind::Arrow { inputs, output } => docs![
322                    concat![inputs.iter().map(|input| docs![input, reflow!(" -> ")])],
323                    "Result ",
324                    output
325                ],
326                TyKind::Param(local_id) => docs![local_id],
327                TyKind::Slice(ty) => docs!["RustSlice", line!(), ty].parens().group(),
328                TyKind::Array { ty, length } => {
329                    docs!["RustArray", line!(), ty, line!(), &(**length)]
330                        .parens()
331                        .group()
332                }
333                _ => todo!(),
334            }
335        }
336
337        fn literal(&'a self, literal: &'b Literal) -> DocBuilder<'a, Self, A> {
338            docs![match literal {
339                Literal::String(symbol) => format!("\"{symbol}\""),
340                Literal::Char(c) => format!("'{c}'"),
341                Literal::Bool(b) => format!("{b}"),
342                Literal::Int {
343                    value,
344                    negative,
345                    kind: _,
346                } => format!("{}{value}", if *negative { "-" } else { "" }),
347                Literal::Float {
348                    value: _,
349                    negative: _,
350                    kind: _,
351                } => todo!(),
352            }]
353        }
354
355        fn local_id(&'a self, local_id: &'b LocalId) -> DocBuilder<'a, Self, A> {
356            docs![local_id.0.to_string()]
357        }
358
359        fn spanned_ty(&'a self, spanned_ty: &'b SpannedTy) -> DocBuilder<'a, Self, A> {
360            docs![&spanned_ty.ty]
361        }
362
363        fn primitive_ty(&'a self, primitive_ty: &'b PrimitiveTy) -> DocBuilder<'a, Self, A> {
364            match primitive_ty {
365                PrimitiveTy::Bool => docs!["Bool"],
366                PrimitiveTy::Int(int_kind) => docs![int_kind],
367                PrimitiveTy::Float(_float_kind) => todo!(),
368                PrimitiveTy::Char => docs!["Char"],
369                PrimitiveTy::Str => docs!["String"],
370            }
371        }
372
373        fn int_kind(&'a self, int_kind: &'b IntKind) -> DocBuilder<'a, Self, A> {
374            docs![match (&int_kind.signedness, &int_kind.size) {
375                (Signedness::Signed, IntSize::S8) => "Int8",
376                (Signedness::Signed, IntSize::S16) => "Int16",
377                (Signedness::Signed, IntSize::S32) => "Int32",
378                (Signedness::Signed, IntSize::S64) => "Int64",
379                (Signedness::Signed, IntSize::S128) => todo!(),
380                (Signedness::Signed, IntSize::SSize) => "ISize",
381                (Signedness::Unsigned, IntSize::S8) => "UInt8",
382                (Signedness::Unsigned, IntSize::S16) => "UInt16",
383                (Signedness::Unsigned, IntSize::S32) => "UInt32",
384                (Signedness::Unsigned, IntSize::S64) => "UInt64",
385                (Signedness::Unsigned, IntSize::S128) => todo!(),
386                (Signedness::Unsigned, IntSize::SSize) => "USize",
387            }]
388        }
389
390        fn generic_value(&'a self, generic_value: &'b GenericValue) -> DocBuilder<'a, Self, A> {
391            match generic_value {
392                GenericValue::Ty(ty) => docs![ty],
393                GenericValue::Expr(expr) => docs![expr],
394                GenericValue::Lifetime => todo!(),
395            }
396        }
397
398        fn quote_content(&'a self, quote_content: &'b QuoteContent) -> DocBuilder<'a, Self, A> {
399            match quote_content {
400                QuoteContent::Verbatim(s) => {
401                    intersperse!(s.lines().map(|x| x.to_string()), hardline!())
402                }
403                QuoteContent::Expr(expr) => docs![expr],
404                QuoteContent::Pattern(pat) => docs![pat],
405                QuoteContent::Ty(ty) => docs![ty],
406            }
407        }
408
409        fn quote(&'a self, quote: &'b Quote) -> DocBuilder<'a, Self, A> {
410            concat![&quote.0]
411        }
412
413        fn param(&'a self, param: &'b Param) -> DocBuilder<'a, Self, A> {
414            docs![&param.pat]
415        }
416
417        fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> {
418            docs![&generic_param.ident]
419        }
420
421        fn item_kind(&'a self, item_kind: &'b ItemKind) -> DocBuilder<'a, Self, A> {
422            match item_kind {
423                ItemKind::Fn {
424                    name,
425                    generics,
426                    body,
427                    params,
428                    safety: _,
429                } => match &*body.kind {
430                    // Literal consts. This should be done by a resugaring, see
431                    // https://github.com/cryspen/hax/issues/1614
432                    ExprKind::Literal(l) if params.is_empty() => {
433                        docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group()
434                    }
435                    _ => {
436                        let generics = (!generics.params.is_empty()).then_some(
437                            docs![
438                                line!(),
439                                intersperse!(&generics.params, softline!()).braces().group()
440                            ]
441                            .group(),
442                        );
443                        let args = (!params.is_empty())
444                            .then_some(docs![line!(), intersperse!(params, softline!())].group());
445                        docs![
446                            "def ",
447                            name,
448                            generics,
449                            args,
450                            docs![line!(), ": ", docs!["Result ", &body.ty].group()].group(),
451                            " := do",
452                            line!(),
453                            docs![&*body.kind].group()
454                        ]
455                        .group()
456                        .nest(INDENT)
457                        .append(hardline!())
458                    }
459                },
460                ItemKind::TyAlias {
461                    name,
462                    generics: _,
463                    ty,
464                } => docs!["abbrev ", name, reflow!(" := "), ty].group(),
465                ItemKind::Use {
466                    path: _,
467                    is_external: _,
468                    rename: _,
469                } => nil!(),
470                ItemKind::Quote { quote, origin: _ } => docs![quote],
471                ItemKind::NotImplementedYet => docs!["sorry /- unsupported by the Hax engine -/"],
472                _ => todo!(),
473            }
474        }
475
476        fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A> {
477            if LeanPrinter::printable_item(item) {
478                docs![item.kind()]
479            } else {
480                nil!()
481            }
482        }
483    }
484};
hax_rust_engine/backends/lean.rs

hax_rust_engine/backends/
lean.rs
