--- 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 "\\<not>" 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 [] = "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
-| clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
+fun clause_strs_to_isar clstrs [] =
+ "\"\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\""
+| clause_strs_to_isar clstrs thmvars =
+ "\"\\<And>"^(thmvars_to_quantstring thmvars "")^
+ "\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> 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)
(***********************************************************************)
--- 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)
--- 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
--- 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