notes/HashConsing.txt

   1 Notes on hash consing:
   2
   3 Hash consing can be specified for algebraic datatypes using
   4 the ``unique'' qualifier.  For example:
   5
   6    datatype EXP :: unique = num (int)
   7                           | add (EXP, EXP)
   8                           | sub (EXP, EXP)
   9                           | mul (EXP, EXP)
  10                           | div (EXP, EXP)
  11                           ;
  12
  13
  14 defines an algebraic datatype EXP that is hash consed.  This basically
  15 means that if (and only if) two terms ``e1'' and ``e2'' built with EXP's
  16 constructors are structurally identical, then ``e1 == e2.''  This makes
  17 it possible to implement things like value numbering and the like very
  18 easily.
  19
  20 The current version of Prop (rel 2.0) implements this feature by keeping
  21 a hash table of all existing consed cells for each given hash consed datatype.
  22 To instantiate this hash table, there must be declaration
  23
  24    instantiate datatype EXP;
  25
  26 in some implementation module.  (In general, for future compatibility, it is
  27 a good idea to have instantiate datatype declaration for each datatype used.)
  28
  29 All hash consed datatypes are immutable, and cannot be overwritten.
  30 I.e. it is as if the qualifier ``const'' has been implicitly added.
  31
  32    datatype EXP :: const unique = ...