1.1 --- a/src/HOL/Tools/res_atp.ML Wed Jun 01 14:16:45 2005 +0200
1.2 +++ b/src/HOL/Tools/res_atp.ML Wed Jun 01 14:50:48 2005 +0200
1.3 @@ -31,11 +31,9 @@
1.4 val subgoals = [];
1.5
1.6 val traceflag = ref true;
1.7 -(* used for debug *)
1.8 +
1.9 val debug = ref false;
1.10 -
1.11 fun debug_tac tac = (warning "testing";tac);
1.12 -(* default value is false *)
1.13
1.14 val trace_res = ref false;
1.15 val full_spass = ref false;
1.16 @@ -71,13 +69,10 @@
1.17
1.18 (**** for Isabelle/ML interface ****)
1.19
1.20 -fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
1.21 +fun is_proof_char ch = (ch = " ") orelse
1.22 + ((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?"))
1.23
1.24 -fun proofstring x = let val exp = explode x
1.25 - in
1.26 - List.filter (is_proof_char ) exp
1.27 - end
1.28 -
1.29 +fun proofstring x = List.filter (is_proof_char) (explode x);
1.30
1.31
1.32 (*
1.33 @@ -135,11 +130,11 @@
1.34 val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
1.35 val out = TextIO.openOut(probfile)
1.36 in
1.37 - (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
1.38 + (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
1.39 + if !trace_res then (warning probfile) else ())
1.40 end;
1.41
1.42
1.43 -
1.44 (*********************************************************************)
1.45 (* call SPASS with settings and problem file for the current subgoal *)
1.46 (* should be modified to allow other provers to be called *)
1.47 @@ -221,28 +216,27 @@
1.48
1.49
1.50 fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) =
1.51 - (
1.52 - warning("in call_atp_tac_tfrees");
1.53 -
1.54 - tptp_inputs_tfrees (make_clauses thms) n tfrees;
1.55 - call_resolve_tac sign thms sg_term (childin, childout, pid) n;
1.56 - dummy_tac);
1.57 + (
1.58 + warning("in call_atp_tac_tfrees");
1.59 + tptp_inputs_tfrees (make_clauses thms) n tfrees;
1.60 + call_resolve_tac sign thms sg_term (childin, childout, pid) n;
1.61 + dummy_tac);
1.62
1.63 fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n st =
1.64 -let val sign = sign_of_thm st
1.65 - val _ = warning ("in atp_tac_tfrees ")
1.66 - val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
1.67 -
1.68 - in
1.69 -
1.70 -SELECT_GOAL
1.71 - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
1.72 - METAHYPS(fn negs => ( call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
1.73 -end;
1.74 + let val sign = sign_of_thm st
1.75 + val _ = warning ("in atp_tac_tfrees ")
1.76 + val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
1.77 + in
1.78 + SELECT_GOAL
1.79 + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
1.80 + METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term
1.81 + (childin, childout,pid) ))]) n st
1.82 + end;
1.83
1.84
1.85 fun isar_atp_g tfrees sg_term (childin, childout, pid) n =
1.86 -((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
1.87 + ((warning("in isar_atp_g"));
1.88 + atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
1.89
1.90
1.91
1.92 @@ -256,7 +250,7 @@
1.93 if (k > n)
1.94 then ()
1.95 else
1.96 - let val prems = prems_of thm
1.97 + let val prems = prems_of thm
1.98 val sg_term = ReconOrderClauses.get_nth n prems
1.99 val thmstring = string_of_thm thm
1.100 in
1.101 @@ -282,9 +276,8 @@
1.102
1.103 fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) =
1.104 let val tfree_lits = isar_atp_h thms
1.105 - in
1.106 - (warning("in isar_atp_aux"));
1.107 - isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid)
1.108 + in warning("in isar_atp_aux");
1.109 + isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid)
1.110 end;
1.111
1.112 (******************************************************************)
1.113 @@ -294,9 +287,8 @@
1.114 (* turns off xsymbol at start of function, restoring it at end *)
1.115 (******************************************************************)
1.116 (*FIX changed to clasimp_file *)
1.117 -fun isar_atp' (thms, thm) =
1.118 - let
1.119 - val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
1.120 +fun isar_atp' (ctxt, thms, thm) =
1.121 + let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
1.122 val _= (warning ("in isar_atp'"))
1.123 val prems = prems_of thm
1.124 val sign = sign_of_thm thm
1.125 @@ -305,8 +297,10 @@
1.126 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
1.127
1.128 (* set up variables for writing out the clasimps to a tptp file *)
1.129 - val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file)
1.130 - val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )
1.131 + val (clause_arr, num_of_clauses) =
1.132 + ResClasimp.write_out_clasimp (File.sysify_path clasimp_file)
1.133 + (ProofContext.theory_of ctxt)
1.134 + val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file)
1.135
1.136 (* cq: add write out clasimps to file *)
1.137
1.138 @@ -349,8 +343,6 @@
1.139 safeEs @ safeIs @ hazEs @ hazIs
1.140 end;
1.141
1.142 -
1.143 -
1.144 fun append_name name [] _ = []
1.145 | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
1.146
1.147 @@ -360,7 +352,6 @@
1.148 thms'::(append_names names thmss)
1.149 end;
1.150
1.151 -
1.152 fun get_thms_ss [] = []
1.153 | get_thms_ss thms =
1.154 let val names = map Thm.name_of_thm thms
1.155 @@ -370,9 +361,6 @@
1.156 ResLib.flat_noDup thms''
1.157 end;
1.158
1.159 -
1.160 -
1.161 -
1.162 in
1.163
1.164
1.165 @@ -395,8 +383,6 @@
1.166 *)
1.167
1.168
1.169 -
1.170 -
1.171 (* called in Isar automatically *)
1.172
1.173 fun isar_atp (ctxt,thm) =
1.174 @@ -413,14 +399,12 @@
1.175 (warning ("subgoals in isar_atp: "^prems_string));
1.176 (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
1.177 ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
1.178 - isar_atp' (prems, thm))
1.179 + isar_atp' (ctxt, prems, thm))
1.180 end;
1.181
1.182 end
1.183
1.184
1.185 -
1.186 -
1.187 end;
1.188
1.189 Proof.atp_hook := ResAtp.isar_atp;