smack icon indicating copy to clipboard operation
smack copied to clipboard

Some Rust `Box` operation is internally supported by rustc

Open shaobo-he opened this issue 3 years ago • 1 comments

Consider this program,

// An example from `The Little MLer` chapter 3
#[macro_use]
extern crate smack;
use smack::*;
//#[derive(Debug)]
enum Pizza {
    Crust,
    Cheese(Box<Pizza>),
    Onion(Box<Pizza>),
    Anchovy(Box<Pizza>),
    Sausage(Box<Pizza>),
}
fn make_plain_pizza() -> Pizza {
    Pizza::Crust
}
fn cheese_it_up(pizza: Pizza) -> Pizza {
    Pizza::Cheese(Box::new(pizza))
}
fn add_salt(pizza: Pizza) -> Pizza {
    Pizza::Anchovy(Box::new(pizza))
}
fn remove_anchovy(pizza: Pizza) -> Pizza {
    match pizza {
        Pizza::Crust => pizza,
        Pizza::Cheese(p) => Pizza::Cheese(Box::new(remove_anchovy(*p))),
        Pizza::Onion(p) => Pizza::Onion(Box::new(remove_anchovy(*p))),
        Pizza::Anchovy(p) => remove_anchovy(*p),
        Pizza::Sausage(p) => Pizza::Sausage(Box::new(remove_anchovy(*p))),
    }
}
fn contains_anchovy(pizza: &Pizza) -> bool {
    match pizza {
        Pizza::Crust => false,
        Pizza::Cheese(p) => contains_anchovy(&*p),
        Pizza::Onion(p) => contains_anchovy(&*p),
        Pizza::Anchovy(p) => true,
        Pizza::Sausage(p) => contains_anchovy(&*p),
    }
}
fn main() {
    println!("Hello, world!");
    let salt_double_cheese_pizza = cheese_it_up(add_salt(
                                       cheese_it_up(make_plain_pizza())));
    //println!("{:?}", salt_double_cheese_pizza);
    //assert!(contains_anchovy(&remove_anchovy(salt_double_cheese_pizza)));
    smack::assert!(contains_anchovy(&remove_anchovy(salt_double_cheese_pizza)));
}

SMACK's Box implementation fails to type check with the following message,

error[E0507]: cannot move out of dereference of `smack::Box<Pizza>`
  --> ml.rs:25:67
   |
25 |         Pizza::Cheese(p) => Pizza::Cheese(Box::new(remove_anchovy(*p))),
   |                                                                   ^^ move occurs because value has type `Pizza`, which does not implement the `Copy` trait

It seems *Box<T> is not (cannot be) desugared into a call to deref but instead is treated uniquely by rustc.

This blog post discusses this issue: https://manishearth.github.io/blog/2017/01/10/rust-tidbits-box-is-special/

shaobo-he avatar Feb 03 '22 22:02 shaobo-he

Can we fix this somehow?

zvonimir avatar Feb 13 '22 15:02 zvonimir