Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-10-05 17:04:44 -0700 (Fri, 05 Oct 2001)
Revision: 3418
Log message:
Returned the term representation of the Ocaml record expression
to what we used for Caml 2.x ASTs.
This way we are keeping the correct binding structure
and are staying backwards compatibile with old .prla and display forms.
Changes | Path |
+12 -28 | metaprl/filter/base/filter_ocaml.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-10-05 18:40:01 -0700 (Fri, 05 Oct 2001)
Revision: 3419
Log message:
- I got rid of "MAKE_JOBS" variable in mk/config. If you want "make" to keep
running jobs in parallel when building MetaPRL, you should either
a) Make sure you have MAKEFLAGS environment variable contains appropriate "-j nn"
b) pass "-j nn" manually to make
c) Add "-j nn" to the MAKE_OPTS in mk/config (make will print warnings if you do this).
- I created a new config file - mk/config.local where people can put their
customized settings that do not belong to mk/config
- I fixed the problems caused by Camlp4 switch to keeping "escaped" strings
in the ASTs
- I got rid of the warnings caused by the outdated resource infos in old .prla
- I renamed back "Summary!parent2" -> "Summary!parent" and "Summary!resource2" ->
"Summary!resource" for backwards compatibility with old .prla and display forms.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-10-06 07:09:39 -0700 (Sat, 06 Oct 2001)
Revision: 3420
Log message:
Yesterday's commit was missing a fix to the mc .prla
Changes | Path |
+4 -6 | metaprl/theories/mc/fir_type_state.prla |
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-10-06 22:09:57 -0700 (Sat, 06 Oct 2001)
Revision: 3421
Log message:
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.
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-10-18 02:07:10 -0700 (Thu, 18 Oct 2001)
Revision: 3422
Log message:
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.
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-10-18 17:37:58 -0700 (Thu, 18 Oct 2001)
Revision: 3423
Log message:
Added terms for open and infinite bounds
in Fir_int_set and Fir_rawint_set. Also
Added some simple test cases for the
deadcode elimination tactic.
Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-10-22 14:05:57 -0700 (Mon, 22 Oct 2001)
Revision: 3424
Log message:
Added an example of mutually recursive functions based on records.
Changes | Path |
+27 -0 | metaprl/theories/itt/itt_record_exm.ml |
+1 -0 | metaprl/theories/itt/itt_record_exm.mli |
+3269 -1555 | metaprl/theories/itt/itt_record_exm.prla |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2001-10-23 21:34:08 -0700 (Tue, 23 Oct 2001)
Revision: 3425
Log message:
czf_itt_cyclic_subgroup.ppo added.
Changes | Path |
Added | metaprl/theories/czf/czf_itt_cyclic_subgroup.ppo |
Properties | metaprl/theories/czf/czf_itt_cyclic_subgroup.ppo |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-10-24 06:39:19 -0700 (Wed, 24 Oct 2001)
Revision: 3426
Log message:
Generated files (such as .ppo) should not be in CVS.
Changes | Path |
Deleted | metaprl/theories/czf/czf_itt_cyclic_subgroup.ppo |
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-10-26 22:05:38 -0700 (Fri, 26 Oct 2001)
Revision: 3427
Log message:
- Added more terms for FIR entities (trig functions).
- Changed deadcode elimination slightly.
- Changed evalutation of tyInt arithmetic to sort of
do some type checking.
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-10-27 18:48:19 -0700 (Sat, 27 Oct 2001)
Revision: 3428
Log message:
- Added support for evaluating "raw ints".
- Started adding support of elimination of
constants.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-10-28 14:06:32 -0800 (Sun, 28 Oct 2001)
Revision: 3429
Log message:
- Made sure that div by zero and mod zero raise proper exceptions in
Mp_big_int, Mp_num and Base_meta
- Made the Mp_num.num and Mp_big_int.big_int types abstract.
- Minor changes in the "make realclean" scripts.
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-10-28 23:02:17 -0800 (Sun, 28 Oct 2001)
Revision: 3430
Log message:
- Added some simple RawInt evaulation and constant elimination.
- Added rewrites for common powers (e.g. 2^32).
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-10-29 11:52:31 -0800 (Mon, 29 Oct 2001)
Revision: 3431
Log message:
Inefficiantly implemented termC added. It is similar to funC but function
receives term o be rewritten instead of whole environment.
Changes | Path |
+1 -0 | metaprl/filter/boot/conversionals_boot.ml |
+1 -0 | metaprl/filter/boot/rewrite_boot.ml |
+2 -0 | metaprl/filter/boot/tactic_boot_sig.mlz |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-10-29 11:57:13 -0800 (Mon, 29 Oct 2001)
Revision: 3432
Log message:
Small step toward arithT. I've committed it because I want to show
to Alexey some strange behaviour.
Changes | Path |
+22 -0 | metaprl/theories/itt/itt_int_arith.ml |
+4 -0 | metaprl/theories/itt/itt_int_arith.mli |
Added | metaprl/theories/itt/itt_int_arith.prla |
Properties | metaprl/theories/itt/itt_int_arith.prla |