Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-05 18:25:50 -0700 (Sat, 05 Jul 2003)
Revision: 4703
Log message:

      This is partial progress toward abstract vars.  This is a
      branch commit.
      
      I am giving up on this for a moment.  Unfortunately, string
      hacking on variable names is everywhere, not cleanly isolated,
      and not clearly specified.  This makes a port to abstract
      var names either 1) hard, because all this code has to be cleaned
      up, or 2) nonsense, because of the need to covert back and forth
      between strings all the time.
      
      I still think it is a good idea, but it will take a fair amount of
      effort.
      

Changes  Path
+42 -49 metaprl-branches/abstract_vars/OMakefile
+8 -3 metaprl-branches/abstract_vars/editor/ml/nuprl_jprover.ml
+5 -1 metaprl-branches/abstract_vars/filter/OMakefile
+32 -30 metaprl-branches/abstract_vars/filter/base/filter_ocaml.ml
+2 -1 metaprl-branches/abstract_vars/filter/base/filter_ocaml.mli
+7 -4 metaprl-branches/abstract_vars/filter/base/filter_summary.ml
+1 -0 metaprl-branches/abstract_vars/filter/base/filter_summary.mli
+4 -3 metaprl-branches/abstract_vars/filter/base/filter_summary_util.mli
+12 -11 metaprl-branches/abstract_vars/filter/base/filter_type.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_util.ml
+4 -3 metaprl-branches/abstract_vars/filter/base/filter_util.mli
+1 -0 metaprl-branches/abstract_vars/filter/boot/OMakefile
+6 -6 metaprl-branches/abstract_vars/filter/boot/tactic_boot.ml
+14 -15 metaprl-branches/abstract_vars/filter/boot/tactic_boot_sig.mlz
+15 -11 metaprl-branches/abstract_vars/filter/filter/filter_parse.ml
+17 -12 metaprl-branches/abstract_vars/filter/filter/filter_patt.ml
+18 -12 metaprl-branches/abstract_vars/filter/filter/filter_prog.ml
+35 -45 metaprl-branches/abstract_vars/filter/filter/term_grammar.ml
+1 -0 metaprl-branches/abstract_vars/filter/phobos/OMakefile
+9 -9 metaprl-branches/abstract_vars/filter/phobos/phobos_parser.mly
+14 -6 metaprl-branches/abstract_vars/filter/phobos/phobos_rewrite.ml
+3 -0 metaprl-branches/abstract_vars/library/OMakefile
+20 -7 metaprl-branches/abstract_vars/library/db.ml
+22 -21 metaprl-branches/abstract_vars/library/mbterm.ml
+8 -7 metaprl-branches/abstract_vars/library/nuprl5.mli
+0 -10 metaprl-branches/abstract_vars/mllib/string_util.ml
+1 -5 metaprl-branches/abstract_vars/mllib/string_util.mli
+3 -2 metaprl-branches/abstract_vars/refiner/refiner/OMakefile
+15 -15 metaprl-branches/abstract_vars/refiner/refiner/refine.ml
+22 -11 metaprl-branches/abstract_vars/refiner/refiner/refine_error.ml
+3 -2 metaprl-branches/abstract_vars/refiner/reflib/OMakefile
+20 -18 metaprl-branches/abstract_vars/refiner/reflib/ascii_io.ml
+36 -25 metaprl-branches/abstract_vars/refiner/reflib/dform.ml
+24 -1 metaprl-branches/abstract_vars/refiner/reflib/jall.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/match_seq.ml
+17 -8 metaprl-branches/abstract_vars/refiner/reflib/ml_format.ml
+5 -4 metaprl-branches/abstract_vars/refiner/reflib/ml_format_sig.mlz
+16 -11 metaprl-branches/abstract_vars/refiner/reflib/refine_exn.ml
+21 -16 metaprl-branches/abstract_vars/refiner/reflib/simple_print.ml
+2 -1 metaprl-branches/abstract_vars/refiner/reflib/term_match_table.ml
+25 -24 metaprl-branches/abstract_vars/refiner/reflib/unify_mm.ml
+10 -10 metaprl-branches/abstract_vars/refiner/reflib/unify_mm.mli
+3 -2 metaprl-branches/abstract_vars/refiner/refsig/OMakefile
+11 -9 metaprl-branches/abstract_vars/refiner/refsig/refine_error_sig.ml
+10 -10 metaprl-branches/abstract_vars/refiner/refsig/refine_sig.ml
+12 -11 metaprl-branches/abstract_vars/refiner/refsig/rewrite_sig.ml
+6 -6 metaprl-branches/abstract_vars/refiner/refsig/term_addr_sig.ml
+9 -8 metaprl-branches/abstract_vars/refiner/refsig/term_base_sig.ml
+12 -11 metaprl-branches/abstract_vars/refiner/refsig/term_eval_sig.ml
+5 -29 metaprl-branches/abstract_vars/refiner/refsig/term_hash_sig.ml
+8 -8 metaprl-branches/abstract_vars/refiner/refsig/term_man_sig.ml
+4 -3 metaprl-branches/abstract_vars/refiner/refsig/term_meta_sig.ml
+42 -41 metaprl-branches/abstract_vars/refiner/refsig/term_op_sig.ml
+12 -11 metaprl-branches/abstract_vars/refiner/refsig/term_sig.ml
+20 -20 metaprl-branches/abstract_vars/refiner/refsig/term_subst_sig.ml
+3 -2 metaprl-branches/abstract_vars/refiner/rewrite/OMakefile
+25 -22 metaprl-branches/abstract_vars/refiner/rewrite/rewrite.ml
+39 -24 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_build_contractum.ml
+2 -2 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_build_contractum.mli
+5 -4 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_compile_contractum.ml
+3 -2 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_compile_contractum.mli
+10 -9 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_compile_redex.ml
+2 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_compile_redex.mli
+25 -18 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_debug.ml
+40 -30 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_match_redex.ml
+2 -2 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_match_redex.mli
+9 -8 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_meta.ml
+15 -13 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_types.ml
+28 -27 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_util_sig.ml
+2 -2 metaprl-branches/abstract_vars/refiner/term_ds/OMakefile
+4 -5 metaprl-branches/abstract_vars/refiner/term_ds/term_addr_ds.ml
+33 -34 metaprl-branches/abstract_vars/refiner/term_ds/term_base_ds.ml
+15 -15 metaprl-branches/abstract_vars/refiner/term_ds/term_ds.ml
+27 -27 metaprl-branches/abstract_vars/refiner/term_ds/term_ds_sig.ml
+6 -6 metaprl-branches/abstract_vars/refiner/term_ds/term_eval_ds.ml
+7 -7 metaprl-branches/abstract_vars/refiner/term_ds/term_man_ds.ml
+5 -5 metaprl-branches/abstract_vars/refiner/term_ds/term_op_ds.ml
+45 -44 metaprl-branches/abstract_vars/refiner/term_ds/term_subst_ds.ml
+3 -2 metaprl-branches/abstract_vars/refiner/term_gen/OMakefile
+3 -5 metaprl-branches/abstract_vars/refiner/term_gen/term_addr_gen.ml
+9 -8 metaprl-branches/abstract_vars/refiner/term_gen/term_hash.ml
+15 -15 metaprl-branches/abstract_vars/refiner/term_gen/term_man_gen.ml
+2 -2 metaprl-branches/abstract_vars/refiner/term_std/OMakefile
+5 -4 metaprl-branches/abstract_vars/refiner/term_std/term_eval_std.ml
+12 -11 metaprl-branches/abstract_vars/refiner/term_std/term_std.ml
+20 -19 metaprl-branches/abstract_vars/refiner/term_std/term_std_sig.ml
+17 -16 metaprl-branches/abstract_vars/refiner/term_std/term_subst_std.ml
+5 -4 metaprl-branches/abstract_vars/support/display/perv.mli
+6 -10 metaprl-branches/abstract_vars/support/tactics/simp_typeinf.ml
+3 -3 metaprl-branches/abstract_vars/support/tactics/simp_typeinf.mli
+8 -7 metaprl-branches/abstract_vars/support/tactics/tactic_cache.ml
+3 -2 metaprl-branches/abstract_vars/support/tactics/tactic_cache.mli
+9 -9 metaprl-branches/abstract_vars/support/tactics/typeinf.ml
+5 -5 metaprl-branches/abstract_vars/support/tactics/typeinf.mli
+15 -20 metaprl-branches/abstract_vars/support/tactics/var.ml
+5 -4 metaprl-branches/abstract_vars/support/tactics/var.mli