author  blanchet 
Thu, 29 Jul 2010 23:11:35 +0200  
changeset 38102  019a49759829 
parent 38100  e458a0dd3dc1 
child 38105  373351f5f834 
permissions  rwrr 
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
32996
d2e48879e65a
removed disjunctive group cancellation  provers run independently;
wenzelm
parents:
32995
diff
changeset

3 
Author: Makarius 
35969  4 
Author: Jasmin Blanchette, TU Muenchen 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

5 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

6 
Sledgehammer's heart. 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

7 
*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

8 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

9 
signature SLEDGEHAMMER = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

10 
sig 
38023  11 
type failure = ATP_Systems.failure 
35969  12 
type relevance_override = Sledgehammer_Fact_Filter.relevance_override 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

13 
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command 
35969  14 
type params = 
15 
{debug: bool, 

16 
verbose: bool, 

36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset

17 
overlord: bool, 
35969  18 
atps: string list, 
19 
full_types: bool, 

36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

20 
explicit_apply: bool, 
35969  21 
relevance_threshold: real, 
36922  22 
relevance_convergence: real, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36184
diff
changeset

23 
theory_relevant: bool option, 
36922  24 
defs_relevant: bool, 
35969  25 
isar_proof: bool, 
36924  26 
isar_shrink_factor: int, 
35969  27 
timeout: Time.time, 
28 
minimize_timeout: Time.time} 

35867  29 
type problem = 
35969  30 
{subgoal: int, 
31 
goal: Proof.context * (thm list * thm), 

32 
relevance_override: relevance_override, 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

33 
axioms: (string * thm) list option} 
35867  34 
type prover_result = 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

35 
{outcome: failure option, 
35969  36 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

37 
pool: string Symtab.table, 
38015  38 
used_thm_names: string list, 
35969  39 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

40 
output: string, 
35969  41 
proof: string, 
42 
internal_thm_names: string Vector.vector, 

38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

43 
conjecture_shape: int list list} 
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

44 
type prover = params > minimize_command > problem > prover_result 
35867  45 

38023  46 
val dest_dir : string Config.T 
47 
val problem_prefix : string Config.T 

48 
val measure_runtime : bool Config.T 

35969  49 
val kill_atps: unit > unit 
50 
val running_atps: unit > unit 

29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28835
diff
changeset

51 
val messages: int option > unit 
38023  52 
val get_prover_fun : theory > string > prover 
38044  53 
val run_sledgehammer : 
54 
params > int > relevance_override > (string > minimize_command) 

55 
> Proof.state > unit 

38023  56 
val setup : theory > theory 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

57 
end; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

58 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

59 
structure Sledgehammer : SLEDGEHAMMER = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

60 
struct 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

61 

38028  62 
open ATP_Problem 
63 
open ATP_Systems 

37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

64 
open Metis_Clauses 
38023  65 
open Sledgehammer_Util 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36059
diff
changeset

66 
open Sledgehammer_Fact_Filter 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36059
diff
changeset

67 
open Sledgehammer_Proof_Reconstruct 
37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

68 

38023  69 

37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

70 
(** The Sledgehammer **) 
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

71 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

72 
(* Identifier to distinguish Sledgehammer from other tools using 
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

73 
"Async_Manager". *) 
37585  74 
val das_Tool = "Sledgehammer" 
75 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

76 
(* Freshness almost guaranteed! *) 
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

77 
val sledgehammer_weak_prefix = "Sledgehammer:" 
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

78 

37585  79 
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" 
80 
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" 

81 
val messages = Async_Manager.thread_messages das_Tool "ATP" 

35969  82 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

83 
(** problems, results, provers, etc. **) 
35969  84 

85 
type params = 

86 
{debug: bool, 

87 
verbose: bool, 

36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset

88 
overlord: bool, 
35969  89 
atps: string list, 
90 
full_types: bool, 

36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

91 
explicit_apply: bool, 
35969  92 
relevance_threshold: real, 
36922  93 
relevance_convergence: real, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36184
diff
changeset

94 
theory_relevant: bool option, 
36922  95 
defs_relevant: bool, 
35969  96 
isar_proof: bool, 
36924  97 
isar_shrink_factor: int, 
35969  98 
timeout: Time.time, 
99 
minimize_timeout: Time.time} 

35867  100 

101 
type problem = 

35969  102 
{subgoal: int, 
103 
goal: Proof.context * (thm list * thm), 

104 
relevance_override: relevance_override, 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

105 
axioms: (string * thm) list option} 
35867  106 

107 
type prover_result = 

36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

108 
{outcome: failure option, 
35969  109 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

110 
pool: string Symtab.table, 
38015  111 
used_thm_names: string list, 
35969  112 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

113 
output: string, 
35969  114 
proof: string, 
115 
internal_thm_names: string Vector.vector, 

38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

116 
conjecture_shape: int list list} 
35867  117 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

118 
type prover = params > minimize_command > problem > prover_result 
35867  119 

38023  120 
(* configuration attributes *) 
121 

122 
val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); 

123 
(*Empty string means create files in Isabelle's temporary files directory.*) 

124 

125 
val (problem_prefix, problem_prefix_setup) = 

126 
Attrib.config_string "atp_problem_prefix" (K "prob"); 

127 

128 
val (measure_runtime, measure_runtime_setup) = 

129 
Attrib.config_bool "atp_measure_runtime" (K false); 

28484  130 

38023  131 
fun with_path cleanup after f path = 
132 
Exn.capture f path 

133 
> tap (fn _ => cleanup path) 

134 
> Exn.release 

135 
> tap (after path) 

136 

137 
(* Splits by the first possible of a list of delimiters. *) 

138 
fun extract_proof delims output = 

139 
case pairself (find_first (fn s => String.isSubstring s output)) 

140 
(ListPair.unzip delims) of 

141 
(SOME begin_delim, SOME end_delim) => 

142 
(output > first_field begin_delim > the > snd 

143 
> first_field end_delim > the > fst 

144 
> first_field "\n" > the > snd 

145 
handle Option.Option => "") 

146 
 _ => "" 

28484  147 

38023  148 
fun extract_proof_and_outcome complete res_code proof_delims known_failures 
149 
output = 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

150 
case known_failure_in_output output known_failures of 
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

151 
NONE => (case extract_proof proof_delims output of 
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

152 
"" => ("", SOME MalformedOutput) 
38023  153 
 proof => if res_code = 0 then (proof, NONE) 
154 
else ("", SOME UnknownError)) 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

155 
 SOME failure => 
38023  156 
("", SOME (if failure = IncompleteUnprovable andalso complete then 
157 
Unprovable 

158 
else 

159 
failure)) 

28582  160 

28586
d238b83ba3fc
renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents:
28582
diff
changeset

161 

38023  162 
(* Clause preparation *) 
163 

164 
datatype fol_formula = 

165 
FOLFormula of {formula_name: string, 

166 
kind: kind, 

167 
combformula: (name, combterm) formula, 

168 
ctypes_sorts: typ list} 

169 

170 
fun mk_anot phi = AConn (ANot, [phi]) 

171 
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) 

172 
fun mk_ahorn [] phi = phi 

173 
 mk_ahorn (phi :: phis) psi = 

174 
AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) 

175 

176 
(* ### FIXME: reintroduce 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

177 
fun make_formula_table xs = 
38023  178 
fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

179 
(* Remove existing axioms from the conjecture, as this can 
38023  180 
dramatically boost an ATP's performance (for some reason). *) 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

181 
fun subtract_cls axioms = 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

182 
filter_out (Termtab.defined (make_formula_table axioms) o prop_of) 
38023  183 
*) 
184 

185 
fun combformula_for_prop thy = 

186 
let 

187 
val do_term = combterm_from_term thy 

188 
fun do_quant bs q s T t' = 

189 
do_formula ((s, T) :: bs) t' 

190 
#>> (fn phi => AQuant (q, [`make_bound_var s], phi)) 

191 
and do_conn bs c t1 t2 = 

192 
do_formula bs t1 ##>> do_formula bs t2 

193 
#>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) 

194 
and do_formula bs t = 

195 
case t of 

196 
@{const Not} $ t1 => 

197 
do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) 

198 
 Const (@{const_name All}, _) $ Abs (s, T, t') => 

199 
do_quant bs AForall s T t' 

200 
 Const (@{const_name Ex}, _) $ Abs (s, T, t') => 

201 
do_quant bs AExists s T t' 

202 
 @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 

203 
 @{const "op "} $ t1 $ t2 => do_conn bs AOr t1 t2 

204 
 @{const "op >"} $ t1 $ t2 => do_conn bs AImplies t1 t2 

205 
 Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => 

206 
do_conn bs AIff t1 t2 

207 
 _ => (fn ts => do_term bs (Envir.eta_contract t) 

38034  208 
>> AAtom > union (op =) ts) 
38023  209 
in do_formula [] end 
210 

211 
(* Converts an elimrule into an equivalent theorem that does not have the 

212 
predicate variable. Leaves other theorems unchanged. We simply instantiate 

213 
the conclusion variable to False. (Cf. "transform_elim_term" in 

214 
"ATP_Systems".) *) 

215 
(* FIXME: test! *) 

216 
fun transform_elim_term t = 

217 
case Logic.strip_imp_concl t of 

218 
@{const Trueprop} $ Var (z, @{typ bool}) => 

219 
subst_Vars [(z, @{const True})] t 

220 
 Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t 

221 
 _ => t 

222 

223 
(* Removes the lambdas from an equation of the form "t = (%x. u)". 

224 
(Cf. "extensionalize_theorem" in "Clausifier".) *) 

225 
fun extensionalize_term t = 

226 
let 

227 
fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _])) 

228 
$ t2 $ Abs (s, var_T, t')) = 

229 
let val var_t = Var (("x", j), var_T) in 

230 
Const (@{const_name "op ="}, T' > T' > HOLogic.boolT) 

231 
$ betapply (t2, var_t) $ subst_bound (var_t, t') 

232 
> aux (j + 1) 

233 
end 

234 
 aux _ t = t 

235 
in aux (maxidx_of_term t + 1) t end 

236 

38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

237 
fun presimplify_term thy = 
38091  238 
Skip_Proof.make_thm thy 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

239 
#> Meson.presimplify 
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

240 
#> prop_of 
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

241 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

242 
fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j 
38023  243 
fun conceal_bounds Ts t = 
244 
subst_bounds (map (Free o apfst concealed_bound_name) 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

245 
(0 upto length Ts  1 ~~ Ts), t) 
38023  246 
fun reveal_bounds Ts = 
247 
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) 

248 
(0 upto length Ts  1 ~~ Ts)) 

249 

250 
fun introduce_combinators_in_term ctxt kind t = 

251 
let 

252 
val thy = ProofContext.theory_of ctxt 

253 
fun aux Ts t = 

254 
case t of 

255 
@{const Not} $ t1 => @{const Not} $ aux Ts t1 

256 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 

257 
t0 $ Abs (s, T, aux (T :: Ts) t') 

258 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 

259 
t0 $ Abs (s, T, aux (T :: Ts) t') 

260 
 (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 

261 
 (t0 as @{const "op "}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 

262 
 (t0 as @{const "op >"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 

263 
 (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) 

264 
$ t1 $ t2 => 

265 
t0 $ aux Ts t1 $ aux Ts t2 

266 
 _ => if not (exists_subterm (fn Abs _ => true  _ => false) t) then 

267 
t 

268 
else 

269 
let 

270 
val t = t > conceal_bounds Ts 

271 
> Envir.eta_contract 

272 
val ([t], ctxt') = Variable.import_terms true [t] ctxt 

273 
in 

274 
t > cterm_of thy 

275 
> Clausifier.introduce_combinators_in_cterm 

276 
> singleton (Variable.export ctxt' ctxt) 

277 
> prop_of > Logic.dest_equals > snd 

278 
> reveal_bounds Ts 

279 
end 

280 
in t > not (Meson.is_fol_term thy t) ? aux [] end 

281 
handle THM _ => 

282 
(* A type variable of sort "{}" will make abstraction fail. *) 

283 
case kind of 

284 
Axiom => HOLogic.true_const 

285 
 Conjecture => HOLogic.false_const 

286 

38098
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

287 
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

288 
same in Sledgehammer to prevent the discovery of unreplable proofs. *) 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

289 
fun freeze_term t = 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

290 
let 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

291 
fun aux (t $ u) = aux t $ aux u 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

292 
 aux (Abs (s, T, t)) = Abs (s, T, aux t) 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

293 
 aux (Var ((s, i), T)) = 
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

294 
Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) 
38098
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

295 
 aux t = t 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

296 
in t > exists_subterm is_Var t ? aux end 
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

297 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

298 
(* making axiom and conjecture formulas *) 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

299 
fun make_formula ctxt presimp (formula_name, kind, t) = 
38023  300 
let 
301 
val thy = ProofContext.theory_of ctxt 

302 
val t = t > transform_elim_term 

303 
> Object_Logic.atomize_term thy 

38091  304 
val t = t > fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop 
38023  305 
> extensionalize_term 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

306 
> presimp ? presimplify_term thy 
38091  307 
> perhaps (try (HOLogic.dest_Trueprop)) 
38023  308 
> introduce_combinators_in_term ctxt kind 
38098
db90d313cf53
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
blanchet
parents:
38092
diff
changeset

309 
> kind = Conjecture ? freeze_term 
38023  310 
val (combformula, ctypes_sorts) = combformula_for_prop thy t [] 
311 
in 

312 
FOLFormula {formula_name = formula_name, combformula = combformula, 

313 
kind = kind, ctypes_sorts = ctypes_sorts} 

314 
end 

315 

38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

316 
fun make_axiom ctxt presimp (name, th) = 
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

317 
(name, make_formula ctxt presimp (name, Axiom, prop_of th)) 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

318 
fun make_conjectures ctxt ts = 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

319 
map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t)) 
38023  320 
(0 upto length ts  1) ts 
321 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

322 
(** Helper facts **) 
38023  323 

324 
fun count_combterm (CombConst ((s, _), _, _)) = 

325 
Symtab.map_entry s (Integer.add 1) 

326 
 count_combterm (CombVar _) = I 

327 
 count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] 

328 
fun count_combformula (AQuant (_, _, phi)) = count_combformula phi 

329 
 count_combformula (AConn (_, phis)) = fold count_combformula phis 

38034  330 
 count_combformula (AAtom tm) = count_combterm tm 
38023  331 
fun count_fol_formula (FOLFormula {combformula, ...}) = 
332 
count_combformula combformula 

333 

334 
val optional_helpers = 

335 
[(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), 

336 
(["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), 

337 
(["c_COMBS"], @{thms COMBS_def})] 

338 
val optional_typed_helpers = 

339 
[(["c_True", "c_False"], @{thms True_or_False}), 

340 
(["c_If"], @{thms if_True if_False True_or_False})] 

341 
val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} 

342 

343 
val init_counters = 

344 
Symtab.make (maps (maps (map (rpair 0) o fst)) 

345 
[optional_helpers, optional_typed_helpers]) 

346 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

347 
fun get_helper_facts ctxt is_FO full_types conjectures axioms = 
38023  348 
let 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

349 
val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters 
38023  350 
fun is_needed c = the (Symtab.lookup ct c) > 0 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

351 
in 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

352 
(optional_helpers 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

353 
> full_types ? append optional_typed_helpers 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

354 
> maps (fn (ss, ths) => 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

355 
if exists is_needed ss then map (`Thm.get_name_hint) ths 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

356 
else [])) @ 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

357 
(if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

358 
> map (snd o make_axiom ctxt false) 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

359 
end 
38023  360 

38086  361 
fun meta_not t = @{const "==>"} $ t $ @{prop False} 
38023  362 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

363 
fun prepare_formulas ctxt full_types hyp_ts concl_t axcls = 
38023  364 
let 
365 
val thy = ProofContext.theory_of ctxt 

366 
val goal_t = Logic.list_implies (hyp_ts, concl_t) 

367 
val is_FO = Meson.is_fol_term thy goal_t 

38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

368 
val axtms = map (prop_of o snd) axcls 
38023  369 
val subs = tfree_classes_of_terms [goal_t] 
370 
val supers = tvar_classes_of_terms axtms 

371 
val tycons = type_consts_of_terms thy (goal_t :: axtms) 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

372 
(* TFrees in the conjecture; TVars in the axioms *) 
38086  373 
val conjectures = map meta_not hyp_ts @ [concl_t] > make_conjectures ctxt 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
38088
diff
changeset

374 
val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls) 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

375 
val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms 
38023  376 
val (supers', arity_clauses) = make_arity_clauses thy tycons supers 
377 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 

378 
in 

379 
(Vector.fromList clnames, 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

380 
(conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) 
38023  381 
end 
382 

383 
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) 

384 

385 
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) 

386 
 fo_term_for_combtyp (CombTFree name) = ATerm (name, []) 

387 
 fo_term_for_combtyp (CombType (name, tys)) = 

388 
ATerm (name, map fo_term_for_combtyp tys) 

389 

390 
fun fo_literal_for_type_literal (TyLitVar (class, name)) = 

391 
(true, ATerm (class, [ATerm (name, [])])) 

392 
 fo_literal_for_type_literal (TyLitFree (class, name)) = 

393 
(true, ATerm (class, [ATerm (name, [])])) 

394 

38034  395 
fun formula_for_fo_literal (pos, t) = AAtom t > not pos ? mk_anot 
38023  396 

397 
fun fo_term_for_combterm full_types = 

398 
let 

399 
fun aux top_level u = 

400 
let 

401 
val (head, args) = strip_combterm_comb u 

402 
val (x, ty_args) = 

403 
case head of 

38087
dddb8ba3a1ce
generate correct names for "$true" and "$false";
blanchet
parents:
38086
diff
changeset

404 
CombConst (name as (s, s'), _, ty_args) => 
38088
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

405 
if s = "equal" then 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

406 
(if top_level andalso length args = 2 then name 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

407 
else ("c_fequal", @{const_name fequal}), []) 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

408 
else if top_level then 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

409 
case s of 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

410 
"c_False" => (("$false", s'), []) 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

411 
 "c_True" => (("$true", s'), []) 
a9847fb539dd
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
blanchet
parents:
38087
diff
changeset

412 
 _ => (name, if full_types then [] else ty_args) 
38023  413 
else 
414 
(name, if full_types then [] else ty_args) 

415 
 CombVar (name, _) => (name, []) 

416 
 CombApp _ => raise Fail "impossible \"CombApp\"" 

417 
val t = ATerm (x, map fo_term_for_combtyp ty_args @ 

418 
map (aux false) args) 

419 
in 

420 
if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t 

421 
end 

422 
in aux true end 

423 

424 
fun formula_for_combformula full_types = 

425 
let 

426 
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) 

427 
 aux (AConn (c, phis)) = AConn (c, map aux phis) 

38034  428 
 aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) 
38023  429 
in aux end 
430 

431 
fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = 

432 
mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) 

433 
(type_literals_for_types ctypes_sorts)) 

434 
(formula_for_combformula full_types combformula) 

435 

436 
fun problem_line_for_axiom full_types 

437 
(formula as FOLFormula {formula_name, kind, ...}) = 

438 
Fof (axiom_prefix ^ ascii_of formula_name, kind, 

439 
formula_for_axiom full_types formula) 

440 

441 
fun problem_line_for_class_rel_clause 

442 
(ClassRelClause {axiom_name, subclass, superclass, ...}) = 

443 
let val ty_arg = ATerm (("T", "T"), []) in 

444 
Fof (ascii_of axiom_name, Axiom, 

38034  445 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
446 
AAtom (ATerm (superclass, [ty_arg]))])) 

38023  447 
end 
448 

449 
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = 

450 
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) 

451 
 fo_literal_for_arity_literal (TVarLit (c, sort)) = 

452 
(false, ATerm (c, [ATerm (sort, [])])) 

453 

454 
fun problem_line_for_arity_clause 

455 
(ArityClause {axiom_name, conclLit, premLits, ...}) = 

456 
Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, 

457 
mk_ahorn (map (formula_for_fo_literal o apfst not 

458 
o fo_literal_for_arity_literal) premLits) 

459 
(formula_for_fo_literal 

460 
(fo_literal_for_arity_literal conclLit))) 

461 

462 
fun problem_line_for_conjecture full_types 

463 
(FOLFormula {formula_name, kind, combformula, ...}) = 

464 
Fof (conjecture_prefix ^ formula_name, kind, 

465 
formula_for_combformula full_types combformula) 

466 

467 
fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = 

468 
map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) 

469 

470 
fun problem_line_for_free_type lit = 

471 
Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) 

472 
fun problem_lines_for_free_types conjectures = 

473 
let 

474 
val litss = map free_type_literals_for_conjecture conjectures 

475 
val lits = fold (union (op =)) litss [] 

476 
in map problem_line_for_free_type lits end 

477 

478 
(** "hBOOL" and "hAPP" **) 

479 

480 
type const_info = {min_arity: int, max_arity: int, sub_level: bool} 

481 

482 
fun consider_term top_level (ATerm ((s, _), ts)) = 

483 
(if is_tptp_variable s then 

484 
I 

485 
else 

486 
let val n = length ts in 

487 
Symtab.map_default 

488 
(s, {min_arity = n, max_arity = 0, sub_level = false}) 

489 
(fn {min_arity, max_arity, sub_level} => 

490 
{min_arity = Int.min (n, min_arity), 

491 
max_arity = Int.max (n, max_arity), 

492 
sub_level = sub_level orelse not top_level}) 

493 
end) 

494 
#> fold (consider_term (top_level andalso s = type_wrapper_name)) ts 

495 
fun consider_formula (AQuant (_, _, phi)) = consider_formula phi 

496 
 consider_formula (AConn (_, phis)) = fold consider_formula phis 

38034  497 
 consider_formula (AAtom tm) = consider_term true tm 
38023  498 

499 
fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi 

500 
fun consider_problem problem = fold (fold consider_problem_line o snd) problem 

501 

502 
fun const_table_for_problem explicit_apply problem = 

503 
if explicit_apply then NONE 

504 
else SOME (Symtab.empty > consider_problem problem) 

505 

506 
val tc_fun = make_fixed_type_const @{type_name fun} 

507 

508 
fun min_arity_of thy full_types NONE s = 

509 
(if s = "equal" orelse s = type_wrapper_name orelse 

510 
String.isPrefix type_const_prefix s orelse 

511 
String.isPrefix class_prefix s then 

512 
16383 (* large number *) 

513 
else if full_types then 

514 
0 

515 
else case strip_prefix_and_undo_ascii const_prefix s of 

516 
SOME s' => num_type_args thy (invert_const s') 

517 
 NONE => 0) 

518 
 min_arity_of _ _ (SOME the_const_tab) s = 

519 
case Symtab.lookup the_const_tab s of 

520 
SOME ({min_arity, ...} : const_info) => min_arity 

521 
 NONE => 0 

522 

523 
fun full_type_of (ATerm ((s, _), [ty, _])) = 

524 
if s = type_wrapper_name then ty else raise Fail "expected type wrapper" 

525 
 full_type_of _ = raise Fail "expected type wrapper" 

526 

527 
fun list_hAPP_rev _ t1 [] = t1 

528 
 list_hAPP_rev NONE t1 (t2 :: ts2) = 

529 
ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) 

530 
 list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = 

531 
let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, 

532 
[full_type_of t2, ty]) in 

533 
ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) 

534 
end 

535 

536 
fun repair_applications_in_term thy full_types const_tab = 

537 
let 

538 
fun aux opt_ty (ATerm (name as (s, _), ts)) = 

539 
if s = type_wrapper_name then 

540 
case ts of 

541 
[t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) 

542 
 _ => raise Fail "malformed type wrapper" 

543 
else 

544 
let 

545 
val ts = map (aux NONE) ts 

546 
val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts 

547 
in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end 

548 
in aux NONE end 

549 

550 
fun boolify t = ATerm (`I "hBOOL", [t]) 

551 

552 
(* True if the constant ever appears outside of the toplevel position in 

553 
literals, or if it appears with different arities (e.g., because of different 

554 
type instantiations). If false, the constant always receives all of its 

555 
arguments and is used as a predicate. *) 

556 
fun is_predicate NONE s = 

557 
s = "equal" orelse String.isPrefix type_const_prefix s orelse 

558 
String.isPrefix class_prefix s 

559 
 is_predicate (SOME the_const_tab) s = 

560 
case Symtab.lookup the_const_tab s of 

561 
SOME {min_arity, max_arity, sub_level} => 

562 
not sub_level andalso min_arity = max_arity 

563 
 NONE => false 

564 

565 
fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = 

566 
if s = type_wrapper_name then 

567 
case ts of 

568 
[_, t' as ATerm ((s', _), _)] => 

569 
if is_predicate const_tab s' then t' else boolify t 

570 
 _ => raise Fail "malformed type wrapper" 

571 
else 

572 
t > not (is_predicate const_tab s) ? boolify 

573 

574 
fun close_universally phi = 

575 
let 

576 
fun term_vars bounds (ATerm (name as (s, _), tms)) = 

577 
(is_tptp_variable s andalso not (member (op =) bounds name)) 

578 
? insert (op =) name 

579 
#> fold (term_vars bounds) tms 

580 
fun formula_vars bounds (AQuant (q, xs, phi)) = 

581 
formula_vars (xs @ bounds) phi 

582 
 formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis 

38034  583 
 formula_vars bounds (AAtom tm) = term_vars bounds tm 
38023  584 
in 
585 
case formula_vars [] phi [] of [] => phi  xs => AQuant (AForall, xs, phi) 

586 
end 

587 

588 
fun repair_formula thy explicit_forall full_types const_tab = 

589 
let 

590 
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) 

591 
 aux (AConn (c, phis)) = AConn (c, map aux phis) 

38034  592 
 aux (AAtom tm) = 
593 
AAtom (tm > repair_applications_in_term thy full_types const_tab 

38023  594 
> repair_predicates_in_term const_tab) 
595 
in aux #> explicit_forall ? close_universally end 

596 

597 
fun repair_problem_line thy explicit_forall full_types const_tab 

598 
(Fof (ident, kind, phi)) = 

599 
Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) 

600 
fun repair_problem_with_const_table thy = 

601 
map o apsnd o map ooo repair_problem_line thy 

602 

603 
fun repair_problem thy explicit_forall full_types explicit_apply problem = 

604 
repair_problem_with_const_table thy explicit_forall full_types 

605 
(const_table_for_problem explicit_apply problem) problem 

606 

607 
fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

608 
file (conjectures, axioms, helper_facts, class_rel_clauses, 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

609 
arity_clauses) = 
38023  610 
let 
38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

611 
val axiom_lines = map (problem_line_for_axiom full_types) axioms 
38023  612 
val class_rel_lines = 
613 
map problem_line_for_class_rel_clause class_rel_clauses 

614 
val arity_lines = map problem_line_for_arity_clause arity_clauses 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

615 
val helper_lines = map (problem_line_for_axiom full_types) helper_facts 
38023  616 
val conjecture_lines = 
617 
map (problem_line_for_conjecture full_types) conjectures 

618 
val tfree_lines = problem_lines_for_free_types conjectures 

619 
(* Reordering these might or might not confuse the proof reconstruction 

620 
code or the SPASS Flotter hack. *) 

621 
val problem = 

622 
[("Relevant facts", axiom_lines), 

623 
("Class relationships", class_rel_lines), 

624 
("Arity declarations", arity_lines), 

625 
("Helper facts", helper_lines), 

626 
("Conjectures", conjecture_lines), 

627 
("Type variables", tfree_lines)] 

628 
> repair_problem thy explicit_forall full_types explicit_apply 

629 
val (problem, pool) = nice_tptp_problem readable_names problem 

630 
val conjecture_offset = 

631 
length axiom_lines + length class_rel_lines + length arity_lines 

632 
+ length helper_lines 

633 
val _ = File.write_list file (strings_for_tptp_problem problem) 

634 
in 

635 
(case pool of SOME the_pool => snd the_pool  NONE => Symtab.empty, 

636 
conjecture_offset) 

637 
end 

638 

639 
fun extract_clause_sequence output = 

640 
let 

641 
val tokens_of = String.tokens (not o Char.isAlphaNum) 

642 
fun extract_num ("clause" :: (ss as _ :: _)) = 

643 
Int.fromString (List.last ss) 

644 
 extract_num _ = NONE 

645 
in output > split_lines > map_filter (extract_num o tokens_of) end 

646 

647 
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" 

648 

649 
val parse_clause_formula_pair = 

650 
$$ "("  scan_integer  $$ ","  Symbol.scan_id  $$ ")" 

651 
 Scan.option ($$ ",") 

652 
val parse_clause_formula_relation = 

653 
Scan.this_string set_ClauseFormulaRelationN  $$ "(" 

654 
 Scan.repeat parse_clause_formula_pair 

655 
val extract_clause_formula_relation = 

656 
Substring.full 

657 
#> Substring.position set_ClauseFormulaRelationN 

658 
#> snd #> Substring.string #> strip_spaces #> explode 

659 
#> parse_clause_formula_relation #> fst 

660 

661 
fun repair_conjecture_shape_and_theorem_names output conjecture_shape 

662 
thm_names = 

663 
if String.isSubstring set_ClauseFormulaRelationN output then 

664 
(* This is a hack required for keeping track of axioms after they have been 

665 
clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part 

666 
of this hack. *) 

667 
let 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

668 
val j0 = hd (hd conjecture_shape) 
38023  669 
val seq = extract_clause_sequence output 
670 
val name_map = extract_clause_formula_relation output 

671 
fun renumber_conjecture j = 

672 
AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j  j0)) 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

673 
> map (fn s => find_index (curry (op =) s) seq + 1) 
38023  674 
in 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

675 
(conjecture_shape > map (maps renumber_conjecture), 
38023  676 
seq > map (the o AList.lookup (op =) name_map) 
677 
> map (fn s => case try (unprefix axiom_prefix) s of 

678 
SOME s' => undo_ascii_of s' 

679 
 NONE => "") 

680 
> Vector.fromList) 

681 
end 

682 
else 

683 
(conjecture_shape, thm_names) 

684 

685 

686 
(* generic TPTPbased provers *) 

687 

688 
fun prover_fun name 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

689 
{exec, required_execs, arguments, proof_delims, known_failures, 
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

690 
max_new_relevant_facts_per_iter, prefers_theory_relevant, 
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

691 
explicit_forall} 
38023  692 
({debug, overlord, full_types, explicit_apply, relevance_threshold, 
693 
relevance_convergence, theory_relevant, defs_relevant, isar_proof, 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

694 
isar_shrink_factor, timeout, ...} : params) 
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

695 
minimize_command 
38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

696 
({subgoal, goal, relevance_override, axioms} : problem) = 
38023  697 
let 
698 
val (ctxt, (_, th)) = goal; 

699 
val thy = ProofContext.theory_of ctxt 

700 
(* ### FIXME: (1) preprocessing for "if" etc. *) 

701 
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

702 
val the_axioms = 
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

703 
case axioms of 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

704 
SOME axioms => axioms 
38023  705 
 NONE => relevant_facts full_types relevance_threshold 
706 
relevance_convergence defs_relevant 

707 
max_new_relevant_facts_per_iter 

708 
(the_default prefers_theory_relevant theory_relevant) 

709 
relevance_override goal hyp_ts concl_t 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

710 
val (internal_thm_names, formulas) = 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

711 
prepare_formulas ctxt full_types hyp_ts concl_t the_axioms 
38023  712 

713 
(* path to unique problem file *) 

714 
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" 

715 
else Config.get ctxt dest_dir; 

716 
val the_problem_prefix = Config.get ctxt problem_prefix; 

717 
fun prob_pathname nr = 

718 
let 

719 
val probfile = 

720 
Path.basic ((if overlord then "prob_" ^ name 

721 
else the_problem_prefix ^ serial_string ()) 

722 
^ "_" ^ string_of_int nr) 

723 
in 

724 
if the_dest_dir = "" then File.tmp_path probfile 

725 
else if File.exists (Path.explode the_dest_dir) 

726 
then Path.append (Path.explode the_dest_dir) probfile 

727 
else error ("No such directory: " ^ the_dest_dir ^ ".") 

728 
end; 

729 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

730 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
38023  731 
(* write out problem file and call prover *) 
732 
fun command_line complete probfile = 

733 
let 

734 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

735 
" " ^ File.shell_path probfile 

736 
in 

737 
(if Config.get ctxt measure_runtime then 

738 
"TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" 

739 
else 

740 
"exec " ^ core) ^ " 2>&1" 

741 
end 

742 
fun split_time s = 

743 
let 

744 
val split = String.tokens (fn c => str c = "\n"); 

745 
val (output, t) = s > split > split_last > apfst cat_lines; 

746 
fun as_num f = f >> (fst o read_int); 

747 
val num = as_num (Scan.many1 Symbol.is_ascii_digit); 

748 
val digit = Scan.one Symbol.is_ascii_digit; 

749 
val num3 = as_num (digit ::: digit ::: (digit >> single)); 

750 
val time = num  Scan.$$ "."  num3 >> (fn (a, b) => a * 1000 + b); 

751 
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; 

752 
in (output, as_time t) end; 

753 
fun run_on probfile = 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

754 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  755 
(home_var, _) :: _ => 
38023  756 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  757 
 [] => 
758 
if File.exists command then 

759 
let 

760 
fun do_run complete = 

761 
let 

762 
val command = command_line complete probfile 

763 
val ((output, msecs), res_code) = 

764 
bash_output command 

765 
>> (if overlord then 

766 
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") 

767 
else 

768 
I) 

769 
>> (if Config.get ctxt measure_runtime then split_time 

770 
else rpair 0) 

771 
val (proof, outcome) = 

772 
extract_proof_and_outcome complete res_code proof_delims 

773 
known_failures output 

774 
in (output, msecs, proof, outcome) end 

775 
val readable_names = debug andalso overlord 

776 
val (pool, conjecture_offset) = 

777 
write_tptp_file thy readable_names explicit_forall full_types 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38084
diff
changeset

778 
explicit_apply probfile formulas 
38032  779 
val conjecture_shape = 
780 
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

781 
> map single 
38032  782 
val result = 
783 
do_run false 

784 
> (fn (_, msecs0, _, SOME _) => 

785 
do_run true 

786 
> (fn (output, msecs, proof, outcome) => 

787 
(output, msecs0 + msecs, proof, outcome)) 

788 
 result => result) 

789 
in ((pool, conjecture_shape), result) end 

790 
else 

791 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  792 

793 
(* If the problem file has not been exported, remove it; otherwise, export 

794 
the proof file too. *) 

795 
fun cleanup probfile = 

796 
if the_dest_dir = "" then try File.rm probfile else NONE 

797 
fun export probfile (_, (output, _, _, _)) = 

798 
if the_dest_dir = "" then 

799 
() 

800 
else 

801 
File.write (Path.explode (Path.implode probfile ^ "_proof")) output 

802 

803 
val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = 

804 
with_path cleanup export run_on (prob_pathname subgoal) 

805 
val (conjecture_shape, internal_thm_names) = 

806 
repair_conjecture_shape_and_theorem_names output conjecture_shape 

807 
internal_thm_names 

808 

809 
val (message, used_thm_names) = 

810 
case outcome of 

811 
NONE => 

812 
proof_text isar_proof 

813 
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 

814 
(full_types, minimize_command, proof, internal_thm_names, th, 

815 
subgoal) 

816 
 SOME failure => (string_for_failure failure ^ "\n", []) 

817 
in 

818 
{outcome = outcome, message = message, pool = pool, 

819 
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, 

820 
output = output, proof = proof, internal_thm_names = internal_thm_names, 

38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

821 
conjecture_shape = conjecture_shape} 
38023  822 
end 
823 

824 
fun get_prover_fun thy name = prover_fun name (get_prover thy name) 

825 

37584  826 
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n 
827 
relevance_override minimize_command proof_state name = 

36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

828 
let 
38023  829 
val thy = Proof.theory_of proof_state 
37584  830 
val birth_time = Time.now () 
831 
val death_time = Time.+ (birth_time, timeout) 

38023  832 
val prover = get_prover_fun thy name 
36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

833 
val {context = ctxt, facts, goal} = Proof.goal proof_state; 
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

834 
val desc = 
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

835 
"ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ 
36392  836 
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); 
37584  837 
in 
37585  838 
Async_Manager.launch das_Tool verbose birth_time death_time desc 
37584  839 
(fn () => 
840 
let 

841 
val problem = 

842 
{subgoal = i, goal = (ctxt, (facts, goal)), 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

843 
relevance_override = relevance_override, axioms = NONE} 
37584  844 
in 
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

845 
prover params (minimize_command name) problem > #message 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37926
diff
changeset

846 
handle ERROR message => "Error: " ^ message ^ "\n" 
37584  847 
end) 
848 
end 

28582  849 

38044  850 
fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set." 
851 
 run_sledgehammer (params as {atps, ...}) i relevance_override 

852 
minimize_command state = 

853 
case subgoal_count state of 

854 
0 => priority "No subgoal!" 

855 
 n => 

856 
let 

857 
val _ = kill_atps () 

858 
val _ = priority "Sledgehammering..." 

859 
val _ = app (start_prover_thread params i n relevance_override 

860 
minimize_command state) atps 

861 
in () end 

862 

38023  863 
val setup = 
864 
dest_dir_setup 

865 
#> problem_prefix_setup 

866 
#> measure_runtime_setup 

867 

28582  868 
end; 