Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-08-01 14:32:20 -0700 (Thu, 01 Aug 2002)
Revision: 3751
Log message:

      Fixed some outdated links.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-04 12:46:26 -0700 (Sun, 04 Aug 2002)
Revision: 3761
Log message:

      This is the initial commit of the new FIR theory.  This commit contains the
      initial set of term declarations, display forms, and documentation.  The next
      step will be to work toward writing up some typing rules.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-05 19:41:19 -0700 (Mon, 05 Aug 2002)
Revision: 3769
Log message:

      Oops.  Let's not print out theories that are not compiled in.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-06 09:28:27 -0700 (Tue, 06 Aug 2002)
Revision: 3770
Log message:

      Adding ``fir'' to ALL_THEORIES.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-06 10:27:44 -0700 (Tue, 06 Aug 2002)
Revision: 3771
Log message:

      Committing some spelling corrections.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-06 13:29:07 -0700 (Tue, 06 Aug 2002)
Revision: 3772
Log message:

      Seems like compare_num was using a naive implementation that was subject to
      overflow errors when two 31-bit ints were being compared.  For lack of better
      solution, I've changed (i - j) to (Pervasives.compare i j).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-06 14:00:47 -0700 (Tue, 06 Aug 2002)
Revision: 3773
Log message:

      Removed mfir_comment since it was redundant; the functionality it provided was
      already present elsewhere in MetaPRL.  Cleaned up Mfir_basic, Mfir_ty, and
      Mfir_exp as needed as a result of this.
      
      Added some additional support for integers and booleans to Mfir_basic so that
      I can start playing around with typing rules.  The Mfir_sequent module will
      deal with, you guessed it, sequent related items.  The Mfir_type_rules file
      will contain the typing rules (at least for now).
      
      The Mfir_test module will be used to test small examples, or to perform
      ``sanity checks'' on other aspects of the theory.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-06 14:01:35 -0700 (Tue, 06 Aug 2002)
Revision: 3774
Log message:

      Adding new modules to the output.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-08 15:14:42 -0700 (Thu, 08 Aug 2002)
Revision: 3778
Log message:

      Flushing out some work on the typing rules.
      
      I've added kinds and some judgments to mfir_sequent.  For mfir_ty, I've had to
      change how some types are represented (so that we get a convinient binding
      structure), and I've also added terms to represent some typing definitions.
      Added some typing rules, which I think all work as expected now.  Comments and
      documentation might need some clarifying still, but at least something's there
      for now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-08-09 08:59:20 -0700 (Fri, 09 Aug 2002)
Revision: 3780
Log message:

      Removed the special-case handling for axioms (rules without arguments and without
      assumptions).
      
      *** WARNING ***
      
      This commit breaks binary compatibility! Before doing "cvs update":
      - make sure all your proof modifications are exported into .prla files
      After "cvs update":
      - do "make clean" and erase the theories/*/*.prlb files.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-09 10:58:54 -0700 (Fri, 09 Aug 2002)
Revision: 3781
Log message:

      Splitting typing rules into multiple files, which will be easier to manage.
      Made other miscellaneous changes, mainly to some display forms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-09 10:59:15 -0700 (Fri, 09 Aug 2002)
Revision: 3782
Log message:

      Adding new modules to the list of modules to print.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-08-09 19:06:41 -0700 (Fri, 09 Aug 2002)
Revision: 3784
Log message:

      Added a new theory for Phobos. Eventually, I'll migrate Phobos-related
      stuff out of the dead mc theory.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-08-09 19:08:33 -0700 (Fri, 09 Aug 2002)
Revision: 3785
Log message:

      Added phobos to ALL~.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-08-10 01:39:22 -0700 (Sat, 10 Aug 2002)
Revision: 3786
Log message:

      Makefile was missing ../phobos.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-08-10 16:28:27 -0700 (Sat, 10 Aug 2002)
Revision: 3787
Log message:

      Rewrite was prepending not appending to the parameter.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-08-10 16:30:52 -0700 (Sat, 10 Aug 2002)
Revision: 3788
Log message:

      I figured out why the new Phobos rewrite wasn't working.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-08-11 12:40:31 -0700 (Sun, 11 Aug 2002)
Revision: 3789
Log message:

      Added theories/phobos
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 11:47:28 -0700 (Mon, 12 Aug 2002)
Revision: 3791
Log message:

      This is an intermediate commit, in the sense that I have a few temporary
      markers indicating places that I still need to finish off.  This commit adds a
      few more typing rules and some documentation updates.  I suppose I should
      tackle the harder typing rules at some point...
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 13:37:37 -0700 (Mon, 12 Aug 2002)
Revision: 3792
Log message:

      Except for values of a union type, this commit finishes an initial pass at
      typing rules for store values.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 15:22:53 -0700 (Mon, 12 Aug 2002)
Revision: 3793
Log message:

      This is my pass at typing rules for union definitions.  Had to add a length
      operator to the list implementation.  Other miscellaneous changes include some
      minor display form changes.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 15:43:43 -0700 (Mon, 12 Aug 2002)
Revision: 3794
Log message:

      Adding kind well-formedness judgments, though I only use them in the equality
      judgement for union definitions.  See the README file for a few musings on why
      this is...
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 15:52:42 -0700 (Mon, 12 Aug 2002)
Revision: 3795
Log message:

      Oops.  Forgot about these minor changes to term operators.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 16:34:08 -0700 (Mon, 12 Aug 2002)
Revision: 3796
Log message:

      Simplifying many rules by the deletion of unnessary premises.  This addresses
      some of the comments that I've had in the README file for a while.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 17:08:17 -0700 (Mon, 12 Aug 2002)
Revision: 3797
Log message:

      Another round of minor documentation/notes-to-myself updates before I start
      tackling the (not-so-easy) type rules...
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 23:01:11 -0700 (Mon, 12 Aug 2002)
Revision: 3798
Log message:

      This finishes my pass at typing rules for tyUnion, tyApply, and union_values.
      In the process, I've implemented some simple operators for getting the length
      of a list, performing type application, and testing set equality and subset.
      I've also done other minor things, like cleaning up some display forms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-12 23:07:48 -0700 (Mon, 12 Aug 2002)
Revision: 3799
Log message:

      Oops, forgot to include these files (again).  At some point, I may consider
      simplifying these files to not include operations that won't be needed when
      connecting with MCC.  (These files are generated by a script that I run every
      now and then.  Once the core set of terms needed to represent the FIR
      stabalizes, I'll go through and clean these files out of anything that's not
      absolutely needed.  Otherwise, these files are total grunge that's painful to
      constantly maintain by hand when the term representation keeps changing.)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-17 20:02:09 -0700 (Sat, 17 Aug 2002)
Revision: 3808
Log message:

      Just wanted to flush some work out before TPHOLs.
      This commits (one version) of the tyProject rule.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-23 10:11:09 -0700 (Fri, 23 Aug 2002)
Revision: 3821
Log message:

      Lots of changes here:
      
      1) The usual ``cleaning up documentation and existing rules''.
         Also cleaned up some display forms.
      
      2) Mfir_basic has been split into Mfir_int, Mfir_int_set, Mfir_list,
         and Mfir_bool.  Mfir_basic was getting a bit unwieldy.
      
      3) Wrote up the rules for atomTyApply, atomTyPack, and atomTyUnpack.
      
      4) Wrote up most of the rules for letAlloc.
      
      5) Wrote up a rule for letExt.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-23 10:11:39 -0700 (Fri, 23 Aug 2002)
Revision: 3822
Log message:

      Updating the list of theories to print to reflect new modules.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-23 10:31:47 -0700 (Fri, 23 Aug 2002)
Revision: 3823
Log message:

      This finishes my initial pass through the typing rules for allocation.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-24 12:48:06 -0700 (Sat, 24 Aug 2002)
Revision: 3824
Log message:

      I've debugged the rewrites in bool, list, and int_set.  In particular,
      in order to implement the typing rules for match statements properly,
      I'm going to need a correct implementation of basic interval set operations.
      So I've corrected the implmentation of the subset relation, and of set
      equality.  I've also simplified integer sets and raw integer sets into
      one generic set term so that I can implement set operations once.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-26 09:56:56 -0700 (Mon, 26 Aug 2002)
Revision: 3825
Log message:

      Committing some stuff before I potentially kill my working copy of MetaPRL.
      I'm updating the README file with some notes to myself.  I'm also adding the
      Python script which i've been using to create mfir_termOp.ml*.  Note that I
      run the script by hand, as needed. The comments at the top of the script
      attempt to capture its assumptions and shortcomings.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 12:30:46 -0700 (Tue, 27 Aug 2002)
Revision: 3826
Log message:

      An initial pass at implementing the union of two interval sets.
      I still need to clean up the conversionals somewhat, and then debug
      them. Fun.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 13:44:39 -0700 (Tue, 27 Aug 2002)
Revision: 3827
Log message:

      This should finish up interaval sets, at least for the time being.
      I'm also updating the list of ``test cases'' and committing the
      proofs used to verify the cases.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 15:58:57 -0700 (Tue, 27 Aug 2002)
Revision: 3828
Log message:

      Oops.  Mistake on the typing rule for tuple types.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 17:47:31 -0700 (Tue, 27 Aug 2002)
Revision: 3829
Log message:

      Wrote up most of the rules for unary operations.  Some unop's
      have been removed from the term-set since we're not sure
      how to deal with them yet.
      
      Also making a note to myself in the README file that the current
      term-set is somewhat out of date, though I'm not going to worry
      about this for a little while.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 19:42:10 -0700 (Tue, 27 Aug 2002)
Revision: 3830
Log message:

      This finishes off the atom typing rules, for the most part.  Finally sat down
      and when through all the binop's (cut, paste, and replace are such wonderful
      operations). (-:
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 21:27:42 -0700 (Tue, 27 Aug 2002)
Revision: 3831
Log message:

      I've written up half of the rules for match expressions.
      I'm leaving the union case for last... (-:
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-27 23:23:34 -0700 (Tue, 27 Aug 2002)
Revision: 3832
Log message:

      This finishes my initial pass at typing rules for match expressions.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-28 10:02:02 -0700 (Wed, 28 Aug 2002)
Revision: 3833
Log message:

      Some minimal documentation for the match expression typing rules.
      I will need to go through them again and clean them up some time.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-28 21:35:33 -0700 (Wed, 28 Aug 2002)
Revision: 3834
Log message:

      Committing some typing rules for subscripting rules.  Haven't dealt with
      the case of unions yet since the only way I've come up with so far
      is absolutely hiddeous.  Also haven't done frames yet, but that's becuase
      I've been avoiding everything related to frames for the time being.
      At this point, I'm thinking it might be wise to go through everything
      I've done and see if there's ways I can make things simpler.
      
      (Oh yeah, the documentation for the subscripting rules is completely
      useless at this point.  I'll make it more informative eventually.)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-29 12:05:17 -0700 (Thu, 29 Aug 2002)
Revision: 3835
Log message:

      Minor cleanup to some terms and typing rules, corrections to typing rules, and
      documentation updates.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-29 13:33:37 -0700 (Thu, 29 Aug 2002)
Revision: 3836
Log message:

      Given my current set of ``test cases'', there's no sensible reason
      why they need to be output into theories.pdf, so I'm removing the
      mfir_test module from the output.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-29 16:23:55 -0700 (Thu, 29 Aug 2002)
Revision: 3837
Log message:

      More corrections to typing rules (and a minor typo fix to a display form).
      Also noting that the match rule for unions that I have might be buggy.
      Looks okay, but I'm going to have to think about how the sequents work
      a bit more before I'll be completely convinced that it's the correct rule.