Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-18 18:59:07 -0800 (Tue, 18 Jan 2005)
Revision: 6437
Log message:

      1. Added some cases to refine_error.
      2. Added Term_subst_sig.so_vars, to compute non-zero arity so-vars.
      3. Opname type checking now works at least minimally.
      

Changes  Path
+2 -1 metaprl-branches/opname_classes/filter/base/filter_cache_fun.ml
+1 -0 metaprl-branches/opname_classes/filter/base/filter_type.ml
+12 -6 metaprl-branches/opname_classes/filter/filter/filter_parse.ml
+2 -2 metaprl-branches/opname_classes/refiner/refiner/refine.ml
+2 -2 metaprl-branches/opname_classes/refiner/refiner/refine.mli
+15 -11 metaprl-branches/opname_classes/refiner/refiner/refine_error.ml
+4 -4 metaprl-branches/opname_classes/refiner/refiner/refine_error.mli
+8 -1 metaprl-branches/opname_classes/refiner/refiner/refiner_ds.ml
+8 -2 metaprl-branches/opname_classes/refiner/refiner/refiner_std.ml
+165 -124 metaprl-branches/opname_classes/refiner/reflib/refine_exn.ml
+117 -51 metaprl-branches/opname_classes/refiner/reflib/term_class_infer.ml
+18 -8 metaprl-branches/opname_classes/refiner/refsig/refine_error_sig.ml
+5 -2 metaprl-branches/opname_classes/refiner/refsig/refiner_sig.ml
+4 -0 metaprl-branches/opname_classes/refiner/refsig/term_class_sig.ml
+2 -0 metaprl-branches/opname_classes/refiner/refsig/term_subst_sig.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_build_contractum.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_compile_contractum.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_compile_contractum.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_compile_redex.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_compile_redex.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_debug.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_debug.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_match_redex.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_meta.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_meta.mli
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_util.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_util.mli
+2 -2 metaprl-branches/opname_classes/refiner/term_ds/term_addr_ds.ml
+2 -2 metaprl-branches/opname_classes/refiner/term_ds/term_addr_ds.mli
+4 -4 metaprl-branches/opname_classes/refiner/term_ds/term_base_ds.ml
+4 -4 metaprl-branches/opname_classes/refiner/term_ds/term_base_ds.mli
+4 -4 metaprl-branches/opname_classes/refiner/term_ds/term_eval_ds.ml
+4 -4 metaprl-branches/opname_classes/refiner/term_ds/term_eval_ds.mli
+2 -2 metaprl-branches/opname_classes/refiner/term_ds/term_man_ds.ml
+2 -2 metaprl-branches/opname_classes/refiner/term_ds/term_man_ds.mli
+4 -4 metaprl-branches/opname_classes/refiner/term_ds/term_op_ds.ml
+6 -5 metaprl-branches/opname_classes/refiner/term_ds/term_op_ds.mli
+46 -4 metaprl-branches/opname_classes/refiner/term_ds/term_subst_ds.ml
+6 -5 metaprl-branches/opname_classes/refiner/term_ds/term_subst_ds.mli
+2 -2 metaprl-branches/opname_classes/refiner/term_gen/term_addr_gen.ml
+2 -2 metaprl-branches/opname_classes/refiner/term_gen/term_addr_gen.mli
+11 -0 metaprl-branches/opname_classes/refiner/term_gen/term_class_gen.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_gen/term_man_gen.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_gen/term_man_gen.mli
+1 -1 metaprl-branches/opname_classes/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_gen/term_meta_gen.mli
+6 -5 metaprl-branches/opname_classes/refiner/term_gen/term_shape_gen.ml
+7 -0 metaprl-branches/opname_classes/refiner/term_gen/term_shape_gen.mli
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_base_std.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_base_std.mli
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_eval_std.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_eval_std.mli
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_op_std.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_op_std.mli
+25 -2 metaprl-branches/opname_classes/refiner/term_std/term_subst_std.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_subst_std.mli
+7 -0 metaprl-branches/opname_classes/support/shell/package_info.ml
+1 -0 metaprl-branches/opname_classes/support/shell/package_info.mli
+3 -0 metaprl-branches/opname_classes/support/shell/shell_core.ml
+16 -0 metaprl-branches/opname_classes/support/shell/shell_state.ml
+2 -0 metaprl-branches/opname_classes/support/shell/shell_state.mli
+2 -1 metaprl-branches/opname_classes/theories/experimental/syntax/syntax_test.ml