(* MOSCOW ML VERSION *) (* New implementation of Mark2 theorem prover *) (* now officially called "Watson" *) (* copyright M. Randall Holmes, 1999 -- you may freely distribute as long as this notice is preserved *) (* at this point, all commands should be documented in babydocs *) (* Dec. 1: corrected incorrect stipulation that @! be scinleft. There is no apparent effect on existing files. There is now an alternative file firstorder.sml with a totally different approach to the problems with multiple universal quantification. (based on a totally different semantics for @!) *) (* Oct. 19: extremely minor correction of higher-order matching: does not affect correct execution of existing files. *) (* Oct. 18: installed SHELL command which invokes the shell from inside an INPUT tactic (or from anywhere, I suppose...) *) (* Oct. 6: attempt to install bailout for INPUT commands -- STOPINPUT aborts execution of all INPUT commands (in fact, of everything) New built in theorem STOPINPUT has effect of converting target theorem to a bogus value and causing all INPUT commands to do the same thing; this has the effect of crashing the tactic interpreter and returning to the first theorem that invoked INPUT, which is just what is wanted for proof editing. *) (* Sept. 7: All modifications in this version are purely technical from the standpoint of current users; they involve the behaviour of the special operator @! , which I have not yet discussed. I'm not happy entirely with the state of @! I could make it entirely safe by restricting matching to arguments ?n other than ?0 (ensuring that all operators matching ?P in the context ?P@!... would be stratified (but possibly inhomogeneous)) and segregating variables representing stratified but inhomogeneous operators from other variables as part of stratification checks. But it is unclear to me that there is any hazard from the present situation. The unexpected new consequence is that at level 0 a variable can match a completely unstratified abstraction! Or can I prove that the current setup is safe? I must opt in favor of security. I will restrict higher-order matching involving @! to positive-indexed bound variables (there is no premium on matching pair and constant function arguments in this case, anyway); this eliminates matching to unstratified abstracts. I will also insert a check for segregation of variables matching possibly inhomogeneous operators from other free variables into stratification criteria. This should make the whole @! facility provably secure. I have made the changes indicated above (making @! theoretically secure) and also inserted a stratification check into the assign command (because it is now possible for a level 0 expression to be unstratified, which was not possible before). Uses of the @! command which are expected should be completely unaffected. segregation checks need to be run on whole theorems; this has been implemented systematically. Fixed glitch in autoeval which caused failure to eliminate some applications of function terms using @! *) (* Sept. 2: fixed autoeval function so that it works correctly with the new match function. The whole library runs except that some old proofs on quantifier switching break; it was necessary to expand some upto commands in the proof of ASSIGN_WP because of the changes in the definition of matching. *) (* Sept. 1: For some reason, UNIV_SWITCH is broken. This version has much stronger higher-order matching facilities than any previous version. It is also better designed: the higher-order matching uses the bind function, so upgrades to BIND will automatically upgrade matching. Fixed up the special case of ?0 in higher order matching; there is no danger of invocations of "level -1" any more. Fixed up BIND to bind intelligently with constant function parameters. BIND now (again) does not commute with EVAL. General problem: extend matching to handle pairs neatly; there need to be matches for P1@x and P2@x as well as for x? This is what's needed to make a new UNEVAL work nicely. Idea: a pairprep which converts a variable ?x occurring in a context p1@?x to variables ?x_1,?x_2 throughout the expression before matching (and carries out execution of p1 and p2 after matching). The handling of constant functions motivates doing pairprep on both left and right (not restricting to list binding). A daring experiment works: implement higher-order matching using the new bind function, and get all kinds of new higher-order binding power all at once! installed automatic execution of applications to ?0, and fixed an old bug in steps() simplified higher order matching to @! to bring it into line with @; I think this ought to work... *) (* August 31st: This seems to be a version with full strength higher order matching. Note that introduction of ?0 as default argument required modifications to declarecheck and also a clause identifying level ~1 with level 1 in strat (as in declarecheck). Further upgrades projected: improve matching and bind/eval functions to take pairing into account. Also, improve matching to handle type labels? This last might or might not fly? When working on the pairing upgrade, think about ?m..?n; think about whether I'm working on a pair or list model. I should check whether matching to ?F@?0 works as expected? Should restrictions be placed on the use of ?0? Should ?0 take over as nil? (this last sounds like an excellent idea!) I have now made BIND into a list binding function. To preserve commutativity of BIND and EVAL, I used new versions p1 and p2 of the projection operators which have functional programming set to evaluate automatically. I have to think about what to do with UNEVAL, and also how to extend this to higher-order matching. Note that the behavior of BIND now depends on the grouping (left or right) of the comma operator. *) (* August 30th: Consider possibility of using ?0 as default value? One could use a general strategy of always evaluating when a "bound variable" is involved? I have commented out the part in declarecheck where ?0 is outlawed. I have also introduced the aptoeq function to handle preemption of higher order matching. Plan to rewrite higher order matching to do it with all bound variables; this will handle one of the new cases automatically! (using ?0 as the default value). Note that one may want to rework bind to handle values at [?x] differently as well as values at ?x,?y? *) (* August 27th: restricted terms to the left of a deepest @! to free variables and function terms. For completely demonstrable soundness, one could further forbid free variables occurring in such a context from occurring in any other context; is there a neat trick for doing this? Idea: add info about free variables to strat? Not readily typable. This is probably enough as it is to support a soundness argument? Fixed up the levels in the implementation of matching with @!; I don't think the earlier ones were actually valid. Get rid of the stuff with @`; this idea can work, but not the way I did it! Also, "=" would work just as well! Introduce a function which changes applications to equations and apply it in the test. *) (* August 26th: In demo mode one can now invoke a noml() shell by hitting s at most (not all) returns. Hit return after the two following messages (turning off diagnostic and demo modes), then type commands as usual. The script will resume after you type quit(); You will sometimes get a message "Unknown command quit in script", which is harmless. Of course, you can mess up what's happening in the script if you aren't careful! Right after the proof of a theorem is usually a safe place to shell out. I outlined but did not implement generalized higher order matching in typed situations. *) (* August 25th (once again an official release): This new release has two major features, one straightforward and one experimental (and maybe even dangerous): the UNEVAL tactic is now much smarter (this is straightforward); it will find iterated (curried) values of multiply bracketed functions. In the existing theory, try s "?x+?y+?z"; ri "UNEVAL@[[[?1+?2+?3]]]"; ex(); There is a new, very special operator @! which allows the construction of terms which will match general terms with iterated quantifiers. For example, there was no term which would match all terms of the form forall@[forall@[...?1...?2...]] in the previous version (whereas forall@[?P@?1] matches all singly universally quantified terms); the term forall@[forall@[(?P@!?1)@?2]] will match all such terms at this point. The basic idea is that ?P@!?1 will match any term with ?1 in it (not necessarily at the same type as ?P@!?1); in order to avoid paradoxes, the term ?P@!?1 can occur only in a context where terms depending on ?1 in any way can be put (for example, both ?1 and [?1] have to be substitutable in such a context). This is true of the context forall@[forall@[...?1...]]; because forall@[...?1...] is known by the prover to be boolean, its type can be manipulated to allow [?1] to replace ?1, for example. The term forall@[forall@[forall@[((?P@!?1)@!?2)@?3]]] will match any triple quantification, and so forth. (A term ((?P@!?1)@!?2) is only permitted in a context where ?1 and ?2 could be adorned with independently chosen numbers of brackets without affecting the stratification of the resulting term.) This will mostly be useful for the construction of tactics which will act intelligently on multiply quantified terms. The strengthening of UNEVAL will also be useful for this. In general, one can think of a term like (?P@!?1)@!?2 as being intended to match any term which is stratified except for the fact that ?1 and ?2 have been translated in type by fixed and possibly different amounts. A term of this form is allowed only in a context where ?1 and ?2 can actually be translated in type (by adding brackets, say) by uniform amounts (possibly different for ?1 and ?2 but the same for all occurrences of ?1 and the same for all occurrences of ?2) without perturbing the stratification of the whole term. This is true, for example, of ?1 and ?2 inside forall@[forall@[forall@[((?P@!?1)@!?2)@?3]]]. Further enhancements of higher-order matching may follow. There is the minor additional feature of a command demoremark which does nothing except get displayed with its string argument in demo mode; it allows remarks to be put into demos, as its name suggests. There's a comment in the function executelines concerning a possible improvement to demo mode; it almost works as written. *) (* standing list of "rough edges" of the prover (arbitrary features which cause trouble) Are defined objects defined via their application as functions actually lambda terms or not? It would be possible to define a built-in function which would handle this automatically. Idea about internalizing type information: provide a built-in tactic which will convert an infix term to a functional form, with appropriate introduction of constant functions and values. definitions of constants have same names as constants; this has inspired the prevention of application of functional programming to theorem names. the problem of new variables breaking stratification -- accommodated but still there and not easily removed. Of course, I might be able to use ?f@!?n instead of ?f@?n and fix the problem in this experimental version! (no, newest treatment of ?f@!?n does not permit this). I might want to generalize the forms allowed as formats to anything with an "eitherhead". This would eliminate the need for the peculiar solution to stratification problems with makescinvar. Should autoeval be more aggressive: should it do more automatic evaluations? Probably to be avoided because it would require repair of many existing theory files! Should there be a way to recognize the kind of "scin" behaviour that the theorem FORALLBOOL2 tells us that forall has? This goes along with the recent generalization of argument lists. There remains the problem of scin/scout for functions with parameter lists. Inconvenience of extracting type information. How about a primitive tactic which labels the terms on each side of an infix with their relative type? How about the major modification of maintaining local type info and info on type of all abstracts to remove the stratification failures due to new variables? Diagnostic information on relative types would be useful when issues of stratification arise? Loss of the prompt when demo mode is invoked inside a demo. The = builtin theorem ought to require matching of the appropriate side of the given equation; it might be that it ought to have a "matchtri" analogue, but this would probably behave extremely unpredictably. I need to analyze the various situations in which stratification errors can show up in the course of execution and make sure that they can't lead to incorrect proofs. The most worrisome situation is the one in which a variable on the left of a @! (matching an operation which may not be a function) is introduced somewhere else as a function; such a theorem will pass stratification tests but will crash with a stratification failure if the operation is instantiated as a non-function; I believe that this is harmless (because it is impossible to generalize over such a variable) but it would be nice to prove this formally. If it were a problem, there is a fix: it would require declaration checking to verify implicit typing of certain variables as general operators, and probably restrict the forms of expressions occurring on the left of a topmost @! to function terms and free variables; maybe I should do this anyway. still question as to whether the implicit typing of stratified inhomogeneous operators should be enforced. idea that operators declared scin or scout should be retyped (scin as flat and scout so as to get smallest type to 0). Recognize that if one is on two of the scin/scout lists one should be on all three? *) (* August 25: I think I finally have a sound definition for behavior of the @! infix for generalized higher-order matching. Further generalizations of matching which are possible involve direct support for matching projections of pairs (iterated projections of free variables would be allowed to match and matches of variables to pairs would induce matches to projections; some care needed to avoid regress) and stronger higher-order matching for cases of concrete type differentials (iterate higher order matching and match to things like (?P@?x)@0 and ?P@[?x]). The idea is that ?P in (e.g.) ((?P@!?m)@!?n must match a "stratified inhomogeneous" operation on ?m and ?n; one which is an operation on ?m and ?n yielding a stratifiable expression but not necessarily one which can be expressed as a function of ?m and ?n (the relative types of ?m and ?n may be too high or low for this to work). A general operation of this kind can appear in a stratified function definition only in special contexts: ones in which the types of its arguments can be arbitrarily displaced with respect to the context and one another without affecting stratification. These are the conditions enforced on the @! operator (along with the condition that the head of a curried expression in @! is an opaque environment; no binding can occur there at all). It doesn't seem that the possibility of having ?P appear in other positions can be exploited to prove anything (after all, it isn't clear that one can prove much of anything about expressions ((?P@!?m)@!?n). *) (* August 24: New experimental implementation of higher-order matching seems to work, more or less. The approach is to allow ?P@!?1 only in positions where the relative type of ?1 floats. The implementation involves carrying out stratification twice, with different output types assigned to @!. The idea is that ?P@!?n matches any expression of the same "level" as ?n (involving no bound variables with higher index) whose type "floats" in its context. The stratification function types each term twice now, with two different output types for the @! operator. The term forall@[forall@[(?P@!?1)@?2]] (note that there is just one @!) matches any double quantification. Any reasoning with terms of the form @! will encounter restrictions; it must preserve the floating character of the typing of all ?P@!?n terms and also respect other logically motivated precautions. I believe this feature is sound in concept, but an earlier version allowed bad proofs; there may of course be bugs! Do we still need more general forms of higher-order matching? is the x@!y@!...z@w pattern enough? UNEVAL is now full-powered; it handles multiple bracket terms as parameters and produces iterated values thereof. I might be able to write a general bound variable switching procedure without running into the usual blocks: forall @ [forall @ [bool : (?P @! ?2) @ ?1]] is an acceptable term! But it still might not work. (LATER: this does work!) *) (* August 23: fixed bug: => and <= were supposed to be scinleft; now they really are! In general, properties of built-in operators need to be updated by the clear() command. *) (* August 20: installed ability to declare scin infix variables with command makescinvar . Corrected match to allow this. Supermatch appears to handle this correctly already. The modifications to other functions appear to be sufficient to allow the declaration of scout, scinleft, or scinright infix variables as well if they are ever wanted. Scout infix variables would need to have their relative types shifted to a canonical form (say with one of the types 0). Scinleft or scinright infix variables would have the "hidden" type switched to 0. Commands for these cases have not been installed. The type transformations suggested above might be desirable for purposes of theory matching for non-variable operators as well. This appears to work; it solves the problem of stratification problems in embedded theorems completely (use a scin infix variable instead of , in the parameter list of a theorem to make it secure). The installation of makescinleftvar, makescinrightvar, makescoutvar is relatively easy, but I do not as yet see applications for such variables? *) (* August 20: nothing implemented here -- just ideas. 1. scin infix variables would be useful. scout, scinleft, and scinright infix variables might also be nice, but this takes more work. I should look at the conjecture that being on more than one of these three lists should put you on the third as well, and check that variables on more than one list are treated correctly. An advantage of scin infix variables is that they could be used to build parameter lists for tactics, eliminating all problems with stratification in embedded theorems. 2. The problem of higher order matching inside more than one bracket appears again. A generalization of UNEVAL to handle curried functions might help. Generalized binding tactics might be useful as well. A true generalization of higher-order matching remains a possibility, I suppose. Use expressions in ?P@[?n] and (?P@?n)@0. I can also write generalized binding tactics (especially when scin infix variables are available). There's an old idea that higher-order matching should be integrated with the type system somehow? *) (* August 19: notes on possible editor function. This would be used in conjunction with makescript. List basic functionalities wanted: load the current autoscript into buffer move around in editor buffer in usual ways search-replace in editor buffer display ranges of lines; copy ranges of lines execute ranges of lines in prover This would create a text-based environment in which all commands passed to prover would be recorded automatically and it would be possible to manipulate these commands and reissue them in a reasonable way without relying on an external editor or the cut/paste capabilities of the OS *) (* August 19: Try the compress() command to get a vertically compressed output format. A dashed line separates dependencies from the text of a theorem. expand undoes compress and both are found on the script command menu. In demo mode, a "d" entered at any pause will exit demo mode while continuing execution of the script (you will have to hit return once or twice in response to messages before the renewed execution starts). The script command inside the noml() interface is now "script" (the same as at the ML prompt) although the alternative "truescript" will still work. The noml() interface now catches any exception, rather than just I/O exceptions, and this source should compile under SML 96 without any change. I suggest trying noml(); compress(); to set up your working environment. To return to the ML prompt, type quit(); makescript "test"; compress(); will set up the same environment, recording your commands in a script test.log.wat. Added demoremark "string" command which does nothing; its only purpose is to be displayed in the demo function. Since I am not planning to add commutative matching to the prover as a standard feature, the (no cmatch) comment has been deleted from the versiondate message. *) (* August 18: more work on look and feel. Theorems are now separated from their dependencies by a dashed line in the compressed theorem display. compress and expand added to script command menu. Also, entering "d" during a script in demo mode will take you out of demo mode, allowing the script to finish (unlike "q", which will stop the script). things now seem to work. *) (* August 17: minor modification to lookhyps: it displays the variable binding situation even if there are no hypotheses. Changes to term display: displayed terms are indented (which should be good for "human factors") and additional commands are provided: the compress() command will eliminate lots of carriage returns (compress things vertically) and the expand() command will restore the usual situation with lots of returns. *) (* August 13: modification to preexecute and preonestep; earlier versions did not do any execution inside embedded theorems; this version executes the parameters of parameterized theorems. This will allow simplification of tactics like POP_CASE. The effects of this change on any current theory should be nil. Ideas from the visit of Aug. 9-12 in Moscow (not implemented yet): an INPUTP@?tactic command which allows one to input parameters to a tactic. a shell command which would allow one to go into a noml shell (with limited command list) from the INPUT prompt. One could do things like thmdisplay, srt, targetruleinto. DONE!!! Can I reduce the number of returns (white lines) in prover output? Jim would like this. DONE There is something funny about the use of demo inside a script; it didn't display the command prompt. Idea: there ought to be a letter one can type to cause a demo'ed file to go back up to full speed. The builtin theorem "=" ought to check for matches to the given equation, not just to the theorem which justifies it. In other words, it should effectively define more specialized versions of theorems. *) (* August 2: at this point all commands should be documented in babydocs. *) (* July 14: statement display now works in lookhyps as well; this is useful in deduction theory, for example. It is a little weird that $|- is the default "prompt" for a hypothesis, due to the preference for "true=T" in hypotheses (which is itself caused by the right associativity preference). a question: does the reversal of free variables in supermatch have to be applied to infix variables as well? The obvious thing to do is to introduce a match between bogus free variables in reverse in addition to the direct match between infix variables which is needed to check declarations? This is implemented, though it is not clear that it is really needed; the problem probably would never arise. A brief note about this problem might be useful. Example is in terms of free variables rather than infix variables. The problem is that if the match direction was what one would naturally expect, a theorem ?x+?y = ?y+?x in a source theory would match a theorem ?x*?x = ?x*?x in a target theory (with * translating +). This would allow the translation of theorems proved using commutativity of + to theorems about *, which is not known to be commutative, which is unsound. The modification preventing this has already been made; the modification made here enforces the same reversal on infix variables. It is hard to see how this could really be a problem, though. The stripvars function needed to be modified to recognize bogus "free variables" generated in supermatch to enforce the reversal of matching for infix variables. *) (* July 13: automatically generated scripts now include texts of theorems in comments after the proof. This is a change in the prove function. fixed matchtri and anothermatchtri to work better added some new abbreviations dtl dtr ut = downtoleft, downtoright, upto ldtl ldtr lut = litdowntoleft, litdowntoright, litupto mtri amtri = matchtri anothermatchtri *) (* July 9: removed pause after OUTPUT because of bad effects on interactions between emacs and the ML interpreter. Installed messages using the OUTPUT command in deduction.wat. Installed autoscript facility, with new commands autoscript and makescript. autoscript puts the current script file in a file with the .log.wat extension. makescript clears the current script file and calls noml, creating a new script file when noml is exited. The scriptinscript command automatically clears the current script when it exits a script successfully (we presumably don't need to duplicate a script which works). Correcting problem with INPUT in the noml() command. The fix is that INPUT will no longer accept a blank input. Final situation: makescript is a user command; autoscript is not. Logging only happens inside the makescript command, and it does not happen in loads or script runs inside the makescript command (the consequences of this when theory files are loaded are disastrous). The makescript command cannot be nested; it will do nothing if scripting is on. *) (* July 6: fix to matchtri; also added command anothermatchtri() which gives further possible theorems; Issuing this command just after matchtri (or anothermatchtri) will change the theorem to the next appropriate one in the list; issuing at other times will have bizarre results. This doesn't seem worth posting as an official upgrade. *) (* July 2: minor modification -- "dropview" command no longer sends an error message if the view dropped does not exist installed new "literal" movement commands litupto litdowntoleft litdowntoright which look for equality rather than a match. Warning: these commands do not do level changes (they won't find [?1] in [[?2]]), and they will find [?2]). A new variant "matchtri" of targetruleintro/tri is now available. This one will look for a theorem which will send the current term to something which its argument matches. For example, if we are looking at "(~ ?x) & ~ ?y", matchtri "~?z" gives us the theorem DEMb, which sends this term to "~ ?x | ?y". This allows us to look for theorems which will send us to terms with a certain structure, rather than to an exact target. matchtri's status in the cmatch version has not been decided. A built-in theorem which implements matchtri might be of interest. This is likely to be more unpredictable than the = builtin theorem. It is important to note that it is dependent on the order of the theorems in the master theorems list, which changes! *) (* July 1: some bug fixes and extensive addition of error messages in the theorem export mechanism. The clause for free variables in supermatch needed to be reversed ((t,s) instead of (s,t)), a rather subtle logical point! Supermatch now uses a new version of mergematches which itself gives messages about match failures. The previous version created more theorems than it needed to in exports; it now looks at the expanded view (after supermatch is run) and does not create a new theorem if it sees that there is a view of that theorem. This also makes it possible to use the expanded view repeatedly; in the previous version it created junk entries. Theorem export remains unstable, I think. *) (* July 1: change to supermatch -- a bijective match between free variables in theorems is needed *) (* June 30: The cmatch version has been changed; its behaviour should be a little less unexpected than the previous version (commfix is used in a different way). Fixed a problem with initialization of the basic view. *) (* June 29: Minor changes made in course of review of comments: the script command will now treat carriage returns in strings as spaces. the statementdisplay() command now sends a message as to whether statement display is on or off. Idea is that June 29 source is a unified source which can be modified to support all versions of the prover desired. All maintenance should be done on this file. investigations of compatibility of the various sources being used. This one will work for SML 93 if the SML 96 conversion functions are commented out and the line flush_Out s = (); is added. For SML 96, one needs to replace Io with IO.Io in the noml function. Plan for today is to add material supporting commutative matching in comments, so that only one source needs to be maintained, then to do cleanup of old comments. cmatch stuff is now included in comments labelled cmatch I made the changes to steps indicated in the cmatch comments, which are needed anyway. Also liberalized the type definition functions to allow the converses of retraction theorems; the wb() in the stereotyped procedure is no longer needed. This also reflects the strengthening of commutative matching caused by use of the function commfix. inserted old comments from the cmatch source: (* June 2 (added here June 28): general cleanup of comments. Liberalized the retraction test in type definitions so that the wb() is no longer needed (a retraction theorem may safely be replaced by its converse). This is experimental source "cmatch.sml" *) (* June 1 (added here June 28): modifications to get commutative matching to post correct dependencies. Put postdeps and dropdeps into steps command. Still stuck with inappropriate posting of commutativity axioms when commutative matching is on. This is rather like the extra deps on typing axioms that show up due to scin/scout. Should I automate makescin and makescout inside the addtheorem command in the same way that I have automated commutative laws? *) (* May 28 (added here June 28): testing commutative matching The prover now maintains a registry of commutative laws User command cmatch() turns commutative matching on and off. Modifications involve the new list COMMUTATIVE, functions iscommutative0 and iscommutative, changes to addtheorem and droptheorem, and changes to match (and use of oldmatch where needed) as well as very important change to mergematches (match gives a nontrivial list of different alternative matches) Prover never uses commutative matching for control structures in the tactic interpreter or for special movement commands use of = in prematchtheorem needed changing to , since = is commutative Note that GCLEAN tactic does not work under cmatch -- maybe the point is that it _does_ work but works very differently. Now testing oldmatch in prematchtheorem; this appears to cause GCLEAN to work correctly. (version weakprematchtheorem does not use oldmatch) The toggle needs to be provided for backward compatibility even if commutative matching is the default! This remains a provisional version: for example, it does not have correct theorem dependencies -- something needs to be done to post dependencies of commutative laws when the matching uses them. *) *) (* June 28: This has been tested with SML 96. The only problem in building it is that the Io x exception in noml doesn't work; use IO.Io instead. It appears that SML96 is perfectly happy with the Moscow ML source-- except for the same problem with the Io exception. What is the I/O exception type for SML 96? Stuff about exportML: exportML, heap image files, @SMLload command line parameter Question: Calling the function exportML, as in - SMLofNJ.exportML "image"; creates a file called "image.mipseb-irix" that is not executable, while with SML/NJ 93 I would get an executable file called "image". I wonder if I am doing the export correctly or if there is a new procedure for using the exported image? Answer: The file "image.mipseb-irix" is a heap image -- not an executable. You can load it as follows: % sml @SMLload=image Note that you do not need to specify the ".mipseb-irix" suffix when specifying the image file, it will be inferred. *) (* June 25: a very minor point; when one leaves the script command, it will always turn off demo mode. Also, turning demo off or on sets the verbosity as appropriate (this means that users will not want to turn demo mode off at the top level -- but they should not have to!) changes to script, reset and demo This still needs to be ported.DONE *) (* June 16: very slight refinement of comments in INPUT text In the June 15 version, either { or } started a comment to the end of the line; now it is only { which starts a comment, which will go either to the end of the line or to a }. A } acts like an end of line and could be used to put more than one input on the same line. changes to script, reset and demo *) (* June 15: upgrade to display local level in lookhyps command; the prover tells what bound variables are locally free *) (* June 14: Modified prover so that input can be supplied to the INPUT command in scripts. The theory stack TESTTH has to be declared early (before applybuiltin) so that the INPUT command knows where to get its input. It is also initialized differently (as [std_in]; no file "dummy" is needed any more). The theory stack is reset to [std_in] when users break out of scripts. A new reset() command is now provided for users to execute whenever they break out of a script with Control-C. The reset() command fixes the theory stack so that INPUT will know to read from std_in again. reset() cannot (and should not!) be run in any script. The DIAGNOSTIC toggle is declared early so that INPUT can behave correctly in diagnostic and demo mode. In diagnostic or demo mode, the user can break out of a script by using "q" instead of hitting return after an input. In scripts, stuff supplied to INPUT is read line by line. Comments with (* *) cannot be embedded in text for INPUT, but to-end-of-line comments can be started with either kind of brace. (this required a modification to the stringinput function). If something breaks in a script with INPUT text in it, one can expect bizarre errors! *) (* June 10: added backuptheory before running scripts fixed bug in tactic interpreter; it did not correctly enter the levels of hypotheses encountered in abstraction terms. The change is in coercehypslistsense. statementdisplay() now enables a special display for true=T theorems (converse statements) with $|- This did not interact with lookhyps, which does not use eqdisplay, contrary to my earlier beliefs. This is OK. *) (* June 2: be aware that the experimental file cmatch.sml now exists (with commutative matching) and will probably eventually supersede this file *) (* May 26: completed modifications of thmtextdeps also added statement display, enabled by statementdisplay() toggle *) (* May 25: introduced statement command: fun statement na ls = axiom na ls "true"; Completely changed the implementation of theorem text dependencies. *) (* May 18: fixed bug in the 1|-|n and 2|-|n commands which did not correct level of hypotheses containing bound variables. *) (* March 24: duplicated from SML/NJ version eliminated lots of old comments (also in this file). no change in code: just a remark that a search for a theorem which will take the current term to something matching a given term would often be useful; a built-in tactic for carrying out such searches also might be interesting. The current version of the prover has almost all the upgrades I care about. Gaps which remain: a redefinition command appropriate for type definitions. This can wait for proof that redefinition will actually be used. treatment of stratification problems caused by embedded theorems: tactics defined by abstraction, built-in theorem type thm, automatic scout declarations for operator theorems (avoiding extra deps posted to SCINSCOUTDEPS). This probably can wait until problems are actually encountered. the general, hard problem of scin/scout for functions or operators with lists of arguments. This is hard, and requires reflection. a theoretical question about weak vs. strong versions of opacity. Should we be able to abstract into opaque contexts when the variables involved are safely "typed"? There are plusses and minusses to this; perhaps a toggle would be the right approach. This seems too technical; a related idea would be revival of predicativity restrictions. "program packages" were not implemented. Wait until programming is in use. Note that tri2 and trimetric are not "upgrades that I care about"; they represent experimentation in a new area. (which will continue). Another thing I still might do is implement parallel execution order for the tactic language. Do this, though it is not highest priority. Note that targetruleintro can make intelligent use of parameterized tactics; is there a way to make the multistep commands do this? This is a good question; think about it! Implementation of standard variable binding. Probably not needed, but useful for educational applications. Improved search options; this should be an area of active work. More versatile movement commands fall under a similar heading. Do this! PARTLY DONE: See litupto and kin and matchtri above. Did not reimplement modularity, comments, or on-line help! On-line help (which can subsume comments) is needed. I need to update the documentation (command reference; also add a section to the command reference on built-in tactics). Do this. add application of commutative laws (and perhaps other laws of stereotyped form) to tri. There is a vague idea of having an ability to register new abstract forms which theorems can take and have the system flag theorems of these kinds? (so one could add idempotent laws, for example, without modifying code). Do this, or at least think about it. let tri know about hypotheses! Think about this and do it if it is easy. rewrite logic? refinement of success/failure? theoretical questions about infix variables (generation of new ones, unification?) All things not to worry about now. other built-in data types? (strings, terms?) true hierarchical organization of theories; labelling of theorems as belonging to particular theories (and keeping them all in the same space). theorem search across theory boundaries (through views). This is a practical issue and should be considered! I need to look at the pretty-printing and see if it is really doing what I want. Do this. Testing of the dependency system is needed; particularly worrying is the possiblity that type definitions might not be handled correctly. Do this by working on examples of export (say teaching files). I definitely need to implement sensible binding and abstraction with multiple variables of each type (?m..n). Try doing it in structural, but be open to idea of doing it hard-wired. Do this, but first try writing tactics for structural.wat that do it. *) (* March 14: see SML/NJ version notes *) (* Sept. 8: it is no longer necessary (or advisable) to run setup() when starting up; all that is needed is load "design"; open design; *) (* August 13: developed unification functions; optimized changelevel and changehlevel by telling them to do nothing when the source and target are the same *) (* August 12: fixed yet another bug in the module; setup didn't properly initialize dependency scratch lists to nil. August 10 and earlier revisions concerned output control; Moscow ML needs to be told to flush the output in certain functions for scripts to work acceptably *) (* comment these out for SML 93 (* SML 96 Conversion functions *) (* load "Int"; *) (* val load = load; *) val std_in = TextIO.stdIn; val std_out = TextIO.stdOut; fun output (out, msg) = TextIO.output(out,msg); fun input (inp, n) = TextIO.inputN(inp,n); fun makestring(value) = Int.toString(value); fun explode (s) = (List.map str (String.explode s)); fun implode (ls) = String.concat ls; fun max(n1,n2) = Int.max(n1,n2); fun open_out(s) = TextIO.openOut(s); fun close_out(s) = TextIO.closeOut(s); fun flush_Out(s) = TextIO.flushOut(s); fun open_in(s) = TextIO.openIn(s); fun close_in(s) = TextIO.closeIn(s); fun flush_Out(s) = TextIO.flushOut(s); fun substring s = String.substring(s); (* fun exit() = OS.Process.exit(OS.Process.success); *) (* fun abort() = OS.Process.exit(OS.Process.failure); *) END SML 96 Conversion functions *) (* used for SML 93 compatibility *) fun flush_Out s = (); (* Error message function with pause control functions *) val ERRORPAUSE = ref false; fun setpause() = ERRORPAUSE := true; fun setnopause() = ERRORPAUSE := false; exception Breakout; val Returns = ref("\n\n"); fun compress() = Returns := "\n"; fun expand() = Returns := "\n\n"; fun errormessage s = (output(std_out,(!Returns)^"Watson: "^s^(!Returns)); flush_Out(std_out); if (!ERRORPAUSE) then if input(std_in,1) = "q" then raise Breakout else () else ()); (* verbosity of output *) val VERBOSITY = ref 2; fun bequiet() = VERBOSITY := 0; fun thmsonly() = VERBOSITY := 1; fun speakup() = VERBOSITY := 2; (* version command *) fun versiondate() = errormessage "Dec. 1, 1999"; (* container classes *) (* Watson requires two kinds of container classes, finite sets and finite functions. These were implemented as balanced binary trees in Mark2. In this design, they are implemented in a very simple way as lists. There doesn't seem to be any deficit in performance. *) (* all operations attempt to maintain the invariant that any set or function element appears no more than once *) (* sets *) (* a set of objects of a given type is simply a list of objects of that type *) (* is an object x found in a given set? *) fun foundinset x nil = false | foundinset x (a::rest) = if x = a then true else foundinset x rest; (* add x to a given set *) fun addtoset x L = if foundinset x L then L else (x::L); (* drop x from given set *) fun dropfromset x nil = nil | dropfromset x (a::rest) = if x = a then rest else (a::(dropfromset x rest)); (* union of sets *) fun union nil L = L | union (a::L) M = a::(union L (dropfromset a M)); fun union2 nil = nil | union2 (L::M) = union L (union2 M); fun intersection nil L = nil | intersection (a::L) M = if foundinset a M then a::(intersection L M) else intersection L M; (* subset relation *) fun subset nil L = true | subset (a::L) M = (foundinset a M) andalso (subset L M); (* the subset of a list of which the predicate f is true *) fun separate f nil = nil | separate f (a::L) = if (f a) then (a::(separate f L)) else separate f L; (* suppose one only wants to find one object for which f is true... *) fun separate2 f nil = nil | separate2 f (a::L) = if (f a) then [a] else separate2 f L; fun setminus a b = separate (fn x=>not(foundinset x b)) a; (* sorting a set *) fun sortsetput (s:string) nil = [s] | sortsetput (s:string) (a::L) = if s < a then (s::(a::L)) else (a::(sortsetput s L)); fun sortset nil = nil | sortset (a::L) = sortsetput a (sortset L); (* functions *) (* find an object in the list associated with key s; return a one-element list of the found object if it is found, otherwise nil *) fun find s nil = nil | find s ((t,x)::rest) = if s = t then [x] else find s rest; (* a safe version of find which gives the object found and a default when there is no such object *) fun safefind default s L = let val A = find s L in if A = nil then default else (hd A) end; (* is there an object with key s in L? *) fun foundin s L = find s L <> nil; (* drop item with given key *) fun drop s nil = nil | drop s ((t,x)::L) = if s = t then L else ((t,x)::(drop s L)); (* an optimization, perhaps; it brings the found item to the front of the list. this version of find is used inside the thmresult function below. *) fun Find s reference = let val A = find s (!reference) in if A = nil then nil else (reference:=((s,hd A)::drop s (!reference));A) end; fun Safefind default s reference = let val A = Find s reference in if A = nil then default else (hd A) end; fun Foundin s L = Find s L <> nil; (* add item with given key; the first will not overwrite and the second will *) fun addto s x L = if foundin s L then L else ((s,x)::L); fun strongadd s x L = addto s x (drop s L); (* is a list of pairs a function? *) fun isfun nil = true | isfun ((s,x)::L) = let val A = find s L in if A = nil orelse A = [x] then isfun L else false end; (* merge function used with match lists; it returns nil as an error object, and packages resultant lists in a unit list *) fun merge L M = if isfun (union L M) then [union L M] else nil; (* BEGIN block for cmatch fun isrelfun f nil = true | isrelfun f ((s,x)::L) = let val A = find s L in if A = nil orelse ((f(hd A)) = (f x)) then isrelfun f L else false end; fun relmerge f L M = if isrelfun f (union L M) then [union L M] else nil; END block for cmatch *) (* sorting a function *) fun sortfunput (s:string,x) nil = [(s,x)] | sortfunput (s:string,x) ((a,y)::L) = if s < a then ((s,x)::((a,y)::L)) else ((a,y)::(sortfunput(s:string,x) L)); fun sortfun nil = nil | sortfun (a::L) = sortfunput a (sortfun L); (* The primary objects manipulated by Mark2 are terms; the manipulations allowed are algebraic. Atomic terms in Mark2 are of three kinds, constants (which must be declared), free and bound variables. Composite terms are of three kinds: terms constructed using binary infix operators (which must be declared; though there is a provision for variable infixes), function terms, and terms defined by cases. Unary operators are also supported, but they are coded as binary operators as will be seen below. *) (* the separate clauses for reserved identifiers and for case expressions are a new idea *) (* term data type declaration *) (* type of infix operators *) datatype operator = ConOp of string | VarOp of string | ResOp of string | (* reserved operator *) ParOp of string; (* an internal device *) datatype term = (* atomic terms *) Constant of string | Numeral of int list | (* Mark2 has built in arithmetic *) FreeVar of string | BoundVar of int | (* composite terms *) Infix of term*operator*term | Function of term | CaseExp of term*term*term | Parenthesis of term; (* Parenthesis is a special construction used internally for various purposes *) (* There are some differences between the surface form of Mark2 terms (as displayed and understood by a user) and the "deep structure" exhibited in the type declaration above. There are also some notational points not capable of being made in this format. All atomic terms are represented by strings made of alphanumeric characters plus the special characters "?" and "_". The empty string does not represent a constant; Constant "" is used internally as an error object. Strings made up entirely of digits stand for numerals. They are stored as lists of digits (in reverse order). The built in arithmetic of Mark2 is unlimited precision arithmetic of non-negative integers. Strings made up of the special character "?" followed by a non-zero-initial numeral represent bound variables. Strings which begin with "?" and do not represent bound variables are used to represent free variables. Strings which do not represent any of the above represent constants. Unlike the three other sorts of atomic term, constants need to be declared by the user. We now consider terms defined using operators. This includes the case of unary prefix operators, which are in fact supported by Mark2, though this is not reflected in the data type. An infix which has been declared may be used as a prefix operator if a declaration has been made which assigns to that infix a default left argument; when the operator is used as a prefix, an invisible left argument is present, equal to the default; moreover, when a term is entered in binary form whose left term happens to be the default left argument for its infix, the prover will display it in unary form. Operators are represented by nonempty strings made up entirely of special characters other than the two special characters allowed in atomic terms. Operators of more than one character beginning with "^" are operator variables. All other operators are constant operators and must be declared. A final refinement: an operator may actually end with alphanumerics: it consists of (zero or more) special characters possibly followed by a suffix consisting of one backquote "`" followed by zero or more alphanumerics, with the length of the whole being nonzero. Function terms are of the form [term]; a term enclosed in brackets is a function term. The appearance of bound variables is restricted to appropriate function terms; the bound variable ?n may only appear in a context within at least n nested brackets. Case expression terms take the surface form ?x || ?y , ?z This causes some peculiarities because the apparent subterm ?y , ?z does not correspond to any actual term. This is handled differently in the current version of Mark2, but a related problem occurs. *) (* we now give code for functions which retrieve the first token of a given kind (atomic term or operator) from a list of characters; it has a companion function which returns the rest of the string *) (* the tokenizer does not consult the declaration lists, but it does recognize reserved constants and operators *) (* the list of reserved operators *) val RESERVED = ref([("bogus",(0,0))]); (* RESERVED := nil; *) fun isreserved x = foundin x (!RESERVED); (* kinds of character *) fun iscap x = x = "A" orelse x= "B" orelse x = "C" orelse x = "D" orelse x = "E" orelse x = "F" orelse x = "G" orelse x = "H" orelse x = "I" orelse x = "J" orelse x = "K" orelse x = "L" orelse x = "M" orelse x = "N" orelse x = "O" orelse x = "P" orelse x = "Q" orelse x = "R" orelse x = "S" orelse x = "T" orelse x = "U" orelse x = "V" orelse x = "W" orelse x = "X" orelse x = "Y" orelse x = "Z"; fun islowercase x = x = "a" orelse x= "b" orelse x = "c" orelse x = "d" orelse x = "e" orelse x = "f" orelse x = "g" orelse x = "h" orelse x = "i" orelse x = "j" orelse x = "k" orelse x = "l" orelse x = "m" orelse x = "n" orelse x = "o" orelse x = "p" orelse x = "q" orelse x = "r" orelse x = "s" orelse x = "t" orelse x = "u" orelse x = "v" orelse x = "w" orelse x = "x" orelse x = "y" orelse x = "z"; fun isspecial x = x = "!" orelse x = "@" orelse x = "#" orelse x = "$" orelse x = "%" orelse x = "^" orelse x = "&" orelse x = "*" orelse x = "=" orelse x = "+" orelse x = "-" orelse x = "<" orelse x = ">" orelse x = "/" orelse x = "," orelse x = ";" orelse x = "." orelse x = ":" orelse x = "~" orelse x = "|"; fun isdigit x = x = "0" orelse x = "1" orelse x = "2" orelse x = "3" orelse x = "4" orelse x = "5" orelse x = "6" orelse x = "7"orelse x = "8" orelse x = "9"; (* remove whitespace *) fun strip nil = nil | strip (" "::L) = strip L | strip ("\n"::L) = strip L | strip ("\t"::L) = strip L | strip L = L; fun isalpha x = iscap x orelse islowercase x orelse isdigit x orelse x = "?" orelse x = "_"; (* get desired characters from a list of characters *) fun getalpha nil = nil | getalpha (a::L) = if isalpha a then a::(getalpha L) else nil and restalpha nil = nil | restalpha (a::L) = if isalpha a then restalpha L else (a::L); fun getnumeral nil = nil | getnumeral (a::L) = if isdigit a then a::(getnumeral L) else nil and restnumeral nil = nil | restnumeral (a::L) = if isdigit a then restnumeral L else (a::L); fun getspecial nil = nil | getspecial (a::L) = if isspecial a then (a::(getspecial L)) else if a = "`" then (a::(getalpha L)) else nil and restspecial nil = nil | restspecial (a::L) = if isspecial a then restspecial L else if a = "`" then restalpha L else (a::L); (* integer character value *) fun numvalue "0" = 0 | numvalue "1" = 1 | numvalue "2" = 2 | numvalue "3" = 3 | numvalue "4" = 4 | numvalue "5" = 5 | numvalue "6" = 6 | numvalue "7" = 7 | numvalue "8" = 8 | numvalue "9" = 9 | numvalue x = ~1; (* fun evalnum nil = 0 | evalnum ("0"::L) = 0 + 10*(evalnum L) | evalnum ("1"::L) = 1 + 10*(evalnum L) | evalnum ("2"::L) = 2 + 10*(evalnum L) | evalnum ("3"::L) = 3 + 10*(evalnum L) | evalnum ("4"::L) = 4 + 10*(evalnum L) | evalnum ("5"::L) = 5 + 10*(evalnum L) | evalnum ("6"::L) = 6 + 10*(evalnum L) | evalnum ("7"::L) = 7 + 10*(evalnum L) | evalnum ("8"::L) = 8 + 10*(evalnum L) | evalnum ("9"::L) = 9 + 10*(evalnum L) | evalnum x = ~1; *) fun evalnum nil = 0 | evalnum (x::L) = if isdigit x then let val A = evalnum L in if A = ~1 then ~1 else (numvalue x) + (10*A) end else ~1; fun listtoint nil = 0 | listtoint (n::L) = n + 10*(listtoint L); (* strips unwanted zeroes off fronts of numerals *) fun stripzeroes nil = (0::nil) | stripzeroes (0::nil) = 0::nil | stripzeroes (0::L) = stripzeroes L | stripzeroes L = L; (* strips unwanted zeroes off ends of reversed lists of digits (our internal representation of integers) *) fun stripzeroes2 L = rev(stripzeroes(rev L)); (* functions which extract the first atom represented in a list of characters and return the rest of the list *) fun prefirstatom s = let val A = getnumeral s and B = getalpha s in if A <> nil andalso A = B then Numeral (rev (stripzeroes(map numvalue A))) else if B<>nil then if hd B = "?" then let val C = getnumeral (tl B) in if C <> nil andalso C = tl B then BoundVar (evalnum (rev C)) else FreeVar (implode B) end else Constant (implode B) else Constant "" end (* conventional error value *) and prerestfirstatom s = let val A = getnumeral s and B = getalpha s in if A <> nil andalso A = B then restnumeral s else if B<>nil then restalpha s else s end (* conventional error value *) (* this function returns the first atomic term in the string s, if any. A locution like "stringtocon s = FreeVar s" asks whether s is a free variable; in the case of constants, one also needs to stipulate that s is not "" *) fun stringtocon s = prefirstatom (strip (explode s)); fun firstatom s = prefirstatom (strip s); fun restfirstatom s = prerestfirstatom (strip s); (* functions for getting the first operator from a list of characters and the rest of the list *) fun prefirstop s = let val A = getspecial s in if A = nil then ConOp "" (* error value *) else if hd A = "^" andalso tl A <> nil then VarOp (implode A) else if isreserved (implode A) then ResOp (implode A) else ConOp (implode A) end; (* this function gets the first operator from a string; see comments under stringtocon *) fun stringtoop s = prefirstop (strip (explode s)); fun firstop s = prefirstop (strip s); fun restfirstop s = restspecial (strip s); (* cleans up parentheses -- appears here because stringtoop is needed *) fun deparenthesize1 (Parenthesis t) = t | deparenthesize1 t = t; fun deparenthesize (Parenthesis t) = deparenthesize t | deparenthesize (Function s) = Function(deparenthesize s) | deparenthesize (Infix(x,ParOp s,y)) =Infix(deparenthesize x, stringtoop s, deparenthesize y) | deparenthesize (Infix(x,i,y)) = Infix(deparenthesize x,i, deparenthesize y) | deparenthesize (CaseExp(u,v,w)) = CaseExp(deparenthesize u, deparenthesize v,deparenthesize w) | deparenthesize t = t; (* We now construct a family of functions culminating in the parser. In this version, we do not allow user declared precedence, which is found in the full implementation; most users have been content with the APL precedence (all operators have same precedence, all operators group to the right) which is the default in the full implementation *) (* We begin with the declaration lists (needed by the display function to handle prefix operators, as well as by the parser), follow with the display functions, and conclude with the parser *) (* the constant declaration list *) val CONSTANTS = ref(["bogus"]); fun isaconstant s = (stringtocon s = Numeral (rev(stripzeroes(map (numvalue) (explode s))))) orelse foundinset s (!CONSTANTS); (* USER COMMAND *) fun declareconstant s = if s <> "" andalso stringtocon s = Constant s then if foundinset s (!CONSTANTS) then errormessage ("Constant "^s^" already declared") else CONSTANTS:=addtoset s (!CONSTANTS) else errormessage ("Ill-formed constant "^s^" cannot be declared"); (* operator declarations *) (* operators require integer "left type" and "right type" parameters for the stratification function *) val OPERATORS = ref([("bogus",(1,2))]); fun isoperator s = if stringtoop s = VarOp s then true else if stringtoop s = ResOp s then true else if s <> "" andalso stringtoop s = ConOp s then if foundin s (!OPERATORS) then true else false else false; val defaultop = (0,0); fun opof s = if (stringtoop s) = ResOp s then safefind defaultop s (!RESERVED) else safefind defaultop s (!OPERATORS); fun lefttype s = (fn (a,b) => a) (opof s); fun righttype s = (fn (a,b) => b) (opof s); (* It is permissible to declare variable operators in order to record their type information *) (* USER COMMAND *) fun declaretypedinfix m n s = if stringtoop s = ResOp s then errormessage ("Reserved operator "^s^" cannot be redeclared") else if stringtoop s = VarOp s then if foundin s (!OPERATORS) then errormessage ("Variable operator "^s^" has already been typed") else OPERATORS:= addto s (m,n)(!OPERATORS) else if s <> "" andalso stringtoop s = ConOp s then if foundin s (!OPERATORS) then errormessage ("Operator "^s^" has already been declared") else OPERATORS:= addto s (m,n) (!OPERATORS) else errormessage ("Ill-formed operator "^s^" cannot be declared"); (* Declaration of reserved operators: not a user command! *) fun reserveop m n s = if s <> "" andalso stringtoop s = ConOp s andalso (not (isoperator s)) then RESERVED:=addto s (m,n) (!RESERVED) else errormessage ("Improper operator reservation of "^s); (* reserveop 0 0 "||"; reserveop 0 0 ","; *) (* declares the usual "flat" operators with only trivial type information *) (* USER COMMAND *) fun declareinfix s = declaretypedinfix 0 0 s; (* lists of operators with special properties needed by the stratification functions of the prover *) val OPAQUE = ref["bogus"]; val SCOUT = ref[("bogus","bogus")]; val SCINLEFT = ref[("bogus","bogus")]; val SCINRIGHT = ref[("bogus","bogus")]; (* opaque operators are "opaque" to abstraction; one cannot define a function in a way which essentially involves an opaque operator (an opaque operator could appear in the name of a constant) *) (* distinct from defined opaque "constant" operators (not used in any current theory, though they could be) are opaque variable operators; an operator variable with declared type matches only operators of that same type, while an opaque operator matches any operator, and for that reason must observe the same restrictions on abstraction as an opaque declared operator *) fun isopaque s = foundinset s (!OPAQUE); fun istypedoperator s = (foundin s (!RESERVED) orelse foundin s (!OPERATORS)) andalso not (isopaque s); (* declare opaque operator *) fun declareopaque s = if stringtoop s = ResOp s then errormessage ("Reserved operator "^s^" cannot be made opaque") else if stringtoop s = VarOp s then if foundin s (!OPERATORS) then errormessage ("Reserved or variable operator "^s^" has already been typed") else (OPERATORS:= addto s (0,0)(!OPERATORS);OPAQUE:=addtoset s (!OPAQUE)) else if s <> "" andalso stringtoop s = ConOp s then if foundin s (!OPERATORS) then errormessage ("Operator "^s^" has already been declared") else (OPERATORS:= addto s (0,0) (!OPERATORS);OPAQUE:=addtoset s (!OPAQUE)) else errormessage ("Ill-formed operator "^s^" cannot be declared"); (* scout = strongly Cantorian output; scinleft = strongly Cantorian input (left argument) and scinright = strongly Cantorian input (right argument) strongly Cantorian = (in practice) belonging to some data type *) val SCINSCOUT = ref ["bogus"]; (* list used in posting axiom dependencies induced by scin/scout functions *) fun scoutof s = safefind "" s (!SCOUT); fun scinleftof s = safefind "" s (!SCINLEFT); fun scinrightof s = safefind "" s (!SCINRIGHT); fun isscout s = let val A = foundin s (!SCOUT) in (if A then SCINSCOUT:=addtoset (scoutof s) (!SCINSCOUT) else ();A) end; fun isscinleft s = let val A = foundin s (!SCINLEFT) in (if A then SCINSCOUT:=addtoset (scinleftof s) (!SCINSCOUT) else ();A) end; fun isscinright s = let val A = foundin s (!SCINRIGHT) in (if A then SCINSCOUT:=addtoset (scinrightof s) (!SCINSCOUT) else ();A) end; (* assignment of scin/scout properties to theorems needs to be witnessed by existence of theorems of appropriate forms and will be handled later *) (* prefix display declarations -- needed for display as well as parser *) (* variable prefix operators are needed! *) (* the default left argument of an operator will be an atomic constant *) val PREFIX = ref([("bogus","bogus")]); (* PREFIX := nil; *) fun prefixof s = safefind "" s (!PREFIX); fun hasprefix s = foundin s (!PREFIX); (* command to assign a default left argument to an operator; this version only permits such an assignment to be made once *) (* USER COMMAND *) fun declareprefix s t = if hasprefix s then errormessage ("Cannot reassign default left argument of "^s) else if (stringtoop s = ResOp s orelse (stringtoop s = ConOp s andalso isoperator s)) andalso isaconstant t then PREFIX := addto s t (!PREFIX) else errormessage ("Invalid prefix "^t^" proposed for operator "^s); (* NOT a user command -- this command creates strict prefix operators, which are those operators which have a prefix on the list equal to "" *) (* it is necessary to be able to declare strict prefix operator variables so that one can build structural tactics which will work on prefix terms *) fun isstrictprefix s = hasprefix s andalso prefixof s = ""; fun declarestrictprefix s = if (stringtoop s = ResOp s orelse stringtoop s = VarOp s orelse (stringtoop s = ConOp s andalso isoperator s)) then PREFIX := addto s "" (!PREFIX) else errormessage ("Undeclared operator "^s^" cannot be declared strict prefix"); (* declarations of strictly unary operators *) fun declaretypedunary n s = (declaretypedinfix 0 n s; declarestrictprefix s); fun declareunary s = declaretypedunary 0 s; fun declareunaryopaque s = (declareopaque s; declarestrictprefix s); (* default type handling: this allows the suppression of type labels on variables which are understood to usually have a given type; the type label infix : appears as a prefix operator in this case *) val VARTYPES = ref [("bogus",Constant "")]; (* VARTYPES := nil; *) fun hasdefaulttype v = foundin v (!VARTYPES); fun defaulttypeof v = safefind (Constant "") v (!VARTYPES); fun hasdtprefix ":" (FreeVar v) = hasdefaulttype v | hasdtprefix s t = false; fun dtprefixof ":" (FreeVar v) = defaulttypeof v | dtprefixof s t = Constant ""; fun haseitherprefix s t = hasprefix s orelse hasdtprefix s t; fun eitherprefixof s t = if hasprefix s then stringtocon (prefixof s) else dtprefixof s t; (* USER COMMAND *) fun notypeinfo v = if foundin v (!VARTYPES) then VARTYPES:=drop v (!VARTYPES) else errormessage ("No default type for "^v^" found to drop"); (* function for assigning types is found below; it requires declaration checking *) (* I might want to add scin/scout information *) fun showdec s = if stringtocon s = Constant s then if isaconstant s then errormessage (s^" is a declared constant") else errormessage ("Undeclared constant "^s) else if stringtocon s = Numeral (rev (stripzeroes(map numvalue (explode s)))) then errormessage "Numerals are predeclared" else if (stringtoop s = ResOp s) then if isopaque s then errormessage ("Opaque reserved operator "^s) else if isoperator s then errormessage ("Reserved operator "^s^" left type: " ^(makestring (lefttype s))^" right type: " ^(makestring(righttype s)^ " left arg (if any): "^(prefixof s))) else errormessage ("Undeclared reserved operator?!") else if (stringtoop s = ConOp s) then if isopaque s then errormessage ("Opaque declared operator "^s) else if isoperator s then errormessage ("Declared operator "^s^ " left type: " ^(makestring (lefttype s))^" right type: " ^(makestring(righttype s))^ (if hasprefix s then if prefixof s = "" then " Prefix operator only" else " Default left argument: "^(prefixof s) else " Infix argument only")) else errormessage ("Undeclared operator") else if stringtoop s = VarOp s andalso foundin s (!OPERATORS) then errormessage ("Typed variable operator "^s^" left type: " ^(makestring (lefttype s))^" right type: "^ (makestring(righttype s))^ (if hasprefix s then " (strict prefix)" else "")) else if stringtoop s = VarOp s andalso isopaque s then errormessage ("Opaque operator variable "^s^ (if hasprefix s then " (strict prefix)" else "")) else if stringtoop s = VarOp s then errormessage ("Undeclared operator variable "^s) else errormessage "No applicable declaration"; (* simple display function *) fun opdisplay (ConOp s) = s | opdisplay (VarOp s) = s | opdisplay (ResOp s) = s | opdisplay (ParOp s) = "{"^s^"}"; (* the master precedence list *) val PRECEDENCES = ref ([("bogus",0)]); (* PRECEDENCES:=nil; *) (* default precedence *) val DEFAULTPREC = ref 0; (* user command to set precedence of an operator *) fun setprecedence s n = if n<0 then setprecedence s 0 else PRECEDENCES := strongadd s n (!PRECEDENCES); (* user command to set default precedence *) fun setdefaultprec n = if n < 0 then setdefaultprec 0 else DEFAULTPREC := n; (* user command to reset precedences to standard *) fun clearprecs () = (PRECEDENCES := nil; DEFAULTPREC := 0); fun precedenceof s = safefind (!DEFAULTPREC) s (!PRECEDENCES); fun stickiness (Infix(x,s,y)) = precedenceof (opdisplay s) | stickiness (CaseExp(u,v,w)) = precedenceof "||" | stickiness x = 0; (* this refers to surface form *) fun isinfixterm (Infix(x,s,y)) = true | isinfixterm (CaseExp(u,v,w)) = true | isinfixterm x = false; (* parentest x s b tells us whether term x needs to be parenthesized when it is term b (left term has b=0, right term has b=1) in an infix term with infix s *) fun parentest x s b = isinfixterm x andalso ((stickiness x < precedenceof (opdisplay s)) orelse (stickiness x = precedenceof (opdisplay s) andalso ((stickiness x) mod 2 = b))); (* pp for "possible parenthesis" *) fun pp x s b p = if parentest x s b then p else ""; (* function for converting preparsed terms to correct form *) fun reassociate1 (Infix(x,s,Infix(y,t,z))) = if ((precedenceof (opdisplay s) > precedenceof (opdisplay t)) orelse (precedenceof (opdisplay s) = precedenceof (opdisplay t) andalso ((precedenceof (opdisplay s)) mod 2) = 1)) (* andalso y <> eitherprefixof (opdisplay t) z *) then Infix(reassociate1(Infix(x,s,y)),t,z) else (Infix(x,s,Infix(y,t,z))) | reassociate1 t = t; fun reassociate (Parenthesis t) = Parenthesis (reassociate t) | reassociate (Function t) = Function (reassociate t) | reassociate (Infix(x,s,y)) = reassociate1 (Infix(reassociate x,s,reassociate y)) | reassociate t = t; (* baredisplay should now handle user-defined precedence correctly *) fun baredisplay (Constant s) = s | baredisplay (Numeral n) = implode(rev (map makestring n)) | baredisplay (FreeVar s) = s | baredisplay (BoundVar s) = "?"^(makestring s) | baredisplay (Infix(t,i,u)) = let val T = baredisplay t in (* the baredisplay function does not use default type information; this avoids trouble for load and save commands *) if T = prefixof (opdisplay i) then (opdisplay i)^" "^(pp u i 1 "(")^ (baredisplay u)^(pp u i 1 ")") else (pp t i 0 "(")^T^(pp t i 0 ")")^" " ^(opdisplay i)^" " ^(pp u i 1 "(") ^(baredisplay u)^(pp u i 1 ")") end | baredisplay (Function t) = "["^(baredisplay t)^"]" | (* display of case expressions "cheats"; it relies on the surface form of case expressions as complex infix expressions *) (* this works because the display functions are independent of declarations *) baredisplay (CaseExp(t,u,v)) = baredisplay (Infix(t,ResOp("||"),Infix(u,ResOp(","),v))) | (* the case for Parenthesis handles highlighting the current subterm *) baredisplay (Parenthesis t) = "{"^(baredisplay t)^"}"; val CURSOR = ref 0; fun bumpcursor s = (CURSOR:=(!CURSOR)+(length(explode s));s); val MARGIN = ref 50; fun setline n = MARGIN:=n; fun spaces 0 = " " | spaces n = (spaces (n-1))^" "; fun predashes 0 = "" | predashes 1 = " " | predashes 2 = " " | predashes 3 = " " | predashes n = if n<0 then "" else (predashes (n-1))^"-"; fun dashes() = predashes (!MARGIN); fun Newline() = (CURSOR:=0;"\n"); fun maybebreak d = if (!CURSOR) >= (!MARGIN) then (Newline()^bumpcursor(spaces d)) else ""; fun predisplay d (Constant s) = (bumpcursor s) | predisplay d (Numeral n) = (bumpcursor (implode(rev (map makestring n)))) | predisplay d (FreeVar s) =(bumpcursor s) | predisplay d (BoundVar s) = (bumpcursor ("?"^(makestring s))) | predisplay d (Infix(t,i,u)) = let val T = baredisplay t in if T = baredisplay(eitherprefixof (opdisplay i) u) then (bumpcursor (opdisplay i)) ^" " ^(bumpcursor (pp u i 1 "(")) ^(predisplay (if parentest u i 1 then d+1 else d) u) ^(bumpcursor (pp u i 1 ")")) else (bumpcursor (pp t i 0 "(")) ^(predisplay (if parentest t i 0 then d+1 else d) t) ^(bumpcursor (pp t i 0 ")")) ^(bumpcursor " ") ^(maybebreak d) ^(bumpcursor(opdisplay i)) ^(bumpcursor " ") ^(bumpcursor (pp u i 1 "(")) ^(predisplay (if parentest t i 0 then d+1 else d) u) ^(bumpcursor (pp u i 1 ")")) end | predisplay d (Function t) = (bumpcursor "[")^ (predisplay (d+1) t)^(bumpcursor "]") | (* display of case expressions "cheats"; it relies on the surface form of case expressions as complex infix expressions *) (* this works because the display functions are independent of declarations *) predisplay d (CaseExp(t,u,v)) = predisplay d (Infix(t,ResOp("||"),Infix(u,ResOp(","),v))) | (* the case for Parenthesis handles highlighting the current subterm *) predisplay d (Parenthesis t) = (bumpcursor "{") ^(predisplay (d+1) t)^(bumpcursor "}"); fun display t = (CURSOR:=0;(spaces 0)^(predisplay 0 t)); (* the parser *) (* the parser engine works, like the tokenizer, with a list of characters *) (* functions for extracting projections from pairs *) fun p1(x,y) = x; fun p2(x,y) = y; (* the only change involved in user-defined precedence is recording of user-supplied parentheses *) fun getfirstterm L = if (strip L) = nil then (Constant "", nil) else let val A = firstatom L and B = strip(restfirstatom L) in if A <> Constant "" then (* first term is atomic *) (A,B) else let val C = firstop L and D = strip(restfirstop L) in if C <> ConOp "" then (* first term has a prefix operator *) let val E = getterm D in if haseitherprefix (opdisplay C) (p1 E) then if p1 E = Constant "" then (Constant "",nil) else (Parenthesis( Infix(eitherprefixof(opdisplay C)(p1 E), C,p1 E)),p2 E) else (Infix(Constant "",C,p1 E),p2 E) end else if hd (strip L) = "[" then (* function term *) let val G = getterm (tl(strip L)) in if p1 G = Constant "" orelse p2 G = nil orelse hd(p2 G) <> "]" then (Constant "", nil) else (Function(p1 G),strip(tl(p2 G))) end else if hd (strip L) = "(" then (* parenthesis term *) let val G = getterm (tl(strip L)) in if p1 G = Constant "" orelse p2 G = nil orelse hd(p2 G) <> ")" then (Constant "", nil) else (Parenthesis (p1 G),strip(tl(p2 G))) end else (Constant "",nil) end end and getterm L = let val (A,B) = getfirstterm L in if A = Constant "" then (Constant "",nil) else if B = nil orelse hd B = "]" orelse hd B = ")" then (A,B) else let val C = firstop B and D = strip(restfirstop B) in if C = ConOp "" then (Constant "",nil) else let val E = getterm D in if p1 E = Constant "" then (Constant "",nil) else (Infix(A,C,p1 E),p2 E) end end end; (* the parser reads case expressions as a particular kind of infix expression; the casefix function rectifies this situation and rejects expressions of the form ?x || ?y where ?y is not a pair. *) fun casefix (Infix(x, ResOp "||",Infix(y,ResOp",",z))) = CaseExp(casefix x,casefix y,casefix z) | casefix (Infix(x,ResOp"||",y)) = (errormessage "Ill-formed case expression"; Constant "") | casefix (Function t) = Function (casefix t) | casefix (Infix (x,s,y)) = Infix(casefix x,s,casefix y) | casefix t = t; fun parse s = let val A = getterm(explode s) in if p2 A = nil then casefix(deparenthesize(reassociate(p1 A))) else Constant "" end; (* the theorem-embedding infixes which signal intentions to rewrite *) (* reserveop 0 0 "=>"; reserveop 0 0 "<="; *) (* they are actually declared in the setup command at the end *) (* in the old version, =>> and <<= were rule infixes as well, but they are not in this version (they are operators linking a pair of theorems) *) fun ruleinfix s = s = "=>" orelse s = "<="; (* operators of built-in arithmetic *) (* the declarations are actually made later in the setup command *) (* reserveop 0 0 "+!"; reserveop 0 0 "-!"; reserveop 0 0 "*!"; reserveop 0 0 "/!"; reserveop 0 0 "%!"; reserveop 0 0 "!"; reserveop 0 0 "=!"; *) fun arithop s = s = "+!" orelse s = "-!" orelse s = "*!" orelse s = "/!" orelse s = "%!" orelse s = "!" orelse s = "=!"; (* the rulefree function certifies a term as free of "execution behaviour" *) (* execution behaviour refers to presence of embedded theorems, operations of the built-in arithmetic, or case expressions whose hyotheses are truth values or equations with first term true. This omits the case of "functional programs" found in the original implementation; it adds the new case of equations with first term true *) (* declarations for functional programming *) val PROGRAMS = ref ([("bogus","bogus")]); (* command setprogram to bind a program to a constant or operator is found below *) (* USER COMMAND *) (* user program to remove any tactic bound to a function or operator *) fun deprogram s = PROGRAMS := drop s (!PROGRAMS); fun hasprogram s = foundin s (!PROGRAMS); fun programof s = safefind "" s (!PROGRAMS); (* moved here from near changehlevel below because of needs of enhanced higher-order matching *) fun changelevel source target (BoundVar s) = if s <= source andalso s <= target then BoundVar s else if s <= source andalso s > target then Constant "" else BoundVar (target + (s - source)) | changelevel source target (Function t) = let val TRY = changelevel source target t in if TRY = Constant "" then Constant "" else Function TRY end | changelevel source target (Infix(x,i,y)) = let val TRY1 = changelevel source target x and TRY2 = changelevel source target y in if (TRY1 = Constant "" andalso ((not(hasprefix (opdisplay i))) orelse prefixof (opdisplay i) <> "")) orelse TRY2 = Constant "" then Constant "" else Infix(TRY1,i,TRY2) end | changelevel source target (CaseExp(u,v,w)) = let val TRY1 = changelevel source target u and TRY2 = changelevel source target v and TRY3 = changelevel source target w in if TRY1 = Constant "" orelse TRY2 = Constant "" orelse TRY3 = Constant "" then Constant "" else (CaseExp(TRY1,TRY2,TRY3)) end | changelevel source target (Parenthesis u) = let val TRY = changelevel source target u in if TRY = Constant "" then Constant "" else Parenthesis TRY end | changelevel source target t = t; fun rulefree (Infix(Numeral m,ResOp s,Numeral n)) = not(arithop s) | rulefree (Infix(Function t,ResOp"@",BoundVar 0)) = false | rulefree (Infix(x,ResOp s, y)) = (not(ruleinfix s)) andalso rulefree x andalso rulefree y | rulefree (CaseExp(Infix(Constant"true",ResOp"=",x),y,z)) = false | rulefree (CaseExp (u,v,w)) = u <> Constant "true" andalso u <> Constant "false" andalso rulefree u andalso rulefree v andalso rulefree w | rulefree (Function t) = rulefree t | rulefree (Infix(x,i,y)) = rulefree x andalso rulefree y | rulefree t = true; (* the master declaration checking function; it checks constants, operators, and bound variables for meaningfulness *) (* declarecheck sends error messages (if the quiet parameter is false), but only for the first error it encounters *) (* design decision: we do not check for meaningless m|-|n, because such things appear to be harmless (and even potentially useful) *) fun declarecheck quiet (level:int) (Constant s) = if isaconstant s then true else ((if quiet then () else errormessage ("Undeclared constant "^s^" found"));false) | declarecheck quiet level (Numeral n) = true | declarecheck quiet level (FreeVar s) = true | declarecheck quiet level (BoundVar s) = if s<=level (* andalso s <> 0 *) then true else ((if quiet then () else errormessage ("Meaningless bound variable ?"^(makestring s)^" found"));false) | declarecheck quiet level (Function t) = declarecheck quiet ((level:int)+1) t | declarecheck quiet level (CaseExp(u,v,w)) = (declarecheck quiet level u) andalso (declarecheck quiet level v) andalso (declarecheck quiet level w) | declarecheck quiet level (Infix(u,ResOp s,v)) = if isstrictprefix s then if u = Constant "" then declarecheck quiet level v else ((if quiet then () else errormessage ("Exclusive prefix operator "^s^" used as infix"));false) else (* if ruleinfix s then rulefree u andalso (declarecheck quiet level u) andalso (declarecheck quiet level v) (* embedded theorems may not themselves have any execution behaviour *) else *) (declarecheck quiet level u) andalso (declarecheck quiet level v) | declarecheck quiet level (Infix(u,VarOp s,v)) = if stringtoop s <> VarOp s then ((if quiet then () else errormessage ("Ill-formed infix variable "^s));false) else if isstrictprefix s then if u = Constant "" then declarecheck quiet level v else ((if quiet then () else errormessage ("Exclusive prefix operator "^s^" used as infix"));false) else (declarecheck quiet level u) andalso (declarecheck quiet level v) | declarecheck quiet level (Infix(u,ConOp s,v)) = if isstrictprefix s then if u = Constant "" then (declarecheck quiet level v) andalso if isoperator s then true else ((if quiet then () else errormessage ("Undeclared operator "^s^" found"));false) else ((if quiet then () else errormessage ("Exclusive prefix operator "^s^" used as infix"));false) else (declarecheck quiet level u) andalso (declarecheck quiet level v) andalso if isoperator s then true else ((if quiet then () else errormessage ("Undeclared operator "^s^" found"));false) | declarecheck quiet level (Parenthesis u) = ((if quiet then () else errormessage ("Braces found"));false); (* stratification checking *) (* reserveop 0 0 ":"; *) (* the type label (retraction) infix *) (* the actual declaration is deferred to setup *) (* the stratification function takes as its parameter a local type and generates a list of lists of type assignments to bound variables, which will be empty if there is no consistent type assignment; otherwise, the first of these lists will be the types fixed for bound variables in the given context, while subsequent lists record known "relative" types which may be shifted by a constant amount *) (* utilities which operate on lists of type assignments *) fun shifttype n nil = nil | shifttype (n:int) ((p,q)::L) = ((p,q+n)::shifttype n L); (* finds a candidate for the displacement between two type assignments -- does not check for consistency! *) (* returns nil if there is no point of contact between the lists *) fun typediff nil L = nil | typediff ((p,q:int)::L) M = let val A = find p M in if A = nil then typediff L M else [q -(hd A)] end; (* shiftmerge, given two type assignment lists, returns the list of the two if they have no point of contact, returns nil if they are inconsistent, and returns the merged list otherwise (shifting the second list by the amount reported by typediff) *) (* the first two clauses allow for considerable simplification; "floating" lists with zero or one entry do not supply any information, but may not merge using the third clause *) fun shiftmerge L nil = [L] | shiftmerge L (x::nil) = [L] | shiftmerge L M = if typediff L M = nil then [L, M] else merge L (shifttype (hd (typediff L M)) M); (* crushtypes simplifies a list of type assignment lists, merging any lists which have a point of contact and preserving the special role of the head of the list (whose types must be fixed) *) fun crushtypes nil = nil | crushtypes (L::nil) = (L::nil) | crushtypes (L::(M::rest)) = let val A = crushtypes (M::rest) in if A = nil then nil else let val (N::rest2) = A in if shiftmerge L N = nil then nil else if shiftmerge L N = [L,N] then ((crushtypes (L::rest2))@[N]) else crushtypes ((shiftmerge L N)@rest2) end end; (* merges two type lists *) fun mergetypes nil L = nil | mergetypes M nil = nil | mergetypes (L::rest1) (M::rest2) = if merge L M = nil then nil else crushtypes((merge L M)@rest1@rest2); (* checkappend is used in strat for "floating" a type list; we check that the list we are "floating" isn't nil before we prepend [nil] to it *) fun checkappend L M = if M = nil then nil else L@M; (* list of "locally free" bound variables on which a term depends -- obviously this needs the level as a parameter *) fun boundvarlist level (BoundVar s) = if s=0 then nil else [s] | boundvarlist level (Infix(u,i,v)) = union (boundvarlist level u) (boundvarlist level v) | boundvarlist level (Function t) = dropfromset (level + 1) (boundvarlist (level+1) t) | boundvarlist level (CaseExp(u,v,w)) = union (boundvarlist level u) (union (boundvarlist level v)(boundvarlist level w)) | boundvarlist level t = nil; (* the main stratification function *) (* another stratification function will be needed by the definition function -- it will type free variables rather than bound variables *) val CHECKTYPE = ref 0; fun strat level localtype (Constant s) = [nil] | strat level localtype (FreeVar s) = [nil] | strat level localtype (Numeral s) = [nil] | strat level localtype (BoundVar s) = if s = 0 then [nil] else [[(s,localtype)]] | strat level localtype (Function s) = map (drop (level+1)) (mergetypes (strat (level+1) (localtype-1) s) [[(level+1,localtype-1)]]) | strat level localtype (CaseExp(t,u,v)) = mergetypes((checkappend[nil](strat level localtype t))) (mergetypes(strat level localtype u) (strat level localtype v)) | strat level localtype (Infix(t,ResOp":",u)) = mergetypes (strat level (localtype+1) t) (checkappend [nil] (strat level localtype u)) | strat level localtype (Infix(Constant f,ResOp "@",t)) = crushtypes(checkappend (if level = 0 orelse isscout f orelse isscinright f then [nil] else []) (strat level localtype t)) | strat level localtype (Infix(Infix(t,ResOp"@!",m),ResOp"@!",n)) = mergetypes (strat level (localtype+(!CHECKTYPE)) n) (strat level (localtype+(!CHECKTYPE)) (Infix(t,ResOp"@!",m))) | strat level localtype (Infix(Function t,ResOp "@!",n)) = if declarecheck true 0 (changelevel level 0 (Function t)) then mergetypes (strat level (localtype+(!CHECKTYPE)) n) (strat level localtype (Function t)) else nil | strat level localtype (Infix(FreeVar t,ResOp "@!",n)) = strat level (localtype+(!CHECKTYPE)) n | strat level localtype (Infix(t,ResOp"@!",u)) = nil | strat level localtype (Infix(t,i,u)) = if istypedoperator (opdisplay i) then crushtypes(checkappend (if level = 0 orelse isscout (opdisplay i) then [nil] else []) (mergetypes (checkappend(if level = 0 orelse isscinleft (opdisplay i) then [nil] else []) (strat level (lefttype(opdisplay i)+localtype) t)) (checkappend(if level = 0 orelse isscinright (opdisplay i) then [nil] else []) (strat level (righttype(opdisplay i)+localtype) u)))) else (* case of opaque or undeclared variable operators *) if boundvarlist level (Infix(t,i,u)) = nil andalso strat level 0 t <> nil andalso strat level 0 u <> nil then [nil] else nil; (* the double check supports the peculiar behavior of "@!" *) (* functions to check segregation of general free variables from free variables matching possibly inhomogeneous operators *) fun segregationlist1 (Infix(FreeVar P,ResOp"@!",t)) = addtoset P (segregationlist1 t) | segregationlist1 (Function t) = segregationlist1 t | segregationlist1 (Infix(x,i,y)) = union(segregationlist1 x)(segregationlist1 y) | segregationlist1 (CaseExp(u,v,w)) = union(segregationlist1 u) (union(segregationlist1 v)(segregationlist1 w)) | segregationlist1 t = nil; fun segregationlist2 (Infix(FreeVar P,ResOp"@!",t)) =(segregationlist2 t) | segregationlist2 (FreeVar P) = [P] | segregationlist2 (Function t) = segregationlist2 t | segregationlist2 (Infix(x,i,y)) = union(segregationlist2 x)(segregationlist2 y) | segregationlist2 (CaseExp(u,v,w)) = union(segregationlist2 u) (union(segregationlist2 v)(segregationlist2 w)) | segregationlist2 t = nil; fun issegregated t = intersection(segregationlist1 t) (segregationlist2 t) = nil; fun isstratified level t = strat level 0 t <> nil andalso (CHECKTYPE:=1; let val S = strat level 0 t <> nil in (CHECKTYPE:=0;S) end) andalso issegregated t; (* USER COMMAND *) (* delayed to here because it uses declaration and stratification checking *) fun defaulttypeinfo v t = if stringtocon v = FreeVar v andalso declarecheck false 0 (parse t) andalso isstratified 0 (parse t) then VARTYPES := strongadd v (parse t) (!VARTYPES) else errormessage ("Declaration or syntax error in assigning type "^t^" to variable "^v); (* the prover environment comes into view! *) (* the prover environment consists of the following elements: name of environment (a string) "format" of environment (a term, used to indicate parameters of a parameterized theorem/tactic) left side of equation being proved (a term) right side of equation being proved (a term) current position in term (a list of booleans, true = right, false = left, the step into a function term is either right or left indifferently) current level and "hypothesis level" (two integers) list of local hypotheses (a list of "theorems" derived from hypotheses of case expressions -- a triple consisting of two terms to be equated and an integer coding the "sense" (positive, negative, or inactive) of the hypothesis) dependencies of current environment -- only the traditional kind will be considered; the new definition and theorem-text dependencies will be maintained separately The theorem data structure is almost the same, except that it does not have position-dependent components *) (* a workhorse function -- apply a function to a term at a position *) fun applyat f nil t = f t | applyat f (a::L) (Constant s) = (errormessage "Subterm error";Constant s) | applyat f (a::L) (FreeVar s) = (errormessage "Subterm error";FreeVar s) | applyat f (a::L) (BoundVar s) = (errormessage "Subterm error";BoundVar s) | applyat f (a::L) (Numeral s) = (errormessage "Subterm error";Numeral s) | applyat f (a::L) (Function t) = Function (applyat f L t) | applyat f (false::L) (Infix(u,i,v)) = if u = Constant "" then (errormessage "Subterm error";(Infix(u,i,v))) else (Infix(applyat f L u,i,v)) | applyat f (true::L) (Infix(u,i,v)) = (Infix(u,i,applyat f L v)) | applyat f (false::L) (CaseExp(u,v,w)) = CaseExp(applyat f L u,v,w) | applyat f (true::(false::L)) (CaseExp(u,v,w)) = CaseExp(u,applyat f L v,w) | applyat f (true::(true::L)) (CaseExp(u,v,w)) = CaseExp(u,v,applyat f L w) | (* the Parenthesis case below helps prevent the prover from issuing an error message when just looking at the virtual subterm *) applyat f (true::nil) (CaseExp(u,v,w)) = ((let val A = f (Infix(v,ResOp",",w)) in if A = (Infix(v,ResOp",",w)) orelse A = Parenthesis((Infix(v,ResOp",",w))) then () else errormessage "Virtual subterm of case expression" end); (CaseExp(u,v,w))); (* the prover environment data type *) (* this is a structure with nine fields as indicated above *) fun ename (na,fo,lt,rt,po,lev,hlev,hyps,deps) = na; fun formatof (na,fo,lt,rt,po,lev,hlev,hyps,deps) = fo; fun leftside (na,fo,lt,rt,po,lev,hlev,hyps,deps) = lt; fun rightside (na,fo,lt,rt,po,lev,hlev,hyps,deps) = rt; fun position (na,fo,lt,rt,po,lev,hlev,hyps,deps) = po; fun level (na,fo,lt,rt,po,lev,hlev,hyps,deps) = lev; fun hlevel (na,fo,lt,rt,po,lev,hlev,hyps,deps) = hlev; fun hypslist (na,fo,lt,rt,po,lev,hlev,hyps,deps) = hyps; fun deps (na,fo,lt,rt,po,lev,hlev,hyps,deps) = deps; (* functions which change environment fields to given values *) fun changeename na2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na2,fo,lt,rt,po,lev,hlev,hyps,deps); fun changeformatof fo2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo2,lt,rt,po,lev,hlev,hyps,deps); fun changeleftside lt2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt2,rt,po,lev,hlev,hyps,deps); fun changerightside rt2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt2,po,lev,hlev,hyps,deps); fun changeposition po2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt,po2,lev,hlev,hyps,deps); fun changeelevel lev2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt,po,lev2,hlev,hyps,deps); fun changeehlevel hlev2 (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt,po,lev,hlev2,hyps,deps); fun changehypslist hyps2 (na,fo,lt,rt,po,lev,hlev,hyps,deps)= (na,fo,lt,rt,po,lev,hlev,hyps2,deps); fun changedeps deps2 (na,fo,lt,rt,po,lev,hlev,hyps,deps)= (na,fo,lt,rt,po,lev,hlev,hyps,deps2); (* functions which apply given functions to environment fields *) fun changeename2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (f na,fo,lt,rt,po,lev,hlev,hyps,deps); fun changeformatof2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,f fo,lt,rt,po,lev,hlev,hyps,deps); fun changeleftside2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,f lt,rt,po,lev,hlev,hyps,deps); fun changerightside2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,f rt,po,lev,hlev,hyps,deps); fun changeposition2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt,f po,lev,hlev,hyps,deps); fun changelevel2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt,po,f lev,hlev,hyps,deps); fun changehlevel2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps) = (na,fo,lt,rt,po,lev,f hlev,hyps,deps); fun changehypslist2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps)= (na,fo,lt,rt,po,lev,hlev,f hyps,deps); fun changedeps2 f (na,fo,lt,rt,po,lev,hlev,hyps,deps)= (na,fo,lt,rt,po,lev,hlev,hyps,f deps); (* the current prover environment *) val ENV = ref("",Constant "", Constant "", Constant "", [true],0,0,[(Constant"",Constant"",[true],0,0)],["bogus"]); (* apply a function to the environment *) fun envmod f = ENV:=f (!ENV); (* reference for temporarily posting new dependencies *) val NEWDEPS = ref ["bogus"]; (* dependency posting function *) fun postdeps() = (envmod(changedeps2 (union(!NEWDEPS))) ;NEWDEPS:=nil); fun dropdeps() = NEWDEPS:=nil; (* term viewing functions *) (* these are actually identity functions with side effects *) val PROMPT = ref true; fun termprompts() = PROMPT := not (!PROMPT); fun showterm prompt t = (if (!VERBOSITY) = 2 then (output(std_out, (if (!PROMPT) then ("\n"^prompt^":") else "") ^"\n\n"^(display t)^(!Returns)); flush_Out(std_out)) else ();t); fun exec f = envmod (changerightside2 (applyat f (position(!ENV)))); (* USER COMMAND *) (* look at current subterm *) fun lookhere() = exec (showterm "Local term display"); (* variables controlling the look display *) val LOCAL_DISPLAY = ref true; val GLOBAL_DISPLAY = ref true; (* USER COMMAND *) (* look at current subterm and at top of right side of equation *) (* insert a "parenthesis" temporarily to highlight current subterm *) fun look() = (exec Parenthesis; envmod(changerightside2 (if (!GLOBAL_DISPLAY) then (showterm "Global term display") else (fn x => x))); exec deparenthesize1; lookhere()); (* USER COMMANDS (3) *) (* control the look display *) fun localdisplayoff() = (LOCAL_DISPLAY:=false;GLOBAL_DISPLAY:=true;look()); fun globaldisplayoff()= (LOCAL_DISPLAY:=true;GLOBAL_DISPLAY:=false;look()); fun bothdisplays()= (LOCAL_DISPLAY:=true;GLOBAL_DISPLAY:=true;look()); (* USER COMMAND *) (* look at the left side of the equation under construction *) fun lookback() = envmod(changeleftside2 (showterm "Initial term display")); (* term starting functions appear below after the environment saving commands, which have to appear after the declaration of the theorem list *) val SWAPTERM = ref (Constant ""); (* USER COMMAND *) (* interchange the left and right sides of the equation under construction *) fun workback() = (SWAPTERM:=leftside(!ENV); envmod(changeleftside (rightside(!ENV))); envmod(changerightside (!SWAPTERM)); envmod(changeposition nil); envmod(changeelevel 0); envmod(changeehlevel 0); envmod(changehypslist nil);look()); (* functions acting on positions that implement the term navigation commands *) fun preup nil = (errormessage "At top already!";nil) | preup L = rev(tl(rev L)); fun preright L = rev (true::(rev L)); fun preleft L = rev (false::(rev L)); (* we also need functions acting on levels, hlevels, and hypothesis lists which support the movement commands *) (* when one moves into or out of a function term, one needs to adjust the level (the number of nested brackets enclosing one); when moving into or out of case expressions, one needs to adjust the hlevel (the number of relevant hypotheses of case expressions) and the list of relevant hypotheses with their senses (positive, negative, or (at the virtual subexpression) inactive) *) val CURRENTTERM = ref(Constant ""); fun makecurrent t = (CURRENTTERM:=t;t); fun getcurrent() = exec (makecurrent); fun levelchange (Function f) n = n+1 | levelchange t n = n; fun uplevelchange (Function f) n = n-1 | uplevelchange t n = n; fun hlevelchange (CaseExp(u,v,w)) n = n+1 | hlevelchange t n = n; fun uphlevelchange (CaseExp(u,v,w)) n = n-1 | uphlevelchange t n = n; (* builds equation from hypothesis of a case expression and records current position *) (* true=?y is indistinguishable from ?y *) fun equationfromterm (Infix(x,ResOp"=",y)) = (x,y,position(!ENV),0,level(!ENV)) | equationfromterm t = (Constant "true",t,position(!ENV),0,level(!ENV)); fun hypslistchange (CaseExp(u,v,w)) L = rev((equationfromterm u)::(rev L)) | hypslistchange t L = L; fun listindex n nil = nil | listindex 1 (a::L) = [a] | listindex n (a::L) = listindex (n-1) L; fun presethypslistsense (x,y,p,n,l) = let val A = listindex ((length p)+2) (position(!ENV)) in if A = nil then (x,y,p,0,l) else if A = [false] then (x,y,p,1,l) else if A = [true] then (x,y,p,2,l) else (x,y,p,0,l) end; fun sethypslistsense L = if L = nil then nil else rev((presethypslistsense(hd (rev L)))::(tl (rev L))); (* this now coerces level as well, fixing the June 10 bug *) fun coercehypslistsense n lv (x,y,p,m,l) = (x,y,p,n,lv); fun uphypslistchange (CaseExp(u,v,w)) L = if L = nil then nil else rev(tl (rev L)) | uphypslistchange t L = L; (* the basic movement commands *) (* they have "silent" variants used by the fancy movement commands below *) (* USER COMMAND *) fun up() = if position(!ENV) = nil then errormessage "At top already!" else if hd (rev (position (!ENV))) = true then (* coming up from right *) (envmod (changeposition2 preup); getcurrent(); envmod (changelevel2 (uplevelchange (!CURRENTTERM))); envmod (changehlevel2 (uphlevelchange (!CURRENTTERM))); envmod (changehypslist2 (uphypslistchange(!CURRENTTERM))); envmod (changehypslist2 (sethypslistsense)); look()) else (* coming up from left *) (envmod (changeposition2 preup); getcurrent(); envmod (changelevel2 (uplevelchange (!CURRENTTERM))); envmod (changehypslist2 (sethypslistsense)); look()); fun sup() = if position(!ENV) = nil then errormessage "At top already!" else if hd (rev (position (!ENV))) = true then (* coming up from right *) (envmod (changeposition2 preup); getcurrent(); envmod (changelevel2 (uplevelchange (!CURRENTTERM))); envmod (changehlevel2 (uphlevelchange (!CURRENTTERM))); envmod (changehypslist2 (uphypslistchange(!CURRENTTERM))); envmod (changehypslist2 (sethypslistsense))) else (* coming up from left *) (envmod (changeposition2 preup); getcurrent(); envmod (changelevel2 (uplevelchange (!CURRENTTERM))); envmod (changehypslist2 (sethypslistsense)) ); (* USER COMMAND *) fun left() = (getcurrent(); envmod (changelevel2 (levelchange (!CURRENTTERM))); envmod (changeposition2 preleft); envmod (changehypslist2 (sethypslistsense)); look()); fun sleft() = (getcurrent(); envmod (changelevel2 (levelchange (!CURRENTTERM))); envmod (changeposition2 preleft); envmod (changehypslist2 (sethypslistsense)) ); (* USER COMMAND *) fun right() = (getcurrent(); envmod (changelevel2 (levelchange (!CURRENTTERM))); envmod (changehlevel2 (hlevelchange (!CURRENTTERM))); envmod (changehypslist2 (hypslistchange (!CURRENTTERM))); envmod (changeposition2 preright); envmod (changehypslist2 (sethypslistsense)); look()); fun sright() = (getcurrent(); envmod (changelevel2 (levelchange (!CURRENTTERM))); envmod (changehlevel2 (hlevelchange (!CURRENTTERM))); envmod (changehypslist2 (hypslistchange (!CURRENTTERM))); envmod (changeposition2 preright); envmod (changehypslist2 (sethypslistsense)) ); (* USER COMMAND *) fun top() = (envmod (changeelevel 0); envmod (changeehlevel 0); envmod(changehypslist nil); envmod (changeposition nil); look()); (* ADD: downtoleft, downtoright,upto with literal text arguments *) (* theorem declaration list *) (* A theorem consists of the following components: a name (which appears as a key in the theorems list rather than part of the structure) a format (used to supply parameters) (a term) left side of equation (a term) right side of equation (a term) a dependency list (the new definition and theorem-text dependency schemes will be supported by separate lists) Note the similarity to a proof environment; eliminating the components of a proof environment which support navigation yields a theorem. *) val THEOREMS = ref ([("bogus",(Constant "",Constant "",Constant "",["bogus"]))]); (* theorems declared but to be proved later -- i.e., recursive tactics *) val PRETHEOREMS = ref ["bogus"]; (* BEGIN block for cmatch (* infixes with commutative laws *) val COMMUTATIVE = ref [("bogus","bogus")]; (* function to recognize commutative laws *) (* used to modify addtheorem so that it maintains a registry of commutative laws *) fun iscommutative0 (Infix(x,ResOp s,y)) (Infix(z,ResOp t,w)) = s=t andalso x = w andalso y=z andalso x <> y | iscommutative0 (Infix(x,ConOp s,y)) (Infix(z,ConOp t,w)) = s=t andalso x = w andalso y=z andalso x <> y | iscommutative0 a b = false; fun infixof (Infix(x,i,y)) = opdisplay i; END block for cmatch *) (* commands for manipulating theorems list and individual theorems *) fun addtheorem name fo ls rs dps = (THEOREMS:= strongadd name (fo,ls,rs,dps) (!THEOREMS); PRETHEOREMS := dropfromset name (!PRETHEOREMS)); fun droptheorem name = THEOREMS:= drop name (!THEOREMS); (* BEGIN versions of addtheorem and droptheorem for cmatch fun addtheorem name fo ls rs dps = (THEOREMS:= strongadd name (fo,ls,rs,dps) (!THEOREMS); PRETHEOREMS := dropfromset name (!PRETHEOREMS); if (fo = Constant name) andalso (iscommutative0 ls rs) then COMMUTATIVE := addto (infixof ls) name (!COMMUTATIVE) else ()); fun droptheorem name = (THEOREMS:= drop name (!THEOREMS); COMMUTATIVE:=map (fn(x,y)=>(y,x)) (drop name (map (fn(x,y)=>(y,x)) (!COMMUTATIVE)))); END versions of addtheorem and droptheorem for cmatch *) val dummythm = (Constant "", Constant "", Constant "", []); fun PreFormatof (a,b,c,d) = a; fun PreLeftside (a,b,c,d) = b; fun PreRightside (a,b,c,d) = c; fun PreDeps (a,b,c,d) = d; fun Thm name = safefind dummythm name (!THEOREMS); fun Formatof name = PreFormatof (safefind dummythm name (!THEOREMS)); fun Leftside name = PreLeftside (safefind dummythm name (!THEOREMS)); fun Rightside name = PreRightside (safefind dummythm name (!THEOREMS)); fun Deps name = PreDeps (safefind dummythm name (!THEOREMS)); (* string lists will be converted to terms when needed for theorem deps *) fun listtoterm nil = Numeral [0] | listtoterm (s::L) = Infix(if stringtocon s = Constant s then Constant s else Infix(FreeVar "?x",ConOp s,FreeVar "?y") ,ResOp ",",listtoterm L); fun listtoterm2 L = baredisplay(listtoterm L); fun termtolist (Numeral [0]) = nil | termtolist (Infix(Constant s,ResOp",",y)) = (s::(termtolist y)) | termtolist (Infix(Infix(x,ConOp s,y),ResOp",",z)) = (s::(termtolist z)) | termtolist x = nil; fun termtolist2 s = termtolist (parse s); (* possibly optimized versions -- not used *) fun Thm2 name = Safefind dummythm name (THEOREMS); fun Formatof2 name = PreFormatof (Safefind dummythm name (THEOREMS)); fun Leftside2 name = PreLeftside (Safefind dummythm name (THEOREMS)); fun Rightside2 name = PreRightside (Safefind dummythm name (THEOREMS)); fun Deps2 name = PreDeps (Safefind dummythm name (THEOREMS)); (* either version of isatheorem is true only of "theorems" actually found on the theorem list; built-in tactics are treated separately *) fun isatheorem name = foundin name (!THEOREMS); (* this version of isatheorem is used inside thmresult only as a possible optimization *) fun Isatheorem name = Foundin name (THEOREMS); fun isapretheorem name = foundinset name (!PRETHEOREMS); (* this version of isstratified posts dependencies to the environment *) fun Isstratified1 level t = (SCINSCOUT := nil; let val A = isstratified level t in ((if A then (envmod (changedeps2 (union (union2(map Deps (!SCINSCOUT)))))) else ());SCINSCOUT:=nil;A) end); fun Isstratified t = Isstratified1 0 t; (* built-in tactics *) fun isbuiltinthm name = foundinset name ["EVAL","BIND","UNEVAL","FLIP", "INPUT","OUTPUT","STOPINPUT","SHELL", "|-|","=", "=>>", "<<=","*>","<*","!@","!$"]; (* other aspects of theorems are not usually changed, but dependencies are more often modified *) fun changedeps name f = if isatheorem name then let val A = hd (find name (!THEOREMS)) in (droptheorem name; addtheorem name (PreFormatof A) (PreLeftside A) (PreRightside A) (f (PreDeps A))) end else (); (* theorem display command *) val STATEMENTDISPLAY = ref false; (* USER COMMAND *) (* toggle which turns on and off special statement display *) fun statementdisplay() = (STATEMENTDISPLAY := not (!STATEMENTDISPLAY); errormessage ("Statement display is "^(if (!STATEMENTDISPLAY) then "on" else "off"))); fun eqdisplay fo ls rs dps = if (!STATEMENTDISPLAY) andalso rs = Constant "true" then output(std_out,(!Returns)^(display fo)^":"^(!Returns)^ "|-"^(display ls)^(!Returns)^ (if (!Returns) = "\n" then (dashes())^(!Returns) else "")^ (display (listtoterm dps))^(!Returns)) else if (!STATEMENTDISPLAY) andalso ls = Constant "true" then output(std_out,(!Returns)^(display fo)^":"^(!Returns)^ "$|-"^(display rs)^(!Returns)^ (if (!Returns) = "\n" then (dashes())^(!Returns) else "")^ (display (listtoterm dps))^(!Returns)) else output(std_out,(!Returns)^(display fo)^": "^(!Returns)^ (display ls)^" ="^(!Returns)^(display rs)^(!Returns)^ (if (!Returns) = "\n" then (dashes())^(!Returns) else "")^ (display (listtoterm dps))^(!Returns)); (* USER COMMAND *) (* display a theorem *) fun thmdisplay name = if isatheorem name then if (!VERBOSITY) > 0 then let val (fo,ls,rs,dps) = Thm name in (eqdisplay fo ls rs dps;flush_Out(std_out)) end else () else if isbuiltinthm name then errormessage (name^" is a built in tactic") else errormessage ("Theorem "^name^" not found"); (* USER COMMAND *) (* look at dependencies of current environment *) fun seedeps() = output(std_out,display(listtoterm(deps(!ENV)))^(!Returns)); (* command for displaying selected theorems; hit enter to go to the next theorem or q to stop. The order in which theorems are displayed is pretty random, and more so with the "optimization" *) (* names beginning with "}" (which cannot appear in a theorem name or any term) are keys of saved environments; see saveenv below *) fun showsometheorems filter nil = () | showsometheorems filter ((na,x)::L) = if filter na andalso hd(explode na) <> "}" then (thmdisplay na; (* flush_Out(std_out); *) if input(std_in,1) = "q" then () else showsometheorems filter L) else showsometheorems filter L; fun showalltheorems() = showsometheorems (fn x => true) (sortfun(!THEOREMS)); (* shows axioms and definitions *) fun showaxioms() = showsometheorems (fn x => foundinset x (Deps x)) (sortfun(!THEOREMS)); (* definition facility *) (* definitions require a second stratification function, whose object is to type free variables so that implicitly defined functions behave correctly *) (* list of all free variables (including infix variables) in a given term *) (* it is possible that some glitches will arise from including infix variables *) fun freevarlist (FreeVar s) = [s] | freevarlist (Infix(u,VarOp s,v)) = addtoset s (union (freevarlist u) (freevarlist v)) | freevarlist (Infix(u,i,v)) = union (freevarlist u) (freevarlist v) | freevarlist (Function t) = freevarlist t | freevarlist (CaseExp(u,v,w)) = union (freevarlist u) (union (freevarlist v)(freevarlist w)) | freevarlist t = nil; (* variant which does not include infix variables, introduced to support autoformat built-in tactics *) fun freevarlist2 (FreeVar s) = [s] | freevarlist2 (Infix(u,i,v)) = union (freevarlist2 u) (freevarlist2 v) | freevarlist2 (Function t) = freevarlist2 t | freevarlist2 (CaseExp(u,v,w)) = union (freevarlist2 u) (union (freevarlist2 v)(freevarlist2 w)) | freevarlist2 t = nil; fun strat2 localtype (Constant s) = [nil] | strat2 localtype (FreeVar s) = [[(s,localtype)]] | strat2 localtype (Numeral s) = [nil] | strat2 localtype (BoundVar s) = [nil] | strat2 localtype (Function s) = (strat2 (localtype-1) s) | strat2 localtype (CaseExp(t,u,v)) = mergetypes((checkappend [nil] (strat2 localtype t))) (mergetypes(strat2 localtype u) (strat2 localtype v)) | strat2 localtype (Infix(t,ResOp":",u)) = mergetypes (strat2 (localtype+1) t) (checkappend [nil] (strat2 localtype u)) | strat2 localtype (Infix(Constant f,ResOp "@",t)) = crushtypes(checkappend (if isscout f orelse isscinright f then [nil] else []) (strat2 localtype t)) | strat2 localtype (Infix(t,ResOp "@!",u)) = nil | strat2 localtype (Infix(t,i,u)) = if istypedoperator (opdisplay i) then crushtypes(checkappend (if isscout (opdisplay i) then [nil] else []) (mergetypes (checkappend(if isscinleft (opdisplay i) then [nil] else []) (strat2 (lefttype(opdisplay i)+localtype) t)) (checkappend(if isscinright (opdisplay i) then [nil] else []) (strat2 (righttype(opdisplay i)+localtype) u)))) else (* case of opaque or undeclared variable operators *) if freevarlist (Infix(t,i,u)) = nil andalso strat2 0 t <> nil andalso strat2 0 u <> nil then [nil] else nil; fun isstrat2 t = strat2 0 t <> nil; (* functions used to define format for left sides of definitions *) (* other functions, used to define format for parameter lists of tactics, are also given here *) fun iterconvar (FreeVar s) = true | iterconvar (Function t) = iterconvar t | iterconvar t = false; fun pairsovervars (Infix(u,ResOp ",",v)) = (pairsovervars u) andalso (pairsovervars v) | pairsovervars t = iterconvar t; fun atomdefinitionformat (Constant s) = s<>"" | atomdefinitionformat (Infix(u,ResOp"@",v)) = (atomdefinitionformat u) andalso (pairsovervars v) | atomdefinitionformat t = false; fun opdefinitionformat (Infix(x,ConOp s,y)) = s<>"" andalso ( (x = (stringtocon (prefixof s)) orelse (pairsovervars x)) andalso (pairsovervars y)) | opdefinitionformat (Infix(u,ResOp"@",v)) = (opdefinitionformat u) andalso (pairsovervars v) | opdefinitionformat t = false; fun opaqueopdefinitionformat (Infix(x,ConOp s,y)) = s<>"" andalso ( (x = (stringtocon (prefixof s)) orelse (pairsovervars x)) andalso (pairsovervars y)) | opaqueopdefinitionformat t = false; fun atomhead (Constant s) = s | atomhead (Infix(x,ResOp"@",y)) = atomhead x | atomhead t = ""; fun ophead (Infix(u,ResOp"@",v)) = ophead u | ophead (Infix(x,ConOp s,y)) = s | ophead (Infix(x,ResOp s,y)) = s | ophead t = ""; fun eitherhead x = if atomhead x = "" then ophead x else atomhead x; (* formats used by parameterized tactics *) fun weakpairsovervars (Infix(u,ResOp ",",v)) = (weakpairsovervars u) andalso (weakpairsovervars v) | weakpairsovervars (Infix(u,VarOp s,v)) = if isstrictprefix s then u = Constant "" andalso (weakpairsovervars v) else (weakpairsovervars u) andalso (weakpairsovervars v) | weakpairsovervars t = iterconvar t; fun weakatomdefinitionformat (Constant s) = s<>"" | weakatomdefinitionformat (Infix(u,ResOp"@",v)) = (weakatomdefinitionformat u) andalso (weakpairsovervars v) | weakatomdefinitionformat t = false; fun weakopdefinitionformat (Infix(u,ResOp"@",v)) = (weakopdefinitionformat u) andalso (weakpairsovervars v) | weakopdefinitionformat (Infix(x,i,y)) = (((opdisplay i) <>"" andalso ( (x = (stringtocon (prefixof (opdisplay i)))))) orelse (weakpairsovervars x)) andalso (weakpairsovervars y) | weakopdefinitionformat t = false; (* a variation on the "head" functions allowing variables and reserved operators where appropriate *) (* also used for parameterized tactics rather than general functions *) fun varatomhead (Constant s) = s | varatomhead (FreeVar s) = s | varatomhead (Infix(x,ResOp"@",y)) = varatomhead x | varatomhead t = ""; fun varophead (Infix(x,ConOp s,y)) = s | varophead (Infix(x,ResOp s,y)) = if s = "@" then varophead x else s | varophead (Infix(x,VarOp s,y)) = s | varophead t = ""; fun eithervarhead t = if varatomhead t = "" then varophead t else varatomhead t; (* the list of defined constants and operators with defining theorems *) val DEFINITIONS = ref [("bogus","bogus")]; (* the converse of the definition list *) val DEFINITIONS2 = ref [("bogus","bogus")]; (* DEFINITIONS:=nil; DEFINITIONS2:= nil; *) fun adddef name named = (DEFINITIONS:=addto name named (!DEFINITIONS); DEFINITIONS2:= addto named name (!DEFINITIONS2)); fun isdefinition name = foundin name (!DEFINITIONS); fun isdefined name = foundin name (!DEFINITIONS2); fun definitionof named = safefind "" named (!DEFINITIONS2); (* scin/scout functions *) (* is the theorem s = t of the correct form to verify that an operator or function is scout? *) fun scoutform S (Infix(Constant s,ResOp"@",FreeVar x)) (Infix(t,ResOp":",(Infix(Constant s2,ResOp"@",FreeVar x2)))) = if S <> s orelse s<>s2 orelse x<>x2 then false else let val A = strat2 0 t in if A = nil then false else (A = [nil]) end | scoutform S (Infix(t,ResOp":",(Infix(Constant s,ResOp"@",FreeVar x)))) (Infix(Constant s2,ResOp"@",FreeVar x2)) = if S <> s orelse s<>s2 orelse x<>x2 then false else let val A = strat2 0 t in if A = nil then false else (A = [nil]) end | scoutform S (Infix(FreeVar s,i,FreeVar t)) (Infix(T,ResOp":",(Infix(FreeVar s2,i2,FreeVar t2)))) = if S <> (opdisplay i) orelse s <> s2 orelse t <> t2 orelse i<>i2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scoutform S (Infix(T,ResOp":",(Infix(FreeVar s,i,FreeVar t)))) (Infix(FreeVar s2,i2,FreeVar t2)) = if S <> (opdisplay i) orelse s <> s2 orelse t <> t2 orelse i <> i2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scoutform S (Infix(Constant "",i,FreeVar t)) (Infix(T,ResOp":",(Infix(Constant "",i2,FreeVar t2)))) = if S <> (opdisplay i) orelse t <> t2 orelse i<>i2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scoutform S (Infix(T,ResOp":",(Infix(Constant "",i,FreeVar t)))) (Infix(Constant "",i2,FreeVar t2)) = if S <> (opdisplay i) orelse t <> t2 orelse i <> i2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scoutform S t u = false; (* make an operator scout if given a theorem of the appropriate form *) fun makescout s thm = if isscout s then errormessage (s^" is already scout") else if scoutform s (Leftside thm) (Rightside thm) then (SCOUT:=addto s thm (!SCOUT)) else errormessage ("Scout declaration of "^s^" using "^thm^" failed"); (* is a theorem of the correct form to declare an operator "scin" (both left and right)? *) fun scinform S (Infix(Constant s,ResOp"@",t)) (Infix(Constant s2,ResOp"@",Infix(T,ResOp":",t2))) = if S <> s orelse s <> s2 orelse t <> t2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scinform S (Infix(Constant s,ResOp"@",Infix(T,ResOp":",t))) (Infix(Constant s2,ResOp"@",t2)) = if S <> s orelse s <> s2 orelse t <> t2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scinform S (Infix(FreeVar x,i,FreeVar y)) (Infix(Infix(T,ResOp":",FreeVar x2),i2, Infix(U,ResOp":",FreeVar y2))) = if S <> (opdisplay i) orelse x <> x2 orelse y <> y2 then false else let val A = strat2 0 T and B = strat2 0 U in if A = nil orelse B = nil then false else (A = [nil]) andalso (B = [nil]) end | scinform S (Infix(Infix(T,ResOp":",FreeVar x),i, Infix(U,ResOp":",FreeVar y))) (Infix(FreeVar x2,i2,FreeVar y2)) = if S <> (opdisplay i) orelse x <> x2 orelse y <> y2 orelse i <> i2 then false else let val A = strat2 0 T and B = strat2 0 U in if A = nil orelse B = nil then false else (A = [nil]) andalso (B = [nil]) end | scinform S (Infix(Constant "",i,FreeVar y)) (Infix(Constant "",i2, Infix(U,ResOp":",FreeVar y2))) = if S <> (opdisplay i) orelse y <> y2 orelse i <> i2 then false else let val B = strat2 0 U in if B = nil then false else (B = [nil]) end | scinform S (Infix(Constant "",i, Infix(U,ResOp":",FreeVar y))) (Infix(Constant "",i2,FreeVar y2)) = if S <> (opdisplay i) orelse y <> y2 orelse i <> i2 then false else let val B = strat2 0 U in if B = nil then false else (B = [nil]) end | scinform s t u = false; fun scinleftform S (Infix(FreeVar x,i,FreeVar y)) (Infix(Infix(T,ResOp":",FreeVar x2),i2, FreeVar y2)) = if S <> (opdisplay i) orelse x <> x2 orelse y <> y2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scinleftform S (Infix(Infix(T,ResOp":",FreeVar x),i, FreeVar y)) (Infix(FreeVar x2,i2,FreeVar y2)) = if S <> (opdisplay i) orelse x <> x2 orelse y <> y2 orelse i <> i2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scinleftform s t u = false; fun scinrightform S (Infix(FreeVar x,i,FreeVar y)) (Infix(FreeVar x2,i2, Infix(T,ResOp":",FreeVar y2))) = if S <> (opdisplay i) orelse x <> x2 orelse y <> y2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scinrightform S (Infix(FreeVar x,i, Infix(T,ResOp":",FreeVar y))) (Infix(FreeVar x2,i2,FreeVar y2)) = if S <> (opdisplay i) orelse x <> x2 orelse y <> y2 orelse i <> i2 then false else let val A = strat2 0 T in if A = nil then false else (A = [nil]) end | scinrightform s t u = false; (* USER COMMANDS (3) *) (* make an operator scin(left/right) if an appropriate witness theorem is given *) fun makescin s thm = if isscinleft s andalso isscinright s then errormessage (s^" is already scin") else if scinform s (Leftside thm) (Rightside thm) then (SCINLEFT:= addto s thm (!SCINLEFT); SCINRIGHT:= addto s thm (!SCINRIGHT)) else errormessage ("Scin declaration of "^s^" using "^thm^" failed"); fun makescinvar s = if s = "" orelse stringtoop s <> VarOp s orelse istypedoperator s orelse isopaque s then errormessage(s^" cannot be made a scin infix variable") else (declareinfix s;SCINLEFT:= addto s "" (!SCINLEFT); SCINRIGHT:= addto s "" (!SCINRIGHT)); fun makescinleft s thm = if isscinleft s then errormessage (s^" is already scinleft") else if scinleftform s (Leftside thm) (Rightside thm) then (SCINLEFT:= addto s thm (!SCINLEFT)) else errormessage ("Scinleft declaration of "^s^" using " ^thm^" failed"); fun makescinright s thm = if isscinright s then errormessage (s^" is already scinright") else if scinrightform s (Leftside thm) (Rightside thm) then (SCINRIGHT:= addto s thm (!SCINRIGHT)) else errormessage ("Scinright declaration of "^s^" using " ^thm^" failed"); (* is the equation of the second and third arguments a theorem to the effect that Constant S is a retraction? Used by typedefinition below. *) (* prove command and variations -- note that the prove command needs to know about definition format! *) (* the use of weak definition formats effectively allows operator variable parameters to parameterized tactics *) (* definition dependencies of a term can be read from the term (no need to maintain in environment); if a defined term does not appear in a theorem, then the proof of the theorem could in principle have been carried out without reference to the definition at all This indicates that definitions can go back to null axiom dependencies if a separate definition dependency scheme is maintained; master definition dependency list needs references to all constants, not just to theorems, so is naturally not part of the theorems list. The master theorem-text dependency list will also be separate, though it could more naturally be part of the theorem list *) (* management of theorem text and definition dependencies of theorems, which will support reaxiomatization, redefinition, and theorem export facilities *) val DEFDEPS = ref [("bogus",["bogus"])]; val DEFDEPS2 = ref [("bogus",["bogus"])]; (* inverse list *) fun defdeps s = safefind nil s (!DEFDEPS); fun defdeps2 s = safefind nil s (!DEFDEPS2); (* now should update inverse list correctly *) fun adddefdep s L = ( map(fn x=>let val A = find x (!DEFDEPS2) in DEFDEPS2:=strongadd x (if A = nil then nil else (dropfromset s (hd A)))(!DEFDEPS2)end) (defdeps s); DEFDEPS:= strongadd s L (!DEFDEPS); map(fn x => DEFDEPS2:= strongadd x (let val A = find x (!DEFDEPS2) in if A = nil then [s] else addtoset s (hd A) end) (!DEFDEPS2)) L;()); (* lists defined constants and operators not appearing in embedded theorems *) (* also picks up dependencies of defined terms from (!DEFDEPS) *) (* the thm parameter is a technicality for blocking references to the defining theorem (which is then the same as the defined object) within the definition *) fun conlist2 thm (Constant "") = nil | conlist2 thm (Constant s) = if isdefined s then if definitionof s = thm then [thm] else addtoset (definitionof s) (defdeps (definitionof s)) else nil | conlist2 thm (Function t) = conlist2 thm t | conlist2 thm (CaseExp(u,v,w)) = union (conlist2 thm u) (union(conlist2 thm v)(conlist2 thm w)) | conlist2 thm (Infix(x,ResOp "=>",y)) = conlist2 thm y | conlist2 thm (Infix(x,ResOp "<=",y)) = conlist2 thm y | conlist2 thm (Infix(x,i,y)) = union (if isdefined (opdisplay i) then if definitionof(opdisplay i) = thm then [thm] else addtoset (definitionof (opdisplay i)) (defdeps (definitionof (opdisplay i))) else nil) (union (conlist2 thm x) (conlist2 thm y)) | conlist2 thm t = nil; fun makedefdeps thm = if isatheorem thm then let val (fo,rt,lt,dps) = Thm thm in ( adddefdep thm (union(conlist2 thm lt)(conlist2 thm rt)); map (fn (x) => if x <> thm then makedefdeps x else ()) (defdeps2 thm);()) end else errormessage (thm^" is not a theorem"); (* list of all constants (including infixes) on which a term depends, used by theorem text deps functions *) fun conlist (Constant "") = nil | conlist (Constant s) = [s] | conlist (Infix(x,ConOp s,y)) = addtoset s (union (conlist x) (conlist y)) | conlist (Infix(x,ResOp s,y)) = addtoset s (union (conlist x) (conlist y)) | conlist (Infix(x,VarOp s,y)) = (union (conlist x) (conlist y)) | conlist (Function s) = conlist s | conlist (CaseExp(u,v,w)) = union (conlist u) (union (conlist v) (conlist w)) | conlist t = nil; val THMTEXTDEPS = ref [("bogus",["bogus"])]; val THMTEXTDEPS2 = ref [("bogus",["bogus"])]; fun thmtextdeps s = safefind nil s (!THMTEXTDEPS); fun thmtextdeps2 s = safefind nil s (!THMTEXTDEPS2); (* now should update inverse list correctly *) fun addthmtextdep s L = ( map(fn x=>let val A = find x (!THMTEXTDEPS2) in THMTEXTDEPS2:=strongadd x (if A = nil then nil else (dropfromset s (hd A)))(!THMTEXTDEPS2)end) (thmtextdeps s); THMTEXTDEPS:= strongadd s L (!THMTEXTDEPS); map(fn x => THMTEXTDEPS2:= strongadd x (let val A = find x (!THMTEXTDEPS2) in if A = nil then [s] else addtoset s (hd A) end) (!THMTEXTDEPS2)) L;()); fun isatheorem2 s = isatheorem s orelse isapretheorem s; (* determine the text dependencies of a term, L being a list of known recursive dependencies *) (* make this dynamic; it updates the text dependencies as it goes and it short circuits the recursive process where it knows the work has already been done *) val DONELIST = ref ["bogus"]; (* list of theorems whose text dependencies have already been updated *) fun conlist4 L (Constant "") = nil | conlist4 L (Constant s) = if (not (foundinset s L)) andalso foundinset s (!DONELIST) then thmtextdeps s (* short circuit! *) else if isatheorem s then if foundinset s L then thmtextdeps s else ( let val LL = addtoset s (union (conlist4 (addtoset s L) (Leftside s))(conlist4 (addtoset s L) (Rightside s))) in (DONELIST:=addtoset s (!DONELIST); addthmtextdep s (LL);LL) end) else if isdefined s then if foundinset (definitionof s) L then thmtextdeps (definitionof s) else (conlist4 L (Constant (definitionof s))) else if isapretheorem s then [s] else nil | conlist4 L (Function t) = conlist4 L t | conlist4 L (CaseExp(u,v,w)) = union (conlist4 L u) (union(conlist4 L v)(conlist4 L w)) | conlist4 L (Infix(x,i,y)) = union (conlist4 L x) (union (conlist4 L y) (conlist4 L (Constant (opdisplay i)))) | conlist4 L t = nil; fun makethmtextdeps1 thm = if isatheorem thm then let val LIST = (conlist4 nil (Constant thm)) in ( addthmtextdep thm LIST; map (fn x => if (foundinset x (!DONELIST)) then if foundinset thm (thmtextdeps x) then addthmtextdep x LIST else () else makethmtextdeps1 x) (thmtextdeps2 thm);()) end else errormessage (thm^" is not a theorem"); fun makethmtextdeps thm = (DONELIST:=nil;makethmtextdeps1 thm; DONELIST:=nil); (* modification to note that definition deps of an axiom cannot be removed from a theorem using the axiom *) fun fixdeps thm = (makethmtextdeps thm;makedefdeps thm; if isatheorem thm then let val (fo,lt,rt,dps) = Thm thm in addtheorem thm fo lt rt (sortset((setminus dps (setminus (separate isdefinition dps) (union(defdeps thm)(union2(map defdeps (separate (fn x => not(isdefinition x)) dps)))))))) end else ()); (* USER COMMAND *) (* see all dependencies of a theorem *) fun showalldeps thm = if isatheorem thm then output(std_out,(!Returns)^"axiomatic:"^(!Returns) ^(display(listtoterm (sortset(Deps thm)))) ^(!Returns)^"definition:"^(!Returns) ^(display(listtoterm (sortset(defdeps thm))))^(!Returns)^ "theorem text:"^(!Returns) ^(display(listtoterm(sortset(thmtextdeps thm))))^(!Returns)) else if isbuiltinthm thm then errormessage (thm^" is a built-in tactic") else errormessage (thm^" is not a theorem"); (* USER COMMAND *) (* see what theorems use a given theorem (in the theorem text sense) *) fun whatuses thm = if isatheorem thm then output(std_out, (!Returns)^(display(listtoterm(sortset(thmtextdeps2 thm))))^(!Returns)) else if isbuiltinthm thm then errormessage (thm^" is a built-in tactic") else errormessage (thm^" is not a theorem"); (* left sides of theorems may not have execution behaviour *) (* the overloading of existing non-theorem constants as theorems (except by definitions) has been prevented -- it can be forced by hand by using pretheorems (as it could be in the existing version) *) (* commands for creating theorems *) (* left sides of theorems may not have execution behaviour *) (* USER COMMAND *) (* command for declaring recursive tactics prior to their actual proof *) fun declarepretheorem name = if isaconstant name orelse isoperator name then errormessage (name^" is already declared") else if name <> "" andalso stringtocon name = Constant name then (declareconstant name; PRETHEOREMS:=addtoset name (!PRETHEOREMS); addthmtextdep name [name]) else if name <> "" andalso stringtoop name = ConOp name then (declareinfix name; PRETHEOREMS:=addtoset name (!PRETHEOREMS); addthmtextdep name [name]) else errormessage (name^" is ill-formed"); (* USER COMMAND *) (* a technicality, but someone might want it *) fun declareunarypretheorem name = if name <> "" andalso stringtoop name = ConOp name then (declarepretheorem name;declarestrictprefix name) else errormessage ("Inappropriate argument "^name^" for unary pretheorem declaration"); (* should axioms have scin/scout induced deps? *) (* axioms must be rule-free on both sides, or thm text deps must be more complicated *) (* it appears at this point that axioms and definitions can safely be solely dependent on themselves: any application of an axiom or definition introduces its scin/scout deps. Definition dependencies of axioms will not be dropped by fixdeps. In general, axioms and definitions are treated specially by the prover in ways which are likely to avoid problems: they cannot be reproven or forgotten *) (* USER COMMAND *) fun axiom na ls rs = if stringtocon na = Constant na andalso not(isaconstant na) then let val LS = parse ls and RS = parse rs in if declarecheck false 0 LS andalso declarecheck false 0 RS andalso isstratified 0 LS andalso isstratified 0 RS andalso rulefree LS andalso rulefree RS then (addtheorem na (Constant na) LS RS [na]; fixdeps na; declareconstant na;thmdisplay na) else (errormessage ("Declaration or stratification error in proposed theorem "^na)) end else errormessage ("Name of proposed theorem "^na^" is ill-formed or already declared"); (* USER COMMAND *) (* axioms asserting truth of propositions *) fun statement na ls = axiom na ls "true"; (* the definition commands require that the object being defined be undeclared as yet, that no new variables or undeclared constants or operators appear on the right side of the definition, and that the whole definition be stratified *) (* should definitions have scin/scout induced deps? *) (* since thmtextdeps functions follow trail of definitions, it seems safe to allow execution behavior on right side of a definition *) (* in this case it might seem natural to allow definition theorems to be pretheorems to allow definitions with recursive execution behavior -- not implemented *) (* USER COMMAND *) fun defineconstant ls rs = let val LS = parse ls and RS = parse rs in if atomdefinitionformat LS andalso not(isaconstant(atomhead LS)) andalso declarecheck false 0 RS andalso isstratified 0 RS andalso subset (freevarlist RS) (freevarlist LS) andalso isstrat2 (Infix(LS,ResOp"=",RS)) then (declareconstant (atomhead LS); addtheorem (atomhead LS) (Constant(atomhead LS)) LS RS [atomhead LS]; adddef (atomhead LS) (atomhead LS); fixdeps (atomhead LS); thmdisplay (atomhead LS)) else errormessage ("Format, declaration or stratification failure of proposed definition of "^ls) end; (* this version now supports automatic declaration of unary operators (as strict prefixes); the command will accept a left side in unary format *) (* USER COMMAND *) fun definetypedinfix name m n ls rs = let val LS = parse ls and RS = parse rs in if opdefinitionformat LS andalso not(isoperator(ophead LS)) andalso not(isatheorem name orelse isapretheorem name orelse isbuiltinthm name) andalso declarecheck false 0 RS andalso isstratified 0 RS andalso subset (freevarlist RS) (freevarlist LS) then if (declaretypedinfix m n (ophead LS); if not(declarecheck true 0 LS) then declarestrictprefix (ophead LS) else (); isstrat2 (Infix(LS,ResOp"=",RS))) then (declareconstant name; addtheorem (name) (Constant(name)) LS RS [name]; adddef (name) (ophead LS); fixdeps (name); thmdisplay (