summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 02 Jun 2010 17:19:44 +0200 | |

changeset 37323 | 2f2f0d246d0f |

parent 37322 | 0347b1a16682 |

child 37324 | d77250dd2416 |

handle Vampire's definitions smoothly

src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 02 17:06:28 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 02 17:19:44 2010 +0200 @@ -487,8 +487,8 @@ fun decode_lines ctxt full_types tfrees lines = fst (fold_map (decode_line full_types tfrees) lines ctxt) -fun aint_inference _ (Definition _) = true - | aint_inference t (Inference (_, t', _)) = not (t aconv t') +fun aint_actual_inference _ (Definition _) = true + | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t') (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) @@ -510,7 +510,7 @@ if is_only_type_information t then map (replace_deps_in_line (num, [])) lines (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (aint_inference t) lines of + else case take_prefix (aint_actual_inference t) lines of (_, []) => lines (*no repetition of proof line*) | (pre, Inference (num', _, _) :: post) => pre @ map (replace_deps_in_line (num', [num])) post @@ -523,7 +523,7 @@ if is_only_type_information t then Inference (num, t, deps) :: lines (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (aint_inference t) lines of + else case take_prefix (aint_actual_inference t) lines of (* FIXME: Doesn't this code risk conflating proofs involving different types?? *) (_, []) => Inference (num, t, deps) :: lines @@ -539,8 +539,8 @@ and delete_dep num lines = fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) [] -(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly, - removing the offending lines often does the trick. *) +(* ATPs sometimes reuse free variable names in the strangest ways. Removing + offending lines often does the trick. *) fun is_bad_free frees (Free x) = not (member (op =) frees x) | is_bad_free _ _ = false @@ -549,8 +549,8 @@ $ t1 $ t2)) = (t1 aconv t2) | is_trivial_formula t = false -fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) = - (j, line :: lines) +fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) = + (j, line :: map (replace_deps_in_line (num, [])) lines) | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1,