Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-02 21:12:57 -0800 (Fri, 02 Nov 2001)
Revision: 3433
Log message:

      - More const_elim rewrites.
      - Changed the type from ty(Raw)Int -> tyEnum{2} on
        the integer boolean comparison expressions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-11-03 07:15:53 -0800 (Sat, 03 Nov 2001)
Revision: 3434
Log message:

      Added mc directory.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-03 10:58:31 -0800 (Sat, 03 Nov 2001)
Revision: 3435
Log message:

      Everything compiles, but I've managed to break
      something in the last commit.  This commit doesn't
      fix anything, but I'm doing it before I start
      mucking around with a quite a few things.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-03 11:33:42 -0800 (Sat, 03 Nov 2001)
Revision: 3436
Log message:

      Fixed a build error with cons.
      (util needed to be built first.)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-03 12:12:33 -0800 (Sat, 03 Nov 2001)
Revision: 3437
Log message:

      When we replace a goal of a RuleBox, it seems a better idea to use
      Unjustified as a new rule_extract instead of just Goal - this way we
      preserve the original leaf information and only (re)expansion of a
      RuleBox may alter its list of leaves.
      
      Before this change leaf mismatches were producing "nasty" side-effects
      when people were attempting to work inside non-expanded proofs.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-04 02:28:15 -0800 (Sun, 04 Nov 2001)
Revision: 3438
Log message:

      - Added a Conscript
      - const_elim is much simpler now!
        The tactic for it is still a bit slow though.
      - Changed cmp(Raw)IntOp evaluation to reflect
        mc better.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-04 11:38:36 -0800 (Sun, 04 Nov 2001)
Revision: 3439
Log message:

      Changes to get the mc theory compiled in by default.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-04 18:36:58 -0800 (Sun, 04 Nov 2001)
Revision: 3440
Log message:

      cons files:
      - The mp_version.ml file is now created with a proper version string
      - The refiner used is now controlled  by the RFEINER and TERM variables
      specified in the top-level Conscript (but not yet taken from mk/config).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-14 14:20:25 -0800 (Wed, 14 Nov 2001)
Revision: 3441
Log message:

      removed the bugs and todo's that were already fixed.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-11-15 12:25:28 -0800 (Thu, 15 Nov 2001)
Revision: 3442
Log message:

      Itt_int_ext: more conversions added to reduce resource
      
      Itt_int_arih: first working version of arithT!!!
      You can observe proof of test rule and try to replace it with just arithT
      in the root.
      While now arithT knows only numbers, variables and +
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-11-15 12:33:33 -0800 (Thu, 15 Nov 2001)
Revision: 3443
Log message:

      Sorry, forgot to export proof
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-15 15:03:47 -0800 (Thu, 15 Nov 2001)
Revision: 3444
Log message:

      Code cleanup:
      
      I looked (using the code I've put into macro.ml) for places where the same code
      appeared in several branches of a match or function expression. I changed those
      places to use a complex pattern and a single copy of the code.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-16 21:17:28 -0800 (Fri, 16 Nov 2001)
Revision: 3445
Log message:

      - A little clean up for const_elim.
      - Term operations for fir_ty.
      - Don't use cons to build this theory.  I make no guarentees about
        cons correctly being able to navigate dependencies and namespace
        related conflicts, yet.
      - The Makefile now includes meta-prl/mc/fir/..., so make may not work
        either unless you have the Mojave compiler source tree set up appropriately.
      - In short, this code is in a state of flux.  I will get it to cleanly
        compile eventually.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-17 00:13:29 -0800 (Sat, 17 Nov 2001)
Revision: 3446
Log message:

      More term operations.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-18 19:42:48 -0800 (Sun, 18 Nov 2001)
Revision: 3447
Log message:

      - More term operations added.
      - mc_term_op_ds now contains some local functions for
        (de)constructing terms with 4+ subterms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-11-19 07:09:10 -0800 (Mon, 19 Nov 2001)
Revision: 3449
Log message:

      First working version with meta-prl/mc together.
      
      To compile with mc, as of Mon Nov 19 07:04:50 PST 2001:
         0. Get a copy of mc, available from mojave.cs.caltech.edu.
            If you don't know how, you can ask jyh@cs.caltech.edu.
         1. set the MC_ROOT environment variable to the root
            directory for mc.
         2. Compile using cons.  You chould compile from the root
            meta-prl directory first.  After that, you can build
            from the editor/ml directory (use cons -t).
      
      There are still some problems with dependencies in theories/tactic.
      prlc adds a lot of implicit dependencies, and I've only caught a few
      of them.  It compiles for now, but beware of "undefined modules" in
      editor/ml.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-19 12:39:56 -0800 (Mon, 19 Nov 2001)
Revision: 3450
Log message:

      Added some additional info to comments in JProver files.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-20 06:51:38 -0800 (Tue, 20 Nov 2001)
Revision: 3451
Log message:

      Even more term ops implemented.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-20 14:31:15 -0800 (Tue, 20 Nov 2001)
Revision: 3452
Log message:

      - More term operations. Everything in fir_ty and fir_exp should
        have term (de)construction operations now.
      - Started redoing the README file.
      - IMPORTANT: At this point, the default compile setup for the MC theory
        will depend on the source tree for the mojave compiler being present.
      - WARNING: For those using cons, the update of fir_marshal here breaks
        compilation of mp.opt due to a library conflict.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-20 17:45:18 -0800 (Tue, 20 Nov 2001)
Revision: 3453
Log message:

      make will now build the mc theory (and all of MetaPRL) w/o trouble now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-21 01:17:04 -0800 (Wed, 21 Nov 2001)
Revision: 3454
Log message:

      Updates to solve some build problems:
      
      make : Building with make is completely independent of the presence
         of the Mojave compiler source tree, since the MC compiler must
         be built with cons.  Thus, the only code that currently depends
         on MC, theories/mc/fir_marshal is not compiled.  Not including
         it as a part of the build of theories/mc is not a problem since it
         has no logical or otherwise meaningful content beyond the functions to
         convert between terms and the Fir.prog data structure of the compiler,
         i.e. this present no loss to the mc theory.
      
      cons : If the MC_ROOT environment variable is defined, its assumed to point
         to the root directory of the Mojave compiler source tree, and in this
         case, we build the two source trees together.  (To use MC, you need
         to define MC_ROOT anyway, so there's no need to put it as a config
         option somewhere.)  In particular, we (will) compile the
         "connection" code in theores/mc/fir_marshal.  If MC_ROOT is undefined,
         MetaPRL will build almost identically; the only difference is that
         fir_marshal is not compiled in.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-28 01:46:07 -0800 (Wed, 28 Nov 2001)
Revision: 3457
Log message:

      - Continuing implementation of code to convert from Fir.prog to MetaPRL terms,
        and vica versa.
      - Renamed some files to avoid conflicts.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-11-29 12:23:02 -0800 (Thu, 29 Nov 2001)
Revision: 3458
Log message:

      More "connection" code.  Most of the function are there,
      but some still need to be completely defined.