Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-01-21 16:29:08 -0800 (Wed, 21 Jan 2004)
Revision: 5268
Log message:

      Changed the meta_term and hypothesis type definitions in term_sig
      to avoid type duplication.
      
      The new type definitions are toplevel as polymorphic types.  For example
      
      |   type 'term poly_hypothesis = Hypothesis of 'term | ...
      
      Then, once the term type is defined, we can use the following
      definition:
      
      |   type hypothesis = term poly_hypothesis
      
      This is in preparation for extending the hypothesis type with
      cases for recursive sequents.
      

Changes  Path
+1 -0 metaprl/filter/base/filter_summary.ml
+1 -0 metaprl/filter/base/filter_util.ml
+1 -0 metaprl/filter/filter/filter_parse.ml
+4 -4 metaprl/filter/filter/filter_patt.ml
+1 -0 metaprl/filter/filter/term_grammar.ml
+3 -2 metaprl/refiner/reflib/arith.ml
+3 -3 metaprl/refiner/reflib/ascii_io.ml
+1 -0 metaprl/refiner/reflib/dform.ml
+2 -1 metaprl/refiner/reflib/match_seq.ml
+1 -0 metaprl/refiner/reflib/ml_format.ml
+1 -0 metaprl/refiner/reflib/refine_exn.ml
+1 -1 metaprl/refiner/reflib/simple_print.ml
+3 -3 metaprl/refiner/reflib/term_compare.ml
+1 -0 metaprl/refiner/reflib/term_match_table.ml
+12 -10 metaprl/refiner/refsig/term_sig.ml
+1 -0 metaprl/refiner/term_ds/term_addr_ds.ml
+1 -0 metaprl/refiner/term_ds/term_base_ds.ml
+3 -14 metaprl/refiner/term_ds/term_ds.ml
+3 -10 metaprl/refiner/term_ds/term_ds_sig.ml
+2 -2 metaprl/refiner/term_ds/term_man_ds.ml
+1 -0 metaprl/refiner/term_ds/term_op_ds.ml
+1 -0 metaprl/refiner/term_ds/term_subst_ds.ml
+8 -8 metaprl/refiner/term_gen/term_hash.ml
+8 -8 metaprl/refiner/term_gen/term_header_constr.ml
+3 -14 metaprl/refiner/term_std/term_std.ml
+3 -10 metaprl/refiner/term_std/term_std_sig.ml
+1 -0 metaprl/support/display/base_dform.ml
+1 -0 metaprl/support/shell/shell_rule.ml
+1 -0 metaprl/support/tactics/dtactic.ml
+3 -3 metaprl/support/tactics/tactic_cache.ml
+1 -0 metaprl/support/tactics/top_tacticals.ml
+1 -0 metaprl/support/tactics/typeinf.ml
+2 -1 metaprl/theories/experimental/compile/m_util.ml
+3 -12 metaprl/theories/itt/itt_int_arith.ml
+1 -0 metaprl/theories/itt/itt_logic.ml
+13 -39 metaprl/theories/itt/itt_squash.ml
+20 -5 metaprl/theories/itt/itt_supinf.ml
+1 -0 metaprl/theories/tptp/tptp_load.ml
+1 -0 metaprl/theories/tptp/tptp_prove.ml
+14 -14 mpcompiler/mmc/core/mmc_core_closure.ml
+5 -4 mpcompiler/mmc/core/mmc_core_type_infer.ml
+1 -0 mpcompiler/mmc/core/mmc_core_util.ml

Changes by: ( at unknown.email)
Date: 2004-01-28 03:15:41 -0800 (Wed, 28 Jan 2004)
Revision: 5303
Log message:

      This commit was manufactured by cvs2svn to create branch
      'recursive_sequents'.

Changes  Path
Copied metaprl-branches/recursive_sequents
Deleted metaprl-branches/recursive_sequents/Makefile
Deleted metaprl-branches/recursive_sequents/OMakefile
Deleted metaprl-branches/recursive_sequents/doc/latex/theories/OMakefile
Deleted metaprl-branches/recursive_sequents/editor/ml/tests/prop-pigeon.ml
Deleted metaprl-branches/recursive_sequents/editor/ml/tests/test.ml
Deleted metaprl-branches/recursive_sequents/filter/OMakefile
Deleted metaprl-branches/recursive_sequents/filter/base/filter_summary_util.ml
Deleted metaprl-branches/recursive_sequents/filter/base/filter_summary_util.mli
Deleted metaprl-branches/recursive_sequents/filter/base/filter_util.ml
Deleted metaprl-branches/recursive_sequents/filter/base/filter_util.mli
Deleted metaprl-branches/recursive_sequents/filter/filter/filter_parse.ml
Deleted metaprl-branches/recursive_sequents/mk/defaults
Deleted metaprl-branches/recursive_sequents/mk/make_config.sh
Deleted metaprl-branches/recursive_sequents/mk/preface
Deleted metaprl-branches/recursive_sequents/mllib/debug_tables.ml
Deleted metaprl-branches/recursive_sequents/refiner/refiner/refine.ml
Deleted metaprl-branches/recursive_sequents/refiner/reflib/refine_exn.ml
Deleted metaprl-branches/recursive_sequents/refiner/reflib/refine_exn.mli
Deleted metaprl-branches/recursive_sequents/refiner/reflib/term_eq_table.ml
Deleted metaprl-branches/recursive_sequents/refiner/refsig/term_meta_sig.ml
Deleted metaprl-branches/recursive_sequents/refiner/refsig/term_subst_sig.ml
Deleted metaprl-branches/recursive_sequents/refiner/rewrite/rewrite.ml
Deleted metaprl-branches/recursive_sequents/refiner/rewrite/rewrite_compile_redex.ml
Deleted metaprl-branches/recursive_sequents/refiner/rewrite/rewrite_debug.mli
Deleted metaprl-branches/recursive_sequents/refiner/rewrite/rewrite_match_redex.ml
Deleted metaprl-branches/recursive_sequents/refiner/rewrite/rewrite_types.ml
Deleted metaprl-branches/recursive_sequents/refiner/term_ds/term_subst_ds.ml
Deleted metaprl-branches/recursive_sequents/refiner/term_gen/term_meta_gen.ml
Deleted metaprl-branches/recursive_sequents/refiner/term_std/term_subst_std.ml
Deleted metaprl-branches/recursive_sequents/support/display/summary.ml
Deleted metaprl-branches/recursive_sequents/support/display/summary.mli
Deleted metaprl-branches/recursive_sequents/support/shell/package_info.ml
Deleted metaprl-branches/recursive_sequents/support/shell/proof_edit.ml
Deleted metaprl-branches/recursive_sequents/support/shell/shell.ml
Deleted metaprl-branches/recursive_sequents/support/shell/shell_rule.ml
Deleted metaprl-branches/recursive_sequents/support/shell/shell_state.ml
Deleted metaprl-branches/recursive_sequents/support/tactics/tactic_cache.ml
Deleted metaprl-branches/recursive_sequents/tactics/proof/proof_boot.ml
Deleted metaprl-branches/recursive_sequents/tactics/proof/tactic_boot_sig.ml
Deleted metaprl-branches/recursive_sequents/tactics/proof/tacticals_boot.ml
Deleted metaprl-branches/recursive_sequents/theories/czf/czf_itt_bool.ml
Deleted metaprl-branches/recursive_sequents/theories/czf/czf_itt_equiv.ml
Deleted metaprl-branches/recursive_sequents/theories/experimental/compile/m_util.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/Makefile
Deleted metaprl-branches/recursive_sequents/theories/itt/OMakefile
Deleted metaprl-branches/recursive_sequents/theories/itt/ctt_markov.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_antiquotient.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_antiquotient.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_bool.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_bool.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_bugs.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_cyclic_group.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_cyclic_group.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_disect.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_eq_base.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_field.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_field2.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_field2.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_fset.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_fun2.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_group.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_group.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_grouplikeobj.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_grouplikeobj.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_arith.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_arith.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_base.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_base.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_ext.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_ext.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_int_ext.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_intdomain.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_intdomain.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_nat.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_nat.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_nat.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_nequal.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_order.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_poly.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_poly.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_poly.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_prec.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_quotient.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_quotient_group.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_quotient_group.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_rat.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_rat.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_record_label.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_record_renaming.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_relation_str.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_rfun.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_rfun.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_ring.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_ring2.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_ring2.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_squiggle.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_squiggle.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_subset.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_subtype.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_subtype.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_supinf.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_supinf.mli
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_supinf.prla
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_test.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/itt_unitring.ml
Deleted metaprl-branches/recursive_sequents/theories/itt/jprover_tests.ml
Deleted metaprl-branches/recursive_sequents/util/OMakefile
Copied mpcompiler-branches/recursive_sequents
Deleted mpcompiler-branches/recursive_sequents/mmc/core/core_test.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/core_tuple.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_closure.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_cps.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_list_util.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_tast.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_tast.mli
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_tast_util.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_theory.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_type_check.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_type_erase.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_type_infer.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_type_util.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_type_util.mli
Deleted mpcompiler-branches/recursive_sequents/mmc/core/mmc_core_util.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/extensions/ext_arithmetic.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/extensions/ext_arithmetic_integer.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/extensions/ext_array.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/extensions/ext_boolean.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/extensions/ext_int_test.ml
Deleted mpcompiler-branches/recursive_sequents/mmc/extensions/ext_integer.ml
Copied texinputs-branches/recursive_sequents
Deleted texinputs-branches/recursive_sequents/1cm.sty
Deleted texinputs-branches/recursive_sequents/1cml.sty
Deleted texinputs-branches/recursive_sequents/Makefile
Deleted texinputs-branches/recursive_sequents/Makefile-common
Deleted texinputs-branches/recursive_sequents/PPR-macros.tex
Deleted texinputs-branches/recursive_sequents/PPRmyppr.sty
Deleted texinputs-branches/recursive_sequents/bcp.bib
Deleted texinputs-branches/recursive_sequents/citlogo.eps
Deleted texinputs-branches/recursive_sequents/citlogo2.eps
Deleted texinputs-branches/recursive_sequents/config.ppr
Deleted texinputs-branches/recursive_sequents/cornell-logo.eps
Deleted texinputs-branches/recursive_sequents/dag50.eps
Deleted texinputs-branches/recursive_sequents/der.tex
Deleted texinputs-branches/recursive_sequents/gate.eps
Deleted texinputs-branches/recursive_sequents/gate.pdf
Deleted texinputs-branches/recursive_sequents/include.tex
Deleted texinputs-branches/recursive_sequents/omscmsy.fd
Deleted texinputs-branches/recursive_sequents/ot1cmr.fd
Deleted texinputs-branches/recursive_sequents/ot1cmss.fd
Deleted texinputs-branches/recursive_sequents/ot1lcmss.fd
Deleted texinputs-branches/recursive_sequents/ot1lcmtt.fd
Deleted texinputs-branches/recursive_sequents/pprpdf
Deleted texinputs-branches/recursive_sequents/proof.sty
Deleted texinputs-branches/recursive_sequents/rc.bib
Deleted texinputs-branches/recursive_sequents/slides-nogin.cls
Deleted texinputs-branches/recursive_sequents/splncs.bst
Deleted texinputs-branches/recursive_sequents/umsa.fd
Deleted texinputs-branches/recursive_sequents/umsb.fd

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 18:29:59 -0800 (Wed, 28 Jan 2004)
Revision: 5307
Log message:

      Removed all the unused "open" statements.
      

Changes  Path
+0 -1 metaprl/filter/base/filter_util.ml
+3 -5 metaprl/refiner/reflib/refine_exn.ml
+0 -1 metaprl/refiner/reflib/refine_exn.mli
+0 -1 metaprl/refiner/rewrite/rewrite.ml
+0 -1 metaprl/refiner/rewrite/rewrite_debug.mli
+0 -3 metaprl/support/shell/package_info.ml
+0 -1 metaprl/support/shell/shell_rule.ml
+4 -4 metaprl/support/shell/shell_state.ml
+0 -1 metaprl/support/tactics/tactic_cache.ml
+0 -1 metaprl/tactics/proof/tactic_boot_sig.ml
+0 -1 metaprl/theories/experimental/compile/m_util.ml
+0 -2 metaprl/theories/itt/itt_bugs.ml
+0 -10 metaprl/theories/itt/itt_field.ml
+0 -7 metaprl/theories/itt/itt_field2.ml
+0 -1 metaprl/theories/itt/itt_fun2.ml
+1 -11 metaprl/theories/itt/itt_intdomain.ml
+0 -1 metaprl/theories/itt/itt_nat.mli
+0 -14 metaprl/theories/itt/itt_nequal.ml
+0 -9 metaprl/theories/itt/itt_order.ml
+0 -10 metaprl/theories/itt/itt_poly.ml
+0 -3 metaprl/theories/itt/itt_rat.ml
+0 -5 metaprl/theories/itt/itt_record_label.ml
+0 -1 metaprl/theories/itt/itt_record_renaming.ml
+0 -2 metaprl/theories/itt/itt_relation_str.ml
+0 -1 metaprl/theories/itt/itt_rfun.mli
+0 -9 metaprl/theories/itt/itt_ring.ml
+0 -1 metaprl/theories/itt/itt_ring2.ml
+0 -1 metaprl/theories/itt/itt_squiggle.ml
+0 -1 metaprl/theories/itt/itt_squiggle.mli
+0 -12 metaprl/theories/itt/itt_supinf.ml
+0 -1 metaprl/theories/itt/itt_supinf.mli
+0 -9 metaprl/theories/itt/itt_unitring.ml
+0 -1 mpcompiler/mmc/core/mmc_core_closure.ml
+0 -1 mpcompiler/mmc/core/mmc_core_type_infer.ml
+0 -1 mpcompiler/mmc/core/mmc_core_util.ml

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-01-30 17:11:03 -0800 (Fri, 30 Jan 2004)
Revision: 5323
Log message:

      Changed AtomTyApply to take 3 arguments and cleaned up the giant rewrite in CPS.
      

Changes  Path
+8 -8 mpcompiler/mmc/core/core_test.ml
+10 -9 mpcompiler/mmc/core/core_tuple.ml
+1 -0 mpcompiler/mmc/core/mmc_core_closure.ml
+68 -32 mpcompiler/mmc/core/mmc_core_cps.ml
+4 -4 mpcompiler/mmc/core/mmc_core_list_util.ml
+3 -3 mpcompiler/mmc/core/mmc_core_tast.ml
+1 -1 mpcompiler/mmc/core/mmc_core_tast.mli
+1 -1 mpcompiler/mmc/core/mmc_core_tast_util.ml
+0 -1 mpcompiler/mmc/core/mmc_core_theory.ml
+54 -14 mpcompiler/mmc/core/mmc_core_type_check.ml
+1 -1 mpcompiler/mmc/core/mmc_core_type_erase.ml
+15 -4 mpcompiler/mmc/core/mmc_core_type_infer.ml
+37 -14 mpcompiler/mmc/core/mmc_core_type_util.ml
+3 -0 mpcompiler/mmc/core/mmc_core_type_util.mli
+15 -15 mpcompiler/mmc/extensions/ext_arithmetic.ml
+11 -11 mpcompiler/mmc/extensions/ext_arithmetic_integer.ml
+12 -12 mpcompiler/mmc/extensions/ext_array.ml
+26 -28 mpcompiler/mmc/extensions/ext_boolean.ml
+18 -18 mpcompiler/mmc/extensions/ext_int_test.ml
+4 -4 mpcompiler/mmc/extensions/ext_integer.ml