Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-01 11:51:28 -0800 (Wed, 01 Feb 2006)
Revision: 8626
Log message:

      Addec cs136.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-02-02 14:57:30 -0800 (Thu, 02 Feb 2006)
Revision: 8627
Log message:

      Defined BTerms as the basic terms, instead of defining it based on languages.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-05 11:35:56 -0800 (Sun, 05 Feb 2006)
Revision: 8629
Log message:

      Preparing to move "append sequents" to obsolete status.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-05 11:54:18 -0800 (Sun, 05 Feb 2006)
Revision: 8630
Log message:

      Moved append/flat sequents into theories/itt/reflection/obsolete_flat
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-06 17:14:11 -0800 (Mon, 06 Feb 2006)
Revision: 8631
Log message:

      Itt_bool does not depend on Itt_set.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-06 23:20:24 -0800 (Mon, 06 Feb 2006)
Revision: 8632
Log message:

      Minor optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 00:00:50 -0800 (Tue, 07 Feb 2006)
Revision: 8633
Log message:

      Minor cleanup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 18:30:59 -0800 (Tue, 07 Feb 2006)
Revision: 8640
Log message:

      Made the script a bit more flexible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 19:25:53 -0800 (Tue, 07 Feb 2006)
Revision: 8642
Log message:

      Alexei & Aleksey:
      
      - Reformulated the dintersectionSubtype rule (it used to be incorrectly too
        strong) and derived it (it used to be a primitive axiom).
      
      - A little more progress reverifying ITT rules under pairwise functionality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 21:23:33 -0800 (Tue, 07 Feb 2006)
Revision: 8643
Log message:

      Alexei & Aleksey:
      
      - Switching ITT core from pointwise to pairwise functionality!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 00:56:20 -0800 (Wed, 08 Feb 2006)
Revision: 8644
Log message:

      - Fixed a rewriter bug uncovered by a recent change to let_rule rule.
      - Fixed proofs that were broken by a variable naming change in let_rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 02:05:45 -0800 (Wed, 08 Feb 2006)
Revision: 8645
Log message:

      *** Warning: breaks binary compatibility! ***
      
      Simplified and cleaned up the naming of bound variables when building
      contractum in the rewriter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 14:58:34 -0800 (Wed, 08 Feb 2006)
Revision: 8647
Log message:

      Removing an outdated comment.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 20:20:49 -0800 (Wed, 08 Feb 2006)
Revision: 8649
Log message:

      - Changed the filter to add a "Perv!select_crw" label to all the annotations
        on conditional rewrites.
      
      - Added simpleReduceC that calls reduceC while ignoring the conditional
        rewrites.
      
      TODO:
      - Add the "select_crw" label to manual reduce adds (where approproate)
      
      - Try adding simpleReduceT to autoT with a higher priority than the regular
        reduceT (possibly even to AutoNormal and not just AutoComplete)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 20:54:01 -0800 (Wed, 08 Feb 2006)
Revision: 8650
Log message:

      Minor variable naming fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 23:05:17 -0800 (Wed, 08 Feb 2006)
Revision: 8651
Log message:

      Small simplification of definitions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 02:34:57 -0800 (Thu, 09 Feb 2006)
Revision: 8652
Log message:

      Minor improvements in reduce resource for the number theory

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 14:32:05 -0800 (Thu, 09 Feb 2006)
Revision: 8653
Log message:

      The way we had <= and >= defined with reduceT "randomly" turning >= into <=
      was a complete mess! To avoid this mess, I have defined le and le_bool as
      _iforms_ that automatically turn into corresponding ge/ge_bool. Ideally, they
      should be some sort of "soft IO abstractions" so that terms that are entered
      as <= will be displayed as <= (while being idential to >= from the POV of the
      formal rewriter) - see bug 256 and bug 261.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 14:36:49 -0800 (Thu, 09 Feb 2006)
Revision: 8654
Log message:

      Fixed a proof broken by the previous commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 21:32:41 -0800 (Thu, 09 Feb 2006)
Revision: 8657
Log message:

      Proven much stronger elimination rules for Image and union types.
      
      Note: this does break a few proofs in Itt_hoas_* theories. I will fix those
      over the weekend (and try to clean up them a bit - now that we are using
      pairwise functionality they can be done _much_ simpler).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 23:16:10 -0800 (Thu, 09 Feb 2006)
Revision: 8658
Log message:

      - Implemented the splitNatT tactic that does case wplit (0 or not) for a
        natural number.
      
      - Added a missing item (the "not{m = n in nat}" hyp) to the appropriate
        arithT/omegaT resource (ge_elim).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-10 00:44:18 -0800 (Fri, 10 Feb 2006)
Revision: 8659
Log message:

      Derived the itt_list theory!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-10 01:04:26 -0800 (Fri, 10 Feb 2006)
Revision: 8660
Log message:

      Turns out that we do not really need the "weak reverse functionality" axiom
        list{'A} Type --> nil in list{'A} and it sufficient to have
        list{'A} --> nil in list{'A} in nthHypT.
      
      The latter form is actually derivable, so I was able to get rid of the only
      remaining prim rule in itt_list. Now itt_list is truly derived!
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-02-10 12:06:23 -0800 (Fri, 10 Feb 2006)
Revision: 8662
Log message:

      Added a missing comma in addsuffix, relevant to win32 only

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-02-10 12:10:10 -0800 (Fri, 10 Feb 2006)
Revision: 8663
Log message:

      Tiny typo

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 18:20:44 -0800 (Sun, 12 Feb 2006)
Revision: 8667
Log message:

      Working on .cmoz conversion.
      
      We discussed the following scheme for reflecting files:
      for an original (non-reflected) file foo.cmoz, we
      would generate a reflected file as foo_reflect.cmoz.
      
      However, the method has a problem, because the reflected
      theory includes ML code for resources.
      
      This is a pain.  Some options I see:
      
        1. Do not generate a separate file, but include the reflected
           code in the original foo.cmoz (with corresponding ML code in
           foo.cmo).
      
           Problem: it isn't modular, because you have to plan ahead
           for those files you want to reflect.  Also, you don't want the
           existence of theorems in the .cmoz to depend on how MetaPRL
           is configured.
      
           OTOH, if we _always_ generate reflected code, it is modular,
           with a cost.
      
        2. Provide tools:
      
              # Generates foo_reflect.cmi, foo_reflect.cmiz
              prlc --reflect foo_reflect foo.cmiz
      
              # Generates foo_reflect.cmo, foo_reflect.cmoz
              prlc --reflect foo_reflect foo.cmoz
      
           We would have to hack on omake:
              1. Make sure dependencies on _reflect files can be computed.
              2. Build the _reflect files automatically.
      
      I think option 2 is better _if_ it can be done.  The issue is that
      I'm not sure there is enough information in the .cm?z files to
      generate reflected theories.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 18:59:23 -0800 (Sun, 12 Feb 2006)
Revision: 8668
Log message:

      Fixed filter_bin--its been broken for a long time.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 19:15:43 -0800 (Sun, 12 Feb 2006)
Revision: 8669
Log message:

      Might as well fix the "convert" program too.
      This was the program that we could use externally
      to convert .prlb -> .prla.
      
      Not sure that it works, but we probably still
      want it.  It would be nice to be able to run
      "omake export" rather than trying to remember
      what files were changed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 20:13:33 -0800 (Sun, 12 Feb 2006)
Revision: 8670
Log message:

      Reverted revisions 8657, 8659, and 8660. These revisions have made the
      elimination rule for the image type stronger than what is valid under pairwise
      functionality and used those invalid rules to derive the itt_list theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 21:06:24 -0800 (Sun, 12 Feb 2006)
Revision: 8671
Log message:

      Weakened the nilEquality axiom, replacing the 
      "type"{list{'A}} --> nil in list{'A}
      (which is a bit too srtong semantically) with weaker theorems of the form
      list{'A} --> list{'A}
      
      This was first added un rev 8660, but then reverted in rev 8670.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 22:41:00 -0800 (Sun, 12 Feb 2006)
Revision: 8672
Log message:

      Boolean rules should be producing asserts instead of boolean equalities.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 23:32:03 -0800 (Sun, 12 Feb 2006)
Revision: 8673
Log message:

      Maked a conditional rewrite in reduce resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 01:02:22 -0800 (Mon, 13 Feb 2006)
Revision: 8674
Log message:

      Using Itt_pairwise, proved stronger elimination rules for the image type (for
      the "reversible" case only - where the "transitive closure" does not add any
      equalities to the image type).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:06:59 -0800 (Mon, 13 Feb 2006)
Revision: 8675
Log message:

      Derived itt_list from itt_union + itt_nat!
      
      This time it's using the weaker (pairwise-compatible) rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:44:17 -0800 (Mon, 13 Feb 2006)
Revision: 8676
Log message:

      "Strong" elimination rules (dprod, prod, disjoint union) should be formulated
      in thinning form; it should be up to the user and/or tactic to copy the hyp if
      it needs to be preserved (which is never the case in existing proofs).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:45:50 -0800 (Mon, 13 Feb 2006)
Revision: 8677
Log message:

      Getting rid of gt and gt_bool operators - turning them into iforms for lt and
      lt_bool.