avoid references altogether
authorblanchet
Tue Dec 18 02:19:14 2012 +0100 (2012-12-18)
changeset 50591c5e0073558f3
parent 50590 9d2f223ab6d9
child 50592 a39250169636
avoid references altogether
src/HOL/TPTP/mash_eval.ML
     1.1 --- a/src/HOL/TPTP/mash_eval.ML	Tue Dec 18 02:18:45 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Tue Dec 18 02:19:14 2012 +0100
     1.3 @@ -47,10 +47,6 @@
     1.4      val css = clasimpset_rule_table_of ctxt
     1.5      val facts = all_facts ctxt true false Symtab.empty [] [] css
     1.6      val all_names = build_all_names nickname_of facts
     1.7 -    val mepo_ok = Synchronized.var "mepo_ok" 0
     1.8 -    val mash_ok = Synchronized.var "mash_ok" 0
     1.9 -    val mesh_ok = Synchronized.var "mesh_ok" 0
    1.10 -    val isar_ok = Synchronized.var "isar_ok" 0
    1.11      fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
    1.12      fun index_string (j, s) = s ^ "@" ^ string_of_int j
    1.13      fun str_of_res label facts ({outcome, run_time, used_facts, ...}
    1.14 @@ -108,7 +104,7 @@
    1.15                  #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
    1.16                end
    1.17              | set_file_name _ NONE = I
    1.18 -          fun prove ok heading get facts =
    1.19 +          fun prove heading get facts =
    1.20              let
    1.21                fun nickify ((_, stature), th) =
    1.22                  ((K (escape_meta (nickname_of th)), stature), th)
    1.23 @@ -120,30 +116,25 @@
    1.24                val ctxt = ctxt |> set_file_name heading prob_dir_name
    1.25                val res as {outcome, ...} =
    1.26                  run_prover_for_mash ctxt params prover facts goal
    1.27 -              val _ =
    1.28 -                if is_none outcome then Synchronized.change ok (Integer.add 1)
    1.29 -                else ()
    1.30 -            in str_of_res heading facts res end
    1.31 -          val [mepo_s, mash_s, mesh_s, isar_s] =
    1.32 -            [fn () => prove mepo_ok MePoN fst mepo_facts,
    1.33 -             fn () => prove mash_ok MaShN fst mash_facts,
    1.34 -             fn () => prove mesh_ok MeShN I mesh_facts,
    1.35 -             fn () => prove isar_ok IsarN fst isar_facts]
    1.36 +              val ok = if is_none outcome then 1 else 0
    1.37 +            in (str_of_res heading facts res, ok) end
    1.38 +          val ress =
    1.39 +            [fn () => prove MePoN fst mepo_facts,
    1.40 +             fn () => prove MaShN fst mash_facts,
    1.41 +             fn () => prove MeShN I mesh_facts,
    1.42 +             fn () => prove IsarN fst isar_facts]
    1.43              |> (* Par_List. *) map (fn f => f ())
    1.44          in
    1.45 -          ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
    1.46 -           isar_s]
    1.47 +          "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
    1.48            |> cat_lines |> print;
    1.49 -          1
    1.50 +          map snd ress
    1.51          end
    1.52        else
    1.53 -        0
    1.54 +        [0, 0, 0, 0]
    1.55      fun total_of heading ok n =
    1.56 -      let val ok_val = Synchronized.value ok in
    1.57 -        "  " ^ heading ^ ": " ^ string_of_int ok_val ^ " (" ^
    1.58 -        Real.fmt (StringCvt.FIX (SOME 1))
    1.59 -                 (100.0 * Real.fromInt ok_val / Real.fromInt n) ^ "%)"
    1.60 -      end
    1.61 +      "  " ^ heading ^ ": " ^ string_of_int ok ^ " (" ^
    1.62 +      Real.fmt (StringCvt.FIX (SOME 1))
    1.63 +               (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
    1.64      val inst_inducts = Config.get ctxt instantiate_inducts
    1.65      val options =
    1.66        [prover, string_of_int (the max_facts) ^ " facts",
    1.67 @@ -153,7 +144,10 @@
    1.68         "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
    1.69      val _ = print " * * *";
    1.70      val _ = print ("Options: " ^ commas options);
    1.71 -    val n = Integer.sum (Par_List.map solve_goal (tag_list 1 lines))
    1.72 +    val oks = Par_List.map solve_goal (tag_list 1 lines)
    1.73 +    val n = length (hd oks)
    1.74 +    val [mepo_ok, mash_ok, mesh_ok, isar_ok] =
    1.75 +      map Integer.sum (map_transpose I oks)
    1.76    in
    1.77      ["Successes (of " ^ string_of_int n ^ " goals)",
    1.78       total_of MePoN mepo_ok n,