added evaluation method for relevance filter
authorblanchet
Mon Aug 30 10:26:17 2010 +0200 (2010-08-30)
changeset 38892eccc9e2a6412
parent 38891 6e47e54214b8
child 38893 aa21c33a104f
added evaluation method for relevance filter
src/HOL/Mirabelle/Mirabelle_Test.thy
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
     1.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Aug 30 09:41:59 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Aug 30 10:26:17 2010 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    "Tools/mirabelle_quickcheck.ML"
     1.5    "Tools/mirabelle_refute.ML"
     1.6    "Tools/mirabelle_sledgehammer.ML"
     1.7 +  "Tools/mirabelle_sledgehammer_filter.ML"
     1.8  begin
     1.9  
    1.10  text {*
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 10:26:17 2010 +0200
     2.3 @@ -0,0 +1,69 @@
     2.4 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
     2.5 +    Author:     Jasmin Blanchette, TU Munich
     2.6 +*)
     2.7 +
     2.8 +structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
     2.9 +struct
    2.10 +
    2.11 +structure Prooftab =
    2.12 +  Table(type key = int * int val ord = prod_ord int_ord int_ord);
    2.13 +
    2.14 +val proof_table = Unsynchronized.ref Prooftab.empty
    2.15 +
    2.16 +fun init id thy =
    2.17 +  let
    2.18 +    fun do_line line =
    2.19 +      case line |> space_explode ":" of
    2.20 +        [line_num, col_num, proof] =>
    2.21 +        SOME (pairself (the o Int.fromString) (line_num, col_num),
    2.22 +              proof |> space_explode " " |> filter_out (curry (op =) ""))
    2.23 +       | _ => NONE
    2.24 +    val proofs = File.read (Path.explode "$HOME/Judgement/AllProofs/NS_Shared.txt")
    2.25 +    val proof_tab =
    2.26 +      proofs |> space_explode "\n"
    2.27 +             |> map_filter do_line
    2.28 +             |> AList.coalesce (op =)
    2.29 +             |> Prooftab.make
    2.30 +  in proof_table := proof_tab; thy end
    2.31 +
    2.32 +fun done id (args : Mirabelle.done_args) = ()
    2.33 +
    2.34 +val default_max_relevant = 300
    2.35 +
    2.36 +fun action args id ({pre, pos, ...} : Mirabelle.run_args) =
    2.37 +  case (Position.line_of pos, Position.column_of pos) of
    2.38 +    (SOME line_num, SOME col_num) =>
    2.39 +    (case Prooftab.lookup (!proof_table) (line_num, col_num) of
    2.40 +       SOME proofs =>
    2.41 +       let
    2.42 +         val {context = ctxt, facts, goal} = Proof.goal pre
    2.43 +         val thy = ProofContext.theory_of ctxt
    2.44 +         val {relevance_thresholds, full_types, max_relevant, theory_relevant,
    2.45 +              ...} = Sledgehammer_Isar.default_params thy args
    2.46 +         val subgoal = 1
    2.47 +         val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
    2.48 +         val facts =
    2.49 +           Sledgehammer_Fact_Filter.relevant_facts ctxt full_types
    2.50 +               relevance_thresholds
    2.51 +               (the_default default_max_relevant max_relevant)
    2.52 +               (the_default false theory_relevant)
    2.53 +               {add = [], del = [], only = false} facts hyp_ts concl_t
    2.54 +           |> map (fst o fst)
    2.55 +         val (found_facts, missing_facts) =
    2.56 +           List.concat proofs |> sort_distinct string_ord
    2.57 +           |> List.partition (member (op =) facts)
    2.58 +         val found_proofs = filter (forall (member (op =) facts)) proofs
    2.59 +         val _ =
    2.60 +           case length found_proofs of
    2.61 +             0 => writeln "Failure"
    2.62 +           | n => writeln ("Success (" ^ Int.toString n ^ " of " ^
    2.63 +                           Int.toString (length proofs) ^ " proofs)")
    2.64 +         val _ = writeln ("Found facts: " ^ commas found_facts)
    2.65 +         val _ = writeln ("Missing facts: " ^ commas missing_facts)
    2.66 +       in () end
    2.67 +     | NONE => ())
    2.68 +  | _ => ()
    2.69 +
    2.70 +fun invoke args = Mirabelle.register (init, action args, done)
    2.71 +
    2.72 +end;