Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-02-12 15:50:37 -0800 (Fri, 12 Feb 1999)
Revision: 2590
Log message:

      Added the Linear_set implementation based on arrays (the same as was used
      before). Somehow it still made things a little bit faster, I have no idea why.
      
      Added the new compile-time option into mk/config file that allows to choose
      which Linear_set implementation to use. All relevant comments will be added
      to your mk/config file automatically when you ran make for the first time
      after "cvs update"
      

Changes  Path
+9 -5 metaprl/Makefile
Deleted metaprl/mk/config.init
Added metaprl/mk/make_config.sh
Properties metaprl/mk/make_config.sh
+4 -1 metaprl/mk/preface
+0 -2 metaprl/mk/rules
+2 -0 metaprl/mllib/Makefile
Added metaprl/mllib/array_linear_set.ml
Properties metaprl/mllib/array_linear_set.ml
Added metaprl/mllib/array_linear_set.mli
Properties metaprl/mllib/array_linear_set.mli
+16 -0 metaprl/mllib/array_util.ml
+1 -0 metaprl/mllib/array_util.mli
Deleted metaprl/mllib/linear_set.ml
Deleted metaprl/mllib/linear_set.mli
Added metaprl/mllib/linear_set.mlz
Properties metaprl/mllib/linear_set.mlz
Added metaprl/mllib/splay_linear_set.ml
Properties metaprl/mllib/splay_linear_set.ml
Added metaprl/mllib/splay_linear_set.mli
Properties metaprl/mllib/splay_linear_set.mli
+3 -20 metaprl/refiner/refsig/term_base_sig.ml
+9 -19 metaprl/refiner/refsig/tm_base_sig.mlz
+1 -1 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+9 -9 metaprl/refiner/term_ds/term_addr_ds.ml
+14 -57 metaprl/refiner/term_ds/term_base_ds.ml
+2 -2 metaprl/refiner/term_ds/term_ds.ml
+4 -4 metaprl/refiner/term_ds/term_ds_sig.ml
+8 -7 metaprl/refiner/term_ds/term_man_ds.ml
+1 -0 metaprl/refiner/term_ds/term_man_ds.mli
+6 -5 metaprl/refiner/term_ds/term_subst_ds.ml
+1 -0 metaprl/refiner/term_ds/term_subst_ds.mli
+6 -32 metaprl/refiner/term_std/term_base_std.ml
+4 -4 metaprl/refiner/term_std/term_std.ml
+4 -4 metaprl/refiner/term_std/term_std_sig.ml