Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-01 18:04:50 -0700 (Fri, 01 Oct 2004)
Revision: 6211
Log message:

      Proved couple more induction principles (with Xin's help).
      

Changes  Path
+12 -10 metaprl/theories/itt/itt_nat.ml
+2498 -1960 metaprl/theories/itt/itt_nat.prla
+1373 -1491 metaprl/theories/itt/itt_poly.prla

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-04 01:59:01 -0700 (Mon, 04 Oct 2004)
Revision: 6214
Log message:

      Added a quotient elimination for squiddle equality (for Yegor).
      

Changes  Path
+5 -2 metaprl/theories/itt/itt_quotient.ml
+2710 -3146 metaprl/theories/itt/itt_quotient.prla

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-07 19:52:24 -0700 (Thu, 07 Oct 2004)
Revision: 6220
Log message:

      mp.opt expects MP_ROOT to be set.
      

Changes  Path
+4 -0 metaprl/editor/ml/mpopt.bat

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-07 22:25:26 -0700 (Thu, 07 Oct 2004)
Revision: 6221
Log message:

      Fixed bug 327 - added sequents supprot to TermMan.free_meta_variables.
      (Note - this function is only ever used by JProver, it's an informal hack
      to work around JProver deficiencies).
      

Changes  Path
+25 -1 metaprl/refiner/term_ds/term_man_ds.ml
+3 -1 metaprl/refiner/term_gen/term_man_gen.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-08 19:04:25 -0700 (Fri, 08 Oct 2004)
Revision: 6222
Log message:

      Working on rewrite-based normalization of terms (polynomials) over rationals.
      I actually have some problems that I'll post to the newsgroup.
      

Changes  Path
+184 -2 metaprl/theories/itt/itt_rat.ml
+16 -1 metaprl/theories/itt/itt_rat.mli
Added metaprl/theories/itt/itt_rat2.ml
Properties metaprl/theories/itt/itt_rat2.ml
Added metaprl/theories/itt/itt_rat2.mli
Properties metaprl/theories/itt/itt_rat2.mli

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-08 19:17:59 -0700 (Fri, 08 Oct 2004)
Revision: 6223
Log message:

      Forgot .prla
      

Changes  Path
Added metaprl/theories/itt/itt_rat2.prla
Properties metaprl/theories/itt/itt_rat2.prla

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-09 16:28:53 -0700 (Sat, 09 Oct 2004)
Revision: 6224
Log message:

      repeatC used to always do at least two identity steps in the end.
      Changing it so that it only does at most one.
      

Changes  Path
+4 -0 metaprl/OMakefile
+0 -4 metaprl/support/tactics/top_conversionals.ml
+0 -1 metaprl/support/tactics/top_conversionals.mli
+4 -8 metaprl/tactics/proof/conversionals_boot.ml
+1 -2 metaprl/tactics/proof/tactic_boot_sig.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-09 20:57:16 -0700 (Sat, 09 Oct 2004)
Revision: 6225
Log message:

      Replaced quotient-based definition with subset-based.
      It does not normalizes rational number representation after each operation yet.
      I commit it because I think I found a bug in the rewriter.
      

Changes  Path
+273 -387 metaprl/theories/itt/itt_rat.ml
+71 -53 metaprl/theories/itt/itt_rat.mli
+7714 -11523 metaprl/theories/itt/itt_rat.prla

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 18:49:09 -0700 (Sun, 10 Oct 2004)
Revision: 6226
Log message:

      Sligthly nicer display from for spread.
      

Changes  Path
+3 -4 metaprl/theories/itt/itt_dprod.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 18:52:35 -0700 (Sun, 10 Oct 2004)
Revision: 6227
Log message:

      Remove macropp on "omake clean"
      

Changes  Path
+1 -1 metaprl/util/OMakefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 19:59:02 -0700 (Sun, 10 Oct 2004)
Revision: 6228
Log message:

      Only compare the binary name from the command line with "mp.opt"/"mp.top"
      when "!omake" is used, not as startup. This is necessary to avoid an annoying
      warning when using the mp.run binary.
      

Changes  Path
+14 -17 metaprl/support/shell/shell_syscall.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 20:46:26 -0700 (Sun, 10 Oct 2004)
Revision: 6229
Log message:

      (Bug 330) When coming up with variable names for bound variables, it used
      to be the case that we did not take precautions against clashes within the bvars
      list of a single bterm. This commit fixes this problem.
      

Changes  Path
+7 -1 metaprl/refiner/rewrite/rewrite_build_contractum.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 21:21:54 -0700 (Sun, 10 Oct 2004)
Revision: 6230
Log message:

      A few updates to how contexts are handled in display forms:
      - Allow free context parameters on the RHS on informal rewrites.
      - When parsing display forms, deduce the default context parameters
      for the whole display form at once, instead of seperately for each part of it.
      

Changes  Path
+13 -5 metaprl/filter/filter/filter_parse.ml
+1 -1 metaprl/filter/filter/term_grammar.ml
+3 -3 metaprl/refiner/rewrite/rewrite_compile_contractum.ml

Changes by: ( at unknown.email)
Date: 2004-10-10 22:34:11 -0700 (Sun, 10 Oct 2004)
Revision: 6232
Log message:

      This commit was manufactured by cvs2svn to create branch 'new_parser2'.

Changes  Path
Copied metaprl-branches/new_parser2
Copied mpcompiler-branches/new_parser2
Copied texinputs-branches/new_parser2
Deleted texinputs-branches/new_parser2/1cm.sty
Deleted texinputs-branches/new_parser2/1cml.sty
Deleted texinputs-branches/new_parser2/Makefile
Deleted texinputs-branches/new_parser2/Makefile-common
Deleted texinputs-branches/new_parser2/PPR-macros.tex
Deleted texinputs-branches/new_parser2/PPRmyppr.sty
Deleted texinputs-branches/new_parser2/bcp.bib
Deleted texinputs-branches/new_parser2/citlogo.eps
Deleted texinputs-branches/new_parser2/citlogo2.eps
Deleted texinputs-branches/new_parser2/config.ppr
Deleted texinputs-branches/new_parser2/cornell-logo.eps
Deleted texinputs-branches/new_parser2/dag50.eps
Deleted texinputs-branches/new_parser2/der.tex
Deleted texinputs-branches/new_parser2/gate.eps
Deleted texinputs-branches/new_parser2/gate.pdf
Binary texinputs-branches/new_parser2/gccuny-logo.eps
Binary texinputs-branches/new_parser2/gccuny-logo.gif
Binary texinputs-branches/new_parser2/gccuny-logo.pdf
Deleted texinputs-branches/new_parser2/include.tex
Deleted texinputs-branches/new_parser2/omscmsy.fd
Deleted texinputs-branches/new_parser2/ot1cmr.fd
Deleted texinputs-branches/new_parser2/ot1cmss.fd
Deleted texinputs-branches/new_parser2/ot1lcmss.fd
Deleted texinputs-branches/new_parser2/ot1lcmtt.fd
Deleted texinputs-branches/new_parser2/pprpdf
Deleted texinputs-branches/new_parser2/proof.sty
Deleted texinputs-branches/new_parser2/slides-nogin.cls
Deleted texinputs-branches/new_parser2/splncs.bst
Deleted texinputs-branches/new_parser2/umsa.fd
Deleted texinputs-branches/new_parser2/umsb.fd

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 03:10:37 -0700 (Mon, 11 Oct 2004)
Revision: 6233
Log message:

      I've merged the new_parser branch with the trunk. I am putting the result
      of the merge onto a new branch - "new_parser2" as there seems to be a few
      issues with it.
      

Changes  Path
Added metaprl/filter/base/filter_grammar.ml
Properties metaprl/filter/base/filter_grammar.ml
Added metaprl/filter/base/filter_grammar.mli
Properties metaprl/filter/base/filter_grammar.mli
Properties metaprl/tmp
Added metaprl/tmp/OMakefile
Properties metaprl/tmp/OMakefile
Added metaprl/util/genmagic.ml
Properties metaprl/util/genmagic.ml
+3 -3 metaprl-branches/new_parser2/OMakefile
+5 -5 metaprl-branches/new_parser2/editor/emacs/caml.el
Binary metaprl-branches/new_parser2/editor/emacs/caml.elc
+1 -0 metaprl-branches/new_parser2/editor/ml/OMakefile
+1 -0 metaprl-branches/new_parser2/filter/OMakefile
+2 -1 metaprl-branches/new_parser2/filter/base/Files
+256 -127 metaprl-branches/new_parser2/filter/base/filter_cache_fun.ml
+0 -1 metaprl-branches/new_parser2/filter/base/filter_cache_fun.mli
+53 -25 metaprl-branches/new_parser2/filter/base/filter_summary.ml
+78 -59 metaprl-branches/new_parser2/filter/base/filter_summary_type.ml
+30 -29 metaprl-branches/new_parser2/filter/base/filter_type.ml
+220 -38 metaprl-branches/new_parser2/filter/filter/filter_parse.ml
+32 -17 metaprl-branches/new_parser2/filter/filter/filter_prog.ml
+30 -10 metaprl-branches/new_parser2/filter/filter/term_grammar.ml
+2 -1 metaprl-branches/new_parser2/filter/filter/term_grammar.mli
+29 -30 metaprl-branches/new_parser2/mllib/file_base_type.ml
+2 -3 metaprl-branches/new_parser2/refiner/refbase/opname.ml
+1 -1 metaprl-branches/new_parser2/refiner/reflib/term_match_table.mli
+3 -0 metaprl-branches/new_parser2/refiner/refsig/term_shape_sig.ml
+2 -0 metaprl-branches/new_parser2/refiner/refsig/term_sig.ml
+2 -0 metaprl-branches/new_parser2/refiner/rewrite/rewrite_types.ml
+2 -0 metaprl-branches/new_parser2/refiner/term_ds/term_ds_sig.ml
+21 -45 metaprl-branches/new_parser2/refiner/term_gen/term_shape_gen.ml
+1 -1 metaprl-branches/new_parser2/support/display/OMakefile
+9 -4 metaprl-branches/new_parser2/support/shell/package_info.ml
+4 -0 metaprl-branches/new_parser2/support/shell/package_info.mli
+6 -0 metaprl-branches/new_parser2/support/shell/shell_core.ml
+2 -1 metaprl-branches/new_parser2/support/shell/shell_package.ml
+40 -0 metaprl-branches/new_parser2/support/shell/shell_state.ml
+2 -0 metaprl-branches/new_parser2/support/shell/shell_state.mli
Properties metaprl-branches/new_parser2/theories/base
+5 -0 metaprl-branches/new_parser2/util/OMakefile
Added mpcompiler/mmc/core/mmc_core_grammar.ml
Properties mpcompiler/mmc/core/mmc_core_grammar.ml
Added mpcompiler/mmc/core/mmc_core_grammar.mli
Properties mpcompiler/mmc/core/mmc_core_grammar.mli
Added mpcompiler/mmc/test/mmc_grammar.ml
Properties mpcompiler/mmc/test/mmc_grammar.ml
Added mpcompiler/mmc/test/mmc_grammar.mli
Properties mpcompiler/mmc/test/mmc_grammar.mli
Properties mpcompiler-branches/new_parser2/mmc
+1 -0 mpcompiler-branches/new_parser2/mmc/core/Files
+38 -0 mpcompiler-branches/new_parser2/mmc/core/mmc_core_ast.ml
+121 -1 mpcompiler-branches/new_parser2/mmc/core/mmc_core_ast.mli
+10 -0 mpcompiler-branches/new_parser2/mmc/extensions/bool/mmc_ext_bool.ml
+29 -0 mpcompiler-branches/new_parser2/mmc/extensions/bool/mmc_ext_bool.mli
+17 -0 mpcompiler-branches/new_parser2/mmc/extensions/int/mmc_ext_int.ml
+68 -0 mpcompiler-branches/new_parser2/mmc/extensions/int/mmc_ext_int.mli
+1 -0 mpcompiler-branches/new_parser2/mmc/extensions/operator/mmc_ext_operator.mli
+1 -0 mpcompiler-branches/new_parser2/mmc/test/Files
+15 -10 mpcompiler-branches/new_parser2/mmc/test/mmc_int_test.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 03:13:25 -0700 (Mon, 11 Oct 2004)
Revision: 6234
Log message:

      In my previous commit I've accidentally committed the new files onto
      the trunk, removing them from the trunk for now.
      

Changes  Path
Deleted metaprl/filter/base/filter_grammar.ml
Deleted metaprl/filter/base/filter_grammar.mli
Deleted metaprl/util/genmagic.ml
Deleted mpcompiler/mmc/core/mmc_core_grammar.ml
Deleted mpcompiler/mmc/core/mmc_core_grammar.mli
Deleted mpcompiler/mmc/test/mmc_grammar.ml
Deleted mpcompiler/mmc/test/mmc_grammar.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 03:27:47 -0700 (Mon, 11 Oct 2004)
Revision: 6235
Log message:

      Re-adding files properly onto the new_parser2 branch.
      

Changes  Path
Added metaprl-branches/new_parser2/filter/base/filter_grammar.ml
Properties metaprl-branches/new_parser2/filter/base/filter_grammar.ml
Added metaprl-branches/new_parser2/filter/base/filter_grammar.mli
Properties metaprl-branches/new_parser2/filter/base/filter_grammar.mli
Properties metaprl-branches/new_parser2/tmp
Added metaprl-branches/new_parser2/tmp/OMakefile
Properties metaprl-branches/new_parser2/tmp/OMakefile
Added metaprl-branches/new_parser2/util/genmagic.ml
Properties metaprl-branches/new_parser2/util/genmagic.ml
Added mpcompiler-branches/new_parser2/mmc/core/mmc_core_grammar.ml
Properties mpcompiler-branches/new_parser2/mmc/core/mmc_core_grammar.ml
Added mpcompiler-branches/new_parser2/mmc/core/mmc_core_grammar.mli
Properties mpcompiler-branches/new_parser2/mmc/core/mmc_core_grammar.mli
Added mpcompiler-branches/new_parser2/mmc/test/mmc_grammar.ml
Properties mpcompiler-branches/new_parser2/mmc/test/mmc_grammar.ml
Added mpcompiler-branches/new_parser2/mmc/test/mmc_grammar.mli
Properties mpcompiler-branches/new_parser2/mmc/test/mmc_grammar.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 20:43:21 -0700 (Mon, 11 Oct 2004)
Revision: 6237
Log message:

      - (Bug 303) Made sure that in shell_p4 (AKA editor/ml/mp AKA mp.run)
      synchronize and unsynchronize are properly matched.
      
      - Use shell_p4 to open the basic modules (this way the basic commands
      such as cd, ls, etc are available w/o having to #use "x.ml").
      

Changes  Path
+1 -1 metaprl/editor/ml/mp
+21 -20 metaprl/editor/ml/shell_p4.ml
+0 -10 metaprl/editor/ml/x.ml
+9 -7 metaprl/support/shell/shell_state.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-10-12 01:45:01 -0700 (Tue, 12 Oct 2004)
Revision: 6238
Log message:

      Added all basic stuff for itt_reflection, including arities of bterms
      and elimination on bterms.
      
      In Base_reflection, a simple_bterm does not have to be a bterm.
      

Changes  Path
+8 -12 metaprl/theories/base/base_reflection.ml
+235 -49 metaprl/theories/itt/itt_reflection.ml
+13 -3 metaprl/theories/itt/itt_reflection.mli
+4145 -1294 metaprl/theories/itt/itt_reflection.prla
+0 -2 metaprl/theories/itt/itt_reflection_test.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-12 13:14:30 -0700 (Tue, 12 Oct 2004)
Revision: 6239
Log message:

      Made sure theories.pdf compiles.
      

Changes  Path
+0 -1 metaprl/theories/itt/OMakefile
+1 -1 metaprl/theories/itt/itt_rat.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-15 16:22:40 -0700 (Fri, 15 Oct 2004)
Revision: 6241
Log message:

      The tests that require ITT should not be compiled unless ITT is listed in
      the THEORIES variable.
      

Changes  Path
+6 -3 metaprl/editor/ml/OMakefile
+1 -1 metaprl/editor/ml/tests/OMakefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-15 16:28:44 -0700 (Fri, 15 Oct 2004)
Revision: 6242
Log message:

      Fixing a typo in my previous commit.
      

Changes  Path
+1 -1 metaprl/editor/ml/OMakefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-15 17:45:47 -0700 (Fri, 15 Oct 2004)
Revision: 6243
Log message:

      Made sure CIC compiles.
      

Changes  Path
+25 -25 metaprl/filter/filter/filter_parse.ml
+1 -0 metaprl/refiner/refsig/term_meta_sig.ml
+5 -5 metaprl/theories/cic/cic_ind_type.ml
+1 -2 metaprl/theories/cic/cic_ind_type.mli
+1 -5 metaprl/theories/cic/cic_lambda.ml
+1 -3 metaprl/theories/cic/cic_lambda.mli

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-17 18:02:23 -0700 (Sun, 17 Oct 2004)
Revision: 6244
Log message:

      1. Addressing the bug 322 (first part about nat)
      2. Rationals are normalized pairs of integers now (gcd=1)
      3. Rational polynomial normalization
      ToDo: Grounding intermediate assertion of SupInf.
      Doing this efficently is somewhat challenging.
      

Changes  Path
+1 -2 metaprl/theories/itt/OMakefile
+46 -9 metaprl/theories/itt/itt_int_arith.ml
+5 -4 metaprl/theories/itt/itt_int_arith.mli
+5 -1 metaprl/theories/itt/itt_nat.ml
+1450 -1392 metaprl/theories/itt/itt_nat.prla
+266 -38 metaprl/theories/itt/itt_rat.ml
+23 -12 metaprl/theories/itt/itt_rat.mli
+9526 -5392 metaprl/theories/itt/itt_rat.prla
+48 -10 metaprl/theories/itt/itt_rat2.ml
+5049 -3207 metaprl/theories/itt/itt_rat2.prla
+215 -108 metaprl/theories/itt/itt_supinf.ml
+1 -0 metaprl/theories/itt/itt_supinf.mli

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-17 20:07:48 -0700 (Sun, 17 Oct 2004)
Revision: 6245
Log message:

      itt_int_arith - fixing a bug discovered while doing normalization for rationals
      itt_rat2 - improvement of the treatment for this bug
      

Changes  Path
+23 -5 metaprl/theories/itt/itt_int_arith.ml
+26 -12 metaprl/theories/itt/itt_rat2.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-18 05:29:18 -0700 (Mon, 18 Oct 2004)
Revision: 6246
Log message:

      Forgot to commit yesterday
      

Changes  Path
+26 -4 metaprl/refiner/reflib/supinf.ml
+4 -0 metaprl/refiner/reflib/supinf.mli

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-21 12:31:10 -0700 (Thu, 21 Oct 2004)
Revision: 6247
Log message:

      Forgot to remove temporary debug code. Sorry.
      

Changes  Path
+0 -2 metaprl/theories/itt/itt_int_arith.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-22 16:07:58 -0700 (Fri, 22 Oct 2004)
Revision: 6248
Log message:

      A bit of standartization of debug variables:
      - the "debug_foo" variable should have debug_name set to "foo", not "debug_foo"
        (less typing on the command line this way)
      - debug_description should be the same for all the instances of the same variable
        and it should be sufficiently descriptive to be meaningful w/o knowing which
        file it came from (see http://metaprl.org/developer-guide/debugging.html)
      

Changes  Path
+19 -11 metaprl/doc/htmlman/developer-guide/debugging.html
+0 -9 metaprl/filter/phobos/phobos_state.ml
+6 -6 metaprl/refiner/reflib/arith.ml
+1 -1 metaprl/refiner/reflib/supinf.ml
+1 -1 metaprl/refiner/term_ds/term_base_ds.ml
+1 -1 metaprl/support/shell/shell_browser.ml
+1 -1 metaprl/support/shell/shell_state.ml
+1 -1 metaprl/tactics/ensemble/remote_ensemble.ml
+4 -4 metaprl/theories/itt/itt_int_arith.ml
+2 -2 metaprl/theories/itt/itt_int_base.ml
+2 -2 metaprl/theories/itt/itt_mpoly2.ml
+2 -2 metaprl/theories/itt/itt_mpoly3.ml
+3 -3 metaprl/theories/itt/itt_supinf.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-22 16:14:36 -0700 (Fri, 22 Oct 2004)
Revision: 6249
Log message:

      (Bug 322) Itt_nat.nat2ge should not change the type from nat to int.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_nat.ml
+174 -155 metaprl/theories/itt/itt_nat.prla

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-22 20:29:30 -0700 (Fri, 22 Oct 2004)
Revision: 6253
Log message:

      With this fix arithT does not fail on /itt_nat/natFullInduction/1/1/1 even without
      last Aleksey's commit. See bug 322 for more comments.
      

Changes  Path
+1 -1 metaprl/refiner/reflib/arith.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-29 10:15:52 -0700 (Fri, 29 Oct 2004)
Revision: 6254
Log message:

      1.Added "nat{'n} in hyps" to ge_elim resource for Arith.
      2.As far as I understand indEquality was missing positivity hypothesis in the induction step subgoal.
      Luckily the proof didn't break when I've added that missing hyp.
      

Changes  Path
+5 -1 metaprl/theories/itt/itt_nat.ml
+861 -886 metaprl/theories/itt/itt_nat.prla

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-30 14:05:55 -0700 (Sat, 30 Oct 2004)
Revision: 6255
Log message:

      Fixes for proofs broken by a change in Itt_nat.indEquality made yesterday.
      

Changes  Path
+551 -508 metaprl/theories/itt/itt_poly.prla