Add #[is_variant] to enable adt.is_Variant() and adt.get_Variant()

[utaal]

This adds support for the following:

#[is_variant]
pub enum Maybe<T> {
    Some(T),
    None,
}

pub fn test1(m: Maybe<u64>) {
    match m {
        Maybe::Some(_) => assert(m.is_Some()),
        Maybe::None => assert(m.is_None()),
    };
}

pub fn test2(m: Maybe<u64>) -> bool {
    ensures(|res: bool|
        (m.is_Some() >>= res == (m.get_Some().0 == 3)) &&
        (m.is_None() >>= !res)
    );
    match m {
        Maybe::Some(v) => v == 3,
        Maybe::None => false,
    }
}

where is_Some, is_None, and get_Some are auto-generated by the #[is_variant] attribute-proc-macro.
is_Some and is_None are tagged as #[verifier(is_variant)] and encoded using AIR/SMT's builtin (is-Variant) (like pattern matching VCs).

---

Once this is approved, I'll add #[is_variant] to, e.g. pervasive::Option.

[utaal]

This is just moving the derive_structural proc macro to a separate module. No code changes in this function.

[Chris-Hawblitzel]

It looks like the is_variant feature goes straight to the underlying VIR/SMT UnaryOpr::IsVariant, which is efficient. On the other hand, m.get_Some().0 introduces a pattern match, tuple construction, and tuple selection, which is less efficient than just a direct field selection. Is there any way we can support direct translation into a VIR/SMT field access, similar to the treatment of is_variant?

[utaal]

I've discussed this with @Chris-Hawblitzel offline, and implemented direct field selection, with the scheme described here #41
Will wait for comments there before merging.