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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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.