Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-24 19:12:01 -0700 (Mon, 24 May 1999)
Revision: 2671
Log message:

      OK, here is the updated code for the weak-pointers based Term_copy modules
      
      The changes include:
      1) I added the new garbage collecting mechanism written by Yegor.
      2) Parameters are now hashed as a whole instead of recursively weak-hashing them.
      3) I merged the TermHeader module into the TermHash module which allowed me to keep
         most TermHash types abstract.
      4) I cleaned up the code a little.
      
      Yegor, can you run some test on this code and see if there is any evidence that we
      still have the bug? Thanks!
      

Changes  Path
Properties metaprl/mllib
+3 -3 metaprl/mllib/Makefile
Added metaprl/mllib/hash_with_gc.ml
Properties metaprl/mllib/hash_with_gc.ml
Added metaprl/mllib/hash_with_gc.mli
Properties metaprl/mllib/hash_with_gc.mli
Added metaprl/mllib/hash_with_gc_sig.ml
Properties metaprl/mllib/hash_with_gc_sig.ml
Deleted metaprl/mllib/infinite_weak_array.ml
Deleted metaprl/mllib/infinite_weak_array.mli
Deleted metaprl/mllib/infinite_weak_array_sig.mlz
+102 -45 metaprl/mllib/weak_memo.ml
+2 -4 metaprl/mllib/weak_memo.mli
+11 -4 metaprl/mllib/weak_memo_sig.ml
+3 -3 metaprl/refiner/refiner/refiner_ds.ml
+3 -3 metaprl/refiner/refiner/refiner_std.ml
+23 -9 metaprl/refiner/reflib/term_copy2_weak.ml
+1 -2 metaprl/refiner/reflib/term_copy2_weak.mli
+1 -2 metaprl/refiner/reflib/term_copy_weak.ml
+0 -1 metaprl/refiner/reflib/term_copy_weak.mli
+1 -1 metaprl/refiner/refsig/Files
+2 -14 metaprl/refiner/refsig/refiner_sig.ml
+30 -26 metaprl/refiner/refsig/term_hash_sig.ml
Deleted metaprl/refiner/refsig/term_header_sig.mlz
+0 -1 metaprl/refiner/refsig/term_norm_sig.ml
+5 -14 metaprl/refiner/refsig/termmod_hash_sig.ml
+4 -1 metaprl/refiner/refsig/termmod_sig.ml
Added metaprl/refiner/refsig/tm_subst_sig.mlz
Properties metaprl/refiner/refsig/tm_subst_sig.mlz
+0 -1 metaprl/refiner/term_gen/Files
+173 -99 metaprl/refiner/term_gen/term_hash.ml
+2 -15 metaprl/refiner/term_gen/term_hash.mli
Deleted metaprl/refiner/term_gen/term_header.ml
Deleted metaprl/refiner/term_gen/term_header.mli
+60 -81 metaprl/refiner/term_gen/term_header_constr.ml
+4 -17 metaprl/refiner/term_gen/term_header_constr.mli
+3 -14 metaprl/refiner/term_gen/term_norm.ml
+2 -13 metaprl/refiner/term_gen/term_norm.mli