Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-04 22:17:06 -0700 (Sat, 04 May 2002)
Revision: 3595
Log message:

      Redefined "inv_image" with "sep".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-04 22:17:52 -0700 (Sat, 04 May 2002)
Revision: 3596
Log message:

      Removed "setbvd_prop" which can be implemented with "sep".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-04 22:20:43 -0700 (Sat, 04 May 2002)
Revision: 3597
Log message:

      Replaced the use of "setbvd_prop" with "sep".
      Separated the definition of kernels from Czf_itt_hom, and created a new
      module Czf_itt_ker for kernels.
      

Changes by: ( at unknown.email)
Date: 2002-05-04 22:20:43 -0700 (Sat, 04 May 2002)
Revision: 3598
Log message:

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

Changes by: ( at unknown.email)
Date: 2002-05-04 22:20:43 -0700 (Sat, 04 May 2002)
Revision: 3599
Log message:

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-05 20:22:43 -0700 (Sun, 05 May 2002)
Revision: 3600
Log message:

      This is a branch commit that upgrades to ocaml3.04.
      
      Warning: on this branch, metaprl compiles only in byte-code.
      (See Aleksey notes below).
      
      The extra feature: there is now an apply_rewrite function
      in Top_conversionals.
      
         val : apply_rewrite : unit -> conv -> term -> term
      
      Note: always use an instance in this kind of form:
      
         let apply_rewrite = Top_conversionals.apply_rewrite ()
         - : conv -> term -> term
      
      This will (hopefully) capture all the resources at definition time.
      
      Brian: see if this works, and let me know if there are problems.
      Mp_mc_compile is updated...
      
      Aleksey:
      
         1. I don't remember exactly what you included in the upgrade to
            ocaml-3.04...  Please remind me about the features
            needed to be added to camlp4.  Also, can you try and make
            ocaml produce native code for camlp4?  We have the old problem
            with camlp4 not being configured to produce native code.
      
         2. I'm not sure about the new resource code.  To define the
            apply_rewrite function, we need to get ahold of the resources
            live at the src definition point.  I'm assuming that
            Mp_resource.extract_top () will do that--but I'm not sure.
            Question: what can we assume about Mp_resource.extract_top?
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-06 03:11:50 -0700 (Mon, 06 May 2002)
Revision: 3601
Log message:

      Changing some conscripts so that .cmxa targets are no longer
      hardcoded.  Improves the build markedly when started in MetaPRL,
      but theories/itt/itt_squash.ml then fails with
      
         FormatError:
         Filter_ocaml.dest_type : bad arity
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-07 07:53:09 -0700 (Tue, 07 May 2002)
Revision: 3602
Log message:

      Instead of a hard coded flag in the Conscript to determine
      whether or not to generate native or byte code, use
      the environment variable OCAMLRUNPARAM.  See the Conscript
      on how to set this variable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-07 08:02:50 -0700 (Tue, 07 May 2002)
Revision: 3603
Log message:

      Minor changes for 3.04.
      
      Jason, who is working on the filter not liking the .prla - you or me?
      I want to avoid the duplicated effort.
      
      I am getting close to having an RPM with working opt camlp4, will probably get there
      in a few hours.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-07 11:02:52 -0700 (Tue, 07 May 2002)
Revision: 3604
Log message:

      The .prla problem should be fixed.  MetaPRL compiles both
      with "make" and "cons".
      
      Filter_ocaml unmarshaling for str_items now fails softly.  If the
      term format changes, you may get a warning asking you to regenerate
      the .prla files.
      
      This compiles with Aleksey's new OCaml in native code.  Note,
      if you are using RH7.2, the RH7.3 RPM will not work.  You can
      either rpm --rebuild from the RPM source, or maybe Aleksey can
      generate an old version at some point.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-07 15:16:47 -0700 (Tue, 07 May 2002)
Revision: 3605
Log message:

      *** empty log message ***
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-07 15:17:49 -0700 (Tue, 07 May 2002)
Revision: 3606
Log message:

      Forgot to add these 2 files in the last commit.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-07 16:43:08 -0700 (Tue, 07 May 2002)
Revision: 3607
Log message:

      Removed the tactic equalSubsetT, since it is the same as setExtT defined
      in Czf_itt_member. Reproved related theorems.
      Also removed some comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-07 16:45:06 -0700 (Tue, 07 May 2002)
Revision: 3608
Log message:

      Minor change in comments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-08 13:31:36 -0700 (Wed, 08 May 2002)
Revision: 3609
Log message:

      - Changed the top_bookmark implementation to make it more explicit that
      it's always the same bookmark.
      
      - The apply_rewrite now expects a bookmark as its input (Brian, is that OK?)
      There are 3 ways of getting a bookmark:
      1) Use ("Theory", "rule") for a bookmark pointing right *before*
      a rule (rewrite) is defined.
      2) Use Mp_resource.theory_bookmark "Theory" for a bookmark
      pointing at the end of the theory
      3) Use let _ = Mp_resource.bookmark "foo" in a theory to create a bookmark and
      then refer to it as ("Theory", "foo")
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-08 15:45:05 -0700 (Wed, 08 May 2002)
Revision: 3610
Log message:

      Just testing my write access... Sorry.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-08 16:05:55 -0700 (Wed, 08 May 2002)
Revision: 3611
Log message:

      For the comment purposes.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-08 16:09:34 -0700 (Wed, 08 May 2002)
Revision: 3612
Log message:

      Separated preFIR term declarations.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-08 19:59:34 -0700 (Wed, 08 May 2002)
Revision: 3613
Log message:

      Okay, a few little changes here:
      1) Many references to the MC compiler have been
         changed to MCC (it's new name).  I'm still
         calling this theory MC.
      2) Adding new files to split FIR term definitions even further.
         The "prog" files will contain terms necessary to define
         the overal structure of an FIR program, e.g. function definitions.
      3) Updating Mp_mc_compile to use the updated apply_rewrite mechanism.
         The bookmarks seem to be working out okay.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-08 20:57:43 -0700 (Wed, 08 May 2002)
Revision: 3614
Log message:

      This should be a no-op commit. I've rearranged the code in filter_ocaml.ml
      to make it compile faster. This reduces the native code compilation time:
      this file - 1/3
      whole MetaPRL -  9%
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-08 21:09:52 -0700 (Wed, 08 May 2002)
Revision: 3615
Log message:

      Updating Makefile to reflect new files.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 14:08:38 -0700 (Thu, 09 May 2002)
Revision: 3616
Log message:

      -  Adding another program for testing purposes.
      -  MC_ROOT has been replaced by MCC_ROOT (in keeping with
         the name change of MC to MCC).
      -  Changing error reporting in mp_mc_connect_* to
         be more informative.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 16:10:31 -0700 (Thu, 09 May 2002)
Revision: 3617
Log message:

      Okay, this is somewhat major change for those of you using cons to build
      MetaPRL.
      
      If you want to build MetaPRL by itself, you should use make.  cons support for
      building MetaPRL by itself is being removed.
      
      The Conscripts now exist only to build MCC and MetaPRL together.  The procedure
      is that you download the MCC and MetaPRL sources, and then configure MCC
      appropriately (it has directions) for including MetaPRL in the build, and then
      run cons from the top level directory of MCC. Trying to run cons from
      anywhere within the MetaPRL sources should result in an error.
      
      This change allows for a few simplifications of the build system. In
      particular, these silly MP_ROOT and MCC_ROOT environment variables should no
      longer matter.  (They're a bit of a kludge and hack to begin with.)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 17:14:53 -0700 (Thu, 09 May 2002)
Revision: 3618
Log message:

      Fixing the Conscript so that it actually builds some files.
      (-:
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-09 18:58:07 -0700 (Thu, 09 May 2002)
Revision: 3619
Log message:

      Apply reduceC to term...
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 21:50:05 -0700 (Thu, 09 May 2002)
Revision: 3620
Log message:

      Working on adding the terms and conversion
      functions needed to represent entire
      MCC FIR programs.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-10 02:18:31 -0700 (Fri, 10 May 2002)
Revision: 3621
Log message:

      Changed the definition for cosets from set builder to separation.
      The previous definition was wrong.
      Updated proofs wherever coset occurred.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-11 01:38:00 -0700 (Sat, 11 May 2002)
Revision: 3622
Log message:

      Phobos returns a term and a list of (term*term) pairs that represent
      simple rewrites.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-11 03:57:52 -0700 (Sat, 11 May 2002)
Revision: 3623
Log message:

      Finished the comment part.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-11 11:28:23 -0700 (Sat, 11 May 2002)
Revision: 3624
Log message:

      Added "input forms" that are the input analogy to display forms.
      
      An iform is declared exactly like a rewrite.  An example:
      
         declare junk{'t}
         declare magic[v:s]{'t}
         iform bind : junk{magic[x:s]{'t}} <--> lambda{x. 't}
      
         # test_rewrite bind << junk{magic[y:s]{.'y +@ 1}} >>;;
         - lambda{y.y +@ 1} : term
      
      The difference is this: iforms use the rewriter in Relaxed mode,
      where capture is allowed.  The rewrites have no logical meaning;
      the refiner will not allow you to use one in a proof.  However,
      they are otherwise normal conversions, and you can add them
      to resources etc.
      
      Also, I added a function
      
      val Top_conversionals.create_iform : string -> term -> term -> conv
      
      This will allow us to create rewrites on the fly.  I added example
      code to mp_mc_compile to illustrate, but I don't know how to
      test it.
      
      Adam, you should probably change all rewrites in Mp_mc_fir_phobos to
      iforms.  Don't use magic (remove that sample code I added).  The rewrites
      should work as they are written now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-11 17:15:35 -0700 (Sat, 11 May 2002)
Revision: 3625
Log message:

      More structural changes to speed up compilation.
      
      Now "make opt" (after "make clean", but with .prlb already there) works even
      faster than it used to before 3.02 -> 3.04 switch.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-11 18:45:04 -0700 (Sat, 11 May 2002)
Revision: 3626
Log message:

      Print those rewrites that we get from Phobos. Just a copy of what I have
      before I leave, feel free to get rid of the changes.
       ----------------------------------------------------------------------
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-11 21:56:01 -0700 (Sat, 11 May 2002)
Revision: 3627
Log message:

      Adding some minimal display forms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-12 09:48:45 -0700 (Sun, 12 May 2002)
Revision: 3628
Log message:

      Merging the ocaml_3_04 branch.
      
      The major changes in this commit are:
      
      - Switch to OCaml+CamlP4 version 3.04
      - Many cons changes (in particular, cons now only supports mcc+MetaPRL,
      but does not support standalone MetaPRL).
      - Added partial support for "input forms" that are the input analogy to display forms.
      - Added apply_rewrite function.
      - Updated Mp_mc_compile to use the updated apply_rewrite mechanism.
      - Changed the top_bookmark implementation to make it more explicit that
      it's always the same bookmark.
      - Filter_ocaml unmarshaling for str_items now fails softly.  If the
      term format changes, you may get a warning asking you to regenerate
      the .prla files.
      - Filter_ocaml was significantly restructured to speed up the compilation.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 02:05:14 -0700 (Mon, 13 May 2002)
Revision: 3630
Log message:

      Corrected the functionality axioms for the operation and inverse.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 02:05:56 -0700 (Mon, 13 May 2002)
Revision: 3631
Log message:

      Updated the "pair_eq" rule to make it more powerful.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 02:07:16 -0700 (Mon, 13 May 2002)
Revision: 3632
Log message:

      Added an example of group: the klein 4-group.
      It looks pretty ugly now and needs comments.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-13 02:45:56 -0700 (Mon, 13 May 2002)
Revision: 3633
Log message:

      Cleaning up FIR evaluation / operational semantics.  The substantively new
      addition is that we can now evaluate matchExp's (match expressions).
      
      Adding a new conversional firExpEvalC (Mp_mc_fir_eval) which essentially
      evaluates any expression it can.  Essentially, this is firConstElimC, except
      this one works (at least on every example I've tried).  Again, since the MCC
      front ends do so much optimization, I don't know how well this works in
      general, but I do have evidence, based on the errors I had to fix during
      debugging, that it at least gets rid of a (pointless) idOp expression some
      where in MCC's mcc/test/fc/simple/fact.c.  (-:
      
      Granted, it can't evaluate much at the moment, but at least it's a start, and
      it should even be sufficient for the expressions in our power example.
      
      Take a look at theories/mc/tests/mp_mc_test.ml for some examples.
      
      Functions are still a problem at this point.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-13 09:23:26 -0700 (Mon, 13 May 2002)
Revision: 3634
Log message:

      Cleaning up idOp rewrites.  (I don't like how
      the previous set depended on which order you
      applied them in.)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-13 09:36:54 -0700 (Mon, 13 May 2002)
Revision: 3635
Log message:

      Adding a simple test case that demonstrates a problem
      with the setSubscript term (and implicitly, others
      that represent imperative updates of values).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 15:52:10 -0700 (Mon, 13 May 2002)
Revision: 3636
Log message:

      Added comments.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-14 17:32:40 -0700 (Tue, 14 May 2002)
Revision: 3640
Log message:

      Phobos iforms are finally working.
      This commit gets rid of all (iform-)rewrites that were in mp_mc_fir_phobos.ml,
      which were placed in fir.pho earlier.
      Turn on -metaprl_debug to see how the result is being manipulated.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-15 00:18:34 -0700 (Wed, 15 May 2002)
Revision: 3641
Log message:

      Minor comment modification in mp_mc_compile.
      
      I'm also committing two, real simple test cases in mp_mc_test.ml
      to convince myself the firDeadcodeC is working as expected.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-15 01:27:02 -0700 (Wed, 15 May 2002)
Revision: 3642
Log message:

      Removing the mp_mc_fir_phobos* files from
      mp_mc_theory and updating the Makefile
      so that they don't get built as part of a build
      using "make".  (mp_mc_fir_phobos become dependent
      upon MCC)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-15 23:13:15 -0700 (Wed, 15 May 2002)
Revision: 3643
Log message:

      Changing fundef term declaration.  In particular, the argument
      and body subterms have been reduced to one subterm that should
      be some sort of lambda term.  connect_prog code needs to be updated
      to handle this new term, but it does compile.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-15 23:21:53 -0700 (Wed, 15 May 2002)
Revision: 3644
Log message:

      Included Itt_list and Itt_list2 in Mp_mc_theory.
      Now, Phobos is passing a list of inline forms (as mp_pre_term list) as well.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-16 00:08:09 -0700 (Thu, 16 May 2002)
Revision: 3645
Log message:

      Committing part one of inlining.  This is most of the
      basic terms and rewrites that will be needed.
      
      Remaining: given a inline target (a tailCall term),
      I should generate a rewrite to deal with it.  The
      current scheme in this commit can deal with an
      inline target, but not in a general way.
      (Where by general, I mean a general tailCall term.
      General purpose inlining is ways away still.)
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-16 00:48:04 -0700 (Thu, 16 May 2002)
Revision: 3646
Log message:

      Defining groups does not really need equivalence relations, so I changed the group system by replacing equivalence relation with equality. Every occurance was modified and every related rule was reproved.
      
      Besides, separated the power operation for a group from the module Czf_itt_cyclic_subgroup.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-16 00:48:39 -0700 (Thu, 16 May 2002)
Revision: 3647
Log message:

      Forgot these in the last commit.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-16 00:54:07 -0700 (Thu, 16 May 2002)
Revision: 3648
Log message:

      Implementing the fundef conversion code correctly now.
      Preemptive bug fixes to mp_mc_inline.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-16 14:10:58 -0700 (Thu, 16 May 2002)
Revision: 3649
Log message:

      Committing the 2nd part of the inling code I've written.
      I'm not sure if it works since Phobos cannot properly generate
      string / token terms yet.  Other than that, the only other
      real piece of remaining work is to take the term injected
      through the Phobos path and get it back to MCC for further
      compilation.
      

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 16:12:45 -0700 (Thu, 16 May 2002)
Revision: 3650
Log message:

      Correcting hard-coded paths in the Conscript files which prevent successful
      compilation of MetaPRL for those of us with nonstandard ocaml installs. The
      paths are currently stored in the top-level Conscript in MCC, and are auto-
      detected by the configure script there.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-16 16:42:43 -0700 (Thu, 16 May 2002)
Revision: 3651
Log message:

      We also have 7.x RPMs.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-16 17:54:21 -0700 (Thu, 16 May 2002)
Revision: 3652
Log message:

      Allowed string->token and string->number parameter conversion in
      Relaxed mode. Feel free to correct it if I missed something.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-16 17:57:23 -0700 (Thu, 16 May 2002)
Revision: 3653
Log message:

      Changed tailCall to tailCall_com.
      

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 18:19:57 -0700 (Thu, 16 May 2002)
Revision: 3654
Log message:

      Removing hard-coded stuff from util/Conscript; this information is all
      available from the parent Conscript and computed by MCC's configure now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-16 18:42:37 -0700 (Thu, 16 May 2002)
Revision: 3655
Log message:

      Added itt_collection to theories.pdf
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-16 18:51:49 -0700 (Thu, 16 May 2002)
Revision: 3656
Log message:

      Forgot to update mp_mc_fir_phobos_exp.mli with the tailCall change.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-16 18:58:35 -0700 (Thu, 16 May 2002)
Revision: 3657
Log message:

      Change the grammar for terms a little bit.
      
      Now the grammar understands
      (1) Expression for records:
          - Record types:
              {x:A; y:B; ... z:C}
          - Records
              {x=a; y=b; ... z=c}
          - Field selections:
              r^x
            where x,y,z are words or strings, A,B,C,a,b,c,r are terms.
          Actually type {x_1:A_1;x_2:A_2;...x_n:A_n} is a depend typed record.
          It bounds the variable "self" inside terms A_2, ..., A_n. The type of
          self in A_k is {x_1:A_1, ..., x_k-1:A_k-1}. So, you can write, e.g.,
              {car : univ[l:l];
               "*" : 'self^car -> 'self^car -> 'self^car
              }
          This form a type that contains, for example,
              {car = int;
               "*" = lambda{x.lambda{y. 'x+@ 'y}}
              }
      
      (2) Syntax sugar for self.
          You may omit self, in the expressions like self^x.
          That is, you can write ^x instead of self^x.
          So, the following type is equivalent to the previous one.
              {car : univ[l:l];
               "*" : ^car -> ^car -> ^car
              }
      
      (3) Binary operations ^*, ^+, ^=, ^/, ^-, ^<, ^> ,^<>
             x ^* y  stands for  self^"*" x y
             x ^= y  stands for  self^"=" x y
          and so on.
          So you may write
          {car : univ[l:l];
           "*" : ^car -> ^car -> ^car;
           axm : all x,y,z : ^car. ('x ^* 'y) ^* 'z = 'x ^* ('y ^* 'z) in ^car
          }
      
      (4) Let and with operators.
          Now (let x=term1 in term2) and (term2 where x=term1) are both expression for
          the let{term1;x.term2} term defined now in itt_rfun.
      
      (5) Open operators.
              (open e1 in e2) stands for (let self=e1 in e2)
              (forany T. e) stands for (all self:T. e)
              (thereis T. e) stands for (exsts self:T. e)
          So you may write something like this
              open 'g in 'x ^* ^y ^* 'z
              forany group.  all 'x in ^car. 'x ^* ^e = 'x in ^car
      
      (6) Changed associativity and priority of some operators.
          Now the priority is the following (from the lowest priority):
              - operators like if-then-else and let
              - logical operators (in usual order)
              - relations (first =,in,~, then all other relations)
              - type and arithmetic operators in usual order
              - application
              - record field selection
          For example
              'x in 'y and 'z stands for ('x in 'y) and 'z
          but
              'x in 'y * 'z stands for 'x in ('y * 'z)
          I think this is natural.
      
      Corrected a couple of proofs that was broken.
      
      TODO:
        - make sure that display forms respect the new grammar.
      

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 21:25:38 -0700 (Thu, 16 May 2002)
Revision: 3658
Log message:

                                     ***WARNING***
      Building MCC with MetaPRL support will fail without the corresponding patch
      to MCC (just committed).  See the commit message for MCC for details.
                                     ***WARNING***
      
      Revising the build system to support the situation where $env->{MP} is a
      relative path.  A new variable, $env->{MP_HASH}, is the value of MP with a
      # prepended when MP is relative.  These changes are necessary to support
      a symlink pointing from MCC to the MetaPRL source tree.
      

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 22:44:41 -0700 (Thu, 16 May 2002)
Revision: 3659
Log message:

      Removing default targets from Conscript files.  Those of you on MCC,
      see the next MCC commit for how to get these back.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-17 10:36:48 -0700 (Fri, 17 May 2002)
Revision: 3660
Log message:

      Added a Boolean flag to create_iform to control the use of
      Strict or Relaxed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-17 16:39:09 -0700 (Fri, 17 May 2002)
Revision: 3661
Log message:

      Got rid of BackwardsCompatibleLevel params.
      

Changes by: ( at unknown.email)
Date: 2002-05-17 16:39:09 -0700 (Fri, 17 May 2002)
Revision: 3662
Log message:

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

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 17:18:33 -0700 (Fri, 17 May 2002)
Revision: 3663
Log message:

      Extend grammar.
      
      1. Now keywords "in" and "IN" are interchangeable.
      So you may write <<'a in 'T>> instead of <<'a IN 'T>>.
      
      2. You may write 'a='b and 'a<>'b for equal{'a;'b} and nequal{'a;'b}
      correspondingly in theories where such terms are defined.
      For example equal{'a;'b} is defined in czf_itt_eq.
      
      Question to Xin and Jason:
      The czf_itt_eq theory defines two terms for equality: eq and equal.
      Which of them do you think will be more usable?
      If eq is more usable, then it is probably better to define 'a='b as eq{'a;'b}.
      
      3. Added some CZF operators to the parser:
      
        'a In 'b
        all x In 'S. 'P['x]
        all x . 'P['x]
        exst x In 'S. 'P['x]
        exst x . 'P['x]
      
      Question (mainly to Xin and Jason): 'a In 'b is probably not the best shortcut for the set theory membership.
      Other possibilities are  sin, ins, in_s, mem, member.
      Do you have any preference?
      
      4. Now all variables may be words or strings. E.g. yo may write <<all "x^2".'P['"x^2"]>>.
      (Previously in some places variables might be strings, in other places they had to be words)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-17 18:10:45 -0700 (Fri, 17 May 2002)
Revision: 3664
Log message:

      - Removed the .prla files that didn't contain any actual proofs.
      - Refreshed some old .prla files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-17 19:33:37 -0700 (Fri, 17 May 2002)
Revision: 3665
Log message:

      Cleaned up the legacy stuff (Itt_equal!member, etc) somewhat.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 20:42:59 -0700 (Fri, 17 May 2002)
Revision: 3666
Log message:

      Updated userguide.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 20:53:19 -0700 (Fri, 17 May 2002)
Revision: 3667
Log message:

      Minor changes
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 21:36:09 -0700 (Fri, 17 May 2002)
Revision: 3668
Log message:

      Minor change
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-17 23:18:50 -0700 (Fri, 17 May 2002)
Revision: 3669
Log message:

      This is a lot of little changes.
      
      1) I've removed Mp_mc_term_op and folded it into
         the new Mp_mc_base module.  Accordingly, I've
         updated print.ml for the generation of documentation.
         Mp_mc_base contains the contents of Mp_mc_term_op'
         (term construction/deconstructon functions), as well
         as some convinience functions for debugging code.
         (These come in handy in debuggin MCC/MetaPRL interactions.)
         The Conscript and Makefile have also been updated,
         as well as any "open Module" statements.
      
      2) I'm updating the code that performs the inlining
         optimization.  It looks a bit nicer now.
         And it seems to work as expected.
      
      3) I'm updating Mp_mc_fir_phobos(_exp) to be a bit
         cleaner.  In particular, Mp_mc_fir_phobos_exp only
         declares those terms that we have to work
         with directly in MetaPRL, i.e. variable[v:s].
         The conversional to transform a preFIR to FIR term
         has been modified to remove variable[v:s] terms
         last.
      
      Just to emphasize, the inling example (it's in MCC)
      currently works.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-17 23:42:37 -0700 (Fri, 17 May 2002)
Revision: 3670
Log message:

      Now that I've corrected my one word typo in
      Mp_mc_compile, Mp_mc_fir_phobos_exp is completely
      unnecessary as the Phobos post processing rewrites
      take care of everything.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-18 00:13:45 -0700 (Sat, 18 May 2002)
Revision: 3671
Log message:

      My final set of code/comment clean-ups for the night.
      Nothing especially interesting here.  Just some
      comments, and a little code restructuring to a
      slightly more logical organization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-18 10:00:41 -0700 (Sat, 18 May 2002)
Revision: 3672
Log message:

      Docs: Fixed most undefined references.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-18 13:06:40 -0700 (Sat, 18 May 2002)
Revision: 3673
Log message:

      Forgot a @docoff directive.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-18 18:09:55 -0700 (Sat, 18 May 2002)
Revision: 3674
Log message:

      Do not execute inline code if there are no inline terms coming from Phobos.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-19 00:00:00 -0700 (Sun, 19 May 2002)
Revision: 3675
Log message:

      Changed one of the two associative axioms to a regular rule which can be proved from the other.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-19 00:21:32 -0700 (Sun, 19 May 2002)
Revision: 3676
Log message:

      The former definition for group builder was not consistent. Now group_bvd{h; g; s} also requires that subset{s; car{g}}. From it, it can be proven that id{h} = id{g} and inv{h; a} = inv{g; a} for all a in car{h}.
      Reproved all related rules and updated related comments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-19 19:52:26 -0700 (Sun, 19 May 2002)
Revision: 3677
Log message:

      Got rid of reflect_itt - it's pretty outdated
      and is probably not the best way of doing these things anyway...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-20 09:16:44 -0700 (Mon, 20 May 2002)
Revision: 3678
Log message:

      Cleaned up TPTP.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-20 09:42:24 -0700 (Mon, 20 May 2002)
Revision: 3679
Log message:

      Got rid of some legacy compatibility code that's no longer relevant.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-21 00:39:09 -0700 (Tue, 21 May 2002)
Revision: 3680
Log message:

      Adding operational semantics for eqEqOp.
      

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-22 10:45:49 -0700 (Wed, 22 May 2002)
Revision: 3681
Log message:

      Fixing numerous compiler warnings in clib.  Most of these have to do with
      the #pragma directives that were obsoleted; I checked with Jason and he said
      it was okay to remove them.  The rest are adding header files and function
      prototypes for missing symbols, and working around a few uninitialized var
      warnings.  This should not change the semantics of anything in clib.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-22 12:45:33 -0700 (Wed, 22 May 2002)
Revision: 3682
Log message:

      More clib clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-22 18:00:55 -0700 (Wed, 22 May 2002)
Revision: 3683
Log message:

      Changed the meta_lt and meta_eq implementation to be safer.
      Have not changed the meta_{sum,sub,...} etc.
      
      See the "Base_meta" thread in the newsgroup for more information.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-22 21:47:47 -0700 (Wed, 22 May 2002)
Revision: 3684
Log message:

      Updating the Conscript to reflect the removed register.c file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-23 19:51:06 -0700 (Thu, 23 May 2002)
Revision: 3689
Log message:

      Added to theories.pdf:
      - A title: "A Listing of MetaPRL Theories"
      - A list of authors:
      "Jason J. Hickey and Brian Aydemir and Yegor Bryukhov and Alexei Kopylov and Aleksey Nogin and Xin Yu"
      - A 4-line introduction explaining what this is.
      
      I want this to look reasonable enough to cite in a paper. BTW, it can now be addressed simple
      as http://metaprl.org/theories.pdf
      
      Any improvement suggestions?
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-23 21:04:43 -0700 (Thu, 23 May 2002)
Revision: 3690
Log message:

      Adding base_meta rewrites (only for +-*/) to be applied to all
      Phobos iforms. Now the paper example works.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-23 21:33:14 -0700 (Thu, 23 May 2002)
Revision: 3691
Log message:

      Updates to reflect the new MCC FIR.  I've just
      commented out problem code since I need to rethink
      slightly how I represent the FIR in MetaPRL and I don't
      want to spend time updating code that's about to change
      anyways.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 03:22:43 -0700 (Sun, 26 May 2002)
Revision: 3693
Log message:

      Changed the definition of the carrier in cyclic subgroups/groups from
      collection to separation. The reason for this is that we should always
      try to use set primitives rather than collections.
      Updated corresponding rules and proofs.
      Also made some minor changes in comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 03:27:42 -0700 (Sun, 26 May 2002)
Revision: 3694
Log message:

      More changes in the comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 19:47:00 -0700 (Sun, 26 May 2002)
Revision: 3695
Log message:

      Removed all occurences of "rwh unfold_group_bvd ..." in the proof.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-27 01:31:55 -0700 (Mon, 27 May 2002)
Revision: 3696
Log message:

      A bit easier-to-read output from Phobos activity.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-27 22:19:15 -0700 (Mon, 27 May 2002)
Revision: 3697
Log message:

      Changed the occurences of set_bvd to sep, since set_bvd is defined by collection.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-27 22:21:34 -0700 (Mon, 27 May 2002)
Revision: 3698
Log message:

      Rebuilt the prla file.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-27 23:55:07 -0700 (Mon, 27 May 2002)
Revision: 3699
Log message:

      Minor changes in comments.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-28 20:09:00 -0700 (Tue, 28 May 2002)
Revision: 3700
Log message:

      Added more functionality to interface with Phobos.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-29 04:26:11 -0700 (Wed, 29 May 2002)
Revision: 3701
Log message:

      Updated comments.
      Also fixed a small error in the well-formedness rule in Czf_itt_normal_subgroup
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-30 11:56:38 -0700 (Thu, 30 May 2002)
Revision: 3702
Log message:

      Return idC if no iforms are given.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-31 19:40:02 -0700 (Fri, 31 May 2002)
Revision: 3703
Log message:

      I forgot to remove register.mlz when removing register.c
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-31 21:39:06 -0700 (Fri, 31 May 2002)
Revision: 3704
Log message:

      Added edit_cd_list_contents for Lori.
      It's not perfect (it cd's into the module as a side-effect),
      but our top-loop code is very ugly anyway...