ViewVC logotype

Log of /metaprl/theories/tactic/mptop.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: 22584 byte(s)
Diff to previous 3444
- 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 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: 22501 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: 22697 byte(s)
Diff to previous 3294
- 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 3294 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 17:30:44 2001 UTC (20 years ago) by nogin
File length: 21839 byte(s)
Diff to previous 3292
- Corrected precedences in Term_match_table (dforms, dT, etc).
- Mptop now will understand fully qualified names correctly.

Revision 3292 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 10:25:49 2001 UTC (20 years ago) by nogin
File length: 21819 byte(s)
Diff to previous 3278
*** 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 3278 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 00:27:36 2001 UTC (20 years ago) by nogin
File length: 23396 byte(s)
Diff to previous 3086
- Changed the syntax of resource implementation. Now you no longer need to
re-declare resource types in the implementation. Instead of the declaration
and a Mp_resource.create call, use the following syntax in the implementation:

let resource <name> = <expr>

where <expr> is an expression that of the type Mp_resource.info

- Additionally, it is no longer necessary to use _resource in resource names
and resource annotations.

Revision 3086 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 22 20:58:58 2000 UTC (20 years, 8 months ago) by nogin
File length: 23509 byte(s)
Diff to previous 3085
1) Proved some *Formation rules that used to be primitive (using in part
Alexei's cut rule idea). We should probably continue this job and
eliminate "primitiveness" from as much Formation rules as we can.

2) unitSqequal rule should be primitive

3) mk: don't pass -j1 to make when MAKE_JOBS = 1

4) In MP toploop, when a non-negatice integer is found where
an address was expected, that integer is considered to be
the hypothesis number. This enables applying primitive rules
from the MP toploop.

Revision 3085 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 18 21:32:01 2000 UTC (20 years, 8 months ago) by nogin
File length: 23407 byte(s)
Diff to previous 3058
Fixed Yegor's typos that prevented MetaPRL from staring (Yegor, please
take a look at my changes)

Other minor fixes.

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: 23312 byte(s)
Diff to previous 2911
Last commit failed partway through...

Revision 2911 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 24 01:42:53 2000 UTC (21 years, 4 months ago) by jyh
File length: 21399 byte(s)
Diff to previous 2859
Planning for update to .prla files.

Revision 2859 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 22 05:43:56 1999 UTC (21 years, 7 months ago) by nogin
File length: 21370 byte(s)
Diff to previous 2811
Made MetaPRL compatible with ocaml-2.03/camlp4-2.03

At the same time it became incompatible with ocaml-2.02/camlp4-2.02...

Revision 2811 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 3 23:41:50 1999 UTC (21 years, 9 months ago) by jyh
File length: 21374 byte(s)
Diff to previous 2772
Rules are automatically added to mptop toploop.  This just means
that you can use a rule directly in a tactic without having to wrap
it.  Rules require addresses, so they are still hard to use, but
at least they are accessible.

Revision 2772 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 00:42:06 1999 UTC (21 years, 11 months ago) by nogin
File length: 21048 byte(s)
Diff to previous 2743
Small changes

Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 21047 byte(s)
Diff to previous 2630
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).


Revision 2630 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 4 23:35:20 1999 UTC (22 years, 2 months ago) by jyh
File length: 21024 byte(s)
Diff to previous 2629
Added the primitive support for resource improvement through
rule annotations.  There is still no connection with the parser.

Revision 2629 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 4 22:07:38 1999 UTC (22 years, 2 months ago) by jyh
File length: 20938 byte(s)
Diff to previous 2577
This is the first phase for modifying resources.
The Mp_resource interface has been substantially simplified, but
I believe that it retains as much functionality as it did before
the change.

The next step for me to add the Mp_resource support for
adding resources as rule annotations.

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: 22236 byte(s)
Diff to previous 2549
Upgraded to OCaml 2.01.

Revision 2549 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 1 20:14:13 1999 UTC (22 years, 5 months ago) by jyh
File length: 22187 byte(s)
Diff to previous 2525
Fixed up "make clean" to remove more files.
The directory should be like a new checkout afterwards.
Enabled set_debug function in toploop.  You can
turn on debugging with

# set_debug "xxx" true;;

for some debug variable xxx.

Revision 2525 - (view) (download) (annotate) - [select for diffs]
Modified Mon Dec 28 21:07:52 1998 UTC (22 years, 5 months ago) by jyh
File length: 22187 byte(s)
Diff to previous 2502
Numerous minor changes.

Added itt_fset: a theory of finite sets based on a list
implementation quotiented by equivalence under arbitrary
occurrences and ordering.

Added initial reflection theory.  Terms are quotiented by
alpha-equality, so normal well-formedness proofs are difficult,
and more work needs to be done to define free variables and

Revision 2502 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 09:01:06 1998 UTC (22 years, 8 months ago) by nogin
File length: 21805 byte(s)
Diff to previous 2494
More NL -> MP changes

Revision 2494 - (view) (download) (annotate) - [select for diffs]
Added Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 21805 byte(s)
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.

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