Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 16:45:01 -0800 (Mon, 03 Mar 2003)
Revision: 4151
Log message:

      - Defined subset, subStructure (which can be used for semigroup, monoid,
        group, etc.), cyclic group (including the power operation for a group
        and cyclic subgroups); and proved corresponding theorems.
      - Adopted Alexei's new syntax.
      - Removed "itt_abelian_group" module, and moved "isCommutative" to "itt_
        grouplikeobj".
      
      Note: The subset module is rather incomplete. It only includes what I
      currently will use.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 16:48:43 -0800 (Mon, 03 Mar 2003)
Revision: 4152
Log message:

      Added itt_cyclic_group and removed itt_abelian_group for documentation.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 18:39:29 -0800 (Mon, 03 Mar 2003)
Revision: 4153
Log message:

      - Moved "csemigroup"(the set of commutative semigroup) and "cmonoid" to
        "itt_grouplikeobj" and "abelg" to "itt_group"
      - Added the intro and elim rules for them. For example:
          'g in group[i:l] & isCommutative{'g} <=> 'g in abelg[i:l]
      - Corrected a typo in the display form of semigroup
      
      I'm not quite sure whether these elimination rules are better or the ones
      that completely unfold, say "abelg" are better. I put the second option
      in comments for now.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 18:43:45 -0800 (Mon, 03 Mar 2003)
Revision: 4154
Log message:

      I've moved "commutative" to "itt_grouplikeobj" and "itt_group".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 21:56:02 -0800 (Mon, 03 Mar 2003)
Revision: 4155
Log message:

      - Redefined "csemigroup", "cmonoid", and "abelg" following Alexei's advice.
      - Reproved corresponding rules.
      - Removed the intro resources.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 23:05:03 -0800 (Mon, 03 Mar 2003)
Revision: 4156
Log message:

      Can anyone take a look at the rule "/itt_group/subgroup_isect"? I can't
      prove it. It states "the intersection (group) of two subgroups is again
      a subgroup".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-04 18:45:52 -0800 (Tue, 04 Mar 2003)
Revision: 4157
Log message:

      - Added some properties and reduction rules of the group power operation.
      - **Partially proved "Every subgroup of a cyclic group is cyclic" with 2 assumptions:
         1. there is a smallest positive number k such that (a^k)_g in s^car;
         2. exst q,c in int. m=q*k+r & 0<=r<k.
      
        The first one should be provable with induction.
        The second is a common theorem in mathematics.
        (I just found that for 2nd assumption, I used r>0 instead of r>=0, but
         this is minor.)
      
      Besides, there are two problems:
      1. Why can't I apply reduceC for "m * 0" in "/itt_cyclic_group/group_power_power_reduce/2" or "/itt_cyclic_group/group_power_power_reduce/2/1"
         and for "mul_uni_Assoc" in "/itt_cyclic_group/group_power_power_reduce/3/1/1/1/1/1/2".
      2. I'll try writing rules like "group_power_0" as reduce resources.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-06 02:45:27 -0800 (Thu, 06 Mar 2003)
Revision: 4158
Log message:

      - Proved that for if there is a positive number x such that P[x], then there
        is a smallest positive number k such that P[k], as long as P[y] is well-formed
        and decidable for any integer y. (rule "smallest_positive")
      - Stated as a separate rule that for any integer k>0 and m, there exists
        integer r>=0 and q such that m=k*q+r. Not proved yet. (rule "int_div_rem")
      - Now "Every non-trivial subgroup of a cyclic group is cyclic" "should" be
        provable other than "type"{(y^a)_g in s.car} is needed for y in g.car and
        a in int, which is not true. Have I made any mistake along the way or is
        this theorem just incorrect here?! (see "/itt_cyclic_group/subg_cycGroup/1/1"
        for example)
        I'll move "If S is a non-trivial subgroup of a cyclic group G generated by b,
        there exists a positive number k such that (b^k)_g in S" as a separate rule.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-08 01:47:03 -0800 (Sat, 08 Mar 2003)
Revision: 4159
Log message:

       - Added reduce resource for group_power;
       - Moved "positiveRule1T", "positiveRule2T", and "int_div_rem" to "itt_nat".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-08 03:43:05 -0800 (Sat, 08 Mar 2003)
Revision: 4160
Log message:

       - First try of defining group homomorphism.
         I define it as a set of all group homomorphisms from G to H. Any comment?
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-10 02:03:15 -0800 (Mon, 10 Mar 2003)
Revision: 4161
Log message:

       - Proved some properties of group homomorphism.
         "Membership is a type iff it is true" also causes problems in proving
         "If f:A->B is a homomorphism and T is is a subgroup of B, then the
          inverse image of T under f is a subgroup of A", as in
          "/itt_group/groupHom_subg2/2" and "/itt_group/groupHom_subg2/3".
      
       - Uncommented some reduce resources in itt_int_ext.
      
       - Added several theorems about grouplikeobj and groups.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-11 00:41:03 -0800 (Tue, 11 Mar 2003)
Revision: 4162
Log message:

      Aleksey & Xin:
      - Added "AutoMustComplete" to a couple of things
      - Added fnExtensionalT and fnExtenT tactics.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-11 13:56:41 -0800 (Tue, 11 Mar 2003)
Revision: 4163
Log message:

      Xin & Aleksey:
      - proved the subgroup intersection theorem (very straightforward,
      but long proof with a lot of subcases)
      - for ... >- f a in A, use intro in autoT
        for ... >- f a = f' a' in A, only use intro with AutoMustComplete
      - added type inference for group components
      - added term contructors/descructors for the field term
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-11 22:30:11 -0800 (Tue, 11 Mar 2003)
Revision: 4164
Log message:

      - Working on cleaning up and documenting the term addresses interfaces
      (unfortunatelly, there are a lot of bugs in both std/gen and ds implementations
      of those and I need to figure out what the expected behaviour is before I can start
      fixing things).
      - Minor typo in itt_record documentation.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-12 09:09:27 -0800 (Wed, 12 Mar 2003)
Revision: 4165
Log message:

      1. itt_bool - equivalence of "x=false in bool" and "assert(not x)".
      2. thenLocalMT, thenLocalAT, onAllLocalMHypsT added, they respect
         local labels instead of inheritted labels.
      3. itt_list2/nth_wf completed. Two issues are done manually:
      3.a. Use of (1)
      3.b. use of splitIntT for transition from "a<>b" to "a<b or a>b"
      4. several bugs fixed in arithT and normalizeC
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-13 01:19:57 -0800 (Thu, 13 Mar 2003)
Revision: 4166
Log message:

      - Messed with the line_buffer and overflow code to get it do actually produce
      the "..." at the end oif the string in case of overflow.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-13 03:04:00 -0800 (Thu, 13 Mar 2003)
Revision: 4167
Log message:

      - Added intro/elim rules for all concepts in itt_grouplikeobj.ml and added
        elim rule for subset.
      - Changed the organization of itt_grouplikeobj.ml. Now each section reflects
        a concept.
      - ...
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-13 17:11:36 -0800 (Thu, 13 Mar 2003)
Revision: 4168
Log message:

      Partially fix an old bug with parser. Now you can write
      squash{'A & 'B}.
      (Previously you had to write squash{('A & 'B)} or squash{.'A & 'B}).
      
      Unfortunately, this fix is only partial:
      squash{iff{'A;'B} & 'C} does not work, you need to write
      squash{(iff{'A;'B} & 'C)}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-14 03:27:05 -0800 (Fri, 14 Mar 2003)
Revision: 4169
Log message:

      - This is a _major change_ in how sequent contexts are now handles in rule
      arguments. Now arguments corresponding to sequent contexts are passed in as _integers_.
      To tell the rewriter that the corresponding context should match n hypotheses,
      pass n + 1 as an argument. Also, if a context is at the _end_ of the hypotheses list,
      it should _not_ be passed as an argument - instead, rewriter will just put all the remaining
      hyps into it.
      
      To summarize, a typical intro-style rule now does not need any context args at all. A typical
      elim-style rule will now need only one context arg ('H) and that argument will be a straight
      integer. That integer will have the same meaning as in traditional tactics - e.g. just
      the hypothesis number. The only difference is that the arguments to primitive rules _have_
      to be positive. Use Sequent.get_pos_hyp_num or pos_hypT to make numbers positive.
      
      - I changed the semantics of the int arg to assertAtT and second int arg to copyHypT. Now
      that int means the hyp number the new hyp will have in the resulting subgoal (whether
      input is positive or negative).
      
      - I fixed some of the proofs Yegor accidentally broke, but not all. Xin, you might have to
      fix some of the cyclic_group proofs yourself, sorry.
      
      - Cleaned up the address part of the TermAddm and TermMan interfaced, killed some
      unnecessary functionality.
      
      - More changes to line_buffer in Rformat - hopefully this time I finally got it right.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-16 12:36:44 -0800 (Sun, 16 Mar 2003)
Revision: 4170
Log message:

      I simplify definition of the subset relation.
      And define membership: <<'x in 'A subset 'B>>.
      But I don't think we will need it, if we are going to redefine usual equality.
      
      Also add two theories:
        itt_singleton  -- defines singleton
        itt_subset2  -- contains some theorems about subset, in particular
      that intersection of two subsets is subset.
      
      I have not finished some proofs. Most unfinished proofs should be done by autoT if autoT would be more clever. (I'm working on it).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-16 19:59:48 -0800 (Sun, 16 Mar 2003)
Revision: 4171
Log message:

      1. Fix broken proofs.
      Some proofs became much shorter. E.g.,
       -Status: `lcoset_subset' is a derived object with a complete proof (8 rule boxes, 3294 primitive steps)
       +Status: `lcoset_subset' is a derived object with a complete proof (2 rule boxes, 314 primitive steps)
      
      I have not fix incomplete proofd.
      
      Now instead of elimination rule for subset relation you can use rule use_subset, use_superset*.
      
      2. Change display form for subtype. Now subtype is \sqsubseteq.
      My intuition is this: all types operators are sharp and square: +, \times, Type, \sqsubseteq.
      And all set operations are nice and circle: \cap, \cup, Set, \subseteq. ;)
      
      3. Add new theories to documentation.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-16 21:16:16 -0800 (Sun, 16 Mar 2003)
Revision: 4172
Log message:

      More on display forms and documentation
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-17 15:59:17 -0800 (Mon, 17 Mar 2003)
Revision: 4173
Log message:

      Updated the list of people so that all sys descr. authors are also listed here.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-17 16:20:59 -0800 (Mon, 17 Mar 2003)
Revision: 4174
Log message:

      Small no-op change in Term_ds address interface (needed to simplify adding
      some additional debugging functionality to it).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-17 16:37:46 -0800 (Mon, 17 Mar 2003)
Revision: 4175
Log message:

      This is the IR for the new letrec.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-17 17:33:08 -0800 (Mon, 17 Mar 2003)
Revision: 4176
Log message:

      I commit my current status of definition of red-black trees.
      This work in progress, everything subject to change.
      I'll commit prla files later.
      
      itt_relation_str defines algebraic structure for ordered sets, sets with decidable equality
      
      itt_set_str  defines data structure for sets.
      
      Also change some display forms.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-17 17:51:38 -0800 (Mon, 17 Mar 2003)
Revision: 4177
Log message:

      Added new theories in print.ml
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-17 19:39:35 -0800 (Mon, 17 Mar 2003)
Revision: 4178
Log message:

      1. Now parser never generate singleton record, but only empty record.
      
      2. Update record_exm to use new syntax.
      
      Still to do:
      
      1. Allow labels to be meta-parameters and arbitrary term.
      
        token_or_sting  = constant label (as now)
        @token_or_sting  = meta-parameter
        anything else = term
      
      Aleksey, do you agree?
      
      2. Rename rcrd -> record,  record -> Record.
      
      As far as field, I think probably it's not a bad name.
      At least in FIR it's called field. I think we want consistency here.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-17 19:51:47 -0800 (Mon, 17 Mar 2003)
Revision: 4179
Log message:

      Fixed some (hopefull all!) bugs where rewrite mechanism was looking (counting
      hyps, taking subterms out, passing to nth*addr, etc) at the goal, while rewrite
      was being applied to an assumption.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-17 20:07:14 -0800 (Mon, 17 Mar 2003)
Revision: 4180
Log message:

      Updated CPS.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-18 16:24:07 -0800 (Tue, 18 Mar 2003)
Revision: 4181
Log message:

      Finally all our proofs replay with TERMS=std!
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-18 16:29:41 -0800 (Tue, 18 Mar 2003)
Revision: 4182
Log message:

      Updated closure conversion/dead code elimination/inlining to use the
      new representation of functions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-18 18:23:51 -0800 (Tue, 18 Mar 2003)
Revision: 4183
Log message:

      - The rewriter now correctly makes sure that the SO var args have
      to be distinct for it to be a potential "poattern" source (and not
      just an instance). This fixed BUGS 4.11 and allows eliminating the
      "HACK" terms in itt_*isect
      
      - free_vars_terms now returns StringSet.t, not string list
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-18 21:25:05 -0800 (Tue, 18 Mar 2003)
Revision: 4184
Log message:

      Generate initial assembly for the M language.
      This is before register allocation; that's next.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-18 22:36:02 -0800 (Tue, 18 Mar 2003)
Revision: 4185
Log message:

      - I moved the sequent-related *_addr functions from TermMan to TermAddr
      - I got rid of the TermSimleSig signature, use TermSig instead
      - The Lib_term module now uses the Term_man_gen for converting
      from/to term representation of sequents instead of reimplementing it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-19 14:14:00 -0800 (Wed, 19 Mar 2003)
Revision: 4186
Log message:

      Changed instruction format to use string parameters, like this:
         Inst2["mov":s]{'dst; 'src; 'rest}
      
      Added code to manage built-in registers.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-19 19:33:42 -0800 (Wed, 19 Mar 2003)
Revision: 4187
Log message:

      Added code to split a live range.
      

Changes by: ( at unknown.email)
Date: 2003-03-19 19:33:42 -0800 (Wed, 19 Mar 2003)
Revision: 4188
Log message:

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

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-19 22:45:00 -0800 (Wed, 19 Mar 2003)
Revision: 4189
Log message:

      Fixed a typo.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-20 00:13:58 -0800 (Thu, 20 Mar 2003)
Revision: 4190
Log message:

      - Finished the proofs (and cleaned up) in ctt_markov
      - Cleaned up czf_itt_bool to get rid of the error messages those
      "saved on the side" subproofs generate.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-20 00:54:48 -0800 (Thu, 20 Mar 2003)
Revision: 4191
Log message:

      Killed some unused code.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-20 02:06:15 -0800 (Thu, 20 Mar 2003)
Revision: 4192
Log message:

      Changed some rule names for consistence.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-20 14:19:08 -0800 (Thu, 20 Mar 2003)
Revision: 4194
Log message:

      This is a branch commit.
      
      Added lm_libmojave to MetaPRL.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-20 15:33:50 -0800 (Thu, 20 Mar 2003)
Revision: 4195
Log message:

      Added register allocator code.  So far unused.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-20 17:11:36 -0800 (Thu, 20 Mar 2003)
Revision: 4196
Log message:

      Added x86 backend description.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-20 17:16:26 -0800 (Thu, 20 Mar 2003)
Revision: 4197
Log message:

       - Fixed some broken proofs.
       - Updated structure of itt_group.
       - subStructure and subgroup need redefining and anything related with
         subgroup needs to be updated.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-20 17:35:40 -0800 (Thu, 20 Mar 2003)
Revision: 4198
Log message:

      Commited some proofs.
      Most of the proofs are incomplete (if not all of them).
      If they broke, it would be ok, I am going to change them anyway.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-20 17:49:30 -0800 (Thu, 20 Mar 2003)
Revision: 4199
Log message:

      Added main call to register allocator.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-20 19:07:23 -0800 (Thu, 20 Mar 2003)
Revision: 4200
Log message:

      Changed the srripts to include the module name in each "status" line
      along with the rule name - this makes the logs much easier to read
      (no need to be guessing where the rule came from).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-20 22:02:32 -0800 (Thu, 20 Mar 2003)
Revision: 4201
Log message:

      Register allocation runs and produces an assignment, but we
      fail alpha-equality.  Hard to debug...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-20 22:50:59 -0800 (Thu, 20 Mar 2003)
Revision: 4202
Log message:

      The problem with alpha-equality was because some MOVs _must_
      be coalesced.  Specifically, Let{Register{v}, v. e['v]} must
      be coalesced.
      
      This makes the first successful register allocation of the fib
      program.
      
      What's left:
         1. Functions must use a standard calling convention, rather
            than having the allocator choose locations of arguments
            at random.
         2. The LetReg[reg:s]{'src; v. 'e[v]} requires that v be the
            specific register mentioned in the parameter.  The register
            allocator currently ignores them.
      
      Once that's done, we need to pull the runtime from the class version
      of fjava, and try compiling for real.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 01:16:52 -0800 (Fri, 21 Mar 2003)
Revision: 4203
Log message:

      Proved couple of rules that used to be prim.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 01:49:42 -0800 (Fri, 21 Mar 2003)
Revision: 4204
Log message:

      Added a set membership elimination rule.
      
      Alexei, what's your take on membership elimination rules in general - how should
      we manage those? Proving a separate mem. elim for each elim seems somewhat silly...
      Alos, what's a good place for this rule? In can not go into itt_set since it requires
      itt_logic, but itt_struct2 does not seem right either.
      

Changes by: ( at unknown.email)
Date: 2003-03-21 01:49:42 -0800 (Fri, 21 Mar 2003)
Revision: 4205
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 04:25:13 -0800 (Fri, 21 Mar 2003)
Revision: 4206
Log message:

      ***                WARNING                   ***
      *** This check-in breaks .prlb compatibility ***
      *** Export any unsaved proofs to .prla       ***
      *** before running "cvs update"              ***
      
      - I have added support for Hypothesis that do not introduce a binding variable.
      I do not yet have much I/O support for them - there is no mechanism yet for
      inputing such hypotheses explicitly and the display format for them is not
      ideal. I will add this later.
      
      Note:
      1) A hypothesis with an unused binding and a hypothesis without a binding are
      considered equivalent (e.g. in alpha equality comparisons).
      2) All the sequents on _rule box_ level are normalized. When a sequent is normalized,
      all the binding hyps that introduce an unused variable a changed to non-binding ones
      (ideally - for some reason it does yet not always work correctly).
      3) If you want to give a name to a no-name variable, use nameHypT or nameHypsT tactic.
      Note that you have to use that name right away in the _same_ rulebox, otherwise
      normalization (see note 2) will remove it again!
      I plan to extend nameHypT/nameHypsT to be able to rename existing bindings as well,
      but have not done that yet.
      
      - I have changed the way variable names are handled in the rewriter - now it
      will watch them much more carefully, most of the bugs related to the variable
      names are fixed (but a few still remain).
      
      - I fixed all the proofs these changes broke (there were quite a few), except for
      /itt_record/recordEliminationL
      
      - vnewname: now "v_1" would be renamed into "v_2", not "v_1_1"
      
      - I bumped MetaPRL version number to 0.8
      - I bumped the ASCII version number to 1.0.1 (it will still read the old 1.0.0,
      but will correctly mark all new .prla as 1.0.1 which will prevent the old MetaPRL
      from thinking it can read them)
      - I changed the magic numbers for .prlb (or at least I hope I did it correctly), so
      hopefully it will ignore any old .prlb you might have and not crash on them.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 05:24:23 -0800 (Fri, 21 Mar 2003)
Revision: 4207
Log message:

      Print a meaningful error message (as opposed to uncaught Not_found) when
      a magic number does not match.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 09:45:08 -0800 (Fri, 21 Mar 2003)
Revision: 4208
Log message:

      Restored the TESTS=yes compile.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-21 09:51:49 -0800 (Fri, 21 Mar 2003)
Revision: 4209
Log message:

      Tailcalls take a variable number of arguments.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-21 11:08:54 -0800 (Fri, 21 Mar 2003)
Revision: 4210
Log message:

      Added memory reserve statements to control GC.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-21 21:34:25 -0800 (Fri, 21 Mar 2003)
Revision: 4211
Log message:

      | Register allocator now adheres to calling convention.
      | We need some work on the spills:
      |     1. The choice of variables to spill is very bad (this
      |        must be affecting us in mcc as well).
      |     2. The MetaPRL spill code needs to be smarter.  Given a
      |        variable "v" to spill, it splits the live range of that
      |        variable by inserting this code in a random location,
      |        then trying to migrate the top move up, and the bottom
      |        move down.
      |
      |           MOV %v, spill
      |           MOV spill, %v
      |
      |        The choice of the location is currently quite bad.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 21:44:50 -0800 (Fri, 21 Mar 2003)
Revision: 4212
Log message:

      - Be even more strict about the variable name clashes (now that hypSubstT
      in Itt_record.recordEliminationL will not be allowed).
      
      - I reordered the args in StringSet.remove to be able to use fold_left
      instead of fold_right.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-22 08:29:26 -0800 (Sat, 22 Mar 2003)
Revision: 4213
Log message:

      Prove of int_div_rem is 80% complete.
      Only some local problems with my normalizeC/arithT remain.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-22 09:22:43 -0800 (Sat, 22 Mar 2003)
Revision: 4214
Log message:

      Forgot two important branches.
      For some reason "export" raises "Not found" exception so I deleted previous
      .prla file before exporting.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-22 14:17:51 -0800 (Sat, 22 Mar 2003)
Revision: 4215
Log message:

      One very important thing I forgot in the last commit: I converted
      the assembly to use three-operand register instructions.  What this
      really means is that all assignments to registers are binding
      occurrences.  In other words, registers are immutable, and we can
      call this functional assembly code (an oxymoron if I ever heard one).
      This allows much greater flexibility in assembly code motion.
      The printer knows how to print these so that they are valid.
      For example, the instruction ADD (src1, src2, dst) prints as:
      
          add src1, dst   /* if src2 = dst (dst is a register) */
      or
          mov src2, dst   /* if src1 != dst */
          add src1, dst
      
      This commit makes a change to Jcc.  They now look like regular
      conditionals, so the assembly has the usual tree structure.
      The printer knows how to print so that this is actually valid
      assembly.
      
      This change makes it easier to move code into the branches of
      the conditional.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-22 17:15:41 -0800 (Sat, 22 Mar 2003)
Revision: 4216
Log message:

      We now generate code the assembles without errors.
      Added a few assembly optimizations too.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-22 19:08:38 -0800 (Sat, 22 Mar 2003)
Revision: 4217
Log message:

      Implemented Alexei's suggestion for the meaning of negative seq. context
      argumets in the rewriter.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-22 20:40:13 -0800 (Sat, 22 Mar 2003)
Revision: 4218
Log message:

      | Yes!  Our first working program is fib!  It is just about as fast
      | as the MCC version from what I can tell.
      |
      | 1. Added the runtime.
      | 2. Random fixes in the other files.  Especially, CPS was broken
      |    (and we should examine it carefully soon), and Reserve was
      |    computed wrong.
      | 3. Integer arithmetic is now 31-bit so the GC can tell between a
      |    pointer and integer.  Need to examine the shifting in M_x86_codegen.
      |    I think Shift will fail on some operands.
      

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-03-23 02:24:53 -0800 (Sun, 23 Mar 2003)
Revision: 4219
Log message:

      Updated the M parser to use records for functions.
      Also added the fib test case in m_test.ml.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-23 07:02:37 -0800 (Sun, 23 Mar 2003)
Revision: 4220
Log message:

      ***                WARNING                ***
      *** This breaks prlb compatibility again! ***
      
      - I got rid of the variable arguments to rules and rewrites. Now the rewriter
      handles all the variable naming internally.
      - All the maybe_new_vars1 - maybe_new_vars9 functions are gone. When creating
      a bind term by var_subst, instead of creating a new variable for it, call
      Perv.var_subst_to_bind
      - To rename a variable in a hypothesis, use the nameHypT tactic - it
      now can handle both binding and binding-free hyps.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-23 12:23:15 -0800 (Sun, 23 Mar 2003)
Revision: 4221
Log message:

      Got rid of the signature files that were only used once.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-23 13:41:36 -0800 (Sun, 23 Mar 2003)
Revision: 4222
Log message:

      In process of completing itt_nat/int_div_rem and debugging the arith tactic.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-03-23 14:42:38 -0800 (Sun, 23 Mar 2003)
Revision: 4223
Log message:

      Some typo fixes to documentation.  (I'm tempted to go through and
      fill out all the documentation, but probably it is not worth it
      just yet.)  Minor tweak to the LetTuple display form.
      
      I think I get the basics of the IR.  Only one statement really
      confuses me at this point:  ``For now, variables are represented
      as variables; we don't need separate atoms.''  Then what is
      AtomVar for?  I am guessing that that statement is out-of-date.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-23 18:02:46 -0800 (Sun, 23 Mar 2003)
Revision: 4224
Log message:

      "subgoals" debug variable added.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-23 18:17:07 -0800 (Sun, 23 Mar 2003)
Revision: 4225
Log message:

      Enforce the type distinctions in Ascii_io (it used to be unnecessary,
      but now an entry for a binding-less hyp can look exactly the same as
      an entry for a binding-less bterm!). This was what cause the "Not_found"
      problems when re-exporting some .prla files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-23 18:55:45 -0800 (Sun, 23 Mar 2003)
Revision: 4226
Log message:

      eflush should be passed via %t, no need to call it on a separate line.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-03-23 19:46:10 -0800 (Sun, 23 Mar 2003)
Revision: 4227
Log message:

      | Whew!  Fixed the register allocator, and completely rewrote the spill code.
      | Current allocation performance is excellent.  We might try to migrate these
      | ideas into mcc, though it may not be as easy to express.
      |
      | The main spill algorithm is this.
      |
      |    1. Remember that the assembly has only one def for each var.
      |       Remember we are pretending that we have three-operand instructions.
      |
      |    2. When a variable $v$ is selected for spilling:
      |       a. add this code after the def:
      |
      |             add src1,src2,%v      // For example
      |             mov %v, spill[name]   // This is a binding occurrence of name
      |
      |       b. convert all following uses of the variable
      |          to the operand (SpillRegister (v, name)).
      |
      |       c. add a mov before each use
      |
      |             mov SpillRegister (v, name), v'
      |
      |          and daisy-chain these mov's so that there is at most two
      |          uses for each spilled var (one for the real use, and one
      |          to copy the daisy-chain).
      |
      | The meaning of SpillRegister (v, name) is that the value is in _both_
      | the register and the spill area.  The reason for the daisy-chain is so
      | the register allocator can now spill only part of a live range.
      |
      |    3. If the register allocator decides to spill part of a daisy-chain,
      |       that part looks like this:
      |
      |          mov %v, spill[name]
      |          ...lots of code that does not use v...
      |          mov SpillRegister (v, name), v'
      |          add 'v, dst
      |
      |       Convert this code to:
      |
      |          mov %v, spill[name]
      |          ...lots of code that does not use v...
      |          mov spill[name], v'
      |          add v', dst
      |
      |       That is, forget that the spill was ever in the register, and
      |       just fetch it from the memory area.
      |
      | Spill variables have to be coalesced just like registers, but I
      | haven't gotten to it.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-23 20:34:05 -0800 (Sun, 23 Mar 2003)
Revision: 4228
Log message:

      Minor modifications of debug and error reporting code according to Aleksey's
      recommendations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-23 22:30:32 -0800 (Sun, 23 Mar 2003)
Revision: 4229
Log message:

      Fixed a bug in alpha equality...