Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-03 10:57:48 -0800 (Wed, 03 Mar 2004)
Revision: 5424
Log message:

      Fixed some bugs in type checking.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-03 23:29:05 -0800 (Wed, 03 Mar 2004)
Revision: 5425
Log message:

      Added "I am stuck where I should not be" error reporting to Naming and CPS.
      Untested for now.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-06 16:05:32 -0800 (Sat, 06 Mar 2004)
Revision: 5427
Log message:

      Fixes to type checking and tuples.  CPS is still broken.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-07 00:30:20 -0800 (Sun, 07 Mar 2004)
Revision: 5430
Log message:

      Added an extra intermediate form of Let so that CPS won't go into an infinite
      loop.  It's still broken but should be easier to debug now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-08 03:26:17 -0800 (Mon, 08 Mar 2004)
Revision: 5433
Log message:

      Allow repeating contexts in redeces (bug 165).
      This is a partial fix (does not allow for full alpha-renaming when comparing
      two context instances) and is not much tested.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 11:42:48 -0800 (Mon, 08 Mar 2004)
Revision: 5435
Log message:

      Added an mcc_main.ml file as the outermost compiler.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 11:56:24 -0800 (Mon, 08 Mar 2004)
Revision: 5436
Log message:

      Added the X86 instruction set.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 12:27:22 -0800 (Mon, 08 Mar 2004)
Revision: 5437
Log message:

      Added an empty code generator based on the M compiler.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 12:29:36 -0800 (Mon, 08 Mar 2004)
Revision: 5438
Log message:

      Added .cvsignore files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-08 12:53:25 -0800 (Mon, 08 Mar 2004)
Revision: 5439
Log message:

      Updated caml-mode to handle quotations correctly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 01:18:33 -0800 (Tue, 09 Mar 2004)
Revision: 5442
Log message:

      Declared the .mlz file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 05:23:47 -0800 (Tue, 09 Mar 2004)
Revision: 5443
Log message:

      Removing the distinction between the Hypothesis and HypBinding - it was
      causing too much trouble unnecessarily complicating a lot of code.
      
      The IO part of the distinction is still there - on IO the "unused" bindings
      are interpreted as variables with an empty "string" part.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-10 11:01:10 -0800 (Wed, 10 Mar 2004)
Revision: 5446
Log message:

      Changes needed by CPS. Added a new resource for type_util.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-10 23:20:39 -0800 (Wed, 10 Mar 2004)
Revision: 5447
Log message:

      Reverting the "uncomment eprintfs" change that Cristian have accidentally
      committed this morning.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-11 17:30:15 -0800 (Thu, 11 Mar 2004)
Revision: 5449
Log message:

      Includes the latest developments in CPS.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-12 17:27:08 -0800 (Fri, 12 Mar 2004)
Revision: 5454
Log message:

      Implemented the grand unified CPS theory.  Exposes a MetaPRL bug.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-13 13:19:13 -0800 (Sat, 13 Mar 2004)
Revision: 5456
Log message:

      Use proper formatting for Invalid_argument and Failure exceptions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-13 15:43:10 -0800 (Sat, 13 Mar 2004)
Revision: 5457
Log message:

      In cpsC, repeat at each node as many times as necessary before descending
      into subterms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-13 18:22:36 -0800 (Sat, 13 Mar 2004)
Revision: 5458
Log message:

      Adding an explicit input type for the exit term.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-15 16:43:27 -0800 (Mon, 15 Mar 2004)
Revision: 5459
Log message:

      Started reorganizing directory structure.  We talked about renaming these files
      but I figured I should wait until we have a firm decision about what the new
      names should be.  The build philosophy for the new layout is that the build
      info lives in the root of the extensions directory tree.  Each extension
      sub-directory contains only code, no build files.  This was a somewhat
      arbitrary choice, but it seems good to me to keep the build control
      centralized.
      
      I know that we are going to put the backend code for each extension in the
      normal extension subdirectory, but what did we decide about the core backend
      code?  Do we leave it the way it is now?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-15 22:44:46 -0800 (Mon, 15 Mar 2004)
Revision: 5461
Log message:

      Adding support for patterns that match _free_ FO variables.
      
      With this commit, any free FO variable in a redex or contractum is taken
      to be a pattern that would match an arbitrary _free_ FO variable. This is
      probably not going to be useful in ITT-like domains, where variables usually
      stand for arbitrary terms (and therefore there is not much difference between
      free FO variables and SO variables), but in programming language domains this
      capability of being able to have patters matching the object-level variables
      should be extremely useful.
      
      On IO, the 'v would still expand into 'v[] _SO_ variable when v is free.
      Therefore, on IO the free _FO_ variables are denoted using the !v syntax.
      
      The new syntax and new rewriting capabilities are not yet used (except in
      the term table, which will now use !v matching) and are not very well tested
      yet.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-15 23:18:25 -0800 (Mon, 15 Mar 2004)
Revision: 5462
Log message:

      The cpsT now works on test_prog1!
      
      TODO:
      - I've added the is_value function to core_type_infer. Currently it just
      checks whether the term is a Lambda, but it should be made resource-driven.
      - I had to add a rule for CPS{ !v; ...} in addition to the
       CPS{ Return{!v}; ...}. Why do we have the two? What is the difference
      between Return{!v} and !v? Should we get rid of Return?
      - The tylambda_intro_base needs to make sure the body of the TyLambda is a
      value.
      - It would be nice to type-check the result of cpsT (at least for testing,
      if not in the compiler proper).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-15 23:40:20 -0800 (Mon, 15 Mar 2004)
Revision: 5463
Log message:

      The test_prog1 and test_prog5 type check after CPS!
      
      A new TODO:
      - A few test progs get stuck on TyCPS{HypsOfList{...}}. This means that we
      have to either get rid of the "Constrain" on cps_var and cps_return, or
      we have to define rewrites for
      sequent[TyCPS{tag}] { <H> >- sequent [tag] { HypsOfList {...} >- ... } }
      (which should not be too hard).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-16 13:38:20 -0800 (Tue, 16 Mar 2004)
Revision: 5464
Log message:

      Added initial x86 code generation for the core.  It doesn't
      handle 1) variables, 2) functions, and 3) application.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-16 14:02:03 -0800 (Tue, 16 Mar 2004)
Revision: 5465
Log message:

      In the current CPS term semantics, there is no need to use Constraint
      when CPS'ing variables and Return statements.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-16 14:24:35 -0800 (Tue, 16 Mar 2004)
Revision: 5466
Log message:

      Migrating to the sequent notation in the backend.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-16 15:23:07 -0800 (Tue, 16 Mar 2004)
Revision: 5467
Log message:

      forgot the .cvsignore files in the new extension directories
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-16 15:40:33 -0800 (Tue, 16 Mar 2004)
Revision: 5468
Log message:

      Added backend support for variables, functions, and application.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-16 15:52:11 -0800 (Tue, 16 Mar 2004)
Revision: 5469
Log message:

      Moved the generic list utilities out of Core_list_util, and
      into Mcc_list_util.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-16 16:24:44 -0800 (Tue, 16 Mar 2004)
Revision: 5471
Log message:

      Getting rid of the Return operator.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-17 15:44:53 -0800 (Wed, 17 Mar 2004)
Revision: 5473
Log message:

      Changed over to Lambda[tag], TyFun[tag] and Apply[tag] in the typed AST.  tag
      can be either "c" for closures or "std" for standard functions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-17 16:31:20 -0800 (Wed, 17 Mar 2004)
Revision: 5474
Log message:

      Changed closure conversion.  This doesnt compile at the moment, to
      be fixed soon.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-17 17:48:40 -0800 (Wed, 17 Mar 2004)
Revision: 5475
Log message:

      Finished closure conversion (maybe, hopefully).
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-17 18:14:25 -0800 (Wed, 17 Mar 2004)
Revision: 5476
Log message:

      Cristian and Aleksey:
      
      - Added macros for including subdirectories from the Mojave theory.
      Now the subdirectories should _not_ have their own OMakefile's, unless
      they want to do something unusual.
      
      - Added minor fixes to get some of the extensions to compile.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-17 21:37:42 -0800 (Wed, 17 Mar 2004)
Revision: 5477
Log message:

      !!! WARNING: With this commit, MetaPRL now requires omake >= 0.7.10 !!!
      
      - Updated the mpconfig to include all the Mojave extensions subdirectories
      - Fixed the "make clean" in the new theories/mojave/OMakefile
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-17 22:21:30 -0800 (Wed, 17 Mar 2004)
Revision: 5478
Log message:

      
      Added a new directory for test files for extensions.
      Updated the extensions to use TyFun['tag] and Apply['tag]
      

Changes by: ( at unknown.email)
Date: 2004-03-17 23:16:41 -0800 (Wed, 17 Mar 2004)
Revision: 5479
Log message:

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

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-18 00:42:08 -0800 (Thu, 18 Mar 2004)
Revision: 5481
Log message:

      Forgot to add the .cvsignore in the test directory.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-18 16:48:16 -0800 (Thu, 18 Mar 2004)
Revision: 5486
Log message:

      Minor changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-18 19:18:25 -0800 (Thu, 18 Mar 2004)
Revision: 5487
Log message:

      Initial pass a code3 generation with closures.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-19 09:21:35 -0800 (Fri, 19 Mar 2004)
Revision: 5490
Log message:

      Added type checking to the codegen phase.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-19 09:25:38 -0800 (Fri, 19 Mar 2004)
Revision: 5491
Log message:

      Changed some :t parameters to :s.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-19 09:43:56 -0800 (Fri, 19 Mar 2004)
Revision: 5492
Log message:

      added a couple well-formedness rules for arrays and integers.
      still missing a couple rules in arrays
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-19 10:21:31 -0800 (Fri, 19 Mar 2004)
Revision: 5493
Log message:

      Added code generation for integers.  Note, binary relations now use
      AtomRelop, not AtomBinop.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-19 10:43:02 -0800 (Fri, 19 Mar 2004)
Revision: 5494
Log message:

      Added code generation for booleans.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-19 15:42:35 -0800 (Fri, 19 Mar 2004)
Revision: 5495
Log message:

      Removed ext_arithmetic files. Moving them to the integer extension
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2004-03-19 16:19:35 -0800 (Fri, 19 Mar 2004)
Revision: 5497
Log message:

      Moved the ext_arithmetic_integer to the integer extension directory.
      
      Fixed CPS, type checking and type inference for all extensions except
      for fix... which is coming next.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-19 17:48:21 -0800 (Fri, 19 Mar 2004)
Revision: 5498
Log message:

      Fixed looping problem in sequent display forms.  There's still a slight visual
      bug, however.  Contexts are displayed as "_:H".
      
      Fixes bug #94.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-19 18:13:40 -0800 (Fri, 19 Mar 2004)
Revision: 5499
Log message:

      A bit nicer display forms for contexts in Mojave nested sequents.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-20 18:49:07 -0800 (Sat, 20 Mar 2004)
Revision: 5504
Log message:

      I've been having trouble with my connection...
      
      1. Added code generation for arrays
      2. Tuples are now an extension, and Core_tuple has been removed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-21 12:34:28 -0800 (Sun, 21 Mar 2004)
Revision: 5505
Log message:

      1. Added code generation for tuples.
      2. Merged the integer files.
      3. The codegen resource is now defined in x86_frame.  This is unfortunate
      .  but necessary, since the utilities in the frame need to be used during
      .  code generation.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-21 12:56:59 -0800 (Sun, 21 Mar 2004)
Revision: 5506
Log message:

      Added code generation for fix.  This is probably wrong, I believe the Fix
      will normally contain a closure application.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 13:51:37 -0800 (Sun, 21 Mar 2004)
Revision: 5508
Log message:

      Jason somehow commited .ml and .mli for an existing .mlz, removing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 15:55:44 -0800 (Sun, 21 Mar 2004)
Revision: 5509
Log message:

      - Changed the dtactic module to use the new API
      (note: this changes the selT semantics slightly and adds full fall-back
      to both intro and elim).
      - Changed the compilers to use the new API.
      - Changed the get_bool_arg, get_sel_arg and get_int_arg to return an option
      instead of raising exception (since we always catch those exceptions anyway).
      
      MetaPRL finally compiles with the new API (but does not really run yet).
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-22 13:35:56 -0800 (Mon, 22 Mar 2004)
Revision: 5516
Log message:

      Completed proof of fun_equal_base.  Closes bug #95.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-22 14:36:03 -0800 (Mon, 22 Mar 2004)
Revision: 5517
Log message:

      Yay, the phone company fixed my DSL!
      
      This is an intermediate commit while I work on the backend.  There are
      some minor changes to the instruction set, and I removed Mcc_x86_inst_type
      because there is no longer any need to convert terms to an ML data type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-22 16:45:40 -0800 (Mon, 22 Mar 2004)
Revision: 5518
Log message:

      Trying to add proper support for .mlz files. I seem to be hitting an omake
      bug with it; committing it anyway to let Jason see it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-22 19:23:29 -0800 (Mon, 22 Mar 2004)
Revision: 5520
Log message:

      This is an initial commit of the x86_backend utilities.  This includes
      the printer, and the conversion to the abstract type used by the register
      allocator.  Still left: standardization and spill code generation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 02:11:41 -0800 (Tue, 23 Mar 2004)
Revision: 5523
Log message:

      !!! WARNING : This commit breaks the .prlb compativility. !!!
      
      !!! This commit makes the "check_status" run about 1.5 times faster !!!
      
      This commit make a major change in how the Term_match_table is imlemented.
      Instead of the hash table at the top only (with linear lookup for subterms)
      this implementation uses the same functional term shape-indexed lookup tables
      at both the top and subterm level. During lookup, this implementation keeps
      an explicit list of "fallback" choices, which makes it easier to return more
      than one match. This implementation is much closer to the one presented
      in the paper submitted to TPHOLs.
      
      This makes a few changes to the semantics of the dT tactic:
      - Previously dT (both elim and intro) would only fall back to another tactic
      if it had the same _term_, now it will fall back to all that have the same
      _pattern_. For example, previously the entries for 'x='y in T, 'a in T and
      'b in T (for a specific T) were all considered separately and at most one
      would be tried, but now when applying the dT to a (t in T), all 3 could be
      tried.
      - Previously, if a pattern had both entires with select argument and entries
      without select argument, then the non-select entries were tried only when dT 0
      was called without the select argument. Now the non-select entries are always
      tried.
      
      This makes a change to the semantics of reduceC as well - now reduceC will try
      _all_ matches (from the most specific to the least specific), not just the most
      specific ones.
      
      The display forms are now handled as a resource, instead of being a "special"
      beast. This may cause the inheritance rules for display forms to change slightly,
      and a few extra "extend" directives might have to be added to compensate.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 09:57:15 -0800 (Tue, 23 Mar 2004)
Revision: 5524
Log message:

      Added the standardizer.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 11:21:43 -0800 (Tue, 23 Mar 2004)
Revision: 5525
Log message:

      Added the spill code generator.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 11:27:24 -0800 (Tue, 23 Mar 2004)
Revision: 5526
Log message:

      Added the coalescing phase.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 11:29:02 -0800 (Tue, 23 Mar 2004)
Revision: 5527
Log message:

      Added the register allocator.  I believe the next step is to define a main
      function to pull all the parts of the backend together.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 11:43:20 -0800 (Tue, 23 Mar 2004)
Revision: 5528
Log message:

      The compiler is now with a complete x86 backend.  Undebugged, though.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-23 16:56:32 -0800 (Tue, 23 Mar 2004)
Revision: 5529
Log message:

      All the parts are complete, now we just need to hook them together.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 17:07:23 -0800 (Tue, 23 Mar 2004)
Revision: 5530
Log message:

      Dulicated the changes that Nathan did:/
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-23 19:05:55 -0800 (Tue, 23 Mar 2004)
Revision: 5533
Log message:

      Minor OMakefile changes to use Mcc_theory as the compiler root.
      
      It seems to me that tests do not belong in extensions because
      we want to test more than just extensions.  What about a directory
      theories/mojave/test?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 19:16:10 -0800 (Tue, 23 Mar 2004)
Revision: 5534
Log message:

      Commenting out the eprintln line.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 11:05:34 -0800 (Wed, 24 Mar 2004)
Revision: 5537
Log message:

      Proper code generation for Ext_int_test.test1.  To see the code, run
      the tactic (coreT thenT codegenT).
      
      Currently, standardization fails because it doesn't handle sequents.
      That's next.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 11:39:47 -0800 (Wed, 24 Mar 2004)
Revision: 5538
Log message:

      Minor fixes in code generation.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 12:55:12 -0800 (Wed, 24 Mar 2004)
Revision: 5540
Log message:

      Partial fix to the register renaming phase.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 14:59:06 -0800 (Wed, 24 Mar 2004)
Revision: 5541
Log message:

      The renameT phase now works for the Ext_int_test.test1 example.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 17:18:13 -0800 (Wed, 24 Mar 2004)
Revision: 5542
Log message:

      Added the Mcc_hoist module, to hoist closed expressions, in particular
      closed lambda expressions, to the top level.  Undebugged for now.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-24 18:15:28 -0800 (Wed, 24 Mar 2004)
Revision: 5543
Log message:

      1.  Fixed some bugs in bools and ints.
      2.  Cooked up a new Mandelbrot test case.  It uses cpp macros and I haven't
      .   worked out how to get omake to build it automatically, so for now I'm
      .   just committing the .ml and .mlp files.  I'll try to fix it...
      3.  Moved all tests to theories/mojave/test.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-24 18:17:26 -0800 (Wed, 24 Mar 2004)
Revision: 5544
Log message:

      Oops, forgot this.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 19:34:49 -0800 (Wed, 24 Mar 2004)
Revision: 5547
Log message:

      Added a couple new stages to the backend:
      .  Mcc_x86_opt1: very simple optimizations
      .  Mcc_x86_convention: make sure the machine conventions are respected
      .    (like at least one operand in a two-operand instruction should
      .     be a register, usually).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 20:02:14 -0800 (Wed, 24 Mar 2004)
Revision: 5548
Log message:

      Working on register allocation.  I get this sad failure:
      .   Failure:
      .       Lm_list_util.remove
      Bah.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-24 20:07:53 -0800 (Wed, 24 Mar 2004)
Revision: 5549
Log message:

      Register allocation seems to do something sensible on test2.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-24 20:45:13 -0800 (Wed, 24 Mar 2004)
Revision: 5554
Log message:

      The .prla needs to be moved too.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-24 22:53:17 -0800 (Wed, 24 Mar 2004)
Revision: 5555
Log message:

      Created a partial Phobos grammar for the Mojave language (a number
      of extension is not fully supported) and converted some of the examples
      in ext_int_test to use Phobos quotations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 11:17:57 -0800 (Thu, 25 Mar 2004)
Revision: 5556
Log message:

      Yay, our first program (ext_int_test/test2) compiles, runs, and
      returns the right answer.  Ok, its only a start.
      
      Added the test/mcc script to run MetaPRL and assemble the output
      to produce an executable.  For example, in theories/mojave/test,
      run the following command.
      
         % ./mcc ext_int_test/test2
      
      This will generate an executable called test2.exe (sorry for the
      suffix, but we need CVS to ignore these files).
      
         % ./test2.exe
         Exit 9
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-25 12:16:53 -0800 (Thu, 25 Mar 2004)
Revision: 5557
Log message:

      Added build instructions to the top comment.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-25 15:30:51 -0800 (Thu, 25 Mar 2004)
Revision: 5558
Log message:

      Added a string extension.  Only constant strings for now.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 16:53:55 -0800 (Thu, 25 Mar 2004)
Revision: 5559
Log message:

      Fixed various bugs with things like using the untyped language
      in places where the typed language should be used.  Fixed a problem
      where the rules for closure conversion were not being used correctly
      in the resource.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 19:31:12 -0800 (Thu, 25 Mar 2004)
Revision: 5560
Log message:

      The hoist phase now lifts out closed functions correctly.
      
      Added a new function Lm_symbol.new_name_gen that acts as
      a new name generator.  See Mcc_hoist for an example of use.
      Sorry about the massive recompile...
      
      Added editor/ml/mpshell for those of use who prefer keeping
      the xterm around.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 20:50:58 -0800 (Thu, 25 Mar 2004)
Revision: 5561
Log message:

      Pretty good code generation for factorial.  The next step is to figure out
      how to eliminate the intermediate mov's.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-25 21:00:30 -0800 (Thu, 25 Mar 2004)
Revision: 5562
Log message:

      Eliminated those pasky mov instructions for function definitions
      in the x86 backend.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-25 21:09:43 -0800 (Thu, 25 Mar 2004)
Revision: 5563
Log message:

      Minor updates (display forms, Core_ast -> Core_base followup fixes, etc).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-25 23:17:47 -0800 (Thu, 25 Mar 2004)
Revision: 5564
Log message:

      Minor clean-up.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-26 10:35:58 -0800 (Fri, 26 Mar 2004)
Revision: 5567
Log message:

      . test_fact compiles, runs, and produces the correct answer!  At this
      . point the compiler is in fair working condition, and we should
      . spend the day organizing the paper.  We can finish the harder
      . examples in parallel.
      .
      . TODO:
      .    1. The quality of the code is pretty bad.  Some notable problems:
      .       a. All relations are bare at this point, even if the result
      .          is only used in a conditional.  We have code like this:
      .
      .          let b = (i == 0) in
      .             if b then e1[] else e2[]
      .
      .          The relation should be migrated into the conditional.
      .
      .          A related note: we are using set/cc to compute bare
      .          relations, but set/cc requires a byte register.  We
      .          will get a failure in the backend if the register
      .          allocator happens to choose %esi or %edi.  It is
      .          probably best to force the register choice here
      .          to, say, %edx.
      .
      .       b. The assembly has far too many register-to-register mov
      .          instructions.
      .       c. It looks like closures are being allocated even for
      .          recursive function calls.
      .       d. We don't do enough constant folding, so we get silly
      .          instruction sequences like this.
      .
      .             add $3, %eax   // eax += 3
      .             dec %eax      // eax--
      .
      .    2. Incomplete parts:
      .       a. Reserve is not implemented, so the garbage collector is
      .          never called.
      .       b. Even for factorial, there are no spills, so the spill
      .          code is not tested.
      .       c. Currently, every function uses the standard calling
      .          convention, where function arguments go in registers
      .          eax, ebx, ecx, edx, esi, edi.  This is both inefficient
      .          and it means we can't handle functions with more than
      .          6 arguments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-26 18:44:40 -0800 (Fri, 26 Mar 2004)
Revision: 5568
Log message:

      Switched all of core_test and more of ext_int_test (including the
      factorial exaple) to the Phobos syntax.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-03-27 22:48:36 -0800 (Sat, 27 Mar 2004)
Revision: 5569
Log message:

      . Mainly a minor cleanup to make the code clearer.
      .     1. Added support for constant memory reservations.
      .        This is done informally, after the formal core operations.
      .     2. Added a few new stages to the backend for optimization,
      .        including register slop code, and dead instruction elimination
      .        (currently, this removes only Mov instructions).
      .
      . Note, Ext_int_test.test_fact is broken with the new parser...
      . I don't know why.  The original code is in Ext_int_test.test_fact_old.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-28 17:07:19 -0800 (Sun, 28 Mar 2004)
Revision: 5570
Log message:

      - Fixed the argument order in the Phobos "let rec" parsing.
      
      - Made the treatment of empty TyAll sequents consistent. Different places
      of the code used to treat << sequent [TyAll] { >- 'ty } >> in different ways:
      .  a) as a TyAll that signifies a that the corresponding expression needs to be
      .  TyApply'ed to nil in order to get an expression of type 'ty
      .  b) as a type that is equivalent to 'ty
      .  c) as an invalid type.
      
      I tried changing it everywhere to use the (a) semantics.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-28 18:42:05 -0800 (Sun, 28 Mar 2004)
Revision: 5571
Log message:

      This commit replaces Perv!cons and Perv!nil with Mcc_list_util!cons and
      Mcc_list_util!nil in all the ast/tast/tuple syntax. This is necessary
      because overriding display forms for Perv!cons and Perv!nil (as we used to do)
      causes problems (for example, comments were displayed incorrectly).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 21:50:09 -0800 (Mon, 29 Mar 2004)
Revision: 5574
Log message:

      Fixing the code that was supposed to complain if more then one rule/rewrite/etc
      had the same name in the same theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 22:05:01 -0800 (Mon, 29 Mar 2004)
Revision: 5575
Log message:

      Adding tail-call optimizations. This makes the asm.s file for the test_fact
      28 (out of 114) lines shorter. The optimizations are mostly added as
      untrusted (interactive) rewrites, but not yet fully proven.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-29 22:34:42 -0800 (Mon, 29 Mar 2004)
Revision: 5576
Log message:

      A number of display form updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-30 19:14:07 -0800 (Tue, 30 Mar 2004)
Revision: 5578
Log message:

      I was finally able to derive the CPS tail call optimizations from eta
      reduction in a reasonable way.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-03-31 00:34:21 -0800 (Wed, 31 Mar 2004)
Revision: 5579
Log message:

      test_fib doesn't compile.  I know it's late to be working on the code, but I
      don't want us to describe a broken CPS in the paper or something.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-31 01:41:20 -0800 (Wed, 31 Mar 2004)
Revision: 5580
Log message:

      Added stuckC error reporting to Codegen.