Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-12 09:48:45 -0700 (Sun, 12 May 2002)
Revision: 3628
Log message:

      Merging the ocaml_3_04 branch.
      
      The major changes in this commit are:
      
      - Switch to OCaml+CamlP4 version 3.04
      - Many cons changes (in particular, cons now only supports mcc+MetaPRL,
      but does not support standalone MetaPRL).
      - Added partial support for "input forms" that are the input analogy to display forms.
      - Added apply_rewrite function.
      - Updated Mp_mc_compile to use the updated apply_rewrite mechanism.
      - Changed the top_bookmark implementation to make it more explicit that
      it's always the same bookmark.
      - Filter_ocaml unmarshaling for str_items now fails softly.  If the
      term format changes, you may get a warning asking you to regenerate
      the .prla files.
      - Filter_ocaml was significantly restructured to speed up the compilation.
      

Changes  Path
Deleted metaprl/Conscript
Deleted metaprl/Construct
+0 -0 metaprl/clib/Conscript
+3 -3 metaprl/editor/ml/Conscript
+3 -0 metaprl/editor/ml/shell.ml
+4 -7 metaprl/editor/ml/shell_state.ml
+1 -1 metaprl/ensemble/Conscript
+2 -2 metaprl/filter/base/Conscript
+1 -2 metaprl/filter/base/filter_cache.ml
+9 -3 metaprl/filter/base/filter_comment.ml
+33 -9 metaprl/filter/base/filter_hash.ml
+1659 -1510 metaprl/filter/base/filter_ocaml.ml
+4 -13 metaprl/filter/base/filter_ocaml.mli
+64 -0 metaprl/filter/base/filter_prog.ml
+81 -45 metaprl/filter/base/filter_summary.ml
+1 -0 metaprl/filter/base/filter_type.ml
+1 -1 metaprl/filter/base/free_vars.ml
+34 -13 metaprl/filter/base/mLast_util.ml
+2 -2 metaprl/filter/boot/Conscript
+5 -0 metaprl/filter/boot/conversionals_boot.ml
+19 -0 metaprl/filter/boot/rewrite_boot.ml
+16 -0 metaprl/filter/boot/tactic_boot.ml
+24 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+11 -11 metaprl/filter/filter/Conscript
+30 -0 metaprl/filter/filter/filter_parse.ml
+7 -3 metaprl/filter/filter/prlcomp.ml
+1 -1 metaprl/library/Conscript
+3 -3 metaprl/mk/preface
+27 -27 metaprl/mk/rules
+1 -1 metaprl/mllib/Conscript
+1 -1 metaprl/refiner/refbase/Conscript
+1 -1 metaprl/refiner/refiner/Conscript
+42 -5 metaprl/refiner/refiner/refine.ml
+1 -1 metaprl/refiner/reflib/Conscript
+23 -12 metaprl/refiner/reflib/mp_resource.ml
+4 -2 metaprl/refiner/reflib/mp_resource.mli
+1 -1 metaprl/refiner/refsig/Conscript
+5 -0 metaprl/refiner/refsig/refine_sig.ml
+1 -1 metaprl/refiner/rewrite/Conscript
+2 -1 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+8 -6 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+1 -1 metaprl/refiner/term_ds/Conscript
+1 -1 metaprl/refiner/term_gen/Conscript
+1 -1 metaprl/refiner/term_std/Conscript
+1 -1 metaprl/theories/Conscript
+1 -1 metaprl/theories/base/Conscript
+1 -1 metaprl/theories/itt/Conscript
+353 -417 metaprl/theories/itt/ctt_markov.prla
+1538 -1484 metaprl/theories/itt/itt_bisect.prla
+4714 -4705 metaprl/theories/itt/itt_bool.prla
+517 -365 metaprl/theories/itt/itt_bunion.prla
+573 -573 metaprl/theories/itt/itt_collection.prla
+71 -71 metaprl/theories/itt/itt_decidable.prla
+2749 -2997 metaprl/theories/itt/itt_derive.prla
+1389 -1764 metaprl/theories/itt/itt_dfun.prla
+869 -890 metaprl/theories/itt/itt_disect.prla
+3078 -3479 metaprl/theories/itt/itt_dprod.prla
+4418 -4468 metaprl/theories/itt/itt_equal.prla
+60 -57 metaprl/theories/itt/itt_esquash.prla
+292 -311 metaprl/theories/itt/itt_ext_equal.prla
+3695 -3691 metaprl/theories/itt/itt_fset.prla
+1777 -1764 metaprl/theories/itt/itt_fun.prla
+215 -212 metaprl/theories/itt/itt_int_arith.prla
+3146 -3376 metaprl/theories/itt/itt_int_base.prla
+4823 -4775 metaprl/theories/itt/itt_int_ext.prla
+1287 -1395 metaprl/theories/itt/itt_isect.prla
+2343 -2429 metaprl/theories/itt/itt_list.prla
+2306 -2295 metaprl/theories/itt/itt_list2.prla
+15759 -15855 metaprl/theories/itt/itt_logic.prla
+2204 -2378 metaprl/theories/itt/itt_nat.prla
+271 -531 metaprl/theories/itt/itt_pointwise.prla
+286 -247 metaprl/theories/itt/itt_pointwise2.prla
+823 -1343 metaprl/theories/itt/itt_prod.prla
+637 -918 metaprl/theories/itt/itt_prop_decide.prla
+2162 -1758 metaprl/theories/itt/itt_quotient.prla
+395 -395 metaprl/theories/itt/itt_record.prla
+331 -316 metaprl/theories/itt/itt_record0.prla
+1081 -1088 metaprl/theories/itt/itt_record_exm.prla
+1482 -1724 metaprl/theories/itt/itt_record_label.prla
+638 -928 metaprl/theories/itt/itt_record_label0.prla
+5537 -6032 metaprl/theories/itt/itt_rfun.prla
+525 -525 metaprl/theories/itt/itt_sort.prla
+8719 -8029 metaprl/theories/itt/itt_squash.prla
+5338 -2171 metaprl/theories/itt/itt_squiggle.prla
+3362 -3176 metaprl/theories/itt/itt_struct.prla
+3974 -3988 metaprl/theories/itt/itt_struct2.prla
+244 -256 metaprl/theories/itt/itt_struct3.prla
+2253 -2224 metaprl/theories/itt/itt_subtype.prla
+272 -290 metaprl/theories/itt/itt_tsquash.prla
+292 -312 metaprl/theories/itt/itt_tunion.prla
+3014 -3122 metaprl/theories/itt/itt_union.prla
+1004 -1763 metaprl/theories/itt/itt_unit.prla
+860 -1239 metaprl/theories/itt/itt_void.prla
+1254 -1247 metaprl/theories/itt/itt_w.prla
+853 -1112 metaprl/theories/itt/itt_well_founded.prla
+17 -24 metaprl/theories/mc/Conscript
+3 -1 metaprl/theories/mc/Makefile
+18 -21 metaprl/theories/mc/README
+3 -3 metaprl/theories/mc/TODO
+72 -10 metaprl/theories/mc/mp_mc_compile.ml
+12 -4 metaprl/theories/mc/mp_mc_compile.mli
+82 -37 metaprl/theories/mc/mp_mc_connect_base.ml
+17 -3 metaprl/theories/mc/mp_mc_connect_base.mli
+127 -155 metaprl/theories/mc/mp_mc_connect_exp.ml
+2 -7 metaprl/theories/mc/mp_mc_connect_exp.mli
Added metaprl/theories/mc/mp_mc_connect_prog.ml
Properties metaprl/theories/mc/mp_mc_connect_prog.ml
Added metaprl/theories/mc/mp_mc_connect_prog.mli
Properties metaprl/theories/mc/mp_mc_connect_prog.mli
+5 -8 metaprl/theories/mc/mp_mc_connect_ty.ml
+2 -2 metaprl/theories/mc/mp_mc_connect_ty.mli
+6 -3 metaprl/theories/mc/mp_mc_const_elim.ml
+1 -1 metaprl/theories/mc/mp_mc_const_elim.mli
+3 -3 metaprl/theories/mc/mp_mc_deadcode.ml
+1 -1 metaprl/theories/mc/mp_mc_deadcode.mli
+24 -0 metaprl/theories/mc/mp_mc_fir_base.ml
+13 -0 metaprl/theories/mc/mp_mc_fir_base.mli
+0 -24 metaprl/theories/mc/mp_mc_fir_exp.ml
+0 -11 metaprl/theories/mc/mp_mc_fir_exp.mli
Added metaprl/theories/mc/mp_mc_fir_phobos.ml
Properties metaprl/theories/mc/mp_mc_fir_phobos.ml
Added metaprl/theories/mc/mp_mc_fir_phobos.mli
Properties metaprl/theories/mc/mp_mc_fir_phobos.mli
Added metaprl/theories/mc/mp_mc_fir_phobos_exp.ml
Properties metaprl/theories/mc/mp_mc_fir_phobos_exp.ml
Added metaprl/theories/mc/mp_mc_fir_phobos_exp.mli
Properties metaprl/theories/mc/mp_mc_fir_phobos_exp.mli
Added metaprl/theories/mc/mp_mc_fir_prog.ml
Properties metaprl/theories/mc/mp_mc_fir_prog.ml
Added metaprl/theories/mc/mp_mc_fir_prog.mli
Properties metaprl/theories/mc/mp_mc_fir_prog.mli
+4 -1 metaprl/theories/mc/mp_mc_theory.mlz
+8 -5 metaprl/theories/mc/tests/Conscript
Added metaprl/theories/mc/tests/mp_mc_test.ml
Properties metaprl/theories/mc/tests/mp_mc_test.ml
Added metaprl/theories/mc/tests/mp_mc_test.mli
Properties metaprl/theories/mc/tests/mp_mc_test.mli
+2 -2 metaprl/theories/ocaml/Conscript
+2 -2 metaprl/theories/tactic/Conscript
+14 -1 metaprl/theories/tactic/mptop.ml
+7 -0 metaprl/theories/tactic/top_conversionals.ml
+5 -0 metaprl/theories/tactic/top_conversionals.mli
+2 -2 metaprl/util/Makefile
+16 -15 metaprl/util/macro.ml