Crate hashconsing[−][src]
Hash consing library.
This library is based on Type-Safe Modular Hash-Consing by Filiâtre
and Conchon. It is probably less efficient as uses Rust's HashMap
s, not a
custom built structure.
If you are not familiar with hashconsing, see the example below or read the paper.
Provides constant time comparison and perfect (maximal) sharing assuming only one consign/factory 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.
Hashconsing consists in wrapping some tree-like datatype in an immutable
container, which in the case of hashconsing
is HConsed
. In this example
we'll call the tree-like datatype ActualTerm
and the hashconsed version
Term
.
A Term
is created from an ActualTerm
by a factory, which hashconsing
calls a consign (see HConsign
). The functions for doing so are in the
HashConsign
trait. The idea is that the consign is a map from actual terms
to Arc
s of hashconsed terms. When given an actual term, the consign checks
whether there's already a hashconsed term for it. If not, then it creates one,
memorizes it and returns that. Otherwise it clones the existing one. Hence
subterm sharing is maximal/perfect.
A HConsed<T>
is exactly two things: a unique identifier uid
and an Arc
to
the real term it represents. (Hence, cloning a hashconsed term is cheap.) This
library guarantees that two hashconsed terms refer to structurally identical
real terms iff their uid
s are equal. Hence, equality checking is constant
time.
extern crate hashconsing ; use hashconsing::{ HConsed, HashConsign, HConsign } ; type Term = HConsed<ActualTerm> ; #[derive(Debug, Hash, Clone, PartialEq, Eq)] enum ActualTerm { Var(usize), Lam(Term), App(Term, Term) } use self::ActualTerm::* ; fn main() { let mut factory: HConsign<ActualTerm> = HConsign::empty() ; assert_eq! { factory.len(), 0 } let v = factory.mk( Var(0) ) ; assert_eq! { factory.len(), 1 } let v2 = factory.mk( Var(3) ) ; assert_eq! { factory.len(), 2 } let lam = factory.mk( Lam( v2.clone() ) ) ; assert_eq! { factory.len(), 3 } let v3 = factory.mk( Var(3) ) ; // v2 is the same as v3: Var(3). Consign has not created anything new, and // v2 and v3 are conceptually the same term. assert_eq! { factory.len(), 3 } assert_eq! { v2.uid(), v3.uid() } assert_eq! { v2.get(), v3.get() } assert_eq! { v2, v3 } let lam2 = factory.mk( Lam(v3) ) ; // Not new either. assert_eq! { factory.len(), 3 } assert_eq! { lam.uid(), lam2.uid() } assert_eq! { lam.get(), lam2.get() } assert_eq! { lam, lam2 } let app = factory.mk( App(lam2, v) ) ; assert_eq! { factory.len(), 4 } }
This library maintains the invariant stated above as long as you never create two consigns for the same type.
Users are free to use the consign however they see fit: one can create a
factory directly as in the example above, but passing it around everywhere it's
needed is tedious. The author recommends the following workflow instead. It
relies on the new_consign
macro which creates a lazy static factory
protected by a RwLock
for thread-safety. The consign and the constructors are
wrapped in an appropriately named module. The consign is invisible and creating
terms is easy.
extern crate hashconsing ; pub mod term { use hashconsing::* ; pub type Term = HConsed<ActualTerm> ; #[derive(Debug, Hash, Clone, PartialEq, Eq)] pub enum ActualTerm { Var(usize), Lam(Term), App(Term, Term) } new_consign! { /// Factory for terms. let factory = consign(37) for ActualTerm ; } pub fn var(v: usize) -> Term { factory.mk( ActualTerm::Var(v) ) } pub fn lam(t: Term) -> Term { factory.mk( ActualTerm::Lam(t) ) } pub fn app(t_1: Term, t_2: Term) -> Term { factory.mk( ActualTerm::App(t_1, t_2) ) } } fn main() { let v = term::var(0) ; let v2 = term::var(3) ; let lam = term::lam(v2) ; let v3 = term::var(3) ; let lam2 = term::lam(v3) ; let app = term::app(lam2, v) ; }
Note that HConsed<T>
Deref
s to T
, so you don't need to extend
HConsed<T>
using some trait to add the functions you need. Just implement
them for T
. Functions taking an & mut self
won't work since HConsed<T>
gives you access to T
through an Arc
.
impl ::std::fmt::Display for ActualTerm { fn fmt(& self, fmt: & mut ::std::fmt::Formatter) -> ::std::fmt::Result { match self { ActualTerm::Var(i) => write!(fmt, "v{}", i), ActualTerm::Lam(t) => write!(fmt, "({})", t.get()), ActualTerm::App(u, v) => write!( fmt, "{}.{}", u.get(), v.get() ), } } } fn main() { let v = term::var(0) ; let v3 = term::var(3) ; let lam2 = term::lam(v3) ; let app = term::app(lam2, v) ; assert_eq! { & format!("{}", app), "(v3).v0" } }
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.
Another way to have efficient sets/maps of/from hashconsed things is to use the
BTree
sets and maps from the standard library.
Re-exports
pub use lazy_static::*; |
Modules
coll |
Efficient collections for hashconsed data. |
Macros
lazy_static | |
new_consign |
Creates a lazy static consign. |
Structs
HConsed |
Stores a hash consed element and its hash in order to avoid recomputing it every time. |
HConsign |
The consign storing the actual hash consed elements as |
Traits
HashConsed |
Internal trait used to recognize hashconsed things. |
HashConsign |
HConsed element creation. |