src/HOL/TPTP/mash_eval.ML
changeset 50437 9762fe72936e
parent 50436 5291606b21e2
child 50439 330d4ad89e92
equal deleted inserted replaced
50436:5291606b21e2 50437:9762fe72936e
     7 
     7 
     8 signature MASH_EVAL =
     8 signature MASH_EVAL =
     9 sig
     9 sig
    10   type params = Sledgehammer_Provers.params
    10   type params = Sledgehammer_Provers.params
    11 
    11 
    12   val evaluate_mash_suggestions : Proof.context -> params -> string -> unit
    12   val evaluate_mash_suggestions :
       
    13     Proof.context -> params -> string -> string -> unit
    13 end;
    14 end;
    14 
    15 
    15 structure MaSh_Eval : MASH_EVAL =
    16 structure MaSh_Eval : MASH_EVAL =
    16 struct
    17 struct
    17 
    18 
    23 val MeshN = "Mesh"
    24 val MeshN = "Mesh"
    24 val IsarN = "Isar"
    25 val IsarN = "Isar"
    25 
    26 
    26 val all_names = map (rpair () o nickname_of) #> Symtab.make
    27 val all_names = map (rpair () o nickname_of) #> Symtab.make
    27 
    28 
    28 fun evaluate_mash_suggestions ctxt params file_name =
    29 fun evaluate_mash_suggestions ctxt params sugg_file_name out_file_name =
    29   let
    30   let
       
    31     val out_path = out_file_name |> Path.explode
       
    32     val _ = File.write out_path ""
       
    33     fun print s = (tracing s; File.append out_path (s ^ "\n"))
    30     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
    34     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
    31       Sledgehammer_Isar.default_params ctxt []
    35       Sledgehammer_Isar.default_params ctxt []
    32     val prover = hd provers
    36     val prover = hd provers
    33     val slack_max_facts = generous_max_facts (the max_facts)
    37     val slack_max_facts = generous_max_facts (the max_facts)
    34     val path = file_name |> Path.explode
    38     val sugg_path = sugg_file_name |> Path.explode
    35     val lines = path |> File.read_lines
    39     val lines = sugg_path |> File.read_lines
    36     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    40     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    37     val facts = all_facts ctxt false Symtab.empty [] [] css
    41     val facts = all_facts ctxt false Symtab.empty [] [] css
    38     val all_names = all_names (facts |> map snd)
    42     val all_names = all_names (facts |> map snd)
    39     val mepo_ok = Unsynchronized.ref 0
    43     val mepo_ok = Unsynchronized.ref 0
    40     val mash_ok = Unsynchronized.ref 0
    44     val mash_ok = Unsynchronized.ref 0
   101            fn () => prove isar_ok IsarN fst isar_facts]
   105            fn () => prove isar_ok IsarN fst isar_facts]
   102           |> Par_List.map (fn f => f ())
   106           |> Par_List.map (fn f => f ())
   103       in
   107       in
   104         ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
   108         ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
   105          isar_s]
   109          isar_s]
   106         |> cat_lines |> tracing
   110         |> cat_lines |> print
   107       end
   111       end
   108     fun total_of heading ok n =
   112     fun total_of heading ok n =
   109       "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
   113       "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
   110       Real.fmt (StringCvt.FIX (SOME 1))
   114       Real.fmt (StringCvt.FIX (SOME 1))
   111                (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
   115                (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
   115        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
   119        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
   116        the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
   120        the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
   117        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
   121        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
   118     val n = length lines
   122     val n = length lines
   119   in
   123   in
   120     tracing " * * *";
   124     print " * * *";
   121     tracing ("Options: " ^ commas options);
   125     print ("Options: " ^ commas options);
   122     List.app solve_goal (tag_list 1 lines);
   126     List.app solve_goal (tag_list 1 lines);
   123     ["Successes (of " ^ string_of_int n ^ " goals)",
   127     ["Successes (of " ^ string_of_int n ^ " goals)",
   124      total_of MePoN mepo_ok n,
   128      total_of MePoN mepo_ok n,
   125      total_of MaShN mash_ok n,
   129      total_of MaShN mash_ok n,
   126      total_of MeshN mesh_ok n,
   130      total_of MeshN mesh_ok n,
   127      total_of IsarN isar_ok n]
   131      total_of IsarN isar_ok n]
   128     |> cat_lines |> tracing
   132     |> cat_lines |> print
   129   end
   133   end
   130 
   134 
   131 end;
   135 end;