--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Sep 14 20:07:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Sep 14 23:01:29 2010 +0200
@@ -64,11 +64,13 @@
datatype raw_step_name = Str of string * string | Num of string
-fun raw_step_name_num (Str (num, _)) = num
- | raw_step_name_num (Num num) = num
+fun raw_step_num (Str (num, _)) = num
+ | raw_step_num (Num num) = num
+
+fun same_raw_step s t = raw_step_num s = raw_step_num t
fun raw_step_name_ord p =
- let val q = pairself raw_step_name_num p in
+ let val q = pairself raw_step_num p in
case pairself Int.fromString q of
(NONE, NONE) => string_ord q
| (NONE, SOME _) => LESS
@@ -77,9 +79,11 @@
end
fun index_in_shape x = find_index (exists (curry (op =) x))
-fun resolve_axiom axiom_names (Str (_, str)) =
- (case find_first_in_list_vector axiom_names str of
- SOME x => [(str, x)]
+fun resolve_axiom axiom_names (Str (_, s)) =
+ (case strip_prefix_and_unascii axiom_prefix s of
+ SOME s' => (case find_first_in_list_vector axiom_names s' of
+ SOME x => [(s', x)]
+ | NONE => [])
| NONE => [])
| resolve_axiom axiom_names (Num num) =
case Int.fromString num of
@@ -93,9 +97,11 @@
fun resolve_conjecture conjecture_shape (Str (num, s)) =
let
- val j = try (unprefix conjecture_prefix) s |> the_default num
- |> Int.fromString |> the_default ~1
- val k = index_in_shape j conjecture_shape
+ val k = case try (unprefix conjecture_prefix) s of
+ SOME s => Int.fromString s |> the_default ~1
+ | NONE => case Int.fromString num of
+ SOME j => index_in_shape j conjecture_shape
+ | NONE => ~1
in if k >= 0 then [k] else [] end
| resolve_conjecture conjecture_shape (Num num) =
resolve_conjecture conjecture_shape (Str (num, "")) (* HACK *)
@@ -142,13 +148,13 @@
fun parse_annotation strict x =
((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
>> (strict ? filter (is_some o Int.fromString)))
- -- Scan.optional (parse_annotation strict) [] >> uncurry (union (op =))
+ -- Scan.optional (parse_annotation strict) [] >> op @
|| $$ "(" |-- parse_annotations strict --| $$ ")"
|| $$ "[" |-- parse_annotations strict --| $$ "]") x
and parse_annotations strict x =
(Scan.optional (parse_annotation strict
::: Scan.repeat ($$ "," |-- parse_annotation strict)) []
- >> (fn numss => fold (union (op =)) numss [])) x
+ >> flat) x
(* Vampire proof lines sometimes contain needless information such as "(0:3)",
which can be hard to disambiguate from function application in an LL(1)
@@ -206,16 +212,23 @@
|-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
-- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
>> (fn (((num, role), phi), deps) =>
- case role of
- "definition" =>
- (case phi of
- AConn (AIff, [phi1 as AAtom _, phi2]) =>
- Definition (Num num, phi1, phi2)
- | AAtom (ATerm ("c_equal", _)) =>
- (* Vampire's equality proxy axiom *)
- Inference (Num num, phi, map Num deps)
- | _ => raise Fail "malformed definition")
- | _ => Inference (Num num, phi, map Num deps))
+ let
+ val (name, deps) =
+ case deps of
+ ["file", _, s] => (Str (num, s), [])
+ | _ => (Num num, deps)
+ in
+ case role of
+ "definition" =>
+ (case phi of
+ AConn (AIff, [phi1 as AAtom _, phi2]) =>
+ Definition (name, phi1, phi2)
+ | AAtom (ATerm ("c_equal", _)) =>
+ (* Vampire's equality proxy axiom *)
+ Inference (name, phi, map Num deps)
+ | _ => raise Fail "malformed definition")
+ | _ => Inference (name, phi, map Num deps)
+ end)
(**** PARSING OF VAMPIRE OUTPUT ****)
@@ -268,6 +281,14 @@
(parse_lines pool)))
o explode o strip_spaces_except_between_ident_chars
+fun clean_up_dependencies _ [] = []
+ | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
+ step :: clean_up_dependencies (name :: seen) steps
+ | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
+ Inference (name, u,
+ map_filter (fn dep => find_first (same_raw_step dep) seen) deps) ::
+ clean_up_dependencies (name :: seen) steps
+
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
exception FO_TERM of string fo_term list
@@ -510,10 +531,11 @@
clsarity). *)
val is_only_type_information = curry (op aconv) HOLogic.true_const
-fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
-fun replace_deps_in_line _ (line as Definition _) = line
- | replace_deps_in_line p (Inference (name, t, deps)) =
- Inference (name, t, fold (union (op =) o replace_one_dep p) deps [])
+fun replace_one_dependency (old, new) dep =
+ if raw_step_num dep = raw_step_num old then new else [dep]
+fun replace_dependencies_in_line _ (line as Definition _) = line
+ | replace_dependencies_in_line p (Inference (name, t, deps)) =
+ Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
(* Discard axioms; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
@@ -524,16 +546,16 @@
if is_axiom axiom_names name then
(* Axioms are not proof lines. *)
if is_only_type_information t then
- map (replace_deps_in_line (name, [])) lines
+ map (replace_dependencies_in_line (name, [])) lines
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference t) lines of
- (_, []) => lines (*no repetition of proof line*)
+ (_, []) => lines (* no repetition of proof line *)
| (pre, Inference (name', _, _) :: post) =>
- pre @ map (replace_deps_in_line (name', [name])) post
+ pre @ map (replace_dependencies_in_line (name', [name])) post
else if is_conjecture conjecture_shape name then
Inference (name, negate_term t, []) :: lines
else
- map (replace_deps_in_line (name, [])) lines
+ map (replace_dependencies_in_line (name, [])) lines
| add_line _ _ (Inference (name, t, deps)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
@@ -545,15 +567,16 @@
(_, []) => Inference (name, t, deps) :: lines
| (pre, Inference (name', t', _) :: post) =>
Inference (name, t', deps) ::
- pre @ map (replace_deps_in_line (name', [name])) post
+ pre @ map (replace_dependencies_in_line (name', [name])) post
(* Recursively delete empty lines (type information) from the proof. *)
fun add_nontrivial_line (Inference (name, t, [])) lines =
- if is_only_type_information t then delete_dep name lines
+ if is_only_type_information t then delete_dependency name lines
else Inference (name, t, []) :: lines
| add_nontrivial_line line lines = line :: lines
-and delete_dep name lines =
- fold_rev add_nontrivial_line (map (replace_deps_in_line (name, [])) lines) []
+and delete_dependency name lines =
+ fold_rev add_nontrivial_line
+ (map (replace_dependencies_in_line (name, [])) lines) []
(* ATPs sometimes reuse free variable names in the strangest ways. Removing
offending lines often does the trick. *)
@@ -561,20 +584,23 @@
| is_bad_free _ _ = false
fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
- (j, line :: map (replace_deps_in_line (name, [])) lines)
+ (j, line :: map (replace_dependencies_in_line (name, [])) lines)
| add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
(Inference (name, t, deps)) (j, lines) =
(j + 1,
if is_axiom axiom_names name orelse
is_conjecture conjecture_shape name orelse
+ (* the last line must be kept *)
+ j = 0 orelse
(not (is_only_type_information t) andalso
null (Term.add_tvars t []) andalso
not (exists_subterm (is_bad_free frees) t) andalso
- (null lines orelse (* last line must be kept *)
- (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
+ length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
+ (* kill next to last line, which usually results in a trivial step *)
+ j <> 1) then
Inference (name, t, deps) :: lines (* keep line *)
else
- map (replace_deps_in_line (name, deps)) lines) (* drop line *)
+ map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
(** EXTRACTING LEMMAS **)
@@ -631,9 +657,9 @@
fun raw_label_for_name conjecture_shape name =
case resolve_conjecture conjecture_shape name of
[j] => (conjecture_prefix, j)
- | _ => case Int.fromString (raw_step_name_num name) of
+ | _ => case Int.fromString (raw_step_num name) of
SOME j => (raw_prefix, j)
- | NONE => (raw_prefix ^ raw_step_name_num name, 0)
+ | NONE => (raw_prefix ^ raw_step_num name, 0)
fun metis_using [] = ""
| metis_using ls =
@@ -696,7 +722,7 @@
fun smart_case_split [] facts = ByMetis facts
| smart_case_split proofs facts = CaseSplit (proofs, facts)
-fun add_fact_from_dep conjecture_shape axiom_names name =
+fun add_fact_from_dependency conjecture_shape axiom_names name =
if is_axiom axiom_names name then
apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
else
@@ -711,8 +737,8 @@
| step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
Have (if j = 1 then [Show] else [],
raw_label_for_name conjecture_shape name, forall_vars t,
- ByMetis (fold (add_fact_from_dep conjecture_shape axiom_names) deps
- ([], [])))
+ ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
+ deps ([], [])))
fun raw_step_name (Definition (name, _, _)) = name
| raw_step_name (Inference (name, _, _)) = name
@@ -724,6 +750,7 @@
atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof pool
|> sort (raw_step_name_ord o pairself raw_step_name)
+ |> clean_up_dependencies []
|> decode_lines ctxt full_types tfrees
|> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
|> rpair [] |-> fold_rev add_nontrivial_line
@@ -819,60 +846,59 @@
second_pass end_qs (proof, (t, l) :: assums, patches)
| second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
patches) =
- if member (op =) (snd (snd patches)) l andalso
- not (member (op =) (fst (snd patches)) l) andalso
- not (AList.defined (op =) (fst patches) l) then
- second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
- else
- (case List.partition (member (op =) contra_ls) ls of
- ([contra_l], co_ls) =>
- if member (op =) qs Show then
- second_pass end_qs (proof, assums,
- patches |>> cons (contra_l, (co_ls, ss)))
- else
- second_pass end_qs
- (proof, assums,
- patches |>> cons (contra_l, (l :: co_ls, ss)))
- |>> cons (if member (op =) (fst (snd patches)) l then
- Assume (l, negate_term t)
- else
- Have (qs, l, negate_term t,
- ByMetis (backpatch_label patches l)))
- | (contra_ls as _ :: _, co_ls) =>
- let
- val proofs =
- map_filter
- (fn l =>
- if l = concl_l then
- NONE
- else
- let
- val drop_ls = filter (curry (op <>) l) contra_ls
- in
- second_pass []
- (proof, assums,
- patches ||> apfst (insert (op =) l)
- ||> apsnd (union (op =) drop_ls))
- |> fst |> SOME
- end) contra_ls
- val (assumes, facts) =
- if member (op =) (fst (snd patches)) l then
- ([Assume (l, negate_term t)], (l :: co_ls, ss))
- else
- ([], (co_ls, ss))
- in
- (case join_proofs proofs of
- SOME (l, t, proofs, proof_tail) =>
- Have (case_split_qualifiers proofs @
- (if null proof_tail then end_qs else []), l, t,
- smart_case_split proofs facts) :: proof_tail
- | NONE =>
- [Have (case_split_qualifiers proofs @ end_qs, no_label,
- concl_t, smart_case_split proofs facts)],
- patches)
- |>> append assumes
- end
- | _ => raise Fail "malformed proof")
+ (if member (op =) (snd (snd patches)) l andalso
+ not (member (op =) (fst (snd patches)) l) andalso
+ not (AList.defined (op =) (fst patches) l) then
+ second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
+ else case List.partition (member (op =) contra_ls) ls of
+ ([contra_l], co_ls) =>
+ if member (op =) qs Show then
+ second_pass end_qs (proof, assums,
+ patches |>> cons (contra_l, (co_ls, ss)))
+ else
+ second_pass end_qs
+ (proof, assums,
+ patches |>> cons (contra_l, (l :: co_ls, ss)))
+ |>> cons (if member (op =) (fst (snd patches)) l then
+ Assume (l, negate_term t)
+ else
+ Have (qs, l, negate_term t,
+ ByMetis (backpatch_label patches l)))
+ | (contra_ls as _ :: _, co_ls) =>
+ let
+ val proofs =
+ map_filter
+ (fn l =>
+ if l = concl_l then
+ NONE
+ else
+ let
+ val drop_ls = filter (curry (op <>) l) contra_ls
+ in
+ second_pass []
+ (proof, assums,
+ patches ||> apfst (insert (op =) l)
+ ||> apsnd (union (op =) drop_ls))
+ |> fst |> SOME
+ end) contra_ls
+ val (assumes, facts) =
+ if member (op =) (fst (snd patches)) l then
+ ([Assume (l, negate_term t)], (l :: co_ls, ss))
+ else
+ ([], (co_ls, ss))
+ in
+ (case join_proofs proofs of
+ SOME (l, t, proofs, proof_tail) =>
+ Have (case_split_qualifiers proofs @
+ (if null proof_tail then end_qs else []), l, t,
+ smart_case_split proofs facts) :: proof_tail
+ | NONE =>
+ [Have (case_split_qualifiers proofs @ end_qs, no_label,
+ concl_t, smart_case_split proofs facts)],
+ patches)
+ |>> append assumes
+ end
+ | _ => raise Fail "malformed proof")
| second_pass _ _ = raise Fail "malformed proof"
val proof_bottom =
second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst