Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-01 10:11:53 -0700 (Wed, 01 Jul 1998)
Revision: 2281
Log message:
When opnames do not match, raise RefineError directly
| Changes | Path |
| +5 -1 | metaprl/refiner/refiner/rewrite.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-01 11:10:10 -0700 (Wed, 01 Jul 1998)
Revision: 2282
Log message:
Replaced 80 with 100
| Changes | Path |
| +4 -1 | metaprl/theories/itt/itt_test.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-02 11:38:08 -0700 (Thu, 02 Jul 1998)
Revision: 2283
Log message:
Refiner modules now raise RefineError exceptions directly.
Modules in this revision have two versions: one that raises
verbose exceptions, and another that uses a generic exception.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-02 15:25:40 -0700 (Thu, 02 Jul 1998)
Revision: 2284
Log message:
Created term_copy module to copy and normalize terms.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-02 20:19:20 -0700 (Thu, 02 Jul 1998)
Revision: 2285
Log message:
Allow changing the ocamlopt -inline option with the INLINE environment variable
| Changes | Path |
| +4 -2 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 12:09:40 -0700 (Fri, 03 Jul 1998)
Revision: 2286
Log message:
Added $(ROOT)/refiner/refsig/refine_error.h to the list
of the files *_verb.ml and *_simp.ml depend on.
| Changes | Path |
| +2 -2 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 12:15:23 -0700 (Fri, 03 Jul 1998)
Revision: 2287
Log message:
Divided refine.ml into a "verbose" and a "simple" versions.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 12:19:30 -0700 (Fri, 03 Jul 1998)
Revision: 2288
Log message:
.
| Changes | Path |
| Properties | metaprl/theories/ocaml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 12:51:03 -0700 (Fri, 03 Jul 1998)
Revision: 2289
Log message:
Fixed a small bug - thanks to Steve Zdancewic.
| Changes | Path |
| +2 -2 | metaprl/mllib/splay_set.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 14:04:17 -0700 (Fri, 03 Jul 1998)
Revision: 2290
Log message:
Specified the full "path" to the Refine module:
open Refiner.Refiner.Refine
| Changes | Path |
| +5 -2 | metaprl/filter/filter_prog.mli |
| +5 -1 | metaprl/theories/base/base_dtactic.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-03 15:06:15 -0700 (Fri, 03 Jul 1998)
Revision: 2291
Log message:
IO terms are now in term_std format.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 15:36:40 -0700 (Fri, 03 Jul 1998)
Revision: 2292
Log message:
Removed some unused files
| Changes | Path |
| Deleted | metaprl/refiner/refsig/refine_error_sig.mli |
| Deleted | metaprl/refiner/term_gen/term_exn.ml |
| Deleted | metaprl/refiner/term_gen/term_exn.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 15:58:40 -0700 (Fri, 03 Jul 1998)
Revision: 2293
Log message:
Added -S option
| Changes | Path |
| +4 -0 | metaprl/filter/prlcomp.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-03 16:20:37 -0700 (Fri, 03 Jul 1998)
Revision: 2294
Log message:
Do not be too verbose in case orelseT fails
| Changes | Path |
| +14 -8 | metaprl/theories/tactic/tactic_type.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 00:40:13 -0700 (Sat, 04 Jul 1998)
Revision: 2295
Log message:
Made make_term function 40% faster.
| Changes | Path |
| +13 -7 | metaprl/refiner/term_ds/term_base_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 15:28:23 -0700 (Sat, 04 Jul 1998)
Revision: 2296
Log message:
Fixed mk_so_var - it should not use mk_term
| Changes | Path |
| +5 -3 | metaprl/refiner/term_ds/term_base_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 15:31:13 -0700 (Sat, 04 Jul 1998)
Revision: 2297
Log message:
Set GC parameters
| Changes | Path |
| +12 -0 | metaprl/refiner/refbase/opname.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 15:34:08 -0700 (Sat, 04 Jul 1998)
Revision: 2298
Log message:
Use fact(125)
| Changes | Path |
| +4 -1 | metaprl/theories/itt/itt_test.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 16:05:15 -0700 (Sat, 04 Jul 1998)
Revision: 2299
Log message:
mk_term should be able to handle the case wher opname == var_opname - ocaml_df uses it.
| Changes | Path |
| +6 -5 | metaprl/refiner/term_ds/term_base_ds.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-04 18:47:36 -0700 (Sat, 04 Jul 1998)
Revision: 2300
Log message:
Itt_theory.ml{,i} are now different.
| Changes | Path |
| Properties | metaprl/theories/itt |
| Added | metaprl/theories/itt/itt_theory.ml |
| Properties | metaprl/theories/itt/itt_theory.ml |
| Added | metaprl/theories/itt/itt_theory.mli |
| Properties | metaprl/theories/itt/itt_theory.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 20:13:06 -0700 (Sat, 04 Jul 1998)
Revision: 2301
Log message:
Rewrote var_subst to make it do what it is actually supposed to do
| Changes | Path |
| +24 -6 | metaprl/refiner/term_ds/term_subst_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 20:41:06 -0700 (Sat, 04 Jul 1998)
Revision: 2302
Log message:
Finally "make -j" and "make -j opt" do everything right
| Changes | Path |
| +4 -7 | metaprl/refiner/Makefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-04 23:52:16 -0700 (Sat, 04 Jul 1998)
Revision: 2303
Log message:
Better Makefiles
| Changes | Path |
| +2 -1 | metaprl/library/Makefile |
| +2 -1 | metaprl/mllib/Makefile |
| +3 -2 | metaprl/refiner/Makefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-05 00:38:52 -0700 (Sun, 05 Jul 1998)
Revision: 2304
Log message:
Do not pass unnecessary arguments in a _simple version of the refiner
| Changes | Path |
| +46 -22 | metaprl/refiner/term_gen/term_addr_gen.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-05 12:08:05 -0700 (Sun, 05 Jul 1998)
Revision: 2305
Log message:
Compile with -noassert by default.
Compile without -noassert if DEBUG_NL environment variable is set.
| Changes | Path |
| +5 -2 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-05 12:14:50 -0700 (Sun, 05 Jul 1998)
Revision: 2306
Log message:
Added -noassert option to prlc
| Changes | Path |
| +5 -1 | metaprl/filter/prlcomp.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-06 10:55:31 -0700 (Mon, 06 Jul 1998)
Revision: 2307
Log message:
Removed $Log messages from all NL files.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-06 13:52:43 -0700 (Mon, 06 Jul 1998)
Revision: 2308
Log message:
Created an alternative apply_fun[_arg]_at_addr for functions that do not depend on bvars list.
Renamed the old ones to apply_var_fun[_arg]_at_addr
| Changes | Path |
| +2 -2 | metaprl/refiner/refiner/refine.mlp |
| +4 -2 | metaprl/refiner/refsig/term_addr_sig.ml |
| +112 -83 | metaprl/refiner/term_gen/term_addr_gen.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-06 14:39:34 -0700 (Mon, 06 Jul 1998)
Revision: 2309
Log message:
Working czf_itt_set.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-07 15:11:16 -0700 (Tue, 07 Jul 1998)
Revision: 2310
Log message:
Test the new CVS server
| Changes | Path |
| +0 -0 | metaprl/README |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-07 16:12:44 -0700 (Tue, 07 Jul 1998)
Revision: 2311
Log message:
Test.
| Changes | Path |
| +0 -0 | metaprl/README |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-07 19:36:00 -0700 (Tue, 07 Jul 1998)
Revision: 2312
Log message:
Moved all "if !debug_..." statements in the refiner
(except for "if !debug_load...") inside the #ifdef VERBOSE_EXN
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-07 21:55:43 -0700 (Tue, 07 Jul 1998)
Revision: 2313
Log message:
Added apply_fun_higher : (term -> term * 'a) -> term -> term * 'a list
The 'a list returned lists all successful applications of the function
"left to right".
When the function raises RefineError _ everywhere inside some subterm,
the sharing is preserved.
| Changes | Path |
| +4 -0 | metaprl/refiner/refsig/term_addr_sig.ml |
| +20 -0 | metaprl/refiner/term_gen/term_addr_gen.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-08 08:42:11 -0700 (Wed, 08 Jul 1998)
Revision: 2314
Log message:
Pushed higherC into the refiner for efficiency.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-08 09:07:59 -0700 (Wed, 08 Jul 1998)
Revision: 2315
Log message:
Fixed firstC to enable higherC optimization.
| Changes | Path |
| +3 -4 | metaprl/refiner/refiner/refine.mlp |
| +3 -3 | metaprl/theories/tactic/conversionals.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-08 09:19:40 -0700 (Wed, 08 Jul 1998)
Revision: 2316
Log message:
Fixed a missing case in firstC.
| Changes | Path |
| +2 -0 | metaprl/theories/tactic/conversionals.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-08 10:50:55 -0700 (Wed, 08 Jul 1998)
Revision: 2317
Log message:
Use fact(250) instead of fact(125).
Right now fact(250) runs in 9 seconds under Term_ds_simp.
| Changes | Path |
| +1 -1 | metaprl/theories/itt/itt_test.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-08 17:35:42 -0700 (Wed, 08 Jul 1998)
Revision: 2318
Log message:
Do not allocate a cons cell before calling apply_rewrite or apply_redex -
use an extra argument instead.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-08 19:37:21 -0700 (Wed, 08 Jul 1998)
Revision: 2319
Log message:
Create ([||], [||], []) and ([||], [||]) in advance, not at every call
| Changes | Path |
| +6 -4 | metaprl/refiner/refiner/refine.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-09 14:08:59 -0700 (Thu, 09 Jul 1998)
Revision: 2320
Log message:
Upgraded czf.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-11 16:18:20 -0700 (Sat, 11 Jul 1998)
Revision: 2321
Log message:
Faster opname_of_term
| Changes | Path |
| +3 -1 | metaprl/refiner/term_ds/term_base_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-11 19:40:37 -0700 (Sat, 11 Jul 1998)
Revision: 2322
Log message:
Faster alpha_equal
| Changes | Path |
| +7 -19 | metaprl/refiner/term_ds/term_subst_ds.mlp |
Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-07-13 12:44:25 -0700 (Mon, 13 Jul 1998)
Revision: 2323
Log message:
Corrected CAMLLIB location in README.
| Changes | Path |
| +1 -1 | metaprl/README |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-13 14:47:02 -0700 (Mon, 13 Jul 1998)
Revision: 2324
Log message:
CAMLLIB & CAMLP4LIB directories should be set to
/usr/lib/ocaml & /usr/lib/camlp4 when my RPMs are used
| Changes | Path |
| +7 -3 | metaprl/README |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-14 08:44:03 -0700 (Tue, 14 Jul 1998)
Revision: 2325
Log message:
Intermediate version with auto tactic.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-14 14:04:31 -0700 (Tue, 14 Jul 1998)
Revision: 2326
Log message:
Added to itt_derived.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-14 14:30:08 -0700 (Tue, 14 Jul 1998)
Revision: 2327
Log message:
Use fact(300)
| Changes | Path |
| +1 -1 | metaprl/theories/itt/itt_test.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-14 15:37:32 -0700 (Tue, 14 Jul 1998)
Revision: 2328
Log message:
Better alpha_equal
| Changes | Path |
| +14 -2 | metaprl/mllib/splay_set.ml |
| +3 -1 | metaprl/mllib/splay_set.mli |
| +5 -5 | metaprl/refiner/term_ds/term_base_ds.mlp |
| +5 -2 | metaprl/refiner/term_ds/term_subst_ds.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-14 18:49:03 -0700 (Tue, 14 Jul 1998)
Revision: 2329
Log message:
Extensions to unix library.
| Changes | Path |
| Added | metaprl/mllib/unix_util.ml |
| Properties | metaprl/mllib/unix_util.ml |
| Added | metaprl/mllib/unix_util.mli |
| Properties | metaprl/mllib/unix_util.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-14 19:40:59 -0700 (Tue, 14 Jul 1998)
Revision: 2330
Log message:
apply_fun_higher was making some unnecessary calls to mk_bterm - fixed.
| Changes | Path |
| +9 -4 | metaprl/refiner/term_gen/term_addr_gen.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-14 21:01:56 -0700 (Tue, 14 Jul 1998)
Revision: 2331
Log message:
Faster alpha_equal
| Changes | Path |
| +11 -6 | metaprl/refiner/term_ds/term_subst_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-15 10:47:27 -0700 (Wed, 15 Jul 1998)
Revision: 2332
Log message:
Faster match_redex
| Changes | Path |
| +125 -100 | metaprl/refiner/refiner/rewrite.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-17 08:39:32 -0700 (Fri, 17 Jul 1998)
Revision: 2333
Log message:
CZF is complete, although we may wish to add pairing and inf.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-17 23:38:47 -0700 (Fri, 17 Jul 1998)
Revision: 2334
Log message:
I am testing the new e-mail notification scripts.
Added the URL for OCAML RPMs to README
Ran ispell on status.tex
| Changes | Path |
| +2 -1 | metaprl/README |
| +6 -6 | metaprl/doc/status.tex |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-20 15:47:14 -0700 (Mon, 20 Jul 1998)
Revision: 2335
Log message:
Use Failure instead of Invalid_argument
| Changes | Path |
| +3 -3 | metaprl/refiner/term_ds/term_subst_ds.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-21 15:47:13 -0700 (Tue, 21 Jul 1998)
Revision: 2336
Log message:
Added NL toploop so that we can compile NL native code.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-21 17:34:42 -0700 (Tue, 21 Jul 1998)
Revision: 2337
Log message:
Removed dest_sequent, and changed Term_man_sig.esequent to use arrays.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-21 18:58:32 -0700 (Tue, 21 Jul 1998)
Revision: 2338
Log message:
Changed opname equality. Opnames should be compared with
the function Opname.eq.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-21 22:53:00 -0700 (Tue, 21 Jul 1998)
Revision: 2339
Log message:
Added *.top
| Changes | Path |
| Properties | metaprl/editor/ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-22 09:47:09 -0700 (Wed, 22 Jul 1998)
Revision: 2340
Log message:
Fixed test.opt compilation
| Changes | Path |
| +2 -1 | metaprl/theories/itt/Makefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-22 16:51:01 -0700 (Wed, 22 Jul 1998)
Revision: 2341
Log message:
Added the Opname.atom type. Opname.opname can be converted to
atoms using Opname.intern, and atoms are always equal iff they
are pointer equal.
| Changes | Path |
| +17 -1 | metaprl/refiner/refbase/opname.ml |
| +4 -0 | metaprl/refiner/refbase/opname.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-22 20:20:30 -0700 (Wed, 22 Jul 1998)
Revision: 2342
Log message:
Do not copy anything to the lib directory, use ln instead
| Changes | Path |
| +1 -1 | metaprl/clib/Makefile |
| +1 -1 | metaprl/library/Makefile |
| +3 -1 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-22 20:23:17 -0700 (Wed, 22 Jul 1998)
Revision: 2343
Log message:
Do not copy anything in bin, use ln instead
| Changes | Path |
| +2 -1 | metaprl/util/Makefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-22 21:31:04 -0700 (Wed, 22 Jul 1998)
Revision: 2344
Log message:
Make "make clean" really clean - remove *.run *.cma and *.cmxa files
| Changes | Path |
| +0 -2 | metaprl/filter/Makefile |
| +1 -1 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-22 21:33:00 -0700 (Wed, 22 Jul 1998)
Revision: 2345
Log message:
Oops, forgot *.cmx
| Changes | Path |
| +1 -1 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-22 21:34:26 -0700 (Wed, 22 Jul 1998)
Revision: 2346
Log message:
Removed CVS $Log messages
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-23 11:40:34 -0700 (Thu, 23 Jul 1998)
Revision: 2347
Log message:
Moved eseqent type to the TermType module.
Made the types of esequent components hidden to make them read-only.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-23 23:01:32 -0700 (Thu, 23 Jul 1998)
Revision: 2348
Log message:
Term_copy now checks if the term is a sequent (with is_sequent_term)
and uses explode_sequent/mk_sequent_term instead of dest_term/make_term
for sequents
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-24 06:33:55 -0700 (Fri, 24 Jul 1998)
Revision: 2349
Log message:
Exceptions reported properly in filter_main.
| Changes | Path |
| +1 -1 | metaprl/filter/filter_main.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-24 09:37:40 -0700 (Fri, 24 Jul 1998)
Revision: 2350
Log message:
Fixed exception reporting in Filter_parse.MakeFilter.save.
| Changes | Path |
| +2 -2 | metaprl/filter/filter_main.ml |
| +21 -13 | metaprl/filter/filter_parse.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-24 10:32:34 -0700 (Fri, 24 Jul 1998)
Revision: 2351
Log message:
Removed rewriteContextCut. This needs to be reimplemented.
| Changes | Path |
| +4 -1 | metaprl/theories/tactic/rewrite_type.ml |
| +2 -0 | metaprl/theories/tactic/rewrite_type.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 11:07:19 -0700 (Fri, 24 Jul 1998)
Revision: 2352
Log message:
Commented out some sequent code that should be rewritten.
| Changes | Path |
| +3 -1 | metaprl/theories/base/base_dform.ml |
| +1 -1 | metaprl/theories/tactic/perv.ml |
| +1 -1 | metaprl/theories/tactic/perv.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 12:18:20 -0700 (Fri, 24 Jul 1998)
Revision: 2353
Log message:
Fixed some typos
| Changes | Path |
| +1 -1 | metaprl/refiner/term_gen/term_man_gen.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 12:37:30 -0700 (Fri, 24 Jul 1998)
Revision: 2354
Log message:
Fixed some other typos
| Changes | Path |
| +3 -6 | metaprl/refiner/term_gen/term_man_gen.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 13:10:05 -0700 (Fri, 24 Jul 1998)
Revision: 2355
Log message:
Renamed Refine_ds to Refine_ds_verb and Refine_std to Refine_std_verb
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 14:11:12 -0700 (Fri, 24 Jul 1998)
Revision: 2356
Log message:
Functorized the Simple_print module over the Refiner module
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 14:28:06 -0700 (Fri, 24 Jul 1998)
Revision: 2357
Log message:
Functorized term_copy module over the whole refiner instead of over seperate term modules
| Changes | Path |
| +149 -199 | metaprl/refiner/reflib/term_copy.ml |
| +6 -45 | metaprl/refiner/reflib/term_copy.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-24 14:43:28 -0700 (Fri, 24 Jul 1998)
Revision: 2358
Log message:
Added debugging to copy_proof.
| Changes | Path |
| +18 -1 | metaprl/filter/filter_summary.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 14:45:48 -0700 (Fri, 24 Jul 1998)
Revision: 2359
Log message:
.
| Changes | Path |
| +2 -2 | metaprl/filter/filter_summary.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 16:36:09 -0700 (Fri, 24 Jul 1998)
Revision: 2360
Log message:
Fixed a bug
| Changes | Path |
| +3 -3 | metaprl/refiner/refbase/opname.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-24 17:07:09 -0700 (Fri, 24 Jul 1998)
Revision: 2361
Log message:
Updated .prlb files.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-24 21:03:42 -0700 (Fri, 24 Jul 1998)
Revision: 2362
Log message:
Fixed nl.run full toploop compilation
| Changes | Path |
| +1 -1 | metaprl/editor/ml/shell_p4.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-25 00:03:48 -0700 (Sat, 25 Jul 1998)
Revision: 2363
Log message:
No need to make opt twice in editor/ml
| Changes | Path |
| +1 -1 | metaprl/Makefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-26 16:00:29 -0700 (Sun, 26 Jul 1998)
Revision: 2364
Log message:
Changed the default camlp4 directory to /usr/lib/camlp4
| Changes | Path |
| +1 -1 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-26 16:52:34 -0700 (Sun, 26 Jul 1998)
Revision: 2365
Log message:
If CAMLLIB is not defined, use /usr/lib/ocaml
| Changes | Path |
| +3 -0 | metaprl/mk/config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-26 17:27:38 -0700 (Sun, 26 Jul 1998)
Revision: 2366
Log message:
Added a new function get_core that is supposed to know how to push down
delayed substitutions into the special terms without converting them into
an "ugly" form.
is_*_term functions should use get_core instead of dest_term since dest_term
should not be called on special terms
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-26 19:02:43 -0700 (Sun, 26 Jul 1998)
Revision: 2367
Log message:
Use $(RM) instead of del or rm -f
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-26 19:06:43 -0700 (Sun, 26 Jul 1998)
Revision: 2368
Log message:
Faster filter functions - preserve sharing when possible
| Changes | Path |
| +3 -2 | metaprl/mllib/list_util.ml |
| +8 -4 | metaprl/mllib/splay_set.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-27 20:03:41 -0700 (Mon, 27 Jul 1998)
Revision: 2369
Log message:
Initial checkin - TermMan module for
Term_ds with special representation of sequent terms
| Changes | Path |
| Added | metaprl/refiner/term_ds/term_man_ds.mlip |
| Properties | metaprl/refiner/term_ds/term_man_ds.mlip |
| Added | metaprl/refiner/term_ds/term_man_ds.mlp |
| Properties | metaprl/refiner/term_ds/term_man_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-29 12:52:53 -0700 (Wed, 29 Jul 1998)
Revision: 2370
Log message:
Better cpp macros (ML code should not have been changed)
| Changes | Path |
| +13 -19 | metaprl/refiner/term_gen/term_addr_gen.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-29 15:33:43 -0700 (Wed, 29 Jul 1998)
Revision: 2371
Log message:
Changed the Term_ds module to treat sequents specially.
Dest_term still works on sequents converting them to "ugly" form, but that should go away eventually.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-30 06:35:54 -0700 (Thu, 30 Jul 1998)
Revision: 2372
Log message:
Sequent-aware alpha-equality
| Changes | Path |
| +2 -0 | metaprl/refiner/term_ds/term_subst_ds.mlip |
| +37 -2 | metaprl/refiner/term_ds/term_subst_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-30 06:43:16 -0700 (Thu, 30 Jul 1998)
Revision: 2373
Log message:
Added optimized code profiled compilation (make profile)
| Changes | Path |
| +9 -2 | metaprl/Makefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-30 10:56:44 -0700 (Thu, 30 Jul 1998)
Revision: 2374
Log message:
Faster opname_of_term
| Changes | Path |
| +2 -2 | metaprl/refiner/term_ds/term_base_ds.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-30 14:41:13 -0700 (Thu, 30 Jul 1998)
Revision: 2375
Log message:
Updated occurs-check in unification.
| Changes | Path |
| +1 -1 | metaprl/refiner/refsig/term_subst_sig.ml |
| +91 -56 | metaprl/refiner/term_ds/term_subst_ds.mlp |
| +104 -68 | metaprl/refiner/term_std/term_subst_std.mlp |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-31 07:35:45 -0700 (Fri, 31 Jul 1998)
Revision: 2376
Log message:
Added TPTP theory, and Ensemble library. Fixed sequent displays.
BUG: rewrites fail on sequents.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-31 07:43:48 -0700 (Fri, 31 Jul 1998)
Revision: 2377
Log message:
Updated indentation style in term_man_ds.mlp
| Changes | Path |
| +147 -109 | metaprl/refiner/term_ds/term_man_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-31 08:23:28 -0700 (Fri, 31 Jul 1998)
Revision: 2378
Log message:
In Term_ds module is_* functions should use get_core instead of dest-term
since dest_term may raise an exception when called on a special term while
is_* functions should not raise any exceptions.
| Changes | Path |
| +4 -4 | metaprl/refiner/term_ds/term_op_ds.mlp |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-31 20:37:49 -0700 (Fri, 31 Jul 1998)
Revision: 2379
Log message:
Added functions append_array and append_list to SeqHyp and SeqGoal modules
Added function replace to the Array_util module