Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-02 02:50:17 -0700 (Wed, 02 Jul 2003)
Revision: 4692
Log message:
Adding a fix that was missing from the previous commit.
| Changes | Path |
| +1 -0 | metaprl/filter/Makefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 16:18:38 -0700 (Thu, 03 Jul 2003)
Revision: 4693
Log message:
Added some example code for how we want new term
constructors and destructors in core_type_infer.ml.
This code doesn't compile, but it demonstrates the
concept.
| Changes | Path |
| +1 -1 | metaprl/editor/ml/mpconfig |
| +3 -3 | metaprl/support/tactics/simp_typeinf.ml |
| +1 -1 | mpcompiler/mmc/core/mmc_core_ast.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 19:16:39 -0700 (Thu, 03 Jul 2003)
Revision: 4695
Log message:
Added Filter_patt to prlc.cma
| Changes | Path |
| +2 -1 | metaprl/filter/OMakefile |
| +1 -1 | metaprl/filter/filter/filter_patt.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 19:25:08 -0700 (Thu, 03 Jul 2003)
Revision: 4696
Log message:
Updating filter/Makefile
| Changes | Path |
| +4 -2 | metaprl/filter/Makefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 20:56:03 -0700 (Thu, 03 Jul 2003)
Revision: 4697
Log message:
Beginning the slow process of migrating MetaPRL toward libmojave.
| Changes | Path |
| +1 -1 | metaprl/Makefile |
| +8 -3 | metaprl/OMakefile |
| +9 -15 | metaprl/editor/ml/OMakefile |
| +4 -0 | metaprl/mk/make_config.sh |
| +1 -1 | mpcompiler/mmc/core/mmc_core_type_infer.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-04 04:09:48 -0700 (Fri, 04 Jul 2003)
Revision: 4698
Log message:
Implemented the <:con< ... >> quotation that is similar to << ... >>, but allows
anti-quotations, which makes it a very espressive mechanism for term construction.
Currently supported syntax:
Terms:
- $e$ where e is an ML expression of type term
- !t! where t is a traditional term "constant" (allows using input shortcuts)
- '$e$ where e is an ML expression of type string (e.g. creates a variable expr).
- opname[params]{bterm; bterm; ... } - standard format (params and/or bterms can be omited)
Params:
- "str" - string constant
- id[:kind] - (kind is one of s,t,n,l) - meta-variable (kind is "s" by default)
- [0-9]+ - numeric constant
- $e:kind - where e is an ML expression of appropriate type
(string for s,t; Mp_num.num for n, level_exp for l)
Bterm:
- t
- bvar, bvar, ..., bvar. term
Bvar:
- id - constant bvar
- $e$ - where e is an ML expression of type string
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-04 13:52:30 -0700 (Fri, 04 Jul 2003)
Revision: 4699
Log message:
Somehow my previous commit was incomplete.
| Changes | Path |
| +1 -1 | metaprl/theories/tptp/tptp_load.ml |
| +1 -1 | metaprl/theories/tptp/tptp_prove.ml |
Changes by: ( at unknown.email)
Date: 2003-07-04 13:52:30 -0700 (Fri, 04 Jul 2003)
Revision: 4700
Log message:
This commit was manufactured by cvs2svn to create branch
'abstract_vars'.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-04 14:51:58 -0700 (Fri, 04 Jul 2003)
Revision: 4701
Log message:
Explode_term must be a total function (we can not have tactics using
it raise Invalid_argument just because they happen to hit an unsupported
parameter).
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-04 17:36:18 -0700 (Fri, 04 Jul 2003)
Revision: 4702
Log message:
Depeting some unused code.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-05 18:25:50 -0700 (Sat, 05 Jul 2003)
Revision: 4703
Log message:
This is partial progress toward abstract vars. This is a
branch commit.
I am giving up on this for a moment. Unfortunately, string
hacking on variable names is everywhere, not cleanly isolated,
and not clearly specified. This makes a port to abstract
var names either 1) hard, because all this code has to be cleaned
up, or 2) nonsense, because of the need to covert back and forth
between strings all the time.
I still think it is a good idea, but it will take a fair amount of
effort.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 16:41:01 -0700 (Sun, 06 Jul 2003)
Revision: 4704
Log message:
I decided to finish the port to abstract vars anyway.
This versdion compiles with omake. Will fix make next.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 19:59:28 -0700 (Sun, 06 Jul 2003)
Revision: 4705
Log message:
Added make support for the abstract vars branch.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 21:11:26 -0700 (Sun, 06 Jul 2003)
Revision: 4706
Log message:
Migrated String_util and Mp_debug to libmojave versions.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 14:32:19 -0700 (Mon, 07 Jul 2003)
Revision: 4707
Log message:
Minor fix for the filter_patt stuff.
| Changes | Path |
| +0 -1 | metaprl-branches/abstract_vars/filter/OMakefile |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 14:42:56 -0700 (Mon, 07 Jul 2003)
Revision: 4708
Log message:
make opt should now work, except on theories/tpt, which is still need
to fix.
| Changes | Path |
| +8 -8 | metaprl-branches/abstract_vars/filter/Makefile |
| +1 -1 | metaprl-branches/abstract_vars/mk/preface |
| +1 -1 | metaprl-branches/abstract_vars/theories/tptp/tptp_load.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 14:57:59 -0700 (Mon, 07 Jul 2003)
Revision: 4709
Log message:
More patches for "make opt"
| Changes | Path |
| +2 -11 | metaprl-branches/abstract_vars/editor/ml/Makefile |
| +1 -1 | metaprl-branches/abstract_vars/mk/preface |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 16:02:18 -0700 (Mon, 07 Jul 2003)
Revision: 4710
Log message:
<:con< ... >> syntax:
- for numeric parameters, we can now use syntax $int:expr$, where expr has type int,
instead of having to convert int to num explicitly.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 17:02:56 -0700 (Mon, 07 Jul 2003)
Revision: 4711
Log message:
Moved Array_util to Lm_array_util.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-07 17:07:11 -0700 (Mon, 07 Jul 2003)
Revision: 4712
Log message:
Changed the string representation of variables. The Lm_symbol.add
function will now try to parse a numeric suffix correctly.
The bindings in Filter_util now use strings instead of variables.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 17:30:06 -0700 (Mon, 07 Jul 2003)
Revision: 4713
Log message:
- In Filter_ocaml, dest_var is supposed to return a string.
- Array_util -> Lm_array_util in *.mlz
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 18:58:47 -0700 (Mon, 07 Jul 2003)
Revision: 4714
Log message:
- Added Lm-symbol.make that takes an explicit string and an int.
- The meta-sequent labels are strings, not variables.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 20:10:57 -0700 (Mon, 07 Jul 2003)
Revision: 4715
Log message:
Backported some of the trunk changes back to the branch.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 21:17:18 -0700 (Mon, 07 Jul 2003)
Revision: 4716
Log message:
- Further cleaning up the Lm_symbol.add's
- Made sure that theories/fir and theories/experimental/compile compile
(at least with LIBMOJAVE=undefined) to be able to have a fair performance
comparison with the trunk.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 17:02:43 -0700 (Tue, 08 Jul 2003)
Revision: 4717
Log message:
Minor simplification of the generatod code for level params in <:con< >>
| Changes | Path |
| +1 -3 | metaprl/filter/filter/filter_parse.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-08 18:10:44 -0700 (Tue, 08 Jul 2003)
Revision: 4718
Log message:
This migrates much of the mllib code to libmojave.
Still to go, use Lm_set instead of Red_black_set,
but we'll probably do that after we merge onto the trunk.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 19:05:06 -0700 (Tue, 08 Jul 2003)
Revision: 4719
Log message:
- Removed the MVar parameter. Now the semantics of the variable parameters (Var)
is the following:
a) In the formal (AKA "Strict") mode, users are not allowed to mention variable
parameters explicitly - at all.
b) In the informal (AKA "Relaxed" or "display") mode, variable parameters are
meta-parameters. But if a contractum has a variable parameter that is not present
in the redices, then it is taken literally (e.g., as a constant).
- In the rewriting stack matching (used only for ML display forms), separated
the concrete/meta distinction for parameters from the destinction between the
different kinds of rewrite stack entries. This makes it easy (and natural) to
write ML display forms that distinquish between paramerers and meta-parameters.
- Fixed the proofs that used to rely on distinction between `v1 and `v_1
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 19:59:00 -0700 (Tue, 08 Jul 2003)
Revision: 4720
Log message:
Got rid of RWVar constant parameter. Now Var parameters are _always_
considered to be meta-parameters in informal rewrites.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 20:59:40 -0700 (Tue, 08 Jul 2003)
Revision: 4721
Log message:
A bunch of minor fixes. I think I finally got display forms to work correctly
on the branch.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-08 23:44:51 -0700 (Tue, 08 Jul 2003)
Revision: 4722
Log message:
Revercing the last (branch) change to these files - now that the variable
handling is a little more sane, the existing (trunk) proofs are OK.
| Changes | Path |
| +2100 -2144 | metaprl-branches/abstract_vars/theories/itt/itt_record0.prla |
| +2208 -2101 | metaprl-branches/abstract_vars/theories/itt/itt_sort.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 00:20:04 -0700 (Wed, 09 Jul 2003)
Revision: 4723
Log message:
Merging in the abstract_vars branch:
- variables are now an abstract type, not strings
- MVar parameters are gone
See the branch log messages for more information.
P.S. This is a pretty big change, so I bumped the version number
in mk/preface.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 00:46:42 -0700 (Wed, 09 Jul 2003)
Revision: 4724
Log message:
Minor clean-up.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 01:08:33 -0700 (Wed, 09 Jul 2003)
Revision: 4725
Log message:
- Got rid of the LIBMOJAVE parameted in mk/config (just always use $(ROOT)/libmojave)
- Converted the theories/experimental/compile to be compatible with the current
incarnation of libmojave
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 03:31:26 -0700 (Wed, 09 Jul 2003)
Revision: 4726
Log message:
Got rid of the "arg_subst" part of the tactic_arg - we never used it, and
I do not thing it is likely to be useful in the future.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 03:49:54 -0700 (Wed, 09 Jul 2003)
Revision: 4727
Log message:
Tests needed to be translated to Lm_symbol as well.
| Changes | Path |
| +5 -17 | metaprl/editor/ml/tests/prop-pigeon.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 04:13:12 -0700 (Wed, 09 Jul 2003)
Revision: 4728
Log message:
Simplified some code using the new (larger) libmojave interfaces.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-11 01:54:01 -0700 (Fri, 11 Jul 2003)
Revision: 4729
Log message:
- Changed the ASCII_IO format to be a bit more flexible. This allowed
me to get rid of having to print sequents on two separate (hyps and goals) lines.
For now I had to keep a lot of ugly backwards-compatibility code, but that
can be cleaned up once we have no files in old format (<= 1.0.6) left.
- Moved the file format version information from Filter_cache to Filter_magic,
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-11 12:52:59 -0700 (Fri, 11 Jul 2003)
Revision: 4730
Log message:
Removed some unused code.
| Changes | Path |
| +0 -1 | metaprl/refiner/refsig/term_man_sig.ml |
| +0 -6 | metaprl/refiner/term_ds/term_man_ds.ml |
| +0 -6 | metaprl/refiner/term_gen/term_man_gen.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-11 18:54:10 -0700 (Fri, 11 Jul 2003)
Revision: 4732
Log message:
This migrates the set/map code to libmojave.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-12 14:59:17 -0700 (Sat, 12 Jul 2003)
Revision: 4733
Log message:
Migrated more code into libmojave.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-12 16:53:22 -0700 (Sat, 12 Jul 2003)
Revision: 4734
Log message:
- Made the display_var a properly declared opname instead of a hacked "internal" one.
- Removed generated symlink files from CVS.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-13 03:34:55 -0700 (Sun, 13 Jul 2003)
Revision: 4735
Log message:
Lm_list_util should not inlcude things that already exist in List.
| Changes | Path |
| +1 -1 | metaprl/support/shell/shell_package.ml |
Changes by: ( at unknown.email)
Date: 2003-07-13 03:34:55 -0700 (Sun, 13 Jul 2003)
Revision: 4736
Log message:
This commit was manufactured by cvs2svn to create branch
'bound_contexts'.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-13 15:56:38 -0700 (Sun, 13 Jul 2003)
Revision: 4737
Log message:
This implements most of the context binding and scoping structure (as
required by the semantics of sequent schemas).
Still TODO:
- Make sure that variables in rule arguments are parsed according to the scoping
they have in a rule.
- Make sure that variables in term arguments in top loop are parsed according
to the scoping they have in the current mterm.
- Fix the rules that have ill-specified context restrictions, debug, etc.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-13 18:39:54 -0700 (Sun, 13 Jul 2003)
Revision: 4738
Log message:
Core_type_infer now compiles, though completely untested.
Fixed a dumb dependency bug in OMakefile.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-14 11:00:00 -0700 (Mon, 14 Jul 2003)
Revision: 4739
Log message:
Some minor changes.
Did not change Term_match_table. We'll have to decide if we
want default cases.
Core_type_erase also has an issue with default cases.
Specifically, all types are erased, but all variables
are left wrapped, like erase{'v}. I'm not sure we want
to add a default case.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-15 20:29:36 -0700 (Tue, 15 Jul 2003)
Revision: 4750
Log message:
Moved some of the new functionality from Term_man to Term_meta (for the only
reason - there is only one copy of Term_meta and I do not want to keep implementing
these things twice).
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-15 23:08:33 -0700 (Tue, 15 Jul 2003)
Revision: 4751
Log message:
Added proper parsing for meta-terms and rule/rewrite arguments -- now the
contexts in arguments are deduced base on what goes on in the meta-term.
I was very surprized by how many rules currently allow SO variable in and
out of contexts! Even with some reasonable heuristicts for figuring out the
correct contexts, I still had to specify them manually in many places.
Unfortunately, it seems that the grammar for bound contexts "killed" the nice
grammar for the set types - so now I have to mess some more with the grammar :-(
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-16 00:21:56 -0700 (Wed, 16 Jul 2003)
Revision: 4752
Log message:
The branch finally compiles! Still TODO:
- A lot of debugging (it currently just dies on startup)
- finish pushing the new parsing changes all the way to the parsing of terms in toploop
- fully implement the context restrictions on rule/rewrite arguments (this is
different from how it works in case of rule/rewrite goals since arguments are compiled
by the rewriter out of the scope of those contexts).
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-16 19:25:34 -0700 (Wed, 16 Jul 2003)
Revision: 4753
Log message:
- Moved the find_subterm function from DTactic to TermAddr module (where it can
interact more nicely with sequents and SO variables)
- Term quotations inside resource annotations should now be parsed correctly
(e.g. the bound contexts should be figured based on what they are in the
rule/rewrite statement).
The top-loop now loads correctly! :-) But still raises exceptions on most
basic things (e.g, ls) :-(
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-16 20:22:59 -0700 (Wed, 16 Jul 2003)
Revision: 4754
Log message:
- Made the TermShape module more tolerant (it will return something
semi-reasonable for sequents and variables instead of raising an exception).
- Fixed the variable-related display forms.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-16 23:29:24 -0700 (Wed, 16 Jul 2003)
Revision: 4755
Log message:
Term_addr_ds needs to use get_core and look ate possible cases; simply doing
dest_term is no longer good enough.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-17 00:18:47 -0700 (Thu, 17 Jul 2003)
Revision: 4756
Log message:
Made sure TESTS=YES compiles.
| Changes | Path |
| +0 -1 | metaprl/editor/ml/tests/prop-pigeon.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-17 01:51:37 -0700 (Thu, 17 Jul 2003)
Revision: 4757
Log message:
Rewriter is getting close to working correctly.
| Changes | Path |
| +17 -15 | metaprl-branches/bound_contexts/refiner/rewrite/rewrite_compile_redex.ml |
| +3 -1 | metaprl-branches/bound_contexts/refiner/rewrite/rewrite_match_redex.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-17 02:53:44 -0700 (Thu, 17 Jul 2003)
Revision: 4758
Log message:
Fixed a bunch of places where dest_term was called on "special" terms.
(Note - this should also be a big help for nested sequents support).
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 14:04:59 -0700 (Fri, 18 Jul 2003)
Revision: 4759
Log message:
Added sequent support to pattern matching and explode_term.
explode_term has moved to TermMan, to add support for sequents.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-18 14:48:31 -0700 (Fri, 18 Jul 2003)
Revision: 4760
Log message:
Bound contexts branch:
- Changed the Ascii_IO to use a separate line formal for SO variables (and
added more backward-compatibility code for old format)
- Typeinf now undersdands new SO variables better.
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 19:29:12 -0700 (Fri, 18 Jul 2003)
Revision: 4761
Log message:
Added sequents to <:con< ... >> quotation.
Here's a short summary of syntax:
e ::= sequent [args] { hyps >- con_term list }
args ::= con_term list -- The usual syntax for these terms
hyp ::= <H> | <H[con_terms]>
| <$e$> -- $e$ should be a list of hypothesis terms
| v:con_term
| $v$:con_term
This is the first pass, undoubtly we'll need some tuning.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-20 00:10:47 -0700 (Sun, 20 Jul 2003)
Revision: 4762
Log message:
Implemented the new parsing of SO vars contexts in the MetaPRL top loop -
now for SO variables that are present in the rule/rewrite statements, it
knows which contexts binding to use when input has them omited.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-20 22:14:33 -0700 (Sun, 20 Jul 2003)
Revision: 4764
Log message:
- apply_all (that expand_all, status_all, etc) use should actually chdir
into each item before attempting to interact with it.
- taugh JProver not to mess with free context bindings. The way I did it
might be a little inefficient and hackish, but compared to other hacks in
JProver, this is not too bad IMO.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-21 14:07:07 -0700 (Mon, 21 Jul 2003)
Revision: 4765
Log message:
Better version of apply_all.
| Changes | Path |
| +27 -28 | metaprl-branches/bound_contexts/support/shell/shell.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-21 19:55:13 -0700 (Mon, 21 Jul 2003)
Revision: 4766
Log message:
- Restoring a display form that was missing.
- Switching macro.ml to a more canonical syntax (it seems that the curried
syntax for constructors will not be supported in future versions of OCaml).
| Changes | Path |
| +1 -0 | metaprl/support/display/summary.ml |
| +21 -21 | metaprl/util/macro.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-22 11:08:56 -0700 (Tue, 22 Jul 2003)
Revision: 4767
Log message:
Switched the m-paper from sig-alternate to llncs.
| Changes | Path |
| +1 -1 | metaprl/doc/latex/theories/Makefile |
| +9 -43 | metaprl/doc/latex/theories/m-paper.tex |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-23 18:10:43 -0700 (Wed, 23 Jul 2003)
Revision: 4770
Log message:
I am changing check-status to expect TESTS=yes instead of TESTS=no
In parricular, now the jprover_tests theory will have actual proofs
and the check-status will track their status as well.
| Changes | Path |
| +52 -5 | metaprl/theories/itt/jprover_tests.ml |
| Added | metaprl/theories/itt/jprover_tests.prla |
| Properties | metaprl/theories/itt/jprover_tests.prla |
| +3 -3 | metaprl/util/check-status |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-23 19:49:46 -0700 (Wed, 23 Jul 2003)
Revision: 4771
Log message:
Fixed a JProver bug that I accidentally introduced on July 3, 2001 (jall.ml rev 1.22)
| Changes | Path |
| +4 -16 | metaprl/refiner/reflib/jall.ml |
| +66 -6 | metaprl/theories/itt/jprover_tests.ml |
| +752 -442 | metaprl/theories/itt/jprover_tests.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-23 22:58:21 -0700 (Wed, 23 Jul 2003)
Revision: 4772
Log message:
When going over a theory or theories (status_all/expand_all/etc), throw
away some of the cached resource data after we are done with each item.
This significantly reduces the memory usage of "status_all" and makes it
approx. 3 times faster on Mojave clients.
| Changes | Path |
| +5 -0 | metaprl/refiner/reflib/mp_resource.ml |
| +2 -0 | metaprl/refiner/reflib/mp_resource.mli |
| +71 -73 | metaprl/support/shell/shell.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-24 03:48:53 -0700 (Thu, 24 Jul 2003)
Revision: 4773
Log message:
Fixed another JProver bug (this time - in the ITT decoding of the JProver
proof). I also cleaned up the proofs in those theories where JProver
shortened some proofs.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-24 17:48:00 -0700 (Thu, 24 Jul 2003)
Revision: 4774
Log message:
Simplified some proofs.
| Changes | Path |
| +4873 -5741 | metaprl/theories/czf/czf_itt_axioms.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-24 17:57:47 -0700 (Thu, 24 Jul 2003)
Revision: 4775
Log message:
Fixed a few bugs on the branch.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-24 19:41:19 -0700 (Thu, 24 Jul 2003)
Revision: 4776
Log message:
macro.ml should be compiled with $(OCAMLC), not ocamlc
| Changes | Path |
| +1 -1 | metaprl/util/Makefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-27 17:13:33 -0700 (Sun, 27 Jul 2003)
Revision: 4777
Log message:
Made the assumT's "assumption -> assertion" conversion algorithm a little
smarter.
| Changes | Path |
| +24 -5 | metaprl/refiner/reflib/match_seq.ml |
| +15 -6 | metaprl/refiner/reflib/match_seq.mli |
| +7654 -8880 | metaprl/theories/czf/czf_itt_bool.prla |
| +29 -42 | metaprl/theories/itt/itt_logic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-27 21:52:11 -0700 (Sun, 27 Jul 2003)
Revision: 4778
Log message:
Gave jprover access to all assumptions (as opposed - to a random subset,
as we had it before). This makes things a lot slower, but also a lot
more consistent.
| Changes | Path |
| +3 -3 | metaprl/support/tactics/top_tacticals.ml |
| +9186 -9896 | metaprl/theories/czf/czf_itt_equiv.prla |
| +72 -83 | metaprl/theories/itt/itt_logic.ml |
| +1 -0 | metaprl/theories/itt/itt_logic.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-27 23:50:58 -0700 (Sun, 27 Jul 2003)
Revision: 4779
Log message:
Simplified some of the proofs.
| Changes | Path |
| +3077 -3533 | metaprl/theories/czf/czf_itt_dall.prla |
| +3393 -3311 | metaprl/theories/czf/czf_itt_dexists.prla |
| +728 -1076 | metaprl/theories/czf/czf_itt_eq.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 00:48:10 -0700 (Mon, 28 Jul 2003)
Revision: 4780
Log message:
- Now one can use withT to tell JProver with term to use as a canonical
element of types (JProver presumes all types to be non-empty) instead
of the default << 'v0_jprover >>.
- Killed some of the debugging printouts in JProver.
| Changes | Path |
| +19 -19 | metaprl/refiner/reflib/jall.ml |
| +2 -1 | metaprl/theories/itt/itt_logic.ml |
| +20 -20 | metaprl/theories/itt/jprover_tests.ml |
| +360 -358 | metaprl/theories/itt/jprover_tests.prla |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 17:33:02 -0700 (Mon, 28 Jul 2003)
Revision: 4781
Log message:
Working on reducing the page count for the M paper. Not going too well so far...
Changes by: ( at unknown.email)
Date: 2003-07-28 17:33:02 -0700 (Mon, 28 Jul 2003)
Revision: 4782
Log message:
This commit was manufactured by cvs2svn to create branch
'bound_contexts2'.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 21:41:30 -0700 (Mon, 28 Jul 2003)
Revision: 4783
Log message:
Merged the bound_contexts branch with the latest trunk changes and re-branched.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-29 00:39:03 -0700 (Tue, 29 Jul 2003)
Revision: 4784
Log message:
By default, return all meta-variables (including the SO vars) in the set
of free variables.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-29 20:10:34 -0700 (Tue, 29 Jul 2003)
Revision: 4785
Log message:
Changed itt_logic to use explicit rule calls instead of dT and autoT
(which can have things overridden in other theories).
| Changes | Path |
| +35 -28 | metaprl/theories/itt/itt_logic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-29 20:41:57 -0700 (Tue, 29 Jul 2003)
Revision: 4786
Log message:
Killing the DoubleWeak testing module.
I ran 33 rounds of "make clean/ remove *.prlb/ make opt" (most of those
with DoubleWeak and a few without), in each round starting up MetaPRL
500 times. In all those 33 compilations and >16,000 startups I have not seen
a single instance of the memoizer bug, so it must really be caused by an
incomplete recompilation.
| Changes | Path |
| +0 -59 | metaprl/mllib/weak_memo.ml |
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-07-29 22:11:06 -0700 (Tue, 29 Jul 2003)
Revision: 4787
Log message:
Cosmetic changes: Fixing some spelling mistakes in the
generated comments.
| Changes | Path |
| +6 -6 | metaprl/mk/make_config.sh |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-29 22:20:02 -0700 (Tue, 29 Jul 2003)
Revision: 4788
Log message:
I am getting really close on the branch - 1419 out of 1448 proofs
currently expand correctly.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-30 02:00:11 -0700 (Wed, 30 Jul 2003)
Revision: 4789
Log message:
Minor code clean-up.
| Changes | Path |
| +11 -12 | metaprl/refiner/reflib/unify_mm.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-30 02:03:55 -0700 (Wed, 30 Jul 2003)
Revision: 4790
Log message:
Minor error handling updates.
| Changes | Path |
| +4 -25 | metaprl-branches/bound_contexts2/filter/boot/proof_boot.ml |
| +2 -1 | metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_match_redex.ml |
Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2003-07-30 08:55:55 -0700 (Wed, 30 Jul 2003)
Revision: 4791
Log message:
Fixing a formatting nit-pick in the parsing section, and
correcting a grammar error in the related works section that was
pointed out by one of the reviewers. No good ideas on how to
shorten the M-paper yet.
| Changes | Path |
| +0 -0 | metaprl/theories/experimental/compile/m_doc_parsing.ml |
| +1 -1 | metaprl/theories/experimental/compile/m_doc_summary.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 00:15:10 -0700 (Thu, 31 Jul 2003)
Revision: 4792
Log message:
Two pages down, two to go.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 01:35:25 -0700 (Thu, 31 Jul 2003)
Revision: 4793
Log message:
For some reason, unification code used == instead of = for comparing
constants. Just can't believe this went unnoticed for almost 4 years!
| Changes | Path |
| +3 -3 | metaprl/refiner/reflib/unify_mm.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 02:54:06 -0700 (Thu, 31 Jul 2003)
Revision: 4794
Log message:
Sequent.maybe_new_var should avoid all free variables, not just the ones
declared in the goal sequent.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 03:48:13 -0700 (Thu, 31 Jul 2003)
Revision: 4795
Log message:
Minor fixes.
| Changes | Path |
| +9 -4 | metaprl-branches/bound_contexts2/refiner/reflib/ascii_io.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 06:24:21 -0700 (Thu, 31 Jul 2003)
Revision: 4796
Log message:
expr <--> patt conversions need to be more general.
| Changes | Path |
| +4 -8 | metaprl/filter/base/filter_ocaml.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 13:38:00 -0700 (Thu, 31 Jul 2003)
Revision: 4797
Log message:
*** WARNING ***
*** This check-in breaks .prlb compatibility ***
*** Export any unsaved proofs to .prla ***
*** before running "cvs update" ***
This is a major change in the way meta-variables work. This commit is supposed
to finally bring the implementation of the rewriter into full argeement with
the on-paper semantics of the sequent schema language and make our implementation
fully valid.
This commit makes sequent contexts binding occurrences and makes all meta-variables
(bot SO variables and sequent contexts) explicitly list all the contexts that can
introduce variables that can occur freely in whatever the meta-variable can match.
For example, f<||>[] can only match closed terms, f<|H|>[] can only match terms whose
only free variables (more specifically - free first-order and context variables) are
those introduced by H.
To avoid having to specify contexts explicitly all the time, the following conventions
are observed:
- in a term (on I/O), the maximal possible contexts are presumed. E.g.
sequent{ <H>; x: A; <J['x]> >- C['x] } is now a shortcut for
sequent{ <H<||>>; x: A<|H|>; <J<|H|>['x]> >- C<|J;H|>['x] }
- in a rule (input only), the terms are scanned top-to-bottom (e.g. conclusion,
then assumptions from last to first, then rule arguments, then whatever terms
are mentioned in resource annotations) and the first time each meta-variable occurs,
its contexts are remembered and copied over all other places where it is used without
contexts being explicitly specified.
For example,
sequent { <H>; <J> >- A } --> sequent { <H>; A; <J> >- C }
will get parsed as ... A <|H|> ... A<|H|> ...
but
sequent { <H>; A; <J> >- C } sequent { <H>; <J> >- A }
will get parsed as ... A <|J;H|> ... A<|J;H|> ...
(as will cause the rule to be rejected by the rewriter since the first sequent
now has a free occurrence of H).
- in a top-loop variables in terms are expanded according to the rule being proven.
for example, if a rule has a s-o variable "v<|H;J|>" in it, then when inside such
a rule, <<'v>> will get parsed as << 'v<|H;J|> >> (and it will get parsed as
a f-o variable v in other rules, where v is not used as a s-o variable). Note
that << lambda{v.'v} >> will still get parsed as << lambda{v.'v} >> (e.g. with v
being a f-o variable), not as << lambda{v. 'v<|H;J|> } >>!
This commit also creates a distinction between 0-arity second-order variables and
free first-order variables. For now (to keep some of the old code happy), the
first-oder variables are considered a special case of second-order variables, but
this will (hopefully) soon go away.
Currently, the free variable computations in TermSubsts return the union of all 3
kinds of variables in a term - free context variables, free f-o variables and all
s-o variables. This is not necessarily the best choice from the semantic standpoint,
but it make the implementation easier. Note that an attempt to substitute something
for a context variable or s-o variable, will produce and Invalid_argument exception.
In the term_std and dest_term'ed representation, v<|contexts|>[terms] is represented
as var[v:v]{[contexts]; terms} where [contexts] is an xlist term with f-o variables
as its leafs.
This commit also refreshes half of the .prla (and simplifies a few proofs). This was
necessary to make sure proofs still expand cleanly.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 13:46:27 -0700 (Thu, 31 Jul 2003)
Revision: 4798
Log message:
The previous commit deserves a new version number
| Changes | Path |
| +1 -1 | metaprl/mk/preface |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 19:13:33 -0700 (Thu, 31 Jul 2003)
Revision: 4799
Log message:
- Added an axiom thin_many that allowing thinning a whole range of hyps
at once (including thinning contexts! the new syntax makes the necessary
free variable restrictions expressible) to itt_struct and fol_struct,
deriving the original thin rule from thin_many
- Changed the thinMatchT (that is used by tactics such nthAssumT) to
use thin_many instead of thin
- Changed the Top_tacticals.prefix_thenT to check whether one of the arguments
is idT (and avoid unnecessarily nesting and copying things when it is).
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 20:02:39 -0700 (Thu, 31 Jul 2003)
Revision: 4800
Log message:
Partial fix for bug 38 - "root ()" top-loop command works again now.
| Changes | Path |
| +19 -21 | metaprl/support/shell/shell.ml |
| +0 -1 | metaprl/support/shell/shell_sig.mlz |