ViewVC logotype

Log of /metaprl/theories/mc/Conscript

Parent Directory Parent Directory | Revision Log Revision Log

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

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: 1422 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: 1326 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, 2 months ago) by emre
File length: 1224 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: 1883 byte(s)
Diff to previous 3480
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

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 3480 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 25 01:27:28 2002 UTC (19 years, 4 months ago) by emre
File length: 1857 byte(s)
Diff to previous 3479
1) Added some test cases to demonstrate what
   the test program will do.
2) Added mp_mc_compile.  This module will (hopefully)
   be used as the main interface to MC.  Right now,
   it only defines one function, compile, which
   is the identity on an Fir.prog.

Revision 3479 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 24 05:49:15 2002 UTC (19 years, 4 months ago) by emre
File length: 1808 byte(s)
Diff to previous 3478
Two changes essentially:
1) Moved more files in theories/mc to have
   the mp_mc_ prefix.
2) Added theories/mc/tests/  The files there are
   pretty empty right now, but the idea is to put
   code there for a simple test program to test
   the mp_mc_connect modules.

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: 1802 byte(s)
Diff to previous 3464
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 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: 1766 byte(s)
Diff to previous 3457
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 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: 1888 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: 1626 byte(s)
Diff to previous 3451
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 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: 754 byte(s)
Diff to previous 3449
Even more term ops implemented.

Revision 3449 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 19 15:09:10 2001 UTC (19 years, 7 months ago) by jyh
File length: 731 byte(s)
Diff to previous 3447
First working version with meta-prl/mc together.

To compile with mc, as of Mon Nov 19 07:04:50 PST 2001:
   0. Get a copy of mc, available from mojave.cs.caltech.edu.
      If you don't know how, you can ask jyh@cs.caltech.edu.
   1. set the MC_ROOT environment variable to the root
      directory for mc.
   2. Compile using cons.  You chould compile from the root
      meta-prl directory first.  After that, you can build
      from the editor/ml directory (use cons -t).

There are still some problems with dependencies in theories/tactic.
prlc adds a lot of implicit dependencies, and I've only caught a few
of them.  It compiles for now, but beware of "undefined modules" in

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: 682 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: 640 byte(s)
Diff to previous 3438
- 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 3438 - (view) (download) (annotate) - [select for diffs]
Added Sun Nov 4 10:28:15 2001 UTC (19 years, 7 months ago) by emre
File length: 589 byte(s)
- Added a Conscript
- const_elim is much simpler now!
  The tactic for it is still a bit slow though.
- Changed cmp(Raw)IntOp evaluation to reflect
  mc better.

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