Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-05-01 09:00:19 -0700 (Mon, 01 May 2000)
Revision: 2947
Log message:

      Some improvements for NuPRL interface
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2000-05-03 06:46:23 -0700 (Wed, 03 May 2000)
Revision: 2948
Log message:

      improved jprover interface to account for variables
      

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-05-03 08:00:46 -0700 (Wed, 03 May 2000)
Revision: 2949
Log message:

      Some optimizations for proof reconstruciton
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2000-05-03 08:02:22 -0700 (Wed, 03 May 2000)
Revision: 2950
Log message:

      some naming updates from nuprllight to metaprl
      

Changes by: ( at unknown.email)
Date: 2000-05-03 08:02:22 -0700 (Wed, 03 May 2000)
Revision: 2951
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-03 22:47:44 -0700 (Wed, 03 May 2000)
Revision: 2952
Log message:

      I started working on removing old (and buggy!) unification and speeding up
      the new "MM" unification.
      
      Note that all these changes are on the unify_mm branch, not the trunk. It means
      that "cvs update" would not give you this changes unless you run it with "-r unify_mm"
      option. This should allow people to continue working on the rest of the MetaPRL without
      being affected by these changes.
      
      This code would not compile until I finish doing tons of trivial changes in ITT typeinf
      updates. (I just wish typeinf would already be implemented using resource annotations!)
      
      Also, the TPTP code expects unification to raise RefineError exceptions,
      but unification currently raises other kinds of exceptions. Hopefully, V.N.
      will be able to fix this.
      
      V.N. - can you double-check my changes? Thanks!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-04 00:16:07 -0700 (Thu, 04 May 2000)
Revision: 2953
Log message:

      Converted couple of files to new unification.
      

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-05-04 15:35:56 -0700 (Thu, 04 May 2000)
Revision: 2954
Log message:

      new
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-05 16:57:47 -0700 (Fri, 05 May 2000)
Revision: 2955
Log message:

      Changed the typeinf tactic to use MM unification. Now this branch will compile.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-05 19:50:23 -0700 (Fri, 05 May 2000)
Revision: 2956
Log message:

      Added some comments on usage of RefineError exceptions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-05 20:31:39 -0700 (Fri, 05 May 2000)
Revision: 2957
Log message:

      I replaced Cycle and Clash exceptions in unify_ds with
      RefineError's and tried to run tests/tptp-gen.ml
      
      For some reason it never terminates.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-05-07 07:22:07 -0700 (Sun, 07 May 2000)
Revision: 2958
Log message:

      The RefineError exceptins are incorporated correctly in Term_unif_ds module
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-07 08:41:31 -0700 (Sun, 07 May 2000)
Revision: 2959
Log message:

      Use fail_core when appropriate.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2000-05-09 13:55:13 -0700 (Tue, 09 May 2000)
Revision: 2960
Log message:

      term functions for jprover/nuprl interface
      

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-05-10 08:12:11 -0700 (Wed, 10 May 2000)
Revision: 2961
Log message:

      Optimized beta-proof computation for proof reconstruction
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-11 22:56:42 -0700 (Thu, 11 May 2000)
Revision: 2962
Log message:

      Added:
      
      6.3) (Formulated by krupski and confirmed by nogin - 2000.05.12)
      After the membership rule is postulated, the corresponding ext rule can often
      be proven using Itt_struct.introduction rule. There is no need to postulate
      the ext rule and it should be actually proven only when it's useful.
      
      Example: After <<'H >- univ[i:l] in int>> is postulated, there is no need
      to postulate <<'H >- univ[i:l]>> with <<int>> extract since it can always
      be proven in the unlikely event that it is actually needed.
      
      P.S. Unfortunatelly, there seems to be no mechanism to do similar trick
      for rules with assumptions. May be it would be a good idea to create one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-13 15:39:41 -0700 (Sat, 13 May 2000)
Revision: 2963
Log message:

      I wrote a small guide to MetaPRL indentation and spacing conventions.
      Jason, Eli, care to add/change something?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-13 16:10:54 -0700 (Sat, 13 May 2000)
Revision: 2964
Log message:

      Removed some unnecessary spaces. Still need to do proper indentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-13 20:24:33 -0700 (Sat, 13 May 2000)
Revision: 2965
Log message:

      Updated the guidelines after talking to Eli and looking at more
      examples of badly indented code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-13 20:38:41 -0700 (Sat, 13 May 2000)
Revision: 2966
Log message:

      get_core is supposed to return a real core and it can not return a Hashed _
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-13 21:01:07 -0700 (Sat, 13 May 2000)
Revision: 2967
Log message:

      - Updated exception handling
      - Corrected the usage of get_core
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-14 12:38:40 -0700 (Sun, 14 May 2000)
Revision: 2968
Log message:

      Better error message.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-14 13:43:26 -0700 (Sun, 14 May 2000)
Revision: 2969
Log message:

      Fixed a bug in red_black_set - it forgot to sort the list and get rid
      of duplicates before converting it to a set!
      
      Added a little more debugging in debug_string_sets
      
      Rolled back the change that I accidentally commited to string_set - it
      is now back to using red_black_set (instead of debug_string_sets).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-14 14:28:09 -0700 (Sun, 14 May 2000)
Revision: 2970
Log message:

      Use String_util.vnewname to rename variables.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-14 17:13:34 -0700 (Sun, 14 May 2000)
Revision: 2971
Log message:

      Use StringSet for unification constants instead of string list.
      
      Converted Term_ds to use String_set.StringSet instead of
      its private copy of StringSet.
      
      2% speedup on TPTP's GEN.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-14 18:10:18 -0700 (Sun, 14 May 2000)
Revision: 2972
Log message:

      Use Opname.eq to compare opnames.
      
      2.5% speedup in TPTP's GEN with unify_mm.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-14 18:33:39 -0700 (Sun, 14 May 2000)
Revision: 2973
Log message:

      terms2temp_multieq:
      
      Replaced List.map (fun ...) with custom functions to avoid
      unnecassry closure creation.
      
      Made sure that Clash is raised as early as possible.
      
      8% speedup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-15 00:56:25 -0700 (Mon, 15 May 2000)
Revision: 2974
Log message:

      Use Red_black_table instead of Splay_table in Tptp_cache.
      
      3% speedup when new unification is used; 5% with the old one
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-15 01:21:05 -0700 (Mon, 15 May 2000)
Revision: 2975
Log message:

      terms2temp_multieq again: Do not create temp_meq before it's really needed.
      
      Use incr for incrementing instead of x:=(!x)+1
      
      1.5% speedup on TPTP's GEN.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-15 02:05:01 -0700 (Mon, 15 May 2000)
Revision: 2976
Log message:

      Create opL once, not every time unify_eqnl_eqnl is ran
      
      5% speedup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-15 23:45:55 -0700 (Mon, 15 May 2000)
Revision: 2977
Log message:

      Wrote lots of debugging code while trying (so far unsuccesfully) to find out
      why splay_table and red_black_table produce mismatching results.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-16 14:40:10 -0700 (Tue, 16 May 2000)
Revision: 2978
Log message:

      Wrote even more debugging code.
      
      Fixed a bug in Splay_table.add. Now Splay_table and Red_black_table
      behave identically in TPTP's GEN example.
      
      Replaced Failure exceptions in Splay_table with Invalid_argument ones since
      they were only used to signal potential bugs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-16 16:43:57 -0700 (Tue, 16 May 2000)
Revision: 2979
Log message:

      This junk shouldn't be here.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-17 00:12:16 -0700 (Wed, 17 May 2000)
Revision: 2980
Log message:

      Small step towards making bytecode profiling more automatic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-17 01:19:35 -0700 (Wed, 17 May 2000)
Revision: 2981
Log message:

      Specialized the terms2temp_multieq code for the case of no subterms
      or subterms with no bound variables.
      
      5% speedup (TPTP's GEN)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-17 16:01:20 -0700 (Wed, 17 May 2000)
Revision: 2982
Log message:

      4.7) (nogin)
      In Ocaml, string is a mutable data structure. In MetaPRL, we use strings everywhere (variable
      names, opnames, etc) as if they were immutable. We need to
      a) Make sure that nobody can cheat the system by starting to mute strings.
      b) Let the compiler and GC know that we are not going to mute strings (which should allow
      them to be more efficient).
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-05-18 12:32:56 -0700 (Thu, 18 May 2000)
Revision: 2984
Log message:

      changes in the order of eqnlists -- m.b. more efficient unification
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-24 22:14:42 -0700 (Wed, 24 May 2000)
Revision: 2985
Log message:

      Merged the unify_mm branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-25 15:29:55 -0700 (Thu, 25 May 2000)
Revision: 2986
Log message:

      Splitted create_tptp into create_ax_statement and tptp_load.
      
      Now editor/ml/ does not refer to Tptp_load which we had to comment and uncomment
      all the time.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-25 15:36:38 -0700 (Thu, 25 May 2000)
Revision: 2987
Log message:

      These were unused for a long time.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-25 15:41:19 -0700 (Thu, 25 May 2000)
Revision: 2988
Log message:

      Print first the rulebox count, then the rule count to be consistent
      with some other part of the system (wish I knew which one) that also
      prints those.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 04:47:26 -0700 (Fri, 26 May 2000)
Revision: 2989
Log message:

      Reverting the last change - the problem is somewhere else.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 05:06:47 -0700 (Fri, 26 May 2000)
Revision: 2990
Log message:

      Finally managed to make sure that rulebox count always goes before the node count.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 05:15:57 -0700 (Fri, 26 May 2000)
Revision: 2991
Log message:

      Inlined cterms2system
      
      1% speedup on TPTP's GEN
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 06:16:40 -0700 (Fri, 26 May 2000)
Revision: 2992
Log message:

      Replaced the free_vars function from TermSubst interface with free_vars_list
      and free_vars_set that return string list and StringSet.t respectively.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 12:57:46 -0700 (Fri, 26 May 2000)
Revision: 2993
Log message:

       - Fixed a nasty bug in Term_ds.subst - it didn't notice when the same variable
      was mentioned several times in the substitution with different terms substituted
      for it. This made it possible to break Term_ds invariants leading to all kinds of
      strange behaviour.
      
       - Changed the argument order for "subst" to be more natural
      
       - Added a subst1 function to substitute for a single variable without having
      to put the substitution into a singleton list.
      
       - Added the resource annotations and updated the rest of the resource code
      in CZF so that it now compiles (but I didn't try to expand anything).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-29 20:55:15 -0700 (Mon, 29 May 2000)
Revision: 2994
Log message:

      I wrote several sections of MetaPRL Developer Guide.
      
      Please take a look at it at
      http://ensemble01.cs.cornell.edu:12000/cvsweb/~checkout~/meta-prl/doc/htmlman/default.html
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-29 22:28:42 -0700 (Mon, 29 May 2000)
Revision: 2995
Log message:

      Moved Jprover output parsing into the JLogic interface. Still need to write the
      output parsing for ITT_JLogic.
      
      Eliminated some excessive whitespace from jall.ml
      
      Eliminated some unnecessary exception handling code from jall.ml
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-30 03:57:44 -0700 (Tue, 30 May 2000)
Revision: 2996
Log message:

      Do something reasonable for term printing in Ocaml toploop.
      
      Modern versions of Ocaml require installed printers to use the Format library.
      The only quick way to do it was to use print a term to a string and use
      Format.print_string.
      
      However, it may be a good idea to abandon Rformat and
      to use Format instead or to write an alternative implementation of the Rformat
      interface using Format.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-30 06:58:39 -0700 (Tue, 30 May 2000)
Revision: 2997
Log message:

      The Jprover interface is almost finished. It's partially working, I just
      need to write some hack for v0_jprover non-empty types hack.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2000-05-30 11:59:12 -0700 (Tue, 30 May 2000)
Revision: 2998
Log message:

      removed global vars used for debugging
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-30 14:33:19 -0700 (Tue, 30 May 2000)
Revision: 2999
Log message:

      The PS and PDF versionf of the documenattion can now be downloaded
      from ftp://ftp.cs.cornell.edu/pub/nuprl/MetaPRL/doc/
      
      I created a cron job on Mojave that would update them nightly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-30 19:47:17 -0700 (Tue, 30 May 2000)
Revision: 3000
Log message:

      Now sequents without hypothesis and axioms (rules without assumptions and paramaters)
      are displayed more or less correctly.
      
      Additionally, I realized that currently resource annotations on axioms are silently ignored.
      I documented it in BUGS. (I am not 100% sure - I haven't actually tested it).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-30 19:53:36 -0700 (Tue, 30 May 2000)
Revision: 3001
Log message:

      Fixed a nasty bug in Jprover (after chaising it with Stephan for couple of hours)
      
      Fixed a bug in the MetaPRL-Jprover interface.
      
      Imported some Jprover tests and examples.