diff --git a/CHANGELOG.md b/CHANGELOG.md index 4514d2dbb..88abdcd14 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] Changes to the Rust Engine: + - Remove `BinOp` resugaring (#1950) Changes to the frontend: diff --git a/rust-engine/src/ast/resugared.rs b/rust-engine/src/ast/resugared.rs index 9da0cd12d..c46f3517c 100644 --- a/rust-engine/src/ast/resugared.rs +++ b/rust-engine/src/ast/resugared.rs @@ -50,22 +50,6 @@ pub enum ResugaredItemKind { // TODO: drop `clippy::large_enum_variant` when https://github.com/cryspen/hax/issues/1666 is addressed. #[allow(clippy::large_enum_variant)] pub enum ResugaredExprKind { - /// Binary operations (identified by resugaring) of the form `f(e1, e2)` - BinOp { - /// The identifier of the operation (`f`) - op: GlobalId, - /// The left-hand side of the operation (`e1`) - lhs: Expr, - /// The right-hand side of the operation (`e2`) - rhs: Expr, - /// The generic arguments applied to the function. - generic_args: Vec, - /// If the function requires generic bounds to be called, `bounds_impls` - /// is a vector of impl. expressions for those bounds. - bounds_impls: Vec, - /// If we apply an associated function, contains the impl. expr used. - trait_: Option<(ImplExpr, Vec)>, - }, /// A tuple constructor. /// /// # Example: diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 4c3831090..e257076f0 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -144,20 +144,6 @@ impl Printer for LeanPrinter { fn resugaring_phases() -> Vec> { vec![ Box::new(RecursiveFunctions), - Box::new(BinOp::new(&[ - binops::add, - binops::sub, - binops::mul, - binops::rem, - binops::div, - binops::shr, - binops::shl, - binops::bitand, - binops::bitxor, - binops::logical_op_and, - binops::logical_op_or, - binops::Index::index, - ])), Box::new(FunctionsToConstants), Box::new(LetPure), ] @@ -901,6 +887,49 @@ const _: () = { ([arg], [], ExprKind::GlobalId(binops::neg)) => { docs!["-?", softline!(), arg].parens() } + ([lhs, rhs], [], ExprKind::GlobalId(binops::Index::index)) => { + docs![lhs, "[", line_!(), rhs, line_!(), "]_?"] + .nest(INDENT) + .group() + } + // TODO: Replace this match pattern with an `if let` guard when the feature stabilizes + // Tracking PR: https://github.com/rust-lang/rust/pull/141295 + ( + [lhs, rhs], + [], + ExprKind::GlobalId( + op @ (binops::add + | binops::sub + | binops::mul + | binops::div + | binops::rem + | binops::shr + | binops::shl + | binops::bitand + | binops::bitxor + | binops::logical_op_and + | binops::logical_op_or), + ), + ) => { + let symbol = match *op { + binops::add => "+?", + binops::sub => "-?", + binops::mul => "*?", + binops::div => "/?", + binops::rem => "%?", + binops::shr => ">>>?", + binops::shl => "<< "&&&?", + binops::bitxor => "^^^?", + binops::logical_op_and => "&&?", + binops::logical_op_or => "||?", + _ => unreachable!(), + }; + docs![lhs, line!(), docs![symbol, softline!(), rhs].group()] + .group() + .nest(INDENT) + .parens() + } _ => { // Fallback for any application docs![ @@ -1015,33 +1044,6 @@ const _: () = { .group() .nest(INDENT), - ExprKind::Resugared(ResugaredExprKind::BinOp { op, lhs, rhs, .. }) => { - // TODO : refactor this, moving this code directly in the `App` node (see - // https://github.com/cryspen/hax/issues/1705) - if *op == binops::Index::index { - return docs![lhs, "[", line_!(), rhs, line_!(), "]_?"] - .nest(INDENT) - .group(); - } - let symbol = match *op { - binops::add => "+?", - binops::sub => "-?", - binops::mul => "*?", - binops::div => "/?", - binops::rem => "%?", - binops::shr => ">>>?", - binops::shl => "<< "&&&?", - binops::bitxor => "^^^?", - binops::logical_op_and => "&&?", - binops::logical_op_or => "||?", - _ => unreachable!(), - }; - docs![lhs, line!(), docs![symbol, softline!(), rhs].group()] - .group() - .nest(INDENT) - .parens() - } ExprKind::Resugared(ResugaredExprKind::Tuple { .. }) => { unreachable!("This printer doesn't use the tuple resugaring") } diff --git a/rust-engine/src/backends/rust.rs b/rust-engine/src/backends/rust.rs index e66605966..2f5a08628 100644 --- a/rust-engine/src/backends/rust.rs +++ b/rust-engine/src/backends/rust.rs @@ -590,7 +590,6 @@ const _: () = { } fn resugared_expr_kind(&self, resugared_expr_kind: &ResugaredExprKind) -> DocBuilder { match resugared_expr_kind { - ResugaredExprKind::BinOp { .. } => unreachable!("BinOp resugaring not active"), ResugaredExprKind::Tuple(values) => print_tuple!(values), ResugaredExprKind::LetPure { .. } => unreachable!("LetPure resugaring not active"), } diff --git a/rust-engine/src/resugarings.rs b/rust-engine/src/resugarings.rs index 12bfa9d25..aa68cbffe 100644 --- a/rust-engine/src/resugarings.rs +++ b/rust-engine/src/resugarings.rs @@ -9,7 +9,6 @@ use crate::ast::resugared::*; use crate::ast::visitors::*; use crate::ast::*; use crate::printer::*; -use std::collections::HashSet; /// Transforms [`ItemKind::Fn`] of arity zero into [`ResugaredItemKind::Constant`]. /// Rust `const` items are encoded by the `ImportThir` phase of the hax engine as function of arity zero. @@ -54,61 +53,6 @@ impl Resugaring for FunctionsToConstants { } } -/// Binop resugaring. Used to identify expressions of the form `(f e1 e2)` where -/// `f` is a known identifier. -pub struct BinOp { - /// Stores a set of identifiers that should be resugared as binary - /// operations. Usually, those identifiers come from the hax encoding. Each - /// backend can select its own set of identifiers Typically, if the backend - /// has a special support for addition, `known_ops` will contain - /// `hax::machine::int::add` - pub known_ops: HashSet, -} - -impl BinOp { - /// Adds a new binary operation from a list of (hax-introduced) names - pub fn new(known_ops: &[GlobalId]) -> Self { - Self { - known_ops: HashSet::from_iter(known_ops.iter().cloned()), - } - } -} - -impl AstVisitorMut for BinOp { - fn enter_expr_kind(&mut self, x: &mut ExprKind) { - let ExprKind::App { - head, - args, - generic_args, - bounds_impls, - trait_, - }: &mut ExprKind = x - else { - return; - }; - let ExprKind::GlobalId(id) = &*head.kind else { - return; - }; - let [lhs, rhs] = &args[..] else { return }; - if self.known_ops.iter().any(|defid| id == defid) { - *x = ExprKind::Resugared(ResugaredExprKind::BinOp { - op: *id, - lhs: lhs.clone(), - rhs: rhs.clone(), - generic_args: generic_args.clone(), - bounds_impls: bounds_impls.clone(), - trait_: trait_.clone(), - }); - } - } -} - -impl Resugaring for BinOp { - fn name(&self) -> String { - "binop".to_string() - } -} - /// Tuples resugaring. Resugars tuple constructors to the dedicated expression variant [`ResugaredExprKind::Tuple`], /// and tuple types to the dedicated type variant [`ResugaredTyKind::Tuple`]. pub struct Tuples;