# HG changeset patch # User immler@in.tum.de # Date 1241473451 -7200 # Node ID 887298ab70dc0d86c126bd5f493664c1c3748baf # Parent ac8669134e7aca0a78b671525d1b7ef70e6a1a93 tuned diff -r ac8669134e7a -r 887298ab70dc src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Mon May 04 23:37:39 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Mon May 04 23:44:11 2009 +0200 @@ -103,7 +103,7 @@ (*If string s has the prefix s1, return the result of deleting it.*) fun strip_prefix s1 s = - if String.isPrefix s1 s + if String.isPrefix s1 s then SOME (ResClause.undo_ascii_of (String.extract (s, size s1, NONE))) else NONE; @@ -278,10 +278,10 @@ in #1 (fold_map (decode_tstp vt0) tuples ctxt) end; (** Finding a matching assumption. The literals may be permuted, and variable names - may disagree. We have to try all combinations of literals (quadratic!) and + may disagree. We have to try all combinations of literals (quadratic!) and match up the variable names consistently. **) -fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) = +fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) = strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t)) | strip_alls_aux _ t = t; @@ -292,20 +292,20 @@ (*Ignore types: they are not to be trusted...*) fun match_literal (t1$u1) (t2$u2) env = match_literal t1 t2 (match_literal u1 u2 env) - | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = + | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = match_literal t1 t2 env - | match_literal (Bound i1) (Bound i2) env = + | match_literal (Bound i1) (Bound i2) env = if i1=i2 then env else raise MATCH_LITERAL - | match_literal (Const(a1,_)) (Const(a2,_)) env = + | match_literal (Const(a1,_)) (Const(a2,_)) env = if a1=a2 then env else raise MATCH_LITERAL - | match_literal (Free(a1,_)) (Free(a2,_)) env = + | match_literal (Free(a1,_)) (Free(a2,_)) env = if a1=a2 then env else raise MATCH_LITERAL | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env | match_literal _ _ env = raise MATCH_LITERAL; (*Checking that all variable associations are unique. The list env contains no repetitions, but does it contain say (x,y) and (y,y)? *) -fun good env = +fun good env = let val (xs,ys) = ListPair.unzip env in not (has_duplicates (op=) xs orelse has_duplicates (op=) ys) end; @@ -316,15 +316,15 @@ let fun match1 us [] = false | match1 us (t::ts) = let val env' = match_literal lit t env - in (good env' andalso matches_aux env' lits (us@ts)) orelse - match1 (t::us) ts + in (good env' andalso matches_aux env' lits (us@ts)) orelse + match1 (t::us) ts end handle MATCH_LITERAL => match1 (t::us) ts - in match1 [] ts end; + in match1 [] ts end; (*Is this length test useful?*) -fun matches (lits1,lits2) = - length lits1 = length lits2 andalso +fun matches (lits1,lits2) = + length lits1 = length lits2 andalso matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2); fun permuted_clause t = @@ -408,7 +408,7 @@ if eq_types t orelse not (null (Term.add_tvars t [])) orelse exists_subterm bad_free t orelse (not (null lines) andalso (*final line can't be deleted for these reasons*) - (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0)) + (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0)) then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*) else (nlines+1, (lno, t, deps) :: lines); @@ -467,7 +467,7 @@ val failure_strings_remote = ["Remote-script could not extract proof"]; fun find_failure proof = let val failures = - map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) + map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote) in if null failures then NONE else SOME (hd failures) end; @@ -481,7 +481,7 @@ "Formulae used in the proof"]; fun get_proof_extract proof = let - (*splits to_split by the first possible of a list of splitters*) + (*splits to_split by the first possible of a list of splitters*) fun first_field_any [] to_split = NONE | first_field_any (splitter::splitters) to_split = let @@ -493,10 +493,10 @@ val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b) in proofextract end; - (* === EXTRACTING LEMMAS === *) + (* === EXTRACTING LEMMAS === *) (* lines have the form "cnf(108, axiom, ...", the number (108) has to be extracted)*) - fun get_step_nums_tstp proofextract = + fun get_step_nums_tstp proofextract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok | inputno _ = NONE @@ -513,7 +513,7 @@ val lines = split_lines proofextract in List.mapPartial (inputno o toks) lines end - (*extracting lemmas from tstp-output between the lines from above*) + (*extracting lemmas from tstp-output between the lines from above*) fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) = let (* get the names of axioms from their numbers*) @@ -521,48 +521,48 @@ let fun is_axiom n = n <= Vector.length thm_names fun getname i = Vector.sub(thm_names, i-1) - in + in sort_distinct string_ord (filter (fn x => x <> "??.unknown") (map getname (filter is_axiom step_nums))) end val proofextract = get_proof_extract proof - in + in get_axiom_names thm_names (get_step_nums proofextract) end; - (* metis-command *) - fun metis_line [] = "apply metis" - | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" + (* metis-command *) + fun metis_line [] = "apply metis" + | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" + + (* atp_minimize [atp=] *) + fun minimize_line _ [] = "" + | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ + (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas) - (* atp_minimize [atp=] *) - fun minimize_line _ [] = "" - | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ - (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas) - - (*Used to label theorems chained into the sledgehammer call*) - val chained_hint = "CHAINED"; - fun sendback_metis_nochained lemmas = - let val nochained = filter_out (fn y => y = chained_hint) - in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end - fun lemma_list_tstp name result = - let val lemmas = extract_lemmas get_step_nums_tstp result - in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end; - fun lemma_list_dfg name result = - let val lemmas = extract_lemmas get_step_nums_dfg result - in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end; + (*Used to label theorems chained into the sledgehammer call*) + val chained_hint = "CHAINED"; + fun sendback_metis_nochained lemmas = + let val nochained = filter_out (fn y => y = chained_hint) + in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end + fun lemma_list_tstp name result = + let val lemmas = extract_lemmas get_step_nums_tstp result + in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end; + fun lemma_list_dfg name result = + let val lemmas = extract_lemmas get_step_nums_dfg result + in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end; - (* === Extracting structured Isar-proof === *) - fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) = - let - (*Could use split_lines, but it can return blank lines...*) - val lines = String.tokens (equal #"\n"); - val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c) - val proofextract = get_proof_extract proof - val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) - val one_line_proof = lemma_list_tstp name result - val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" - else decode_tstp_file cnfs ctxt goal subgoalno thm_names - in - one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured - end + (* === Extracting structured Isar-proof === *) + fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) = + let + (*Could use split_lines, but it can return blank lines...*) + val lines = String.tokens (equal #"\n"); + val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c) + val proofextract = get_proof_extract proof + val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) + val one_line_proof = lemma_list_tstp name result + val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" + else decode_tstp_file cnfs ctxt goal subgoalno thm_names + in + one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured + end - end; +end;