Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-02 14:36:08 -0700 (Thu, 02 Jun 2005)
Revision: 7345
Log message:

      Added a bit more on reference cells.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-02 22:46:24 -0700 (Thu, 02 Jun 2005)
Revision: 7346
Log message:

      Added itt_hoas_bterm to theories.pdf
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-03 03:16:49 -0700 (Fri, 03 Jun 2005)
Revision: 7347
Log message:

      OMakeroot now requires omake 0.9.4.19 (since it refers to STDLIB variable
      that was added in 0.9.4.19)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-03 10:31:07 -0700 (Fri, 03 Jun 2005)
Revision: 7348
Log message:

      Added some initial text on splay trees.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-04 09:50:11 -0700 (Sat, 04 Jun 2005)
Revision: 7354
Log message:

      Documentation update.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-04 12:27:45 -0700 (Sat, 04 Jun 2005)
Revision: 7355
Log message:

      Made the dform_base type abstract.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-04 18:36:51 -0700 (Sat, 04 Jun 2005)
Revision: 7356
Log message:

      This is an example of using the vmount function to specify a build
      directory.
      
      If you run "omake VERSION=foo" then metaprl will be built in the foo/
      subdirectory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-04 19:03:02 -0700 (Sat, 04 Jun 2005)
Revision: 7357
Log message:

      Because of the "VERSION" variable clash, this OMakeroot now requires omake >=
      0.9.4.21
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-05 15:28:49 -0700 (Sun, 05 Jun 2005)
Revision: 7358
Log message:

      Minor changes to the VERSION.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-05 17:40:48 -0700 (Sun, 05 Jun 2005)
Revision: 7359
Log message:

      The .o suffix should be $(EXT_OBJ).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-05 19:14:06 -0700 (Sun, 05 Jun 2005)
Revision: 7360
Log message:

      Opname "shortening" in display forms.
      
      Changed the display forms API making the shortener an integral part of the
      dform_base type. Now all the standard display uses the shortener properly. I
      also changed the shortener type adding an op_kind (OpnameNormal/OpnameToken
      flag) to the list of its arguments and change the slot[opname:t] display to
      use the shortener.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-05 20:48:11 -0700 (Sun, 05 Jun 2005)
Revision: 7361
Log message:

      The proper opname shortener support (previous commit) made a number of display
      forms unnecessary.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-05 21:26:30 -0700 (Sun, 05 Jun 2005)
Revision: 7362
Log message:

      Fixed a typo
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-13 16:22:25 -0700 (Mon, 13 Jun 2005)
Revision: 7366
Log message:

      Minor type fix
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-13 16:51:32 -0700 (Mon, 13 Jun 2005)
Revision: 7367
Log message:

      Minor type fixes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-14 09:39:02 -0700 (Tue, 14 Jun 2005)
Revision: 7369
Log message:

      Added a proper type for logic/calculus specification in JProver (which
      replaces a string encoding).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-14 19:40:32 -0700 (Tue, 14 Jun 2005)
Revision: 7371
Log message:

      replaced array with list for representing node subtrees, there are still several List.nth there but except for the root all lists are either of length 1 or 2
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-14 19:47:19 -0700 (Tue, 14 Jun 2005)
Revision: 7372
Log message:

      reverting my accidental commit
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-16 00:49:07 -0700 (Thu, 16 Jun 2005)
Revision: 7375
Log message:

      Further code clean-up
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-16 13:43:09 -0700 (Thu, 16 Jun 2005)
Revision: 7377
Log message:

      Minor clean-up
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-16 17:51:13 -0700 (Thu, 16 Jun 2005)
Revision: 7378
Log message:

      Changed the string encoding of left/right paths into a list one (reversing the
      order). For example, the path "llrr" is now [Right; Right; Left; Left]
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-16 19:13:45 -0700 (Thu, 16 Jun 2005)
Revision: 7379
Log message:

      Inlined the "permute" function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-16 21:13:20 -0700 (Thu, 16 Jun 2005)
Revision: 7380
Log message:

      Simplified the path handling, getting rid of the next_direction function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-16 23:13:57 -0700 (Thu, 16 Jun 2005)
Revision: 7381
Log message:

      Inlined some of the match tests.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-17 00:54:22 -0700 (Fri, 17 Jun 2005)
Revision: 7382
Log message:

      Further clean-ups:
      - act_addr now only contains the most recent direction followed instead of the
        whole path followed
      
      - some of the function were getting tsubrel as an argument, but never using it
      
      - couple of places had "if expr then expr', true else expr', false" instead of
        just expr', expr
      
      - other minor simplifications
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-17 18:11:13 -0700 (Fri, 17 Jun 2005)
Revision: 7384
Log message:

      This is incomplete, but I better commit before I lose it.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-17 19:00:23 -0700 (Fri, 17 Jun 2005)
Revision: 7385
Log message:

      Moved both instances of unification algorithms into separate files.
      This forced some code to move to separate files as well.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-17 21:19:39 -0700 (Fri, 17 Jun 2005)
Revision: 7386
Log message:

      Unified the way non-unifiability is propagated.
      It was via exceptions in quantifier unification and via return flag in propositional unification.
      Now it's via exceptions in both cases.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-17 22:14:37 -0700 (Fri, 17 Jun 2005)
Revision: 7387
Log message:

      One more function happened to do the same thing in different ways, joined it to one common function.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-18 11:16:31 -0700 (Sat, 18 Jun 2005)
Revision: 7388
Log message:

      added $(EXE) to camlp4o and camlp4r
      
      with Jason's recent commit it seems to fix the problems with Cygwin
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-18 17:41:22 -0700 (Sat, 18 Jun 2005)
Revision: 7389
Log message:

      Unified two unification algorithms into one
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-20 18:29:09 -0700 (Mon, 20 Jun 2005)
Revision: 7395
Log message:

      Unification stage is now uses non-string representation of positions.
      But the rest is still string-base and conversions happen very often,
      so there is actually slow down right now.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-20 19:54:29 -0700 (Mon, 20 Jun 2005)
Revision: 7396
Log message:

      Duplicated the string fieldis with more structural fields in pos and atom types.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-21 07:55:04 -0700 (Tue, 21 Jun 2005)
Revision: 7397
Log message:

      More code converted to non-string format
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-21 21:19:18 -0700 (Tue, 21 Jun 2005)
Revision: 7398
Log message:

      A little more progress on getting rid of string representation.
      There was a problem exposed with only one test !!!
      Making changes in such a situation is a bit scary.
      I'll make the data model more flexible to reflect potential misuses of string representation (just in case they are not actually misuses but legitimate ones).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-06-23 14:42:50 -0700 (Thu, 23 Jun 2005)
Revision: 7399
Log message:

      More text.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-24 15:55:23 -0700 (Fri, 24 Jun 2005)
Revision: 7400
Log message:

      Forgot to commit it for consistency - I changed the name of a probably unused variable,
      provided as a string parameter to J-prover.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-24 19:09:10 -0700 (Fri, 24 Jun 2005)
Revision: 7401
Log message:

      Added the MMC's <#C> notation for contexts that do not introduce bindings to
      the default term grammar.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-24 19:21:42 -0700 (Fri, 24 Jun 2005)
Revision: 7402
Log message:

      Do a backup_all before processing a syscall. This should cure the most common
      cases of bad "!rebuild; !restart" interactions.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 17:00:56 -0700 (Sat, 25 Jun 2005)
Revision: 7403
Log message:

      A little more progress.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 17:15:41 -0700 (Sat, 25 Jun 2005)
Revision: 7404
Log message:

      1. replaced '0'|'1'|...|'9' with '0'..'9'
      
      2. replaced
       let x=...
       and y=...
      with
       let x=... in
       let y=...
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 17:22:33 -0700 (Sat, 25 Jun 2005)
Revision: 7405
Log message:

      replaced and's with let's
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 18:10:36 -0700 (Sat, 25 Jun 2005)
Revision: 7406
Log message:

      Inlined all the unification condition r1..r10 into one big match.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 18:38:35 -0700 (Sat, 25 Jun 2005)
Revision: 7407
Log message:

      Removed a small redundancy introduced in the previous commit.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 18:47:55 -0700 (Sat, 25 Jun 2005)
Revision: 7408
Log message:

      There was a redundant conversion from position to string and back, removed.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 19:01:11 -0700 (Sat, 25 Jun 2005)
Revision: 7409
Log message:

      Removed one more place where new positions where constructed by direct operations
      on strings.
      As far as I understand only one such places remains - in proof reconstruction code,
      by I don't care about that part for now.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 19:13:45 -0700 (Sat, 25 Jun 2005)
Revision: 7410
Log message:

      A small progress. I do commits so often because otherwise it tends to span for 3 hours
      and results in non-working code :(
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 19:41:30 -0700 (Sat, 25 Jun 2005)
Revision: 7411
Log message:

      A little more progress
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 20:02:59 -0700 (Sat, 25 Jun 2005)
Revision: 7412
Log message:

      And more.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 20:32:35 -0700 (Sat, 25 Jun 2005)
Revision: 7413
Log message:

      Getting rid of splitting substitutions into two lists and then recombining them two lines later.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-25 23:33:11 -0700 (Sat, 25 Jun 2005)
Revision: 7414
Log message:

      Replaced another casual use of strings with option-type
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-26 13:27:06 -0700 (Sun, 26 Jun 2005)
Revision: 7415
Log message:

      - Fill reasonable defaults for TERMS, REFINER, etc (instead of "undefined"),
        making it possible to use the initial default mk/config without changes
        (provided "THEORIES = base itt" is what one wants).
      
      - Give a better message when a new mk/config is created. Will work best with
        omake >= 0.9.4.24
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 15:15:22 -0700 (Sun, 26 Jun 2005)
Revision: 7416
Log message:

      Introduced a more unform naming convention for string representation of positions.
      Removed the (hopefully) last place where strings are combined to produce another position.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 15:45:25 -0700 (Sun, 26 Jun 2005)
Revision: 7417
Log message:

      Slowly moving away string representation of positions
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 15:59:47 -0700 (Sun, 26 Jun 2005)
Revision: 7418
Log message:

      More progress
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 16:09:21 -0700 (Sun, 26 Jun 2005)
Revision: 7419
Log message:

      and more progress
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 16:18:29 -0700 (Sun, 26 Jun 2005)
Revision: 7420
Log message:

      and more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 16:26:43 -0700 (Sun, 26 Jun 2005)
Revision: 7421
Log message:

      a little more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 16:36:01 -0700 (Sun, 26 Jun 2005)
Revision: 7422
Log message:

      and more progress
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 16:56:03 -0700 (Sun, 26 Jun 2005)
Revision: 7423
Log message:

      More progress, I expanded it to a new group of functions, hence temporal performance hit.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 17:32:51 -0700 (Sun, 26 Jun 2005)
Revision: 7424
Log message:

      even more changes
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 17:59:17 -0700 (Sun, 26 Jun 2005)
Revision: 7425
Log message:

      and more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 18:42:28 -0700 (Sun, 26 Jun 2005)
Revision: 7426
Log message:

      another small change
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 18:54:55 -0700 (Sun, 26 Jun 2005)
Revision: 7427
Log message:

      another change
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 19:11:04 -0700 (Sun, 26 Jun 2005)
Revision: 7428
Log message:

      And more...
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 19:21:43 -0700 (Sun, 26 Jun 2005)
Revision: 7429
Log message:

      morechanges
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 19:39:07 -0700 (Sun, 26 Jun 2005)
Revision: 7430
Log message:

      and more...
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-26 20:00:13 -0700 (Sun, 26 Jun 2005)
Revision: 7431
Log message:

      Variables bound be All/Exists should be represented as symbols, not as strings.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-26 22:30:42 -0700 (Sun, 26 Jun 2005)
Revision: 7432
Log message:

      Simplified the theory a bit to better match the FOL tutorial:
       - Use "open Basic_tactics" instead of a bunch of seemingly random "open"
         statements for refiner/tactic_type/dtactic/etc modules.
       - unfold_not is a definition, not a prim_rw.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 00:04:10 -0700 (Mon, 27 Jun 2005)
Revision: 7433
Log message:

      a little more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 00:21:31 -0700 (Mon, 27 Jun 2005)
Revision: 7434
Log message:

      more progress
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 00:57:39 -0700 (Mon, 27 Jun 2005)
Revision: 7435
Log message:

      some more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 01:14:55 -0700 (Mon, 27 Jun 2005)
Revision: 7436
Log message:

      And more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 01:28:29 -0700 (Mon, 27 Jun 2005)
Revision: 7437
Log message:

      more changes
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 01:55:22 -0700 (Mon, 27 Jun 2005)
Revision: 7438
Log message:

      more progress
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 14:06:40 -0700 (Mon, 27 Jun 2005)
Revision: 7439
Log message:

      made position ordering as close to their string representation ordering as possible,
      unfortunately 1 and 14 have different order as integers vs as strings and for some reason
      it makes differences for J-prover.
      There is probably some unaccounted string comparison which makes it improtant,
      though I didn't find it.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 15:17:38 -0700 (Mon, 27 Jun 2005)
Revision: 7440
Log message:

      Removed name field (string) from pos type. atom type still has aname because of ordering issue.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 15:44:36 -0700 (Mon, 27 Jun 2005)
Revision: 7441
Log message:

      replaced (atom.aprefix : string list) with (atom.aposprefix : position list)
      renamed polarity O|I to Zero|One for better readability
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 17:02:14 -0700 (Mon, 27 Jun 2005)
Revision: 7442
Log message:

      Subtrees were indexed from 1 to n but because lists are indexed from 0, there was
      lots of adding and subtracting of 1s.
      Now they are gone (except for multiplicity, which is not a big deal).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 18:04:10 -0700 (Mon, 27 Jun 2005)
Revision: 7443
Log message:

      Removed a helper data type that I used in my previous commit to catch all index shifts.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 18:19:02 -0700 (Mon, 27 Jun 2005)
Revision: 7444
Log message:

      bproof as now position-based instead of string-based
      only ptree and sorting is still string based.
      in ptree strings used not only to store positions but for something else also.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 19:58:52 -0700 (Mon, 27 Jun 2005)
Revision: 7445
Log message:

      preparations to remove string encoding from ptree type (the last one, excluding sorting issue).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-27 22:55:55 -0700 (Mon, 27 Jun 2005)
Revision: 7446
Log message:

      from now on ptree uses position type instead of strings.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 00:17:29 -0700 (Tue, 28 Jun 2005)
Revision: 7447
Log message:

      minor changes
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 00:47:32 -0700 (Tue, 28 Jun 2005)
Revision: 7448
Log message:

      use specialized equality for "position" instead of polymorphic (=)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 13:14:49 -0700 (Tue, 28 Jun 2005)
Revision: 7449
Log message:

      I started to experiment with replaciing List.append with List.rev_append.
      In certain cases ordering is not actually improtant.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 13:30:49 -0700 (Tue, 28 Jun 2005)
Revision: 7450
Log message:

      One more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 13:33:20 -0700 (Tue, 28 Jun 2005)
Revision: 7451
Log message:

      And more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 13:34:23 -0700 (Tue, 28 Jun 2005)
Revision: 7452
Log message:

      One more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 13:58:31 -0700 (Tue, 28 Jun 2005)
Revision: 7453
Log message:

      one more
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 14:10:27 -0700 (Tue, 28 Jun 2005)
Revision: 7454
Log message:

      more rev_append's
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 14:28:11 -0700 (Tue, 28 Jun 2005)
Revision: 7455
Log message:

      One more optimization
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 14:32:15 -0700 (Tue, 28 Jun 2005)
Revision: 7456
Log message:

      More rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 14:34:56 -0700 (Tue, 28 Jun 2005)
Revision: 7457
Log message:

      Some more rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 15:51:08 -0700 (Tue, 28 Jun 2005)
Revision: 7458
Log message:

      More rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 16:17:28 -0700 (Tue, 28 Jun 2005)
Revision: 7459
Log message:

      More rev_appends and other optimizations
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 16:32:04 -0700 (Tue, 28 Jun 2005)
Revision: 7460
Log message:

      replaced one map with rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 16:38:59 -0700 (Tue, 28 Jun 2005)
Revision: 7461
Log message:

      one more rev_append and one place idenitifed as not convertible to rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 16:41:24 -0700 (Tue, 28 Jun 2005)
Revision: 7462
Log message:

      Converted three nested mutually recursive functions into three non-nested mutually recursive functions.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 16:59:10 -0700 (Tue, 28 Jun 2005)
Revision: 7463
Log message:

      Moved one more nested function outside
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 17:04:26 -0700 (Tue, 28 Jun 2005)
Revision: 7464
Log message:

      more rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 17:10:05 -0700 (Tue, 28 Jun 2005)
Revision: 7465
Log message:

      one more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 17:16:24 -0700 (Tue, 28 Jun 2005)
Revision: 7466
Log message:

      one more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 17:19:49 -0700 (Tue, 28 Jun 2005)
Revision: 7467
Log message:

      a pair of rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 18:18:41 -0700 (Tue, 28 Jun 2005)
Revision: 7468
Log message:

      total, tot andsolve were mutually nested, now they are non nested
      (but still mutually recursive, of course).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 18:23:38 -0700 (Tue, 28 Jun 2005)
Revision: 7469
Log message:

      one more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 21:53:48 -0700 (Tue, 28 Jun 2005)
Revision: 7470
Log message:

      one more append turned to cons
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 21:56:57 -0700 (Tue, 28 Jun 2005)
Revision: 7471
Log message:

      one more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-28 21:59:00 -0700 (Tue, 28 Jun 2005)
Revision: 7472
Log message:

      append_orderings was reimplementing List.flatten, deleted
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 00:17:38 -0700 (Wed, 29 Jun 2005)
Revision: 7473
Log message:

      un-nested another pair of functions
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 00:45:41 -0700 (Wed, 29 Jun 2005)
Revision: 7474
Log message:

      a couple of appends replaced with cons
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 00:55:45 -0700 (Wed, 29 Jun 2005)
Revision: 7475
Log message:

      three more rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:05:19 -0700 (Wed, 29 Jun 2005)
Revision: 7476
Log message:

      two more rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:08:09 -0700 (Wed, 29 Jun 2005)
Revision: 7477
Log message:

      and more rev_appends
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:19:44 -0700 (Wed, 29 Jun 2005)
Revision: 7478
Log message:

      one more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:27:49 -0700 (Wed, 29 Jun 2005)
Revision: 7479
Log message:

      more re_appends and rev_maps
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:32:52 -0700 (Wed, 29 Jun 2005)
Revision: 7480
Log message:

      documenting a place where rev_append won't work
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:46:18 -0700 (Wed, 29 Jun 2005)
Revision: 7481
Log message:

      one more rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:49:17 -0700 (Wed, 29 Jun 2005)
Revision: 7482
Log message:

      documenting another place where rev_append won't work
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:52:44 -0700 (Wed, 29 Jun 2005)
Revision: 7483
Log message:

      one more place where rev_append won't work, plus some formatting fixes
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 01:55:20 -0700 (Wed, 29 Jun 2005)
Revision: 7484
Log message:

      more rev_maps
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:05:22 -0700 (Wed, 29 Jun 2005)
Revision: 7485
Log message:

      1.One more place where rev_append won't work
      2.One more rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:06:12 -0700 (Wed, 29 Jun 2005)
Revision: 7486
Log message:

      one more rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:07:47 -0700 (Wed, 29 Jun 2005)
Revision: 7487
Log message:

      three rev_maps
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:18:08 -0700 (Wed, 29 Jun 2005)
Revision: 7488
Log message:

      one more rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:19:38 -0700 (Wed, 29 Jun 2005)
Revision: 7489
Log message:

      two rev_maps
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:20:30 -0700 (Wed, 29 Jun 2005)
Revision: 7490
Log message:

      one rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:30:26 -0700 (Wed, 29 Jun 2005)
Revision: 7491
Log message:

      one more rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 02:33:57 -0700 (Wed, 29 Jun 2005)
Revision: 7492
Log message:

      one more rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 10:44:24 -0700 (Wed, 29 Jun 2005)
Revision: 7493
Log message:

      now in jtunify: one rev_append
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 10:55:49 -0700 (Wed, 29 Jun 2005)
Revision: 7494
Log message:

      documented a place where rev_append changes proofs
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 11:00:05 -0700 (Wed, 29 Jun 2005)
Revision: 7495
Log message:

      Replaced append with a cons
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 11:17:26 -0700 (Wed, 29 Jun 2005)
Revision: 7496
Log message:

      map -> rev_map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 11:26:45 -0700 (Wed, 29 Jun 2005)
Revision: 7497
Log message:

      one more place where rev_append does not work
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 15:47:31 -0700 (Wed, 29 Jun 2005)
Revision: 7498
Log message:

      It seems that connections should be stored as a set not as a list, here is first step towards this
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 15:57:38 -0700 (Wed, 29 Jun 2005)
Revision: 7499
Log message:

      lists of solved/unsolved positions are also sets from now on
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 16:12:34 -0700 (Wed, 29 Jun 2005)
Revision: 7500
Log message:

      more functions converted to 'connections in a set'
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 16:47:29 -0700 (Wed, 29 Jun 2005)
Revision: 7501
Log message:

      more position lists converted to sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 17:07:48 -0700 (Wed, 29 Jun 2005)
Revision: 7502
Log message:

      one more connection set
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 17:13:39 -0700 (Wed, 29 Jun 2005)
Revision: 7503
Log message:

      added a small comment
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 17:43:57 -0700 (Wed, 29 Jun 2005)
Revision: 7504
Log message:

      documenting one place where connection sets don't work (at least for now)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 17:45:22 -0700 (Wed, 29 Jun 2005)
Revision: 7505
Log message:

      more connection sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 18:06:54 -0700 (Wed, 29 Jun 2005)
Revision: 7506
Log message:

      more code treats connections as a set
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 18:21:15 -0700 (Wed, 29 Jun 2005)
Revision: 7507
Log message:

      more connection sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 18:37:48 -0700 (Wed, 29 Jun 2005)
Revision: 7508
Log message:

      beta expansions also behave like sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 19:17:18 -0700 (Wed, 29 Jun 2005)
Revision: 7509
Log message:

      one mor eplace where connection sets don't work
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 19:19:37 -0700 (Wed, 29 Jun 2005)
Revision: 7510
Log message:

      removed a function that is not used anymore
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 19:30:33 -0700 (Wed, 29 Jun 2005)
Revision: 7511
Log message:

      more lists replaced with sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 19:47:33 -0700 (Wed, 29 Jun 2005)
Revision: 7512
Log message:

      made one function tail-recursive
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 20:04:32 -0700 (Wed, 29 Jun 2005)
Revision: 7513
Log message:

      more lists converted to sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-29 20:16:54 -0700 (Wed, 29 Jun 2005)
Revision: 7514
Log message:

      one more list replaced with a set
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-30 15:52:34 -0700 (Thu, 30 Jun 2005)
Revision: 7515
Log message:

      more lists converted to sets
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-30 17:02:05 -0700 (Thu, 30 Jun 2005)
Revision: 7516
Log message:

      of_list -> of_sorted_list
      new of_list simply goes over the list and uses Set.add
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-30 18:01:31 -0700 (Thu, 30 Jun 2005)
Revision: 7517
Log message:

      Make use of range_fold
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-30 18:39:56 -0700 (Thu, 30 Jun 2005)
Revision: 7518
Log message:

      Slight update in how the documentation terms are handled.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-30 18:51:06 -0700 (Thu, 30 Jun 2005)
Revision: 7519
Log message:

      replaced one kind of lists with a map
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-06-30 19:29:24 -0700 (Thu, 30 Jun 2005)
Revision: 7520
Log message:

      another kind of lists converted to sets
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-06-30 22:31:30 -0700 (Thu, 30 Jun 2005)
Revision: 7521
Log message:

      Working on making the "doc" comments more uniform.