# HG changeset patch # User paulson # Date 1152181097 -7200 # Node ID b07a138b4e7d1355f311b5a4c911299660205924 # Parent 815393c02db94e5eb933bc867a327c848d611f6d some tidying; fixed the output of theorem names diff -r 815393c02db9 -r b07a138b4e7d src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jul 06 11:26:49 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Jul 06 12:18:17 2006 +0200 @@ -503,8 +503,8 @@ fun make_unique ht xs = (app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht); -fun mem_thm thm [] = false - | mem_thm thm ((thm',name)::thms_names) = equal_thm (thm,thm') orelse mem_thm thm thms_names; +fun mem_thm th [] = false + | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names; fun insert_thms [] thms_names = thms_names | insert_thms ((thm,name)::thms_names) thms_names' = @@ -596,6 +596,7 @@ then ResClause.dfg_write_file goals filename (axioms, classrels, arities) else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities); +(*Called by the oracle-based methods declared in res_atp_methods.ML*) fun write_subgoal_file dfg mode ctxt conjectures user_thms n = let val conj_cls = make_clauses conjectures val hyp_cls = cnf_hyps_thms ctxt @@ -604,18 +605,20 @@ val rm_black_cls = blacklist_filter included_thms val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls val user_cls = ResAxioms.cnf_rules_pairs user_rules - val axclauses_as_thms = get_relevant_clauses ctxt cla_simp_atp_clauses user_cls (map prop_of goal_cls) + val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses + user_cls (map prop_of goal_cls) val thy = ProofContext.theory_of ctxt - val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls] - | Fol => FOL - | Hol => HOL + val prob_logic = case mode of + Auto => problem_logic_goals [map prop_of goal_cls] + | Fol => FOL + | Hol => HOL val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol () val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] val writer = if dfg then dfg_writer else tptp_writer val file = atp_input_file() in - (writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses); + (writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses); Output.debug ("Writing to " ^ file); file) end; @@ -690,35 +693,39 @@ Watcher.callResProvers(childout,atp_list); Output.debug "Sent commands to watcher!" end + +fun trace_array fname = + let val path = File.tmp_path (Path.basic fname) + in Array.app (File.append path o (fn s => s ^ "\n")) end; -(*We write out problem files for each subgoal. Argument pf generates filenames, +(*We write out problem files for each subgoal. Argument probfile generates filenames, and allows the suppression of the suffix "_1" in problem-generation mode. FIXME: does not cope with &&, and it isn't easy because one could have multiple subgoals, each involving &&.*) -fun write_problem_files pf (ctxt,th) = +fun write_problem_files probfile (ctxt,th) = let val goals = Thm.prems_of th val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] val rm_blacklist_cls = blacklist_filter included_thms val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals - val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ - Int.toString (length axclauses)) + val _ = Output.debug ("total clauses from thms = " ^ Int.toString (length axclauses)) val thy = ProofContext.theory_of ctxt fun get_neg_subgoals n = if n=0 then [] else - let val st = Seq.hd (EVERY' - [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th) + let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, + skolemize_tac] n th) val negs = Option.valOf (metahyps_thms n st) val negs_clauses = make_clauses negs in - negs_clauses::(get_neg_subgoals (n - 1)) + negs_clauses :: get_neg_subgoals (n-1) end val neg_subgoals = get_neg_subgoals (length goals) - val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals) - | Fol => FOL - | Hol => HOL + val goals_logic = case !linkup_logic_mode of + Auto => problem_logic_goals (map (map prop_of) neg_subgoals) + | Fol => FOL + | Hol => HOL val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol () val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) @@ -726,11 +733,15 @@ val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val writer = if !prover = "spass" then dfg_writer else tptp_writer fun write_all [] _ = [] - | write_all (subgoal::subgoals) k = - (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1)) - val thm_names = Array.fromList (map (#1 o #2) axclauses) + | write_all (sub::subgoals) k = + (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses), + probfile k) :: write_all subgoals (k-1) + val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals)) + val thm_names = Array.fromList clnames + val _ = if !Output.show_debug_msgs + then trace_array "thm_names" thm_names else () in - (write_all neg_subgoals (length goals), thm_names) + (filenames, thm_names) end; val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * @@ -766,9 +777,9 @@ (fn (ctxt,th) => if Thm.no_prems th then () else - let val pf = if Thm.nprems_of th = 1 then probfile_nosuffix - else prob_pathname - in ignore (write_problem_files pf (ctxt,th)) end); + let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix + else prob_pathname + in ignore (write_problem_files probfile (ctxt,th)) end); (** the Isar toplevel hook **) diff -r 815393c02db9 -r b07a138b4e7d src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Jul 06 11:26:49 2006 +0200 +++ b/src/HOL/Tools/res_clause.ML Thu Jul 06 12:18:17 2006 +0200 @@ -21,7 +21,8 @@ val clause_prefix : string val clause2tptp : clause -> string * string list val const_prefix : string - val dfg_write_file: thm list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit + val dfg_write_file: thm list -> string -> + ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list val fixed_var_prefix : string val gen_tptp_cls : int * string * string * string -> string val gen_tptp_type_cls : int * string * string * string * int -> string @@ -52,7 +53,8 @@ val tptp_classrelClause : classrelClause -> string val tptp_of_typeLit : type_literal -> string val tptp_tfree_clause : string -> string - val tptp_write_file: thm list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit + val tptp_write_file: thm list -> string -> + ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list val tvar_prefix : string val union_all : ''a list list -> ''a list val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit @@ -452,23 +454,18 @@ val make_conjecture_clauses = make_conjecture_clauses_aux 0 - - (*before converting an axiom clause to "clause" format, check if it is FOL*) fun make_axiom_clause thm (ax_name,cls_id) = - let val term = prop_of thm - in - if not (Meson.is_fol_term term) then - (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); - NONE) - else (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE) - end - handle CLAUSE _ => NONE; + if Meson.is_fol_term (prop_of thm) + then (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE) + else (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); NONE) fun make_axiom_clauses [] = [] | make_axiom_clauses ((thm,(name,id))::thms) = - case make_axiom_clause thm (name,id) of SOME cls => if isTaut cls then make_axiom_clauses thms else cls :: make_axiom_clauses thms - | NONE => make_axiom_clauses thms; + case make_axiom_clause thm (name,id) of + SOME cls => if isTaut cls then make_axiom_clauses thms + else (name,cls) :: make_axiom_clauses thms + | NONE => make_axiom_clauses thms; (**** Isabelle arities ****) @@ -777,7 +774,7 @@ let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) val conjectures = make_conjecture_clauses thms - val axclauses' = make_axiom_clauses axclauses + val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures) val clss = conjectures @ axclauses' val funcs = funcs_of_clauses clss arity_clauses @@ -798,7 +795,8 @@ writeln_strs out tfree_clss; writeln_strs out dfg_clss; TextIO.output (out, "end_of_list.\n\nend_problem.\n"); - TextIO.closeOut out + TextIO.closeOut out; + clnames end; @@ -872,7 +870,7 @@ let val _ = Output.debug ("Preparing to write the TPTP file " ^ filename) val clss = make_conjecture_clauses thms - val axclauses' = make_axiom_clauses axclauses + val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename @@ -882,7 +880,8 @@ writeln_strs out tptp_clss; List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses; List.app (curry TextIO.output out o tptp_arity_clause) arity_clauses; - TextIO.closeOut out + TextIO.closeOut out; + clnames end; diff -r 815393c02db9 -r b07a138b4e7d src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Thu Jul 06 11:26:49 2006 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Thu Jul 06 12:18:17 2006 +0200 @@ -15,9 +15,8 @@ val const_typargs = ref (Library.K [] : (string*typ -> typ list)); -fun init thy = (include_combS:=false;include_min_comb:=false;const_typargs := Sign.const_typargs thy); - - +fun init thy = (include_combS:=false; include_min_comb:=false; + const_typargs := Sign.const_typargs thy); (**********************************************************************) (* convert a Term.term with lambdas into a Term.term with combinators *) @@ -434,7 +433,7 @@ let val cls = make_axiom_clause thm (name,id) val clss = make_axiom_clauses thms in - if isTaut cls then clss else (cls::clss) + if isTaut cls then clss else (name,cls)::clss end; @@ -737,7 +736,7 @@ (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *) fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = let val clss = make_conjecture_clauses thms - val axclauses' = make_axiom_clauses axclauses + val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename @@ -749,7 +748,8 @@ List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses; List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses; List.app (curry TextIO.output out) helper_clauses; - TextIO.closeOut out + TextIO.closeOut out; + clnames end; @@ -780,7 +780,7 @@ fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) val conjectures = make_conjecture_clauses thms - val axclauses' = make_axiom_clauses axclauses + val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) val clss = conjectures @ axclauses' val funcs = funcs_of_clauses clss arity_clauses @@ -803,7 +803,8 @@ ResClause.writeln_strs out tfree_clss; ResClause.writeln_strs out dfg_clss; TextIO.output (out, "end_of_list.\n\nend_problem.\n"); - TextIO.closeOut out + TextIO.closeOut out; + clnames end; end \ No newline at end of file