Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-08-01 06:24:09 -0700 (Wed, 01 Aug 2001)
Revision: 3352
Log message:

      - Made sure conditional rewrites are added to toploop the same way the normal
      rules and rewrites are.
      - Added <<if ... then ... else ...>> term syntax macro (stands for iftenelse{ ; ; })
      - Proved and added to reduceC the reduction for ind with constant argument (as Brian
      requested). This reduction does everything except incrementing/decrementing the number
      (it will leave if as n + 1 or n - 1).
      - Fixed lt_bool reduction
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-08-01 07:21:41 -0700 (Wed, 01 Aug 2001)
Revision: 3353
Log message:

      Forgot to commit the proofs.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-01 11:52:04 -0700 (Wed, 01 Aug 2001)
Revision: 3354
Log message:

      Added reductions for the boolean comparisons to the reduce tactic.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-01 17:17:56 -0700 (Wed, 01 Aug 2001)
Revision: 3355
Log message:

      Initial import of a model for the integer sets within the FIR.  Doesn't
      completely model the FIR sets yet, but contains sufficient functionality
      relative to the rest of the code at this point.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-01 17:24:06 -0700 (Wed, 01 Aug 2001)
Revision: 3356
Log message:

      Made some things more internally consistant and cleaned up a few things.
      The next step will be to continue modelling the FIR and cleaning things
      up as needed to make the model faithful to the FIR in the mc compiler.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-02 09:10:16 -0700 (Thu, 02 Aug 2001)
Revision: 3357
Log message:

      Added the not-equals int op.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-02 09:11:47 -0700 (Thu, 02 Aug 2001)
Revision: 3358
Log message:

      Updated letSubCheck to better reflect the FIR.  Still a no-op at this point.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-02 09:22:32 -0700 (Thu, 02 Aug 2001)
Revision: 3359
Log message:

      Updated to compile fir_ty and fir_int_set now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-04 11:39:51 -0700 (Sat, 04 Aug 2001)
Revision: 3360
Log message:

      - Updated some display forms.
      - Organized the term declarations to be in more logical locations.
      - There should be terms for most of the items in the FIR now.
      - Still need to work on semantics of the terms and rewrites.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-04 20:26:02 -0700 (Sat, 04 Aug 2001)
Revision: 3361
Log message:

      I've added display forms for le_bool, gt_bool, and
      ge_bool. The forms for beq_int, bneq_int, and lt_bool
      were used as a model.  They appear to work fine, but
      someone should probably still check them to make sure
      that the details are ok.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-08-06 09:25:57 -0700 (Mon, 06 Aug 2001)
Revision: 3362
Log message:

      Added the OCaml book I wrote December 2000.  Still needs some work
      on typos etc.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-08-07 13:32:03 -0700 (Tue, 07 Aug 2001)
Revision: 3363
Log message:

      Added some initial Conscript files.  cons is a "make" replacement.
      make will continue to work in the usual way, but cons will
      eventually make it easier to produce a build.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-09 18:26:47 -0700 (Thu, 09 Aug 2001)
Revision: 3365
Log message:

      Committing minor changes to the (very confused looking)
      boolean representation before I begin revising everything
      to reflect the presence of a program state.
      

Changes by: ( at unknown.email)
Date: 2001-08-09 18:26:47 -0700 (Thu, 09 Aug 2001)
Revision: 3366
Log message:

      This commit was manufactured by cvs2svn to create tag
      'pre-program-state-aware'.

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-10 16:03:52 -0700 (Fri, 10 Aug 2001)
Revision: 3368
Log message:

      Initial stab at representing the program state, its
      associated operations, and general judgements
      about programs.  This may require revisions/total-rewrites
      as I discover how well this actually lends itself to making
      such things as fir_exp state aware.  Eventually, these
      will be given interpretations within ITT.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-10 22:58:46 -0700 (Fri, 10 Aug 2001)
Revision: 3369
Log message:

      Uploading some new files and some minor changes so
      that I can get some help in understanding what is going
      on with the Fir_state / Fir_itt_state code.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-14 00:50:26 -0700 (Tue, 14 Aug 2001)
Revision: 3370
Log message:

      Everything that I had before should be state aware now. :)
      Fir_test now has a few test cases, and more will be needed
      to make sure everything is working properly.
      
      The complex1 test case blows up horribly right now.
      It evaluates perfectly well, but takes an amazingly
      large amount of resources.  The .prlb file (not included) for that
      one proof is 8.4 MB and MetaPRL ~64MB of RAM and 2 minutes on a
      1 GHz Pentium III system.
      After the proof, the "counts" were [2, ~34000] for that proof
      (took me 2 steps).  After restarting MetaPRL and reloading the proof,
      the counts were [2,290483].  Needless to say, something needs
      to be done concerning efficiency.  As far as I can tell, things
      are not being reduced in an optimal order. I'll be looking more
      into this.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-14 13:42:33 -0700 (Tue, 14 Aug 2001)
Revision: 3371
Log message:

      The execution time problem should be pretty much
      fixed now (complex1 in Fir_test should only take
      a few seconds now).  I reduced the amount of induction
      reduction that had to be done.  The code
      still wants a little more testing done it
      at this point.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-14 23:13:06 -0700 (Tue, 14 Aug 2001)
Revision: 3372
Log message:

      Added some terms for convinience and added more test
      cases, many of which were for completeness, if nothing
      else.  The state related code should be fine by now.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-27 10:53:21 -0700 (Mon, 27 Aug 2001)
Revision: 3374
Log message:

      Commit of type checking rules for FIR programs.
      Unlikely that all programs will type check
      properly at this point (some incredibly simple
      expressions don't check as I expected they
      would), but this is something
      to start from and I'm working on cleaning
      some things up.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-27 23:10:50 -0700 (Mon, 27 Aug 2001)
Revision: 3375
Log message:

      I've simplified the syntax of some things
      with regard to the program state.  This has,
      at least initially, made formulating some
      rules for type checking easier.  As of now,
      type checking has a fairly good start.
      Whether the rules are strong enough, and
      whether they work in practice need to
      be tested.