# HG changeset patch # User paulson # Date 1126280857 -7200 # Node ID 3f12de2e2e6e6ddcb00a07fc8abb8e31e85475ea # Parent fc7cc8137b97ea31a402cbfe8974cfce3fcb4cba Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying diff -r fc7cc8137b97 -r 3f12de2e2e6e src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Sep 09 12:18:15 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Sep 09 17:47:37 2005 +0200 @@ -172,8 +172,7 @@ (***********************************************) val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums - val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls - + val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) (concat clasimp_names) val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode)) @@ -541,37 +540,22 @@ (* then show for the last step *) (* replace ~ by not here *) -fun change_nots [] = [] -| change_nots (x::xs) = if x = "~" - then - ["\\", "<", "n", "o", "t", ">"]@(change_nots xs) - else (x::(change_nots xs)) +val change_nots = String.translate (fn c => if c = #"~" then "\\" else str c); -(* -fun clstrs_to_string [] str = str -| clstrs_to_string (x::[]) str = str^x -| clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; ")) -*) -fun clstrs_to_string [] str = implode (change_nots (explode str)) -| clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x))) -| clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; "))))) - - +fun clstrs_to_string xs = space_implode "; " (map change_nots xs); fun thmvars_to_quantstring [] str = str | thmvars_to_quantstring (x::[]) str =str^x^". " | thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" ")) -fun clause_strs_to_isar clstrs [] = "\"\\"^(clstrs_to_string clstrs "")^"\\ \\ False\"" -| clause_strs_to_isar clstrs thmvars = "\"\\"^(thmvars_to_quantstring thmvars "")^"\\"^(clstrs_to_string clstrs "")^"\\ \\ False\"" +fun clause_strs_to_isar clstrs [] = + "\"\\"^(clstrs_to_string clstrs)^"\\ \\ False\"" +| clause_strs_to_isar clstrs thmvars = + "\"\\"^(thmvars_to_quantstring thmvars "")^ + "\\"^(clstrs_to_string clstrs)^"\\ \\ False\"" -fun frees_to_string [] str = implode (change_nots (explode str)) -| frees_to_string (x::[]) str = implode (change_nots (explode (str^x))) -| frees_to_string (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" "))))) - -fun frees_to_isar_str [] = "" -| frees_to_isar_str clstrs = (frees_to_string clstrs "") +fun frees_to_isar_str clstrs = space_implode " " (map change_nots clstrs) (***********************************************************************) diff -r fc7cc8137b97 -r 3f12de2e2e6e src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Sep 09 12:18:15 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Sep 09 17:47:37 2005 +0200 @@ -87,15 +87,12 @@ fun reap(pid, instr, outstr) = - let - val u = TextIO.closeIn instr; - val u = TextIO.closeOut outstr; - - val (_, status) = - Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) - in - status - end + let val u = TextIO.closeIn instr; + val u = TextIO.closeOut outstr; + val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) + in + status + end fun fdReader (name : string, fd : Posix.IO.file_desc) = Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; @@ -106,8 +103,7 @@ initBlkMode = true, name = name, chunkSize=4096, - fd = fd - }; + fd = fd}; fun openOutFD (name, fd) = TextIO.mkOutstream ( @@ -125,38 +121,31 @@ fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); -fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr); - -fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr))); +fun cmdInStream (CMDPROC{instr,outstr,...}) = instr; -fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = proc_handle; +fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = + (prover,(cmd, (instr,outstr))); -fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (prover); - -fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (thmstring); +fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = + proc_handle; -fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (goalstring); - -fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr); +fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = + prover; -(********************************************************************************************) -(* takes a list of arguments and sends them individually to the watcher process by pipe *) -(********************************************************************************************) +fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = + thmstring; -fun outputArgs (toWatcherStr, []) = () -| outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); - TextIO.flushOut toWatcherStr; - outputArgs (toWatcherStr, xs)) +fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = + goalstring; + (********************************************************************************) (* gets individual args from instream and concatenates them into a list *) (********************************************************************************) -fun getArgs (fromParentStr, toParentStr,ys) = let - val thisLine = TextIO.input fromParentStr - in - ((ys@[thisLine])) - end +fun getArgs (fromParentStr, toParentStr, ys) = + let val thisLine = TextIO.input fromParentStr + in ys@[thisLine] end (********************************************************************************) @@ -164,7 +153,7 @@ (********************************************************************************) fun callResProver (toWatcherStr, arg) = - (sendOutput (toWatcherStr, arg^"\n"); + (TextIO.output (toWatcherStr, arg^"\n"); TextIO.flushOut toWatcherStr) (*****************************************************************************************) @@ -175,14 +164,14 @@ (*Uses the $-character to separate items sent to watcher*) fun callResProvers (toWatcherStr, []) = - (sendOutput (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) + (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) | callResProvers (toWatcherStr, (prover,thmstring,goalstring, proverCmd,settings, axfile, hypsfile,probfile) :: args) = let val _ = File.write (File.tmp_path (Path.basic "tog_comms")) (prover^thmstring^goalstring^proverCmd^settings^ hypsfile^probfile) - in sendOutput (toWatcherStr, + in TextIO.output (toWatcherStr, (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^ settings^"$"^hypsfile^"$"^probfile^"\n")); goals_being_watched := (!goals_being_watched) + 1; @@ -196,7 +185,7 @@ (* Send message to watcher to kill currently running vampires *) (**************************************************************) -fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); TextIO.flushOut toWatcherStr) @@ -262,7 +251,7 @@ TextIO.flushOut toParentStr; (("","","","Kill children",[],"")::cmdList) ) - else let val thisCmd = getCmd (thisLine) + else let val thisCmd = getCmd thisLine (*********************************************************) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*) (* i.e. put back into tuple format *) @@ -270,7 +259,7 @@ in (*TextIO.output (toParentStr, thisCmd); TextIO.flushOut toParentStr;*) - getCmds (toParentStr,fromParentStr, (thisCmd::cmdList)) + getCmds (toParentStr, fromParentStr, (thisCmd::cmdList)) end end @@ -302,16 +291,15 @@ (** pipes for communication between parent and watcher **) val p1 = Posix.IO.pipe () val p2 = Posix.IO.pipe () - fun closep () = ( - Posix.IO.close (#outfd p1); + fun closep () = + (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1); Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p2) - ) + Posix.IO.close (#infd p2)) (***********************************************************) (****** fork a watcher process and get it set up and going *) (***********************************************************) - fun startWatcher (procList) = + fun startWatcher procList = (case Posix.Process.fork() (***************************************) of SOME pid => pid (* parent - i.e. main Isabelle process *) (***************************************) @@ -338,7 +326,7 @@ (*************************************************************) fun pollParentInput () = - let val pd = OS.IO.pollDesc (fromParentIOD) + let val pd = OS.IO.pollDesc fromParentIOD in if isSome pd then let val pd' = OS.IO.pollIn (valOf pd) @@ -356,7 +344,7 @@ else NONE end - fun pollChildInput (fromStr) = + fun pollChildInput fromStr = let val _ = File.append (File.tmp_path (Path.basic "child_poll")) ("In child_poll\n") val iod = getInIoDesc fromStr @@ -465,31 +453,13 @@ (*** add subgoal id num to this *) fun execCmds [] procList = procList - | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child")) ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) - in - if prover = "spass" - then - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = - (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) - val (instr, outstr) = Unix.streamsOf childhandle - val newProcList = (((CMDPROC{ - prover = prover, - cmd = file, - thmstring = thmstring, - goalstring = goalstring, - proc_handle = childhandle, - instr = instr, - outstr = outstr })::procList)) - val _ = File.append (File.tmp_path (Path.basic "exec_child")) - ("\nexecuting command for goal:\n"^ - goalstring^proverCmd^(concat settings)^file^ - " at "^(Date.toString(Date.fromTimeLocal(Time.now())))) - in - Posix.Process.sleep (Time.fromSeconds 1); - execCmds cmds newProcList - end - else - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = + | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = + let val _ = File.write (File.tmp_path (Path.basic "exec_child")) + (space_implode "\n" + (["About to execute command for goal:", + goalstring, proverCmd] @ settings @ + [file, Date.toString(Date.fromTimeLocal(Time.now()))])) + val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (settings@[file]))) val (instr, outstr) = Unix.streamsOf childhandle @@ -503,20 +473,18 @@ outstr = outstr }) :: procList val _ = File.append (File.tmp_path (Path.basic "exec_child")) - ("executing command for goal:\n"^ - goalstring^proverCmd^(concat settings)^file^ - " at "^(Date.toString(Date.fromTimeLocal(Time.now())))) + ("\nFinished at " ^ + Date.toString(Date.fromTimeLocal(Time.now()))) in Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList end - end (****************************************) (* call resolution processes remotely *) (* settings should be a list of strings *) - (* e.g. ["-t 300", "-m 100000"] *) + (* e.g. ["-t300", "-m100000"] *) (****************************************) (* fun execRemoteCmds [] procList = procList @@ -527,23 +495,19 @@ end *) - fun printList (outStr, []) = () - | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) - - (**********************************************) (* Watcher Loop *) (**********************************************) val iterations_left = ref 1000; (*200 seconds, 5 iterations per sec*) fun keepWatching (toParentStr, fromParentStr,procList) = - let fun loop (procList) = + let fun loop procList = let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) val cmdsFromIsa = pollParentInput () fun killchildHandler () = (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); TextIO.flushOut toParentStr; - killChildren (map (cmdchildHandle) procList); + killChildren (map cmdchildHandle procList); ()) in (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) @@ -583,7 +547,7 @@ loop newProcList' end else (* No new input from Isabelle *) - let val newProcList = checkChildren ((procList), toParentStr) + let val newProcList = checkChildren (procList, toParentStr) in (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n "); loop newProcList @@ -625,7 +589,7 @@ (*******************************) val procList = [] - val pid = startWatcher (procList) + val pid = startWatcher procList (**************************************************) (* communication streams to watcher *) (**************************************************) @@ -680,10 +644,10 @@ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) val _ = debug ("subgoals forked to createWatcher: "^prems_string); (*FIXME: do we need an E proofHandler??*) - fun vampire_proofHandler (n) = + fun vampire_proofHandler n = (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"))) - fun spass_proofHandler (n) = ( + fun spass_proofHandler n = ( let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in")) "Starting SPASS signal handler\n" val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin @@ -717,7 +681,7 @@ then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) ("Reaping a watcher, goals watched is: " ^ (string_of_int (!goals_being_watched))^"\n"); - killWatcher (childpid); reapWatcher (childpid,childin, childout); ()) + killWatcher childpid; reapWatcher (childpid,childin, childout); ()) else () ) (* print out a list of rules used from clasimpset*) else if substring (reconstr, 0,5) = "Rules" @@ -729,7 +693,7 @@ then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) ("Reaping a watcher, goals watched is: " ^ (string_of_int (!goals_being_watched))^"\n"); - killWatcher (childpid); reapWatcher (childpid,childin, childout);() + killWatcher childpid; reapWatcher (childpid,childin, childout);() ) else () ) (* if proof translation failed *) @@ -742,7 +706,7 @@ then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) ("Reaping a watcher, goals watched is: " ^ (string_of_int (!goals_being_watched))^"\n"); - killWatcher (childpid); reapWatcher (childpid,childin, childout);() + killWatcher childpid; reapWatcher (childpid,childin, childout);() ) else () ) @@ -755,7 +719,7 @@ then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) ("Reaping a watcher, goals watched is: " ^ (string_of_int (!goals_being_watched))^"\n"); - killWatcher (childpid); reapWatcher (childpid,childin, childout);() + killWatcher childpid; reapWatcher (childpid,childin, childout);() ) else () ) @@ -768,7 +732,7 @@ then (File.write (File.tmp_path (Path.basic "foo_reap_comp")) ("Reaping a watcher, goals watched is: " ^ (string_of_int (!goals_being_watched))^"\n"); - killWatcher (childpid); reapWatcher (childpid,childin, childout);() + killWatcher childpid; reapWatcher (childpid,childin, childout);() ) else () ) end) diff -r fc7cc8137b97 -r 3f12de2e2e6e src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Sep 09 12:18:15 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Sep 09 17:47:37 2005 +0200 @@ -24,7 +24,7 @@ val prover = ref "spass"; (* use spass as default prover *) val custom_spass = (*specialized options for SPASS*) - ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub", + ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub", "-DocProof","-TimeLimit=60"]; val axiom_file = File.tmp_path (Path.basic "axioms"); @@ -147,6 +147,8 @@ val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n) val _ = debug ("prob file in call_resolve_tac is " ^ probfile) in + (*Avoid command arguments containing spaces: Poly/ML and SML/NJ + versions of Unix.execute treat them differently!*) if !prover = "spass" then let val optionline = @@ -154,7 +156,7 @@ (*Proof reconstruction works for only a limited set of inference rules*) then "-" ^ space_implode "%-" (!custom_spass) - else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*) + else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*) val _ = debug ("SPASS option string is " ^ optionline) val _ = ResLib.helper_path "SPASS_HOME" "SPASS" (*We've checked that SPASS is there for ATP/spassshell to run.*) @@ -168,7 +170,7 @@ then let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" in - ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", + ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000", axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end diff -r fc7cc8137b97 -r 3f12de2e2e6e src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Fri Sep 09 12:18:15 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Fri Sep 09 17:47:37 2005 +0200 @@ -27,7 +27,7 @@ val make_conjecture_clause_thm : Thm.thm -> clause val make_hypothesis_clause : Term.term -> clause val special_equal : bool ref - val clause_info : clause -> string * string + val get_axiomName : clause -> string val typed : unit -> unit val untyped : unit -> unit val num_of_clauses : clause -> int @@ -35,7 +35,7 @@ val dfg_clauses2str : string list -> string val clause2dfg : clause -> string * string list val clauses2dfg : clause list -> string -> clause list -> clause list -> - (string * int) list -> (string * int) list -> string list -> string + (string * int) list -> (string * int) list -> string list -> string val tfree_dfg_clause : string -> string val tptp_arity_clause : arityClause -> string @@ -70,8 +70,8 @@ val tfree_prefix = "t_"; val clause_prefix = "cls_"; - val arclause_prefix = "arcls_" +val clrelclause_prefix = "relcls_"; val const_prefix = "c_"; val tconst_prefix = "tc_"; @@ -178,8 +178,8 @@ val id_ref = ref 0; fun generate_id () = - let val id = !id_ref - in id_ref := id + 1; id end; + let val id = !id_ref + in id_ref := id + 1; id end; @@ -196,13 +196,12 @@ datatype type_literal = LTVar of string | LTFree of string; -datatype folTerm = UVar of string * fol_type| Fun of string * fol_type * folTerm list; +datatype folTerm = UVar of string * fol_type + | Fun of string * fol_type * folTerm list; datatype predicate = Predicate of pred_name * fol_type * folTerm list; - datatype literal = Literal of polarity * predicate * tag; - datatype typ_var = FOLTVar of indexname | FOLTFree of string; @@ -220,17 +219,20 @@ functions: (string*int) list}; - exception CLAUSE of string; - (*** make clauses ***) +fun isFalse (Literal (pol,Predicate(a,_,[]),_)) = + (pol andalso a = "c_False") orelse + (not pol andalso a = "c_True") + | isFalse _ = false; + fun make_clause (clause_id,axiom_name,kind,literals, types_sorts,tvar_type_literals, tfree_type_literals,tvars, predicates, functions) = - if null literals + if forall isFalse literals then error "Problem too trivial for resolution (empty clause)" else Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, @@ -241,6 +243,20 @@ functions = functions}; +(** Some Clause destructor functions **) + +fun string_of_kind (Clause cls) = name_of_kind (#kind cls); + +fun get_axiomName (Clause cls) = #axiom_name cls; + +fun get_clause_id (Clause cls) = #clause_id cls; + +fun funcs_of_cls (Clause cls) = #functions cls; + +fun preds_of_cls (Clause cls) = #predicates cls; + + + (*Definitions of the current theory--to allow suppressing types.*) val curr_defs = ref Defs.empty; @@ -640,16 +656,6 @@ | _ => classrelClauses_of_aux (sub, sups); - -(***** convert clauses to DFG format *****) - -fun string_of_clauseID (Clause cls) = - clause_prefix ^ string_of_int (#clause_id cls); - -fun string_of_kind (Clause cls) = name_of_kind (#kind cls); - -fun string_of_axiomName (Clause cls) = #axiom_name cls; - (****!!!! Changed for typed equality !!!!****) fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; @@ -686,6 +692,12 @@ else name ^ (ResLib.list_to_string terms_as_strings) end; + +fun string_of_clausename (cls_id,ax_name) = + clause_prefix ^ ascii_of ax_name ^ "_" ^ string_of_int cls_id; + +fun string_of_type_clsname (cls_id,ax_name,idx) = + string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (string_of_int idx); (********************************) @@ -714,22 +726,14 @@ | forall_close (vars,tvars) = ")" fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = - let val ax_str = - if ax_name = "" then cls_id - else cls_id ^ "_" ^ ascii_of ax_name - in - "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ - "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ - ax_str ^ ")." - end; + "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ + "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ + string_of_clausename (cls_id,ax_name) ^ ")."; -fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars,vars) = - let val ax_str = cls_id ^ "_tcs" ^ (string_of_int idx) - in - "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ - "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ - ax_str ^ ")." - end; +fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = + "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ + "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ + string_of_type_clsname (cls_id,ax_name,idx) ^ ")."; fun dfg_clause_aux (Clause cls) = let val lits = map dfg_literal (#literals cls) @@ -767,8 +771,8 @@ fun dfg_vars (Clause cls) = - let val lits = (#literals cls) - val folterms = mergelist(map dfg_folterms lits) + let val lits = (#literals cls) + val folterms = mergelist(map dfg_folterms lits) val vars = ResLib.flat_noDup(map get_uvars folterms) in vars @@ -787,7 +791,8 @@ (* make this return funcs and preds too? *) - fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) +fun string_of_predicate (Predicate("equal",typ,terms)) = + string_of_equality(typ,terms) | string_of_predicate (Predicate(name,_,[])) = name | string_of_predicate (Predicate(name,typ,terms)) = let val terms_as_strings = map string_of_term terms @@ -810,26 +815,20 @@ (*"lits" includes the typing assumptions (TVars)*) val vars = dfg_vars cls val tvars = dfg_tvars cls - val cls_id = string_of_clauseID cls - val ax_name = string_of_axiomName cls val knd = string_of_kind cls val lits_str = commas lits - val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) + val cls_id = get_clause_id cls + val axname = get_axiomName cls + val cls_str = gen_dfg_cls(cls_id,axname,knd,lits_str,tvars, vars) fun typ_clss k [] = [] | typ_clss k (tfree :: tfrees) = - (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: + (gen_dfg_type_cls(cls_id,axname,knd,tfree,k, tvars,vars)) :: (typ_clss (k+1) tfrees) in cls_str :: (typ_clss 0 tfree_lits) end; -fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls); - -fun funcs_of_cls (Clause cls) = #functions cls; - -fun preds_of_cls (Clause cls) = #predicates cls; - -fun string_of_arity (name, num) = name ^"," ^ (string_of_int num) +fun string_of_arity (name, num) = name ^ "," ^ (string_of_int num) fun string_of_preds preds = "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n"; @@ -865,8 +864,8 @@ fun clause2dfg cls = let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) - val cls_id = string_of_clauseID cls - val ax_name = string_of_axiomName cls + val cls_id = get_clause_id cls + val ax_name = get_axiomName cls val vars = dfg_vars cls val tvars = dfg_tvars cls val funcs = funcs_of_cls cls @@ -911,8 +910,8 @@ | clauses2dfg (cls::clss) probname axioms conjectures funcs preds tfrees = let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) - val cls_id = string_of_clauseID cls - val ax_name = string_of_axiomName cls + val cls_id = get_clause_id cls + val ax_name = get_axiomName cls val vars = dfg_vars cls val tvars = dfg_tvars cls val funcs' = distinct((funcs_of_cls cls)@funcs) @@ -973,28 +972,6 @@ end; -val clrelclause_prefix = "relcls_"; - -(* FIX later. Doesn't seem to be used in clasimp *) - -(*fun tptp_classrelLits sub sup = - let val tvar = "(T)" - in - case sup of NONE => "[++" ^ sub ^ tvar ^ "]" - | (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" - end; - - -fun tptp_classrelClause (ClassrelClause cls) = - let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) - val sub = #subclass cls - val sup = #superclass cls - val lits = tptp_classrelLits sub sup - in - "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." - end; - *) - (********************************) (* code to produce TPTP files *) (********************************) @@ -1015,13 +992,11 @@ fun gen_tptp_cls (cls_id,ax_name,knd,lits) = - let val ax_str = (if ax_name = "" then "" else ("_" ^ ascii_of ax_name)) - in - "input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." - end; + "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ + knd ^ "," ^ lits ^ ")."; -fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = - "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ +fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = + "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; fun tptp_clause_aux (Clause cls) = @@ -1041,14 +1016,15 @@ fun tptp_clause cls = let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) - val cls_id = string_of_clauseID cls - val ax_name = string_of_axiomName cls + val cls_id = get_clause_id cls + val ax_name = get_axiomName cls val knd = string_of_kind cls val lits_str = ResLib.list_to_string' lits val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] | typ_clss k (tfree :: tfrees) = - (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: typ_clss (k+1) tfrees + gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: + typ_clss (k+1) tfrees in cls_str :: (typ_clss 0 tfree_lits) end; @@ -1056,8 +1032,8 @@ fun clause2tptp cls = let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) - val cls_id = string_of_clauseID cls - val ax_name = string_of_axiomName cls + val cls_id = get_clause_id cls + val ax_name = get_axiomName cls val knd = string_of_kind cls val lits_str = ResLib.list_to_string' lits val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) @@ -1105,12 +1081,10 @@ val knd = string_of_arKind arcls val all_lits = concl_lit :: prems_lits in - "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")." + "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ + (ResLib.list_to_string' all_lits) ^ ")." end; - -val clrelclause_prefix = "relcls_"; - fun tptp_classrelLits sub sup = let val tvar = "(T)" in