--- 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 **)
--- 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;
--- 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