Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-27 08:15:13 -0700 (Wed, 27 May 1998)
Revision: 2184
Log message:

      Functorized the refiner over the Term module.
      

Changes	Path
+1 -0	metaprl/clib/Makefile
Added	metaprl/clib/truncate.c
Properties	metaprl/clib/truncate.c
+5 -2	metaprl/filter/filter_ast.mli
+6 -1	metaprl/filter/filter_cache.ml
+4 -1	metaprl/filter/filter_cache.mli
+4 -1	metaprl/filter/filter_cache_fun.ml
+4 -1	metaprl/filter/filter_cache_fun.mli
+5 -2	metaprl/filter/filter_html.ml
+4 -1	metaprl/filter/filter_html.mli
+7 -1	metaprl/filter/filter_ocaml.ml
+4 -1	metaprl/filter/filter_ocaml.mli
+13 -8	metaprl/filter/filter_parse.ml
+4 -1	metaprl/filter/filter_parse.mli
+45 -35	metaprl/filter/filter_prog.ml
+4 -1	metaprl/filter/filter_prog.mli
+7 -2	metaprl/filter/filter_proof.ml
+4 -1	metaprl/filter/filter_proof.mli
+5 -2	metaprl/filter/filter_proof_type.mlz
+8 -2	metaprl/filter/filter_summary.ml
+5 -2	metaprl/filter/filter_summary.mli
+4 -1	metaprl/filter/filter_summary_io.ml
+4 -1	metaprl/filter/filter_summary_io.mli
+4 -1	metaprl/filter/filter_summary_type.mlz
+4 -1	metaprl/filter/filter_summary_util.ml
+4 -1	metaprl/filter/filter_summary_util.mli
+6 -2	metaprl/filter/filter_type.mlz
+8 -4	metaprl/filter/filter_util.ml
+5 -2	metaprl/filter/filter_util.mli
+7 -2	metaprl/filter/term_grammar.ml
+5 -2	metaprl/filter/term_grammar.mli
+3 -3	metaprl/library/basic.ml
+1 -1	metaprl/library/basic.mli
+13 -12	metaprl/library/db.ml
+1 -1	metaprl/library/db.mli
+1 -1	metaprl/library/definition.ml
+1 -1	metaprl/library/definition.mli
+2 -1	metaprl/library/library.ml
+1 -1	metaprl/library/library.mli
+1 -1	metaprl/library/library_eval.ml
+1 -1	metaprl/library/library_eval.mli
+4 -1	metaprl/library/library_type_base.ml
+4 -1	metaprl/library/library_type_base.mli
+2 -2	metaprl/library/link.ml
+1 -1	metaprl/library/link.mli
+11 -11	metaprl/library/mbterm.ml
+1 -1	metaprl/library/mbterm.mli
+7 -7	metaprl/library/nuprl5.ml
+1 -1	metaprl/library/nuprl5.mli
+1 -1	metaprl/library/oidtable.ml
+1 -1	metaprl/library/oidtable.mli
+2 -1	metaprl/library/orb.ml
+1 -1	metaprl/library/orb.mli
+1 -1	metaprl/library/test.ml
Properties	metaprl/refiner
+35 -9	metaprl/refiner/Makefile
+7 -3	metaprl/refiner/dform.ml
+6 -3	metaprl/refiner/dform.mli
+5 -2	metaprl/refiner/dform_print.mli
+5 -2	metaprl/refiner/ml_file.ml
+5 -2	metaprl/refiner/ml_format_sig.ml
+5 -2	metaprl/refiner/ml_print.ml
+5 -2	metaprl/refiner/ml_print_sig.ml
+135 -102	metaprl/refiner/refine.ml
+27 -1	metaprl/refiner/refine.mli
+9 -4	metaprl/refiner/refine_exn.ml
+5 -2	metaprl/refiner/refine_exn.mli
+83 -79	metaprl/refiner/refine_sig.ml
Deleted	metaprl/refiner/refine_util.ml
Deleted	metaprl/refiner/refine_util.mli
Added	metaprl/refiner/refiner.ml
Properties	metaprl/refiner/refiner.ml
Added	metaprl/refiner/refiner.mli
Properties	metaprl/refiner/refiner.mli
Added	metaprl/refiner/refiner_sig.ml
Properties	metaprl/refiner/refiner_sig.ml
Added	metaprl/refiner/refiner_std.ml
Properties	metaprl/refiner/refiner_std.ml
Added	metaprl/refiner/refiner_std.mli
Properties	metaprl/refiner/refiner_std.mli
+1163 -1484	metaprl/refiner/rewrite.ml
+23 -75	metaprl/refiner/rewrite.mli
Added	metaprl/refiner/rewrite_sig.ml
Properties	metaprl/refiner/rewrite_sig.ml
+8 -6	metaprl/refiner/simple_print.ml
+6 -57	metaprl/refiner/simple_print.mli
Deleted	metaprl/refiner/term.ml
Deleted	metaprl/refiner/term.mli
Added	metaprl/refiner/term_addr_sig.ml
Properties	metaprl/refiner/term_addr_sig.ml
Added	metaprl/refiner/term_addr_std.ml
Properties	metaprl/refiner/term_addr_std.ml
Added	metaprl/refiner/term_addr_std.mli
Properties	metaprl/refiner/term_addr_std.mli
+6 -3	metaprl/refiner/term_dtable.ml
+4 -1	metaprl/refiner/term_dtable.mli
Added	metaprl/refiner/term_eval_sig.ml
Properties	metaprl/refiner/term_eval_sig.ml
Added	metaprl/refiner/term_eval_std.ml
Properties	metaprl/refiner/term_eval_std.ml
Added	metaprl/refiner/term_eval_std.mli
Properties	metaprl/refiner/term_eval_std.mli
Added	metaprl/refiner/term_man_sig.ml
Properties	metaprl/refiner/term_man_sig.ml
Added	metaprl/refiner/term_man_std.ml
Properties	metaprl/refiner/term_man_std.ml
Added	metaprl/refiner/term_man_std.mli
Properties	metaprl/refiner/term_man_std.mli
Added	metaprl/refiner/term_meta_sig.ml
Properties	metaprl/refiner/term_meta_sig.ml
Added	metaprl/refiner/term_meta_std.ml
Properties	metaprl/refiner/term_meta_std.ml
Added	metaprl/refiner/term_meta_std.mli
Properties	metaprl/refiner/term_meta_std.mli
Added	metaprl/refiner/term_op_sig.ml
Properties	metaprl/refiner/term_op_sig.ml
Added	metaprl/refiner/term_op_std.ml
Properties	metaprl/refiner/term_op_std.ml
Added	metaprl/refiner/term_op_std.mli
Properties	metaprl/refiner/term_op_std.mli
Added	metaprl/refiner/term_shape_sig.ml
Properties	metaprl/refiner/term_shape_sig.ml
Added	metaprl/refiner/term_shape_std.ml
Properties	metaprl/refiner/term_shape_std.ml
Added	metaprl/refiner/term_shape_std.mli
Properties	metaprl/refiner/term_shape_std.mli
Added	metaprl/refiner/term_sig.ml
Properties	metaprl/refiner/term_sig.ml
+6 -3	metaprl/refiner/term_stable.ml
+4 -1	metaprl/refiner/term_stable.mli
Added	metaprl/refiner/term_std.ml
Properties	metaprl/refiner/term_std.ml
Added	metaprl/refiner/term_std.mli
Properties	metaprl/refiner/term_std.mli
Added	metaprl/refiner/term_subst_sig.ml
Properties	metaprl/refiner/term_subst_sig.ml
Added	metaprl/refiner/term_subst_std.ml
Properties	metaprl/refiner/term_subst_std.ml
Added	metaprl/refiner/term_subst_std.mli
Properties	metaprl/refiner/term_subst_std.mli
+8 -3	metaprl/refiner/term_table.ml
+5 -2	metaprl/refiner/term_table.mli
+6 -2	metaprl/refiner/term_template.ml
+4 -1	metaprl/refiner/term_template.mli
Deleted	metaprl/refiner/term_util.ml
Deleted	metaprl/refiner/term_util.mli
+6 -3	metaprl/refiner/theory.ml
+5 -2	metaprl/refiner/theory.mli