// See the LICENSE files at the top-level directory of this distribution.
//
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
// option. This file may not be copied, modified, or distributed
// except according to those terms.

//! Hash consing library.
//!
//! This library is based on [Type-Safe Modular Hash-Consing](paper) 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](#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][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.
//!
//! ```rust
//! 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 [`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.
//!
//! ```rust
//! #[macro_use]
//! extern crate hashconsing ;
//!
//! pub mod term {
//!     use hashconsing::{ HConsed, HashConsign } ;
//!     pub type Term = HConsed<ActualTerm> ;
//!     #[derive(Debug, Hash, Clone, PartialEq, Eq)]
//!     pub enum ActualTerm {
//!         Var(usize),
//!         Lam(Term),
//!         App(Term, Term)
//!     }
//!
//!     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`.
//!
//! ```rust
//! # 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)
//! #     }
//! #
//! #     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) )
//! #     }
//! 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.][coll mod]
//!
//! Another way to have efficient sets/maps of/from hashconsed things is to use the `BTree` sets
//! and maps from the standard library.
//!
//! [paper]: http://dl.acm.org/citation.cfm?doid=1159876.1159880
//! (Type-safe modular hash-consing)
//! [`HConsed`]: trait.HashConsed.html (HConsed type)
//! [`HConSet`]: coll/struct.HConSet.html (HConSet documentation)
//! [`HConMap`]: coll/struct.HConMap.html (HConMap documentation)
//! [`HashConsign` trait]: trait.HashConsign.html (HashConsign trait)
//! [`HConsign`]: struct.HConsign.html (HConsign type)
//! [`consign`]: macro.consign.html (consign macro)
//! [coll mod]: coll/index.html (coll module documentation)
//! [lazy static]: https://crates.io/crates/lazy_static
//! (lazy_static library on crates.io)

use std::cmp::{Eq, Ord, Ordering, PartialEq, PartialOrd};
use std::collections::HashMap;
use std::fmt;
use std::hash::{Hash, Hasher};
use std::marker::{Send, Sync};
use std::ops::Deref;
use std::sync::{Arc, RwLock, Weak};

pub use lazy_static::*;

/// Creates a lazy static consign.
///
/// The consign is protected by a `RwLock`.
///
/// Arguments:
/// - `$(#[$meta:meta])*` meta stuff, typically comments ;
/// - `$name:ident` name of the consign ;
/// - `$capa:expr` initial capacity when creating the consign ;
/// - `$typ:typ,` type being hashconsed (the underlying type, not the
///     hashconsed one) ;
#[macro_export]
macro_rules! consign {
    (
        $(#[$meta:meta])*
        let $name:ident = consign($capa:expr) for $typ:ty ;
    ) => (
        lazy_static! {
            $(#[$meta])*
            static ref $name: ::std::sync::RwLock<
                $crate::HConsign<$typ>
            > = ::std::sync::RwLock::new(
                $crate::HConsign::with_capacity( $capa )
            );
        }
    );
}

pub mod coll;

/// Internal trait used to recognize hashconsed things.
///
/// The only purpose of this trait (currently) is to simplify the type
/// signature of the collections of hashconsed things.
pub trait HashConsed {
    /// Elements stored inside a hashconsed value.
    type Inner;
}

/// Stores a hash consed element and its hash in order to avoid recomputing it
/// every time.
pub struct HConsed<T> {
    /// The actual element.
    elm: Arc<T>,
    /// Unique identifier of the element.
    uid: u64,
}
impl<T> HashConsed for HConsed<T> {
    type Inner = T;
}

impl<T> HConsed<T> {
    /// The inner element. Can also be accessed *via* dereferencing.
    #[inline]
    pub fn get(&self) -> &T {
        self.elm.deref()
    }
    /// The unique identifier of the element.
    #[inline]
    pub fn uid(&self) -> u64 {
        self.uid
    }
    /// Turns a hashconsed thing in a weak hashconsed thing.
    #[inline]
    fn to_weak(&self) -> WHConsed<T> {
        WHConsed {
            elm: Arc::downgrade(&self.elm),
            uid: self.uid,
        }
    }

    /// Number of (strong) references to this term.
    pub fn arc_count(&self) -> usize {
        Arc::strong_count(&self.elm)
    }
}

impl<T: fmt::Debug> fmt::Debug for HConsed<T> {
    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
        write!(fmt, "{:?}", self.elm)
    }
}

impl<T> Clone for HConsed<T> {
    fn clone(&self) -> Self {
        HConsed {
            elm: self.elm.clone(),
            uid: self.uid,
        }
    }
}

impl<T> PartialEq for HConsed<T> {
    #[inline]
    fn eq(&self, rhs: &Self) -> bool {
        self.uid == rhs.uid
    }
}
impl<T> Eq for HConsed<T> {}
impl<T> PartialOrd for HConsed<T> {
    #[inline]
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        self.uid.partial_cmp(&other.uid)
    }
}
impl<T> Ord for HConsed<T> {
    #[inline]
    fn cmp(&self, other: &Self) -> Ordering {
        self.uid.cmp(&other.uid)
    }
}
impl<T: Hash> Hash for HConsed<T> {
    #[inline]
    fn hash<H>(&self, state: &mut H)
    where
        H: Hasher,
    {
        self.uid.hash(state)
    }
}

impl<T> Deref for HConsed<T> {
    type Target = T;
    #[inline]
    fn deref(&self) -> &T {
        self.elm.deref()
    }
}

unsafe impl<T> Sync for HConsed<T> {}
unsafe impl<T> Send for HConsed<T> {}

impl<T: fmt::Display> fmt::Display for HConsed<T> {
    #[inline]
    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
        self.elm.fmt(fmt)
    }
}

/// Weak version of `HConsed` (internal).
struct WHConsed<T> {
    /// The actual element.
    elm: Weak<T>,
    /// Unique identifier of the element.
    uid: u64,
}
impl<T> WHConsed<T> {
    /// Turns a weak hashconsed thing in a hashconsed thing.
    pub fn to_hconsed(&self) -> Option<HConsed<T>> {
        if let Some(arc) = self.elm.upgrade() {
            Some(HConsed {
                elm: arc,
                uid: self.uid,
            })
        } else {
            None
        }
    }
}

impl<T: fmt::Display> fmt::Display for WHConsed<T> {
    #[inline]
    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
        if let Some(arc) = self.elm.upgrade() {
            arc.fmt(fmt)
        } else {
            write!(fmt, "<freed>")
        }
    }
}

impl<T> Hash for WHConsed<T> {
    #[inline]
    fn hash<H>(&self, state: &mut H)
    where
        H: Hasher,
    {
        self.uid.hash(state)
    }
}

impl<T> PartialEq for WHConsed<T> {
    #[inline]
    fn eq(&self, rhs: &Self) -> bool {
        self.uid == rhs.uid
    }
}
impl<T> Eq for WHConsed<T> {}
impl<T> PartialOrd for WHConsed<T> {
    #[inline]
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        self.uid.partial_cmp(&other.uid)
    }
}
impl<T> Ord for WHConsed<T> {
    #[inline]
    fn cmp(&self, other: &Self) -> Ordering {
        self.uid.cmp(&other.uid)
    }
}

/// The consign storing the actual hash consed elements as `HConsed`s.
pub struct HConsign<T: Hash + Eq + Clone> {
    /// The actual hash consing table.
    table: HashMap<T, WHConsed<T>>,
    /// Counter for uids.
    count: u64,
}

impl<T: Hash + Eq + Clone> HConsign<T> {
    /// Creates an empty consign.
    #[inline]
    pub fn empty() -> Self {
        HConsign {
            table: HashMap::new(),
            count: 0,
        }
    }

    /// Creates an empty consign with a capacity.
    #[inline]
    pub fn with_capacity(capacity: usize) -> Self {
        HConsign {
            table: HashMap::with_capacity(capacity),
            count: 0,
        }
    }

    /// Fold on the elements stored in the consign.
    #[inline]
    pub fn fold<Acc, F>(&self, mut init: Acc, mut f: F) -> Acc
    where
        F: FnMut(Acc, HConsed<T>) -> Acc,
    {
        for weak in self.table.values() {
            if let Some(consed) = weak.to_hconsed() {
                init = f(init, consed)
            }
        }
        init
    }

    /// Fold on the elements stored in the consign, result version.
    #[inline]
    pub fn fold_res<Acc, F, E>(&self, mut init: Acc, mut f: F) -> Result<Acc, E>
    where
        F: FnMut(Acc, HConsed<T>) -> Result<Acc, E>,
    {
        for weak in self.table.values() {
            if let Some(consed) = weak.to_hconsed() {
                init = f(init, consed)?
            }
        }
        Ok(init)
    }

    /// The number of elements stored, mostly for testing.
    #[inline]
    pub fn len(&self) -> usize {
        self.table.len()
    }
    /// True if the consign is empty.
    #[inline]
    pub fn is_empty(&self) -> bool {
        self.table.is_empty()
    }

    /// Inserts in the consign.
    ///
    /// One of the following must hold:
    ///
    /// - `self.table` is not defined at `key`
    /// - the weak ref in `self.table` at `key` returns `None` when upgraded.
    ///
    /// This is checked in `debug` but not `release`.
    #[inline]
    fn insert(&mut self, key: T, wconsed: WHConsed<T>) {
        let prev = self.table.insert(key, wconsed);
        debug_assert!(match prev {
            None => true,
            Some(prev) => prev.to_hconsed().is_none(),
        })
    }

    /// Attempts to retrieve an *upgradable* value from the map.
    #[inline]
    fn get(&self, key: &T) -> Option<HConsed<T>> {
        if let Some(old) = self.table.get(key) {
            old.to_hconsed()
        } else {
            None
        }
    }
}

impl<T: Hash + Eq + Clone> fmt::Display for HConsign<T>
where
    T: Hash + fmt::Display,
{
    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
        write!(fmt, "consign:")?;
        for e in self.table.values() {
            write!(fmt, "\n  | {}", e)?;
        }
        Ok(())
    }
}

/// HConsed element creation.
///
/// Implemented *via* a trait to be able to extend `RwLock` for lazy static
/// consigns.
pub trait HashConsign<T: Hash>: Sized {
    /// Hashconses something and returns the hash consed version.
    ///
    /// Returns `true` iff the element
    ///
    /// - was not in the consign at all, or
    /// - was in the consign but it is not referenced (weak ref cannot be
    ///   upgraded.)
    fn mk_is_new(self, elm: T) -> (HConsed<T>, bool);
    /// Creates a HConsed element.
    fn mk(self, elm: T) -> HConsed<T> {
        self.mk_is_new(elm).0
    }
}
impl<'a, T: Hash + Eq + Clone> HashConsign<T> for &'a mut HConsign<T> {
    /// Hash conses something and returns the hash consed version.
    fn mk_is_new(self, elm: T) -> (HConsed<T>, bool) {
        // If the element is known and upgradable return it.
        if let Some(hconsed) = self.get(&elm) {
            debug_assert!(*hconsed.elm == elm);
            return (hconsed.clone(), false);
        }
        // Otherwise build hconsed version.
        let hconsed = HConsed {
            elm: Arc::new(elm.clone()),
            uid: self.count,
        };
        // Increment uid count.
        self.count += 1;
        // ...add weak version to the table...
        self.insert(elm, hconsed.to_weak());
        // ...and return consed version.
        (hconsed, true)
    }
}
impl<'a, T: Hash + Eq + Clone> HashConsign<T> for &'a RwLock<HConsign<T>> {
    /// If the element is already in the consign, only read access will be
    /// requested.
    fn mk_is_new(self, elm: T) -> (HConsed<T>, bool) {
        // Request read and check if element already exists.
        {
            let slf = self.read().unwrap();
            // If the element is known and upgradable return it.
            if let Some(hconsed) = slf.get(&elm) {
                debug_assert!(*hconsed.elm == elm);
                return (hconsed, false);
            }
        };
        // Otherwise get mutable `self`.
        let mut slf = self.write().unwrap();

        // Someone might have inserted since we checked, check again.
        if let Some(hconsed) = slf.get(&elm) {
            debug_assert!(*hconsed.elm == elm);
            return (hconsed, false);
        }

        // Otherwise build hconsed version.
        let hconsed = HConsed {
            elm: Arc::new(elm.clone()),
            uid: slf.count,
        };
        // Increment uid count.
        slf.count += 1;
        // ...add weak version to the table...
        slf.insert(elm, hconsed.to_weak());
        // ...and return consed version.
        (hconsed, true)
    }
}

#[cfg(test)]
mod example {

    use crate::coll::*;
    use crate::example::ActualTerm::*;
    use crate::*;
    use std::fmt;

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

    #[test]
    fn run() {
        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.var(0), "v1");
        println!("creating {}", 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);

        let (v2, v2_name) = (consign.var(3), "v2");
        println!("creating {}", v2);
        assert_eq!(consign.len(), 2);
        assert_ne!(v1.uid(), v2.uid());
        let prev = map.insert(v2.clone(), v2_name);
        assert_eq!(prev, None);
        let is_new = set.insert(v2.clone());
        assert!(is_new);

        let (lam, lam_name) = (consign.lam(v2.clone()), "lam");
        println!("creating {}", lam);
        assert_eq!(consign.len(), 3);
        assert_ne!(v1.uid(), lam.uid());
        assert_ne!(v2.uid(), lam.uid());
        let prev = map.insert(lam.clone(), lam_name);
        assert_eq!(prev, None);
        let is_new = set.insert(lam.clone());
        assert!(is_new);

        let (v3, v3_name) = (consign.var(3), "v3");
        println!("creating {}", v3);
        assert_eq!(consign.len(), 3);
        assert_eq!(v2.uid(), v3.uid());
        let prev = map.insert(v3.clone(), v3_name);
        assert_eq!(prev, Some(v2_name));
        let is_new = set.insert(v3.clone());
        assert!(!is_new);

        let (lam2, lam2_name) = (consign.lam(v3.clone()), "lam2");
        println!("creating {}", lam2);
        assert_eq!(consign.len(), 3);
        assert_eq!(lam.uid(), lam2.uid());
        let prev = map.insert(lam2.clone(), lam2_name);
        assert_eq!(prev, Some(lam_name));
        let is_new = set.insert(lam2.clone());
        assert!(!is_new);

        let (app, app_name) = (consign.app(lam2, v1), "app");
        println!("creating {}", app);
        assert_eq!(consign.len(), 4);
        let prev = map.insert(app.clone(), app_name);
        assert_eq!(prev, None);
        let is_new = set.insert(app.clone());
        assert!(is_new);

        for term in &set {
            assert!(map.contains_key(term))
        }
        for (term, val) in &map {
            println!("looking for `{}`", val);
            assert!(set.contains(term))
        }
    }
}