/[mojave]/metaprl/filter/base/filter_cache_fun.ml
ViewVC logotype

Log of /metaprl/filter/base/filter_cache_fun.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: 31045 byte(s)
Diff to previous 3410
- 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 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: 31041 byte(s)
Diff to previous 3322
- 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 3322 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 8 16:12:09 2001 UTC (19 years, 11 months ago) by nogin
File length: 30957 byte(s)
Diff to previous 3278
Use String.concat instead of String_util.concat


Revision 3278 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 20 00:27:36 2001 UTC (20 years ago) by nogin
File length: 30962 byte(s)
Diff to previous 3223
- 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 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: 30933 byte(s)
Diff to previous 3057
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 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: 28852 byte(s)
Diff to previous 3050
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 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: 28635 byte(s)
Diff to previous 3032
- 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 3032 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 25 23:10:51 2000 UTC (20 years, 10 months ago) by jyh
File length: 28620 byte(s)
Diff to previous 3031
Fixed the problem with loading and editing several theories that have common
parents.

Fixed a problem with bytecode make forgetting to do things in filter.


Revision 3031 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 25 17:24:20 2000 UTC (20 years, 11 months ago) by jyh
File length: 28043 byte(s)
Diff to previous 2828
Fixed the problem with loading multiple theories that share
a common theory (BUGS 2.3).  Still have a problem with displaying
terms correctly in the toplevel.


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: 26686 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: 26685 byte(s)
Diff to previous 2785
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 2785 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 5 13:07:54 1999 UTC (21 years, 11 months ago) by jyh
File length: 26713 byte(s)
Diff to previous 2781
Filter creates .prlb file from .prla if it does not exist.
Fixed prec_rel term format that was causing parsing errors when
the .prla file was read.


Revision 2781 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 5 05:40:01 1999 UTC (21 years, 11 months ago) by jyh
File length: 26487 byte(s)
Diff to previous 2775
Filter now reads .prla file even if .prlb file does not exist.


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: 26479 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