src/HOL/TPTP/mash_eval.ML

   let
     val thy = Proof_Context.theory_of ctxt
     val zeros = [0, 0, 0, 0, 0, 0]
     val report_path = report_file_name |> Path.explode
     val _ = File.write report_path ""
+
     fun print s = File.append report_path (s ^ "\n")
+
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
     val prover = hd provers
     val max_suggs = generous_max_suggestions (the max_facts)
     val lines_of = Path.explode #> try File.read_lines #> these
     val file_names =

        mesh_isar_file_name, mesh_prover_file_name]
     val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
                   mesh_isar_lines, mesh_prover_lines] =
       map lines_of file_names
     val num_lines = fold (Integer.max o length) lines 0
+
     fun pad lines = lines @ replicate (num_lines - length lines) ""
+
     val lines =
       pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
       pad mesh_isar_lines ~~ pad mesh_prover_lines
     val css = clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt true false Symtab.empty [] [] css
     val name_tabs = build_name_tables nickname_of_thm facts
+
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_str (j, s) = s ^ "@" ^ string_of_int j
     val str_of_method = enclose "  " ": "
-    fun str_of_result method facts ({outcome, run_time, used_facts, ...}
-                                     : prover_result) =
+
+    fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) =
       let val facts = facts |> map (fst o fst) in
         str_of_method method ^
         (if is_none outcome then
            "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
            (used_facts |> map (with_index facts o fst)

            "Failure: " ^
            (facts |> take (the max_facts) |> tag_list 1
                   |> map index_str
                   |> space_implode " "))
       end
-    fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line),
-                         mesh_isar_line), mesh_prover_line)) =
+
+    fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), mesh_isar_line),
+        mesh_prover_line)) =
       if in_range range j then
         let
           val get_suggs = extract_suggestions ##> (take max_suggs #> map fst)
           val (name1, mepo_suggs) = get_suggs mepo_line
           val (name2, mash_isar_suggs) = get_suggs mash_isar_line

             | NONE => error ("No fact called \"" ^ name ^ "\".")
           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
           val isar_deps = these (isar_dependencies_of name_tabs th)
           val facts = facts |> filter (fn (_, th') => thm_less (th', th))
+
           (* adapted from "mirabelle_sledgehammer.ML" *)
           fun set_file_name method (SOME dir) =
               let
-                val prob_prefix =
-                  "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
-                  method
+                val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method
               in
                 Config.put atp_dest_dir dir
                 #> Config.put atp_problem_prefix (prob_prefix ^ "__")
                 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I
+
           fun prove method suggs =
             if not (member (op =) methods method) orelse
                (null facts andalso method <> IsarN) then
               (str_of_method method ^ "Skipped", 0)
             else
               let
                 fun nickify ((_, stature), th) =
                   ((K (encode_str (nickname_of_thm th)), stature), th)
+
                 val facts =
                   suggs
                   |> find_suggested_facts ctxt facts
                   |> map (fact_of_raw_fact #> nickify)
                   |> maybe_instantiate_inducts ctxt hyp_ts concl_t

                   |> map fact_of_raw_fact
                 val ctxt = ctxt |> set_file_name method prob_dir_name
                 val res as {outcome, ...} =
                   run_prover_for_mash ctxt params prover name facts goal
                 val ok = if is_none outcome then 1 else 0
-              in (str_of_result method facts res, ok) end
+              in
+                (str_of_result method facts res, ok)
+              end
+
           val ress =
             [fn () => prove MePoN mepo_suggs,
              fn () => prove MaSh_IsarN mash_isar_suggs,
              fn () => prove MaSh_ProverN mash_prover_suggs,
              fn () => prove MeSh_IsarN mesh_isar_suggs,

           |> cat_lines |> print;
           map snd ress
         end
       else
         zeros
+
     fun total_of method ok n =
       str_of_method method ^ string_of_int ok ^ " (" ^
       Real.fmt (StringCvt.FIX (SOME 1))
                (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
+
     val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
       ["prover = " ^ prover,
        "max_facts = " ^ string_of_int (the max_facts),
        "slice" |> not slice ? prefix "dont_",

        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val _ = print " * * *";
     val _ = print ("Options: " ^ commas options);
     val oks = Par_List.map solve_goal (tag_list 1 lines)
     val n = length oks
-    val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
-         isar_ok] =
+    val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, isar_ok] =
       if n = 0 then zeros else map Integer.sum (map_transpose I oks)
   in
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,
      total_of MaSh_IsarN mash_isar_ok n,