Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-01 13:57:31 -0700 (Fri, 01 Jun 2001)
Revision: 3246
Log message:

      - The theory ctt_markov (Constructive type theory with Markov
        Principle) is added.
      
      - Some definitions and simple facts are added to itt_int_ext
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-01 14:36:46 -0700 (Fri, 01 Jun 2001)
Revision: 3247
Log message:

      *** empty log message ***
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-04 14:34:41 -0700 (Mon, 04 Jun 2001)
Revision: 3250
Log message:

      The function that was supposed to remove duplicate subgoals at the end of
      each rulebox application was not doing anything - fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-04 18:59:26 -0700 (Mon, 04 Jun 2001)
Revision: 3251
Log message:

      Updated Itt_squash documentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-05 15:41:19 -0700 (Tue, 05 Jun 2001)
Revision: 3252
Log message:

      Fixed squash_resource annotations for empty types.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-06 17:45:23 -0700 (Wed, 06 Jun 2001)
Revision: 3253
Log message:

      Some proofs in ctt_markov are simplified.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-07 12:14:04 -0700 (Thu, 07 Jun 2001)
Revision: 3254
Log message:

      - For symbolic keywords, use tt instead of bf
      - Use tt for non-math < and > to make sure that are displayed properly.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-08 12:24:25 -0700 (Fri, 08 Jun 2001)
Revision: 3255
Log message:

      moveToConlT is fixed
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-13 12:32:30 -0700 (Wed, 13 Jun 2001)
Revision: 3257
Log message:

      1. I added new primitive rules:
           Itt_struct.exchange
           Itt_pointwise.hypSubstPointwise
           Itt_pointwise.contextSubstPointwise
      
         The last two rules show the differences between pointwise and pairwise functionality.
         They are valid in pointwise functionality (as well as quoationtElimination2).
      
      2. Itt_struct3 contains some rules that derived from these new ones.
         But thesd rules are valid in both functionalities.
      
      3. I moved definition of natural numbers to a new theory Itt_nat.
         To prove induction for natural numbers one needs Itt_struct3.
         I almost proved it (leaving some simple arithmetic subgoals, that should
         be killed by arith)
      
      4. I defined record type.
         Itt_record is a main theory of records.
         Itt_record_exm contains some examples.
      
      5. I add a new conversion
              * applyAllC : conv list -> conv
         that applies all conversions to all subterms and a tactic
              * rwa : conv list -> int -> tactic
              = rw (applyAllC convs)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-13 13:25:12 -0700 (Wed, 13 Jun 2001)
Revision: 3258
Log message:

      Prevent make from thinking there is a circular dependency.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-13 13:27:06 -0700 (Wed, 13 Jun 2001)
Revision: 3259
Log message:

      I am adding the current version of the resource problem and a description
      of a proposed solution to CVS.
      
      Left to do: write module 5; update parsing description to show how it
      would use the new functionality.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2001-06-13 14:39:18 -0700 (Wed, 13 Jun 2001)
Revision: 3260
Log message:

      fixed representation of level expression for mathbus
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-13 14:48:05 -0700 (Wed, 13 Jun 2001)
Revision: 3261
Log message:

      More specific details in Modules 2 and 3. Still need to finish 4 and write 5.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-14 13:46:42 -0700 (Thu, 14 Jun 2001)
Revision: 3262
Log message:

      
      - More record theorems are proved
      
      - I restored eta-reduction rule, which is valid (with correct mechanism
        for conditional rewrites)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-14 14:48:03 -0700 (Thu, 14 Jun 2001)
Revision: 3263
Log message:

      Fixed Module 1, added lazyness wish (Problem 2.2).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-14 15:31:17 -0700 (Thu, 14 Jun 2001)
Revision: 3264
Log message:

      I finished describing the code I propose; still need to specify the
      parser changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-14 17:32:00 -0700 (Thu, 14 Jun 2001)
Revision: 3265
Log message:

      Finished the parsing part.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-14 18:03:18 -0700 (Thu, 14 Jun 2001)
Revision: 3266
Log message:

      Start writing documentation for records.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-15 13:35:54 -0700 (Fri, 15 Jun 2001)
Revision: 3267
Log message:

      expand_all() should go to next item on any exception, not just
      RefineError.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-15 16:16:03 -0700 (Fri, 15 Jun 2001)
Revision: 3268
Log message:

      Implemented object status inquiry:
       status ();;
         -- tells the status of the current object
       status_all ();;
         -- re-runs all proofs in the current node and tells their status
         -- from root - same for all the proofs in MetaPRL
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-15 16:36:41 -0700 (Fri, 15 Jun 2001)
Revision: 3269
Log message:

      SOrt packages.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-16 11:04:02 -0700 (Sat, 16 Jun 2001)
Revision: 3270
Log message:

      Fixed a few proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-17 03:55:32 -0700 (Sun, 17 Jun 2001)
Revision: 3271
Log message:

      - A little better code for subgoal matching during proof expansion.
      - Better output for some non-Refiner exceptions during proof expansion.
      - Some FOL theories had both .prla and .prlb in CVS, fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-17 07:10:39 -0700 (Sun, 17 Jun 2001)
Revision: 3272
Log message:

      Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but
      can also do thinning. I added it to trivialT, so now trivialT and autoT can
      do thinning when matching the goal against assumptions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-17 08:54:07 -0700 (Sun, 17 Jun 2001)
Revision: 3273
Log message:

      ASCII IO improvements for the case of a manually edited prla file containing
      repeated entries.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-17 14:41:29 -0700 (Sun, 17 Jun 2001)
Revision: 3274
Log message:

      - Added tacticals whileProgressMT and untilFailMT
      
      - Implemented dependend records
      
      - Change a rule for depended intersection
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-18 14:59:30 -0700 (Mon, 18 Jun 2001)
Revision: 3275
Log message:

      - Added the Itt_inv_typing theory that contain some inverse typing rule
      - More on records
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-19 08:17:10 -0700 (Tue, 19 Jun 2001)
Revision: 3276
Log message:

      Added support for the following syntax of resource improvement:
      let resource name += expr
      and
      let resource name += [ expr1; expr2; ...; exprn ]
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-19 17:12:25 -0700 (Tue, 19 Jun 2001)
Revision: 3277
Log message:

      - New tacticals
          onAllAssumT : (int -> tactic) -> tactic
          onAllMAssumT : (int -> tactic) -> tactic
        apply a tactic to all assumtions
      
       rwAll applies a convertion to all clauses
       rwcAll applies a convertion to all clauses for the given assumption
       rwAllAll applies a convertion to all assumption and to the goal sequent
      
       rwhAll,rwchAll,rwhAllAll, rwaAll,rwcaAll,rwaAllAll work by analogy
      
       Now these tactics does not work properly (see BUGS 3.12-3.14)
      
      - Most of the theorems on records are proved
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-19 17:27:36 -0700 (Tue, 19 Jun 2001)
Revision: 3278
Log message:

      - Changed the syntax of resource implementation. Now you no longer need to
      re-declare resource types in the implementation. Instead of the declaration
      and a Mp_resource.create call, use the following syntax in the implementation:
      
      let resource <name> = <expr>
      
      where <expr> is an expression that of the type Mp_resource.info
      
      - Additionally, it is no longer necessary to use _resource in resource names
      and resource annotations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-20 04:48:09 -0700 (Wed, 20 Jun 2001)
Revision: 3279
Log message:

      - Renamed andthenC -> thenC
      - Added byDefT : conv -> tactic
      - Proved rewrites in Itt_dprod
      - Removed some unused stuff from one of the filter_prog interfaces.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-20 06:40:29 -0700 (Wed, 20 Jun 2001)
Revision: 3280
Log message:

      Use byDefT in a few places.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-20 06:56:53 -0700 (Wed, 20 Jun 2001)
Revision: 3281
Log message:

      The redundant "_resource" suffix should not be used in resource names.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-20 11:41:55 -0700 (Wed, 20 Jun 2001)
Revision: 3282
Log message:

      New tactics ans cnversionals are documented.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-20 12:21:25 -0700 (Wed, 20 Jun 2001)
Revision: 3283
Log message:

      Fix an error
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-20 13:23:09 -0700 (Wed, 20 Jun 2001)
Revision: 3284
Log message:

      Got rid of annoying extra set (or 'arg) type argument in table functors.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-20 16:04:03 -0700 (Wed, 20 Jun 2001)
Revision: 3285
Log message:

      Resource annotations fix, thanks to Alexei K. for noticing this.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-21 10:00:19 -0700 (Thu, 21 Jun 2001)
Revision: 3286
Log message:

      Simplified some Camlp4 code.
      <:expr< $uid:"Aa"$ . $lid:"bb"$ >> is equivalent to just <:expr< Aa.bb >>, etc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-22 15:26:33 -0700 (Fri, 22 Jun 2001)
Revision: 3287
Log message:

      These were obsoleted by Term_match_table in '99 and are no longer in use.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-23 19:35:09 -0700 (Sat, 23 Jun 2001)
Revision: 3288
Log message:

      Converted remining .prlb's in CVS into .prla's.
      I had two kill 3 .prlb files - they were too old and could no longer be read.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-23 23:03:37 -0700 (Sat, 23 Jun 2001)
Revision: 3289
Log message:

      Made sure reflect_itt compiles.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-23 23:24:03 -0700 (Sat, 23 Jun 2001)
Revision: 3290
Log message:

      Removed the hack for old IO proof type - I believe that
      we no longer have any "old IO" files.
      

Changes by: ( at unknown.email)
Date: 2001-06-23 23:24:03 -0700 (Sat, 23 Jun 2001)
Revision: 3291
Log message:

      This commit was manufactured by cvs2svn to create tag
      'meta-prl-0_6_0'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-24 03:25:49 -0700 (Sun, 24 Jun 2001)
Revision: 3292
Log message:

      *** IMPORTANT: before doing "cvs update" see warning below ***
      
      This commit implements a global resource that brings together resource management
      that used to be done by each resource in its own way.
      
      - A much simplier object (Mp_resource.resource_info) is now needed to create a new resource.
      Additionally, many resource helper modules, such as term_match_table now provide functions
      that create a resource_info for you.
      
      - Funtions get_tactic_arg, get_int_tactic_arg, etc were replaced by a single function
      get_resource_arg (note: functions for basci types, such as get_with_arg, get_sel_args, etc
      were _not_ affected)
      
      - Resource declaration statement now declares and resource creation statement now creates
      a function get_<name>_resource. This function ca be passed as a second argument
      to get_resource_arg to retrieve the current value of a particular resource.
      
      - Resource annotation functions are now separate from the resource declaration/creation
      mechanism. Resource annotation on a rule are now passed to a function named
      process_<name>_resource_annotation. This function must have the appropriate
      Mp_resource.annotation_processor type for the resource. This function can be declared
      and implemented in _any_ module, not just the module that declares and creates the
      <name> resource.
      
      - Currenlty MetaPRL leaves it to Ocaml to keep track of these functions.
      Consequently the module that defines the process_<name>_resource_annotation function
      must be open'ed (not included!) by modules that use <name> annotations.
      
      -----
      
      Unfinished business in this commit:
      - Remainder of TODO 1.12 and 1.13
      
      - Some proofs were broken by this commit. It appears that they were broken for
      a "good" reason, but still need to be fixed.
      
      - I need to make sure things now always have the right precedences (all things being equal,
      the later an item is added to resource, the earlier precedence it should have).
      
      - Consider adding refiner sentinels and display forms to global resource as well.
      Currently each of them still does its own way of resource management (although the way
      display forms are managed was changed by this commit - need to make sure the precedences
      are right).
      
      - Distributed refinement: I am afraid that the current resource code
      will either work correctly only if all processes in the distributed group have
      the same global resource, or it will attempt to pass around all the resource data.
      Obviously, neither of these choices is a good one.
      
      *** WARNING ***
      
      This commit changes the tactic_arg type and also makes minor changes in
      the FilterCache.info type. Because of that old .prlb and .cmoz files
      *will no longer work*. Old .prla files will work, but will produce lots
      of (harmless) Filter_summary.dest_term warning.
      
      Before doing "cvs update" do the following:
      1) export all your unsaved proofs into .prla files.
      2) rm -f theories/*/*.prlb
      3) run "make clean"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-24 04:13:06 -0700 (Sun, 24 Jun 2001)
Revision: 3293
Log message:

      Fixed a few proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-24 10:30:44 -0700 (Sun, 24 Jun 2001)
Revision: 3294
Log message:

      - Corrected precedences in Term_match_table (dforms, dT, etc).
      - Mptop now will understand fully qualified names correctly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-24 11:46:24 -0700 (Sun, 24 Jun 2001)
Revision: 3295
Log message:

      - Term_match_table seems to be finally doing the right thing.
      It turned out that it was alternating the order on each next term dept,
      so the order appeared pretty random.
      
      - Fixed handling of (unit -> 'a) toploop functions in filter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-24 13:26:12 -0700 (Sun, 24 Jun 2001)
Revision: 3296
Log message:

      Fixed a problem with cond rewrites labels that I accidentally introduced earlier.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-24 14:45:02 -0700 (Sun, 24 Jun 2001)
Revision: 3297
Log message:

      Resource intermediate data type is irrelevant, so they are no longer required
      in the resource declaration.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-24 18:34:52 -0700 (Sun, 24 Jun 2001)
Revision: 3298
Log message:

      - All rules in record theories are prooved (except some simple arith facts).
      
      - Now progressT checks whether the assumptions are changed (not only the goal).
      
      - Add a new operator tsquash{A}={Top|A}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-26 07:08:42 -0700 (Tue, 26 Jun 2001)
Revision: 3299
Log message:

      sub/sup should assume math mode.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-28 13:52:56 -0700 (Thu, 28 Jun 2001)
Revision: 3300
Log message:

      
      - I moved the rule quotientElimination2 to the Itt_pointwise2, since it is
      valid only for the pointwise functionality. Now this rule is derived
      from Itt_pointwise.
      I also proved t/bunionElimination2. Also I prove new versions of these rules
      (t/bunion/quotientElimination_eq) that are stronger that weak eliminations,
      but still valid in any functionality.
      
      - I also moved the Eta reduction to a separate theory.
      
      - I fixed and proved two rules in Itt_union.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-28 18:50:17 -0700 (Thu, 28 Jun 2001)
Revision: 3301
Log message:

      Updated SIL theory to a compilable state.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-29 16:06:26 -0700 (Fri, 29 Jun 2001)
Revision: 3302
Log message:

      Added a functionality to be able to limit JProver's maximal multiplicity level.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-29 17:45:30 -0700 (Fri, 29 Jun 2001)
Revision: 3303
Log message:

      Simplify primitive rules and improve tactics for elimination of intersection types.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-29 20:22:54 -0700 (Fri, 29 Jun 2001)
Revision: 3304
Log message:

      Added num_assums and nth_assums to Refine and Sequent.