# HG changeset patch # User paulson # Date 1128700641 -7200 # Node ID 2679ba74411f61322a145ba0964b8d0bc71ee48c # Parent 0ecfb66ea072e571e38afc09f2de19c0e70aff0e minor code tidyig diff -r 0ecfb66ea072 -r 2679ba74411f src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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.*) diff -r 0ecfb66ea072 -r 2679ba74411f src/HOL/Tools/res_atp.ML --- 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 diff -r 0ecfb66ea072 -r 2679ba74411f src/HOL/Tools/res_clause.ML --- 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 diff -r 0ecfb66ea072 -r 2679ba74411f src/HOL/Tools/res_lib.ML --- 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 =