feat: LeanCtorLayout trait and lean_inductive! macro

[samuelburnham]

Adds a LeanCtorLayout trait for inductives and structures with a LAYOUTS array that contains the number of objects, usizes, and scalar types (e.g. u64 or bool) for each inductive variant. The LAYOUTS index is the tag/variant index of the inductive:

pub struct SingleCtorLayout {
    pub num_obj: usize,
    pub num_usize: usize,
    pub num_64: usize,
    pub num_32: usize,
    pub num_16: usize,
    pub num_8: usize,
}
pub trait LeanCtorLayout {
    const LAYOUTS: &'static [SingleCtorLayout];
}

This allows the user to implement the trait as follows:

// In Lean:
//structure Pair where
//  fst : String
//  snd : bool

impl<R: LeanRef> LeanCtorLayout for LeanPair<R> {
    const LAYOUTS: &'static [SingleCtorLayout] = &[
        SingleCtorLayout { num_obj: 1, num_8: 1, ..SingleCtorLayout::ZERO },
    ];
}

Or use the lean_inductive! convenience macro, which also calls lean_domain_type! to create the LeanPair wrapper type and generates getters and setters for every type in SingleCtorLayout:

lean_inductive! {
    // Strings are stored as objects and booleans are stored as uint8_t in C
    LeanPair [ { num_obj: 1, num_8: 1 } ]  
}

Then the user can write:

let p = LeanPair::alloc(0); // Ctor tag is 0 for structures
p.set_obj(0, LeanString::new("hello")); // 0 is the object index 
p.set_num_8(0, true as u8); // 0 is the 8-bit type index (bool in this case)

Users still have to know how many fields of a given size are in the Lean structure and the index of each one they want to access, but it's better than having to manually compute byte offsets for scalar values.

[arthurpaulino]

My first review pass focuses mainly on booleans, given the recent changes that happened on ix.

[arthurpaulino]

Looks good!
I'll wait for argumentcomputer/ix#380 to be updated with this new approach

[arthurpaulino]

Looks great!