Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-05 17:36:06 -0800 (Wed, 05 Feb 2003)
Revision: 4038
Log message:
Unicode fixes for couple of display forms.
Changes | Path |
+1 -1 | metaprl/theories/itt/itt_tsquash.ml |
+5 -1 | metaprl/theories/tactic/nuprl_font.ml |
+1 -0 | metaprl/theories/tactic/nuprl_font.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-12 16:09:36 -0800 (Wed, 12 Feb 2003)
Revision: 4075
Log message:
Added a "funded in part by" statement.
Changes | Path |
+5 -0 | metaprl/doc/htmlman/mp.html |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-12 16:10:20 -0800 (Wed, 12 Feb 2003)
Revision: 4076
Log message:
Need an HR.
Changes | Path |
+1 -0 | metaprl/doc/htmlman/mp.html |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-12 16:24:16 -0800 (Wed, 12 Feb 2003)
Revision: 4077
Log message:
Supported in part by ONR.
Changes | Path |
+4 -3 | metaprl/doc/htmlman/mp.html |
+5 -1 | metaprl/doc/latex/theories/all-theories.tex |
Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-16 21:32:47 -0800 (Sun, 16 Feb 2003)
Revision: 4079
Log message:
Fixed a bug in a record elimination tactic. Thanks to Xin for noticing this.
Changes | Path |
+2 -105 | metaprl/theories/itt/itt_record.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-17 00:56:18 -0800 (Mon, 17 Feb 2003)
Revision: 4080
Log message:
Added Phobos (with a few features stripped out) to MetaPRL.
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-17 00:57:26 -0800 (Mon, 17 Feb 2003)
Revision: 4081
Log message:
Include Phobos in Makefiles.
Changes | Path |
+4 -3 | metaprl/filter/Makefile |
+1 -1 | metaprl/filter/filter/Makefile |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-17 00:59:38 -0800 (Mon, 17 Feb 2003)
Revision: 4082
Log message:
Added Phobos grammar for M_ir.
For now, I also added the compiled list module.
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-18 14:44:28 -0800 (Tue, 18 Feb 2003)
Revision: 4083
Log message:
Added M AST. Next is putting back the ability in Phobos to apply
relaxed rewrites (post-parsing) since these were taken out with
the initial integration, and commiting the MetaPRL term
definitions and display forms for M AST.
The current AST is different from the IR in only that
functions are defined/called with a list of params/args.
I have to think about whether we can do currying in MetaPRL, or
have to resort to Phobos and its relaxed rewrites (when I put them
back).
For now, the ext: quotation uses m_ir.pho, but I will commit a quick
fix to allow the changing of the grammar as one compiles MetaPRL.
Changes | Path |
Added | metaprl/theories/experimental/compile/m_ast.pho |
Properties | metaprl/theories/experimental/compile/m_ast.pho |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-18 14:47:25 -0800 (Tue, 18 Feb 2003)
Revision: 4084
Log message:
Now you can use the environment variable LANG_FILE to set the name
of the grammar file to be used in the ext: quotation.
You can also set DEBUG_PHOBOS to see the parsing process, although
I don't see why anyone would be interested in seeing that. To
disable it, set it to "off".
Changes | Path |
+19 -1 | metaprl/filter/phobos/filter_phobos.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:27:04 -0800 (Wed, 19 Feb 2003)
Revision: 4086
Log message:
Added new rule for the term symbol that calls Phobos on a string.
This was approach II, as we discussed earlier.
Here is an example:
sequent [m] { 'H >- $"let t = 1 in let u = 2 in t+u"$ }
The default language is "m_ir.pho", assumed to be in the current
directory. You can also control the default language through
the LANG_FILE environment variable.
As before, there remains an ext: quotation that can be used in
Ocaml expressions and patterns, such as
let t = <:ext<let t = 1 in let u = 2 in t+u>> in ...
Changes | Path |
+12 -1 | metaprl/filter/filter/filter_parse.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:29:01 -0800 (Wed, 19 Feb 2003)
Revision: 4087
Log message:
Switched over to Mp_debug. I am still not convinced that MP_DEBUG
is read from the environment, though.
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:30:10 -0800 (Wed, 19 Feb 2003)
Revision: 4088
Log message:
We should clear up Phobos-generated files on clean-up.
Changes | Path |
+1 -1 | metaprl/theories/experimental/compile/Makefile |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:37:45 -0800 (Wed, 19 Feb 2003)
Revision: 4089
Log message:
Switched hardcoded term with the new Phobos-enabled term notation.
Fancy way of saying putting things to the test.
Changes | Path |
+12 -10 | metaprl/theories/experimental/compile/m_ir.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:38:56 -0800 (Wed, 19 Feb 2003)
Revision: 4090
Log message:
Changed comment to say M IR and not AST (which was added earlier).
Changes | Path |
+1 -2 | metaprl/theories/experimental/compile/m_ir.pho |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:55:43 -0800 (Wed, 19 Feb 2003)
Revision: 4091
Log message:
Cleaned up m_ir.pho:
-eliminated dependence on list.cph (which was getting cleared out
in make clean anyways)
-no need to include Phobos-related modules (it is a clean module...)
-function calls take only one argument
-got rid of enclosing "syntax" term.
Changes | Path |
+4 -10 | metaprl/theories/experimental/compile/m_ir.pho |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 12:37:34 -0800 (Wed, 19 Feb 2003)
Revision: 4092
Log message:
This should finish off quotations... I have enabled term/ext quotations
in terms, so now you can write
sequent [m] { 'H >- <<AtomInt[1:n]>> }
sequent [m] { 'H >- <:term<....>> }
sequent [m] { 'H >- <:ext<let t = 1 in let u = 2 in u*t>> }
and of course you can still use
sequent [m] { 'H >- $"let t = 1 in let u = 2 in u*t"$ }
The key part that we were missing was the fact that there is a token
type QUOTATION.
Changes | Path |
+24 -5 | metaprl/filter/filter/filter_parse.ml |
+0 -4 | metaprl/filter/phobos/filter_phobos.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 17:17:55 -0800 (Wed, 19 Feb 2003)
Revision: 4093
Log message:
Phobos error messages should be caught by the Phobos exnhdlr.
Also, the list of tokens was not destroyed between different calls
to Phobos, resulting in the same term returned from each (since
parsing stopped at the first syntactically correct term - this
can be fixed in the local copy of m_ir/m_ast.pho).
Changes | Path |
+2 -3 | metaprl/filter/filter/filter_parse.ml |
+2 -0 | metaprl/filter/phobos/phobos_tokenizer.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 17:18:32 -0800 (Wed, 19 Feb 2003)
Revision: 4094
Log message:
Added .cvsignore.
Changes | Path |
Properties | metaprl/filter/phobos |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-19 19:43:23 -0800 (Wed, 19 Feb 2003)
Revision: 4095
Log message:
Please remember this:
*** All ML files in an application have to have different names ***
Please, do not add files to MetaPRL named set.ml for instance. It is
not possible to compile MetaPRL if you do so.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-19 19:51:42 -0800 (Wed, 19 Feb 2003)
Revision: 4096
Log message:
Adam, please do not commit files that do not compile.
If you want to do so, please go off on a branch.
It is very annoying to have to fix your files.
Changes | Path |
+0 -0 | metaprl/theories/experimental/compile/Makefile |
+7 -12 | metaprl/theories/experimental/compile/m_ir.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-19 19:53:39 -0800 (Wed, 19 Feb 2003)
Revision: 4097
Log message:
Some minor changes to get MetaPRL to compile in Windows/Cygwin.
Also, a minor update to filter_main.ml to force an exit after
preprocessing. For some reason prlcomp.ml is linked into camlp4n!
Changes | Path |
+3 -0 | metaprl/clib/termsize.c |
+1 -1 | metaprl/filter/filter/filter_main.ml |
+3 -0 | metaprl/mk/rules |
+2 -2 | metaprl/util/ocamldep.mll |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-19 20:40:38 -0800 (Wed, 19 Feb 2003)
Revision: 4098
Log message:
The final part of the CYGWIN-related fix:
- Only compile prlcomp into prlc, but not into camlp*.
Changes | Path |
+7 -6 | metaprl/filter/Makefile |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-20 18:03:47 -0800 (Thu, 20 Feb 2003)
Revision: 4103
Log message:
We raise an exception if term quotation is used in terms, like
sequent [m] { 'H >- <<...>> }
Added .cvsignore to filter/phobos, and changed the Makefile
to clear out all generated files.
Added pairs to m_ast.pho and m_ir.pho, removed list.cph, and
changed the test program sequent to use the :ext quotation.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-21 00:29:40 -0800 (Fri, 21 Feb 2003)
Revision: 4104
Log message:
- Defined group like objects: groupoid, semigroup, and monoid with dependent
records.
- Defined groups based on the definitions of group like objects with
dependent records.
- Proved all properties in CZF for groups here in ITT.
TODO:
1. Might simplify the display forms of "*" later.
2. Might need more research on using constants as field names.
3. After the rewriter bug is fixed, some proofs might be simplified and the
elimination rules for groups etc. are unnecessary.
Changes | Path |
+2 -0 | metaprl/theories/itt/Makefile |
Added | metaprl/theories/itt/itt_group.ml |
Properties | metaprl/theories/itt/itt_group.ml |
Added | metaprl/theories/itt/itt_group.mli |
Properties | metaprl/theories/itt/itt_group.mli |
Added | metaprl/theories/itt/itt_group.prla |
Properties | metaprl/theories/itt/itt_group.prla |
Added | metaprl/theories/itt/itt_grouplikeobj.ml |
Properties | metaprl/theories/itt/itt_grouplikeobj.ml |
Added | metaprl/theories/itt/itt_grouplikeobj.mli |
Properties | metaprl/theories/itt/itt_grouplikeobj.mli |
Added | metaprl/theories/itt/itt_grouplikeobj.prla |
Properties | metaprl/theories/itt/itt_grouplikeobj.prla |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-21 18:07:07 -0800 (Fri, 21 Feb 2003)
Revision: 4107
Log message:
1. Added the fold form of rewritings.
2. Added the commutative property and defined commutative semigroup/monoid
and abelian group.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-22 09:03:49 -0800 (Sat, 22 Feb 2003)
Revision: 4108
Log message:
Instead of LetFun, using AtomFun instead. This will make CPS easier.
I reverted to the term syntax until Phobos can be updated.
Changes | Path |
+20 -19 | metaprl/theories/experimental/compile/m_ir.ml |
+2 -1 | metaprl/theories/experimental/compile/m_ir.mli |
+1 -1 | metaprl/theories/tactic/nuprl_font.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-22 12:57:49 -0800 (Sat, 22 Feb 2003)
Revision: 4109
Log message:
Fixed m_ast/m_ir to use AtomFuns in function definitions, added
another testing sequent with the :ext quotation (which you should just
comment out next time something does not work), and removed the
debugging line from filter_parse.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-22 17:12:39 -0800 (Sat, 22 Feb 2003)
Revision: 4110
Log message:
A partial implementation of CPS as discussed to Aleksey.
However, I am going to scrap this, and formulate it with
inference rules instead.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-22 19:29:08 -0800 (Sat, 22 Feb 2003)
Revision: 4111
Log message:
- Added more automation to itt_int_base and itt_int_ext
(reductions for "a - b + b", "a + b - b", "a - a", "a < a", etc)
- Simplified the Itt_nat proofs using the new automation
(most of the proofs are still incomplete since they need an inequality
tactic).
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 10:28:36 -0800 (Sun, 23 Feb 2003)
Revision: 4112
Log message:
Trying CPS with inference rules.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 17:45:46 -0800 (Sun, 23 Feb 2003)
Revision: 4113
Log message:
This is an initial attempt at using inference rules for rewriting.
To make this work, we would either have to:
1. Add explicit context vars for rewriting
2. Quantify free variables in a rewrite
#1 seems the better choice.
In any case, I think I'll go back to trying to use rewrites,
until we talk about this approach.
Changes | Path |
+28 -3 | metaprl/theories/experimental/compile/m_cps.ml |
+1 -0 | metaprl/theories/experimental/compile/m_cps.mli |
+1 -1 | metaprl/theories/experimental/compile/m_test.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 19:09:57 -0800 (Sun, 23 Feb 2003)
Revision: 4114
Log message:
This is a working version of CPS transformation, but I am not sure
if it is the best approach.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 20:35:43 -0800 (Sun, 23 Feb 2003)
Revision: 4115
Log message:
***Notice***
I changed the MetaPRL formatter. If you have problems with it let me
know and I will try to fix them.
The objective of this fix was to get indentation working again.
An unrelated change was to remove specially-coded line formatting,
since the formatter already has line zones.
On the CPS end, I added the code to convert function applications
and conditionals.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 21:45:01 -0800 (Sun, 23 Feb 2003)
Revision: 4116
Log message:
Reintroduced Aleksey's column limit.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 21:46:12 -0800 (Sun, 23 Feb 2003)
Revision: 4117
Log message:
Oops, left in a debugging comment.
Also, I added minimal support for boldface in terminal windows.
Changes | Path |
+0 -1 | metaprl/refiner/reflib/dform.ml |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-23 23:36:05 -0800 (Sun, 23 Feb 2003)
Revision: 4118
Log message:
According to Alexei's comments:
1. Simplified the representation of {self : {record} | P[self]}
to {record; P[self]};
2. Changed the names of "G" and "e" to "car" and "1"; in the the extendend
syntax for records, removed quotes where labels are constant other than
"*" and "1".
3. Removed "group_is_monoid" from the intro resources.
Updated proofs accordingly.
TODO:
Need to work on improving the syntax and display forms of "*", "inv".
Alexei will work on the syntax part.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-24 19:18:07 -0800 (Mon, 24 Feb 2003)
Revision: 4119
Log message:
Added more formatting.
Changes | Path |
+2 -2 | metaprl/theories/experimental/compile/m_cps.ml |
+12 -12 | metaprl/theories/experimental/compile/m_ir.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-24 19:52:29 -0800 (Mon, 24 Feb 2003)
Revision: 4120
Log message:
One of the srec rules was missing one of the necessary wf assumptions.
Alexei, Jason, please double-check.
Changes | Path |
+1 -0 | metaprl/theories/itt/itt_srec.ml |
+1 -0 | metaprl/theories/itt/itt_srec.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-24 20:26:14 -0800 (Mon, 24 Feb 2003)
Revision: 4121
Log message:
Added the formatting bounds-check that Aleksey and I have
talked about. Ithink I fixed the TeX error; will check that next.
Changes | Path |
+52 -19 | metaprl/refiner/reflib/rformat.ml |
+13 -0 | metaprl/refiner/reflib/rformat.mli |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-24 21:51:45 -0800 (Mon, 24 Feb 2003)
Revision: 4122
Log message:
1. Added display forms for the terms.
2. Separate commutative semigroup/monoid and abelian group from the
grouplikeobj/group modules.
Any comment on the display forms?
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-24 21:52:56 -0800 (Mon, 24 Feb 2003)
Revision: 4123
Log message:
Added 3 group files for documentation.
Changes | Path |
+3 -0 | metaprl/doc/latex/theories/itt/print.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 00:00:41 -0800 (Tue, 25 Feb 2003)
Revision: 4124
Log message:
Two changes:
1. Added the refiner error RewriteStringOpnameOpnameError;
I was having too much trouble finding out why rewrites
weren't working.
2. Added the first phase of closure conversion. This is
the simpler phase, but it requires an inverse beta-reduction,
and I was having trouble with it (turns out, I was just being
dumb).
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 00:19:40 -0800 (Tue, 25 Feb 2003)
Revision: 4125
Log message:
Completed closure conversion.
If this really works, it is amazing. Closure conversion in 225 lines,
and most of those can be eliminated!
BTW, Brian is welcome to look at this; don't worry about lab4.
Changes | Path |
+36 -0 | metaprl/theories/experimental/compile/m_closure.ml |
+10 -0 | metaprl/theories/experimental/compile/m_closure.mli |
+3 -2 | metaprl/theories/experimental/compile/m_test.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 00:29:24 -0800 (Tue, 25 Feb 2003)
Revision: 4126
Log message:
Added a compileT tactic that does both CPS and closure conversion.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 11:02:17 -0800 (Tue, 25 Feb 2003)
Revision: 4127
Log message:
Working on program normalization, but the rewriter is giving me
a bad match and I'm having trouble tracking it down.
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-25 14:18:10 -0800 (Tue, 25 Feb 2003)
Revision: 4128
Log message:
Put back post-parsing rewrites.
Also, when applying a rewrite, apply it along with the global rewrites.
With these changes, I will go ahead and remove Phobos from mcc, and
hopefully all the dynamic front-end stuff will work as before.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 18:59:52 -0800 (Tue, 25 Feb 2003)
Revision: 4129
Log message:
Perform program hoisting as a sequence of pairwise swaps.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 20:02:49 -0800 (Tue, 25 Feb 2003)
Revision: 4130
Log message:
Modified CPS conversion slightly to enclose the entire program
in a function.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 20:13:54 -0800 (Tue, 25 Feb 2003)
Revision: 4131
Log message:
Moved generic resource code into M_util.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 20:33:21 -0800 (Tue, 25 Feb 2003)
Revision: 4132
Log message:
Added dead code elimination.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 21:00:30 -0800 (Tue, 25 Feb 2003)
Revision: 4133
Log message:
Added constant folding.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-26 09:35:33 -0800 (Wed, 26 Feb 2003)
Revision: 4134
Log message:
Prog hoisting is more complete.
Changes | Path |
+20 -4 | metaprl/theories/experimental/compile/m_prog.ml |
Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 14:15:01 -0800 (Wed, 26 Feb 2003)
Revision: 4135
Log message:
Extended grammar:
1. Syntax for binary algebraic operations:
'a *['g] 'b stands for 'g^"*" 'a 'b
The same for +,-,/,^ and relations: <,=,>,<=,>=,<>
For binary algebraic operations with self the syntax remains unchanged:
'a ^* 'b (is the same as 'a *['self] 'b) stands for 'self^"*" 'a 'b
2. Fixed a bug: now field selection (r^l) has higher priority than application.
So you may write: g^inv 'a instead of (g^inv) 'a
3. Boolean relations for integers <@, =@, >@, <>@, <=@, >=@.
(That is, a<b is proposition and a<@ b is a boolean).
4. Power for integers: a ^@ b
5. Syntax for field update: 'r^x:='a
6. Wild card (_) is removed.
Changes | Path |
+162 -100 | metaprl/filter/base/term_grammar.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-26 16:00:43 -0800 (Wed, 26 Feb 2003)
Revision: 4137
Log message:
I am committing this file separately.
I added another :desc "quotation" (for IR descriptions). Among others,
this would be useful in rewrite rules, which expect mterms, but ideally
we shouldn't duplicate code. So if you can figure out a better parse
symbol to extend (so that you can use this "quotation" in sequents as well),
feel free to revert this code. I didn't think nonwordterm was the right
symbol to extend for this.
Changes | Path |
+35 -1 | metaprl/filter/filter/filter_parse.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-26 16:05:41 -0800 (Wed, 26 Feb 2003)
Revision: 4138
Log message:
Added :desc quotation for IR descriptions. For a sample, see
the changes in m_closure.ml.
Also, m_ir.pho now lives in m_ast.pho, and m_ir.pho now parses
the IR descriptions. Consequently, the :ext quotation uses
m_ast.pho, and the :desc quotation used m_ir.pho.
I will now be working on the M AST.
Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 18:28:47 -0800 (Wed, 26 Feb 2003)
Revision: 4139
Log message:
I extend syntax with the following expressions:
'A subtype 'B
'A subset 'B
'x in 'A subset 'B
x:A isect B[x]
A bunion B
Union x:A. B[x]
Isect x:A. B[x]
(All changes are reflected in doc/htmlman/user-guide/mp-terms.html).
Now words subtype, subset, isect, bunion, Union and Isect are keywords.
So you can't write just subtype{'A;'B}.
You should write
'A subtype 'B
or
"subtype"{'A;'B}
or
\subtype{'A ;'B}
I hope this will not create problems.
If it annoys someone, let me know.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-26 21:43:45 -0800 (Wed, 26 Feb 2003)
Revision: 4141
Log message:
Added initial assembly code.
Will have to talk about how we handle tailcalls, and closures.
It will take some work.
Adam, phobos goes into an infinite loop on m_closure.ml.
Can you check it out?
Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 22:35:15 -0800 (Wed, 26 Feb 2003)
Revision: 4142
Log message:
Fixed proofs that were broken by my last commit.
Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 22:43:50 -0800 (Wed, 26 Feb 2003)
Revision: 4143
Log message:
Use new syntax in some czf theories.
Changes | Path |
+14 -14 | metaprl/theories/czf/czf_itt_eq.ml |
+11 -11 | metaprl/theories/czf/czf_itt_subset.ml |
Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-27 01:40:58 -0800 (Thu, 27 Feb 2003)
Revision: 4145
Log message:
Added M source language definition. It is a superset of the M IR,
the only extension is our own tuple terms which are used to encode
function arguments.
The parser takes care of currying function definitions and properly
declares all mutually recursive functions before their definition.
These are implemented with relaxed rewrites.
Then in m_post_parsing, we curry function calls by partially applying
them one by one, storing the result of each partial function
application in a temporary variable.
There is one step missing, which is identifying function variables
in the program term. This should be easy enough:
FunDecl{f. 'e[AtomVar{'f}]} <--> FunDecl{f. 'e[AtomFunVar{'f}]}
but a straight rewrite rule just does not cut it. So this remains
to be done.
I put a test program in m_test, but the old stuff should work as
before. The post-processing tactic is called ppT.
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-02-28 23:16:39 -0800 (Fri, 28 Feb 2003)
Revision: 4150
Log message:
In an effort to avoid my actual homework, I decided to take a look
at M_dead, M_inline, and M_prog.
-------------------------------------------------
M_dead: Fixed a few cut-and-paste typos in the comments. My only
other observation is that it seems that something like
LetAtom{AtomBinop{DivOp; AtomInt[1]; AtomInt[0]}; v. 'e} <--> 'e
is allowed. Which might be fine, depending on what the evaluation
order is and how strictly you want to preserve the semantics of
the program.
-------------------------------------------------
M_inline: Fixed even more cut-and-paste typos. Before,
AtomBinop{SubOp; AtomInt[i:n]; AtomInt[j:n]}
could have been folded using meta_diff, meta_prod, or meta_quot.
I decided that perhaps someone intended to fold together
multiplications and divisions together, instead of specifying
three separate ways (two of which made no sense) to fold a
subtraction...
-------------------------------------------------
M_prog: Fixed a few more cut-and-paste typos in comments. Also
fixed a cut-and-paste typo present where fundecl_if_false is added
to the prog resource (the term to match against was the same as in
the fundecl_if_true case, which seemed bogus). The other change
is I added a rewrite fundef_let_pair which swaps FunDef with
LetPair. This might be wrong, but I couldn't think of any reason
why you wouldn't want to have that rule, or why that rule would be
incorrect.
I suppose if I have more time on my hands, I'll try to take a look
at closure conversion and CPS conversion, and maybe even pay
attention to the discussions about this stuff. (-:
Changes | Path |
+3 -3 | metaprl/theories/experimental/compile/m_dead.ml |
+5 -5 | metaprl/theories/experimental/compile/m_inline.ml |
+6 -2 | metaprl/theories/experimental/compile/m_prog.ml |