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  Path
+4 -6 metaprl/Makefile
+1 -1 metaprl/doc/htmlman/mp-people.html
+2 -2 metaprl/filter/base/filter_prog.ml
+10 -3 metaprl/filter/base/filter_summary.ml
+3 -3 metaprl/filter/base/term_grammar.ml
Properties metaprl/mk
+16 -12 metaprl/mk/make_config.sh
+3 -9 metaprl/mk/preface
+1 -5 metaprl/refiner/reflib/ml_term.ml
+1274 -3989 metaprl/theories/itt/itt_decidable.prla
+65 -67 metaprl/theories/itt/itt_int_base.prla
+272 -274 metaprl/theories/itt/itt_record.prla
+86 -86 metaprl/theories/mc/fir_type.prla
+88 -88 metaprl/theories/mc/fir_type_exp.prla
+88 -88 metaprl/theories/mc/fir_type_int.prla
+87 -87 metaprl/theories/mc/fir_type_state.prla
+1 -1 metaprl/theories/ocaml/Makefile
+1 -1 metaprl/theories/ocaml/ocaml_expr_df.ml

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  Path
+1 -6 metaprl/theories/mc/Makefile
+5 -16 metaprl/theories/mc/README
Added metaprl/theories/mc/fir_eval.ml
Properties metaprl/theories/mc/fir_eval.ml
Added metaprl/theories/mc/fir_eval.mli
Properties metaprl/theories/mc/fir_eval.mli
+66 -110 metaprl/theories/mc/fir_exp.ml
+33 -30 metaprl/theories/mc/fir_exp.mli
Deleted metaprl/theories/mc/fir_int.ml
Deleted metaprl/theories/mc/fir_int.mli
+2 -10 metaprl/theories/mc/fir_int_set.ml
+2 -1 metaprl/theories/mc/fir_int_set.mli
Deleted metaprl/theories/mc/fir_state.ml
Deleted metaprl/theories/mc/fir_state.mli
+0 -55 metaprl/theories/mc/fir_ty.ml
+0 -32 metaprl/theories/mc/fir_ty.mli
+2 -1 metaprl/theories/mc/fir_type_exp.ml
+0 -1 metaprl/theories/mc/fir_type_exp.mli
+0 -1 metaprl/theories/mc/fir_type_int.mli
Deleted metaprl/theories/mc/fir_type_state.ml
Deleted metaprl/theories/mc/fir_type_state.mli
Deleted metaprl/theories/mc/fir_type_state.prla
+5 -6 metaprl/theories/mc/mc_theory.ml
+5 -6 metaprl/theories/mc/mc_theory.mli

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  Path
+3 -0 metaprl/theories/mc/Makefile
Added metaprl/theories/mc/fir_deadcode.ml
Properties metaprl/theories/mc/fir_deadcode.ml
Added metaprl/theories/mc/fir_deadcode.mli
Properties metaprl/theories/mc/fir_deadcode.mli
Added metaprl/theories/mc/fir_deadcode.prla
Properties metaprl/theories/mc/fir_deadcode.prla
+12 -2 metaprl/theories/mc/fir_eval.ml
+5 -0 metaprl/theories/mc/fir_eval.mli
+243 -36 metaprl/theories/mc/fir_exp.ml
+72 -39 metaprl/theories/mc/fir_exp.mli
Added metaprl/theories/mc/fir_marshal.ml
Properties metaprl/theories/mc/fir_marshal.ml
Added metaprl/theories/mc/fir_marshal.mli
Properties metaprl/theories/mc/fir_marshal.mli
Added metaprl/theories/mc/fir_rawint_set.ml
Properties metaprl/theories/mc/fir_rawint_set.ml
Added metaprl/theories/mc/fir_rawint_set.mli
Properties metaprl/theories/mc/fir_rawint_set.mli
+4 -0 metaprl/theories/mc/fir_ty.ml
+5 -0 metaprl/theories/mc/fir_ty.mli
+3 -0 metaprl/theories/mc/mc_theory.ml
+3 -0 metaprl/theories/mc/mc_theory.mli

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  Path
+8 -0 metaprl/theories/mc/fir_int_set.ml
+6 -0 metaprl/theories/mc/fir_int_set.mli
+8 -0 metaprl/theories/mc/fir_rawint_set.ml
+6 -0 metaprl/theories/mc/fir_rawint_set.mli
+21 -0 metaprl/theories/mc/fir_test.ml

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  Path
+0 -1 metaprl/theories/mc/Makefile
+11 -0 metaprl/theories/mc/README
+5 -9 metaprl/theories/mc/fir_deadcode.ml
+1 -2 metaprl/theories/mc/fir_deadcode.mli
+24 -31 metaprl/theories/mc/fir_eval.ml
+2 -4 metaprl/theories/mc/fir_eval.mli
+12 -0 metaprl/theories/mc/fir_exp.ml
+4 -0 metaprl/theories/mc/fir_exp.mli
+16 -1 metaprl/theories/mc/fir_marshal.ml
+1 -1 metaprl/theories/mc/fir_marshal.mli
+0 -1 metaprl/theories/mc/mc_theory.ml
+0 -1 metaprl/theories/mc/mc_theory.mli

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  Path
+1 -0 metaprl/theories/mc/Makefile
Added metaprl/theories/mc/fir_const_elim.ml
Properties metaprl/theories/mc/fir_const_elim.ml
Added metaprl/theories/mc/fir_const_elim.mli
Properties metaprl/theories/mc/fir_const_elim.mli
Added metaprl/theories/mc/fir_const_elim.prla
Properties metaprl/theories/mc/fir_const_elim.prla
+2 -2 metaprl/theories/mc/fir_deadcode.ml
+66 -7 metaprl/theories/mc/fir_eval.ml
+24 -0 metaprl/theories/mc/fir_eval.mli
+25 -0 metaprl/theories/mc/fir_test.ml
+1 -0 metaprl/theories/mc/mc_theory.ml
+1 -0 metaprl/theories/mc/mc_theory.mli

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  Path
+1 -1 metaprl/Makefile
+18 -16 metaprl/filter/base/filter_ocaml.ml
+14 -11 metaprl/filter/base/filter_summary.ml
+2 -2 metaprl/filter/base/term_grammar.ml
+2 -2 metaprl/filter/boot/proof_term_boot.ml
+20 -22 metaprl/library/basic.ml
+2 -2 metaprl/library/link.ml
+44 -50 metaprl/library/nuprl5.ml
+2 -2 metaprl/library/orb.ml
+2 -2 metaprl/mk/cvs_realclean.sh
+12 -8 metaprl/mllib/mp_big_int.ml
+7 -7 metaprl/mllib/mp_big_int.mli
+15 -9 metaprl/mllib/mp_num.ml
+7 -10 metaprl/mllib/mp_num.mli
+7 -4 metaprl/theories/base/base_meta.ml
+1 -1 metaprl/theories/tactic/summary.ml

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  Path
+38 -3 metaprl/theories/mc/fir_const_elim.ml
+8 -0 metaprl/theories/mc/fir_const_elim.mli
+744 -295 metaprl/theories/mc/fir_const_elim.prla
+95 -2 metaprl/theories/mc/fir_eval.ml
+21 -1 metaprl/theories/mc/fir_eval.mli
Added metaprl/theories/mc/fir_eval.prla
Properties metaprl/theories/mc/fir_eval.prla
+5 -3 metaprl/theories/mc/fir_exp.ml
+1 -1 metaprl/theories/mc/fir_exp.mli
+13 -0 metaprl/theories/mc/fir_test.ml

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