Remove BinOp resugaring

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

@@ -36,22 +36,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

@@ -142,24 +142,7 @@ impl RenderView for LeanPrinter {
 
 impl Printer for LeanPrinter {
     fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
-        vec![
-            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),
-        ]
+        vec![Box::new(FunctionsToConstants), Box::new(LetPure)]
     }
 }
 
@@ -879,6 +862,20 @@ const _: () = {
                     bounds_impls: _,
                     trait_,
                 } => {
+                    let bin_ops = [
+                        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,
+                        binops::Index::index,
+                    ];
                     match (&args[..], &generic_args[..], head.kind()) {
                         ([arg], [], ExprKind::GlobalId(LIFT)) => docs![reflow!("← "), arg].parens(),
                         ([arg], [], ExprKind::GlobalId(PURE)) => {
@@ -900,6 +897,31 @@ const _: () = {
                         ([arg], [], ExprKind::GlobalId(binops::neg)) => {
                             docs!["-?", softline!(), arg].parens()
                         }
+                        ([lhs, rhs], [], ExprKind::GlobalId(op)) if bin_ops.contains(op) => {
+                            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()
+                        }
                         _ => {
                             // Fallback for any application
                             docs![
@@ -1014,33 +1036,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

@@ -54,61 +54,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;