Crate hashconsing

Hash consing library.

It is a based on Type-Safe Modular Hash-Consing by Filiâtre and Conchon. It is slightly less efficient as uses Rust's HashMaps, not a custom built structure.

Provides constant time comparison and perfect (maximal) sharing assuming only one HashConsign is created for a given type. This assumption must never be falsified unless you really, really know what you are doing.

Hash consed elements are immutable and therefore thread-safe: HConsed implements Send and Sync.

The consign actually stores weak references to values. This ensures that values are dropped once they are not used anymore.

Collections with trivial hash function

This library provides two special collections: HConSet and HConMap. They use the trivial hash function over hashconsed values' unique identifier. Read more.

Example

Simple example for lambda calculus from the paper.

extern crate hashconsing ;

use std::fmt ;
use ::hashconsing::* ;


use self::ActualTerm::* ;

type Term = HConsed<ActualTerm> ;

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


impl fmt::Display for ActualTerm {
  fn fmt(& self, fmt: & mut fmt::Formatter) -> fmt::Result {
    match self {
      & Var(i) => write!(fmt, "v{}", i),
      & Lam(ref t) => write!(fmt, "({})", t.get()),
      & App(ref u, ref v) => write!(fmt, "{}.{}", u.get(), v.get()),
    }
  }
}

trait TermFactory {
  fn var(& mut self, v: usize) -> Term ;
  fn lam(& mut self, t: Term) -> Term ;
  fn app(& mut self, u: Term, v: Term) -> Term ;
}


impl TermFactory for HashConsign<ActualTerm> {
  fn var(& mut self, v: usize) -> Term { self.mk( Var(v) ) }
  fn lam(& mut self, t: Term) -> Term { self.mk( Lam(t) ) }
  fn app(& mut self, u: Term, v: Term) -> Term {
    self.mk( App(u, v) )
  }
}

pub fn main() {
  let mut consign = HashConsign::empty() ;
  assert_eq!(consign.len(), 0) ;

  let v = consign.var(0) ;
  assert_eq!(consign.len(), 1) ;

  let v2 = consign.var(3) ;
  assert_eq!(consign.len(), 2) ;

  let lam = consign.lam(v2) ;
  assert_eq!(consign.len(), 3) ;

  let v3 = consign.var(3) ;
  assert_eq!(consign.len(), 3) ;

  let lam2 = consign.lam(v3) ;
  assert_eq!(consign.len(), 3) ;

  let app = consign.app(lam2, v) ;
  assert_eq!(consign.len(), 4) ;
}

Modules

coll	Efficient collections for hashconsed data.

Structs

HConsed	Stores a hash consed element and its hash in order to avoid recomputing it every time.
HashConsign	The consign storing the actual hash consed elements as HConseds.

Traits

HConser	HConsed element creation.
HashConsed	Internal trait used to recognize hashconsed things.