Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-05 17:36:06 -0800 (Wed, 05 Feb 2003)
Revision: 4038
Log message:

      Unicode fixes for couple of display forms.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_tsquash.ml
+5 -1 metaprl/theories/tactic/nuprl_font.ml
+1 -0 metaprl/theories/tactic/nuprl_font.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-12 16:09:36 -0800 (Wed, 12 Feb 2003)
Revision: 4075
Log message:

      Added a "funded in part by" statement.
      

Changes  Path
+5 -0 metaprl/doc/htmlman/mp.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-12 16:10:20 -0800 (Wed, 12 Feb 2003)
Revision: 4076
Log message:

      Need an HR.
      

Changes  Path
+1 -0 metaprl/doc/htmlman/mp.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-12 16:24:16 -0800 (Wed, 12 Feb 2003)
Revision: 4077
Log message:

      Supported in part by ONR.
      

Changes  Path
+4 -3 metaprl/doc/htmlman/mp.html
+5 -1 metaprl/doc/latex/theories/all-theories.tex

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-16 21:32:47 -0800 (Sun, 16 Feb 2003)
Revision: 4079
Log message:

      Fixed a bug in a record elimination tactic. Thanks to Xin for noticing this.
      

Changes  Path
+2 -105 metaprl/theories/itt/itt_record.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-17 00:56:18 -0800 (Mon, 17 Feb 2003)
Revision: 4080
Log message:

      Added Phobos (with a few features stripped out) to MetaPRL.
      

Changes  Path
Added metaprl/filter/phobos/Files
Properties metaprl/filter/phobos/Files
Added metaprl/filter/phobos/Makefile
Properties metaprl/filter/phobos/Makefile
Added metaprl/filter/phobos/filter_phobos.ml
Properties metaprl/filter/phobos/filter_phobos.ml
Added metaprl/filter/phobos/filter_phobos.mli
Properties metaprl/filter/phobos/filter_phobos.mli
Added metaprl/filter/phobos/map.ml
Properties metaprl/filter/phobos/map.ml
Added metaprl/filter/phobos/map.mli
Properties metaprl/filter/phobos/map.mli
Added metaprl/filter/phobos/phobos_builtin.ml
Properties metaprl/filter/phobos/phobos_builtin.ml
Added metaprl/filter/phobos/phobos_builtin.mli
Properties metaprl/filter/phobos/phobos_builtin.mli
Added metaprl/filter/phobos/phobos_compile.ml
Properties metaprl/filter/phobos/phobos_compile.ml
Added metaprl/filter/phobos/phobos_compile.mli
Properties metaprl/filter/phobos/phobos_compile.mli
Added metaprl/filter/phobos/phobos_cons.ml
Properties metaprl/filter/phobos/phobos_cons.ml
Added metaprl/filter/phobos/phobos_constants.ml
Properties metaprl/filter/phobos/phobos_constants.ml
Added metaprl/filter/phobos/phobos_constants.mli
Properties metaprl/filter/phobos/phobos_constants.mli
Added metaprl/filter/phobos/phobos_debug.ml
Properties metaprl/filter/phobos/phobos_debug.ml
Added metaprl/filter/phobos/phobos_debug.mli
Properties metaprl/filter/phobos/phobos_debug.mli
Added metaprl/filter/phobos/phobos_exn.ml
Properties metaprl/filter/phobos/phobos_exn.ml
Added metaprl/filter/phobos/phobos_exn.mli
Properties metaprl/filter/phobos/phobos_exn.mli
Added metaprl/filter/phobos/phobos_grammar.ml
Properties metaprl/filter/phobos/phobos_grammar.ml
Added metaprl/filter/phobos/phobos_grammar.mli
Properties metaprl/filter/phobos/phobos_grammar.mli
Added metaprl/filter/phobos/phobos_lexer.ml
Properties metaprl/filter/phobos/phobos_lexer.ml
Added metaprl/filter/phobos/phobos_lexer.mli
Properties metaprl/filter/phobos/phobos_lexer.mli
Added metaprl/filter/phobos/phobos_lexer.mll
Properties metaprl/filter/phobos/phobos_lexer.mll
Added metaprl/filter/phobos/phobos_main.ml
Properties metaprl/filter/phobos/phobos_main.ml
Added metaprl/filter/phobos/phobos_main.mli
Properties metaprl/filter/phobos/phobos_main.mli
Added metaprl/filter/phobos/phobos_marshal.ml
Properties metaprl/filter/phobos/phobos_marshal.ml
Added metaprl/filter/phobos/phobos_marshal.mli
Properties metaprl/filter/phobos/phobos_marshal.mli
Added metaprl/filter/phobos/phobos_parse_state.ml
Properties metaprl/filter/phobos/phobos_parse_state.ml
Added metaprl/filter/phobos/phobos_parse_state.mli
Properties metaprl/filter/phobos/phobos_parse_state.mli
Added metaprl/filter/phobos/phobos_parser.ml
Properties metaprl/filter/phobos/phobos_parser.ml
Added metaprl/filter/phobos/phobos_parser.mli
Properties metaprl/filter/phobos/phobos_parser.mli
Added metaprl/filter/phobos/phobos_parser.mly
Properties metaprl/filter/phobos/phobos_parser.mly
Added metaprl/filter/phobos/phobos_parser_internals.ml
Properties metaprl/filter/phobos/phobos_parser_internals.ml
Added metaprl/filter/phobos/phobos_parser_internals.mli
Properties metaprl/filter/phobos/phobos_parser_internals.mli
Added metaprl/filter/phobos/phobos_print.ml
Properties metaprl/filter/phobos/phobos_print.ml
Added metaprl/filter/phobos/phobos_print.mli
Properties metaprl/filter/phobos/phobos_print.mli
Added metaprl/filter/phobos/phobos_report.ml
Properties metaprl/filter/phobos/phobos_report.ml
Added metaprl/filter/phobos/phobos_report.mli
Properties metaprl/filter/phobos/phobos_report.mli
Added metaprl/filter/phobos/phobos_rewrite.ml
Properties metaprl/filter/phobos/phobos_rewrite.ml
Added metaprl/filter/phobos/phobos_rewrite.mli
Properties metaprl/filter/phobos/phobos_rewrite.mli
Added metaprl/filter/phobos/phobos_state.ml
Properties metaprl/filter/phobos/phobos_state.ml
Added metaprl/filter/phobos/phobos_state.mli
Properties metaprl/filter/phobos/phobos_state.mli
Added metaprl/filter/phobos/phobos_token_inheritance.ml
Properties metaprl/filter/phobos/phobos_token_inheritance.ml
Added metaprl/filter/phobos/phobos_token_inheritance.mli
Properties metaprl/filter/phobos/phobos_token_inheritance.mli
Added metaprl/filter/phobos/phobos_tokenizer.ml
Properties metaprl/filter/phobos/phobos_tokenizer.ml
Added metaprl/filter/phobos/phobos_tokenizer.mli
Properties metaprl/filter/phobos/phobos_tokenizer.mli
Added metaprl/filter/phobos/phobos_type.ml
Properties metaprl/filter/phobos/phobos_type.ml
Added metaprl/filter/phobos/phobos_type.mli
Properties metaprl/filter/phobos/phobos_type.mli
Added metaprl/filter/phobos/phobos_util.ml
Properties metaprl/filter/phobos/phobos_util.ml
Added metaprl/filter/phobos/phobos_util.mli
Properties metaprl/filter/phobos/phobos_util.mli
Added metaprl/filter/phobos/set.ml
Properties metaprl/filter/phobos/set.ml
Added metaprl/filter/phobos/set.mli
Properties metaprl/filter/phobos/set.mli
Added metaprl/filter/phobos/smap.ml
Properties metaprl/filter/phobos/smap.ml
Added metaprl/filter/phobos/smap.mli
Properties metaprl/filter/phobos/smap.mli
Added metaprl/filter/phobos/xstr_search.ml
Properties metaprl/filter/phobos/xstr_search.ml
Added metaprl/filter/phobos/xstr_search.mli
Properties metaprl/filter/phobos/xstr_search.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-17 00:57:26 -0800 (Mon, 17 Feb 2003)
Revision: 4081
Log message:

      Include Phobos in Makefiles.
      

Changes  Path
+4 -3 metaprl/filter/Makefile
+1 -1 metaprl/filter/filter/Makefile

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-17 00:59:38 -0800 (Mon, 17 Feb 2003)
Revision: 4082
Log message:

      Added Phobos grammar for M_ir.
      For now, I also added the compiled list module.
      

Changes  Path
Properties metaprl/theories/experimental/compile
Added metaprl/theories/experimental/compile/list.cph
Properties metaprl/theories/experimental/compile/list.cph
+3 -0 metaprl/theories/experimental/compile/m_ir.ml
Added metaprl/theories/experimental/compile/m_ir.pho
Properties metaprl/theories/experimental/compile/m_ir.pho

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-18 14:44:28 -0800 (Tue, 18 Feb 2003)
Revision: 4083
Log message:

      Added M AST. Next is putting back the ability in Phobos to apply
      relaxed rewrites (post-parsing) since these were taken out with
      the initial integration, and commiting the MetaPRL term
      definitions and display forms for M AST.
      The current AST is different from the IR in only that
      functions are defined/called with a list of params/args.
      I have to think about whether we can do currying in MetaPRL, or
      have to resort to Phobos and its relaxed rewrites (when I put them
      back).
      For now, the ext: quotation uses m_ir.pho, but I will commit a quick
      fix to allow the changing of the grammar as one compiles MetaPRL.
      

Changes  Path
Added metaprl/theories/experimental/compile/m_ast.pho
Properties metaprl/theories/experimental/compile/m_ast.pho

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-18 14:47:25 -0800 (Tue, 18 Feb 2003)
Revision: 4084
Log message:

      Now you can use the environment variable LANG_FILE to set the name
      of the grammar file to be used in the ext: quotation.
      You can also set DEBUG_PHOBOS to see the parsing process, although
      I don't see why anyone would be interested in seeing that. To
      disable it, set it to "off".
      

Changes  Path
+19 -1 metaprl/filter/phobos/filter_phobos.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:27:04 -0800 (Wed, 19 Feb 2003)
Revision: 4086
Log message:

      Added new rule for the term symbol that calls Phobos on a string.
      This was approach II, as we discussed earlier.
      Here is an example:
      
      sequent [m] { 'H >- $"let t = 1 in let u = 2 in t+u"$ }
      
      The default language is "m_ir.pho", assumed to be in the current
      directory. You can also control the default language through
      the LANG_FILE environment variable.
      
      As before, there remains an ext: quotation that can be used in
      Ocaml expressions and patterns, such as
      
      let t = <:ext<let t = 1 in let u = 2 in t+u>> in ...
      

Changes  Path
+12 -1 metaprl/filter/filter/filter_parse.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:29:01 -0800 (Wed, 19 Feb 2003)
Revision: 4087
Log message:

      Switched over to Mp_debug. I am still not convinced that MP_DEBUG
      is read from the environment, though.
      

Changes  Path
+2 -12 metaprl/filter/phobos/filter_phobos.ml
+24 -14 metaprl/filter/phobos/phobos_debug.ml
+1 -0 metaprl/filter/phobos/phobos_debug.mli
+2 -2 metaprl/filter/phobos/phobos_grammar.ml
+19 -18 metaprl/filter/phobos/phobos_main.ml
+182 -183 metaprl/filter/phobos/phobos_parser.ml
+5 -6 metaprl/filter/phobos/phobos_parser.mly
+0 -1 metaprl/filter/phobos/phobos_state.ml
+0 -2 metaprl/filter/phobos/phobos_state.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:30:10 -0800 (Wed, 19 Feb 2003)
Revision: 4088
Log message:

      We should clear up Phobos-generated files on clean-up.
      

Changes  Path
+1 -1 metaprl/theories/experimental/compile/Makefile

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:37:45 -0800 (Wed, 19 Feb 2003)
Revision: 4089
Log message:

      Switched hardcoded term with the new Phobos-enabled term notation.
      Fancy way of saying putting things to the test.
      

Changes  Path
+12 -10 metaprl/theories/experimental/compile/m_ir.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:38:56 -0800 (Wed, 19 Feb 2003)
Revision: 4090
Log message:

      Changed comment to say M IR and not AST (which was added earlier).
      

Changes  Path
+1 -2 metaprl/theories/experimental/compile/m_ir.pho

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 02:55:43 -0800 (Wed, 19 Feb 2003)
Revision: 4091
Log message:

      Cleaned up m_ir.pho:
      -eliminated dependence on list.cph (which was getting cleared out
      in make clean anyways)
      -no need to include Phobos-related modules (it is a clean module...)
      -function calls take only one argument
      -got rid of enclosing "syntax" term.
      

Changes  Path
+4 -10 metaprl/theories/experimental/compile/m_ir.pho

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 12:37:34 -0800 (Wed, 19 Feb 2003)
Revision: 4092
Log message:

      This should finish off quotations... I have enabled term/ext quotations
      in terms, so now you can write
      
      sequent [m] { 'H >- <<AtomInt[1:n]>> }
      sequent [m] { 'H >- <:term<....>> }
      sequent [m] { 'H >- <:ext<let t = 1 in let u = 2 in u*t>> }
      
      and of course you can still use
      
      sequent [m] { 'H >- $"let t = 1 in let u = 2 in u*t"$ }
      
      The key part that we were missing was the fact that there is a token
      type QUOTATION.
      

Changes  Path
+24 -5 metaprl/filter/filter/filter_parse.ml
+0 -4 metaprl/filter/phobos/filter_phobos.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 17:17:55 -0800 (Wed, 19 Feb 2003)
Revision: 4093
Log message:

      Phobos error messages should be caught by the Phobos exnhdlr.
      Also, the list of tokens was not destroyed between different calls
      to Phobos, resulting in the same term returned from each (since
      parsing stopped at the first syntactically correct term - this
      can be fixed in the local copy of m_ir/m_ast.pho).
      

Changes  Path
+2 -3 metaprl/filter/filter/filter_parse.ml
+2 -0 metaprl/filter/phobos/phobos_tokenizer.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-19 17:18:32 -0800 (Wed, 19 Feb 2003)
Revision: 4094
Log message:

      Added .cvsignore.
      

Changes  Path
Properties metaprl/filter/phobos

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-19 19:43:23 -0800 (Wed, 19 Feb 2003)
Revision: 4095
Log message:

      Please remember this:
      
      *** All ML files in an application have to have different names ***
      
      Please, do not add files to MetaPRL named set.ml for instance.  It is
      not possible to compile MetaPRL if you do so.
      

Changes  Path
+2 -2 metaprl/filter/phobos/Files
Deleted metaprl/filter/phobos/map.ml
Deleted metaprl/filter/phobos/map.mli
Added metaprl/filter/phobos/mc_map.ml
Properties metaprl/filter/phobos/mc_map.ml
Added metaprl/filter/phobos/mc_map.mli
Properties metaprl/filter/phobos/mc_map.mli
Added metaprl/filter/phobos/mc_set.ml
Properties metaprl/filter/phobos/mc_set.ml
Added metaprl/filter/phobos/mc_set.mli
Properties metaprl/filter/phobos/mc_set.mli
+0 -0 metaprl/filter/phobos/phobos_lexer.ml
+16 -16 metaprl/filter/phobos/phobos_type.ml
+16 -16 metaprl/filter/phobos/phobos_type.mli
Deleted metaprl/filter/phobos/set.ml
Deleted metaprl/filter/phobos/set.mli
+12 -12 metaprl/filter/phobos/smap.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-19 19:51:42 -0800 (Wed, 19 Feb 2003)
Revision: 4096
Log message:

      Adam, please do not commit files that do not compile.
      If you want to do so, please go off on a branch.
      It is very annoying to have to fix your files.
      

Changes  Path
+0 -0 metaprl/theories/experimental/compile/Makefile
+7 -12 metaprl/theories/experimental/compile/m_ir.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-19 19:53:39 -0800 (Wed, 19 Feb 2003)
Revision: 4097
Log message:

      Some minor changes to get MetaPRL to compile in Windows/Cygwin.
      
      Also, a minor update to filter_main.ml to force an exit after
      preprocessing.  For some reason prlcomp.ml is linked into camlp4n!
      

Changes  Path
+3 -0 metaprl/clib/termsize.c
+1 -1 metaprl/filter/filter/filter_main.ml
+3 -0 metaprl/mk/rules
+2 -2 metaprl/util/ocamldep.mll

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-19 20:40:38 -0800 (Wed, 19 Feb 2003)
Revision: 4098
Log message:

      The final part of the CYGWIN-related fix:
       - Only compile prlcomp into prlc, but not into camlp*.
      

Changes  Path
+7 -6 metaprl/filter/Makefile

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-20 18:03:47 -0800 (Thu, 20 Feb 2003)
Revision: 4103
Log message:

      We raise an exception if term quotation is used in terms, like
      sequent [m] { 'H >- <<...>> }
      
      Added .cvsignore to filter/phobos, and changed the Makefile
      to clear out all generated files.
      
      Added pairs to m_ast.pho and m_ir.pho, removed list.cph, and
      changed the test program sequent to use the :ext quotation.
      

Changes  Path
+4 -2 metaprl/filter/filter/filter_parse.ml
Properties metaprl/filter/phobos
+4 -4 metaprl/filter/phobos/Makefile
Deleted metaprl/filter/phobos/phobos_lexer.ml
+30 -15 metaprl/filter/phobos/phobos_lexer.mli
Deleted metaprl/theories/experimental/compile/list.cph
+2 -0 metaprl/theories/experimental/compile/m_ast.pho
+13 -7 metaprl/theories/experimental/compile/m_ir.ml
+2 -0 metaprl/theories/experimental/compile/m_ir.pho

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-21 00:29:40 -0800 (Fri, 21 Feb 2003)
Revision: 4104
Log message:

      - Defined group like objects: groupoid, semigroup, and monoid with dependent
        records.
      - Defined groups based on the definitions of group like objects with
        dependent records.
      - Proved all properties in CZF for groups here in ITT.
      
      TODO:
      1. Might simplify the display forms of "*" later.
      2. Might need more research on using constants as field names.
      3. After the rewriter bug is fixed, some proofs might be simplified and the
         elimination rules for groups etc. are unnecessary.
      

Changes  Path
+2 -0 metaprl/theories/itt/Makefile
Added metaprl/theories/itt/itt_group.ml
Properties metaprl/theories/itt/itt_group.ml
Added metaprl/theories/itt/itt_group.mli
Properties metaprl/theories/itt/itt_group.mli
Added metaprl/theories/itt/itt_group.prla
Properties metaprl/theories/itt/itt_group.prla
Added metaprl/theories/itt/itt_grouplikeobj.ml
Properties metaprl/theories/itt/itt_grouplikeobj.ml
Added metaprl/theories/itt/itt_grouplikeobj.mli
Properties metaprl/theories/itt/itt_grouplikeobj.mli
Added metaprl/theories/itt/itt_grouplikeobj.prla
Properties metaprl/theories/itt/itt_grouplikeobj.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-21 18:07:07 -0800 (Fri, 21 Feb 2003)
Revision: 4107
Log message:

      1. Added the fold form of rewritings.
      2. Added the commutative property and defined commutative semigroup/monoid
         and abelian group.
      

Changes  Path
+23 -3 metaprl/theories/itt/itt_group.ml
+7 -0 metaprl/theories/itt/itt_group.mli
+2270 -1550 metaprl/theories/itt/itt_group.prla
+46 -5 metaprl/theories/itt/itt_grouplikeobj.ml
+21 -1 metaprl/theories/itt/itt_grouplikeobj.mli
+2243 -822 metaprl/theories/itt/itt_grouplikeobj.prla

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-22 09:03:49 -0800 (Sat, 22 Feb 2003)
Revision: 4108
Log message:

      Instead of LetFun, using AtomFun instead.  This will make CPS easier.
      I reverted to the term syntax until Phobos can be updated.
      

Changes  Path
+20 -19 metaprl/theories/experimental/compile/m_ir.ml
+2 -1 metaprl/theories/experimental/compile/m_ir.mli
+1 -1 metaprl/theories/tactic/nuprl_font.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-22 12:57:49 -0800 (Sat, 22 Feb 2003)
Revision: 4109
Log message:

      Fixed m_ast/m_ir to use AtomFuns in function definitions, added
      another testing sequent with the :ext quotation (which you should just
      comment out next time something does not work), and removed the
      debugging line from filter_parse.
      

Changes  Path
+0 -1 metaprl/filter/filter/filter_parse.ml
+3 -3 metaprl/theories/experimental/compile/m_ast.pho
+10 -0 metaprl/theories/experimental/compile/m_ir.ml
+3 -3 metaprl/theories/experimental/compile/m_ir.pho

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-22 17:12:39 -0800 (Sat, 22 Feb 2003)
Revision: 4110
Log message:

      A partial implementation of CPS as discussed to Aleksey.
      However, I am going to scrap this, and formulate it with
      inference rules instead.
      

Changes  Path
+3 -1 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_cps.ml
Properties metaprl/theories/experimental/compile/m_cps.ml
Added metaprl/theories/experimental/compile/m_cps.mli
Properties metaprl/theories/experimental/compile/m_cps.mli
+1 -23 metaprl/theories/experimental/compile/m_ir.ml
Added metaprl/theories/experimental/compile/m_test.ml
Properties metaprl/theories/experimental/compile/m_test.ml
Added metaprl/theories/experimental/compile/m_test.mli
Properties metaprl/theories/experimental/compile/m_test.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-22 19:29:08 -0800 (Sat, 22 Feb 2003)
Revision: 4111
Log message:

      - Added more automation to itt_int_base and itt_int_ext
      (reductions for "a - b + b", "a + b - b", "a - a", "a < a", etc)
      - Simplified the Itt_nat proofs using the new automation
      (most of the proofs are still incomplete since they need an inequality
      tactic).
      

Changes  Path
+7 -7 metaprl/editor/ml/tests/prop-pigeon.ml
+1552 -1250 metaprl/theories/czf/czf_itt_group_power.prla
+8 -1 metaprl/theories/itt/itt_bool.ml
+0 -4 metaprl/theories/itt/itt_bool.mli
+5313 -5280 metaprl/theories/itt/itt_bool.prla
+26 -3 metaprl/theories/itt/itt_int_base.ml
+5 -0 metaprl/theories/itt/itt_int_base.mli
+4425 -3946 metaprl/theories/itt/itt_int_base.prla
+6 -4 metaprl/theories/itt/itt_int_ext.ml
+33 -11 metaprl/theories/itt/itt_nat.ml
+2 -3 metaprl/theories/itt/itt_nat.mli
+2950 -2489 metaprl/theories/itt/itt_nat.prla
+1 -1 metaprl/theories/itt/itt_squiggle.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 10:28:36 -0800 (Sun, 23 Feb 2003)
Revision: 4112
Log message:

      Trying CPS with inference rules.
      

Changes  Path
+37 -35 metaprl/theories/experimental/compile/m_cps.ml
+4 -10 metaprl/theories/experimental/compile/m_cps.mli
+95 -25 metaprl/theories/experimental/compile/m_ir.ml
+6 -0 metaprl/theories/experimental/compile/m_ir.mli
+16 -4 metaprl/theories/experimental/compile/m_test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 17:45:46 -0800 (Sun, 23 Feb 2003)
Revision: 4113
Log message:

      This is an initial attempt at using inference rules for rewriting.
      To make this work, we would either have to:
         1. Add explicit context vars for rewriting
         2. Quantify free variables in a rewrite
      #1 seems the better choice.
      
      In any case, I think I'll go back to trying to use rewrites,
      until we talk about this approach.
      

Changes  Path
+28 -3 metaprl/theories/experimental/compile/m_cps.ml
+1 -0 metaprl/theories/experimental/compile/m_cps.mli
+1 -1 metaprl/theories/experimental/compile/m_test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 19:09:57 -0800 (Sun, 23 Feb 2003)
Revision: 4114
Log message:

      This is a working version of CPS transformation, but I am not sure
      if it is the best approach.
      

Changes  Path
+79 -59 metaprl/theories/experimental/compile/m_cps.ml
+12 -6 metaprl/theories/experimental/compile/m_cps.mli
+26 -10 metaprl/theories/experimental/compile/m_ir.ml
+6 -0 metaprl/theories/experimental/compile/m_ir.mli
+6 -6 metaprl/theories/experimental/compile/m_test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 20:35:43 -0800 (Sun, 23 Feb 2003)
Revision: 4115
Log message:

      ***Notice***
      
      I changed the MetaPRL formatter.  If you have problems with it let me
      know and I will try to fix them.
      
      The objective of this fix was to get indentation working again.
      An unrelated change was to remove specially-coded line formatting,
      since the formatter already has line zones.
      
      On the CPS end, I added the code to convert function applications
      and conditionals.
      

Changes  Path
+183 -230 metaprl/refiner/reflib/rformat.ml
+1 -1 metaprl/refiner/reflib/rformat.mli
+12 -1 metaprl/theories/experimental/compile/m_cps.ml
+40 -8 metaprl/theories/experimental/compile/m_ir.ml
+11 -0 metaprl/theories/experimental/compile/m_ir.mli
+10 -0 metaprl/theories/experimental/compile/m_test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 21:45:01 -0800 (Sun, 23 Feb 2003)
Revision: 4116
Log message:

      Reintroduced Aleksey's column limit.
      

Changes  Path
+1 -1 metaprl/filter/base/filter_cache_fun.ml
+44 -3 metaprl/refiner/reflib/dform.ml
+11 -12 metaprl/refiner/reflib/rformat.ml
+3 -3 metaprl/theories/experimental/compile/m_ir.ml
+15 -15 metaprl/theories/tactic/nuprl_font.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-23 21:46:12 -0800 (Sun, 23 Feb 2003)
Revision: 4117
Log message:

      Oops, left in a debugging comment.
      Also, I added minimal support for boldface in terminal windows.
      

Changes  Path
+0 -1 metaprl/refiner/reflib/dform.ml

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-23 23:36:05 -0800 (Sun, 23 Feb 2003)
Revision: 4118
Log message:

      According to Alexei's comments:
      1. Simplified the representation of {self : {record} | P[self]}
         to {record; P[self]};
      2. Changed the names of "G" and "e" to "car" and "1"; in the the extendend
         syntax for records, removed quotes where labels are constant other than
         "*" and "1".
      3. Removed "group_is_monoid" from the intro resources.
      
      Updated proofs accordingly.
      
      TODO:
      Need to work on improving the syntax and display forms of "*", "inv".
      Alexei will work on the syntax part.
      

Changes  Path
+72 -72 metaprl/theories/itt/itt_group.ml
+4970 -5018 metaprl/theories/itt/itt_group.prla
+12 -12 metaprl/theories/itt/itt_grouplikeobj.ml
+2181 -2176 metaprl/theories/itt/itt_grouplikeobj.prla

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-24 19:18:07 -0800 (Mon, 24 Feb 2003)
Revision: 4119
Log message:

      Added more formatting.
      

Changes  Path
+2 -2 metaprl/theories/experimental/compile/m_cps.ml
+12 -12 metaprl/theories/experimental/compile/m_ir.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-24 19:52:29 -0800 (Mon, 24 Feb 2003)
Revision: 4120
Log message:

      One of the srec rules was missing one of the necessary wf assumptions.
      Alexei, Jason, please double-check.
      

Changes  Path
+1 -0 metaprl/theories/itt/itt_srec.ml
+1 -0 metaprl/theories/itt/itt_srec.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-24 20:26:14 -0800 (Mon, 24 Feb 2003)
Revision: 4121
Log message:

      Added the formatting bounds-check that Aleksey and I have
      talked about.  Ithink I fixed the TeX error; will check that next.
      

Changes  Path
+52 -19 metaprl/refiner/reflib/rformat.ml
+13 -0 metaprl/refiner/reflib/rformat.mli

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-24 21:51:45 -0800 (Mon, 24 Feb 2003)
Revision: 4122
Log message:

      1. Added display forms for the terms.
      2. Separate commutative semigroup/monoid and abelian group from the
         grouplikeobj/group modules.
      
      Any comment on the display forms?
      

Changes  Path
+1 -0 metaprl/theories/itt/Makefile
Added metaprl/theories/itt/itt_abelian_group.ml
Properties metaprl/theories/itt/itt_abelian_group.ml
Added metaprl/theories/itt/itt_abelian_group.mli
Properties metaprl/theories/itt/itt_abelian_group.mli
Added metaprl/theories/itt/itt_abelian_group.prla
Properties metaprl/theories/itt/itt_abelian_group.prla
+111 -0 metaprl/theories/itt/itt_comment.ml
+16 -0 metaprl/theories/itt/itt_comment.mli
+9 -17 metaprl/theories/itt/itt_group.ml
+4 -2 metaprl/theories/itt/itt_group.mli
+1993 -2291 metaprl/theories/itt/itt_group.prla
+17 -38 metaprl/theories/itt/itt_grouplikeobj.ml
+0 -8 metaprl/theories/itt/itt_grouplikeobj.mli
+1789 -2579 metaprl/theories/itt/itt_grouplikeobj.prla

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-24 21:52:56 -0800 (Mon, 24 Feb 2003)
Revision: 4123
Log message:

      Added 3 group files for documentation.
      

Changes  Path
+3 -0 metaprl/doc/latex/theories/itt/print.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 00:00:41 -0800 (Tue, 25 Feb 2003)
Revision: 4124
Log message:

      Two changes:
      
      1. Added the refiner error RewriteStringOpnameOpnameError;
         I was having too much trouble finding out why rewrites
         weren't working.
      
      2. Added the first phase of closure conversion.  This is
         the simpler phase, but it requires an inverse beta-reduction,
         and I was having trouble with it (turns out, I was just being
         dumb).
      

Changes  Path
+1 -1 metaprl/mk/preface
+2 -0 metaprl/refiner/refiner/refine_error.ml
+8 -0 metaprl/refiner/reflib/refine_exn.ml
+2 -0 metaprl/refiner/refsig/refine_error_sig.ml
+7 -2 metaprl/refiner/rewrite/rewrite.ml
Properties metaprl/theories/experimental/compile
+4 -0 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_closure.ml
Properties metaprl/theories/experimental/compile/m_closure.ml
Added metaprl/theories/experimental/compile/m_closure.mli
Properties metaprl/theories/experimental/compile/m_closure.mli
+16 -0 metaprl/theories/experimental/compile/m_ir.ml
+12 -0 metaprl/theories/experimental/compile/m_ir.mli
+1 -1 metaprl/theories/experimental/compile/m_test.ml
Added metaprl/theories/experimental/compile/m_theory.mlz
Properties metaprl/theories/experimental/compile/m_theory.mlz

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 00:19:40 -0800 (Tue, 25 Feb 2003)
Revision: 4125
Log message:

      Completed closure conversion.
      
      If this really works, it is amazing.  Closure conversion in 225 lines,
      and most of those can be eliminated!
      
      BTW, Brian is welcome to look at this; don't worry about lab4.
      

Changes  Path
+36 -0 metaprl/theories/experimental/compile/m_closure.ml
+10 -0 metaprl/theories/experimental/compile/m_closure.mli
+3 -2 metaprl/theories/experimental/compile/m_test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 00:29:24 -0800 (Tue, 25 Feb 2003)
Revision: 4126
Log message:

      Added a compileT tactic that does both CPS and closure conversion.
      

Changes  Path
Properties metaprl/theories/experimental/compile
+0 -2 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_theory.ml
Properties metaprl/theories/experimental/compile/m_theory.ml
Added metaprl/theories/experimental/compile/m_theory.mli
Properties metaprl/theories/experimental/compile/m_theory.mli
Deleted metaprl/theories/experimental/compile/m_theory.mlz

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 11:02:17 -0800 (Tue, 25 Feb 2003)
Revision: 4127
Log message:

      Working on program normalization, but the rewriter is giving me
      a bad match and I'm having trouble tracking it down.
      

Changes  Path
+1 -0 metaprl/refiner/refiner/refine_error.ml
+6 -0 metaprl/refiner/reflib/refine_exn.ml
+1 -0 metaprl/refiner/refsig/refine_error_sig.ml
+2 -2 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -0 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_prog.ml
Properties metaprl/theories/experimental/compile/m_prog.ml
Added metaprl/theories/experimental/compile/m_prog.mli
Properties metaprl/theories/experimental/compile/m_prog.mli
+1 -0 metaprl/theories/experimental/compile/m_theory.ml
+1 -0 metaprl/theories/experimental/compile/m_theory.mli

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-25 14:18:10 -0800 (Tue, 25 Feb 2003)
Revision: 4128
Log message:

      Put back post-parsing rewrites.
      Also, when applying a rewrite, apply it along with the global rewrites.
      With these changes, I will go ahead and remove Phobos from mcc, and
      hopefully all the dynamic front-end stuff will work as before.
      

Changes  Path
+1 -1 metaprl/filter/phobos/Makefile
+9 -5 metaprl/filter/phobos/phobos_compile.ml
+8 -4 metaprl/filter/phobos/phobos_main.ml
Deleted metaprl/filter/phobos/phobos_parser.ml
+27 -4 metaprl/filter/phobos/phobos_rewrite.ml
+6 -8 metaprl/filter/phobos/phobos_rewrite.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 18:59:52 -0800 (Tue, 25 Feb 2003)
Revision: 4129
Log message:

      Perform program hoisting as a sequence of pairwise swaps.
      

Changes  Path
+4 -0 metaprl/theories/experimental/compile/m_cps.ml
+5 -0 metaprl/theories/experimental/compile/m_cps.mli
+133 -35 metaprl/theories/experimental/compile/m_prog.ml
+13 -1 metaprl/theories/experimental/compile/m_prog.mli
+4 -1 metaprl/theories/experimental/compile/m_theory.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 20:02:49 -0800 (Tue, 25 Feb 2003)
Revision: 4130
Log message:

      Modified CPS conversion slightly to enclose the entire program
      in a function.
      

Changes  Path
Deleted metaprl/filter/phobos/phobos_parser.mli
+14 -1 metaprl/theories/experimental/compile/m_cps.ml
+1 -1 metaprl/theories/experimental/compile/m_prog.ml
+11 -11 metaprl/theories/experimental/compile/m_test.ml
+16 -7 metaprl/theories/tactic/base_dform.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 20:13:54 -0800 (Tue, 25 Feb 2003)
Revision: 4131
Log message:

      Moved generic resource code into M_util.
      

Changes  Path
+1 -0 metaprl/theories/experimental/compile/Makefile
+2 -34 metaprl/theories/experimental/compile/m_cps.ml
+0 -1 metaprl/theories/experimental/compile/m_cps.mli
+1 -28 metaprl/theories/experimental/compile/m_prog.ml
+0 -1 metaprl/theories/experimental/compile/m_prog.mli
Added metaprl/theories/experimental/compile/m_util.ml
Properties metaprl/theories/experimental/compile/m_util.ml
Added metaprl/theories/experimental/compile/m_util.mli
Properties metaprl/theories/experimental/compile/m_util.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 20:33:21 -0800 (Tue, 25 Feb 2003)
Revision: 4132
Log message:

      Added dead code elimination.
      

Changes  Path
+1 -0 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_dead.ml
Properties metaprl/theories/experimental/compile/m_dead.ml
Added metaprl/theories/experimental/compile/m_dead.mli
Properties metaprl/theories/experimental/compile/m_dead.mli
+0 -9 metaprl/theories/experimental/compile/m_prog.ml
+4 -0 metaprl/theories/experimental/compile/m_theory.ml
+1 -0 metaprl/theories/experimental/compile/m_theory.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-25 21:00:30 -0800 (Tue, 25 Feb 2003)
Revision: 4133
Log message:

      Added constant folding.
      

Changes  Path
+1 -0 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_inline.ml
Properties metaprl/theories/experimental/compile/m_inline.ml
Added metaprl/theories/experimental/compile/m_inline.mli
Properties metaprl/theories/experimental/compile/m_inline.mli
+1 -1 metaprl/theories/experimental/compile/m_ir.ml
+1 -1 metaprl/theories/experimental/compile/m_ir.mli
+6 -0 metaprl/theories/experimental/compile/m_theory.ml
+1 -0 metaprl/theories/experimental/compile/m_theory.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-26 09:35:33 -0800 (Wed, 26 Feb 2003)
Revision: 4134
Log message:

      Prog hoisting is more complete.
      

Changes  Path
+20 -4 metaprl/theories/experimental/compile/m_prog.ml

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 14:15:01 -0800 (Wed, 26 Feb 2003)
Revision: 4135
Log message:

      Extended grammar:
      
      1. Syntax for binary algebraic operations:
       'a *['g] 'b stands for 'g^"*" 'a 'b
      The same for +,-,/,^ and relations: <,=,>,<=,>=,<>
      
      For binary algebraic operations with self the syntax remains unchanged:
       'a ^* 'b (is the same as 'a *['self] 'b) stands for 'self^"*" 'a 'b
      
      2. Fixed a bug: now field selection (r^l) has higher priority than application.
      So you may write: g^inv 'a instead of (g^inv) 'a
      
      3. Boolean relations for integers <@, =@, >@, <>@, <=@, >=@.
      (That is, a<b is proposition and a<@ b is a boolean).
      
      4. Power for integers: a ^@ b
      
      5. Syntax for field update: 'r^x:='a
      
      6. Wild card (_) is removed.
      

Changes  Path
+162 -100 metaprl/filter/base/term_grammar.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-26 16:00:43 -0800 (Wed, 26 Feb 2003)
Revision: 4137
Log message:

      I am committing this file separately.
      I added another :desc "quotation" (for IR descriptions). Among others,
      this would be useful in rewrite rules, which expect mterms, but ideally
      we shouldn't duplicate code. So if you can figure out a better parse
      symbol to extend (so that you can use this "quotation" in sequents as well),
      feel free to revert this code. I didn't think nonwordterm was the right
      symbol to extend for this.
      

Changes  Path
+35 -1 metaprl/filter/filter/filter_parse.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-26 16:05:41 -0800 (Wed, 26 Feb 2003)
Revision: 4138
Log message:

      Added :desc quotation for IR descriptions. For a sample, see
      the changes in m_closure.ml.
      Also, m_ir.pho now lives in m_ast.pho, and m_ir.pho now parses
      the IR descriptions. Consequently, the :ext quotation uses
      m_ast.pho, and the :desc quotation used m_ir.pho.
      I will now be working on the M AST.
      

Changes  Path
+17 -0 metaprl/filter/phobos/filter_phobos.ml
+2 -1 metaprl/filter/phobos/phobos_state.ml
+1 -0 metaprl/filter/phobos/phobos_state.mli
+13 -18 metaprl/theories/experimental/compile/m_ast.pho
+14 -0 metaprl/theories/experimental/compile/m_closure.ml
+46 -18 metaprl/theories/experimental/compile/m_ir.pho

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 18:28:47 -0800 (Wed, 26 Feb 2003)
Revision: 4139
Log message:

      I extend syntax with the following expressions:
      
          'A subtype 'B
          'A subset 'B
          'x in 'A subset 'B
      
          x:A isect B[x]
          A bunion B
          Union x:A. B[x]
          Isect x:A. B[x]
      
      (All changes are reflected in doc/htmlman/user-guide/mp-terms.html).
      
      Now words subtype, subset, isect, bunion, Union and Isect are keywords.
      
      So you can't write just subtype{'A;'B}.
      You should write
      
      'A subtype 'B
      or
      "subtype"{'A;'B}
      or
      \subtype{'A ;'B}
      
      I hope this will not create problems.
      If it annoys someone, let me know.
      

Changes  Path
+75 -17 metaprl/doc/htmlman/user-guide/mp-terms.html
+25 -5 metaprl/filter/base/term_grammar.ml
+2 -2 metaprl/theories/czf/czf_itt_comment.ml
+2 -2 metaprl/theories/czf/czf_itt_coset.ml
+2 -2 metaprl/theories/czf/czf_itt_group_bvd.ml
+1 -1 metaprl/theories/czf/czf_itt_group_bvd.mli
+2 -2 metaprl/theories/czf/czf_itt_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_subgroup.mli
+18 -18 metaprl/theories/czf/czf_itt_subset.ml
+2 -2 metaprl/theories/czf/czf_itt_subset.mli
+1 -1 metaprl/theories/czf/czf_itt_subset.prla
+17 -17 metaprl/theories/fir/mfir_int_set.ml
+1 -1 metaprl/theories/fir/mfir_int_set.mli
+2 -2 metaprl/theories/fir/mfir_termOp.ml
+8 -6 metaprl/theories/fir/mfir_test.ml
+2 -2 metaprl/theories/fir/mfir_tr_types.ml
+8 -8 metaprl/theories/itt/ctt_markov.ml
+3 -3 metaprl/theories/itt/itt_antiquotient.ml
+3 -3 metaprl/theories/itt/itt_atom_bool.ml
+22 -22 metaprl/theories/itt/itt_bisect.ml
+1 -1 metaprl/theories/itt/itt_bisect.mli
+29 -29 metaprl/theories/itt/itt_bool.ml
+4 -4 metaprl/theories/itt/itt_bool.mli
+14 -14 metaprl/theories/itt/itt_bunion.ml
+1 -1 metaprl/theories/itt/itt_bunion.mli
+109 -109 metaprl/theories/itt/itt_collection.ml
+4 -4 metaprl/theories/itt/itt_derive.ml
+11 -11 metaprl/theories/itt/itt_dfun.ml
+11 -11 metaprl/theories/itt/itt_dfun.mli
+3 -3 metaprl/theories/itt/itt_dfun.prla
+34 -34 metaprl/theories/itt/itt_disect.ml
+4 -4 metaprl/theories/itt/itt_disect.mli
+9 -9 metaprl/theories/itt/itt_disect.prla
+5 -5 metaprl/theories/itt/itt_dprod.ml
+5 -5 metaprl/theories/itt/itt_dprod.mli
+10 -10 metaprl/theories/itt/itt_dprod_imp.ml
+11 -11 metaprl/theories/itt/itt_equal.ml
+8 -8 metaprl/theories/itt/itt_equal.mli
+7 -7 metaprl/theories/itt/itt_esquash.ml
+1 -1 metaprl/theories/itt/itt_eta.ml
+1 -1 metaprl/theories/itt/itt_eta.mli
+28 -28 metaprl/theories/itt/itt_example.ml
+4 -4 metaprl/theories/itt/itt_ext_equal.ml
+3 -3 metaprl/theories/itt/itt_ext_equal.mli
+172 -172 metaprl/theories/itt/itt_fset.ml
+4 -4 metaprl/theories/itt/itt_fun.ml
+4 -4 metaprl/theories/itt/itt_fun.mli
+39 -39 metaprl/theories/itt/itt_int_arith.ml
+2 -2 metaprl/theories/itt/itt_int_arith.mli
+92 -92 metaprl/theories/itt/itt_int_base.ml
+52 -52 metaprl/theories/itt/itt_int_base.mli
+96 -96 metaprl/theories/itt/itt_int_ext.ml
+53 -53 metaprl/theories/itt/itt_int_ext.mli
+3 -3 metaprl/theories/itt/itt_inv_typing.ml
+40 -40 metaprl/theories/itt/itt_isect.ml
+12 -12 metaprl/theories/itt/itt_isect.mli
+3 -3 metaprl/theories/itt/itt_list.ml
+3 -3 metaprl/theories/itt/itt_list.mli
+1 -1 metaprl/theories/itt/itt_list.prla
+79 -79 metaprl/theories/itt/itt_list2.ml
+1 -1 metaprl/theories/itt/itt_list2.mli
+5 -5 metaprl/theories/itt/itt_logic.ml
+3 -3 metaprl/theories/itt/itt_nat.ml
+1 -1 metaprl/theories/itt/itt_pointwise2.ml
+3 -3 metaprl/theories/itt/itt_prec.ml
+3 -3 metaprl/theories/itt/itt_prec.mli
+3 -3 metaprl/theories/itt/itt_prod.ml
+3 -3 metaprl/theories/itt/itt_prod.mli
+4 -4 metaprl/theories/itt/itt_quotient.ml
+4 -4 metaprl/theories/itt/itt_quotient.mli
+14 -14 metaprl/theories/itt/itt_record.ml
+2 -2 metaprl/theories/itt/itt_record.mli
+2 -2 metaprl/theories/itt/itt_record.prla
+29 -29 metaprl/theories/itt/itt_record0.ml
+23 -23 metaprl/theories/itt/itt_record_exm.ml
+1 -1 metaprl/theories/itt/itt_record_label.ml
+5 -5 metaprl/theories/itt/itt_record_label0.ml
+2 -2 metaprl/theories/itt/itt_record_label0.mli
+11 -11 metaprl/theories/itt/itt_rfun.ml
+1 -1 metaprl/theories/itt/itt_rfun.mli
+2 -2 metaprl/theories/itt/itt_rfun.prla
+1 -1 metaprl/theories/itt/itt_set.ml
+1 -1 metaprl/theories/itt/itt_set.mli
+49 -49 metaprl/theories/itt/itt_sort.ml
+6 -6 metaprl/theories/itt/itt_squash.ml
+2 -2 metaprl/theories/itt/itt_squash.mli
+1 -1 metaprl/theories/itt/itt_squiggle.ml
+4 -4 metaprl/theories/itt/itt_srec.ml
+3 -3 metaprl/theories/itt/itt_srec.mli
+1 -1 metaprl/theories/itt/itt_struct.ml
+1 -1 metaprl/theories/itt/itt_struct.mli
+2 -2 metaprl/theories/itt/itt_struct2.ml
+4 -4 metaprl/theories/itt/itt_struct3.ml
+4 -4 metaprl/theories/itt/itt_struct3.mli
+24 -24 metaprl/theories/itt/itt_subtype.ml
+17 -17 metaprl/theories/itt/itt_subtype.mli
+1 -1 metaprl/theories/itt/itt_subtype.prla
+4 -4 metaprl/theories/itt/itt_tunion.ml
+2 -2 metaprl/theories/itt/itt_tunion.mli
+5 -5 metaprl/theories/itt/itt_union.ml
+4 -4 metaprl/theories/itt/itt_union.mli
+2 -2 metaprl/theories/itt/itt_unit.ml
+2 -2 metaprl/theories/itt/itt_unit.mli
+2 -2 metaprl/theories/itt/itt_void.ml
+2 -2 metaprl/theories/itt/itt_void.mli
+2 -2 metaprl/theories/itt/itt_well_founded.ml
+4 -4 metaprl/theories/itt/jprover_tests.ml
+1 -1 metaprl/theories/tactic/comment.ml
+4 -4 metaprl/theories/tactic/nuprl_font.ml
+1 -1 metaprl/theories/tactic/nuprl_font.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-02-26 21:43:45 -0800 (Wed, 26 Feb 2003)
Revision: 4141
Log message:

      Added initial assembly code.
      Will have to talk about how we handle tailcalls, and closures.
      It will take some work.
      
      Adam, phobos goes into an infinite loop on m_closure.ml.
      Can you check it out?
      

Changes  Path
+2 -0 metaprl/theories/experimental/compile/Makefile
+3 -0 metaprl/theories/experimental/compile/m_closure.ml
+2 -0 metaprl/theories/experimental/compile/m_theory.ml
+2 -0 metaprl/theories/experimental/compile/m_theory.mli
Added metaprl/theories/experimental/compile/m_x86.ml
Properties metaprl/theories/experimental/compile/m_x86.ml
Added metaprl/theories/experimental/compile/m_x86.mli
Properties metaprl/theories/experimental/compile/m_x86.mli
Added metaprl/theories/experimental/compile/x86_asm.ml
Properties metaprl/theories/experimental/compile/x86_asm.ml
Added metaprl/theories/experimental/compile/x86_asm.mli
Properties metaprl/theories/experimental/compile/x86_asm.mli

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 22:35:15 -0800 (Wed, 26 Feb 2003)
Revision: 4142
Log message:

      Fixed proofs that were broken by my last commit.
      

Changes  Path
+2 -2 metaprl/filter/base/term_grammar.ml
+1 -1 metaprl/theories/czf/czf_itt_subset.prla
+3 -3 metaprl/theories/itt/itt_dfun.prla
+3 -3 metaprl/theories/itt/itt_isect.prla
+1 -1 metaprl/theories/itt/itt_list.prla
+0 -0 metaprl/theories/itt/itt_rfun.ml
+2 -2 metaprl/theories/itt/itt_rfun.prla
+2 -2 metaprl/theories/itt/itt_subtype.ml
+2 -2 metaprl/theories/itt/itt_subtype.mli
+1 -1 metaprl/theories/itt/itt_subtype.prla

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-02-26 22:43:50 -0800 (Wed, 26 Feb 2003)
Revision: 4143
Log message:

      Use new syntax in some czf theories.
      

Changes  Path
+14 -14 metaprl/theories/czf/czf_itt_eq.ml
+11 -11 metaprl/theories/czf/czf_itt_subset.ml

Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-27 01:40:58 -0800 (Thu, 27 Feb 2003)
Revision: 4145
Log message:

      Added M source language definition. It is a superset of the M IR,
      the only extension is our own tuple terms which are used to encode
      function arguments.
      The parser takes care of currying function definitions and properly
      declares all mutually recursive functions before their definition.
      These are implemented with relaxed rewrites.
      Then in m_post_parsing, we curry function calls by partially applying
      them one by one, storing the result of each partial function
      application in a temporary variable.
      There is one step missing, which is identifying function variables
      in the program term. This should be easy enough:
      
      FunDecl{f. 'e[AtomVar{'f}]} <--> FunDecl{f. 'e[AtomFunVar{'f}]}
      
      but a straight rewrite rule just does not cut it. So this remains
      to be done.
      I put a test program in m_test, but the old stuff should work as
      before. The post-processing tactic is called ppT.
      

Changes  Path
+2 -0 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_ast.ml
Properties metaprl/theories/experimental/compile/m_ast.ml
Added metaprl/theories/experimental/compile/m_ast.mli
Properties metaprl/theories/experimental/compile/m_ast.mli
+57 -18 metaprl/theories/experimental/compile/m_ast.pho
+0 -3 metaprl/theories/experimental/compile/m_closure.ml
Added metaprl/theories/experimental/compile/m_post_parsing.ml
Properties metaprl/theories/experimental/compile/m_post_parsing.ml
Added metaprl/theories/experimental/compile/m_post_parsing.mli
Properties metaprl/theories/experimental/compile/m_post_parsing.mli
+6 -2 metaprl/theories/experimental/compile/m_test.ml
+7 -1 metaprl/theories/experimental/compile/m_theory.ml
+2 -0 metaprl/theories/experimental/compile/m_theory.mli

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-02-28 23:16:39 -0800 (Fri, 28 Feb 2003)
Revision: 4150
Log message:

      In an effort to avoid my actual homework, I decided to take a look
      at M_dead, M_inline, and M_prog.
      
      
      -------------------------------------------------
      M_dead:  Fixed a few cut-and-paste typos in the comments.  My only
      other observation is that it seems that something like
      
      LetAtom{AtomBinop{DivOp; AtomInt[1]; AtomInt[0]}; v. 'e} <--> 'e
      
      is allowed.  Which might be fine, depending on what the evaluation
      order is and how strictly you want to preserve the semantics of
      the program.
      
      
      -------------------------------------------------
      M_inline:  Fixed even more cut-and-paste typos.  Before,
      
      AtomBinop{SubOp; AtomInt[i:n]; AtomInt[j:n]}
      
      could have been folded using meta_diff, meta_prod, or meta_quot.
      I decided that perhaps someone intended to fold together
      multiplications and divisions together, instead of specifying
      three separate ways (two of which made no sense) to fold a
      subtraction...
      
      
      -------------------------------------------------
      M_prog:  Fixed a few more cut-and-paste typos in comments.  Also
      fixed a cut-and-paste typo present where fundecl_if_false is added
      to the prog resource (the term to match against was the same as in
      the fundecl_if_true case, which seemed bogus).  The other change
      is I added a rewrite fundef_let_pair which swaps FunDef with
      LetPair.  This might be wrong, but I couldn't think of any reason
      why you wouldn't want to have that rule, or why that rule would be
      incorrect.
      
      
      I suppose if I have more time on my hands, I'll try to take a look
      at closure conversion and CPS conversion, and maybe even pay
      attention to the discussions about this stuff.  (-:
      

Changes  Path
+3 -3 metaprl/theories/experimental/compile/m_dead.ml
+5 -5 metaprl/theories/experimental/compile/m_inline.ml
+6 -2 metaprl/theories/experimental/compile/m_prog.ml