# HG changeset patch # User blanchet # Date 1283175567 -7200 # Node ID c91be1e503bd2b26c98ccbc5012f30f285770763 # Parent ee36b983ca22a03bc1e8cb1cc135b9400ae9cb4c move imperative code to where it belongs diff -r ee36b983ca22 -r c91be1e503bd src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon Aug 30 15:25:15 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon Aug 30 15:39:27 2010 +0200 @@ -5,6 +5,18 @@ structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = struct +val relevance_filter_args = + [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight), + ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight), + ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight), + ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus), + ("local_bonus", Sledgehammer_Fact_Filter.local_bonus), + ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus), + ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor), + ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold), + ("max_max_imperfect_fudge_factor", + Sledgehammer_Fact_Filter.max_max_imperfect_fudge_factor)] + structure Prooftab = Table(type key = int * int val ord = prod_ord int_ord int_ord); @@ -75,6 +87,13 @@ let val {context = ctxt, facts, goal} = Proof.goal pre val thy = ProofContext.theory_of ctxt + val args = + args + |> filter (fn (key, value) => + case AList.lookup (op =) relevance_filter_args key of + SOME rf => (rf := the (Real.fromString value); false) + | NONE => true) + val {relevance_thresholds, full_types, max_relevant, theory_relevant, ...} = Sledgehammer_Isar.default_params thy args val subgoal = 1 @@ -104,38 +123,36 @@ val _ = add id num_lost_proofs (length proofs - n) val _ = add id num_found_facts (length found_facts) val _ = add id num_lost_facts (length lost_facts) - val _ = if null found_facts then + val _ = + if null found_facts then + () + else + let + val found_weight = + Real.fromInt (fold (fn (n, _) => + Integer.add (n * n)) found_facts 0) + / Real.fromInt (length found_facts) + |> Math.sqrt |> Real.ceil + in + log ("Found facts (among " ^ string_of_int (length facts) ^ + ", weight " ^ string_of_int found_weight ^ "): " ^ + commas (map with_index found_facts)) + end + val _ = if null lost_facts then () else - log ("Found facts: " ^ commas (map with_index found_facts)) - val _ = if null lost_facts then () - else log ("Lost facts: " ^ commas lost_facts) + log ("Lost facts (among " ^ string_of_int (length facts) ^ + "): " ^ commas lost_facts) in () end | NONE => log "No known proof") | _ => () val proof_fileK = "proof_file" -val relevance_filter_args = - [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight), - ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight), - ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight), - ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus), - ("local_bonus", Sledgehammer_Fact_Filter.local_bonus), - ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus), - ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor), - ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold), - ("max_max_imperfect_fudge_factor", - Sledgehammer_Fact_Filter.max_max_imperfect_fudge_factor)] - fun invoke args = let val (pf_args, other_args) = args |> List.partition (curry (op =) proof_fileK o fst) - ||> filter (fn (key, value) => - case AList.lookup (op =) relevance_filter_args key of - SOME rf => (rf := the (Real.fromString value); false) - | NONE => true) val proof_file = case pf_args of [] => error "No \"proof_file\" specified" | (_, s) :: _ => s