feat(rengine): add KnownApplications resugaring

CHANGELOG.md

@@ -9,6 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 Changes to the Rust Engine:
  - The module `names` now produces `ExplicitDefId`s instead of `DefId`s (#1648)
+ - Add a new resugaring `KnownApplications` (#1656)
 
 ## 0.3.4
 

rust-engine/Cargo.toml

@@ -19,6 +19,6 @@ schemars.workspace = true
 itertools.workspace = true
 serde_stacker = "0.1.12"
 pretty = "0.12"
-derive_generic_visitor = "0.3.0"
+derive_generic_visitor = { branch = "basic_impls_arrays", git = "https://github.com/W95Psp/derive-generic-visitor.git" }
 pastey = "0.1.0"
 camino = "1.1.11"

rust-engine/macros/src/replace.rs

@@ -66,7 +66,9 @@ impl Parse for AttributeArgs {
                         GenericConstraint, ErrorNode, Module,
 
                         ResugaredExprKind, ResugaredTyKind, ResugaredPatKind,
-                        ResugaredImplItemKind, ResugaredTraitItemKind, ResugaredItemKind
+                        ResugaredImplItemKind, ResugaredTraitItemKind, ResugaredItemKind,
+
+                        FunApp, NullaryName, UnaryName, BinaryName, TernaryName
                     }.into(),
                     _ => {
                         return Err(syn::Error::new_spanned(

rust-engine/src/ast/resugared.rs

@@ -22,24 +22,172 @@ 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,
+    /// A function application, with special cases for symbols recognized by the engine.
+    /// For instance, we know that `core::ops::Add::add` is a binary operator.
+    FunApp {
         /// 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>)>,
+        /// What know application is this?
+        app: FunApp,
+        /// The function being applied: the original expression, including its metadata.
+        head: Expr,
     },
 }
 
+mod fun_app {
+    use super::*;
+    use crate::ast::identifiers::global_id::{ConcreteId, ExplicitDefId};
+
+    #[derive_group_for_ast]
+    /// A function application, with special cases for sumbols recognized by the engine.
+    /// Symbols recognized by the engine comes with static guarantees about their arity.
+    /// This enum encodes a map between list of known names and static aritites.
+    pub enum FunApp {
+        /// A nullary application
+        Nullary(NullaryName),
+        /// An unary application
+        Unary(UnaryName, [Expr; 1]),
+        /// A binary application
+        Binary(BinaryName, [Expr; 2]),
+        /// Fallback case for unknown applications
+        Unknown {
+            /// The argument of the application.
+            /// Here there is no head, since the head of the application is already available on [`ResugaredExprKind::App`].
+            args: Vec<Expr>,
+        },
+    }
+
+    impl FunApp {
+        /// Tries to destruct a function application to produce a `FunApp`.
+        pub fn destruct_function_application(head: &Expr, args: &[Expr]) -> Self {
+            (|| {
+                let ExprKind::GlobalId(head) = &*head.kind else {
+                    return None;
+                };
+                Some(match args {
+                    [] => Self::Nullary(NullaryName::from_global_id(head.clone())?),
+                    [a] => Self::Unary(UnaryName::from_global_id(head.clone())?, [a.clone()]),
+                    [a, b] => Self::Binary(
+                        BinaryName::from_global_id(head.clone())?,
+                        [a.clone(), b.clone()],
+                    ),
+                    _ => return None,
+                })
+            })()
+            .unwrap_or_else(|| Self::Unknown {
+                args: args.to_vec(),
+            })
+        }
+
+        /// Reconstruct a list of argument from a `FunApp`.
+        pub fn args(&self) -> &[Expr] {
+            match self {
+                Self::Nullary(_) => &[],
+                Self::Unary(_, args) => &args[..],
+                Self::Binary(_, args) => &args[..],
+                Self::Unknown { args } => args,
+            }
+        }
+    }
+
+    macro_rules! mk_enum {
+        ($(
+            $(#$attr:tt)*
+            pub enum $enum_name:ident {
+                $($variant:ident = $name:expr),*
+                $(,)?
+            }
+        )*) => {$(
+            $(#$attr)*
+            pub enum $enum_name {
+                $(
+                    #[doc = concat!("The name `", stringify!($name), "`.")]
+                    $variant,
+                )*
+            }
+
+            impl From<$enum_name> for ExplicitDefId {
+                fn from(v: $enum_name) -> ExplicitDefId {
+                    match v {
+                        $($enum_name::$variant => $name,)*
+                    }
+                }
+            }
+            impl From<$enum_name> for ConcreteId {
+                fn from(v: $enum_name) -> ConcreteId {
+                    ConcreteId {
+                        def_id: v.into(),
+                        moved: None,
+                        suffix: None,
+                    }
+                }
+            }
+            impl From<$enum_name> for GlobalId {
+                fn from(v: $enum_name) -> GlobalId {
+                    GlobalId::Concrete(v.into())
+                }
+            }
+
+            impl $enum_name {
+                #[doc = concat!("Tries to match a global identifier as a [`", stringify!($enum_name), "`]. If the global identifier cannot be turned into a [`", stringify!($enum_name), "`], this method returns `None`.")]
+                #[allow(unused_variables)] // in case of empty enums
+                pub fn from_global_id(global_id: GlobalId) -> Option<$enum_name> {
+                    $(
+                        if global_id == $name {
+                            return Some($enum_name::$variant);
+                        }
+                    )*
+                    return None;
+                }
+            }
+        )*};
+    }
+
+    mod binops {
+        pub use crate::names::rust_primitives::hax::machine_int::{
+            add, div, mul, rem, shl, shr, sub,
+        };
+        pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
+    }
+
+    mk_enum! {
+        #[derive_group_for_ast]
+        /// The names corresponding to callable items of arity 0
+        pub enum NullaryName {}
+
+        #[derive_group_for_ast]
+        /// The names corresponding to callable items of arity 1
+        pub enum UnaryName {
+            DerefOp = crate::names::rust_primitives::hax::deref_op(),
+        }
+
+        #[derive_group_for_ast]
+        /// The names corresponding to callable items of arity 2
+        pub enum BinaryName {
+            Add = binops::add(),
+            Sub = binops::sub(),
+            Mul = binops::mul(),
+            Rem = binops::rem(),
+            Div = binops::div(),
+            Shr = binops::shr(),
+            Shl = binops::shl(),
+            LogicalAnd = binops::logical_op_and(),
+            LogicalOr = binops::logical_op_or(),
+        }
+
+        #[derive_group_for_ast]
+        /// The names corresponding to callable items of arity 2
+        pub enum TernaryName {
+        }
+    }
+}
+pub use fun_app::*;
+
 /// Resugared variants for patterns. This represent extra printing-only patterns, see [`super::PatKind::Resugared`].
 #[derive_group_for_ast]
 pub enum ResugaredPatKind {}

rust-engine/src/ast/visitors.rs

@@ -265,6 +265,7 @@ mod replaced {
                 for<T: AstVisitable> Box<T>, for<T: AstVisitable> Option<T>, for<T: AstVisitable> Vec<T>,
                 for<A: AstVisitable, B: AstVisitable> (A, B),
                 for<A: AstVisitable, B: AstVisitable, C: AstVisitable> (A, B, C),
+                for<T: AstVisitable, const N: usize> [T; N],
                 usize
             ),
             override(AstNodes),
@@ -296,6 +297,7 @@ mod replaced {
                 for<T: AstVisitable> Box<T>, for<T: AstVisitable> Option<T>, for<T: AstVisitable> Vec<T>,
                 for<A: AstVisitable, B: AstVisitable> (A, B),
                 for<A: AstVisitable, B: AstVisitable, C: AstVisitable> (A, B, C),
+                for<T: AstVisitable, const N: usize> [T; N],
                 usize
             ),
             override(AstNodes),

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()
@@ -245,42 +213,58 @@ set_option linter.unusedVariables false
                 .parens()
                 .group()
                 .nest(INDENT),
-                ExprKind::Resugared(resugared_expr_kind) => match resugared_expr_kind {
-                    ResugaredExprKind::BinOp {
-                        op,
-                        lhs,
-                        rhs,
-                        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!()
+                ExprKind::Resugared(resugared_expr_kind) => docs![resugared_expr_kind],
+                _ => todo!(),
+            }
+        }
+        fn resugared_expr_kind(
+            &'a self,
+            resugared_expr_kind: &'b ResugaredExprKind,
+        ) -> DocBuilder<'a, Self, A> {
+            match resugared_expr_kind {
+                ResugaredExprKind::FunApp {
+                    app,
+                    head,
+                    generic_args,
+                    bounds_impls: _,
+                    trait_: _,
+                } => 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
-                        docs!["← ", lhs, softline!(), symbol, softline!(), rhs]
-                            .group()
-                            .parens()
+                        Some(
+                            docs!["← ", lhs, softline!(), op, softline!(), rhs]
+                                .group()
+                                .parens(),
+                        )
                     }
-                },
-                _ => todo!(),
+                    _ => None,
+                }
+                .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()
+                }),
             }
         }