Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-07-05 17:47:08 -0700 (Mon, 05 Jul 2004)
Revision: 6036
Log message:

      Starting object implementation
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-07-07 14:59:28 -0700 (Wed, 07 Jul 2004)
Revision: 6037
Log message:

      Started implementing the basic computational aspects of reflection.
      This is the first step - if_bterm is implemented.
      
      (Alexei, Aleksey and Xin)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-07 21:39:25 -0700 (Wed, 07 Jul 2004)
Revision: 6038
Log message:

      The is_bterm rewrites can not be added to reduce directly, we need to wrap
      them in a simple rewriting tactic first.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-07 21:40:42 -0700 (Wed, 07 Jul 2004)
Revision: 6039
Log message:

      Minor clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-07 22:34:20 -0700 (Wed, 07 Jul 2004)
Revision: 6040
Log message:

      A few display form updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-07 22:49:29 -0700 (Wed, 07 Jul 2004)
Revision: 6041
Log message:

      Some more clean-up.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-07-08 00:25:35 -0700 (Thu, 08 Jul 2004)
Revision: 6042
Log message:

      Changed Apply so that the list of type arguments is a sequent.  For example:
      .   Apply{ 'f; 'args; sequent{ <H> >- }
      
      Note that there is no conclusion to the sequent.  This is one way of
      distinguishing type lists from other kinds of sequents.
      
      This change allows us to clear out a lot of ugly code, including the ListOfHyps
      hack and some really gnarly stuff for type checking Apply expressions.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-07-08 15:15:30 -0700 (Thu, 08 Jul 2004)
Revision: 6043
Log message:

      Added a caution about building MetaPRL with threads enabled.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-07-08 18:45:32 -0700 (Thu, 08 Jul 2004)
Revision: 6047
Log message:

      More on the theory of objects
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-07-08 19:16:59 -0700 (Thu, 08 Jul 2004)
Revision: 6048
Log message:

      Added a theory for testing reflection in itt. Fixed two bugs in base_reflection.ml.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-07-08 19:53:08 -0700 (Thu, 08 Jul 2004)
Revision: 6049
Log message:

      Aleksey Nogin wrote:
      
      > You defined the ITT's is_bterm to be a boolean. Wouldn't it be
      > better to define it as a prop (if_bterm{'bt; true})?
      > The thing is only well-formed when it is true, so it has
      > a certain "propositionality" to it. And this way, of course,
      >there will be no need to assert it all the time.
      
      I agree.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-07-09 11:41:34 -0700 (Fri, 09 Jul 2004)
Revision: 6050
Log message:

      Theory of Objects: Another example of recursive object
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-09 22:36:10 -0700 (Fri, 09 Jul 2004)
Revision: 6052
Log message:

      Added a "-batch" command-line option to MetaPRL that causes MetaPRL to be
      a bit quieter. "-batch" implies "-cli".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-10 00:07:43 -0700 (Sat, 10 Jul 2004)
Revision: 6053
Log message:

      - Made the tracking of "this operation modified some proof" flag more precise
      by having the low-level operations (e.g. edit_interpret) report whether something
      was modified as opposed to having the high-level operations guess what have happened.
      
      - Do not do auto-backups when "-batch" command-line flag is used (we do not want
      things like status-all and mmc compiler to do auto-backups).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-07-12 15:40:45 -0700 (Mon, 12 Jul 2004)
Revision: 6060
Log message:

      Added dest_bterm and make_bterm.
      
      Currently, for make_bterm, when n=0, consider it a 0-arity bterm.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-12 18:11:05 -0700 (Mon, 12 Jul 2004)
Revision: 6063
Log message:

      Added a Refiner.Refiner.Term.ops_eq function that should be used for testing
      equality of operators.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-12 23:16:27 -0700 (Mon, 12 Jul 2004)
Revision: 6064
Log message:

      Use dummy_loc instead of (0, 0)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-12 23:20:44 -0700 (Mon, 12 Jul 2004)
Revision: 6065
Log message:

      More "0, 0" -> "dummy_loc"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-12 23:23:41 -0700 (Mon, 12 Jul 2004)
Revision: 6066
Log message:

      Even more "0, 0" -> dummy_loc
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-12 23:28:13 -0700 (Mon, 12 Jul 2004)
Revision: 6067
Log message:

      Use MLast.loc instead of int * int
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-12 23:34:20 -0700 (Mon, 12 Jul 2004)
Revision: 6068
Log message:

      Some more "0, 0" -> dummy_loc
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-07-12 23:54:29 -0700 (Mon, 12 Jul 2004)
Revision: 6069
Log message:

      Added if_same_op, if_simple_bterm, if_var_bterm, and subst.
      
      Done with the base computation on bterms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-13 11:45:39 -0700 (Tue, 13 Jul 2004)
Revision: 6070
Log message:

      - Removed the "reduce" annotation that was preventing MetaPRL from starting.
      - Formatted the commen ts and code a bit more consistently.
      - In subst, the bterm that is being substituted must be simple (this is necessary
      because we may allow combining nested bterm operators).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-13 14:39:47 -0700 (Tue, 13 Jul 2004)
Revision: 6071
Log message:

      - Added support for resource annotations on ML rewrites.
      - Added a few more definitions to Itt_reflection_test.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-13 15:48:46 -0700 (Tue, 13 Jul 2004)
Revision: 6072
Log message:

      When "-batch" flag is used, do not save/restore seessions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 12:22:37 -0700 (Wed, 14 Jul 2004)
Revision: 6075
Log message:

      If OCAMLLIB is not set, use C:\ocaml\lib (since README.WIN32 suggests that
      this is the default). Thanks to Jirka Hana for reporting this.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 13:19:21 -0700 (Wed, 14 Jul 2004)
Revision: 6076
Log message:

      In preparation for 3.06 -> 3,08 switch, I am calling this MetaPRL version 0.9.6.1
      

Changes by: ( at unknown.email)
Date: 2004-07-14 13:19:21 -0700 (Wed, 14 Jul 2004)
Revision: 6077
Log message:

      This commit was manufactured by cvs2svn to create tag
      'metaprl-0_9_6_1'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-14 13:42:43 -0700 (Wed, 14 Jul 2004)
Revision: 6078
Log message:

      Omake-generated config file.
      
      Question: is there some reason to name variables BLAH_DEFAULT in
      mk/default?
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-14 13:44:38 -0700 (Wed, 14 Jul 2004)
Revision: 6079
Log message:

      Ignore .lib files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 13:57:53 -0700 (Wed, 14 Jul 2004)
Revision: 6080
Log message:

      Added a paragraph on having to edit mk/config.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 14:27:10 -0700 (Wed, 14 Jul 2004)
Revision: 6081
Log message:

      ***************************************************************************
      * WARNING: With this commit MetaPRL now requires OCaml 3.08 and OMake 0.8 *
      ***************************************************************************
      
      This commit:
      - Updates MetaPRL to be compatible with OCaml 3.08 (some of the code for
      handling the new "position" type is still half-baked, waiting for the
      resolution of bug 256.
      - Moves the "C:\ocaml\lib" default into mk/defaults.
      - Removes references to mk/make_config.sh from mk/make_config
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-14 14:49:02 -0700 (Wed, 14 Jul 2004)
Revision: 6082
Log message:

      Re-implemented prlcomp in mk/prlcomp.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 14:56:58 -0700 (Wed, 14 Jul 2004)
Revision: 6083
Log message:

      On Unix, environment variables need to be escaped with signle quotes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-14 18:39:21 -0700 (Wed, 14 Jul 2004)
Revision: 6084
Log message:

      Empty change.
      MetaPRL now compiles with OCaml 3.08.0 on Win32.
      Strangely enough, OCaml works out of the box.  No
      need to copy the 6 extra files...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 19:07:52 -0700 (Wed, 14 Jul 2004)
Revision: 6086
Log message:

      Added dependencies on camlp4 (actually - camlp4o and camlp4r) and
      ocamlmktop versions. This should complete the bug 47 requirements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 19:52:16 -0700 (Wed, 14 Jul 2004)
Revision: 6088
Log message:

      "There were errors." is not a very good error message, should at least
      include the origin in the error message.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 20:04:33 -0700 (Wed, 14 Jul 2004)
Revision: 6090
Log message:

      Print a message when mk/config is updated.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 21:01:49 -0700 (Wed, 14 Jul 2004)
Revision: 6091
Log message:

      - Got rid of the annoying _DEFAULT suffix.
      - On Windows, do not include the ignored variables (NCURSES, etc) in mk/config
      - Try turning the booleans in mk/config to canonical true/false values.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-14 21:25:35 -0700 (Wed, 14 Jul 2004)
Revision: 6092
Log message:

      Variable names fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-15 14:24:46 -0700 (Thu, 15 Jul 2004)
Revision: 6093
Log message:

      Updated for 3.08
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-15 16:16:15 -0700 (Thu, 15 Jul 2004)
Revision: 6094
Log message:

      Use the right commands for .p4i and .p4
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-07-15 16:46:01 -0700 (Thu, 15 Jul 2004)
Revision: 6095
Log message:

      Updated to reflect 3.08.0 upgrade.  Hooray!  No more patching!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-15 17:12:38 -0700 (Thu, 15 Jul 2004)
Revision: 6096
Log message:

      Simplified the term grammar a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-15 20:34:36 -0700 (Thu, 15 Jul 2004)
Revision: 6097
Log message:

      - Cleaned up the handling of bterms in term grammar. The annoying cases
      where one had to put a "." at a beginnig of a subterm are now ***gone***!
      
      - Updated most of the files in theories/itt (and a few outside of the itt)
      removing periods from these places since they now can be omited.
      
      - Updated the BUGS file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-15 21:04:47 -0700 (Thu, 15 Jul 2004)
Revision: 6098
Log message:

      - Added an input shortcut for sequents with a unary sequent_arg. Now instead
      of typing
        sequent [t]{ ... }
      one can type
        t{| ... |}
      (where t can be an arbitrary term).
      
      - Switched base_reflection to using the new syntax for bterm sequents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-15 21:22:18 -0700 (Thu, 15 Jul 2004)
Revision: 6099
Log message:

      Use "-batch" instead of "-cli" when printing theories to .tex
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-16 12:04:14 -0700 (Fri, 16 Jul 2004)
Revision: 6100
Log message:

      - Added a work-around for Camlp4 bugs handling new-style positions
      (filed OCaml PR#2953 and PR#2954).
      
      - Fixed the problem that we were forgetting to advance by 6 (length of
      "<:doc<") when converting locations within a comment into locations
      within the file.
      
      - Fixed the problem with Comment_parse module giving a wrong location
      of the quotations (it was giving the location of the closing ">>" instead
      of the location of the whole thing).
      
      - Allow subterms to be quotations, not just "top-level" terms.
      
      - At parsing, before discarding the "aname" field of "aterms" (potentially
      named terms), make sure the aname was None. (This uncovered a typo
      in itt_rbtree.ml).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-16 12:45:34 -0700 (Fri, 16 Jul 2004)
Revision: 6101
Log message:

      Get MMC to compile on Win32.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-20 19:42:34 -0700 (Tue, 20 Jul 2004)
Revision: 6103
Log message:

      Added links to new mailing lists.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-21 13:03:52 -0700 (Wed, 21 Jul 2004)
Revision: 6104
Log message:

      Some formatting changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-21 16:32:02 -0700 (Wed, 21 Jul 2004)
Revision: 6105
Log message:

      Need Omake 0.8.1 (which provides the "echo" macro).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-21 20:38:32 -0700 (Wed, 21 Jul 2004)
Revision: 6106
Log message:

      Override the -native flag for OCAMLDEPFLAGS
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-07-26 13:04:22 -0700 (Mon, 26 Jul 2004)
Revision: 6107
Log message:

      Removed all -I suffixes from INCLUDES
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-07-28 14:12:53 -0700 (Wed, 28 Jul 2004)
Revision: 6108
Log message:

      Fixed a couple of problems that occured probably due to Jason's
      search and replace of -I
      
      There is still one problem with MP_DIRS
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-07-28 14:21:53 -0700 (Wed, 28 Jul 2004)
Revision: 6109
Log message:

      Fixed the MP_DIRS problem.
      Added a split call on MP_DIRS where the array OCAMLINCLUDES
      was created (editor/ml/OMakefile)
      
      OCAMLINCLUDES[] +=
              $(ROOT)/$(ENSEMBLE_DIR)
              $(split ' ',$(MP_DIRS))
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2004-07-30 10:22:09 -0700 (Fri, 30 Jul 2004)
Revision: 6111
Log message:

      Making a note that the ranlib issue has been fixed in OCaml CVS.