ViewVC logotype

Log of /metaprl/theories/mc/README

Parent Directory Parent Directory | Revision Log Revision Log

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

Revision 3588 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 27 02:45:24 2002 UTC (19 years, 1 month ago) by emre
File length: 2244 byte(s)
Diff to previous 3583
Updating modules so that they generate documentation
for theories.pdf.  Right now, it's _very_ minimal and
not so useful.  Hopefully, I will get around to updating
them and making them decent.

Also updating the README file to properly reflect the
name of our research group at Caltech.

Revision 3583 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 05:26:29 2002 UTC (19 years, 2 months ago) by emre
File length: 2231 byte(s)
Diff to previous 3564
Committing a much needed update of the README file.
Currently contains a brief introduction to the motiviations
that led to this theory's creation and some notes
about compiling MetaPRL with MC (the Mojave Compiler).

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: 1155 byte(s)
Diff to previous 3551
-  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 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: 2423 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: 7435 byte(s)
Diff to previous 3483
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 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: 7441 byte(s)
Diff to previous 3472
Adding more test cases.  Some of the cases
have already hilighted some bugs (which
I need to track down and fix).

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: 7370 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: 7079 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]
Modified Sun Dec 9 03:10:53 2001 UTC (19 years, 6 months ago) by emre
File length: 6916 byte(s)
Diff to previous 3458
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.

Revision 3458 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 29 20:23:02 2001 UTC (19 years, 6 months ago) by emre
File length: 2182 byte(s)
Diff to previous 3457
More "connection" code.  Most of the function are there,
but some still need to be completely defined.

Revision 3457 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 28 09:46:07 2001 UTC (19 years, 6 months ago) by emre
File length: 2077 byte(s)
Diff to previous 3454
- Continuing implementation of code to convert from Fir.prog to MetaPRL terms,
  and vica versa.
- Renamed some files to avoid conflicts.

Revision 3454 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 21 09:17:04 2001 UTC (19 years, 7 months ago) by emre
File length: 1925 byte(s)
Diff to previous 3452
Updates to solve some build problems:

make : Building with make is completely independent of the presence
   of the Mojave compiler source tree, since the MC compiler must
   be built with cons.  Thus, the only code that currently depends
   on MC, theories/mc/fir_marshal is not compiled.  Not including
   it as a part of the build of theories/mc is not a problem since it
   has no logical or otherwise meaningful content beyond the functions to
   convert between terms and the Fir.prog data structure of the compiler,
   i.e. this present no loss to the mc theory.

cons : If the MC_ROOT environment variable is defined, its assumed to point
   to the root directory of the Mojave compiler source tree, and in this
   case, we build the two source trees together.  (To use MC, you need
   to define MC_ROOT anyway, so there's no need to put it as a config
   option somewhere.)  In particular, we (will) compile the
   "connection" code in theores/mc/fir_marshal.  If MC_ROOT is undefined,
   MetaPRL will build almost identically; the only difference is that
   fir_marshal is not compiled in.

Revision 3452 - (view) (download) (annotate) - [select for diffs]
Modified Tue Nov 20 22:31:15 2001 UTC (19 years, 7 months ago) by emre
File length: 1865 byte(s)
Diff to previous 3451
- More term operations. Everything in fir_ty and fir_exp should
  have term (de)construction operations now.
- Started redoing the README file.
- IMPORTANT: At this point, the default compile setup for the MC theory
  will depend on the source tree for the mojave compiler being present.
- WARNING: For those using cons, the update of fir_marshal here breaks
  compilation of mp.opt due to a library conflict.

Revision 3451 - (view) (download) (annotate) - [select for diffs]
Modified Tue Nov 20 14:51:38 2001 UTC (19 years, 7 months ago) by emre
File length: 4120 byte(s)
Diff to previous 3447
Even more term ops implemented.

Revision 3447 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 19 03:42:48 2001 UTC (19 years, 7 months ago) by emre
File length: 3963 byte(s)
Diff to previous 3445
- More term operations added.
- mc_term_op_ds now contains some local functions for
  (de)constructing terms with 4+ subterms.

Revision 3445 - (view) (download) (annotate) - [select for diffs]
Modified Sat Nov 17 05:17:28 2001 UTC (19 years, 7 months ago) by emre
File length: 3242 byte(s)
Diff to previous 3427
- A little clean up for const_elim.
- Term operations for fir_ty.
- Don't use cons to build this theory.  I make no guarentees about
  cons correctly being able to navigate dependencies and namespace
  related conflicts, yet.
- The Makefile now includes meta-prl/mc/fir/..., so make may not work
  either unless you have the Mojave compiler source tree set up appropriately.
- In short, this code is in a state of flux.  I will get it to cleanly
  compile eventually.

Revision 3427 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 27 05:05:38 2001 UTC (19 years, 7 months ago) by emre
File length: 2905 byte(s)
Diff to previous 3421
- Added more terms for FIR entities (trig functions).
- Changed deadcode elimination slightly.
- Changed evalutation of tyInt arithmetic to sort of
  do some type checking.

Revision 3421 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 7 05:09:57 2001 UTC (19 years, 8 months ago) by emre
File length: 2335 byte(s)
Diff to previous 3417
Essentially, this commit is a bunch of
code reorganization so that rewrites
and term declareations are now found
in more logical places (I claim).
   - Fir*state* is now removed.
   - Fir_ty and Fir_exp now just declare terms.
     All evaluations is done with firEvalT in Fir_eval.
     This means that Fir_int also went away.
   - Fir_*type* are no longer compiled by default.
     I'll come back to these when I need to,
     under the assumption that by then, everything
     else will have stabilized / be close to that state.

Revision 3417 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 29 08:01:35 2001 UTC (19 years, 8 months ago) by emre
File length: 2925 byte(s)
Diff to previous 3413
Entered in some final end of summer comments,
to ease picking up the code at a later date.
(Really, its not that bad, but this is still
a good idea anyways.)

Revision 3413 - (view) (download) (annotate) - [select for diffs]
Added Thu Sep 27 00:40:57 2001 UTC (19 years, 8 months ago) by emre
File length: 691 byte(s)
Updated some comments and added some for clarification.
Added a letSubscript rewrite.
Added a README file to hold some general 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