AdrienChampion/hashconsing

Derive macro?

Opened this issue · 9 comments

Hey! This is a super cool crate. I actually just had someone introduce me to this topic and it was cool to see a crate that does it. I was curious if there had been any thought into implementing a derive macro for this? I'm not 100% on the details but I'm imagining something like

#[derive(HConsed, Debug, Hash, Clone, PartialEq, Eq)]
enum Term {
    Var(usize),
    Lam(Term),
    App(Term, Term)
}

instead of currently

type Term = HConsed<ActualTerm> ;

#[derive(Debug, Hash, Clone, PartialEq, Eq)]
enum ActualTerm {
    Var(usize),
    Lam(Term),
    App(Term, Term)
}

And just randomly, I'm wondering if you have any thoughts on updating the edition to 2021? Sorry if you've already considered this.

Hey thank you for your kind words 😸

Regarding the derive macro, it's definitely something we could propose. We can generate the identifier RawTerm for the raw term type automatically, but having a way to specify this identifier explicitly seems mandatory to me.

Other than that I'm all for it, it's really a matter of taking the time to write the proc-macro.

And just randomly, I'm wondering if you have any thoughts on updating the edition to 2021? Sorry if you've already considered this.

Oh sure that's quite easy to do, the library is fairly small and I don't expect anything significant to deal with when upgrading to 2021.

I have not done it because i) nobody asked and ii) it's not very interesting a change by itself. Definitely something we would do alongside a fix / new feature (like a derive macro) before publishing though

For the derive macro, I would expect it to look like this:

#[derive(HConsed(RawTerm), Debug, Hash, Clone, PartialEq, Eq)]
enum Term {
    Var(usize),
    Lam(RawTerm),
    App(Term, RawTerm)
}

This means the proc-macro is transparent in that it does not need to change anything in your enum definition. It also gives more control in case someone decides to put a Term (not a RawTerm) somewhere --- though this seems like a bad idea.

@Pat-Lafon would you be interested in writing the derive macro by any chance?

Sure, I would be interested in attempting it.

For the derive macro, I would expect it to look like this:

#[derive(HConsed(RawTerm), Debug, Hash, Clone, PartialEq, Eq)]
enum Term {
    Var(usize),
    Lam(RawTerm),
    App(Term, RawTerm)
}

This means the proc-macro is transparent in that it does not need to change anything in your enum definition. It also gives more control in case someone decides to put a Term (not a RawTerm) somewhere --- though this seems like a bad idea.

To clarify on the kind of code you want this to generate, will your example generate something like?

type Term = HConsed<RawTerm>;

#[derive(Debug, Hash, Clone, PartialEq, Eq)]
enum RawTerm {
    Var(usize),
    Lam(RawTerm),
    App(Term, RawTerm)
}

I've written a proc_macro or two but I'm not totally sure what actually goes into a derive, so there are probably limitations here that I'm not aware of yet. I might not be able to rename the enum for instance. I'm not sure yet if derive can take arguments. Maybe an attribute macro is more appropriate? https://doc.rust-lang.org/reference/procedural-macros.html#derive-macros

I was also wondering if you were interested in generating additional parts of the documentation example?

The following appears at first glance to be rather standard and shouldn't be that hard to derive.

    consign! {
        /// Factory for terms.
        let factory = consign(37) for RawlTerm ;
    }
    pub fn var(v: usize) -> Term {
        factory.mk( RawTerm::Var(v) )
    }
    pub fn lam(t: Term) -> Term {
        factory.mk( RawTerm::Lam(t) )
    }
    pub fn app(t_1: Term, t_2: Term) -> Term {
        factory.mk( RawTerm::App(t_1, t_2) )
    }

If one was going down this route, I think I would switch from using type aliasing of the HConsed<T> and instead use https://doc.rust-lang.org/rust-by-example/generics/new_types.html . Then maybe you could derive something like Term::Var(v) via

impl Term {
    pub fn Var(v:usize) -> Term {
        Term(FACTORY.mk(RawTerm::Var(v)))
    }
}

(or maybe some other name like Term::mk_Var(v))