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
      
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-12 17:13:59 -0800 (Mon, 12 Dec 2005)
Revision: 8284
Log message:

      Initial work on the BTerm version of sequents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-12 20:10:12 -0800 (Mon, 12 Dec 2005)
Revision: 8288
Log message:

      My lm_hash.ml change have changed the magic number.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-13 15:29:24 -0800 (Tue, 13 Dec 2005)
Revision: 8291
Log message:

      Generated symlinks somehow got added to the repository; removing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-13 21:44:44 -0800 (Tue, 13 Dec 2005)
Revision: 8294
Log message:

      Generated symlinks need to be ignored

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-14 11:49:48 -0800 (Wed, 14 Dec 2005)
Revision: 8295
Log message:

      Some initial progress with HOAS sequent derivations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-14 15:52:13 -0800 (Wed, 14 Dec 2005)
Revision: 8296
Log message:

      Minor code clean-up. Use Lm_symbol.eq in place of = for variables (and
      variable lists).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-14 17:21:29 -0800 (Wed, 14 Dec 2005)
Revision: 8298
Log message:

      Improved error reporting on mismatches.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-14 17:38:10 -0800 (Wed, 14 Dec 2005)
Revision: 8299
Log message:

      Ignore generated symlinks.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-14 17:57:17 -0800 (Wed, 14 Dec 2005)
Revision: 8300
Log message:

      Fixing a bug - we should not be using of_sorted_list here.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-14 20:44:06 -0800 (Wed, 14 Dec 2005)
Revision: 8301
Log message:

      Another intermediate commmit.
      
      This gets half of the work for automation of ProofRule{'ty_sequent}
      well-formedness checking.  Time to do some work on raw BTerms.
      
      Why have all the reflection people disappeared several months ago?
      Peoples have better things to do, they should let me know!
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-12-14 22:40:39 -0800 (Wed, 14 Dec 2005)
Revision: 8303
Log message:

      More on implementation of object theory

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-12-15 12:09:33 -0800 (Thu, 15 Dec 2005)
Revision: 8305
Log message:

      This file was commited by mistake
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-12-15 15:12:10 -0800 (Thu, 15 Dec 2005)
Revision: 8307
Log message:

      More on objects

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

      I was curious, so I tried the approach that Aleksey suggested.
      As you might guess, it worked, and it was pretty easy:b  This is in
      Itt_hoas_debruijn.reduce_vec_bind_of_mk_bterm_of_list_of_fun (sorry
      about the long name, I was dubious at the time).
      
      It would be nice to see a shorter proof than mine (19 ruleboxes).
      Perhaps one of you (including the Aleksey oracle) can do better?
      
      Sorry I suggested a simple (though non-obvious to me) theorem.  However,
      I am sure I will once again be flabbergasted, and soon enough we will come
      up with a nontrivial example that will strain/elucidate the heuristic.
      
      ---- Aside ----
      
      Itt_vec_sequent_term is another example of the heuristic, where the
      destructor part (the "length" term) is not originally in non-dependent
      form.  However, it can be proved that the dependent form is equivalent
      to a non-dependent form.  Basically, it works like this:
      
      1. Prove that the destructor does not depend on the binders.
      
         For some interesting terms "e":
      
         bind{<H> >- e[length{'x}] }
         <-->
         bind{<H> >- e[length{bind{<H> >- 'x}}]}
      
      2. Hoist the closed destructor <<length{bind{<H> >- 'x}}>>.
      
      3. Now work hard for a while, and you are done.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-16 21:12:55 -0800 (Fri, 16 Dec 2005)
Revision: 8313
Log message:

      Alexei & Aleksey: making some progress towards being able to switch to
      pairwise.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-17 23:15:23 -0800 (Sat, 17 Dec 2005)
Revision: 8314
Log message:

      Another proof version for "reduce_vec_bind_of_mk_bterm_of_list_of_fun" in "t2".
      The idea is similar as Jason's, but a little simpler.
      
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-18 15:09:58 -0800 (Sun, 18 Dec 2005)
Revision: 8315
Log message:

      Added enough automation to prove that (TyTop in TyExp)
      is a well-formed proof rule.
      
      The list_of_fun theorem in Itt_hoas_debruijn was only the first
      step, because any actual term needs to have its subterms
      converted to list_of_fun form.  This raises the standard problem,
      that the length{...} term is stated in dependent form, though
      we know that it is ultimately independent.
      
      Here are the steps to prove a wf goal of the form
      
         bind{.... mk_term{op; [s1; ...; sn]}} in BTerm{...}
      
         1. First, convert the subterm list to a vlist{| s1; ...; sn |}.
            The vlist{| ... |} form is nice because it is always
            a list, no matter what the elements are.  These vector
            form are somewhere in between a variable and an actual
            concrete list.
      
            Proved various lemmas like:
               length{vlist{| <J[x]> |}} <--> length{vlist{| <J[it]> |}}
      
         2. Defined a subterms_bind{bind{...; terms}} term that is used
            to push the binds into the list.
      
         3. Defined a tactic bindWFT to perform all the steps in the
            wf reasoning.
      
      Problems:
         I don't know why, but adding the bindWFT tactic to autoT does not
         work.  We get some strange things like.
      
            dT 0 thenT autoT  (* completely proves the goal *)
         but
            autoT (* does nothing... *)
      
         I am not sure of all the strategies in autoT, but it seems
         to me that adding something to "intro" should have some effect
         on autoT...
      
      The final tactic then is:
      
         let proofRuleWFT = repeatT (autoT thenT tryT bindWFT thenT rw reduceC 0)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-18 16:56:03 -0800 (Sun, 18 Dec 2005)
Revision: 8316
Log message:

      Proved TyFun{'t1; 't2} in TyExp.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-18 18:27:04 -0800 (Sun, 18 Dec 2005)
Revision: 8317
Log message:

      Attempting the proof for TyAll{'ty1; x. 'ty2['x]}.
      
      This might be the challenge of a canonical form.
      The general goal is generalized eta-reduction.
      
         t in BTerm{'n +@ 1} -->
         bind{'n; x. bind{y. subst{substl{'t; 'x}; 'y}}}
         <-->
         t
      
      This individual theorem probably has an easy proof,
      and in general the concept seems obviously true.
      
      In the general case, there will be a stack of binds,
      usually of alternating vector/scalar form.
      
         bind{'n1; x1. bind{y1. bind{'n2; x2. bind{y1. ...}}}}}
      
      Let's see if we can prove it in general (not just
      this instance).
      
      Option 1:
         Do induction on 't.  Unfortunately, the bind-pushing
         tools in Itt_hoas_bterm_wf work only on concrete
         subterms lists.  Perhaps this can be generalized,
         but it is not obvious.
      
      Option 2:
         Prove a general bind-coalescing theorem, where we show
         that
            bind{'n; x. bind{y. ...}}
         turns into
            bind{'n +@ 1; x. ...}.
         See Itt_hoas_bterm_wf.coalesce_bindn_bind for a
         proof statement.
      
      Both options are not obvious at least to me.  Let's pose this as the
      immediate challenge.  Some immediate proposals that do not work:
      
         1. "I will tell Xin how to do it" (well, for Xin
            that is a good answer:)
         2. "You should write the subst{substl{...}}
             as substl{subst{...}}" (unless it can be shown
             how to write the conversion from one to the other).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-19 00:47:02 -0800 (Mon, 19 Dec 2005)
Revision: 8318
Log message:

      Some minor clean-ups.
      

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

      Here is a slightly different approach, where the idea
      is to rewrite
      
         substl{substl{'e; 'l1}; 'l2}
         <-->
         substl{'e; append{'l1; 'l2}}
      
      To do so, we need to know that 'l1 and 'l2 are lists.
      The Itt_hoas_vector.bindn_to_list_of_fun is such
      an attempt:
      
         bind{'n; x. 'e['x]}
         <-->
         bind{'n; x. 'e[list_of_fun{i. nth_elem{'x; 'i}; 'n}]}
      
      Unfinished, the proof is not easy AFAIK.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-19 16:15:23 -0800 (Mon, 19 Dec 2005)
Revision: 8323
Log message:

      Added rewrite bind_to_list_of_fun, which I believe is needed to prove
      bindn_to_list_of_fun. However, I don't know how to prove bind_to_list_of_fun
      -- I think we are missing a primitive rewrite like this or sth more basic.
      
      Now we should be able to prove bindn_to_list_of_fun by the handling of
      list_of_fun as Aleksey suggested in another thread.
      
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-19 17:52:59 -0800 (Mon, 19 Dec 2005)
Revision: 8324
Log message:

      Aleksey proved the bind theorem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-19 18:28:41 -0800 (Mon, 19 Dec 2005)
Revision: 8325
Log message:

      Exploring using list_of_fun directly in Itt_hoas_bterm_wf.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-19 18:36:36 -0800 (Mon, 19 Dec 2005)
Revision: 8326
Log message:

      Removed bind_to_list_of_fun.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-19 20:43:05 -0800 (Mon, 19 Dec 2005)
Revision: 8329
Log message:

      Well, this is a (very) partial approach to using list_of_fun
      by itself.
      
      I really believe this is absurd.  This approach is grundge-driven.
      In contrast, the vlist{| ... |} approach is purely forward-directed,
      reduce-driven, no destructor-driven tactics.
      
      With the direct list_of_fun approach, you need non-reduce-driven
      tactics like splitITE.  Here is an example.
      
         mk_bterm{'n; 'op; list_of_fun{i.
            bind{'m; x. if i = 0 then e0
                        else if i = 1 then e1
                        ...
                        else if i = n then en}; 'k}}
         --> grundge forward and push the bind into the ITE
         (hard to express in canonical form)
      
      So now, to prove compatible_shapes, split apart the operator shape;
      do a bunch of ITE reductions, etc.  Very grundgy.
      
      Now consider the vlist approach.
      
         mk_bterm{'n; 'op; subterms_bind{bind{'m; x. vlist{| e0[x]; ... en[x] |}}}}
         --> reduce subterms_bind (yes, that is a _reduce_)
         mk_bterm{'n; 'op; vlist{| bind{'m; x. e0[x]}; ...; bind{'m; x. en[x]} |}}
      
      Now *that* is obvious and beautiful.
      
      Here is the dogma I am espousing:
         - Express each transformation in its natural form.
         - It is preferable to implement as much of a transformation
           as possible with *theorems*, rather than tactics.
      
      Of course, the vlist implementation relies on list_of_fun.  However, I
      suggest that list_of_fun be viewed as assembly code, not to be purported
      to be ideal in all situations.
      
      Of course, I just want it to be beautiful.  If there is a beautiful
      list_of_fun approach, I'm all for it.  If I may ask, once you have done
      your coding, do a _serious_ comparison.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-20 11:09:50 -0800 (Tue, 20 Dec 2005)
Revision: 8330
Log message:

      - Added a "DEFAULT_UI" variable to the mk/config file, with possible values:
        "browser" (default) and "cli".
        
      - Also added a "-browser" command-line option. Of course, -browser/-cli
        command line options (which are exclusive) have higher precedence thatn
        DEFAULT_UI. The DEFAULT_UI is only consulted when neither of the two
        command-line options are given.
      
      - Simplified some of the WrapC/PrlC/procomp setup, adding value dependencies
        to make it more precise.
      
      - Added pa_macro to MetaPRL filter. Now we can use structured IFDEFs in the
        MetaPRL files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-20 15:25:11 -0800 (Tue, 20 Dec 2005)
Revision: 8334
Log message:

      Made Itt_struct.nthAssumT smarter, capable of using the nth_hyp resource
      instead of requiring a literal match.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-20 20:35:15 -0800 (Tue, 20 Dec 2005)
Revision: 8336
Log message:

      Further nthAssumT improvements.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-21 00:02:26 -0800 (Wed, 21 Dec 2005)
Revision: 8337
Log message:

      Added foldClose2C in Itt_Struct2, and using it reproved
      Itt_hoas_debruijn.reduce_vec_bind_of_mk_bterm_of_list_of_fun.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-21 00:42:49 -0800 (Wed, 21 Dec 2005)
Revision: 8338
Log message:

      No-op: updating a comment

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-21 01:54:12 -0800 (Wed, 21 Dec 2005)
Revision: 8339
Log message:

      Minor code simplification

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-21 12:54:59 -0800 (Wed, 21 Dec 2005)
Revision: 8340
Log message:

      - Removing the unsafe_lookup function from the Weak_memo module. We never used
        it and it is safer and easier not to provide it.
      
      - Fixing a type in an error message.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-21 13:57:59 -0800 (Wed, 21 Dec 2005)
Revision: 8341
Log message:

      I believe this should finally fix the Weak_memo bug!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-21 15:46:12 -0800 (Wed, 21 Dec 2005)
Revision: 8342
Log message:

      Disabling (by moving under an IFDEF) consistency checks in Weak_memo. These
      checks never caught any bugs, and I am pretty confident that they are
      unnecessary.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-21 18:59:18 -0800 (Wed, 21 Dec 2005)
Revision: 8343
Log message:

      Changing substT to be resource-based.
      
      Still need to do:
        - Implement {| subst |} resource annotations.
        - Annotate "a = b in int => a ~ b" and "a = b in nat => a ~ b" to make it so
          that hypSubstT/revHypSubstT would use squiggle rewriting instead of
          equality one for those types.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-21 22:35:04 -0800 (Wed, 21 Dec 2005)
Revision: 8344
Log message:

      Added Itt_struct2.foldCloseC. The usage is
       foldCloseC [<<'x1>>;...;<<'xn>>] <<'t>>
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-22 15:39:54 -0800 (Thu, 22 Dec 2005)
Revision: 8345
Log message:

      - Added a "sqsimple" resource (with the term->bool output type) that can be
        used to tell whether an ITT type is squiggle-simple.
      
      - Added a sqsimple resource annotation processor that can be used to annotate
        rules of the form "sqsimple{nat}" and "sqsimple{A} --> sqsimple{A List}"
      
      - Changed the substT tactic to take advantage of the new sqsimple resource.
        Now when one runs something like "substT << a = b in (list{nat * int} + bool) >>,
        substT will know how to turn the equality into a squiggle one and do a
        substitution w/o generating any wf subgoals. hypSubstT and revHypSubstT will
        act similarly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-22 17:32:34 -0800 (Thu, 22 Dec 2005)
Revision: 8346
Log message:

      Added a limited support for "assert"{beq_int{'a;'b}} to substT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-22 18:00:56 -0800 (Thu, 22 Dec 2005)
Revision: 8347
Log message:

      - Changing the exception handling in "expand" - now it will no longer give up
        expanding on non-RefinerError exceptions (unless OCAMLRUNPARAM=b is being
        used).
      
      - Improving the sqsimple resource; adding the BTerm type to it
      
      - Removing the sqsimple/sqsimple_type distinction (so now there is only the
        sqsimple{'T} predicate, which implies type{'T}).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-22 20:54:09 -0800 (Thu, 22 Dec 2005)
Revision: 8348
Log message:

      Trying to get arithT/omegaT to work better with hypotheses of the form << 'n
      in nat >> and << 'm = 'n in nat >>.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-22 21:16:14 -0800 (Thu, 22 Dec 2005)
Revision: 8349
Log message:

      Changed Itt_struct2.foldCloseC to use string list instead of term list.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-23 00:04:38 -0800 (Fri, 23 Dec 2005)
Revision: 8350
Log message:

      Proved coalescence of bindn.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-23 01:26:34 -0800 (Fri, 23 Dec 2005)
Revision: 8351
Log message:

      Added lemmas for appending two list_of_funs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-23 08:16:18 -0800 (Fri, 23 Dec 2005)
Revision: 8352
Log message:

      A number of arithT/omegaT improvements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-23 08:35:29 -0800 (Fri, 23 Dec 2005)
Revision: 8353
Log message:

      - Proved Xin's reduce_lof_append_lof (append of two list_of_fun's) lemma.
      - Fixed another reference to removed foldClose1C rewrite.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-23 09:56:55 -0800 (Fri, 23 Dec 2005)
Revision: 8354
Log message:

      Further omegaT improvements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-23 12:40:17 -0800 (Fri, 23 Dec 2005)
Revision: 8355
Log message:

      This merges Itt_list2!nth with Itt_list3!nth_elem. The new operation is called
      Itt_list2!nth, but is defined the way Itt_list3!nth_elem used to be defined ---
      namely nth{l;2} is unconditionally equal to hd{tl{tl{l}}.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-23 14:04:05 -0800 (Fri, 23 Dec 2005)
Revision: 8356
Log message:

      Proved some of the arith lemmas

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-24 14:53:39 -0800 (Sat, 24 Dec 2005)
Revision: 8357
Log message:

      Proved the Itt_hoas_vector.substl_substl_lof theorem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-24 15:02:46 -0800 (Sat, 24 Dec 2005)
Revision: 8358
Log message:

      I should have proved Itt_hoas_vector.append_of_substl_substl too:b
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-24 17:32:38 -0800 (Sat, 24 Dec 2005)
Revision: 8359
Log message:

      Some simplifications.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-24 20:25:10 -0800 (Sat, 24 Dec 2005)
Revision: 8360
Log message:

      Sorry---- 
      
      For the short term, we need to remove the "denormalizing" rewrites from
      reduceC.  This includes the following rewrites in Itt_hoas_debruijn:
         reduce_mk_bterm_base
         reduce_mk_bterm_step
         reduce_mk_bterm_empty
      All of these are "denormalization" rules, because they hoist binds
      out of bterms.
      
      This is only a half-hearted attempt.  Itt_hoas_lang fails miserably
      if these are removed from reduceC.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-24 20:35:11 -0800 (Sat, 24 Dec 2005)
Revision: 8361
Log message:

      Proved some extra theories without the "denormalization" theorems.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-25 17:15:50 -0800 (Sun, 25 Dec 2005)
Revision: 8362
Log message:

      Removed denormalization rules from the reduce resource in Itt_hoas_vector.
      
      I really don't like doing this--we should figure out the right way
      to do it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-25 18:42:36 -0800 (Sun, 25 Dec 2005)
Revision: 8363
Log message:

      Changed the grammar variable convention to reduce the need for quotes.
      
         - "<id>" is always a term
         - '<id> is always a variable
         - <id> is:
            + a term if a term "<id>" is in scope
            + a variable otherwise
      
      Remaining issues:
         - There is still an ambiguity:
              name[1]
           Is it a sovar, or a term?
      
         - I would like to use "in" rather than "IN" for membership.
           The conflict comes from "let ... = ... in ...", but maybe
           it is possible to define precedences to give priority to
           the "let" in this case.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-25 18:58:23 -0800 (Sun, 25 Dec 2005)
Revision: 8364
Log message:

      Membership can be stated as "<term> in <term>".  I don't know why this
      suddenly works.  Strangely, I can't compile itt anymore.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-26 10:16:31 -0800 (Mon, 26 Dec 2005)
Revision: 8365
Log message:

      Adding some normalization rules for list_of_fun.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-26 10:35:27 -0800 (Mon, 26 Dec 2005)
Revision: 8366
Log message:

      Separate the "sloppy" lists from Itt_list3 into Itt_list_sloppy.
      The sloppy lists are not used anymore.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-26 13:53:20 -0800 (Mon, 26 Dec 2005)
Revision: 8367
Log message:

      Working on a list_of_fun theory.
      
      The main problem with list_of_fun{i. 'f['i]; 'n} is that
      the function 'f['i] can be arbitrary, and reasoning about
      arbitrary functions is hard.
      
      In particular, information can be lost during normalization.
      For example:
      
          interactive_rw nth_prefix_lof {| normalize_lof |} :
             'n in nat -->
             'm in nat -->
             'm <= 'n -->
             nth_prefix{lof{i. 'f['i]; 'n}; 'm}
             <-->
             lof{i. 'f['i]; 'm}
      
      Here, we lost some information (the variable 'n), and so the rewrite is
      not easy to reverse.
      
      The plan is to define a set of reversible rewrites for lof normalization.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-26 14:47:03 -0800 (Mon, 26 Dec 2005)
Revision: 8368
Log message:

      Added the reversible lof theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-26 17:45:45 -0800 (Mon, 26 Dec 2005)
Revision: 8369
Log message:

      Fixing variable handling in genSOVarT.
      

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

      Partial update to the normalizer.  It doesn't work atm, but
      I want to checkpoint.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-26 20:30:30 -0800 (Mon, 26 Dec 2005)
Revision: 8371
Log message:

      Some progress toward normalization.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-26 21:44:22 -0800 (Mon, 26 Dec 2005)
Revision: 8372
Log message:

      Small fix in foldCloseC
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-27 00:09:32 -0800 (Tue, 27 Dec 2005)
Revision: 8373
Log message:

      In tcaT (AKA ...ttca) and the "MustComplete" part of autoT, give up quicker
      when hitting a subgoal that can not be completed. 
      
      This makes "status-all" approx. 12% faster.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-27 11:40:29 -0800 (Tue, 27 Dec 2005)
Revision: 8374
Log message:

      Shifted the work of normalization into the lof form,
      so now Itt_hoas_normalize has no theorems.
      
      Not quite finished, still tuning.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-27 14:14:49 -0800 (Tue, 27 Dec 2005)
Revision: 8375
Log message:

      A minor autoT update.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-27 17:21:46 -0800 (Tue, 27 Dec 2005)
Revision: 8376
Log message:

      Removing the second form of bind migration.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-27 19:22:17 -0800 (Tue, 27 Dec 2005)
Revision: 8377
Log message:

      Added lof "rippling" (unrelated to Bundy's induction scheme).  The idea
      is cool, here is a summary:
      
         - It is easy to prove theorems like
              lof{i. f['i]; 'n} ~ lof{i. g['i]; 'n}
           for some concrete f['i] and g['i].  To be clear,
           I don't mean f and g are sovars, I mean they
           represent some concrete terms.
      
           Example:
               lof{i. lof_append{j1. lof_nth_prefix{j2. lof_nth{'x; 'j2}; 'j1; 'n1; 'n2};
                                 j2. lof_cons{j3. lof_nil; 'j2; lof_nth{'x; 'n2}};
                                 'i; 'n3; 'n4}; 'n5}
               <-->
               lof{i. lof_nth{'x; 'i}; 'n5}
      
         - It is not easy, and often impossible, to prove
           a similar theorem when the lof is not the immediate
           ancestor of f['i] and g['i].
      
           You might argue that this is all due the "free algebra" that I
           am using.  If you are dubious in this respect, please look at the
           "bind pushing" theorems in Itt_hoas_lof, like "lof_bind_nil".
           These theorems are not obviously expressible in nested form.
           See Itt_hoas_lof rev 8376, where I tried to do so.  To prove these
           theorems we need contexts, and some very hard arguments.  OTOH,
           the simple forms are trivial.
      
         - So the idea is to use the reversible lof conversion
           in rippling form:
      
              - sweep up (normalizeLofC)
              - sweep dn (reduceLofC)
              - repeat until nothing changes
      
           In each phase, the lof will pass through the right place
           so that an optimization can be performed.
      
      Summary:
         - This is a very cool idea.
         - I expect to be shunned:)
         - For comments, please see if you can understand what is going on--
           I am more than happy to help if needed.  Destructive comments are
           ok, but scientific constructive arguments are even better.
      
      Comments:
         - To see it work, try expanding the theorems in Pmn_core_terms
           (wf_term_TyAll finally works!)
      
         - It is unoptimized
           -- wf_term_TyAll takes 70k-100k primitive steps!
              I am daunted by optimizing a proof of this size...
      
           -- I believe most of the steps are because we have a
              massive number of redundant subgoals like
                  <H>; ... >- |H1| in nat
              In any give proof we may have thousands of the same
              (identical) goal of this form.
      
              It would be nice to have a tactic for explicit
              caching/redundant-subgoal-elimination.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-28 11:55:36 -0800 (Wed, 28 Dec 2005)
Revision: 8379
Log message:

      The "thm" form is now supported.
      
         thm foo :
            sequent { <H> >- it in top } =
            "autoT"
      
      This creates an interactive theorem, where the initial rulebox
      is filled with the string "autoT".  The proof is not checked
      otherwise.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-28 12:06:21 -0800 (Wed, 28 Dec 2005)
Revision: 8380
Log message:

      Add initial rule boxes to reflected wf proofs.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-28 12:29:14 -0800 (Wed, 28 Dec 2005)
Revision: 8381
Log message:

      Add the reflection rules to the intro resources.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-28 20:11:36 -0800 (Wed, 28 Dec 2005)
Revision: 8383
Log message:

      CAUTION: the magic number has changed!  Please save your work before
      updating.
      
      Added the "const" modifier to declare/define.  An example:
      
         declare const void
      
      This affects only Filter_grammar-based parsing, where an identifier is
      interpreted as a term only if it is declared as a "const".  Otherwise there
      is no affect, and you won't notice any difference.
      
      - Generalized the opname "shape_class" modifiers, which are now
        represented as a bitset.  This should help if we ever want things like
        private/protected/public modifiers.
      
      - Added the following const declarations:
        ./theories/itt/core/itt_list2.mli:define const iform unfold_list : list <--> list{top}
        ./theories/itt/core/itt_atom.mli:declare const atom
        ./theories/itt/core/itt_unit.mli:declare const unit
        ./theories/itt/core/itt_nat.mli:define const unfold_nat :
        ./theories/itt/core/itt_void.mli:declare const void
        ./theories/meta/base/base_trivial.mli:declare const it
      
      - TODO: "const" modifiers should not be allowed on terms with non-zero arity,
        and probably not allowed even if the term has parameters.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-29 13:08:12 -0800 (Thu, 29 Dec 2005)
Revision: 8384
Log message:

      Itt_hoas_lof does not need to extend Itt_hoas_bterm -- extending Itt_hoas_debruijn suffices.
      

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

      Reformulating the Provable theorems.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-31 08:13:21 -0800 (Sat, 31 Dec 2005)
Revision: 8386
Log message:

      Returning to a single logic, rather than one logic per-rule.