--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Oct 07 15:08:28 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Oct 07 17:57:21 2005 +0200
@@ -156,27 +156,9 @@
map (fn x => Array.sub(clause_arr, x)) clasimp_nums
end
-
-(*****************************************************)
-(* get names of clasimp axioms used *)
-(*****************************************************)
-
+(* get names of clasimp axioms used*)
fun get_axiom_names step_nums clause_arr =
- let
- (* not sure why this is necessary again, but seems to be *)
- val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
-
- (***********************************************)
- (* here need to add the clauses from clause_arr*)
- (***********************************************)
-
- val clasimp_names_cls = get_clasimp_cls clause_arr step_nums
- val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
- val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
- in
- clasimp_names
- end
-
+ map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums);
fun get_axiom_names_spass proofstr clause_arr =
let (* parse spass proof into datatype *)
@@ -227,9 +209,7 @@
fun addvars c (a,b) = (a,b,c)
fun get_axioms_used proof_steps thms clause_arr =
- let
- val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
- val axioms = (List.filter is_axiom) proof_steps
+ let val axioms = (List.filter is_axiom) proof_steps
val step_nums = get_step_nums axioms []
val clauses = make_clauses thms (*FIXME: must this be repeated??*)
@@ -266,9 +246,9 @@
val extra_with_vars = if (not (extra_metas = []) )
then ListPair.zip (extra_metas,extra_vars)
else []
- in
- (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
- end;
+ in
+ (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
+ end;
(*********************************************************************)
@@ -277,7 +257,7 @@
(*********************************************************************)
fun rules_to_string [] = "NONE"
- | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
+ | rules_to_string xs = space_implode " " xs
(*The signal handler in watcher.ML must be able to read the output of this.*)
--- a/src/HOL/Tools/res_atp.ML Fri Oct 07 15:08:28 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Oct 07 17:57:21 2005 +0200
@@ -55,18 +55,18 @@
(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
- let
- val clss = map (ResClause.make_conjecture_clause_thm) thms
- val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
- val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
- val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
- val arity_cls = map ResClause.tptp_arity_clause arity_clauses
- val out = TextIO.openOut(pf n)
- in
- writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
- writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
- TextIO.closeOut out
- end;
+ let
+ val clss = map (ResClause.make_conjecture_clause_thm) thms
+ val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
+ val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
+ val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
+ val arity_cls = map ResClause.tptp_arity_clause arity_clauses
+ val out = TextIO.openOut(pf n)
+ in
+ writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
+ writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
+ TextIO.closeOut out
+ end;
(* write out a subgoal in DFG format to the file "xxxx_N"*)
fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
@@ -165,9 +165,17 @@
pf n :: writenext (n-1))
in (writenext (length prems), clause_arr) end;
-val last_watcher_pid =
- ref (NONE : (TextIO.instream * TextIO.outstream *
- Posix.Process.pid * string list) option);
+val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
+ Posix.Process.pid * string list) option);
+
+fun kill_last_watcher () =
+ (case !last_watcher_pid of
+ NONE => ()
+ | SOME (_, childout, pid, files) =>
+ (debug ("Killing old watcher, pid = " ^ Int.toString (ResLib.intOfPid pid));
+ Watcher.killWatcher pid;
+ ignore (map (try OS.FileSys.remove) files)))
+ handle OS.SysErr _ => debug "Attempt to kill watcher failed";
(*writes out the current clasimpset to a tptp file;
turns off xsymbol at start of function, restoring it at end *)
@@ -176,13 +184,7 @@
if Thm.no_prems th then ()
else
let
- val _ = (case !last_watcher_pid of NONE => ()
- | SOME (_, childout, pid, files) =>
- (debug ("Killing old watcher, pid = " ^
- Int.toString (ResLib.intOfPid pid));
- Watcher.killWatcher pid;
- ignore (map (try OS.FileSys.remove) files)))
- handle OS.SysErr _ => debug "Attempt to kill watcher failed";
+ val _ = kill_last_watcher()
val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
in
--- a/src/HOL/Tools/res_clause.ML Fri Oct 07 15:08:28 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Fri Oct 07 17:57:21 2005 +0200
@@ -77,8 +77,10 @@
val class_prefix = "class_";
-(**** some useful functions ****)
+fun union_all xss = foldl (op union) [] xss;
+
+(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [("op =", "equal"),
("op <=", "lessequals"),
@@ -287,8 +289,8 @@
let val foltyps_ts = map type_of Ts
val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
val (ts, funcslist) = ListPair.unzip ts_funcs
- val ts' = ResLib.flat_noDup ts
- val funcs' = ResLib.flat_noDup funcslist
+ val ts' = union_all ts
+ val funcs' = union_all funcslist
val t = make_fixed_type_const a
in
((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
@@ -366,8 +368,8 @@
let val (funName,(funType,ts1),funcs) = fun_name_type f args
val (args',ts_funcs) = ListPair.unzip (map term_of args)
val (ts2,funcs') = ListPair.unzip ts_funcs
- val ts3 = ResLib.flat_noDup (ts1::ts2)
- val funcs'' = ResLib.flat_noDup((funcs::funcs'))
+ val ts3 = union_all (ts1::ts2)
+ val funcs'' = union_all(funcs::funcs')
in
(Fun(funName,funType,args'), (ts3,funcs''))
end
@@ -378,8 +380,8 @@
val equal_name = make_fixed_const ("op =")
in
(Fun(equal_name,arg_typ,args'),
- (ResLib.flat_noDup ts,
- (make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs))
+ (union_all ts,
+ (make_fixed_var equal_name, 2):: union_all funcs))
end
in
case f of Const ("op =", typ) => term_of_eq (f,args)
@@ -400,16 +402,16 @@
val equal_name = make_fixed_const "op ="
in
(Predicate(equal_name,arg_typ,args'),
- ResLib.flat_noDup ts,
+ union_all ts,
[((make_fixed_var equal_name), 2)],
- (ResLib.flat_noDup funcs))
+ union_all funcs)
end
| pred_of (pred,args) =
let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
val (args',ts_funcs) = ListPair.unzip (map term_of args)
val (ts2,ffuncs) = ListPair.unzip ts_funcs
- val ts3 = ResLib.flat_noDup (ts1::ts2)
- val ffuncs' = (ResLib.flat_noDup ffuncs)
+ val ts3 = union_all (ts1::ts2)
+ val ffuncs' = union_all ffuncs
val newfuncs = distinct (pfuncs@ffuncs')
val arity =
case pred of
@@ -445,9 +447,8 @@
let val ((pred,ts', preds', funcs'), pol, tag) =
predicate_of (P,true,false)
val lits' = Literal(pol,pred,tag) :: lits
- val ts'' = ResLib.no_rep_app ts ts'
in
- (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
+ (lits', ts union ts', distinct(preds'@preds), distinct(funcs'@funcs))
end;
@@ -487,14 +488,14 @@
val preds' = (map pred_of_sort vs)@preds
val (vss,fss, preds'') = add_typs_aux tss preds'
in
- (ResLib.no_rep_app vs vss, fss, preds'')
+ (vs union vss, fss, preds'')
end
| add_typs_aux ((FOLTFree x,s)::tss) preds =
let val fs = sorts_on_typs (FOLTFree x, s)
val preds' = (map pred_of_sort fs)@preds
val (vss,fss, preds'') = add_typs_aux tss preds'
in
- (vss, ResLib.no_rep_app fs fss,preds'')
+ (vss, fs union fss, preds'')
end;
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds
@@ -614,7 +615,7 @@
val tvars = get_TVars nargs
val conclLit = make_TConsLit(true,(res,tcons,tvars))
val tvars_srts = ListPair.zip (tvars,args)
- val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
+ val tvars_srts' = union_all(map pack_sort tvars_srts)
val false_tvars_srts' = map (pair false) tvars_srts'
val premLits = map make_TVarLit false_tvars_srts'
in
@@ -761,7 +762,7 @@
fun get_uvars (UVar(a,typ)) = [a]
-| get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
+| get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
fun is_uvar (UVar _) = true
@@ -777,7 +778,7 @@
let val lits = #literals cls
val folterms = mergelist(map dfg_folterms lits)
in
- ResLib.flat_noDup(map get_uvars folterms)
+ union_all(map get_uvars folterms)
end
@@ -888,7 +889,7 @@
val axstr = (space_implode "\n" axstrs) ^ "\n\n"
val conjstrs_tfrees = (map clause2dfg conjectures)
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
- val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees)
+ val tfree_clss = map tfree_dfg_clause (union_all atfrees)
val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
val funcstr = string_of_funcs funcs
val predstr = string_of_preds preds
@@ -900,8 +901,8 @@
end;
fun clauses2dfg [] probname axioms conjectures funcs preds =
- let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs
- val preds' = (ResLib.flat_noDup(map preds_of_cls axioms)) @ preds
+ let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs
+ val preds' = (union_all(map preds_of_cls axioms)) @ preds
in
gen_dfg_file probname axioms conjectures funcs' preds'
end
--- a/src/HOL/Tools/res_lib.ML Fri Oct 07 15:08:28 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML Fri Oct 07 17:57:21 2005 +0200
@@ -8,10 +8,7 @@
signature RES_LIB =
sig
-val flat_noDup : ''a list list -> ''a list
val helper_path : string -> string -> string
-val no_rep_add : ''a -> ''a list -> ''a list
-val no_rep_app : ''a list -> ''a list -> ''a list
val intOfPid : Posix.Process.pid -> Int.int
val pidOfInt : Int.int -> Posix.Process.pid
end;
@@ -20,16 +17,6 @@
structure ResLib : RES_LIB =
struct
-fun no_rep_add x [] = [x]
- | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
-
-fun no_rep_app l1 [] = l1
- | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
-
-fun flat_noDup [] = []
- | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
-
-
(*Return the path to a "helper" like SPASS or tptp2X, first checking that
it exists. --lcp *)
fun helper_path evar base =