Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-01 11:34:14 -0700 (Wed, 01 Sep 2004)
Revision: 6154
Log message:

      More updates to the book.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-01 13:28:56 -0700 (Wed, 01 Sep 2004)
Revision: 6156
Log message:

      More changes to the book.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-01 20:36:38 -0700 (Wed, 01 Sep 2004)
Revision: 6157
Log message:

      Remove *.omc on "omake clean" (bug 291).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 03:20:58 -0700 (Thu, 02 Sep 2004)
Revision: 6158
Log message:

      Some code in proof_edit relied on left-to-right order of evaluation of
      tuple components. Turns out that the order is actually right-to left (at
      least in this particular case), so I had to rewrite the code making the
      evaluation order more explicit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 03:39:19 -0700 (Thu, 02 Sep 2004)
Revision: 6159
Log message:

      Added a work-around for bug 175. Hopefully, once we start using extracts
      somewhere other that ITT (CIC, may be?), we would get more insight and
      finally figure out what's the right "truly general" way of specifying extraction
      is.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-09-02 11:06:31 -0700 (Thu, 02 Sep 2004)
Revision: 6160
Log message:

      Added Natalia's and mine paper (TPHOLs 2004, cat B).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-02 12:56:43 -0700 (Thu, 02 Sep 2004)
Revision: 6161
Log message:

      This is an initial start at an alternate form of parsing.
      See theories/mmc/test/mmc_grammar.ml for an example.
      This version is resource-based, but I've reached an issue.
      
      If parsing is resource-based, then it has to be delayed until
      runtime.  That isn't so bad, and it has the advantage of being
      able to use runtime values like precedences and conversions.
      
      However, the filter still has to participate a little, by handling
      special quotations.  Something like:
      
         <:parse< text >> --> Base_parser.parse "text"
      
      This doesn't really work--we need the resource that contains the grammar.
      
         <:parse< text >> --> Base_parser.parse (get_parser_resource ???) "text"
      
      The problem is the ???.
      It could be:
      
         let mark = gensym () in
            Mp_resource.set_bookmark mark;
            get_parser_resource (Mp_resource.find mark)
      
      However, it is obvious that Mp_resource was not designed for
      this kind of interaction.
      
      So, we either fix Mp_resource, or push this all back into the filter.
      
      I don't really like the latter option because we add another resource-like
      thing that the filter has to manage; we have to design a new syntax for it;
      filter_prog.ml gets even larger; and we have to marshal PDAs and such.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 17:27:55 -0700 (Thu, 02 Sep 2004)
Revision: 6162
Log message:

      Moving Jason's parser commit to the "new_parser" branch.
      

Changes by: ( at unknown.email)
Date: 2004-09-02 17:27:55 -0700 (Thu, 02 Sep 2004)
Revision: 6163
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 17:36:24 -0700 (Thu, 02 Sep 2004)
Revision: 6164
Log message:

      Re-adding Jason's filter changes to the branch
      (without the base_parser and mmc_grammar files).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 19:18:48 -0700 (Thu, 02 Sep 2004)
Revision: 6165
Log message:

      (Bug 294) Do not insist on building the proxyedit binary in native code.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-09-02 19:18:51 -0700 (Thu, 02 Sep 2004)
Revision: 6166
Log message:

      BYTECODE_ENABLED -> BYTE_ENABLED
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 19:43:00 -0700 (Thu, 02 Sep 2004)
Revision: 6167
Log message:

      Fixing typo in a comment.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-02 19:55:48 -0700 (Thu, 02 Sep 2004)
Revision: 6168
Log message:

      filter/base/filter_grammar.ml is the file that does most of the work
      with parsing and lexing.
      
      Added the initial lexer part.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-03 09:39:24 -0700 (Fri, 03 Sep 2004)
Revision: 6169
Log message:

      This completes the base parser.  Next thing is to hook it into the filter.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-03 13:52:09 -0700 (Fri, 03 Sep 2004)
Revision: 6170
Log message:

      Added the grammar to Filter_cache_fun.  Still no hooks to
      camlp4.  Needs a little more work in Lm_parser to take
      the union of two parsers, but that part is nearly done.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-03 19:03:57 -0700 (Fri, 03 Sep 2004)
Revision: 6171
Log message:

      Include the full search path in the "Failed to find the specified format of"
      error message.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-04 13:19:06 -0700 (Sat, 04 Sep 2004)
Revision: 6172
Log message:

      Added hooks in Filter_cache_fun for calling the grammar functions.
      Implemented precedence union in Lm_grammar.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-04 14:40:28 -0700 (Sat, 04 Sep 2004)
Revision: 6174
Log message:

      Added the hooks in Filter_parse for the grammar.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-04 16:05:44 -0700 (Sat, 04 Sep 2004)
Revision: 6175
Log message:

      Initial grammar.  See theories/mmc/test/mmc_grammar.ml for an example.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-05 10:00:08 -0700 (Sun, 05 Sep 2004)
Revision: 6176
Log message:

      Parser now rewrites in Relaxed mode so we can do capture and all that.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-05 20:30:52 -0700 (Sun, 05 Sep 2004)
Revision: 6178
Log message:

      Added the grammar for MMC.
      
      This is in Mmc_core_ast, Mmc_ext_boolean, Mmc_ext_integer.
      
      We have 3 shift/reduce conflicts in the core grammar.  Somehow I'm
      having trouble turning on the debug flags, MP_DEBUG=parsegen doesn't
      seem to work, so I'll leave these conflicts for later.
      
      Also, defining grammars in the .mli file is a little awkward.
      Perhaps necessary, but I'm not sure.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-06 15:21:43 -0700 (Mon, 06 Sep 2004)
Revision: 6179
Log message:

      Added a patch for 3.08.1 to make it work with MetaPRL.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-06 16:03:31 -0700 (Mon, 06 Sep 2004)
Revision: 6180
Log message:

      Added MMC grammar.  Added post-processing based on iforms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-06 16:33:53 -0700 (Mon, 06 Sep 2004)
Revision: 6182
Log message:

      Added quotation expansion to the toploop.
      Everything seems to work as expected; this branch is done.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-06 20:04:53 -0700 (Mon, 06 Sep 2004)
Revision: 6183
Log message:

      Added the magic number generator.  If you are concerned that your
      data structure might be Marshaled, delimit the type definitions
      as follows:
      
         (* %%MAGICBEGIN%% *)
         type foo = ...
         ...
         (* %%MAGICEND%% *)
      
      We actually don't need to worry much about marshaling the grammar.
      Things marshaled are: a) lexer, b) parser, c) rewrites, d) terms,
      e) sets, f) tables.
      
      However, when one of these data structures changes, it will usually
      force the theory files to be recompiled anyway.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-08 09:56:32 -0700 (Wed, 08 Sep 2004)
Revision: 6184
Log message:

      More mods to the book.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-09-09 20:17:24 -0700 (Thu, 09 Sep 2004)
Revision: 6185
Log message:

      Removed reference to MS Visual C Toolkit because it does not include MASM :(
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-10 13:26:04 -0700 (Fri, 10 Sep 2004)
Revision: 6187
Log message:

      Migrated the grammars into the .cm?z files.
      Not quite finished, because grammar unions don't appear as
      separate grammars.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-10 17:03:27 -0700 (Fri, 10 Sep 2004)
Revision: 6188
Log message:

      Actually, it all works as expected, but parser generation
      is a bit slow.  I'm tuning it,
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-09-11 18:32:42 -0700 (Sat, 11 Sep 2004)
Revision: 6189
Log message:

      The new LALR changes look good.
      
      Grammar compilation is now about 25 times faster than it
      used to be.  There is still room for improvement,
      especially in the widespread use of Pervasives.compare,
      which is being used in the comparison of production sets,
      which are essentially shape list sets.
      
      However, we are in the sub-second range for the grammars
      that we have, and this is just a compile-time cost.  Still
      we want to keep compile times down.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-09-16 16:23:24 -0700 (Thu, 16 Sep 2004)
Revision: 6200
Log message:

      Eliminated the massive over-indentation on uncaught exceptions in the toploop.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-19 23:05:14 -0700 (Sun, 19 Sep 2004)
Revision: 6201
Log message:

      Turned out we never checked arity (and context bindings!) of sequent contexts ---
      should be fixed now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-21 16:33:48 -0700 (Tue, 21 Sep 2004)
Revision: 6202
Log message:

      Added a "submit" button.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-09-21 16:41:15 -0700 (Tue, 21 Sep 2004)
Revision: 6203
Log message:

      Fix files broken after switch to Lm_format.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-09-21 16:48:33 -0700 (Tue, 21 Sep 2004)
Revision: 6204
Log message:

      Better error reporting on refine errors during rewrite application.  Use
          set_debug "refine" true;;
      to see the benefits.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-24 16:50:09 -0700 (Fri, 24 Sep 2004)
Revision: 6206
Log message:

      Make sure the new genmagic stuff is properly cleaned up on "omake clean".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-24 17:13:42 -0700 (Fri, 24 Sep 2004)
Revision: 6208
Log message:

      - Remove references to .cmig/.cmog since they are no longer used.
      - Backport the "omake clean" .omc fix from the trunk.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-24 17:38:14 -0700 (Fri, 24 Sep 2004)
Revision: 6209
Log message:

      Adding a few comments on the things we've discussed on the way back from ICFP.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-29 16:09:12 -0700 (Wed, 29 Sep 2004)
Revision: 6210
Log message:

      Use the -batch flag.