Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-08-01 02:31:10 -0700 (Fri, 01 Aug 2003)
Revision: 4801
Log message:

      A little hacking on the M-paper ::
      
      
      Fixed some formatting inconsistencies and moved some figure
      declarations around so that they are declared in the ``correct''
      locations (right after the paragraph in which they are first
      referenced, according to the LNCS style).
      
      Of course, having adhered to that little bit of the LNCS style, I
      go ahead and override their figure placement policy in m-paper.tex
      (look for the bit of code tagged with EMRE).  Personally, I
      dislike figures appearing in the middle of a page.  My policy may
      have an added bonus of shortening the paper slightly (by 1/2 a
      page at some point) over the LNCS default.
      
      Observation: The placement of figures 4--7 is hit-or-miss.  Either
      you get something reasonable, or two of them end up on their own
      page and waste _a lot_ of space.
      
      Another observation: if you delete the blank line before every
      $$...$$ environment and ensure that out of figures 4--7, 3 of them
      end up on the same page, you can get the paper down to 24 pages.
      I'm not quite sure why so much white space appears before these
      environments...
      
      I think that if you want to shorten the paper any further,
      probably more text will have to be cut (intro, summary, related
      work?).  If I get a chance, maybe I'll try to come up with more
      ideas in the morning.
      

Changes  Path
+6 -0 metaprl/doc/latex/theories/m-paper.tex
+10 -5 metaprl/theories/experimental/compile/m_doc_intro.ml
+22 -22 metaprl/theories/experimental/compile/m_doc_ir.ml
+29 -29 metaprl/theories/experimental/compile/m_doc_parsing.ml
+7 -7 metaprl/theories/experimental/compile/m_doc_summary.ml
+5 -5 metaprl/theories/experimental/compile/m_doc_x86_asm.ml
+33 -33 metaprl/theories/experimental/compile/m_doc_x86_codegen.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 10:17:06 -0700 (Fri, 01 Aug 2003)
Revision: 4802
Log message:

      Some minor formatting changes.
      

Changes  Path
+1 -1 metaprl/OMakefile
+2 -1 metaprl/doc/latex/theories/m-paper.tex
+1 -0 metaprl/theories/experimental/compile/Makefile
+3 -3 metaprl/theories/experimental/compile/OMakefile
+8 -8 metaprl/theories/experimental/compile/m_doc_comment.ml
+2 -0 metaprl/theories/experimental/compile/m_doc_comment.mli
+2 -0 metaprl/theories/experimental/compile/m_doc_intro.ml
+9 -6 metaprl/theories/experimental/compile/m_doc_ir.ml
+9 -7 metaprl/theories/experimental/compile/m_doc_parsing.ml
+9 -6 metaprl/theories/experimental/compile/m_doc_x86_asm.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 10:17:49 -0700 (Fri, 01 Aug 2003)
Revision: 4803
Log message:

      Forgot to commit this file from proposal.
      

Changes  Path
Added metaprl/theories/experimental/compile/m_doc_proposal.ml
Properties metaprl/theories/experimental/compile/m_doc_proposal.ml
Added metaprl/theories/experimental/compile/m_doc_proposal.mli
Properties metaprl/theories/experimental/compile/m_doc_proposal.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 10:32:38 -0700 (Fri, 01 Aug 2003)
Revision: 4804
Log message:

      Reduced the text in the parsing section.
      

Changes  Path
+6 -10 metaprl/theories/experimental/compile/m_doc_intro.ml
+17 -30 metaprl/theories/experimental/compile/m_doc_parsing.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 10:45:31 -0700 (Fri, 01 Aug 2003)
Revision: 4805
Log message:

      More formatting, half a page to go.
      

Changes  Path
+1 -0 metaprl/doc/latex/theories/m-paper.tex
+4 -2 metaprl/theories/experimental/compile/m_doc_x86_codegen.ml
+0 -0 metaprl/theories/experimental/compile/m_doc_x86_regalloc.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 11:12:01 -0700 (Fri, 01 Aug 2003)
Revision: 4806
Log message:

      Reformatted some figures.
      

Changes  Path
+12 -12 metaprl/theories/experimental/compile/m_doc_ir.ml
+18 -18 metaprl/theories/experimental/compile/m_doc_x86_asm.ml
+12 -8 metaprl/theories/experimental/compile/m_doc_x86_codegen.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 11:19:10 -0700 (Fri, 01 Aug 2003)
Revision: 4807
Log message:

      Really stripped down the optimization section.  Just one reference
      overflows.
      

Changes  Path
+16 -12 metaprl/theories/experimental/compile/m_doc_opt.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 11:22:51 -0700 (Fri, 01 Aug 2003)
Revision: 4808
Log message:

      Removed a few sentences in the related work.  The paper is now 23 pages.
      

Changes  Path
+1 -1 metaprl/doc/latex/theories/m-paper.tex
+5 -4 metaprl/theories/experimental/compile/m_doc_summary.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-01 15:42:26 -0700 (Fri, 01 Aug 2003)
Revision: 4809
Log message:

      Added some extra statements about HOAS.  I think the paper is ready to go.
      

Changes  Path
+1 -1 metaprl/doc/latex/theories/m-paper.tex
+2 -1 metaprl/theories/experimental/compile/m_doc_intro.ml
+3 -2 metaprl/theories/experimental/compile/m_doc_ir.ml
+2 -2 metaprl/theories/experimental/compile/m_doc_x86_opt.ml
+1 -1 metaprl/theories/experimental/compile/m_doc_x86_regalloc.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-02 05:51:22 -0700 (Sat, 02 Aug 2003)
Revision: 4810
Log message:

      Minor display forms updates. "make latex" now works.
      

Changes  Path
+2 -2 metaprl/support/display/base_dform.ml
+1 -1 metaprl/support/display/summary.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-03 10:56:48 -0700 (Sun, 03 Aug 2003)
Revision: 4811
Log message:

      Minor changes towards getting mojave_sequents to compile.
      

Changes  Path
+8 -4 metaprl/filter/filter/filter_parse.ml
+8 -8 metaprl/filter/filter/filter_patt.ml
+6 -10 metaprl/filter/filter/term_grammar.ml
+2 -2 metaprl/refiner/term_ds/term_man_ds.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 13:34:06 -0700 (Mon, 04 Aug 2003)
Revision: 4813
Log message:

      The new explicit-contexts code discovered a bug, now we have to
      figure out how to fix it.
      
      Consider the following rewrite, which is obviously sensible.
      
         Lambda{x. 'e['x]} : TyAll{y. 't['y]}
         <-->
         Lambda{x. TyConstrain{'e['x]; 't['x]}} : TyAll{y. 't['y]}
      
      Now consider the sequent form, which does something similar,
      but fails because of the context substitution.
      
         sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
         <-->
         sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
         sequent [TyAll] { <H> >- 't<|K|> }
      

Changes  Path
+9 -3 metaprl/OMakefile
+1 -0 metaprl/clib/OMakefile
+1 -1 metaprl/doc/latex/theories/m-paper.tex
+8 -1 metaprl/filter/filter/filter_main.ml
+17 -5 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+33 -16 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_cps.ml
+5 -1 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_tast.ml
+36 -42 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_check.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 17:37:15 -0700 (Mon, 04 Aug 2003)
Revision: 4814
Log message:

      This is an unsatisfying workaround to the context scoping
      problem.  As mentioned in the previous commit, this is what
      we want:
      
       sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
       <-->
       sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
       sequent [TyAll] { <K> >- 't<|K|> }
      
      We should really get this notation to work.  In the meantime,
      we use this workaround:
      
       sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
       <-->
              collect{ty_vars. sequent [Lambda] { <H> >-
                 TyConstrain{'e; Apply{sequent [Lambda] { <K> >- 't<|K|> }; 'ty_vars}} :
       sequent [TyAll] { <H> >- 't<|K|> }
      
      Remember, collect{ty_vars. sequent [...] { <H> >- ... }} builds
      a list of the binding vars in <H>.
      
      That is, we use beta-reduction to perform an explicit substitution.
      It should work, but makes the code large, slow, and ugly.
      

Changes  Path
+2 -1 metaprl/filter/filter/filter_patt.ml
+15 -3 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_cps.ml
+15 -16 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-06 14:20:48 -0700 (Wed, 06 Aug 2003)
Revision: 4817
Log message:

      Added some support for sequent operations.
      
      subC now works correctly for sequents, but the sequent test is in the
      inner loop, so it will be a little slower.
      
      Haven't changed higherC yet.
      
      Added sequent support in Term_op_ds.{map_up,map_down}.
      

Changes  Path
+5 -0 metaprl/OMakefile
+38 -17 metaprl/editor/ml/shell_mp.ml
+67 -18 metaprl/filter/boot/conversionals_boot.ml
+13 -3 metaprl/filter/boot/exn_boot.ml
+1 -0 metaprl/filter/boot/exn_boot.mli
+8 -8 metaprl/filter/boot/rewrite_boot.ml
+1 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+2 -2 metaprl/refiner/reflib/term_match_table.ml
+1 -0 metaprl/refiner/refsig/term_addr_sig.ml
+5 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+3 -3 metaprl/refiner/term_ds/term_base_ds.ml
+42 -2 metaprl/refiner/term_ds/term_op_ds.ml
+8 -4 metaprl/refiner/term_ds/term_op_ds.mli
+1 -1 metaprl/refiner/term_gen/term_addr_gen.ml
+0 -2 metaprl/support/shell/shell.ml
+5 -6 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-11 14:31:31 -0700 (Mon, 11 Aug 2003)
Revision: 4821
Log message:

      . Fixed several things to work with sequents.
      .    1. In apply_redex, return *something* for a StackSeqContext.
      .       Even though we can't return the right thing, this should
      .       not fail.
      .    2. term_match_table now works with sequents.
      .
      . It is possible to define display form for sequents the normal way.
      . See core_ast.ml for an example.
      .
      . In core, the namer now works, type inference is stuck because
      . Unify_mm needs to be upgraded to work with sequents.
      

Changes  Path
+0 -5 metaprl/OMakefile
+10 -10 metaprl/editor/ml/shell_mp.ml
+8 -8 metaprl/filter/boot/conversionals_boot.ml
+9 -0 metaprl/mk/make_config.sh
+1 -1 metaprl/refiner/reflib/dform.ml
+389 -133 metaprl/refiner/reflib/term_match_table.ml
+2 -0 metaprl/refiner/reflib/term_match_table.mli
+3 -1 metaprl/refiner/refsig/term_shape_sig.ml
+5 -1 metaprl/refiner/rewrite/rewrite.ml
+3 -3 metaprl/refiner/rewrite/rewrite_debug.ml
+5 -5 metaprl/refiner/rewrite/rewrite_debug.mli
+1 -0 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+2 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+47 -16 metaprl/refiner/term_gen/term_shape_gen.ml
+3 -3 metaprl/support/display/base_dform.ml
+5 -0 metaprl/support/shell/shell.ml
+5 -0 metaprl/support/shell/shell.mli
+1 -1 metaprl/util/check-status.sh
+1 -0 mpcompiler-branches/mojave_sequents/mmc/core/Files
+2 -2 mpcompiler-branches/mojave_sequents/mmc/core/core_test.ml
+11 -22 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+1 -2 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.mli
Added mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.ml
Properties mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.ml
Added mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.mli
Properties mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.mli
+17 -7 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.ml
+8 -2 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.mli
+58 -10 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-12 11:44:27 -0700 (Tue, 12 Aug 2003)
Revision: 4826
Log message:

      Made some progress on unification.
      
      NOTE: Aleksey, there are various problems with sequents in
      Rewrite.extract_redex_values.  I've marked them with a BUG
      comment, and you should look when you get a chance.
      

Changes  Path
+35 -38 metaprl/refiner/reflib/dform.ml
+58 -0 metaprl/refiner/reflib/unify_mm.ml
+20 -6 metaprl/refiner/rewrite/rewrite.ml
+48 -10 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+7 -0 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.mli
+45 -9 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_tast.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-12 12:09:51 -0700 (Tue, 12 Aug 2003)
Revision: 4827
Log message:

      Tell infer_fun_type to pay attention to Hypothesis values
      as well as HypBinding.
      
      Here is the latest error:
      Uncaught exception: Invalid_argument("Rewrite_match_redex.check_sequent_hyps: binding clash in a sequent. Please let Aleksey Nogin know if this happens to you.")
      
      Apparently, we are creating sequents somewhere with shadowing in the hyps.
      

Changes  Path
+3 -3 metaprl/refiner/rewrite/rewrite_match_redex.ml
+8 -1 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-12 12:52:40 -0700 (Tue, 12 Aug 2003)
Revision: 4828
Log message:

      Turned off the hyp check so that we can at least see the sequents.
      However, it looks like my hack in Unify_mm doesn't work like we want.
      

Changes  Path
+9 -0 metaprl/refiner/rewrite/rewrite_debug.ml
+3 -0 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+10 -10 metaprl/refiner/rewrite/rewrite_match_redex.ml
+5 -16 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+0 -1 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.mli
+5 -13 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_tast.ml
+2 -5 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-12 17:23:29 -0700 (Tue, 12 Aug 2003)
Revision: 4829
Log message:

      Use `uname` to set the OSTYPE variable.
      

Changes  Path
+1 -1 metaprl/mk/preface

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-13 11:47:39 -0700 (Wed, 13 Aug 2003)
Revision: 4836
Log message:

      Updated the sequent code in Unify_mm.  The idea is to add a "compatibility
      layer" that converts sequents to the old format for use during unification,
      and these sequents have to be converted back to normal form when the
      unification is done.
      
      To do this, we just redefine dest_term and make_term to do the right thing.
      

Changes  Path
+179 -135 metaprl/refiner/reflib/unify_mm.ml
+5 -0 metaprl/refiner/reflib/unify_mm.mli
+14 -0 metaprl/support/shell/shell.ml
+4 -0 metaprl/support/shell/shell.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-13 12:00:04 -0700 (Wed, 13 Aug 2003)
Revision: 4837
Log message:

      Added sequent support in allSubC.
      

Changes  Path
+31 -7 metaprl/filter/boot/rewrite_boot.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-13 13:36:46 -0700 (Wed, 13 Aug 2003)
Revision: 4838
Log message:

      Type inference appears to complete on simple cases.
      
      There is something strange going on with rwc--it sems to
      be rewriting the proof, not the goal.
      

Changes  Path
+7 -3 metaprl/filter/boot/proof_boot.ml
+1 -0 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+1 -0 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.mli
+1 -4 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.mli
+41 -18 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_erase.ml
+2 -2 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-13 15:06:43 -0700 (Wed, 13 Aug 2003)
Revision: 4839
Log message:

      Backticks don't work in makefiles.  :-(  Use $(shell ...) instead.
      

Changes  Path
+1 -1 metaprl/mk/preface

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-17 01:44:53 -0700 (Sun, 17 Aug 2003)
Revision: 4844
Log message:

      Oops... forgot to add changes to editor/ml/mpconfig
      

Changes  Path
+1 -1 metaprl/OMakefile
+1 -1 metaprl/editor/ml/mpconfig

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-18 02:40:30 -0700 (Mon, 18 Aug 2003)
Revision: 4845
Log message:

      Towards compiling UNITY.
      

Changes  Path
+1 -1 metaprl/editor/ml/mpconfig
Properties metaprl/theories/experimental/unity
Added metaprl/theories/experimental/unity/Files
Properties metaprl/theories/experimental/unity/Files
Added metaprl/theories/experimental/unity/Makefile
Properties metaprl/theories/experimental/unity/Makefile
Added metaprl/theories/experimental/unity/OMakefile
Properties metaprl/theories/experimental/unity/OMakefile
Added metaprl/theories/experimental/unity/unity_ast.ml
Properties metaprl/theories/experimental/unity/unity_ast.ml
Added metaprl/theories/experimental/unity/unity_ast.mli
Properties metaprl/theories/experimental/unity/unity_ast.mli
Added metaprl/theories/experimental/unity/unity_source.ml
Properties metaprl/theories/experimental/unity/unity_source.ml
Added metaprl/theories/experimental/unity/unity_source.mli
Properties metaprl/theories/experimental/unity/unity_source.mli
Added metaprl/theories/experimental/unity/unity_test.ml
Properties metaprl/theories/experimental/unity/unity_test.ml
Added metaprl/theories/experimental/unity/unity_test.mli
Properties metaprl/theories/experimental/unity/unity_test.mli
Added metaprl/theories/experimental/unity/unity_theory.ml
Properties metaprl/theories/experimental/unity/unity_theory.ml
Added metaprl/theories/experimental/unity/unity_theory.mli
Properties metaprl/theories/experimental/unity/unity_theory.mli
Added metaprl/theories/experimental/unity/unity_translate.ml
Properties metaprl/theories/experimental/unity/unity_translate.ml
Added metaprl/theories/experimental/unity/unity_translate.mli
Properties metaprl/theories/experimental/unity/unity_translate.mli
Added metaprl/theories/experimental/unity/unity_util.ml
Properties metaprl/theories/experimental/unity/unity_util.ml
Added metaprl/theories/experimental/unity/unity_util.mli
Properties metaprl/theories/experimental/unity/unity_util.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-18 13:10:07 -0700 (Mon, 18 Aug 2003)
Revision: 4846
Log message:

      Replaced subterm_count with subterm_addresses (which is more sequent-friendly).
      
      Surprizingly, this did not eliminate the breakage that Jason's recent sequents-related
      commit have introduced (see "status update" message from Aug 14).
      

Changes  Path
+10 -77 metaprl/filter/boot/conversionals_boot.ml
+4 -35 metaprl/filter/boot/rewrite_boot.ml
+2 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+4 -1 metaprl/refiner/refsig/term_addr_sig.ml
+0 -1 metaprl/refiner/refsig/term_base_sig.ml
+24 -52 metaprl/refiner/term_ds/term_addr_ds.ml
+0 -7 metaprl/refiner/term_ds/term_base_ds.ml
+0 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+4 -2 metaprl/refiner/term_gen/term_addr_gen.ml
+0 -2 metaprl/refiner/term_std/term_base_std.ml
+0 -1 metaprl/refiner/term_std/term_std_sig.ml

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-18 17:13:09 -0700 (Mon, 18 Aug 2003)
Revision: 4849
Log message:

      Merged mojave_sequents branch back to the trunk.
      

Changes  Path
+1 -1 metaprl/mk/preface
Properties mpcompiler/mmc
Added mpcompiler/mmc/Makefile
Properties mpcompiler/mmc/Makefile
+22 -0 mpcompiler/mmc/OMakefile
+17 -12 mpcompiler/mmc/core/Files
+2 -5 mpcompiler/mmc/core/core_sequent.ml
+52 -3 mpcompiler/mmc/core/core_test.ml
Added mpcompiler/mmc/core/core_tuple.ml
Properties mpcompiler/mmc/core/core_tuple.ml
Added mpcompiler/mmc/core/core_tuple.mli
Properties mpcompiler/mmc/core/core_tuple.mli
+59 -12 mpcompiler/mmc/core/mmc_core_ast.ml
+15 -5 mpcompiler/mmc/core/mmc_core_ast.mli
Added mpcompiler/mmc/core/mmc_core_ast_util.ml
Properties mpcompiler/mmc/core/mmc_core_ast_util.ml
Added mpcompiler/mmc/core/mmc_core_ast_util.mli
Properties mpcompiler/mmc/core/mmc_core_ast_util.mli
Added mpcompiler/mmc/core/mmc_core_closure.ml
Properties mpcompiler/mmc/core/mmc_core_closure.ml
Added mpcompiler/mmc/core/mmc_core_closure.mli
Properties mpcompiler/mmc/core/mmc_core_closure.mli
+69 -30 mpcompiler/mmc/core/mmc_core_cps.ml
+7 -0 mpcompiler/mmc/core/mmc_core_cps.mli
Added mpcompiler/mmc/core/mmc_core_list_util.ml
Properties mpcompiler/mmc/core/mmc_core_list_util.ml
Added mpcompiler/mmc/core/mmc_core_list_util.mli
Properties mpcompiler/mmc/core/mmc_core_list_util.mli
+34 -8 mpcompiler/mmc/core/mmc_core_name.ml
+7 -2 mpcompiler/mmc/core/mmc_core_name.mli
+47 -13 mpcompiler/mmc/core/mmc_core_tast.ml
+3 -4 mpcompiler/mmc/core/mmc_core_tast.mli
Added mpcompiler/mmc/core/mmc_core_tast_util.ml
Properties mpcompiler/mmc/core/mmc_core_tast_util.ml
Added mpcompiler/mmc/core/mmc_core_tast_util.mli
Properties mpcompiler/mmc/core/mmc_core_tast_util.mli
+9 -0 mpcompiler/mmc/core/mmc_core_theory.ml
+118 -29 mpcompiler/mmc/core/mmc_core_type_check.ml
+1 -0 mpcompiler/mmc/core/mmc_core_type_check.mli
+55 -15 mpcompiler/mmc/core/mmc_core_type_erase.ml
+129 -31 mpcompiler/mmc/core/mmc_core_type_infer.ml
+44 -7 mpcompiler/mmc/core/mmc_core_type_util.ml
Properties mpcompiler/mmc/extensions
+3 -1 mpcompiler/mmc/extensions/Files
+49 -5 mpcompiler/mmc/extensions/ext_arithmetic_integer.ml
Added mpcompiler/mmc/extensions/ext_array_integer.ml
Properties mpcompiler/mmc/extensions/ext_array_integer.ml
Added mpcompiler/mmc/extensions/ext_array_integer.mli
Properties mpcompiler/mmc/extensions/ext_array_integer.mli
Added mpcompiler/mmc/extensions/ext_int_test.ml
Properties mpcompiler/mmc/extensions/ext_int_test.ml
Added mpcompiler/mmc/extensions/ext_int_test.mli
Properties mpcompiler/mmc/extensions/ext_int_test.mli
+10 -12 mpcompiler/mmc/extensions/ext_integer.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-18 21:48:05 -0700 (Mon, 18 Aug 2003)
Revision: 4850
Log message:

      - The rw*All family (rwAll, rwhAll, whAllAll, etc) will now use
      allSubC to descend into the goal instead of onAllClausesT. This means that
      it will now work correctly with any goal/assumption terms, not just
      sequents, and that it now avoids issues with sequent contexts not being a
      proper subterm.
      
      Note that this means that the rw*All will now try to rewrite the sequent argument
      as well!
      
      - thenC, firstT, and a few other similar tacticals and conversionals now check
      whether one of the argunemts is an idC (idT) and try to avoid creating
      identity proof steps unnecessarily.
      

Changes  Path
+1 -1 metaprl/editor/ml/mpconfig
+3 -3 metaprl/filter/boot/conversionals_boot.ml
+2 -2 metaprl/filter/boot/proof_boot.ml
+6 -4 metaprl/filter/boot/rewrite_boot.ml
+26 -13 metaprl/filter/boot/tactic_boot.ml
+9 -10 metaprl/filter/boot/tacticals_boot.ml
+1 -3 metaprl/support/tactics/top_tacticals.ml
+41 -41 metaprl/theories/fol/fol_itt_and.prla
+1524 -1485 metaprl/theories/fol/fol_itt_or.prla
+403 -766 metaprl/theories/itt/itt_record.prla
+1 -1 metaprl/theories/itt/itt_record_exm.prla

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-19 20:08:04 -0700 (Tue, 19 Aug 2003)
Revision: 4851
Log message:

      Cleaned up display of sequents a bit in simple_print.
      
      Also fixed bug that was causing core_test/test_prog1 to fail.  The problem was
      that this doesn't work:
      .   match explode_term t with
      .       << sequent ['foo] { ... }
      .               when alpha_equal foo << Foo >> ->
      
      The last line actually needs to be:
      .               when alpha_equal foo << sequent_arg{Foo} >> ->
      
      Ah, the joys of untyped languages...
      
      That fixed test_prog1, but test_prog2 now fails.  Beware, there's lots of grubby
      debugging output in core_type_infer.ml...
      

Changes  Path
+11 -7 metaprl/refiner/reflib/simple_print.ml
+6 -5 mpcompiler/mmc/core/core_tuple.ml
+3 -2 mpcompiler/mmc/core/mmc_core_closure.ml
+1 -1 mpcompiler/mmc/core/mmc_core_tast.ml
+28 -11 mpcompiler/mmc/core/mmc_core_type_infer.ml
+13 -0 mpcompiler/mmc/core/mmc_core_type_util.ml
+3 -0 mpcompiler/mmc/core/mmc_core_type_util.mli
+2 -1 mpcompiler/mmc/extensions/Files
+27 -64 mpcompiler/mmc/extensions/ext_arithmetic_integer.ml
+4 -4 mpcompiler/mmc/extensions/ext_arithmetic_integer.mli
+9 -5 mpcompiler/mmc/extensions/ext_int_test.ml
+3 -5 mpcompiler/mmc/extensions/ext_integer.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-19 20:46:23 -0700 (Tue, 19 Aug 2003)
Revision: 4852
Log message:

      - Unification should now give something slightly resembling meaningful error messages.
      - Minor clean-ups of recently committed code.
      

Changes  Path
+0 -1 metaprl/library/Makefile
Deleted metaprl/library/lib_term.ml
Deleted metaprl/library/lib_term.mli
+6 -30 metaprl/refiner/refiner/refine.ml
+1 -2 metaprl/refiner/refiner/refine_error.ml
+1 -0 metaprl/refiner/reflib/Files
+0 -3 metaprl/refiner/reflib/dform.ml
Added metaprl/refiner/reflib/lib_term.ml
Properties metaprl/refiner/reflib/lib_term.ml
Added metaprl/refiner/reflib/lib_term.mli
Properties metaprl/refiner/reflib/lib_term.mli
+1 -3 metaprl/refiner/reflib/refine_exn.ml
+163 -213 metaprl/refiner/reflib/unify_mm.ml
+1 -2 metaprl/refiner/refsig/refine_error_sig.ml
+0 -1 metaprl/refiner/refsig/term_addr_sig.ml
+2 -2 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+3 -16 metaprl/refiner/rewrite/rewrite_debug.ml
+0 -2 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+2 -3 metaprl/refiner/rewrite/rewrite_match_redex.ml
+0 -4 metaprl/refiner/term_ds/term_addr_ds.ml
+0 -1 metaprl/refiner/term_gen/term_addr_gen.ml
+1 -1 metaprl/support/shell/shell_rewrite.ml
+1 -1 metaprl/support/shell/shell_rule.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-19 21:34:11 -0700 (Tue, 19 Aug 2003)
Revision: 4853
Log message:

      Added better support for win32.  The main changes are for the C files,
      where a lot of support (like readline, ncurses) is missing.
      

Changes  Path
+15 -11 metaprl/OMakefile
+3 -1 metaprl/clib/OMakefile
+10 -10 metaprl/editor/ml/OMakefile
+0 -1 metaprl/filter/filter/prlcomp.ml
+8 -0 metaprl/theories/itt/itt_int_base.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-19 22:33:17 -0700 (Tue, 19 Aug 2003)
Revision: 4856
Log message:

      util/check_status seems to work.
      

Changes  Path
+2 -2 metaprl/library/OMakefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-20 14:00:16 -0700 (Wed, 20 Aug 2003)
Revision: 4857
Log message:

      Do not allow running make when .omakedb is present.
      

Changes  Path
+20 -6 metaprl/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-20 15:02:44 -0700 (Wed, 20 Aug 2003)
Revision: 4858
Log message:

      Better error message from unify_mm.
      

Changes  Path
+1 -1 metaprl/filter/base/filter_summary.ml
+1 -1 metaprl/refiner/refiner/refine_error.ml
+4 -1 metaprl/refiner/reflib/refine_exn.ml
+14 -11 metaprl/refiner/reflib/unify_mm.ml
+1 -1 metaprl/refiner/refsig/refine_error_sig.ml
+1 -1 metaprl/refiner/term_ds/term_subst_ds.ml
+1 -1 metaprl/refiner/term_std/term_subst_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-20 16:15:03 -0700 (Wed, 20 Aug 2003)
Revision: 4859
Log message:

      mk/config* should not require check_omake.
      

Changes  Path
+2 -2 metaprl/Makefile

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-20 17:28:31 -0700 (Wed, 20 Aug 2003)
Revision: 4860
Log message:

      Type inference is now working on test_prog[1-2].  Haven't tried any other cases
      yet.  Changed simp_typeinf to take a tenv *and* a venv.
      

Changes  Path
+10 -8 metaprl/support/tactics/simp_typeinf.ml
+7 -5 metaprl/support/tactics/simp_typeinf.mli
+1 -1 mpcompiler/mmc/core/core_test.ml
+8 -8 mpcompiler/mmc/core/core_tuple.ml
+69 -59 mpcompiler/mmc/core/mmc_core_type_infer.ml
+4 -4 mpcompiler/mmc/extensions/ext_arithmetic.ml
+1 -1 mpcompiler/mmc/extensions/ext_arithmetic_integer.ml
+11 -11 mpcompiler/mmc/extensions/ext_array.ml
+1 -1 mpcompiler/mmc/extensions/ext_integer.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-20 19:51:56 -0700 (Wed, 20 Aug 2003)
Revision: 4861
Log message:

      Moving [o]make variable defaults into a shared file mk/defaults.
      This should (more-or-less) fix bug 34.
      

Changes  Path
+2 -2 metaprl/Makefile
+22 -17 metaprl/OMakefile
+0 -3 metaprl/clib/OMakefile
+2 -2 metaprl/editor/ml/Makefile
+2 -3 metaprl/editor/ml/OMakefile
Properties metaprl/mk
Added metaprl/mk/config.local.empty
Properties metaprl/mk/config.local.empty
Added metaprl/mk/defaults
Properties metaprl/mk/defaults
+2 -2 metaprl/mk/make_config.sh
+22 -18 metaprl/mk/preface

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-20 20:49:51 -0700 (Wed, 20 Aug 2003)
Revision: 4862
Log message:

      Some OMakefile changes to get MetaPRL to compile.
      

Changes  Path
+21 -23 metaprl/OMakefile
+2 -1 metaprl/theories/fir/OMakefile
+7 -6 metaprl/theories/tptp/OMakefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-20 21:52:45 -0700 (Wed, 20 Aug 2003)
Revision: 4863
Log message:

      Verified that omake restarts when mk/make_config.sh changes.
      

Changes  Path
+24 -15 metaprl/mk/config.win32
+0 -1 metaprl/mk/make_config.sh
+11 -8 metaprl/theories/tptp/OMakefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-20 22:22:45 -0700 (Wed, 20 Aug 2003)
Revision: 4864
Log message:

      Removed the -f option to cvs_realclean, so that removals wil prompt for
      deletion.
      

Changes  Path
+1 -1 metaprl/OMakefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-20 22:56:48 -0700 (Wed, 20 Aug 2003)
Revision: 4865
Log message:

      clean *.a and ensemble/thread_refiner.ml on "omake clean".
      

Changes  Path
+1 -1 metaprl/OMakefile
+1 -1 metaprl/ensemble/OMakefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-21 20:31:41 -0700 (Thu, 21 Aug 2003)
Revision: 4866
Log message:

      This is a hacked commit, to temporarily fix the weak memo problem
      by using arrays instead of weak arrays.  This completely fixes the
      problem as far as I can tell, but of course it may greatly increase
      the amount of memory used by MetaPRL.
      
      Here is my suspicion.  There are two indexes into the weak memo,
      a weak_descriptor (and int), and a descriptor (the int and the value).
      Assumed invariant: a weak_descriptor is live iff the descriptor is live.
      The implementation guarantees that the weak_descriptor is live if the
      descriptor is.  We get into trouble the other way around.  If the
      descriptor goes dead, the value referred to by the weak_descriptor
      will change without notice.
      
      This seems to match the current problem.  I'll do some more investigating.
      

Changes  Path
+6 -5 metaprl/mllib/hash_with_gc.ml
+24 -5 metaprl/mllib/weak_memo.ml
+0 -2 metaprl/theories/itt/itt_int_base.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-21 22:51:28 -0700 (Thu, 21 Aug 2003)
Revision: 4867
Log message:

      Making the refiner interface smaller and more abstract.
      

Changes  Path
+1 -1 metaprl/filter/boot/proof_boot.ml
+2 -2 metaprl/filter/boot/rewrite_boot.ml
+4 -143 metaprl/refiner/refiner/refine.ml
+3 -29 metaprl/refiner/refsig/refine_sig.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-22 16:34:43 -0700 (Fri, 22 Aug 2003)
Revision: 4868
Log message:

      The core of the AST->IR conversion for the M language.
      Next is to add new source-level features to the language (loops, etc.).
      Then I return to the UNITY translation, which should be straightforward
      at that point.
      

Changes  Path
+2 -0 metaprl/theories/experimental/compile/Makefile
+2 -0 metaprl/theories/experimental/compile/OMakefile
+79 -5 metaprl/theories/experimental/compile/m_ast.ml
+71 -4 metaprl/theories/experimental/compile/m_ast.mli
+87 -69 metaprl/theories/experimental/compile/m_ast.pho
Added metaprl/theories/experimental/compile/m_ir_ast.ml
Properties metaprl/theories/experimental/compile/m_ir_ast.ml
Added metaprl/theories/experimental/compile/m_ir_ast.mli
Properties metaprl/theories/experimental/compile/m_ir_ast.mli
+0 -2 metaprl/theories/experimental/compile/m_test.ml
+6 -1 metaprl/theories/experimental/compile/m_theory.ml
+2 -0 metaprl/theories/experimental/compile/m_theory.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-23 05:51:26 -0700 (Sat, 23 Aug 2003)
Revision: 4869
Log message:

      Fix so that omake is happy.
      

Changes  Path
+1 -0 metaprl/theories/experimental/unity/OMakefile

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-23 11:48:53 -0700 (Sat, 23 Aug 2003)
Revision: 4870
Log message:

      Getting closer.
      

Changes  Path
+51 -3 metaprl/theories/experimental/compile/m_ir_ast.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-23 16:01:57 -0700 (Sat, 23 Aug 2003)
Revision: 4871
Log message:

      Display forms for AST terms.
      

Changes  Path
+98 -14 metaprl/theories/experimental/compile/m_ast.ml
+0 -7 metaprl/theories/experimental/compile/m_ast.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-24 04:37:35 -0700 (Sun, 24 Aug 2003)
Revision: 4872
Log message:

      Fixed a bug for non-recursive functions. They were translated to
      ordinary lambdas instead of lambda_p.
      Added a test case for if expressions.
      

Changes  Path
+1 -1 metaprl/theories/experimental/compile/m_ast.ml
+10 -5 metaprl/theories/experimental/compile/m_ast.pho
+1 -1 metaprl/theories/experimental/compile/m_ir_ast.ml
+26 -1 metaprl/theories/experimental/compile/m_test.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-24 05:54:08 -0700 (Sun, 24 Aug 2003)
Revision: 4873
Log message:

      Added test for multi-argument functions.
      

Changes  Path
+4 -4 metaprl/theories/experimental/compile/m_ir_ast.ml
+12 -0 metaprl/theories/experimental/compile/m_test.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-24 10:11:11 -0700 (Sun, 24 Aug 2003)
Revision: 4874
Log message:

      The spill_prog and spill_prog2 test cases now produce the same output.
      This is good, but unfortunately, they both raise an uncaught exception
      in the code generation phase. Jason should look at it.
      

Changes  Path
+9 -0 metaprl/theories/experimental/compile/m_ast.ml
+6 -0 metaprl/theories/experimental/compile/m_ast.mli
+5 -1 metaprl/theories/experimental/compile/m_ast.pho
+7 -8 metaprl/theories/experimental/compile/m_ir_ast.ml
+0 -0 metaprl/theories/experimental/compile/m_test.ml
+1 -1 metaprl/theories/experimental/compile/m_theory.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-24 13:20:55 -0700 (Sun, 24 Aug 2003)
Revision: 4875
Log message:

      I have no idea why ext_test1 and ext_test2 does not compile.
      Can someone look at it and tell me where the IR code is bogus?
      
      To check it out, include experimental/compile in your build,
      and cd into m_test/ext_test[1|2]. Both are AST terms, to convert
      them to IR use the irT tactic, or simply use compileT to try
      to compile them to asm.
      

Changes  Path
+3 -3 metaprl/theories/experimental/compile/m_ir_ast.ml
+1 -1 metaprl/theories/experimental/compile/m_test.ml

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-25 16:17:08 -0700 (Mon, 25 Aug 2003)
Revision: 4876
Log message:

      Matching sequents is now a bit simpler.  You don't need to use "with" clauses to
      match on sequent arguments because now this works correctly:
          match explode_term t with
              << sequent [Lambda] { <args> >- 'e } >>
      
      Also includes some new test cases and random minor changes.
      

Changes  Path
+13 -3 metaprl/filter/filter/filter_patt.ml
+1 -1 metaprl/refiner/refsig/term_sig.ml
+1 -1 metaprl/refiner/term_ds/term_ds.ml
+1 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+4 -2 metaprl/refiner/term_ds/term_man_ds.ml
+4 -2 metaprl/refiner/term_gen/term_man_gen.ml
+1 -1 metaprl/refiner/term_std/term_std.ml
+1 -1 metaprl/refiner/term_std/term_std_sig.ml
+1 -0 mpcompiler/mmc/core/mmc_core_ast.ml
+1 -2 mpcompiler/mmc/core/mmc_core_closure.ml
+5 -1 mpcompiler/mmc/core/mmc_core_cps.ml
+0 -1 mpcompiler/mmc/core/mmc_core_tast.ml
+2 -3 mpcompiler/mmc/core/mmc_core_type_infer.ml
+1 -2 mpcompiler/mmc/core/mmc_core_type_util.ml
+2 -0 mpcompiler/mmc/extensions/ext_arithmetic_integer.mli
+1 -0 mpcompiler/mmc/extensions/ext_array.mli
+74 -6 mpcompiler/mmc/extensions/ext_int_test.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-26 13:06:35 -0700 (Tue, 26 Aug 2003)
Revision: 4878
Log message:

      Switched Phobos to using the libmojave versions of lm_set and lm_map
      instead of locally forked copies.
      

Changes  Path
+0 -2 metaprl/filter/phobos/Files
Deleted metaprl/filter/phobos/mc_map.ml
Deleted metaprl/filter/phobos/mc_map.mli
Deleted metaprl/filter/phobos/mc_set.ml
Deleted metaprl/filter/phobos/mc_set.mli
+16 -16 metaprl/filter/phobos/phobos_type.ml
+18 -493 metaprl/filter/phobos/phobos_type.mli
+1 -1 metaprl/filter/phobos/phobos_util.ml
+148 -147 metaprl/filter/phobos/phobos_util.mli
+4 -3 metaprl/filter/phobos/smap.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-27 02:54:35 -0700 (Wed, 27 Aug 2003)
Revision: 4881
Log message:

      Fix for using Libmojave's map.
      

Changes  Path
+4 -3 metaprl/filter/phobos/phobos_report.ml
+0 -0 metaprl/filter/phobos/phobos_rewrite.ml
+42 -35 metaprl/filter/phobos/phobos_util.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-27 08:25:21 -0700 (Wed, 27 Aug 2003)
Revision: 4882
Log message:

      Added tuples and subscripting.
      Now, the simple tuple test (ext_test3) program compiles.
      

Changes  Path
+13 -1 metaprl/theories/experimental/compile/m_ast.ml
+4 -1 metaprl/theories/experimental/compile/m_ast.mli
+7 -7 metaprl/theories/experimental/compile/m_ast.pho
+53 -0 metaprl/theories/experimental/compile/m_ir_ast.ml
+13 -0 metaprl/theories/experimental/compile/m_test.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-27 12:38:57 -0700 (Wed, 27 Aug 2003)
Revision: 4883
Log message:

      - Removed (using the util/clean-opens script) approx. 2400 unneeded "open"
       statements. This will hopefully reduce the dependency tree size, reduce
      the dependency analysis time during compilation and possibly speed up
      some partial compilations.
      
      - Removed a number of blank lines (MetaPRL policy is to try not to have more
      than one blank line in a row)
      
      - A few minor changes to better disambiguate cases where two modules declare
      a type with the same name and both modules are opened.
      

Changes  Path
+0 -2 metaprl/editor/ml/nuprl_eval.ml
+0 -7 metaprl/editor/ml/nuprl_run.ml
+0 -1 metaprl/editor/ml/nuprl_sig.mlz
+0 -9 metaprl/editor/ml/shell_mp.ml
+1 -3 metaprl/filter/base/filter_ast.ml
+0 -2 metaprl/filter/base/filter_ast.mli
+0 -1 metaprl/filter/base/filter_buffer.ml
+0 -2 metaprl/filter/base/filter_cache.ml
+0 -1 metaprl/filter/base/filter_cache.mli
+0 -4 metaprl/filter/base/filter_cache_fun.ml
+0 -1 metaprl/filter/base/filter_cache_fun.mli
+0 -2 metaprl/filter/base/filter_comment.ml
+0 -3 metaprl/filter/base/filter_exn.ml
+0 -2 metaprl/filter/base/filter_exn.mli
+0 -2 metaprl/filter/base/filter_grammar.ml
+0 -1 metaprl/filter/base/filter_hash.ml
+0 -1 metaprl/filter/base/filter_magic.ml
+0 -1 metaprl/filter/base/filter_ocaml.mli
+0 -2 metaprl/filter/base/filter_summary.ml
+0 -1 metaprl/filter/base/filter_summary.mli
+0 -1 metaprl/filter/base/filter_summary_io.ml
+0 -2 metaprl/filter/base/filter_summary_io.mli
+0 -1 metaprl/filter/base/filter_summary_type.ml
+0 -3 metaprl/filter/base/filter_summary_util.ml
+0 -1 metaprl/filter/base/filter_summary_util.mli
+0 -4 metaprl/filter/base/filter_util.ml
+0 -1 metaprl/filter/base/filter_util.mli
+0 -1 metaprl/filter/base/infix.mli
+0 -1 metaprl/filter/base/mLast_util.ml
+0 -5 metaprl/filter/boot/conversionals_boot.ml
+0 -8 metaprl/filter/boot/proof_boot.ml
+0 -1 metaprl/filter/boot/proof_boot.mli
+0 -4 metaprl/filter/boot/proof_convert.ml
+0 -1 metaprl/filter/boot/proof_term_boot.ml
+0 -1 metaprl/filter/boot/proof_term_boot.mli
+0 -4 metaprl/filter/boot/rewrite_boot.ml
+0 -1 metaprl/filter/boot/sequent_boot.ml
+0 -5 metaprl/filter/boot/tactic_boot.ml
+0 -7 metaprl/filter/boot/tactic_boot_sig.mlz
+0 -1 metaprl/filter/boot/tactic_type.mli
+0 -3 metaprl/filter/boot/tacticals_boot.ml
+0 -1 metaprl/filter/boot/tacticals_boot.mli
+0 -2 metaprl/filter/filter/filter_bin.ml
+0 -6 metaprl/filter/filter/filter_convert.ml
+0 -5 metaprl/filter/filter/filter_parse.ml
+0 -1 metaprl/filter/filter/filter_parse.mli
+0 -7 metaprl/filter/filter/filter_patt.ml
+0 -1 metaprl/filter/filter/filter_patt.mli
+0 -5 metaprl/filter/filter/filter_prog.ml
+0 -1 metaprl/filter/filter/filter_prog.mli
+0 -6 metaprl/filter/filter/term_grammar.ml
+0 -3 metaprl/filter/filter/term_grammar.mli
+0 -1 metaprl/filter/phobos/filter_phobos.ml
+0 -2 metaprl/filter/phobos/phobos_compile.ml
+0 -2 metaprl/filter/phobos/phobos_exn.ml
+0 -2 metaprl/filter/phobos/phobos_exn.mli
+0 -2 metaprl/filter/phobos/phobos_grammar.ml
+0 -1 metaprl/filter/phobos/phobos_lexer.mll
+0 -5 metaprl/filter/phobos/phobos_main.ml
+0 -1 metaprl/filter/phobos/phobos_parse_state.ml
+0 -1 metaprl/filter/phobos/phobos_report.mli
+0 -3 metaprl/filter/phobos/phobos_rewrite.ml
+0 -4 metaprl/filter/phobos/phobos_rewrite.mli
+0 -4 metaprl/filter/phobos/phobos_token_inheritance.ml
+0 -6 metaprl/filter/phobos/phobos_token_inheritance.mli
+0 -2 metaprl/filter/phobos/phobos_tokenizer.ml
+0 -0 metaprl/filter/phobos/phobos_util.ml
+0 -1 metaprl/library/ascii_scan.ml
+0 -4 metaprl/library/basic.ml
+0 -1 metaprl/library/basic.mli
+225 -228 metaprl/library/db.ml
+0 -1 metaprl/library/definition.ml
+0 -2 metaprl/library/library.ml
+0 -1 metaprl/library/library_type_base.ml
+0 -1 metaprl/library/link.ml
+22 -23 metaprl/library/lint32.ml
+22 -22 metaprl/library/lint32.mli
+16 -17 metaprl/library/mathBus.ml
+23 -24 metaprl/library/mathBus.mli
+1 -3 metaprl/library/mbterm.ml
+0 -1 metaprl/library/mbterm.mli
+0 -3 metaprl/library/nuprl5.ml
+4 -5 metaprl/library/oidtable.ml
+0 -3 metaprl/library/orb.ml
+1 -2 metaprl/library/orb.mli
+5 -7 metaprl/library/registry.ml
+4 -4 metaprl/library/registry.mli
+0 -1 metaprl/library/socketIo.ml
+0 -1 metaprl/library/tentfunctor.ml
+0 -2 metaprl/library/utils.ml
+0 -1 metaprl/library/utils.mli
+0 -1 metaprl/mllib/bitset.ml
+0 -1 metaprl/mllib/file_type_base.ml
+0 -1 metaprl/mllib/precedence.ml
+0 -1 metaprl/mllib/weak_memo.ml
+0 -2 metaprl/refiner/refbase/opname.ml
+0 -1 metaprl/refiner/refiner/refine.ml
+0 -1 metaprl/refiner/refiner/refiner_ds.ml
+0 -2 metaprl/refiner/refiner/refiner_ds.mli
+0 -1 metaprl/refiner/refiner/refiner_std.ml
+0 -2 metaprl/refiner/refiner/refiner_std.mli
+0 -1 metaprl/refiner/reflib/arith.ml
+0 -1 metaprl/refiner/reflib/dform.ml
+0 -1 metaprl/refiner/reflib/dform.mli
+0 -1 metaprl/refiner/reflib/dform_print.ml
+0 -3 metaprl/refiner/reflib/dform_print.mli
+0 -1 metaprl/refiner/reflib/jall.ml
+0 -3 metaprl/refiner/reflib/jall.mli
+0 -4 metaprl/refiner/reflib/jlogic_sig.ml
+0 -6 metaprl/refiner/reflib/ml_file.ml
+0 -2 metaprl/refiner/reflib/ml_format.ml
+0 -1 metaprl/refiner/reflib/ml_format_sig.mlz
+0 -3 metaprl/refiner/reflib/ml_print.ml
+0 -1 metaprl/refiner/reflib/ml_print_sig.mlz
+0 -2 metaprl/refiner/reflib/ml_string.ml
+0 -3 metaprl/refiner/reflib/ml_term.ml
+0 -1 metaprl/refiner/reflib/ml_term.mli
+0 -1 metaprl/refiner/reflib/mp_resource.ml
+0 -1 metaprl/refiner/reflib/mp_resource.mli
+0 -4 metaprl/refiner/reflib/refine_exn.ml
+0 -1 metaprl/refiner/reflib/refine_exn.mli
+0 -1 metaprl/refiner/reflib/simple_print.ml
+0 -1 metaprl/refiner/reflib/simple_print_sig.ml
+0 -2 metaprl/refiner/reflib/term_compare.ml
+0 -1 metaprl/refiner/reflib/term_compare.mli
+0 -1 metaprl/refiner/reflib/term_copy2_weak.ml
+0 -1 metaprl/refiner/reflib/term_copy_weak.ml
+0 -4 metaprl/refiner/reflib/term_dtable.ml
+0 -1 metaprl/refiner/reflib/term_eq_table.ml
+0 -1 metaprl/refiner/reflib/term_io.ml
+0 -2 metaprl/refiner/reflib/term_match_table.ml
+0 -1 metaprl/refiner/reflib/term_match_table.mli
+0 -3 metaprl/refiner/reflib/term_stable.ml
+0 -2 metaprl/refiner/reflib/theory.ml
+0 -4 metaprl/refiner/reflib/unify_mm.ml
+0 -3 metaprl/refiner/reflib/unify_mm.mli
+0 -3 metaprl/refiner/refsig/refiner_sig.ml
+0 -1 metaprl/refiner/refsig/term_base_minimal_sig.ml
+0 -1 metaprl/refiner/refsig/term_hash_sig.ml
+0 -1 metaprl/refiner/refsig/term_sig.ml
+0 -1 metaprl/refiner/refsig/termmod_hash_sig.ml
+0 -1 metaprl/refiner/refsig/termmod_sig.ml
+0 -4 metaprl/refiner/rewrite/rewrite.ml
+0 -1 metaprl/refiner/rewrite/rewrite.mli
+0 -4 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+0 -1 metaprl/refiner/rewrite/rewrite_build_contractum.mli
+0 -4 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+0 -1 metaprl/refiner/rewrite/rewrite_compile_contractum.mli
+0 -5 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+0 -1 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+0 -1 metaprl/refiner/rewrite/rewrite_debug.ml
+0 -1 metaprl/refiner/rewrite/rewrite_debug.mli
+0 -1 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+0 -1 metaprl/refiner/rewrite/rewrite_match_redex.mli
+0 -3 metaprl/refiner/rewrite/rewrite_meta.ml
+0 -2 metaprl/refiner/rewrite/rewrite_meta.mli
+0 -1 metaprl/refiner/rewrite/rewrite_types.mli
+0 -3 metaprl/refiner/rewrite/rewrite_util.ml
+0 -1 metaprl/refiner/rewrite/rewrite_util.mli
+0 -3 metaprl/refiner/term_ds/term_addr_ds.ml
+0 -2 metaprl/refiner/term_ds/term_base_ds.mli
+0 -1 metaprl/refiner/term_ds/term_ds.ml
+0 -2 metaprl/refiner/term_ds/term_ds_sig.ml
+0 -1 metaprl/refiner/term_ds/term_man_ds.ml
+0 -3 metaprl/refiner/term_gen/term_addr_gen.ml
+0 -3 metaprl/refiner/term_gen/term_hash.ml
+0 -1 metaprl/refiner/term_gen/term_hash.mli
+0 -8 metaprl/refiner/term_gen/term_header_constr.ml
+0 -1 metaprl/refiner/term_gen/term_header_constr.mli
+0 -1 metaprl/refiner/term_gen/term_man_gen.ml
+0 -1 metaprl/refiner/term_gen/term_man_gen.mli
+0 -1 metaprl/refiner/term_gen/term_meta_gen.ml
+0 -2 metaprl/refiner/term_gen/term_norm.ml
+0 -1 metaprl/refiner/term_gen/term_norm.mli
+0 -1 metaprl/refiner/term_std/term_base_std.ml
+0 -2 metaprl/refiner/term_std/term_base_std.mli
+0 -1 metaprl/refiner/term_std/term_eval_std.ml
+0 -1 metaprl/refiner/term_std/term_op_std.ml
+0 -2 metaprl/refiner/term_std/term_std.ml
+0 -2 metaprl/refiner/term_std/term_std_sig.ml
+0 -2 metaprl/support/display/base_dform.ml
+0 -2 metaprl/support/display/nuprl_font.ml
+0 -2 metaprl/support/display/ocaml_base_df.ml
+0 -1 metaprl/support/display/ocaml_expr_df.ml
+0 -1 metaprl/support/display/ocaml_me_df.ml
+0 -1 metaprl/support/display/ocaml_mt_df.ml
+0 -1 metaprl/support/display/ocaml_patt_df.ml
+0 -1 metaprl/support/display/ocaml_sig_df.ml
+0 -1 metaprl/support/display/ocaml_str_df.ml
+0 -1 metaprl/support/display/ocaml_type_df.ml
+0 -3 metaprl/support/display/perv.ml
+0 -3 metaprl/support/display/summary.ml
+0 -4 metaprl/support/shell/display_term.ml
+0 -4 metaprl/support/shell/mptop.ml
+0 -2 metaprl/support/shell/mptop.mli
+0 -6 metaprl/support/shell/package_info.ml
+3 -6 metaprl/support/shell/package_sig.mlz
+0 -5 metaprl/support/shell/proof_edit.ml
+0 -1 metaprl/support/shell/proof_edit.mli
+0 -2 metaprl/support/shell/shell.ml
+0 -5 metaprl/support/shell/shell_p4_sig.mlz
+0 -4 metaprl/support/shell/shell_package.ml
+0 -7 metaprl/support/shell/shell_rewrite.ml
+0 -2 metaprl/support/shell/shell_root.ml
+0 -8 metaprl/support/shell/shell_rule.ml
+0 -3 metaprl/support/shell/shell_sig.mlz
+0 -2 metaprl/support/shell/shell_state.ml
+0 -3 metaprl/support/shell/shell_state.mli
+0 -7 metaprl/support/tactics/auto_tactic.ml
+0 -4 metaprl/support/tactics/auto_tactic.mli
+0 -1 metaprl/support/tactics/base_cache.ml
+0 -1 metaprl/support/tactics/base_cache.mli
+0 -1 metaprl/support/tactics/dtactic.ml
+0 -1 metaprl/support/tactics/dtactic.mli
+0 -10 metaprl/support/tactics/simp_typeinf.ml
+0 -2 metaprl/support/tactics/simp_typeinf.mli
+0 -2 metaprl/support/tactics/tactic_cache.ml
+0 -1 metaprl/support/tactics/tactic_cache.mli
+0 -4 metaprl/support/tactics/top_conversionals.ml
+0 -2 metaprl/support/tactics/top_conversionals.mli
+0 -1 metaprl/support/tactics/top_tacticals.ml
+2 -6 metaprl/support/tactics/top_tacticals.mli
+0 -4 metaprl/support/tactics/typeinf.ml
+0 -2 metaprl/support/tactics/typeinf.mli
+0 -2 metaprl/support/tactics/var.ml
+0 -9 metaprl/theories/base/base_rewrite.ml
+0 -1 metaprl/theories/base/base_rewrite.mli
+0 -17 metaprl/theories/czf/czf_itt_abel_group.ml
+0 -19 metaprl/theories/czf/czf_itt_abel_group.mli
+0 -16 metaprl/theories/czf/czf_itt_all.ml
+0 -8 metaprl/theories/czf/czf_itt_and.ml
+0 -3 metaprl/theories/czf/czf_itt_axioms.ml
+0 -19 metaprl/theories/czf/czf_itt_bool.ml
+0 -2 metaprl/theories/czf/czf_itt_bool.mli
+0 -14 metaprl/theories/czf/czf_itt_coset.ml
+0 -16 metaprl/theories/czf/czf_itt_coset.mli
+0 -17 metaprl/theories/czf/czf_itt_cyclic_group.ml
+0 -19 metaprl/theories/czf/czf_itt_cyclic_group.mli
+0 -17 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+0 -18 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+0 -6 metaprl/theories/czf/czf_itt_dall.ml
+0 -1 metaprl/theories/czf/czf_itt_dall.mli
+0 -6 metaprl/theories/czf/czf_itt_dexists.ml
+0 -1 metaprl/theories/czf/czf_itt_dexists.mli
+0 -4 metaprl/theories/czf/czf_itt_empty.ml
+0 -5 metaprl/theories/czf/czf_itt_eq.ml
+0 -8 metaprl/theories/czf/czf_itt_equiv.ml
+0 -23 metaprl/theories/czf/czf_itt_equiv.mli
+0 -16 metaprl/theories/czf/czf_itt_exists.ml
+0 -4 metaprl/theories/czf/czf_itt_false.ml
+0 -18 metaprl/theories/czf/czf_itt_group.ml
+0 -18 metaprl/theories/czf/czf_itt_group.mli
+0 -18 metaprl/theories/czf/czf_itt_group_bvd.ml
+0 -20 metaprl/theories/czf/czf_itt_group_bvd.mli
+0 -17 metaprl/theories/czf/czf_itt_group_power.ml
+0 -19 metaprl/theories/czf/czf_itt_group_power.mli
+0 -18 metaprl/theories/czf/czf_itt_hom.ml
+0 -17 metaprl/theories/czf/czf_itt_hom.mli
+0 -8 metaprl/theories/czf/czf_itt_implies.ml
+0 -16 metaprl/theories/czf/czf_itt_inv_image.ml
+0 -18 metaprl/theories/czf/czf_itt_inv_image.mli
+0 -7 metaprl/theories/czf/czf_itt_isect.ml
+0 -18 metaprl/theories/czf/czf_itt_iso.ml
+0 -20 metaprl/theories/czf/czf_itt_iso.mli
+0 -18 metaprl/theories/czf/czf_itt_ker.ml
+0 -17 metaprl/theories/czf/czf_itt_ker.mli
+0 -18 metaprl/theories/czf/czf_itt_kleingroup.ml
+0 -20 metaprl/theories/czf/czf_itt_kleingroup.mli
+0 -7 metaprl/theories/czf/czf_itt_member.ml
+0 -1 metaprl/theories/czf/czf_itt_member.mli
+0 -4 metaprl/theories/czf/czf_itt_nat.ml
+0 -1 metaprl/theories/czf/czf_itt_nat.mli
+0 -14 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+0 -14 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+0 -8 metaprl/theories/czf/czf_itt_or.ml
+0 -1 metaprl/theories/czf/czf_itt_power.ml
+0 -1 metaprl/theories/czf/czf_itt_power.mli
+0 -2 metaprl/theories/czf/czf_itt_rel.ml
+0 -6 metaprl/theories/czf/czf_itt_sall.ml
+0 -1 metaprl/theories/czf/czf_itt_sall.mli
+0 -6 metaprl/theories/czf/czf_itt_sep.ml
+0 -1 metaprl/theories/czf/czf_itt_sep.mli
+0 -14 metaprl/theories/czf/czf_itt_set.ml
+0 -2 metaprl/theories/czf/czf_itt_set.mli
+0 -16 metaprl/theories/czf/czf_itt_set_bvd.ml
+0 -19 metaprl/theories/czf/czf_itt_set_bvd.mli
+0 -5 metaprl/theories/czf/czf_itt_set_ind.ml
+0 -18 metaprl/theories/czf/czf_itt_setdiff.ml
+0 -9 metaprl/theories/czf/czf_itt_setdiff.mli
+0 -6 metaprl/theories/czf/czf_itt_sexists.ml
+0 -4 metaprl/theories/czf/czf_itt_singleton.ml
+0 -14 metaprl/theories/czf/czf_itt_subgroup.ml
+0 -11 metaprl/theories/czf/czf_itt_subgroup.mli
+0 -4 metaprl/theories/czf/czf_itt_true.ml
+0 -6 metaprl/theories/czf/czf_itt_union.ml
+0 -2 metaprl/theories/experimental/compile/m_ast.ml
+0 -2 metaprl/theories/experimental/compile/m_ast.mli
+0 -6 metaprl/theories/experimental/compile/m_closure.ml
+0 -1 metaprl/theories/experimental/compile/m_closure.mli
+0 -8 metaprl/theories/experimental/compile/m_cps.ml
+0 -3 metaprl/theories/experimental/compile/m_cps.mli
+0 -2 metaprl/theories/experimental/compile/m_dead.ml
+0 -1 metaprl/theories/experimental/compile/m_dead.mli
+0 -1 metaprl/theories/experimental/compile/m_ir_ast.ml
+0 -3 metaprl/theories/experimental/compile/m_ir_ast.mli
+0 -11 metaprl/theories/experimental/compile/m_prog.ml
+0 -2 metaprl/theories/experimental/compile/m_prog.mli
+0 -3 metaprl/theories/experimental/compile/m_ra_main.ml
+0 -1 metaprl/theories/experimental/compile/m_standardize.ml
+0 -0 metaprl/theories/experimental/compile/m_test.ml
+0 -2 metaprl/theories/experimental/compile/m_theory.ml
+0 -2 metaprl/theories/experimental/compile/m_util.ml
+0 -5 metaprl/theories/experimental/compile/m_x86_codegen.ml
+0 -2 metaprl/theories/experimental/compile/m_x86_codegen.mli
+0 -1 metaprl/theories/experimental/compile/m_x86_frame.ml
+0 -1 metaprl/theories/experimental/compile/m_x86_opt.ml
+0 -1 metaprl/theories/experimental/compile/m_x86_opt.mli
+0 -3 metaprl/theories/experimental/compile/m_x86_regalloc.ml
+0 -7 metaprl/theories/experimental/compile/m_x86_spill.ml
+0 -3 metaprl/theories/experimental/compile/m_x86_spill.mli
+0 -2 metaprl/theories/experimental/compile/m_x86_term.ml
+0 -1 metaprl/theories/fir/mfir_termOp_base.ml
+0 -1 metaprl/theories/fir/mfir_token.ml
+0 -1 metaprl/theories/fir/mfir_ty.ml
+0 -1 metaprl/theories/fir/mfir_ty.mli
+0 -2 metaprl/theories/fol/cfol_itt_base.ml
+0 -1 metaprl/theories/fol/cfol_itt_base.mli
+0 -1 metaprl/theories/fol/cfol_magic.ml
+0 -1 metaprl/theories/fol/fol_false.ml
+0 -1 metaprl/theories/fol/fol_pred.ml
+0 -1 metaprl/theories/fol/fol_prop.ml
+0 -16 metaprl/theories/itt/ctt_markov.ml
+0 -15 metaprl/theories/itt/itt_algebra_df.ml
+0 -7 metaprl/theories/itt/itt_atom.ml
+0 -5 metaprl/theories/itt/itt_atom_bool.ml
+0 -15 metaprl/theories/itt/itt_bintree.ml
+0 -20 metaprl/theories/itt/itt_bintree.mli
+0 -8 metaprl/theories/itt/itt_bisect.ml
+0 -7 metaprl/theories/itt/itt_bool.ml
+0 -1 metaprl/theories/itt/itt_bool.mli
+0 -10 metaprl/theories/itt/itt_bunion.ml
+0 -10 metaprl/theories/itt/itt_collection.ml
+0 -6 metaprl/theories/itt/itt_collection.mli
+0 -18 metaprl/theories/itt/itt_cyclic_group.ml
+0 -19 metaprl/theories/itt/itt_cyclic_group.mli
+0 -15 metaprl/theories/itt/itt_datatree.ml
+0 -4 metaprl/theories/itt/itt_datatree.mli
+0 -8 metaprl/theories/itt/itt_decidable.ml
+0 -2 metaprl/theories/itt/itt_decidable.mli
+0 -4 metaprl/theories/itt/itt_derive.ml
+0 -12 metaprl/theories/itt/itt_dfun.ml
+0 -1 metaprl/theories/itt/itt_dfun.mli
+0 -7 metaprl/theories/itt/itt_disect.ml
+0 -11 metaprl/theories/itt/itt_dprod.ml
+0 -1 metaprl/theories/itt/itt_dprod.mli
+0 -6 metaprl/theories/itt/itt_equal.ml
+0 -3 metaprl/theories/itt/itt_equal.mli
+0 -1 metaprl/theories/itt/itt_esquash.mli
+0 -1 metaprl/theories/itt/itt_eta.mli
+0 -3 metaprl/theories/itt/itt_ext_equal.ml
+0 -1 metaprl/theories/itt/itt_ext_equal.mli
+0 -7 metaprl/theories/itt/itt_fset.ml
+0 -1 metaprl/theories/itt/itt_fset.mli
+0 -5 metaprl/theories/itt/itt_fun.ml
+0 -1 metaprl/theories/itt/itt_fun.mli
+0 -20 metaprl/theories/itt/itt_group.ml
+0 -19 metaprl/theories/itt/itt_group.mli
+0 -20 metaprl/theories/itt/itt_grouplikeobj.ml
+0 -19 metaprl/theories/itt/itt_grouplikeobj.mli
+0 -5 metaprl/theories/itt/itt_int_arith.ml
+0 -4 metaprl/theories/itt/itt_int_arith.mli
+0 -7 metaprl/theories/itt/itt_int_base.ml
+0 -2 metaprl/theories/itt/itt_int_base.mli
+0 -13 metaprl/theories/itt/itt_int_ext.ml
+0 -1 metaprl/theories/itt/itt_int_ext.mli
+0 -13 metaprl/theories/itt/itt_inv_typing.ml
+0 -15 metaprl/theories/itt/itt_inv_typing.mli
+0 -4 metaprl/theories/itt/itt_isect.ml
+0 -1 metaprl/theories/itt/itt_isect.mli
+0 -11 metaprl/theories/itt/itt_list.ml
+0 -1 metaprl/theories/itt/itt_list.mli
+0 -11 metaprl/theories/itt/itt_list2.ml
+0 -1 metaprl/theories/itt/itt_list2.mli
+0 -4 metaprl/theories/itt/itt_logic.ml
+0 -1 metaprl/theories/itt/itt_logic.mli
+0 -16 metaprl/theories/itt/itt_nat.ml
+0 -15 metaprl/theories/itt/itt_pointwise.ml
+0 -16 metaprl/theories/itt/itt_pointwise2.ml
+0 -5 metaprl/theories/itt/itt_prec.ml
+0 -9 metaprl/theories/itt/itt_prod.ml
+0 -1 metaprl/theories/itt/itt_prod.mli
+0 -3 metaprl/theories/itt/itt_prop_decide.ml
+0 -4 metaprl/theories/itt/itt_quotient.ml
+0 -13 metaprl/theories/itt/itt_rbtree.ml
+0 -4 metaprl/theories/itt/itt_rbtree.mli
+0 -11 metaprl/theories/itt/itt_record.ml
+0 -2 metaprl/theories/itt/itt_record.mli
+0 -15 metaprl/theories/itt/itt_record0.ml
+0 -4 metaprl/theories/itt/itt_record0.mli
+0 -16 metaprl/theories/itt/itt_record_exm.ml
+0 -4 metaprl/theories/itt/itt_record_exm.mli
+0 -13 metaprl/theories/itt/itt_record_label.ml
+0 -2 metaprl/theories/itt/itt_record_label.mli
+0 -8 metaprl/theories/itt/itt_record_label0.ml
+0 -4 metaprl/theories/itt/itt_record_label0.mli
+0 -15 metaprl/theories/itt/itt_relation_str.ml
+0 -2 metaprl/theories/itt/itt_relation_str.mli
+0 -11 metaprl/theories/itt/itt_rfun.ml
+0 -11 metaprl/theories/itt/itt_set.ml
+0 -1 metaprl/theories/itt/itt_set.mli
+0 -17 metaprl/theories/itt/itt_set_str.ml
+0 -4 metaprl/theories/itt/itt_set_str.mli
+0 -21 metaprl/theories/itt/itt_singleton.ml
+0 -5 metaprl/theories/itt/itt_sort.ml
+0 -1 metaprl/theories/itt/itt_sort.mli
+0 -12 metaprl/theories/itt/itt_sortedtree.ml
+0 -4 metaprl/theories/itt/itt_sortedtree.mli
+0 -3 metaprl/theories/itt/itt_squash.ml
+0 -1 metaprl/theories/itt/itt_squash.mli
+0 -9 metaprl/theories/itt/itt_squiggle.ml
+0 -3 metaprl/theories/itt/itt_squiggle.mli
+1 -9 metaprl/theories/itt/itt_srec.ml
+0 -8 metaprl/theories/itt/itt_struct.ml
+0 -1 metaprl/theories/itt/itt_struct.mli
+0 -8 metaprl/theories/itt/itt_struct2.ml
+0 -1 metaprl/theories/itt/itt_struct2.mli
+0 -14 metaprl/theories/itt/itt_struct3.ml
+0 -15 metaprl/theories/itt/itt_struct3.mli
+0 -17 metaprl/theories/itt/itt_subset.ml
+0 -1 metaprl/theories/itt/itt_subset.mli
+0 -23 metaprl/theories/itt/itt_subset2.ml
+0 -4 metaprl/theories/itt/itt_subset2.mli
+0 -5 metaprl/theories/itt/itt_subtype.ml
+0 -1 metaprl/theories/itt/itt_subtype.mli
+0 -2 metaprl/theories/itt/itt_theory.ml
+0 -12 metaprl/theories/itt/itt_tsquash.ml
+0 -4 metaprl/theories/itt/itt_tunion.ml
+0 -9 metaprl/theories/itt/itt_union.ml
+0 -1 metaprl/theories/itt/itt_union.mli
+0 -1 metaprl/theories/itt/itt_union2.ml
+0 -8 metaprl/theories/itt/itt_unit.ml
+0 -1 metaprl/theories/itt/itt_unit.mli
+0 -6 metaprl/theories/itt/itt_void.ml
+0 -1 metaprl/theories/itt/itt_void.mli
+0 -10 metaprl/theories/itt/itt_w.ml
+0 -2 metaprl/theories/ocaml_doc/ocaml_doc_mod1.ml
+0 -2 metaprl/theories/phobos/phobos_base.ml
+0 -5 metaprl/theories/phobos/phobos_base.mli
+0 -2 metaprl/theories/sil/sil_itt_sos.ml
+0 -1 metaprl/theories/sil/sil_itt_sos.mli
+0 -4 metaprl/theories/tptp/tptp.ml
+0 -1 metaprl/theories/tptp/tptp.mli
+0 -2 metaprl/theories/tptp/tptp_cache.ml
+0 -2 metaprl/theories/tptp/tptp_load.ml
+0 -1 metaprl/theories/tptp/tptp_parse.mly
+0 -5 metaprl/theories/tptp/tptp_prove.ml
+0 -2 metaprl/theories/tptp/tptp_prove.mli
Added metaprl/util/clean-opens
Properties metaprl/util/clean-opens
+0 -1 metaprl/util/ocamldep.mll
+0 -4 mpcompiler/mmc/core/core_sequent.ml
+0 -2 mpcompiler/mmc/core/core_sequent.mli
+0 -10 mpcompiler/mmc/core/core_tuple.ml
+0 -3 mpcompiler/mmc/core/mmc_core_closure.ml
+0 -1 mpcompiler/mmc/core/mmc_core_cps.mli
+0 -1 mpcompiler/mmc/core/mmc_core_name.ml
+0 -2 mpcompiler/mmc/core/mmc_core_name.mli
+0 -6 mpcompiler/mmc/core/mmc_core_type_check.ml
+0 -2 mpcompiler/mmc/core/mmc_core_type_erase.ml
+0 -2 mpcompiler/mmc/core/mmc_core_type_erase.mli
+0 -6 mpcompiler/mmc/core/mmc_core_type_infer.ml
+0 -3 mpcompiler/mmc/core/mmc_core_type_infer.mli
+0 -2 mpcompiler/mmc/core/mmc_core_type_util.ml
+0 -1 mpcompiler/mmc/core/mmc_core_type_util.mli
+0 -2 mpcompiler/mmc/core/mmc_core_util.ml
+0 -17 mpcompiler/mmc/extensions/ext_arithmetic.ml
+0 -22 mpcompiler/mmc/extensions/ext_arithmetic_integer.ml
+0 -17 mpcompiler/mmc/extensions/ext_array.ml
+0 -3 mpcompiler/mmc/extensions/ext_integer.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-27 13:41:53 -0700 (Wed, 27 Aug 2003)
Revision: 4884
Log message:

      Added assignments. The source language has everything we need.
      Now, the rest of the compiler needs work.
      

Changes  Path
+10 -8 metaprl/theories/experimental/compile/m_ast.ml
+1 -2 metaprl/theories/experimental/compile/m_ast.mli
+6 -10 metaprl/theories/experimental/compile/m_ast.pho
+13 -0 metaprl/theories/experimental/compile/m_ir_ast.ml
+7 -0 metaprl/theories/experimental/compile/m_test.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-27 13:50:54 -0700 (Wed, 27 Aug 2003)
Revision: 4885
Log message:

      Added code to do CPS on assignment.
      

Changes  Path
+4 -0 metaprl/theories/experimental/compile/m_cps.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-27 13:57:20 -0700 (Wed, 27 Aug 2003)
Revision: 4886
Log message:

      Aleksey's jumbo commit to rid of all unnecessary open's is too
      optimistic. There are modules that are opened for side-effect...
      

Changes  Path
+1 -0 metaprl/editor/ml/shell_mp.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-27 14:45:03 -0700 (Wed, 27 Aug 2003)
Revision: 4887
Log message:

      Removed an unused precedence directive.
      
      Aleksey:
      You have to do a 'make clean' when .pho files change to clear out .cph
      files. Otherwise, Phobos uses the saved grammars to parse and not the
      source grammars.
      Eventually, grammars will be embedded in the theory files, so this
      hack will go away.
      

Changes  Path
+0 -1 metaprl/theories/experimental/compile/m_ast.pho

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-27 14:55:44 -0700 (Wed, 27 Aug 2003)
Revision: 4888
Log message:

      Use the correct version string.
      

Changes  Path
+1 -2 metaprl/editor/ml/shell_mp.ml
+1 -2 metaprl/editor/ml/shell_p4.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-27 17:09:33 -0700 (Wed, 27 Aug 2003)
Revision: 4889
Log message:

      - Phobos warnings should go to stderr, not stdout. Otherwise they end up
      in the .ppo file (at least in omake compile) causing it to become corrupted.
      
      - "omake clean" in theories/experimental/compile should know to delete *.cph
      

Changes  Path
+1 -1 metaprl/filter/phobos/phobos_util.ml
+1 -1 metaprl/theories/experimental/compile/OMakefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-27 22:26:19 -0700 (Wed, 27 Aug 2003)
Revision: 4890
Log message:

      Resource annotation processor has no business having access to extract args.
      

Changes  Path
+3 -3 metaprl/filter/filter/filter_prog.ml
+3 -4 metaprl/refiner/reflib/mp_resource.ml
+3 -4 metaprl/refiner/reflib/mp_resource.mli
+2 -2 metaprl/support/tactics/dtactic.ml
+1 -1 metaprl/theories/itt/itt_equal.ml
+1 -1 metaprl/theories/itt/itt_squash.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-28 00:35:45 -0700 (Thu, 28 Aug 2003)
Revision: 4893
Log message:

      Do not pass fake extract args when creating non-prim rules.
      

Changes  Path
+6 -8 metaprl/filter/base/filter_util.ml
+8 -18 metaprl/filter/filter/filter_prog.ml
+35 -7 metaprl/refiner/refiner/refine.ml
+4 -4 metaprl/refiner/refsig/refine_sig.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-28 16:59:07 -0700 (Thu, 28 Aug 2003)
Revision: 4894
Log message:

      The ext: quotation uses the default grammar file 'syntax.pho'.
      

Changes  Path
+2 -2 metaprl/filter/phobos/phobos_state.ml
Deleted metaprl/theories/experimental/compile/m_ast.pho
Added metaprl/theories/experimental/compile/syntax.pho
Properties metaprl/theories/experimental/compile/syntax.pho

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-28 17:09:07 -0700 (Thu, 28 Aug 2003)
Revision: 4895
Log message:

      This is another major re-arrangement of directories (hopefully,
      the last one - at least until we start working on a shared installation mode)
      that I've been planning for a while.
      
      Basically, I moved the high-level proof/tactic layer into the tactics top-level
      directory (my major objection was that it had absolutely no business being in
      filter/boot - the tactic layer has nothing to do with parsing/compiling MetaPRL
      files).
      
      In short this, commit moves:
       - filter/boot -> tactics/proof
       - ensemble -> tactics/null, tactics/ensemble (splitting the directory
      into separate ones for the distributed and sequential versions).
      

Changes  Path
+3 -2 metaprl/Makefile
+10 -1 metaprl/OMakefile
+15 -36 metaprl/editor/ml/Makefile
+26 -35 metaprl/editor/ml/OMakefile
+4 -5 metaprl/filter/Makefile
+3 -4 metaprl/filter/OMakefile
+1 -0 metaprl/filter/base/filter_cache.ml
+1 -0 metaprl/filter/base/filter_cache.mli
+0 -15 metaprl/filter/base/filter_summary_type.ml
+0 -1 metaprl/filter/filter/OMakefile
+1 -1 metaprl/filter/phobos/Makefile
+0 -1 metaprl/filter/phobos/OMakefile
+5 -0 metaprl/mk/preface
+2 -1 metaprl/refiner/refsig/Files
+1 -0 metaprl/refiner/refsig/OMakefile
Added metaprl/refiner/refsig/thread_refiner_sig.ml
Properties metaprl/refiner/refsig/thread_refiner_sig.ml
Properties metaprl/tactics/ensemble
Added metaprl/tactics/ensemble/Makefile
Properties metaprl/tactics/ensemble/Makefile
Added metaprl/tactics/ensemble/OMakefile
Properties metaprl/tactics/ensemble/OMakefile
Added metaprl/tactics/ensemble/appl_closure.ml
Properties metaprl/tactics/ensemble/appl_closure.ml
Added metaprl/tactics/ensemble/appl_closure.mli
Properties metaprl/tactics/ensemble/appl_closure.mli
Added metaprl/tactics/ensemble/appl_ensemble.ml
Properties metaprl/tactics/ensemble/appl_ensemble.ml
Added metaprl/tactics/ensemble/appl_ensemble.mli
Properties metaprl/tactics/ensemble/appl_ensemble.mli
Added metaprl/tactics/ensemble/appl_outboard_client.ml
Properties metaprl/tactics/ensemble/appl_outboard_client.ml
Added metaprl/tactics/ensemble/appl_outboard_client.mli
Properties metaprl/tactics/ensemble/appl_outboard_client.mli
Added metaprl/tactics/ensemble/appl_outboard_common.ml
Properties metaprl/tactics/ensemble/appl_outboard_common.ml
Added metaprl/tactics/ensemble/appl_outboard_common.mli
Properties metaprl/tactics/ensemble/appl_outboard_common.mli
Added metaprl/tactics/ensemble/appl_outboard_server.ml
Properties metaprl/tactics/ensemble/appl_outboard_server.ml
Added metaprl/tactics/ensemble/appl_outboard_server.mli
Properties metaprl/tactics/ensemble/appl_outboard_server.mli
Added metaprl/tactics/ensemble/ensemble_queue.ml
Properties metaprl/tactics/ensemble/ensemble_queue.ml
Added metaprl/tactics/ensemble/ensemble_queue.mli
Properties metaprl/tactics/ensemble/ensemble_queue.mli
Added metaprl/tactics/ensemble/remote_ensemble.ml
Properties metaprl/tactics/ensemble/remote_ensemble.ml
Added metaprl/tactics/ensemble/remote_ensemble.mli
Properties metaprl/tactics/ensemble/remote_ensemble.mli
Added metaprl/tactics/ensemble/remote_monitor.ml
Properties metaprl/tactics/ensemble/remote_monitor.ml
Added metaprl/tactics/ensemble/remote_monitor.mli
Properties metaprl/tactics/ensemble/remote_monitor.mli
Added metaprl/tactics/ensemble/remote_null.ml
Properties metaprl/tactics/ensemble/remote_null.ml
Added metaprl/tactics/ensemble/remote_null.mli
Properties metaprl/tactics/ensemble/remote_null.mli
Added metaprl/tactics/ensemble/remote_sig.mlz
Properties metaprl/tactics/ensemble/remote_sig.mlz
Added metaprl/tactics/ensemble/thread_refiner.ml
Properties metaprl/tactics/ensemble/thread_refiner.ml
Added metaprl/tactics/ensemble/thread_refiner.mli
Properties metaprl/tactics/ensemble/thread_refiner.mli
Properties metaprl/tactics/null
Added metaprl/tactics/null/Makefile
Properties metaprl/tactics/null/Makefile
Added metaprl/tactics/null/OMakefile
Properties metaprl/tactics/null/OMakefile
Added metaprl/tactics/null/thread_refiner.ml
Properties metaprl/tactics/null/thread_refiner.ml
Added metaprl/tactics/null/thread_refiner.mli
Properties metaprl/tactics/null/thread_refiner.mli
Properties metaprl/tactics/proof
Added metaprl/tactics/proof/Files
Properties metaprl/tactics/proof/Files
Added metaprl/tactics/proof/Makefile
Properties metaprl/tactics/proof/Makefile
Added metaprl/tactics/proof/OMakefile
Properties metaprl/tactics/proof/OMakefile
Added metaprl/tactics/proof/conversionals_boot.ml
Properties metaprl/tactics/proof/conversionals_boot.ml
Added metaprl/tactics/proof/conversionals_boot.mli
Properties metaprl/tactics/proof/conversionals_boot.mli
Added metaprl/tactics/proof/exn_boot.ml
Properties metaprl/tactics/proof/exn_boot.ml
Added metaprl/tactics/proof/exn_boot.mli
Properties metaprl/tactics/proof/exn_boot.mli
Added metaprl/tactics/proof/proof_boot.ml
Properties metaprl/tactics/proof/proof_boot.ml
Added metaprl/tactics/proof/proof_boot.mli
Properties metaprl/tactics/proof/proof_boot.mli
Added metaprl/tactics/proof/proof_convert.ml
Properties metaprl/tactics/proof/proof_convert.ml
Added metaprl/tactics/proof/proof_convert.mli
Properties metaprl/tactics/proof/proof_convert.mli
Added metaprl/tactics/proof/proof_term_boot.ml
Properties metaprl/tactics/proof/proof_term_boot.ml
Added metaprl/tactics/proof/proof_term_boot.mli
Properties metaprl/tactics/proof/proof_term_boot.mli
Added metaprl/tactics/proof/rewrite_boot.ml
Properties metaprl/tactics/proof/rewrite_boot.ml
Added metaprl/tactics/proof/rewrite_boot.mli
Properties metaprl/tactics/proof/rewrite_boot.mli
Added metaprl/tactics/proof/sequent_boot.ml
Properties metaprl/tactics/proof/sequent_boot.ml
Added metaprl/tactics/proof/sequent_boot.mli
Properties metaprl/tactics/proof/sequent_boot.mli
Added metaprl/tactics/proof/tactic_boot.ml
Properties metaprl/tactics/proof/tactic_boot.ml
Added metaprl/tactics/proof/tactic_boot.mli
Properties metaprl/tactics/proof/tactic_boot.mli
Added metaprl/tactics/proof/tactic_boot_sig.ml
Properties metaprl/tactics/proof/tactic_boot_sig.ml
Added metaprl/tactics/proof/tactic_type.ml
Properties metaprl/tactics/proof/tactic_type.ml
Added metaprl/tactics/proof/tactic_type.mli
Properties metaprl/tactics/proof/tactic_type.mli
Added metaprl/tactics/proof/tacticals_boot.ml
Properties metaprl/tactics/proof/tacticals_boot.ml
Added metaprl/tactics/proof/tacticals_boot.mli
Properties metaprl/tactics/proof/tacticals_boot.mli

Changes by: ( at unknown.email)
Date: 2003-08-28 17:09:07 -0700 (Thu, 28 Aug 2003)
Revision: 4896
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.1.4'.

Changes  Path
Copied metaprl-branches/unlabeled-1.1.4
Deleted metaprl-branches/unlabeled-1.1.4/BUGS
Deleted metaprl-branches/unlabeled-1.1.4/Makefile
Deleted metaprl-branches/unlabeled-1.1.4/OMakefile
Deleted metaprl-branches/unlabeled-1.1.4/OMakeroot
Deleted metaprl-branches/unlabeled-1.1.4/README
Deleted metaprl-branches/unlabeled-1.1.4/README.MACOSX
Deleted metaprl-branches/unlabeled-1.1.4/README.WIN32
Deleted metaprl-branches/unlabeled-1.1.4/refiner/Makefile
Deleted metaprl-branches/unlabeled-1.1.4/refiner/OMakefile
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/Files
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/Makefile
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/OMakefile
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/refine_error.h
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/refine_error.mlh
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/refine_error_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/refine_minimal_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/refine_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/refiner_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/rewrite_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_addr_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_base_minimal_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_base_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_eval_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_hash_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_man_minimal_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_man_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_meta_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_norm_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_op_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_shape_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_subst_minimal_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/term_subst_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/termmod_hash_sig.ml
Deleted metaprl-branches/unlabeled-1.1.4/refiner/refsig/termmod_sig.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-28 17:36:48 -0700 (Thu, 28 Aug 2003)
Revision: 4897
Log message:

      As Aleksey suggested, I fixed up ocamldep so that it knows about
      the ext: quotation. If the default .pho file changes in a directory,
      all files which have :ext quotation in them (or depend on such
      files) will be recompiled. This eliminates the need to manually
      clean outdated .cph files.
      

Changes  Path
+3 -0 metaprl/mk/rules
+23 -0 metaprl/util/ocamldep.mll

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-29 02:19:15 -0700 (Fri, 29 Aug 2003)
Revision: 4898
Log message:

      Removing a few more unused "open" statements.
      

Changes  Path
+0 -1 metaprl/editor/ml/mp.mli
+0 -6 metaprl/editor/ml/shell_p4.ml
+0 -1 metaprl/editor/ml/shell_p4.mli
+0 -1 metaprl/filter/base/filter_util.ml
+0 -1 metaprl/tactics/null/thread_refiner.ml
+3 -3 metaprl/util/clean-opens
+0 -2 mpcompiler/mmc/extensions/ext_integer.ml

Changes by: ( at unknown.email)
Date: 2003-08-29 02:19:15 -0700 (Fri, 29 Aug 2003)
Revision: 4899
Log message:

      This commit was manufactured by cvs2svn to create branch
      'unlabeled-1.2.4'.

Changes  Path
Copied metaprl-branches/unlabeled-1.2.4
Deleted metaprl-branches/unlabeled-1.2.4/BUGS
Deleted metaprl-branches/unlabeled-1.2.4/Makefile
Deleted metaprl-branches/unlabeled-1.2.4/OMakefile
Deleted metaprl-branches/unlabeled-1.2.4/OMakeroot
Deleted metaprl-branches/unlabeled-1.2.4/README
Deleted metaprl-branches/unlabeled-1.2.4/README.MACOSX
Deleted metaprl-branches/unlabeled-1.2.4/README.WIN32
Deleted metaprl-branches/unlabeled-1.2.4/tactics/null/Makefile
Deleted metaprl-branches/unlabeled-1.2.4/tactics/null/OMakefile
Deleted metaprl-branches/unlabeled-1.2.4/tactics/null/thread_refiner.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-29 17:07:53 -0700 (Fri, 29 Aug 2003)
Revision: 4900
Log message:

      Phobos dependency is now based on .pho file, not the .cph file.
      

Changes  Path
+1 -1 metaprl/util/ocamldep.mll

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-29 17:41:44 -0700 (Fri, 29 Aug 2003)
Revision: 4901
Log message:

      - Changed the ``ls ""'' to display fewer things. In particular, it will no longer
      show display forms (as they do not add anything to existing "displayed as") and
      "Id" statements.
      
      - Added a "d" option to ls - ``ls "d"'' will show all dforms-related stuff
      (dforms, precedences, etc).
      

Changes  Path
+5 -2 metaprl/editor/ml/QUICKSTART
+2 -0 metaprl/support/shell/shell.ml
+20 -17 metaprl/support/shell/shell_package.ml
+2 -1 metaprl/support/shell/shell_sig.mlz

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-29 18:10:36 -0700 (Fri, 29 Aug 2003)
Revision: 4903
Log message:

      Fixed this up.
      

Changes  Path
+4 -1 metaprl/theories/tutorial/OMakefile

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-08-30 06:34:54 -0700 (Sat, 30 Aug 2003)
Revision: 4904
Log message:

      Made Phobos smarter about checking which file to use to parse
      :ext quotations.
      Now, the following happens:
      
      1. if no .cph exists, we use the .pho file and create a .cph as
         a side-effect
      2. if no .pho exists but only a .cph, we use that file (this would
         have caused failure under what we had yesterday). This doesn't
         happen anywhere in MetaPRL, but may be useful. In fact, in
         mcc we used this for dynamic frontends.
      3. if neither file exists, we raise an error message
      4. if both files exist, we look at the time stamps and file sizes.
         a) we recover these for the .pho file using Unix.stat
         b) for the .cph file, we use a header storing the above (and other)
            information for the .pho file that produced the .cph file
      5. if everything is the same, we use the .cph file
      6. if the .pho file is newer
         a) we check the MD5 sum, if it is the same as in the .cph, we
            use the .cph file instead
         b) otherwise, we use the .pho file
      7. in any other case, we use the .cph file
      
      I question why we needed this as opposed to what I had yesterday.
      MD5 checking is already provided in omake, now we shifted that
      into Phobos as well. Although things are conceptually cleaner
      this way and to realize the change was not difficult, we duplicated
      functionality that is already found in omake.
      

Changes  Path
+1 -0 metaprl/filter/phobos/Files
+45 -6 metaprl/filter/phobos/phobos_compile.ml
+7 -0 metaprl/filter/phobos/phobos_constants.ml
+2 -0 metaprl/filter/phobos/phobos_constants.mli
+1 -1 metaprl/filter/phobos/phobos_grammar.ml
Added metaprl/filter/phobos/phobos_header.ml
Properties metaprl/filter/phobos/phobos_header.ml
Added metaprl/filter/phobos/phobos_header.mli
Properties metaprl/filter/phobos/phobos_header.mli
+5 -2 metaprl/filter/phobos/phobos_marshal.ml
+3 -2 metaprl/filter/phobos/phobos_marshal.mli
+1 -1 metaprl/filter/phobos/phobos_parser.mly
+0 -2 metaprl/mk/rules