Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-03 10:04:51 -0800 (Sat, 03 Apr 1999)
Revision: 2625
Log message:

      There is no need to list TODO here
      

Changes  Path
+1 -3 metaprl/README

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-03 21:24:42 -0800 (Sat, 03 Apr 1999)
Revision: 2626
Log message:

      Added MetaLabeled of string * meta_term variant to meta_term type
      
      Ml_format.print_term would raise an exception when given meta_term -
      I could not figure out what is supposed to go there.
      
      In filter_simmary in functions meta_term_of_term and term_of_meta_term
      MetaLabeled (l, t) is encoded as   meta_labeled [String l] (t)
      

Changes  Path
+15 -1 metaprl/filter/filter_summary.ml
+40 -35 metaprl/refiner/reflib/dform.ml
+3 -0 metaprl/refiner/reflib/ml_format.ml
+39 -35 metaprl/refiner/reflib/simple_print.ml
+2 -0 metaprl/refiner/refsig/term_header_sig.mlz
+1 -0 metaprl/refiner/refsig/term_simple_sig.mlz
+1 -0 metaprl/refiner/term_ds/term_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+2 -0 metaprl/refiner/term_gen/term_hash.ml
+4 -0 metaprl/refiner/term_gen/term_header.ml
+2 -0 metaprl/refiner/term_gen/term_header_constr.ml
+34 -21 metaprl/refiner/term_gen/term_meta_gen.ml
+2 -0 metaprl/refiner/term_std/term_std.ml
+1 -0 metaprl/refiner/term_std/term_std_sig.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-03 21:38:15 -0800 (Sat, 03 Apr 1999)
Revision: 2627
Log message:

      This file was never used.
      

Changes  Path
Deleted metaprl/refiner/refsig/resource.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-03 22:15:11 -0800 (Sat, 03 Apr 1999)
Revision: 2628
Log message:

      Added parsing of resource annotations. Used {| ... |} delimiters
      

Changes  Path
+27 -5 metaprl/filter/filter_parse.ml
+7 -0 metaprl/filter/filter_type.mlz

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-04-04 15:07:38 -0700 (Sun, 04 Apr 1999)
Revision: 2629
Log message:

      This is the first phase for modifying resources.
      The Mp_resource interface has been substantially simplified, but
      I believe that it retains as much functionality as it did before
      the change.
      
      The next step for me to add the Mp_resource support for
      adding resources as rule annotations.
      

Changes  Path
+10 -10 metaprl/editor/ml/package_info.ml
+4 -4 metaprl/editor/ml/shell_mp.ml
+2 -0 metaprl/filter/filter_comment.ml
+10 -0 metaprl/filter/filter_hash.ml
+36 -0 metaprl/filter/filter_ocaml.ml
+10 -10 metaprl/filter/filter_prog.ml
+10 -0 metaprl/filter/mLast_util.ml
+1 -1 metaprl/mk/rules
+90 -10 metaprl/refiner/reflib/mp_resource.ml
+45 -11 metaprl/refiner/reflib/mp_resource.mli
+32 -93 metaprl/theories/base/base_auto_tactic.ml
+4 -4 metaprl/theories/base/base_auto_tactic.mli
+18 -47 metaprl/theories/base/base_cache.ml
+4 -7 metaprl/theories/base/base_cache.mli
+16 -44 metaprl/theories/base/base_dtactic.ml
+5 -5 metaprl/theories/base/base_rewrite.ml
+28 -84 metaprl/theories/base/typeinf.ml
+4 -4 metaprl/theories/czf/czf_itt_all.ml
+4 -4 metaprl/theories/czf/czf_itt_and.ml
+3 -3 metaprl/theories/czf/czf_itt_dall.ml
+3 -3 metaprl/theories/czf/czf_itt_dexists.ml
+2 -2 metaprl/theories/czf/czf_itt_empty.ml
+11 -11 metaprl/theories/czf/czf_itt_eq.ml
+4 -4 metaprl/theories/czf/czf_itt_eq_inner.ml
+4 -4 metaprl/theories/czf/czf_itt_exists.ml
+4 -4 metaprl/theories/czf/czf_itt_false.ml
+6 -6 metaprl/theories/czf/czf_itt_implies.ml
+2 -2 metaprl/theories/czf/czf_itt_member.ml
+4 -4 metaprl/theories/czf/czf_itt_or.ml
+7 -7 metaprl/theories/czf/czf_itt_pre_set.ml
+1 -1 metaprl/theories/czf/czf_itt_rel.ml
+2 -2 metaprl/theories/czf/czf_itt_sall.ml
+2 -2 metaprl/theories/czf/czf_itt_sep.ml
+8 -8 metaprl/theories/czf/czf_itt_set.ml
+7 -7 metaprl/theories/czf/czf_itt_set_ext.ml
+4 -4 metaprl/theories/czf/czf_itt_set_ind.ml
+2 -2 metaprl/theories/czf/czf_itt_sexists.ml
+10 -10 metaprl/theories/czf/czf_itt_small.ml
+4 -4 metaprl/theories/czf/czf_itt_true.ml
+2 -2 metaprl/theories/czf/czf_itt_union.ml
+2 -2 metaprl/theories/fol/fol_all.ml
+2 -2 metaprl/theories/fol/fol_and.ml
+2 -2 metaprl/theories/fol/fol_bisect_itt.ml
+2 -2 metaprl/theories/fol/fol_exists.ml
+2 -2 metaprl/theories/fol/fol_false.ml
+2 -2 metaprl/theories/fol/fol_implies.ml
+2 -2 metaprl/theories/fol/fol_not.ml
+2 -2 metaprl/theories/fol/fol_or.ml
+1 -1 metaprl/theories/fol/fol_struct.ml
+2 -2 metaprl/theories/fol/fol_true.ml
+1 -1 metaprl/theories/fol/fol_type.ml
+1 -1 metaprl/theories/fol/fol_univ.ml
+3 -3 metaprl/theories/fol/fol_univ_itt.ml
+7 -7 metaprl/theories/itt/itt_atom.ml
+2 -2 metaprl/theories/itt/itt_atom_bool.ml
+7 -7 metaprl/theories/itt/itt_bisect.ml
+26 -26 metaprl/theories/itt/itt_bool.ml
+4 -4 metaprl/theories/itt/itt_bunion.ml
+10 -10 metaprl/theories/itt/itt_dfun.ml
+11 -11 metaprl/theories/itt/itt_dprod.ml
+28 -54 metaprl/theories/itt/itt_equal.ml
+9 -9 metaprl/theories/itt/itt_fset.ml
+11 -11 metaprl/theories/itt/itt_fun.ml
+7 -7 metaprl/theories/itt/itt_int.ml
+2 -2 metaprl/theories/itt/itt_int_bool.ml
+8 -8 metaprl/theories/itt/itt_isect.ml
+19 -19 metaprl/theories/itt/itt_list.ml
+5 -5 metaprl/theories/itt/itt_list2.ml
+53 -53 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_prec.ml
+8 -8 metaprl/theories/itt/itt_prod.ml
+8 -8 metaprl/theories/itt/itt_quotient.ml
+5 -5 metaprl/theories/itt/itt_rfun.ml
+8 -9 metaprl/theories/itt/itt_set.ml
+18 -45 metaprl/theories/itt/itt_squash.ml
+4 -4 metaprl/theories/itt/itt_squash.mli
+6 -6 metaprl/theories/itt/itt_srec.ml
+1 -1 metaprl/theories/itt/itt_struct.ml
+19 -47 metaprl/theories/itt/itt_subtype.ml
+4 -4 metaprl/theories/itt/itt_tsub.ml
+5 -5 metaprl/theories/itt/itt_tunion.ml
+14 -14 metaprl/theories/itt/itt_union.ml
+10 -11 metaprl/theories/itt/itt_unit.ml
+7 -9 metaprl/theories/itt/itt_void.ml
+11 -11 metaprl/theories/itt/itt_w.ml
+10 -10 metaprl/theories/reflect_itt/refl_raw_term.ml
+1 -1 metaprl/theories/reflect_itt/refl_term.ml
+3 -3 metaprl/theories/reflect_itt/refl_var.ml
+15 -42 metaprl/theories/tactic/conversionals.ml
+1 -1 metaprl/theories/tactic/conversionals.mli
+22 -65 metaprl/theories/tactic/mptop.ml
+4 -8 metaprl/theories/tactic/mptop.mli
Added metaprl/theories/tactic/pre_tactic_type.ml
Properties metaprl/theories/tactic/pre_tactic_type.ml
Added metaprl/theories/tactic/pre_tactic_type.mli
Properties metaprl/theories/tactic/pre_tactic_type.mli
+7 -7 metaprl/theories/tptp/tptp.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-04-04 16:35:20 -0700 (Sun, 04 Apr 1999)
Revision: 2630
Log message:

      Added the primitive support for resource improvement through
      rule annotations.  There is still no connection with the parser.
      

Changes  Path
+10 -9 metaprl/filter/filter_parse.ml
+8 -5 metaprl/filter/filter_prog.ml
+18 -12 metaprl/filter/filter_summary.ml
+6 -5 metaprl/filter/filter_summary.mli
+15 -4 metaprl/refiner/reflib/mp_resource.ml
+18 -10 metaprl/refiner/reflib/mp_resource.mli
+7 -7 metaprl/refiner/term_gen/term_meta_gen.ml
+15 -7 metaprl/theories/base/base_auto_tactic.ml
+3 -2 metaprl/theories/base/base_auto_tactic.mli
+2 -1 metaprl/theories/base/base_cache.ml
+1 -1 metaprl/theories/base/base_cache.mli
+2 -1 metaprl/theories/base/base_dtactic.ml
+1 -1 metaprl/theories/base/base_dtactic.mli
+4 -2 metaprl/theories/base/typeinf.ml
+2 -2 metaprl/theories/base/typeinf.mli
+2 -1 metaprl/theories/itt/itt_equal.ml
+2 -1 metaprl/theories/itt/itt_equal.mli
+2 -1 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_squash.mli
+2 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_subtype.mli
+10 -2 metaprl/theories/tactic/conversionals.ml
+1 -1 metaprl/theories/tactic/conversionals.mli
+2 -1 metaprl/theories/tactic/mptop.ml
+1 -1 metaprl/theories/tactic/mptop.mli
+5 -0 metaprl/util/macro.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-04-05 12:51:04 -0700 (Mon, 05 Apr 1999)
Revision: 2631
Log message:

      Added MetaLabeled to term_grammar.
      

Changes  Path
+1 -1 metaprl/filter/term_grammar.ml
+1 -1 metaprl/util/macro.ml

Changes by: ( at unknown.email)
Date: 1999-04-05 12:51:04 -0700 (Mon, 05 Apr 1999)
Revision: 2632
Log message:

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

Changes  Path
Copied metaprl-tags/meta-prl-0_5

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-05 14:16:49 -0700 (Mon, 05 Apr 1999)
Revision: 2633
Log message:

      I've created a tag "meta-prl-0_5", bumped the version number to 0.5.1
      and moved the vesrion number from editor/ml/Makefile to mk/preface
      

Changes  Path
+2 -2 metaprl/editor/ml/Makefile
+1 -0 metaprl/mk/preface

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-05 20:50:43 -0700 (Mon, 05 Apr 1999)
Revision: 2634
Log message:

      This logo isn't perfect but at least it is better than what we have now.
      

Changes  Path
Binary metaprl/doc/htmlman/images/mp-logo.gif

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-05 20:55:18 -0700 (Mon, 05 Apr 1999)
Revision: 2635
Log message:

      Changes the parameters of the IMG tag to fit the size of the new logo
      

Changes  Path
+1 -1 metaprl/doc/htmlman/mp.html

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-04-06 12:50:03 -0700 (Tue, 06 Apr 1999)
Revision: 2636
Log message:

      Removed Resource{Int,String} type.
      

Changes  Path
+1 -11 metaprl/filter/filter_parse.ml
+4 -11 metaprl/filter/filter_type.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-06 16:29:52 -0700 (Tue, 06 Apr 1999)
Revision: 2637
Log message:

      Added ENSROOT and OCAMLSRC to mk/config.
      
      When the mk/config is created for the first time, the environment
      variables would be consulted and if they point to existing directories,
      they would be added to mk/config, otherwise "undefined" is used.
      
      Once ENSROOT and OCAMLSRC are entered into mk/config,
      make would ignore ENSROOT and OCAMLSRC environment variables
      

Changes  Path
+2 -2 metaprl/Makefile
+4 -2 metaprl/clib/Makefile
+1 -1 metaprl/debug/Makefile
+15 -14 metaprl/doc/htmlman/mp-install.html
+1 -1 metaprl/editor/ml/Makefile
+10 -6 metaprl/ensemble/Makefile
+22 -0 metaprl/mk/make_config.sh
+6 -0 metaprl/mk/preface

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-07 18:33:12 -0700 (Wed, 07 Apr 1999)
Revision: 2638
Log message:

      Moved most filter_summary types into the filter_type.mlz
      

Changes  Path
+2 -2 metaprl/editor/ml/mp.mli
+2 -1 metaprl/editor/ml/package_df.ml
+1 -1 metaprl/editor/ml/package_df.mli
+1 -1 metaprl/editor/ml/proof_edit.ml
+3 -3 metaprl/editor/ml/proof_edit.mli
+1 -0 metaprl/editor/ml/shell.ml
+2 -2 metaprl/editor/ml/shell.mli
+22 -21 metaprl/editor/ml/shell_rewrite.ml
+1 -1 metaprl/editor/ml/shell_rewrite.mli
+20 -19 metaprl/editor/ml/shell_rule.ml
+1 -1 metaprl/editor/ml/shell_rule.mli
+1 -1 metaprl/editor/ml/shell_type.mlz
+2 -134 metaprl/filter/filter_summary.ml
+2 -148 metaprl/filter/filter_summary.mli
+1 -0 metaprl/filter/filter_summary_util.ml
+1 -0 metaprl/filter/filter_summary_util.mli
+155 -0 metaprl/filter/filter_type.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-07 20:40:01 -0700 (Wed, 07 Apr 1999)
Revision: 2639
Log message:

      Added *_resources components to rewrite_info, axiom_info,
      cond_rewrite_info and rule_info filter_summary types.
      
      So far we are not doing anything smart with those fields - in most
      cases they are set to [] and ignored, but the parser already puts
      the (supposedly) correct information in there.
      
      From what I can tell, we are still able to read old .prlb files after these
      changes.
      

Changes  Path
+6 -3 metaprl/editor/ml/shell_rewrite.ml
+2 -2 metaprl/editor/ml/shell_rewrite.mli
+6 -3 metaprl/editor/ml/shell_rule.ml
+2 -2 metaprl/editor/ml/shell_rule.mli
+36 -32 metaprl/filter/filter_parse.ml
+8 -8 metaprl/filter/filter_prog.ml
+8 -8 metaprl/filter/filter_prog.mli
+107 -41 metaprl/filter/filter_summary.ml
+4 -4 metaprl/filter/filter_summary.mli
+17 -13 metaprl/filter/filter_type.mlz
+4 -0 metaprl/refiner/refsig/term_op_sig.ml
+25 -4 metaprl/refiner/term_ds/term_op_ds.ml
+25 -0 metaprl/refiner/term_std/term_op_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-08 09:13:40 -0700 (Thu, 08 Apr 1999)
Revision: 2640
Log message:

      Updated the .prlb files.
      
      There is some bootstrapping issue here - I had to copy .cmoz to .prlb
      and recompile three times before they stopped changing.
      

Changes  Path
+1 -1 metaprl/mk/preface
Binary metaprl/theories/czf/czf_itt_all.prlb
Binary metaprl/theories/czf/czf_itt_and.prlb
Binary metaprl/theories/czf/czf_itt_axioms.prlb
Binary metaprl/theories/czf/czf_itt_dall.prlb
Binary metaprl/theories/czf/czf_itt_dexists.prlb
Binary metaprl/theories/czf/czf_itt_eq.prlb
Binary metaprl/theories/czf/czf_itt_exists.prlb
Binary metaprl/theories/czf/czf_itt_false.prlb
Binary metaprl/theories/czf/czf_itt_implies.prlb
Binary metaprl/theories/czf/czf_itt_member.prlb
Binary metaprl/theories/czf/czf_itt_or.prlb
Binary metaprl/theories/czf/czf_itt_rel.prlb
Binary metaprl/theories/czf/czf_itt_sall.prlb
Binary metaprl/theories/czf/czf_itt_sep.prlb
Binary metaprl/theories/czf/czf_itt_set.prlb
Binary metaprl/theories/czf/czf_itt_set_ind.prlb
Binary metaprl/theories/czf/czf_itt_sexists.prlb
Binary metaprl/theories/czf/czf_itt_true.prlb
Binary metaprl/theories/czf/czf_itt_union.prlb
Binary metaprl/theories/fol/fol_ctheory.prlb
Binary metaprl/theories/fol/fol_not.prlb
Binary metaprl/theories/fol/fol_theory.prlb
Binary metaprl/theories/itt/itt_bisect.prlb
Binary metaprl/theories/itt/itt_bool.prlb
Binary metaprl/theories/itt/itt_bunion.prlb
Binary metaprl/theories/itt/itt_derive.prlb
Binary metaprl/theories/itt/itt_equal.prlb
Binary metaprl/theories/itt/itt_fset.prlb
Binary metaprl/theories/itt/itt_isect.prlb
Binary metaprl/theories/itt/itt_list.prlb
Binary metaprl/theories/itt/itt_list2.prlb
Binary metaprl/theories/itt/itt_logic.prlb
Binary metaprl/theories/itt/itt_prop_decide.prlb
Binary metaprl/theories/reflect_itt/refl_free_vars.prlb
Binary metaprl/theories/reflect_itt/refl_raw_term.prlb
Binary metaprl/theories/reflect_itt/refl_term.prlb
Binary metaprl/theories/reflect_itt/refl_var.prlb
Binary metaprl/theories/reflect_itt/refl_var_set.prlb
Binary metaprl/theories/tptp/tptp.prlb

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-08 11:00:30 -0700 (Thu, 08 Apr 1999)
Revision: 2641
Log message:

      When a new rule/axiom/rewrite_info is created the resource filed
      is set to [] only if there are actually no resource updates
      associated with this item.
      
      However it is still possible that resource field is ignored or discarded
      in some places.
      

Changes  Path
+16 -9 metaprl/editor/ml/shell_rewrite.ml
+16 -9 metaprl/editor/ml/shell_rule.ml
+62 -81 metaprl/filter/filter_summary.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-08 18:54:01 -0700 (Thu, 08 Apr 1999)
Revision: 2642
Log message:

      Better dependence generation.
      
      We still put both native and bytecode dependences
      in the same Makefile.dep file, but now the dependence list
      should be more complete.
      
      For example, if you run "make all" first, ocamldep would look
      for .ml and .cmo files and when found, it would generate a
      .cmx: .cmx dependence, so if you run "make opt" afterwards,
      you do not have missing dependencies problem.
      

Changes  Path
+45 -28 metaprl/util/ocamldep.mll

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-04-28 17:18:11 -0700 (Wed, 28 Apr 1999)
Revision: 2643
Log message:

      Reverted the last change
      

Changes  Path
+0 -0 metaprl/mk/rules

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 1999-04-28 17:30:51 -0700 (Wed, 28 Apr 1999)
Revision: 2644
Log message:

      Added module name (Rewrtie_compile_contractum.) to all the RefinerError raised from this file
      

Changes  Path
+9 -9 metaprl/refiner/rewrite/rewrite_compile_contractum.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-29 11:21:53 -0700 (Thu, 29 Apr 1999)
Revision: 2645
Log message:

      dT: thin after eliminating independant product from a hypothesis.
      

Changes  Path
+4 -1 metaprl/theories/itt/itt_prod.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-29 17:00:55 -0700 (Thu, 29 Apr 1999)
Revision: 2646
Log message:

      ref_raise should only be used for raising RefineError errors
      

Changes  Path
+2 -2 metaprl/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl/refiner/term_std/term_eval_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-29 19:49:58 -0700 (Thu, 29 Apr 1999)
Revision: 2647
Log message:

      Fixed the error reporting that I broke when added the resource annotations
      

Changes  Path
+3 -3 metaprl/filter/filter_parse.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-29 20:08:08 -0700 (Thu, 29 Apr 1999)
Revision: 2648
Log message:

      Forced the typechecker to test whether print_exn is applied correctly.
      Found some other potential problems with the resource argument missing
      

Changes  Path
+23 -17 metaprl/filter/filter_parse.ml