Merge pull request #1950 from JuanCoRo/remove-binops-resugaring

Remove `BinOp` resugaring

Author: maximebuyse

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:
 

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<GenericValue>,
-        /// If the function requires generic bounds to be called, `bounds_impls`
-        /// is a vector of impl. expressions for those bounds.
-        bounds_impls: Vec<ImplExpr>,
-        /// If we apply an associated function, contains the impl. expr used.
-        trait_: Option<(ImplExpr, Vec<GenericValue>)>,
-    },
     /// A tuple constructor.
     ///
     /// # Example:

rust-engine/src/backends/lean.rs

@@ -144,20 +144,6 @@ impl Printer for LeanPrinter {
     fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
         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::bitand => "&&&?",
+                                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::bitand => "&&&?",
-                        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")
                 }

rust-engine/src/backends/rust.rs

@@ -590,7 +590,6 @@ const _: () = {
         }
         fn resugared_expr_kind(&self, resugared_expr_kind: &ResugaredExprKind) -> DocBuilder<A> {
             match resugared_expr_kind {
-                ResugaredExprKind::BinOp { .. } => unreachable!("BinOp resugaring not active"),
                 ResugaredExprKind::Tuple(values) => print_tuple!(values),
                 ResugaredExprKind::LetPure { .. } => unreachable!("LetPure resugaring not active"),
             }

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<GlobalId>,
-}
-
-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;