[nogin] Use silent mode, when VERBOSE is _false_, not when it_s _undefined_ _but if it_ Mon Sep 19 06:56:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-53-201730000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-53-201730000-PDT.html [nogin] d_apply_equalT should not be topval_ Mon Sep 19 06:56:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-53-589450000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-53-589450000-PDT.html [nogin] When Stdpp.Exc_located is raised and the file name is empty _as it happens,_ Mon Sep 19 06:56:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-53-966314000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-53-966314000-PDT.html [nogin] Deleted some unused code_ Mon Sep 19 06:56:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-54-365856000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-54-365856000-PDT.html [jyh] Changed the indentation of begin_end blocks._ Mon Sep 19 06:56:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-54-771356000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-54-771356000-PDT.html [nogin] The context_vars function makes more sense in TermMan, then in TermSubst._ Mon Sep 19 06:56:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-55-605650000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-55-605650000-PDT.html [kopylov] Add a theory Itt_synt_bterm_ Mon Sep 19 06:56:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-56-346752000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-56-346752000-PDT.html [kopylov] More on reflection_ Mon Sep 19 06:56:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-57-061366000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-57-061366000-PDT.html [xiny] proofs._ Mon Sep 19 06:56:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-57-686143000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-57-686143000-PDT.html [xiny] fixed a small bug_ Mon Sep 19 06:56:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-59-196671000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-56-59-196671000-PDT.html [jyh] Whew, mmc now compiles with full type information._ Mon Sep 19 06:57:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-01-766331000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-01-766331000-PDT.html [jyh] The standalone libmojave was forgetting all INCLUDES, so_ Mon Sep 19 06:57:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-07-309794000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-07-309794000-PDT.html [kopylov] Add the connection between synt_bterm and base_reflection _numerals__ Mon Sep 19 06:57:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-07-673606000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-07-673606000-PDT.html [xiny] proofs._ Mon Sep 19 06:57:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-08-171869000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-08-171869000-PDT.html [kopylov] Forget to commit base_reflection last time_ Mon Sep 19 06:57:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-09-767677000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-09-767677000-PDT.html [nogin] Minor updates_ Mon Sep 19 06:57:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-10-213290000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-10-213290000-PDT.html [xiny] made bterm_elim primitive and bterm_ind_wf interactive._ Mon Sep 19 06:57:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-10-673364000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-10-673364000-PDT.html [nogin] Removing an unused opname_ Mon Sep 19 06:57:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-11-084641000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-11-084641000-PDT.html [nogin] Made the interface slightly more specific_ Mon Sep 19 06:57:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-11-452395000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-11-452395000-PDT.html [nogin] This brings the support for non_sequent contexts one step closer. Now the_ Mon Sep 19 06:57:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-11-924203000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-11-924203000-PDT.html [nogin] Do not include the tests directory, unless any test files are actually in use._ Mon Sep 19 06:57:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-14-738143000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-14-738143000-PDT.html [] This commit was manufactured by cvs2svn to create branch_ Mon Sep 19 06:57:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-15-134878000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-15-134878000-PDT.html [jyh] 1. Strip type constraints at parse time after type checking._ Mon Sep 19 06:57:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-15-561566000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-15-561566000-PDT.html [nogin] The display form operators __slot_, _pushm_, etc_ and options __mode_,_ Mon Sep 19 06:57:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-16-654495000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-16-654495000-PDT.html [nogin] Display forms updates to support the recently added address parameters._ Mon Sep 19 06:57:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-17-265339000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-17-265339000-PDT.html [nogin] Removing TermMan.sweep_up_term _which was a dup of TermOp.map_up_term__ Mon Sep 19 06:57:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-17-679056000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-17-679056000-PDT.html [nogin] It_s map_up, not map_up_term, sorry__ Mon Sep 19 06:57:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-18-478313000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-18-478313000-PDT.html [jyh] Ported the display form changes, and removed the wildcard types_ Mon Sep 19 06:57:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-18-898164000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-18-898164000-PDT.html [nogin] Fixing TERMS_std_ Mon Sep 19 06:57:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-20-055115000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-20-055115000-PDT.html [] This commit was manufactured by cvs2svn to create branch_ Mon Sep 19 06:57:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-20-431145000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-20-431145000-PDT.html [jyh] Added the Quote typeclass. Quoted terms have types like the following._ Mon Sep 19 06:57:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-38-068813000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-38-068813000-PDT.html [nogin] Yet another instance of the opname_classes branch, merged once again with the_ Mon Sep 19 06:57:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-38-529801000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-57-38-529801000-PDT.html [nogin] These got accidentally resurrected in one of the merges. Removing them again._ Mon Sep 19 06:58:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-29-192188000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-29-192188000-PDT.html [nogin] Annotated a few things with __ Dform__ Mon Sep 19 06:58:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-29-930658000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-29-930658000-PDT.html [nogin] _ Removed the obsolte _Opname_ and _Definition_ choices from the summary_item_ Mon Sep 19 06:58:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-30-706797000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-30-706797000-PDT.html [jyh] Copy declare items from the interface during the checking phase._ Mon Sep 19 06:58:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-32-100712000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-32-100712000-PDT.html [jyh] Prevent redeclaration of shapes._ Mon Sep 19 06:58:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-33-028965000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-33-028965000-PDT.html [nogin] Adding a few _XXX BUG_ comments on some of the places Jason found._ Mon Sep 19 06:58:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-33-651666000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-33-651666000-PDT.html [jyh] Thread the flag for shape checking, rather than using an imperative_ Mon Sep 19 06:58:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-34-115583000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-34-115583000-PDT.html [nogin] Fixing the documentation display forms _that I broke when merging_ Mon Sep 19 06:58:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-34-629725000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-34-629725000-PDT.html [kopylov] Fix a bug in itt_rbtrees_ Mon Sep 19 06:58:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-35-214700000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-35-214700000-PDT.html [nogin] Improved display forms for the _declare_ directives._ Mon Sep 19 06:58:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-35-646702000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-35-646702000-PDT.html [jyh] This tries to be more careful about parsing terms._ Mon Sep 19 06:58:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-36-116259000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-36-116259000-PDT.html [jyh] Starting display form typing. Removed the create_term_parser function in_ Mon Sep 19 06:58:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-36-885857000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-36-885857000-PDT.html [nogin] Added comments with the exact shell command lines needed to generate the code_ Mon Sep 19 06:58:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-37-536121000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-37-536121000-PDT.html [xiny] added and proved some useful rules._ Mon Sep 19 06:58:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-38-246274000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-38-246274000-PDT.html [nogin] Added a bunch of comments_ Mon Sep 19 06:58:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-43-552917000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-43-552917000-PDT.html [jyh] Added display_form type checking. This was a little painful because_ Mon Sep 19 06:58:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-44-117375000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-58-44-117375000-PDT.html [jyh] Added typechecking on productions._ Mon Sep 19 06:59:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-18-773708000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-18-773708000-PDT.html [nogin] squiddle __ squiggle_ Mon Sep 19 06:59:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-19-204700000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-19-204700000-PDT.html [jyh] Disallow type constraints rules and rewrites. For type inference,_ Mon Sep 19 06:59:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-20-759819000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-20-759819000-PDT.html [jyh] Typechecking is now stricter._ Mon Sep 19 06:59:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-22-890822000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-22-890822000-PDT.html [nogin] Removed a bit of unused code_ Mon Sep 19 06:59:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-25-593160000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-25-593160000-PDT.html [nogin] Term_shape_gen.term_shape type does not need to be concrete_ Mon Sep 19 06:59:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-26-471475000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-26-471475000-PDT.html [nogin] Perv_dummy_arg is now Comment_dummy_arg and has a display form._ Mon Sep 19 06:59:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-26-961379000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-26-961379000-PDT.html [jyh] 1. Some work on mmc._ Mon Sep 19 06:59:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-27-518800000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-27-518800000-PDT.html [nogin] _ I_ve added a _docon_ term that is the opposite of the _docoff_. One can now_ Mon Sep 19 06:59:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-28-203447000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-28-203447000-PDT.html [jyh] OCaml code uses ocons/onil, not xcons/xnil._ Mon Sep 19 06:59:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-29-615756000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-29-615756000-PDT.html [nogin] Annotated a lot of the _dforms helper_ operators _including all in itt_comment_ Mon Sep 19 06:59:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-30-813945000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-30-813945000-PDT.html [nogin] display_col can now be typed properly_ Mon Sep 19 06:59:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-32-048855000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-32-048855000-PDT.html [nogin] Annotated a few more dform _helper_ opname with the __ Dform_ type annotation._ Mon Sep 19 06:59:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-32-474437000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-32-474437000-PDT.html [nogin] My previos changes would not actually compile, fixing._ Mon Sep 19 06:59:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-33-318007000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-33-318007000-PDT.html [nogin] df_rev_concat needs to know about ocons/onil as well._ Mon Sep 19 06:59:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-33-854281000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-33-854281000-PDT.html [nogin] Trivial comment change_ Mon Sep 19 06:59:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-34-251128000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-34-251128000-PDT.html [nogin] Added support for non_sequent contexts to Term_man_ds.context_vars_info_ Mon Sep 19 06:59:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-34-683988000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-34-683988000-PDT.html [nogin] Display form fixes._ Mon Sep 19 06:59:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-35-146910000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-35-146910000-PDT.html [nogin] Added display forms for the labels declared in Itt_labels._ Mon Sep 19 06:59:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-35-609665000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-35-609665000-PDT.html [xiny] Proved most of the rules in itt_synt_bterm._ Mon Sep 19 06:59:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-36-262598000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-36-262598000-PDT.html [nogin] ____________________________________________________________________________ Mon Sep 19 06:59:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-39-935257000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-06-59-39-935257000-PDT.html [nogin] Added a _gc_compact_ topval function that can be used to call Gc.compact and_ Mon Sep 19 07:00:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-55-979506000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-55-979506000-PDT.html [xiny] Proved more rules._ Mon Sep 19 07:00:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-56-439511000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-56-439511000-PDT.html [nogin] _ Package_info was putting packages into a complicated dag structure, but the_ Mon Sep 19 07:00:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-58-151860000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-58-151860000-PDT.html [nogin] PackReadOnly flag was never used _we were testing for it, but never setting_ Mon Sep 19 07:00:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-58-702069000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-58-702069000-PDT.html [jyh] I overlooked free type variables in the environment during existential_ Mon Sep 19 07:00:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-59-187332000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-00-59-187332000-PDT.html [nogin] _ Changed the default_extract error message to a more verbose one._ Mon Sep 19 07:01:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-02-226239000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-02-226239000-PDT.html [jyh] Progress toward removing package info that is not needed._ Mon Sep 19 07:01:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-02-743442000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-02-743442000-PDT.html [kopylov] Defined substitution_ Mon Sep 19 07:01:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-03-455453000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-03-455453000-PDT.html [xiny] a little more proofs._ Mon Sep 19 07:01:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-03-962557000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-03-962557000-PDT.html [kopylov] New list rules_ Mon Sep 19 07:01:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-06-015109000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-06-015109000-PDT.html [nogin] Working on properties of the substitution_ Mon Sep 19 07:01:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-06-527431000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-06-527431000-PDT.html [nogin] Adding couple of missing declarations._ Mon Sep 19 07:01:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-07-138231000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-07-138231000-PDT.html [jyh] Improve the space used by MetaPRL._ Mon Sep 19 07:01:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-07-547352000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-07-547352000-PDT.html [jyh] Collected the resource state into a record. Aleksey, can some of the_ Mon Sep 19 07:01:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-09-028072000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-09-028072000-PDT.html [yegor] Added length function to TableSig_ Mon Sep 19 07:01:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-09-950083000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-09-950083000-PDT.html [yegor] Removed dark shadows _ they can only be used to disprove things._ Mon Sep 19 07:01:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-10-407402000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-10-407402000-PDT.html [xiny] proved some rules._ Mon Sep 19 07:01:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-11-257343000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-11-257343000-PDT.html [nogin] _ The status_and_abandon_all will now call Package_info.abandon instead of_ Mon Sep 19 07:01:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-22-961025000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-22-961025000-PDT.html [nogin] Mp_resource.clean was too aggressive _keeping the data from implrove_resource,_ Mon Sep 19 07:01:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-23-737961000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-23-737961000-PDT.html [nogin] _ Call Proof_boot.Proof.clear_cache between modules when doing_ Mon Sep 19 07:01:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-24-159473000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-24-159473000-PDT.html [xiny] finished a proof due to Yegor_s omegaT improvement._ Mon Sep 19 07:01:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-24-877236000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-24-877236000-PDT.html [jyh] Fixed Package_info.abandon so that the proofs are deleted as well._ Mon Sep 19 07:01:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-25-813497000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-25-813497000-PDT.html [yegor] Removed debugging code._ Mon Sep 19 07:01:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-26-433634000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-26-433634000-PDT.html [kopylov] Some proofs in Itt_list2_ Mon Sep 19 07:01:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-26-934308000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-26-934308000-PDT.html [jyh] The type checker should not just assume that every variable is sensible__ Mon Sep 19 07:01:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-35-250830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-35-250830000-PDT.html [nogin] Rewriter was using __ instead of Lm_num.eq_num for comparing numbers, which_ Mon Sep 19 07:01:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-35-772445000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-35-772445000-PDT.html [kopylov] Fixed substitution. We don_t need subst_var anymore._ Mon Sep 19 07:01:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-36-298435000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-36-298435000-PDT.html [yegor] Omega became smarter, in some cases it significantly dropped_ Mon Sep 19 07:01:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-36-823294000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-36-823294000-PDT.html [kopylov] Some proofs for substituion._ Mon Sep 19 07:01:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-37-471888000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-37-471888000-PDT.html [kopylov] some more theorems_ Mon Sep 19 07:01:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-39-419721000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-39-419721000-PDT.html [kopylov] Added a definition of bind for bterms, but I_m not sure about it_ Mon Sep 19 07:01:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-39-950513000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-39-950513000-PDT.html [xiny] more proofs_ Mon Sep 19 07:01:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-41-209366000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-41-209366000-PDT.html [xiny] extend itt_list_ Mon Sep 19 07:01:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-44-231465000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-44-231465000-PDT.html [kopylov] Renamed a couple of rules._ Mon Sep 19 07:01:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-44-712695000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-44-712695000-PDT.html [nogin] We had a nasty problem in Itt_synt_operator where list_..._ in an _axiom__ Mon Sep 19 07:01:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-45-177473000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-45-177473000-PDT.html [jyh] Actually, only two files needed fixing with the new Ocaml typeclass._ Mon Sep 19 07:01:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-46-384531000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-46-384531000-PDT.html [jyh] Migrated the Refine.check__ tests so they are performed before_ Mon Sep 19 07:01:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-47-981242000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-47-981242000-PDT.html [yegor] I_ve implemented one of heurisitcs for Omega test_ Mon Sep 19 07:01:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-48-857145000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-48-857145000-PDT.html [jyh] Updated the term hashing in Filter_cache_fun. This propagates_ Mon Sep 19 07:01:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-49-441539000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-49-441539000-PDT.html [yegor] Variables that have only lower or only upper bounds can be removed_ Mon Sep 19 07:01:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-50-539132000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-50-539132000-PDT.html [yegor] Changed places where terms _polynoms_ have to be normalized._ Mon Sep 19 07:01:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-51-195214000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-51-195214000-PDT.html [xiny] proved theorems in itt_synt_subst_ Mon Sep 19 07:01:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-51-725280000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-51-725280000-PDT.html [jyh] Corrected the subtyping rule for hyp contexts._ Mon Sep 19 07:01:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-55-566874000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-55-566874000-PDT.html [yegor] Certain conditions _like ___ doubles number of problems omega_ Mon Sep 19 07:01:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-56-542270000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-56-542270000-PDT.html [yegor] Warning _branching is not supported yet_ should be printed_ Mon Sep 19 07:01:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-57-212725000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-57-212725000-PDT.html [kopylov] Add the rule subst_commute_ Mon Sep 19 07:01:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-57-702997000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-57-702997000-PDT.html [nogin] Fixed a rewriter bug. Made hypSubstT and revHypSubstT a bit smarter at_ Mon Sep 19 07:01:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-58-889819000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-58-889819000-PDT.html [nogin] Minor code cleanup. Minor optimizations._ Mon Sep 19 07:01:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-59-439941000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-01-59-439941000-PDT.html [xiny] Added some rewrites in itt_synt_subst_ on the way to prove _subst_commute_._ Mon Sep 19 07:02:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-00-095207000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-00-095207000-PDT.html [kopylov] Proved that T Type ___ T Type Type_ Mon Sep 19 07:02:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-01-740561000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-01-740561000-PDT.html [xiny] partial proof for all_list_wf_ Mon Sep 19 07:02:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-11-576845000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-11-576845000-PDT.html [kopylov] Proved a new induction principle for lists _tail_induction_ and proved all_list_wf using it_ Mon Sep 19 07:02:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-19-493053000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-02-19-493053000-PDT.html [yegor] Forgot positivity condition in one rule._ Mon Sep 19 07:03:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-03-52-851495000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-03-52-851495000-PDT.html [nogin] _ BUGS 3.14 was fixed some time ago._ Mon Sep 19 07:03:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-03-53-363951000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-03-53-363951000-PDT.html [yegor] Fixed gcd and beq_rat definitions_ Mon Sep 19 07:03:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-03-53-914905000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-03-53-914905000-PDT.html [nogin] The rules for dependent function, dependent product, and quantifiers needed to_ Mon Sep 19 07:04:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-19-240010000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-19-240010000-PDT.html [kopylov] Proved rules in itt_pairwise2_ Mon Sep 19 07:04:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-20-113447000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-20-113447000-PDT.html [xiny] still on they way to prove _subst_commute__ Mon Sep 19 07:04:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-20-820909000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-20-820909000-PDT.html [nogin] Fixed the do_check_all script._ Mon Sep 19 07:04:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-22-769410000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-22-769410000-PDT.html [nogin] Exception printer was raising an exception, fixed._ Mon Sep 19 07:04:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-23-333186000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-23-333186000-PDT.html [nogin] Proved a few rules._ Mon Sep 19 07:04:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-23-783548000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-23-783548000-PDT.html [nogin] Proved /itt_subtype/subtypeReflexivity_ Mon Sep 19 07:04:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-42-330987000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-42-330987000-PDT.html [nogin] Finished couple of proofs_ Mon Sep 19 07:04:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-47-393694000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-04-47-393694000-PDT.html [xiny] The proofs in itt_list2 messed up due to the replacement of list_top_ with list. Cleaned up and proved a few rules._ Mon Sep 19 07:06:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-22-318802000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-22-318802000-PDT.html [nogin] Finished a few simple proofs_ Mon Sep 19 07:06:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-30-832545000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-30-832545000-PDT.html [yegor] Replaced List.map with List.rev_map _it was causing stack overflow__ Mon Sep 19 07:06:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-35-903348000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-35-903348000-PDT.html [kopylov] Changed definition of not_fre_ Mon Sep 19 07:06:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-37-078730000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-37-078730000-PDT.html [xiny] Changed list_top_ back to list upon Aleksey_s request._ Mon Sep 19 07:06:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-37-579019000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-37-579019000-PDT.html [xiny] strengthened the subst rules_ Mon Sep 19 07:06:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-41-981427000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-41-981427000-PDT.html [kopylov] added Vars_of in mli_ Mon Sep 19 07:06:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-42-524029000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-42-524029000-PDT.html [kopylov] Small fixes of last Xin_s commits_ Mon Sep 19 07:06:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-42-939478000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-42-939478000-PDT.html [nogin] Make Itt_list2_list an I/O abstraction for list_top_. Note _ because of bug_ Mon Sep 19 07:06:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-43-399914000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-43-399914000-PDT.html [yegor] Some border cases fixes._ Mon Sep 19 07:06:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-47-368003000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-47-368003000-PDT.html [jyh] Fixed the problem with iforms in command_line terms._ Mon Sep 19 07:06:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-47-859446000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-47-859446000-PDT.html [nogin] The rules left_id and right_id were too strong and needed extra conditions._ Mon Sep 19 07:06:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-48-484331000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-48-484331000-PDT.html [nogin] Adding couple of typing conditions to couple of rewrites _this is a follow_up_ Mon Sep 19 07:06:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-49-794504000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-06-49-794504000-PDT.html [xiny] Trying to prove _subst_commute_._ Mon Sep 19 07:07:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-10-927115000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-10-927115000-PDT.html [nogin] _subst_commute_ __ _subst_commutativity__ Mon Sep 19 07:07:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-15-946989000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-15-946989000-PDT.html [nogin] _ Proved all the theorems in itt_synt_subst, except for the_ Mon Sep 19 07:07:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-16-746361000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-16-746361000-PDT.html [nogin] Proved a few rules as needed to make itt_nat fully grounded._ Mon Sep 19 07:07:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-20-969615000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-07-20-969615000-PDT.html [nogin] Proved a number of theorems in itt_list2. Had to add extra wf conditions in_ Mon Sep 19 07:08:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-51-388897000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-51-388897000-PDT.html [jyh] Make sure the grammar is prepared before marshaling. This addresses_ Mon Sep 19 07:08:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-54-452396000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-54-452396000-PDT.html [xiny] Finally, all theorems are proved now._ Mon Sep 19 07:08:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-54-955549000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-54-955549000-PDT.html [nogin] Proved a few theorems. Still missing /itt_list2/all_list_elim _ Alexei, can_ Mon Sep 19 07:08:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-56-767159000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-56-767159000-PDT.html [jyh] Oops_ Sorry, my last commit also reintroduced bug _405._ Mon Sep 19 07:08:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-58-307830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-58-307830000-PDT.html [xiny] rearranged the orders of some rules, and proved some rules._ Mon Sep 19 07:08:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-58-771107000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-08-58-771107000-PDT.html [kopylov] Proved all_list_elim_ Mon Sep 19 07:09:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-00-995163000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-00-995163000-PDT.html [kopylov] Proved more theorems in Itt_list2. Now as far as I can tell proofs in Itt_synt_ depend only on /itt_omega/var_elim2_ Mon Sep 19 07:09:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-03-594866000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-03-594866000-PDT.html [yegor] All proofs needed for omegaT are ground now._ Mon Sep 19 07:09:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-04-809642000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-04-809642000-PDT.html [yegor] Forgot to commit prla_file itself_ Mon Sep 19 07:09:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-07-573080000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-07-573080000-PDT.html [kopylov] Now all proofs in itt_synt_ are grounded_ Mon Sep 19 07:09:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-21-134946000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-21-134946000-PDT.html [kopylov] Add the reflection rules_ Mon Sep 19 07:09:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-25-379995000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-25-379995000-PDT.html [nogin] Updated to match the paper_ Mon Sep 19 07:09:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-25-887855000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-25-887855000-PDT.html [yegor] It_s a reference implementation with core of Omega Test_ Mon Sep 19 07:09:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-26-318030000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-26-318030000-PDT.html [yegor] More improvements for constraint that unfolds to_ Mon Sep 19 07:09:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-27-032560000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-27-032560000-PDT.html [yegor] Added fold_map and replace._ Mon Sep 19 07:09:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-31-408469000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-31-408469000-PDT.html [yegor] Subtraction and addition of linear forms were inefficient._ Mon Sep 19 07:09:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-31-917782000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-31-917782000-PDT.html [yegor] itt_int_bench3 time drop from 100 to 69 seconds._ Mon Sep 19 07:09:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-32-507045000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-32-507045000-PDT.html [jyh] Added some documentation on declarations._ Mon Sep 19 07:09:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-32-970490000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-32-970490000-PDT.html [yegor] Added some determinicity in the choice of next variable to eliminate_ Mon Sep 19 07:09:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-34-155147000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-34-155147000-PDT.html [jyh] Check token types too._ Mon Sep 19 07:09:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-34-693320000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-34-693320000-PDT.html [kopylov] Add some documentation_ Mon Sep 19 07:09:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-37-226452000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-37-226452000-PDT.html [kopylov] For some reason itt_bintree didn_t complile. Fixed._ Mon Sep 19 07:09:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-37-740715000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-37-740715000-PDT.html [jyh] Added a ___ form for productions, which really makes more sense than_ Mon Sep 19 07:09:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-39-380289000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-39-380289000-PDT.html [jyh] Different quotations should not be required to use the_ Mon Sep 19 07:09:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-39-979925000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-39-979925000-PDT.html [yegor] It now checks for pairs like F_3 _ F_2, i.e. opposite with empty intersection._ Mon Sep 19 07:09:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-41-093789000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-41-093789000-PDT.html [yegor] Proofs for the paper benchmark._ Mon Sep 19 07:09:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-41-695557000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-41-695557000-PDT.html [yegor] The paper benchmark is generated here_ Mon Sep 19 07:09:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-43-932995000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-43-932995000-PDT.html [jyh] Added two new iform terms__ Mon Sep 19 07:09:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-44-870143000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-44-870143000-PDT.html [jyh] Added contexts, so you can write such things as__ Mon Sep 19 07:09:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-48-530812000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-48-530812000-PDT.html [jyh] Added support for nested quotations. Here is an example._ Mon Sep 19 07:09:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-49-253081000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-49-253081000-PDT.html [jyh] Yay, my first codegen rule, codegen_hoist_fun. It is wrong,_ Mon Sep 19 07:09:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-53-716681000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-53-716681000-PDT.html [jyh] Progress for generating code for closures._ Mon Sep 19 07:09:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-54-658789000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-54-658789000-PDT.html [jyh] Added nested lexing to handle nested matching pairs._ Mon Sep 19 07:09:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-55-427359000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-55-427359000-PDT.html [kopylov] Added some display forms and documentation._ Mon Sep 19 07:09:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-57-058728000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-57-058728000-PDT.html [nogin] _ _Bug 409_ Removed an obsolete test for duplicate bindings in redex pattern_ Mon Sep 19 07:09:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-57-583490000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-57-583490000-PDT.html [kopylov] Started adapting Itt_reflection_example_lambda to new definition._ Mon Sep 19 07:09:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-58-267005000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-58-267005000-PDT.html [xiny] Some comments and proofs fixes in Itt_synt_var._ Mon Sep 19 07:09:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-59-594090000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-09-59-594090000-PDT.html [nogin] Added a display from for iform items_ minor fix in display forms for primitive_ Mon Sep 19 07:10:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-01-594328000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-01-594328000-PDT.html [jyh] Changed args to be a vector instead of a list._ Mon Sep 19 07:10:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-02-159992000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-02-159992000-PDT.html [jyh] Added support for closure elimination for recursive functions._ Mon Sep 19 07:10:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-10-881964000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-10-881964000-PDT.html [nogin] Removed the dash from the logo_ Mon Sep 19 07:10:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-21-488384000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-21-488384000-PDT.html [kopylov] Added some tactics, changed difinitons in itt_reflection_example_lambda_ Mon Sep 19 07:10:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-21-938443000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-21-938443000-PDT.html [nogin] Minor code clean_up_ Mon Sep 19 07:10:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-22-483994000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-22-483994000-PDT.html [nogin] Fixed an Ascii IO bug_ a corner case when overwriting a manually changed .prla_ Mon Sep 19 07:10:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-24-039452000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-24-039452000-PDT.html [nogin] This is an interesting one _ CVS stripping white space off at the end of the_ Mon Sep 19 07:10:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-24-695991000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-24-695991000-PDT.html [kopylov] Added some rewrites to reduce resource. Proved some theorems_ Mon Sep 19 07:10:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-25-242255000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-02/2005-09-19-07-10-25-242255000-PDT.html