Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-05 14:49:58 -0700 (Thu, 05 Aug 2004)
Revision: 6114
Log message:

      This syntax.pho seems to not be used at all.  The one in test is used.
      

Changes by: ( at unknown.email)
Date: 2004-08-06 17:06:32 -0700 (Fri, 06 Aug 2004)
Revision: 6116
Log message:

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

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-06 17:23:21 -0700 (Fri, 06 Aug 2004)
Revision: 6117
Log message:

      The parser now supports mutual recursion, of the form:
          let rec foo(x, y) = 27*x + y - baz(x*y)
              and bar(z) = foo(2, z)
              and baz(w) = w*w
          in e
      
      converting this to a term like:
          ULetFunDecl{| foo:UTy; bar:UTy; baz:UTy >-
          ULetFunDef{| FunDef{'foo; ULambda{...}}; FunDef{'bar; ULambda{...}};
              FunDef{'bar; ULambda{...}} >- e |} |}
      
      I also added display forms that seem to work ok, though the paren precedence for
      lambdas is a bit wacky.  This is a pre-existing condition, however.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-11 19:13:21 -0700 (Wed, 11 Aug 2004)
Revision: 6119
Log message:

      First stab at type inference for let rec.  This is *really* complicated and it
      doesn't work yet.  I'm sure there's a better way.  I'll try to work on it in
      Seattle but I probably won't be able to do much, so hopefully I can fix it on
      Monday.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-12 00:12:29 -0700 (Thu, 12 Aug 2004)
Revision: 6120
Log message:

      Slightly less broken type inference for let rec.  Needed to add an equation
      between each inferred function type and the corresponding assigned function
      type.  At the moment I just assign a type var for the function type.  It works,
      but eventually I'll change it to a TyFun with the correct arity.
      
      I also cleaned up the code a bit and added another test case.  This version
      correctly infers test_letrec but not test_letrec2.  I'm not sure where those
      darn free type variables are coming from.  Why must *every* variable be bound?
      Are we so variables so dangerous that society cannot tolerate them roaming free?
      How will history judge us, who bind our variables so tightly?
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-18 16:50:37 -0700 (Wed, 18 Aug 2004)
Revision: 6121
Log message:

      A quick commit before trying a new direction with type inference.  We now think
      that each recursive function should only be quantified over its free type
      variables, not the union of all free type variables from all functions.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-19 16:58:30 -0700 (Thu, 19 Aug 2004)
Revision: 6122
Log message:

      Switched AtomTyApply{'e; 'e_ty; 'ty_args} so that 'ty_args is a sequent, similar
      to the change to Apply.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-19 18:57:37 -0700 (Thu, 19 Aug 2004)
Revision: 6123
Log message:

      Argh.  I now come really close to correct results but I can't get the binding
      structure to come out right.  I get things like:
      
          foo : \all(ty_x100). ( ty_x100 ) -> ty_x100 =
              \lambda(x:!ty_x100). x
      
      Notice that the ty_x100 in the lambda is unbound.  I don't know what's wrong.
      Jason, maybe you can take a look at test_letrec2 and infer_letfuns to see if you
      notice a problem.
      
      One thing that might be an issue -- the function bodies are inferred without
      their quantified types in the tenv.  I don't know what effect that might have.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-24 11:48:23 -0700 (Tue, 24 Aug 2004)
Revision: 6128
Log message:

      Type inference for recursive functions works now.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-24 18:18:29 -0700 (Tue, 24 Aug 2004)
Revision: 6129
Log message:

      Implemented type checking for recursive functions.  There's a hack to work
      around bug 175.  Also, it's inefficient but I'm going to improve it.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-24 18:21:08 -0700 (Tue, 24 Aug 2004)
Revision: 6130
Log message:

      Oops, accidentally commited a bogus version of one file.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-25 19:29:26 -0700 (Wed, 25 Aug 2004)
Revision: 6138
Log message:

      A fix for type checking of let rec.
      Also cleaned up display forms quite a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 22:54:44 -0700 (Wed, 25 Aug 2004)
Revision: 6141
Log message:

      The MMC part of the df_context commit I just made. With this change, I
      get the correct behavior for contexts in LetFun* sequents:
      
      # << LetFunDecl{| <H>; f: 'ty >- LetFunDef{| <J> ; FunDef{'f; 'def[]} >- 'f |} |} >>;;
      (* Recursive functions: <?\239?\191?\189?\239?\191?\189>, f : !ty *) let rec <?\239?\191?\189?\239?\191?\189> and f = def in f : term
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-26 18:35:32 -0700 (Thu, 26 Aug 2004)
Revision: 6142
Log message:

      This is a branch to bring metaprl in line with the omake branch.
      98% of these changes are just to .cvsignore files, which should
      ignore .omc and .omo generated files.
      
      There are a few changes to OMakefiles.  This is because
      the $'(...) sequence has been replaced by $`(...).
      $'a b c' is now symmetric with $"a b c", as a quotation.
      $'...' does not expand variables in the quotation, $"..." does.
      
      This will probably be a very short-lived branch...
      We can remove the tag later if this is a problem.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-26 18:48:03 -0700 (Thu, 26 Aug 2004)
Revision: 6143
Log message:

      Merging letfun branch
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-26 19:00:03 -0700 (Thu, 26 Aug 2004)
Revision: 6144
Log message:

      Ignore default CVS files in the include path.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-27 15:11:21 -0700 (Fri, 27 Aug 2004)
Revision: 6145
Log message:

      Fixed type checking so it's not quadratic in the number of recursive functions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-27 20:23:35 -0700 (Fri, 27 Aug 2004)
Revision: 6146
Log message:

      More .cvsignore changes.
      I should have committed the book changes to the trunk....
      Well, this brings MetaPRL in line with the latest omake changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-27 20:35:06 -0700 (Fri, 27 Aug 2004)
Revision: 6147
Log message:

      More .cvsignore changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-29 19:09:44 -0700 (Sun, 29 Aug 2004)
Revision: 6148
Log message:

      Merged the shell_begin branch.