(* \begin{verbatim} *) (* EFTTP Mark 2 Source Code *) (* draft version of June 4, 1998 *) (* Copyright 1998 by M. Randall Holmes. May be reproduced and used freely as long as this copyright notice accompanies all distributions *) (* PRELIMINARIES MODULE *) (* Error message function for all types*) val ERRORPAUSE = ref false; fun setpause() = ERRORPAUSE := true; fun setnopause() = ERRORPAUSE := false; fun errormessage s = (output(std_out,"\n\nMARK2: "^s^"\n\n"); if (!ERRORPAUSE) then output(std_out,input(std_in,1)) else ()); (* USER COMMAND *) (* version command *) fun versiondate() = errormessage "June 4, 1998"; (* Counter for generating new string extensions *) val COUNTER = ref 0; (* USER COMMAND *) (* set counter to 0 *) (* useful in scripts! *) fun initializecounter () = COUNTER:=0; (* increment counter; it cycles below 1000, which may not always be desirable *) fun newcounter () = (COUNTER:=((!COUNTER)+1) mod 1000;makestring(!COUNTER)); (* lengths of lists and strings *) fun length nil = 0 | length L = 1 + (length(tl L)); fun stringlength s = length (explode s); (* functions for coding and decoding comment text *) fun precommentcode nil = nil | precommentcode ("\n"::rest) = ("\\"::"n"::(precommentcode rest)) | precommentcode ("\t"::rest) = ("\\"::"t"::(precommentcode rest)) | precommentcode ("\\"::rest) = ("\\"::"\\"::(precommentcode rest)) | precommentcode (x::rest) = x::(precommentcode rest); fun commentcode s = implode(precommentcode(explode s)); fun precommentdecode nil = nil | precommentdecode ("\\"::"\\"::x) = "\\"::(precommentdecode x) | precommentdecode ("\\"::"n"::x) = "\n"::(precommentdecode x) | precommentdecode ("\\"::"t"::x) = "\t"::(precommentdecode x) | precommentdecode (x::y) = x::(precommentdecode y); fun commentdecode s = implode(precommentdecode(explode s)); (* function for reading string input *) (* input line is terminated by a newline or tab (not by a space!) *) (* leading spaces are ignored, but not internal or trailing spaces *) val NEXTCHAR = ref "a"; val CHARSYET = ref false; fun prestringinput file = ( NEXTCHAR:=input(file,1); if (!NEXTCHAR) = "\n" orelse (!NEXTCHAR) = "\t" then "" else if (!NEXTCHAR) = " " then if (!CHARSYET) then " "^ (prestringinput file) else prestringinput file else (CHARSYET:=true;(!NEXTCHAR)^(prestringinput file))); fun stringinput file = (CHARSYET:=false;prestringinput file); (* MATH MODULE *) (* Integer type -- represented by int list *) (* the base of integer operations *) (* intended to be either less than 10 or a power of 10 *) (* changing base away from 10 renders the system unsound in various peculiar ways at present; this will be corrected in due course *) (* it is hoped that the system is now sound in single theories as long as the command clearbase is always used to set bases; setbase is not a user command and there is no provision for base conversions. This does mean that the theorem export mechanism is not sound unless bases are the same! *) (* unsigned integers are implemented *) val BASE = ref 10; (* changes of base while working with a theory are not safe *) (* but using base 10000 instead of base 10 seems to work nicely *) (* convert ML integers to digit lists (in reverse order) and vice versa *) (* last digit of ML integer n *) fun lastdigit n = n mod (!BASE); (* functions to convert between ML integers and lists of digits in reverse order used to represent infinite-precision integers *) fun restofdigits n = inttolist(n div (!BASE)) and inttolist 0 = nil | inttolist n = (lastdigit n)::(restofdigits n); fun listtoint nil = 0 | listtoint (head::tail) = head + (!BASE)*(listtoint tail); (* bring length of a numeral up to a certain length by padding with zeroes; used to handle the long digits of large bases *) fun padwithzeroesto n s = if stringlength s >= n then s else "0"^(padwithzeroesto (n-1) s); (* functions to manage the current length of a digit *) val BASETEMP = ref 10; val DIGITL = ref 1; (* length of a single "digit" in the current base *) (* in base 12, for example, a "digit" is a sequence of two base 10 digits *) fun setdigitlength() = (BASETEMP := (!BASE); BASE := 10; DIGITL := length(inttolist((!BASETEMP)-1)); BASE := (!BASETEMP)); (* setbase should not be used in a theory which already mentions numerals; there is no global correction of base information, so numerals already present will be read incorrectly; the installation of global base correction and saved base information is a desirable upgrade *) (* this function is not a user command; it is only to be invoked by the theory clearing function and in load files *) fun setbase n = (BASE:=n;setdigitlength()); fun paddigit d = padwithzeroesto (!DIGITL) d; (* crop removes leading zeroes (also ensures that 0 has one left!) *) fun precrop nil = ["0"] | precrop (" "::x) = precrop x | precrop ("0"::x) = precrop x | precrop x = x; fun crop s = implode(precrop(explode s)); (* cropnumeral converts digit lists to string identifiers *) fun numeral nil = "" | numeral ((head:int)::tail) = (numeral(tail))^ (paddigit(makestring head)); fun cropnumeral L = crop(numeral L); (* built in arithmetic operations *) fun addlistints nil L = L | addlistints L nil = L | addlistints (head1::L) (head2::M) = (lastdigit(head1 + head2)):: (addlistints (restofdigits (head1+head2)) (addlistints L M)); fun multiplyints nil L = nil | multiplyints L nil = nil | multiplyints (head1::tail1) (head2::tail2) = addlistints (inttolist (head1*head2)) (addlistints (0::((multiplyints [head1] tail2))) (addlistints (0::((multiplyints [head2] tail1))) (0::(0::(multiplyints tail1 tail2))))); fun lessints L nil = false | lessints nil L = true | lessints (head1::tail1) (head2::tail2) = (lessints tail1 tail2) orelse ((tail1 = tail2) andalso ((head1:int) < head2)); (* This is subtraction of unsigned integers; it returns zero *) (* when a negative answer would normally be expected *) fun subtractints L M = if lessints L M orelse L=M then nil else if M = nil then L else if hd L >= hd M then ((hd L - hd M):: (subtractints (tl L) (tl M))) else (((!BASE) + hd L - hd M)::(subtractints (tl L) (addlistints [1] (tl M)))); fun divideints L M = if lessints M [1] then (errormessage "Division by zero!";nil) else if lessints L M then nil else if lessints (tl L) M then addlistints [1] (divideints (subtractints L M) M) else addlistints (0::divideints (tl L) M) (divideints (addlistints (0:: (remainder (tl L) M)) [hd L]) M) and remainder L M = if lessints M [1] then (errormessage "Division by zero!";L) else if lessints L M then L else if lessints (tl L) M then remainder (subtractints L M) M else remainder (addlistints (0::(remainder (tl L) M)) [hd L]) M; (* TOKENIZATION MODULE *) (* numeral tokenization *) (* functions for reading numerals; note that they are read backwards! *) fun isnumeral 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"; fun readdigit n nil = 0 | readdigit 0 L = 0 | readdigit n ("0"::x) = 0 + 10*(readdigit (n-1) x) | readdigit n("1"::x) = 1 + 10*(readdigit (n-1)x) | readdigit n("2"::x) = 2 + 10*(readdigit (n-1)x) | readdigit n("3"::x) = 3 + 10*(readdigit (n-1)x) | readdigit n("4"::x) = 4 + 10*(readdigit (n-1)x) | readdigit n("5"::x) = 5 + 10*(readdigit (n-1)x) | readdigit n("6"::x) = 6 + 10*(readdigit (n-1)x) | readdigit n("7"::x) = 7 + 10*(readdigit (n-1)x) | readdigit n("8"::x) = 8 + 10*(readdigit (n-1)x) | readdigit n("9"::x) = 9 + 10*(readdigit (n-1)x) | readdigit n x = 0; fun restdigit n nil = nil | restdigit 0 L = L | restdigit n (head::x) = if isnumeral head then restdigit (n-1) x else (head::x); fun readalldigits L = readdigit (length L) L; fun readalldigits2 s = readalldigits (rev (explode s)); (* is a string a numeral? *) (* it would be a good idea to refine this so that it checks that a numeral actully is a standard numeral for the current base! *) fun preisdigits nil = true | preisdigits (head::tail) = isnumeral head andalso preisdigits tail; fun isdigits s = preisdigits(explode s); (* convert string identifiers to digit lists *) fun readnumeral nil = nil | readnumeral (head::tail) = if isnumeral head then (readdigit (!DIGITL) (head::tail))::(readnumeral (restdigit(!DIGITL) (head::tail))) else nil; (* evaluate string as a digit list *) fun readnumeralstring s = readnumeral (rev(explode s)); (* evaluate string as an ML integer *) fun evalnum s = listtoint(readnumeralstring s); (* evaluate string as an ML integer, assuming base 10 rather than current base; used in variable binding scheme *) val EVALNUM = ref 1; fun evalnum10 s = (BASETEMP:=(!BASE);BASE := 10;EVALNUM := evalnum s; setbase (!BASETEMP); (!EVALNUM)); (* read integer input from a file *) fun intinput file = evalnum(stringinput file); (* constant and infix tokenization *) (* Character classification functions *) (* infixes/prefixes are made up of special characters, *) (* names of objects and theorems are made up of letters *) (* and numerals *) 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 = "|"; (* Functions which manipulate identifiers *) (* (often via the list form of the strings) *) (* strip leading spaces *) fun strip (" "::L) = strip L | strip L = L; (* reads object/theorem names; variable names start with ? *) fun getident nil = "" | getident (head::tail) = if iscap head orelse islowercase head orelse isnumeral head orelse head = "?" orelse head = "_" then head^(getident tail) else ""; (* what is left when the first identifier is read off *) fun restofident nil = nil | restofident (head::tail) = if iscap head orelse islowercase head orelse isnumeral head orelse head = "?" orelse head = "_" then restofident tail else strip(head::tail); (* functions for reading leading numerals *) fun getdigits nil = "" | getdigits (head::tail) = if isnumeral head then head^(getdigits tail) else ""; (* what is left when the first identifier is read off *) fun restofdigits nil = nil | restofdigits (head::tail) = if isnumeral head then restofdigits tail else head::tail; (* The next two functions recapitulate the last two for the case of *) (* infixes/prefixes *) (* infixes are composed of special characters *) fun getinfix nil = "" | getinfix (head::tail) = if isspecial head then head^(getinfix tail) else if head = "`" then ("`"^(getident tail)) else ""; fun restofinfix nil = nil | restofinfix (head::tail) = if isspecial head then restofinfix tail else if head = "`" then restofident tail else strip(head::tail); (* Functions which identify identifiers and infixes *) fun isident s = s <> "" andalso getident(explode s) = s; fun isinfix s = s <> "" andalso getinfix(explode s) = s; (* Functions which help further with ignoring spaces *) (* variations on hd and tl *) fun HD nil = " " | HD (" "::L) = HD L | HD L = hd L; fun TL nil = nil | TL (" "::L) = TL L | TL L = strip(tl L); (* functions recognizing reserved constants and infixes *) fun arithop s = s = "+!" orelse s = "*!" orelse s = "-!" orelse s = "" orelse s = "<=" orelse s = "=>>" orelse s = "<<="; fun isbuiltinthm s = s = "RAISE" orelse s = "VALUE" orelse s = "INPUT" orelse s = "OUTPUT" orelse s = "ORDERED" orelse s = "EVAL" orelse s = "BIND" orelse s = "UNEVAL" orelse s = "=" orelse s = "*>" orelse s = "<*" orelse s = "!!" orelse s = "|-|"; (* (* constant declarations *) (* apparently not usable because of pattern matching *) (* preserved since it's handy to have list of built-in constants *) val FORWARD = "=>"; val BACKWARD = "<="; val ALTFORWARD = "=>>"; val ALTBACKWARD = "<<="; val EQUALS = "="; val RAISE = "RAISE"; val SUCCFORWARD = "*>"; val SUCCBACKWARD = "<*"; val INLINE = "!!"; val APP = "@"; val PAIR = ","; val DELAY = "#"; val ADD = "+!"; val SUB = "-!"; val TIMES = "*!"; val DIV = "/!"; val MOD = "%!"; val LESS = " t then M else M; fun lefttree (Fork (n, (s,x), L, M)) = L; fun righttree (Fork (n, (s,x), L, M)) = M; fun topitem (Fork (n,(s,x), L, M)) = x; fun toplabel (Fork (n,(s,x), L, M)) = s; fun topnode (Fork (n,(s,x), L, M)) = (s,x); fun counttree Empty=0 |counttree (Fork(n,(s,x),L,M)) = n; (* Functions which manipulate "finite sets" of strings *) (* the "item" field is ignored here *) (* addto will overwrite items with duplicate labels *) (* thus foundin must be used to test *) fun leftmost (Fork(n,(s,x),Empty,M)) = (s,x) | leftmost (Fork(n,(s,x),L,M)) = leftmost L; fun rightmost (Fork(n,(s,x),L,Empty)) = (s,x) | rightmost (Fork(n,(s,x),L,M)) = rightmost M; fun popleftmost (Fork(n,(s,x),Empty,M)) = M | popleftmost (Fork(n,(s,x),L,M)) = Fork(n-1,(s,x),popleftmost L,M); fun poprightmost (Fork(n,(s,x),L,Empty)) = L | poprightmost (Fork(n,(s,x),L,M)) = Fork(n-1,(s,x),L,poprightmost M); fun poptree Empty = Empty | poptree (Fork (n,(s,x),L,M)) = if L = Empty then M else if M = Empty then L else if counttree L < counttree M then (Fork (n-1,leftmost M,L,popleftmost M)) else (Fork (n-1,rightmost L,poprightmost L,M)); (* is first argument found in the second, tree argument? *) fun foundin s Empty = false | foundin s (Fork(n,(t,x), L, M)) = if s = t then true else foundin s (treechoose s t L M); fun foundinrange y Empty = false | foundinrange y (Fork(n,(s,x),L,M)) = if y = x then true else (foundinrange y L) orelse (foundinrange y M); (* add an item to a tree -- won't overwrite *) fun preaddto s x Empty = Fork(1,(s,x),Empty,Empty) | preaddto s x (Fork(n,(t,y),L,M)) = if s = t then (Fork(n,(t,y),L,M)) else if s < t then rebalance(Fork(n+1,(t,y),preaddto s x L,M)) else rebalance(Fork(n+1,(t,y),L,preaddto s x M)) and rebalance Empty = Empty | rebalance (Fork(n,(s,x),L,M)) = if counttree L < (counttree M) - 1 then (Fork(n,leftmost M, preaddto s x L,popleftmost M)) else if counttree M < (counttree L) - 1 then (Fork(n,rightmost L,poprightmost L, preaddto s x M)) else (Fork(n,(s,x),L,M)); (* drop an item from a tree (by label) *) fun drop s Empty = Empty | drop s (Fork (n,(t,x), L, M)) = if foundin s (Fork (n,(t,x), L, M)) then if s = t then poptree (Fork (n,(t,x), L, M)) else if s < t then rebalance(Fork (n-1,(t,x), drop s L, M)) else rebalance(Fork(n-1,(t,x), L, drop s M)) else(Fork (n,(t,x), L, M)) ; (* a synonym; not equivalent in older implementations *) val dropitem = drop; (* preaddto will not overwrite items, as the addto function will *) (* it may be that preaddto will work in all actual applications in *) (* the program; this should be checked *) fun addto s x L = if foundin s L then preaddto s x (dropitem s L) else preaddto s x L; (* a "set" of strings with one element *) fun singleton s = addto s () Empty; (* addto for sets of strings *) fun addtoset s L = addto s () L; (* a single pair *) fun onepair (s,x) = addto s x Empty; (* uncurried addto *) fun addnode (s,x) L = addto s x L; (* merge trees *) (* does not check for consistency; will overwrite data *) fun mergewith Empty L = L | mergewith L Empty = L | mergewith (Fork(n,(s,x),L,M)) N = addto s x (mergewith N (mergewith L M)); (* apply a function to each label-data pair in a tree *) fun Map f Empty = Empty | Map f (Fork(n,(s,x),L,M)) = addnode (f(s,x)) (mergewith (Map f L) (Map f M)); (* carry out an action for each label in a tree *) fun dofor f Empty = () | dofor f (Fork (n,(s,x),L,M)) = (dofor f L;f(s);dofor f M); fun conglomerate g f u Empty = u | conglomerate g f u (Fork(n,(s,x),L,M)) = f(conglomerate g f u L) (f(g s) (conglomerate g f u M)); (* are all the elements of the first list argument found in the second? *) fun sublist Empty L = true | sublist (Fork (n,(s,x), L, M)) N = foundin s N andalso sublist L N andalso sublist M N; (* convert trees to lists in various ways *) (* list of labels *) fun treetolabellist Empty = nil | treetolabellist (Fork(n,(s,x),L,M)) = (treetolabellist L)@[s]@(treetolabellist M); (* list of label-data pairs *) fun treetolist Empty = nil | treetolist (Fork(n,(s,x),L,M)) = (treetolist L)@[(s,x)]@(treetolist M); (* flat list of alternating labels and data *) fun treetolist2 Empty = nil | treetolist2 (Fork(n,(s,x),L,M)) = (treetolist2 L)@ [s,x]@(treetolist2 M); (* convert a list to a string of items separated by tabs *) fun listtostring nil = "" | listtostring (s::L) = s^"\t"^(listtostring L); (* convert lists to trees in various ways *) (* source is list of label-data pairs *) fun listtotree nil = Empty | listtotree ((s,x)::L) = addto s x (listtotree L); (* source is list of labels only *) fun labellisttotree nil = Empty | labellisttotree (s::L) = addto s () (labellisttotree L); (* flatten an unbalanced tree; used only by the scan function *) fun flatten Empty = Empty | flatten (Fork(n,(s,x),L,M)) = if counttree L < (counttree M)-1 then flatten(Fork(n,leftmost M,addto s x L, popleftmost M)) else if counttree M < (counttree L)-1 then flatten(Fork(n,rightmost L,poprightmost L, addto s x M)) else (Fork(n,(s,x),flatten L,flatten M)); (* output functions for this type *) fun tailstring nil = "]" | tailstring [s] = "\""^s^"\"]" | tailstring (x::y) = "\""^x^"\","^(tailstring y); fun liststring L = "["^(tailstring L); fun treelabelstring L = liststring(treetolabellist L); (* functions used to handle save files from the CAML Light version *) (* (* produces strings in CAML format *) fun camltailstring nil = "]" | camltailstring [s] = "\""^s^"\"]" | camltailstring (x::y) = "\""^x^"\";"^(camltailstring y); fun camlliststring L = "["^(camltailstring L); fun camltreelabelstring L = (camlliststring (treetolabellist L)); *) (* functions to extract labels and data from pairs *) fun label (s,t) = s; fun item (s,t) = t; (* is an item labelled by the first argument found in the second argument *) (* returns a singleton list containing the item so labelled, otherwise *) (* returns nil *) fun find s Empty = nil | find s (Fork(n,(t,x),L,M)) = if s = t then [x] else find s (treechoose s t L M); (* a variation on find which returns the item or a default value *) (* now optimized to supersede find wherever a natural default exists *) fun safefind default s Empty = default | safefind default s (Fork(n,(t,u),L,M)) = if s = t then u else safefind default s (treechoose s t L M); (* a safe test for presence or absence of items on a list *) fun isnotin default s L = safefind default s L = default; fun isin default s L = safefind default s L <> default; (* drops item labelled by first argument from second, list argument *) (* if there is one *) (* can two lists be merged without loss of data? *) fun compatible Empty L = true | compatible (Fork(n,(s,x),L,M)) N = (find s N = nil orelse find s N = [x]) andalso compatible L N andalso compatible M N; (* are two lists disjoint (labelwise)? *) fun disjoint Empty L = true | disjoint (Fork(n,(s,x),L,M)) N = find s N = nil andalso disjoint L N andalso disjoint M N; (* merge two nonempty lists if they are compatible; under all other conditions return Empty *) fun consistentwith L M = if L = Empty orelse M = Empty then Empty else if compatible L M then (mergewith L M) else Empty; (* as the previous, but requires disjointness instead of compatibility *) (* not in use *) fun linearconsistentwith L M = if disjoint L M then (mergewith L M) else Empty; (* diagnostic tool for looking at trees *) fun treestructure Empty = "" | treestructure (Fork(n,(s,t),L,M)) = "("^(treestructure L)^")" ^(makestring(counttree L))^" " ^s^" " ^(makestring(counttree M))^" ("^(treestructure M)^")"; fun showtreestructure L = output(std_out,treestructure L); (* display trees with string data in tabular form *) fun showtable Empty = () | showtable (Fork(n,(s,t),L,M)) = (showtable L; output(std_out,s^"\t "^t^"\n");showtable M); (* variation showing only the labels; produces string, not unit *) fun showsettable Empty = "" | showsettable (Fork(n,(s,t),L,M)) = (showsettable L)^ s^"\n"^(showsettable M); (* tool for scanning a tree; parameters are a reference to the tree and a function for reading the data *) (* this command has its own interface; one types l to go left, r to go right, q to quit, to see the item currently being scanned without moving, h (or any other character) for help *) (* definitely use q to quit! The scanning process unbalances the tree to be scanned! *) val QUERY = ref "a"; fun scan reader book = (QUERY := input(std_in,1); if (!QUERY) = "q" orelse (!book) = Empty then (book:=flatten(!book)) else if (!QUERY) = "\n" then (reader (label(topnode(!book))); scan reader book) else if (!QUERY) = "l" then if lefttree (!book) = Empty then (errormessage "At beginning";scan reader book) else ((* reader(label(rightmost(lefttree(!book))));*) book := Fork(counttree (!book), rightmost(lefttree(!book)), poprightmost(lefttree(!book)), addnode (topnode(!book)) (righttree(!book))); (scan reader book)) else if (!QUERY) = "r" then if righttree (!book) = Empty then (errormessage "At end";scan reader book) else ( book := Fork(counttree (!book), leftmost (righttree (!book)), addnode (topnode(!book)) (lefttree(!book)), popleftmost (righttree(!book))); (scan reader book)) else (errormessage " to view,l to go left, r to go right, q to quit"; scan reader book)); (* are all labels in first "set of strings" found in second tree? *) fun allfound Empty list1 = true | allfound (Fork(n,(x,()),L,M)) list1 = (find x list1 <> nil) andalso allfound L list1 andalso allfound M list1; (* are all labels in first "set of strings" found as data in second tree? *) fun allfoundinrange Empty list1 = true | allfoundinrange (Fork(n,(x,()),L,M)) list1 = foundinrange x list1 andalso allfoundinrange L list1 andalso allfoundinrange M list1; (* how many times is x found as data in a tree? *) fun numberfound x Empty = 0 | numberfound x (Fork(n,(s,y),L,M)) = (if x = y then 1 else 0)+(numberfound x L)+(numberfound x M); (* is a tree a one-to-one function? *) fun isafunction Empty = true | isafunction (Fork(n,(s,x),L,M)) = (numberfound x (Fork(n,(s,x),L,M)) = 1 andalso isafunction (mergewith L M)); fun funtest L = if isafunction L then L else Empty; (* crunch together a tree of trees *) fun crunch Empty = Empty | crunch (Fork(n,(s,t),L,M)) = mergewith t (mergewith(crunch L)(crunch M)); (* output functions for this type (when range items are strings only) *) fun tailstringpair nil = "]" | tailstringpair [(s,t)] = "(\""^s^"\",\""^t^"\")]" | tailstringpair ((s,t)::tail) = "(\""^s^"\",\""^t^"\")," ^(tailstringpair tail); fun liststringpair L = "["^(tailstringpair L); fun treestringpair L = liststringpair(treetolist L); (* (* CAML versions *) fun camltailstringpair nil = "]" | camltailstringpair [(s,t)] = "(\""^s^"\",\""^t^"\")]" | camltailstringpair ((s,t)::tail) = "(\""^s^"\",\""^t^"\");" ^(camltailstringpair tail); fun camlliststringpair L = "["^(camltailstringpair L); fun camltreestingpair L = camlliststringpair(treetolist L); *) (* input functions for reading trees and "sets of strings" from files *) val DEPQUERY = ref "a"; fun walkreadlist file s = (DEPQUERY:=stringinput file; if (!DEPQUERY)="" then () else (s:= addtoset (!DEPQUERY) (!s);walkreadlist file s)); val LISTQUERY2 = ref"a"; fun walkreadpairlist file s = (DEPQUERY:=stringinput file; if (!DEPQUERY)="" then () else (LISTQUERY2:= stringinput file; if (!LISTQUERY2)="" then () else ( s:= addto (!DEPQUERY)(!LISTQUERY2)(!s);walkreadpairlist file s))); (* structure and commands supporting online help *) val HELP = ref(listtotree([("bogus","bogus")])); HELP:=Empty; fun posthelp key text = HELP:=addto key text (!HELP); posthelp "posthelp" "posthelp key text; causes `text' to be used\nas online help text for `key'"; fun gethelp key = if foundin key (!HELP) then errormessage (safefind "" key (!HELP)) else errormessage ("No help available on "^key); posthelp "gethelp" "gethelp key; causes the prover to display online help about `key'"; fun displayhelp key = (errormessage key; gethelp key); fun scanhelp() = scan displayhelp HELP; posthelp "scanhelp" "scanhelp(); allows one to browse the online help.\n use to see where you are, l to go back in alphabetical order,\nr to go forward, q to quit"; posthelp "versiondate" "versiondate(); causes the date of the source code to be displayed"; posthelp "initializecounter" "initializecounter(); causes the new variable counter to be set to zero.\nThis is useful in scripts."; (* TERM MODULE *) (* The type of terms of the underlying language, with its parser *) (* and display function, plus matching, substitution, and *) (* definition format functions *) (* Some user commands in the working environment *) (* also have access to term structure *) (* Miscellaneous functions with access to this type will be listed *) (* The type itself *) datatype term = Constant of string | Variable of string | ConstantFunction of term | (* name now misleading; general binding context *) Parenthesis of term | (* used only by the parser so far *) Infix of term*string*term; (* generic items *) val genericconstant = Constant "x"; val genericvariable = Variable "x"; val nameofgenericvariable = "?x" ; (* Given an atomic term, returns the appropriate identifier: use to fix *) (* some ADT violations below *) fun ident (Constant s) = s | ident (Variable s) = "?"^s | ident x = "{"; (*an impossible value*) fun identstring (Constant s) = s | identstring (Variable s) = s | identstring x = "{"; (*an impossible value*) fun isvariable s = s <> "" andalso hd(explode s) = "?"; (* Given an atomic object identifier, returns the appropriate constant or *) (* variable term *) fun ConorVar s = if isvariable s then Variable(implode(tl(explode s))) else Constant s; (* variables with numeral names will be bound variables *) fun isplusdigits s = s<>"" andalso hd(explode s)<>"0" andalso isdigits s; fun hasleadingdigits s = getdigits (explode s) <> "" andalso hd(explode(getdigits (explode s))) <> "0" andalso restofdigits(explode s) <> nil andalso hd(restofdigits(explode s)) = "_"; fun digitprefix s = evalnum10 (getdigits(explode s)); fun digitrestof s = implode(tl(restofdigits (explode s))); fun isboundvar s = isvariable s andalso s<>"?" andalso isplusdigits (implode(tl(explode s))); fun numboundvars Empty = 0 | numboundvars(Fork(n,(s,x),L,M)) = (if isboundvar s then 1 else 0)+ (numboundvars L) + (numboundvars M); (* this function determines whether a "stratification list" contains any information *) fun stratinfo L = (numboundvars (hd L) > 0) orelse map (fn x => numboundvars x > 1) L <> map (fn x=> false) L; fun isfreevar s = isvariable s andalso not(isboundvar s); fun p1(x,y)=x; fun p2(x,y) = y; fun numfreevars Empty = 0 | numfreevars(Fork(n,(s,x),L,M)) = (if isfreevar s then 1 else 0)+ (numfreevars L) + (numfreevars M); (* this function determines whether a "stratification list" contains any information *) fun freestratinfo L = (numfreevars (hd L) > 0) orelse map (fn x => numfreevars x > 1) L <> map (fn x=> false) L; (* the parameter f is either "isboundvar" or "isfreevar" *) (* these functions are used for fine-tuning stratification *) fun findshift f Empty L = (false,0) | findshift f (Fork(n,(s,(x:int)),L,M)) N = if find s N <> nil andalso (f(s)) then (true,(x-(hd(find s N)))) else let val (found,shift) = findshift f L N in if found then (found,shift) else findshift f M N end; fun shiftcompatible f L M = compatible L (Map (fn (s,x) => (s,if f(s) then x+p2(findshift f L M) else x)) M); fun shiftconsistentwith f L M = consistentwith L (Map (fn (s,x) => (s,if f(s) then x+p2(findshift f L M) else x)) M); fun shiftcollapse1 f nil = nil | shiftcollapse1 f (Empty::tl) = [Empty] | shiftcollapse1 f (hd::nil) = hd::nil | shiftcollapse1 f (hd::(Empty::tl)) = [Empty] | shiftcollapse1 f (hd::(tl1::tl)) = if p1(findshift f hd tl1) then shiftcollapse1 f ((shiftconsistentwith f hd tl1)::tl) else (shiftcollapse1 f (hd::tl))@[tl1]; fun shiftcollapse f nil = nil | shiftcollapse f (hd::tl) = shiftcollapse1 f (hd::(shiftcollapse f tl)); (* shiftmerge keeps all separate lists apart; it seems to be expensive to try to figure out which ones should and which ones should not be merged *) (* the first element of a list is always "fixed" types *) fun shiftmerge f list1 list2 = if list1 = nil orelse list2 = nil then nil else shiftcollapse f ([consistentwith (hd list1) (hd list2)]@(tl list1)@(tl list2)); fun varnum s = if isboundvar s then evalnum10 (implode(tl(explode s))) else ~1; (* Functions for identifying type-raised infixes (infixes to which the unary operation represented by initial ":" has been applied one or more times) and infix variables (with prefixed "^") *) fun isinfixvar s = s<>"" andalso s <> "^" andalso hd(explode s) = "^"; fun prederaise nil = nil | prederaise [":"] = [":"] | prederaise (head::tail) = if head = ":" then prederaise tail else (head::tail); fun deraise s = implode(prederaise(explode s)); fun israised s = s <> "" andalso s <> ":" andalso hd(explode s) = ":"; fun prelowerone nil = nil | prelowerone (":"::tail) = tail | prelowerone x = x; fun lowerone s = implode(prelowerone(explode s)); fun raiseone s = ":"^s; (* List of instructions for parsing prefix expressions *) (* Unary operators are always overloaded infixes; the prefix list *) (* supplies a default first argument for the infix expression, which *) (* the parser inserts. The display function always omits this default *) (* first argument. For example, if the first argument for subtraction is 0: *) (* -x means 0-x, and 0-x is always displayed as 0. *) (* the tree of default type information *) val TYPEINFO = ref(listtotree([("bogus",Constant "bogus")])); TYPEINFO := Empty; fun typeinfoval s = safefind (Constant "") s (!TYPEINFO); (* fun declaretypeinfo s t = TYPEINFO := addto s (parse t) (!TYPEINFO); *) fun detypeinfo s = TYPEINFO := dropitem s (!TYPEINFO); fun typeinfoterm (Variable s) = typeinfoval s | typeinfoterm x = Constant ""; (* the tree of default left argument information *) val PREFIXINFO = ref(listtotree([("bogus","bogus")])); PREFIXINFO := Empty; fun prefixval s = safefind ("") s (!PREFIXINFO); fun prefixterm s = if not(israised s) then Constant(prefixval s) else ConstantFunction (prefixterm (lowerone s)); (* USER COMMANDS (2) *) (* declare or remove a default left argument for an infix *) fun declareprefix s t = if s = ":" then errormessage "No default prefix of :" else PREFIXINFO := (addto s t (!PREFIXINFO)); posthelp "declareprefix" "declareprefix s t; allows s to be used as a unary prefix operator\nt will be the default left subterm of a prefix term with operator s."; fun deprefix s = PREFIXINFO := (dropitem s (!PREFIXINFO)); posthelp "deprefix" "deprefix s; causes the operator s to no longer be usable as a unary operator"; (* tree of precedence information *) (* even precedences associate to the right, odd to the left *) val PRECEDENCEINFO = ref(listtotree([("bogus",0)])); PRECEDENCEINFO:= Empty; (* the highest precedence in use *) val MAXPREC = ref 0; (* USER COMMAND *) (* set the precedence of an infix. Odd precedences associate to the left, even to the right *) fun setprecedence s n = if n <0 then errormessage "No negative precedence" else (PRECEDENCEINFO := (addto s n (!PRECEDENCEINFO)); if n>(!MAXPREC) then MAXPREC := n else ()); posthelp "setprecedence" "setprecedence s n; sets precedence of operator s to\nnonnegative integer value n; even values associate to the left\nand odd to the right."; fun precedenceof s = safefind 0 (deraise s) (!PRECEDENCEINFO); (* USER COMMAND *) (* clear all precedences, restoring the APL convention (flat precedence, everything associates to the right *) fun clearprecs() = (PRECEDENCEINFO:=Empty;MAXPREC:=0); posthelp "clearprecs" "clearprecs(); sets all precedences to 0, which restores\nthe default APL convention;\nall operators have the same predecence and associate to the right."; (* USER COMMAND *) (* Show infix precedences in a table format *) fun showprecs() = showtable (Map (fn (s,n) => (s,(makestring n)^"\t"^(if n mod 2 = 0 then "R" else "L"))) (!PRECEDENCEINFO) ); posthelp "showprecs" "showprecs(); displays all precedences in a table format\nincluding the redundant associativity information (L or R)"; (* The old display function. Constant "" is an error value. Spaces are inserted flanking binary infixes. Used in save files.*) (* WARNING: this function always displays in the default order of operations mode!!! *) fun display (Constant "") = (errormessage("Errors found in displayed term"); " ") | display (Constant s) = ident(Constant s) | display (Variable s) = ident(Variable s) | display (ConstantFunction x) = "["^(display x)^"]" | display (Infix(Infix (x,s,y),t,z)) = (* if precedenceof s <= precedenceof t then *) "("^(display(Infix(x,s,y)))^") "^t^" "^(display z) (* else (display(Infix(x,s,y)))^" "^t^" "^(display z) *) | display (Infix(x,s,y)) = if x = prefixterm s then " "^s^(display y) else (display x)^" "^s^" "^(display y); (* The pretty display function *) (* precedence testing functions *) fun stickiness (Infix(x,s,y)) = precedenceof s | stickiness x = 0; fun isinfixterm (Infix(x,s,y)) = true | isinfixterm x = false; fun parentest x s b = isinfixterm x andalso ((stickiness x < precedenceof s) orelse (stickiness x = precedenceof s andalso ((stickiness x) mod 2 = b))); fun reassociate p (Infix(x,s,Infix(y,t,z))) = if p mod 2 = 1 andalso precedenceof s = p andalso precedenceof t = p andalso y <> prefixterm t then (Infix(reassociate p (Infix(x,s,y)),t,z)) else (Infix(x,s,(Infix(y,t,z)))) | reassociate p x = x; fun deparenthesize (Parenthesis x) = deparenthesize x | deparenthesize (Infix(x,s,y)) = Infix(deparenthesize x,s,deparenthesize y) | deparenthesize (ConstantFunction x) = ConstantFunction (deparenthesize x) | deparenthesize x = x; (* term length function *) fun termlength (Constant s) = stringlength(ident(Constant s)) | termlength (Variable s) = stringlength (ident(Variable s)) | termlength (Parenthesis x) = 2+(termlength x) | termlength (ConstantFunction s) = 2+(termlength s) | (* termlength (Infix(x,"><",y)) = 2+(termlength y) | *) termlength (Infix(x,s,y)) = if x = prefixterm s then (stringlength s)+(termlength y)+1+ (if parentest y s 1 then 2 else 0) else (stringlength s)+(termlength x)+ (termlength y) + 2 + (if parentest x s 0 then 2 else 0) +(if parentest y s 1 then 2 else 0); fun firsttermlength (Infix(x,s,y)) = if x = prefixterm s then termlength (Infix(x,s,y)) else (termlength x) + (if parentest x s 0 then 2 else 0) | firsttermlength x = termlength x; fun lasttermlength (Infix(x,s,y)) = if x = prefixterm s then termlength (Infix(x,s,y)) else (termlength y) + (if parentest y s 1 then 2 else 0) | lasttermlength x = termlength x; (* the position of the cursor as term is displayed *) val CURSOR = ref 0; val LINE = ref 50; val OLDLINE = ref 50; val DEPTH = ref ~1; fun movecursor t = CURSOR := (!CURSOR) + (termlength t); fun cursorhome n = CURSOR := 3*n; fun bumpcursor n = CURSOR := (!CURSOR)+(n:int); fun indents n = if n <= 0 then "" else (indents(n-1)^" "); (* tests for line breaks *) fun maybeline n m1 m = if ((!CURSOR) + m) > (!LINE) orelse (!CURSOR) < m1 then (cursorhome((!DEPTH)-n);"\n"^ (indents((!DEPTH)-n))) else ""; (* parameters are depth of display and term to be displayed; displays in a nice indented format reflecting the precedence structure of the term *) (* attempted fix for problem with display of long left-associated terms; effect can be reversed by getting rid of "lasttermlength" in favor of "termlength" *) fun bdisplay n (Constant "") = (errormessage("Errors found in displayed term"); " ") | bdisplay n (Constant s) = (movecursor(Constant s);ident(Constant s)) | bdisplay n (Variable s) = (movecursor(Variable s);ident(Variable s)) | bdisplay 0 t = (bumpcursor 5; " ?#? ") | bdisplay n (ConstantFunction x) = ((bumpcursor 1);"[")^ (bdisplay (n-1) x)^((bumpcursor 1);"]") | bdisplay n (Parenthesis x) = ((bumpcursor 1);"{")^ (bdisplay (n-1) x)^((bumpcursor 1);"}") | (* bdisplay n (Infix(x,"><",y)) = (bumpcursor ((stringlength "><")+1); " "^"><")^(bdisplay n y) | (* hiding infix *) *) bdisplay n (Infix(x,s,y)) = if x = prefixterm s orelse (s = ":" andalso x = typeinfoterm y) then (bumpcursor ((stringlength s));(* " "^ *) s)^ (if parentest y s 1 then (bumpcursor 1;"(") else (bumpcursor 1;" "))^ (bdisplay (n-1)y)^ (if parentest y s 1 then (bumpcursor 1;")") else "") else (if parentest x s 0 then (bumpcursor 1;"(") else "")^ (bdisplay(if parentest x s 0 then n-1 else n)x)^ (if parentest x s 0 then (bumpcursor 1;")") else "")^ (bumpcursor 1;" ")^ (maybeline n (lasttermlength x) ((stringlength s)+1+ (firsttermlength y)))^ (bumpcursor(stringlength s);s)^(bumpcursor 1;" ")^ (if parentest y s 1 then (bumpcursor 1;"(") else "")^ (bdisplay (if parentest y s 1 then n-1 else n) y)^ (if parentest y s 1 then (bumpcursor 1;")") else ""); (* the directly usable display function *) fun bddisplay t = (cursorhome 0;bdisplay (!DEPTH) t); val QUIET = ref 2; fun bequiet() = QUIET:=0; (* cuts off all display *) fun thmsonly() = QUIET:=1; (* cuts off term display; theorems still shown *) fun speakup() = QUIET:=2; (* restores full verbosity *) fun lookat t = if (!QUIET)<>2 then t else (output(std_out,"\n\n"^(bddisplay t)^"\n\n");t); (* nice display without newlines *) fun nicedisplay (Constant "") = (errormessage( "Errors found in displayed term"); " ") | nicedisplay (Constant s) = (ident(Constant s)) | nicedisplay (Variable s) = (ident(Variable s)) | nicedisplay (ConstantFunction x) = ("[")^ (nicedisplay x)^("]") | nicedisplay (Infix(x,s,y)) = if x = prefixterm s orelse(s = ":" andalso x = typeinfoterm y) then (s)^ (if parentest y s 1 then ("(") else " ")^ (nicedisplay y)^ (if parentest y s 1 then (")") else "") else (if parentest x s 0 then ("(") else "")^ (nicedisplay x)^ (if parentest x s 0 then (")") else "")^ (" ")^ (s)^(" ")^ (if parentest y s 1 then ("(") else "")^ (nicedisplay y)^ (if parentest y s 1 then (")") else ""); (* The parser -- divided into "first term read from string" and *) (* "rest of string" *) fun quotelessthan m n = (m:int)< n; (* originally was less simple *) fun restofterm p nil = nil | restofterm p z = let val x = HD z and L = TL z and y = strip z in if p = (!MAXPREC) then if x = " " then restofterm p L else if iscap x orelse islowercase x orelse isnumeral x orelse x = "?" orelse x = "_" then if restofident y = nil orelse HD(restofident y) = ")" orelse HD(restofident y) = "]" orelse HD(restofident y) = " " orelse (isspecial (HD(restofident y)) andalso (quotelessthan (precedenceof(getinfix(restofident y))) p)) then restofident y else if (isspecial(HD(restofident y)) orelse (HD(restofident y))="`") then restofterm p (restofinfix(restofident y)) else nil else if x = "(" then let val M = restofterm 0 L in if M = nil then nil else if HD(M) = ")" then if M = [")"] orelse HD(TL(M)) = ")" orelse HD(TL(M)) = "]" orelse HD(TL(M)) = " " orelse (isspecial (HD(TL(M))) orelse (HD(TL(M)))="`" ) andalso (quotelessthan (precedenceof(getinfix(TL(M)))) p) then TL(M) else if isspecial(HD(TL(M))) orelse (HD(TL(M)))="`" then restofterm p (restofinfix(TL(M))) else nil else nil end else if x = "[" then let val M = restofterm 0 L in if M = nil then nil else if HD(M) = "]" then if M = ["]"] orelse HD(TL(M)) = ")" orelse HD(TL(M)) = "]" orelse HD(TL(M)) = " " orelse ((isspecial (HD(TL(M)))) orelse (HD(TL(M)))="`") andalso (quotelessthan (precedenceof(getinfix(TL(M)))) p) then TL(M) else if (isspecial(HD(TL(M))) orelse (HD(TL(M)))="`") then restofterm p (restofinfix(TL(M))) else nil else nil end else if (isspecial x orelse x = "`") then restofterm p (restofinfix y) else nil else let val M = restofterm (p+1) y in if M = nil orelse HD(M) = ")" orelse HD(M) = "]" orelse HD(M) = " " orelse ((isspecial (HD M) orelse HD M = "`") andalso (quotelessthan (precedenceof (getinfix M)) p)) then M else restofterm p (restofinfix(M)) end end; fun getterm p nil = Constant "" | getterm p z = let val x = HD z and L = TL z and y = strip z in if p = (!MAXPREC) then if x = " " then getterm p L else if iscap x orelse islowercase x orelse isnumeral x orelse x = "?" orelse x = "_" then if restofident y = nil orelse HD(restofident y) = ")" orelse HD(restofident y) = "]" orelse ((isspecial (HD(restofident y)) orelse (HD(restofident y)) = "`") andalso (quotelessthan (precedenceof(getinfix(restofident y))) p)) then ConorVar(getident y) else if (isspecial(HD(restofident y)) orelse (HD(restofident y)) = "`") then reassociate p (Infix(ConorVar(getident (y)), getinfix(restofident y), getterm p (restofinfix(restofident y)))) else Constant "" else if x = "(" then let val M = restofterm 0 L in if M = nil then Constant "" else if HD(M) = ")" then if M = [")"] orelse HD(TL(M)) = ")" orelse HD(TL(M)) = "]" orelse HD(TL(M)) = " " orelse ((isspecial (HD(TL(M))) orelse (HD(TL(M))) = "`") andalso (quotelessthan (precedenceof(getinfix (TL(M)))) p)) then Parenthesis(getterm 0 L) else if (isspecial(HD(TL(M))) orelse (HD(TL(M))) = "`") then reassociate p ( Infix(Parenthesis(getterm 0 L), getinfix(TL(M)), getterm p (restofinfix(TL(M))))) else Constant "" else Constant "" end else if x = "[" then let val M = restofterm 0 L in if M = nil then Constant "" else if HD(M) = "]" then if M = ["]"] orelse HD(TL(M)) = ")" orelse HD(TL(M)) = "]" orelse HD(TL(M)) = " " orelse ((isspecial (HD(TL M)) orelse (HD(TL M)) = "`") andalso quotelessthan (precedenceof (getinfix (TL M))) p) then ConstantFunction(getterm 0 L) else if (isspecial(HD(TL(M))) orelse (HD(TL M)) = "`") then reassociate p (Infix(ConstantFunction(getterm 0 L), getinfix(TL(M)), getterm p (restofinfix (TL(M))))) else Constant "" else Constant "" end else if x = ":" andalso getinfix y = ":" then reassociate p (Infix( (typeinfoterm(getterm p (restofinfix y)), ":",getterm p (restofinfix y)))) else if (isspecial x orelse x = "`") then reassociate p (Infix((prefixterm(getinfix(y))), getinfix(y), getterm p (restofinfix y))) else Constant "" else let val M = restofterm (p+1) y in if M = nil orelse HD(M) = ")" orelse HD(M) = "]" orelse HD(M) = " " orelse ((isspecial (HD M) orelse HD M = "`") andalso (quotelessthan (precedenceof (getinfix M)) p)) then getterm (p+1) y else reassociate p (Infix(getterm (p+1) y, getinfix M, getterm p (restofinfix M))) end end; (* The parser proper; if the entire string is not used, it adds a leading parenthesis, issues a warning, and tries again *) fun parse s = if restofterm 0 (explode s) = nil then deparenthesize(getterm 0 (explode s)) else (errormessage "Warning: adding leading parenthesis"; parse ("("^s)); (* used by following function *) fun subtermcomplain x = (errormessage "Subterm error";x); (* function which enables application of a function to a *) (* subterm indicated by a list of booleans; *) (* used by "exec" function below. *) fun preexec nil f t = f t | preexec (true::L) f (Infix(x,s,y)) = Infix(preexec L f x,s,y) | preexec (false::L) f (Infix(x,s,y)) = Infix(x,s,preexec L f y) | preexec (b::L) f (ConstantFunction t) = ConstantFunction(preexec L f t) | preexec L f t = subtermcomplain t; (* function which checks the constants in the term against a list *) (* it rejects terms with constants not on the list *) (* it issues its own error messages for badly formed hypotheses and case expressions *) fun constantcheck L (Constant s) = s <> "" andalso (isdigits s orelse isbuiltinthm s orelse not(find s L = nil))| constantcheck L (Variable s) = true | constantcheck L (ConstantFunction t) = constantcheck L t | constantcheck L (Parenthesis t) = constantcheck L t | constantcheck L (Infix(Constant x,"|-|",Constant y)) = (x = "0" orelse x = "1" orelse x = "2") andalso isplusdigits y | constantcheck L (Infix(x,"|-|",y)) = (errormessage "Ill-formed hypothesis";false) | constantcheck L (Infix(x,"||",Infix(y,",",z))) = constantcheck L (Infix(x,",",Infix(y,",",z))) | constantcheck L (Infix(x,"||",y)) = (errormessage "Ill-formed case expression";false) | (* case expressions must have alternatives *) constantcheck L (Infix(x,s,y)) = (isinfixvar (deraise s) orelse isbuiltinthm (deraise s) orelse (not(find (deraise s) L = nil))) andalso constantcheck L x andalso constantcheck L y; (* minimum "level" (in sense of deBruijn levels) at which this term can appear *) fun minlevel (Constant s) = 0 | minlevel (Variable s) = if isplusdigits s then (evalnum10 s) else 0 | minlevel (ConstantFunction x) = if minlevel x = 0 then 0 else (minlevel x) - 1 | minlevel (Parenthesis x) = minlevel x | minlevel (Infix(x,s,y)) = max(minlevel x,minlevel y); (* same for hypothesis level *) fun minhlevel (Constant s) = 0 | minhlevel (Variable s) = 0 | minhlevel (Parenthesis x) = minhlevel x | minhlevel (ConstantFunction x) = minhlevel x | minhlevel (Infix(x,"|-|",Constant s)) = if isplusdigits s then evalnum10 s else 0 | minhlevel (Infix(x,"||",y)) = max(minhlevel x, minhlevel y - 1) | minhlevel (Infix(x,s,y)) = max (minhlevel x,minhlevel y); (* functions for recognition of definition and program format *) (* it recognizes expressions consisting essentially of a function *) (* applied to a list of parameters ("@" is function application; *) (* "," is pairing). This may be applied to further lists of parameters *) (* and parameters may have iterated applications of the constant function *) (* operator to allow type manipulation *) (* The list of bound variables appearing in a term *) fun boundvarlist (Constant s) = Empty | boundvarlist (Variable s) = if isplusdigits s then addto s () Empty else Empty | boundvarlist (ConstantFunction t) = boundvarlist t | boundvarlist (Infix (t,s,u)) = (mergewith(boundvarlist t)(boundvarlist u)); (* functions which count free and bound variables. Used in temporary fix of problem with s.c. types *) fun boundvarnumber Empty = 0 | boundvarnumber (Fork(n,(s,t),L,M)) = (if isboundvar s then 1 else 0) + (boundvarnumber L) + (boundvarnumber M); fun varnumber Empty = 0 | varnumber (Fork(n,(s,t),L,M)) = (if (isvariable s andalso (not(isboundvar s))) then 1 else 0) + (varnumber L) + (varnumber M); (* change a term from level level1 to level level2: all bound variables of index higher than level1 (bound in the original term) need to be transposed by (level2 - level1); it is also necessary to check, if level2 is less than level1, that there are no variables free in the original term which become bound in the new term; bad terms signalled by a return value of Constant "" *) (* fixed so that arithmetic on bound variable names is always done in base 10 *) fun prechangelevel level1 level2 (Constant s) = Constant s | prechangelevel level1 level2 (Variable s) = if isplusdigits s then if (evalnum10 s) > level1 then (Variable (makestring ((evalnum10 s) + level2 - level1))) else if evalnum10 s <= level1 andalso evalnum10 s > level2 then Constant "" (* a locally free variable became bound *) else Variable s else Variable s | prechangelevel level1 level2 (Parenthesis t) = Parenthesis (prechangelevel level1 level2 t) | prechangelevel level1 level2 (ConstantFunction t) = let val CHANGED = prechangelevel (level1) (level2) t in if CHANGED = Constant "" then Constant "" else ConstantFunction(CHANGED) end | prechangelevel level1 level2 (Infix(x,s,y)) = let val CHANGED1 = prechangelevel level1 level2 x and CHANGED2 = prechangelevel level1 level2 y in if CHANGED1 = Constant "" orelse CHANGED2 = Constant "" then Constant "" else Infix(CHANGED1,s,CHANGED2) end; (* produces the value of [last argument]@t when evaluated at level *) fun prebeta level t (Constant s) = Constant s | prebeta level t (Variable s) = if isplusdigits s then if (evalnum10 s) > level+1 then Variable(makestring((evalnum10 s)-1)) else if evalnum10 s = level+1 then t else Variable s else Variable s | prebeta level t (ConstantFunction u) = ConstantFunction (prebeta level (prechangelevel level (level+1) t) u) | prebeta level t (Infix(x,f,y)) = Infix(prebeta level t x,f,prebeta level t y); (* prebind will produce the innards of the variable binding context needed to express the final argument as a function of t *) fun prebind level t (Constant s) = if (Constant s) = t then Variable (makestring (level+1)) else Constant s | prebind level t (Variable s) = if isplusdigits s andalso evalnum10 s > level then Variable (makestring ((evalnum10 s)+1)) else if (Variable s) = t then Variable(makestring(level+1)) else Variable s | prebind level t (ConstantFunction u) = if t = (ConstantFunction u) then Variable (makestring (level+1)) else ConstantFunction(prebind level (prechangelevel level (level+1) t) u) | prebind level t (Infix(x,f,y)) = if t = (Infix(x,f,y)) then Variable (makestring (level+1)) else Infix(prebind level t x,f,prebind level t y); fun prechangehlevel hlevel1 hlevel2 (Constant s) = Constant s | prechangehlevel hlevel1 hlevel2 (Variable s) = Variable s | prechangehlevel hlevel1 hlevel2 (ConstantFunction x) = let val CHANGED = prechangehlevel (hlevel1) (hlevel2) x in if CHANGED = Constant "" then Constant "" else ConstantFunction CHANGED end | prechangehlevel hlevel1 hlevel2 (Infix(x,"|-|",Constant s)) = if isplusdigits s then if (evalnum10 s) > hlevel1 then (Infix(x,"|-|", Constant (makestring ((evalnum10 s) + hlevel2 - hlevel1)))) else if evalnum10 s <= hlevel1 andalso evalnum10 s > hlevel2 then Constant "" (* a locally free hyp became bound *) else Infix(x,"|-|",Constant s) else Infix(x,"|-|",Constant s) | prechangehlevel level1 level2 (Parenthesis t) = Parenthesis (prechangehlevel level1 level2 t) | (* prechangehlevel hlevel1 hlevel2 (Infix(x,"||",y)) = let val CHANGED1 = prechangehlevel hlevel1 hlevel2 x and CHANGED2 = prechangehlevel (hlevel1+1) (hlevel2+1) y in if CHANGED1 = Constant "" orelse CHANGED2 = Constant "" then Constant "" else Infix(CHANGED1,"||",CHANGED2) end | *) prechangehlevel hlevel1 hlevel2 (Infix(x,s,y)) = let val CHANGED1 = prechangehlevel hlevel1 hlevel2 x and CHANGED2 = prechangehlevel hlevel1 hlevel2 y in if CHANGED1 = Constant "" orelse CHANGED2 = Constant "" then Constant "" else Infix(CHANGED1,s,CHANGED2) end; fun changelevel level1 level2 hlevel1 hlevel2 t = let val FIRSTAPPROX = prechangelevel level1 level2 (prechangehlevel hlevel1 hlevel2 t) in if minlevel FIRSTAPPROX <= level2 andalso minhlevel FIRSTAPPROX <= hlevel2 then FIRSTAPPROX else Constant "" end; (* change levels of a matching list; return Empty if bad terms show up *) fun changelevels level1 level2 hlevel1 hlevel2 x = let val FIRSTAPPROX = Map (fn (x,y) => (x,changelevel level1 level2 hlevel1 hlevel2 y)) x in if foundinrange (Constant "") FIRSTAPPROX then Empty else FIRSTAPPROX end; fun iterconvar (Variable s) = not(isplusdigits s) | (* bound variables excluded *) (* iterconvar (ConstantFunction(Infix(Variable s,"@", Variable "1"))) = (not (isplusdigits s)) | (* in effect, allow variables specified as functions *) (* this idea doesn't work without more restrictions *) *) iterconvar (ConstantFunction t) = iterconvar (prechangelevel 1 0 t) | iterconvar t = false; (* Consider introduction of user-definable "constructors" with the *) (* same privileges as "," *) fun pairsovervars (Infix(x,s,y)) = (s = "," andalso pairsovervars x andalso pairsovervars y) | pairsovervars x = iterconvar x; fun definitionformat (Constant s) = true | definitionformat (Infix(x,"@",y)) = (definitionformat x)andalso(pairsovervars y) | definitionformat x = false; (* if a term is the left side of a definition of a constant, defhead will find this constant *) fun defhead (Constant s) = s | defhead (Infix(x,"@",y)) = defhead x | defhead x = ""; (* variant of defhead which recognizes variable defheads; used in recognizing valid forms for theorem names *) fun vdefhead (Constant s) = s | vdefhead (Variable s) = ident(Variable s) | vdefhead (Infix(x,"@",y)) = vdefhead x | vdefhead x = ""; (* recapitulates the previous set of functions for definitions of infixes *) fun preinfixdefinitionformat (Infix(x,s,y)) = (pairsovervars x orelse x = prefixterm s) andalso (pairsovervars y) | preinfixdefinitionformat x = false; fun infixdefinitionformat (Infix(x,"@",y)) = infixdefinitionformat x andalso pairsovervars y | infixdefinitionformat x = preinfixdefinitionformat x; (* if a term is the left side of the definition of an infix, ix will find this infix *) fun ix (Infix(x,"@",y)) = ix x | ix (Infix(x,s,y)) = s | ix y = ""; (* has effect of defhead or ix as appropriate *) fun eitherhead x = if defhead x = "" then ix x else defhead x; (* The list of free variables appearing in a term *) fun varlist (Constant s) = Empty | varlist (Variable s) = if isplusdigits s then Empty else addto s () Empty | varlist (ConstantFunction t) = varlist t | varlist (Infix (t,s,u)) = mergewith (if isinfixvar (deraise s) then addto (deraise s) () Empty else Empty) (mergewith(varlist t)(varlist u)); (* The master constant list -- declared early due to typed infix variables *) val trivtypes = (0,0,""); val CONSTANTS = ref(listtotree([("bogus",trivtypes)])); CONSTANTS := Empty; (* functions acting on the type "constant kind" *) fun addtypes s m n L = addto s (m,n,"") L; fun addcomment s m n c L = addto s (m,n,c) L; fun lefttype (m,n,s) = m; fun righttype (m,n,s) = n; fun commentof (m,n,s) = s; (* left and right types are relative type differentials of arguments *) (* of an infix for purposes of stratification; object constants have *) (* default zero values *) fun Lefttype s = lefttype(safefind trivtypes (deraise s) (!CONSTANTS)); fun Righttype s = righttype(safefind trivtypes (deraise s) (!CONSTANTS)); fun Commentof s = commentdecode( commentof(safefind trivtypes (deraise s) (!CONSTANTS))); (* identify infix variables with declared relative types *) (* Components of the "theory" type: lists of declarations and *) (* theorems implemented as finite sets and finite functions *) (* Auxiliary list of infixes declared "referentially opaque" *) (* also includes explicitly untyped infix variables *) val OPAQUE = ref (labellisttotree(["bogus"])); OPAQUE := Empty; (* Auxiliary lists to tell stratification checker that certain operators have "strongly Cantorian" input or output types *) (* Currently, these lists are not saved and can only be built by hand *) val SCIN = ref (listtotree([("bogus","bogus")])); val SCOUT = ref (listtotree([("bogus","bogus")])); val SCINSCOUTDEPS = ref (labellisttotree(["bogus"])); SCIN := Empty; SCOUT := Empty; SCINSCOUTDEPS := Empty; fun istypedinfixvar s = isinfix s andalso isinfixvar s andalso find s (!CONSTANTS) <> nil; (* Functions for access to declared constants *) fun changeconstants f = CONSTANTS := f(!CONSTANTS); fun dropaconstant s = changeconstants (dropitem s); fun isaconstant s = s <> "" andalso (isdigits s orelse isbuiltinthm s orelse find (deraise s) (!CONSTANTS) <> nil); (* this makes me unhappy because it includes typed infix variables! *) fun isnotaconstant s = not(isaconstant s); (* operations on opacity list *) fun isopaque s = (isaconstant s orelse isinfixvar s) andalso foundin s (!OPAQUE); fun makeopaque s = if (isinfix s andalso isaconstant s andalso (not(isopaque s))) orelse (isinfix s andalso isinfixvar s andalso not(istypedinfixvar s)) (* formula for declaring untyped infix variables *) then OPAQUE := addtoset s (!OPAQUE) else errormessage "Illegal opacity declaration"; fun isscin s = find (s) (!SCIN) <> nil; fun isscout s = find (s) (!SCOUT) <> nil; fun scinof s = safefind "" (s) (!SCIN); fun scoutof s = safefind "" (s) (!SCOUT); (* The matching function *) (* returns a finite function from the variables of the first argument *) (* to corresponding terms in the second argument, or Empty if it fails *) (* it also provides (identity) values for constants *) (* The prefix "#" is used by the onestep procedure to mark terms whose *) (* execution has been delayed; it is ignored in matching *) (* Now takes the de Bruijn level of its argument as a parameter. *) (* this assumes that the source and target are at the same level; use changelevel to avoid this assumption *) (* the match function modified on Sept. 28 in two ways: the full laziness operator has been reintroduced as "##", and restrictions on matching have been introduced to enforce confluence. An inconvenient effect of this is that expressions with rule infixes or delay prefixes in them now do not match anything; this is inconvenient for the upto family of commands and limits the usefulness of matchthm commands as well. These may be reasons to abandon confluence enforcement or to introduce a different match command for these cases (or to provide it as a parameter) *) fun isbinder (ConstantFunction x) = true | isbinder y = false; fun unbind (ConstantFunction x) = x | unbind y = y; (* Functions manipulating the constant list *) (* This is mostly a term operation, but it depends on info *) (* about infixes available only from the declarations list *) (* determines whether a term is "stratified" in the sense of *) (* "New Foundations" *) (* rejects terms with variables in "opaque" contexts as `unstratified' *) (* ignores embedded theorem applications *) (* a wee utility function *) fun safedrop s Empty = Empty | safedrop s x = addto "0" 0 (drop s x); (* stratification functions *) (* idea is that stratifications are lists of matching trees matching variables to numbers. The first element of each such list contains the types fixed relative to the type of the current term; the others are "floating" lists of types derived from terms with s.c. type labels *) (* is predicativity being enforced? *) val PREDICATIVE = ref false; fun impredicative() = PREDICATIVE := false; posthelp "impredicative" "impredicative(); causes a `predicative' theory to become `impredicative',\nwhich allows more general forms of function abstraction.\nObsolete for most purposes since theories are now impredicative by default."; (* Theorem list basic declarations; they appear here because needed by weakstratification for its management of scin/scout deps *) datatype theorem = Thm of term*term*term*(unit BinTree)*(theorem BinTree); (* Functions for the ADT "theorem" (equation plus deps) *) fun formatof (Thm(w,x,y,z,u)) = w; fun leftside (Thm(w,x,y,z,u)) = x; fun rightside (Thm(w,x,y,z,u)) = y; fun deps (Thm(w,x,y,z,u)) = z; fun module (Thm(w,x,y,z,u)) = u; (* The master list of theorems (with auxiliary lists)*) (* saved proof environments are also stored in the theorem list; their keys begin with "}", which is impossible for the name of a theorem *) val THEOREMS = ref(listtotree([("TRIV",Thm(Constant"TRIV",genericvariable, genericvariable,labellisttotree ["TRIV"],Empty))])); (* local cache for the thmresult command *) val EXCACHE = ref(!THEOREMS); EXCACHE := Empty; (* the list of theorems bound to functions (functional programs) *) val PROGRAMS = ref(listtotree([("bogus","bogus")])); (* the list of theorems which are definitions *) val DEFINITIONS = ref(listtotree([("bogus","bogus")])); PROGRAMS := Empty; THEOREMS := Empty; DEFINITIONS := Empty; (* the list of intended theorems (declared for recursive definitions) *) val PRETHEOREMS = ref (labellisttotree(["bogus"])); PRETHEOREMS := Empty; (* Functions giving access to the type "theorem designated by string" *) (* Names should be self-explanatory *) fun isatheorem s = s <>"" andalso ((isbuiltinthm s) orelse find s (!EXCACHE) <> nil orelse find s (!THEOREMS) <> nil); fun isnotatheorem s = not(isatheorem s); fun isnotapretheorem s = foundin s (!PRETHEOREMS) = false; fun isapretheorem s = foundin s (!PRETHEOREMS); fun isadefinition s = foundin s (Map(fn(x,y)=>(y,()))(!DEFINITIONS)); fun isdefined s = foundin (deraise s) (Map(fn(x,y)=>(x,()))(!DEFINITIONS)); fun definitionof s = safefind "" (deraise s) (!DEFINITIONS); (* is the object or infix s bound to a program/theorem? *) fun hasnoprogram s = safefind "" s (!PROGRAMS) = ""; fun hasaprogram s = safefind "" s (!PROGRAMS) <> ""; (* the program/theorem attached to constant s *) fun Programof s = (safefind "" s (!PROGRAMS)); (* is term in form where built-in arithmetic can be applied? *) fun arithform (Infix(Constant x,s,Constant y)) = arithop s andalso isdigits x andalso isdigits y | arithform x = false; (* the left and right sides of the theorem s *) (* val dummythm = (Constant"",Constant"",Constant"",Empty); *) val dummythm = Thm(Constant"",Constant"",Constant"",Empty,Empty); fun Formatof s = if (foundin s (!EXCACHE)) then formatof(hd(find s (!EXCACHE))) else formatof(safefind dummythm s (!THEOREMS)); fun Leftside s = if (foundin s (!EXCACHE)) then leftside(hd(find s (!EXCACHE))) else leftside(safefind dummythm s (!THEOREMS)); fun Rightside s = if (foundin s (!EXCACHE)) then rightside(hd(find s (!EXCACHE))) else rightside(safefind dummythm s (!THEOREMS)); (* experimental declaration commands for s.c. input/output of operators *) (* updates needed: these need to be incorporated into "stratification" as well as into "weakstratification". Theorems witnessing the status of the infixes should be required; the witnessing theorems should be recorded on the lists *) (* the scinform and scoutform commands do not allow the use of complex types *) fun scinform s (Infix(Variable x,s2,Variable y), Infix(Infix(t1,":",Variable x2),s3, Infix(t2,":",Variable y2))) = varlist t1 = Empty andalso varlist t2 = Empty andalso s=s2 andalso s = s3 andalso x=x2 andalso y = y2 andalso x <> y | scinform s (Infix(Infix(t1,":",Variable x2),s2, Infix(t2,":",Variable y2)), Infix(Variable x,s3,Variable y)) = varlist t1 = Empty andalso varlist t2 = Empty andalso s=s2 andalso s = s3 andalso x=x2 andalso y = y2 andalso x <> y | scinform s (Infix(Constant s2,"@",Variable x), Infix(Constant s3,"@",Infix(t,":",Variable x2))) = varlist t = Empty andalso s=s2 andalso s=s3 andalso x=x2 | scinform s (Infix(Constant s2,"@",Infix(t,":",Variable x2)), Infix(Constant s3,"@",Variable x)) = varlist t = Empty andalso s=s2 andalso s=s3 andalso x=x2 | scinform s t = false; fun scoutform s (Infix(Variable x,s1,Variable y), Infix(t,":",Infix(Variable x2,s2,Variable y2))) = varlist t = Empty andalso s = s1 andalso s = s2 andalso x = x2 andalso y = y2 andalso x<>y | scoutform s (Infix(t,":",Infix(Variable x2,s2,Variable y2)), Infix(Variable x,s1,Variable y)) = varlist t = Empty andalso s = s1 andalso s = s2 andalso x = x2 andalso y = y2 andalso x<>y | scoutform s (Infix(Constant s1,"@",Variable y), Infix(t,":",Infix(Constant s2,"@",Variable y2))) = varlist t = Empty andalso s = s1 andalso s = s2 andalso y = y2 | scoutform s (Infix(t,":", Infix(Constant s2,"@",Variable y2)),Infix(Constant s1,"@",Variable y)) = varlist t = Empty andalso s = s1 andalso s = s2 andalso y = y2 | scoutform s t = false; (* USER COMMANDS *) (* declare operators or functions to be "scin" or "scout" *) fun makescin s th = if not (isaconstant s) orelse (not (isatheorem th andalso not(isbuiltinthm th))) then errormessage "Bad argument(s)" else if scinform s (Leftside th,Rightside th) then SCIN := addto s th (!SCIN) else errormessage "Theorem not of correct form"; posthelp "makescin" "makescin s th; makes operator s `scin' if the theorem th\nis of the correct form to witness this."; fun makescout s th = if not (isaconstant s) orelse (not (isatheorem th andalso not(isbuiltinthm th))) then errormessage "Bad argument(s)" else if scoutform s (Leftside th,Rightside th) then SCOUT := addto s th (!SCOUT) else errormessage "Theorem not of correct form"; posthelp "makescout" "makescout s th; makes operator s `scout' if the theorem th\nis of the correct form to witness this."; (* safetheorem gives the whole theorem with dependencies as a package *) (* Useful for optimization *) fun safetheorem s = if foundin s (!EXCACHE) then hd(find s (!EXCACHE)) else safefind dummythm s (!THEOREMS); (* dependencies *) fun Deps s = deps(safetheorem s); fun Moduleof s = module(safetheorem s); (* stratification now enforces predicativity *) (* BEGIN *) fun weakstratification toplevel level (n:int) (Constant s) = [addto "0" 0 Empty] | weakstratification toplevel level n (Variable s) = if isplusdigits s then [addto (ident(Variable s)) n Empty] else [addto "0" 0 Empty] | weakstratification toplevel level n (ConstantFunction t) = if (not(!PREDICATIVE)) orelse prechangelevel level toplevel (ConstantFunction t) <> Constant "" then map (safedrop (ident(Variable(makestring(level+1))))) (shiftmerge isboundvar (weakstratification toplevel (level+1) (n-1) t) [(onepair ((ident(Variable(makestring (level+1)))),n-1))]) else [Empty] | weakstratification toplevel level n (Infix(x,":",y)) = let val A = weakstratification toplevel level n y and B = weakstratification toplevel level n x in if A = [Empty] orelse B = [Empty] (* this clause enforces a requirement that type labels contain bound variables only in typed contexts; a type label should carry no stratification information *) orelse stratinfo (B) then [Empty] else (B)@ (A) end | weakstratification toplevel level n (Infix(x,s,y)) = if isruleinfix s then if weakstratification toplevel level n x = [Empty] then [Empty] else weakstratification toplevel level n y else if ((not (isopaque s) andalso (not(isinfixvar s) orelse istypedinfixvar s)) orelse (prechangelevel level toplevel (Infix(x,s,y)) <> Constant "")) andalso ((not(!PREDICATIVE)) orelse ((Lefttype s >= 0 orelse prechangelevel level toplevel x <> Constant "") andalso (Righttype s >= 0 orelse prechangelevel level toplevel y <> Constant ""))) then if isscin s then (if level = 0 then () else SCINSCOUTDEPS:=mergewith (Deps(scinof s)) (!SCINSCOUTDEPS); let val A = weakstratification toplevel level n x and B = weakstratification toplevel level n y in if A = [Empty] orelse B = [Empty] then [Empty] else [addto "0" 0 Empty]@ A@ B end) else if isscout s then (if level = 0 then () else SCINSCOUTDEPS:=mergewith (Deps(scoutof s)) (!SCINSCOUTDEPS); let val A = (weakstratification toplevel level (n+(Lefttype s)) x) and B = (weakstratification toplevel level (n+(Righttype s)) y) in if A = [Empty] orelse B = [Empty] then [Empty] else [addto "0" 0 Empty]@(shiftmerge isboundvar A B) end ) else if s = "@" andalso (fn (Constant t)=> isscin t orelse isscout t | u => false) x then (if level = 0 then () else SCINSCOUTDEPS:= mergewith (Deps(let val X = (fn (Constant t)=>t) x in if isscin X then scinof X else scoutof X end ))(!SCINSCOUTDEPS); let val A = weakstratification toplevel level n y in if A = [Empty] then [Empty] else [addto "0" 0 Empty]@ A end) else shiftmerge isboundvar (weakstratification toplevel level (n+(Lefttype s)) x) (weakstratification toplevel level (n+(Righttype s)) y) else [Empty] | weakstratification toplevel level n (Parenthesis s) = weakstratification toplevel level n s; (* this function needs to be modified so that it will handle variable binding contexts correctly *) (* it may work now -- weakstratification of variable binding constants is checked as part of declaration checking *) fun stratification (n:int) (Constant s) = [addto s 0 Empty] | stratification n (Variable s) = if isplusdigits s then [addto (ident (Variable s)) 0 Empty] else [addto (ident(Variable s)) n Empty] | stratification n (ConstantFunction t) = if ((not(!PREDICATIVE)) orelse varlist (ConstantFunction t) = Empty) then stratification (n-1) t else [Empty] | stratification n (Infix(x,":",y)) = if stratification n y = [Empty] orelse stratification n x = [Empty] (* Here is the clause forbidding nontrivial type information in type labels; type labels may only have typed parameters *) orelse freestratinfo (stratification n x) then [Empty] else (stratification n x)@(stratification n y) | stratification n (Infix(x,s,y)) = if isruleinfix s then if stratification n x = [Empty] then [Empty] else stratification n y else if ((not (isopaque s) andalso (not(isinfixvar s) orelse istypedinfixvar s)) orelse (varlist(Infix(x,s,y)) = Empty)) andalso ((not(!PREDICATIVE)) orelse ((Lefttype s >= 0 orelse varlist x = Empty) andalso (Righttype s >= 0 orelse varlist y = Empty))) then shiftmerge isfreevar (stratification (n+(Lefttype s)) x) (stratification (n+(Righttype s)) y) else [Empty]; (* END *) (* new improved strat functions *) (* predicativity checking is now carried out inside the stratification functions *) (* tools for checking predicativity if desired *) (* checks for occurrences of variables in contexts which should be opaque in predicative theories *) (* is predicativity for expressions with variable binding handled correctly? *) (* Should write functions to test variable binding contexts for predicativity *) (* fun prepredtest (ConstantFunction t) = varlist t = Empty | prepredtest (Infix(x,s,y)) = (Lefttype s >= 0 orelse varlist x = Empty) andalso (Righttype s >= 0 orelse varlist y = Empty) andalso prepredtest x andalso prepredtest y | prepredtest x = true; fun predtest x = if (!PREDICATIVE) then prepredtest x else true; *) (* higher order matching is being curbed to apply to only one variable *) (* higher-order matching tool *) (* fun rightform n (Variable s) = not(isplusdigits s) | rightform n (Infix(x,"@",Variable m)) = isplusdigits m andalso (evalnum10 m) = n andalso rightform (n-1) x | rightform n x = false; *) (* confluence does not quite hold *) fun match level hlevel x (Infix(z,"#",y)) = match level hlevel x y | match level hlevel (Infix(z,"#",x)) y = (Empty) | (* prefix above forms inert forms of "active" infixes *) match level hlevel x (Infix(z,"##",y)) = match level hlevel x y | match level hlevel (Infix(z,"##",y)) x = (Empty) | (* full laziness prefix above *) (* treat the two laziness prefixes above like rule infixes; theorems are not allowed to manipulate them (no preemption of normal program construct behaviour) *) match level hlevel (Variable s) x = if (not(isplusdigits s) andalso minlevel x <= level) then addto(ident(Variable s)) x Empty else if (isplusdigits s) andalso (evalnum10 s) <= level andalso x = Variable s then addto("0")(Constant "0")Empty else Empty | match level hlevel (Infix(x,"|-|",Constant s)) y = if y = (Infix(x,"|-|",Constant s)) then if not(isplusdigits s) then addto("0")(Constant "0")Empty else if evalnum10 s <= hlevel then addto("0")(Constant "0")Empty else Empty else Empty | (* match level hlevel z (Infix(x,"=>",y)) = addto "{maybematch}" (Constant "0") Empty | match level hlevel z (Infix(x,"=>>",y)) = addto "{maybematch}" (Constant "0") Empty | match level hlevel z (Infix(x,"<=",y)) = addto "{maybematch}" (Constant "0") Empty | match level hlevel z (Infix(x,"<<=",y)) = addto "{maybematch}" (Constant "0") Empty | (* where an expression matches something whose eventual form cannot be predicted, report a possible match *) *) match level hlevel (Constant s) (Constant t) = if s = t then addto (ident(Constant s)) (Constant s) Empty else Empty| match level hlevel (Constant s) x = Empty | match level hlevel (ConstantFunction x) (ConstantFunction y) = changelevels (level+1) (level) (hlevel) (hlevel) (match (level+1) hlevel x y) | match level hlevel (ConstantFunction x) y = Empty | match level hlevel (Infix(x,"||",y)) (Infix(u,"||",v)) = consistentwith (match level hlevel x u) (changelevels level level (hlevel+1) (hlevel) (match level (hlevel+1) y v)) | (* limited higher-order matching under construction *) match level hlevel (Infix (Variable x,"@",Variable y)) (Infix(u,s,v)) = if ((not(isplusdigits y)) orelse evalnum10 y <> level orelse (isplusdigits x)) orelse weakstratification (level-1) (level-1) 0 (ConstantFunction(Infix((Infix (Variable x,"@",Variable y)),",",(Infix(u,s,v))))) = [Empty] then if s = "@" then consistentwith(addto "@" (Constant "@") Empty) (consistentwith (match level hlevel (Variable x) u) (match level hlevel (Variable y) v)) else Empty else (* higher order matching situation obtains *) if s = "@" andalso v = Variable y andalso let val U = prechangelevel level (level-1) u in U <> Constant "" andalso minlevel U < level end then consistentwith(addto "@" (Constant "@") Empty) (consistentwith (match level hlevel (Variable x) u) (match level hlevel (Variable y) v)) else changelevels (level-1) level hlevel hlevel (match (level-1) hlevel (prechangelevel level (level-1) (Variable x)) (ConstantFunction(Infix(u,s,v)))) | match level hlevel (Infix (Variable x,"@",Variable y)) z = if (not(isplusdigits y)) orelse evalnum10 y <> level orelse (isplusdigits x) orelse weakstratification (level-1) (level-1) 0 (ConstantFunction(Infix((Infix (Variable x,"@",Variable y)),",",z))) = [Empty] then Empty else (* higher order matching situation obtains *) changelevels (level-1) level hlevel hlevel (match (level-1) hlevel (prechangelevel level (level-1) (Variable x)) (ConstantFunction z)) | match level hlevel (Infix (x,s,y)) (Infix(u,t,v)) = (* enforcement of confluence *) if isruleinfix s orelse (isinfixvar s andalso isruleinfix t) then (Empty) else if israised s andalso israised t then match level hlevel (Infix(x,lowerone s,y)) (Infix(u,lowerone t,v)) else if s = t orelse (isinfixvar s andalso (* supports typed infix variables *) ((not (istypedinfixvar s)) orelse (((not(isinfixvar t)) orelse istypedinfixvar t) andalso Lefttype s = Lefttype t andalso Righttype s = Righttype t andalso (not (foundin t (!OPAQUE)))))) (* an opaque infix is regarded as not matching a typed infix variable of any type *) then consistentwith (addto s (Constant t) Empty) (consistentwith (match level hlevel x u) (match level hlevel y v)) else Empty | match level hlevel (Infix (x,s,y)) z = Empty; (* this match function does not enforce confluence restrictions *) (* the use of this function will be more questionable if it is decided that embedded theorem texts themselves will be executed; textmatch is being used to allow reference to tactics by matchthm, usefulness of which is open to question. The inconvenience to users of "upto" commands of confluence restrictions on matching is much smaller and might be acceptable *) fun textmatch level hlevel x (Infix(z,"#",y)) = textmatch level hlevel x y | (* textmatch level hlevel (Infix(z,"#",x)) y = (Empty) | *) (* prefix above forms inert forms of "active" infixes *) textmatch level hlevel x (Infix(z,"##",y)) = textmatch level hlevel x y | (* textmatch level hlevel (Infix(z,"##",y)) x = (Empty) | *) (* full laziness prefix above *) (* treat the two laziness prefixes above like rule infixes; theorems are not allowed to manipulate them (no preemption of normal program construct behaviour) *) textmatch level hlevel (Variable s) x = if (not(isplusdigits s) andalso minlevel x <= level) then addto(ident(Variable s)) x Empty else if (isplusdigits s) andalso (evalnum10 s) <= level andalso x = Variable s then addto("0")(Constant "0")Empty else Empty | textmatch level hlevel (Infix(x,"|-|",Constant s)) y = if y = (Infix(x,"|-|",Constant s)) then if not(isplusdigits s) then addto("0")(Constant "0")Empty else if evalnum10 s <= hlevel then addto("0")(Constant "0")Empty else Empty else Empty | (* textmatch level hlevel z (Infix(x,"=>",y)) = addto "{maybematch}" (Constant "0") Empty | textmatch level hlevel z (Infix(x,"=>>",y)) = addto "{maybematch}" (Constant "0") Empty | textmatch level hlevel z (Infix(x,"<=",y)) = addto "{maybematch}" (Constant "0") Empty | textmatch level hlevel z (Infix(x,"<<=",y)) = addto "{maybematch}" (Constant "0") Empty | (* where an expression matches something whose eventual form cannot be predicted, report a possible match *) *) textmatch level hlevel (Constant s) (Constant t) = if s = t then addto (ident(Constant s)) (Constant s) Empty else Empty| textmatch level hlevel (Constant s) x = Empty | textmatch level hlevel (ConstantFunction x) (ConstantFunction y) = changelevels (level+1) (level) (hlevel) (hlevel) (textmatch (level+1) hlevel x y) | textmatch level hlevel (ConstantFunction x) y = Empty | textmatch level hlevel (Infix(x,"||",y)) (Infix(u,"||",v))= consistentwith (textmatch level hlevel x u) (changelevels level level (hlevel+1) (hlevel) (textmatch level (hlevel+1) y v)) | (* limited higher-order matching under construction *) textmatch level hlevel (Infix (Variable x,"@",Variable y)) (Infix(u,s,v)) = if ((not(isplusdigits y)) orelse evalnum10 y <> level orelse (isplusdigits x)) orelse weakstratification (level-1) (level-1) 0 (ConstantFunction(Infix((Infix (Variable x,"@",Variable y)),",",(Infix(u,s,v))))) = [Empty] then if s = "@" then consistentwith(addto "@" (Constant "@") Empty) (consistentwith (textmatch level hlevel (Variable x) u) (textmatch level hlevel (Variable y) v)) else Empty else (* higher order matching situation obtains *) if s = "@" andalso v = Variable y andalso let val U = prechangelevel level (level-1) u in U <> Constant"" andalso minlevel U < level end then consistentwith(addto "@" (Constant "@") Empty) (consistentwith (textmatch level hlevel (Variable x) u) (textmatch level hlevel (Variable y) v)) else changelevels (level-1) level hlevel hlevel (textmatch (level-1) hlevel (prechangelevel level (level-1) (Variable x)) (ConstantFunction(Infix(u,s,v)))) | textmatch level hlevel (Infix (Variable x,"@",Variable y)) z = if (not(isplusdigits y)) orelse evalnum10 y <> level orelse (isplusdigits x) orelse weakstratification (level-1) (level-1) 0 (ConstantFunction(Infix((Infix (Variable x,"@",Variable y)),",",z))) = [Empty] then Empty else (* higher order matching situation obtains *) changelevels (level-1) level hlevel hlevel (textmatch (level-1) hlevel (prechangelevel level (level-1) (Variable x)) (ConstantFunction z)) | (* limited higher-order matching under construction--saved earlier version *) (* BEGIN textmatch level hlevel (Infix (Variable x,"@",Variable y)) (Infix(u,s,v)) = if ((not(isplusdigits y)) orelse evalnum10 y <> level) then if s = "@" then consistentwith(addto "@" (Constant "@") Empty) (consistentwith (textmatch level hlevel (Variable x) u) (textmatch level hlevel (Variable y) v)) else Empty else (* higher order matching situation obtains *) if s = "@" andalso v = Variable y andalso let val U = prechangelevel level (level-1) u in U <> Constant"" andalso minlevel U < level end then consistentwith(addto "@" (Constant "@") Empty) (consistentwith (textmatch level hlevel (Variable x) u) (textmatch level hlevel (Variable y) v)) else textmatch level hlevel (Variable x) (prechangelevel (level-1) (level) (ConstantFunction(Infix(u,s,v)))) | textmatch level hlevel (Infix (Variable x,"@",Variable y)) z = if (not(isplusdigits y)) orelse evalnum10 y <> level then Empty else (* higher order matching situation obtains *) textmatch level hlevel (Variable x) (prechangelevel (level-1) (level) (ConstantFunction z)) | END *) textmatch level hlevel (Infix (x,s,y)) (Infix(u,t,v)) = (* (* enforcement of confluence *) if isruleinfix s orelse (isinfixvar s andalso isruleinfix t) then (Empty) else *) (*disabled*) if israised s andalso israised t then textmatch level hlevel (Infix(x,lowerone s,y)) (Infix(u,lowerone t,v)) else if s = t orelse (isinfixvar s andalso (* supports typed infix variables *) ((not (istypedinfixvar s)) orelse (((not(isinfixvar t)) orelse istypedinfixvar t) andalso Lefttype s = Lefttype t andalso Righttype s = Righttype t andalso (not (foundin t (!OPAQUE)))))) then consistentwith (addto s (Constant t) Empty) (consistentwith (textmatch level hlevel x u) (textmatch level hlevel y v)) else Empty | textmatch level hlevel (Infix (x,s,y)) z = Empty; (* this matching function allows matching for constants and requires *) (* precise matching of variables with variables *) (* It is used in theorem export *) (* by allowing a slightly more general form of matching for variables, could export to subdomains of theories *) (* supermatch does not need to take level into account *) fun supermatch (Constant s) (Constant t) = (* force built-in notions to match themselves *) if (isdigits s orelse isbuiltinthm s) andalso s<>t then Empty else onepair(ident(Constant s),Constant t) | supermatch (Constant s) x = Empty | supermatch (Variable s) (Variable t) = if isplusdigits s andalso s<>t then Empty else onepair(ident(Variable s),Variable t) | supermatch (Variable s) x = Empty | supermatch (ConstantFunction x) (ConstantFunction y) = supermatch x y | supermatch (ConstantFunction x) y = Empty | supermatch (Infix (x,s,y)) (Infix(u,t,v)) = (* force built-in notions to match themselves *) if (arithop s orelse isbuiltinthm s orelse isruleinfix s) andalso s<>t then Empty else if israised s andalso israised t then supermatch (Infix(x,lowerone s,y)) (Infix(u,lowerone t,v)) else if (isinfixvar s andalso isinfixvar t) orelse ((not(isinfixvar s)) andalso (not(isinfixvar t))) (* make sure that infix variables are matched only by infix variables! *) then consistentwith (onepair(s,Constant t)) (consistentwith (supermatch x u) (supermatch y v)) else Empty | supermatch (Infix (x,s,y)) z = Empty; (* strip variables and empty strings out of matching lists *) (* used by listmatch below *) fun stripvars Empty = Empty | stripvars (Fork(n,(s,t),Empty,Empty)) = if s = "" orelse isvariable s orelse isinfixvar s then onepair( nameofgenericvariable ,genericvariable) else listtotree([(s,t), ( nameofgenericvariable ,genericvariable)]) | stripvars (Fork(n,(s,t),L,M)) = if s = "" orelse isvariable s (* orelse isinfixvar s *) then (mergewith(stripvars L)(stripvars M)) else addto (s)(t)(mergewith(stripvars L)(stripvars M)); (* Substitution and theorem application operations *) (* implements substitutions using matching functions generated by match *) (* the basic substitution function *) (* sourcelevel is the level of terms in the matching list *) (* fun maybematch L = foundin "{maybematch}" L; (* checks for incomplete matches *) *) (* levelvar and fixnewvars are used to introduce "new" variables at appropriate levels *) (* fun levelvar L N = if L <= 0 then Variable N else Infix(levelvar (L-1) N,"@", Variable (makestring L)); *) fun levelvar L N = if L <= 0 then Variable N else Infix(Variable N,"@", Variable(makestring L)); (* the variable THETERM and the consistentlevel function support the facility for introducing new variables with consistent level in the form ?x_m@?n (depending on local level); variables with inconsistent level are treated as top-level free variables *) val THETERM = ref (Variable "x"); fun consistentlevel N (Constant s) = ~2 | consistentlevel N (Variable s) = if s = N then 0 else ~2 | consistentlevel N (ConstantFunction t) = (consistentlevel N t) + 1 | consistentlevel N (Parenthesis t) = (consistentlevel N t) | consistentlevel N (Infix(x,s,y)) = if consistentlevel N x = ~2 then consistentlevel N y else if consistentlevel N y = ~2 then consistentlevel N x else if consistentlevel N x = consistentlevel N y then consistentlevel N x else ~1; fun fixnewvar p L (Parenthesis (Variable N)) = if p = "" orelse consistentlevel N (!THETERM) = ~1 then Variable N else levelvar L N | fixnewvar p L x = x; fun subs sourcelevel level sourcehlevel hlevel p L (Constant s) = Constant s | subs sourcelevel level sourcehlevel hlevel p L (Variable s) = if isplusdigits s then Variable s else fixnewvar p level ( changelevel sourcelevel level sourcehlevel hlevel (safefind (Parenthesis(Variable(s^(if p = "" then "" else "_")^p))) (ident(Variable s)) L)) | subs sourcelevel level sourcehlevel hlevel p L (ConstantFunction x) = ConstantFunction(subs sourcelevel (level+1) sourcehlevel hlevel p L x) | subs sourcelevel level sourcehlevel hlevel p L (Infix(x,"||",y)) = (Infix(subs sourcelevel level sourcehlevel (hlevel) p L x ,"||",(subs sourcelevel level sourcehlevel (hlevel+1) p L y))) | (* limited higher order matching under construction *) subs sourcelevel level sourcehlevel hlevel p L (Infix(Variable x,"@",Variable y)) = if (not (isplusdigits y)) orelse evalnum10 y <> level orelse (isplusdigits x) then Infix(subs sourcelevel level sourcehlevel hlevel p L (Variable x),"@", subs sourcelevel level sourcehlevel hlevel p L (Variable y)) else let val F = prechangelevel (level-1) level (subs sourcelevel (level-1) sourcehlevel hlevel p L (Variable x)) in if isbinder F andalso let val U = prechangelevel level (level-1) F in U <> Constant "" andalso minlevel U < level end then unbind(changelevel level (level-1) hlevel hlevel (F)) else (Infix(F,"@",subs sourcelevel level sourcehlevel hlevel p L (Variable y))) end | subs sourcelevel level sourcehlevel hlevel p L (Infix(x,s,y)) = Infix(subs sourcelevel level sourcehlevel hlevel p L x, if israised s then (fn(Infix(x,s,y))=>raiseone s) (subs sourcelevel level sourcehlevel hlevel p L (Infix(x,lowerone s,y))) else ident(safefind (Constant s) s L) ,subs sourcelevel level sourcehlevel hlevel p L y); (* apply a theorem (given as a triple format/left side/right side) to a term; arguments are the "theorem", the current format, and the term to which the theorem is to be applied *) fun USE level hlevel (fm,t,u) fm2 v = let val MATCH = consistentwith (match level hlevel (changelevel 0 level 0 hlevel t) v) (match level hlevel (changelevel 0 level 0 hlevel fm) fm2) in if MATCH = Empty (* orelse maybematch (MATCH) *) then v else (THETERM:=u; subs level level hlevel hlevel (newcounter()) MATCH (changelevel 0 level 0 hlevel u)) end; (* utility supporting the new built-in theorem UNEVAL *) (* preunbind will convert a term to the form ?f@?t, given the function ?f (a lambda-term) if possible *) fun preunbind level hlevel (ConstantFunction x) y = let val new_variable = (Variable ("x_"^(newcounter()))) in let val TERM = prebeta level new_variable x in let val TEMP_MATCH = match level hlevel TERM y in if TEMP_MATCH = Empty orelse subs level level hlevel hlevel "" TEMP_MATCH (ConstantFunction x) <> ConstantFunction x then y else Infix(ConstantFunction x,"@", safefind new_variable (ident(new_variable)) TEMP_MATCH) end end end | preunbind level hlevel x y = y; (* checks for undeclared constants; also checks for meaningless bound variables and failures of weak stratification *) fun constantsOK level hlevel t = constantcheck (!CONSTANTS) t andalso minlevel t <= level andalso minhlevel t <= hlevel andalso weakstratification level level 0 t <> [Empty]; fun constantclean level hlevel t = if constantsOK 0 0 t then t else if weakstratification level level 0 t <> [Empty] andalso minlevel t <= level andalso minhlevel t <= level then (errormessage "Undeclared constants or embedded theorems present";t) else (errormessage "Meaningless bound variable or unstratified abstraction error";t); (* USER COMMAND *) (* add declarations to comments *) fun newcomment s c = if isaconstant s then (CONSTANTS:=addcomment s (Lefttype s) (Righttype s) (commentcode c) (!CONSTANTS)) else errormessage "No such declaration to comment"; posthelp "newcomment" "newcomment s c; causes c to become the comment text\nfor the operator or constant s"; fun appendcomment s c = newcomment s ((Commentof s)^"\n\n"^c); posthelp "appendcomment" "appendcomment s c; causes c to be appended to the comment text\nfor the operator or constant s"; (* USER COMMAND *) (* declare a constant *) fun declareconstant s = if not(s = "") andalso isident s andalso not(isvariable s) andalso isnotaconstant s then (CONSTANTS := addto s trivtypes (!CONSTANTS)) else errormessage ("Illegal or repeated constant declaration of "^s); posthelp "declareconstant" "declareconstant s; causes s, a string of alphanumerics with some nondigit,\nto be declared as a constant"; (* USER COMMAND *) (* declare an infix; use declareprefix to declare as unary as well *) (* m and n are relative type differentials of arguments from term *) (* for purposes of stratification *) (* type declarations of infix variables _are_ permitted (to set relative types for purposes of stratification *) fun declaretypedinfix m n s = if (isinfix s) andalso (not(israised s)) andalso isnotaconstant s andalso (not (isinfixvar s) orelse not(isopaque s)) (* last clause blocks redeclaration of explicitly untyped infix variables as typed *) then (CONSTANTS := addtypes s m n (!CONSTANTS)) else errormessage ("Illegal or repeated infix declaration of "^s); posthelp "declaretypedinfix" "declaretypedinfix m n s; causes s, a string of special characters,\nto be declared as an operator with left and right arguments\nof integer types m, n respectively."; (* USER COMMANDS (3) *) (* declare infix with no type differentials *) fun declareinfix s = declaretypedinfix 0 0 s; posthelp "declareinfix" "declareinfix s; declares s, a string of special characters,\nas an operator with left and right arguments of the same type as the term."; (* declare prefix with no relative type differentials *) fun declareunary s = (declareinfix s; declareprefix s "defaultprefix"); posthelp "declareunary" "declareunary s; causes the operator s to be declared and to be assigned\ndefault left argument `defaultprefix'\n so that it can be used as a prefix operator"; fun makeunary s = declareprefix s "defaultprefix"; posthelp "makeunary" "makeunary s; allows the operator s (already declared)\nto be used as a prefix operator with the default left argument `defaultprefix'"; (* modified so that a constant previously not opaque cannot be made opaque; makeopaque (the old declareopaque) is not a user command *) fun declareopaque s = if isinfix s then if isaconstant s then errormessage "Name already in use" else if isinfixvar s then makeopaque s else (declareinfix s; makeopaque s) else errormessage "Not an infix"; posthelp "declareopaque" "declareopaque s; causes the operator s to be declared\nas an opaque operator (meaning that no abstraction is allowed into its scope)"; (* it is permissible to remove an opacity restriction *) fun declarenotopaque s = if isinfix s andalso isaconstant s andalso isopaque s then OPAQUE := dropitem s (!OPAQUE) else errormessage "Illegal opacity declaration"; posthelp "declarenotopaque" "declarenotopaque s; removes opacity restrictions from operator s"; (* USER COMMAND *) (* display an infix or object declaration *) fun showdec s = if isaconstant s then if isdigits s then errormessage "Constant is a numeral" else output (std_out,s ^" "^(makestring (Lefttype s)) ^" "^(makestring(Righttype s))^" "^(prefixval s)^" "^ (if isopaque s then "opaque" else "")^ "\n"^(Commentof s)^"\n") else if isinfix s andalso isopaque s then errormessage "Opaque infix variable" else errormessage "Constant not found"; posthelp "showdec" "showdec s; displays the declaration of the constant or operator s,\nif there is such"; (* probably opaque infix variables should also appear on the declaration list *) (* tools for building "showall" below *) exception Quit; (* used for bailing out of loops originally broken with Control-C *) fun always x = true; fun preshowall test viewer Empty = () | preshowall test viewer (Fork(n,(s,x),L,M)) = (preshowall test viewer L; if not(test s) then preshowall test viewer M else (viewer s; if input(std_in,1) = "\n" then preshowall test viewer M else raise Quit)); (* all-purpose command for displaying tree contents; test indicates which items are to be displayed, viewer indicates how they are to be viewed, target is a reference to the target tree *) fun showall test viewer target = (preshowall test viewer (!target)) handle Quit => (); (* USER COMMAND *) (* scan declarations interactively *) fun scandecs() = scan showdec CONSTANTS; posthelp "scandecs" "scandecs(); allows one to browse in the declarations list.\nUse to look, l to go left, r to go right, q to quit."; (* USER COMMAND *) (* Show all declarations *) fun showalldecs () = showall always showdec CONSTANTS; posthelp "showalldecs" "showalldecs() shows all declarations.\n for next entry, q to quit."; (* Some constant declarations *) fun preamble1 () = ( (* declareinfix "><"; (* hides subterms from display *) *) declaretypedinfix 1 0 "@"; (* function application *) declaretypedinfix 1 1 "!"; (* "Hilbert symbol" *) declareinfix ","; (* pairing or cons *) declareinfix ":"; (* type retraction infix *) declareinfix "=>"; (* direct theorem application *) declareinfix "<="; (* converse theorem application *) declareinfix "=>>"; (* embedded theorem application for lists *) (* of alternatives *) declareinfix "<<="; (* declareinfix "*>"; (* on-success connectives *) declareinfix "<*"; declareunary "!!"; (* "inline" operator *) *) declareprefix "!!" "defaultprefix"; declareprefix "|-|" "defaultprefix"; declareinfix "//"; (* throws away first argument; used for theorem *) (* parameters *) declareinfix "+!"; (* built-in unsigned integer arithmetic operations *) declareinfix "*!"; declareinfix "-!"; declareinfix " th2 andalso isatheorem th1 andalso isatheorem th2 andalso not(isbuiltinthm th1) andalso not(isbuiltinthm th2) andalso not(isanaxiom th1) andalso not(isanaxiom th2) then (clearcache(); THEOREMS:= dropitem th1 (addto th2 (Thm(Formatof th2,Leftside th2,Rightside th2,Deps th2, addto th1 (safetheorem th1) (Moduleof th2))) (!THEOREMS)); appendcomment th1 ("Pushed into module "^th2)) else errormessage "Unknown or inappropriate theorem(s)"; posthelp "pushtheorem" "pushtheorem th1 th2; `pushes' theorem th1\ninto the module associated with theorem th2"; fun poptheorem th1 th2 = if isatheorem th2 andalso not(isbuiltinthm th2) andalso foundin th1 (Moduleof th2) then (clearcache(); THEOREMS := addto th1 (hd(find th1 (Moduleof th2))) (addto th2 (Thm(Formatof th2,Leftside th2,Rightside th2,Deps th2, dropitem th1 (Moduleof th2))) (!THEOREMS)); appendcomment th1 ("Popped from module "^th2)) else errormessage "Unknown theorem(s)"; posthelp "poptheorem" "poptheorem th1 th2; `pops' theorem th1\nrom the module associated with theorem th2"; (* versions of pushtheorem and poptheorem which don't post comments *) fun pushtheorem2 th1 th2 = if th1 <> th2 andalso isatheorem th1 andalso isatheorem th2 andalso not(isbuiltinthm th1) andalso not(isbuiltinthm th2) andalso not(isanaxiom th1) andalso not(isanaxiom th2) then (clearcache(); THEOREMS:= dropitem th1 (addto th2 (Thm(Formatof th2,Leftside th2,Rightside th2,Deps th2, addto th1 (safetheorem th1) (Moduleof th2))) (!THEOREMS))) else errormessage "Unknown or inappropriate theorem(s)"; fun poptheorem2 th1 th2 = if isatheorem th2 andalso not(isbuiltinthm th2) andalso foundin th1 (Moduleof th2) then (clearcache(); THEOREMS := addto th1 (hd(find th1 (Moduleof th2))) (addto th2 (Thm(Formatof th2,Leftside th2,Rightside th2,Deps th2, dropitem th1 (Moduleof th2))) (!THEOREMS))) else errormessage "Unknown theorem(s)"; (* add,drop pretheorem to/from that list *) fun addapretheorem s = (PRETHEOREMS := (addtoset s (!PRETHEOREMS)) ); fun dropapretheorem s = PRETHEOREMS := drop s (!PRETHEOREMS); (* add/drop definitions from their list *) fun addadefinition s t = (DEFINITIONS := addto s t (!DEFINITIONS)); fun dropadefinition s = (DEFINITIONS := dropitem s (!DEFINITIONS)); (* apply a function to the master theorem list *) fun changetheorems f = (clearcache(); THEOREMS := f(!THEOREMS)); (* drop a theorem from the master list *) fun dropatheorem s = changetheorems (dropitem s); fun weakdropatheorem s = THEOREMS:=dropitem s (!THEOREMS); (* Functions acting on the master theorem list *) (* Theorem display operations *) (* USER COMMAND *) (* display a single theorem with dependencies *) fun thmdisplay s = if (!QUIET)=0 then () else (clearcache(); if isnotatheorem s then errormessage "Theorem not found" else if (isbuiltinthm s) then errormessage "Built-in operation" else ( output(std_out,(bddisplay(Formatof s))^":\n\n"^(bddisplay( Leftside s))^" = \n\n"^(bddisplay( Rightside s))^ "\n\n"^(liststring(treetolabellist(Deps s)))^ (if Moduleof s = Empty then "" else "\nmodule components:\n"^ (showsettable (Moduleof s)))^"\n"^ (Commentof s)^"\n"))); posthelp "thmdisplay" "thmdisplay th; shows the theorem named th, if any"; (* USER COMMAND *) (* displays all modules associated with a theorem *) fun moddisplay s = (thmdisplay s; if (Moduleof s) <> Empty then output(std_out, "\nIn module "^s^":\n\n") else (); dofor (fn th => (poptheorem2 th s; moddisplay th; pushtheorem2 th s)) (Moduleof s)); posthelp "moddisplay" "moddisplay th; shows a theorem and all associated modules."; (* USER COMMANDS (2) *) (* view definitions *) fun seedef s = if isdefined s then thmdisplay (definitionof s) else errormessage "No definition found"; posthelp "seedef" "seedef s; displays the definition of constant or operator s (if any)"; fun seealldefs() = showall isdefined seedef CONSTANTS; posthelp "seealldefs" "seealldefs(); shows all definitions.\n for next item, q to quit."; fun scandefs() = scan seedef DEFINITIONS; posthelp "scandefs" "scandefs(); allows one to browse the definitions list.\n to look, l to go left, r to go right, q to quit."; (* USER COMMAND *) (* look at the program bound to a constant or infix *) fun seeprogram s = if hasnoprogram s then errormessage "Program not found" else thmdisplay (Programof s); posthelp "seeprogram" "seeprogram s; displays tactic (functional program)\nto be applied wherever constant or operator s is seen, if there is one."; (* USER COMMANDS (2) *) (* look at all programs *) fun seeallprograms () = showall always seeprogram PROGRAMS; posthelp "seeallprograms" "seeallprograms(); allows one to browse the functional\nprogram list. to look, l to go left, r to go right, q to quit."; fun scanprograms () = scan seeprogram PROGRAMS; posthelp "scanprograms" "scanprograms(); allows one to browse the functional programs list.\n to look, l to go left, r to go right, q to quit."; (* USER COMMANDS *) (* display all theorems, modules, axioms *) fun showalltheorems() = showall always thmdisplay THEOREMS; posthelp "showalltheorems" "showalltheorems(); displays all theorems.\n to see next item, q to quit."; fun showallmodules() = showall always moddisplay THEOREMS; posthelp "showallmodules" "showallmodules(); displays all modules.\n to see next item, q to quit."; fun showallaxioms() = showall isanaxiom thmdisplay THEOREMS; posthelp "showallaxioms" "showallaxioms(); displays all axioms and definitions.\n to see next item, q to quit."; fun scantheorems() = scan thmdisplay THEOREMS; posthelp "scantheorems" "scantheorems(); allows one to browse the theorem list.\n to look, l to go left, r to go right, q to quit"; fun scanmodules() = scan moddisplay THEOREMS; posthelp "scanmodules" "scanmodules(); allows one to browse the theorem list, displaying contents of all modules\n to look, l to go left, r to go right, q to quit"; (* find a theorem which can justify a given equation *) fun prematchthm level hlevel x Empty = Constant "" | prematchthm level hlevel (Infix(x,"=",y)) (Fork(n,(s,th),L,M)) = if hd(explode s) = "}" (* avoid saved environments *) orelse textmatch level hlevel (changelevel 0 level 0 hlevel (Infix(Leftside s,"=",Rightside s))) (Infix(x,"=",y)) = Empty then if prematchthm level hlevel (Infix(x,"=",y)) L = Constant "" then if prematchthm level hlevel (Infix(x,"=",y)) M = Constant "" then (Constant "") else prematchthm level hlevel (Infix(x,"=",y)) M else prematchthm level hlevel (Infix(x,"=",y)) L else subs level level hlevel hlevel "" (textmatch level hlevel (changelevel 0 level 0 hlevel (Infix(Leftside s,"=",Rightside s))) (Infix(x,"=",y))) (Formatof s) | prematchthm level hlevel x y = (errormessage "Not an equation!";Constant ""); fun matchthm level hlevel x = let val mightbe = prematchthm level hlevel (parse x) (!EXCACHE) in if mightbe <> Constant "" then mightbe else prematchthm level hlevel (parse x) (!THEOREMS) end; fun termmatchthm level hlevel x = let val mightbe = prematchthm level hlevel (x) (!EXCACHE) in if mightbe <> Constant "" then mightbe else prematchthm level hlevel (x) (!THEOREMS) end; (* USER COMMAND *) (* will display theorem which matches a given equation (with parameters if needed) *) fun showmatchthm x = (clearcache();if matchthm 0 0 x = Constant "" then errormessage "No such theorem" else (errormessage (nicedisplay(matchthm 0 0 x)); thmdisplay (eitherhead(matchthm 0 0 x)))); posthelp "showmatchthm" "showmatchthm x; will find and display a theorem\nwhich justifies the equation x, if there is one."; (* USER COMMAND *) (* Axiom construction command -- first argument is name, second and third *) (* are the two sides of the equation *) fun axiom s x y = if isident s andalso constantsOK 0 0 (parse x) andalso constantsOK 0 0 (parse y) andalso isnotaconstant s then (addtheorem s (Constant s) (parse x) (parse y) (singleton s); declareconstant s;thmdisplay s) else errormessage "Illegal theorem declaration"; posthelp "axiom" "axiom s x y; will make `x = y' an axiom and name it s."; (* Functions for global dependency modifications *) (* fun predepfix s L Empty = Empty | predepfix s L (Fork(n,(label,(fm,t,u,d)),M1,M2)) = (Fork(n,(label,(fm,t,u, if foundin s d then (mergewith L (drop s d)) else d)),(predepfix s L M1), predepfix s L M2)); *) fun predepfix s L Empty = Empty | predepfix s L (Fork(n,(label,(Thm(fm,t,u,d,m))),M1,M2)) = (Fork(n,(label,(Thm(fm,t,u, (if foundin s d then (mergewith L (drop s d)) else d),m))),(predepfix s L M1), predepfix s L M2)); fun depfix s L = changetheorems (predepfix s L); (* USER COMMAND *) (* define object and infix constants. Definitions may be parameterized, *) (* though only in a stratified manner. Infixes/unary operations may be *) (* inhomogeneous or type-raising. *) fun defineconstant T U = let val t = parse T and u = parse U in if definitionformat (t) andalso isnotaconstant (defhead(t)) andalso constantsOK 0 0 (u) (* andalso minlevel t = 0 andalso weakstratification 0 0 0 t <> [Empty] *) andalso sublist (varlist(u)) (varlist(t)) then if stratification 0 (Infix((t),"=",(u))) = [Empty] (* orelse (not(predtest (u))) *) then errormessage "Stratification, opacity or impredicativity error in definition" else (addadefinition (defhead(t)) (defhead(t)); addtheorem (defhead(t)) (Constant(defhead(t))) (t) (u) (singleton(defhead t)); declareconstant(defhead t); thmdisplay (defhead t)) else errormessage "Declaration or syntax error in definition" end; posthelp "defineconstant" "defineconstant T U; will check whether `T=U'\nhas the correct form to be the definition of a constant t\nand, if so, declare t, create `T=U' as a theorem with name t and bound to t\nas its definition."; (* USER COMMAND *) (* the integer parameters m and n are the types of the first and second *) (* arguments of the infix relative to the value of the whole expression *) fun definetypedinfix name m n T U = let val t = parse T and u = parse U in if infixdefinitionformat (t) andalso (not(israised (ix(t)))) andalso isnotaconstant (ix (t)) andalso (not (isinfixvar (ix(t)))) andalso constantsOK 0 0 (u) (* andalso minlevel t = 0 *) andalso sublist (varlist(u)) (varlist (t)) then ( declaretypedinfix m n (ix (t)); if (* weakstratification 0 0 0 t = [Empty] orelse *) stratification 0 (Infix(t,"=",u)) = [Empty] (* orelse (not(predtest (u))) *) then (errormessage "Stratification or opacity error in infix definition"; dropaconstant (ix(t))) else ( (* inserted new mechanism to declare prefixes automatically if no left argument has been supplied -- requires reparsing of left side of definition below *) if constantsOK 0 0 t then () else (errormessage "Warning: automatically declaring default left argument of defined prefix"; declareprefix (ix t) "defaultprefix"); addadefinition (ix(t)) name;(addtheorem name (Constant name) (parse T) u (singleton name));declareconstant name; thmdisplay name)) else errormessage "Declaration or syntax error in infix declaration" end; posthelp "definetypedinfix" "definetypedinfix name m n T U; causes Mark2 to check\nwhether `T=U' has the correct form to be the definition of an operator t\nwith left type m and right type n.\nIf it does, t is declared and a theorem with name `name' is created\nand bound to the operator t as its definition."; (* USER COMMAND *) (* defineinfix defines genuine binary functions *) (* (no funny business with types) *) fun defineinfix name t u = definetypedinfix name 0 0 t u; posthelp "defineinfix" "defineinfix name T U; causes Mark2 to check\nwhether `T=U' has the correct form to be the definition of an operator t\nwith left type and right type 0.\nIf it does, t is declared and a theorem with name `name' is created\nand bound to the operator t as its definition."; (* USER COMMAND *) (* define an opaque infix; avoids stratification restrictions *) fun defineopaque name T U = let val t = parse T and u = parse U in if infixdefinitionformat (t) andalso (not(israised (ix(t)))) andalso isnotaconstant (ix (t)) andalso (not (isinfixvar (ix(t)))) andalso constantsOK 0 0 (u) andalso sublist (varlist(u)) (varlist (t)) then ( declareopaque (ix (t)); (* inserted new mechanism to declare prefixes automatically if no left argument has been supplied -- requires reparsing of left side of definition below *) if constantsOK 0 0 t then () else (errormessage "Warning: automatically declaring default left argument of defined prefix"; declareprefix (ix t) "defaultprefix"); addadefinition (ix(t)) name;(addtheorem name (Constant name) (parse T) u (singleton name));declareconstant name; thmdisplay name) else errormessage "Declaration or syntax error in infix declaration" end; posthelp "defineopaque" "defineopaque name T U; causes Mark2 to check\nwhether `T=U' has the correct form to be the definition of an opaque operator t.\nIf it does, t is declared (opaque) and a theorem with name `name' is created\nand bound to the operator t as its definition."; (* definition restructuring tools -- under construction *) (* the redefineconstant and redefineinfix commands are found below with proveanaxiom, because they depend on the current proof environment *) (* this function produces the set of defined terms upon which a term depends *) (* actually, includes all terms on which a term depends and looks at embedded theorems as well.*) (* predefsin is needed to avoid circularity *) fun predefsin L (Constant s) = if isdefined s then mergewith (singleton s) (predefsin L (Rightside s)) else if isatheorem s andalso not (isbuiltinthm s) andalso (not(foundin s L)) then mergewith (singleton s) (mergewith (predefsin (mergewith (singleton s) L) (Leftside s)) (predefsin (mergewith (singleton s) L) (Rightside s))) else (singleton s) | predefsin L (Variable s) = Empty | predefsin L (ConstantFunction t) = predefsin L t | predefsin L (Infix(x,S,y)) = let val s = deraise S in mergewith (predefsin L x) ( mergewith (predefsin L y) ( if isdefined s then mergewith (singleton s) ( mergewith (singleton (definitionof s)) (predefsin L (Rightside(definitionof s)))) else if isatheorem s andalso not (isbuiltinthm s) andalso not(foundin s L) then mergewith (singleton s) (mergewith (predefsin (mergewith (singleton s) L) (Leftside s)) (predefsin (mergewith (singleton s) L) (Rightside s))) else (singleton s))) end; fun defsin s = (clearcache();predefsin Empty s); (* USER COMMAND *) (* convert a defined notion (constant or infix) to a primitive *) fun undefine T = if isdefined T andalso isanaxiom (definitionof T) then dropadefinition (T) else errormessage "Argument is not defined appropriately"; posthelp "undefine" "undefine T; converts T from a defined notion to a primitive\n(and its erstwhile definition to an axiom)."; (* USER COMMAND *) (* Define an erstwhile primitive notion; argument is the defining theorem *) fun defineprimitive T = (clearcache(); if isnotatheorem T orelse isbuiltinthm T orelse isadefinition T then errormessage "Inappropriate argument" else let val t = Leftside T and u = Rightside T in if definitionformat t andalso not(isdefined (defhead t)) andalso not(foundin (defhead t) (defsin u)) then if stratification 0 (Infix((t),"=",(u))) = [Empty] (* orelse (not(predtest (u))) *) then errormessage "Stratification, opacity or impredicativity error in definition" else (addtheorem (defhead t) (Constant(defhead t)) t u (singleton(defhead t)); addadefinition (defhead t) (defhead t); addtheorem T (Formatof T) (Leftside T) (Rightside T) (singleton(defhead t));thmdisplay T;thmdisplay(defhead t)) else if infixdefinitionformat t andalso not(isdefined(ix t)) andalso not(foundin (ix t) (defsin u)) then if stratification 0 (Infix((t),"=",(u))) = [Empty] (* orelse (not(predtest (u))) *) then errormessage "Stratification, opacity or impredicativity error in definition" else (addtheorem T (Constant T) (t) (u) (singleton T); addadefinition (ix t) T; thmdisplay T) else errormessage "Definition format error" end); posthelp "defineprimitive" "defineprimitive T; determines whether T could be the\ndefinition of a current primitive constant or operator t\nand makes it so if possible."; (* USER COMMAND *) (* Declare any theorem to be an axiom. Useful in reaxiomatization *) fun makeanaxiom s = (clearcache();if isnotatheorem s then errormessage "Not a theorem" else if isadefinition s then errormessage "Not applicable to definitions" else if isbuiltinthm s then errormessage "Not applicable to built-in theorems" else let val (lefts,rights) = (Leftside s,Rightside s) in (dropatheorem s; addtheorem s (Constant s) lefts rights (singleton s)) end); posthelp "makeanaxiom" "makeanaxiom s; makes theorem s an axiom."; (* Functions for the auxiliary theorem types *) (* USER COMMAND *) (* declare a theorem for future recursive definition *) fun declarepretheorem s = if (isident s orelse isinfix s) andalso isnotaconstant s then (addapretheorem s; if isident s then declareconstant s else declareinfix s) else errormessage "Illegal pretheorem declaration"; posthelp "declarepretheorem" "declarepretheorem s; declares that s will be proved as a theorem.\nUsed for developing recursive tactics."; (* USER COMMAND *) (* bind a theorem/program th to a constant s *) (* this theorem will then be automatically applied when *) (* preexecute is invoked, if appropriate current dependencies *) (* are present *) fun proveprogram s th = (clearcache();if isnotatheorem th = false andalso isaconstant s then if isident s then if definitionformat(Leftside(th)) andalso defhead(Leftside(th)) = s andalso hasnoprogram s then PROGRAMS := addto(s)(th)(!PROGRAMS) else errormessage "Theorem is not of right form" else if isinfix s then if infixdefinitionformat (Leftside (th)) andalso ix (Leftside(th)) = s then PROGRAMS := addto(s)(th)(!PROGRAMS) else errormessage "Theorem is not of right form" else errormessage "Impossible error in program declaration" else errormessage "Undeclared object error or program already present"); posthelp "proveprogram" "proveprogram s th; binds the theorem or tactic th\nto the function or operator s to be applied automatically wherever s appears."; (* unbind any programs from constant s *) (* USER COMMAND *) fun deprogram s = if isnotaconstant s then errormessage "Deprogram what???!" else if hasnoprogram s then errormessage "No program to delete or change" else PROGRAMS := (dropitem s (!PROGRAMS)); posthelp "deprogram" "deprogram s; unbinds any programs from function or operator s."; (* Some axioms *) fun preamble2 () = ( (* axiom "HIDE" "?x> (s,safetheorem s))) (find (deraise s) (!DEFINITIONS)))))); (* USER COMMAND -- brutal *) (* eliminate an identifier -- will not handle occurrences embedded in theorems! *) fun clobber s = (deprogram s; declarenotopaque s; dropapretheorem s; dropadefinition s; dropatheorem s; dropaconstant s); (* PROOF ENVIRONMENT MODULE *) (* The type "working environment" *) (* components of the environment *) fun orig (x,y,z,w,u,v,a) = x; (* The expression one starts with *) (* Eventually, the left side of a new theorem *) fun current (x,y,z,w,u,v,a) = y; (* The expression one currently has *) (* Eventually, the right side of a new theorem *) fun position (x,y,z,w,u,v,a) = z; (* a string of booleans representing *) (* the position of the subterm currently under *) (* examination *) fun curdeps (x,y,z,w,u,v,a) = w; (* the current dependencies; axioms used so *) (* far *) fun level (x,y,z,w,u,v,a) = u; (* deBruijn level of current subterm *) fun hlevel (x,y,z,w,u,v,a) = v; (* hypothesis level of current subterm *) fun hlist (x,y,z,w,u,v,a) = a; (* list of positions of hypotheses *) (* new component of environment consisting of local hypotheses will be added, adding the last unimplemented idea from the original conception *) (* the environment itself *) val ENV = ref (genericconstant,genericconstant ,[true],singleton("bogus"),0,0,[(Constant "",[true],0,0)]); ENV := (genericvariable,genericvariable,nil,Empty,0,0,nil); (* the term modification workhorse *) (* exec f applies function f to the subterm of current(!ENV) indicated by *) (* position(!ENV). *) fun exec f = ENV := (orig (!ENV), preexec (position(!ENV)) f (current(!ENV)), position(!ENV),curdeps(!ENV),level(!ENV),hlevel(!ENV), hlist(!ENV)); fun strongexec f = ENV := (orig (!ENV), let val T = preexec (position(!ENV)) f (current(!ENV)) in if weakstratification 0 0 0 T <> [Empty] then T else (errormessage "Introduces stratification error"; current(!ENV)) end, position(!ENV),curdeps(!ENV),level(!ENV),hlevel(!ENV), hlist(!ENV)); (* used to increment or decrement deBruijn level of current subterm *) fun bumplevel n = ENV := (orig(!ENV),current(!ENV),position(!ENV),curdeps(!ENV),level(!ENV)+n, hlevel(!ENV),hlist(!ENV)); (* used to increment or decrement hypothesis level of current subterm *) fun bumphlevel n = ENV := (orig(!ENV),current(!ENV),position(!ENV),curdeps(!ENV),level(!ENV), hlevel(!ENV)+n,hlist(!ENV)); (* function used by up below but also by pophlist; takes last item off position lists *) fun preup nil = (errormessage "At top already";nil) | preup [x] = nil | preup (x::L) = x::preup L; fun lastup nil = nil | lastup [x] = [x] | lastup (x::L) = lastup L; (* functions for hypothesis list management *) fun addtohlist stuff = ENV := (orig(!ENV),current(!ENV),position(!ENV),curdeps(!ENV),level(!ENV), hlevel(!ENV),(hlist(!ENV))@[stuff]); fun prehlistmove (Infix(x,"||",y)) = (addtohlist (x,position(!ENV),level(!ENV),hlevel(!ENV));(Infix(x,"||",y))) | prehlistmove x = x; fun pophlist() = ENV := (orig(!ENV),current(!ENV),position(!ENV),curdeps(!ENV),level(!ENV), hlevel(!ENV),if hlist(!ENV) = nil then nil else preup(hlist(!ENV))); fun nullhlist() = ENV := (orig(!ENV),current(!ENV),position(!ENV),curdeps(!ENV),level(!ENV), hlevel(!ENV),nil); fun zerolevel () = bumplevel (0-(level(!ENV)));; fun zerohlevel () = (bumphlevel (0-(hlevel(!ENV)));nullhlist()); (* list of senses (0 = inactive, 1 = positive, 2 = negative) of hypotheses; this is set using the following sethypsenses command when a tactic interpreter is called, then manipulated dynamically by the tactic interpreter *) val HYPSENSES = ref [0]; fun nextmove M nil = nil | nextmove nil (x::L) = [x] | nextmove (y::M) (x::L) = nextmove M L; val NOTEPAIR = ref true; fun notepair (Infix(x,",",y)) = (NOTEPAIR:=true;Infix(x,",",y)) | notepair x = (NOTEPAIR:=false;x); fun setahypsense (term,pos,level,hlevel) = (preexec (pos@[false]) notepair (current(!ENV)); if (!NOTEPAIR) andalso nextmove (pos@[false]) (position(!ENV)) <> nil then if hd(nextmove (pos@[false]) (position(!ENV))) then 1 else 2 else 0); fun sethypsenses() = HYPSENSES := map setahypsense (hlist(!ENV)); fun iteminlist n (x::L) = if n = 1 then x else iteminlist (n-1) L; (* viewing functions *) (* USER COMMAND *) (* shows the whole current term, then the specified subterm *) fun look() = (exec(fn x => Parenthesis x);lookat(current(!ENV)); exec(fn (Parenthesis x) => x);exec lookat); posthelp "look" "look(); shows the whole current term above the current subterm"; (* USER COMMAND *) (* set line length *) fun setline (n:int) = (LINE := n;look()); posthelp "setline" "setline n; sets current line length to n"; (* USER COMMANDS (2) *) (* set display depth (negative values give full display) *) fun setdepth n = (DEPTH := n;look()); posthelp "setdepth" "setdepth n; sets display depth to n;\nnegative values give full display."; fun nodepth () = setdepth ~1; posthelp "nodepth" "nodepth(); removes any bound on display depth."; (* USER COMMAND *) (* shows just the current term *) (* USER COMMAND *) fun lookhere() = exec lookat; posthelp "lookhere" "lookhere(); shows just the current subterm."; (* shows the original term *) (* USER COMMAND *) fun lookback() = (lookat(orig(!ENV));()); posthelp "lookback" "lookback(); shows the original term entered\n(as possibly modified by assignments)."; (* USER COMMAND *) fun lookhyp n = if n >= 0 andalso length (hlist(!ENV)) >= n then ((fn (x,y,z,w) => lookat( changelevel z (level(!ENV)) w (hlevel(!ENV)) x)) (iteminlist n (hlist(!ENV))); ()) else errormessage "No such hypothesis"; posthelp "lookhyp" "lookhyp n; displays local hypothesis n."; fun prelookhyps n = if n <= 0 then () else (output(std_out,(makestring (hlevel(!ENV)-n+1))^" ("^ (let val SENSE = iteminlist (hlevel(!ENV)-n+1) (!HYPSENSES) in if SENSE = 1 then "positive" else if SENSE = 2 then "negative" else "inactive" end) ^"):"); lookhyp (hlevel(!ENV)-n+1); output(std_out,"\n"); prelookhyps (n-1)); (* slookhyps doesn't disturb hypsenses under tactic interpreter *) fun slookhyps() = prelookhyps (hlevel(!ENV)); (* USER COMMAND *) fun lookhyps() = (sethypsenses();slookhyps()); posthelp "lookhyps" "lookhyps(); shows all local hypotheses\n(conditions defining case expressions which enable rewrite rules in current context)."; (* System for initializing, saving and retrieving environments *) (* term naming the current environment; is used as the default name of the theorem to be proved *) val CURRENTTHEOREM = ref (Constant "backup"); (* USER COMMAND *) (* reports proof environment name *) fun envname() = errormessage (nicedisplay(!CURRENTTHEOREM)); posthelp "envname" "envname(); reports name of current environment."; (* the list of saved environments *) val ENVS = ref(listtotree([("bogus",(!ENV))])); ENVS := Empty; (* function for removing inappropriate dependencies on definitions *) (* This function is invoked automatically by all commands which add theorems or saved environments to the master theorem list *) fun preremovedefdeps Empty = Empty | preremovedefdeps (Fork(n,(s,t), L, M)) = mergewith(if not(isadefinition s) orelse foundin s (defsin(Infix(orig(!ENV),"=",current(!ENV)))) then (singleton s) else Empty) (mergewith(preremovedefdeps L)(preremovedefdeps M)); fun removedefdeps() = clearcache(); (* (clearcache();ENV:= (orig(!ENV),current(!ENV),position(!ENV), preremovedefdeps(curdeps(!ENV)),level(!ENV),hlevel(!ENV),hlist(!ENV))); *) fun reallyremovedefdeps() = (clearcache();ENV:= (orig(!ENV),current(!ENV),position(!ENV), preremovedefdeps(curdeps(!ENV)),level(!ENV), hlevel(!ENV),hlist(!ENV))); (* tools for changing current dependencies *) fun preadddeps L (x,y,z,u,v,w,a) = (x,y,z,mergewith(L)(u),v,w,a); fun predropdep s (x,y,z,u,v,w,a) = (x,y,z,drop s u,v,w,a); fun adddeps L = ENV := preadddeps L (!ENV); fun dropdep s = ENV := predropdep s (!ENV); (* functions that get dependencies due to stratification subversion *) fun clearscinscoutdeps() = SCINSCOUTDEPS := Empty; fun getscinscoutdeps() = (adddeps (!SCINSCOUTDEPS);SCINSCOUTDEPS:=Empty); (* USER COMMANDS (2) *) (* commands for saving working environment, with and without a *) (* user-supplied tag *) (* to prevent dependency corruption, theorems are saved to the master theorem list with unparsable names, so that global dependency fixes will act on them *) fun saveenv S = let val s = eitherhead (parse S) in if s<>"" andalso constantsOK 0 0 (orig(!ENV)) andalso constantsOK 0 0 (current(!ENV)) then (getscinscoutdeps(); (ENVS := addto(s)(!ENV)(dropitem s (!ENVS)); dropatheorem ("}"^s); addtheorem ("}"^s) (parse("saved_environment:"^S)) (orig(!ENV)) (current(!ENV)) (curdeps(!ENV)); CURRENTTHEOREM:=(parse S))) else errormessage "Bad environment name or corrupt environment" end; posthelp "saveenv" "saveenv S; saves current environment on desktop with format S\n(and implied name)."; fun backupenv() = saveenv (nicedisplay (!CURRENTTHEOREM)); posthelp "backupenv" "backupenv(); backs up current environment with name `backup';\noften invoked automatically by other commands."; (* term starting functions *) (* USER COMMAND *) (* set up a "clean slate"; s is the original and current term, *) (* everything else is default *) fun start s = (backupenv(); ENV := (constantclean 0 0 (parse s),parse s,nil,Empty,0,0,nil); CURRENTTHEOREM := Constant "backup";look()); posthelp "start" "start s; starts a new environment with term s"; (* version of start which sets the intended theorem *) fun startfor th s = (start s;CURRENTTHEOREM := (parse th)); posthelp "startfor" "startfor th s; starts a new environment with term s and name th"; fun prestartover (x,y,z,u,v,w,a) = (x,x,nil,Empty,0,0,nil); (* USER COMMAND *) (* go back to original term *) fun startover () = (backupenv();ENV := prestartover (!ENV);look()); posthelp "startover" "startover(); restarts current environment at original term"; (* reverse roles of original and current terms *) fun preworkback (x,y,z,u,v,w,a) = (y,x,nil,u,0,0,nil); (* set original term to be current term and clean slate *) fun prestarthere (x,y,z,u,v,w,a) = (y,y,nil,Empty,0,0,nil); (* USER COMMAND *) fun workback() = (backupenv();ENV := preworkback (!ENV);look()); posthelp "workback" "workback(); interchanges roles of current and original terms"; (* USER COMMAND *) fun starthere () = (backupenv();ENV := prestarthere (!ENV);look()); posthelp "starthere" "starthere() starts a new environment with the current term as original term."; (* term starting functions using theorems *) (* useful in combination with "reprove" function for editing programs *) (* USER COMMAND *) fun getleftside s = (backupenv(); clearcache(); ENV := (Leftside s,Leftside s,nil,Empty,0,0,nil); CURRENTTHEOREM := (Formatof s); backupenv();look()); posthelp "getleftside" "getleftside s; star