Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-02 08:27:02 -0700 (Wed, 02 May 2001)
Revision: 3204
Log message:

      Reviwed ocaml_sos.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-02 08:35:09 -0700 (Wed, 02 May 2001)
Revision: 3205
Log message:

      Eliminated some non-standard and unnecessary usage of slot{}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-02 12:33:01 -0700 (Wed, 02 May 2001)
Revision: 3206
Log message:

      Exposed the param_shape type that I need to add shapes to opname parsing.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-05-04 01:45:12 -0700 (Fri, 04 May 2001)
Revision: 3207
Log message:

      1.Some minor changes in old files
      2.First ugly approach to Arith implementation. It just can find contradiction
        and construct contradictory inequality. Next step will be polynoms and
        inequalities normalization. It will increase range of input inequalities and
        let easily prove resulting contradictory inequality.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-05-04 01:49:54 -0700 (Fri, 04 May 2001)
Revision: 3208
Log message:

      Core of Arith - search positive cycle in labelled graph.
      It also contains bridge from meta-prl sequents to graphs.
      Probably it should be splitted into piece for mllib and
      sequent-dependent part.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-05-04 02:03:12 -0700 (Fri, 04 May 2001)
Revision: 3209
Log message:

      Forgot to commit
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-05-04 02:03:50 -0700 (Fri, 04 May 2001)
Revision: 3210
Log message:

      Forgot to checkin
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-04 09:38:27 -0700 (Fri, 04 May 2001)
Revision: 3211
Log message:

      Eliminated more unnecessary usages of slot.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-06 14:08:07 -0700 (Sun, 06 May 2001)
Revision: 3212
Log message:

      A few display form fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-06 15:31:55 -0700 (Sun, 06 May 2001)
Revision: 3213
Log message:

      - Rformat now will use no more than 1/3 of the total width on the left tabs.
      
      - I've added the short_string_of_term function to Simple_print that creates
      a string of the length at most 120. More importantly, it aborts printing
      as soone as it hits the margin, so no matter how big the term is, it should
      work fast.
      
      - debug_dform debugging now uses the short_string_of_term, so it will now
      hopefully produce managable output even on big terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-07 14:12:15 -0700 (Mon, 07 May 2001)
Revision: 3214
Log message:

      Check display forms at compile time.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-07 15:04:01 -0700 (Mon, 07 May 2001)
Revision: 3215
Log message:

      Pass the "strictness" flag to compile_contractum too, not just compile_redex.
      For now, the compile_contractum is not using it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-07 16:29:35 -0700 (Mon, 07 May 2001)
Revision: 3216
Log message:

      - Check the arity of the SO variables in the contractum at compile time.
      
      - In rules & rewrites (``Strict'' mode) disallow turning bound variables
      into free ones. I actually found two bugs in itt_rfun using this one!
      
      - In display forms (``Relaxed'' mode) allow turning anything (parameters,
      bound variables, etc) into variables.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-07 20:37:36 -0700 (Mon, 07 May 2001)
Revision: 3217
Log message:

      - Better error messages for typos in rules and rewrites.
      
      - Fixed syntax of the Fol_struct.thin rule
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-07 20:57:53 -0700 (Mon, 07 May 2001)
Revision: 3218
Log message:

      The code responsible for computing extracts is completely broken (see BUGS 4.4
      and 4.10) and is generating unwarranted error messages as soon as I start
      fixing rewriter bugs that were masking refiner bugs...
      
      As a temporary measure I am disabling the extract computation code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 09:32:08 -0700 (Tue, 08 May 2001)
Revision: 3219
Log message:

      I accidentally disabled the code that was creating display forms - fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 10:57:28 -0700 (Tue, 08 May 2001)
Revision: 3220
Log message:

      Reverting the last change I did on dforms in this file - that was a mistake.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 12:50:28 -0700 (Tue, 08 May 2001)
Revision: 3221
Log message:

      Disallow changing parameter types in rewriter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 15:00:34 -0700 (Tue, 08 May 2001)
Revision: 3222
Log message:

      - Fixed slot["raw", ...]
      - Fixed couple small typos.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 16:59:11 -0700 (Tue, 08 May 2001)
Revision: 3223
Log message:

      Finally, I am able to commit what I was getting to
      in all these commits over the last several days.
      
      I changed the parser to index declared opnames by its "shape" -
      last string of opname + parameter types + subterm arities
      instead of just the last string (as it used to be). This means that
      the parser now checks whether the usage of an opname corresponds
      to its declaration. This allowed me to detect numerous typos in
      display forms and even some rules and rewrites and, hopefully,
      will prevent people from making such typos in the future.
      
      This is only the first pass of the implementation. I still need to:
      - make sure none of my fixes broke any display forms that used to work
        because of typos cancelling each other
      - update the documentation
      - implement checking of shapes on the opnames specified using the
        Module!name notation (currently no checking is done on such opnames)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 18:46:15 -0700 (Tue, 08 May 2001)
Revision: 3224
Log message:

      Replaced the member operator with equal to match what we did for ITT
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-08 19:10:06 -0700 (Tue, 08 May 2001)
Revision: 3225
Log message:

      TPTP: added missing declarations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-09 09:26:54 -0700 (Wed, 09 May 2001)
Revision: 3226
Log message:

      - Removed references to [un]fold_momber from FOL.
      - TeX fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-14 13:53:50 -0700 (Mon, 14 May 2001)
Revision: 3229
Log message:

      Cosmetic changes to avoid warnings with newer versions of GCC.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-14 23:55:08 -0700 (Mon, 14 May 2001)
Revision: 3230
Log message:

      Minor tweaks.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-15 00:10:57 -0700 (Tue, 15 May 2001)
Revision: 3231
Log message:

      Use Mozilla when available.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-17 15:06:20 -0700 (Thu, 17 May 2001)
Revision: 3232
Log message:

      I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals
      with both the meta-level squash operator (Base_trivial!squash{}) and the type
      theory squash operator (Itt_squash!squash{'A}). This makes sense because
      these two operators are almost exectly the same in nature except for oe
      being a meta-level operator and another - an object-level one.
      
      This commit also renames Itt_hide!hide into Itt_squash!squash. This means
      that we now have two operators named "squash", however this should not cause
      any confusion since all part of the system (including the parser and display
      form mechanism) take into account the number of arguments.
      
      Warning: This commit probably broke lots of proofs. I plan to fix that
      after I have a chance to rewrite the squash theory a little better (for
      now I just copied the one from Itt_hide). Hopefully, I should have it
      done within a week.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-20 14:38:52 -0700 (Sun, 20 May 2001)
Revision: 3233
Log message:

      These are unused since May'99.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-20 15:10:16 -0700 (Sun, 20 May 2001)
Revision: 3234
Log message:

      Exported locale-aware libc functions such as isdigit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-20 16:04:08 -0700 (Sun, 20 May 2001)
Revision: 3235
Log message:

      Display form fixes.
      
      - TeX: all object-level terms (theorem statements, etc) are now typeset
      in math mode.
      
      - Tex: variable names are now parsed to detect indeces. In particular,
        'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.
      
      - Tex: `|' symbol in display forms is now always handled correctly.
      
      - Numerous small fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-23 08:42:53 -0700 (Wed, 23 May 2001)
Revision: 3236
Log message:

      - Proved all the theorems in itt_squash.
      - Still need to figure out the right way to do squash_resource and
      the relevant tactics.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-26 13:21:05 -0700 (Sat, 26 May 2001)
Revision: 3237
Log message:

      Fixed term -> AST conversion for array patterns.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-27 11:08:16 -0700 (Sun, 27 May 2001)
Revision: 3238
Log message:

      I rewrote the Itt_squash tactics and the squash_resource implementation
      and made sure most of the theories expand.
      
      - I implemented squash_resource annotations - see documentation for
      more information
      - autoT will now always attempt to squash the sequent and unsquash all
      the hypotheses
      
      Left to do:
      - Update the documentation, especially the itt_quickref.txt
      - Itt_collections would not expand, but I was planning to rewrite it anyway,
      so it does not make sense to try fixing the current version.
      - Itt_fset would not expand, it needs lots of work, including (preferably)
      some improvements to autoT (not squash-related).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-28 08:14:24 -0700 (Mon, 28 May 2001)
Revision: 3239
Log message:

      CZF: renamed squash-related tactics, but haven't checked that all proofs
      will expand correctly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-28 15:16:27 -0700 (Mon, 28 May 2001)
Revision: 3240
Log message:

      Use terminal width for output in a more consistent manner.