Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-03 10:29:07 -0700 (Tue, 03 Sep 2002)
Revision: 3838
Log message:

      Stange, the comment.ml file was totally out-of-date.
      We were missing chapters, sections, subsections, etc.
      This is fixed.  No major changes on the book dcoument
      yet.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-03 11:08:16 -0700 (Tue, 03 Sep 2002)
Revision: 3839
Log message:

      3 minor typo corrections before I go off to eat lunch. (-:
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-03 12:43:49 -0700 (Tue, 03 Sep 2002)
Revision: 3840
Log message:

      Added a title page and table of contents.
      
      We should try to get security to open the lab...
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-03 12:53:08 -0700 (Tue, 03 Sep 2002)
Revision: 3841
Log message:

      A few more typo corrections before we go through the book as a group.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-03 17:49:49 -0700 (Tue, 03 Sep 2002)
Revision: 3842
Log message:

      Updates through Chapter 4.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-03 18:55:28 -0700 (Tue, 03 Sep 2002)
Revision: 3843
Log message:

      Added update script as a temporary hack until we move
      the book into the right place.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-03 22:11:04 -0700 (Tue, 03 Sep 2002)
Revision: 3844
Log message:

      Updates on the OCaml book.
      
      Also, the MetaPRL comment parser was being too aggressive
      in coalescing newlines.  This update restores paragraphs
      to the OCaml book.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-04 10:58:08 -0700 (Wed, 04 Sep 2002)
Revision: 3845
Log message:

      Minor changes to the book.  Still working on the introduction.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-04 12:48:26 -0700 (Wed, 04 Sep 2002)
Revision: 3846
Log message:

      Updated the intro some.  Can you all take a look and see what you
      think?
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-04 12:51:23 -0700 (Wed, 04 Sep 2002)
Revision: 3847
Log message:

      Oops, be careful about the @ in an email address.
      

Changes by: Justin David Smith (justins at cs.caltech.edu)
Date: 2002-09-04 14:24:41 -0700 (Wed, 04 Sep 2002)
Revision: 3848
Log message:

      Correcting grammar/spelling errors in the introduction.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-04 18:52:46 -0700 (Wed, 04 Sep 2002)
Revision: 3849
Log message:

      This is the final version I'm sending to Benjamin.
      Thanks everyone!
      
      Jason
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-09-04 19:44:21 -0700 (Wed, 04 Sep 2002)
Revision: 3850
Log message:

      Spoke too soon.  Fixed some line breaks in the book.
      I sent this version off, and I replaced the copy at the
      cs134b web site.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-05 15:39:26 -0700 (Thu, 05 Sep 2002)
Revision: 3851
Log message:

      Cleaning up the code for rewriting integer set operations.  They
      should at least be somewhat readable now.  I also got rid of the
      shorthand singleton term since it was pretty much useless.
      

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

      Cleaning up generated documentation for Mfir_int_set. Also updating
      the README file with some new notes to myself about what I need to
      look at next, and removing notes that are no longer relevant.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-05 17:34:59 -0700 (Thu, 05 Sep 2002)
Revision: 3853
Log message:

      Starting a list of known BUGS with the Mojave FIR theory.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-06 14:08:37 -0700 (Fri, 06 Sep 2002)
Revision: 3854
Log message:

      I'm in the middle of resyncing the term declarations with the FIR.
      In the process, I've added some support for rudimentary records
      and ``options''.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-06 14:09:49 -0700 (Fri, 06 Sep 2002)
Revision: 3855
Log message:

      I'm going to go ahead and commit the change that hardcodes the location
      of my ``words'' file.  We should probably read this from a config
      file eventually.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-06 14:10:07 -0700 (Fri, 06 Sep 2002)
Revision: 3856
Log message:

      Updating the list of modules to print out.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-06 14:37:25 -0700 (Fri, 06 Sep 2002)
Revision: 3858
Log message:

      Finally addressing the frame type now that I have some notion
      of a record.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-06 15:40:13 -0700 (Fri, 06 Sep 2002)
Revision: 3859
Log message:

      This finishes my update of all the FIR atoms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-09 10:05:55 -0700 (Mon, 09 Sep 2002)
Revision: 3860
Log message:

      Minor cleanup to documentation.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-09 12:08:57 -0700 (Mon, 09 Sep 2002)
Revision: 3861
Log message:

      Updates to get the FIR theory to build with MCC.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-09 14:28:40 -0700 (Mon, 09 Sep 2002)
Revision: 3862
Log message:

      Beginning work on updating the functions needed to convert the
      MCC FIR to the MetaPRL term representation declared in the FIR theory.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-09 15:54:33 -0700 (Mon, 09 Sep 2002)
Revision: 3863
Log message:

      Adding the code to handle (raw) integer sets.  This should
      finish off the basic conversion functions, for now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-09 17:08:16 -0700 (Mon, 09 Sep 2002)
Revision: 3864
Log message:

      Beginning work on the functions needed to convert the FIR type system
      into (and out of) terms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-10 09:42:09 -0700 (Tue, 10 Sep 2002)
Revision: 3865
Log message:

      Wahoo!  This should finish the initial pass at the functions needed
      to convert between the FIR type system and terms.  I've changed
      a few term declarations so that they'd be more convinient to
      work with.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-10 14:58:52 -0700 (Tue, 10 Sep 2002)
Revision: 3866
Log message:

      Minor clean-up only.  Nothing new here.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-10 18:37:33 -0700 (Tue, 10 Sep 2002)
Revision: 3868
Log message:

      Fixed compilation with TESTS=yes.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-11 22:01:29 -0700 (Wed, 11 Sep 2002)
Revision: 3871
Log message:

      Updating documentation to make some things a bit clearer.
      (In particular, I'm trying to make it somewhat easier for
      me to figure out what the code's doing in the event that
      I don't look at it for a long time.)
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-12 15:24:38 -0700 (Thu, 12 Sep 2002)
Revision: 3873
Log message:

      Enabled ->v parameter conversion in relaxed mode.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-13 01:04:15 -0700 (Fri, 13 Sep 2002)
Revision: 3874
Log message:

      Added a simple error term to halt with an error message.
      Also, reduceC contains the Phobos-related rewrites and all Base_meta
      rewrites if you include Phobos_theory.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-13 01:05:17 -0700 (Fri, 13 Sep 2002)
Revision: 3875
Log message:

      Phobos_theory.mlz is now split up.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-13 01:06:29 -0700 (Fri, 13 Sep 2002)
Revision: 3876
Log message:

      Took out extra rewrites, since they should be in reduceC.
      Eventually, this stuff will move to theories/phobos.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-13 14:43:25 -0700 (Fri, 13 Sep 2002)
Revision: 3877
Log message:

      In context_vars, do a deep search for context vars, do not just look at the
      toplevel sequent.
      
      P.S. Term_std seems to do the right thing already.
      P.P.S. See the thread "Sequents of sequents." in the ng for more information
      on this change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-13 14:49:40 -0700 (Fri, 13 Sep 2002)
Revision: 3878
Log message:

      Fixed a syntax error - it's weird I've never caught it before...
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-20 08:16:49 -0700 (Fri, 20 Sep 2002)
Revision: 3879
Log message:

      Many of the files in this commit were simply touched becuase of minor
      formatting changes that I made when I was bored.  Other than that, the
      main changes here are:
      
      1. Updates to the set of terms to reflect the new FIR.  This is not
      complete yet.  The allocation operators need to be updated, and I
      need to declare terms for a few more things.  Some of the actual
      expression forms may need updating.
      
      2. Typing rules are in the middle of being updated to reflect the
      idea of of using sequents to represent a FIR program.
      
      As of this commit, lots of documentation is probably non-existant or
      innaccurate at this point, and I will be going back within the next
      week to clean everything up.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-20 08:20:34 -0700 (Fri, 20 Sep 2002)
Revision: 3880
Log message:

      Updating the list of theories to print.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-20 08:27:19 -0700 (Fri, 20 Sep 2002)
Revision: 3881
Log message:

      Oops.  Attempting to fix build problem with MCC when the FIR theory
      is included.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-20 08:30:35 -0700 (Fri, 20 Sep 2002)
Revision: 3882
Log message:

      Okay.  _Now_ the MCC/MetaPRL build problem that I created in my
      last few commits is fixed... *sigh*
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-20 15:40:18 -0700 (Fri, 20 Sep 2002)
Revision: 3883
Log message:

      Cleaning up documentation and some of the typing rules from my
      commit earlier today.  Remaining work:
      
      1. Anything relating to FIR expressions has not been cleaned up yet.
      2. I need to automate the typing rules eventually.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-20 17:00:18 -0700 (Fri, 20 Sep 2002)
Revision: 3884
Log message:

      I am working on creating a proper locale mapping
      of MetaPRL font table ("mode[prl]") to Unicode.
      
      I fixed a few bugs with nuprl_font doing some mappings incorrectly.
      
      The rest is still work-in-progress.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-20 18:47:53 -0700 (Fri, 20 Sep 2002)
Revision: 3885
Log message:

      Initial version of the charmap.
      
      I now have mappings for all the symbols that are referenced in nuprl_font.
      For 5 simbols (superscript circle, subscript letters a,b,c,z) I could not
      find any Unicode analogs, so had to pick something close (superscript 0
      instead of superscript circle and parentesized small letters instead of
      subscript small letters).
      
      Note that many symbols are never referenced in the nuprl_font, so
      we still have a lot of space left for more symbols.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-20 18:57:15 -0700 (Fri, 20 Sep 2002)
Revision: 3886
Log message:

      Added relational meta operations. Before only < existed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-20 19:04:20 -0700 (Fri, 20 Sep 2002)
Revision: 3887
Log message:

      A few mapping fixes.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-20 20:47:25 -0700 (Fri, 20 Sep 2002)
Revision: 3888
Log message:

      Reverted changes I made earlier.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-20 23:51:32 -0700 (Fri, 20 Sep 2002)
Revision: 3889
Log message:

      Added relational operators to Phobos theory. They are the usual
      abbreviations: lt, le, gt, ge or eq. Also, there are true and false
      terms as well. For now, I left each relop as relop[a,b]{'t; 'f},
      just to be consistent with Base_meta, but I might switch them to
      return true{}/false{} instead of 't/'f.
      Each operator is defined via Base_meta.lt, as Aleksey suggested.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-21 02:52:36 -0700 (Sat, 21 Sep 2002)
Revision: 3890
Log message:

      Print actual "Nuprl_font!vdash" terms in prl mode sequents display form instead
      of printing a hardcoded representation of vdash'es.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-21 03:27:46 -0700 (Sat, 21 Sep 2002)
Revision: 3891
Log message:

      Degree sign.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-21 03:30:34 -0700 (Sat, 21 Sep 2002)
Revision: 3892
Log message:

      Inmy previous commit I've accidentally included my Unicode changes.
      
      While they are probably the right thing, I am not sure if we are ready to switch
      to Unicode, so reverting for now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-23 08:54:49 -0700 (Mon, 23 Sep 2002)
Revision: 3893
Log message:

      Committing some work done over the weekend.  I've pretty much fixed
      all the typing rules I had done previously; the exceptions are the
      FIR allocation operators.  Places where documentation is lacking
      should be explicitly marked now.
      
      The only other major change is the addition of a script, atom_base_gen.py,
      which processes mfir_tr_aotm_base.spec to generate mfir_tr_atom_base.ml*.
      As with termOp_gen.py, I run the script by hand, as needed.  (Both
      scripts have saved me quite a bit of typing...)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-23 09:13:15 -0700 (Mon, 23 Sep 2002)
Revision: 3894
Log message:

      Adding the file that will be used to convert FIR expressions
      to/from terms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-24 09:48:25 -0700 (Tue, 24 Sep 2002)
Revision: 3895
Log message:

      Committing a little work on the functions to translate the FIR into terms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-24 14:44:06 -0700 (Tue, 24 Sep 2002)
Revision: 3896
Log message:

      Removing one instance in which I depended on rewrites being
      executed in a certain order to get the correct semantics for
      something.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-24 15:07:44 -0700 (Tue, 24 Sep 2002)
Revision: 3897
Log message:

      Eliminating another case in which I depended on rewrites being
      executes in a certain order.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-09-25 12:03:59 -0700 (Wed, 25 Sep 2002)
Revision: 3898
Log message:

      Committing a few minor documentation updates, fixing the typing rule
      for tail calls, and adding some of the typing rules for allocations
      back.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-25 16:04:30 -0700 (Wed, 25 Sep 2002)
Revision: 3899
Log message:

      This commit switches the PRL mode output from using the mp12 font
      to using Unicode (UTF-8) encoding.
      
      I will post a separate message in the newsgroup about this switch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-25 18:00:24 -0700 (Wed, 25 Sep 2002)
Revision: 3900
Log message:

      Utilities for selection proper Unicode font.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-30 16:51:15 -0700 (Mon, 30 Sep 2002)
Revision: 3904
Log message:

      Added another version of a "gate" logo.