Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-01 12:58:04 -0700 (Thu, 01 Sep 2005)
Revision: 7694
Log message:
- Xin, we are no longer using "operator" = "bterm" approach (in fact, we are
no longer using explicit bterms at all - bterms are just an external concent).
- Added a configure test for htmldoc.
| Changes | Path |
| +19 -11 | metaprl/doc/OMakefile |
| +4 -10 | metaprl/theories/itt/itt_hoas_operator.ml |
| +1 -1 | metaprl/theories/itt/itt_reflection_new.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-01 13:09:46 -0700 (Thu, 01 Sep 2005)
Revision: 7695
Log message:
More on concrete operators.
| Changes | Path |
| +1 -3 | metaprl/theories/base/base_operator.mli |
| +6 -10 | metaprl/theories/itt/itt_hoas_operator.ml |
| +0 -2 | metaprl/theories/itt/itt_hoas_operator.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-02 14:08:56 -0700 (Fri, 02 Sep 2005)
Revision: 7696
Log message:
Revised the text on functors.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-02 14:09:36 -0700 (Fri, 02 Sep 2005)
Revision: 7697
Log message:
Forgot these files.
| Changes | Path |
| Added | metaprl/theories/ocaml_doc/programs/setfunctor.ml |
| Properties | metaprl/theories/ocaml_doc/programs/setfunctor.ml |
| Added | metaprl/theories/ocaml_doc/programs/setfunctor2.ml |
| Properties | metaprl/theories/ocaml_doc/programs/setfunctor2.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-02 17:30:03 -0700 (Fri, 02 Sep 2005)
Revision: 7698
Log message:
*** WARNING: Breaks binary compatibility ***
Implemented the "Operator" parameters that allow imbedding reflected
"operators" into terms. This is similar to the recently introduces Shape
parameters.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-03 16:34:04 -0700 (Sat, 03 Sep 2005)
Revision: 7699
Log message:
RefineError -> RefineForceError.
| Changes | Path |
| +1 -1 | metaprl/theories/itt/itt_logic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-03 16:40:57 -0700 (Sat, 03 Sep 2005)
Revision: 7700
Log message:
Use LexStringSet instead of StringSet in UI.
| Changes | Path |
| +6 -6 | metaprl/support/shell/package_info.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-04 20:57:18 -0700 (Sun, 04 Sep 2005)
Revision: 7701
Log message:
One unification rule that was introduced for multi-modal case
was applied too generously - similar result could be obtained
by more than one sequence of rules. Hence we were wasting some time
in unification. This commit limits that rule application to
only one case where it really needed.
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 10:20:34 -0700 (Mon, 05 Sep 2005)
Revision: 7702
Log message:
Made multimodal-specific rule more narrow
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 10:42:30 -0700 (Mon, 05 Sep 2005)
Revision: 7703
Log message:
Removed one more redundant application of the multi-modal rule.
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 12:59:41 -0700 (Mon, 05 Sep 2005)
Revision: 7704
Log message:
More tests
| Changes | Path |
| +6 -0 | metaprl/theories/s4lp/s4_tests.ml |
| +934 -849 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Limin Jia (ljia at CS.Princeton.EDU)
Date: 2005-09-06 07:05:35 -0700 (Tue, 06 Sep 2005)
Revision: 7705
Log message:
Add examples
Changes by: ( at unknown.email)
Date: 2005-09-06 07:05:35 -0700 (Tue, 06 Sep 2005)
Revision: 7706
Log message:
This commit was manufactured by cvs2svn to create branch
'omake_0_9_7_pre6'.
Changes by: Limin Jia (ljia at CS.Princeton.EDU)
Date: 2005-09-06 07:16:32 -0700 (Tue, 06 Sep 2005)
Revision: 7707
Log message:
Edit
| Changes | Path |
| +0 -0 | metaprl/theories/ilc/ilc_mergesort.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-06 16:24:09 -0700 (Tue, 06 Sep 2005)
Revision: 7708
Log message:
OMakefiles for omake 0.9.7
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-15 01:36:29 -0700 (Thu, 15 Sep 2005)
Revision: 7710
Log message:
Use configure for readline/ncurses.
| Changes | Path |
| +2 -11 | metaprl/OMakefile |
| +8 -3 | metaprl/mk/defaults |
| +4 -3 | metaprl/mk/make_config |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-17 03:53:44 -0700 (Sat, 17 Sep 2005)
Revision: 7713
Log message:
Changed the names of some of the "J" modules. This was necessary because OCaml
was getting confused on OS X (where the file names are not case-sensitive).
| Changes | Path |
| +4 -4 | metaprl/refiner/reflib/jall.ml |
| +2 -2 | metaprl/refiner/reflib/jordering.ml |
| +6 -6 | metaprl/refiner/reflib/jtunify.ml |
| +1 -1 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-17 14:16:32 -0700 (Sat, 17 Sep 2005)
Revision: 7714
Log message:
More text for the book.
Aleksey, don't worry if this doesn't make it into the conversion.
I can copy them over afterwards.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-18 16:06:21 -0700 (Sun, 18 Sep 2005)
Revision: 7715
Log message:
Added "listmem_set".
| Changes | Path |
| +31 -0 | metaprl/theories/itt/itt_list2.ml |
| +4 -0 | metaprl/theories/itt/itt_list2.mli |
| +10753 -10838 | metaprl/theories/itt/itt_list2.prla |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-19 09:58:48 -0700 (Mon, 19 Sep 2005)
Revision: 7716
Log message:
Added the svn:externals link for libmojave.
| Changes | Path |
| Properties | metaprl |
| +1 -1 | metaprl/theories/itt/OMakefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-19 12:25:15 -0700 (Mon, 19 Sep 2005)
Revision: 7718
Log message:
We better use svn:// for libmojave, so people can check out read-only
copies.
| Changes | Path |
| Properties | metaprl |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-19 12:38:29 -0700 (Mon, 19 Sep 2005)
Revision: 7719
Log message:
Updated the externals definition for libmojave; added an externals definition
for doc/latex/inputs.
| Changes | Path |
| Properties | metaprl |
| Properties | metaprl/doc/latex |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-19 12:46:42 -0700 (Mon, 19 Sep 2005)
Revision: 7720
Log message:
Setting mime-type "application/x-metaprl" on all the *.prla files to tell
subversion that they should not be merged.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-19 13:45:42 -0700 (Mon, 19 Sep 2005)
Revision: 7722
Log message:
Changes related to CVS -> Subversion switch:
- Updated the documentation to use svn.metaprl.org URLs instead of the
cvs.metaprl.org ones.
- Updated checkout instructions (both read-only and read-write) to talk about
subversion instead of CVS.
- Updated *.eps and *.ai to be svn:eol-style=native,
svn:mime-type=application/postscript.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-22 13:43:54 -0700 (Thu, 22 Sep 2005)
Revision: 7777
Log message:
1.Original set of prefix unification rules was incomplete for S4nJ, so it was slow on certain problems.
I discovered t while working on a paper and now I believe the rules are complete.
2.Because of (1) original formulation of Muddy Children
could be solved in less than a second (vs half a minute before). But I replaced with with two more interesting formulations so the total time to check s4_tests actually increased.
3.It seems also that the optimization which forces Jprover
to prefer conclusion as a source of contradictions backfires in some cases:
consider A1...An >- B & C
and A1...An is complex
it will try to "prove" B,A1...An first and then for C,A1...An and in some cases it might not be able to reuse the unifier of A1...An from B,Ai for C,Ai
I'm not sure yet that this is actually what happens but I have examples when A >- B & C takes much more time than the sum of A >- B and A >- C
| Changes | Path |
| +138 -16 | metaprl/refiner/reflib/jtunify.ml |
| +40 -8 | metaprl/theories/s4lp/s4_tests.ml |
| Binary | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-22 15:20:21 -0700 (Thu, 22 Sep 2005)
Revision: 7778
Log message:
Partial work on inheritance.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-22 17:31:03 -0700 (Thu, 22 Sep 2005)
Revision: 7779
Log message:
Changed the definition of lang a little bit
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-23 22:56:41 -0700 (Fri, 23 Sep 2005)
Revision: 7781
Log message:
Changed the design of "Lang" so that "BTerm" can be defined from it.
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-23 23:51:20 -0700 (Fri, 23 Sep 2005)
Revision: 7782
Log message:
Changed the definion of BTerm and other related notions using "Lang".
Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-24 18:21:55 -0700 (Sat, 24 Sep 2005)
Revision: 7784
Log message:
Proved some examples using the new operator implementaion.
| Changes | Path |
| +6 -6 | metaprl/theories/itt/itt_hoas_operator.ml |
| Binary | metaprl/theories/itt/itt_hoas_operator.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-26 01:31:15 -0700 (Mon, 26 Sep 2005)
Revision: 7785
Log message:
Fixing a few minor problesm that were preventing the Itt_hoas_operator proofs
from going through.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-27 02:32:44 -0700 (Tue, 27 Sep 2005)
Revision: 7786
Log message:
Do not forget to close the INCLUDE files.
| Changes | Path |
| +3 -2 | metaprl/util/pa_macro.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-27 05:00:16 -0700 (Tue, 27 Sep 2005)
Revision: 7787
Log message:
I finnally found a way to solve the issue with locations in pa_macro-processed
files being wrong!!!!!!
| Changes | Path |
| +19 -3 | metaprl/util/pa_macro.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-27 06:32:00 -0700 (Tue, 27 Sep 2005)
Revision: 7788
Log message:
Implemented proper location handling in quotations parsing (including the
<:doc< >> quotations and nested quotations).
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-27 07:22:42 -0700 (Tue, 27 Sep 2005)
Revision: 7789
Log message:
My previous commit was incomplete, sorry!
| Changes | Path |
| +1 -0 | metaprl/editor/ml/shell_mp.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-28 00:24:02 -0700 (Wed, 28 Sep 2005)
Revision: 7790
Log message:
Complain if a Perv!Ignore binding is actually used.
| Changes | Path |
| +19 -6 | metaprl/refiner/reflib/term_ty_infer.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-28 05:42:53 -0700 (Wed, 28 Sep 2005)
Revision: 7791
Log message:
Removing a bit of unused code.
| Changes | Path |
| +0 -2 | metaprl/filter/base/filter_cache_fun.ml |
| +1 -2 | metaprl/filter/base/filter_summary_type.ml |
| +0 -1 | metaprl/filter/base/filter_type.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-28 23:15:54 -0700 (Wed, 28 Sep 2005)
Revision: 7793
Log message:
Minor parser clean-up.
| Changes | Path |
| +2 -2 | metaprl/filter/base/filter_type.ml |
| +5 -14 | metaprl/filter/filter/filter_parse.ml |
| +3 -3 | metaprl/filter/filter/term_grammar.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-28 23:32:36 -0700 (Wed, 28 Sep 2005)
Revision: 7794
Log message:
Ignore gen_int_bench*
| Changes | Path |
| Properties | metaprl/theories/itt |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-29 06:23:34 -0700 (Thu, 29 Sep 2005)
Revision: 7798
Log message:
This is a significant simplification of the interfaces that "push through" the
state needed by the term_grammar parser.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-29 08:23:04 -0700 (Thu, 29 Sep 2005)
Revision: 7802
Log message:
Implemented the type-sensitive interpretation of binding contexts. Now
arg{| <H> >- 'C |}
that is currently parsed as
arg{| <H<||>[]> >- 'C<|H|>[] |}
will get parsed as
arg{| <H<||>[]> >- 'C<||>[] |}
(i.e. 'C no longer depends on H) when arg is declared as
declare sequent [arg] { Ignore : ... >- ...} : ...
`
