Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-01 07:49:18 -0800 (Sun, 01 Feb 2004)
Revision: 5328
Log message:

      (Hopefully) all cases covered.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-01 17:34:01 -0800 (Sun, 01 Feb 2004)
Revision: 5329
Log message:

      Removed all tryT, switched off debug output
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-01 19:50:58 -0800 (Sun, 01 Feb 2004)
Revision: 5330
Log message:

      "Do not re-assert same thing more than once" - added but disabled due to
      VERY weird behaviour - will describe it in "supinf todo" thread.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-01 21:31:30 -0800 (Sun, 01 Feb 2004)
Revision: 5331
Log message:

      "Do not re-assert same thing more than once" - enabled,
      more than 10 times speedup gained (test4, from 32 to less than 3 seconds)
      
      For "weird behaviour" see "supinf todo" thread.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-01 22:21:05 -0800 (Sun, 01 Feb 2004)
Revision: 5332
Log message:

      Some wf-goals are asserted to avoid re-proving them many times.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-01 23:00:41 -0800 (Sun, 01 Feb 2004)
Revision: 5333
Log message:

      thenAT tac does not apply tac to subgoals with empty label anymore.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-02 18:00:29 -0800 (Mon, 02 Feb 2004)
Revision: 5334
Log message:

      When chdir fails, make the best effort to put things back where they were.
      This fixes bug 143, as well as a number of less obvious issues.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-02 18:02:56 -0800 (Mon, 02 Feb 2004)
Revision: 5335
Log message:

      Display the status of the current node (e.g. the status of the proof generated
      by the current rulebox only).
      I implemented it to be displayed after the path status in "< >".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-02 22:36:55 -0800 (Mon, 02 Feb 2004)
Revision: 5336
Log message:

      Removed the bound_vars function and all the places that used it (for no good
      reason).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-02-02 23:53:34 -0800 (Mon, 02 Feb 2004)
Revision: 5337
Log message:

      Temporary solution for solve the incompleteness of rule "int_div_rem".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-03 00:18:42 -0800 (Tue, 03 Feb 2004)
Revision: 5338
Log message:

      Adding a slightly more conservative version of nat_is_int
      to the intro resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-03 15:51:57 -0800 (Tue, 03 Feb 2004)
Revision: 5339
Log message:

      - For prim rules, check whether the specified extract is "universal".
      - Fixed a number of places where a non-universal extract was specified.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-03 15:54:09 -0800 (Tue, 03 Feb 2004)
Revision: 5340
Log message:

      Fixing the extract specs for the prim rules. I am not sure what the correct
      extracts are, so using "it".
      

Changes by: ( at unknown.email)
Date: 2004-02-05 08:39:21 -0800 (Thu, 05 Feb 2004)
Revision: 5342
Log message:

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

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-06 16:13:39 -0800 (Fri, 06 Feb 2004)
Revision: 5343
Log message:

      1.arith - Aleksey's suggestions implemented but not really used yet.
      2.supinf - some theory-independent parts moved outside.
      3.term_order - comparison of terms moved outside of itt_int_arith,
      comparison of bound-terms implemented in correct way (hopefully).
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-06 16:13:48 -0800 (Fri, 06 Feb 2004)
Revision: 5344
Log message:

      Took the first step in implementing recursive sequents.
      
      My practice has been to change e.g. Hypothesis to Hypothesis' as I correct each
      function.  That way rebuilding metaprl will tell me where to look for the next
      error.  Once the implementation is finished we can strip out the primes with a
      sed script.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-06 21:42:57 -0800 (Fri, 06 Feb 2004)
Revision: 5346
Log message:

      This might return the status-check time to "normal" or even improve it.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-06 23:11:05 -0800 (Fri, 06 Feb 2004)
Revision: 5347
Log message:

      Hopefully this will fix all the proofs broken by previous two commits.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-07 19:10:12 -0800 (Sat, 07 Feb 2004)
Revision: 5348
Log message:

      Proved lemmas that were introduced yesterday.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-07 19:28:04 -0800 (Sat, 07 Feb 2004)
Revision: 5349
Log message:

      Were too careless in applying normalizeC
      (in order to normalize candidate inequalities for arithT) so it was applied to
      some terms it shouldn't have been to, and that injected some needless wf-subgoals.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-07 21:33:03 -0800 (Sat, 07 Feb 2004)
Revision: 5350
Log message:

      all occurences of dT in arithT replaced with explicit rules.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-09 06:30:05 -0800 (Mon, 09 Feb 2004)
Revision: 5351
Log message:

      Introduced one small resource arith_unfold - it does all rewrites which are not
      actually reductions (distributivity, getting rid of subtraction).
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-09 17:25:38 -0800 (Mon, 09 Feb 2004)
Revision: 5352
Log message:

      Converted to recursive sequents.  build_HypBinding could be simplified if
      new_name is guaranteed to come up with something unique.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-09 22:12:34 -0800 (Mon, 09 Feb 2004)
Revision: 5353
Log message:

      Moved whole normalizeC to arith_unfold resource. Though some rewrites
      results in failC (because there is no way to express ordering of term in
      patterns, sorting rewrites just fail of there is no need to swap certain terms)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-09 22:58:49 -0800 (Mon, 09 Feb 2004)
Revision: 5354
Log message:

      Bug fix for previous rewrite: one more rewrite added (-a) <--> (-1)*a
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-09 23:35:58 -0800 (Mon, 09 Feb 2004)
Revision: 5355
Log message:

      Bug fix to a bug fix - accidentally erased one character in a "wrong place".
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-10 16:56:06 -0800 (Tue, 10 Feb 2004)
Revision: 5356
Log message:

      Efficiency improvements suggested by Aleksey.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-10 17:19:09 -0800 (Tue, 10 Feb 2004)
Revision: 5357
Log message:

      Cleaning up all unused code left after yesterday commits,
      proved all new lemmas.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-10 17:35:35 -0800 (Tue, 10 Feb 2004)
Revision: 5358
Log message:

      A bit more effort to maintain sharing.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-10 18:41:06 -0800 (Tue, 10 Feb 2004)
Revision: 5359
Log message:

      Removed old interface.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-11 15:14:56 -0800 (Wed, 11 Feb 2004)
Revision: 5360
Log message:

      Convert to recursive sequents.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-11 16:41:36 -0800 (Wed, 11 Feb 2004)
Revision: 5361
Log message:

      Convert to recursive sequents.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-11 23:25:53 -0800 (Wed, 11 Feb 2004)
Revision: 5364
Log message:

      Fixed potential capture bug involving substitution through sequents.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-02-11 23:33:21 -0800 (Wed, 11 Feb 2004)
Revision: 5365
Log message:

      Changing an anonymous function into a named function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-11 23:51:28 -0800 (Wed, 11 Feb 2004)
Revision: 5366
Log message:

      Inline the folding to make it tail-recursive and minimize the allocations;
      other fixes.
      

Changes by: ( at unknown.email)
Date: 2004-02-11 23:51:28 -0800 (Wed, 11 Feb 2004)
Revision: 5367
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-12 00:12:49 -0800 (Thu, 12 Feb 2004)
Revision: 5368
Log message:

      This is a new approach to implementing recursive sequents (as discussed
      with Nathan and Cristian earlier today) - instead of modifying the hypothesis
      type, modify the esequent type by adding a separate "array" with the "equality"
      parts of the sequent hypothesis. This should make it much easier to process the
      sequent in a binding-consistent order.
      
      P.S. The new array component is allowed (but not required) to have zero length
      to signify that the sequent is non-recursive.
      
      This commit is the first step - I modifed some (but not all) interface files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-12 19:40:43 -0800 (Thu, 12 Feb 2004)
Revision: 5370
Log message:

      Top_conversionals.apply_rewrite should use tactic_arg, not bookmark as an input.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-13 00:31:35 -0800 (Fri, 13 Feb 2004)
Revision: 5371
Log message:

      Added an nth_hyp resource. Any axiom (e.g. assumption-free rule) of the form
      
      <H>; x: ...; <J[x]> >- ...
      
      can now be annotated with {| nth_hyp |}. The corresponding tactic is
      Auto_tactic.nthHypT (the old limited Itt_struct.nthHypT went away),
      which is also included in trivialT and autoT.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2004-02-13 13:53:33 -0800 (Fri, 13 Feb 2004)
Revision: 5373
Log message:

      updated jprover and metaprl connections to fdl
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2004-02-13 16:41:07 -0800 (Fri, 13 Feb 2004)
Revision: 5374
Log message:

      changed mathbus registry so that it is only parsed and loaded when needed
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-13 17:36:36 -0800 (Fri, 13 Feb 2004)
Revision: 5375
Log message:

      A follow-up to the previous nthHypT commit - I simplified a few things.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-13 22:26:00 -0800 (Fri, 13 Feb 2004)
Revision: 5376
Log message:

      Normalize only contradictory subset of all inequalities.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-14 16:03:38 -0800 (Sat, 14 Feb 2004)
Revision: 5377
Log message:

      Removing unused "open" directives.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-14 22:22:36 -0800 (Sat, 14 Feb 2004)
Revision: 5378
Log message:

      Added an artificial example "testn" to check usefulness of my yesterday commit.
      I generate 10 "random" terms (of depth 3) and 10 inequalities over them.
      After yesterday commit it takes 5 secs to find a contradiction among those inequalities,
      a day before it would take 108 secs(!)
      So I think we should keep yesterday commit despite a small slowing down.
      It is slow on simple terms because contradictory inequalities are normalized twice but
      as terms become more complex and number of "unutilized" inequlaities grows
      we save more and more time.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-16 21:53:23 -0800 (Mon, 16 Feb 2004)
Revision: 5379
Log message:

      Some lemmas on the way to integer support in SupInf.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-17 22:04:40 -0800 (Tue, 17 Feb 2004)
Revision: 5383
Log message:

      1.previous fix for thenAT behaviour was not complete.
      2.itt_ring and itt_field removed.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-17 22:07:17 -0800 (Tue, 17 Feb 2004)
Revision: 5384
Log message:

      forgot to include:
      1.previous fix for thenAT behaviour was not complete.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-19 23:02:32 -0800 (Thu, 19 Feb 2004)
Revision: 5389
Log message:

      itt_int_arith: added "cacheT info tac" which runs tac once,
      memorizes all aux-goals, assert them, reruns tac and complete
      all aux-goals with nthHypT.
      
      tactic_boot_sig: exposed type extract and function refine in TacticSig in order
      to be able to rerun a tactic. This might go away if we decide to move cacheT
      to the "general purpose library".
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-20 12:26:50 -0800 (Fri, 20 Feb 2004)
Revision: 5391
Log message:

      Just want to make arithT to work correctly with cacheT
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-20 14:17:58 -0800 (Fri, 20 Feb 2004)
Revision: 5393
Log message:

      Forgot to remove debugging messages.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-20 22:34:25 -0800 (Fri, 20 Feb 2004)
Revision: 5398
Log message:

      Removing cacheT from arithT because it does not give any noticable performance boost.
      

Changes by: ( at unknown.email)
Date: 2004-02-20 22:34:25 -0800 (Fri, 20 Feb 2004)
Revision: 5399
Log message:

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

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-21 20:05:26 -0800 (Sat, 21 Feb 2004)
Revision: 5400
Log message:

      I don't know why it refers to "cygwin32", on my computer OSTYPE is "cygwin".
      So I added one more case for setting EXE var.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-23 22:30:03 -0800 (Mon, 23 Feb 2004)
Revision: 5401
Log message:

      Minor change: I believe that we need to keep the "local" contexts intact
      for the sequent stuff to work correctly. Not fully tested, but the rest
      of term_match_table will soon change a lot anyway...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-24 01:01:27 -0800 (Tue, 24 Feb 2004)
Revision: 5402
Log message:

      Minor documentation fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-24 01:28:36 -0800 (Tue, 24 Feb 2004)
Revision: 5403
Log message:

      More docummentation fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-24 01:37:15 -0800 (Tue, 24 Feb 2004)
Revision: 5404
Log message:

      More minor doccumentation fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-24 02:07:11 -0800 (Tue, 24 Feb 2004)
Revision: 5405
Log message:

      Yet more docummentation fixes.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-24 17:58:33 -0800 (Tue, 24 Feb 2004)
Revision: 5406
Log message:

      testn is now complete (if arithT succeeds)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-24 18:18:14 -0800 (Tue, 24 Feb 2004)
Revision: 5407
Log message:

      This commit partly solves problem the bug 159 though it could be incorrect,
      at least rewrites with sequent args do compile with this change.
      (Application does not work unfortunately).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-25 00:54:40 -0800 (Wed, 25 Feb 2004)
Revision: 5409
Log message:

      *******************************************
      *               WARNING                   *
      * This commit breaks .prla compatibility! *
      * Export your proofs before updating!!!   *
      *******************************************
      
      Removing the unused ref_parent field from the tactic_arg (as well as related
      fields from related data structures).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-25 01:04:31 -0800 (Wed, 25 Feb 2004)
Revision: 5410
Log message:

      Removed a bunch of unsed modules (a small portion of filter_ast that was still
      relevant was merged into filter_prog).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-25 01:10:54 -0800 (Wed, 25 Feb 2004)
Revision: 5411
Log message:

      Removing some more ref_parent - related code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-25 22:48:34 -0800 (Wed, 25 Feb 2004)
Revision: 5413
Log message:

      This is just code clean-up and should be a no-op:
      - I reformatted some of the code - removed unneeded parens, changed to the
      canonical indentation style, etc.
      - I simplified some of the code (mostly - common subexpression elimination,
      created a helper function for some very frequently used constructs, etc).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 00:46:25 -0800 (Thu, 26 Feb 2004)
Revision: 5414
Log message:

      Replaced a number of "with _" with more specific exeption matches,
      commented others with "we do want to catch everything here".
      
      I've filed bug 164 for the remaining "with _" (all in the FDL code).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 01:19:06 -0800 (Thu, 26 Feb 2004)
Revision: 5415
Log message:

      Even when the domain of a substitution happens to clash with the name
      of a SO variable included in the term the substitution is being applied to,
      there is absolutely no reason for MetaPRL to complain about it. Substitutions
      just substitute for FO variables and ignore everything else (for now we still
      complain about clashes with context variables - just in case).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 01:57:07 -0800 (Thu, 26 Feb 2004)
Revision: 5416
Log message:

      Old .prla file generate Proof_boot.io_proof_of_proof warnings, which is probably OK.
      The warnings used to be huge and ugly, made them shorter (at least until we regenerate
      all the old .prla files that give them).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 04:21:27 -0800 (Thu, 26 Feb 2004)
Revision: 5417
Log message:

      Keep FO variables as FO variable (not as a wwildcard pattern) in a term table.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 05:27:30 -0800 (Thu, 26 Feb 2004)
Revision: 5418
Log message:

      - Turned a few primitive rules into interactive.
      - Annotated couple more rules for inclusion into nth_hyp.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 16:00:17 -0800 (Thu, 26 Feb 2004)
Revision: 5419
Log message:

      Use the Term_match_table's built-in resource creator instead of building
      it "manually".
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-28 22:03:01 -0800 (Sat, 28 Feb 2004)
Revision: 5423
Log message:

      Changed normalization rewrite from top-down to bottom-up strategy.
      It makes noticable improvement both un expand time and number of primitive steps.