Crate hashconsing [−] [src]

Hash consing library. Ideally we'd like to use weak references in the consign but they're currently feature gated. Waiting for dust to settle.

Module sync contains a thread-safe version.

See the paper by Filiâtre and Conchon.

Example

Simple example for lambda calculus.

#[macro_use]
extern crate hashconsing as hc ;

use std::rc::Rc ;
use std::fmt ;
use hc::* ;


use ::ActualTerm::* ;

hash_cons!{pub Term for ActualTerm}

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

impl PartialEq for ActualTerm {
  fn eq(& self, rhs: & Self) -> bool {
    match (self, rhs) {
      (& Var(i), & Var(j)) =>
        i == j,
      (& Lam(ref t1), & Lam(ref t2)) =>
        t1.hkey() == t2.hkey(),
      (& App(ref u1, ref v1), & App(ref u2, ref v2)) =>
        u1.hkey() == u2.hkey() && v1.hkey() == v2.hkey(),
      _ => false
    }
  }
}
impl Eq for ActualTerm {}


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) )
  }
}


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

sync	Thread safe version of the hash consed library. The consign is wrapped in a mutex. The main difference for users is that hash cons operations now take a `& self` and note a `& mut self`.

Macros

hash_cons!	Creates a hash consed type for some type.
hc_match!	Convenience macro to match hash consed things.
sync_hash_cons!	Creates a thread safe hash consed type for some type.

Structs

HashConsed	Stores a hash consed element and its hash in order to avoid recomputing it every time. A (synced) consign stores stores `Rc`s (`Arc`s) of that type for (thread-safe) sharing.
HashConsign	The consign storing the actual hash consed elements as `Rc`s.

Traits

Hash	A hashable type.
Hasher	A trait which represents the ability to hash an arbitrary stream of bytes.

Type Definitions

HConsed

Actual type stored and returned by the consign.