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

Log of /metaprl/theories/mc/Makefile

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3565 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 5 09:33:57 2002 UTC (19 years, 2 months ago) by emre
File length: 644 byte(s)
Diff to previous 3550
Redoing constant elimination, now that I've corrected
the mistake I made in FIR evaluation.  As a sidenote, I'm not
completely convinced that I've expressed how division expressions evaluation
"correctly".


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: 622 byte(s)
Diff to previous 3540
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 3540 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 16:03:51 2002 UTC (19 years, 3 months ago) by emre
File length: 547 byte(s)
Diff to previous 3479
Updated theories/mc/Makefile to
reflect new file names (oops!).
Changed editor/ml/Conscript to use a more
appropriate mechanism for declaring the
hidden dependencies of mpopt.


Revision 3479 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 24 05:49:15 2002 UTC (19 years, 5 months ago) by emre
File length: 541 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: 500 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: 491 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: 516 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: 519 byte(s)
Diff to previous 3453
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 3453 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 21 01:45:18 2001 UTC (19 years, 7 months ago) by emre
File length: 574 byte(s)
Diff to previous 3451
make will now build the mc theory (and all of MetaPRL) w/o trouble now.


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: 591 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: 574 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: 555 byte(s)
Diff to previous 3428
- 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 3428 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 28 01:48:19 2001 UTC (19 years, 7 months ago) by emre
File length: 500 byte(s)
Diff to previous 3427
- Added support for evaluating "raw ints".
- Started adding support of elimination of
  constants.


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: 480 byte(s)
Diff to previous 3422
- 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 3422 - (view) (download) (annotate) - [select for diffs]
Modified Thu Oct 18 09:07:10 2001 UTC (19 years, 8 months ago) by emre
File length: 497 byte(s)
Diff to previous 3421
Lots of changes in this update:
- Added terms for rawint sets.
- Added additional terms for FIR entities. There
  should be terms for just about anything.
- Moved a few more things into Fir_eval since
  that's where they belonged.  Fir_eval contains
  terms that are needed just to evaluate programs.
- Added a deadcode elimination tactic.  The rewrites
  are simple and proven.
- Added stub files for marshalling to and from
  the mojave compiler Fir.prog type.


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: 442 byte(s)
Diff to previous 3388
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 3388 - (view) (download) (annotate) - [select for diffs]
Modified Thu Sep 20 04:33:32 2001 UTC (19 years, 9 months ago) by emre
File length: 526 byte(s)
Diff to previous 3384
Removed fir_auto since the one automation I provided doesn't work
effectively on actual compiler output.  Updated some comments
and added some rewrites to evaluate output from the compiler.
Compiler output of simple programs seems to evaluate now.


Revision 3384 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 18 02:23:22 2001 UTC (19 years, 9 months ago) by emre
File length: 555 byte(s)
Diff to previous 3381
Modified some terms to work with the output
from the mc compiler.  Still need to work on
getting output from mc to evaluate and type check
properly.


Revision 3381 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 14 22:45:03 2001 UTC (19 years, 9 months ago) by emre
File length: 540 byte(s)
Diff to previous 3377
Mc_theory now pulls together everything in
this theory.  Fir_auto defines an automation
tactic that can be used for evaluation.
Also added some support for allocUnion.


Revision 3377 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 12 21:03:34 2001 UTC (19 years, 9 months ago) by emre
File length: 538 byte(s)
Diff to previous 3374
Improved automation on type checking rules.
Added types to let/set Subscript terms.


Revision 3374 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 27 17:53:21 2001 UTC (19 years, 9 months ago) by emre
File length: 520 byte(s)
Diff to previous 3370
Commit of type checking rules for FIR programs.
Unlikely that all programs will type check
properly at this point (some incredibly simple
expressions don't check as I expected they
would), but this is something
to start from and I'm working on cleaning
some things up.


Revision 3370 - (view) (download) (annotate) - [select for diffs]
Modified Tue Aug 14 07:50:26 2001 UTC (19 years, 10 months ago) by emre
File length: 468 byte(s)
Diff to previous 3369
Everything that I had before should be state aware now. :)
Fir_test now has a few test cases, and more will be needed
to make sure everything is working properly.

The complex1 test case blows up horribly right now.
It evaluates perfectly well, but takes an amazingly
large amount of resources.  The .prlb file (not included) for that
one proof is 8.4 MB and MetaPRL ~64MB of RAM and 2 minutes on a
1 GHz Pentium III system.
After the proof, the "counts" were [2, ~34000] for that proof
(took me 2 steps).  After restarting MetaPRL and reloading the proof,
the counts were [2,290483].  Needless to say, something needs
to be done concerning efficiency.  As far as I can tell, things
are not being reduced in an optimal order. I'll be looking more
into this.


Revision 3369 - (view) (download) (annotate) - [select for diffs]
Modified Sat Aug 11 05:58:46 2001 UTC (19 years, 10 months ago) by emre
File length: 502 byte(s)
Diff to previous 3360
Uploading some new files and some minor changes so
that I can get some help in understanding what is going
on with the Fir_state / Fir_itt_state code.


Revision 3360 - (view) (download) (annotate) - [select for diffs]
Modified Sat Aug 4 18:39:51 2001 UTC (19 years, 10 months ago) by emre
File length: 452 byte(s)
Diff to previous 3359
- Updated some display forms.
- Organized the term declarations to be in more logical locations.
- There should be terms for most of the items in the FIR now.
- Still need to work on semantics of the terms and rewrites.


Revision 3359 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 2 16:22:32 2001 UTC (19 years, 10 months ago) by emre
File length: 452 byte(s)
Diff to previous 3349
Updated to compile fir_ty and fir_int_set now.


Revision 3349 - (view) (download) (annotate) - [select for diffs]
Added Thu Jul 26 04:21:46 2001 UTC (19 years, 10 months ago) by emre
File length: 423 byte(s)
Initial import.  mc is the name of Jason's compiler project, and functional
internal representation referrs to one of the stages in the compiler.  This
theory will hopefully be a formalization of that representation in MetaPRL.

The files right now are far from useful/complete.
(fir_exp.ml is unduly messy since it reflects a talk I had with Jason today and
so has lots of notes and ad hoc code.)  Hopefully, I'll also add some comments
that will make the files a bit more readable to people who know nothing
about the compiler.


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