Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-03 21:02:01 -0800 (Fri, 03 Jan 2003)
Revision: 3976
Log message:

      - I added a list of authors to User Guid, Developr Guis and System Description.
      I came up with the lists based on quick browsing of CVS logs, so I might be mistaken,
      please let me know or feel free to fix yourself, if so.
      
      The current lists are:
      * Jason Hickey and Aleksey Nogin. MetaPRL System Description
      * Jason Hickey, Aleksey Nogin and Alexei Kopylov. MetaPRL User Guide
      * Aleksey Nogin and Vladimir Krupski. MetaPRL Developer Guide
      
      - Reorganized the "Hnn" headings - now only the main title page has H1, and the
      sections/subsections/subsubsections have H2-H4. Among other things this makes
      it look better in htmldoc'ed PDFs and PSs.
      
      - In the "simplified syntax" moved the "low priority terms closer to the end,
      it looked weird when the listings started with it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-03 23:59:38 -0800 (Fri, 03 Jan 2003)
Revision: 3977
Log message:

      Updated all the HTML files to be (hopefully) in correct
      "HTML 4.01 Transitional" compliant syntax.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-04 00:19:43 -0800 (Sat, 04 Jan 2003)
Revision: 3978
Log message:

      Some more HTML fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-08 13:50:26 -0800 (Wed, 08 Jan 2003)
Revision: 3984
Log message:

      Changed the order of arguments in StringSet.add to be able to use
      more efficient (tail-recursive) List.fold_left instead of fold_right
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-01-08 22:07:06 -0800 (Wed, 08 Jan 2003)
Revision: 3985
Log message:

      Added the definition for cyclic groups where the generator is not specified.
      Changed cycgroupAbelT to cycgAbelT.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-01-09 18:27:48 -0800 (Thu, 09 Jan 2003)
Revision: 3986
Log message:

      Added math form def. for cycg.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-09 19:07:26 -0800 (Thu, 09 Jan 2003)
Revision: 3987
Log message:

      - Added a version of a dest_bterm function (dest_bterm_and_rename)
      that will alpha-rename the returned bterm to avoid clashes with
      the specified set of variables.
      - Changed the "match_redex" part of the rewriter to always use
      dest_bterm_and_rename instead of dest_bterm. It now collects all the
      bound variables that are explicitly mentioned (e.g. all of them except
      those matched by a context) and makes sure dest_bterm_and_rename avoid
      any possibility of clashes. It will also avoid clashes between
      the hypotheses variable and the hypotheses contents (this last part
      is somewhat contrary to the logical binding structure, but can not hurt).
      
      Example, when matching ...; n: {n:Z| n>=0}; ... against a redex pattern
      H; u: {v:T| P[v]}; J[u] >- C[u], the rewriter now will rename the "inner"
      n into n_1.
      
      This does not fix as many variable clash issues as I hoped for - it seems
      many of those are coming from the build_contractum part of the rewriter.
      I plan to address those later (I will probably post a proposed solution to
      the newsgroup later today).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-10 18:22:30 -0800 (Fri, 10 Jan 2003)
Revision: 3988
Log message:

      Killed onVarT - for two reasons:
      - we never use it
      - variable names are supposed to be allowed to fluctuate. Intentionally
      tying a tactic to a variable name is IMO silly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-10 21:09:48 -0800 (Fri, 10 Jan 2003)
Revision: 3989
Log message:

      Got rid of some of the namer code that seems to no longer be relevant.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-01-11 08:21:35 -0800 (Sat, 11 Jan 2003)
Revision: 3990
Log message:

      Proved that cycg and cycgroup are equivalent.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-01-13 22:54:34 -0800 (Mon, 13 Jan 2003)
Revision: 3995
Log message:

      Changed Phobos tactic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-19 19:41:55 -0800 (Sun, 19 Jan 2003)
Revision: 4000
Log message:

      Added a link to the CUCS CVS HOWTO
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-21 02:41:52 -0800 (Tue, 21 Jan 2003)
Revision: 4001
Log message:

      For ThinOption in elim resource, determine the hyp number for thinning
      upfront (when processing the annotation) instead of trying to guess it at
      run-time based on the hyp. variable names.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-21 22:56:04 -0800 (Tue, 21 Jan 2003)
Revision: 4002
Log message:

      Added something semi-reasonable for mathbbB in prl (Unicode) mode.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-01-22 16:39:13 -0800 (Wed, 22 Jan 2003)
Revision: 4004
Log message:

      Add some documentation on record type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-22 22:08:38 -0800 (Wed, 22 Jan 2003)
Revision: 4008
Log message:

      Something that actually compiles (I hope).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-22 23:45:27 -0800 (Wed, 22 Jan 2003)
Revision: 4009
Log message:

      Removed some outdated code:
      - support for parsing <:con< >> quotations (for ml_* things) that
      I don't even remember being ever used.
      - filter_html - not sure if it was ever used, but it is not currently
      being compiled and looks very ourdated, removing for now.
      
      Jason, please confirm that removing these is reasonable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-23 00:24:18 -0800 (Thu, 23 Jan 2003)
Revision: 4010
Log message:

      Unused ml_ code (ml_rule and conditional ml_rw) seems to be quite outdated.
      Added an Invalid_argument there warning about the need for a clean-up
      in case somebody decides to use the code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-23 12:04:34 -0800 (Thu, 23 Jan 2003)
Revision: 4011
Log message:

      Doccumentation fixes:
      - section/subsection headings should be inside @doc
      (or its equivalent @begin[doc]/@end[doc])
      - theory should end in @docoff mode (otherwise some junk is printed at the end)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-23 18:09:24 -0800 (Thu, 23 Jan 2003)
Revision: 4013
Log message:

      Got rid of separate contractum functions in rewriter (contractum functionality
      is now only available as a part of the combined rewrite functionality).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-01-23 20:05:03 -0800 (Thu, 23 Jan 2003)
Revision: 4014
Log message:

      This is a first version of a syntax that parallels the MCC FIR.
      Haven't tried to compile yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-01-24 09:21:38 -0800 (Fri, 24 Jan 2003)
Revision: 4015
Log message:

      Try again without the papers directory.
      
      Added the IR for the M language.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-01-24 09:23:29 -0800 (Fri, 24 Jan 2003)
Revision: 4016
Log message:

      Added display form for m{}.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-01-24 09:39:37 -0800 (Fri, 24 Jan 2003)
Revision: 4017
Log message:

      Minor documentation change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-24 19:21:01 -0800 (Fri, 24 Jan 2003)
Revision: 4020
Log message:

      Created names for ([||], [||]) and ([||], [||], []) that are used all the time
      for rewrites that do not require any arguments. This looks nices, is more
      maintainable and more efficient (no need for allocating tuples every time).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-24 20:47:08 -0800 (Fri, 24 Jan 2003)
Revision: 4021
Log message:

      Forgot to include this in my last commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-25 00:00:19 -0800 (Sat, 25 Jan 2003)
Revision: 4022
Log message:

      Split nth_nyp into two functions: nth_hyp and nth_binding.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-25 02:35:15 -0800 (Sat, 25 Jan 2003)
Revision: 4023
Log message:

      - Now the msequents in tactic_args on RuleBox level are normalized
      (e.g. cons-hashed).
      - The proofs are normalized (e.g. redundant identity steps are eliminated)
      before doing a node count.
      - Removed some extremely old code that was there for handling old (1999!)
      binary proof format. Obviously, it is no longer needed.
      
      Note - there are to reasons for the msequent normalization:
      - I am planning to add the code that during term normalization
      would drop variables from hypotheses bindings, if the variable is unused.
      This would means that sequents can become slightly different (still alpha-equal,
      of course) as a result of being normalized. Since disk IO uses normalization
      as well, this could potentially cause users tactics to behave differently when
      saved and reloaded. By making sure ruleboxes are always normalized, we
      can make sure user tactics are always applied to normalized sequents (both
      before the disk IO and after), so they should still behave the same.
      - This gave about 8-9% speed-up on "status_all()" - primarily (I guess) by
      reducing the memory footprint.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-26 22:11:31 -0800 (Sun, 26 Jan 2003)
Revision: 4024
Log message:

      - Fixed an evil bug in Term_subst_std.subst1.
      - Finished the dest_bterm_and_rename implementation and made Rewriter
      use it more extensively.
      - Minor enhancements to utility scripts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-28 16:26:29 -0800 (Tue, 28 Jan 2003)
Revision: 4028
Log message:

      - Moved unify_mm from Term_ds to reflib. The code didn't have anything
      that really needed access to Term_ds internal interfaces and reflib
      is a more appropriate place for code like it (a basic proof-search
      helper tool that is not a part of "trusted" system core).
      
      - Removed Rob_ds from the list of compiled files. Since it's not currently
      being used, there does not seem to be any reason to have it compiled
      (VN, do you agree?)
      
      - Added limited support for TermMan.clause_addr to Term_std (it is true
      that Term_std does not have a agenric way fo addressing a goal, but it
      doesn't mean we can not make clause_addr work for positive numbers,
      which is what it is ever used for anyway).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-31 20:30:06 -0800 (Fri, 31 Jan 2003)
Revision: 4033
Log message:

      A few minor changes.