Crate hashconsing [−] [src]
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 HashMap
s, 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.
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) ; }
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 |
Traits
HConser |
HConsed element creation. |