Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-01 15:07:56 -0700 (Sat, 01 Oct 2005)
Revision: 7810
Log message:

      Updated MMC to play nicely with the recently introduced enforcing of the
      Perv!Ignore meta-type for bindings.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 11:46:40 -0700 (Mon, 03 Oct 2005)
Revision: 7816
Log message:

      Use a Map to register extensions.
      This doesn't compile because of type errors (I believe these
      are due to changes wrt Ignore).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 11:47:05 -0700 (Mon, 03 Oct 2005)
Revision: 7817
Log message:

      Use a Map to register extensions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 11:47:36 -0700 (Mon, 03 Oct 2005)
Revision: 7818
Log message:

      Ignore .a files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 12:16:46 -0700 (Mon, 03 Oct 2005)
Revision: 7819
Log message:

      Skeleton for naive POPLmark solution.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-03 14:33:57 -0700 (Mon, 03 Oct 2005)
Revision: 7820
Log message:

      Couple more Ignore-related fixed (I have not seen these before because they
      were masked by a buggy mmc_ext_tuple.mli).
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2005-10-03 15:18:02 -0700 (Mon, 03 Oct 2005)
Revision: 7821
Log message:

      Reverting my last commit, which included some mutable tuple work that was not ready for prime time.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-03 16:00:33 -0700 (Mon, 03 Oct 2005)
Revision: 7822
Log message:

      Another Ignore fix

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 16:48:51 -0700 (Mon, 03 Oct 2005)
Revision: 7823
Log message:

      Re-add the extensions to the EXTENSIONS variable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-03 18:23:29 -0700 (Mon, 03 Oct 2005)
Revision: 7824
Log message:

      MMC Finally compiles!
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 18:32:37 -0700 (Mon, 03 Oct 2005)
Revision: 7825
Log message:

      Added the grammar for F<:
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 19:00:29 -0700 (Mon, 03 Oct 2005)
Revision: 7826
Log message:

      Removed some useless terms from the PMN judgments.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 19:40:06 -0700 (Mon, 03 Oct 2005)
Revision: 7828
Log message:

      This adds the foundation/~boilerplate for Fsub.
      
      We should probably do a little factoring to separate the
      real boilerplate from the logic-specific code.
      
      I'll punt on this now until the logic is a bit more developed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-03 20:37:07 -0700 (Mon, 03 Oct 2005)
Revision: 7832
Log message:

      Adding the induction principle for simple Fsub.
      It doesn't typecheck yet, I'll work on it tomorrow.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-03 21:09:32 -0700 (Mon, 03 Oct 2005)
Revision: 7833
Log message:

      Tests run correctly now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-03 21:12:36 -0700 (Mon, 03 Oct 2005)
Revision: 7835
Log message:

      Bumping the OMake/MetaPRL version requirements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-04 06:17:48 -0700 (Tue, 04 Oct 2005)
Revision: 7837
Log message:

      Use the relative path and the MP_CWD variable for producing output in the
      current directory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 11:58:56 -0700 (Tue, 04 Oct 2005)
Revision: 7838
Log message:

      Investigating the use of second-order abstract syntax (SOAS), a'la DH94.
      
      This makes only a slight change to the formalism, requiring explicit
      Var constructors, which are somewhat more satisfying anyway.  That is,
      the terms are:
      
          declare typeclass Var -> Term
          declare typeclass Exp -> Term
          declare typeclass TyExp -> Term
      
          declare Var[v:v] : Exp
          declare Apply{'e1 : Exp; 'e2 : Exp} : Exp
          declare Lambda{'ty : TyExp; x : Var. 'e['x] : Exp} : Exp
           --- note the type! -------------^
      
      The intention is that this will lead to defining the type of terms as
      a simple recursive type in ITT, allowing the induction principle to
      be derived.  In pseudo-code:
      
        define Exp <-->
           srec(Exp.
               Var of var
             | Apply of Exp * Exp
             | Lambda of TyExp * (var -> Exp))
      
      Note that this definition is positive and well-formed.
      
      Note, it probably also means that a well-formedness constraint will be
      needed to rule out exotic terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 14:08:35 -0700 (Tue, 04 Oct 2005)
Revision: 7839
Log message:

      Added the induction principles.
      
      Next, I'll define the model, and derive the induction rules.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 14:41:10 -0700 (Tue, 04 Oct 2005)
Revision: 7840
Log message:

      Adding the ITT model.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 14:57:28 -0700 (Tue, 04 Oct 2005)
Revision: 7842
Log message:

      Remove base_judgment, and use ITT sequents instead.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 15:51:42 -0700 (Tue, 04 Oct 2005)
Revision: 7843
Log message:

      Defined the ITT srec model and proved the WF lemmas.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 16:14:52 -0700 (Tue, 04 Oct 2005)
Revision: 7844
Log message:

      Induction is easy to prove, except for the following error
      
      !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      
      # save ()
      Saving pmn_core_ind
      Invalid Argument:
          output_value: functional value
      
      !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      
      This is very sad.  It seems to appear right after the srecElimination
      rule is used.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-04 17:16:25 -0700 (Tue, 04 Oct 2005)
Revision: 7846
Log message:

      Punting on Bug #529 since I have a temporary workaround.
      
      The induction is not quite right, because srec induction works
      on a subtype, not the original type.  I'll have to reformulate.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-05 10:50:07 -0700 (Wed, 05 Oct 2005)
Revision: 7847
Log message:

      Added a grammar for a fragment of ITT.
      Using Aleksey's suggestion to include Itt_eta.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-05 11:25:56 -0700 (Wed, 05 Oct 2005)
Revision: 7848
Log message:

      Proved the induction principle for types.
      Expressions are provable by the same methods.
      
      The only unsatisfying part is the use of subtypes.
      
      This is the rule we would like:
      
          <H>; ty1 : TyExp; ty2 : TyExp; C[ty1]; C[ty2] >- C[ty1 -> ty2] -->
          ...
          <H>; x: TyExp >- C[x]
      
      This is the rule we get:
          <H>; T: univ[1:l]; T subtype TyExp; ty1 : T; ty2 : T; C[ty1]; C[ty2] >- C[ty1 -> ty2] -->
          ...
          <H>; x: TyExp >- C[x]
      
      Any thoughts on how to avoid this mess?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-05 23:12:10 -0700 (Wed, 05 Oct 2005)
Revision: 7852
Log message:

      *.prla should have svn:eol-style property set to "native"

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-05 23:37:16 -0700 (Wed, 05 Oct 2005)
Revision: 7854
Log message:

      Excellent, I am so happy:)  Using
          - Itt_eta: for eta expansion
          - Itt_pairwise2: for pairwise functionality
      I have proved the naive induction rules for Fsub
      in Pmn_core_ind.
      
      Pairwise functionality is awesome!  And
      thanks Aleksey for the guidance.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 00:12:13 -0700 (Thu, 06 Oct 2005)
Revision: 7855
Log message:

      Added typing rules.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 00:34:33 -0700 (Thu, 06 Oct 2005)
Revision: 7856
Log message:

      Added subtyping rules.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 00:39:52 -0700 (Thu, 06 Oct 2005)
Revision: 7857
Log message:

      Added the transitive subtyping (PM challenge #1) theorem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 00:42:32 -0700 (Thu, 06 Oct 2005)
Revision: 7858
Log message:

      Rename Pmn_core_ind to Pmn_core_final.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 01:02:25 -0700 (Thu, 06 Oct 2005)
Revision: 7859
Log message:

      Bleh, for the original POPLmark challenge rules, it isn't even
      clear that (top <: top).
      
      I'd like to add a reflexive rule like (X in type -> X <: X) but
      that is not in the spirit of the challenge.
      
      Please, if you can look at page 8 of the challenge, tell me how
      (top <: top)...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 01:34:28 -0700 (Thu, 06 Oct 2005)
Revision: 7860
Log message:

      Proved reflexivity of subtyping.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 02:20:29 -0700 (Thu, 06 Oct 2005)
Revision: 7861
Log message:

      Getting tired...  Transitivity is partially proved,
      I need to explore it later.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 10:29:56 -0700 (Thu, 06 Oct 2005)
Revision: 7863
Log message:

      Proved transitivity of subtyping.
      
      The proof is a little disconcerting because it is basically
      a two-step proof.
      
         1. Peform induction
         2. autoT proves all subgoals
      
      Stated as a tactic, the proof is a one-liner:
      
         dT 2 thenT autoT
      
      This is both good and bad.  POPLmark says that a simultaneous
      induction is required, and narrowing must be proved at the
      same time.
      
      Here is narrowing as stated in POPLmark.
      
         <H>; X <: Q; <J[X]> >- M <: N -->
         <H> >- P <: Q -->
         <H>; X <: P; <J[X]> >- M <: N
      
      I assume narrowing reduces to transitivity in the ITT
      formulation I am using, because the ITT sequents look
      like this:
      
         <H>; X : TyExp; X <: Q; <J[X]> >- M <: N --> ...
      
      Since the hyp X <: Q is not a binding occurrence, it can
      move around just like any other proposition, and narrowing
      is no different from simple transitivity.
      
      So here is the big question:
      
         - Is the use of sequents in a rich logic (ITT) unfaithful 
           to the challenge?  It might be; the alternative is to  
           define a custom sequent.                              
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-06 13:08:35 -0700 (Thu, 06 Oct 2005)
Revision: 7864
Log message:

      Time to rethink the entire model.
      
      The problem is with proof induction.  When we write down
      a type system, what we mean is that the typing rules
      are the *only* rules that are allowed, which gives
      us an induction principle.
      
      This doesn't work if you formalize a type system as a
      logic in MetaPRL, because logics are open-ended.  You can
      state some kind of induction principle as an axiom,
      but we've had that argument before.
      
      So, another solution is the state a language of derivations,
      reducing proof induction to structural induction, which
      we know how to do.
      
      Unfortunately, I don't immediately see how to define a
      language of derivations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-07 19:16:49 -0700 (Fri, 07 Oct 2005)
Revision: 7874
Log message:

      Adding a propositional definition of type checking.
      Not finished, I want to shift some of the grammar to
      ITT.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-08 17:22:04 -0700 (Sat, 08 Oct 2005)
Revision: 7880
Log message:

      Much of the grammar infrastructure is now generic
      and moved to ITT.
      
      This commit now assumes that PMN is defined as part of ITT.
      Fixed up most of the old proofs (this was trivial, since autoT solved
      everything anyway).
      
      Working on the propositional form of the type judgment.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-08 18:36:56 -0700 (Sat, 08 Oct 2005)
Revision: 7882
Log message:

      Partial definition of propositional type judgment.
      This is tricky.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 14:04:02 -0700 (Sun, 09 Oct 2005)
Revision: 7883
Log message:

      Preparing to copy into the MetaPRL tree.