From c0c89587d2ac1fcc3048cc1b6737b2e56f8f6640 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 19 Aug 2025 14:38:36 +0200 Subject: [PATCH 01/21] Make more names available in the printer prelude --- rust-engine/src/backends.rs | 9 +++++++-- rust-engine/src/backends/rust.rs | 6 +++--- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/rust-engine/src/backends.rs b/rust-engine/src/backends.rs index 0884d67e7..2d1b0e522 100644 --- a/rust-engine/src/backends.rs +++ b/rust-engine/src/backends.rs @@ -18,7 +18,7 @@ pub mod lean; pub mod rust; use crate::{ - ast::{Item, Metadata, Module, span::Span}, + ast::{span::Span, Item, Metadata, Module}, printer::{Print, Printer}, }; use hax_types::engine_api::File; @@ -51,7 +51,7 @@ pub trait Backend { /// The AST phases to apply before printing. /// - /// Backends can override this to add transformations. + /// Backends can override this to add transformations. /// The default is an empty list (no transformations). fn phases(&self) -> Vec> { vec![] @@ -115,10 +115,15 @@ mod prelude { //! Importing this prelude saves repetitive `use` lists in per-backend //! modules without forcing these names on downstream users. pub use super::Backend; + pub use crate::ast::identifiers::*; + pub use crate::ast::literals::*; + pub use crate::ast::resugared::*; pub use crate::ast::*; pub use crate::printer::*; + pub use crate::symbol::Symbol; pub use hax_rust_engine_macros::prepend_associated_functions_with; pub use pretty::DocAllocator; + pub use pretty::DocBuilder; pub use pretty::Pretty; pub use pretty_ast::install_pretty_helpers; } diff --git a/rust-engine/src/backends/rust.rs b/rust-engine/src/backends/rust.rs index 6936f84ca..7abdea2d8 100644 --- a/rust-engine/src/backends/rust.rs +++ b/rust-engine/src/backends/rust.rs @@ -42,13 +42,13 @@ const _: () = { macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};} impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for RustPrinter { - fn module(&'a self, module: &'b Module) -> pretty::DocBuilder<'a, Self, A> { + fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> { intersperse!(&module.items, docs![hardline!(), hardline!()]) } - fn item(&'a self, item: &'b Item) -> pretty::DocBuilder<'a, Self, A> { + fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A> { docs![&item.meta, item.kind()] } - fn item_kind(&'a self, item_kind: &'b ItemKind) -> pretty::DocBuilder<'a, Self, A> { + fn item_kind(&'a self, item_kind: &'b ItemKind) -> DocBuilder<'a, Self, A> { match item_kind { ItemKind::Fn { name, From d7e371c1b027823aab2a32115d4a8763bd944bab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 19 Aug 2025 14:43:53 +0200 Subject: [PATCH 02/21] Update lean test --- tests/lean-tests/src/lib.rs | 29 +++++++++++++++++++++++------ 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index f98bc471b..fec8d1a63 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -1,6 +1,7 @@ #![allow(dead_code)] const FORTYTWO: usize = 42; +const MinusFORTYTWO: isize = -42; fn returns42() -> usize { FORTYTWO @@ -19,16 +20,32 @@ fn letBinding(x: usize, y: usize) -> usize { fn closure() -> i32 { let x = 41; - let f1 = |y| y + x ; + let f1 = |y| y + x; let f2 = |y, z| y + x + z; - f1(1) + f2(2,3) + f1(1) + f2(2, 3) } #[hax_lib::lean::before("@[spec]")] -fn test_before_verbatime_single_line(x: u8) -> u8 { 42 } +fn test_before_verbatime_single_line(x: u8) -> u8 { + 42 +} -#[hax_lib::lean::before(" +#[hax_lib::lean::before( + " def multiline : Unit := () -")] -fn test_before_verbatim_multi_line(x: u8) -> u8 { 32 } +" +)] +fn test_before_verbatim_multi_line(x: u8) -> u8 { + 32 +} + +type TId = i8; +type TTuple = ( + (), + (u8,), + (u8, u16), + (u8, u16, u32), + (u8, u16, u32, u64), + (u8, u16, u32, u64, usize), +); From 4292f0fe6f39e91e8385b826bcfb87feebe8aa22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 19 Aug 2025 17:19:16 +0200 Subject: [PATCH 03/21] Rewrote Lean backend --- rust-engine/src/backends.rs | 2 +- rust-engine/src/backends/lean.rs | 961 ++++++------------ rust-engine/src/main.rs | 52 +- .../toolchain__lean-tests into-lean.snap | 51 +- tests/lean-tests/src/lib.rs | 10 - 5 files changed, 367 insertions(+), 709 deletions(-) diff --git a/rust-engine/src/backends.rs b/rust-engine/src/backends.rs index 2d1b0e522..e832ad787 100644 --- a/rust-engine/src/backends.rs +++ b/rust-engine/src/backends.rs @@ -18,7 +18,7 @@ pub mod lean; pub mod rust; use crate::{ - ast::{span::Span, Item, Metadata, Module}, + ast::{Item, Metadata, Module, span::Span}, printer::{Print, Printer}, }; use hax_types::engine_api::File; diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index a0104d7ac..98bd2733c 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -4,128 +4,40 @@ //! Pretty::Doc type, which can in turn be exported to string (or, eventually, //! source maps). -use crate::ast::span::Span; - -use pretty::{DocAllocator, DocBuilder, Pretty, docs}; - -use crate::ast::identifiers::*; -use crate::ast::literals::*; -use crate::ast::*; - -// Note: this module was moved here temporarly. -// This module used to provide a wrapper type `Allocator`. -// This wrapper type is no longer useful. -// It was thus removed from the `printer`, and moved here, where it is still used. -// This is temporary: see https://github.com/cryspen/hax/issues/1604. -mod deprecated_allocator_module { - //! This module provides a custom [`pretty`] allocator, indexed by a printer, - //! enabling multiple printers to cohexist and to implement the type `Pretty`. - - use crate::ast::span::Span; - use pretty::*; - - /// A printer-specific [`pretty`] allocator. - pub struct Allocator { - /// The pretty allocator - allocator: BoxAllocator, - /// Extra printer-specific context - pub printer: Printer, - } - - impl Allocator { - /// Creates a new allocator from a printer. - pub fn new(printer: Printer) -> Self { - Self { - allocator: BoxAllocator, - printer, - } - } - } +use super::prelude::*; - impl<'a, P, A: 'a> DocAllocator<'a, A> for Allocator

{ - type Doc = >::Doc; +/// The Lean printer +#[derive(Default)] +pub struct LeanPrinter; +impl_doc_allocator_for!(LeanPrinter); - fn alloc(&'a self, doc: Doc<'a, Self::Doc, A>) -> Self::Doc { - self.allocator.alloc(doc) - } - - fn alloc_column_fn( - &'a self, - f: impl Fn(usize) -> Self::Doc + 'a, - ) -> >::ColumnFn { - self.allocator.alloc_column_fn(f) - } - - fn alloc_width_fn( - &'a self, - f: impl Fn(isize) -> Self::Doc + 'a, - ) -> >::WidthFn { - self.allocator.alloc_width_fn(f) - } +impl Printer for LeanPrinter { + fn resugaring_phases() -> Vec> { + vec![] } - /// A helper type used to manually implement `Pretty` for types that carry spans. - /// - /// By default, we implement the `Pretty` trait for all span-carrying - /// types. These implementations annotate spans in the generated document, allowing - /// source spans to be produced during pretty-printing. However, this default behavior - /// does not provide access to the underlying data, which is sometimes necessary - /// for custom printing logic. - /// - /// For example, when printing an item, it's often useful to access its attributes. - /// To support this, the default `Pretty` implementations delegate to `Manual`, - /// which allows printers to access the inner value directly. - /// - /// In practice, calling `expr.pretty(..)` will internally use - /// `Manual(expr).pretty(..)`, enabling more flexible control over printing behavior. - struct Manual(T); - - use crate::ast::*; - macro_rules! impl_pretty_kind_meta { - ($($type:ty),*) => { - $(impl<'a, 'b, P> Pretty<'a, Allocator

, Span> for &'b $type - where - Manual<&'b $type>: Pretty<'a, Allocator

, Span>, - { - fn pretty(self, allocator: &'a Allocator

) -> DocBuilder<'a, Allocator

, Span> { - let doc = Manual(self).pretty(allocator); - doc.annotate(self.span()) - } - })* - }; - } - impl_pretty_kind_meta!( - Item, - Expr, - Pat, - Guard, - Arm, - ImplItem, - TraitItem, - GenericParam, - Attribute - ); + const NAME: &str = "Lean"; } -pub use deprecated_allocator_module::Allocator; - -macro_rules! print_todo { - ($allocator:ident) => { - $allocator - .text(format!( - "/- Unsupported by the Lean Backend (line {}) -/", - line!() - )) - .parens() - }; +const INDENT: isize = 2; + +/// The Lean backend +pub struct LeanBackend; + +fn crate_name(items: &Vec) -> String { + let head_item = items.get(0).unwrap(); + head_item.ident.krate() } -const INDENT: isize = 2; +impl Backend for LeanBackend { + type Printer = LeanPrinter; -/// Placeholder structure for lean printer -pub struct Lean; + fn module_path(&self, module: &Module) -> std::path::PathBuf { + std::path::PathBuf::from(format!("{}.lean", crate_name(&module.items))) + } +} -impl Lean { +impl LeanPrinter { /// A filter for items blacklisted by the Lean backend : returns false if /// the item is definitely not printable, but might return true on /// unsupported items @@ -154,568 +66,359 @@ impl Lean { } } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Item { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.kind.pretty(allocator) - } -} +#[prepend_associated_functions_with(install_pretty_helpers!(self: Self))] +const _: () = { + // Boilerplate: define local macros to disambiguate otherwise `std` macros. + #[allow(unused)] + macro_rules! todo {($($tt:tt)*) => {disambiguated_todo!($($tt)*)};} + #[allow(unused)] + macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};} + #[allow(unused)] + macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};} + + impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter { + fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> { + let items = &module.items; + // .iter() + // .filter(LeanPrinter::printable_item); + docs![ + intersperse!( + " +-- Experimental lean backend for Hax +-- Lib.lean can be found in hax/proof-libs/lean : +import Hax +import Std.Tactic.Do +import Std.Do.Triple +import Std.Tactic.Do.Syntax +open Std.Do +open Std.Tactic + +set_option mvcgen.warning false +set_option linter.unusedVariables false" + .lines(), + hardline!(), + ), + hardline!(), + hardline!(), + intersperse!(items, hardline!()) + ] + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - ItemKind::Fn { - name, - generics, - body, - params, - safety: _, - } => { - match &*body.kind { - ExprKind::Literal(l) => { - // Literal consts, printed without monadic encoding - // Todo: turn it into a proper refactor (see Hax issue #1542) + fn global_id(&'a self, global_id: &'b GlobalId) -> DocBuilder<'a, Self, A> { + docs![global_id.to_debug_string()] + } + + fn expr(&'a self, expr: &'b Expr) -> DocBuilder<'a, Self, A> { + docs![expr.kind()] + } + + fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> { + docs![&*pat.kind, reflow!(" : "), &pat.ty].parens().group() + } + + fn expr_kind(&'a self, expr_kind: &'b ExprKind) -> DocBuilder<'a, Self, A> { + match expr_kind { + ExprKind::If { + condition, + then, + else_, + } => { + if let Some(else_branch) = else_ { docs![ - allocator, - "def ", - name, - allocator.reflow(" : "), - &body.ty, - allocator.reflow(" :="), - allocator.line(), - l + docs!["if", line!(), condition].group(), + line!(), + docs!["then", line!(), then].group().nest(INDENT), + line!(), + docs!["else", line!(), else_branch].group().nest(INDENT) ] .group() + } else { + todo!() } - _ => { - // Normal definition - let generics = if generics.params.is_empty() { - None - } else { - Some( - docs![ - allocator, - allocator.line(), - allocator - .intersperse(&generics.params, allocator.softline()) - .braces() - .group() + } + ExprKind::App { + head, + args, + generic_args, + bounds_impls: _, + trait_: _, + } => { + let generic_args = (!generic_args.is_empty()).then_some( + docs![ + line!(), + self.intersperse(generic_args, line!()).nest(INDENT) + ] + .group(), + ); + let args = (!args.is_empty()).then_some( + docs![line!(), intersperse!(args, line!()).nest(INDENT)].group(), + ); + docs!["← ", head, generic_args, args].parens().group() + } + ExprKind::Literal(literal) => docs![literal], + ExprKind::Array(exprs) => { + docs!["#v[", intersperse!(exprs, reflow!(", ")).nest(INDENT)].group() + } + ExprKind::Construct { + constructor, + is_record: _, + is_struct: _, + fields, + base: _, + } => { + // Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged + let record_args = (fields.len() > 0).then_some( + docs![ + line!(), + intersperse!( + fields.iter().map(|field: &(GlobalId, Expr)| docs![ + &field.0, + reflow!(" := "), + &field.1 ] - .group(), + .parens() + .group()), + line!() ) - }; - let args = if params.is_empty() { - allocator.nil() - } else { - docs![ - allocator, - allocator.line(), - allocator.intersperse(params, allocator.softline()), - ] - .nest(INDENT) .group() - }; - docs![ - allocator, - "def ", - name, - generics, - args, - docs![ - allocator, - allocator.line(), - ": ", - docs![allocator, "Result ", &body.ty].group() - ] - .group(), - " := do", - allocator.line(), - docs![allocator, &*body.kind].group() ] - .nest(INDENT) - .group() - .append(allocator.hardline()) - } - } - } - ItemKind::TyAlias { - name, - generics: _, - ty, - } => docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty].group(), - ItemKind::Type { - name: _, - generics: _, - variants: _, - is_struct: _, - } => print_todo!(allocator), - ItemKind::Trait { - name: _, - generics: _, - items: _, - } => print_todo!(allocator), - ItemKind::Impl { - generics: _, - self_ty: _, - of_trait: _, - items: _, - parent_bounds: _, - safety: _, - } => print_todo!(allocator), - ItemKind::Alias { name: _, item: _ } => print_todo!(allocator), - ItemKind::Use { - path: _, - is_external: _, - rename: _, - } => allocator.nil(), - ItemKind::Quote { quote, origin: _ } => quote.pretty(allocator), - ItemKind::Error(_diagnostic) => print_todo!(allocator), - ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator), - ItemKind::NotImplementedYet => allocator.text("/- unsupported by Hax engine (yet) -/"), - } - } -} - -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Ty { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.kind().pretty(allocator) - } -} - -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - TyKind::Primitive(primitive_ty) => primitive_ty.pretty(allocator), - TyKind::Tuple(items) => allocator.intersperse(items, allocator.reflow(" * ")), - TyKind::App { head, args } => { - if args.len() == 0 { - head.pretty(allocator) - } else { - head.pretty(allocator) - .append(allocator.softline()) - .append(allocator.intersperse(args, allocator.softline())) + .group(), + ); + docs!["constr_", constructor, record_args] .parens() .group() + .nest(INDENT) } + ExprKind::Let { lhs, rhs, body } => docs![ + "let ", + lhs, + " ←", + softline!(), + docs!["pure", line!(), rhs].group().nest(INDENT), + ";", + line!(), + body, + ], + ExprKind::GlobalId(global_id) => docs![global_id], + ExprKind::LocalId(local_id) => docs![local_id], + ExprKind::Ascription { e, ty } => docs![ + match *e.kind { + ExprKind::Literal(_) | ExprKind::Construct { .. } => None, + _ => Some("← "), + }, + e, + reflow!(" : "), + ty + ] + .parens() + .group(), + ExprKind::Closure { + params, + body, + captures: _, + } => docs![ + reflow!("fun "), + intersperse!(params, softline!()).group(), + reflow!(" => do "), + body + ] + .parens() + .group() + .nest(INDENT), + _ => todo!(), } - TyKind::Arrow { inputs, output } => docs![ - allocator, - allocator.concat(inputs.into_iter().map(|input| docs![ - allocator, - input, - allocator.reflow(" -> ") - ])), - "Result ", - output - ] - .parens(), - TyKind::Ref { - inner: _, - mutable: _, - region: _, - } => print_todo!(allocator), - TyKind::Param(local_id) => local_id.pretty(allocator), - TyKind::Slice(ty) => docs![allocator, "Array ", ty].parens(), - TyKind::Array { ty, length } => { - docs![allocator, "Vector ", ty, allocator.softline(), &(**length),] - .parens() - .group() - } - TyKind::RawPointer => print_todo!(allocator), - TyKind::AssociatedType { impl_: _, item: _ } => print_todo!(allocator), - TyKind::Opaque(_global_id) => print_todo!(allocator), - TyKind::Dyn(_dyn_trait_goals) => print_todo!(allocator), - TyKind::Resugared(_resugared_ty_kind) => print_todo!(allocator), - TyKind::Error(_diagnostic) => print_todo!(allocator), } - } -} -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b SpannedTy { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.ty.pretty(allocator) - } -} - -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b PrimitiveTy { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - PrimitiveTy::Bool => allocator.text("Bool"), - PrimitiveTy::Int(int_kind) => int_kind.pretty(allocator), - PrimitiveTy::Float(float_kind) => float_kind.pretty(allocator), - PrimitiveTy::Char => allocator.text("Char"), - PrimitiveTy::Str => allocator.text("String"), + fn pat_kind(&'a self, pat_kind: &'b PatKind) -> DocBuilder<'a, Self, A> { + match pat_kind { + PatKind::Wild => docs!["_"], + PatKind::Ascription { pat, ty: _ } => docs![pat], + PatKind::Binding { + mutable, + var, + mode, + sub_pat, + } => match (mutable, mode, sub_pat) { + (false, BindingMode::ByValue, None) => docs![var], + _ => panic!(), + }, + _ => todo!(), + } } - } -} - -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Expr { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - (*self.kind).pretty(allocator) - } -} -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Pat { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - docs![ - allocator, - self.kind.pretty(allocator), - allocator.reflow(" : "), - &self.ty - ] - .parens() - .group() - } -} - -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b PatKind { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - PatKind::Wild => allocator.text("_"), - PatKind::Ascription { pat, ty: _ } => pat.kind.pretty(allocator), - PatKind::Or { sub_pats: _ } => print_todo!(allocator), - PatKind::Array { args: _ } => print_todo!(allocator), - PatKind::Deref { sub_pat: _ } => print_todo!(allocator), - PatKind::Constant { lit: _ } => print_todo!(allocator), - PatKind::Binding { - mutable, - var, - mode, - sub_pat, - } => match (mutable, mode, sub_pat) { - (false, BindingMode::ByValue, None) => var.pretty(allocator), - _ => panic!(), - }, - PatKind::Construct { - constructor: _, - is_record: _, - is_struct: _, - fields: _, - } => print_todo!(allocator), - PatKind::Resugared(_resugared_pat_kind) => print_todo!(allocator), - PatKind::Error(_diagnostic) => print_todo!(allocator), + fn ty(&'a self, ty: &'b Ty) -> DocBuilder<'a, Self, A> { + ty.kind().pretty(self) } - } -} - -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Lhs { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - print_todo!(allocator) - } -} -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - ExprKind::If { - condition, - then, - else_, - } => match else_ { - Some(else_branch) => docs![ - allocator, - allocator - .text("if") - .append(allocator.line()) - .append(condition) - .group(), - allocator.line(), - allocator - .text("then") - .append(allocator.line()) - .append(then) - .group() - .nest(INDENT), - allocator.line(), - allocator - .text("else") - .append(allocator.line()) - .append(else_branch) - .group() - .nest(INDENT), - ] - .group(), - None => print_todo!(allocator), - }, - ExprKind::App { - head, - args, - generic_args: _, - bounds_impls: _, - trait_: _, - } if match &*head.kind { - ExprKind::GlobalId(name) => { - *name == crate::names::rust_primitives::hax::machine_int::add() + fn ty_kind(&'a self, ty_kind: &'b TyKind) -> DocBuilder<'a, Self, A> { + match ty_kind { + TyKind::Primitive(primitive_ty) => docs![primitive_ty], + TyKind::Tuple(items) => intersperse!(items, reflow![" * "]).parens().group(), + TyKind::App { head, args } => { + if args.len() == 0 { + docs![head] + } else { + docs![head, softline!(), intersperse!(args, softline!())] + .parens() + .group() + } } - _ => false, - } && args.len() == 2 => - { - docs![ - allocator, - "← ", - args.get(0), - allocator.reflow(" +? "), - args.get(1), - ] - .parens() - .group() + TyKind::Arrow { inputs, output } => docs![ + concat![ + inputs + .into_iter() + .map(|input| docs![input, reflow!(" -> ")]) + ], + "Result ", + output + ], + TyKind::Param(local_id) => docs![local_id], + TyKind::Slice(ty) => docs!["RustSlice ", ty].parens().group(), + TyKind::Array { ty, length } => docs!["RustArray ", ty, softline!(), &(**length)], + _ => todo!(), } - ExprKind::App { - head, - args, - generic_args, - bounds_impls: _, - trait_: _, - } => { - let generic_args = (!generic_args.is_empty()).then_some( - allocator - .line() - .append( - allocator - .intersperse(generic_args, allocator.line()) - .nest(INDENT), - ) - .group(), - ); - let args = if args.is_empty() { - None - } else { - Some( - allocator - .line() - .append(allocator.intersperse(args, allocator.line()).nest(INDENT)) - .group(), - ) - }; - docs![allocator, "← ", head, generic_args, args] - .parens() - .group() - } - ExprKind::Literal(literal) => literal.pretty(allocator), - ExprKind::Array(exprs) => docs![ - allocator, - "#v[", - allocator - .intersperse(exprs, allocator.text(",").append(allocator.line())) - .nest(INDENT), - "]" - ] - .group(), - ExprKind::Construct { - constructor, - is_record: _, - is_struct: _, - fields, - base: _, - } => { - // Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged - let record_args = (fields.len() > 0).then_some( - allocator - .line() - .append( - allocator - .intersperse( - fields.iter().map(|field: &(GlobalId, Expr)| { - docs![ - allocator, - &field.0, - allocator.reflow(" := "), - &field.1 - ] - .parens() - .group() - }), - allocator.line(), - ) - .group(), - ) - .group(), - ); - docs![allocator, "constr_", constructor, record_args] - .parens() - .group() - .nest(INDENT) - } - ExprKind::Match { - scrutinee: _, - arms: _, - } => print_todo!(allocator), - ExprKind::Tuple(_exprs) => print_todo!(allocator), - ExprKind::Borrow { - mutable: _, - inner: _, - } => print_todo!(allocator), - ExprKind::AddressOf { - mutable: _, - inner: _, - } => print_todo!(allocator), - ExprKind::Deref(_expr) => print_todo!(allocator), - ExprKind::Let { lhs, rhs, body } => docs![ - allocator, - "let ", - lhs, - " ←", - allocator.softline(), - docs![allocator, "pure", allocator.line(), rhs] - .group() - .nest(INDENT), - ";", - allocator.line(), - body, - ] - .group(), - ExprKind::GlobalId(global_id) => global_id.pretty(allocator), - ExprKind::LocalId(local_id) => local_id.pretty(allocator), - ExprKind::Ascription { e, ty } => { - let monadic_encoding = match *e.kind { - ExprKind::Literal(_) | ExprKind::Construct { .. } => None, - _ => Some("← "), - }; - docs![allocator, monadic_encoding, e, allocator.reflow(" : "), ty] - .parens() - .group() - } - ExprKind::Assign { lhs: _, value: _ } => print_todo!(allocator), - ExprKind::Loop { - body: _, - kind: _, - state: _, - control_flow: _, - label: _, - } => print_todo!(allocator), - ExprKind::Break { value: _, label: _ } => print_todo!(allocator), - ExprKind::Return { value: _ } => print_todo!(allocator), - ExprKind::Continue { label: _ } => print_todo!(allocator), - ExprKind::Closure { - params, - body, - captures: _, - } => docs![ - allocator, - allocator.reflow("fun "), - allocator.intersperse(params, allocator.softline()).group(), - allocator.reflow("=> do"), - allocator.line(), - body - ] - .parens() - .group() - .nest(INDENT), - ExprKind::Block { - body: _, - safety_mode: _, - } => print_todo!(allocator), - ExprKind::Quote { contents } => allocator.concat(&contents.0), - ExprKind::Resugared(_resugared_expr_kind) => print_todo!(allocator), - ExprKind::Error(_diagnostic) => print_todo!(allocator), } - } -} -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Literal { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - docs![ - allocator, - match self { + fn literal(&'a self, literal: &'b Literal) -> DocBuilder<'a, Self, A> { + docs![match literal { Literal::String(symbol) => format!("\"{}\"", symbol.to_string()), Literal::Char(c) => format!("'{}'", c), Literal::Bool(b) => format!("{}", b), Literal::Int { value, - negative: _, + negative, kind: _, - } => format!("{}", value), + } => format!("{}{value}", if *negative { "-" } else { "" }), Literal::Float { value: _, negative: _, kind: _, } => todo!(), - } - ] - } -} + }] + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b IntKind { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - docs![ - allocator, - match (&self.size, &self.signedness) { - (IntSize::S8, Signedness::Signed) => "i8", - (IntSize::S8, Signedness::Unsigned) => "u8", - (IntSize::S16, Signedness::Signed) => "i16", - (IntSize::S16, Signedness::Unsigned) => "u16", - (IntSize::S32, Signedness::Signed) => "i32", - (IntSize::S32, Signedness::Unsigned) => "u32", - (IntSize::S64, Signedness::Signed) => "i64", - (IntSize::S64, Signedness::Unsigned) => "u64", - (IntSize::S128, Signedness::Signed) => "i128", - (IntSize::S128, Signedness::Unsigned) => "u128", - (IntSize::SSize, Signedness::Signed) => "isize", - (IntSize::SSize, Signedness::Unsigned) => "usize", - } - ] - } -} + fn local_id(&'a self, local_id: &'b LocalId) -> DocBuilder<'a, Self, A> { + docs![local_id.0.to_string()] + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b FloatKind { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - FloatKind::F16 => print_todo!(allocator), - FloatKind::F32 => allocator.text("Float32"), - FloatKind::F64 => allocator.text("Float"), - FloatKind::F128 => print_todo!(allocator), + fn spanned_ty(&'a self, spanned_ty: &'b SpannedTy) -> DocBuilder<'a, Self, A> { + docs![&spanned_ty.ty] } - } -} -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b GenericValue { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - GenericValue::Ty(ty) => ty.pretty(allocator), - GenericValue::Expr(expr) => expr.pretty(allocator), - GenericValue::Lifetime => panic!(), + fn primitive_ty(&'a self, primitive_ty: &'b PrimitiveTy) -> DocBuilder<'a, Self, A> { + match primitive_ty { + PrimitiveTy::Bool => docs!["Bool"], + PrimitiveTy::Int(int_kind) => docs![int_kind], + PrimitiveTy::Float(_float_kind) => todo!(), + PrimitiveTy::Char => docs!["Char"], + PrimitiveTy::Str => docs!["String"], + } } - } -} -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b LocalId { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - allocator.text(self.to_string()) - } -} + fn int_kind(&'a self, int_kind: &'b IntKind) -> DocBuilder<'a, Self, A> { + docs![match (&int_kind.signedness, &int_kind.size) { + (Signedness::Signed, IntSize::S8) => "Int8", + (Signedness::Signed, IntSize::S16) => "Int16", + (Signedness::Signed, IntSize::S32) => "Int32", + (Signedness::Signed, IntSize::S64) => "Int64", + (Signedness::Signed, IntSize::S128) => todo!(), + (Signedness::Signed, IntSize::SSize) => "ISize", + (Signedness::Unsigned, IntSize::S8) => "UInt8", + (Signedness::Unsigned, IntSize::S16) => "UInt16", + (Signedness::Unsigned, IntSize::S32) => "UInt32", + (Signedness::Unsigned, IntSize::S64) => "UInt64", + (Signedness::Unsigned, IntSize::S128) => todo!(), + (Signedness::Unsigned, IntSize::SSize) => "USize", + }] + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b GlobalId { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - allocator.text(self.to_debug_string()) - } -} + fn generic_value(&'a self, generic_value: &'b GenericValue) -> DocBuilder<'a, Self, A> { + match generic_value { + GenericValue::Ty(ty) => docs![ty], + GenericValue::Expr(expr) => docs![expr], + GenericValue::Lifetime => todo!(), + } + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Param { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.pat.pretty(allocator) - } -} + fn quote_content(&'a self, quote_content: &'b QuoteContent) -> DocBuilder<'a, Self, A> { + match quote_content { + QuoteContent::Verbatim(s) => { + intersperse!(s.lines().map(|x| x.to_string()), hardline!()) + } + QuoteContent::Expr(expr) => docs![expr], + QuoteContent::Pattern(pat) => docs![pat], + QuoteContent::Ty(ty) => docs![ty], + } + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b GenericParam { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.ident.pretty(allocator) - } -} + fn quote(&'a self, quote: &'b Quote) -> DocBuilder<'a, Self, A> { + concat!["e.0] + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Quote { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - allocator.concat(&self.0) - } -} + fn param(&'a self, param: &'b Param) -> DocBuilder<'a, Self, A> { + docs![¶m.pat] + } + + fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> { + docs![&generic_param.ident] + } -impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b QuoteContent { - fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - match self { - QuoteContent::Verbatim(s) => { - allocator.intersperse(s.lines().map(|x| x.to_string()), allocator.hardline()) + fn item_kind(&'a self, item_kind: &'b ItemKind) -> DocBuilder<'a, Self, A> { + match item_kind { + ItemKind::Fn { + name, + generics, + body, + params, + safety: _, + } => match &*body.kind { + // Literal consts + ExprKind::Literal(l) if params.len() == 0 => { + docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group() + } + _ => { + let generics = (!generics.params.is_empty()).then_some( + docs![ + line!(), + intersperse!(&generics.params, softline!()).braces().group() + ] + .group(), + ); + let args = (!params.is_empty()) + .then_some(docs![line!(), intersperse!(params, softline!())].group()); + docs![ + "def ", + name, + generics, + args, + docs![line!(), ": ", docs!["Result ", &body.ty].group()].group(), + " := do", + line!(), + docs![&*body.kind].group() + ] + .group() + .nest(INDENT) + .append(hardline!()) + } + }, + ItemKind::TyAlias { + name, + generics: _, + ty, + } => docs!["abbrev ", name, reflow!(" := "), ty].group(), + ItemKind::Use { + path: _, + is_external: _, + rename: _, + } => nil!(), + ItemKind::Quote { quote, origin: _ } => docs![quote], + ItemKind::NotImplementedYet => docs!["sorry /- unsupported by the Hax engine -/"], + _ => todo!(), } - QuoteContent::Expr(expr) => expr.pretty(allocator), - QuoteContent::Pattern(pat) => pat.pretty(allocator), - QuoteContent::Ty(ty) => ty.pretty(allocator), + } + + fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A> { + docs![item.kind()] } } -} +}; diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index be9036a5b..a7fe35437 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -1,59 +1,9 @@ use hax_rust_engine::{ - ast::{Item, span::Span}, backends, ocaml_engine::{ExtendedToEngine, Response}, }; use hax_types::{cli_options::Backend, engine_api::File}; -use pretty::{DocAllocator, DocBuilder, docs}; - -fn krate_name(items: &Vec) -> String { - let head_item = items.get(0).unwrap(); - head_item.ident.krate() -} - -fn lean_backend(items: Vec) -> Vec { - use backends::lean::*; - let krate = krate_name(&items); - - // For now, the main function always calls the Lean backend - let allocator = &Allocator::new(Lean); - - let header = docs![ - allocator, - allocator.intersperse( - " --- Experimental lean backend for Hax --- Lib.lean can be found in hax/proof-libs/lean : -import Lib -import Std.Tactic.Do -import Std.Do.Triple -import Std.Tactic.Do.Syntax -open Std.Do -open Std.Tactic - -set_option mvcgen.warning false -set_option linter.unusedVariables false" - .lines(), - allocator.hardline(), - ), - allocator.hardline(), - allocator.hardline() - ]; - - let items = items - .iter() - .filter(|item: &&hax_rust_engine::ast::Item| Lean::printable_item(*item)); - let item_docs: DocBuilder<_, Span> = - header.append(allocator.intersperse(items, allocator.hardline())); - - vec![File { - path: krate + ".lean", - contents: item_docs.pretty(80).to_string(), - sourcemap: None, - }] -} - fn main() { let ExtendedToEngine::Query(input) = hax_rust_engine::hax_io::read() else { panic!() @@ -82,7 +32,7 @@ fn main() { "The Rust engine cannot be called with backend {}.", value.backend.backend ), - Backend::Lean => lean_backend(items), + Backend::Lean => backends::apply_backend(backends::lean::LeanBackend, items), Backend::Rust => backends::apply_backend(backends::rust::RustBackend, items), Backend::GenerateRustEngineNames => vec![File { path: "generated.rs".into(), diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index 870526afd..0934be3eb 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -31,7 +31,7 @@ diagnostics = [] -- Experimental lean backend for Hax -- Lib.lean can be found in hax/proof-libs/lean : -import Lib +import Hax import Std.Tactic.Do import Std.Do.Triple import Std.Tactic.Do.Syntax @@ -41,29 +41,44 @@ open Std.Tactic set_option mvcgen.warning false set_option linter.unusedVariables false -def FORTYTWO : usize := 42 -def returns42 (_ : hax_Tuple0) : Result usize := do FORTYTWO -def add_two_numbers (x : usize) (y : usize) : Result usize := do (← x +? y) +sorry /- unsupported by the Hax engine -/ +def FORTYTWO : USize := 42 +def MinusFORTYTWO : ISize := -42 +def returns42 (_ : hax_Tuple0) : Result USize := do FORTYTWO -def letBinding (x : usize) (y : usize) : Result usize := do +def add_two_numbers (x : USize) (y : USize) : Result USize := do + (← hax_machine_int_add x y) + +def letBinding (x : USize) (y : USize) : Result USize := do let (useless : hax_Tuple0) ← pure (constr_hax_Tuple0); - let (result1 : usize) ← pure (← x +? y); - let (result2 : usize) ← pure (← result1 +? 2); (← result2 +? 1) + let (result1 : USize) ← pure (← hax_machine_int_add x y); + let (result2 : USize) ← pure (← hax_machine_int_add result1 2); + (← hax_machine_int_add result2 1) + +def closure (_ : hax_Tuple0) : Result Int32 := do + let (x : Int32) ← pure 41; + let (f1 : Int32 -> Result Int32) ← pure + (fun (y : Int32) => do (← hax_machine_int_add y x)); + let (f2 : Int32 -> Int32 -> Result Int32) ← pure + (fun (y : Int32) (z : Int32) => do (← hax_machine_int_add + (← hax_machine_int_add y x) + z)); + (← hax_machine_int_add + (← ops_function_Fn_call f1 (constr_hax_Tuple1 (hax_Tuple1_Tuple0 := 1))) + (← ops_function_Fn_call + f2 + (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) -def closure (_ : hax_Tuple0) : Result i32 := do - let (x : i32) ← pure 41; - let (f1 : (i32 -> Result i32)) ← pure (fun (y : i32)=> do (← y +? x)); - let (f2 : (i32 -> i32 -> Result i32)) ← pure - (fun (y : i32) (z : i32)=> do (← (← y +? x) +? z)); - (← (← ops_function_Fn_call f1 (constr_hax_Tuple1 (hax_Tuple1_Tuple0 := 1))) +? - (← ops_function_Fn_call - f2 - (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) +def _ : Result hax_Tuple0 := do hax_Tuple0 @[spec] -def test_before_verbatime_single_line : u8 := 42 +def test_before_verbatime_single_line (x : UInt8) : Result UInt8 := do 42 + +def _ : Result hax_Tuple0 := do hax_Tuple0 + def multiline : Unit := () -def test_before_verbatim_multi_line : u8 := 32''' +def test_before_verbatim_multi_line (x : UInt8) : Result UInt8 := do 32 +''' diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index fec8d1a63..382bd3d0b 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -39,13 +39,3 @@ def multiline : Unit := () fn test_before_verbatim_multi_line(x: u8) -> u8 { 32 } - -type TId = i8; -type TTuple = ( - (), - (u8,), - (u8, u16), - (u8, u16, u32), - (u8, u16, u32, u64), - (u8, u16, u32, u64, usize), -); From 17700dea16a6d2b089de14b03ce356b410dc3862 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 20 Aug 2025 10:49:08 +0200 Subject: [PATCH 04/21] Update Lean header --- rust-engine/src/backends/lean.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 98bd2733c..3e6da2812 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -85,7 +85,7 @@ const _: () = { intersperse!( " -- Experimental lean backend for Hax --- Lib.lean can be found in hax/proof-libs/lean : +-- The Hax prelude library can be found in hax/proof-libs/lean import Hax import Std.Tactic.Do import Std.Do.Triple @@ -94,12 +94,13 @@ open Std.Do open Std.Tactic set_option mvcgen.warning false -set_option linter.unusedVariables false" - .lines(), +set_option linter.unusedVariables false + + +" + .lines(), hardline!(), ), - hardline!(), - hardline!(), intersperse!(items, hardline!()) ] } From 12cefd9e0b0540dc47fdd40230409be4d31dbcc0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 20 Aug 2025 11:04:16 +0200 Subject: [PATCH 05/21] Do not print unprintable items --- rust-engine/src/backends/lean.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 3e6da2812..02a71747a 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -419,7 +419,11 @@ set_option linter.unusedVariables false } fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A> { - docs![item.kind()] + if LeanPrinter::printable_item(&item) { + docs![item.kind()] + } else { + nil!() + } } } }; From 40f4dd68c03e20e7ab0ddc81bcc2eaf9bbe3f873 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 20 Aug 2025 11:04:28 +0200 Subject: [PATCH 06/21] Add missing coercions for numeric constants --- hax-lib/proof-libs/lean/Lib.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index e82ea89f8..f2b57befc 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -220,6 +220,8 @@ instance {β} : Coe (α -> i32 -> β) (α -> Nat -> β) where instance : OfNat (Result Nat) n where ofNat := pure (n) +instance {α n} [i: OfNat α n] : OfNat (Result α) n where + ofNat := pure (i.ofNat) /- From baeb0e0087a95152ab26747993d480a1912378a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 20 Aug 2025 11:28:40 +0200 Subject: [PATCH 07/21] Update test snapshot --- .../src/snapshots/toolchain__lean-tests into-lean.snap | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index 0934be3eb..0283d9f9b 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -30,7 +30,7 @@ diagnostics = [] "lean_tests.lean" = ''' -- Experimental lean backend for Hax --- Lib.lean can be found in hax/proof-libs/lean : +-- The Hax prelude library can be found in hax/proof-libs/lean import Hax import Std.Tactic.Do import Std.Do.Triple @@ -42,7 +42,7 @@ set_option mvcgen.warning false set_option linter.unusedVariables false -sorry /- unsupported by the Hax engine -/ + def FORTYTWO : USize := 42 def MinusFORTYTWO : ISize := -42 def returns42 (_ : hax_Tuple0) : Result USize := do FORTYTWO @@ -70,12 +70,10 @@ def closure (_ : hax_Tuple0) : Result Int32 := do f2 (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) -def _ : Result hax_Tuple0 := do hax_Tuple0 @[spec] def test_before_verbatime_single_line (x : UInt8) : Result UInt8 := do 42 -def _ : Result hax_Tuple0 := do hax_Tuple0 def multiline : Unit := () From 4bd0b4017e4a7bae5392b4349a7411be1d105c9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 20 Aug 2025 11:31:46 +0200 Subject: [PATCH 08/21] Update Lib --- hax-lib/proof-libs/lean/Lib.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index f2b57befc..3ecfe71e2 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -817,7 +817,9 @@ end Fold Rust arrays, are represented as Lean `Vector` (Lean Arrays of known size) -/ -section Array +section RustArray + +abbrev RustArray := Vector inductive array_TryFromSliceError where | array_TryFromSliceError @@ -849,7 +851,7 @@ def convert_TryInto_try_into {α n} (a: Array α) : .err .array_TryFromSliceError ) -end Array +end RustArray /- @@ -1040,6 +1042,8 @@ Rust vectors are represented as Lean Arrays (variable size) -/ section RustVectors +abbrev RustVector := Array + def alloc_Global : Type := Unit def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α From f9fe3f0223582bb17f128c31d75c309df561a23b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 18:52:18 +0200 Subject: [PATCH 09/21] Update name in test --- test-harness/src/snapshots/toolchain__lean-tests into-lean.snap | 2 +- tests/lean-tests/src/lib.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index 0283d9f9b..3d43536c2 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -44,7 +44,7 @@ set_option linter.unusedVariables false def FORTYTWO : USize := 42 -def MinusFORTYTWO : ISize := -42 +def MINUS_FORTYTWO : ISize := -42 def returns42 (_ : hax_Tuple0) : Result USize := do FORTYTWO def add_two_numbers (x : USize) (y : USize) : Result USize := do diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index 382bd3d0b..60b994067 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -1,7 +1,7 @@ #![allow(dead_code)] const FORTYTWO: usize = 42; -const MinusFORTYTWO: isize = -42; +const MINUS_FORTYTWO: isize = -42; fn returns42() -> usize { FORTYTWO From aeb0f4d7484e013cfe78fbbb721437069ff259e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 18:54:10 +0200 Subject: [PATCH 10/21] Remove commented out lines --- rust-engine/src/backends/lean.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 02a71747a..120a25480 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -79,8 +79,6 @@ const _: () = { impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter { fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> { let items = &module.items; - // .iter() - // .filter(LeanPrinter::printable_item); docs![ intersperse!( " From b4910b2a9341932862c103ff3d23f3111a3c9ff2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 18:57:05 +0200 Subject: [PATCH 11/21] Add a comment point to the issue #1599 --- rust-engine/src/backends/lean.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 120a25480..95e6579e8 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -104,6 +104,8 @@ set_option linter.unusedVariables false } fn global_id(&'a self, global_id: &'b GlobalId) -> DocBuilder<'a, Self, A> { + // This a temporary fix before a proper treatment of identifiers, + // see https://github.com/cryspen/hax/issues/1599 docs![global_id.to_debug_string()] } From e8ced8d0ef33ca3c53da4125696f8c988a38c47d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 18:58:43 +0200 Subject: [PATCH 12/21] Turn todo into unreachable + add comment --- rust-engine/src/backends/lean.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 95e6579e8..6a78a71c9 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -134,7 +134,8 @@ set_option linter.unusedVariables false ] .group() } else { - todo!() + // The Hax engine should ensure that there is always an else branch + unreachable!() } } ExprKind::App { From 30353da3d9671a9030092be872660b3339222c2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 19:03:36 +0200 Subject: [PATCH 13/21] Remove out-of-date comment --- rust-engine/src/backends/lean.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 6a78a71c9..3bb72e19a 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -168,7 +168,6 @@ set_option linter.unusedVariables false fields, base: _, } => { - // Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged let record_args = (fields.len() > 0).then_some( docs![ line!(), From 7cbb4d6fc6c31df1977857342b6c0be89f2849c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 19:06:34 +0200 Subject: [PATCH 14/21] Style change --- rust-engine/src/backends/lean.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 3bb72e19a..f65cb2923 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -248,7 +248,7 @@ set_option linter.unusedVariables false } fn ty(&'a self, ty: &'b Ty) -> DocBuilder<'a, Self, A> { - ty.kind().pretty(self) + docs![ty.kind()] } fn ty_kind(&'a self, ty_kind: &'b TyKind) -> DocBuilder<'a, Self, A> { From c6e6ba71eaf77abb3a8768ae98412ae7e9d032d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= <40171892+clementblaudeau@users.noreply.github.com> Date: Thu, 21 Aug 2025 19:08:05 +0200 Subject: [PATCH 15/21] Replace `len() == 0` by `is_empty()` Co-authored-by: Lucas Franceschino --- rust-engine/src/backends/lean.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index f65cb2923..4233099c7 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -256,7 +256,7 @@ set_option linter.unusedVariables false TyKind::Primitive(primitive_ty) => docs![primitive_ty], TyKind::Tuple(items) => intersperse!(items, reflow![" * "]).parens().group(), TyKind::App { head, args } => { - if args.len() == 0 { + if args.is_empty() { docs![head] } else { docs![head, softline!(), intersperse!(args, softline!())] From 5dbd2ade6d1230cb8c034ac5752d275fe1eff52b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 19:09:20 +0200 Subject: [PATCH 16/21] Add spaces line-break points instead of hard spaces --- rust-engine/src/backends/lean.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 4233099c7..cf7e98410 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -274,8 +274,12 @@ set_option linter.unusedVariables false output ], TyKind::Param(local_id) => docs![local_id], - TyKind::Slice(ty) => docs!["RustSlice ", ty].parens().group(), - TyKind::Array { ty, length } => docs!["RustArray ", ty, softline!(), &(**length)], + TyKind::Slice(ty) => docs!["RustSlice", line!(), ty].parens().group(), + TyKind::Array { ty, length } => { + docs!["RustArray", line!(), ty, line!(), &(**length)] + .parens() + .group() + } _ => todo!(), } } From fbb4509e1465937a84fa2f4c20e6dc29d631b951 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 21 Aug 2025 19:13:57 +0200 Subject: [PATCH 17/21] Open issue for a missing resugaring --- rust-engine/src/backends/lean.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index cf7e98410..533a03482 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -377,7 +377,8 @@ set_option linter.unusedVariables false params, safety: _, } => match &*body.kind { - // Literal consts + // Literal consts. This should be done by a resugaring, see + // https://github.com/cryspen/hax/issues/1614 ExprKind::Literal(l) if params.len() == 0 => { docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group() } From 33135196311d7ba1accacf81edd1dfdc27a5a1a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 25 Aug 2025 09:31:55 +0200 Subject: [PATCH 18/21] Add a todo for the unwrap --- rust-engine/src/backends/lean.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 533a03482..26d88d952 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -25,6 +25,8 @@ const INDENT: isize = 2; pub struct LeanBackend; fn crate_name(items: &Vec) -> String { + // We should have a proper treatment of empty modules, see + // https://github.com/cryspen/hax/issues/1617 let head_item = items.get(0).unwrap(); head_item.ident.krate() } From f5f166142a71587caaa2f8c85524ec15d70182a6 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Aug 2025 18:42:42 +0200 Subject: [PATCH 19/21] chore(rengine): `cargo clippy -- --fix --no-deps` + mnual edits --- rust-engine/src/ast/identifiers.rs | 2 +- rust-engine/src/backends/lean.rs | 20 ++++++++------------ rust-engine/src/main.rs | 6 +++--- 3 files changed, 12 insertions(+), 16 deletions(-) diff --git a/rust-engine/src/ast/identifiers.rs b/rust-engine/src/ast/identifiers.rs index 203169ed8..a3739b6e9 100644 --- a/rust-engine/src/ast/identifiers.rs +++ b/rust-engine/src/ast/identifiers.rs @@ -105,7 +105,7 @@ pub mod global_id { /// Tests if the raw output is reduced to "_". Should be used only for /// testing. See https://github.com/cryspen/hax/issues/1599 pub fn is_empty(&self) -> bool { - self.to_debug_string() == "_".to_string() + self.to_debug_string() == "_" } /// Extract the raw `DefId` from a `GlobalId`. diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 26d88d952..ff4416de5 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -27,7 +27,7 @@ pub struct LeanBackend; fn crate_name(items: &Vec) -> String { // We should have a proper treatment of empty modules, see // https://github.com/cryspen/hax/issues/1617 - let head_item = items.get(0).unwrap(); + let head_item = items.first().unwrap(); head_item.ident.krate() } @@ -170,7 +170,7 @@ set_option linter.unusedVariables false fields, base: _, } => { - let record_args = (fields.len() > 0).then_some( + let record_args = (!fields.is_empty()).then_some( docs![ line!(), intersperse!( @@ -267,11 +267,7 @@ set_option linter.unusedVariables false } } TyKind::Arrow { inputs, output } => docs![ - concat![ - inputs - .into_iter() - .map(|input| docs![input, reflow!(" -> ")]) - ], + concat![inputs.iter().map(|input| docs![input, reflow!(" -> ")])], "Result ", output ], @@ -288,9 +284,9 @@ set_option linter.unusedVariables false fn literal(&'a self, literal: &'b Literal) -> DocBuilder<'a, Self, A> { docs![match literal { - Literal::String(symbol) => format!("\"{}\"", symbol.to_string()), - Literal::Char(c) => format!("'{}'", c), - Literal::Bool(b) => format!("{}", b), + Literal::String(symbol) => format!("\"{symbol}\""), + Literal::Char(c) => format!("'{c}'"), + Literal::Bool(b) => format!("{b}"), Literal::Int { value, negative, @@ -381,7 +377,7 @@ set_option linter.unusedVariables false } => match &*body.kind { // Literal consts. This should be done by a resugaring, see // https://github.com/cryspen/hax/issues/1614 - ExprKind::Literal(l) if params.len() == 0 => { + ExprKind::Literal(l) if params.is_empty() => { docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group() } _ => { @@ -426,7 +422,7 @@ set_option linter.unusedVariables false } fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A> { - if LeanPrinter::printable_item(&item) { + if LeanPrinter::printable_item(item) { docs![item.kind()] } else { nil!() diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index a7fe35437..b23971f62 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -25,9 +25,9 @@ fn main() { let files = match &value.backend.backend { Backend::Fstar { .. } - | Backend::Coq { .. } - | Backend::Ssprove { .. } - | Backend::Easycrypt { .. } + | Backend::Coq + | Backend::Ssprove + | Backend::Easycrypt | Backend::ProVerif { .. } => panic!( "The Rust engine cannot be called with backend {}.", value.backend.backend From 00006b8f129c7791b29b4dfe1679856cc88ffd24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 25 Aug 2025 12:15:11 +0200 Subject: [PATCH 20/21] clippy --- rust-engine/src/backends/lean.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 5e50f2f22..7060ca73f 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -24,7 +24,7 @@ const INDENT: isize = 2; /// The Lean backend pub struct LeanBackend; -fn crate_name(items: &Vec) -> String { +fn crate_name(items: &[Item]) -> String { // We should have a proper treatment of empty modules, see // https://github.com/cryspen/hax/issues/1617 let head_item = items.first().unwrap(); From 6f30e9aceed26c924682d27ab5c22997cb3f3f47 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 25 Aug 2025 12:52:00 +0200 Subject: [PATCH 21/21] Open #1620 and refer to it in comment --- rust-engine/src/backends/lean.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 7060ca73f..3785c3cd7 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -205,6 +205,8 @@ set_option linter.unusedVariables false ExprKind::GlobalId(global_id) => docs![global_id], ExprKind::LocalId(local_id) => docs![local_id], ExprKind::Ascription { e, ty } => docs![ + // This insertion should be done by a monadic phase (or resugaring). See + // https://github.com/cryspen/hax/issues/1620 match *e.kind { ExprKind::Literal(_) | ExprKind::Construct { .. } => None, _ => Some("← "),