Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-01 14:11:57 -0800 (Thu, 01 Dec 2005)
Revision: 8255
Log message:

      Some intermediate results.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-01 14:11:57 -0800 (Thu, 01 Dec 2005)
Revision: 8255
Log message:

      Some intermediate results.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-02 20:39:16 -0800 (Fri, 02 Dec 2005)
Revision: 8256
Log message:

      Sorry about moving all files in theories/itt/extensions to
      theories/itt/extensions/base, but I would really like to use pairwise
      functionality in extensions/vector.  This required that a dependency
      be established.
      
      Let me know if I am being too aggressive with pairwise, but it is
      really nice:)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-02 20:44:53 -0800 (Fri, 02 Dec 2005)
Revision: 8257
Log message:

      Saving partial work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-03 14:10:22 -0800 (Sat, 03 Dec 2005)
Revision: 8258
Log message:

      Made "itt/extensions" into a "virtual" theory and made sure MetaPRL with
      THEORIES=all again.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-03 20:00:26 -0800 (Sat, 03 Dec 2005)
Revision: 8261
Log message:

      Change the parse-time representation of the "default context dependencies" to
      be v<|!!|> (two exclamation signs) instead of v<|v|>.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-03 20:15:08 -0800 (Sat, 03 Dec 2005)
Revision: 8262
Log message:

      Improving the prlcomp function.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-04 09:29:25 -0800 (Sun, 04 Dec 2005)
Revision: 8264
Log message:

      Added a theory of "sloppy" or "lazy" lists.  The intent is
      to minimize wf reasoning.
      
      The type Cons{n} stands for a term with at least 'n cons cells.
      It is defined with the Img type.
      
      Proved the key lemma
      
         l IN Cons{n} -->
         0 <= i < n -->
         l ~ (nth_prefix{l; i} @ nth_suffix{l; i})
      
      I used pairwise extensively.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-04 12:51:31 -0800 (Sun, 04 Dec 2005)
Revision: 8265
Log message:

      Another "itt/extensions -> /itt/extensions/base" fix.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-05 18:40:38 -0800 (Mon, 05 Dec 2005)
Revision: 8266
Log message:

      Intermediate commit while considering strategy sugeessted by Aleksey.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-07 11:22:11 -0800 (Wed, 07 Dec 2005)
Revision: 8267
Log message:

      Added ConsFun, containing terms of the form lambda{x. e1[x]::e2[x]}
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-08 13:13:23 -0800 (Thu, 08 Dec 2005)
Revision: 8268
Log message:

      Minor changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-08 17:01:40 -0800 (Thu, 08 Dec 2005)
Revision: 8269
Log message:

      Re-investigating the list_of_fun representation.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-09 15:24:41 -0800 (Fri, 09 Dec 2005)
Revision: 8271
Log message:

      This time I think I really have it solved--but we'll see.  The problem
      with all the different approaches is that the conversion expression
      includes a destructor, which is in general in the scope of binders.
      However, the destructor doesn't care about the binders, so the computation
      should work anyway.
      
      In general, the issue is that we need to solve the following rewrite,
      for <K> nonempty.  Note that <K> *does* depend on <J>, however the
      length{...} doesn't care.
      
         (<J> >-bind if length{hypconslist{| <K> >- nil |}} then nil else e2)
         <-->
         (<J> >-bind e2)
      
      The idea is pretty simple.  All I've proved so far
      is the unconditional rewrite
      
         length{hypconslist{| <K> >- nil |}}
         <-->
         length{squashlist{| <K> >- nil |}}
      
      where squashlist{| ... |} evaluates to a real list
         [it; ...; it]
      
      This *should* be enough, because rewriting with
      squashlist{| ... |} is easy because the bindings
      go away.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-10 18:46:26 -0800 (Sat, 10 Dec 2005)
Revision: 8273
Log message:

      Proved the suffix part of sequent reduction.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-11 13:48:17 -0800 (Sun, 11 Dec 2005)
Revision: 8274
Log message:

      Sequent reduction is finished.  I don't know if there are any
      lessons here.  If anything I would say that, when performing
      rewriting under a binder, concentrate on defining closed terms that
      are equivalent to the destructors under the binder.  That's pretty
      obvious though.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-12 14:16:08 -0800 (Mon, 12 Dec 2005)
Revision: 8278
Log message:

      Renaming files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-12 14:23:37 -0800 (Mon, 12 Dec 2005)
Revision: 8279
Log message:

      Renamed Itt_vec_sequent_term1 to Itt_vec_sequent_term.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-12 15:33:50 -0800 (Mon, 12 Dec 2005)
Revision: 8280
Log message:

      Defining sequent bterms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-12 16:30:39 -0800 (Mon, 12 Dec 2005)
Revision: 8281
Log message:

      When computing dependencies, ML rules should automatically be considered
      primitive.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-12 16:50:03 -0800 (Mon, 12 Dec 2005)
Revision: 8282
Log message:

      Merged in the trunk changes (revisions 8123:8281):
         svn merge -r 8123:8281 svn+ssh://svn.metaprl.org/svnroot/mojave/metaprl