-
Notifications
You must be signed in to change notification settings - Fork 6
/
lib.rs
722 lines (675 loc) · 21.6 KB
/
lib.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
// 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 ;
) => (
$crate::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))
}
}
}