Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-06-22 21:50:29 -0700 (Tue, 22 Jun 1999)
Revision: 2743
Log message:

      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
      

Changes  Path
+1 -1 metaprl/Makefile
Deleted metaprl/editor/java/ActiveApplet.java
Deleted metaprl/editor/java/ActiveApplication.java
Deleted metaprl/editor/java/BoundTerm.java
Deleted metaprl/editor/java/Closure.java
Deleted metaprl/editor/java/DebugFlags.java
Deleted metaprl/editor/java/DisplayDynamic.java
Deleted metaprl/editor/java/DisplayEngine.java
Deleted metaprl/editor/java/DisplayTerm.java
Deleted metaprl/editor/java/Eval.java
Deleted metaprl/editor/java/EvalError.java
Deleted metaprl/editor/java/FontBase.java
Deleted metaprl/editor/java/FreeVar.java
Deleted metaprl/editor/java/GateSequence.java
Deleted metaprl/editor/java/ImageView.java
Added metaprl/editor/java/InText.java
Properties metaprl/editor/java/InText.java
Deleted metaprl/editor/java/IntStack.java
Deleted metaprl/editor/java/LevelExp.java
Deleted metaprl/editor/java/LevelVar.java
Deleted metaprl/editor/java/Lexer.java
Deleted metaprl/editor/java/LispExpression.java
Deleted metaprl/editor/java/LispParser.java
Deleted metaprl/editor/java/LispSExpression.java
Deleted metaprl/editor/java/LispSoApply.java
Deleted metaprl/editor/java/LispVar.java
Deleted metaprl/editor/java/Makefile
Deleted metaprl/editor/java/MatchError.java
Deleted metaprl/editor/java/Matching.java
Added metaprl/editor/java/ModeLine.java
Properties metaprl/editor/java/ModeLine.java
Deleted metaprl/editor/java/NetscapeApplet.java
Binary metaprl/editor/java/Nuprl.dsp
Binary metaprl/editor/java/Nuprl.dsw
Deleted metaprl/editor/java/Nuprl.java
Added metaprl/editor/java/Nuprl.man
Properties metaprl/editor/java/Nuprl.man
Binary metaprl/editor/java/Nuprl.opt
Binary metaprl/editor/java/Nuprl.plg
Added metaprl/editor/java/NuprlArgumentToken.java
Properties metaprl/editor/java/NuprlArgumentToken.java
Added metaprl/editor/java/NuprlAuthorization.java
Properties metaprl/editor/java/NuprlAuthorization.java
Added metaprl/editor/java/NuprlBus.java
Properties metaprl/editor/java/NuprlBus.java
Added metaprl/editor/java/NuprlBusClient.java
Properties metaprl/editor/java/NuprlBusClient.java
Added metaprl/editor/java/NuprlBusEndpoint.java
Properties metaprl/editor/java/NuprlBusEndpoint.java
Added metaprl/editor/java/NuprlBusMessage.java
Properties metaprl/editor/java/NuprlBusMessage.java
Added metaprl/editor/java/NuprlBusPort.java
Properties metaprl/editor/java/NuprlBusPort.java
Added metaprl/editor/java/NuprlClient.java
Properties metaprl/editor/java/NuprlClient.java
Added metaprl/editor/java/NuprlCommand.java
Properties metaprl/editor/java/NuprlCommand.java
Added metaprl/editor/java/NuprlCommandToken.java
Properties metaprl/editor/java/NuprlCommandToken.java
Added metaprl/editor/java/NuprlConstants.java
Properties metaprl/editor/java/NuprlConstants.java
Added metaprl/editor/java/NuprlContext.java
Properties metaprl/editor/java/NuprlContext.java
Added metaprl/editor/java/NuprlControl.java
Properties metaprl/editor/java/NuprlControl.java
Added metaprl/editor/java/NuprlControlToken.java
Properties metaprl/editor/java/NuprlControlToken.java
Added metaprl/editor/java/NuprlDataToken.java
Properties metaprl/editor/java/NuprlDataToken.java
Added metaprl/editor/java/NuprlDebug.java
Properties metaprl/editor/java/NuprlDebug.java
Added metaprl/editor/java/NuprlEscapedToken.java
Properties metaprl/editor/java/NuprlEscapedToken.java
Added metaprl/editor/java/NuprlException.java
Properties metaprl/editor/java/NuprlException.java
Added metaprl/editor/java/NuprlFrame.java
Properties metaprl/editor/java/NuprlFrame.java
Added metaprl/editor/java/NuprlHost.java
Properties metaprl/editor/java/NuprlHost.java
Added metaprl/editor/java/NuprlHyperlinkToken.java
Properties metaprl/editor/java/NuprlHyperlinkToken.java
Binary metaprl/editor/java/NuprlIcon.dsp
Deleted metaprl/editor/java/NuprlIcon.java
Binary metaprl/editor/java/NuprlIcon.plg
Added metaprl/editor/java/NuprlInternalFrame.java
Properties metaprl/editor/java/NuprlInternalFrame.java
Added metaprl/editor/java/NuprlLogin.java
Properties metaprl/editor/java/NuprlLogin.java
Added metaprl/editor/java/NuprlManager.java
Properties metaprl/editor/java/NuprlManager.java
Added metaprl/editor/java/NuprlMenu.java
Properties metaprl/editor/java/NuprlMenu.java
Added metaprl/editor/java/NuprlOptionBlockToken.java
Properties metaprl/editor/java/NuprlOptionBlockToken.java
Added metaprl/editor/java/NuprlOptionRequestToken.java
Properties metaprl/editor/java/NuprlOptionRequestToken.java
Added metaprl/editor/java/NuprlOptionResponseToken.java
Properties metaprl/editor/java/NuprlOptionResponseToken.java
Added metaprl/editor/java/NuprlOptionSBToken.java
Properties metaprl/editor/java/NuprlOptionSBToken.java
Added metaprl/editor/java/NuprlOptionToken.java
Properties metaprl/editor/java/NuprlOptionToken.java
Added metaprl/editor/java/NuprlPrlToken.java
Properties metaprl/editor/java/NuprlPrlToken.java
Added metaprl/editor/java/NuprlProof.java
Properties metaprl/editor/java/NuprlProof.java
Added metaprl/editor/java/NuprlSyncToken.java
Properties metaprl/editor/java/NuprlSyncToken.java
Binary metaprl/editor/java/NuprlTerm.dsp
Deleted metaprl/editor/java/NuprlTerm.java
Binary metaprl/editor/java/NuprlTerm.plg
Added metaprl/editor/java/NuprlText.java
Properties metaprl/editor/java/NuprlText.java
Added metaprl/editor/java/NuprlText.java.new
Properties metaprl/editor/java/NuprlText.java.new
Added metaprl/editor/java/NuprlToken.java
Properties metaprl/editor/java/NuprlToken.java
Added metaprl/editor/java/NuprlTokenInputStream.java
Properties metaprl/editor/java/NuprlTokenInputStream.java
Added metaprl/editor/java/NuprlURLToken.java
Properties metaprl/editor/java/NuprlURLToken.java
Deleted metaprl/editor/java/Operator.java
Deleted metaprl/editor/java/Opname.java
Added metaprl/editor/java/OutText.java
Properties metaprl/editor/java/OutText.java
Deleted metaprl/editor/java/Param.java
Deleted metaprl/editor/java/ParamLevelExp.java
Deleted metaprl/editor/java/ParamMDiff.java
Deleted metaprl/editor/java/ParamMEqual.java
Deleted metaprl/editor/java/ParamMLessThan.java
Deleted metaprl/editor/java/ParamMLevel.java
Deleted metaprl/editor/java/ParamMNotEqual.java
Deleted metaprl/editor/java/ParamMNumber.java
Deleted metaprl/editor/java/ParamMPair.java
Deleted metaprl/editor/java/ParamMProduct.java
Deleted metaprl/editor/java/ParamMQuotient.java
Deleted metaprl/editor/java/ParamMRem.java
Deleted metaprl/editor/java/ParamMString.java
Deleted metaprl/editor/java/ParamMSum.java
Deleted metaprl/editor/java/ParamMToken.java
Deleted metaprl/editor/java/ParamMVar.java
Deleted metaprl/editor/java/ParamMatchError.java
Deleted metaprl/editor/java/ParamMeta.java
Deleted metaprl/editor/java/ParamNumber.java
Deleted metaprl/editor/java/ParamString.java
Deleted metaprl/editor/java/ParamToken.java
Deleted metaprl/editor/java/ParamVar.java
Added metaprl/editor/java/PromptPasswordRecognizer.java
Properties metaprl/editor/java/PromptPasswordRecognizer.java
Added metaprl/editor/java/PromptRecognizer.java
Properties metaprl/editor/java/PromptRecognizer.java
Added metaprl/editor/java/PromptUserRecognizer.java
Properties metaprl/editor/java/PromptUserRecognizer.java
Deleted metaprl/editor/java/QuickSort.java
Deleted metaprl/editor/java/Rewrite.java
Deleted metaprl/editor/java/Semaphore.java
Deleted metaprl/editor/java/SmallScrollGroup.java
Deleted metaprl/editor/java/Sort.java
Added metaprl/editor/java/StringBooleanFunction.java
Properties metaprl/editor/java/StringBooleanFunction.java
Added metaprl/editor/java/StringIntFunction.java
Properties metaprl/editor/java/StringIntFunction.java
Added metaprl/editor/java/StringTokenizer.java
Properties metaprl/editor/java/StringTokenizer.java
Deleted metaprl/editor/java/Subst.java
Deleted metaprl/editor/java/SubstParam.java
Deleted metaprl/editor/java/SubstSimul.java
Deleted metaprl/editor/java/SubstSingle.java
Added metaprl/editor/java/Target.java
Properties metaprl/editor/java/Target.java
Deleted metaprl/editor/java/Term.java
Deleted metaprl/editor/java/TermBreak.java
Deleted metaprl/editor/java/TermDisplay.java
Deleted metaprl/editor/java/TermFont.java
Deleted metaprl/editor/java/TermLexer.java
Deleted metaprl/editor/java/TermNuprl.java
Deleted metaprl/editor/java/TermParser.java
Deleted metaprl/editor/java/TermPop.java
Deleted metaprl/editor/java/TermPush.java
Deleted metaprl/editor/java/TermSoApply.java
Deleted metaprl/editor/java/TermSoVar.java
Deleted metaprl/editor/java/TermString.java
Deleted metaprl/editor/java/TermVar.java
Deleted metaprl/editor/java/TermView.java
Deleted metaprl/editor/java/TermZone.java
Deleted metaprl/editor/java/TextBuffer.java
Deleted metaprl/editor/java/TextViewBuffer.java
Deleted metaprl/editor/java/Token.java
Added metaprl/editor/java/TtyArea.java
Properties metaprl/editor/java/TtyArea.java
Deleted metaprl/editor/java/controller.html
Deleted metaprl/editor/java/frameset.html
Binary metaprl/editor/java/images/back.gif
Binary metaprl/editor/java/images/back_gray.gif
Binary metaprl/editor/java/images/back_press.gif
Binary metaprl/editor/java/images/background.gif
Binary metaprl/editor/java/images/background41.gif
Binary metaprl/editor/java/images/background_dark.gif
Binary metaprl/editor/java/images/forward.gif
Binary metaprl/editor/java/images/forward_gray.gif
Binary metaprl/editor/java/images/forward_press.gif
Binary metaprl/editor/java/images/gate_1.jpg
Binary metaprl/editor/java/images/gate_2.jpg
Binary metaprl/editor/java/images/gate_3.jpg
Binary metaprl/editor/java/images/gate_4.jpg
Binary metaprl/editor/java/images/gate_5.jpg
Binary metaprl/editor/java/images/gate_6.jpg
Binary metaprl/editor/java/images/gate_7.jpg
Binary metaprl/editor/java/images/gate_8.jpg
Binary metaprl/editor/java/images/gate_9.jpg
Binary metaprl/editor/java/images/home.gif
Binary metaprl/editor/java/images/home_gray.gif
Binary metaprl/editor/java/images/home_press.gif
Added metaprl/editor/java/images/image1.gif
Properties metaprl/editor/java/images/image1.gif
Binary metaprl/editor/java/images/info.gif
Binary metaprl/editor/java/images/key.gif
Binary metaprl/editor/java/images/mkdir.gif
Binary metaprl/editor/java/images/mkdir_gray.gif
Binary metaprl/editor/java/images/mkdir_press.gif
Binary metaprl/editor/java/images/turn_close.gif
Binary metaprl/editor/java/images/turn_open.gif
Binary metaprl/editor/java/images/up.gif
Binary metaprl/editor/java/images/up_gray.gif
Binary metaprl/editor/java/images/up_press.gif
Added metaprl/editor/java/lucidaSansUnicode.html
Properties metaprl/editor/java/lucidaSansUnicode.html
Deleted metaprl/editor/java/raw.html
Deleted metaprl/editor/java/resize.js
Deleted metaprl/editor/java/styles.html
Deleted metaprl/editor/java/test.html
Properties metaprl/editor/ml
+34 -33 metaprl/editor/ml/Makefile
Added metaprl/editor/ml/display_term.ml
Properties metaprl/editor/ml/display_term.ml
Added metaprl/editor/ml/display_term.mli
Properties metaprl/editor/ml/display_term.mli
Deleted metaprl/editor/ml/io_proof_type.mlz
+79 -88 metaprl/editor/ml/library_eval.ml
+66 -60 metaprl/editor/ml/mp.ml
+2 -4 metaprl/editor/ml/mp.mli
+3 -2 metaprl/editor/ml/mp_top.ml
Added metaprl/editor/ml/mux_channel.ml
Properties metaprl/editor/ml/mux_channel.ml
Added metaprl/editor/ml/mux_channel.mli
Properties metaprl/editor/ml/mux_channel.mli
+10 -10 metaprl/editor/ml/package_df.ml
Added metaprl/editor/ml/package_edit.ml
Properties metaprl/editor/ml/package_edit.ml
Added metaprl/editor/ml/package_edit.mli
Properties metaprl/editor/ml/package_edit.mli
+452 -356 metaprl/editor/ml/package_info.ml
+8 -13 metaprl/editor/ml/package_info.mli
Added metaprl/editor/ml/package_sig.mlz
Properties metaprl/editor/ml/package_sig.mlz
Deleted metaprl/editor/ml/package_type.mlz
Deleted metaprl/editor/ml/proof.ml
Deleted metaprl/editor/ml/proof.mli
+318 -494 metaprl/editor/ml/proof_edit.ml
+60 -32 metaprl/editor/ml/proof_edit.mli
Deleted metaprl/editor/ml/proof_type.mlz
Added metaprl/editor/ml/recursive_lock.ml
Properties metaprl/editor/ml/recursive_lock.ml
Added metaprl/editor/ml/recursive_lock.mli
Properties metaprl/editor/ml/recursive_lock.mli
+725 -503 metaprl/editor/ml/shell.ml
+7 -96 metaprl/editor/ml/shell.mli
Added metaprl/editor/ml/shell_http.ml
Properties metaprl/editor/ml/shell_http.ml
Added metaprl/editor/ml/shell_http.mli
Properties metaprl/editor/ml/shell_http.mli
+121 -411 metaprl/editor/ml/shell_mp.ml
+6 -6 metaprl/editor/ml/shell_mp.mli
Deleted metaprl/editor/ml/shell_null.ml
Deleted metaprl/editor/ml/shell_null.mli
+61 -305 metaprl/editor/ml/shell_p4.ml
+7 -11 metaprl/editor/ml/shell_p4.mli
Added metaprl/editor/ml/shell_p4_sig.mlz
Properties metaprl/editor/ml/shell_p4_sig.mlz
Deleted metaprl/editor/ml/shell_p4_type.mlz
Added metaprl/editor/ml/shell_package.ml
Properties metaprl/editor/ml/shell_package.ml
Added metaprl/editor/ml/shell_package.mli
Properties metaprl/editor/ml/shell_package.mli
+81 -96 metaprl/editor/ml/shell_rewrite.ml
+13 -8 metaprl/editor/ml/shell_rewrite.mli
Added metaprl/editor/ml/shell_root.ml
Properties metaprl/editor/ml/shell_root.ml
Added metaprl/editor/ml/shell_root.mli
Properties metaprl/editor/ml/shell_root.mli
+73 -93 metaprl/editor/ml/shell_rule.ml
+13 -8 metaprl/editor/ml/shell_rule.mli
Added metaprl/editor/ml/shell_sig.mlz
Properties metaprl/editor/ml/shell_sig.mlz
Added metaprl/editor/ml/shell_state.ml
Properties metaprl/editor/ml/shell_state.ml
Added metaprl/editor/ml/shell_state.mli
Properties metaprl/editor/ml/shell_state.mli
Deleted metaprl/editor/ml/shell_type.mlz
+2 -39 metaprl/editor/ml/test.ml
+1 -4 metaprl/editor/ml/test.mli
+3 -4 metaprl/ensemble/thread_refiner.mli
+31 -20 metaprl/ensemble/thread_refiner_null.ml
+4 -4 metaprl/ensemble/thread_refiner_null.mli
+2 -4 metaprl/ensemble/thread_refiner_null_mod.ml
+28 -28 metaprl/ensemble/thread_refiner_sig.mlz
+2 -0 metaprl/filter/Makefile
+41 -27 metaprl/filter/filter_bin.ml
+255 -275 metaprl/filter/filter_cache.ml
+18 -12 metaprl/filter/filter_cache.mli
+32 -25 metaprl/filter/filter_cache_fun.ml
+5 -5 metaprl/filter/filter_cache_fun.mli
+4 -5 metaprl/filter/filter_exn.ml
+13 -10 metaprl/filter/filter_main.ml
+1914 -1872 metaprl/filter/filter_ocaml.ml
+67 -52 metaprl/filter/filter_ocaml.mli
+348 -247 metaprl/filter/filter_parse.ml
+355 -110 metaprl/filter/filter_prog.ml
+14 -9 metaprl/filter/filter_prog.mli
+1299 -1285 metaprl/filter/filter_summary.ml
+105 -102 metaprl/filter/filter_summary.mli
+11 -10 metaprl/filter/filter_summary_io.ml
+8 -6 metaprl/filter/filter_summary_io.mli
+13 -11 metaprl/filter/filter_summary_type.mlz
+3 -2 metaprl/filter/filter_type.mlz
+11 -11 metaprl/filter/filter_util.ml
+5 -5 metaprl/filter/filter_util.mli
+5 -4 metaprl/filter/infix.mli
+12 -4 metaprl/filter/infix.pre.ml
+67 -19 metaprl/filter/term_grammar.ml
+5 -4 metaprl/filter/term_grammar.mli
+4 -2 metaprl/library/library_type_base.ml
+1 -1 metaprl/mk/preface
+5 -5 metaprl/mk/rules
+8 -2 metaprl/mllib/Makefile
+3 -2 metaprl/mllib/debug_string_sets.ml
+8 -7 metaprl/mllib/debug_string_sets.mli
+14 -1 metaprl/mllib/env_arg.ml
+27 -10 metaprl/mllib/env_arg.mli
+93 -68 metaprl/mllib/file_base.ml
+5 -4 metaprl/mllib/file_base.mli
+20 -15 metaprl/mllib/file_base_type.ml
+28 -24 metaprl/mllib/file_type_base.ml
+18 -11 metaprl/mllib/file_type_base.mli
+29 -5 metaprl/mllib/filename_util.ml
+11 -5 metaprl/mllib/filename_util.mli
+6 -5 metaprl/mllib/fun_splay_set.mli
+6 -5 metaprl/mllib/hash_set.mli
+131 -128 metaprl/mllib/hash_with_gc.ml
+44 -13 metaprl/mllib/hash_with_gc_sig.ml
Added metaprl/mllib/http_server.ml
Properties metaprl/mllib/http_server.ml
Added metaprl/mllib/http_server.mli
Properties metaprl/mllib/http_server.mli
Added metaprl/mllib/list_neq_append.ml
Properties metaprl/mllib/list_neq_append.ml
Added metaprl/mllib/list_neq_append.mli
Properties metaprl/mllib/list_neq_append.mli
+57 -7 metaprl/mllib/list_util.ml
+8 -4 metaprl/mllib/list_util.mli
+160 -151 metaprl/mllib/memo.ml
+6 -39 metaprl/mllib/memo.mli
Added metaprl/mllib/memo_sig.ml
Properties metaprl/mllib/memo_sig.ml
Added metaprl/mllib/mp_inet.ml
Properties metaprl/mllib/mp_inet.ml
Added metaprl/mllib/mp_inet.mli
Properties metaprl/mllib/mp_inet.mli
+10 -34 metaprl/mllib/red_black_set.mli
Added metaprl/mllib/red_black_table.ml
Properties metaprl/mllib/red_black_table.ml
Added metaprl/mllib/red_black_table.mli
Properties metaprl/mllib/red_black_table.mli
+8 -5 metaprl/mllib/red_black_test.mli
Added metaprl/mllib/set_sig.mlz
Properties metaprl/mllib/set_sig.mlz
+6 -5 metaprl/mllib/small_set.ml
+7 -6 metaprl/mllib/small_set.mli
+5 -2 metaprl/mllib/splay_linear_set.mli
+272 -85 metaprl/mllib/splay_table.ml
+7 -28 metaprl/mllib/splay_table.mli
+6 -5 metaprl/mllib/string_set.mli
+128 -12 metaprl/mllib/string_util.ml
+17 -5 metaprl/mllib/string_util.mli
Added metaprl/mllib/table_util.ml
Properties metaprl/mllib/table_util.ml
Added metaprl/mllib/table_util.mli
Properties metaprl/mllib/table_util.mli
+242 -102 metaprl/mllib/weak_memo.ml
+8 -6 metaprl/mllib/weak_memo.mli
+98 -55 metaprl/mllib/weak_memo_sig.ml
+1 -0 metaprl/refiner/refiner/Files
+876 -238 metaprl/refiner/refiner/refine.ml
+6 -4 metaprl/refiner/refiner/refine_error.ml
+4 -4 metaprl/refiner/refiner/refiner.mli
+12 -3 metaprl/refiner/refiner/refiner_ds.ml
+1 -0 metaprl/refiner/refiner/refiner_ds.mli
Added metaprl/refiner/refiner/refiner_io.ml
Properties metaprl/refiner/refiner/refiner_io.ml
Added metaprl/refiner/refiner/refiner_io.mli
Properties metaprl/refiner/refiner/refiner_io.mli
+14 -4 metaprl/refiner/refiner/refiner_std.ml
+1 -0 metaprl/refiner/refiner/refiner_std.mli
+2 -1 metaprl/refiner/reflib/Files
+19 -21 metaprl/refiner/reflib/ascii_io.ml
+53 -54 metaprl/refiner/reflib/dform.ml
+16 -6 metaprl/refiner/reflib/dform.mli
+3 -2 metaprl/refiner/reflib/ml_term.ml
+13 -4 metaprl/refiner/reflib/mp_resource.ml
+20 -3 metaprl/refiner/reflib/mp_resource.mli
+4 -4 metaprl/refiner/reflib/refine_exn.ml
+880 -514 metaprl/refiner/reflib/rformat.ml
+29 -33 metaprl/refiner/reflib/rformat.mli
+7 -0 metaprl/refiner/reflib/simple_print.ml
+20 -21 metaprl/refiner/reflib/simple_print.mli
+8 -8 metaprl/refiner/reflib/simple_print_sig.ml
+148 -27 metaprl/refiner/reflib/term_copy2_weak.ml
+89 -10 metaprl/refiner/reflib/term_copy2_weak.mli
+14 -10 metaprl/refiner/reflib/term_copy_weak.ml
+26 -15 metaprl/refiner/reflib/term_copy_weak.mli
Added metaprl/refiner/reflib/term_eq_table.ml
Properties metaprl/refiner/reflib/term_eq_table.ml
Added metaprl/refiner/reflib/term_eq_table.mli
Properties metaprl/refiner/reflib/term_eq_table.mli
+7 -7 metaprl/refiner/reflib/term_io.ml
+10 -14 metaprl/refiner/reflib/term_io.mli
Added metaprl/refiner/reflib/term_match_table.ml
Properties metaprl/refiner/reflib/term_match_table.ml
Added metaprl/refiner/reflib/term_match_table.mli
Properties metaprl/refiner/reflib/term_match_table.mli
+4 -4 metaprl/refiner/reflib/theory.ml
+4 -4 metaprl/refiner/reflib/theory.mli
+4 -3 metaprl/refiner/refsig/Files
+6 -4 metaprl/refiner/refsig/refine_error_sig.ml
Added metaprl/refiner/refsig/refine_minimal_sig.ml
Properties metaprl/refiner/refsig/refine_minimal_sig.ml
+124 -48 metaprl/refiner/refsig/refine_sig.ml
+63 -15 metaprl/refiner/refsig/refiner_sig.ml
+2 -0 metaprl/refiner/refsig/term_addr_sig.ml
Added metaprl/refiner/refsig/term_base_minimal_sig.ml
Properties metaprl/refiner/refsig/term_base_minimal_sig.ml
+198 -47 metaprl/refiner/refsig/term_hash_sig.ml
Added metaprl/refiner/refsig/term_man_minimal_sig.ml
Properties metaprl/refiner/refsig/term_man_minimal_sig.ml
+3 -0 metaprl/refiner/refsig/term_man_sig.ml
+5 -5 metaprl/refiner/refsig/term_meta_sig.ml
+43 -18 metaprl/refiner/refsig/term_norm_sig.ml
+4 -0 metaprl/refiner/refsig/term_op_sig.ml
Added metaprl/refiner/refsig/term_subst_minimal_sig.ml
Properties metaprl/refiner/refsig/term_subst_minimal_sig.ml
+8 -10 metaprl/refiner/refsig/term_subst_sig.ml
+17 -11 metaprl/refiner/refsig/termmod_hash_sig.ml
+51 -12 metaprl/refiner/refsig/termmod_sig.ml
Deleted metaprl/refiner/refsig/tm_base_sig.mlz
Deleted metaprl/refiner/refsig/tm_man_sig.mlz
Deleted metaprl/refiner/refsig/tm_subst_sig.mlz
+16 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+41 -17 metaprl/refiner/term_ds/term_base_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds.ml
+8 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+22 -0 metaprl/refiner/term_ds/term_man_ds.ml
+33 -2 metaprl/refiner/term_ds/term_op_ds.ml
+24 -23 metaprl/refiner/term_ds/term_subst_ds.ml
+14 -1 metaprl/refiner/term_gen/term_addr_gen.ml
+156 -109 metaprl/refiner/term_gen/term_hash.ml
+7 -6 metaprl/refiner/term_gen/term_hash.mli
+31 -23 metaprl/refiner/term_gen/term_header_constr.ml
+11 -8 metaprl/refiner/term_gen/term_header_constr.mli
+34 -0 metaprl/refiner/term_gen/term_man_gen.ml
+30 -14 metaprl/refiner/term_gen/term_meta_gen.ml
+31 -13 metaprl/refiner/term_gen/term_norm.ml
+11 -8 metaprl/refiner/term_gen/term_norm.mli
+11 -4 metaprl/refiner/term_std/term_base_std.ml
+30 -2 metaprl/refiner/term_std/term_op_std.ml
+6 -0 metaprl/refiner/term_std/term_std_sig.ml
+16 -17 metaprl/refiner/term_std/term_subst_std.ml
+1 -3 metaprl/theories/base/Makefile
+21 -6 metaprl/theories/base/base_auto_tactic.ml
+6 -4 metaprl/theories/base/base_auto_tactic.mli
+2 -2 metaprl/theories/base/base_cache.ml
+2 -2 metaprl/theories/base/base_cache.mli
+97 -11 metaprl/theories/base/base_dform.ml
+9 -4 metaprl/theories/base/base_dform.mli
+273 -37 metaprl/theories/base/base_dtactic.ml
+12 -6 metaprl/theories/base/base_dtactic.mli
+22 -33 metaprl/theories/base/base_meta.ml
+2 -0 metaprl/theories/base/base_meta.mli
Deleted metaprl/theories/base/base_rewrite.ml
Deleted metaprl/theories/base/base_rewrite.mli
+4 -4 metaprl/theories/base/base_theory.mlz
Deleted metaprl/theories/base/nuprl_font.ml
Deleted metaprl/theories/base/nuprl_font.mli
+348 -87 metaprl/theories/base/summary.ml
+62 -17 metaprl/theories/base/summary.mli
+10 -9 metaprl/theories/base/typeinf.ml
+3 -3 metaprl/theories/base/typeinf.mli
Properties metaprl/theories/boot
Added metaprl/theories/boot/Makefile
Properties metaprl/theories/boot/Makefile
Added metaprl/theories/boot/conversionals_boot.ml
Properties metaprl/theories/boot/conversionals_boot.ml
Added metaprl/theories/boot/conversionals_boot.mli
Properties metaprl/theories/boot/conversionals_boot.mli
Added metaprl/theories/boot/exn_boot.ml
Properties metaprl/theories/boot/exn_boot.ml
Added metaprl/theories/boot/exn_boot.mli
Properties metaprl/theories/boot/exn_boot.mli
Added metaprl/theories/boot/proof_boot.ml
Properties metaprl/theories/boot/proof_boot.ml
Added metaprl/theories/boot/proof_boot.mli
Properties metaprl/theories/boot/proof_boot.mli
Added metaprl/theories/boot/proof_term_boot.ml
Properties metaprl/theories/boot/proof_term_boot.ml
Added metaprl/theories/boot/proof_term_boot.mli
Properties metaprl/theories/boot/proof_term_boot.mli
Added metaprl/theories/boot/rewrite_boot.ml
Properties metaprl/theories/boot/rewrite_boot.ml
Added metaprl/theories/boot/rewrite_boot.mli
Properties metaprl/theories/boot/rewrite_boot.mli
Added metaprl/theories/boot/sequent_boot.ml
Properties metaprl/theories/boot/sequent_boot.ml
Added metaprl/theories/boot/sequent_boot.mli
Properties metaprl/theories/boot/sequent_boot.mli
Added metaprl/theories/boot/tactic_boot.ml
Properties metaprl/theories/boot/tactic_boot.ml
Added metaprl/theories/boot/tactic_boot.mli
Properties metaprl/theories/boot/tactic_boot.mli
Added metaprl/theories/boot/tactic_boot_sig.mlz
Properties metaprl/theories/boot/tactic_boot_sig.mlz
Added metaprl/theories/boot/tactic_type.ml
Properties metaprl/theories/boot/tactic_type.ml
Added metaprl/theories/boot/tactic_type.mli
Properties metaprl/theories/boot/tactic_type.mli
Added metaprl/theories/boot/tacticals_boot.ml
Properties metaprl/theories/boot/tacticals_boot.ml
Added metaprl/theories/boot/tacticals_boot.mli
Properties metaprl/theories/boot/tacticals_boot.mli
+1 -1 metaprl/theories/czf/Makefile
+3 -3 metaprl/theories/czf/czf_itt_all.ml
+1 -1 metaprl/theories/czf/czf_itt_all.mli
+3 -3 metaprl/theories/czf/czf_itt_and.ml
+3 -3 metaprl/theories/czf/czf_itt_dall.ml
+1 -1 metaprl/theories/czf/czf_itt_dall.mli
+3 -3 metaprl/theories/czf/czf_itt_dexists.ml
+1 -1 metaprl/theories/czf/czf_itt_dexists.mli
+2 -2 metaprl/theories/czf/czf_itt_empty.ml
+2 -2 metaprl/theories/czf/czf_itt_eq.ml
+1 -1 metaprl/theories/czf/czf_itt_eq.mli
+2 -2 metaprl/theories/czf/czf_itt_eq_inner.ml
+1 -1 metaprl/theories/czf/czf_itt_eq_inner.mli
+3 -3 metaprl/theories/czf/czf_itt_exists.ml
+1 -1 metaprl/theories/czf/czf_itt_exists.mli
+2 -2 metaprl/theories/czf/czf_itt_false.ml
+1 -1 metaprl/theories/czf/czf_itt_false.mli
+3 -3 metaprl/theories/czf/czf_itt_implies.ml
+1 -1 metaprl/theories/czf/czf_itt_isect.mli
+3 -3 metaprl/theories/czf/czf_itt_member.ml
+2 -2 metaprl/theories/czf/czf_itt_member.mli
+3 -3 metaprl/theories/czf/czf_itt_or.ml
+4 -4 metaprl/theories/czf/czf_itt_pre_set.ml
+2 -2 metaprl/theories/czf/czf_itt_pre_set.mli
+1 -1 metaprl/theories/czf/czf_itt_rel.ml
+3 -3 metaprl/theories/czf/czf_itt_sall.ml
+2 -2 metaprl/theories/czf/czf_itt_sall.mli
+3 -3 metaprl/theories/czf/czf_itt_sep.ml
+1 -1 metaprl/theories/czf/czf_itt_sep.mli
+10 -10 metaprl/theories/czf/czf_itt_set.ml
+2 -2 metaprl/theories/czf/czf_itt_set.mli
+4 -4 metaprl/theories/czf/czf_itt_set_ext.ml
+2 -2 metaprl/theories/czf/czf_itt_set_ext.mli
+1 -1 metaprl/theories/czf/czf_itt_set_ind.ml
+3 -3 metaprl/theories/czf/czf_itt_sexists.ml
+1 -1 metaprl/theories/czf/czf_itt_sexists.mli
+3 -3 metaprl/theories/czf/czf_itt_small.ml
+2 -2 metaprl/theories/czf/czf_itt_small.mli
+2 -2 metaprl/theories/czf/czf_itt_true.ml
+3 -3 metaprl/theories/czf/czf_itt_union.ml
+1 -1 metaprl/theories/czf/czf_itt_union.mli
+1 -1 metaprl/theories/fol/Makefile
+9 -42 metaprl/theories/fol/fol_all.ml
+9 -28 metaprl/theories/fol/fol_and.ml
+2 -1 metaprl/theories/fol/fol_class.ml
+1 -1 metaprl/theories/fol/fol_class.mli
+9 -30 metaprl/theories/fol/fol_exists.ml
+2 -22 metaprl/theories/fol/fol_false.ml
+9 -30 metaprl/theories/fol/fol_implies.ml
+7 -26 metaprl/theories/fol/fol_not.ml
+14 -36 metaprl/theories/fol/fol_or.ml
+3 -2 metaprl/theories/fol/fol_struct.ml
+1 -1 metaprl/theories/fol/fol_struct.mli
+1 -1 metaprl/theories/fol/fol_theory.ml
+2 -19 metaprl/theories/fol/fol_true.ml
+3 -2 metaprl/theories/fol/fol_type.ml
+3 -2 metaprl/theories/fol/fol_univ.ml
+1 -1 metaprl/theories/fol/fol_univ_itt.ml
+2 -2 metaprl/theories/itt/Makefile
Deleted metaprl/theories/itt/collection.ml
Deleted metaprl/theories/itt/collection.mli
Deleted metaprl/theories/itt/collection.prlb
+1 -3 metaprl/theories/itt/itt_arith.ml
+24 -40 metaprl/theories/itt/itt_atom.ml
+1 -4 metaprl/theories/itt/itt_atom.mli
+10 -31 metaprl/theories/itt/itt_atom_bool.ml
+1 -1 metaprl/theories/itt/itt_atom_bool.mli
+36 -71 metaprl/theories/itt/itt_bisect.ml
+94 -298 metaprl/theories/itt/itt_bool.ml
+2 -6 metaprl/theories/itt/itt_bool.mli
+18 -62 metaprl/theories/itt/itt_bunion.ml
+1 -1 metaprl/theories/itt/itt_bunion.mli
Added metaprl/theories/itt/itt_collection.ml
Properties metaprl/theories/itt/itt_collection.ml
Added metaprl/theories/itt/itt_collection.mli
Properties metaprl/theories/itt/itt_collection.mli
Added metaprl/theories/itt/itt_collection.prlb
Properties metaprl/theories/itt/itt_collection.prlb
+17 -22 metaprl/theories/itt/itt_derive.ml
+1 -1 metaprl/theories/itt/itt_derive.mli
+47 -135 metaprl/theories/itt/itt_dfun.ml
+5 -13 metaprl/theories/itt/itt_dfun.mli
+26 -116 metaprl/theories/itt/itt_dprod.ml
+5 -10 metaprl/theories/itt/itt_dprod.mli
+205 -262 metaprl/theories/itt/itt_equal.ml
+18 -10 metaprl/theories/itt/itt_equal.mli
Binary metaprl/theories/itt/itt_equal.prlb
+5 -5 metaprl/theories/itt/itt_ext_equal.ml
+10 -7 metaprl/theories/itt/itt_fset.ml
+4 -2 metaprl/theories/itt/itt_fset.mli
+52 -126 metaprl/theories/itt/itt_fun.ml
+6 -9 metaprl/theories/itt/itt_fun.mli
+53 -81 metaprl/theories/itt/itt_int.ml
+7 -8 metaprl/theories/itt/itt_int.mli
+10 -31 metaprl/theories/itt/itt_int_bool.ml
+1 -1 metaprl/theories/itt/itt_int_bool.mli
+22 -89 metaprl/theories/itt/itt_isect.ml
+1 -4 metaprl/theories/itt/itt_isect.mli
+30 -140 metaprl/theories/itt/itt_list.ml
+1 -4 metaprl/theories/itt/itt_list.mli
+39 -132 metaprl/theories/itt/itt_list2.ml
+1 -1 metaprl/theories/itt/itt_list2.mli
+162 -439 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_logic.mli
+21 -21 metaprl/theories/itt/itt_prec.ml
+16 -76 metaprl/theories/itt/itt_prod.ml
+5 -11 metaprl/theories/itt/itt_prod.mli
+5 -4 metaprl/theories/itt/itt_prop_decide.ml
+1 -1 metaprl/theories/itt/itt_prop_decide.mli
+50 -131 metaprl/theories/itt/itt_quotient.ml
+1 -4 metaprl/theories/itt/itt_quotient.mli
+98 -121 metaprl/theories/itt/itt_rfun.ml
+18 -5 metaprl/theories/itt/itt_rfun.mli
+36 -110 metaprl/theories/itt/itt_set.ml
+2 -5 metaprl/theories/itt/itt_set.mli
+3 -5 metaprl/theories/itt/itt_squash.ml
+2 -5 metaprl/theories/itt/itt_squash.mli
+19 -53 metaprl/theories/itt/itt_srec.ml
+82 -62 metaprl/theories/itt/itt_struct.ml
+4 -2 metaprl/theories/itt/itt_struct.mli
+27 -79 metaprl/theories/itt/itt_subtype.ml
+2 -4 metaprl/theories/itt/itt_subtype.mli
+7 -7 metaprl/theories/itt/itt_test.ml
+2 -2 metaprl/theories/itt/itt_test.mli
+1 -1 metaprl/theories/itt/itt_tsub.ml
+17 -78 metaprl/theories/itt/itt_tunion.ml
+32 -137 metaprl/theories/itt/itt_union.ml
+5 -11 metaprl/theories/itt/itt_union.mli
+30 -50 metaprl/theories/itt/itt_unit.ml
+2 -8 metaprl/theories/itt/itt_unit.mli
+22 -45 metaprl/theories/itt/itt_void.ml
+1 -4 metaprl/theories/itt/itt_void.mli
+21 -115 metaprl/theories/itt/itt_w.ml
+71 -70 metaprl/theories/ocaml/ocaml_base_df.ml
+5 -4 metaprl/theories/ocaml/ocaml_base_df.mli
+70 -70 metaprl/theories/ocaml/ocaml_expr_df.ml
+13 -13 metaprl/theories/ocaml/ocaml_mt_df.ml
+95 -95 metaprl/theories/ocaml/ocaml_patt_df.ml
+15 -15 metaprl/theories/ocaml/ocaml_sig_df.ml
+29 -29 metaprl/theories/ocaml/ocaml_str_df.ml
+36 -36 metaprl/theories/ocaml/ocaml_type_df.ml
+1 -1 metaprl/theories/reflect_itt/Makefile
+15 -15 metaprl/theories/reflect_itt/refl_free_vars.ml
+1 -1 metaprl/theories/reflect_itt/refl_free_vars.mli
+36 -105 metaprl/theories/reflect_itt/refl_raw_term.ml
+2 -2 metaprl/theories/reflect_itt/refl_raw_term.mli
+75 -175 metaprl/theories/reflect_itt/refl_term.ml
+2 -3 metaprl/theories/reflect_itt/refl_term.mli
+28 -71 metaprl/theories/reflect_itt/refl_var.ml
+2 -2 metaprl/theories/reflect_itt/refl_var.mli
+86 -190 metaprl/theories/reflect_itt/refl_var_set.ml
+2 -2 metaprl/theories/reflect_itt/refl_var_set.mli
+5 -7 metaprl/theories/tactic/Makefile
Deleted metaprl/theories/tactic/conversionals.ml
Deleted metaprl/theories/tactic/conversionals.mli
+2 -2 metaprl/theories/tactic/mptop.ml
+2 -2 metaprl/theories/tactic/mptop.mli
Added metaprl/theories/tactic/nuprl_font.ml
Properties metaprl/theories/tactic/nuprl_font.ml
Added metaprl/theories/tactic/nuprl_font.mli
Properties metaprl/theories/tactic/nuprl_font.mli
+4 -5 metaprl/theories/tactic/perv.mli
Deleted metaprl/theories/tactic/pre_tactic_type.ml
Deleted metaprl/theories/tactic/pre_tactic_type.mli
Deleted metaprl/theories/tactic/remote_null.ml
Deleted metaprl/theories/tactic/remote_null.mli
Deleted metaprl/theories/tactic/remote_sig.mlz
Deleted metaprl/theories/tactic/rewrite_type.ml
Deleted metaprl/theories/tactic/rewrite_type.mli
Deleted metaprl/theories/tactic/sequent.ml
Deleted metaprl/theories/tactic/sequent.mli
Deleted metaprl/theories/tactic/tactic_type.ml
Deleted metaprl/theories/tactic/tactic_type.mli
Deleted metaprl/theories/tactic/tacticals.ml
Deleted metaprl/theories/tactic/tacticals.mli
Added metaprl/theories/tactic/top_conversionals.ml
Properties metaprl/theories/tactic/top_conversionals.ml
Added metaprl/theories/tactic/top_conversionals.mli
Properties metaprl/theories/tactic/top_conversionals.mli
Added metaprl/theories/tactic/top_tacticals.ml
Properties metaprl/theories/tactic/top_tacticals.ml
Added metaprl/theories/tactic/top_tacticals.mli
Properties metaprl/theories/tactic/top_tacticals.mli
+28 -3 metaprl/theories/tactic/var.ml
+2 -1 metaprl/theories/tactic/var.mli
+1 -1 metaprl/theories/tptp/Makefile
+27 -83 metaprl/theories/tptp/tptp.ml
+16 -16 metaprl/theories/tptp/tptp.mli
+6 -5 metaprl/theories/tptp/tptp_cache.ml
+2 -1 metaprl/theories/tptp/tptp_prove.ml
+1 -1 metaprl/theories/tptp/tptp_prove.mli
+1 -2 metaprl/util/ocamldep.mll