Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 12:52:01 -0800 (Tue, 01 Nov 2005)
Revision: 8071
Log message:

      Proved the induction principle on derivations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 20:01:07 -0800 (Tue, 01 Nov 2005)
Revision: 8075
Log message:

      Rebuilt the FSub languages directly from BTerm.
      I think this is the way to go, the theories are much smaller.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 20:33:50 -0800 (Tue, 01 Nov 2005)
Revision: 8076
Log message:

      Separate the judgments from the rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-02 16:35:41 -0800 (Wed, 02 Nov 2005)
Revision: 8080
Log message:

      I am working on rewriting and simplifying MetaPRL core IO - I want to change
      it so that the "role" of .cmoz/.prlb/.prla files is better established.
      
      In particular. my goals are
      
       - In the editor, the module is always taken from the .cmoz. (Optionally: if
         .prlb or .prla is newer, then the proofs are read and _merged_)
       - The .prlb is a "cache" for the .prla. If the .prla have changed since the
         .prlb was generated, the old .prlb is discarded (even if it happens to be
         newer).
       - Optionally: refuse to load .cmoz into toploop, if it was compiled against a
         version of MetaPRL that is different from the one currently running.
       - Longer term: only store proofs (and other items created or modified from
         the toploop) in .prlb/.prla. This way the .prla are much smaller, the
         locations are not stored in .prlb, the items created from the toploop are
         not discarded at repompile.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-02 16:43:10 -0800 (Wed, 02 Nov 2005)
Revision: 8081
Log message:

      Working on the new IO. This commit mostly just rips apart the old code,
      without yet contributing much new.
      
      Not even close to compiling.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-02 21:13:35 -0800 (Wed, 02 Nov 2005)
Revision: 8082
Log message:

      Added string options.  These are like selT, but you need to use
      addOptionT or withOptionT.
      
      The differences with selT:
         1. The option is a string (perhaps it should be an opname?)
         2. A rule annotation can have multiple options using the
            [StringOption "foo"; StringOption "bar"] intro/elim
            argument.
      
      The addOptionT adds the option for the entire rest of the proof tree.
      The withOptionT adds it for a single tactic.
      The removeOptionT removes it for the rest of the proof tree.
      The withoutOptionT removes it for a single tactic.
      
      Unfortunately, the addOptionT isn't currently working.  Somewhere,
      it looks like proof annotations are getting cleared.  Looking
      into it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 10:38:21 -0800 (Thu, 03 Nov 2005)
Revision: 8084
Log message:

      Commented the code in Proof_boot that was removing all annotations
      from IO proofs.
      
      If I understand correctly, this code was added to clean up old proofs
      where annotations were mistakenly lying around.  That is, it was added
      for backwards compatibility.
      
      The best solution is probably just to re-export those broken proofs
      to fix the problem.  Alternately, and less satisfying, we could add
      another annotation that says "I really want to keep my annotations."
      
      We may want to add an annotation check to the subgoal/cache matcher
      so that subgoals are considered to be equal only if the annotations
      match.  This is probably good enough, or we could add an explicit
      annotation transformation rulebox before pulling in a subgoal with
      different annotations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 16:47:41 -0800 (Thu, 03 Nov 2005)
Revision: 8085
Log message:

      Updated with Itt_dfun axioms instead of the Itt_rfun ones and Itt_pairwise
      axioms instead of Itt_pointwise ones.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 18:29:13 -0800 (Thu, 03 Nov 2005)
Revision: 8088
Log message:

      - Proved the nilSqequal rule (it used to be primitive).
      - Some more progress verifying ITT Core under the pairwise functionality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 21:01:47 -0800 (Thu, 03 Nov 2005)
Revision: 8089
Log message:

      Defined the IO module for .cmiz
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 21:08:10 -0800 (Thu, 03 Nov 2005)
Revision: 8090
Log message:

      - Proof steps match only if the annotations match.
      - Removed annotation removal during IO squashing.
      - Expanded all proofs that produce warning messages,
        and re-exported them.
      
      Note, I believe I hit the weak-memo bug, or something like it
      during proof expansion, and I got crazy terms appearing in
      unrelated theorems:(  I believe I have re-fixed all those
      broken proofs.  check-status reports that all is well.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 21:35:59 -0800 (Thu, 03 Nov 2005)
Revision: 8091
Log message:

      Added ty_exp_elim_slow for testing purposes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 22:00:17 -0800 (Thu, 03 Nov 2005)
Revision: 8092
Log message:

      Moving the closed branches out of the way.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 22:14:06 -0800 (Thu, 03 Nov 2005)
Revision: 8093
Log message:

      Adding lm_set.ml to the list of files to be included in the "magic" digest
      calculation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 22:16:24 -0800 (Thu, 03 Nov 2005)
Revision: 8094
Log message:

      Exploring the "this takes too long" example further. Simply running jproverT
      in /poplmark_naive/pmn_core_terms/ty_exp_elim_slow/1/1/1/1/1/2/2/1/1/1/1/2
      seems to take too long.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-04 09:27:20 -0800 (Fri, 04 Nov 2005)
Revision: 8095
Log message:

      Relaxed a bit the test for "may be patterns". If all occurrences of a second
      variable in the redex are "pattern-like" occurrences inside another second
      order variable (which means that in the actual match in may not occur at all
      if that other SO variable does not depend on its argument), the rewriter used
      to complain. I've changed it so that if that SO variable does not occur in the
      contractum, then rewriter accepts such rewrite.
      
      Example:
      
      interactive tunionHyp {| nth_hyp |} 'H :
         sequent { <H>; x: 'B['a]; <J['x]> >- 'x in Union x:'A. 'B['x]  }
         
      Here the rewriter used to complain that 'a does not have a pattern and needs
      to be passed in as an argument, which is clearly unnecessary in this case.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-04 10:05:14 -0800 (Fri, 04 Nov 2005)
Revision: 8096
Log message:

      - Updated the elimination rules for Union so that they better preserve binding
        names.
      
      - Fixed the proof of tunionElimination_disjoint
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-04 14:07:15 -0800 (Fri, 04 Nov 2005)
Revision: 8097
Log message:

      Apparently we had forgotten to save string attributes to the IO proof
      terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-04 20:36:28 -0800 (Fri, 04 Nov 2005)
Revision: 8100
Log message:

      Added the (Annotate of tactic_arg * tactic_arg) proof step.  This
      addresses the problem with proof annotations being dropped.
      
      Proof files (.prlb and .prla) are defined to be backwards-compatible,
      but not forwards-compatible.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 13:20:43 -0800 (Sat, 05 Nov 2005)
Revision: 8109
Log message:

      Save the current version with structural induction while I
      try the pure BTerm approach.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 15:50:05 -0800 (Sat, 05 Nov 2005)
Revision: 8110
Log message:

      Trying out the "well-formedness"-based Fsub logic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 20:40:58 -0800 (Sat, 05 Nov 2005)
Revision: 8111
Log message:

      Added the "reflected_logic" block, see Pmn_core_logic for an example.
      Currently working out the rule arguments, so the final few
      rules are disabled.
      
      The main goal is, for a rule
      
         interactive foo : <mt>
      
      Do 3 things:
         1. Define unfold_foo : foo <--> <mt>
         2. Add a wf rule, <H> >- foo IN ProofRule
         3. Add the provability rule (one direction of reflection):
      
            If <mt> == <t1> --> ... -> <tn>
            Add the real rule:
      
               <H> -> Provable{t1} -->
               ...
               <H> -> Provable{tn}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-05 23:48:24 -0800 (Sat, 05 Nov 2005)
Revision: 8112
Log message:

      Further "autoT is taking too long" investagation - in 
      /poplmark_naive/pmn_core_terms_test/ty_exp_elim_slow/1/1/1/1/1/2/2/1/1/1/2/1
      even the simple_jproverT tactic is taking forever.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-06 18:03:10 -0800 (Sun, 06 Nov 2005)
Revision: 8116
Log message:

      Returned to requiring wf of sequents, so that we don't need wf-subgoals
      in the object logic.
      
      This mostly completes the initial phase of the Filter_parse reflection.
      You can define a logic of syntax, or a logic of rules, or any mixture.
      
         reflected_logic foo_logic =
         struct
            declare typeclass AExp
            declare typeclass BExp
      
            declare A : AExp
            declare B{'e : AExp} : AExp
            declare C{a: AExp. 'e['a] : BExp} : BExp
      
            interactive c_intro :
               sequent { <H>; a: A >- 'e['a] } -->
               sequent { <H> >- C{a. 'e['a]} }
         end
      
      Declarations are processed as normal in this block, plus 3 new parts
      are added.  Only the reflected rule makes sense.
      
      Each declaration/rule produces 3 parts:
         1. A definition (unfold_X : X <--> <definition>)
         2. A wf-goal (interactive X_wf : X in ProofRule)
         3. An ITT rule:
            interactive X_itt :
               <H1> >- Provable{$`(<H>; a: A >- e[a])} -->
               <H1> >- Provable{$`(<H> >- C{a. e[a]})}
      
      Plus you get the complete logic, containing all the rules
      that were defined (an no others).
      
         define foo_logic <--> [A; B; C; c_intro]
         define Provable{'e} <-->
            Itt_hoas_sequent_native!Provable{Sequent; foo_logic; 'e}
      
      I haven't proved any theorems, so we'll see how that goes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-06 18:18:30 -0800 (Sun, 06 Nov 2005)
Revision: 8117
Log message:

      OMake should be checked out from the 0.9.6.x branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-06 22:35:45 -0800 (Sun, 06 Nov 2005)
Revision: 8119
Log message:

      Minor fixes in the IO code. Still a long way to go.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 01:14:46 -0800 (Mon, 07 Nov 2005)
Revision: 8123
Log message:

      - env_arg.mli: use self-documentary type names (e.g. "Arg.usage_msg" instead
        of "string")
      
      - removed a little bit of unused code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 01:22:48 -0800 (Mon, 07 Nov 2005)
Revision: 8124
Log message:

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