diff -r 42d56a6dec6e -r ae5bb6001afb src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Sep 20 18:42:56 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue Sep 20 18:43:39 2005 +0200 @@ -61,30 +61,29 @@ (* write out a subgoal as tptp clauses to the file "xxxx_N"*) -fun tptp_inputs_tfrees thms n axclauses = +fun tptp_inputs_tfrees thms n (axclauses,classrel_clauses,arity_clauses) = let - val _ = debug ("in tptp_inputs_tfrees 0") val clss = map (ResClause.make_conjecture_clause_thm) thms - val _ = debug ("in tptp_inputs_tfrees 1") val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) - val _ = debug ("in tptp_inputs_tfrees 2") val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss) - val _ = debug ("in tptp_inputs_tfrees 3") - val probfile = prob_pathname() ^ "_" ^ string_of_int n + val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses + val arity_cls = map ResClause.tptp_arity_clause arity_clauses + val probfile = prob_pathname() ^ "_" ^ Int.toString n val out = TextIO.openOut(probfile) in ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses)); - ResLib.writeln_strs out (tfree_clss @ tptp_clss); + ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls); TextIO.closeOut out; debug probfile end; (* write out a subgoal in DFG format to the file "xxxx_N"*) -fun dfg_inputs_tfrees thms n axclauses = +fun dfg_inputs_tfrees thms n (axclauses,classrel_clauses,arity_clauses) = let val clss = map (ResClause.make_conjecture_clause_thm) thms - val probfile = prob_pathname() ^ "_" ^ (string_of_int n) + val probfile = prob_pathname() ^ "_" ^ (Int.toString n) + (*FIXME: classrel_clauses and arity_clauses*) val _ = debug ("about to write out dfg prob file " ^ probfile) - val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ string_of_int n) + val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n) axclauses [] [] [] val out = TextIO.openOut(probfile) in @@ -104,7 +103,7 @@ val goalstring = proofstring (Sign.string_of_term sign sg_term) val _ = debug ("goalstring in make_atp_lists is " ^ goalstring) - val probfile = prob_pathname() ^ "_" ^ string_of_int n + val probfile = prob_pathname() ^ "_" ^ Int.toString n val _ = debug ("problem file in watcher_call_provers is " ^ probfile) in (*Avoid command arguments containing spaces: Poly/ML and SML/NJ @@ -151,34 +150,31 @@ debug "Sent commands to watcher!" end -(*We write out problem files for each subgoal, but work is repeated (skolemize)*) -fun write_problem_files axclauses thm n = +(*We write out problem files for each subgoal*) +fun write_problem_files clause thm n = if n=0 then () else (SELECT_GOAL - (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, + (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, METAHYPS(fn negs => (if !prover = "spass" - then dfg_inputs_tfrees (make_clauses negs) n axclauses - else tptp_inputs_tfrees (make_clauses negs) n axclauses; - write_problem_files axclauses thm (n-1); + then dfg_inputs_tfrees (make_clauses negs) n clause + else tptp_inputs_tfrees (make_clauses negs) n clause; + write_problem_files clause thm (n-1); all_tac))]) n thm; ()); val last_watcher_pid = ref (NONE : Posix.Process.pid option); -(******************************************************************) -(* called in Isar automatically *) -(* writes out the current clasimpset to a tptp file *) -(* turns off xsymbol at start of function, restoring it at end *) -(******************************************************************) -(*FIX changed to clasimp_file *) + +(*writes out the current clasimpset to a tptp file; + turns off xsymbol at start of function, restoring it at end *) val isar_atp = setmp print_mode [] (fn (ctxt, thm) => if Thm.no_prems thm then () else let - val _= debug ("in isar_atp") + val _= debug "in isar_atp" val thy = ProofContext.theory_of ctxt val prems = Thm.prems_of thm val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems) @@ -193,13 +189,17 @@ val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) (*FIXME: hack!! need to consider relevance for all prems*) val _ = debug ("claset and simprules total clauses = " ^ - string_of_int (Array.length clause_arr)) + Int.toString (Array.length clause_arr)) + val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy + val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) + val arity_clauses = ResTypesSorts.arity_clause_thy thy + val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr) in last_watcher_pid := SOME pid; debug ("subgoals: " ^ prems_string); debug ("pid: " ^ Int.toString (ResLib.intOfPid pid)); - write_problem_files axclauses thm (length prems); + write_problem_files (axclauses,classrel_clauses,arity_clauses) thm (length prems); watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid) end); @@ -207,10 +207,14 @@ (fn (ctxt, thm) => if Thm.no_prems thm then () else - let val prems = Thm.prems_of thm - val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) + let + val prems = Thm.prems_of thm + val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) + val thy = ProofContext.theory_of ctxt + val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy + val arity_clauses = ResTypesSorts.arity_clause_thy thy in - write_problem_files axclauses thm (length prems) + write_problem_files (axclauses,classrel_clauses,arity_clauses) thm (length prems) end); @@ -228,10 +232,10 @@ debug ("subgoals in isar_atp: " ^ Pretty.string_of (ProofContext.pretty_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)))); - debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal)); + debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal)); debug ("current theory: " ^ Context.theory_name thy); hook_count := !hook_count +1; - debug ("in hook for time: " ^(string_of_int (!hook_count)) ); + debug ("in hook for time: " ^(Int.toString (!hook_count)) ); ResClause.init thy; if !destdir = "" then isar_atp (ctxt, goal) else isar_atp_writeonly (ctxt, goal)