Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 01:37:30 -0700 (Thu, 01 May 2003)
Revision: 4527
Log message:
Some of the proofs were missing.
| Changes | Path |
| +260 -72 | metaprl-branches/CS101_branch/theories/cs101/cs101_int.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 02:28:20 -0700 (Thu, 01 May 2003)
Revision: 4528
Log message:
Posting HW5
| Changes | Path |
| +1 -1 | metaprl-branches/CS101_branch/mk/preface |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-01 10:20:47 -0700 (Thu, 01 May 2003)
Revision: 4529
Log message:
Added FIR syntax.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-01 12:39:09 -0700 (Thu, 01 May 2003)
Revision: 4530
Log message:
*** empty log message ***
| Changes | Path |
| +5 -1 | metaprl/OMakefile |
| +1 -0 | metaprl/theories/experimental/mcc/fir/util/OMakefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 15:41:39 -0700 (Thu, 01 May 2003)
Revision: 4531
Log message:
linux-gnu is Linux
| Changes | Path |
| +3 -0 | metaprl/mk/preface |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 15:43:44 -0700 (Thu, 01 May 2003)
Revision: 4532
Log message:
Moved things around.
| Changes | Path |
| +3 -0 | metaprl/mk/preface |
| +0 -6 | metaprl/mk/rules |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-01 16:27:28 -0700 (Thu, 01 May 2003)
Revision: 4533
Log message:
Propagate funT changes into theories/experimental/compile.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 16:47:36 -0700 (Thu, 01 May 2003)
Revision: 4534
Log message:
The top-level directory for MetaPRL is now supposed to be just "metaprl"
(e.g. without a dash).
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-01 19:54:48 -0700 (Thu, 01 May 2003)
Revision: 4535
Log message:
*** empty log message ***
| Changes | Path |
| +3 -1 | metaprl/OMakefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-01 20:21:18 -0700 (Thu, 01 May 2003)
Revision: 4536
Log message:
Add -rectypes option to prlc.
| Changes | Path |
| +4 -3 | metaprl/OMakefile |
| +1 -0 | metaprl/filter/filter/OMakefile |
| +1 -0 | metaprl/filter/filter/prlcomp.ml |
| +16 -2 | metaprl/theories/experimental/mcc/fir/util/OMakefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-01 20:44:26 -0700 (Thu, 01 May 2003)
Revision: 4537
Log message:
Getting started on FIR<->term conversion.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 20:54:08 -0700 (Thu, 01 May 2003)
Revision: 4538
Log message:
- Spelling fixes
- Moved some of the bind-term+vars manipulation from Perv to Var
- Added couple of helper funs in var, used them to simplify a few tactics.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 21:32:45 -0700 (Thu, 01 May 2003)
Revision: 4539
Log message:
This is a first part of a directory restructuring.
I've created support/display, support/shell and support/tactics and
moved everything from theories/tactic and theories/ocaml into support.
P.S. This would break omake, sorry.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 21:54:27 -0700 (Thu, 01 May 2003)
Revision: 4540
Log message:
Moved and renamed:
theories/base/typeinf -> support/tactics/typeinf
theories/base/base_auto_tactic -> support/tactics/auto_tactic
theories/base/base_dtactic -> support/tactics/dtactic
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 21:58:37 -0700 (Thu, 01 May 2003)
Revision: 4541
Log message:
Moved and renamed:
theories/base/typeinf -> support/tactics/typeinf
theories/base/base_auto_tactic -> support/tactics/auto_tactic
theories/base/base_dtactic -> support/tactics/dtactic
P.S. This is the "tail" of the commit - previous commit failed half-way
through :-( Turns out that if you simultaneously run "cvs commit" and
"cvs update" on a single tree (from different machines over NFS),
they will fight...
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-02 01:16:44 -0700 (Fri, 02 May 2003)
Revision: 4542
Log message:
Updated the debug (OCaml) toploop to use correct path to term printer.
| Changes | Path |
| +1 -1 | metaprl/editor/ml/shell_p4.ml |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-02 03:40:19 -0700 (Fri, 02 May 2003)
Revision: 4543
Log message:
Defined quotient group.
Added universe equality for mem, subset, and member.
Changes by: ( at unknown.email)
Date: 2003-05-02 03:40:19 -0700 (Fri, 02 May 2003)
Revision: 4544
Log message:
This commit was manufactured by cvs2svn to create branch 'CS101_branch'.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-02 18:52:05 -0700 (Fri, 02 May 2003)
Revision: 4545
Log message:
to reflect some module renaming
| Changes | Path |
| +207 -239 | metaprl/theories/itt/itt_cyclic_group.prla |
| +2 -2 | metaprl/theories/itt/itt_quotient_group.ml |
| +2 -2 | metaprl/theories/itt/itt_quotient_group.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-02 19:55:36 -0700 (Fri, 02 May 2003)
Revision: 4546
Log message:
Moved the shell files from editor/ml to support/shell.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-03 09:04:11 -0700 (Sat, 03 May 2003)
Revision: 4547
Log message:
Added config.default, for use in Win32.
| Changes | Path |
| Added | metaprl/mk/config.default |
| Properties | metaprl/mk/config.default |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-03 10:26:35 -0700 (Sat, 03 May 2003)
Revision: 4548
Log message:
Updated omake system to match Aleksey's changes.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-03 13:26:47 -0700 (Sat, 03 May 2003)
Revision: 4549
Log message:
Ported MetaPRL to native Win32. The docs for this commit
are in README.WIN32.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-03 13:28:11 -0700 (Sat, 03 May 2003)
Revision: 4550
Log message:
Forgot to add the script file to run MetaPRL in Win32.
| Changes | Path |
| Added | metaprl/editor/ml/mptop.bat |
| Properties | metaprl/editor/ml/mptop.bat |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-03 14:11:10 -0700 (Sat, 03 May 2003)
Revision: 4551
Log message:
My previous fix to Yegor's compilation problem was incomplete. But this
should fix it - now the library code should not ctry to resolve anything,
unless it is actually used.
| Changes | Path |
| +1 -4 | metaprl/library/basic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-03 18:51:55 -0700 (Sat, 03 May 2003)
Revision: 4552
Log message:
- Updated the editor/ml/tests to use the new funT
- A few more display forms to address Yegor's "make latex" problems.
| Changes | Path |
| +92 -96 | metaprl/editor/ml/tests/prop-pigeon.ml |
| +7 -0 | metaprl/support/display/comment.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-03 19:08:39 -0700 (Sat, 03 May 2003)
Revision: 4553
Log message:
Removing the cons files (they are outdated anyway).
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-03 20:32:29 -0700 (Sat, 03 May 2003)
Revision: 4554
Log message:
Documentation updates.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-03 21:28:07 -0700 (Sat, 03 May 2003)
Revision: 4555
Log message:
Some documentation added.
| Changes | Path |
| +111 -11 | metaprl/theories/itt/itt_int_arith.ml |
| +2 -13 | metaprl/theories/itt/itt_int_base.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-03 21:43:21 -0700 (Sat, 03 May 2003)
Revision: 4556
Log message:
A few more display froms for Yegor.
| Changes | Path |
| +6 -0 | metaprl/support/display/comment.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-04 14:40:54 -0700 (Sun, 04 May 2003)
Revision: 4557
Log message:
These are true type fonts for MetaPRL.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-04 14:52:38 -0700 (Sun, 04 May 2003)
Revision: 4558
Log message:
I just noticed that metaprl-cvs will accept .gz files as binary.
Added true-type fonts, mainly for use on Windows. They are derived
from the X11 Luxi fonts.
Changed several mathbb display forms in nuprl_font.ml. Somehow,
the UTF-8 encoding was invalid, and I wasn't sure what was intended.
The changed chars now display as bold caps; feel free to change this
back if there is a better way.
| Changes | Path |
| +22 -22 | metaprl/support/display/nuprl_font.ml |
| Added | metaprl/util/unicode.ml |
| Properties | metaprl/util/unicode.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-04 15:11:21 -0700 (Sun, 04 May 2003)
Revision: 4559
Log message:
More minor changes for Win32. For some reason Itt_collection.isect_wf
gives me a rewrite error at load time...
| Changes | Path |
| +21 -2 | metaprl/README.WIN32 |
| Properties | metaprl/editor/ml |
| +2 -2 | metaprl/editor/ml/OMakefile |
| +6 -13 | metaprl/theories/itt/itt_collection.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-04 16:16:48 -0700 (Sun, 04 May 2003)
Revision: 4560
Log message:
1.Display form of nequal{;} was missing.
2.All intermediate tactics/conversionals removed from itt_int_arith.mli
(they were there for debugging).
Only normalizeC and arithT are there (well, thenLocalT will be removed soon).
3.add_normalizeC replaced with normalizeC in itt_cyclic_group
(add_normalizeC is no longer in the interface of itt_int_arith).
4.Some documentation added to itt_int_arith.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-04 18:26:52 -0700 (Sun, 04 May 2003)
Revision: 4561
Log message:
Yegor, I've put omake on the mojave web site. I also updated README.WIN32
to point to the right location.
MetaPRL on native Win32 seems to work fine, and it also seems
a little faster than Cygwin. Cygwin still works of course. In
either case, you'll need to install the OCaml patches on
http://mojave.caltech.edu/downloads.html
| Changes | Path |
| +3 -3 | metaprl/README.WIN32 |
| +1 -0 | metaprl/clib/readline.c |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-05 16:41:04 -0700 (Mon, 05 May 2003)
Revision: 4562
Log message:
- Uncommenting the rule that was giving Jason trouble (so that we can figure
out what is going on).
- "make clean" in doc/latex/theories needs to erase *.toc as well.
| Changes | Path |
| +1 -1 | metaprl/doc/latex/theories/Makefile |
| +0 -3 | metaprl/theories/itt/itt_collection.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-05 19:47:22 -0700 (Mon, 05 May 2003)
Revision: 4563
Log message:
| 1. Fixed the build problem with prlc quitting too early on win32,
| requiring repeated runs of omake.
|
| This was actually problem with Unix.execvp, which doesn't
| work as advertised. The problem is fixed in prlcomp.ml
| by using Unix.create_process instead. I actually ran into
| this several years ago, and the appropriate code was still
| around in a comment.
|
| 2. Add some missing .cvsignore entries, since win32 copies
| files instead of using symbolic links, which don't exist.
|
| 3. Moved infix.ml to infix.win32.ml as discussed with Aleksey.
| Changes | Path |
| +3 -7 | metaprl/OMakefile |
| Properties | metaprl/clib |
| +1 -1 | metaprl/editor/ml/OMakefile |
| Properties | metaprl/ensemble |
| +7 -2 | metaprl/filter/base/OMakefile |
| Deleted | metaprl/filter/base/infix.ml |
| Added | metaprl/filter/base/infix.win32.ml |
| Properties | metaprl/filter/base/infix.win32.ml |
| +11 -12 | metaprl/filter/filter/prlcomp.ml |
| Deleted | metaprl/mk/config.default |
| Added | metaprl/mk/config.win32 |
| Properties | metaprl/mk/config.win32 |
| Properties | metaprl/mllib |
| Properties | metaprl/refiner/reflib |
| Properties | metaprl/refiner/refsig |
| Properties | metaprl/refiner/rewrite |
| Properties | metaprl/refiner/term_gen |
| Properties | metaprl/support/shell |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-05 20:13:51 -0700 (Mon, 05 May 2003)
Revision: 4564
Log message:
1.The proof of itt_nat/positive_rule1 is fixed.
2.One more bug/unaccounted case fixed in arithT.
| Changes | Path |
| +2 -2 | metaprl/theories/itt/itt_int_arith.ml |
| +7 -0 | metaprl/theories/itt/itt_int_arith.mli |
| +1286 -1976 | metaprl/theories/itt/itt_nat.prla |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-05 20:24:48 -0700 (Mon, 05 May 2003)
Revision: 4565
Log message:
Added more complete version of omake realclean target. Note, this
migrates the rewrite error to a rule called singleton_elim.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-05 22:00:23 -0700 (Mon, 05 May 2003)
Revision: 4566
Log message:
- Rewriter redex compilation will now prohibit having a second-order variable
with the same name as other kinds of variables (including bound variables,
paramater and context ones).
- Updated display forms (prl and HTML):
a) Reverted back the times_df for prl (and listed a large number of alternatives)
b) Now subset, subseteq, sqsubset and sqsubseteq will be displayed correctly
(both prl and html modes) using four different symbols, as opposed to always
using the subseteq symbol, as before.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-05 23:49:51 -0700 (Mon, 05 May 2003)
Revision: 4567
Log message:
Fixed a few spelling mistakes in Yegor's documentation of Itt_int_arith
and added the Itt_int_arith theory to theories.pdf
| Changes | Path |
| +1 -0 | metaprl/doc/latex/theories/itt/print.ml |
| +2 -0 | metaprl/lib/words |
| +3 -1 | metaprl/support/display/comment.ml |
| +13 -14 | metaprl/theories/itt/itt_int_arith.ml |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-06 03:06:13 -0700 (Tue, 06 May 2003)
Revision: 4568
Log message:
Added left/right pointing triangle (white) to display normal subgroup.
Added quotient group to documentation.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-06 21:58:34 -0700 (Tue, 06 May 2003)
Revision: 4569
Log message:
Changed the definitions for injection, surjection, and bijection.
Added more rules for quotient group.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 00:42:49 -0700 (Wed, 07 May 2003)
Revision: 4570
Log message:
- Sequent args are now parsed int a term with a "sequent_arg" opname,
not an xlist term
- Restored the code for "dfrom_depth" debugging
- Fixed an unballanced display form for ifthenelse in Ocaml_expr_df
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 01:20:41 -0700 (Wed, 07 May 2003)
Revision: 4571
Log message:
- Added a new option for ls: ``ls "f"'' will list all formal contents of the theory.
- Reordered a few things in ITT slightly for better presentability.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-07 01:50:46 -0700 (Wed, 07 May 2003)
Revision: 4572
Log message:
minor.
| Changes | Path |
| +1 -3 | metaprl/theories/itt/itt_group.ml |
| +17024 -17338 | metaprl/theories/itt/itt_group.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 03:23:21 -0700 (Wed, 07 May 2003)
Revision: 4573
Log message:
- Added the fall-back for dT's elim. Now if several rules/tactics are added
to elim resource for the same term, dT will try them all until one succeeds
instead of only trying the first one. Note that dT 0 (intro) was doing this
for a very long time.
- Added nil sequents args to sequents in comments on support/tactics modules
(forgot this in my previous commit).
- Added another version of elimination rule for quotients, as Xin requested.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 17:52:36 -0700 (Wed, 07 May 2003)
Revision: 4574
Log message:
Added a few helper functions for the case we need to pass two terms to an intro
or elim rule and the first one can be typeinf'ed.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-08 00:45:05 -0700 (Thu, 08 May 2003)
Revision: 4575
Log message:
CS101 HW5 solutions; CS101 updates for MetaPRL 0.8.3
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-08 01:50:02 -0700 (Thu, 08 May 2003)
Revision: 4576
Log message:
thinAllT should work correctly with negative arguments.
| Changes | Path |
| +5 -2 | metaprl/theories/itt/itt_struct.ml |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-09 04:44:01 -0700 (Fri, 09 May 2003)
Revision: 4577
Log message:
- Added extentional group equality.
- Proved some (somewhat) complicated theorems about quotient groups.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-09 16:05:59 -0700 (Fri, 09 May 2003)
Revision: 4578
Log message:
Aleksey and Xin:
- Print more detailed debugging info for debug_auto
| Changes | Path |
| +6 -4 | metaprl/support/tactics/auto_tactic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-10 03:27:33 -0700 (Sat, 10 May 2003)
Revision: 4579
Log message:
Refreshed a few .prla files
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-10 03:47:25 -0700 (Sat, 10 May 2003)
Revision: 4580
Log message:
Defined {i..j-1} and {0..j-1} (in order to define finite sets).
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-05-10 14:13:43 -0700 (Sat, 10 May 2003)
Revision: 4581
Log message:
These are patches to enable MetaPRL to build under MacOS X.
The README.MACOSX file is pretty raw. It's enough for me to
remember how I built MetaPRL under OS X, but it is probably
insufficient for the average user. I will update and make it
more verbose the next chance I get.
| Changes | Path |
| Added | metaprl/README.MACOSX |
| Properties | metaprl/README.MACOSX |
| +3 -3 | metaprl/editor/ml/nuprl_jprover.ml |
| +5 -0 | metaprl/mk/rules |
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-05-10 17:07:07 -0700 (Sat, 10 May 2003)
Revision: 4582
Log message:
Updated the Mac OS X readme to make it a bit more usable.
| Changes | Path |
| +74 -27 | metaprl/README.MACOSX |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-10 19:08:47 -0700 (Sat, 10 May 2003)
Revision: 4583
Log message:
1. Itt_int_arith immediately follows after Itt_int_base and Itt_int_ext in
the documentation template.
2. More documentations added (and reorganized).
| Changes | Path |
| +1 -1 | metaprl/doc/latex/theories/itt/print.ml |
| +1 -1 | metaprl/theories/itt/itt_int_arith.ml |
| +13 -1 | metaprl/theories/itt/itt_int_base.ml |
| +67 -55 | metaprl/theories/itt/itt_int_ext.ml |
Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2003-05-10 21:44:55 -0700 (Sat, 10 May 2003)
Revision: 4584
Log message:
more updates for importing into the FDL (formal digital library)
| Changes | Path |
| +3 -2 | metaprl/editor/ml/nuprl_eval.ml |
| +3 -1 | metaprl/editor/ml/nuprl_run.mli |
| +1 -1 | metaprl/library/orb.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-11 08:09:42 -0700 (Sun, 11 May 2003)
Revision: 4585
Log message:
Added FIR<->term translation. 4000 lines of pure grundge code.
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-05-11 13:28:30 -0700 (Sun, 11 May 2003)
Revision: 4586
Log message:
Documenting 2 issues with MetaPRL on Mac OS X:
(1) Fonts: none seem to have all the necessary characters
(2) status_all: dies with an uncaught exception :-(
See the README.MACOSX file for more details.
| Changes | Path |
| +35 -18 | metaprl/README.MACOSX |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-12 03:59:47 -0700 (Mon, 12 May 2003)
Revision: 4587
Log message:
Cleaned up couple of theories.
| Changes | Path |
| +56 -60 | metaprl/theories/itt/itt_list.ml |
| +3788 -4286 | metaprl/theories/itt/itt_list.prla |
| +27 -31 | metaprl/theories/itt/itt_subtype.ml |
| +3514 -3673 | metaprl/theories/itt/itt_subtype.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-12 04:48:10 -0700 (Mon, 12 May 2003)
Revision: 4588
Log message:
Cleaned up a few more theories.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-12 20:47:53 -0700 (Mon, 12 May 2003)
Revision: 4589
Log message:
Stated migrating the toploop commands in Shell module from an ad-hoc mechanism
to the "topval" one.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-12 21:17:58 -0700 (Mon, 12 May 2003)
Revision: 4590
Log message:
Minor.
| Changes | Path |
| +3 -1 | metaprl/theories/itt/itt_struct.ml |
| +4930 -6295 | metaprl/theories/itt/itt_struct.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-13 00:56:50 -0700 (Tue, 13 May 2003)
Revision: 4591
Log message:
Some more progress on refactoring the shell commands.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-13 17:11:18 -0700 (Tue, 13 May 2003)
Revision: 4592
Log message:
Exporting the NuprlRUn instantiation (for Lori).
| Changes | Path |
| +8 -0 | metaprl/editor/ml/mp.mli |
Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2003-05-13 17:22:57 -0700 (Tue, 13 May 2003)
Revision: 4593
Log message:
more updates to the nuprl connection, and added run_nuprl to mp.mli
| Changes | Path |
| +1 -0 | metaprl/editor/ml/mp.mli |
| +156 -98 | metaprl/editor/ml/nuprl_eval.ml |
| +31 -20 | metaprl/library/basic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-13 18:18:49 -0700 (Tue, 13 May 2003)
Revision: 4594
Log message:
Exported the term_of_meta_term conversion for use in the FDL connection.
| Changes | Path |
| +1 -3 | metaprl/editor/ml/nuprl_eval.ml |
| +3 -2 | metaprl/filter/base/filter_cache.ml |
| +2 -0 | metaprl/filter/base/filter_cache.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-13 18:46:38 -0700 (Tue, 13 May 2003)
Revision: 4595
Log message:
Use "equiv" instead of "sim" for squiggle equality; other minor changes.
| Changes | Path |
| +1 -1 | metaprl/Makefile |
| +7 -12 | metaprl/refiner/reflib/ml_term.ml |
| +1 -1 | metaprl/theories/itt/itt_squiggle.ml |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-14 04:05:07 -0700 (Wed, 14 May 2003)
Revision: 4596
Log message:
minor.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-14 04:38:34 -0700 (Wed, 14 May 2003)
Revision: 4597
Log message:
Changed the genAssumT tactic to put things into hypothesis list.
More specifically, all assumtions up to the first membership one
(inclusively) will be turned into hypothesis, and only the ones after
the first membership one will go into conclusion using the universal
quanitifier and implication, as before.
The main reason for this change is that the manual "dT 0" would generate
wf subgoals that are trivially true, but could require non-trivial amount
of typing.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-14 16:23:36 -0700 (Wed, 14 May 2003)
Revision: 4598
Log message:
Adding things I presented in class today.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-14 16:26:45 -0700 (Wed, 14 May 2003)
Revision: 4599
Log message:
Forgot the prla.
| Changes | Path |
| Added | metaprl-branches/CS101_branch/theories/itt/cs101_list2.prla |
| Properties | metaprl-branches/CS101_branch/theories/itt/cs101_list2.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-15 00:45:27 -0700 (Thu, 15 May 2003)
Revision: 4600
Log message:
HW6 solutions.
Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2003-05-15 12:45:56 -0700 (Thu, 15 May 2003)
Revision: 4601
Log message:
updated and cleaned calls and doc for connecting to the fdl and using jprover from nuprl. Alexey, I got rid of your NuprlRun hack as I no longer need it. thnks.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-16 03:41:35 -0700 (Fri, 16 May 2003)
Revision: 4604
Log message:
Removed couple redundant rules (they seemed to be left over from the times
we had separate member and equal operators in ITT).
| Changes | Path |
| +2 -6 | metaprl/theories/itt/itt_logic.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-17 17:20:36 -0700 (Sat, 17 May 2003)
Revision: 4605
Log message:
Temporary modification aimed to catch source of problems with weak array,
wich is replaced with two weak arrays (DoubledWeak plays a role of Weak).
Right now I can not reproduce the problem with weak array so everybody who
still have it please respond how behavior changed with this update.
| Changes | Path |
| +59 -0 | metaprl/mllib/weak_memo.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-17 20:49:46 -0700 (Sat, 17 May 2003)
Revision: 4606
Log message:
A few minor efficiency and clean-up fixes.
| Changes | Path |
| +5 -4 | metaprl/mllib/hash_with_gc.ml |
| +2 -5 | metaprl/mllib/weak_memo.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-17 21:44:17 -0700 (Sat, 17 May 2003)
Revision: 4607
Log message:
Further code simplifications
| Changes | Path |
| +18 -35 | metaprl/mllib/weak_memo.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-18 01:42:25 -0700 (Sun, 18 May 2003)
Revision: 4608
Log message:
Sanity check a module before "blindly" cd'ing into it.
| Changes | Path |
| +1 -0 | metaprl/support/shell/mptop.ml |
| +1 -0 | metaprl/support/shell/mptop.mli |
| +14 -3 | metaprl/support/shell/shell.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-18 04:26:44 -0700 (Sun, 18 May 2003)
Revision: 4609
Log message:
Turned remaining top-loop commands in Shell module into proper topval's.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-18 10:40:01 -0700 (Sun, 18 May 2003)
Revision: 4610
Log message:
print-theory should still work correctly when a theory is non-interactive
(e.g. does not extend Shell).
| Changes | Path |
| +6 -5 | metaprl/support/shell/shell.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 03:04:06 -0700 (Mon, 19 May 2003)
Revision: 4611
Log message:
- Amended the dform for the "define" directive to include the "displayed as"
part
- Simplified a bunch of proofs in itt_bool.
| Changes | Path |
| +7 -4 | metaprl/support/display/summary.ml |
| +6876 -8323 | metaprl/theories/itt/itt_bool.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 12:49:02 -0700 (Mon, 19 May 2003)
Revision: 4612
Log message:
Fixing the bytecode compile that I broke.
| Changes | Path |
| +0 -1 | metaprl/editor/ml/mp.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-05-19 13:35:31 -0700 (Mon, 19 May 2003)
Revision: 4613
Log message:
*** empty log message ***
| Changes | Path |
| +9 -0 | metaprl/README.WIN32 |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 17:56:12 -0700 (Mon, 19 May 2003)
Revision: 4614
Log message:
Added goals of the form ... >- t1 = t2 in T --> ... >- T type to trivialT
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 18:31:52 -0700 (Mon, 19 May 2003)
Revision: 4615
Log message:
Removed a redundant rule.
| Changes | Path |
| +14 -16 | metaprl/theories/itt/itt_bool.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 21:57:03 -0700 (Mon, 19 May 2003)
Revision: 4616
Log message:
Removed the segment of the documentation that used to cover the
sequent squash operator (e.g. the meta-squash) that was removed
couple of weeks ago.
| Changes | Path |
| +5 -27 | metaprl/theories/itt/itt_squash.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 22:18:25 -0700 (Mon, 19 May 2003)
Revision: 4617
Log message:
- Refiner was not passing the assumptions to rewriter when checking
a conditional rewrite at compile-time. As a result, the check was incomplete.
- Added "-sb -sl 1000" to xterm scripts.
| Changes | Path |
| +1 -1 | metaprl/editor/ml/mpxterm |
| +1 -1 | metaprl/editor/ml/mpxterm-large |
| +5 -9 | metaprl/refiner/refiner/refine.ml |
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-19 23:57:07 -0700 (Mon, 19 May 2003)
Revision: 4618
Log message:
Fixed a well-formedness rule.
| Changes | Path |
| +0 -1 | metaprl/theories/itt/itt_list2.ml |
| +4595 -5627 | metaprl/theories/itt/itt_list2.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-21 05:04:28 -0700 (Wed, 21 May 2003)
Revision: 4619
Log message:
Now the MetaPRL top-loop has a real type system!
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-21 05:15:49 -0700 (Wed, 21 May 2003)
Revision: 4620
Log message:
The componentwise equality rules for the int operators (e.g. rules like
a = a' in int --> b = b' in int --> a + b = a' + b' in int) should only
be added to intro with AutoMustComplete!
TODO: we probably need to add a form of AutoMustComplete that would check
whether the conclusion is a membership and would only enforce MustComplete
when it's not a membership.
| Changes | Path |
| +5 -5 | metaprl/theories/itt/itt_int_base.ml |
| +5 -5 | metaprl/theories/itt/itt_int_ext.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-21 22:54:06 -0700 (Wed, 21 May 2003)
Revision: 4621
Log message:
Added support for "conditional MustComplete" to intro resource. I used it
to make a few rules as MustComplete when the goal is an equality term,
but freely usable in autoT when the goal is a membership term.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-22 21:31:01 -0700 (Thu, 22 May 2003)
Revision: 4622
Log message:
Added input form 'T Type (for "type"{'T} )
| Changes | Path |
| +4 -2 | metaprl/doc/htmlman/user-guide/mp-terms.html |
| +6 -0 | metaprl/filter/filter/term_grammar.ml |
| +12 -12 | metaprl/theories/itt/itt_equal.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-22 22:30:17 -0700 (Thu, 22 May 2003)
Revision: 4623
Log message:
- Adding CS101 HW7 solutions and HW8 theory.
- Somewhat saner intro annotations in itt_esquash.
- Better parentization in itt_equal dforms.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-23 02:04:41 -0700 (Fri, 23 May 2003)
Revision: 4624
Log message:
- Made nthHypT be more efficient at choosing a tactic to apply.
- Updated the intro rules for esquash to be more aggressive in
esquashAutoT and more conservative in simple autoT.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-23 02:14:42 -0700 (Fri, 23 May 2003)
Revision: 4625
Log message:
Updated for the new esquash tactics.
| Changes | Path |
| +150 -324 | metaprl-branches/CS101_branch/theories/itt/cs101_hw8.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-28 01:07:16 -0700 (Wed, 28 May 2003)
Revision: 4626
Log message:
*** !!!!!!!!!!!!! WARNING !!!!!!!!!!!!!!!! ***
*** This commit breaks .prlb compatibility ***
I've cleaned up (and removed) some code on the way
towards implementing a full support for extracting
computational content from proofs.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-28 03:25:05 -0700 (Wed, 28 May 2003)
Revision: 4627
Log message:
- Moved the "top" type declaration from Itt_void (where it resided
for hackish reasons) to Itt_isect, where it belongs.
- The rule /itt_isect/intersectionSubtype was not valid. Made it weaker
and derived it.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-29 12:01:34 -0700 (Thu, 29 May 2003)
Revision: 4628
Log message:
Fixed a couple of typoes.
| Changes | Path |
| +3 -7 | metaprl/theories/itt/itt_int_arith.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-29 21:56:53 -0700 (Thu, 29 May 2003)
Revision: 4631
Log message:
CS101 HW8 solutions.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-29 23:11:50 -0700 (Thu, 29 May 2003)
Revision: 4633
Log message:
Documented fnExtensionalityT and fnExtenT
| Changes | Path |
| +24 -9 | metaprl/doc/itt_quickref.txt |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-30 00:30:50 -0700 (Fri, 30 May 2003)
Revision: 4634
Log message:
Made the typing rules for "and" stronger. For A/\B to be a type, B has to be
a type only when A is true.