/[mojave]/metaprl/theories/itt/itt_well_founded.ml
ViewVC logotype

Log of /metaprl/theories/itt/itt_well_founded.ml

Parent Directory Parent Directory | Revision Log Revision Log


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

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: 5559 byte(s)
Diff to previous 3292
- 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 3292 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 10:25:49 2001 UTC (20 years ago) by nogin
File length: 5560 byte(s)
Diff to previous 3281
*** 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 3281 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 13:56:53 2001 UTC (20 years ago) by nogin
File length: 5541 byte(s)
Diff to previous 3124
The redundant "_resource" suffix should not be used in resource names.


Revision 3124 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 31 22:44:31 2001 UTC (20 years, 4 months ago) by nogin
File length: 5559 byte(s)
Diff to previous 3058
Spelling changes.
For best results, upgrade to http://www.cs.cornell.edu/nogin/RPM/MetaPRL/noarch/words-2.1-1.noarch.html


Revision 3058 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 20:41:19 2000 UTC (20 years, 9 months ago) by jyh
File length: 5567 byte(s)
Diff to previous 3056
Last commit failed partway through...


Revision 3056 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 4 17:09:49 2000 UTC (20 years, 9 months ago) by cwitty
File length: 3895 byte(s)
Diff to previous 3050
Started changing declare/prim_rw to define (as in TODO 2.01.2).
Also fixed an unsoundness in itt_dprod.ml where fst{} had two definitions:

 prim_rw unfoldFst : fst{'e} <--> spread{'e; u, v. 'u}
 prim_rw unfoldSnd : fst{'e} <--> spread{'e; u, v. 'v}


Revision 3050 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 20 01:40:18 2000 UTC (20 years, 10 months ago) by nogin
File length: 4214 byte(s)
Diff to previous 3042
- I added my personal TODO file that contains a list of things
that I am considering doing with/in/about/around MetaPRL

- I fixed the display form modes in ITT!!!
1) I added the except_mode[...] display form option. It is opposite
to the mode[...] option. The main idea was to be able to say
except_mode[src]
2) I made sure all the display forms in ITT (and below it, except for
Ocaml) are annotated with proper mode and except_mode options.
3) I added (in one of the previous commits) the  set_dfmode
command to MetaPRL toploop. Now  set_dfmode "src"  can be used
to produce terms in a form suitable for cutting and pasting into
.ml files and command line tactic arguments.
4) I updated the documentation accordingly.


Revision 3042 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 9 23:54:39 2000 UTC (20 years, 10 months ago) by nogin
File length: 4174 byte(s)
Diff to previous 2775
Got rid of Itt_equal!member.
----------------------------

Now the only way to represent membership in ITT is to use << equals{T;x;x} >>
To avoid extra typing, this can be typed as << x IN T >> (note that "IN" has
to be capitalized here, while in << x=x in T >> it has to be lowercase).

I updated the rules and tactics approprially. I also updated itt_quickref.txt
(Although I have not checked whether the original text was correct and if it was
not, my modifications could also be incorrect).

I reexpanded all the proofs. Most worked correctly, except for the following:
- Some proofs were nonexistant or incomplete even before my changes.
- Itt_fset is very outdated and would not expand without some major effort.
- Many proofs in Itt_collection are broken because of heavy reliance on tatcics
that need term arguments that were broken by the variable naming bug (BUGS 3.11).
I am not sure whether it's the only problem with Itt_collection (probably not).


Revision 2775 - (view) (download) (annotate) - [select for diffs]
Added Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 4186 byte(s)
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.


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