/[mojave]/metaprl/library/db.ml
ViewVC logotype

Log of /metaprl/library/db.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 2922 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 16 19:52:02 2000 UTC (21 years, 3 months ago) by lolorigo
File length: 30959 byte(s)
Diff to previous 2822
added/improved functionality for metaprl/jprover/nuprl5 io


Revision 2822 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 22 01:07:59 1999 UTC (21 years, 7 months ago) by nogin
File length: 29195 byte(s)
Diff to previous 2669
Added new function to mp_debug
let show_loading s = if !debug_load then Printf.eprintf s eflush

and replaced all usages of debug_load with show_loading


Revision 2669 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 23 21:55:17 1999 UTC (22 years ago) by jyh
File length: 29223 byte(s)
Diff to previous 2523
This is a major modification to how parameters are handled.
1. All level parmeters are now meta.  That is, univ[@i:l] is
   exactly the same as univ[i:l].  The rewriter handles
   lavel expressions, so matching with levels like
   univ[3 | i':l | j:l] should work correctly.

   The syntax still requires the @ for meta-parameter of
   other types.  For instance, token["hello world":t] is
   a normal token, and token[@"hello world":t] is a
   token with a meta-parameter.

2. There are no more parameter expressions.  For instance,
   the term natural_number[@i + @j] is not valid anymore.
   To replace them, the module theories/base/base_meta.ml
   defines ML rewrites that implement the same functionality.
   For example,
      meta_sum{number[12]; number[5]} --> number[17]

3. There is no term natural_number[@i:n] any more.  This was
   always a bad name, since it has always been possible for the
   parameter to be negative.

4. The Itt_equal.cumulativity rule is no longer defined as a
   side-condition.  It now uses Base_meta.meta_lt to define
   inclusion on level expression.  Cumulativity expansion
   should be performed automatically by the dT tactic.
   So:
      sequent ['ext] { ... >- univ[@i:l] = univ[@i:l] in univ[@j:l] }
      BY dT 0
   should always either succeed or fail, without producing
   subgoals.

I haven't fully tested the side-conditions.  As usual, let me know
if you see anything strange.  Next, I'm looking at the
rewriter free variable soundness problem.


Revision 2523 - (view) (download) (annotate) - [select for diffs]
Modified Thu Dec 17 15:57:52 1998 UTC (22 years, 6 months ago) by lolorigo
File length: 28943 byte(s)
Diff to previous 2522
added improvements to mathbus speed, and functionality for edits in nuprl


Revision 2522 - (view) (download) (annotate) - [select for diffs]
Modified Fri Dec 11 19:14:25 1998 UTC (22 years, 6 months ago) by nogin
File length: 27426 byte(s)
Diff to previous 2494
Fixed some "this expression should have type unit" Ocaml-2.01 warnings


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 27367 byte(s)
Diff to previous 2456
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2456 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 22:31:37 1998 UTC (22 years, 9 months ago) by jyh
File length: 27371 byte(s)
Diff to previous 2443
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.


Revision 2443 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 24 13:43:48 1998 UTC (22 years, 9 months ago) by jyh
File length: 26271 byte(s)
Diff to previous 2336
Slightly better Ensemble scheduling.
Native-code compiler has trouble marshaling functions--
its probably a problem with the marshaler.

Added Nl_num, a ML-only implementation of bignums.
This is slower than the C version used by OCaml, but
we can marshal the Nl_nums.  Most of the files changed
are just replacements of Num.* with Nl_num.*.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 10 months ago) by jyh
File length: 26222 byte(s)
Diff to previous 2283
Added NL toploop so that we can compile NL native code.


Revision 2283 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 18:38:08 1998 UTC (22 years, 11 months ago) by jyh
File length: 26219 byte(s)
Diff to previous 2251
Refiner modules now raise RefineError exceptions directly.
Modules in this revision have two versions: one that raises
verbose exceptions, and another that uses a generic exception.


Revision 2251 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 16 16:26:27 1998 UTC (23 years ago) by jyh
File length: 26206 byte(s)
Diff to previous 2209
Added itt_test.


Revision 2209 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 13:57:13 1998 UTC (23 years ago) by jyh
File length: 25970 byte(s)
Diff to previous 2190
Proving twice one is two.


Revision 2190 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 13:48:44 1998 UTC (23 years ago) by jyh
File length: 26079 byte(s)
Diff to previous 2184
Updated the editor to use new Refiner structure.
ITT needs dform names.


Revision 2184 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 27 15:15:13 1998 UTC (23 years ago) by jyh
File length: 25987 byte(s)
Diff to previous 2167
Functorized the refiner over the Term module.


Revision 2167 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 5 20:05:57 1998 UTC (23 years, 1 month ago) by eaton
File length: 25931 byte(s)
Diff to previous 2162
.


Revision 2162 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 30 14:55:29 1998 UTC (23 years, 1 month ago) by lolorigo
File length: 25826 byte(s)
Diff to previous 2155
.


Revision 2155 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 27 19:18:21 1998 UTC (23 years, 1 month ago) by eaton
File length: 25764 byte(s)
Diff to previous 2154
.


Revision 2154 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 27 13:25:47 1998 UTC (23 years, 1 month ago) by lolorigo
File length: 24652 byte(s)
Diff to previous 2149
ascii


Revision 2149 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 22 18:25:10 1998 UTC (23 years, 1 month ago) by eaton
File length: 23705 byte(s)
Diff to previous 2144
.


Revision 2144 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 21:57:06 1998 UTC (23 years, 2 months ago) by eaton
File length: 22674 byte(s)
Diff to previous 2142
.


Revision 2142 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 16:47:09 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 14894 byte(s)
Diff to previous 2141
.


Revision 2141 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 15:31:04 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 14465 byte(s)
Diff to previous 2140
.


Revision 2140 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 15:13:53 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 14481 byte(s)
Diff to previous 2139
.


Revision 2139 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 15:12:52 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 14486 byte(s)
Diff to previous 2135
.


Revision 2135 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 16 21:21:21 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 15213 byte(s)
Diff to previous 2131
.


Revision 2131 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 16 03:33:19 1998 UTC (23 years, 2 months ago) by eaton
File length: 13133 byte(s)
Diff to previous 2130
.


Revision 2130 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 15 22:59:18 1998 UTC (23 years, 2 months ago) by eaton
File length: 13107 byte(s)
Diff to previous 2128
.


Revision 2128 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 15 19:53:47 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 5441 byte(s)
Diff to previous 2127
ascii


Revision 2127 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 15 19:51:35 1998 UTC (23 years, 2 months ago) by lolorigo
File length: 5447 byte(s)
Diff to previous 2072
ascii


Revision 2072 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 30 21:25:23 1997 UTC (23 years, 8 months ago) by lolorigo
File length: 1347 byte(s)
Diff to previous 2069
.


Revision 2069 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 17 13:12:06 1997 UTC (23 years, 9 months ago) by lolorigo
File length: 1374 byte(s)
Diff to previous 2063
.


Revision 2063 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 9 16:09:45 1997 UTC (23 years, 9 months ago) by eaton
File length: 1253 byte(s)
Diff to previous 2060
.


Revision 2060 - (view) (download) (annotate) - [select for diffs]
Added Wed Sep 3 15:15:46 1997 UTC (23 years, 9 months ago) by lolorigo
File length: 1234 byte(s)
.


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