feat(rengine): drop BinOp resugaring in favor of FunctionApplications

Author: W95Psp

rust-engine/src/ast/resugared.rs

@@ -22,22 +22,6 @@ pub enum ResugaredItemKind {}
 /// Resugared variants for expressions. This represent extra printing-only expressions, see [`super::ExprKind::Resugared`].
 #[derive_group_for_ast]
 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 function application recognized by the engine, with static arity.
     FunApp {
         /// The generic arguments applied to the function.

rust-engine/src/backends/lean.rs

@@ -5,12 +5,7 @@
 //! source maps).
 
 use super::prelude::*;
-use crate::resugarings::BinOp;
-
-mod binops {
-    pub use crate::names::rust_primitives::hax::machine_int::{add, div, mul, rem, shr, sub};
-    pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
-}
+use crate::resugarings;
 
 /// The Lean printer
 #[derive(Default)]
@@ -19,16 +14,7 @@ impl_doc_allocator_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::logical_op_and(),
-            binops::logical_op_or(),
-        ]))]
+        vec![Box::new(resugarings::FunctionApplications)]
     }
 
     const NAME: &str = "Lean";
@@ -155,25 +141,7 @@ set_option linter.unusedVariables false
                         unreachable!()
                     }
                 }
-                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::App { .. } => unreachable!("See resugaring [FunctionApplications]"),
                 ExprKind::Literal(literal) => docs![literal],
                 ExprKind::Array(exprs) => {
                     docs!["#v[", intersperse!(exprs, reflow!(", ")).nest(INDENT)].group()
@@ -254,38 +222,49 @@ set_option linter.unusedVariables false
             resugared_expr_kind: &'b ResugaredExprKind,
         ) -> DocBuilder<'a, Self, A> {
             match resugared_expr_kind {
-                ResugaredExprKind::BinOp {
-                    op,
-                    lhs,
-                    rhs,
-                    generic_args: _,
+                ResugaredExprKind::FunApp {
+                    app,
+                    head,
+                    generic_args,
                     bounds_impls: _,
                     trait_: _,
-                } => {
-                    let symbol = if op == &binops::add() {
-                        "+?"
-                    } else if op == &binops::sub() {
-                        "-?"
-                    } else if op == &binops::mul() {
-                        "*?"
-                    } else if op == &binops::div() {
-                        "/?"
-                    } else if op == &binops::rem() {
-                        "%?"
-                    } else if op == &binops::shr() {
-                        ">>>?"
-                    } else if op == &binops::logical_op_and() {
-                        "&&"
-                    } else if op == &binops::logical_op_or() {
-                        "||"
-                    } else {
-                        unreachable!()
-                    };
-                    docs!["← ", lhs, softline!(), symbol, softline!(), rhs]
-                        .group()
-                        .parens()
+                } => match app {
+                    FunApp::Binary(op, [lhs, rhs]) => {
+                        let op = match op {
+                            BinaryName::Add => "+?",
+                            BinaryName::Sub => "-?",
+                            BinaryName::Mul => "*?",
+                            BinaryName::Rem => "%?",
+                            BinaryName::Div => "/?",
+                            BinaryName::Shr => ">>>?",
+                            BinaryName::Shl => "<<<?",
+                            BinaryName::LogicalAnd => "&&",
+                            BinaryName::LogicalOr => "||",
+                        };
+                        // This monad lifting should be handled by a phase/resugaring, see
+                        // https://github.com/cryspen/hax/issues/1620
+                        Some(
+                            docs!["← ", lhs, softline!(), op, softline!(), rhs]
+                                .group()
+                                .parens(),
+                        )
+                    }
+                    _ => None,
                 }
-                _ => todo!(),
+                .unwrap_or_else(|| {
+                    let args = app.args();
+                    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()
+                }),
             }
         }
 

rust-engine/src/resugarings.rs

@@ -4,12 +4,10 @@
 //! [`hax_rust_engine::ast::Resugaring`] for the definition of a
 //! resugaring). Each backend defines its own set of resugaring phases.
 
-use crate::ast::identifiers::global_id::ExplicitDefId;
 use crate::ast::resugared::*;
 use crate::ast::visitors::*;
 use crate::ast::*;
 use crate::printer::*;
-use std::collections::HashSet;
 
 /// Rewrite every expression application node [`ExprKind::App`] into a
 /// [`ResugaredExprKind::App`]. [`ResugaredExprKind::App`] represent known
@@ -44,58 +42,3 @@ impl Resugaring for FunctionApplications {
         "function-applications".to_string()
     }
 }
-
-/// 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<ExplicitDefId>,
-}
-
-impl BinOp {
-    /// Adds a new binary operation from a list of (hax-introduced) names
-    pub fn new(known_ops: &[ExplicitDefId]) -> 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.clone(),
-                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()
-    }
-}