[steph] Some improvements for NuPRL interface_ Mon Sep 19 02:30:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-13-410760000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-13-410760000-PDT.html [lolorigo] improved jprover interface to account for variables_ Mon Sep 19 02:30:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-13-929613000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-13-929613000-PDT.html [steph] Some optimizations for proof reconstruciton_ Mon Sep 19 02:30:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-14-411827000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-14-411827000-PDT.html [lolorigo] some naming updates from nuprllight to metaprl_ Mon Sep 19 02:30:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-16-477409000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-16-477409000-PDT.html [] This commit was manufactured by cvs2svn to create branch _unify_mm_._ Mon Sep 19 02:30:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-16-915824000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-16-915824000-PDT.html [nogin] I started working on removing old _and buggy__ unification and speeding up_ Mon Sep 19 02:30:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-17-466544000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-17-466544000-PDT.html [nogin] Converted couple of files to new unification._ Mon Sep 19 02:30:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-20-440175000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-20-440175000-PDT.html [steph] new_ Mon Sep 19 02:30:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-22-059826000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-22-059826000-PDT.html [nogin] Changed the typeinf tactic to use MM unification. Now this branch will compile._ Mon Sep 19 02:30:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-22-540106000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-22-540106000-PDT.html [nogin] Added some comments on usage of RefineError exceptions._ Mon Sep 19 02:30:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-23-420550000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-23-420550000-PDT.html [nogin] I replaced Cycle and Clash exceptions in unify_ds with_ Mon Sep 19 02:30:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-25-015365000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-25-015365000-PDT.html [krupski] The RefineError exceptins are incorporated correctly in Term_unif_ds module_ Mon Sep 19 02:30:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-25-570233000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-25-570233000-PDT.html [nogin] Use fail_core when appropriate._ Mon Sep 19 02:30:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-26-116402000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-26-116402000-PDT.html [lolorigo] term functions for jprover/nuprl interface_ Mon Sep 19 02:30:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-26-522375000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-26-522375000-PDT.html [steph] Optimized beta_proof computation for proof reconstruction_ Mon Sep 19 02:30:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-28-172692000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-28-172692000-PDT.html [nogin] Added__ Mon Sep 19 02:30:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-28-879692000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-28-879692000-PDT.html [nogin] I wrote a small guide to MetaPRL indentation and spacing conventions._ Mon Sep 19 02:30:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-29-279442000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-29-279442000-PDT.html [nogin] Removed some unnecessary spaces. Still need to do proper indentation._ Mon Sep 19 02:30:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-30-860358000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-30-860358000-PDT.html [nogin] Updated the guidelines after talking to Eli and looking at more_ Mon Sep 19 02:30:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-31-956205000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-31-956205000-PDT.html [nogin] get_core is supposed to return a real core and it can not return a Hashed __ Mon Sep 19 02:30:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-32-336683000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-32-336683000-PDT.html [nogin] _ Updated exception handling_ Mon Sep 19 02:30:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-32-769215000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-32-769215000-PDT.html [nogin] Better error message._ Mon Sep 19 02:30:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-33-349927000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-33-349927000-PDT.html [nogin] Fixed a bug in red_black_set _ it forgot to sort the list and get rid_ Mon Sep 19 02:30:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-33-750409000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-33-750409000-PDT.html [nogin] Use String_util.vnewname to rename variables._ Mon Sep 19 02:30:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-34-272510000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-34-272510000-PDT.html [nogin] Use StringSet for unification constants instead of string list._ Mon Sep 19 02:30:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-35-666906000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-35-666906000-PDT.html [nogin] Use Opname.eq to compare opnames._ Mon Sep 19 02:30:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-36-814898000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-36-814898000-PDT.html [nogin] terms2temp_multieq__ Mon Sep 19 02:30:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-37-206521000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-37-206521000-PDT.html [nogin] Use Red_black_table instead of Splay_table in Tptp_cache._ Mon Sep 19 02:30:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-38-653678000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-38-653678000-PDT.html [nogin] terms2temp_multieq again_ Do not create temp_meq before it_s really needed._ Mon Sep 19 02:30:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-39-800504000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-39-800504000-PDT.html [nogin] Create opL once, not every time unify_eqnl_eqnl is ran_ Mon Sep 19 02:30:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-40-282894000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-40-282894000-PDT.html [nogin] Wrote lots of debugging code while trying _so far unsuccesfully_ to find out_ Mon Sep 19 02:30:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-40-683395000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-40-683395000-PDT.html [nogin] Wrote even more debugging code._ Mon Sep 19 02:30:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-41-251833000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-41-251833000-PDT.html [nogin] This junk shouldn_t be here._ Mon Sep 19 02:30:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-42-754199000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-42-754199000-PDT.html [nogin] Small step towards making bytecode profiling more automatic._ Mon Sep 19 02:30:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-43-142609000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-43-142609000-PDT.html [nogin] Specialized the terms2temp_multieq code for the case of no subterms_ Mon Sep 19 02:30:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-43-700082000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-43-700082000-PDT.html [nogin] 4.7_ _nogin__ Mon Sep 19 02:30:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-44-170079000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-44-170079000-PDT.html [krupski] changes in the order of eqnlists __ m.b. more efficient unification_ Mon Sep 19 02:30:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-46-251164000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-46-251164000-PDT.html [nogin] Merged the unify_mm branch._ Mon Sep 19 02:30:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-46-650430000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-46-650430000-PDT.html [nogin] Splitted create_tptp into create_ax_statement and tptp_load._ Mon Sep 19 02:30:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-50-003685000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-50-003685000-PDT.html [nogin] These were unused for a long time._ Mon Sep 19 02:30:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-50-587963000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-50-587963000-PDT.html [nogin] Print first the rulebox count, then the rule count to be consistent_ Mon Sep 19 02:30:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-51-945834000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-51-945834000-PDT.html [nogin] Reverting the last change _ the problem is somewhere else._ Mon Sep 19 02:30:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-52-339110000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-52-339110000-PDT.html [nogin] Finally managed to make sure that rulebox count always goes before the node count._ Mon Sep 19 02:30:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-52-705652000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-52-705652000-PDT.html [nogin] Inlined cterms2system_ Mon Sep 19 02:30:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-54-331786000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-54-331786000-PDT.html [nogin] Replaced the free_vars function from TermSubst interface with free_vars_list_ Mon Sep 19 02:30:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-55-338285000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-55-338285000-PDT.html [nogin] _ Fixed a nasty bug in Term_ds.subst _ it didn_t notice when the same variable_ Mon Sep 19 02:30:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-57-532717000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-30-57-532717000-PDT.html [nogin] I wrote several sections of MetaPRL Developer Guide._ Mon Sep 19 02:31:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-00-136674000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-00-136674000-PDT.html [nogin] Moved Jprover output parsing into the JLogic interface. Still need to write the_ Mon Sep 19 02:31:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-03-059843000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-03-059843000-PDT.html [nogin] Do something reasonable for term printing in Ocaml toploop._ Mon Sep 19 02:31:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-07-758939000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-07-758939000-PDT.html [nogin] The Jprover interface is almost finished. It_s partially working, I just_ Mon Sep 19 02:31:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-08-253865000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-08-253865000-PDT.html [lolorigo] removed global vars used for debugging_ Mon Sep 19 02:31:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-08-814481000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-08-814481000-PDT.html [nogin] The PS and PDF versionf of the documenattion can now be downloaded_ Mon Sep 19 02:31:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-11-016023000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-11-016023000-PDT.html [nogin] Now sequents without hypothesis and axioms _rules without assumptions and paramaters__ Mon Sep 19 02:31:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-11-434610000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-11-434610000-PDT.html [nogin] Fixed a nasty bug in Jprover _after chaising it with Stephan for couple of hours__ Mon Sep 19 02:31:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-11-988476000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-05/2005-09-19-02-31-11-988476000-PDT.html