Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-04 11:58:04 -0700 (Mon, 04 Aug 2003)
Revision: 4812
Log message:

      Latest version of the mojave/core files
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 13:34:06 -0700 (Mon, 04 Aug 2003)
Revision: 4813
Log message:

      The new explicit-contexts code discovered a bug, now we have to
      figure out how to fix it.
      
      Consider the following rewrite, which is obviously sensible.
      
         Lambda{x. 'e['x]} : TyAll{y. 't['y]}
         <-->
         Lambda{x. TyConstrain{'e['x]; 't['x]}} : TyAll{y. 't['y]}
      
      Now consider the sequent form, which does something similar,
      but fails because of the context substitution.
      
         sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
         <-->
         sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
         sequent [TyAll] { <H> >- 't<|K|> }
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 17:37:15 -0700 (Mon, 04 Aug 2003)
Revision: 4814
Log message:

      This is an unsatisfying workaround to the context scoping
      problem.  As mentioned in the previous commit, this is what
      we want:
      
       sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
       <-->
       sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
       sequent [TyAll] { <K> >- 't<|K|> }
      
      We should really get this notation to work.  In the meantime,
      we use this workaround:
      
       sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
       <-->
              collect{ty_vars. sequent [Lambda] { <H> >-
                 TyConstrain{'e; Apply{sequent [Lambda] { <K> >- 't<|K|> }; 'ty_vars}} :
       sequent [TyAll] { <H> >- 't<|K|> }
      
      Remember, collect{ty_vars. sequent [...] { <H> >- ... }} builds
      a list of the binding vars in <H>.
      
      That is, we use beta-reduction to perform an explicit substitution.
      It should work, but makes the code large, slow, and ugly.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 17:55:27 -0700 (Mon, 04 Aug 2003)
Revision: 4815
Log message:

      mojave/core now compiles.  Next step is to do some testing.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 18:08:18 -0700 (Mon, 04 Aug 2003)
Revision: 4816
Log message:

      Added CPS conversion tactic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-06 14:20:48 -0700 (Wed, 06 Aug 2003)
Revision: 4817
Log message:

      Added some support for sequent operations.
      
      subC now works correctly for sequents, but the sequent test is in the
      inner loop, so it will be a little slower.
      
      Haven't changed higherC yet.
      
      Added sequent support in Term_op_ds.{map_up,map_down}.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-07 16:25:08 -0700 (Thu, 07 Aug 2003)
Revision: 4818
Log message:

      Nathan and I came up with a few testcases...
      
      Unfortunatelly metaprl doesn't refine any of the testcases...
      
      We also ran into a few problems when compiling metaprl with omake.
      Apparently there are a few OMakefiles missing in directories like
      lib, editor...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-11 14:31:31 -0700 (Mon, 11 Aug 2003)
Revision: 4821
Log message:

      . Fixed several things to work with sequents.
      .    1. In apply_redex, return *something* for a StackSeqContext.
      .       Even though we can't return the right thing, this should
      .       not fail.
      .    2. term_match_table now works with sequents.
      .
      . It is possible to define display form for sequents the normal way.
      . See core_ast.ml for an example.
      .
      . In core, the namer now works, type inference is stuck because
      . Unify_mm needs to be upgraded to work with sequents.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-11 17:11:22 -0700 (Mon, 11 Aug 2003)
Revision: 4822
Log message:

      Tuples code added. It compiles...
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-11 20:29:33 -0700 (Mon, 11 Aug 2003)
Revision: 4825
Log message:

      Added some files that were missing. I wonder why cvs doesn't flag
      them to me when I do an update...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-12 11:44:27 -0700 (Tue, 12 Aug 2003)
Revision: 4826
Log message:

      Made some progress on unification.
      
      NOTE: Aleksey, there are various problems with sequents in
      Rewrite.extract_redex_values.  I've marked them with a BUG
      comment, and you should look when you get a chance.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-12 12:09:51 -0700 (Tue, 12 Aug 2003)
Revision: 4827
Log message:

      Tell infer_fun_type to pay attention to Hypothesis values
      as well as HypBinding.
      
      Here is the latest error:
      Uncaught exception: Invalid_argument("Rewrite_match_redex.check_sequent_hyps: binding clash in a sequent. Please let Aleksey Nogin know if this happens to you.")
      
      Apparently, we are creating sequents somewhere with shadowing in the hyps.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-12 12:52:40 -0700 (Tue, 12 Aug 2003)
Revision: 4828
Log message:

      Turned off the hyp check so that we can at least see the sequents.
      However, it looks like my hack in Unify_mm doesn't work like we want.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-12 18:25:45 -0700 (Tue, 12 Aug 2003)
Revision: 4830
Log message:

      Committing today's work.  I've been having CVS issues so I hope this doesn't
      screw everything up...
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-12 18:27:42 -0700 (Tue, 12 Aug 2003)
Revision: 4835
Log message:

      Adding new files from today.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-13 13:36:46 -0700 (Wed, 13 Aug 2003)
Revision: 4838
Log message:

      Type inference appears to complete on simple cases.
      
      There is something strange going on with rwc--it sems to
      be rewriting the proof, not the goal.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-14 17:03:22 -0700 (Thu, 14 Aug 2003)
Revision: 4840
Log message:

      Adding topval closeT.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-14 17:09:32 -0700 (Thu, 14 Aug 2003)
Revision: 4841
Log message:

      Adding extensions for integers and arithmetic.
      

Changes by: ( at unknown.email)
Date: 2003-08-14 17:09:32 -0700 (Thu, 14 Aug 2003)
Revision: 4842
Log message:

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

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-17 01:43:15 -0700 (Sun, 17 Aug 2003)
Revision: 4843
Log message:

      Here is a compiling version of metaprl which includes the integers and
      arithmetics on integers that I and Nathan worked on on Thursday plus
      a version of arrays of ints that I came up with on Friday.
      
      Today I created display forms for integers and binops and fixed
      a few type inference issues.
      
      There are still problems with both arithmetics and arrays...
      Type inference doesn't work as we want it to. I am a bit confused on
      what exactly needs to be done to fix it but I will try to look at it
      again tomorrow morning.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-18 14:23:15 -0700 (Mon, 18 Aug 2003)
Revision: 4847
Log message:

      Some more changes... I don't know why all the files say they were touched...
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-18 16:37:16 -0700 (Mon, 18 Aug 2003)
Revision: 4848
Log message:

      Just a brief commit while moving to a different machine.
      

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-08-18 17:13:09 -0700 (Mon, 18 Aug 2003)
Revision: 4849
Log message:

      Merged mojave_sequents branch back to the trunk.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-19 20:08:04 -0700 (Tue, 19 Aug 2003)
Revision: 4851
Log message:

      Cleaned up display of sequents a bit in simple_print.
      
      Also fixed bug that was causing core_test/test_prog1 to fail.  The problem was
      that this doesn't work:
      .   match explode_term t with
      .       << sequent ['foo] { ... }
      .               when alpha_equal foo << Foo >> ->
      
      The last line actually needs to be:
      .               when alpha_equal foo << sequent_arg{Foo} >> ->
      
      Ah, the joys of untyped languages...
      
      That fixed test_prog1, but test_prog2 now fails.  Beware, there's lots of grubby
      debugging output in core_type_infer.ml...
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-19 22:25:49 -0700 (Tue, 19 Aug 2003)
Revision: 4854
Log message:

      Forgot to cvs add these guys.  Thanks Jason.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-19 22:28:39 -0700 (Tue, 19 Aug 2003)
Revision: 4855
Log message:

      These are important too...
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-20 17:28:31 -0700 (Wed, 20 Aug 2003)
Revision: 4860
Log message:

      Type inference is now working on test_prog[1-2].  Haven't tried any other cases
      yet.  Changed simp_typeinf to take a tenv *and* a venv.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-25 16:17:08 -0700 (Mon, 25 Aug 2003)
Revision: 4876
Log message:

      Matching sequents is now a bit simpler.  You don't need to use "with" clauses to
      match on sequent arguments because now this works correctly:
          match explode_term t with
              << sequent [Lambda] { <args> >- 'e } >>
      
      Also includes some new test cases and random minor changes.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-25 17:18:42 -0700 (Mon, 25 Aug 2003)
Revision: 4877
Log message:

      Type inference for arrays was broken if anything (the array, the index, etc)
      had an undetermined type.  (See ext_int_test/{test3_0,test3_1,text6} for test
      cases that trigger the bug.  I fixed it for construction and subscript, but
      don't have time to fix set_subscript at the moment.  I'll try to fix it tonight
      unless some enterprising fellow beats me to it... :-)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-27 12:38:57 -0700 (Wed, 27 Aug 2003)
Revision: 4883
Log message:

      - Removed (using the util/clean-opens script) approx. 2400 unneeded "open"
       statements. This will hopefully reduce the dependency tree size, reduce
      the dependency analysis time during compilation and possibly speed up
      some partial compilations.
      
      - Removed a number of blank lines (MetaPRL policy is to try not to have more
      than one blank line in a row)
      
      - A few minor changes to better disambiguate cases where two modules declare
      a type with the same name and both modules are opened.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-27 23:57:37 -0700 (Wed, 27 Aug 2003)
Revision: 4891
Log message:

      Finished fixing type inference for arrays.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-28 00:01:39 -0700 (Thu, 28 Aug 2003)
Revision: 4892
Log message:

      Don't need to do any matching when inferring the type of an Integer literal.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-29 02:19:15 -0700 (Fri, 29 Aug 2003)
Revision: 4898
Log message:

      Removing a few more unused "open" statements.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-08-29 17:44:32 -0700 (Fri, 29 Aug 2003)
Revision: 4902
Log message:

      Trivial change.