merged

--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 05 11:05:23 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 05 11:05:34 2012 +0100
@@ -11,8 +11,8 @@
 ML_file "mash_eval.ML"
 
 sledgehammer_params
-  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
-   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+  [provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native,
+   lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
 
 declare [[sledgehammer_instantiate_inducts]]
 
@@ -22,13 +22,12 @@
 
 ML {*
 val do_it = false (* switch to "true" to generate the files *)
-val thy = @{theory Nat}
 val params = Sledgehammer_Isar.default_params @{context} []
 *}
 
 ML {*
 if do_it then
-  evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions"
+  evaluate_mash_suggestions @{context} params "/tmp/mash_suggestions"
 else
   ()
 *}

--- a/src/HOL/TPTP/mash_eval.ML	Wed Dec 05 11:05:23 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Dec 05 11:05:34 2012 +0100
@@ -9,8 +9,7 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val evaluate_mash_suggestions :
-    Proof.context -> params -> theory -> string -> unit
+  val evaluate_mash_suggestions : Proof.context -> params -> string -> unit
 end;
 
 structure MaSh_Eval : MASH_EVAL =
@@ -28,7 +27,7 @@
 
 val all_names = map (rpair () o nickname_of) #> Symtab.make
 
-fun evaluate_mash_suggestions ctxt params thy file_name =
+fun evaluate_mash_suggestions ctxt params file_name =
   let
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
       Sledgehammer_Isar.default_params ctxt []
@@ -37,8 +36,7 @@
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts =
-      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+    val facts = all_facts ctxt false Symtab.empty [] [] css
     val all_names = all_names (facts |> map snd)
     val mepo_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0
@@ -72,7 +70,7 @@
           case find_first (fn (_, th) => nickname_of th = name) facts of
             SOME (_, th) => th
           | NONE => error ("No fact called \"" ^ name ^ "\".")
-        val goal = goal_of_thm thy th
+        val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val isar_deps = isar_dependencies_of all_names th |> these
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)

--- a/src/HOL/TPTP/mash_export.ML	Wed Dec 05 11:05:23 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Wed Dec 05 11:05:34 2012 +0100
@@ -93,7 +93,7 @@
         val name = nickname_of th
         val feats =
           features_of ctxt prover (theory_of_thm th) stature [prop_of th]
-        val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
+        val s = escape_meta name ^ ": " ^ encode_features feats ^ "\n"
       in File.append path s end
   in List.app do_fact facts end
 
@@ -156,7 +156,7 @@
         val kind = Thm.legacy_get_kind th
         val core =
           escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
-          escape_metas feats
+          encode_features feats
         val query =
           if kind = "" orelse null deps then "" else "? " ^ core ^ "\n"
         val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 11:05:23 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 11:05:34 2012 +0100
@@ -28,15 +28,16 @@
   val escape_metas : string list -> string
   val unescape_meta : string -> string
   val unescape_metas : string -> string list
+  val encode_features : (string * real) list -> string
   val extract_query : string -> string * (string * real) list
   val mash_CLEAR : Proof.context -> unit
   val mash_ADD :
     Proof.context -> bool
-    -> (string * string list * string list * string list) list -> unit
+    -> (string * string list * (string * real) list * string list) list -> unit
   val mash_REPROVE :
     Proof.context -> bool -> (string * string list) list -> unit
   val mash_QUERY :
-    Proof.context -> bool -> int -> string list * string list
+    Proof.context -> bool -> int -> string list * (string * real) list
     -> (string * real) list
   val mash_unlearn : Proof.context -> unit
   val nickname_of : thm -> string
@@ -50,7 +51,8 @@
   val run_prover_for_mash :
     Proof.context -> params -> string -> fact list -> thm -> prover_result
   val features_of :
-    Proof.context -> string -> theory -> stature -> term list -> string list
+    Proof.context -> string -> theory -> stature -> term list
+    -> (string * real) list
   val isar_dependencies_of : unit Symtab.table -> thm -> string list option
   val atp_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
@@ -176,15 +178,30 @@
 val unescape_metas =
   space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
 
+val supports_weights = false
+
+fun encode_feature (name, weight) =
+  let val s = escape_meta name in
+    if Real.== (weight, 1.0) then
+      s
+    else if supports_weights then
+      s ^ "=" ^ Real.toString weight
+    else
+      map (prefix (s ^ ".") o string_of_int) (1 upto Real.ceil weight)
+      |> space_implode " "
+  end
+
+val encode_features = map encode_feature #> space_implode " "
+
 fun str_of_add (name, parents, feats, deps) =
   "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
-  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
+  encode_features feats ^ "; " ^ escape_metas deps ^ "\n"
 
 fun str_of_reprove (name, deps) =
   "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
 
 fun str_of_query (parents, feats) =
-  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
+  "? " ^ escape_metas parents ^ "; " ^ encode_features feats ^ "\n"
 
 fun extract_suggestion sugg =
   case space_explode "=" sugg of
@@ -221,7 +238,7 @@
      run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ()))
 
 fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
-  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
+  (trace_msg ctxt (fn () => "MaSh QUERY " ^ encode_features feats);
    run_mash_tool ctxt overlord false max_suggs
        ([query], str_of_query)
        (fn suggs =>
@@ -280,7 +297,9 @@
 
 local
 
-val version = "*** MaSh 0.1 ***"
+val version = "*** MaSh version 20121204a ***"
+
+exception Too_New of unit
 
 fun extract_node line =
   case space_explode ":" line of
@@ -309,8 +328,12 @@
                update_fact_graph_node (name, kind)
                #> fold (add_edge_to name) parents
            val fact_G =
-             try_graph ctxt "loading state" Graph.empty (fn () =>
-                 Graph.empty |> version' = version ? fold add_node node_lines)
+             case string_ord (version', version) of
+               EQUAL =>
+               try_graph ctxt "loading state" Graph.empty (fn () =>
+                   fold add_node node_lines Graph.empty)
+             | LESS => Graph.empty (* can't parse old file *)
+             | GREATER => raise Too_New ()
          in
            trace_msg ctxt (fn () =>
                "Loaded fact graph (" ^ graph_info fact_G ^ ")");
@@ -350,12 +373,14 @@
 
 fun mash_map ctxt f =
   Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
+  handle Too_New () => ()
 
 fun mash_peek ctxt f =
-  Synchronized.change_result global_state (load ctxt #> `snd #>> f)
+  Synchronized.change_result global_state
+      (perhaps (try (load ctxt)) #> `snd #>> f)
 
 fun mash_get ctxt =
-  Synchronized.change_result global_state (load ctxt #> `snd)
+  Synchronized.change_result global_state (perhaps (try (load ctxt)) #> `snd)
 
 fun mash_unlearn ctxt =
   Synchronized.change global_state (fn _ =>
@@ -428,10 +453,14 @@
             |> map snd |> take max_facts
     end
 
-val thy_feature_name_of = prefix "y"
-val const_name_of = prefix "c"
-val type_name_of = prefix "t"
-val class_name_of = prefix "s"
+fun thy_feature_of s = ("y" ^ s, 1.0 (* FUDGE *))
+fun term_feature_of s = ("c" ^ s, 1.0 (* FUDGE *))
+fun type_feature_of s = ("t" ^ s, 1.0 (* FUDGE *))
+fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
+fun status_feature_of status = (string_of_status status, 1.0 (* FUDGE *))
+val local_feature = ("local", 20.0 (* FUDGE *))
+val lams_feature = ("lams", 1.0 (* FUDGE *))
+val skos_feature = ("skos", 1.0 (* FUDGE *))
 
 fun theory_ord p =
   if Theory.eq_thy p then
@@ -444,7 +473,12 @@
     EQUAL => string_ord (pairself Context.theory_name p)
   | order => order
 
-val thm_ord = theory_ord o pairself theory_of_thm
+fun thm_ord thp =
+  case theory_ord (pairself theory_of_thm thp) of
+    EQUAL =>
+    (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
+    string_ord (pairself nickname_of (swap thp))
+  | ord => ord
 
 val freezeT = Type.legacy_freeze_type
 
@@ -480,24 +514,26 @@
       member (op =) logical_consts s orelse
       fst (is_built_in_const_for_prover ctxt prover x args)
     fun add_classes @{sort type} = I
-      | add_classes S = union (op =) (map class_name_of S)
+      | add_classes S = union (op = o pairself fst) (map class_feature_of S)
     fun do_add_type (Type (s, Ts)) =
-        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
+        (not (member (op =) bad_types s)
+         ? insert (op = o pairself fst) (type_feature_of s))
         #> fold do_add_type Ts
       | do_add_type (TFree (_, S)) = add_classes S
       | do_add_type (TVar (_, S)) = add_classes S
     fun add_type T = type_max_depth >= 0 ? do_add_type T
     fun patternify_term _ ~1 _ = []
       | patternify_term args _ (Const (x as (s, _))) =
-        if is_bad_const x args then [] else [const_name_of s]
+        if is_bad_const x args then [] else [s]
       | patternify_term _ 0 _ = []
       | patternify_term args depth (t $ u) =
         let
           val ps = patternify_term (u :: args) depth t
           val qs = "" :: patternify_term [] (depth - 1) u
-        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
+        in map_product (fn p => fn "" => p | q => "(" ^ q ^ ")") ps qs end
       | patternify_term _ _ _ = []
-    val add_term_pattern = union (op =) oo patternify_term []
+    val add_term_pattern =
+      union (op = o pairself fst) o map term_feature_of oo patternify_term []
     fun add_term_patterns ~1 _ = I
       | add_term_patterns depth t =
         add_term_pattern depth t #> add_term_patterns (depth - 1) t
@@ -521,15 +557,13 @@
 
 (* TODO: Generate type classes for types? *)
 fun features_of ctxt prover thy (scope, status) ts =
-  thy_feature_name_of (Context.theory_name thy) ::
+  thy_feature_of (Context.theory_name thy) ::
   interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
                                       ts
-(* Temporarily disabled: These frequent features can easily dominate the others.
-  |> exists (not o is_lambda_free) ts ? cons "lams"
-  |> exists (exists_Const is_exists) ts ? cons "skos"
-  |> scope <> Global ? cons "local"
-*)
-  |> (case string_of_status status of "" => I | s => cons s)
+  |> status <> General ? cons (status_feature_of status)
+  |> scope <> Global ? cons local_feature
+  |> exists (not o is_lambda_free) ts ? cons lams_feature
+  |> exists (exists_Const is_exists) ts ? cons skos_feature
 
 (* Too many dependencies is a sign that a crazy decision procedure is at work.
    There isn't much to learn from such proofs. *)