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

      Changed xhypcontext to take the context name as a parameter instead of using a
      binding as a context name. This is necessary because we do not want to use
      binding in sequents with binding meta-type set to Perv!Ignore.
      

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

      Bumping the version number (to account for Ignore-related changes).
      

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

      Before changing to editor/ml, set MP_CWD environment variable to point to the
      wd where the MetaPRL script was originally started from.
      

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

      I'm having trouble using untyped ITT with Fsub where I want types.
      This define Ty -> Term so that I can make some progress.
      

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

      Define srecElimination2 that hard-codes universe univ[1:l]
      to avoid triggering Bug #529.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-05 18:28:01 -0700 (Wed, 05 Oct 2005)
Revision: 7849
Log message:

      Bug 529 is not what we originally thought it was (and can be easily worked
      around by using "export"), so I am reverting r7845.
      

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

      Add some convenience rules for eta-expansion.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-05 23:11:55 -0700 (Wed, 05 Oct 2005)
Revision: 7851
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:23:27 -0700 (Wed, 05 Oct 2005)
Revision: 7853
Log message:

      I simply must reorder the arguments to the supertype rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 02:23:31 -0700 (Thu, 06 Oct 2005)
Revision: 7862
Log message:

      Deleting an outdated comment.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 22:30:39 -0700 (Thu, 06 Oct 2005)
Revision: 7867
Log message:

      Removing svn:mime-type from *.prla
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 22:35:23 -0700 (Thu, 06 Oct 2005)
Revision: 7868
Log message:

      Added a section on setting up auto-props.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 22:37:29 -0700 (Thu, 06 Oct 2005)
Revision: 7869
Log message:

      "CVS" -> "Subversion".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 22:40:30 -0700 (Thu, 06 Oct 2005)
Revision: 7870
Log message:

      "Make sure you have subversion installed"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 23:04:10 -0700 (Thu, 06 Oct 2005)
Revision: 7871
Log message:

      Removing the Itt_fun module. Now the independent function is just a dependent
      function where the dependency variable does not occur (and will normally be
      represented by an empty string).
      

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

      !! This breaks binary compatibility !!
      !! Export your theories before doing an update !!
      
      Two things:
          - Use omake_0_9_7_pre7/libmojave instead of the trunk libmojave
          - Added a minimal grammar to ITT
      
      I believe I have fixed the "functional value" marshaling problem,
      but PLEASE let me know if you encounter a "functional value"
      problem.
      
      This appears as follows:
       
          # save ()
          Invalid Argument:
              output_value: functional value
      
      The workaround is to use "export ()" instead of "save ()" if this
      happens.
      

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

      Some changes to simple pattern matching.
      

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

      Copied the naive POPLmark into the MetaPRL tree.  The separation
      was getting tiresome.
      
      But, I still do not think this is the right solution.
      We need better support for people who work outside the tree.
      

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

      Rebuilding the theory.  The plan is as follows:
      
        1. Define the SOAS
      
        2. Derive the induction principle
      
        3. Define HOAS, based on a left-indexed deBruijn
           representation.  Sigh, this is more-or-less inevitable because we
           need a substitution principle.
      
           The proposed solution is to carry around an environment of the
           following form, and is much like a model of closures.
      
               VEnv <--> n:N * ({0..n-1} -> Exp)
      
           The type is slightly better than in Coq, because Coq does not have
           function extensionality.
      
        4. Derive the induction principle.
      

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

      Added the SOAS model.
      
      Minor rewriter bug--the following production fails.
      We should allow it in non-strict mode.
      
          production itt_term{univ[i:l]} <--
              tok_univ; tok_id[i:s]
      
      We would also like this to work:
      
          production itt_term{univ[i:l]} <--
              tok_univ; tok_int[i:n]
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 15:03:54 -0700 (Sun, 09 Oct 2005)
Revision: 7887
Log message:

      Added the induction rule for SOAS.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 15:27:52 -0700 (Sun, 09 Oct 2005)
Revision: 7888
Log message:

      The HOAS term symtax is exactly the same as SOAS.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 15:57:03 -0700 (Sun, 09 Oct 2005)
Revision: 7889
Log message:

      Added grammars for a fragment of integers, sets, etc.
      
      Also, Itt_nat was not included in Itt_theory.  Is there
      a reason why it shouldn't be there?
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 16:32:24 -0700 (Sun, 09 Oct 2005)
Revision: 7890
Log message:

      First pass on defining the HOAS model.
      I think I need a theory of finite functions first.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 18:35:56 -0700 (Sun, 09 Oct 2005)
Revision: 7891
Log message:

      Added a preliminary Itt_finite_fun1.
      
      Would someone who knows how to prove arithmetic finish
      the proof of Itt_finite_fun1.add_ffun_wf?
      
      It is true, but I don't know how to prove it, and I would
      like to see how the proof is done.