From 18484e28ef7b13b95dc3af0b1e34c2181e1778e5 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Wed, 17 Apr 2024 00:01:34 +0200 Subject: compiler: map `core::mem::swap` to the pure swap In the pure functional model, `swap` is mostly about borrow checking and should simplify to the pure swap in our backends. Other backends than Lean are not done in this commit. Signed-off-by: Ryan Lahfa --- compiler/ExtractBuiltin.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'compiler') diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 3e96c320..531f1d8b 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -287,6 +287,7 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = in [ mk_fun "core::mem::replace" None None; + mk_fun "core::mem::swap" None None; mk_fun "core::slice::{[@T]}::len" (Some (backend_choice "slice::len" "Slice::len")) None; @@ -517,6 +518,7 @@ let builtin_fun_effects = "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"; "alloc::vec::{alloc::vec::Vec<@T, @A>}::len"; "core::mem::replace"; + "core::mem::swap"; "core::mem::take"; "core::option::{core::option::Option<@T>}::take"; "core::clone::impls::{core::clone::Clone}::clone"; -- cgit v1.2.3