15608

1 
(* Author: Jia Meng, Cambridge University Computer Laboratory


2 
ID: $Id$


3 
Copyright 2004 University of Cambridge

15347

4 


5 
ATPs with TPTP format input.


6 
*)

15452

7 


8 
(*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*)


9 

15347

10 
signature RES_ATP =


11 
sig


12 

15608

13 
val trace_res : bool ref


14 
val axiom_file : Path.T


15 
val hyps_file : Path.T


16 
val isar_atp : ProofContext.context * Thm.thm > unit


17 
val prob_file : Path.T


18 
val atp_ax_tac : Thm.thm list > int > Tactical.tactic


19 
val atp_tac : int > Tactical.tactic


20 
val debug: bool ref

15347

21 


22 
end;


23 


24 
structure ResAtp : RES_ATP =

15608

25 

15347

26 
struct


27 

15608

28 
(* used for debug *)


29 
val debug = ref false;

15452

30 

15608

31 
fun debug_tac tac = (warning "testing";tac);


32 
(* default value is false *)

15347

33 

15608

34 
val trace_res = ref false;

15347

35 

15608

36 
val skolem_tac = skolemize_tac;


37 

15347

38 

15608

39 
val atomize_tac =


40 
SUBGOAL


41 
(fn (prop,_) =>


42 
let val ts = Logic.strip_assums_hyp prop


43 
in EVERY1


44 
[METAHYPS


45 
(fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),


46 
REPEAT_DETERM_N (length ts) o (etac thin_rl)]


47 
end);

15347

48 

15608

49 
(* temporarily use these files, which will be loaded by Vampire *)


50 
val prob_file = File.tmp_path (Path.basic "prob");


51 
val axiom_file = File.tmp_path (Path.basic "axioms");


52 
val hyps_file = File.tmp_path (Path.basic "hyps");


53 
val dummy_tac = PRIMITIVE(fn thm => thm );


54 


55 

15347

56 

15608

57 
fun tptp_inputs thms n =


58 
let val clss = map (ResClause.make_conjecture_clause_thm) thms


59 
val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss)


60 
val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)


61 
val out = TextIO.openOut(probfile)


62 
in


63 
(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))


64 
end;

15347

65 


66 


67 
(**** for Isabelle/ML interface ****)


68 

15608

69 
fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);


70 


71 


72 

15452

73 

15608

74 
fun atp_tac n = SELECT_GOAL


75 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,


76 
METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n ;


77 

15347

78 

15608

79 
fun atp_ax_tac axioms n =


80 
let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms)


81 
val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls))


82 
val axiomfile = File.sysify_path axiom_file


83 
val out = TextIO.openOut (axiomfile)


84 
in


85 
(TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n)


86 
end;

15347

87 

15608

88 


89 
fun atp thm =


90 
let val prems = prems_of thm


91 
in


92 
case prems of [] => ()


93 
 _ => (atp_tac 1 thm; ())


94 
end;

15347

95 


96 


97 
(**** For running in Isar ****)


98 

15608

99 
(* same function as that in res_axioms.ML *)


100 
fun repeat_RS thm1 thm2 =


101 
let val thm1' = thm1 RS thm2 handle THM _ => thm1


102 
in


103 
if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)


104 
end;


105 


106 
(* a special version of repeat_RS *)


107 
fun repeat_someI_ex thm = repeat_RS thm someI_ex;


108 

15347

109 

15608

110 
(* convert clauses from "assume" to conjecture. write to file "hyps" *)


111 
fun isar_atp_h thms =


112 
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms


113 
val prems' = map repeat_someI_ex prems


114 
val prems'' = make_clauses prems'


115 
val prems''' = ResAxioms.rm_Eps [] prems''


116 
val clss = map ResClause.make_conjecture_clause prems'''


117 
val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)


118 
val tfree_lits = ResLib.flat_noDup tfree_litss


119 
val tfree_clss = map ResClause.tfree_clause tfree_lits


120 
val hypsfile = File.sysify_path hyps_file


121 
val out = TextIO.openOut(hypsfile)


122 
in


123 
((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits)


124 
end;

15347

125 

15608

126 
fun tptp_inputs_tfrees thms n tfrees =


127 
let val clss = map (ResClause.make_conjecture_clause_thm) thms


128 
val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)


129 
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)


130 
val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)


131 
val out = TextIO.openOut(probfile)


132 
in


133 
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))


134 
end;

15452

135 

15608

136 


137 
fun call_atp_tac_tfrees thms n tfrees = (tptp_inputs_tfrees thms n tfrees; dummy_tac);


138 


139 


140 
fun atp_tac_tfrees tfrees n = SELECT_GOAL


141 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,


142 
METAHYPS(fn negs => (call_atp_tac_tfrees (make_clauses negs) n tfrees))]) n;


143 


144 


145 
fun isar_atp_g tfrees = atp_tac_tfrees tfrees;

15452

146 

15608

147 
fun isar_atp_goal' thm k n tfree_lits =


148 
if (k > n) then () else (isar_atp_g tfree_lits k thm; isar_atp_goal' thm (k+1) n tfree_lits);


149 

15452

150 

15608

151 
fun isar_atp_goal thm n_subgoals tfree_lits = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits));

15603

152 

15608

153 

15452

154 

15608

155 
fun isar_atp_aux thms thm n_subgoals =


156 
let val tfree_lits = isar_atp_h thms


157 
in


158 
isar_atp_goal thm n_subgoals tfree_lits


159 
end;


160 

15452

161 

15608

162 
fun isar_atp' (thms, thm) =


163 
let val prems = prems_of thm


164 
in


165 
case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())


166 
 _ => (isar_atp_aux thms thm (length prems))


167 
end;


168 

15452

169 

15608

170 


171 


172 
local


173 


174 
fun get_thms_cs claset =


175 
let val clsset = rep_cs claset


176 
val safeEs = #safeEs clsset


177 
val safeIs = #safeIs clsset


178 
val hazEs = #hazEs clsset


179 
val hazIs = #hazIs clsset


180 
in


181 
safeEs @ safeIs @ hazEs @ hazIs


182 
end;


183 


184 

15452

185 

15608

186 
fun append_name name [] _ = []


187 
 append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));


188 


189 
fun append_names (name::names) (thms::thmss) =


190 
let val thms' = append_name name thms 0


191 
in


192 
thms'::(append_names names thmss)


193 
end;


194 

15452

195 

15608

196 
fun get_thms_ss [] = []


197 
 get_thms_ss thms =


198 
let val names = map Thm.name_of_thm thms


199 
val thms' = map (mksimps mksimps_pairs) thms


200 
val thms'' = append_names names thms'


201 
in


202 
ResLib.flat_noDup thms''


203 
end;


204 

15452

205 

15608

206 


207 


208 
in


209 

15452

210 

15608

211 
(* convert locally declared rules to axiom clauses *)


212 
(* write axiom clauses to ax_file *)


213 
fun isar_local_thms (delta_cs, delta_ss_thms) =


214 
let val thms_cs = get_thms_cs delta_cs


215 
val thms_ss = get_thms_ss delta_ss_thms


216 
val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))


217 
val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)


218 
val ax_file = File.sysify_path axiom_file


219 
val out = TextIO.openOut ax_file


220 
in


221 
(ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)


222 
end;

15347

223 

15608

224 


225 


226 

15347

227 

15608

228 
(* called in Isar automatically *)


229 
fun isar_atp (ctxt,thm) =


230 
let val prems = ProofContext.prems_of ctxt


231 
val d_cs = Classical.get_delta_claset ctxt


232 
val d_ss_thms = Simplifier.get_delta_simpset ctxt


233 
in


234 
(isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))


235 
end;

15347

236 

15608

237 
end


238 


239 


240 

15452

241 

15347

242 
end;


243 


244 
Proof.atp_hook := ResAtp.isar_atp;

15608

245 


246 
