Module hashconsing::coll

Efficient collections for hashconsed data.

This module provide hash set and hash map types with trivial hash functions for hashconsed types. The hash of an hashconsed value is its unique identifier, verbatim. This is obviously extremely dangerous from a security point of view: these collections should never be used for cryptographic purposes.

Note that you can use BTreeMap and BTreeSet on hashconsed types since they are totally ordered.

Usage

TL;DR You need to specify the hashconsed type when creating one of the collections in this module.

There is a bit of internal gymnastic so that the type signatures of these collections are natural. If Term is the hashconsed version of RTerm, then you want the type of the sets to be the natural one, e.g. HConSet<Term>.

However, since Term is really an alias for HConsed<RTerm>, then if we wanted to declare HConSet as an alias for HashSet we would get type HConSet<Inner> = HashSet< HConsed<Inner> > (omitting the custom hasher). That is, our sets would have type HConSet<RTerm>, which is not very pretty. We could just define an alias though: type TermSet = HConSet<RTerm>, but it turns out it's better to wrap the actual set in a struct anyway. Mostly to be able to define new and with_capacity without relying on a trait (users would need to import) to do that.

So actually HConsed types automatically implement the internal trait HashConsed { type Inner ; }. The sole purpose of this trait (currently) is to pass the inner type implicitly thanks to a T: HashConsed bound. Rust's type inference does not seem to really like this, and struggles a bit to infer the types at play. In practice, it means that you need to specify the type of the hashconsed elements in your set/map.

use hashconsing::* ;
use hashconsing::coll::* ;

#[derive(Hash, Clone, PartialEq, Eq)]
enum ActualTerm {
  Var(usize),
  Lam(Term),
  App(Term, Term)
}
type Term = HConsed<ActualTerm> ;

let mut consign = HConsign::empty() ;
assert_eq!(consign.len(), 0) ;

let mut map: HConMap<Term,_> = HConMap::with_capacity(100) ;
let mut set: HConSet<Term> = HConSet::with_capacity(100) ;

let (v1, v1_name) = (
  consign.mk( ActualTerm::Var(0) ), "v1"
) ;
assert_eq!(consign.len(), 1) ;
let prev = map.insert(v1.clone(), v1_name) ;
assert_eq!( prev, None ) ;
let is_new = set.insert(v1.clone()) ;
assert!( is_new ) ;

The problem completely goes away if you redefine your set/map type, and is the recommended way of using these collections.

use hashconsing::* ;
use hashconsing::coll::* ;

#[derive(Hash, Clone, PartialEq, Eq)]
enum ActualTerm {
  Var(usize),
  Lam(Term),
  App(Term, Term)
}
type Term = HConsed<ActualTerm> ;
type TermMap<T> = HConMap<Term, T> ;
type TermSet = HConSet<Term> ;

let mut consign = HConsign::empty() ;
assert_eq!(consign.len(), 0) ;

let mut map = TermMap::with_capacity(100) ;
let mut set = TermSet::with_capacity(100) ;

let (v1, v1_name) = (
  consign.mk( ActualTerm::Var(0) ), "v1"
) ;
assert_eq!(consign.len(), 1) ;
let prev = map.insert(v1.clone(), v1_name) ;
assert_eq!( prev, None ) ;
let is_new = set.insert(v1.clone()) ;
assert!( is_new ) ;

Structs

HConMap	A hash map of hash-consed things with trivial hashing.
HConSet	A hash set of hash-consed things with trivial hashing.