/[mojave]/metaprl/theories/mc/TODO
ViewVC logotype

Log of /metaprl/theories/mc/TODO

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 4482)

Revision 3564 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 5 07:07:58 2002 UTC (19 years, 2 months ago) by emre
File length: 2428 byte(s)
Diff to previous 3563
-  Fixed some problems in Mp_mc_fir_eval and proved
   the rewrites in it.
-  Proved 2 of the deadcode elimination rewrites (in Mp_mc_deadcode).


Revision 3563 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 5 01:16:49 2002 UTC (19 years, 2 months ago) by emre
File length: 2367 byte(s)
Diff to previous 3562
Updates to reflect the (ever changing) MC FIR.


Revision 3562 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 3 08:37:31 2002 UTC (19 years, 2 months ago) by emre
File length: 2224 byte(s)
Diff to previous 3551
So, I've defined the compile function in Mp_mc_compile to actually
take an Fir.prog, convert the function definitions to terms,
and then back again, in one big identity operation.  The current
term representation of the FIR functions is a bit of a hack that
will need to be cleaned up if anything non-trivial is to be done.
(Each individual function is fine I hope.  It's the program as a whole
that's represented rather poorly.  It's essentially a (term SymbolTable.t),
one term for each fundef in the original Fir.prog.prog_funs.)
Though, this should be sufficient for basic testing I think.


Revision 3551 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 31 02:48:35 2002 UTC (19 years, 2 months ago) by emre
File length: 1735 byte(s)
Diff to previous 3550
Test cases for the "connection" code are pretty much complete.
I've fixed a few bugs that cropped up (including a major one
in Mp_mc_term_op).  What's needed now is the final set of functions
to take an entire MC Fir.prog to some sort of MetaPRL term.


Revision 3550 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 24 22:35:29 2002 UTC (19 years, 3 months ago) by emre
File length: 1772 byte(s)
Diff to previous 3533
Updating files to reflect the newest version of the MC FIR (which happens to be
in the websplit branch).  In the process, I've also moved every file in this
theory to use the same prefix for the filenames. I've also removed quite
a few files that have been dead for a while now.

Right now, the "connect" files are not compiled in by default since they will
only compile against the websplit branch of MC and not the trunk.

Lastly, since the definition of FIR evaluation is a bit more precise now,
the need to seperately define constant elimination has been removed.


Revision 3533 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 09:54:10 2002 UTC (19 years, 3 months ago) by emre
File length: 2726 byte(s)
Diff to previous 3531
I've renamed theories/mc/fir_eval to use my
(attrocious) prefix so that a file name collision
with fir_eval in the MC source tree doesn't happen.
Other files in theories/mc have been changed
accordingly.

I've renamed mp_mc_theory to just use a .mlz
file since the .ml and .mli files were the
exact same and it's a hassle to modify them
both whenever they need to be changed.

I've updated editor/ml/Conscript so that mpopt
actually includes the Itt_theory and Mp_mc_theory.
This makes it much more useful.

mc/Conscript has been updated to reflect new code
in the MC source tree.

After this, MetaPRL should compile with the
main trunk of the MC source tree if the MC_ROOT
environment variable is set appropriately.


Revision 3531 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 10 07:50:56 2002 UTC (19 years, 3 months ago) by emre
File length: 2570 byte(s)
Diff to previous 3483
Modify my TODO file so that I actually remember
what I need to do, for when I finally get around
to having time to work on it.


Revision 3483 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 29 01:51:50 2002 UTC (19 years, 4 months ago) by emre
File length: 2597 byte(s)
Diff to previous 3478
Adding more test cases.  Some of the cases
have already hilighted some bugs (which
I need to track down and fix).


Revision 3478 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 22 23:38:59 2002 UTC (19 years, 5 months ago) by emre
File length: 2547 byte(s)
Diff to previous 3477
1) The main Conscript has been modified.  Added lines for CPP so that MC
   compiles properly from MetaPRL.
2) Renamed some files in theories/mc/ so as to not confliced with
   files in MC.  I've chosen the (arguably atrocious) prefix
   of mp_mc_.

Assuming string_util.ml and rformat.ml, in the MC source tree,
are renamed to something else and the changes propagated as
necessary, this commit should re-enable MetaPRL and MC to build together
(using cons).


Revision 3477 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 18 16:35:35 2002 UTC (19 years, 5 months ago) by emre
File length: 2520 byte(s)
Diff to previous 3472
1. Re-exported fir_eval.prla.
2. Mc_set : minor display form change.
3. Randomly reformatted some Conscripts it seems.
   (I removed tab characters from the files.)

The next steps will be to:
1. Consider renaming all files in theories/mc
   to start with mp_ or some other "unique" prefix
   so that the naming is consistant
   and avoids conflicts with files in MC.
2. Begin testing the mc_fir_connect code.  This
   will probably take some time to get completely
   correct.


Revision 3472 - (view) (download) (annotate) - [select for diffs]
Modified Sat Dec 22 05:43:27 2001 UTC (19 years, 6 months ago) by emre
File length: 1984 byte(s)
Diff to previous 3471
-  Removed util/Construct since it seems to be
   unnecessary for building MetaPRL with cons.
-  Minor changes to other Conscript(s).
   Mostly formatting (changing tabs to spaces).
-  Top level Conscript only uses the MC std. lib.
   if MC_ROOT is defined.  Before, if MC_ROOT wasn't
   defined, the -I cmd. line arguments would have
   unnecessary things like -I /lib/naml/...
-  Minor changes to display forms in theories/mc.
-  Minor changes to code formatting in theories/mc.
-  Filled in missing Mc_fir_connect_* functions.
   I need to look over them at some point for
   obvious typo-bugs and perform other testing.


Revision 3471 - (view) (download) (annotate) - [select for diffs]
Modified Sun Dec 16 20:25:09 2001 UTC (19 years, 6 months ago) by emre
File length: 1592 byte(s)
Diff to previous 3464
A final commit before I take off for the break.
Various minor changes and improvements.  Work
remaining is listed in TODO.


Revision 3464 - (view) (download) (annotate) - [select for diffs]
Added Sun Dec 9 03:10:53 2001 UTC (19 years, 6 months ago) by emre
File length: 1413 byte(s)
Many changes:
-  Began to redo the README file to be more useful/informative.
-  Added a TODO file for this theory to keep track of what still
   needs to be done.
-  Regorganized where I declared int_set and rawint_set (Mc_set).
-  Rewrote exceptions to use RefineError where reasonable/possible.
-  Continuing to add "conversion" functions for MC FIR types
   and MetaPRL terms.  The great majority of them are there, but
   they still need work and testing.
-  Random updates to comments.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26