/[mojave]/metaprl/refiner/reflib/dform.ml
ViewVC logotype

Log of /metaprl/refiner/reflib/dform.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

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: 23194 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: 22751 byte(s)
Diff to previous 3240
*** 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 3240 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 28 22:16:27 2001 UTC (20 years ago) by nogin
File length: 23243 byte(s)
Diff to previous 3223
Use terminal width for output in a more consistent manner.


Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 23177 byte(s)
Diff to previous 3222
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)


Revision 3222 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 22:00:34 2001 UTC (20 years, 1 month ago) by nogin
File length: 22877 byte(s)
Diff to previous 3221
- Fixed slot["raw", ...]
- Fixed couple small typos.


Revision 3221 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 19:50:28 2001 UTC (20 years, 1 month ago) by nogin
File length: 22851 byte(s)
Diff to previous 3219
Disallow changing parameter types in rewriter.


Revision 3219 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 16:32:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 23339 byte(s)
Diff to previous 3215
I accidentally disabled the code that was creating display forms - fixed.


Revision 3215 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 7 22:04:01 2001 UTC (20 years, 1 month ago) by nogin
File length: 23319 byte(s)
Diff to previous 3213
Pass the "strictness" flag to compile_contractum too, not just compile_redex.
For now, the compile_contractum is not using it.


Revision 3213 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 6 22:31:55 2001 UTC (20 years, 1 month ago) by nogin
File length: 23262 byte(s)
Diff to previous 3057
- Rformat now will use no more than 1/3 of the total width on the left tabs.

- I've added the short_string_of_term function to Simple_print that creates
a string of the length at most 120. More importantly, it aborts printing
as soone as it hits the margin, so no matter how big the term is, it should
work fast.

- debug_dform debugging now uses the short_string_of_term, so it will now
hopefully produce managable output even on big terms.


Revision 3057 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 18:26:37 2000 UTC (20 years, 9 months ago) by jyh
File length: 23238 byte(s)
Diff to previous 3046
This jumbo update is a documentation update.  There are no
logical changes.  I did two things:

1. First, comments that begin with the sequence "(*!" are
   interpreted as structured comments.  The contents are parsed
   as terms, and the comments will display in the editor window.
   The comments may contain arbitrary text, as usual, and they
   can also contain explicit terms.  The syntax for terms is:

   @opname[p1, ..., pn]{t1; ...; tm}

   or there is an alternate syntax:

   @begin[opname, p1, ..., pn]
   arg
   @end[opname]

   Text sequences count as a single term.  So, for instance, the
   term @bf{Hello world} display the "Hello world" text in a bold
   font.

   The "doc" term is used for text that is considered to be
   documentation.  There is a set of LaTeX-like terms that you can
   use to produce good-looking documentation.  These are all
   documented in the theories/tactic/comment.ml module.  The exact
   syntax of structured comments is defined in the
   mllib/comment_parse.mll file.  You can also look at any of the
   module in the theories/itt directory if you want to see examples.

   You can generate a pritable version of documentation with the
   print_theory command in the editor.  For example, the command

   # print_theory "itt_equal";;

   produces a file called output.tex that can be formatted with
   your favorite version of latex2e.  You can also generate a
   manule of all the theories by running "make tex" in the
   editor/ml directory.  Or you can run "make" in the
   doc/latex/theories directory.

   The files are hyperlinked, and they contain a table of contents
   and an index.  The preferred reader is acrobat, and the preferred
   formatter is pdflatex.

2. Second, I documented the tactic, base, itt, and czf theories.

3. Oh, and I also added a spelling checker:)  You can turn on the
   spelling checker with the -debug spell option or MP_DEBUG=spell.
   If prlc thinks that your files contain spelling mistakes, it will
   print them out and abort.  You can fix this problem by 1) fixing
   the spelling error, 2) adding the words withing a @spelling{words}
   term in a comment, or adding the words to you .ispell_english
   directory.

   For example, we could either do this:

   @begin[spelling]
   Aleksey Nogin
   @end[spelling]

   Or we could just add Alexey to either $cwd/.ispell_english, or
   ~/.ispell_english.

   The spell checker uses /usr/dict/words as a database, which it
   compiles to a hashtable in /tmp/metaprl-spell-$USER.dat.  Don't
   worry about the tmp file, it is generated automatically.


Revision 3046 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 14 04:23:46 2000 UTC (20 years, 10 months ago) by nogin
File length: 22412 byte(s)
Diff to previous 3034
Fixed the display form order - now the newer display form takes priority over
an older one instead of the other way around. This make it possible to overwrite
a standard display form with a theory-specific one (for example, itt_sort overwrites
the display form for Itt_list!list_ind).


Revision 3034 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 26 02:10:31 2000 UTC (20 years, 10 months ago) by nogin
File length: 22215 byte(s)
Diff to previous 2883
debug_base display form base should be in Dform, not in Proof_boot.Proof


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: 22183 byte(s)
Diff to previous 2828
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 2828 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 26 22:14:51 1999 UTC (21 years, 7 months ago) by nogin
File length: 22175 byte(s)
Diff to previous 2822
Renamed break -> hbreak (dforms construction) to be more consistent.


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: 22168 byte(s)
Diff to previous 2809
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 2809 - (view) (download) (annotate) - [select for diffs]
Modified Tue Aug 31 17:31:53 1999 UTC (21 years, 9 months ago) by jyh
File length: 22196 byte(s)
Diff to previous 2799
Display changes to get Java to work a little better.


Revision 2799 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 23 00:24:57 1999 UTC (21 years, 11 months ago) by nogin
File length: 20775 byte(s)
Diff to previous 2743
Now one can use SO variables in display form specifications


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 20773 byte(s)
Diff to previous 2669
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.

Changes:
   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
      otherwise.

   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).

Jason


Revision 2669 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 23 21:55:17 1999 UTC (22 years, 1 month ago) by jyh
File length: 20807 byte(s)
Diff to previous 2668
This is a major modification to how parameters are handled.
1. All level parmeters are now meta.  That is, univ[@i:l] is
   exactly the same as univ[i:l].  The rewriter handles
   lavel expressions, so matching with levels like
   univ[3 | i':l | j:l] should work correctly.

   The syntax still requires the @ for meta-parameter of
   other types.  For instance, token["hello world":t] is
   a normal token, and token[@"hello world":t] is a
   token with a meta-parameter.

2. There are no more parameter expressions.  For instance,
   the term natural_number[@i + @j] is not valid anymore.
   To replace them, the module theories/base/base_meta.ml
   defines ML rewrites that implement the same functionality.
   For example,
      meta_sum{number[12]; number[5]} --> number[17]

3. There is no term natural_number[@i:n] any more.  This was
   always a bad name, since it has always been possible for the
   parameter to be negative.

4. The Itt_equal.cumulativity rule is no longer defined as a
   side-condition.  It now uses Base_meta.meta_lt to define
   inclusion on level expression.  Cumulativity expansion
   should be performed automatically by the dT tactic.
   So:
      sequent ['ext] { ... >- univ[@i:l] = univ[@i:l] in univ[@j:l] }
      BY dT 0
   should always either succeed or fail, without producing
   subgoals.

I haven't fully tested the side-conditions.  As usual, let me know
if you see anything strange.  Next, I'm looking at the
rewriter free variable soundness problem.


Revision 2668 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 23 00:00:51 1999 UTC (22 years, 1 month ago) by jyh
File length: 20788 byte(s)
Diff to previous 2626
Added ML side-conditions, so that rewrites and rules can be defined
with ML code in the really necessary cases.  The ml_rw keyword
declares/defines an ML rewrite, and ml_rule declares/defines
an rule application defined in ML.


Revision 2626 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 4 05:24:42 1999 UTC (22 years, 2 months ago) by nogin
File length: 20785 byte(s)
Diff to previous 2528
Added MetaLabeled of string * meta_term variant to meta_term type

Ml_format.print_term would raise an exception when given meta_term -
I could not figure out what is supposed to go there.

In filter_simmary in functions meta_term_of_term and term_of_meta_term
MetaLabeled (l, t) is encoded as   meta_labeled [String l] (t)


Revision 2528 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 29 20:14:09 1998 UTC (22 years, 5 months ago) by jyh
File length: 20582 byte(s)
Diff to previous 2494
Added "kreitz" command to fold up an entire proof subtree into a single node.


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: 20540 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: 20544 byte(s)
Diff to previous 2376
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 2376 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 31 14:35:45 1998 UTC (22 years, 10 months ago) by jyh
File length: 19385 byte(s)
Diff to previous 2356
Added TPTP theory, and Ensemble library.  Fixed sequent displays.
BUG: rewrites fail on sequents.


Revision 2356 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 24 21:11:12 1998 UTC (22 years, 11 months ago) by nogin
File length: 19058 byte(s)
Diff to previous 2338
Functorized the Simple_print module over the Refiner module


Revision 2338 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 22 01:58:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 19046 byte(s)
Diff to previous 2336
Changed opname equality.  Opnames should be compared with
the function Opname.eq.


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: 19037 byte(s)
Diff to previous 2333
Added NL toploop so that we can compile NL native code.


Revision 2333 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 17 15:39:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 19034 byte(s)
Diff to previous 2325
CZF is complete, although we may wish to add pairing and inf.


Revision 2325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 14 15:44:03 1998 UTC (22 years, 11 months ago) by jyh
File length: 18996 byte(s)
Diff to previous 2307
Intermediate version with auto tactic.


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: 18586 byte(s)
Diff to previous 2283
Removed $Log messages from all NL files.


Revision 2283 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 18:38:08 1998 UTC (22 years, 11 months ago) by jyh
File length: 20706 byte(s)
Diff to previous 2244
Refiner modules now raise RefineError exceptions directly.
Modules in this revision have two versions: one that raises
verbose exceptions, and another that uses a generic exception.


Revision 2244 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 15 22:33:52 1998 UTC (23 years ago) by jyh
File length: 20440 byte(s)
Diff to previous 2226
Added CZF.


Revision 2226 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 12 18:36:50 1998 UTC (23 years ago) by jyh
File length: 20361 byte(s)
Diff to previous 2209
Working factorial proof.


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


Revision 2191 - (view) (download) (annotate) - [select for diffs]
Added Thu May 28 15:02:46 1998 UTC (23 years ago) by jyh
File length: 19658 byte(s)
Partitioned refiner into subdirectories.


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