Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-01 13:27:30 -0700 (Sun, 01 Jul 2001)
Revision: 3305
Log message:

      Moved nthAssumT from Itt_struct to Itt_squash and made it do
      sequent squashing/unsquashing as needed to match the assumption.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-01 17:47:04 -0700 (Sun, 01 Jul 2001)
Revision: 3306
Log message:

      src mode dform fixes.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-02 15:34:20 -0700 (Mon, 02 Jul 2001)
Revision: 3307
Log message:

      - added rules applyEquality to intro resource
      
      - many rules (e.g. letT and elimination rules for the intersection and union types)
        produces equality hypotheses in the subgoals that rarely used in practice.
        Now such rules thin these hypotheses by default.
        To avoid this one can use doNotThinT = thinningT false.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-02 15:46:40 -0700 (Mon, 02 Jul 2001)
Revision: 3308
Log message:

      Fixed a minor bug.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-03 12:09:56 -0700 (Tue, 03 Jul 2001)
Revision: 3309
Log message:

      Fixed some proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-03 15:37:36 -0700 (Tue, 03 Jul 2001)
Revision: 3310
Log message:

      Better sequent matching code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-03 16:12:24 -0700 (Tue, 03 Jul 2001)
Revision: 3311
Log message:

      JProver shouldn't do "make_opname" all the time.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-03 16:55:20 -0700 (Tue, 03 Jul 2001)
Revision: 3312
Log message:

      - Now substitution (s1=s2 in S) for conclution (t in T[s1]) produces a wf subgoal
         s:S |- T[s] Type
      (instead of s:S |- (t in T[s]) Type which was annoying)
      
      - Now assertEqT is more powerful than it was.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-04 08:52:29 -0700 (Wed, 04 Jul 2001)
Revision: 3313
Log message:

      Made var_subst a little more general.
      This fixes another bug that was affecting JProver.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-04 11:08:37 -0700 (Wed, 04 Jul 2001)
Revision: 3314
Log message:

      Fixed the bug in match_terms that was causing the stack overflow errors
      in autoT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-05 14:15:43 -0700 (Thu, 05 Jul 2001)
Revision: 3315
Log message:

      I have changed the way autoT works.
      
      Now autoT and trivialT share the same auto_resource. When a new tactic is
      added to auto_resource, the auto_flag provides information on how to use the
      tactic:
      - AutoTrivial - use in trivialT; use in autoT before other tactics
      - AutoNormal - use in autoT after AutoTrivial tactics
      - AutoComplete - use in autoT after AutoTrivial and AutoNormal; use only
      if autoT can prove all the genarated subgoals.
      
      I added a few tactics to autoT with AutoComplete flag:
      - dT elimination rules (but only when dT will do the thinning)
      - JProver with multiplicity 1 (with some assumptions magic); use jAutoT i
      to get an autoT version that will run JProver with multiplicity i intead of 1.
      
      I added a flag AutoMustComplete to intro resource flags. This flag takes the
      rule to AutoComplete level instead of the usual AutoNormal.
      
      The new autoT no longer does backThruHypT and backThruAssumT (other than through
      JProver). I added a new tactic logicAutoT that will do backThruHypT
      and backThruAssumT in addition to normal autoT functionality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-05 18:20:52 -0700 (Thu, 05 Jul 2001)
Revision: 3316
Log message:

      - Added "'H; x: 'A; 'J['x] >- "type"{'A}" to autoT
      - Fixed a few itt_fset proofs.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-06 12:19:56 -0700 (Fri, 06 Jul 2001)
Revision: 3317
Log message:

      Fixed two proofs
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-06 13:02:02 -0700 (Fri, 06 Jul 2001)
Revision: 3318
Log message:

      - Fixed some bugs in Itt_w:
        (a) The rule ruduce_tree_eta was unsound (we could prove unconditional
            eta from it). Removed
        (b) The rule wElimination was also unsound. Fixed.
        (c) There old bug noticed by Carl 2 years ago survived in the rule
            tree_indEquality. I fixed this rule, make it more general,
            make it interacative instead of primitive and proved it.
      
      - Display forms for srec and prec types are fixed.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-06 14:48:58 -0700 (Fri, 06 Jul 2001)
Revision: 3319
Log message:

      - Changed intro rule for the set type according to Alexey's beter_itt.
      
      - Proved that sets can be defined as dependend intersection.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-06 16:33:15 -0700 (Fri, 06 Jul 2001)
Revision: 3320
Log message:

      Added elim_typeinf and intro_typeinf functions
      to make creating typeinf annotations easier.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-06 17:29:40 -0700 (Fri, 06 Jul 2001)
Revision: 3321
Log message:

      More itt_fset fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-08 09:12:09 -0700 (Sun, 08 Jul 2001)
Revision: 3322
Log message:

      Use String.concat instead of String_util.concat
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-09 10:33:39 -0700 (Mon, 09 Jul 2001)
Revision: 3323
Log message:

      Fix some proofs
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-09 13:57:19 -0700 (Mon, 09 Jul 2001)
Revision: 3324
Log message:

      Numerous display form updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-09 17:11:03 -0700 (Mon, 09 Jul 2001)
Revision: 3325
Log message:

      - Rewrote the Itt_esquash theory based on my "better_tt" ideas.
      - Now esquash is a primitive operator and not a defined one.
      - This change also broke a few FOL and CZF theories that relied
      on a bunch of invalid rules that I had to remove from Itt_esquash.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-11 08:23:32 -0700 (Wed, 11 Jul 2001)
Revision: 3326
Log message:

      - trivialT can now do equalRefT and equalSymT when necessary to match
      the conclusion with a hypothesis.
      - turned couple of Itt_equal rules from primitives into interactives
      - fixed a few FOL proofs
      - removed some obsolete files
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-11 16:14:27 -0700 (Wed, 11 Jul 2001)
Revision: 3327
Log message:

      Finished fixing cfol proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-11 16:58:51 -0700 (Wed, 11 Jul 2001)
Revision: 3328
Log message:

      FOL theory is now complete.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-13 14:34:19 -0700 (Fri, 13 Jul 2001)
Revision: 3329
Log message:

      I've removed old Itt_int* theories and switched all the ITT to Yegor's
      new theories.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-14 10:51:05 -0700 (Sat, 14 Jul 2001)
Revision: 3330
Log message:

      .
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-14 14:32:24 -0700 (Sat, 14 Jul 2001)
Revision: 3331
Log message:

      - The Itt_quotient theory is now a theory of _intensional_ quotient type
      (one can still get extensional one by esquash'ing the equality predicate).
      - Most of the Itt_quotient theory rules are now reversible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-14 22:17:00 -0700 (Sat, 14 Jul 2001)
Revision: 3333
Log message:

      When eliminating a quotient hyp, dT will now use a simplier rule
      (and use thinT ThinOption). quotientT may be used instead to get
      additional equality hyps (and no thinning).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-15 00:01:49 -0700 (Sun, 15 Jul 2001)
Revision: 3334
Log message:

      When a bound variable already exists in the goal, it should not be
      supplied in the rule argument to prevent it from being renamed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-15 02:14:11 -0700 (Sun, 15 Jul 2001)
Revision: 3335
Log message:

      Fixed more Itt_fset proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-16 11:43:31 -0700 (Mon, 16 Jul 2001)
Revision: 3336
Log message:

      More proof fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-16 20:04:06 -0700 (Mon, 16 Jul 2001)
Revision: 3339
Log message:

      - Improved proof replay.
      - Fset proof fixes.
      - Other minor fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-17 10:26:57 -0700 (Tue, 17 Jul 2001)
Revision: 3340
Log message:

      More itt_fset fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-18 17:44:40 -0700 (Wed, 18 Jul 2001)
Revision: 3341
Log message:

      Had to increase the bytecode stack size so that bytecode can handle large
      .prla files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-20 10:01:33 -0700 (Fri, 20 Jul 2001)
Revision: 3342
Log message:

      - Proved list cons-cons equality elimination.
      - More itt_fset proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-20 16:06:48 -0700 (Fri, 20 Jul 2001)
Revision: 3343
Log message:

      Itt_fset is finally complete!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-21 16:23:43 -0700 (Sat, 21 Jul 2001)
Revision: 3344
Log message:

      - created a tcaT tactic that is equivalent to tryT (completeT autoT)
      - created a filter macro "ttca" that is equivalent to
      "thenT tcaT"
      - moved memberTypeT from itt_collection to itt_struct
      - updated itt_quickref a little.
      - some cleanup in itt_fset and itt_collection
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-22 14:10:07 -0700 (Sun, 22 Jul 2001)
Revision: 3345
Log message:

      - Added a new tactic copyHypT for copying hypotheses (useful in elimination rules).
      - Simplified a few Itt_fset proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-22 20:46:49 -0700 (Sun, 22 Jul 2001)
Revision: 3346
Log message:

      Added subtypeT function:
      subtypeT <<A>> replaces a conclusion of the form <<t1 = t2 in B>> with
      <<t1 = t2 in A>> and conclusion of any other form <<B>> with just
      <<A>> and generates an "aux" subgoal of the form <<subtype{A;B}>>.
      

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

      I rewrote itt_collection using my "better_tt" ideas and proved all the
      theorems in that theory.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-25 20:42:20 -0700 (Wed, 25 Jul 2001)
Revision: 3348
Log message:

      I changed the rule subtypeElimination2 and proved use_subtype1.
      Now elimination rule for subtyping request one or two term parameters.
      With one parameter it works as usual, with two params 'a and 'b it produces
      a subgoal 'a='b in 'A.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-07-25 21:21:46 -0700 (Wed, 25 Jul 2001)
Revision: 3349
Log message:

      Initial import.  mc is the name of Jason's compiler project, and functional
      internal representation referrs to one of the stages in the compiler.  This
      theory will hopefully be a formalization of that representation in MetaPRL.
      
      The files right now are far from useful/complete.
      (fir_exp.ml is unduly messy since it reflects a talk I had with Jason today and
      so has lots of notes and ad hoc code.)  Hopefully, I'll also add some comments
      that will make the files a bit more readable to people who know nothing
      about the compiler.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-07-27 09:27:41 -0700 (Fri, 27 Jul 2001)
Revision: 3350
Log message:

      Initial import of the type system for the FIR.  Not everything is here yet.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-28 06:41:16 -0700 (Sat, 28 Jul 2001)
Revision: 3351
Log message:

      Updated the "Simplified Syntax" section of User Guide.