Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-04 22:17:06 -0700 (Sat, 04 May 2002)
Revision: 3595
Log message:

      Redefined "inv_image" with "sep".
      

Changes  Path
+5 -11 metaprl/theories/czf/czf_itt_inv_image.ml
+2 -3 metaprl/theories/czf/czf_itt_inv_image.mli
+550 -549 metaprl/theories/czf/czf_itt_inv_image.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-04 22:17:52 -0700 (Sat, 04 May 2002)
Revision: 3596
Log message:

      Removed "setbvd_prop" which can be implemented with "sep".
      

Changes  Path
+0 -25 metaprl/theories/czf/czf_itt_set_bvd.ml
+0 -3 metaprl/theories/czf/czf_itt_set_bvd.mli
+205 -451 metaprl/theories/czf/czf_itt_set_bvd.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-04 22:20:43 -0700 (Sat, 04 May 2002)
Revision: 3597
Log message:

      Replaced the use of "setbvd_prop" with "sep".
      Separated the definition of kernels from Czf_itt_hom, and created a new
      module Czf_itt_ker for kernels.
      

Changes  Path
+1 -0 metaprl/theories/czf/Makefile
+0 -134 metaprl/theories/czf/czf_itt_hom.ml
+0 -10 metaprl/theories/czf/czf_itt_hom.mli
+729 -10834 metaprl/theories/czf/czf_itt_hom.prla
Added metaprl/theories/czf/czf_itt_ker.ml
Properties metaprl/theories/czf/czf_itt_ker.ml
Added metaprl/theories/czf/czf_itt_ker.mli
Properties metaprl/theories/czf/czf_itt_ker.mli
Added metaprl/theories/czf/czf_itt_ker.prla
Properties metaprl/theories/czf/czf_itt_ker.prla

Changes by: ( at unknown.email)
Date: 2002-05-04 22:20:43 -0700 (Sat, 04 May 2002)
Revision: 3598
Log message:

      This commit was manufactured by cvs2svn to create tag
      'before_ocaml_3_04'.

Changes  Path
Copied metaprl-tags/before_ocaml_3_04
Copied texinputs-tags/before_ocaml_3_04
Deleted texinputs-tags/before_ocaml_3_04/1cm.sty
Deleted texinputs-tags/before_ocaml_3_04/1cml.sty
Deleted texinputs-tags/before_ocaml_3_04/Makefile-common
Deleted texinputs-tags/before_ocaml_3_04/bcp.bib
Deleted texinputs-tags/before_ocaml_3_04/citlogo.eps
Deleted texinputs-tags/before_ocaml_3_04/cornell-logo.eps
Deleted texinputs-tags/before_ocaml_3_04/dag50.eps
Deleted texinputs-tags/before_ocaml_3_04/der.tex
Deleted texinputs-tags/before_ocaml_3_04/include.tex
Deleted texinputs-tags/before_ocaml_3_04/llncs.cls
Deleted texinputs-tags/before_ocaml_3_04/omscmsy.fd
Deleted texinputs-tags/before_ocaml_3_04/ot1cmr.fd
Deleted texinputs-tags/before_ocaml_3_04/ot1cmss.fd
Deleted texinputs-tags/before_ocaml_3_04/ot1lcmss.fd
Deleted texinputs-tags/before_ocaml_3_04/ot1lcmtt.fd
Deleted texinputs-tags/before_ocaml_3_04/rc.bib
Deleted texinputs-tags/before_ocaml_3_04/slides-nogin.cls
Deleted texinputs-tags/before_ocaml_3_04/umsa.fd
Deleted texinputs-tags/before_ocaml_3_04/umsb.fd

Changes by: ( at unknown.email)
Date: 2002-05-04 22:20:43 -0700 (Sat, 04 May 2002)
Revision: 3599
Log message:

      This commit was manufactured by cvs2svn to create branch 'ocaml_3_04'.

Changes  Path
Copied metaprl-branches/ocaml_3_04
Copied texinputs-branches/ocaml_3_04
Deleted texinputs-branches/ocaml_3_04/1cm.sty
Deleted texinputs-branches/ocaml_3_04/1cml.sty
Deleted texinputs-branches/ocaml_3_04/Makefile-common
Deleted texinputs-branches/ocaml_3_04/bcp.bib
Deleted texinputs-branches/ocaml_3_04/citlogo.eps
Deleted texinputs-branches/ocaml_3_04/cornell-logo.eps
Deleted texinputs-branches/ocaml_3_04/dag50.eps
Deleted texinputs-branches/ocaml_3_04/der.tex
Deleted texinputs-branches/ocaml_3_04/include.tex
Deleted texinputs-branches/ocaml_3_04/llncs.cls
Deleted texinputs-branches/ocaml_3_04/omscmsy.fd
Deleted texinputs-branches/ocaml_3_04/ot1cmr.fd
Deleted texinputs-branches/ocaml_3_04/ot1cmss.fd
Deleted texinputs-branches/ocaml_3_04/ot1lcmss.fd
Deleted texinputs-branches/ocaml_3_04/ot1lcmtt.fd
Deleted texinputs-branches/ocaml_3_04/rc.bib
Deleted texinputs-branches/ocaml_3_04/slides-nogin.cls
Deleted texinputs-branches/ocaml_3_04/umsa.fd
Deleted texinputs-branches/ocaml_3_04/umsb.fd

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-05 20:22:43 -0700 (Sun, 05 May 2002)
Revision: 3600
Log message:

      This is a branch commit that upgrades to ocaml3.04.
      
      Warning: on this branch, metaprl compiles only in byte-code.
      (See Aleksey notes below).
      
      The extra feature: there is now an apply_rewrite function
      in Top_conversionals.
      
         val : apply_rewrite : unit -> conv -> term -> term
      
      Note: always use an instance in this kind of form:
      
         let apply_rewrite = Top_conversionals.apply_rewrite ()
         - : conv -> term -> term
      
      This will (hopefully) capture all the resources at definition time.
      
      Brian: see if this works, and let me know if there are problems.
      Mp_mc_compile is updated...
      
      Aleksey:
      
         1. I don't remember exactly what you included in the upgrade to
            ocaml-3.04...  Please remind me about the features
            needed to be added to camlp4.  Also, can you try and make
            ocaml produce native code for camlp4?  We have the old problem
            with camlp4 not being configured to produce native code.
      
         2. I'm not sure about the new resource code.  To define the
            apply_rewrite function, we need to get ahold of the resources
            live at the src definition point.  I'm assuming that
            Mp_resource.extract_top () will do that--but I'm not sure.
            Question: what can we assume about Mp_resource.extract_top?
      

Changes  Path
+4 -3 metaprl-branches/ocaml_3_04/Conscript
+0 -0 metaprl-branches/ocaml_3_04/clib/Conscript
+4 -3 metaprl-branches/ocaml_3_04/editor/ml/Conscript
+1 -1 metaprl-branches/ocaml_3_04/filter/base/Conscript
+9 -3 metaprl-branches/ocaml_3_04/filter/base/filter_comment.ml
+33 -9 metaprl-branches/ocaml_3_04/filter/base/filter_hash.ml
+139 -29 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.ml
+1 -1 metaprl-branches/ocaml_3_04/filter/base/free_vars.ml
+34 -13 metaprl-branches/ocaml_3_04/filter/base/mLast_util.ml
+2 -2 metaprl-branches/ocaml_3_04/filter/boot/Conscript
+4 -0 metaprl-branches/ocaml_3_04/filter/boot/conversionals_boot.ml
+14 -0 metaprl-branches/ocaml_3_04/filter/boot/rewrite_boot.ml
+16 -0 metaprl-branches/ocaml_3_04/filter/boot/tactic_boot.ml
+12 -0 metaprl-branches/ocaml_3_04/filter/boot/tactic_boot_sig.mlz
+11 -11 metaprl-branches/ocaml_3_04/filter/filter/Conscript
+2 -2 metaprl-branches/ocaml_3_04/mk/preface
+1 -1 metaprl-branches/ocaml_3_04/refiner/reflib/Conscript
+2 -1 metaprl-branches/ocaml_3_04/theories/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/base/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/itt/Conscript
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+5 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+3 -3 metaprl-branches/ocaml_3_04/theories/mc/tests/Conscript
+2 -2 metaprl-branches/ocaml_3_04/theories/ocaml/Conscript
+2 -2 metaprl-branches/ocaml_3_04/theories/tactic/Conscript
+14 -1 metaprl-branches/ocaml_3_04/theories/tactic/mptop.ml
+5 -0 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.ml
+4 -0 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.mli
+1 -1 metaprl-branches/ocaml_3_04/util/Makefile
+26 -8 metaprl-branches/ocaml_3_04/util/macro.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-06 03:11:50 -0700 (Mon, 06 May 2002)
Revision: 3601
Log message:

      Changing some conscripts so that .cmxa targets are no longer
      hardcoded.  Improves the build markedly when started in MetaPRL,
      but theories/itt/itt_squash.ml then fails with
      
         FormatError:
         Filter_ocaml.dest_type : bad arity
      

Changes  Path
+1 -1 metaprl-branches/ocaml_3_04/ensemble/Conscript
+1 -1 metaprl-branches/ocaml_3_04/filter/base/Conscript
+1 -1 metaprl-branches/ocaml_3_04/library/Conscript
+1 -1 metaprl-branches/ocaml_3_04/mllib/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/refbase/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/refiner/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/refsig/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/rewrite/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/term_ds/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/term_gen/Conscript
+1 -1 metaprl-branches/ocaml_3_04/refiner/term_std/Conscript

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-07 07:53:09 -0700 (Tue, 07 May 2002)
Revision: 3602
Log message:

      Instead of a hard coded flag in the Conscript to determine
      whether or not to generate native or byte code, use
      the environment variable OCAMLRUNPARAM.  See the Conscript
      on how to set this variable.
      

Changes  Path
+4 -2 metaprl-branches/ocaml_3_04/Conscript

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-07 08:02:50 -0700 (Tue, 07 May 2002)
Revision: 3603
Log message:

      Minor changes for 3.04.
      
      Jason, who is working on the filter not liking the .prla - you or me?
      I want to avoid the duplicated effort.
      
      I am getting close to having an RPM with working opt camlp4, will probably get there
      in a few hours.
      

Changes  Path
+1 -1 metaprl-branches/ocaml_3_04/mk/preface
+11 -28 metaprl-branches/ocaml_3_04/util/macro.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-07 11:02:52 -0700 (Tue, 07 May 2002)
Revision: 3604
Log message:

      The .prla problem should be fixed.  MetaPRL compiles both
      with "make" and "cons".
      
      Filter_ocaml unmarshaling for str_items now fails softly.  If the
      term format changes, you may get a warning asking you to regenerate
      the .prla files.
      
      This compiles with Aleksey's new OCaml in native code.  Note,
      if you are using RH7.2, the RH7.3 RPM will not work.  You can
      either rpm --rebuild from the RPM source, or maybe Aleksey can
      generate an old version at some point.
      

Changes  Path
+6 -1 metaprl-branches/ocaml_3_04/Conscript
+0 -1 metaprl-branches/ocaml_3_04/editor/ml/Conscript
+1 -2 metaprl-branches/ocaml_3_04/filter/base/filter_cache.ml
+55 -56 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.ml
+4 -0 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.mli
+1 -29 metaprl-branches/ocaml_3_04/filter/base/filter_summary.ml
+0 -1 metaprl-branches/ocaml_3_04/theories/Conscript
+353 -417 metaprl-branches/ocaml_3_04/theories/itt/ctt_markov.prla
+1538 -1484 metaprl-branches/ocaml_3_04/theories/itt/itt_bisect.prla
+4714 -4705 metaprl-branches/ocaml_3_04/theories/itt/itt_bool.prla
+517 -365 metaprl-branches/ocaml_3_04/theories/itt/itt_bunion.prla
+573 -573 metaprl-branches/ocaml_3_04/theories/itt/itt_collection.prla
+71 -71 metaprl-branches/ocaml_3_04/theories/itt/itt_decidable.prla
+2749 -2997 metaprl-branches/ocaml_3_04/theories/itt/itt_derive.prla
+1389 -1764 metaprl-branches/ocaml_3_04/theories/itt/itt_dfun.prla
+869 -890 metaprl-branches/ocaml_3_04/theories/itt/itt_disect.prla
+3078 -3479 metaprl-branches/ocaml_3_04/theories/itt/itt_dprod.prla
+4418 -4468 metaprl-branches/ocaml_3_04/theories/itt/itt_equal.prla
+60 -57 metaprl-branches/ocaml_3_04/theories/itt/itt_esquash.prla
+292 -311 metaprl-branches/ocaml_3_04/theories/itt/itt_ext_equal.prla
+3695 -3691 metaprl-branches/ocaml_3_04/theories/itt/itt_fset.prla
+1777 -1764 metaprl-branches/ocaml_3_04/theories/itt/itt_fun.prla
+215 -212 metaprl-branches/ocaml_3_04/theories/itt/itt_int_arith.prla
+3146 -3376 metaprl-branches/ocaml_3_04/theories/itt/itt_int_base.prla
+4823 -4775 metaprl-branches/ocaml_3_04/theories/itt/itt_int_ext.prla
+1287 -1395 metaprl-branches/ocaml_3_04/theories/itt/itt_isect.prla
+2343 -2429 metaprl-branches/ocaml_3_04/theories/itt/itt_list.prla
+2306 -2295 metaprl-branches/ocaml_3_04/theories/itt/itt_list2.prla
+15759 -15855 metaprl-branches/ocaml_3_04/theories/itt/itt_logic.prla
+2204 -2378 metaprl-branches/ocaml_3_04/theories/itt/itt_nat.prla
+271 -531 metaprl-branches/ocaml_3_04/theories/itt/itt_pointwise.prla
+286 -247 metaprl-branches/ocaml_3_04/theories/itt/itt_pointwise2.prla
+823 -1343 metaprl-branches/ocaml_3_04/theories/itt/itt_prod.prla
+637 -918 metaprl-branches/ocaml_3_04/theories/itt/itt_prop_decide.prla
+2162 -1758 metaprl-branches/ocaml_3_04/theories/itt/itt_quotient.prla
+395 -395 metaprl-branches/ocaml_3_04/theories/itt/itt_record.prla
+331 -316 metaprl-branches/ocaml_3_04/theories/itt/itt_record0.prla
+1081 -1088 metaprl-branches/ocaml_3_04/theories/itt/itt_record_exm.prla
+1482 -1724 metaprl-branches/ocaml_3_04/theories/itt/itt_record_label.prla
+638 -928 metaprl-branches/ocaml_3_04/theories/itt/itt_record_label0.prla
+5537 -6032 metaprl-branches/ocaml_3_04/theories/itt/itt_rfun.prla
+525 -525 metaprl-branches/ocaml_3_04/theories/itt/itt_sort.prla
+8719 -8029 metaprl-branches/ocaml_3_04/theories/itt/itt_squash.prla
+5338 -2171 metaprl-branches/ocaml_3_04/theories/itt/itt_squiggle.prla
+3362 -3176 metaprl-branches/ocaml_3_04/theories/itt/itt_struct.prla
+3974 -3988 metaprl-branches/ocaml_3_04/theories/itt/itt_struct2.prla
+244 -256 metaprl-branches/ocaml_3_04/theories/itt/itt_struct3.prla
+2253 -2224 metaprl-branches/ocaml_3_04/theories/itt/itt_subtype.prla
+272 -290 metaprl-branches/ocaml_3_04/theories/itt/itt_tsquash.prla
+292 -312 metaprl-branches/ocaml_3_04/theories/itt/itt_tunion.prla
+3014 -3122 metaprl-branches/ocaml_3_04/theories/itt/itt_union.prla
+1004 -1763 metaprl-branches/ocaml_3_04/theories/itt/itt_unit.prla
+860 -1239 metaprl-branches/ocaml_3_04/theories/itt/itt_void.prla
+1254 -1247 metaprl-branches/ocaml_3_04/theories/itt/itt_w.prla
+853 -1112 metaprl-branches/ocaml_3_04/theories/itt/itt_well_founded.prla
+1 -1 metaprl-branches/ocaml_3_04/util/Makefile

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-07 15:16:47 -0700 (Tue, 07 May 2002)
Revision: 3605
Log message:

      *** empty log message ***
      

Changes  Path
+1 -1 metaprl-branches/ocaml_3_04/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+15 -7 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+3 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.mli
+3 -3 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_deadcode.ml
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_deadcode.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-07 15:17:49 -0700 (Tue, 07 May 2002)
Revision: 3606
Log message:

      Forgot to add these 2 files in the last commit.
      

Changes  Path
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.ml
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.ml
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.mli
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.mli

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-07 16:43:08 -0700 (Tue, 07 May 2002)
Revision: 3607
Log message:

      Removed the tactic equalSubsetT, since it is the same as setExtT defined
      in Czf_itt_member. Reproved related theorems.
      Also removed some comments.
      

Changes  Path
+138 -34 metaprl/theories/czf/czf_itt_ker.ml
+65 -0 metaprl/theories/czf/czf_itt_ker.mli
+12165 -8941 metaprl/theories/czf/czf_itt_ker.prla
+9 -22 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+56 -0 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+654 -1124 metaprl/theories/czf/czf_itt_normal_subgroup.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-07 16:45:06 -0700 (Tue, 07 May 2002)
Revision: 3608
Log message:

      Minor change in comments.
      

Changes  Path
+0 -7 metaprl/theories/czf/czf_itt_normal_subgroup.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-08 13:31:36 -0700 (Wed, 08 May 2002)
Revision: 3609
Log message:

      - Changed the top_bookmark implementation to make it more explicit that
      it's always the same bookmark.
      
      - The apply_rewrite now expects a bookmark as its input (Brian, is that OK?)
      There are 3 ways of getting a bookmark:
      1) Use ("Theory", "rule") for a bookmark pointing right *before*
      a rule (rewrite) is defined.
      2) Use Mp_resource.theory_bookmark "Theory" for a bookmark
      pointing at the end of the theory
      3) Use let _ = Mp_resource.bookmark "foo" in a theory to create a bookmark and
      then refer to it as ("Theory", "foo")
      

Changes  Path
+4 -7 metaprl-branches/ocaml_3_04/editor/ml/shell_state.ml
+7 -9 metaprl-branches/ocaml_3_04/filter/boot/rewrite_boot.ml
+2 -2 metaprl-branches/ocaml_3_04/filter/boot/tactic_boot_sig.mlz
+23 -12 metaprl-branches/ocaml_3_04/refiner/reflib/mp_resource.ml
+4 -2 metaprl-branches/ocaml_3_04/refiner/reflib/mp_resource.mli
+1 -1 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-08 15:45:05 -0700 (Wed, 08 May 2002)
Revision: 3610
Log message:

      Just testing my write access... Sorry.
      

Changes  Path
+0 -7 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.mli

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-08 16:05:55 -0700 (Wed, 08 May 2002)
Revision: 3611
Log message:

      For the comment purposes.
      

Changes  Path
+297 -1 metaprl/theories/czf/czf_itt_comment.ml
+66 -0 metaprl/theories/czf/czf_itt_comment.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-08 16:09:34 -0700 (Wed, 08 May 2002)
Revision: 3612
Log message:

      Separated preFIR term declarations.
      

Changes  Path
+1 -15 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.ml
+3 -3 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.mli
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos_exp.ml
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos_exp.ml
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos_exp.mli
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos_exp.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-08 19:59:34 -0700 (Wed, 08 May 2002)
Revision: 3613
Log message:

      Okay, a few little changes here:
      1) Many references to the MC compiler have been
         changed to MCC (it's new name).  I'm still
         calling this theory MC.
      2) Adding new files to split FIR term definitions even further.
         The "prog" files will contain terms necessary to define
         the overal structure of an FIR program, e.g. function definitions.
      3) Updating Mp_mc_compile to use the updated apply_rewrite mechanism.
         The bookmarks seem to be working out okay.
      

Changes  Path
+6 -3 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+3 -1 metaprl-branches/ocaml_3_04/theories/mc/Makefile
+18 -18 metaprl-branches/ocaml_3_04/theories/mc/README
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/TODO
+20 -12 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+10 -5 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.mli
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_base.ml
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_base.mli
+2 -20 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_exp.ml
+2 -7 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_exp.mli
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_prog.ml
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_prog.ml
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_prog.mli
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_prog.mli
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_ty.ml
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_ty.mli
+3 -3 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_const_elim.ml
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_const_elim.mli
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_deadcode.ml
+0 -24 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_exp.ml
+0 -11 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_exp.mli
+2 -8 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.mli
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.ml
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.ml
Added metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.mli
Properties metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.mli
+4 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_theory.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-08 20:57:43 -0700 (Wed, 08 May 2002)
Revision: 3614
Log message:

      This should be a no-op commit. I've rearranged the code in filter_ocaml.ml
      to make it compile faster. This reduces the native code compilation time:
      this file - 1/3
      whole MetaPRL -  9%
      

Changes  Path
+1088 -1042 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.ml
+0 -1 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.mli
+27 -27 metaprl-branches/ocaml_3_04/mk/rules

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-08 21:09:52 -0700 (Wed, 08 May 2002)
Revision: 3615
Log message:

      Updating Makefile to reflect new files.
      

Changes  Path
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/Makefile

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 14:08:38 -0700 (Thu, 09 May 2002)
Revision: 3616
Log message:

      -  Adding another program for testing purposes.
      -  MC_ROOT has been replaced by MCC_ROOT (in keeping with
         the name change of MC to MCC).
      -  Changing error reporting in mp_mc_connect_* to
         be more informative.
      

Changes  Path
+4 -4 metaprl-branches/ocaml_3_04/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/README
+4 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+29 -34 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_base.ml
+6 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_base.mli
+125 -135 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_exp.ml
+4 -4 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_prog.ml
+3 -6 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_ty.ml
+4 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_const_elim.ml
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_deadcode.ml
+5 -2 metaprl-branches/ocaml_3_04/theories/mc/tests/Conscript
Added metaprl-branches/ocaml_3_04/theories/mc/tests/mp_mc_test.ml
Properties metaprl-branches/ocaml_3_04/theories/mc/tests/mp_mc_test.ml
Added metaprl-branches/ocaml_3_04/theories/mc/tests/mp_mc_test.mli
Properties metaprl-branches/ocaml_3_04/theories/mc/tests/mp_mc_test.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 16:10:31 -0700 (Thu, 09 May 2002)
Revision: 3617
Log message:

      Okay, this is somewhat major change for those of you using cons to build
      MetaPRL.
      
      If you want to build MetaPRL by itself, you should use make.  cons support for
      building MetaPRL by itself is being removed.
      
      The Conscripts now exist only to build MCC and MetaPRL together.  The procedure
      is that you download the MCC and MetaPRL sources, and then configure MCC
      appropriately (it has directions) for including MetaPRL in the build, and then
      run cons from the top level directory of MCC. Trying to run cons from
      anywhere within the MetaPRL sources should result in an error.
      
      This change allows for a few simplifications of the build system. In
      particular, these silly MP_ROOT and MCC_ROOT environment variables should no
      longer matter.  (They're a bit of a kludge and hack to begin with.)
      

Changes  Path
Deleted metaprl-branches/ocaml_3_04/Conscript
Deleted metaprl-branches/ocaml_3_04/Construct
+11 -24 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+2 -5 metaprl-branches/ocaml_3_04/theories/mc/README

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 17:14:53 -0700 (Thu, 09 May 2002)
Revision: 3618
Log message:

      Fixing the Conscript so that it actually builds some files.
      (-:
      

Changes  Path
+3 -5 metaprl-branches/ocaml_3_04/theories/mc/Conscript

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-09 18:58:07 -0700 (Thu, 09 May 2002)
Revision: 3619
Log message:

      Apply reduceC to term...
      

Changes  Path
+2 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+18 -18 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.ml
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_theory.mlz

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-09 21:50:05 -0700 (Thu, 09 May 2002)
Revision: 3620
Log message:

      Working on adding the terms and conversion
      functions needed to represent entire
      MCC FIR programs.
      

Changes  Path
+5 -1 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+1 -1 metaprl-branches/ocaml_3_04/theories/mc/TODO
+2 -2 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+51 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_base.ml
+9 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_connect_base.mli
+24 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_base.ml
+13 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_base.mli
+43 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.ml
+38 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.mli

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-10 02:18:31 -0700 (Fri, 10 May 2002)
Revision: 3621
Log message:

      Changed the definition for cosets from set builder to separation.
      The previous definition was wrong.
      Updated proofs wherever coset occurred.
      

Changes  Path
+6 -6 metaprl/theories/czf/czf_itt_comment.ml
+2 -2 metaprl/theories/czf/czf_itt_comment.mli
+3201 -1788 metaprl/theories/czf/czf_itt_comment.prla
+158 -21 metaprl/theories/czf/czf_itt_coset.ml
+51 -2 metaprl/theories/czf/czf_itt_coset.mli
+5203 -596 metaprl/theories/czf/czf_itt_coset.prla
+38 -24 metaprl/theories/czf/czf_itt_ker.ml
+7594 -6918 metaprl/theories/czf/czf_itt_ker.prla
+96 -7 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+3167 -814 metaprl/theories/czf/czf_itt_normal_subgroup.prla

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-11 01:38:00 -0700 (Sat, 11 May 2002)
Revision: 3622
Log message:

      Phobos returns a term and a list of (term*term) pairs that represent
      simple rewrites.
      

Changes  Path
+1 -0 metaprl-branches/ocaml_3_04/theories/mc/Conscript
+5 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+2 -1 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.mli

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-11 03:57:52 -0700 (Sat, 11 May 2002)
Revision: 3623
Log message:

      Finished the comment part.
      

Changes  Path
+93 -3 metaprl/theories/czf/czf_itt_abel_group.ml
+44 -3 metaprl/theories/czf/czf_itt_abel_group.mli
+2440 -431 metaprl/theories/czf/czf_itt_abel_group.prla
+125 -2 metaprl/theories/czf/czf_itt_cyclic_group.ml
+50 -0 metaprl/theories/czf/czf_itt_cyclic_group.mli
+3277 -596 metaprl/theories/czf/czf_itt_cyclic_group.prla
+159 -10 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+51 -2 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+4148 -760 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+310 -74 metaprl/theories/czf/czf_itt_equiv.ml
+42 -5 metaprl/theories/czf/czf_itt_equiv.mli
+9377 -4275 metaprl/theories/czf/czf_itt_equiv.prla
+219 -19 metaprl/theories/czf/czf_itt_group.ml
+56 -6 metaprl/theories/czf/czf_itt_group.mli
+6453 -1681 metaprl/theories/czf/czf_itt_group.prla
+105 -5 metaprl/theories/czf/czf_itt_group_bvd.ml
+44 -0 metaprl/theories/czf/czf_itt_group_bvd.mli
+3138 -317 metaprl/theories/czf/czf_itt_group_bvd.prla
+214 -28 metaprl/theories/czf/czf_itt_hom.ml
+59 -0 metaprl/theories/czf/czf_itt_hom.mli
+5260 -751 metaprl/theories/czf/czf_itt_hom.prla
+104 -1 metaprl/theories/czf/czf_itt_inv_image.ml
+46 -2 metaprl/theories/czf/czf_itt_inv_image.mli
+2809 -377 metaprl/theories/czf/czf_itt_inv_image.prla
+91 -15 metaprl/theories/czf/czf_itt_iso.ml
+44 -5 metaprl/theories/czf/czf_itt_iso.mli
+2398 -366 metaprl/theories/czf/czf_itt_iso.prla
+115 -2 metaprl/theories/czf/czf_itt_set_bvd.ml
+44 -0 metaprl/theories/czf/czf_itt_set_bvd.mli
+3169 -391 metaprl/theories/czf/czf_itt_set_bvd.prla
+146 -12 metaprl/theories/czf/czf_itt_subgroup.ml
+52 -1 metaprl/theories/czf/czf_itt_subgroup.mli
+3846 -572 metaprl/theories/czf/czf_itt_subgroup.prla

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-11 11:28:23 -0700 (Sat, 11 May 2002)
Revision: 3624
Log message:

      Added "input forms" that are the input analogy to display forms.
      
      An iform is declared exactly like a rewrite.  An example:
      
         declare junk{'t}
         declare magic[v:s]{'t}
         iform bind : junk{magic[x:s]{'t}} <--> lambda{x. 't}
      
         # test_rewrite bind << junk{magic[y:s]{.'y +@ 1}} >>;;
         - lambda{y.y +@ 1} : term
      
      The difference is this: iforms use the rewriter in Relaxed mode,
      where capture is allowed.  The rewrites have no logical meaning;
      the refiner will not allow you to use one in a proof.  However,
      they are otherwise normal conversions, and you can add them
      to resources etc.
      
      Also, I added a function
      
      val Top_conversionals.create_iform : string -> term -> term -> conv
      
      This will allow us to create rewrites on the fly.  I added example
      code to mp_mc_compile to illustrate, but I don't know how to
      test it.
      
      Adam, you should probably change all rewrites in Mp_mc_fir_phobos to
      iforms.  Don't use magic (remove that sample code I added).  The rewrites
      should work as they are written now.
      

Changes  Path
+3 -0 metaprl-branches/ocaml_3_04/editor/ml/shell.ml
+64 -0 metaprl-branches/ocaml_3_04/filter/base/filter_prog.ml
+80 -16 metaprl-branches/ocaml_3_04/filter/base/filter_summary.ml
+1 -0 metaprl-branches/ocaml_3_04/filter/base/filter_type.ml
+1 -0 metaprl-branches/ocaml_3_04/filter/boot/conversionals_boot.ml
+7 -0 metaprl-branches/ocaml_3_04/filter/boot/rewrite_boot.ml
+13 -1 metaprl-branches/ocaml_3_04/filter/boot/tactic_boot_sig.mlz
+30 -0 metaprl-branches/ocaml_3_04/filter/filter/filter_parse.ml
+7 -3 metaprl-branches/ocaml_3_04/filter/filter/prlcomp.ml
+42 -5 metaprl-branches/ocaml_3_04/refiner/refiner/refine.ml
+5 -0 metaprl-branches/ocaml_3_04/refiner/refsig/refine_sig.ml
+2 -1 metaprl-branches/ocaml_3_04/refiner/rewrite/rewrite_build_contractum.ml
+8 -6 metaprl-branches/ocaml_3_04/refiner/rewrite/rewrite_compile_contractum.ml
+28 -6 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml
+10 -4 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.ml
+2 -4 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_phobos.mli
+2 -0 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.ml
+1 -0 metaprl-branches/ocaml_3_04/theories/tactic/top_conversionals.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-11 17:15:35 -0700 (Sat, 11 May 2002)
Revision: 3625
Log message:

      More structural changes to speed up compilation.
      
      Now "make opt" (after "make clean", but with .prlb already there) works even
      faster than it used to before 3.02 -> 3.04 switch.
      

Changes  Path
+1514 -1520 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.ml
+0 -12 metaprl-branches/ocaml_3_04/filter/base/filter_ocaml.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-11 18:45:04 -0700 (Sat, 11 May 2002)
Revision: 3626
Log message:

      Print those rewrites that we get from Phobos. Just a copy of what I have
      before I leave, feel free to get rid of the changes.
       ----------------------------------------------------------------------
      

Changes  Path
+13 -4 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_compile.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-11 21:56:01 -0700 (Sat, 11 May 2002)
Revision: 3627
Log message:

      Adding some minimal display forms.
      

Changes  Path
+93 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.ml
+11 -0 metaprl-branches/ocaml_3_04/theories/mc/mp_mc_fir_prog.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-12 09:48:45 -0700 (Sun, 12 May 2002)
Revision: 3628
Log message:

      Merging the ocaml_3_04 branch.
      
      The major changes in this commit are:
      
      - Switch to OCaml+CamlP4 version 3.04
      - Many cons changes (in particular, cons now only supports mcc+MetaPRL,
      but does not support standalone MetaPRL).
      - Added partial support for "input forms" that are the input analogy to display forms.
      - Added apply_rewrite function.
      - Updated Mp_mc_compile to use the updated apply_rewrite mechanism.
      - Changed the top_bookmark implementation to make it more explicit that
      it's always the same bookmark.
      - Filter_ocaml unmarshaling for str_items now fails softly.  If the
      term format changes, you may get a warning asking you to regenerate
      the .prla files.
      - Filter_ocaml was significantly restructured to speed up the compilation.
      

Changes  Path
Deleted metaprl/Conscript
Deleted metaprl/Construct
+0 -0 metaprl/clib/Conscript
+3 -3 metaprl/editor/ml/Conscript
+3 -0 metaprl/editor/ml/shell.ml
+4 -7 metaprl/editor/ml/shell_state.ml
+1 -1 metaprl/ensemble/Conscript
+2 -2 metaprl/filter/base/Conscript
+1 -2 metaprl/filter/base/filter_cache.ml
+9 -3 metaprl/filter/base/filter_comment.ml
+33 -9 metaprl/filter/base/filter_hash.ml
+1659 -1510 metaprl/filter/base/filter_ocaml.ml
+4 -13 metaprl/filter/base/filter_ocaml.mli
+64 -0 metaprl/filter/base/filter_prog.ml
+81 -45 metaprl/filter/base/filter_summary.ml
+1 -0 metaprl/filter/base/filter_type.ml
+1 -1 metaprl/filter/base/free_vars.ml
+34 -13 metaprl/filter/base/mLast_util.ml
+2 -2 metaprl/filter/boot/Conscript
+5 -0 metaprl/filter/boot/conversionals_boot.ml
+19 -0 metaprl/filter/boot/rewrite_boot.ml
+16 -0 metaprl/filter/boot/tactic_boot.ml
+24 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+11 -11 metaprl/filter/filter/Conscript
+30 -0 metaprl/filter/filter/filter_parse.ml
+7 -3 metaprl/filter/filter/prlcomp.ml
+1 -1 metaprl/library/Conscript
+3 -3 metaprl/mk/preface
+27 -27 metaprl/mk/rules
+1 -1 metaprl/mllib/Conscript
+1 -1 metaprl/refiner/refbase/Conscript
+1 -1 metaprl/refiner/refiner/Conscript
+42 -5 metaprl/refiner/refiner/refine.ml
+1 -1 metaprl/refiner/reflib/Conscript
+23 -12 metaprl/refiner/reflib/mp_resource.ml
+4 -2 metaprl/refiner/reflib/mp_resource.mli
+1 -1 metaprl/refiner/refsig/Conscript
+5 -0 metaprl/refiner/refsig/refine_sig.ml
+1 -1 metaprl/refiner/rewrite/Conscript
+2 -1 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+8 -6 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+1 -1 metaprl/refiner/term_ds/Conscript
+1 -1 metaprl/refiner/term_gen/Conscript
+1 -1 metaprl/refiner/term_std/Conscript
+1 -1 metaprl/theories/Conscript
+1 -1 metaprl/theories/base/Conscript
+1 -1 metaprl/theories/itt/Conscript
+353 -417 metaprl/theories/itt/ctt_markov.prla
+1538 -1484 metaprl/theories/itt/itt_bisect.prla
+4714 -4705 metaprl/theories/itt/itt_bool.prla
+517 -365 metaprl/theories/itt/itt_bunion.prla
+573 -573 metaprl/theories/itt/itt_collection.prla
+71 -71 metaprl/theories/itt/itt_decidable.prla
+2749 -2997 metaprl/theories/itt/itt_derive.prla
+1389 -1764 metaprl/theories/itt/itt_dfun.prla
+869 -890 metaprl/theories/itt/itt_disect.prla
+3078 -3479 metaprl/theories/itt/itt_dprod.prla
+4418 -4468 metaprl/theories/itt/itt_equal.prla
+60 -57 metaprl/theories/itt/itt_esquash.prla
+292 -311 metaprl/theories/itt/itt_ext_equal.prla
+3695 -3691 metaprl/theories/itt/itt_fset.prla
+1777 -1764 metaprl/theories/itt/itt_fun.prla
+215 -212 metaprl/theories/itt/itt_int_arith.prla
+3146 -3376 metaprl/theories/itt/itt_int_base.prla
+4823 -4775 metaprl/theories/itt/itt_int_ext.prla
+1287 -1395 metaprl/theories/itt/itt_isect.prla
+2343 -2429 metaprl/theories/itt/itt_list.prla
+2306 -2295 metaprl/theories/itt/itt_list2.prla
+15759 -15855 metaprl/theories/itt/itt_logic.prla
+2204 -2378 metaprl/theories/itt/itt_nat.prla
+271 -531 metaprl/theories/itt/itt_pointwise.prla
+286 -247 metaprl/theories/itt/itt_pointwise2.prla
+823 -1343 metaprl/theories/itt/itt_prod.prla
+637 -918 metaprl/theories/itt/itt_prop_decide.prla
+2162 -1758 metaprl/theories/itt/itt_quotient.prla
+395 -395 metaprl/theories/itt/itt_record.prla
+331 -316 metaprl/theories/itt/itt_record0.prla
+1081 -1088 metaprl/theories/itt/itt_record_exm.prla
+1482 -1724 metaprl/theories/itt/itt_record_label.prla
+638 -928 metaprl/theories/itt/itt_record_label0.prla
+5537 -6032 metaprl/theories/itt/itt_rfun.prla
+525 -525 metaprl/theories/itt/itt_sort.prla
+8719 -8029 metaprl/theories/itt/itt_squash.prla
+5338 -2171 metaprl/theories/itt/itt_squiggle.prla
+3362 -3176 metaprl/theories/itt/itt_struct.prla
+3974 -3988 metaprl/theories/itt/itt_struct2.prla
+244 -256 metaprl/theories/itt/itt_struct3.prla
+2253 -2224 metaprl/theories/itt/itt_subtype.prla
+272 -290 metaprl/theories/itt/itt_tsquash.prla
+292 -312 metaprl/theories/itt/itt_tunion.prla
+3014 -3122 metaprl/theories/itt/itt_union.prla
+1004 -1763 metaprl/theories/itt/itt_unit.prla
+860 -1239 metaprl/theories/itt/itt_void.prla
+1254 -1247 metaprl/theories/itt/itt_w.prla
+853 -1112 metaprl/theories/itt/itt_well_founded.prla
+17 -24 metaprl/theories/mc/Conscript
+3 -1 metaprl/theories/mc/Makefile
+18 -21 metaprl/theories/mc/README
+3 -3 metaprl/theories/mc/TODO
+72 -10 metaprl/theories/mc/mp_mc_compile.ml
+12 -4 metaprl/theories/mc/mp_mc_compile.mli
+82 -37 metaprl/theories/mc/mp_mc_connect_base.ml
+17 -3 metaprl/theories/mc/mp_mc_connect_base.mli
+127 -155 metaprl/theories/mc/mp_mc_connect_exp.ml
+2 -7 metaprl/theories/mc/mp_mc_connect_exp.mli
Added metaprl/theories/mc/mp_mc_connect_prog.ml
Properties metaprl/theories/mc/mp_mc_connect_prog.ml
Added metaprl/theories/mc/mp_mc_connect_prog.mli
Properties metaprl/theories/mc/mp_mc_connect_prog.mli
+5 -8 metaprl/theories/mc/mp_mc_connect_ty.ml
+2 -2 metaprl/theories/mc/mp_mc_connect_ty.mli
+6 -3 metaprl/theories/mc/mp_mc_const_elim.ml
+1 -1 metaprl/theories/mc/mp_mc_const_elim.mli
+3 -3 metaprl/theories/mc/mp_mc_deadcode.ml
+1 -1 metaprl/theories/mc/mp_mc_deadcode.mli
+24 -0 metaprl/theories/mc/mp_mc_fir_base.ml
+13 -0 metaprl/theories/mc/mp_mc_fir_base.mli
+0 -24 metaprl/theories/mc/mp_mc_fir_exp.ml
+0 -11 metaprl/theories/mc/mp_mc_fir_exp.mli
Added metaprl/theories/mc/mp_mc_fir_phobos.ml
Properties metaprl/theories/mc/mp_mc_fir_phobos.ml
Added metaprl/theories/mc/mp_mc_fir_phobos.mli
Properties metaprl/theories/mc/mp_mc_fir_phobos.mli
Added metaprl/theories/mc/mp_mc_fir_phobos_exp.ml
Properties metaprl/theories/mc/mp_mc_fir_phobos_exp.ml
Added metaprl/theories/mc/mp_mc_fir_phobos_exp.mli
Properties metaprl/theories/mc/mp_mc_fir_phobos_exp.mli
Added metaprl/theories/mc/mp_mc_fir_prog.ml
Properties metaprl/theories/mc/mp_mc_fir_prog.ml
Added metaprl/theories/mc/mp_mc_fir_prog.mli
Properties metaprl/theories/mc/mp_mc_fir_prog.mli
+4 -1 metaprl/theories/mc/mp_mc_theory.mlz
+8 -5 metaprl/theories/mc/tests/Conscript
Added metaprl/theories/mc/tests/mp_mc_test.ml
Properties metaprl/theories/mc/tests/mp_mc_test.ml
Added metaprl/theories/mc/tests/mp_mc_test.mli
Properties metaprl/theories/mc/tests/mp_mc_test.mli
+2 -2 metaprl/theories/ocaml/Conscript
+2 -2 metaprl/theories/tactic/Conscript
+14 -1 metaprl/theories/tactic/mptop.ml
+7 -0 metaprl/theories/tactic/top_conversionals.ml
+5 -0 metaprl/theories/tactic/top_conversionals.mli
+2 -2 metaprl/util/Makefile
+16 -15 metaprl/util/macro.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 02:05:14 -0700 (Mon, 13 May 2002)
Revision: 3630
Log message:

      Corrected the functionality axioms for the operation and inverse.
      

Changes  Path
+10 -12 metaprl/theories/czf/czf_itt_group.ml
+1808 -1820 metaprl/theories/czf/czf_itt_group.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 02:05:56 -0700 (Mon, 13 May 2002)
Revision: 3631
Log message:

      Updated the "pair_eq" rule to make it more powerful.
      

Changes  Path
+8 -0 metaprl/theories/czf/czf_itt_equiv.ml
+2238 -2021 metaprl/theories/czf/czf_itt_equiv.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 02:07:16 -0700 (Mon, 13 May 2002)
Revision: 3632
Log message:

      Added an example of group: the klein 4-group.
      It looks pretty ugly now and needs comments.
      

Changes  Path
+2 -1 metaprl/theories/czf/Makefile
Added metaprl/theories/czf/czf_itt_kleingroup.ml
Properties metaprl/theories/czf/czf_itt_kleingroup.ml
Added metaprl/theories/czf/czf_itt_kleingroup.mli
Properties metaprl/theories/czf/czf_itt_kleingroup.mli
Added metaprl/theories/czf/czf_itt_kleingroup.prla
Properties metaprl/theories/czf/czf_itt_kleingroup.prla

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-13 02:45:56 -0700 (Mon, 13 May 2002)
Revision: 3633
Log message:

      Cleaning up FIR evaluation / operational semantics.  The substantively new
      addition is that we can now evaluate matchExp's (match expressions).
      
      Adding a new conversional firExpEvalC (Mp_mc_fir_eval) which essentially
      evaluates any expression it can.  Essentially, this is firConstElimC, except
      this one works (at least on every example I've tried).  Again, since the MCC
      front ends do so much optimization, I don't know how well this works in
      general, but I do have evidence, based on the errors I had to fix during
      debugging, that it at least gets rid of a (pointless) idOp expression some
      where in MCC's mcc/test/fc/simple/fact.c.  (-:
      
      Granted, it can't evaluate much at the moment, but at least it's a start, and
      it should even be sufficient for the expressions in our power example.
      
      Take a look at theories/mc/tests/mp_mc_test.ml for some examples.
      
      Functions are still a problem at this point.
      

Changes  Path
+28 -12 metaprl/theories/mc/mp_mc_compile.ml
+8 -1 metaprl/theories/mc/mp_mc_compile.mli
+3 -5 metaprl/theories/mc/mp_mc_connect_base.ml
+12 -7 metaprl/theories/mc/mp_mc_const_elim.ml
+1 -0 metaprl/theories/mc/mp_mc_const_elim.mli
+2 -2 metaprl/theories/mc/mp_mc_deadcode.ml
+212 -29 metaprl/theories/mc/mp_mc_fir_eval.ml
+70 -10 metaprl/theories/mc/mp_mc_fir_eval.mli
+62 -11 metaprl/theories/mc/tests/mp_mc_test.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-13 09:23:26 -0700 (Mon, 13 May 2002)
Revision: 3634
Log message:

      Cleaning up idOp rewrites.  (I don't like how
      the previous set depended on which order you
      applied them in.)
      

Changes  Path
+22 -5 metaprl/theories/mc/mp_mc_fir_eval.ml
+4 -1 metaprl/theories/mc/mp_mc_fir_eval.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-13 09:36:54 -0700 (Mon, 13 May 2002)
Revision: 3635
Log message:

      Adding a simple test case that demonstrates a problem
      with the setSubscript term (and implicitly, others
      that represent imperative updates of values).
      

Changes  Path
+13 -2 metaprl/theories/mc/tests/mp_mc_test.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-13 15:52:10 -0700 (Mon, 13 May 2002)
Revision: 3636
Log message:

      Added comments.
      

Changes  Path
+28 -0 metaprl/theories/czf/czf_itt_comment.ml
+8 -0 metaprl/theories/czf/czf_itt_comment.mli
+664 -389 metaprl/theories/czf/czf_itt_comment.prla
+152 -28 metaprl/theories/czf/czf_itt_kleingroup.ml
+54 -5 metaprl/theories/czf/czf_itt_kleingroup.mli
+4491 -1324 metaprl/theories/czf/czf_itt_kleingroup.prla

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-14 17:32:40 -0700 (Tue, 14 May 2002)
Revision: 3640
Log message:

      Phobos iforms are finally working.
      This commit gets rid of all (iform-)rewrites that were in mp_mc_fir_phobos.ml,
      which were placed in fir.pho earlier.
      Turn on -metaprl_debug to see how the result is being manipulated.
      

Changes  Path
+17 -36 metaprl/theories/mc/mp_mc_compile.ml
+21 -101 metaprl/theories/mc/mp_mc_fir_phobos.ml
+2 -2 metaprl/theories/mc/mp_mc_fir_phobos.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-15 00:18:34 -0700 (Wed, 15 May 2002)
Revision: 3641
Log message:

      Minor comment modification in mp_mc_compile.
      
      I'm also committing two, real simple test cases in mp_mc_test.ml
      to convince myself the firDeadcodeC is working as expected.
      

Changes  Path
+1 -1 metaprl/theories/mc/mp_mc_compile.ml
+26 -1 metaprl/theories/mc/tests/mp_mc_test.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-15 01:27:02 -0700 (Wed, 15 May 2002)
Revision: 3642
Log message:

      Removing the mp_mc_fir_phobos* files from
      mp_mc_theory and updating the Makefile
      so that they don't get built as part of a build
      using "make".  (mp_mc_fir_phobos become dependent
      upon MCC)
      

Changes  Path
+0 -2 metaprl/theories/mc/Makefile
+0 -2 metaprl/theories/mc/mp_mc_theory.mlz

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-15 23:13:15 -0700 (Wed, 15 May 2002)
Revision: 3643
Log message:

      Changing fundef term declaration.  In particular, the argument
      and body subterms have been reduced to one subterm that should
      be some sort of lambda term.  connect_prog code needs to be updated
      to handle this new term, but it does compile.
      

Changes  Path
+6 -0 metaprl/theories/mc/mp_mc_connect_prog.ml
+7 -8 metaprl/theories/mc/mp_mc_fir_prog.ml
+3 -3 metaprl/theories/mc/mp_mc_fir_prog.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-15 23:21:53 -0700 (Wed, 15 May 2002)
Revision: 3644
Log message:

      Included Itt_list and Itt_list2 in Mp_mc_theory.
      Now, Phobos is passing a list of inline forms (as mp_pre_term list) as well.
      

Changes  Path
+8 -3 metaprl/theories/mc/mp_mc_compile.ml
+1 -1 metaprl/theories/mc/mp_mc_compile.mli
+7 -0 metaprl/theories/mc/mp_mc_fir_phobos.ml
+2 -0 metaprl/theories/mc/mp_mc_theory.mlz

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-16 00:08:09 -0700 (Thu, 16 May 2002)
Revision: 3645
Log message:

      Committing part one of inlining.  This is most of the
      basic terms and rewrites that will be needed.
      
      Remaining: given a inline target (a tailCall term),
      I should generate a rewrite to deal with it.  The
      current scheme in this commit can deal with an
      inline target, but not in a general way.
      (Where by general, I mean a general tailCall term.
      General purpose inlining is ways away still.)
      

Changes  Path
+1 -1 metaprl/theories/mc/Conscript
+1 -0 metaprl/theories/mc/Makefile
Added metaprl/theories/mc/mp_mc_inline.ml
Properties metaprl/theories/mc/mp_mc_inline.ml
Added metaprl/theories/mc/mp_mc_inline.mli
Properties metaprl/theories/mc/mp_mc_inline.mli
+1 -0 metaprl/theories/mc/mp_mc_theory.mlz
+43 -1 metaprl/theories/mc/tests/mp_mc_test.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-16 00:48:04 -0700 (Thu, 16 May 2002)
Revision: 3646
Log message:

      Defining groups does not really need equivalence relations, so I changed the group system by replacing equivalence relation with equality. Every occurance was modified and every related rule was reproved.
      
      Besides, separated the power operation for a group from the module Czf_itt_cyclic_subgroup.
      

Changes  Path
+1 -0 metaprl/theories/czf/Makefile
+2 -2 metaprl/theories/czf/czf_itt_abel_group.ml
+1 -1 metaprl/theories/czf/czf_itt_abel_group.mli
+2720 -2783 metaprl/theories/czf/czf_itt_abel_group.prla
+26 -37 metaprl/theories/czf/czf_itt_coset.ml
+3 -3 metaprl/theories/czf/czf_itt_coset.mli
+4661 -5820 metaprl/theories/czf/czf_itt_coset.prla
+3912 -3983 metaprl/theories/czf/czf_itt_cyclic_group.prla
+9 -114 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+2 -7 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+4310 -15346 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+116 -171 metaprl/theories/czf/czf_itt_group.ml
+0 -5 metaprl/theories/czf/czf_itt_group.mli
+8760 -10938 metaprl/theories/czf/czf_itt_group.prla
+10 -18 metaprl/theories/czf/czf_itt_group_bvd.ml
+2 -4 metaprl/theories/czf/czf_itt_group_bvd.mli
+3344 -3722 metaprl/theories/czf/czf_itt_group_bvd.prla
Added metaprl/theories/czf/czf_itt_group_power.ml
Properties metaprl/theories/czf/czf_itt_group_power.ml
Added metaprl/theories/czf/czf_itt_group_power.mli
Properties metaprl/theories/czf/czf_itt_group_power.mli
Added metaprl/theories/czf/czf_itt_group_power.prla
Properties metaprl/theories/czf/czf_itt_group_power.prla
+13 -24 metaprl/theories/czf/czf_itt_hom.ml
+1 -1 metaprl/theories/czf/czf_itt_hom.mli
+11946 -13211 metaprl/theories/czf/czf_itt_hom.prla
+1 -11 metaprl/theories/czf/czf_itt_iso.ml
+1 -1 metaprl/theories/czf/czf_itt_iso.mli
+4023 -4860 metaprl/theories/czf/czf_itt_iso.prla
+23 -23 metaprl/theories/czf/czf_itt_ker.ml
+3 -3 metaprl/theories/czf/czf_itt_ker.mli
+12700 -15057 metaprl/theories/czf/czf_itt_ker.prla
+37 -66 metaprl/theories/czf/czf_itt_kleingroup.ml
+2 -2 metaprl/theories/czf/czf_itt_kleingroup.mli
+9198 -13326 metaprl/theories/czf/czf_itt_kleingroup.prla
+2 -3 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+0 -1 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+4166 -4173 metaprl/theories/czf/czf_itt_normal_subgroup.prla
+29 -32 metaprl/theories/czf/czf_itt_subgroup.ml
+1 -2 metaprl/theories/czf/czf_itt_subgroup.mli
+5623 -7492 metaprl/theories/czf/czf_itt_subgroup.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-16 00:48:39 -0700 (Thu, 16 May 2002)
Revision: 3647
Log message:

      Forgot these in the last commit.
      

Changes  Path
+35 -39 metaprl/theories/czf/czf_itt_comment.ml
+12 -10 metaprl/theories/czf/czf_itt_comment.mli
+773 -826 metaprl/theories/czf/czf_itt_comment.prla

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-16 00:54:07 -0700 (Thu, 16 May 2002)
Revision: 3648
Log message:

      Implementing the fundef conversion code correctly now.
      Preemptive bug fixes to mp_mc_inline.
      

Changes  Path
+24 -11 metaprl/theories/mc/mp_mc_connect_prog.ml
+9 -0 metaprl/theories/mc/mp_mc_inline.ml
+2 -0 metaprl/theories/mc/mp_mc_inline.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-16 14:10:58 -0700 (Thu, 16 May 2002)
Revision: 3649
Log message:

      Committing the 2nd part of the inling code I've written.
      I'm not sure if it works since Phobos cannot properly generate
      string / token terms yet.  Other than that, the only other
      real piece of remaining work is to take the term injected
      through the Phobos path and get it back to MCC for further
      compilation.
      

Changes  Path
+62 -12 metaprl/theories/mc/mp_mc_compile.ml
+38 -1 metaprl/theories/mc/mp_mc_inline.ml
+12 -0 metaprl/theories/mc/mp_mc_inline.mli
+15 -1 metaprl/theories/mc/tests/mp_mc_test.ml

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 16:12:45 -0700 (Thu, 16 May 2002)
Revision: 3650
Log message:

      Correcting hard-coded paths in the Conscript files which prevent successful
      compilation of MetaPRL for those of us with nonstandard ocaml installs. The
      paths are currently stored in the top-level Conscript in MCC, and are auto-
      detected by the configure script there.
      

Changes  Path
+6 -3 metaprl/clib/Conscript
+2 -2 metaprl/editor/ml/Conscript
+1 -1 metaprl/filter/base/Conscript
+1 -1 metaprl/filter/boot/Conscript
+2 -2 metaprl/filter/filter/Conscript
+2 -2 metaprl/theories/mc/tests/Conscript
+1 -1 metaprl/theories/ocaml/Conscript
+1 -1 metaprl/theories/tactic/Conscript

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-16 16:42:43 -0700 (Thu, 16 May 2002)
Revision: 3651
Log message:

      We also have 7.x RPMs.
      

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

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-16 17:54:21 -0700 (Thu, 16 May 2002)
Revision: 3652
Log message:

      Allowed string->token and string->number parameter conversion in
      Relaxed mode. Feel free to correct it if I missed something.
      

Changes  Path
+2 -0 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+9 -3 metaprl/refiner/rewrite/rewrite_compile_contractum.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-16 17:57:23 -0700 (Thu, 16 May 2002)
Revision: 3653
Log message:

      Changed tailCall to tailCall_com.
      

Changes  Path
+2 -1 metaprl/theories/mc/mp_mc_compile.ml
+1 -1 metaprl/theories/mc/mp_mc_fir_phobos_exp.ml

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 18:19:57 -0700 (Thu, 16 May 2002)
Revision: 3654
Log message:

      Removing hard-coded stuff from util/Conscript; this information is all
      available from the parent Conscript and computed by MCC's configure now.
      

Changes  Path
+15 -14 metaprl/util/Conscript

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-16 18:42:37 -0700 (Thu, 16 May 2002)
Revision: 3655
Log message:

      Added itt_collection to theories.pdf
      

Changes  Path
+1 -1 metaprl/doc/latex/theories/itt/print.ml
+26 -13 metaprl/theories/itt/itt_collection.ml
+10 -0 texinputs/metaprl.bib

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-16 18:51:49 -0700 (Thu, 16 May 2002)
Revision: 3656
Log message:

      Forgot to update mp_mc_fir_phobos_exp.mli with the tailCall change.
      

Changes  Path
+1 -1 metaprl/theories/mc/mp_mc_fir_phobos_exp.mli

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-16 18:58:35 -0700 (Thu, 16 May 2002)
Revision: 3657
Log message:

      Change the grammar for terms a little bit.
      
      Now the grammar understands
      (1) Expression for records:
          - Record types:
              {x:A; y:B; ... z:C}
          - Records
              {x=a; y=b; ... z=c}
          - Field selections:
              r^x
            where x,y,z are words or strings, A,B,C,a,b,c,r are terms.
          Actually type {x_1:A_1;x_2:A_2;...x_n:A_n} is a depend typed record.
          It bounds the variable "self" inside terms A_2, ..., A_n. The type of
          self in A_k is {x_1:A_1, ..., x_k-1:A_k-1}. So, you can write, e.g.,
              {car : univ[l:l];
               "*" : 'self^car -> 'self^car -> 'self^car
              }
          This form a type that contains, for example,
              {car = int;
               "*" = lambda{x.lambda{y. 'x+@ 'y}}
              }
      
      (2) Syntax sugar for self.
          You may omit self, in the expressions like self^x.
          That is, you can write ^x instead of self^x.
          So, the following type is equivalent to the previous one.
              {car : univ[l:l];
               "*" : ^car -> ^car -> ^car
              }
      
      (3) Binary operations ^*, ^+, ^=, ^/, ^-, ^<, ^> ,^<>
             x ^* y  stands for  self^"*" x y
             x ^= y  stands for  self^"=" x y
          and so on.
          So you may write
          {car : univ[l:l];
           "*" : ^car -> ^car -> ^car;
           axm : all x,y,z : ^car. ('x ^* 'y) ^* 'z = 'x ^* ('y ^* 'z) in ^car
          }
      
      (4) Let and with operators.
          Now (let x=term1 in term2) and (term2 where x=term1) are both expression for
          the let{term1;x.term2} term defined now in itt_rfun.
      
      (5) Open operators.
              (open e1 in e2) stands for (let self=e1 in e2)
              (forany T. e) stands for (all self:T. e)
              (thereis T. e) stands for (exsts self:T. e)
          So you may write something like this
              open 'g in 'x ^* ^y ^* 'z
              forany group.  all 'x in ^car. 'x ^* ^e = 'x in ^car
      
      (6) Changed associativity and priority of some operators.
          Now the priority is the following (from the lowest priority):
              - operators like if-then-else and let
              - logical operators (in usual order)
              - relations (first =,in,~, then all other relations)
              - type and arithmetic operators in usual order
              - application
              - record field selection
          For example
              'x in 'y and 'z stands for ('x in 'y) and 'z
          but
              'x in 'y * 'z stands for 'x in ('y * 'z)
          I think this is natural.
      
      Corrected a couple of proofs that was broken.
      
      TODO:
        - make sure that display forms respect the new grammar.
      

Changes  Path
+160 -70 metaprl/filter/base/term_grammar.ml
+141 -141 metaprl/theories/czf/czf_itt_group_power.prla
+149 -149 metaprl/theories/itt/ctt_markov.prla
+1 -1 metaprl/theories/itt/itt_record.ml
+1 -0 metaprl/theories/itt/itt_rfun.ml
+1 -0 metaprl/theories/itt/itt_rfun.mli

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 21:25:38 -0700 (Thu, 16 May 2002)
Revision: 3658
Log message:

                                     ***WARNING***
      Building MCC with MetaPRL support will fail without the corresponding patch
      to MCC (just committed).  See the commit message for MCC for details.
                                     ***WARNING***
      
      Revising the build system to support the situation where $env->{MP} is a
      relative path.  A new variable, $env->{MP_HASH}, is the value of MP with a
      # prepended when MP is relative.  These changes are necessary to support
      a symlink pointing from MCC to the MetaPRL source tree.
      

Changes  Path
+2 -2 metaprl/debug/Conscript
+22 -22 metaprl/editor/ml/Conscript
+3 -3 metaprl/ensemble/Conscript
+11 -11 metaprl/filter/Conscript
+1 -1 metaprl/filter/boot/Conscript
+3 -3 metaprl/filter/filter/Conscript
+15 -12 metaprl/lib/Conscript
+4 -4 metaprl/library/Conscript
+2 -2 metaprl/mllib/Conscript
+2 -2 metaprl/refiner/Conscript
+1 -1 metaprl/refiner/refiner/Conscript
+1 -1 metaprl/refiner/term_ds/Conscript
+1 -1 metaprl/refiner/term_gen/Conscript
+14 -14 metaprl/theories/Conscript
+4 -4 metaprl/theories/mc/Conscript
+1 -1 metaprl/theories/mc/tests/Conscript
+5 -5 metaprl/theories/tactic/Conscript

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-16 22:44:41 -0700 (Thu, 16 May 2002)
Revision: 3659
Log message:

      Removing default targets from Conscript files.  Those of you on MCC,
      see the next MCC commit for how to get these back.
      

Changes  Path
+1 -1 metaprl/clib/Conscript
+1 -1 metaprl/debug/Conscript
+1 -1 metaprl/editor/ml/Conscript
+1 -1 metaprl/ensemble/Conscript
+1 -1 metaprl/filter/base/Conscript
+1 -1 metaprl/filter/boot/Conscript
+1 -1 metaprl/filter/filter/Conscript
+1 -1 metaprl/lib/Conscript
+1 -1 metaprl/library/Conscript
+1 -1 metaprl/mllib/Conscript
+1 -1 metaprl/refiner/refbase/Conscript
+1 -1 metaprl/refiner/refiner/Conscript
+1 -1 metaprl/refiner/reflib/Conscript
+2 -2 metaprl/refiner/refsig/Conscript
+1 -1 metaprl/refiner/rewrite/Conscript
+1 -1 metaprl/refiner/term_ds/Conscript
+1 -1 metaprl/refiner/term_gen/Conscript
+1 -1 metaprl/refiner/term_std/Conscript
+1 -1 metaprl/theories/base/Conscript
+1 -1 metaprl/theories/itt/Conscript
+1 -1 metaprl/theories/mc/Conscript
+1 -1 metaprl/theories/mc/tests/Conscript
+1 -1 metaprl/theories/ocaml/Conscript
+1 -1 metaprl/theories/tactic/Conscript
+1 -1 metaprl/util/Conscript

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-17 10:36:48 -0700 (Fri, 17 May 2002)
Revision: 3660
Log message:

      Added a Boolean flag to create_iform to control the use of
      Strict or Relaxed.
      

Changes  Path
+2 -2 metaprl/filter/boot/rewrite_boot.ml
+2 -2 metaprl/filter/boot/tactic_boot_sig.mlz
+3 -2 metaprl/refiner/refiner/refine.ml
+1 -0 metaprl/refiner/refsig/refine_sig.ml
+2 -1 metaprl/theories/itt/Makefile
Added metaprl/theories/itt/itt_example.ml
Properties metaprl/theories/itt/itt_example.ml
Added metaprl/theories/itt/itt_example.mli
Properties metaprl/theories/itt/itt_example.mli
+1 -1 metaprl/theories/mc/mp_mc_fir_phobos.ml
+1 -1 metaprl/theories/tactic/top_conversionals.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-17 16:39:09 -0700 (Fri, 17 May 2002)
Revision: 3661
Log message:

      Got rid of BackwardsCompatibleLevel params.
      

Changes  Path
+0 -4 metaprl/library/mbterm.ml
+0 -3 metaprl/refiner/reflib/ml_format.ml
+0 -4 metaprl/refiner/reflib/simple_print.ml
+0 -1 metaprl/refiner/refsig/term_simple_sig.mlz
+3 -5 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+0 -1 metaprl/refiner/term_ds/term_ds.ml
+0 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+0 -1 metaprl/refiner/term_gen/term_header_constr.ml
+0 -1 metaprl/refiner/term_std/term_std.ml
+0 -1 metaprl/refiner/term_std/term_std_sig.ml

Changes by: ( at unknown.email)
Date: 2002-05-17 16:39:09 -0700 (Fri, 17 May 2002)
Revision: 3662
Log message:

      This commit was manufactured by cvs2svn to create branch
      'filter_phobos'.

Changes  Path
Copied metaprl-branches/filter_phobos
Deleted metaprl-branches/filter_phobos/.cpdir
Deleted metaprl-branches/filter_phobos/.cprc
Deleted metaprl-branches/filter_phobos/BUGS
Deleted metaprl-branches/filter_phobos/Makefile
Deleted metaprl-branches/filter_phobos/README
Deleted metaprl-branches/filter_phobos/refiner/Conscript
Deleted metaprl-branches/filter_phobos/refiner/Makefile
Deleted metaprl-branches/filter_phobos/refiner/refsig/Conscript
Deleted metaprl-branches/filter_phobos/refiner/refsig/Files
Deleted metaprl-branches/filter_phobos/refiner/refsig/Makefile
Deleted metaprl-branches/filter_phobos/refiner/refsig/refine_error.h
Deleted metaprl-branches/filter_phobos/refiner/refsig/refine_error.mlh
Deleted metaprl-branches/filter_phobos/refiner/refsig/refine_error_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/refine_minimal_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/refine_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/refiner_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/rewrite_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_addr_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_base_minimal_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_base_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_eval_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_hash_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_man_minimal_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_man_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_meta_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_norm_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_op_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_shape_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_subst_minimal_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/term_subst_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/termmod_hash_sig.ml
Deleted metaprl-branches/filter_phobos/refiner/refsig/termmod_sig.ml

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 17:18:33 -0700 (Fri, 17 May 2002)
Revision: 3663
Log message:

      Extend grammar.
      
      1. Now keywords "in" and "IN" are interchangeable.
      So you may write <<'a in 'T>> instead of <<'a IN 'T>>.
      
      2. You may write 'a='b and 'a<>'b for equal{'a;'b} and nequal{'a;'b}
      correspondingly in theories where such terms are defined.
      For example equal{'a;'b} is defined in czf_itt_eq.
      
      Question to Xin and Jason:
      The czf_itt_eq theory defines two terms for equality: eq and equal.
      Which of them do you think will be more usable?
      If eq is more usable, then it is probably better to define 'a='b as eq{'a;'b}.
      
      3. Added some CZF operators to the parser:
      
        'a In 'b
        all x In 'S. 'P['x]
        all x . 'P['x]
        exst x In 'S. 'P['x]
        exst x . 'P['x]
      
      Question (mainly to Xin and Jason): 'a In 'b is probably not the best shortcut for the set theory membership.
      Other possibilities are  sin, ins, in_s, mem, member.
      Do you have any preference?
      
      4. Now all variables may be words or strings. E.g. yo may write <<all "x^2".'P['"x^2"]>>.
      (Previously in some places variables might be strings, in other places they had to be words)
      

Changes  Path
+41 -25 metaprl/filter/base/term_grammar.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-17 18:10:45 -0700 (Fri, 17 May 2002)
Revision: 3664
Log message:

      - Removed the .prla files that didn't contain any actual proofs.
      - Refreshed some old .prla files.
      

Changes  Path
+553 -692 metaprl/theories/base/base_rewrite.prla
+677 -1081 metaprl/theories/czf/czf_itt_all.prla
+773 -984 metaprl/theories/czf/czf_itt_and.prla
+1506 -1454 metaprl/theories/czf/czf_itt_axioms.prla
+1461 -1527 metaprl/theories/czf/czf_itt_dall.prla
+1196 -1388 metaprl/theories/czf/czf_itt_dexists.prla
+602 -924 metaprl/theories/czf/czf_itt_empty.prla
+5270 -5762 metaprl/theories/czf/czf_itt_eq.prla
+653 -893 metaprl/theories/czf/czf_itt_exists.prla
+572 -892 metaprl/theories/czf/czf_itt_false.prla
Deleted metaprl/theories/czf/czf_itt_fol.prla
+790 -1026 metaprl/theories/czf/czf_itt_implies.prla
+1057 -1344 metaprl/theories/czf/czf_itt_isect.prla
+1941 -2124 metaprl/theories/czf/czf_itt_member.prla
+2324 -3011 metaprl/theories/czf/czf_itt_nat.prla
+692 -959 metaprl/theories/czf/czf_itt_or.prla
+803 -1123 metaprl/theories/czf/czf_itt_pair.prla
+1674 -1765 metaprl/theories/czf/czf_itt_power.prla
+1214 -1535 metaprl/theories/czf/czf_itt_rel.prla
+761 -1165 metaprl/theories/czf/czf_itt_sall.prla
+1594 -1592 metaprl/theories/czf/czf_itt_sep.prla
+3428 -3370 metaprl/theories/czf/czf_itt_set_ind.prla
+773 -1183 metaprl/theories/czf/czf_itt_sexists.prla
+843 -1042 metaprl/theories/czf/czf_itt_singleton.prla
+726 -1101 metaprl/theories/czf/czf_itt_subset.prla
Deleted metaprl/theories/czf/czf_itt_theory.prla
+574 -895 metaprl/theories/czf/czf_itt_true.prla
+2456 -2619 metaprl/theories/czf/czf_itt_union.prla
+737 -962 metaprl/theories/fol/cfol_itt_all.prla
Deleted metaprl/theories/fol/cfol_theory.prla
Deleted metaprl/theories/fol/fol_all.prla
Deleted metaprl/theories/fol/fol_and.prla
Deleted metaprl/theories/fol/fol_exists.prla
Deleted metaprl/theories/fol/fol_false.prla
Deleted metaprl/theories/fol/fol_implies.prla
+655 -969 metaprl/theories/fol/fol_itt_and.prla
+543 -859 metaprl/theories/fol/fol_itt_false.prla
+649 -970 metaprl/theories/fol/fol_itt_implies.prla
+661 -959 metaprl/theories/fol/fol_itt_or.prla
Deleted metaprl/theories/fol/fol_itt_prop.prla
+527 -827 metaprl/theories/fol/fol_itt_true.prla
Deleted metaprl/theories/fol/fol_itt_type.prla
+365 -582 metaprl/theories/fol/fol_not.prla
Deleted metaprl/theories/fol/fol_or.prla
Deleted metaprl/theories/fol/fol_pred.prla
Deleted metaprl/theories/fol/fol_struct.prla
Deleted metaprl/theories/fol/fol_theory.prla
Deleted metaprl/theories/fol/fol_true.prla
Deleted metaprl/theories/fol/fol_type.prla
+1 -1 metaprl/theories/itt/itt_prec.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-17 19:33:37 -0700 (Fri, 17 May 2002)
Revision: 3665
Log message:

      Cleaned up the legacy stuff (Itt_equal!member, etc) somewhat.
      

Changes  Path
+49 -51 metaprl/theories/reflect_itt/refl_free_vars.prla
+17 -19 metaprl/theories/reflect_itt/refl_raw_term.prla
+232 -234 metaprl/theories/reflect_itt/refl_term.prla
+39 -41 metaprl/theories/reflect_itt/refl_var.prla
+19 -21 metaprl/theories/reflect_itt/refl_var_set.prla

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 20:42:59 -0700 (Fri, 17 May 2002)
Revision: 3666
Log message:

      Updated userguide.
      

Changes  Path
+227 -127 metaprl/doc/htmlman/user-guide/mp-terms.html

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 20:53:19 -0700 (Fri, 17 May 2002)
Revision: 3667
Log message:

      Minor changes
      

Changes  Path
+7 -8 metaprl/doc/htmlman/user-guide/mp-terms.html

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-17 21:36:09 -0700 (Fri, 17 May 2002)
Revision: 3668
Log message:

      Minor change
      

Changes  Path
+0 -4 metaprl/filter/base/term_grammar.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-17 23:18:50 -0700 (Fri, 17 May 2002)
Revision: 3669
Log message:

      This is a lot of little changes.
      
      1) I've removed Mp_mc_term_op and folded it into
         the new Mp_mc_base module.  Accordingly, I've
         updated print.ml for the generation of documentation.
         Mp_mc_base contains the contents of Mp_mc_term_op'
         (term construction/deconstructon functions), as well
         as some convinience functions for debugging code.
         (These come in handy in debuggin MCC/MetaPRL interactions.)
         The Conscript and Makefile have also been updated,
         as well as any "open Module" statements.
      
      2) I'm updating the code that performs the inlining
         optimization.  It looks a bit nicer now.
         And it seems to work as expected.
      
      3) I'm updating Mp_mc_fir_phobos(_exp) to be a bit
         cleaner.  In particular, Mp_mc_fir_phobos_exp only
         declares those terms that we have to work
         with directly in MetaPRL, i.e. variable[v:s].
         The conversional to transform a preFIR to FIR term
         has been modified to remove variable[v:s] terms
         last.
      
      Just to emphasize, the inling example (it's in MCC)
      currently works.
      

Changes  Path
+0 -1 metaprl/doc/latex/theories/mc/print.ml
+4 -6 metaprl/theories/mc/Conscript
+1 -2 metaprl/theories/mc/Makefile
Added metaprl/theories/mc/mp_mc_base.ml
Properties metaprl/theories/mc/mp_mc_base.ml
Added metaprl/theories/mc/mp_mc_base.mli
Properties metaprl/theories/mc/mp_mc_base.mli
+37 -88 metaprl/theories/mc/mp_mc_compile.ml
+6 -7 metaprl/theories/mc/mp_mc_compile.mli
+1 -1 metaprl/theories/mc/mp_mc_fir_base.ml
+47 -7 metaprl/theories/mc/mp_mc_fir_eval.ml
+4 -0 metaprl/theories/mc/mp_mc_fir_eval.mli
+2 -1 metaprl/theories/mc/mp_mc_fir_exp.ml
+1 -0 metaprl/theories/mc/mp_mc_fir_exp.mli
+22 -34 metaprl/theories/mc/mp_mc_fir_phobos.ml
+9 -8 metaprl/theories/mc/mp_mc_fir_phobos.mli
+13 -20 metaprl/theories/mc/mp_mc_fir_phobos_exp.ml
+14 -27 metaprl/theories/mc/mp_mc_fir_phobos_exp.mli
+2 -1 metaprl/theories/mc/mp_mc_fir_prog.ml
+1 -0 metaprl/theories/mc/mp_mc_fir_prog.mli
+36 -181 metaprl/theories/mc/mp_mc_inline.ml
+4 -76 metaprl/theories/mc/mp_mc_inline.mli
Added metaprl/theories/mc/mp_mc_inline_aux.ml
Properties metaprl/theories/mc/mp_mc_inline_aux.ml
Added metaprl/theories/mc/mp_mc_inline_aux.mli
Properties metaprl/theories/mc/mp_mc_inline_aux.mli
Deleted metaprl/theories/mc/mp_mc_term_op.ml
Deleted metaprl/theories/mc/mp_mc_term_op.mli
+3 -2 metaprl/theories/mc/mp_mc_theory.mlz
+25 -61 metaprl/theories/mc/tests/mp_mc_test.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-17 23:42:37 -0700 (Fri, 17 May 2002)
Revision: 3670
Log message:

      Now that I've corrected my one word typo in
      Mp_mc_compile, Mp_mc_fir_phobos_exp is completely
      unnecessary as the Phobos post processing rewrites
      take care of everything.
      

Changes  Path
+1 -1 metaprl/theories/mc/Conscript
+1 -1 metaprl/theories/mc/mp_mc_compile.ml
+1 -4 metaprl/theories/mc/mp_mc_fir_phobos.ml
+0 -1 metaprl/theories/mc/mp_mc_fir_phobos.mli
Deleted metaprl/theories/mc/mp_mc_fir_phobos_exp.ml
Deleted metaprl/theories/mc/mp_mc_fir_phobos_exp.mli
+1 -0 metaprl/theories/mc/mp_mc_theory.mlz

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-18 00:13:45 -0700 (Sat, 18 May 2002)
Revision: 3671
Log message:

      My final set of code/comment clean-ups for the night.
      Nothing especially interesting here.  Just some
      comments, and a little code restructuring to a
      slightly more logical organization.
      

Changes  Path
+3 -0 metaprl/theories/mc/mp_mc_compile.ml
+21 -96 metaprl/theories/mc/mp_mc_const_elim.ml
+6 -21 metaprl/theories/mc/mp_mc_const_elim.mli
+8 -1 metaprl/theories/mc/mp_mc_deadcode.ml
+0 -1 metaprl/theories/mc/mp_mc_deadcode.mli
+8 -114 metaprl/theories/mc/mp_mc_fir_eval.ml
+0 -43 metaprl/theories/mc/mp_mc_fir_eval.mli
+17 -4 metaprl/theories/mc/mp_mc_inline.ml
+7 -0 metaprl/theories/mc/mp_mc_inline.mli
+2 -3 metaprl/theories/mc/mp_mc_inline_aux.ml
+1 -1 metaprl/theories/mc/mp_mc_inline_aux.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-18 10:00:41 -0700 (Sat, 18 May 2002)
Revision: 3672
Log message:

      Docs: Fixed most undefined references.
      

Changes  Path
+1 -0 metaprl/doc/latex/theories/Makefile
+1 -1 metaprl/theories/base/base_auto_tactic.ml
+1 -1 metaprl/theories/base/base_dtactic.ml
+2 -2 metaprl/theories/base/base_theory.mlz
+1 -1 metaprl/theories/czf/czf_itt_set.ml
+1 -1 metaprl/theories/czf/czf_itt_theory.mlz
+2 -2 metaprl/theories/itt/itt_disect.ml
+1 -1 metaprl/theories/itt/itt_rfun.ml
+3 -3 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_unit.ml
+2 -2 metaprl/theories/itt/itt_void.ml
+3 -3 metaprl/theories/tactic/top_conversionals.ml
+1 -8 texinputs/metaprl.bib

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-18 13:06:40 -0700 (Sat, 18 May 2002)
Revision: 3673
Log message:

      Forgot a @docoff directive.
      

Changes  Path
+1 -0 metaprl/theories/mc/mp_mc_fir_exp.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-18 18:09:55 -0700 (Sat, 18 May 2002)
Revision: 3674
Log message:

      Do not execute inline code if there are no inline terms coming from Phobos.
      

Changes  Path
+4 -1 metaprl/theories/mc/mp_mc_compile.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-19 00:00:00 -0700 (Sun, 19 May 2002)
Revision: 3675
Log message:

      Changed one of the two associative axioms to a regular rule which can be proved from the other.
      

Changes  Path
+10 -10 metaprl/theories/czf/czf_itt_group.ml
+131 -108 metaprl/theories/czf/czf_itt_group.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-19 00:21:32 -0700 (Sun, 19 May 2002)
Revision: 3676
Log message:

      The former definition for group builder was not consistent. Now group_bvd{h; g; s} also requires that subset{s; car{g}}. From it, it can be proven that id{h} = id{g} and inv{h; a} = inv{g; a} for all a in car{h}.
      Reproved all related rules and updated related comments.
      

Changes  Path
+31 -6 metaprl/theories/czf/czf_itt_group_bvd.ml
+4 -2 metaprl/theories/czf/czf_itt_group_bvd.mli
+1839 -687 metaprl/theories/czf/czf_itt_group_bvd.prla
+8 -6 metaprl/theories/czf/czf_itt_hom.ml
+888 -989 metaprl/theories/czf/czf_itt_hom.prla
+8 -4 metaprl/theories/czf/czf_itt_ker.ml
+1 -2 metaprl/theories/czf/czf_itt_ker.mli
+1372 -1279 metaprl/theories/czf/czf_itt_ker.prla
+6 -4 metaprl/theories/czf/czf_itt_subgroup.ml
+0 -1 metaprl/theories/czf/czf_itt_subgroup.mli
+2594 -2598 metaprl/theories/czf/czf_itt_subgroup.prla

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-19 19:52:26 -0700 (Sun, 19 May 2002)
Revision: 3677
Log message:

      Got rid of reflect_itt - it's pretty outdated
      and is probably not the best way of doing these things anyway...
      

Changes  Path
+1 -1 metaprl/mk/preface
Deleted metaprl/theories/reflect_itt/Makefile
Deleted metaprl/theories/reflect_itt/refl_free_vars.ml
Deleted metaprl/theories/reflect_itt/refl_free_vars.mli
Deleted metaprl/theories/reflect_itt/refl_free_vars.prla
Deleted metaprl/theories/reflect_itt/refl_raw_term.ml
Deleted metaprl/theories/reflect_itt/refl_raw_term.mli
Deleted metaprl/theories/reflect_itt/refl_raw_term.prla
Deleted metaprl/theories/reflect_itt/refl_term.ml
Deleted metaprl/theories/reflect_itt/refl_term.mli
Deleted metaprl/theories/reflect_itt/refl_term.prla
Deleted metaprl/theories/reflect_itt/refl_var.ml
Deleted metaprl/theories/reflect_itt/refl_var.mli
Deleted metaprl/theories/reflect_itt/refl_var.prla
Deleted metaprl/theories/reflect_itt/refl_var_set.ml
Deleted metaprl/theories/reflect_itt/refl_var_set.mli
Deleted metaprl/theories/reflect_itt/refl_var_set.prla

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-20 09:16:44 -0700 (Mon, 20 May 2002)
Revision: 3678
Log message:

      Cleaned up TPTP.
      

Changes  Path
+5 -0 metaprl/refiner/reflib/ascii_io.ml
+5 -3 metaprl/theories/base/base_auto_tactic.ml
+1 -0 metaprl/theories/base/base_auto_tactic.mli
+1 -1 metaprl/theories/fol/cfol_itt_and.prla
+2 -2 metaprl/theories/itt/itt_collection.prla
+1 -1 metaprl/theories/itt/itt_fset.prla
+34 -54 metaprl/theories/tptp/tptp.ml
+30 -49 metaprl/theories/tptp/tptp.mli
+6809 -7259 metaprl/theories/tptp/tptp.prla

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-20 09:42:24 -0700 (Mon, 20 May 2002)
Revision: 3679
Log message:

      Got rid of some legacy compatibility code that's no longer relevant.
      

Changes  Path
+1 -8 metaprl/filter/base/filter_summary.ml
+8 -16 metaprl/refiner/term_gen/term_header_constr.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-21 00:39:09 -0700 (Tue, 21 May 2002)
Revision: 3680
Log message:

      Adding operational semantics for eqEqOp.
      

Changes  Path
+5 -0 metaprl/theories/mc/mp_mc_fir_eval.ml
+1 -0 metaprl/theories/mc/mp_mc_fir_eval.mli

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-05-22 10:45:49 -0700 (Wed, 22 May 2002)
Revision: 3681
Log message:

      Fixing numerous compiler warnings in clib.  Most of these have to do with
      the #pragma directives that were obsoleted; I checked with Jason and he said
      it was okay to remove them.  The rest are adding header files and function
      prototypes for missing symbols, and working around a few uninitialized var
      warnings.  This should not change the semantics of anything in clib.
      

Changes  Path
+0 -3 metaprl/clib/debug.c
+0 -3 metaprl/clib/debug.h
+5 -1 metaprl/clib/getrusage.c
+8 -3 metaprl/clib/marshal_shared.c
+2 -5 metaprl/clib/ml_debug.c
+0 -3 metaprl/clib/mmap.c
+1 -4 metaprl/clib/print_symbols.c
+0 -3 metaprl/clib/print_symbols.h
+7 -8 metaprl/clib/register.c
+1 -0 metaprl/clib/termsize.c

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-22 12:45:33 -0700 (Wed, 22 May 2002)
Revision: 3682
Log message:

      More clib clean-up.
      

Changes  Path
+0 -1 metaprl/clib/Makefile
+0 -1 metaprl/clib/getrusage.c
+1 -2 metaprl/clib/ml_debug.c
+1 -1 metaprl/clib/mmap.c
+0 -1 metaprl/clib/print_symbols.c
+2 -1 metaprl/clib/readline.c
Deleted metaprl/clib/register.c
+1 -1 metaprl/clib/termsize.c
+1 -1 metaprl/mk/preface

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-22 18:00:55 -0700 (Wed, 22 May 2002)
Revision: 3683
Log message:

      Changed the meta_lt and meta_eq implementation to be safer.
      Have not changed the meta_{sum,sub,...} etc.
      
      See the "Base_meta" thread in the newsgroup for more information.
      

Changes  Path
+49 -85 metaprl/theories/base/base_meta.ml
+18 -6 metaprl/theories/base/base_meta.mli
+2 -2 metaprl/theories/itt/itt_atom_bool.ml
+2 -2 metaprl/theories/itt/itt_equal.ml
+4 -4 metaprl/theories/itt/itt_int_base.ml
+2 -2 metaprl/theories/itt/itt_record_label.ml
+1 -1 metaprl/theories/sil/sil_sos.ml

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-22 21:47:47 -0700 (Wed, 22 May 2002)
Revision: 3684
Log message:

      Updating the Conscript to reflect the removed register.c file.
      

Changes  Path
+0 -2 metaprl/clib/Conscript

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-23 19:51:06 -0700 (Thu, 23 May 2002)
Revision: 3689
Log message:

      Added to theories.pdf:
      - A title: "A Listing of MetaPRL Theories"
      - A list of authors:
      "Jason J. Hickey and Brian Aydemir and Yegor Bryukhov and Alexei Kopylov and Aleksey Nogin and Xin Yu"
      - A 4-line introduction explaining what this is.
      
      I want this to look reasonable enough to cite in a paper. BTW, it can now be addressed simple
      as http://metaprl.org/theories.pdf
      
      Any improvement suggestions?
      

Changes  Path
+1 -1 metaprl/doc/htmlman/mp.html
+10 -0 metaprl/doc/latex/theories/all-theories.tex
+7 -0 texinputs/metaprl.bib

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-23 21:04:43 -0700 (Thu, 23 May 2002)
Revision: 3690
Log message:

      Adding base_meta rewrites (only for +-*/) to be applied to all
      Phobos iforms. Now the paper example works.
      

Changes  Path
+2 -0 metaprl/theories/mc/mp_mc_compile.ml
+14 -1 metaprl/theories/mc/mp_mc_fir_phobos.ml
+1 -0 metaprl/theories/mc/mp_mc_fir_phobos.mli
+1 -0 metaprl/theories/mc/mp_mc_theory.mlz

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-05-23 21:33:14 -0700 (Thu, 23 May 2002)
Revision: 3691
Log message:

      Updates to reflect the new MCC FIR.  I've just
      commented out problem code since I need to rethink
      slightly how I represent the FIR in MetaPRL and I don't
      want to spend time updating code that's about to change
      anyways.
      

Changes  Path
+4 -0 metaprl/theories/mc/mp_mc_connect_exp.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 03:22:43 -0700 (Sun, 26 May 2002)
Revision: 3693
Log message:

      Changed the definition of the carrier in cyclic subgroups/groups from
      collection to separation. The reason for this is that we should always
      try to use set primitives rather than collections.
      Updated corresponding rules and proofs.
      Also made some minor changes in comments.
      

Changes  Path
+9 -16 metaprl/theories/czf/czf_itt_cyclic_group.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_group.mli
+2617 -2779 metaprl/theories/czf/czf_itt_cyclic_group.prla
+20 -6 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+2499 -1928 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+1 -1 metaprl/theories/czf/czf_itt_group.ml
+3 -3 metaprl/theories/czf/czf_itt_group_power.ml
+19 -15 metaprl/theories/czf/czf_itt_hom.ml
+25 -24 metaprl/theories/czf/czf_itt_ker.ml
+1123 -1126 metaprl/theories/czf/czf_itt_ker.prla
+1 -0 metaprl/theories/czf/czf_itt_kleingroup.ml
+1 -1 metaprl/theories/czf/czf_itt_subgroup.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 03:27:42 -0700 (Sun, 26 May 2002)
Revision: 3694
Log message:

      More changes in the comments.
      

Changes  Path
+2 -2 metaprl/theories/czf/czf_itt_inv_image.ml
+81 -81 metaprl/theories/czf/czf_itt_inv_image.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 19:47:00 -0700 (Sun, 26 May 2002)
Revision: 3695
Log message:

      Removed all occurences of "rwh unfold_group_bvd ..." in the proof.
      

Changes  Path
+9048 -9475 metaprl/theories/czf/czf_itt_ker.prla

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-27 01:31:55 -0700 (Mon, 27 May 2002)
Revision: 3696
Log message:

      A bit easier-to-read output from Phobos activity.
      

Changes  Path
+4 -0 metaprl/theories/mc/mp_mc_base.ml
+1 -0 metaprl/theories/mc/mp_mc_base.mli
+6 -8 metaprl/theories/mc/mp_mc_compile.ml
+2 -2 metaprl/theories/mc/mp_mc_fir_phobos.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-27 22:19:15 -0700 (Mon, 27 May 2002)
Revision: 3697
Log message:

      Changed the occurences of set_bvd to sep, since set_bvd is defined by collection.
      

Changes  Path
+1 -2 metaprl/theories/czf/czf_itt_hom.ml
+1644 -1631 metaprl/theories/czf/czf_itt_hom.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-27 22:21:34 -0700 (Mon, 27 May 2002)
Revision: 3698
Log message:

      Rebuilt the prla file.
      

Changes  Path
+292 -300 metaprl/theories/czf/czf_itt_inv_image.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-27 23:55:07 -0700 (Mon, 27 May 2002)
Revision: 3699
Log message:

      Minor changes in comments.
      

Changes  Path
+1 -0 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+3 -5 metaprl/theories/czf/czf_itt_group.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-28 20:09:00 -0700 (Tue, 28 May 2002)
Revision: 3700
Log message:

      Added more functionality to interface with Phobos.
      

Changes  Path
+37 -6 metaprl/theories/mc/mp_mc_compile.ml
+8 -0 metaprl/theories/mc/mp_mc_compile.mli
+14 -3 metaprl/theories/mc/mp_mc_fir_phobos.ml
+1 -0 metaprl/theories/mc/mp_mc_fir_phobos.mli

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-29 04:26:11 -0700 (Wed, 29 May 2002)
Revision: 3701
Log message:

      Updated comments.
      Also fixed a small error in the well-formedness rule in Czf_itt_normal_subgroup
      

Changes  Path
+3 -13 metaprl/theories/czf/czf_itt_comment.ml
+15 -16 metaprl/theories/czf/czf_itt_coset.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_group.ml
+6 -6 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+24 -20 metaprl/theories/czf/czf_itt_group.ml
+1 -1 metaprl/theories/czf/czf_itt_group_power.ml
+15 -17 metaprl/theories/czf/czf_itt_hom.ml
+5 -5 metaprl/theories/czf/czf_itt_inv_image.ml
+1 -1 metaprl/theories/czf/czf_itt_iso.ml
+12 -15 metaprl/theories/czf/czf_itt_ker.ml
+0 -2 metaprl/theories/czf/czf_itt_ker.mli
+2 -2 metaprl/theories/czf/czf_itt_kleingroup.ml
+0 -1 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+3 -3 metaprl/theories/czf/czf_itt_subgroup.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-05-30 11:56:38 -0700 (Thu, 30 May 2002)
Revision: 3702
Log message:

      Return idC if no iforms are given.
      

Changes  Path
+5 -1 metaprl/theories/mc/mp_mc_fir_phobos.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-31 19:40:02 -0700 (Fri, 31 May 2002)
Revision: 3703
Log message:

      I forgot to remove register.mlz when removing register.c
      

Changes  Path
+2 -3 metaprl/filter/boot/tactic_boot.ml
+0 -2 metaprl/mllib/Conscript
+1 -2 metaprl/mllib/Makefile
Deleted metaprl/mllib/register.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-05-31 21:39:06 -0700 (Fri, 31 May 2002)
Revision: 3704
Log message:

      Added edit_cd_list_contents for Lori.
      It's not perfect (it cd's into the module as a side-effect),
      but our top-loop code is very ugly anyway...
      

Changes  Path
+1 -0 metaprl/editor/ml/mp.ml
+2 -0 metaprl/editor/ml/mp.mli
+2 -3 metaprl/editor/ml/proof_edit.ml
+2 -3 metaprl/editor/ml/proof_edit.mli
+13 -15 metaprl/editor/ml/shell.ml
+3 -3 metaprl/editor/ml/shell_package.ml
+11 -11 metaprl/editor/ml/shell_rewrite.ml
+3 -3 metaprl/editor/ml/shell_root.ml
+7 -3 metaprl/editor/ml/shell_rule.ml
+3 -1 metaprl/editor/ml/shell_sig.mlz