Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-01 02:23:09 -0800 (Fri, 01 Apr 2005)
Revision: 7078
Log message:

      '$0" is a literal string $0; to protect from spaces one needs to use double
      quotes: "$0".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-02 14:17:01 -0800 (Sat, 02 Apr 2005)
Revision: 7084
Log message:

      Use Lm_symbol.compare instead of Pervasives.compare where appropriate.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-02 14:32:53 -0800 (Sat, 02 Apr 2005)
Revision: 7085
Log message:

      Got rid of .mlz in mllib and refiner directories.
      Note: you will have to run "cvs update" twice!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-02 15:00:43 -0800 (Sat, 02 Apr 2005)
Revision: 7086
Log message:

      Removed an unused module.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-02 18:14:15 -0800 (Sat, 02 Apr 2005)
Revision: 7088
Log message:

      Added a line to term_base_ds to avoid the capture problem in bug #432.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-02 20:29:05 -0800 (Sat, 02 Apr 2005)
Revision: 7090
Log message:

      Added string lexing as a primitive to Filter_grammar.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-02 20:54:07 -0800 (Sat, 02 Apr 2005)
Revision: 7092
Log message:

      This augments the basic term type, adding support for the "shape" parameters.
      
      Syntax:
       - write "operator[op:sh]" for the shape meta-parameter "op"
       - write "opetator[('t1 't2)]" or opetator[('t1 't2):sh] for a concrete shape
         "apply[]{0; 0}"
      
      TODO:
       - Add support for display forms (add slot[s:sh]; make sure that in the "src"
         mode shapes are printed in a parseable way)
       - Convert the reflection theory to using the shape parameters in operators.
      
      WARNING: This breaks backwards compatibility for binary files. Export your
      proofs before updating.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-02 21:14:50 -0800 (Sat, 02 Apr 2005)
Revision: 7093
Log message:

      Incomplete support for strings in the backend.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-02 22:00:48 -0800 (Sat, 02 Apr 2005)
Revision: 7094
Log message:

      Made term_std's standardize function closer to term_ds's one.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 15:14:04 -0700 (Sun, 03 Apr 2005)
Revision: 7096
Log message:

      Added explicit iform category for terms.  The syntax is:
      
         declare iform <term_declaration>
      
      and the usual variants.  For the others, the iform keyword goes last
      for now.
      
         declare type iform ...
      
      "iform" terms are not allowed after input processing, so this is the
      way to make sure your helper terms do not appear in any logical
      context.
      
      There were only a few rules in mmc that broke.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 15:36:02 -0700 (Sun, 03 Apr 2005)
Revision: 7097
Log message:

      Ignore quoted terms during checking.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-03 17:33:15 -0700 (Sun, 03 Apr 2005)
Revision: 7098
Log message:

      WARNING: Jason's earlier commit broke binary compatibility; this one makes it
      explicit. Export your proofs before updating.
      
      - Updated the filter_magic to account for Jason's changes
      - Marked the parts of filter_summary that are only there for compatibility
        with pre-change PRLA files.
      - The ShapeIForm items are not formal and are display items (when interpreting
        the ls flags).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-03 18:11:18 -0700 (Sun, 03 Apr 2005)
Revision: 7100
Log message:

      In ITT, annotated the iform opnames with "declare iform"
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 18:24:25 -0700 (Sun, 03 Apr 2005)
Revision: 7101
Log message:

      In iform checking, handle quoted shapes by stripping the quotes.
      
      Splitting inliner into multiple parts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-03 18:39:43 -0700 (Sun, 03 Apr 2005)
Revision: 7102
Log message:

      Updated display forms for the "declare" directives to match the current term
      encoding of those directives.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-03 18:45:41 -0700 (Sun, 03 Apr 2005)
Revision: 7103
Log message:

      Updated refiner_debug.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 19:29:56 -0700 (Sun, 03 Apr 2005)
Revision: 7105
Log message:

      Removed the $ignore check in input term checking.  I had forgotten
      that the check is not being used on declarations.
      
      It brings up another issue: input checking is not being
      used on terms that are being declared (because the term doesn't
      exist yet).  However, it is probably a good idea to do input
      checking on all the subterms.
      
      The other place where the input checker is bypassed is for
      iforms, and in the !!!WARNING!!! section of Term_grammar.  We
      should probably add checking where appropriate.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-03 21:22:38 -0700 (Sun, 03 Apr 2005)
Revision: 7108
Log message:

      "define iform" will now correctly create an iform, not a rewrite.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 23:51:39 -0700 (Sun, 03 Apr 2005)
Revision: 7114
Log message:

      Added a little better error messages to the unifier.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 23:57:04 -0700 (Sun, 03 Apr 2005)
Revision: 7115
Log message:

      Minor cleanups.  Aleksey found the problem with type inference, we
      better fix this.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-04-04 17:39:22 -0700 (Mon, 04 Apr 2005)
Revision: 7123
Log message:

      Changed the way to interpreting op_bdepth and variablesin Itt_reflection_new.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-04-04 17:40:50 -0700 (Mon, 04 Apr 2005)
Revision: 7124
Log message:

      Changed comments with "fake_mlrw".
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-04-04 17:46:15 -0700 (Mon, 04 Apr 2005)
Revision: 7125
Log message:

      Fixed a definition of beta_redex
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 17:48:15 -0700 (Mon, 04 Apr 2005)
Revision: 7126
Log message:

      - When displaying slot["raw","s"], the string "s" _must_ really be displayed
        as is (no String.escape or other wrappers) in order for LaTeX and HTML
        output to work correctly.
      
      - Commented out the lucida fonts in LaTeX output header files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 19:51:23 -0700 (Mon, 04 Apr 2005)
Revision: 7127
Log message:

      Simplified the rlist code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 20:05:41 -0700 (Mon, 04 Apr 2005)
Revision: 7128
Log message:

      More precise meta-typing for the qouted terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 20:35:53 -0700 (Mon, 04 Apr 2005)
Revision: 7129
Log message:

      Rudimentary support for displaying shapes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 22:29:02 -0700 (Mon, 04 Apr 2005)
Revision: 7130
Log message:

      In table-based tactics and conversions, call the get_resource_arg once in the
      high-level tactic/conversion (e.g. reduceC) instead of every time the
      low-level tactic/conversion (e.g. reduceTopC) is called from the high-level
      one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 23:16:39 -0700 (Mon, 04 Apr 2005)
Revision: 7132
Log message:

      Killed a leftover MLZFILES definition.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 23:21:54 -0700 (Mon, 04 Apr 2005)
Revision: 7133
Log message:

      Updated the "You need OMake" error message.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 23:45:28 -0700 (Mon, 04 Apr 2005)
Revision: 7134
Log message:

      With TERMS=std, we were getting an "illegal subterm Perv!concl{...}" error
      message (because of the Term_man_gen encoding for sequents using the internal
      operators for encoding sequents). I added a hack that skips the "internal"
      sequent subterms when iterating/mapping over terms (those should not be
      getting exposed anyway).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-05 11:46:46 -0700 (Tue, 05 Apr 2005)
Revision: 7140
Log message:

      This is the bare template for pmc, which is completely empty right
      now, but at least it compiles:)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-05 12:30:28 -0700 (Tue, 05 Apr 2005)
Revision: 7142
Log message:

      Move the config to the compiler-specific directories.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-05 13:47:23 -0700 (Tue, 05 Apr 2005)
Revision: 7147
Log message:

      Remove mmc configuration.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-06 15:32:19 -0700 (Wed, 06 Apr 2005)
Revision: 7160
Log message:

      Added meta_eq[sh, sh]
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-07 12:31:20 -0700 (Thu, 07 Apr 2005)
Revision: 7164
Log message:

      In messages that say that a config file was created/updated, give the full
      path to the config file (relative to $(ROOT)) instead of just "mk/config"
      every time.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-08 18:49:04 -0700 (Fri, 08 Apr 2005)
Revision: 7182
Log message:

      Letting the paper cook for a while.
      
      Reverted the spill_split rule to its previous correct version.
      The basic problem is that var_subst seems to be substituting
      for values that it shouldn't.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-08 20:59:04 -0700 (Fri, 08 Apr 2005)
Revision: 7183
Log message:

      replaced applHLeft with prodApp (which is a combination of prodH and application)
      there's still a bug issue with forAll1T1DT and last premise of Dep
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-09 11:29:07 -0700 (Sat, 09 Apr 2005)
Revision: 7186
Log message:

      I think, I fixed the Dep rule by switching from generic ForAll1T1DT to a
      more custom ForAll1TConstr (which I also had to define).
      No it's time to try and see if it works the way it is intended to.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-10 14:38:55 -0700 (Sun, 10 Apr 2005)
Revision: 7193
Log message:

      As far as I understand, type_subst v t TypeExists(v', ...) was not handling
      v=v' correctly.
      
      - Jason should double-check this!
      - This did not fix the problem I was having with ty_exists :-(
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-10 18:49:58 -0700 (Sun, 10 Apr 2005)
Revision: 7196
Log message:

      Commiting some experimental proofs before bringing up-to-date local metaprl tree.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-11 00:15:53 -0700 (Mon, 11 Apr 2005)
Revision: 7199
Log message:

      Allow intro resource annotations of the form
      
      rule foo {| intro [...] |} 'H :
         ...
         sequent { <H>; x : T; <J['x]> >- C['x] }
      
      where C['x] is _not_ a second-order variable.
      
      This adds an "onSomeHypT foo" for the pattern C['x] to the intro resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-11 17:39:37 -0700 (Mon, 11 Apr 2005)
Revision: 7206
Log message:

      A better "precedence not found" error message.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-12 00:06:45 -0700 (Tue, 12 Apr 2005)
Revision: 7208
Log message:

      Print an error message when trying to compile a MetaPRL file that has a .ml,
      but no .mli.
      
      (Nathan and I have spent quite some time figuring out while one of his files
      was not being compiled properly :-( ).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-15 01:39:11 -0700 (Fri, 15 Apr 2005)
Revision: 7221
Log message:

      Created a typeclass MTerm for meta-terms and changed the
      Summary!meta_operators to have the MTerm type instead of Dform.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-19 01:48:56 -0700 (Tue, 19 Apr 2005)
Revision: 7222
Log message:

      Added slot["esc", s:s] and slot["cesc", s:s] display forms for printing the
      OCaml-escaped and C-escaped variants of the string s. Updated the display
      forms in the string extension of MMC to use the "esc" slots for string
      constants.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-19 12:21:05 -0700 (Tue, 19 Apr 2005)
Revision: 7223
Log message:

      Updated Filter_grammar to match the Lm_lexer change from omake.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-19 14:50:03 -0700 (Tue, 19 Apr 2005)
Revision: 7224
Log message:

      Oops, I was confused.  MetaPRL requires the newest version of Lm_lexer,
      but it doesn't really care whether omake is using it too.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-21 13:25:10 -0700 (Thu, 21 Apr 2005)
Revision: 7225
Log message:

      The magic numbers are now compatible across omake versions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-21 14:27:46 -0700 (Thu, 21 Apr 2005)
Revision: 7226
Log message:

      Added a blank line.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-26 19:15:50 -0700 (Tue, 26 Apr 2005)
Revision: 7230
Log message:

      Rename the "string" extension to "str", to avoid confusion with
      the "string" function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-27 16:59:37 -0700 (Wed, 27 Apr 2005)
Revision: 7231
Log message:

      Reverting the magic number to the Unix one.
      Adding *.out, *.fls to .cvsignore.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-27 19:22:22 -0700 (Wed, 27 Apr 2005)
Revision: 7232
Log message:

      Some fixes and improvements in cic_ind_elim*
      Removed bind-parameters where they are not needed anymore,
      added intro-annotation in several places
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-27 22:19:47 -0700 (Wed, 27 Apr 2005)
Revision: 7233
Log message:

      More fixes, still incomplete
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-27 22:58:43 -0700 (Wed, 27 Apr 2005)
Revision: 7234
Log message:

      Added a comment
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-28 14:28:15 -0700 (Thu, 28 Apr 2005)
Revision: 7235
Log message:

      Added to the exceptions chapter.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-28 21:09:33 -0700 (Thu, 28 Apr 2005)
Revision: 7236
Log message:

      Old proofs are up-to-date now.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-30 16:52:35 -0700 (Sat, 30 Apr 2005)
Revision: 7237
Log message:

      Working on outstanding issues for Win32.
      
      This is a fix to be more careful about spaces in filenames,
      so that placing ocaml in
      
         C:\Program Files\Objective Caml
      
      actually works.  This adds the $(quote-argv ...) function that
      quotes an array in a way that the command-line parser can recover
      the argv string.  This allows include directories with spaces in
      a -pp option.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-30 18:42:24 -0700 (Sat, 30 Apr 2005)
Revision: 7238
Log message:

      It's almost working. We have two problems:
      1. can't apply elimCaseTypeDep_inductive for some reason
      2. ala Mojave display forms for sequents
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-04-30 18:55:34 -0700 (Sat, 30 Apr 2005)
Revision: 7239
Log message:

      Forgot proofs