Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-03 23:29:05 -0800 (Wed, 03 Mar 2004)
Revision: 5425
Log message:

      Added "I am stuck where I should not be" error reporting to Naming and CPS.
      Untested for now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-08 01:24:45 -0800 (Mon, 08 Mar 2004)
Revision: 5431
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-08 02:20:15 -0800 (Mon, 08 Mar 2004)
Revision: 5432
Log message:

      Make sure a free variable does not get captured by a context.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-08 03:26:17 -0800 (Mon, 08 Mar 2004)
Revision: 5433
Log message:

      Allow repeating contexts in redeces (bug 165).
      This is a partial fix (does not allow for full alpha-renaming when comparing
      two context instances) and is not much tested.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-08 03:38:52 -0800 (Mon, 08 Mar 2004)
Revision: 5434
Log message:

      One of the optimizations I've added a few hours ago was not right - removing it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 11:42:48 -0800 (Mon, 08 Mar 2004)
Revision: 5435
Log message:

      Added an mcc_main.ml file as the outermost compiler.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 12:53:25 -0800 (Mon, 08 Mar 2004)
Revision: 5439
Log message:

      Updated caml-mode to handle quotations correctly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-08 23:33:01 -0800 (Mon, 08 Mar 2004)
Revision: 5440
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 01:14:43 -0800 (Tue, 09 Mar 2004)
Revision: 5441
Log message:

      Cleaned up the "extends" directives a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 05:23:47 -0800 (Tue, 09 Mar 2004)
Revision: 5443
Log message:

      Removing the distinction between the Hypothesis and HypBinding - it was
      causing too much trouble unnecessarily complicating a lot of code.
      
      The IO part of the distinction is still there - on IO the "unused" bindings
      are interpreted as variables with an empty "string" part.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 18:06:23 -0800 (Tue, 09 Mar 2004)
Revision: 5444
Log message:

      Bug 165: Added support for alpha-renaming/alpha-conversion when matching
      against redeces with two or more occurrences of the same sequent context.
      
      The support is a bit incomplete (a match might fail when the term does
      match - see the XXX BUG comment in rewrite_match_redex.ml), but I am hoping
      that it would not occur in real life scenarious.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 20:48:33 -0800 (Tue, 09 Mar 2004)
Revision: 5445
Log message:

      Do not be to quick to erase unused hypothesis bindings at parse time.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-10 23:45:58 -0800 (Wed, 10 Mar 2004)
Revision: 5448
Log message:

      - Bug 159: allow context arguments in rewrites (but not in ML rewrites).
      - Other minor updates in filter_parse and filter_prog code.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-03-11 20:16:33 -0800 (Thu, 11 Mar 2004)
Revision: 5450
Log message:

      Initial revision
      

Changes by: ( at unknown.email)
Date: 2004-03-11 20:16:33 -0800 (Thu, 11 Mar 2004)
Revision: 5451
Log message:

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

Changes by: ( at unknown.email)
Date: 2004-03-11 20:16:34 -0800 (Thu, 11 Mar 2004)
Revision: 5453
Log message:

      This commit was manufactured by cvs2svn to create tag 'start'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-13 12:42:21 -0800 (Sat, 13 Mar 2004)
Revision: 5455
Log message:

      Partial support for fully qualified resource names.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-13 13:19:13 -0800 (Sat, 13 Mar 2004)
Revision: 5456
Log message:

      Use proper formatting for Invalid_argument and Failure exceptions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-13 15:43:10 -0800 (Sat, 13 Mar 2004)
Revision: 5457
Log message:

      In cpsC, repeat at each node as many times as necessary before descending
      into subterms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-15 22:44:46 -0800 (Mon, 15 Mar 2004)
Revision: 5461
Log message:

      Adding support for patterns that match _free_ FO variables.
      
      With this commit, any free FO variable in a redex or contractum is taken
      to be a pattern that would match an arbitrary _free_ FO variable. This is
      probably not going to be useful in ITT-like domains, where variables usually
      stand for arbitrary terms (and therefore there is not much difference between
      free FO variables and SO variables), but in programming language domains this
      capability of being able to have patters matching the object-level variables
      should be extremely useful.
      
      On IO, the 'v would still expand into 'v[] _SO_ variable when v is free.
      Therefore, on IO the free _FO_ variables are denoted using the !v syntax.
      
      The new syntax and new rewriting capabilities are not yet used (except in
      the term table, which will now use !v matching) and are not very well tested
      yet.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-16 16:19:01 -0800 (Tue, 16 Mar 2004)
Revision: 5470
Log message:

      - Correcting the .ppo .SCANNER rule.
      
      - Added the -omake mode for the ocamdep - in the omake mode, the proper
      .cmiz dependencies are generated for the .ppo and .cmiz files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-17 15:15:25 -0800 (Wed, 17 Mar 2004)
Revision: 5472
Log message:

      In the -prl -omake mode, the ocamldep produces dependencies for both
      .cmiz and .cmi
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-17 21:37:42 -0800 (Wed, 17 Mar 2004)
Revision: 5477
Log message:

      !!! WARNING: With this commit, MetaPRL now requires omake >= 0.7.10 !!!
      
      - Updated the mpconfig to include all the Mojave extensions subdirectories
      - Fixed the "make clean" in the new theories/mojave/OMakefile
      

Changes by: ( at unknown.email)
Date: 2004-03-17 23:16:41 -0800 (Wed, 17 Mar 2004)
Revision: 5479
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-17 23:16:41 -0800 (Wed, 17 Mar 2004)
Revision: 5480
Log message:

      This is a first draft of the new implementation for the Term_match_table module.
      
      TODO:
      - Update all clients of the module to use the new interface (dforms are
      probably going to be the trickiest one).
      - Add the sequent matching to the new implementation (for now it does not
      handle sequents).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-18 02:24:19 -0800 (Thu, 18 Mar 2004)
Revision: 5482
Log message:

      Adding Cristian's theories/mojave/extensions/test
      

Changes by: ( at unknown.email)
Date: 2004-03-18 02:24:19 -0800 (Thu, 18 Mar 2004)
Revision: 5483
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-18 12:55:02 -0800 (Thu, 18 Mar 2004)
Revision: 5484
Log message:

      First pass at migrating the display forms to the new table code.
      
      I am planning to make display forms be a regular resource (one shared
      resource for all display modes - this should make it easier to add mode
      hierarchy later). This commit implements most of teh basic fuctionality,
      except for the resource itself.
      
      This commit also eliminates support for the unusd "internal" dform flag,
      w/o eliminating usages of the flag yet.
      
      !!! Does not compile. !!!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-18 13:59:59 -0800 (Thu, 18 Mar 2004)
Revision: 5485
Log message:

      Simplified the interface a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-19 02:08:07 -0800 (Fri, 19 Mar 2004)
Revision: 5488
Log message:

      A few minor changes:
      - Do not complain if the "internal" flag is used, just ignore it
      - Make sure the "raw" mode is not referenced directly.
      - Simplified mode handling a little.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-19 02:11:27 -0800 (Fri, 19 Mar 2004)
Revision: 5489
Log message:

      In the map case, use "term -> term list" rewriter maps instead of just
      "term -> term" ones.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-03-19 20:33:17 -0800 (Fri, 19 Mar 2004)
Revision: 5500
Log message:

      normalizeC: two complicated conversionals were split into individual slots of arith_unfold resource.
      Hopefully it will make it a little faster.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-19 23:23:30 -0800 (Fri, 19 Mar 2004)
Revision: 5501
Log message:

      - Finished implementing an Mp_resource-based dforms management mechanism.
      - Updated support/shell to use the new API.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-03-20 12:32:28 -0800 (Sat, 20 Mar 2004)
Revision: 5502
Log message:

      This should fix broken proofs.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-03-20 15:41:21 -0800 (Sat, 20 Mar 2004)
Revision: 5503
Log message:

      Slight speed improvement.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 13:45:50 -0800 (Sun, 21 Mar 2004)
Revision: 5507
Log message:

      Adding -I ../../theories/mojave/extensions/tuple.
      
      Please remember to update mpconfig when adding new directories!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 15:55:44 -0800 (Sun, 21 Mar 2004)
Revision: 5509
Log message:

      - Changed the dtactic module to use the new API
      (note: this changes the selT semantics slightly and adds full fall-back
      to both intro and elim).
      - Changed the compilers to use the new API.
      - Changed the get_bool_arg, get_sel_arg and get_int_arg to return an option
      instead of raising exception (since we always catch those exceptions anyway).
      
      MetaPRL finally compiles with the new API (but does not really run yet).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 17:56:22 -0800 (Sun, 21 Mar 2004)
Revision: 5510
Log message:

      First attempt at adding sequent matching to the table. Completely untested
      for now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 18:37:11 -0800 (Sun, 21 Mar 2004)
Revision: 5511
Log message:

      Fixed a few minot bugs. Things still appear to act very differently.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 19:47:57 -0800 (Sun, 21 Mar 2004)
Revision: 5512
Log message:

      The default value for the thinning arg is true, not false.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 21:37:12 -0800 (Sun, 21 Mar 2004)
Revision: 5513
Log message:

      Fixing the bytecode compilation problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 22:40:45 -0800 (Sun, 21 Mar 2004)
Revision: 5514
Log message:

      Fixed the sequent matching code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-22 01:24:01 -0800 (Mon, 22 Mar 2004)
Revision: 5515
Log message:

      Removing a redundant entry from autoT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-22 17:15:14 -0800 (Mon, 22 Mar 2004)
Revision: 5519
Log message:

      Added a few missing dependencies. This should finally fix bug 98.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-22 19:23:29 -0800 (Mon, 22 Mar 2004)
Revision: 5520
Log message:

      This is an initial commit of the x86_backend utilities.  This includes
      the printer, and the conversion to the abstract type used by the register
      allocator.  Still left: standardization and spill code generation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-22 23:09:29 -0800 (Mon, 22 Mar 2004)
Revision: 5521
Log message:

      Updated to do the symlinks correctly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 01:19:42 -0800 (Tue, 23 Mar 2004)
Revision: 5522
Log message:

      Changed the dT back from that "full fail-through" back ot only trying the
      items with the same pattern, and fixed all the cases of autoT looping.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 02:11:41 -0800 (Tue, 23 Mar 2004)
Revision: 5523
Log message:

      !!! WARNING : This commit breaks the .prlb compativility. !!!
      
      !!! This commit makes the "check_status" run about 1.5 times faster !!!
      
      This commit make a major change in how the Term_match_table is imlemented.
      Instead of the hash table at the top only (with linear lookup for subterms)
      this implementation uses the same functional term shape-indexed lookup tables
      at both the top and subterm level. During lookup, this implementation keeps
      an explicit list of "fallback" choices, which makes it easier to return more
      than one match. This implementation is much closer to the one presented
      in the paper submitted to TPHOLs.
      
      This makes a few changes to the semantics of the dT tactic:
      - Previously dT (both elim and intro) would only fall back to another tactic
      if it had the same _term_, now it will fall back to all that have the same
      _pattern_. For example, previously the entries for 'x='y in T, 'a in T and
      'b in T (for a specific T) were all considered separately and at most one
      would be tried, but now when applying the dT to a (t in T), all 3 could be
      tried.
      - Previously, if a pattern had both entires with select argument and entries
      without select argument, then the non-select entries were tried only when dT 0
      was called without the select argument. Now the non-select entries are always
      tried.
      
      This makes a change to the semantics of reduceC as well - now reduceC will try
      _all_ matches (from the most specific to the least specific), not just the most
      specific ones.
      
      The display forms are now handled as a resource, instead of being a "special"
      beast. This may cause the inheritance rules for display forms to change slightly,
      and a few extra "extend" directives might have to be added to compensate.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-23 16:56:32 -0800 (Tue, 23 Mar 2004)
Revision: 5529
Log message:

      All the parts are complete, now we just need to hook them together.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 17:26:48 -0800 (Tue, 23 Mar 2004)
Revision: 5531
Log message:

      Updated the sequent printout in "raw" mode.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-03-23 18:46:44 -0800 (Tue, 23 Mar 2004)
Revision: 5532
Log message:

      commit of all changes before major update
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 22:09:02 -0800 (Tue, 23 Mar 2004)
Revision: 5535
Log message:

      Fixing a few issues with how the theory hierarchy is managed
      by the Mp_resource. There still seem to be some issues left, though...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-24 00:07:50 -0800 (Wed, 24 Mar 2004)
Revision: 5536
Log message:

      Eliminated the last (hopefully) source of dups in the Mp_resource
      handling of the logical hierarchy.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 11:05:34 -0800 (Wed, 24 Mar 2004)
Revision: 5537
Log message:

      Proper code generation for Ext_int_test.test1.  To see the code, run
      the tactic (coreT thenT codegenT).
      
      Currently, standardization fails because it doesn't handle sequents.
      That's next.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 12:35:12 -0800 (Wed, 24 Mar 2004)
Revision: 5539
Log message:

      The standardize code now handles sequents too.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-24 18:15:28 -0800 (Wed, 24 Mar 2004)
Revision: 5543
Log message:

      1.  Fixed some bugs in bools and ints.
      2.  Cooked up a new Mandelbrot test case.  It uses cpp macros and I haven't
      .   worked out how to get omake to build it automatically, so for now I'm
      .   just committing the .ml and .mlp files.  I'll try to fix it...
      3.  Moved all tests to theories/mojave/test.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-24 18:28:10 -0800 (Wed, 24 Mar 2004)
Revision: 5545
Log message:

      Forgot to fix this for the new directory structure.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-24 19:18:11 -0800 (Wed, 24 Mar 2004)
Revision: 5546
Log message:

      Added support for sequents to the Phobos .pho grammar file parser.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 20:07:53 -0800 (Wed, 24 Mar 2004)
Revision: 5549
Log message:

      Register allocation seems to do something sensible on test2.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-03-24 20:25:28 -0800 (Wed, 24 Mar 2004)
Revision: 5550
Log message:

      First compilable version (with some workaround of bug175)
      It has inductive definitions without one very complicated case of
      positivity condition on terms.
      Case analysis and fixpoint is not implemented yet.
      And it's very ugly yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 20:28:22 -0800 (Wed, 24 Mar 2004)
Revision: 5551
Log message:

      Commit the .jyh script hack.  Someday we will enable standalone
      MetaPRL installations......
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-24 20:32:18 -0800 (Wed, 24 Mar 2004)
Revision: 5552
Log message:

      Updating the list of the implicit -prl mode dependencies.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-03-24 20:44:56 -0800 (Wed, 24 Mar 2004)
Revision: 5553
Log message:

      rules.ml split into
      
      cic_lambda - contains CC/lambda-Pw from Barendregt's cube
      cic_ind_type - contains intro-rules for inductive definitions
      
      I hope Makefile is correct.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-24 22:53:17 -0800 (Wed, 24 Mar 2004)
Revision: 5555
Log message:

      Created a partial Phobos grammar for the Mojave language (a number
      of extension is not fully supported) and converted some of the examples
      in ext_int_test to use Phobos quotations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 11:17:57 -0800 (Thu, 25 Mar 2004)
Revision: 5556
Log message:

      Yay, our first program (ext_int_test/test2) compiles, runs, and
      returns the right answer.  Ok, its only a start.
      
      Added the test/mcc script to run MetaPRL and assemble the output
      to produce an executable.  For example, in theories/mojave/test,
      run the following command.
      
         % ./mcc ext_int_test/test2
      
      This will generate an executable called test2.exe (sorry for the
      suffix, but we need CVS to ignore these files).
      
         % ./test2.exe
         Exit 9
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 19:31:12 -0800 (Thu, 25 Mar 2004)
Revision: 5560
Log message:

      The hoist phase now lifts out closed functions correctly.
      
      Added a new function Lm_symbol.new_name_gen that acts as
      a new name generator.  See Mcc_hoist for an example of use.
      Sorry about the massive recompile...
      
      Added editor/ml/mpshell for those of use who prefer keeping
      the xterm around.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-25 23:17:47 -0800 (Thu, 25 Mar 2004)
Revision: 5564
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-26 00:57:06 -0800 (Fri, 26 Mar 2004)
Revision: 5565
Log message:

      Changed the algorithms used for computing the Id hash value:
      
      - Made sure that all the signature items are hashed, not the first few.
      (Remember, on large data structures Hashtbl.hash only hashes the top!)
      
      - Changed it to also hash the _full_ (e.g. local and inherited) opname
      lookup table.
      
      This should have the desired effect of getting modules to be recompiled when
      their opname context changes via an indirect dependency _without_ making the
      dependencies fully recursive (which would have caused too many things
      to be recompiled on a non-opname .mli change).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-03-26 06:55:56 -0800 (Fri, 26 Mar 2004)
Revision: 5566
Log message:

      Interface of removed rules.ml should also be removed
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-26 18:44:40 -0800 (Fri, 26 Mar 2004)
Revision: 5568
Log message:

      Switched all of core_test and more of ext_int_test (including the
      factorial exaple) to the Phobos syntax.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-27 22:48:36 -0800 (Sat, 27 Mar 2004)
Revision: 5569
Log message:

      . Mainly a minor cleanup to make the code clearer.
      .     1. Added support for constant memory reservations.
      .        This is done informally, after the formal core operations.
      .     2. Added a few new stages to the backend for optimization,
      .        including register slop code, and dead instruction elimination
      .        (currently, this removes only Mov instructions).
      .
      . Note, Ext_int_test.test_fact is broken with the new parser...
      . I don't know why.  The original code is in Ext_int_test.test_fact_old.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-03-29 18:48:38 -0800 (Mon, 29 Mar 2004)
Revision: 5572
Log message:

      It's a first step towards resource-driven selection of hypotheses (and rules)
      that produce >=-inequalities used by the core of arithT.
      
      Current implementation is somewhatcomplicated I'll try to simplify it later.
      
      Rules that produce more than one main subgoal are not supported yet.
      (e.g. when conlusion was "not equal" it branches into two goals ">" and "<")
      I don't see an elegant solution for it yet.
      
      This commit might degrade overall performance but hopefully not too much.
      
      arith.ml - tiny optimization to avoid double-looping along edges
      from a node to itself.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 19:25:17 -0800 (Mon, 29 Mar 2004)
Revision: 5573
Log message:

      Regenerating the .prla hoping that it would "scare off" this particular
      instance of the Weak_memo bug (that seem to be occurring a lot on this file
      lately :-( ).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 21:50:09 -0800 (Mon, 29 Mar 2004)
Revision: 5574
Log message:

      Fixing the code that was supposed to complain if more then one rule/rewrite/etc
      had the same name in the same theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 22:05:01 -0800 (Mon, 29 Mar 2004)
Revision: 5575
Log message:

      Adding tail-call optimizations. This makes the asm.s file for the test_fact
      28 (out of 114) lines shorter. The optimizations are mostly added as
      untrusted (interactive) rewrites, but not yet fully proven.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 22:34:42 -0800 (Mon, 29 Mar 2004)
Revision: 5576
Log message:

      A number of display form updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 23:11:51 -0800 (Mon, 29 Mar 2004)
Revision: 5577
Log message:

      Further attempts to make display forms in the Mojave theory nicer.