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.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-09 19:48:01 -0700 (Sun, 09 Oct 2005)
Revision: 7892
Log message:

      Hmm, I should probably use infinite functions instead.  That is, instead
      of the finite function
      
          VEnv <--> n: int * { 0..n- } -> Exp
      
      I should use
      
          VEnv <--> int * (int -> Exp)
      
      just to make wf theorems easier (otherwise the wf theorem has to be
      indexed by the VEnv).
      
      I'll still have a ton of arithmetic to do...
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-10-09 23:05:57 -0700 (Sun, 09 Oct 2005)
Revision: 7893
Log message:

      Finished Itt_finite_fun1.add_ffun_wf
      I hope, my addition to elim-resource in Itt_bool won't break to many proofs. I'll deal with it tomorrow, now it is too late.

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

      Added a "weak" form of finite countable functions,
      where the underlying function is actually inifinite
      to make well-formedness checking easier.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-10-10 22:23:18 -0700 (Mon, 10 Oct 2005)
Revision: 7895
Log message:

      It's probably not me who broke /ctt_markov/markov2
      but anyway, here is a fix.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-11 10:15:09 -0700 (Tue, 11 Oct 2005)
Revision: 7896
Log message:

      Setting the SOAS POPLmark model to the side for the moment
      while I look at the infrastructure for reflection.
      
      My plan is to work through it by adding a grammar.
      By the time I am done, I should understand what it contains.
      
      Unfortunately, the reflection files are not commented,
      so this means a lot more interaction than necessary.
      
      Reminder: it is unacceptable to write undocumented code.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-11 11:26:18 -0700 (Tue, 11 Oct 2005)
Revision: 7897
Log message:

      Added a grammar for HOAS vectors and lists.
      
      Note the following ambiguity.
      
          let f = fun x -> x in f [1; 2; 3]
      
      This is resolved by prefering second-order variables
      over application to lists.  So, to get what you probably
      intended, you have to write.
      
          let f = fun x -> x in f ([1; 2; 3])
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-11 12:16:45 -0700 (Tue, 11 Oct 2005)
Revision: 7898
Log message:

      Added a grammar for deBruijn terms.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-10-14 09:02:38 -0700 (Fri, 14 Oct 2005)
Revision: 7911
Log message:

      Fixed the proof of apply_ffun_wf which was probably broken by my recent commit to itt_finite_fun1.prla and to itt_bool

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-10-14 14:44:52 -0700 (Fri, 14 Oct 2005)
Revision: 7912
Log message:

      Almost proved the correct induction rule for hoas_lang.
      Add a bunch of theorems in other theories.
      Still need to prove some of them.
      
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-16 21:34:10 -0700 (Sun, 16 Oct 2005)
Revision: 7914
Log message:

      - Fixed the corrupted itt_subset.prla file.
      - Finished the remaining 3 proofs in itt_subset.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-16 23:27:47 -0700 (Sun, 16 Oct 2005)
Revision: 7915
Log message:

      Proved the itt_bisect lemmas that did not have a complete proof

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-17 10:50:21 -0700 (Mon, 17 Oct 2005)
Revision: 7918
Log message:

      Rewrite should rewrite terms->operator-params in relaxed mode.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-17 11:15:25 -0700 (Mon, 17 Oct 2005)
Revision: 7919
Log message:

      Added itt/test, defining untype lambda calculus.
      

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

      Added an attempt at an induction rule for ULambda.
      
      But, I just noticed that the elimination rules in Itt_hoas_lang
      are not induction principles.  Well I suppose Aleksey told me
      that once.
      
      In any case, I hope we can get induction principles!
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-17 12:28:28 -0700 (Mon, 17 Oct 2005)
Revision: 7921
Log message:

      I'm not sure what lambda{...} looks like in terms of mk_bterm{...}
      (is there a binding occurrence somewhere?).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-17 13:32:32 -0700 (Mon, 17 Oct 2005)
Revision: 7922
Log message:

      Removed the non-existent itt_fun from the list of theories to print.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-17 19:31:05 -0700 (Mon, 17 Oct 2005)
Revision: 7923
Log message:

      Mostly finished the generic term parser.  This uses Perv!xterm
      and Perv!xbterm for the raw representation (see Itt_grammar for
      the current real grammar).
      
          term ::= ... | "opname" opt_params opt_bterms
          params ::= [ param, ..., param ]
          bterms ::= { bterm; ...; bterm }
          bterm ::= term | \v1, ..., vn. term
      
      Note, proper bterms need a leading backslash.  I just don't
      really want to get into the whole issue of disambiguating pairs
      from bterms:/
      
      Some examples.
      
          "int"
          "type"{T}
          "number"[1:n]
          "lambda"{\x. x}
      
      I still need to add support for params.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-17 19:41:26 -0700 (Mon, 17 Oct 2005)
Revision: 7924
Log message:

      Slightly different term grammar.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 12:58:52 -0700 (Tue, 18 Oct 2005)
Revision: 7925
Log message:

      Finished the generic term parser.  The grammar is:
      
          term ::= ... | opname opt_params opt_bterms
          opname ::= <string> | opname . <string>
          params ::= [ param; ...; param ]
          param ::= pexp | pexp : kind
          pexp  ::= <int> | - <int> | <string> | <id> | pexp ' | pexp|pexp | ( term )
          bterms ::= { bterm; ...; bterm }
          bterm ::= term | \v1, ..., vn. term
      
      Some examples
      
         "number"[-1]
         "add"{1; 2}
         "Itt_rfun"."lambda"{\x. x}
         "spread"{e1; \x, y. e2[x; y]}
         "operator"[(fun x -> y):op]
      
      The reason for the quotes around the opname is because variables
      are not quoted.  The reason for the backslash before binders is
      to simplify the grammar.
      
      Of course, it is also possible to define a variant for the
      traditional syntax.  We may wish to do so someday.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 13:59:11 -0700 (Tue, 18 Oct 2005)
Revision: 7926
Log message:

      Moved the core term grammar into Base_grammar.  It is now
      called "xterm", "xrule", and "xrewrite".
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 15:34:29 -0700 (Tue, 18 Oct 2005)
Revision: 7927
Log message:

      This is an initial experiment in reflection syntax.
      The syntax is as follows, based loosely on Lisp quotations.
      
          $`[depth] term : quotes a term at a specific binding depth
          $,term         : cancels the quotation
      
      Examples:
      
          $`[d] "apply"{e1; e2} ==
              mk_bterm{d; operator[(apply{e1; e2}):op]; [e1; e2]}
      
          $`[d] "lambda"{x. "apply"{$,(e1 +@ x); e2}} ==
              mk_bterm{d; operator[(lambda{x. it}):op];
                 [bind{x. mk_bterm{d -@ 1; operator[(apply{it; it}):op]; [e1 +@ x; e2]}]
      
      Don't worry that the term doesn't make sense, I'm just showing the syntax.
      
      (I don't know if bind{x. ...} is the right thing to do on the subterm.
      In fact, I'm just guessing about what reflected terms look like.)
      
      To simplify a little, I would like to add a depth marker $#.
      This would simplify the code in the case where the depth
      is computed bottom-up.
      
      (I'm using the simpler syntax here--the term is similar to the
      one above).
      
          $`(fun x -> ($,(e1 + x) $#e2))
      
      In this case, the depth of the lambda is (depth{e2} +@ 1).
      
      !! Note !!
      
      I hardcoded this iform into Filter_grammar.  I think it should go
      somewhere else, preferably into one of the Itt_hoas_* files, but
      this is not easy at the moment.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 16:38:50 -0700 (Tue, 18 Oct 2005)
Revision: 7928
Log message:

      Added the $# marker I was talking about.
      Added the Var type:
         Var <--> Img{nat * nat; v. spread{v; i, j. var{'i; 'j}}}
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 18:31:15 -0700 (Tue, 18 Oct 2005)
Revision: 7929
Log message:

      Looks like the basic reduction rules are missing, like
      |[e1; e2]| doesn't normalize:(
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 19:06:25 -0700 (Tue, 18 Oct 2005)
Revision: 7930
Log message:

      Proved that an application is a program.
      The proof Itt_hoas_ulambda.apply_wf is painfully complicated--
      if someone has more experience with compatible_shapes, would
      you take a look at the proof?
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-18 19:43:33 -0700 (Tue, 18 Oct 2005)
Revision: 7931
Log message:

      Added the $`"Lambda"{x. e[x]} wf theorem Itt_hoas_ulambda.lambda_wf.
      
      Please help:)  I don't know what quoted terms look like.
      
      I am using the following.
      
         $`[depth] Lambda{x. e[x]} ==
             mk_bterm{depth; operator[Lambda{1}]; [bind{x. e[x]}]}
      
      I assume the bind{x. ...} is wrong, is this true?
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-10-18 22:42:47 -0700 (Tue, 18 Oct 2005)
Revision: 7932
Log message:

      Ocaml 3.08.0 and 3.08.1 are not good enough - they don't have Pcaml.position needed to compile util/pa_macro.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-19 18:25:17 -0700 (Wed, 19 Oct 2005)
Revision: 7935
Log message:

      The typeclass Ty is no longer a subtype of Term, it is back to
      begin a subtype of Dform.
      
      This breaks the poplmark/naive theory, we will need to find
      some other way of resurrecting it if needed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-19 19:19:01 -0700 (Wed, 19 Oct 2005)
Revision: 7936
Log message:

      Simplified quotation iform expander, and re-proved Itt_hoas_ulambda.apply_wf.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-19 19:42:12 -0700 (Wed, 19 Oct 2005)
Revision: 7937
Log message:

      Proved Itt_hoas_ulambda.lambda_wf.
      
      Add Itt_hoas_jyh for terms/theorems that that I need 
      until I can find where to add them back into the reflection
      theories.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 11:42:08 -0700 (Thu, 20 Oct 2005)
Revision: 7938
Log message:

      Part way to proving the induction principal for ULambda.
      Proving some lemmas first.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 11:43:26 -0700 (Thu, 20 Oct 2005)
Revision: 7939
Log message:

      Call the lemma Itt_hoas_lang2.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 12:34:38 -0700 (Thu, 20 Oct 2005)
Revision: 7940
Log message:

      Also problems with extensional sets.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-10-20 14:46:31 -0700 (Thu, 20 Oct 2005)
Revision: 7941
Log message:

      Proved some theorems
      
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-10-20 15:04:27 -0700 (Thu, 20 Oct 2005)
Revision: 7942
Log message:

      A very draft version of lambda calculus.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 15:08:07 -0700 (Thu, 20 Oct 2005)
Revision: 7943
Log message:

      Added extensional elistmem_set{'l; 'T}.  It turns out that this
      doesn't really help me, but sometime this may be useful.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 15:26:36 -0700 (Thu, 20 Oct 2005)
Revision: 7944
Log message:

      Added itt_hoas_lang2.prla
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 16:10:01 -0700 (Thu, 20 Oct 2005)
Revision: 7945
Log message:

      Changed listmem_set_elim2 to a more expressive definition.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 16:28:23 -0700 (Thu, 20 Oct 2005)
Revision: 7946
Log message:

      Removed extensional version elistmem_set{'l; 'T}
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-10-20 16:32:28 -0700 (Thu, 20 Oct 2005)
Revision: 7947
Log message:

      Aleksey: Forgot to add this.
      

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

      Merged the ITT spelling list into the global one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-20 18:42:24 -0700 (Thu, 20 Oct 2005)
Revision: 7950
Log message:

      For some reason, itt_list2 was using itt_pairwise, which is bad. I removed the
      "extends Itt_pairwise" for now, but now a few proofs will need fixing.
      

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

      Group/VNC editing (Aleksey, Alexei, Jason and Xin):
      
      This refactors ITT into several subdirectories instead of a single huge pile
      that we used to have.