1.1 --- a/src/HOL/TPTP/atp_export.ML Fri Nov 18 06:50:05 2011 +0100
1.2 +++ b/src/HOL/TPTP/atp_export.ML Fri Nov 18 11:47:12 2011 +0100
1.3 @@ -175,13 +175,14 @@
1.4 val path = file_name |> Path.explode
1.5 val _ = File.write path ""
1.6 val facts = facts_of thy
1.7 - val (atp_problem, _, _, _, _, _, _, _) =
1.8 + val atp_problem =
1.9 facts
1.10 |> map (fn ((_, loc), th) =>
1.11 ((Thm.get_name_hint th, loc),
1.12 th |> prop_of |> mono ? monomorphize_term ctxt))
1.13 |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN
1.14 false true [] @{prop False}
1.15 + |> #1
1.16 val atp_problem =
1.17 atp_problem
1.18 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Nov 18 06:50:05 2011 +0100
2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Nov 18 11:47:12 2011 +0100
2.3 @@ -33,7 +33,7 @@
2.4 InternalError |
2.5 UnknownError of string
2.6
2.7 - type step_name = string * string list option
2.8 + type step_name = string * string list
2.9
2.10 datatype 'a step =
2.11 Definition of step_name * 'a * 'a |
2.12 @@ -187,7 +187,7 @@
2.13 | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
2.14 | (tstplike_proof, _) => (tstplike_proof, NONE)
2.15
2.16 -type step_name = string * string list option
2.17 +type step_name = string * string list
2.18
2.19 fun is_same_atp_step (s1, _) (s2, _) = s1 = s2
2.20
2.21 @@ -375,7 +375,7 @@
2.22
2.23 fun find_formula_in_problem problem phi =
2.24 problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
2.25 - |> try (single o hd)
2.26 + |> try (single o hd) |> the_default []
2.27
2.28 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
2.29 <formula> <extra_arguments>\).
2.30 @@ -396,11 +396,11 @@
2.31 if s = waldmeister_conjecture then
2.32 find_formula_in_problem problem (mk_anot phi)
2.33 else
2.34 - SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]), "",
2.35 + [s |> perhaps (try (unprefix tofof_fact_prefix))]), "",
2.36 [])
2.37 | File_Source _ =>
2.38 ((num, find_formula_in_problem problem phi), "", [])
2.39 - | Inference_Source (rule, deps) => ((num, NONE), rule, deps)
2.40 + | Inference_Source (rule, deps) => ((num, []), rule, deps)
2.41 in
2.42 case role of
2.43 "definition" =>
2.44 @@ -409,9 +409,9 @@
2.45 Definition (name, phi1, phi2)
2.46 | AAtom (ATerm ("equal", _)) =>
2.47 (* Vampire's equality proxy axiom *)
2.48 - Inference (name, phi, rule, map (rpair NONE) deps)
2.49 + Inference (name, phi, rule, map (rpair []) deps)
2.50 | _ => raise UNRECOGNIZED_ATP_PROOF ())
2.51 - | _ => Inference (name, phi, rule, map (rpair NONE) deps)
2.52 + | _ => Inference (name, phi, rule, map (rpair []) deps)
2.53 end)
2.54
2.55 (**** PARSING OF SPASS OUTPUT ****)
2.56 @@ -445,10 +445,10 @@
2.57 fun resolve_spass_num spass_names num =
2.58 case Int.fromString num of
2.59 SOME j => if j > 0 andalso j <= Vector.length spass_names then
2.60 - SOME (Vector.sub (spass_names, j - 1))
2.61 + Vector.sub (spass_names, j - 1)
2.62 else
2.63 - NONE
2.64 - | NONE => NONE
2.65 + []
2.66 + | NONE => []
2.67
2.68 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
2.69 fun parse_spass_line spass_names =
2.70 @@ -461,7 +461,7 @@
2.71 (* Syntax: <name> *)
2.72 fun parse_satallax_line x =
2.73 (scan_general_id --| Scan.option ($$ " ")
2.74 - >> (fn s => Inference ((s, SOME [s]), dummy_phi, "", []))) x
2.75 + >> (fn s => Inference ((s, [s]), dummy_phi, "", []))) x
2.76
2.77 fun parse_line problem spass_names =
2.78 parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
3.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 06:50:05 2011 +0100
3.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100
3.3 @@ -26,8 +26,8 @@
3.4 type one_line_params =
3.5 play * string * (string * locality) list * minimize_command * int * int
3.6 type isar_params =
3.7 - bool * bool * int * string Symtab.table * int list list * int
3.8 - * (string * locality) list vector * int Symtab.table * string proof * thm
3.9 + bool * bool * int * string Symtab.table * (string * locality) list vector
3.10 + * int Symtab.table * string proof * thm
3.11
3.12 val metisN : string
3.13 val smtN : string
3.14 @@ -41,12 +41,12 @@
3.15 val full_type_encs : string list
3.16 val partial_type_encs : string list
3.17 val used_facts_in_atp_proof :
3.18 - Proof.context -> int -> (string * locality) list vector -> string proof
3.19 + Proof.context -> (string * locality) list vector -> string proof
3.20 -> (string * locality) list
3.21 val used_facts_in_unsound_atp_proof :
3.22 - Proof.context -> int list list -> int -> (string * locality) list vector
3.23 - -> 'a proof -> string list option
3.24 - val uses_typed_helpers : int list -> 'a proof -> bool
3.25 + Proof.context -> (string * locality) list vector -> 'a proof
3.26 + -> string list option
3.27 + val uses_typed_helpers : 'a proof -> bool
3.28 val unalias_type_enc : string -> string list
3.29 val metis_default_lam_trans : string
3.30 val metis_call : string -> string -> string
3.31 @@ -87,11 +87,8 @@
3.32 type one_line_params =
3.33 play * string * (string * locality) list * minimize_command * int * int
3.34 type isar_params =
3.35 - bool * bool * int * string Symtab.table * int list list * int
3.36 - * (string * locality) list vector * int Symtab.table * string proof * thm
3.37 -
3.38 -val is_typed_helper_name =
3.39 - String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
3.40 + bool * bool * int * string Symtab.table * (string * locality) list vector
3.41 + * int Symtab.table * string proof * thm
3.42
3.43 fun find_first_in_list_vector vec key =
3.44 Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
3.45 @@ -99,11 +96,6 @@
3.46
3.47 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
3.48
3.49 -val vampire_step_prefix = "f" (* grrr... *)
3.50 -
3.51 -val extract_step_number =
3.52 - Int.fromString o perhaps (try (unprefix vampire_step_prefix))
3.53 -
3.54 fun resolve_one_named_fact fact_names s =
3.55 case try (unprefix fact_prefix) s of
3.56 SOME s' =>
3.57 @@ -111,43 +103,22 @@
3.58 s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
3.59 end
3.60 | NONE => NONE
3.61 -fun resolve_fact _ fact_names (_, SOME ss) =
3.62 - map_filter (resolve_one_named_fact fact_names) ss
3.63 - | resolve_fact facts_offset fact_names (num, NONE) =
3.64 - (case extract_step_number num of
3.65 - SOME j =>
3.66 - let val j = j - facts_offset in
3.67 - if j > 0 andalso j <= Vector.length fact_names then
3.68 - Vector.sub (fact_names, j - 1)
3.69 - else
3.70 - []
3.71 - end
3.72 - | NONE => [])
3.73 -
3.74 -fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
3.75 +fun resolve_fact fact_names (_, ss) =
3.76 + map_filter (resolve_one_named_fact fact_names) ss
3.77 +val is_fact = not o null oo resolve_fact
3.78
3.79 fun resolve_one_named_conjecture s =
3.80 case try (unprefix conjecture_prefix) s of
3.81 SOME s' => Int.fromString s'
3.82 | NONE => NONE
3.83
3.84 -fun resolve_conjecture _ (_, SOME ss) =
3.85 - map_filter resolve_one_named_conjecture ss
3.86 - | resolve_conjecture conjecture_shape (num, NONE) =
3.87 - case extract_step_number num of
3.88 - SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
3.89 - ~1 => []
3.90 - | j => [j])
3.91 - | NONE => []
3.92 +fun resolve_conjecture (_, ss) = map_filter resolve_one_named_conjecture ss
3.93 +val is_conjecture = not o null o resolve_conjecture
3.94
3.95 -fun is_conjecture conjecture_shape =
3.96 - not o null o resolve_conjecture conjecture_shape
3.97 -
3.98 -fun is_typed_helper _ (_, SOME ss) = exists is_typed_helper_name ss
3.99 - | is_typed_helper typed_helpers (num, NONE) =
3.100 - (case extract_step_number num of
3.101 - SOME i => member (op =) typed_helpers i
3.102 - | NONE => false)
3.103 +val is_typed_helper_name =
3.104 + String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
3.105 +fun is_typed_helper (_, ss) = exists is_typed_helper_name ss
3.106 + | is_typed_helper _ = false
3.107
3.108 val leo2_ext = "extcnf_equal_neg"
3.109 val isa_ext = Thm.get_name_hint @{thm ext}
3.110 @@ -160,19 +131,20 @@
3.111 else
3.112 isa_ext
3.113
3.114 -fun add_fact _ facts_offset fact_names (Inference (name, _, _, [])) =
3.115 - union (op =) (resolve_fact facts_offset fact_names name)
3.116 - | add_fact ctxt _ _ (Inference (_, _, rule, _)) =
3.117 +fun add_fact _ fact_names (Inference (name, _, _, [])) =
3.118 + union (op =) (resolve_fact fact_names name)
3.119 + | add_fact ctxt _ (Inference (_, _, rule, _)) =
3.120 if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
3.121 - | add_fact _ _ _ _ = I
3.122 + | add_fact _ _ _ = I
3.123
3.124 -fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof =
3.125 +fun used_facts_in_atp_proof ctxt fact_names atp_proof =
3.126 if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
3.127 - else fold (add_fact ctxt facts_offset fact_names) atp_proof []
3.128 + else fold (add_fact ctxt fact_names) atp_proof []
3.129
3.130 -fun is_conjecture_used_in_proof conjecture_shape =
3.131 - exists (fn Inference (name, _, _, []) => is_conjecture conjecture_shape name
3.132 - | _ => false)
3.133 +(* FIXME ### merge with other similar functions *)
3.134 +fun is_conjecture_used_in_proof proof =
3.135 + exists (fn Inference (name, _, _, []) => is_conjecture name | _ => false)
3.136 + proof
3.137
3.138 (* (quasi-)underapproximation of the truth *)
3.139 fun is_locality_global Local = false
3.140 @@ -180,23 +152,21 @@
3.141 | is_locality_global Chained = false
3.142 | is_locality_global _ = true
3.143
3.144 -fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE
3.145 - | used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset
3.146 - fact_names atp_proof =
3.147 +fun used_facts_in_unsound_atp_proof _ _ [] = NONE
3.148 + | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
3.149 let
3.150 - val used_facts =
3.151 - used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
3.152 + val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
3.153 in
3.154 if forall (is_locality_global o snd) used_facts andalso
3.155 - not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
3.156 + not (is_conjecture_used_in_proof atp_proof) then
3.157 SOME (map fst used_facts)
3.158 else
3.159 NONE
3.160 end
3.161
3.162 -fun uses_typed_helpers typed_helpers =
3.163 - exists (fn Inference (name, _, _, []) => is_typed_helper typed_helpers name
3.164 - | _ => false)
3.165 +fun uses_typed_helpers proof =
3.166 + exists (fn Inference (name, _, _, []) => is_typed_helper name | _ => false)
3.167 + proof
3.168
3.169
3.170 (** Soft-core proof reconstruction: one-liners **)
3.171 @@ -311,8 +281,8 @@
3.172 val assum_prefix = "A"
3.173 val have_prefix = "F"
3.174
3.175 -fun raw_label_for_name conjecture_shape name =
3.176 - case resolve_conjecture conjecture_shape name of
3.177 +fun raw_label_for_name name =
3.178 + case resolve_conjecture name of
3.179 [j] => (conjecture_prefix, j)
3.180 | _ => case Int.fromString (fst name) of
3.181 SOME j => (raw_prefix, j)
3.182 @@ -619,8 +589,8 @@
3.183
3.184 (* Discard facts; consolidate adjacent lines that prove the same formula, since
3.185 they differ only in type information.*)
3.186 -fun add_line _ _ (line as Definition _) lines = line :: lines
3.187 - | add_line conjecture_shape fact_names (Inference (name, t, rule, [])) lines =
3.188 +fun add_line _ (line as Definition _) lines = line :: lines
3.189 + | add_line fact_names (Inference (name, t, rule, [])) lines =
3.190 (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
3.191 definitions. *)
3.192 if is_fact fact_names name then
3.193 @@ -633,11 +603,11 @@
3.194 | (pre, Inference (name', _, _, _) :: post) =>
3.195 pre @ map (replace_dependencies_in_line (name', [name])) post
3.196 | _ => raise Fail "unexpected inference"
3.197 - else if is_conjecture conjecture_shape name then
3.198 + else if is_conjecture name then
3.199 Inference (name, s_not t, rule, []) :: lines
3.200 else
3.201 map (replace_dependencies_in_line (name, [])) lines
3.202 - | add_line _ _ (Inference (name, t, rule, deps)) lines =
3.203 + | add_line _ (Inference (name, t, rule, deps)) lines =
3.204 (* Type information will be deleted later; skip repetition test. *)
3.205 if is_only_type_information t then
3.206 Inference (name, t, rule, deps) :: lines
3.207 @@ -665,13 +635,13 @@
3.208 fun is_bad_free frees (Free x) = not (member (op =) frees x)
3.209 | is_bad_free _ _ = false
3.210
3.211 -fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
3.212 +fun add_desired_line _ _ _ (line as Definition (name, _, _)) (j, lines) =
3.213 (j, line :: map (replace_dependencies_in_line (name, [])) lines)
3.214 - | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
3.215 + | add_desired_line isar_shrink_factor fact_names frees
3.216 (Inference (name, t, rule, deps)) (j, lines) =
3.217 (j + 1,
3.218 if is_fact fact_names name orelse
3.219 - is_conjecture conjecture_shape name orelse
3.220 + is_conjecture name orelse
3.221 (* the last line must be kept *)
3.222 j = 0 orelse
3.223 (not (is_only_type_information t) andalso
3.224 @@ -706,23 +676,19 @@
3.225 fun smart_case_split [] facts = ByMetis facts
3.226 | smart_case_split proofs facts = CaseSplit (proofs, facts)
3.227
3.228 -fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
3.229 +fun add_fact_from_dependency fact_names name =
3.230 if is_fact fact_names name then
3.231 - apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
3.232 + apsnd (union (op =) (map fst (resolve_fact fact_names name)))
3.233 else
3.234 - apfst (insert (op =) (raw_label_for_name conjecture_shape name))
3.235 + apfst (insert (op =) (raw_label_for_name name))
3.236
3.237 -fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
3.238 - | step_for_line conjecture_shape _ _ _ (Inference (name, t, _, [])) =
3.239 - Assume (raw_label_for_name conjecture_shape name, t)
3.240 - | step_for_line conjecture_shape facts_offset fact_names j
3.241 - (Inference (name, t, _, deps)) =
3.242 - Have (if j = 1 then [Show] else [],
3.243 - raw_label_for_name conjecture_shape name,
3.244 +fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
3.245 + | step_for_line _ _ (Inference (name, t, _, [])) =
3.246 + Assume (raw_label_for_name name, t)
3.247 + | step_for_line fact_names j (Inference (name, t, _, deps)) =
3.248 + Have (if j = 1 then [Show] else [], raw_label_for_name name,
3.249 fold_rev forall_of (map Var (Term.add_vars t [])) t,
3.250 - ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
3.251 - fact_names)
3.252 - deps ([], [])))
3.253 + ByMetis (fold (add_fact_from_dependency fact_names) deps ([], [])))
3.254
3.255 fun repair_name "$true" = "c_True"
3.256 | repair_name "$false" = "c_False"
3.257 @@ -735,8 +701,8 @@
3.258 else
3.259 s
3.260
3.261 -fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor conjecture_shape
3.262 - facts_offset fact_names sym_tab params frees atp_proof =
3.263 +fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names sym_tab
3.264 + params frees atp_proof =
3.265 let
3.266 val lines =
3.267 atp_proof
3.268 @@ -744,16 +710,14 @@
3.269 |> nasty_atp_proof pool
3.270 |> map_term_names_in_atp_proof repair_name
3.271 |> decode_lines ctxt sym_tab
3.272 - |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
3.273 + |> rpair [] |-> fold_rev (add_line fact_names)
3.274 |> rpair [] |-> fold_rev add_nontrivial_line
3.275 |> rpair (0, [])
3.276 - |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape
3.277 - fact_names frees)
3.278 + |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
3.279 |> snd
3.280 in
3.281 (if null params then [] else [Fix params]) @
3.282 - map2 (step_for_line conjecture_shape facts_offset fact_names)
3.283 - (length lines downto 1) lines
3.284 + map2 (step_for_line fact_names) (length lines downto 1) lines
3.285 end
3.286
3.287 (* When redirecting proofs, we keep information about the labels seen so far in
3.288 @@ -1047,8 +1011,8 @@
3.289 in do_proof end
3.290
3.291 fun isar_proof_text ctxt isar_proof_requested
3.292 - (debug, full_types, isar_shrink_factor, pool, conjecture_shape,
3.293 - facts_offset, fact_names, sym_tab, atp_proof, goal)
3.294 + (debug, full_types, isar_shrink_factor, pool, fact_names, sym_tab,
3.295 + atp_proof, goal)
3.296 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
3.297 let
3.298 val isar_shrink_factor =
3.299 @@ -1058,8 +1022,8 @@
3.300 val one_line_proof = one_line_proof_text one_line_params
3.301 fun isar_proof_for () =
3.302 case atp_proof
3.303 - |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor
3.304 - conjecture_shape facts_offset fact_names sym_tab params frees
3.305 + |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names
3.306 + sym_tab params frees
3.307 |> redirect_proof hyp_ts concl_t
3.308 |> kill_duplicate_assumptions_in_proof
3.309 |> then_chain_proof
4.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Nov 18 06:50:05 2011 +0100
4.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Nov 18 11:47:12 2011 +0100
4.3 @@ -101,9 +101,8 @@
4.4 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
4.5 -> bool -> string -> bool -> bool -> term list -> term
4.6 -> ((string * locality) * term) list
4.7 - -> string problem * string Symtab.table * int * int
4.8 - * (string * locality) list vector * int list * (string * term) list
4.9 - * int Symtab.table
4.10 + -> string problem * string Symtab.table * (string * locality) list vector
4.11 + * (string * term) list * int Symtab.table
4.12 val atp_problem_weights : string problem -> (string * real) list
4.13 end;
4.14
4.15 @@ -2311,11 +2310,6 @@
4.16 poly <> Mangled_Monomorphic
4.17 | needs_type_tag_idempotence _ _ = false
4.18
4.19 -fun offset_of_heading_in_problem _ [] j = j
4.20 - | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
4.21 - if heading = needle then j
4.22 - else offset_of_heading_in_problem needle problem (j + length lines)
4.23 -
4.24 val implicit_declsN = "Should-be-implicit typings"
4.25 val explicit_declsN = "Explicit typings"
4.26 val factsN = "Relevant facts"
4.27 @@ -2406,22 +2400,12 @@
4.28 | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
4.29 implicit_declsN)
4.30 val (problem, pool) = problem |> nice_atp_problem readable_names
4.31 - val helpers_offset = offset_of_heading_in_problem helpersN problem 0
4.32 - val typed_helpers =
4.33 - map_filter (fn (j, {name, ...}) =>
4.34 - if String.isSuffix typed_helper_suffix name then SOME j
4.35 - else NONE)
4.36 - ((helpers_offset + 1 upto helpers_offset + length helpers)
4.37 - ~~ helpers)
4.38 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
4.39 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
4.40 in
4.41 (problem,
4.42 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
4.43 - offset_of_heading_in_problem conjsN problem 0,
4.44 - offset_of_heading_in_problem factsN problem 0,
4.45 fact_names |> Vector.fromList,
4.46 - typed_helpers,
4.47 lifted,
4.48 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
4.49 end
5.1 --- a/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 06:50:05 2011 +0100
5.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100
5.3 @@ -230,7 +230,7 @@
5.4 cat_lines (map (Syntax.string_of_term ctxt o snd) props))
5.5 *)
5.6 val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
5.7 - val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
5.8 + val (atp_problem, _, _, lifted, sym_tab) =
5.9 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
5.10 false false [] @{prop False} props
5.11 (*
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 06:50:05 2011 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
6.3 @@ -680,8 +680,7 @@
6.4 case lam_trans of
6.5 SOME s => s
6.6 | NONE => best_lam_trans
6.7 - val (atp_problem, pool, conjecture_offset, facts_offset,
6.8 - fact_names, typed_helpers, _, sym_tab) =
6.9 + val (atp_problem, pool, fact_names, _, sym_tab) =
6.10 prepare_atp_problem ctxt format conj_sym_kind prem_kind
6.11 type_enc false lam_trans readable_names true hyp_ts
6.12 concl_t facts
6.13 @@ -695,10 +694,6 @@
6.14 val _ = atp_problem |> lines_for_atp_problem format
6.15 |> cons ("% " ^ command ^ "\n")
6.16 |> File.write_list prob_file
6.17 - val conjecture_shape =
6.18 - conjecture_offset + 1
6.19 - upto conjecture_offset + length hyp_ts + 1
6.20 - |> map single
6.21 val ((output, run_time), (atp_proof, outcome)) =
6.22 TimeLimit.timeLimit generous_slice_timeout
6.23 Isabelle_System.bash_output command
6.24 @@ -719,8 +714,8 @@
6.25 val outcome =
6.26 case outcome of
6.27 NONE =>
6.28 - (case used_facts_in_unsound_atp_proof ctxt
6.29 - conjecture_shape facts_offset fact_names atp_proof
6.30 + (case used_facts_in_unsound_atp_proof ctxt fact_names
6.31 + atp_proof
6.32 |> Option.map (sort string_ord) of
6.33 SOME facts =>
6.34 let
6.35 @@ -736,8 +731,7 @@
6.36 | NONE => NONE)
6.37 | _ => outcome
6.38 in
6.39 - ((pool, conjecture_shape, facts_offset, fact_names,
6.40 - typed_helpers, sym_tab, lam_trans),
6.41 + ((pool, fact_names, sym_tab, lam_trans),
6.42 (output, run_time, atp_proof, outcome))
6.43 end
6.44 val timer = Timer.startRealTimer ()
6.45 @@ -756,8 +750,8 @@
6.46 end
6.47 | maybe_run_slice _ result = result
6.48 in
6.49 - ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty,
6.50 - no_lamsN), ("", Time.zeroTime, [], SOME InternalError))
6.51 + ((Symtab.empty, Vector.fromList [], Symtab.empty, no_lamsN),
6.52 + ("", Time.zeroTime, [], SOME InternalError))
6.53 |> fold maybe_run_slice actual_slices
6.54 end
6.55 else
6.56 @@ -772,8 +766,7 @@
6.57 ()
6.58 else
6.59 File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
6.60 - val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
6.61 - sym_tab, lam_trans),
6.62 + val ((pool, fact_names, sym_tab, lam_trans),
6.63 (output, run_time, atp_proof, outcome)) =
6.64 with_path cleanup export run_on problem_path_name
6.65 val important_message =
6.66 @@ -786,8 +779,7 @@
6.67 case outcome of
6.68 NONE =>
6.69 let
6.70 - val used_facts =
6.71 - used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
6.72 + val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
6.73 val reconstrs =
6.74 standard_reconstructors
6.75 (if member (op =) metis_lam_transs lam_trans then lam_trans
6.76 @@ -805,11 +797,10 @@
6.77 end,
6.78 fn preplay =>
6.79 let
6.80 - val full_types = uses_typed_helpers typed_helpers atp_proof
6.81 + val full_types = uses_typed_helpers atp_proof
6.82 val isar_params =
6.83 - (debug, full_types, isar_shrink_factor, pool,
6.84 - conjecture_shape, facts_offset, fact_names, sym_tab,
6.85 - atp_proof, goal)
6.86 + (debug, full_types, isar_shrink_factor, pool, fact_names,
6.87 + sym_tab, atp_proof, goal)
6.88 val one_line_params =
6.89 (preplay, proof_banner mode name, used_facts,
6.90 choose_minimize_command minimize_command name preplay,