Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-12 17:41:54 -0800 (Wed, 12 Jan 2005)
Revision: 6392
Log message:

      osh version of compile script.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-13 17:29:24 -0800 (Thu, 13 Jan 2005)
Revision: 6397
Log message:

      Hoisting is partially implemented.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-13 19:17:14 -0800 (Thu, 13 Jan 2005)
Revision: 6400
Log message:

      This is the non-working version of hoisting.
      The problem is hoisting recursive functions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-13 23:06:12 -0800 (Thu, 13 Jan 2005)
Revision: 6402
Log message:

      The MMC part of my yesterday's dT changes
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-15 19:54:43 -0800 (Sat, 15 Jan 2005)
Revision: 6409
Log message:

      Moved the meta_let, etc. to Mmc_base_meta.
      
      Making progress on hoisting, but I've run into a rewriter bug I believe.
      See the rewrite Mmc_core_hoist.hoist_letrec.  As far as I know, this rewrite
      should work, but I get the following error:
      
      Invalid Argument:
         Rewrite_match_redex.extract_cont_bvars: invalid stack entry: StackVoid
      
      I guess this means the rewriter did not extract a context correctly.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 12:57:40 -0800 (Sun, 16 Jan 2005)
Revision: 6413
Log message:

      Working version of hoisting.
      
      Currently, the result of hoisting is a mix of non-recursive and
      recursive functions.
      
         let hoist f1 = lambda ... in
         let rec f2 : ty2
         and f2 = lambda ...
         in
            e
      
      I'd like to combine these all into a single letrec,
      but for that we need to compute the type of a
      nonrecursive function.
      

Changes by: ( at unknown.email)
Date: 2005-01-16 12:57:40 -0800 (Sun, 16 Jan 2005)
Revision: 6414
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 18:53:03 -0800 (Tue, 18 Jan 2005)
Revision: 6436
Log message:

      The MMC part of the single-conclusion sequents change (untested)
      

Changes by: ( at unknown.email)
Date: 2005-01-19 21:21:00 -0800 (Wed, 19 Jan 2005)
Revision: 6450
Log message:

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 19:57:51 -0800 (Sun, 23 Jan 2005)
Revision: 6481
Log message:

      Adding types.  This won't compile until I push through the changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-24 22:55:29 -0800 (Mon, 24 Jan 2005)
Revision: 6500
Log message:

      Upgrading mmc.
      
      Currently in Mmc_core_type_check.
      
      Judgments like the following are a problem.
      
         sequent { <H> >- LetFunDecl{| <J> >- LetFunDef {| <K> >- 'prop |} |} }
      
      We *could* make such typings as the follows:
      
         LetFunDecl {| Exp : TyExp >- 'a |} : 'a
      
      But I don't know if this is so wise to let the body be so polymorphic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 00:19:38 -0800 (Tue, 25 Jan 2005)
Revision: 6501
Log message:

      This is my current work for tonight.
      This allows the following rule in mmc_core_type_check.ml to type check,
      but it really isn't clear that this is a good idea.
      
      prim letrec_start {| intro [] |} :
         sequent { <H> >-
               LetFunDecl{| <J> >- LetFunDef{| <K> >- 'e in 'ty_e |} |} } -->
         sequent { <H> >-
               LetFunDecl{| <J> >- LetFunDef{| <K> >- 'e |} |} in 'ty_e }
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 12:12:13 -0800 (Tue, 25 Jan 2005)
Revision: 6504
Log message:

      Improved the error messages from the type checker.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 16:37:16 -0800 (Tue, 25 Jan 2005)
Revision: 6505
Log message:

      This changes the sequent_arg in mmc_base_judgment to the following:
      
         declare sequent [sequent_arg] { Univ[name:UnivClass,i:l] : Univ[name:UnivClass,i':l] >- Prop } : Judgment
      
      where for convenience, we have the following:
      
         iform unfold_exp       : Exp <--> Univ["exp":t,0:l]
         iform unfold_ty_exp    : TyExp <--> Univ["exp":t,1:l]
         iform unfold_kind_exp  : KindExp <--> Univ["exp":t,2:l]
         iform unfold_prop_exp  : Prop <--> Univ["prop":t,1:l]
      
      The parameter quantifiers are *within* the hyps clause (still
      be added to the type checker).
      
         declare sequent [sequent_arg] { (all name:t, all i:l.
                                            Univ[name:UnivClass,i:l]
                                            : Univ[name:UnivClass,i':l])
                                        >- Prop } : Judgment
      
      The non-disjoint union types make a lot of sense, but are impossible
      to implement.
      
      This solution preserves parametric polymorphism.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 20:34:11 -0800 (Tue, 25 Jan 2005)
Revision: 6506
Log message:

      Ok, I've decided the semi-non-disjoint union scheme is the best.
      Currently, sequents in mmc are defined as follows:
      
          declare sequent [sequent_arg]
             { Exp   : TyExp
             | TyExp : KindExp
             | Prop  : Prop
             >- Prop
             } : Judgment
      
      The restriction is that non-context variables cannot have union
      types.  Of course, it immediately becomes clear that this is not
      quite enough (I should have seen this of course).
      
          prim thin 'H :
             ('ext : sequent { <H>; <J> >- 'C }) -->
             sequent { <H>; 'h; <J> >- 'C }
             = 'ext
      
      Here the type of 'h is indeed a union, and of course it doesn't
      matter.
      
      I still like this version, the source language is very nice.
      I believe the solution may be to allow restricted union types.
      
      In the rule above, perhaps 'h can have type (TyExp | KindExp | Prop).
      
      During unification, we can:
         - reject if we ever try to unify two non-similar union types.
         - try to do something smarter.
      
      Of course, the above rule is missing the binding vars.
      It could be written as:
      
          prim thin 'H :
             ('ext : sequent { <H>; <J> >- 'C }) -->
             sequent { <H>; x : 'h; <J> >- 'C }
             = 'ext
      
      The question is, what is the type of x?  Perhaps we can say that
      the type is Term, since we know so little about it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-26 10:53:48 -0800 (Wed, 26 Jan 2005)
Revision: 6508
Log message:

      Normalize types before unification.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-27 19:40:40 -0800 (Thu, 27 Jan 2005)
Revision: 6517
Log message:

      Packaging the type environment.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-29 21:14:14 -0800 (Sat, 29 Jan 2005)
Revision: 6525
Log message:

      On the branch:
      
        1. Union types are gone.  For example,
      
           sequent { A : B | C : D >- E } : F
      
        2. They are replaced with a restricted form of dependent types.
      
           declare typeclass TyHyp -> Ty
           declare type A
           declare type B : TyHyp
           declare type C
           declare type D : TyHyp
      
           declare type Z{'ty : TyHyp} : Ty
           declare rewrite Z{B} <--> A
           declare rewrite Z{D} <--> C
      
           declare sequent { Z{'a} : ('a :> TyHyp) >- Prop } : Judgment
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 13:50:24 -0800 (Sun, 30 Jan 2005)
Revision: 6528
Log message:

      This is an intermediate commit.
      Progress on the dependent type system.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 15:19:30 -0800 (Sun, 30 Jan 2005)
Revision: 6529
Log message:

      Added delayed type constraints.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 19:25:44 -0800 (Sun, 30 Jan 2005)
Revision: 6531
Log message:

      Whew, the rules in mmc_core_type_check.ml now type check.
      Added hypothesis and universal types.  So we now have:
      
      declare sequent { all a : TyProp. TyElem{'a} : 'a >- ('b :> TyProp) } : Judgment
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 20:56:02 -0800 (Sun, 30 Jan 2005)
Revision: 6532
Log message:

      Lots of new typing declarations.
      
      The sweep module is strange, and doesn't typecheck yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 22:04:23 -0800 (Sun, 30 Jan 2005)
Revision: 6533
Log message:

      Let's make a clear distinction between typed and untyped expressions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 22:31:32 -0800 (Sun, 30 Jan 2005)
Revision: 6534
Log message:

      I'm getting awfully tired to typing declare statements twice.
      
      Automatically include declare statements from the .mli in the .ml.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-31 00:20:11 -0800 (Mon, 31 Jan 2005)
Revision: 6535
Log message:

      More progress on mmc.
      
      We now need token matching in Filter_patt.  Perhaps this is string list
      matching...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-31 09:22:34 -0800 (Mon, 31 Jan 2005)
Revision: 6536
Log message:

      Hypotheses have existential type, not universal.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-31 17:41:26 -0800 (Mon, 31 Jan 2005)
Revision: 6541
Log message:

      Use ustd and urec in the untyped language.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-31 18:22:10 -0800 (Mon, 31 Jan 2005)
Revision: 6542
Log message:

      This is the MMC part of the "more transparent address type" changes
      from last week.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-31 18:32:01 -0800 (Mon, 31 Jan 2005)
Revision: 6543
Log message:

      Removed the unused parts of the core_type_util
      

Changes by: ( at unknown.email)
Date: 2005-01-31 21:16:57 -0800 (Mon, 31 Jan 2005)
Revision: 6547
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-31 21:16:57 -0800 (Mon, 31 Jan 2005)
Revision: 6548
Log message:

      Merged the opname_classes2 branch with the trunk changes.