Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-19 22:10:54 -0800 (Wed, 19 Nov 2003)
Revision: 5116
Log message:

      Improvement of global GC strategy (though it will probably be replaced with generational GC). Now it's not really global but sticks to mutually recursive memos only.
      I tried different values of threshold in weak_memo.ml but recompilation of metaprl for different values didn't show any substantial difference in compilation time (basically for two settings - often and never).
      

Changes  Path
+1 -0 metaprl/mllib/hash_with_gc.ml
+1 -0 metaprl/mllib/hash_with_gc_sig.ml
+1 -1 metaprl/mllib/memo.ml
+0 -1 metaprl/mllib/memo_sig.ml
+133 -86 metaprl/mllib/weak_memo.ml
+10 -2 metaprl/mllib/weak_memo.mli
+12 -4 metaprl/mllib/weak_memo_sig.ml
+20 -10 metaprl/refiner/reflib/term_copy2_weak.ml
+2 -1 metaprl/refiner/reflib/term_copy2_weak.mli
+4 -3 metaprl/refiner/refsig/term_hash_sig.ml
+14 -13 metaprl/refiner/term_gen/term_hash.ml
+12 -12 metaprl/tactics/proof/proof_term_boot.ml