# HG changeset patch
# User blanchet
# Date 1355793554 -3600
# Node ID c5e0073558f3b40f73a0c97555118853d3fbbdba
# Parent  9d2f223ab6d994b15a2a54f9c4a3914a4368315f
avoid references altogether

diff -r 9d2f223ab6d9 -r c5e0073558f3 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Tue Dec 18 02:18:45 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Dec 18 02:19:14 2012 +0100
@@ -47,10 +47,6 @@
     val css = clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt true false Symtab.empty [] [] css
     val all_names = build_all_names nickname_of facts
-    val mepo_ok = Synchronized.var "mepo_ok" 0
-    val mash_ok = Synchronized.var "mash_ok" 0
-    val mesh_ok = Synchronized.var "mesh_ok" 0
-    val isar_ok = Synchronized.var "isar_ok" 0
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
     fun str_of_res label facts ({outcome, run_time, used_facts, ...}
@@ -108,7 +104,7 @@
                 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I
-          fun prove ok heading get facts =
+          fun prove heading get facts =
             let
               fun nickify ((_, stature), th) =
                 ((K (escape_meta (nickname_of th)), stature), th)
@@ -120,30 +116,25 @@
               val ctxt = ctxt |> set_file_name heading prob_dir_name
               val res as {outcome, ...} =
                 run_prover_for_mash ctxt params prover facts goal
-              val _ =
-                if is_none outcome then Synchronized.change ok (Integer.add 1)
-                else ()
-            in str_of_res heading facts res end
-          val [mepo_s, mash_s, mesh_s, isar_s] =
-            [fn () => prove mepo_ok MePoN fst mepo_facts,
-             fn () => prove mash_ok MaShN fst mash_facts,
-             fn () => prove mesh_ok MeShN I mesh_facts,
-             fn () => prove isar_ok IsarN fst isar_facts]
+              val ok = if is_none outcome then 1 else 0
+            in (str_of_res heading facts res, ok) end
+          val ress =
+            [fn () => prove MePoN fst mepo_facts,
+             fn () => prove MaShN fst mash_facts,
+             fn () => prove MeShN I mesh_facts,
+             fn () => prove IsarN fst isar_facts]
             |> (* Par_List. *) map (fn f => f ())
         in
-          ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
-           isar_s]
+          "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
           |> cat_lines |> print;
-          1
+          map snd ress
         end
       else
-        0
+        [0, 0, 0, 0]
     fun total_of heading ok n =
-      let val ok_val = Synchronized.value ok in
-        "  " ^ heading ^ ": " ^ string_of_int ok_val ^ " (" ^
-        Real.fmt (StringCvt.FIX (SOME 1))
-                 (100.0 * Real.fromInt ok_val / Real.fromInt n) ^ "%)"
-      end
+      "  " ^ heading ^ ": " ^ string_of_int ok ^ " (" ^
+      Real.fmt (StringCvt.FIX (SOME 1))
+               (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
     val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
       [prover, string_of_int (the max_facts) ^ " facts",
@@ -153,7 +144,10 @@
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val _ = print " * * *";
     val _ = print ("Options: " ^ commas options);
-    val n = Integer.sum (Par_List.map solve_goal (tag_list 1 lines))
+    val oks = Par_List.map solve_goal (tag_list 1 lines)
+    val n = length (hd oks)
+    val [mepo_ok, mash_ok, mesh_ok, isar_ok] =
+      map Integer.sum (map_transpose I oks)
   in
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,