/[mojave]/metaprl/theories/tactic/tactic_cache.ml
ViewVC logotype

Log of /metaprl/theories/tactic/tactic_cache.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 4538)

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 2 months ago) by nogin
File length: 67645 byte(s)
Diff to previous 3532
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.


Revision 3532 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 10 23:29:54 2002 UTC (19 years, 3 months ago) by nogin
File length: 67648 byte(s)
Diff to previous 3444
I am committing David Bustos' changes to the cons build system for Metaprl.

See David's message "cons for MetaPRL" in the newsgroup for more information -
news://news.metaprl.org:119/20020310131332.A13595@wink.caltech.edu


Revision 3444 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 15 23:03:47 2001 UTC (19 years, 7 months ago) by nogin
File length: 67672 byte(s)
Diff to previous 3410
Code cleanup:

I looked (using the code I've put into macro.ml) for places where the same code
appeared in several branches of a match or function expression. I changed those
places to use a complex pattern and a single copy of the code.


Revision 3410 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 25 16:52:43 2001 UTC (19 years, 8 months ago) by nogin
File length: 67690 byte(s)
Diff to previous 3292
- Merged the Ocaml 3.02 changes

- Now http server is compiled in by default, but is only started if
the "-http true" argument is passed or MP_HTTP environment variable
is set to "true".

- A few other minor changes.


Revision 3292 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 10:25:49 2001 UTC (20 years ago) by nogin
File length: 67666 byte(s)
Diff to previous 2993
*** IMPORTANT: before doing "cvs update" see warning below ***

This commit implements a global resource that brings together resource management
that used to be done by each resource in its own way.

- A much simplier object (Mp_resource.resource_info) is now needed to create a new resource.
Additionally, many resource helper modules, such as term_match_table now provide functions
that create a resource_info for you.

- Funtions get_tactic_arg, get_int_tactic_arg, etc were replaced by a single function
get_resource_arg (note: functions for basci types, such as get_with_arg, get_sel_args, etc
were _not_ affected)

- Resource declaration statement now declares and resource creation statement now creates
a function get_<name>_resource. This function ca be passed as a second argument
to get_resource_arg to retrieve the current value of a particular resource.

- Resource annotation functions are now separate from the resource declaration/creation
mechanism. Resource annotation on a rule are now passed to a function named
process_<name>_resource_annotation. This function must have the appropriate
Mp_resource.annotation_processor type for the resource. This function can be declared
and implemented in _any_ module, not just the module that declares and creates the
<name> resource.

- Currenlty MetaPRL leaves it to Ocaml to keep track of these functions.
Consequently the module that defines the process_<name>_resource_annotation function
must be open'ed (not included!) by modules that use <name> annotations.

-----

Unfinished business in this commit:
- Remainder of TODO 1.12 and 1.13

- Some proofs were broken by this commit. It appears that they were broken for
a "good" reason, but still need to be fixed.

- I need to make sure things now always have the right precedences (all things being equal,
the later an item is added to resource, the earlier precedence it should have).

- Consider adding refiner sentinels and display forms to global resource as well.
Currently each of them still does its own way of resource management (although the way
display forms are managed was changed by this commit - need to make sure the precedences
are right).

- Distributed refinement: I am afraid that the current resource code
will either work correctly only if all processes in the distributed group have
the same global resource, or it will attempt to pass around all the resource data.
Obviously, neither of these choices is a good one.

*** WARNING ***

This commit changes the tactic_arg type and also makes minor changes in
the FilterCache.info type. Because of that old .prlb and .cmoz files
*will no longer work*. Old .prla files will work, but will produce lots
of (harmless) Filter_summary.dest_term warning.

Before doing "cvs update" do the following:
1) export all your unsaved proofs into .prla files.
2) rm -f theories/*/*.prlb
3) run "make clean"


Revision 2993 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 26 19:57:46 2000 UTC (21 years ago) by nogin
File length: 67947 byte(s)
Diff to previous 2883
 - Fixed a nasty bug in Term_ds.subst - it didn't notice when the same variable
was mentioned several times in the substitution with different terms substituted
for it. This made it possible to break Term_ds invariants leading to all kinds of
strange behaviour.

 - Changed the argument order for "subst" to be more natural

 - Added a subst1 function to substitute for a single variable without having
to put the substitution into a singleton list.

 - Added the resource annotations and updated the rest of the resource code
in CZF so that it now compiles (but I didn't try to expand anything).


Revision 2883 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 16 00:31:35 2000 UTC (21 years, 4 months ago) by nogin
File length: 67947 byte(s)
Diff to previous 2822
Enabled the "strict" rewriter mode.

In "strict" mode, <<lambda{x.'t}>> will only match terms where "t" does not contain
free occurences of "x" while <<lambda{x.'t['x]}>> will match any lambda expression.
In "relaxed" mode both redices will match any lambda expression.

This is done
1) To force rule authors to completely specify the binding structure
2) To allow rule authors to specify free variables restrictions easier

refiner/refiner/refine.ml, filter/boot/rewrite_boot.ml and theories/tactic/tactic_cache.ml
use the strict mode.

filter/base/filter_prog.ml uses relaxed mode for d.f. and compiles ml rewrites
using the strict mode

refiner/reflib/dform.ml, refiner/reflib/term_dtable.ml and refiner/reflib/term_match_table.ml
use the relaxed mode.

Please let me know if this change breaks something.


Revision 2822 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 22 01:07:59 1999 UTC (21 years, 8 months ago) by nogin
File length: 67926 byte(s)
Diff to previous 2652
Added new function to mp_debug
let show_loading s = if !debug_load then Printf.eprintf s eflush

and replaced all usages of debug_load with show_loading


Revision 2652 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 13 23:18:29 1999 UTC (22 years, 1 month ago) by kopylov
File length: 67954 byte(s)
Diff to previous 2577
1) Added a bug list into BUGS

2) Changed the keywords:
axiom -> rule  (.mli files)
primrw -> prim_rw  (.ml files)
rwthm -> thm_rw  (.ml files)

3) Fixed the rule Itt_struct.hypSubstitution


Revision 2577 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 28 18:44:05 1999 UTC (22 years, 4 months ago) by jyh
File length: 67968 byte(s)
Diff to previous 2494
Upgraded to OCaml 2.01.


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 67923 byte(s)
Diff to previous 2456
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2456 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 22:31:37 1998 UTC (22 years, 9 months ago) by jyh
File length: 67927 byte(s)
Diff to previous 2347
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.


Revision 2347 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 23 18:40:34 1998 UTC (22 years, 11 months ago) by nogin
File length: 66768 byte(s)
Diff to previous 2337
Moved eseqent type to the TermType module.
Made the types of esequent components hidden to make them read-only.


Revision 2337 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 22 00:34:42 1998 UTC (22 years, 11 months ago) by jyh
File length: 66714 byte(s)
Diff to previous 2336
Removed dest_sequent, and changed Term_man_sig.esequent to use arrays.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 11 months ago) by jyh
File length: 66807 byte(s)
Diff to previous 2318
Added NL toploop so that we can compile NL native code.


Revision 2318 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 9 00:35:42 1998 UTC (22 years, 11 months ago) by nogin
File length: 66804 byte(s)
Diff to previous 2307
Do not allocate a cons cell before calling apply_rewrite or apply_redex -
use an extra argument instead.


Revision 2307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 17:55:31 1998 UTC (22 years, 11 months ago) by nogin
File length: 66475 byte(s)
Diff to previous 2284
Removed $Log messages from all NL files.


Revision 2284 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 22:25:40 1998 UTC (22 years, 11 months ago) by jyh
File length: 68388 byte(s)
Diff to previous 2280
Created term_copy module to copy and normalize terms.


Revision 2280 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 1 04:38:04 1998 UTC (22 years, 11 months ago) by nogin
File length: 68249 byte(s)
Diff to previous 2224
Moved Refiner exceptions into a separate module RefineErrors


Revision 2224 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 12 13:47:49 1998 UTC (23 years ago) by jyh
File length: 68103 byte(s)
Diff to previous 2222
D tactic works, added itt_bool.


Revision 2222 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 9 20:53:04 1998 UTC (23 years ago) by jyh
File length: 68030 byte(s)
Diff to previous 2209
Propagated refinement changes.
New tacticals module.


Revision 2209 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 13:57:13 1998 UTC (23 years ago) by jyh
File length: 61579 byte(s)
Diff to previous 2190
Proving twice one is two.


Revision 2190 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 13:48:44 1998 UTC (23 years ago) by jyh
File length: 61750 byte(s)
Diff to previous 2171
Updated the editor to use new Refiner structure.
ITT needs dform names.


Revision 2171 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 7 16:03:13 1998 UTC (23 years, 1 month ago) by jyh
File length: 61564 byte(s)
Diff to previous 2159
Adding interactive proofs.


Revision 2159 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 29 14:50:25 1998 UTC (23 years, 1 month ago) by jyh
File length: 60626 byte(s)
Diff to previous 2152
Added ocaml_sos.


Revision 2152 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 24 02:44:07 1998 UTC (23 years, 2 months ago) by jyh
File length: 60523 byte(s)
Diff to previous 2146
Added more extensive debugging capabilities.


Revision 2146 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 21 20:58:10 1998 UTC (23 years, 2 months ago) by jyh
File length: 60302 byte(s)
Diff to previous 2108
Fixed typing problems introduced by refiner msequents.


Revision 2108 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 8 15:08:37 1998 UTC (23 years, 2 months ago) by jyh
File length: 60199 byte(s)
Diff to previous 2107
Moved precedence to mllib.


Revision 2107 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 8 14:57:37 1998 UTC (23 years, 2 months ago) by jyh
File length: 60125 byte(s)
Diff to previous 2032
ImpDag is in mllib.


Revision 2032 - (view) (download) (annotate) - [select for diffs]
Added Mon Apr 28 15:52:46 1997 UTC (24 years, 1 month ago) by jyh
File length: 60060 byte(s)
This is the initial checkin of Nuprl-Light.
I am porting the editor, so it is not included
in this checkin.

Directories:
    refiner: logic engine
    filter: front end to the Ocaml compiler
    editor: Emacs proof editor
    util: utilities
    mk: Makefile templates


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26