--- a/src/HOL/Tools/res_atp.ML Fri Jan 21 13:55:07 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML Fri Jan 21 18:00:18 2005 +0100
@@ -4,16 +4,20 @@
ATPs with TPTP format input.
*)
+
+(*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*)
+
signature RES_ATP =
sig
val trace_res : bool ref
val axiom_file : Path.T
val hyps_file : Path.T
-val isar_atp : Thm.thm list * Thm.thm -> unit
+val isar_atp : ProofContext.context * Thm.thm -> unit
val prob_file : Path.T
val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
val atp_tac : int -> Tactical.tactic
+val debug: bool ref
end;
@@ -21,6 +25,10 @@
struct
+(* used for debug *)
+val debug = ref false;
+
+fun debug_tac tac = (warning "testing";tac);
(* default value is false *)
val trace_res = ref false;
@@ -46,10 +54,10 @@
-fun tptp_inputs thms =
+fun tptp_inputs thms n =
let val clss = map (ResClause.make_conjecture_clause_thm) thms
val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss)
- val probfile = File.sysify_path prob_file
+ val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
val out = TextIO.openOut(probfile)
in
(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
@@ -58,12 +66,14 @@
(**** for Isabelle/ML interface ****)
-fun call_atp_tac thms = (tptp_inputs thms; dummy_tac);
+fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
+
-val atp_tac = SELECT_GOAL
- (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac,
- METAHYPS(fn negs => (call_atp_tac(make_clauses negs)))]);
+
+fun atp_tac n = SELECT_GOAL
+ (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
+ METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n;
fun atp_ax_tac axioms n =
@@ -97,13 +107,13 @@
fun repeat_someI_ex thm = repeat_RS thm someI_ex;
-
+(* convert clauses from "assume" to conjecture. write to file "hyps" *)
fun isar_atp_h thms =
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
val prems' = map repeat_someI_ex prems
val prems'' = make_clauses prems'
val prems''' = ResAxioms.rm_Eps [] prems''
- val clss = map ResClause.make_hypothesis_clause prems'''
+ val clss = map ResClause.make_conjecture_clause prems'''
val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
val hypsfile = File.sysify_path hyps_file
val out = TextIO.openOut(hypsfile)
@@ -116,21 +126,109 @@
val isar_atp_g = atp_tac;
-fun isar_atp_aux thms thm =
- (isar_atp_h thms; isar_atp_g 1 thm;());
+
+fun isar_atp_goal' thm k n =
+ if (k > n) then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
+
+
+fun isar_atp_goal thm n_subgoals = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals));
+
+
+
+fun isar_atp_aux thms thm n_subgoals =
+ (isar_atp_h thms; isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
+
+
+fun isar_atp' (thms, thm) =
+ let val prems = prems_of thm
+ in
+ case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
+ | _ => (isar_atp_aux thms thm (length prems))
+ end;
+
+
+
+
+local
+
+fun retr_thms ([]:MetaSimplifier.rrule list) = []
+ | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
+
+
+fun snds [] = []
+ | snds ((x,y)::l) = y::(snds l);
+
+
+
+
+fun get_thms_cs claset =
+ let val clsset = rep_cs claset
+ val safeEs = #safeEs clsset
+ val safeIs = #safeIs clsset
+ val hazEs = #hazEs clsset
+ val hazIs = #hazIs clsset
+ in
+ safeEs @ safeIs @ hazEs @ hazIs
+ end;
+
+
+
+fun append_name name [] _ = []
+ | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
+
+fun append_names (name::names) (thms::thmss) =
+ let val thms' = append_name name thms 0
+ in
+ thms'::(append_names names thmss)
+ end;
+
+
+fun get_thms_ss [] = []
+ | get_thms_ss thms =
+ let val names = map Thm.name_of_thm thms
+ val thms' = map (mksimps mksimps_pairs) thms
+ val thms'' = append_names names thms'
+ in
+ ResLib.flat_noDup thms''
+ end;
+
+
+
+
+in
+
+
+(* convert locally declared rules to axiom clauses *)
+(* write axiom clauses to ax_file *)
+fun isar_local_thms (delta_cs, delta_ss_thms) =
+ let val thms_cs = get_thms_cs delta_cs
+ val thms_ss = get_thms_ss delta_ss_thms
+ val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
+ val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
+ val ax_file = File.sysify_path axiom_file
+ val out = TextIO.openOut ax_file
+ in
+ (ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
+ end;
(* called in Isar automatically *)
-fun isar_atp (thms, thm) =
- let val prems = prems_of thm
+fun isar_atp (ctxt,thm) =
+ let val prems = ProofContext.prems_of ctxt
+ val d_cs = Classical.get_delta_claset ctxt
+ val d_ss_thms = Simplifier.get_delta_simpset ctxt
in
- case prems of [] => ()
- | _ => (isar_atp_aux thms thm)
+ (isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
end;
+end
+
+
+
+
end;
Proof.atp_hook := ResAtp.isar_atp;