Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-01 09:14:48 -0800 (Tue, 01 Mar 2005)
Revision: 6786
Log message:

      Fixed some comments
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-01 09:23:06 -0800 (Tue, 01 Mar 2005)
Revision: 6787
Log message:

      More theorems
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-01 10:24:50 -0800 (Tue, 01 Mar 2005)
Revision: 6788
Log message:

      Added a definition:
      iform make_bterm: make_bterm{'op;'bdepth;'subterms} <--> make_bterm{inject{'op;'bdepth};'subterms}
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-01 10:31:00 -0800 (Tue, 01 Mar 2005)
Revision: 6789
Log message:

      Fixed theorems in the lambda example. Now, I belive, all theorems there should be provable. I'll try to prove them
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-01 15:09:16 -0800 (Tue, 01 Mar 2005)
Revision: 6790
Log message:

      Use omake to construct the final mmc theory.
      
      In mk/config, you now have the option to specify the
      mmc extensions and backends.
      
      For each extension, you must specify:
         1. The name of the extension
         2. The files
         3. Any backend-specific files
      
      See any of the extensions/*/Files for examples.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-01 16:04:01 -0800 (Tue, 01 Mar 2005)
Revision: 6792
Log message:

      Minor code simplification
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-01 21:02:47 -0800 (Tue, 01 Mar 2005)
Revision: 6797
Log message:

      Deleted some unused functionality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-01 21:09:13 -0800 (Tue, 01 Mar 2005)
Revision: 6799
Log message:

      Removed some unused code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-01 23:10:05 -0800 (Tue, 01 Mar 2005)
Revision: 6805
Log message:

      - Itt_set: alpha-renamed the rules to make them better preserve the names of
        the bound variables.
      
      - Replaces all the usages of the ad-hoc Var.maybe_new_var_arg with a more
        correct Var.maybe_new_var_set.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-02 11:31:16 -0800 (Wed, 02 Mar 2005)
Revision: 6813
Log message:

      Simplified the instance/pattern code a bit - when we already have a pattern,
      there is no need to turn patterns into instances - the code for matching two
      patters is more efficient that the code for matching a pattern and an
      instance.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-02 11:31:40 -0800 (Wed, 02 Mar 2005)
Revision: 6814
Log message:

      "Opname.eq" instead of "="
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-02 11:36:59 -0800 (Wed, 02 Mar 2005)
Revision: 6816
Log message:

      Some display forms
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-02 13:38:16 -0800 (Wed, 02 Mar 2005)
Revision: 6817
Log message:

      On display, if a 0-arity SO var clashes with an FO binding, then leave the
      variable "fully qualified" to avoid confusion.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-02 17:31:03 -0800 (Wed, 02 Mar 2005)
Revision: 6818
Log message:

      Changed make_bterm_eval, fixed make_bterm_eval
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-02 17:47:11 -0800 (Wed, 02 Mar 2005)
Revision: 6819
Log message:

      Added comments, display forms, ...
      Changed dest_bterm to using "iform".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-02 18:23:24 -0800 (Wed, 02 Mar 2005)
Revision: 6820
Log message:

      "De-kreitzed" the proof of /itt/itt_record0/record_exchange
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-02 23:52:01 -0800 (Wed, 02 Mar 2005)
Revision: 6823
Log message:

      Added more comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-03 00:01:04 -0800 (Thu, 03 Mar 2005)
Revision: 6824
Log message:

      Removed some useless stuff.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-03 16:56:02 -0800 (Thu, 03 Mar 2005)
Revision: 6829
Log message:

      Added comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-03 17:38:10 -0800 (Thu, 03 Mar 2005)
Revision: 6830
Log message:

      Added comments.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-03 19:42:40 -0800 (Thu, 03 Mar 2005)
Revision: 6832
Log message:

      Added (minor) x86 optimizations.
      The simple contexts seem to be working.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-03 22:53:53 -0800 (Thu, 03 Mar 2005)
Revision: 6836
Log message:

      supinfT did not convert integer subtraction and unary minus to operations on rationals.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-04 20:14:47 -0800 (Fri, 04 Mar 2005)
Revision: 6842
Log message:

      Added the x86 conventions.
      
      Note, this includes a commit to MetaPRL to handle quotation patterns.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-05 00:17:34 -0800 (Sat, 05 Mar 2005)
Revision: 6844
Log message:

      Proved some rules in Itt_reflection_example_lambda;
      Fixed a bug in Itt_reflection_new.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-05 12:00:52 -0800 (Sat, 05 Mar 2005)
Revision: 6846
Log message:

      The files for register allocation now compile.  Untested.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-05 15:49:57 -0800 (Sat, 05 Mar 2005)
Revision: 6847
Log message:

      Yay!  The backend is complete, and mmc_int_test/test0 compiles and
      runs correctly.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-06 12:04:38 -0800 (Sun, 06 Mar 2005)
Revision: 6852
Log message:

      Added the "typeof" operator to x86.
      The current method for elimination
         1. adds constraints for all the variables
         2. Eliminates the typeof
         3. Erase all leftover constraints
      
      This seems like it can be generalized.  Adding a "sweep"
      operator that sweeps down a type environment (as we have
      discussed for the core).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-07 00:33:42 -0800 (Mon, 07 Mar 2005)
Revision: 6855
Log message:

      A more complete sweeper for x86.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-07 17:04:34 -0800 (Mon, 07 Mar 2005)
Revision: 6857
Log message:

      Start to write a definition of language
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-07 17:06:50 -0800 (Mon, 07 Mar 2005)
Revision: 6858
Log message:

      some fixes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-08 12:11:56 -0800 (Tue, 08 Mar 2005)
Revision: 6859
Log message:

      Converted the x86 sweeper to propositional form.  That is, the sweep
      environment is a collection of propositions.  This is probably what
      we want to use for tast optimization too.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-08 15:50:51 -0800 (Tue, 08 Mar 2005)
Revision: 6860
Log message:

      Add a definition of find
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-08 22:20:42 -0800 (Tue, 08 Mar 2005)
Revision: 6868
Log message:

      More on Itt_synt_langage
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-09 09:19:13 -0800 (Wed, 09 Mar 2005)
Revision: 6869
Log message:

      Convert "std" lambdas to "rec" lambdas during type inference.
      I'm not sure exactly the difference between "rec" and "std",
      but let's work with it for now.
      
      Also, I renamed Sequent.explode_sequent to Sequent.explode_sequent_arg
      to avoid the shadowing hassle with TermMan.explode_sequent.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-09 14:49:07 -0800 (Wed, 09 Mar 2005)
Revision: 6874
Log message:

      - Added a definition of the type of lists with different elements diff_list. (What is the better name for it?)
      - More on itt_synt_language. Some rules probably still miss well-formednes conditions
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-09 18:28:08 -0800 (Wed, 09 Mar 2005)
Revision: 6875
Log message:

      1. Fixed a bug noted by Xin
      2. Some documentation
      3. Rewrote reflection_example using synt_language`
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-09 21:19:03 -0800 (Wed, 09 Mar 2005)
Revision: 6876
Log message:

      Added lazy computation of grammars (this is bug #411).  This should
      reduce compile times in mmc significantly.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-10 13:48:46 -0800 (Thu, 10 Mar 2005)
Revision: 6880
Log message:

      Some proofs (especially for "find")
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 14:06:18 -0800 (Thu, 10 Mar 2005)
Revision: 6881
Log message:

      Made the parsetree.cmi checking smarter. This makes MetaPRL compatible with
      GODI's default way of compiling and installing OCaml (both 3.08 and dev
      branches of GODI).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 14:20:20 -0800 (Thu, 10 Mar 2005)
Revision: 6882
Log message:

      Mention GODI option for installation
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-10 15:28:08 -0800 (Thu, 10 Mar 2005)
Revision: 6883
Log message:

      Add a definition of last_var
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 15:28:57 -0800 (Thu, 10 Mar 2005)
Revision: 6884
Log message:

      *******************************************************************
      * WARNING: This breaks binary compatibility for .cmoz/.prlb files *
      *******************************************************************
      
      This commit increases the separation between the first-order variables and the
      meta-variables:
      - The free variables computation will no longer include the SO variables in
        the free variables list.
      - The rewriter should handle correctly the case of a FO variable and a SO
        variable (even a 0-arity one) sharing the same name (the rewriter now will
        consider the two completely unrelated).
      - When applying rules and cond. rewrites, the refiner will give the rewriter
        the set of all the meta-vars in the sequent, so that the rewriter can avoid
        creating new binding that would clash with meta-vars (this is only needed to
        avoid user confusion on I/O, the semantics does not depend on this).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-10 16:19:55 -0800 (Thu, 10 Mar 2005)
Revision: 6885
Log message:

      1. Added the operator make_depth{'s;'n}, that adds some variables to the term $s$ to make its binding depth to be equal to $n$.
          I can't think of the better name.
         I changed definition of add_vars_upto{'s;'t}. Xin, could you fix the proofs?
      
      2. Added some operators in lambda_example.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 17:15:14 -0800 (Thu, 10 Mar 2005)
Revision: 6886
Log message:

      (Bug 415) removed an unnecessary check for non-repeating bindings in sequents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 17:17:09 -0800 (Thu, 10 Mar 2005)
Revision: 6887
Log message:

      Some functions were not properly implemented; fixing.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-10 17:29:47 -0800 (Thu, 10 Mar 2005)
Revision: 6888
Log message:

      rules and proofs for diff_list.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-10 17:31:14 -0800 (Thu, 10 Mar 2005)
Revision: 6889
Log message:

      Fixed a bug in the definition of "dest";
      Some proofs.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-10 18:01:08 -0800 (Thu, 10 Mar 2005)
Revision: 6890
Log message:

      Added a definition of beta-reduction for the simple lambda-calculus
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 19:07:18 -0800 (Thu, 10 Mar 2005)
Revision: 6891
Log message:

      Made the var_subst function alpha-invariant.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 20:06:22 -0800 (Thu, 10 Mar 2005)
Revision: 6892
Log message:

      Created a separate SOContext choice for contexts in Term_ds.core_term type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 20:40:26 -0800 (Thu, 10 Mar 2005)
Revision: 6893
Log message:

      Fixing a bug in Term_std.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 20:41:30 -0800 (Thu, 10 Mar 2005)
Revision: 6894
Log message:

      Added a possibility to debug internal interfaces for Refine and Rewrite
      modules, instead of the external ones.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-10 22:24:56 -0800 (Thu, 10 Mar 2005)
Revision: 6895
Log message:

      Fixed a painful bug in the parser where precedences were not
      being translated correctly during a grammar merge.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-10 23:49:48 -0800 (Thu, 10 Mar 2005)
Revision: 6896
Log message:

      Fixed proofs of add_vars_upto and finished proofs of make_depth.
      
      Note: The definition of last_var is invalid for a 0-depth non-var bterm. Alexei,
      is this what you really want?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 23:53:27 -0800 (Thu, 10 Mar 2005)
Revision: 6897
Log message:

      - When calling the type inference from filter, pass only the "proper" term
        parameters (i.e. skip IntArg and AddrArg parameters) to the typechecker.
      
      - In type inference, take the context environment from the redex and params,
        not just from the redex (this should partially solve Yegor's problem with
        the indWrap in CIC).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-11 00:53:53 -0800 (Fri, 11 Mar 2005)
Revision: 6899
Log message:

      Put back the occurs check that I've unintentially removed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-11 01:46:12 -0800 (Fri, 11 Mar 2005)
Revision: 6900
Log message:

      itt_int_bench3 is also generated by gen_bench
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-11 14:05:49 -0800 (Fri, 11 Mar 2005)
Revision: 6903
Log message:

      (Bug 416) Give a meaningful error message when:
      
      - One of the keywords rule/rewrite/topval is encountered in an .ml file
      
      - One of the keywords prim/interactive/prim_rw/interactive_rw is encountered
        in an .mli file.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-11 16:55:35 -0800 (Fri, 11 Mar 2005)
Revision: 6905
Log message:

      Added the subject reduction theorem and started the proof.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-11 17:41:45 -0800 (Fri, 11 Mar 2005)
Revision: 6907
Log message:

      In a rewriter, I added a way to consider "!v" as bindings. If a term
      Perv!xbinder{!v} is specified as one of the rewrite arguments, then 'v is
      considered "bound" in the redex. In other words, terms like 'e[!v] in the
      redex would be considered _patterns_ for 'e (so no need to pass in
      bind{x.'e['x]} any more).
      
      Note that while the implementation of such a rule will now require that all
      the occurrence of !v in 'e are "selected", we should still consider the
      semantics to be the original one (where any subset of !v occurrences might get
      "selected"). Otherwise we might get into trouble with derived rules/rewrite
      (I am not sure).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-11 19:36:39 -0800 (Fri, 11 Mar 2005)
Revision: 6908
Log message:

      I'm being a little anal here.  I prefer the form where the <singleton_params_c>
      is a context, containing singleton types.  This gets the arity of the functions
      right, and I feel a little better about it just because I have a better
      understanding of the semantics.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-11 22:39:53 -0800 (Fri, 11 Mar 2005)
Revision: 6911
Log message:

      NOTE: this breaks binary compatibility, bleh.
      
      Added much better error messages to the parser, as Aleksey and I
      discussed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-12 11:25:50 -0800 (Sat, 12 Mar 2005)
Revision: 6915
Log message:

      Added non-binding contexts (bug #417).
      mmc_int_test/test1 now passes closure conversion.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-13 20:50:15 -0800 (Sun, 13 Mar 2005)
Revision: 6917
Log message:

      A lot of changes:
         1. Added a typeof operator, to be used during sweeping.
         2. Closure elimination is a sweep phase, but not correct
            yet because we need to convert it to positive form.
      
      We need to add IsValue rules for the closure pairs...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 16:13:05 -0800 (Mon, 14 Mar 2005)
Revision: 6919
Log message:

      Minor fix in the match_terms function.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-14 16:46:40 -0800 (Mon, 14 Mar 2005)
Revision: 6920
Log message:

      Proved the well_formedness of is_same_op for Operator.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 18:35:24 -0800 (Mon, 14 Mar 2005)
Revision: 6921
Log message:

      Allow arg{|... >- ... |} notation for sequents in the dform "options" list.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 18:57:55 -0800 (Mon, 14 Mar 2005)
Revision: 6922
Log message:

      - Fixed a bug in parsing quotations within the <:doc< >> quotations.
      
      - Added underline{'t} display form operator (which works correctly in HTML,
        TeX and even PRL modes)
      
      - Simplified and improved the display forms for the Base_reflection!bterm
        sequents.
      
      - Added a sample documenation to one of the ML rewrites in Base_reflection.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 19:21:25 -0800 (Mon, 14 Mar 2005)
Revision: 6923
Log message:

      Added a fake_mlrw operator to make documenting ML rewrites easier.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 21:15:10 -0800 (Mon, 14 Mar 2005)
Revision: 6926
Log message:

      Do not try to read/write the MetaPRL history file when the -batch flag is
      used.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-14 21:38:43 -0800 (Mon, 14 Mar 2005)
Revision: 6928
Log message:

      In TermSubst.match_terms, do include the trivial v->v "renamings" in the
      returned subst.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-15 00:32:53 -0800 (Tue, 15 Mar 2005)
Revision: 6929
Log message:

      More proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-15 16:28:20 -0800 (Tue, 15 Mar 2005)
Revision: 6937
Log message:

      Proper scoping for OCamlGeneratedFiles.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-15 23:08:42 -0800 (Tue, 15 Mar 2005)
Revision: 6943
Log message:

      More proofs.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-16 00:39:25 -0800 (Wed, 16 Mar 2005)
Revision: 6944
Log message:

      Finished proofs in Itt_synt_language.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-16 15:00:18 -0800 (Wed, 16 Mar 2005)
Revision: 6948
Log message:

      Added BTerm{'n} and BTerm_plus{'n} in Itt_synt_bterm; Corrected last_var{'bt}
      in Itt_synt_subst.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-16 15:27:57 -0800 (Wed, 16 Mar 2005)
Revision: 6949
Log message:

      The apply_var_fun[_arg]_at_addr now rename the bterm bindings among the
      addressed path to avoid clashes. This is necessary to be able to properly
      handle non-sequent contexts in the rewriter.
      
      TODO: the sequent bindings need to be renamed as well.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-16 16:11:03 -0800 (Wed, 16 Mar 2005)
Revision: 6950
Log message:

      Replaced *language* with *lang* to avoid misspelling.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-16 16:14:00 -0800 (Wed, 16 Mar 2005)
Revision: 6952
Log message:

      Remove the Itt_synt_language module.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-16 17:01:55 -0800 (Wed, 16 Mar 2005)
Revision: 6955
Log message:

      Renamed Itt_synt_bterm!is_same_op/same_op to is_same_op_of/same_op_of
      in order to avoid confusion with Itt_synt_operator!is_same_op/same_op.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-03-16 17:51:32 -0800 (Wed, 16 Mar 2005)
Revision: 6957
Log message:

      More on the proof of the subject reduction
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-16 18:13:36 -0800 (Wed, 16 Mar 2005)
Revision: 6958
Log message:

      Added a missing check that makes sure SO instances do not have free contexts.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-16 22:33:31 -0800 (Wed, 16 Mar 2005)
Revision: 6959
Log message:

      (Bug 405) When loading a .cmiz or .cmoz file, the grammar needs to be
      reconstructed correctly.
      
      It used to be the case that the following invariant may be assumed to be true
      "among all the extended parents, at most one will have a non-empty grammar, or
      the current module will have its own copy of the grammar". However now that
      the filter-grammar keeps track of the grammar inheritance, this is no longer
      true (one parent may have a grammar that contains the grammars of all other
      parents). In other words, when loading a file and scanning parents, one now
      has to take a _union_ of grammars (knowing that this lazy union will either
      become singleton when flattened, or it will be shadowed by a PRLGrammar).
      
      Also, when loading a .cmoz, we need to start by loading the grammar from .cmiz
      (because this is what filter_parse starts with when parsing an .ml file).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-17 01:09:00 -0800 (Thu, 17 Mar 2005)
Revision: 6960
Log message:

      More proofs.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-17 12:55:03 -0800 (Thu, 17 Mar 2005)
Revision: 6961
Log message:

      Added the ability to use quotations to specify meta_terms.
      
      mmc_int_test/test1 now passes code generation.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-17 14:17:56 -0800 (Thu, 17 Mar 2005)
Revision: 6962
Log message:

      Change Itt_synt_bterm!btermVar from AutoMustComplete to nth_hyp.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-17 16:23:41 -0800 (Thu, 17 Mar 2005)
Revision: 6963
Log message:

      Added code for var_subst on sequents.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-17 16:57:22 -0800 (Thu, 17 Mar 2005)
Revision: 6964
Log message:

      More proofs for Itt_reflection_example_lambda.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-17 17:01:49 -0800 (Thu, 17 Mar 2005)
Revision: 6965
Log message:

      Added meta_term grammar to the mmc core.
      Removed the need for the backquote (`)
      before a meta_term in a rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-17 17:44:52 -0800 (Thu, 17 Mar 2005)
Revision: 6967
Log message:

      When backtrace is on, do not attempt to pretty-print exceptions (this destroys
      backtraces for some reason).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-17 20:59:57 -0800 (Thu, 17 Mar 2005)
Revision: 6968
Log message:

      Some updates to CPS.  Preparing to remove polymorphism introduced earlier.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-17 21:00:43 -0800 (Thu, 17 Mar 2005)
Revision: 6969
Log message:

      Changed splitITE to use TermAddr functionality for finding appropriate
      if-then-else locations, instead of using its own ad-hoc version which didn't
      play nicely with nested sequents (such as reflected bterms).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-18 00:10:54 -0800 (Fri, 18 Mar 2005)
Revision: 6971
Log message:

      MetaPRL is compatible with OCaml 3.08.3
      
      P.S. The RPMs of the new OCaml are available at
      http://rpm.nogin.org/ocaml.html
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-18 18:43:35 -0800 (Fri, 18 Mar 2005)
Revision: 6977
Log message:

      Some display form improvements.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-18 21:34:42 -0800 (Fri, 18 Mar 2005)
Revision: 6980
Log message:

      Added hash codes to most of the data values in Lm_parser.
      This gives a 20-30% speedup.  I'll work on the propagate-fixpoint next.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-19 12:26:33 -0800 (Sat, 19 Mar 2005)
Revision: 6981
Log message:

      Modified the lookahead propagation for performance (it is now
      faster by about 10x).  The main changes are a more explicit data
      representation, and computing a fixpoint *within* a state
      before moving on to the next one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-19 15:12:12 -0800 (Sat, 19 Mar 2005)
Revision: 6982
Log message:

      In Ocamldep:
      - Split the list of PRL dependencies into a list of implementation-only
        dependencies and a list of dependencies for both implementations and
        interfaces.
      - Added Ml_term to the list of implementation dependencies.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-19 17:18:37 -0800 (Sat, 19 Mar 2005)
Revision: 6983
Log message:

      Added more timing printouts.  Use MP_DEBUG=parsetiming to see them.
      
      Removed normal productions, so we just use production items
      (the production with a . position).  A normal production is
      just a production with the . at the front.
      

Changes by: ( at unknown.email)
Date: 2005-03-19 17:18:37 -0800 (Sat, 19 Mar 2005)
Revision: 6984
Log message:

      This commit was manufactured by cvs2svn to create branch 'fast_parser'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-20 19:03:11 -0800 (Sun, 20 Mar 2005)
Revision: 6985
Log message:

      Term_order:
      - Changed to make sure it is able to handle sequents.
      - Tried making it a bit more efficient.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-20 20:27:09 -0800 (Sun, 20 Mar 2005)
Revision: 6986
Log message:

      Added rules for writing parsed .ml/.mli into .p4/.p4i in macropp-processed
      directories (mllib and refiner).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-20 20:27:23 -0800 (Sun, 20 Mar 2005)
Revision: 6987
Log message:

      Minor API change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-20 21:30:24 -0800 (Sun, 20 Mar 2005)
Revision: 6988
Log message:

      Proper usage of delayed bindings.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-21 11:02:27 -0800 (Mon, 21 Mar 2005)
Revision: 6989
Log message:

      Some additional optimizations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-21 12:48:53 -0800 (Mon, 21 Mar 2005)
Revision: 6990
Log message:

      Grammar construction is now around 0.3sec for our largest grammar,
      which may be good enough.
      
      However, I haven't reconstructed the full shift table, so we'll see.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-21 17:14:32 -0800 (Mon, 21 Mar 2005)
Revision: 6992
Log message:

      Finished proofs in Itt_reflection_example_lambda.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-21 17:16:15 -0800 (Mon, 21 Mar 2005)
Revision: 6993
Log message:

      Remove some useless stuff.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-21 20:40:59 -0800 (Mon, 21 Mar 2005)
Revision: 6994
Log message:

      - Iforms now do not have to be duplicated in .mli and .ml - iforms that exist
        in .mli, but not in .ml will now be automatically copied to .ml.
      
      - No ML code is generated for iforms now; since filter_grammar handles
        iforms internally, there is no need for explicit ML code.
      
      - The .cmoz/.cmiz data structure for iforms now contains neither proofs nor
        resources (note - MetaPRL should still be able to read older binaries).
      
      - Removed references to arguments and conditions from the code for iforms,
        since iforms can not be conditional and can not take arguments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-21 21:17:03 -0800 (Mon, 21 Mar 2005)
Revision: 6995
Log message:

      - Filter_parse: wrapped a number of grammar-related entries with a proper
        handle_exn in order to make sure any error message would point to the
        correct location in the .ml[i] file, as opposed to "line 0, characters 0-1"
      
      - Lm_lexer: prefixed all the Failure error messages with "Lm_lexer: "
      
      Together these changes replace a _very_ confusing:
      
      > File "m_ast.mli", line 0, characters 0-1:
      > Failure: character sequence is not terminated
      
      with a much more self-explanatory:
      
      > While processing lex_token:
      >    Line 183, characters 1-34:
      >       Failure:
      >           Lm_lexer: regex: character sequence is not terminated
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-22 06:36:10 -0800 (Tue, 22 Mar 2005)
Revision: 6996
Log message:

      Removing Phobos from MetaPRL (sorry, Adam). Jason;s new grammar implementation
      is working very well and is much better integrated with MetaPRL. I've also
      converted the "M" grammar in theories/experimental/compile from Phobos to new
      style, this was fairly painless.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-22 08:01:51 -0800 (Tue, 22 Mar 2005)
Revision: 6997
Log message:

      Partially resurrected the "M" compiler. The ext_fib_prog2 (Fibonachi example
      written in "m" syntax) compiles, runs, and produces a correct answer.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-22 13:12:11 -0800 (Tue, 22 Mar 2005)
Revision: 7001
Log message:

      *Important*: when using xbinder{!v} hack, you do have to faithfully consider
      "v" to be a binding.  In particular, this means that _all_ SO variables may
      need to take the !v as an argument - even when you are not intending to
      substitute anything for it!
      
      Note: the "no-op" substitutions would notmally be dropped, so ther do not cost
      much. On the other hand, an occurs check could be a bit expensive (aspecially
      for a long context), so from the preformance POV it does not hurt to include
      [!v] even in contexts that would not normally contain it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-22 14:48:56 -0800 (Tue, 22 Mar 2005)
Revision: 7002
Log message:

      Parse the Filter_grammar quotations correctly on the command line (the code
      that we used to have would bypass iforms and term_of_parsed_term).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-22 15:21:08 -0800 (Tue, 22 Mar 2005)
Revision: 7003
Log message:

      Fixed lookahead propagation, and added empty productions.
      The grammars in mmc now parse.  The maximum compile time has increased
      from 0.3 sec to 0.45, but I have a few minor optimizations left.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-22 19:56:51 -0800 (Tue, 22 Mar 2005)
Revision: 7009
Log message:

      Almost done, we had a power outage here.
      Some more optimizations on the propagation network.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-23 09:35:46 -0800 (Wed, 23 Mar 2005)
Revision: 7011
Log message:

      Additional MAGIC annotations for the stuff that is marshaled.
      Preparing to merge.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-23 09:46:13 -0800 (Wed, 23 Mar 2005)
Revision: 7013
Log message:

      Merged the fast_parser branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-23 15:42:28 -0800 (Wed, 23 Mar 2005)
Revision: 7020
Log message:

      Allow arbitrary non-comma terms as token _subtypes_ in term declarations.
      
      For example, the following is now legal syntax:
      
      declare sequent [Sweep[code:SweepState, kind:SweepKind{'a}]{'op : SweepOperator}] { Ignore : Prop >- 'a } : 'a
      
      where previously it would drop the "{'a}" part and insist on "kind" having
      non-existing type SweepKind{} instead of SweepKind{'a}.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-23 15:46:51 -0800 (Wed, 23 Mar 2005)
Revision: 7021
Log message:

      More proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-23 22:00:17 -0800 (Wed, 23 Mar 2005)
Revision: 7024
Log message:

      When debug_grammar is set, apply_iforms would print the term before and after
      iform applications.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-24 04:40:17 -0800 (Thu, 24 Mar 2005)
Revision: 7026
Log message:

      Minor API change: give access to the hyp index in the SeqHyp.fold function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-24 08:47:36 -0800 (Thu, 24 Mar 2005)
Revision: 7033
Log message:

      Fixing a nasty bug in Term_ds - substitution for "v" in
            sequent{...; v: t[v]; ... >- ...}
      left t[v] unchnaged!
      
      This fixes the misterious closeT bug...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-24 09:20:10 -0800 (Thu, 24 Mar 2005)
Revision: 7035
Log message:

      Implemented sweep and code generation for the Booleans.
      mmc_int_test/test_fact1 compiles and runs, but it
      produces the square of the factorial.  Interesting.
      
      I actually started this commit last night, but it aborted
      after I went to sleep, because of the white-space issue,
      and then I think Aleksey committed similar work:(
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-24 11:38:58 -0800 (Thu, 24 Mar 2005)
Revision: 7038
Log message:

      Mmc_ext_integer duplicated the sweep rules in Mmc_ext_arithmetic.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-24 20:43:40 -0800 (Thu, 24 Mar 2005)
Revision: 7044
Log message:

      Now it compiles (it was broken for some type)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-25 13:08:48 -0800 (Fri, 25 Mar 2005)
Revision: 7046
Log message:

      Normal spilling is pretty much working, although I have to figure out
      a type error after register allocation.  I need to head in for Cristian's
      journal club.
      
      This does not include spilling of parameters, just intra-procedural
      spilling.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-26 14:00:31 -0800 (Sat, 26 Mar 2005)
Revision: 7051
Log message:

      Indeed, Lm_symbol.to_string is the right solution to the
      standardize problem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-26 15:49:54 -0800 (Sat, 26 Mar 2005)
Revision: 7052
Log message:

      
      
      In Filter_patt, interpret the variable "_" as representing
      a wildcard pattern.
      
      Starting work on spill assignment.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-26 17:09:28 -0800 (Sat, 26 Mar 2005)
Revision: 7053
Log message:

      Oops, the _ variable gets turned into an empty variable.  I'm not sure
      if we should fix Lm_symbol, but in any case, I've updated Filter_patt
      to consider "" to denote a wildcard pattern.
      
      Also, when we use simple wildcards, the syntax become unreadable
      (at least to me).  OCaml plans to treat variables that begin with an
      underscore as real variables, but with special meaning wrt dead code.
      In fact, it may already do this.
      
      To handle these issues, Filter_patt now considers the following veriables
      to denote wildcards:
         1. the empty string,
         2. a single underscore,
         3. a double underscore followed by anything.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2005-03-27 20:14:28 -0800 (Sun, 27 Mar 2005)
Revision: 7059
Log message:

      Case analysis typing rule and reductions are ready.
      We don't have generic versions of them, instead instances are generated
      for each inductive type.
      For now, we don't write them anywhere - they are just printed (as terms).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-27 20:25:22 -0800 (Sun, 27 Mar 2005)
Revision: 7060
Log message:

      Doing fixpoint rules via instances seems impossible;
      Generic fixpoint typing rule is way to complex (and reportedly
      the main source of bugs in Coq).
      So we stopped doing case+fixpoint instead we started to implement
      ITT-style induction operations (like list_ind) - in CIC they
      are called elimination rules.
      Coq community do not like them because they are not as natural to use
      as case+fixpoint but they are present in Coq.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-27 20:46:23 -0800 (Sun, 27 Mar 2005)
Revision: 7061
Log message:

      Forgot "extends Cic_ind_elim"
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-27 20:55:26 -0800 (Sun, 27 Mar 2005)
Revision: 7062
Log message:

      Preliminary research on making omegaT complete for universal fragment
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-29 12:27:33 -0800 (Tue, 29 Mar 2005)
Revision: 7067
Log message:

      Sorry for slipping debug messages into my previous commit.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-30 17:28:43 -0800 (Wed, 30 Mar 2005)
Revision: 7069
Log message:

      Added some rules.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-03-30 23:20:27 -0800 (Wed, 30 Mar 2005)
Revision: 7072
Log message:

      Updated proofs.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2005-03-31 19:13:21 -0800 (Thu, 31 Mar 2005)
Revision: 7075
Log message:

      replaced $0 with '$0' to treat folders with spaces correctly.
      Works under cygwin, I hope it also works under Linux
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-03-31 19:26:46 -0800 (Thu, 31 Mar 2005)
Revision: 7076
Log message:

      Exposed exists_elim in the interface
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2005-03-31 20:59:24 -0800 (Thu, 31 Mar 2005)
Revision: 7077
Log message:

      Typing rule for dependent elimination for mutually inductive definitions.
      It compiles but it is not sound yet.