diff --git a/CHANGELOG.md b/CHANGELOG.md index b94a780c7..5a1ab4f0d 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/Cargo.lock b/Cargo.lock index ce64644ef..02905b6a0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -362,8 +362,7 @@ dependencies = [ [[package]] name = "derive_generic_visitor" version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8307b157ef1ca852032be5723dd87063a30a58bc373d663eb327cfbf71f198da" +source = "git+https://github.com/W95Psp/derive-generic-visitor.git?branch=basic_impls_arrays#d99bb4229af11a11f6e712f8bae95d9aa5ee95f9" dependencies = [ "derive_generic_visitor_macros", ] @@ -371,8 +370,7 @@ dependencies = [ [[package]] name = "derive_generic_visitor_macros" version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e20916a23e6247d36d3526a9dce953303a6a83091eaae6d96f08fb3d976ab257" +source = "git+https://github.com/W95Psp/derive-generic-visitor.git?branch=basic_impls_arrays#d99bb4229af11a11f6e712f8bae95d9aa5ee95f9" dependencies = [ "convert_case", "darling", diff --git a/rust-engine/Cargo.toml b/rust-engine/Cargo.toml index 353e6aa77..14c1d7bc0 100644 --- a/rust-engine/Cargo.toml +++ b/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" diff --git a/rust-engine/macros/src/replace.rs b/rust-engine/macros/src/replace.rs index 6e885686d..34127cd21 100644 --- a/rust-engine/macros/src/replace.rs +++ b/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, UnaryName, BinaryName }.into(), _ => { return Err(syn::Error::new_spanned( diff --git a/rust-engine/src/ast/resugared.rs b/rust-engine/src/ast/resugared.rs index 86a0e0f7c..b0122e402 100644 --- a/rust-engine/src/ast/resugared.rs +++ b/rust-engine/src/ast/resugared.rs @@ -22,14 +22,9 @@ 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, /// If the function requires generic bounds to be called, `bounds_impls` @@ -37,9 +32,152 @@ pub enum ResugaredExprKind { bounds_impls: Vec, /// If we apply an associated function, contains the impl. expr used. trait_: Option<(ImplExpr, Vec)>, + /// 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 { + /// 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, + }, + } + + impl FunApp { + /// Tries to destruct a function application to produce a `FunApp`. + pub fn destruct_function_application(head: &Expr, args: &[Expr]) -> Self { + #[inline] + fn inner(head: &Expr, args: &[Expr]) -> Option { + let ExprKind::GlobalId(head) = &*head.kind else { + return None; + }; + Some(match args { + [a] => FunApp::Unary(UnaryName::from_global_id(head.clone())?, [a.clone()]), + [a, b] => FunApp::Binary( + BinaryName::from_global_id(head.clone())?, + [a.clone(), b.clone()], + ), + _ => return None, + }) + } + + inner(head, args).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::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> { + $( + // TODO: rewrite as a pattern matching when https://github.com/cryspen/hax/issues/1666 is addressed + 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 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(), + } + } +} +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 {} diff --git a/rust-engine/src/ast/visitors.rs b/rust-engine/src/ast/visitors.rs index c76339922..3eb9b0ba8 100644 --- a/rust-engine/src/ast/visitors.rs +++ b/rust-engine/src/ast/visitors.rs @@ -265,6 +265,7 @@ mod replaced { for Box, for Option, for Vec, for (A, B), for (A, B, C), + for [T; N], usize ), override(AstNodes), @@ -296,6 +297,7 @@ mod replaced { for Box, for Option, for Vec, for (A, B), for (A, B, C), + for [T; N], usize ), override(AstNodes), diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 31a6d2d61..637988f5f 100644 --- a/rust-engine/src/backends/lean.rs +++ b/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> { - 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::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() + }), } } diff --git a/rust-engine/src/lib.rs b/rust-engine/src/lib.rs index 66f3af47b..b053d9e56 100644 --- a/rust-engine/src/lib.rs +++ b/rust-engine/src/lib.rs @@ -1,6 +1,7 @@ //! The Rust engine of hax. #![feature(rustc_private)] +#![feature(box_patterns)] #![warn( rustdoc::broken_intra_doc_links, missing_docs, diff --git a/rust-engine/src/resugarings.rs b/rust-engine/src/resugarings.rs index b3c517bba..a9b563507 100644 --- a/rust-engine/src/resugarings.rs +++ b/rust-engine/src/resugarings.rs @@ -4,34 +4,18 @@ //! [`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; -/// 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: &[ExplicitDefId]) -> Self { - Self { - known_ops: HashSet::from_iter(known_ops.iter().cloned()), - } - } -} +/// Rewrite every expression application node [`ExprKind::App`] into a +/// [`ResugaredExprKind::App`]. [`ResugaredExprKind::App`] represent known +/// applications with their arity and matchable names, with a fallback case +/// [`App::Unknown`] for unknown functions. +pub struct FunctionApplications; -impl AstVisitorMut for BinOp { +impl AstVisitorMut for FunctionApplications { fn enter_expr_kind(&mut self, x: &mut ExprKind) { let ExprKind::App { head, @@ -43,25 +27,18 @@ impl AstVisitorMut for BinOp { 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(), - }); - } + *x = ExprKind::Resugared(ResugaredExprKind::FunApp { + generic_args: generic_args.clone(), + bounds_impls: bounds_impls.clone(), + trait_: trait_.clone(), + app: FunApp::destruct_function_application(head, args.as_slice()), + head: head.clone(), + }); } } -impl Resugaring for BinOp { +impl Resugaring for FunctionApplications { fn name(&self) -> String { - "binop".to_string() + "function-applications".to_string() } }