# HG changeset patch # User blanchet # Date 1350554385 -7200 # Node ID 2e7d0655b176b3aeb91631d03e2803e829514630 # Parent a81f95693c684a7b3c4d83409f8695f93c15549e tuning diff -r a81f95693c68 -r 2e7d0655b176 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 09:19:37 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 11:59:45 2012 +0200 @@ -9,11 +9,9 @@ type isar_params = ATP_Proof_Reconstruct.isar_params type one_line_params = ATP_Proof_Reconstruct.one_line_params val isar_proof_text : - Proof.context -> bool -> isar_params -> - one_line_params -> string + Proof.context -> bool -> isar_params -> one_line_params -> string val proof_text : - Proof.context -> bool -> isar_params -> - int -> one_line_params -> string + Proof.context -> bool -> isar_params -> int -> one_line_params -> string end; structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -223,17 +221,18 @@ (if n <> 1 then "next" else "qed") in do_proof end -fun min_local ctxt type_enc lam_trans proof = +fun minimize_locally ctxt type_enc lam_trans proof = let (* Merging spots, greedy algorithm *) fun cost (Prove (_, _ , t, _)) = Term.size_of_term t | cost _ = ~1 - fun can_merge (Prove (_, lbl, _, By_Metis _)) (Prove (_, _, _, By_Metis _)) = - (lbl = no_label) + fun can_merge (Prove (_, lbl, _, By_Metis _)) + (Prove (_, _, _, By_Metis _)) = + (lbl = no_label) | can_merge _ _ = false val merge_spots = - fold_index - (fn (i, s2) => fn (s1, pile) => (s2, pile |> can_merge s1 s2 ? cons (i, cost s1))) + fold_index (fn (i, s2) => fn (s1, pile) => + (s2, pile |> can_merge s1 s2 ? cons (i, cost s1))) (tl proof) (hd proof, []) |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst @@ -241,8 +240,8 @@ val thy = Proof_Context.theory_of ctxt fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = - if lbl = no_label then ctxt - else Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) ctxt + ctxt |> lbl <> no_label + ? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) | enrich_ctxt' _ ctxt = ctxt val rich_ctxt = fold enrich_ctxt' proof ctxt @@ -256,12 +255,12 @@ fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 = let fun thmify (Prove (_, _, t, _)) = sorry t - val facts = fact_names |>> map string_for_label - |> op@ - |> map (Proof_Context.get_thm rich_ctxt) - |> (if member op= qs Then - then cons (the s0 |> thmify) - else I) + val facts = + fact_names + |>> map string_for_label + |> op @ + |> map (Proof_Context.get_thm rich_ctxt) + |> (if member (op =) qs Then then cons (the s0 |> thmify) else I) val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) fun tac {context = ctxt, prems = _} = Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 @@ -273,31 +272,37 @@ fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1))) (Prove (qs2, lbl , t, By_Metis (ls2, ss2))) = let - val qs = (inter op= qs1 qs2) (* FIXME: Is this correct? *) - |> member op= (union op= qs1 qs2) Ultimately ? cons Ultimately - |> member op= qs2 Show ? cons Show - in Prove (qs, lbl, t, By_Metis (ls1@ls2, ss1@ss2)) end + val qs = + inter (op =) qs1 qs2 (* FIXME: Is this correct? *) + |> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately + |> member (op =) qs2 Show ? cons Show + in Prove (qs, lbl, t, By_Metis (ls1 @ ls2, ss1 @ ss2)) end fun try_merge proof i = let val (front, s0, s1, s2, tail) = case (proof, i) of - ((s1::s2::proof), 0) => ([], NONE, s1, s2, proof) - | _ => let val (front, s0::s1::s2::tail) = chop (i-1) proof - in (front, SOME s0, s1, s2, tail) end + ((s1 :: s2 :: proof), 0) => ([], NONE, s1, s2, proof) + | _ => + let val (front, s0 :: s1 :: s2 :: tail) = chop (i - 1) proof in + (front, SOME s0, s1, s2, tail) + end val s12 = merge s1 s2 val t1 = try_metis s1 s0 () val t2 = try_metis s2 (SOME s1) () val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal in (TimeLimit.timeLimit tlimit (try_metis s12 s0) (); - SOME (front @ (case s0 of NONE => s12::tail | SOME s => s::s12::tail))) + SOME (front @ (case s0 of + NONE => s12 :: tail + | SOME s => s :: s12 :: tail))) handle _ => NONE end fun merge_steps proof [] = proof - | merge_steps proof (i::is) = + | merge_steps proof (i :: is) = case try_merge proof i of NONE => merge_steps proof is - | SOME proof' => merge_steps proof' (map (fn j => if j>i then j-1 else j) is) + | SOME proof' => + merge_steps proof' (map (fn j => if j > i then j - 1 else j) is) in merge_steps proof merge_spots end fun isar_proof_text ctxt isar_proof_requested @@ -379,7 +384,7 @@ |> kill_duplicate_assumptions_in_proof |> kill_useless_labels_in_proof |> relabel_proof - |> min_local ctxt type_enc lam_trans) + |> minimize_locally ctxt type_enc lam_trans) |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count in case isar_proof of