Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-03 12:20:18 -0700 (Sat, 03 Jul 1999)
Revision: 2771
Log message:

      For static terms and mterms, use "let ...;; let ... " instead of
      a big "let ... and ... and ...".
      
      Unfortunatelly, this did not fix the "make opt" problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-03 17:42:06 -0700 (Sat, 03 Jul 1999)
Revision: 2772
Log message:

      Small changes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-03 20:02:58 -0700 (Sat, 03 Jul 1999)
Revision: 2773
Log message:

      I wrote a decideT tactic, similar to Nuprl4 Decide tactic.
      
      We need to prove some decidability rules and add them to the decide_resource
      in order to make this tactic useful.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-04 01:45:48 -0700 (Sun, 04 Jul 1999)
Revision: 2774
Log message:

      Forgot to update the .mli
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-04 06:13:44 -0700 (Sun, 04 Jul 1999)
Revision: 2775
Log message:

      Things seem to be working pretty smoothly now.  This is mostly minor
      fixes.  Still need to fix the problems with the mp toploop.
      
          1. Proofs now use Alexey's ASCII format.  By default, proofs
             should be saved to CVS in .prla format.  You can generate ASCII
             files by using "make export", or you can use the "export ()"
             instead of the "save ()" command in the editor.  For speed,
             .prlb files are now saved in a raw, marshaled format.  When you
             edit a theory, the newest of .cmoz, .prlb, or .prla files is
             loaded.  There is a new command "convert" to convert between
             all the different proof file formats.
                convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
                raw: save the file in fast, raw format
         term: save the file as <magic#>/<marshaled term_io>
         lib: send the file to the Nuprl5 library
         ascii: create a .prla file
      
             Developers: _please_ mention any changes to the basic data
                structures in your CVS logs.  The things that matter are:
                Refiner.Refiner.TermType.term
         Filter_summary.summary_info
         Tactic_boot_sig.TacticType.{tactic_arg,extract}
         Proof_boot.io_proof
      
             Users: to be safe, save all your proofs using "make export"
                before doing a cvs update.
      
          2. "expand ()" and "expand_all ()" now work.  I also added
             "clean ()" and "clean_all ()" commands to remove those peasky
             dangling proof nodes when you are satisfied with a proof.  By
             default, proofs are saved only down to the innermost rule-box
             level, and primitive refinements are omitted.  I haven't added
             a "deep_save ()" command; it seems unecessary.
      
          3. Sorry, but I had to move theories/boot into the filter.  There
             are no major changes here, but the directory structure in
             filter has changed significantly.
      
          4. I added a THEORIES variable to the mk/config file that
             specifies what theories you want to compile.  This means that
             you don't have to edit all the Makefiles when you add a theory,
             and it also means that you can keep your own theories without
             having to commit them to cvs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-04 10:50:31 -0700 (Sun, 04 Jul 1999)
Revision: 2776
Log message:

      Fixed "make opt" in filter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-04 12:35:12 -0700 (Sun, 04 Jul 1999)
Revision: 2777
Log message:

      Handle THEORIES variable a little better
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-04 19:34:48 -0700 (Sun, 04 Jul 1999)
Revision: 2778
Log message:

      Added Itt_sort for Alexey's demo.  Reading the .prla file is _really_ slow
      so I added the .prlb file as well.  We known that normalization is exponential:
      do we have to add a number to every term, or can we be smarter?
      
      In Base_dtactic I added two options:
         IntroArgsOption of (tactic_arg -> term -> term list) * term option
         ElimArgsOption of (tactic_arg -> term -> term list) * term option
      The function computes the term arguments for the rule, and the term option
      specifies the subterm to pass.  Example:
         interactive applyMember {| intro_resource [IntroArgsOption (infer_type_args, << 'f >>)] |} 'H ('A -> 'B) :
             [wf] sequent [squash] { 'H >- member{.'A -> 'B; 'f} } -->
             ...
             sequent ['ext] { 'H >- member{'T; .'f 'a} }
      This would use the type inference function "infer_type_args" to infer the type for 'f
      and use it as the term argument ('A -> 'B).  Of course, the refiner will complain if
      the infered type is not a simple function type.
      
      This is only used in Itt_sort right now, and it is experimental.  We want
      an option like this because type inference is such a common requirement.
      But this specification is too ad-hoc, and I will think about it further
      (suggestions welcome).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-04 20:30:15 -0700 (Sun, 04 Jul 1999)
Revision: 2779
Log message:

      Inlined static_term definitions.
      
      This makes .ppo files slightly smaller and will, hopefully,
      speed up compilation a little.
      
      For some reason, num_regs in ocamlopt was almost unaffected by
      this change and ocamlopt still fails of itt_fset.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-04 21:18:58 -0700 (Sun, 04 Jul 1999)
Revision: 2780
Log message:

      Fixed the bug that was preventing updates
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-04 22:40:01 -0700 (Sun, 04 Jul 1999)
Revision: 2781
Log message:

      Filter now reads .prla file even if .prlb file does not exist.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-04 23:15:37 -0700 (Sun, 04 Jul 1999)
Revision: 2782
Log message:

      Improved some display forms
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-05 01:30:08 -0700 (Mon, 05 Jul 1999)
Revision: 2783
Log message:

      Fixed dest_fix
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-05 02:17:12 -0700 (Mon, 05 Jul 1999)
Revision: 2784
Log message:

      Fixed several dest_str function, now all theories/itt/.prla can be read
      successfully.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-05 06:07:54 -0700 (Mon, 05 Jul 1999)
Revision: 2785
Log message:

      Filter creates .prlb file from .prla if it does not exist.
      Fixed prec_rel term format that was causing parsing errors when
      the .prla file was read.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-05 06:38:57 -0700 (Mon, 05 Jul 1999)
Revision: 2786
Log message:

      Added: Itt_logic.genAssumT : int list -> tactic
      This tactical "generalizes" over a set of assumptions.  The first
      assumption should be for a membership judgment.  For example:
         ...
      i. H >- t in T list
         ...
      j. H >- Q[t]
         ...
         H >- P[t]
         BY genAssumT [i; j]
      1. H >- all l: T list. (Q[l] => P[l])
      2. H; x: (all l: T list. (Q[l] => P[l])) >- P[t]
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-05 06:58:43 -0700 (Mon, 05 Jul 1999)
Revision: 2787
Log message:

      There is no reason to keep these .prlb files
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-05 07:49:32 -0700 (Mon, 05 Jul 1999)
Revision: 2788
Log message:

      ifthenelse_member was defined twice.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-06 08:33:34 -0700 (Tue, 06 Jul 1999)
Revision: 2789
Log message:

      Small display form change
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-06 08:35:50 -0700 (Tue, 06 Jul 1999)
Revision: 2790
Log message:

      Changed genAssumT:
      
      generalize all the assumtions that have the "member" goal, not only the first one,
      do the usual assumT thing for non-member goals
      
      After the generalization, prove the "main" subgoal automatically
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-07 05:40:04 -0700 (Wed, 07 Jul 1999)
Revision: 2791
Log message:

      Ignore *.prlb
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-07 05:43:01 -0700 (Wed, 07 Jul 1999)
Revision: 2792
Log message:

      Be more careful to thin the right hypothesis.
      This makes dT work as expected when given a negative hyp number.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-07 09:24:35 -0700 (Wed, 07 Jul 1999)
Revision: 2793
Log message:

      Do not keep normalazing the same opnames over and over.
      
      Added filter_opt target, useful to get convert, etc compiled into the native code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-08 00:22:59 -0700 (Thu, 08 Jul 1999)
Revision: 2794
Log message:

      Performance fixes:
      
      Faster generation of the output in Ascii_io
      Faster collection of bound variables of a term.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-08 00:31:08 -0700 (Thu, 08 Jul 1999)
Revision: 2795
Log message:

      Changed the definition of compare_lt from (lt a b) to assert(lt a b).
      That allowed me to eliminate asserts from all the theorem statements and from most proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-09 07:13:33 -0700 (Fri, 09 Jul 1999)
Revision: 2796
Log message:

      Fixed comments
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-13 00:47:33 -0700 (Tue, 13 Jul 1999)
Revision: 2797
Log message:

      Removed some files that were copied to filter/base
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-07-17 16:16:33 -0700 (Sat, 17 Jul 1999)
Revision: 2798
Log message:

      New version of itt_quickref.txt; should be up to date.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-22 17:24:57 -0700 (Thu, 22 Jul 1999)
Revision: 2799
Log message:

      Now one can use SO variables in display form specifications
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 10:14:39 -0700 (Fri, 23 Jul 1999)
Revision: 2800
Log message:

      Moved ML files from filter to filter/filter
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 10:25:21 -0700 (Fri, 23 Jul 1999)
Revision: 2801
Log message:

      Renamed to avoid name conflicts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 10:40:54 -0700 (Fri, 23 Jul 1999)
Revision: 2802
Log message:

      Hopefully it works now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 11:40:31 -0700 (Fri, 23 Jul 1999)
Revision: 2803
Log message:

      Fixed intro/elim annotations in itt_collection
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 12:50:37 -0700 (Fri, 23 Jul 1999)
Revision: 2804
Log message:

      reduceIfthenelse{True,False} were renamed to reduce_ifthenelse_{true,false}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-07-23 13:51:24 -0700 (Fri, 23 Jul 1999)
Revision: 2805
Log message:

      Some theories still had Itt_squash!squash instead of Base_trivial!squash - fixed.
      Now more old proofs expand correctly.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-07-24 14:08:56 -0700 (Sat, 24 Jul 1999)
Revision: 2806
Log message:

      Added fold_bunion.