Weak tables

[lenianiva]

Is there a way to use WHConsed as keys in a weak hash table like weak_table? If not I can write one and open a PR

[AdrienChampion]

Once you have a HConsed value, you can weak-ify it using to_weak.

[AdrienChampion]

I took a brief look at weak_table, and it seems to be compatible with them we need to implement some trait, probably WeakElement, and/or give access to Weak ref stored in WHConsed.

[AdrienChampion]

I prefer the latter as it avoids conditionally depending on yet another library, what do you think @vleni ?

[lenianiva]

I took a brief look at weak_table, and it seems to be compatible with them we need to implement some trait, probably WeakElement, and/or give access to Weak ref stored in WHConsed.

I think giving access to the weak pointer inside would be a good idea. The to_weak function in HConsed doesn't give a Weak pointer though, and that is needed for weak_table.

[asvarga]

How is this intended to be used? I tried combining the hashconsing and weak_table doc demos, and the only thing I could get to work is:

let mut table = <WeakKeyHashMap<Weak<ActualTerm>, u32>>::new();
let one = var(1);
table.insert(one.to_weak_ref().upgrade().unwrap(), 1);    // yuck
assert_eq!(table.get(&one), Some(&1));

but this seems wrong/redundant.

[AdrienChampion]

Hi @asvarga!

Sorry for the delay. I'm not sure how this is intended to be used as I don't use weak_table myself, it was a feature request.

However, looking at weak_table's API (for the first time), it seems like to_weak_ref is not really what one needs as insert takes a strong version of the reference. As we prefer not adding dependencies if we can avoid it, even optional ones, then the solution would be to have a HConsed::to_ref yielding the underlying Arc which would then work thanks to this implementation in the weak_table crate.

Then you could just write

let mut table = <WeakKeyHashMap<Weak<ActualTerm>, u32>>::new();
let one = var(1);
table.insert(one.to_ref(), 1);    // better (?)
assert_eq!(table.get(&one), Some(&1));

Am I making sense, am I missing something? Do you think that would be fine?

[AdrienChampion]

@asvarga @vleni I created #19 to get a sense of the interest in actual weak_table integration, which would be much nicer for you guys

[asvarga]

Thanks for your response, I kept wanting to do

table.insert(one.elm, 1);

but elm is private so HConsed::to_ref would work. I'll comment on #19 as well.

[AdrienChampion]

Sounds good, I'll merge that ASAP, thank you for your feedback 😺