[jyh] Proving twice one is two._ Mon Sep 19 01:59:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-47-265955000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-47-265955000-PDT.html [jyh] ___ empty log message ____ Mon Sep 19 01:59:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-56-887797000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-56-887797000-PDT.html [jyh] Working addition proof. Removing polymorphism from refiner____ Mon Sep 19 01:59:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-57-225153000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-57-225153000-PDT.html [nogin] Use __ for comparing opnames_ Mon Sep 19 01:59:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-58-222599000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-58-222599000-PDT.html [nogin] Refiner lib depends on term__ .mli files_ Mon Sep 19 01:59:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-58-851562000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-58-851562000-PDT.html [jyh] Generalized many the term_addr, term_man, and term_shape modules._ Mon Sep 19 01:59:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-59-193525000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-01-59-59-193525000-PDT.html [nogin] Fixed dependencies_ Mon Sep 19 02:00:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-02-562441000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-02-562441000-PDT.html [jyh] Nonpolymorphic refiner._ Mon Sep 19 02:00:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-03-425654000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-03-425654000-PDT.html [nogin] Efficiency_ Mon Sep 19 02:00:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-06-471217000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-06-471217000-PDT.html [nogin] ._ Mon Sep 19 02:00:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-07-006249000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-07-006249000-PDT.html [nogin] Clean should also remove generated .ml _ .mli files_ Mon Sep 19 02:00:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-07-349640000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-07-349640000-PDT.html [nogin] Commented out the parts of the code that are not compatible_ Mon Sep 19 02:00:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-07-756309000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-07-756309000-PDT.html [nogin] Use the sets implementation based on the splay trees in Term_ds module_ Mon Sep 19 02:00:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-08-370404000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-08-370404000-PDT.html [jyh] Propagated refinement changes._ Mon Sep 19 02:00:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-09-216068000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-09-216068000-PDT.html [nogin] Trying to make term_ds as fast as possible_ Mon Sep 19 02:00:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-16-116690000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-16-116690000-PDT.html [jyh] D tactic works, added itt_bool._ Mon Sep 19 02:00:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-16-748170000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-16-748170000-PDT.html [jyh] Modified resources._ Mon Sep 19 02:00:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-22-442094000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-22-442094000-PDT.html [jyh] Working factorial proof._ Mon Sep 19 02:00:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-22-902075000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-22-902075000-PDT.html [jyh] Switched to term_ds._ Mon Sep 19 02:00:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-24-547835000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-24-547835000-PDT.html [jyh] Adding timing tactical._ Mon Sep 19 02:00:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-25-175762000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-25-175762000-PDT.html [nogin] ._ Mon Sep 19 02:00:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-25-673827000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-25-673827000-PDT.html [nogin] Added cardinal function_ Mon Sep 19 02:00:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-26-056523000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-26-056523000-PDT.html [nogin] Fixed a typo_ Mon Sep 19 02:00:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-26-467816000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-26-467816000-PDT.html [nogin] Make it faster_ Mon Sep 19 02:00:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-26-891087000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-26-891087000-PDT.html [nogin] Added rev_iter2_ Mon Sep 19 02:00:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-27-254553000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-27-254553000-PDT.html [nogin] Make it faster_ Mon Sep 19 02:00:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-28-216700000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-28-216700000-PDT.html [nogin] _for_all2 f a b_ should not call f when a and b have different length_ Mon Sep 19 02:00:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-28-988496000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-28-988496000-PDT.html [nogin] Do not define helper functions inside a function_ Mon Sep 19 02:00:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-29-347773000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-29-347773000-PDT.html [nogin] Make it faster_ Mon Sep 19 02:00:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-29-931289000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-29-931289000-PDT.html [nogin] Fixed a typo_ Mon Sep 19 02:00:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-30-302950000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-30-302950000-PDT.html [nogin] Make it faster_ Mon Sep 19 02:00:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-30-748028000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-30-748028000-PDT.html [nogin] Speed improvements _ do not create functions inside other functions_ Mon Sep 19 02:00:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-31-661282000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-31-661282000-PDT.html [nogin] Make it faster_ Mon Sep 19 02:00:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-32-900110000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-32-900110000-PDT.html [nogin] ._ Mon Sep 19 02:00:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-33-294057000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-33-294057000-PDT.html [jyh] Added a few new functions._ Mon Sep 19 02:00:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-33-660375000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-33-660375000-PDT.html [jyh] Added CZF._ Mon Sep 19 02:00:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-36-371082000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-36-371082000-PDT.html [jyh] Added Makefile._ Mon Sep 19 02:00:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-42-621995000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-42-621995000-PDT.html [nogin] Use __ for comparing opnames_ Mon Sep 19 02:00:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-43-372158000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-43-372158000-PDT.html [nogin] ._ Mon Sep 19 02:00:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-43-875875000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-43-875875000-PDT.html [nogin] Added OCAMLCP variable _ if set to ocamlcp, make produces profiled code_ Mon Sep 19 02:00:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-44-298556000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-44-298556000-PDT.html [nogin] _make profile_ seems to be working_ Mon Sep 19 02:00:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-44-982377000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-44-982377000-PDT.html [nogin] Added set_writable ___ Mon Sep 19 02:00:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-46-032555000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-46-032555000-PDT.html [jyh] Added itt_test._ Mon Sep 19 02:00:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-46-490574000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-46-490574000-PDT.html [jyh] Added magic numbers._ Mon Sep 19 02:00:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-50-479375000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-50-479375000-PDT.html [nogin] Do not create functions inside a function_ Mon Sep 19 02:00:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-51-556760000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-51-556760000-PDT.html [nogin] Use CAMLPLIB environment variable_ Mon Sep 19 02:00:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-52-327521000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-52-327521000-PDT.html [nogin] Profiling_ Mon Sep 19 02:00:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-52-982402000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-52-982402000-PDT.html [jyh] Added ml_term._ Mon Sep 19 02:00:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-53-363861000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-53-363861000-PDT.html [jyh] Using marshaler for terms._ Mon Sep 19 02:00:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-53-774589000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-53-774589000-PDT.html [jyh] Optimizing compiler._ Mon Sep 19 02:00:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-54-305573000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-54-305573000-PDT.html [jyh] Added punix.ml_ Mon Sep 19 02:00:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-55-251933000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-55-251933000-PDT.html [jyh] Did some profiling._ Mon Sep 19 02:00:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-55-811976000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-55-811976000-PDT.html [nogin] ._ Mon Sep 19 02:00:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-56-518887000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-56-518887000-PDT.html [nogin] Added a dependency, so that make does not try_ Mon Sep 19 02:00:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-56-938080000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-56-938080000-PDT.html [nogin] Added a dependecy for native code build_ Mon Sep 19 02:00:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-57-401436000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-57-401436000-PDT.html [nogin] Removed all runtime closure creations_ Mon Sep 19 02:00:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-57-766571000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-57-766571000-PDT.html [nogin] OCAMLCPOPT allows to pass options to bytecode profiler_ Mon Sep 19 02:00:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-58-316085000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-58-316085000-PDT.html [nogin] ._ Mon Sep 19 02:00:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-58-861970000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-58-861970000-PDT.html [nogin] Fixed some typos_ Mon Sep 19 02:00:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-59-214631000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-59-214631000-PDT.html [jyh] Rewriting in contexts. This required a change in addressing,_ Mon Sep 19 02:00:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-59-588877000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-00-59-588877000-PDT.html [jyh] Fixed syntax error in term_addr_gen.ml_ Mon Sep 19 02:01:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-03-468262000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-03-468262000-PDT.html [nogin] Better profiling_ Mon Sep 19 02:01:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-04-086829000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-04-086829000-PDT.html [nogin] Compile ocamldep to native code_ Mon Sep 19 02:01:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-04-450598000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-04-450598000-PDT.html [jyh] Improved rewriter speed with conversion tree and flist._ Mon Sep 19 02:01:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-04-853986000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-04-853986000-PDT.html [nogin] ._ Mon Sep 19 02:01:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-07-547238000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-07-547238000-PDT.html [nogin] Do not pass __PROFILE_ flag to __OCAMLC__ Mon Sep 19 02:01:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-07-938596000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-07-938596000-PDT.html [nogin] ._ Mon Sep 19 02:01:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-08-313896000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-08-313896000-PDT.html [nogin] Added _compact option_ Mon Sep 19 02:01:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-08-716481000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-08-716481000-PDT.html [nogin] Added a dependency_ Mon Sep 19 02:01:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-09-092296000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-09-092296000-PDT.html [nogin] ._ Mon Sep 19 02:01:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-09-552481000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-09-552481000-PDT.html [nogin] Prevent some closure creations_ Mon Sep 19 02:01:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-10-055475000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-10-055475000-PDT.html [nogin] Moved Refiner exceptions into a separate module RefineErrors_ Mon Sep 19 02:01:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-10-552140000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-06/2005-09-19-02-01-10-552140000-PDT.html