merged

--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 19:59:06 2012 +0200
@@ -26,7 +26,7 @@
 
 ML {*
 if do_it then
-  generate_accessibility thy false "/tmp/mash_accessibility"
+  generate_accessibility @{context} thy false "/tmp/mash_accessibility"
 else
   ()
 *}
@@ -40,14 +40,14 @@
 
 ML {*
 if do_it then
-  generate_isar_dependencies thy false "/tmp/mash_dependencies"
+  generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_commands @{context} prover thy "/tmp/mash_commands"
+  generate_commands @{context} params thy "/tmp/mash_commands"
 else
   ()
 *}

--- a/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -123,7 +123,8 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts =
-      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
+      Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false
+                                  Symtab.empty [] [] css_table
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>

--- a/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -36,8 +36,9 @@
     val slack_max_facts = max_facts_slack * the max_facts
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
-    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of (Proof_Context.init_global thy) css_table
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts =
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
     val all_names = all_names (facts |> map snd)
     val mepo_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0
@@ -70,7 +71,7 @@
         val th =
           case find_first (fn (_, th) => nickname_of th = name) facts of
             SOME (_, th) => th
-          | NONE => error ("No fact called \"" ^ name ^ "\"")
+          | NONE => error ("No fact called \"" ^ name ^ "\".")
         val goal = goal_of_thm thy th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val isar_deps = isar_dependencies_of all_names th |> these

--- a/src/HOL/TPTP/mash_export.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -9,14 +9,14 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val generate_accessibility : theory -> bool -> string -> unit
+  val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
   val generate_features :
     Proof.context -> string -> theory -> bool -> string -> unit
   val generate_isar_dependencies :
-    theory -> bool -> string -> unit
+    Proof.context -> theory -> bool -> string -> unit
   val generate_atp_dependencies :
     Proof.context -> params -> theory -> bool -> string -> unit
-  val generate_commands : Proof.context -> string -> theory -> string -> unit
+  val generate_commands : Proof.context -> params -> theory -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> theory -> int -> string -> unit
 end;
@@ -37,6 +37,12 @@
 fun has_thy thy th =
   Context.theory_name thy = Context.theory_name (theory_of_thm th)
 
+fun all_non_technical_facts ctxt thy =
+  let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
+    all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+    |> filter_out (is_thm_technical o snd)
+  end
+
 fun parent_facts thy thy_map =
   let
     fun add_last thy =
@@ -51,7 +57,12 @@
 
 val all_names = map (rpair () o nickname_of) #> Symtab.make
 
-fun generate_accessibility thy include_thy file_name =
+fun smart_dependencies_of ctxt params prover facts all_names th =
+  case atp_dependencies_of ctxt params prover 0 facts all_names th of
+    SOME deps => deps
+  | NONE => isar_dependencies_of all_names th |> these
+
+fun generate_accessibility ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -61,23 +72,22 @@
         val _ = File.append path s
       in [fact] end
     val thy_map =
-      all_facts_of (Proof_Context.init_global thy) Termtab.empty
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> thy_map_from_facts
     fun do_thy facts =
       let
         val thy = thy_of_fact thy (hd facts)
         val parents = parent_facts thy thy_map
-      in fold do_fact facts parents; () end
+      in fold_rev do_fact facts parents; () end
   in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
 
 fun generate_features ctxt prover thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      all_facts_of (Proof_Context.init_global thy) css_table
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
     fun do_fact ((_, stature), th) =
       let
@@ -88,12 +98,12 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun generate_isar_dependencies thy include_thy file_name =
+fun generate_isar_dependencies ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val ths =
-      all_facts_of (Proof_Context.init_global thy) Termtab.empty
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> map snd
     val all_names = all_names ths
@@ -112,27 +122,24 @@
     val _ = File.write path ""
     val prover = hd provers
     val facts =
-      all_facts_of (Proof_Context.init_global thy) Termtab.empty
+      all_non_technical_facts ctxt thy
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = all_names ths
     fun do_thm th =
       let
         val name = nickname_of th
-        val deps =
-          case atp_dependencies_of ctxt params prover 0 facts all_names th of
-            SOME deps => deps
-          | NONE => isar_dependencies_of all_names th |> these
+        val deps = smart_dependencies_of ctxt params prover facts all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
 
-fun generate_commands ctxt prover thy file_name =
+fun generate_commands ctxt (params as {provers, ...}) thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of (Proof_Context.init_global thy) css_table
+    val prover = hd provers
+    val facts = all_non_technical_facts ctxt thy
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
@@ -142,13 +149,13 @@
       let
         val name = nickname_of th
         val feats = features_of ctxt prover thy stature [prop_of th]
-        val deps = isar_dependencies_of all_names th |> these
+        val deps = smart_dependencies_of ctxt params prover facts all_names th
         val kind = Thm.legacy_get_kind th
-        val core = escape_metas prevs ^ "; " ^ escape_metas feats
+        val core =
+          escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
+          escape_metas feats
         val query = if kind <> "" then "? " ^ core ^ "\n" else ""
-        val update =
-          "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
-          escape_metas deps ^ "\n"
+        val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
         val _ = File.append path (query ^ update)
       in [name] end
     val thy_map = old_facts |> thy_map_from_facts
@@ -161,8 +168,7 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
-    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of (Proof_Context.init_global thy) css_table
+    val facts = all_non_technical_facts ctxt thy
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)

--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -52,8 +52,8 @@
 local
 
 fun make_cmd command options problem_path proof_path = space_implode " " (
-  map File.shell_quote (command () @ options) @
-  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
+  "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
+  [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
 
 fun trace_and ctxt msg f x =
   let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
@@ -99,7 +99,7 @@
     val ls = rev (snd (chop_while (equal "") (rev res)))
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
 
-    val _ = null ls andalso return_code <> 0 andalso
+    val _ = return_code <> 0 andalso
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in ls end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -29,7 +29,9 @@
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     -> (((unit -> string) * 'a) * thm) list
   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
-  val all_facts_of : Proof.context -> status Termtab.table -> fact list
+  val all_facts :
+    Proof.context -> bool -> unit Symtab.table -> thm list -> thm list
+    -> status Termtab.table -> fact list
   val nearly_all_facts :
     Proof.context -> bool -> fact_override -> unit Symtab.table
     -> status Termtab.table -> thm list -> term list -> term -> fact list
@@ -436,10 +438,6 @@
              |> op @
   end
 
-fun all_facts_of ctxt css =
-  all_facts ctxt false Symtab.empty [] [] css
-  |> rev (* partly restore the original order of facts, for MaSh *)
-
 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
                      concl_t =
   if only andalso null add then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -162,21 +162,22 @@
   #> (fn (name, value) =>
          if is_known_raw_param name then
            (name, value)
-         else if is_prover_list ctxt name andalso null value then
-           ("provers", [name])
-         else if can (type_enc_from_string Strict) name andalso null value then
-           ("type_enc", [name])
-         else if can (trans_lams_from_string ctxt any_type_enc) name andalso
-                 null value then
-           ("lam_trans", [name])
-         else if member (op =) fact_filters name then
-           ("fact_filter", [name])
-         else if can Int.fromString name then
-           ("max_facts", [name])
+         else if null value then
+           if is_prover_list ctxt name then
+             ("provers", [name])
+           else if can (type_enc_from_string Strict) name then
+             ("type_enc", [name])
+           else if can (trans_lams_from_string ctxt any_type_enc) name then
+             ("lam_trans", [name])
+           else if member (op =) fact_filters name then
+             ("fact_filter", [name])
+           else if is_some (Int.fromString name) then
+             ("max_facts", [name])
+           else
+             error ("Unknown parameter: " ^ quote name ^ ".")
          else
            error ("Unknown parameter: " ^ quote name ^ "."))
 
-
 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
    read correctly. *)
 val implode_param = strip_spaces_except_between_idents o space_implode " "

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -45,6 +45,7 @@
   val atp_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     -> thm -> string list option
+  val is_thm_technical : thm -> bool
   val mash_CLEAR : Proof.context -> unit
   val mash_ADD :
     Proof.context -> bool
@@ -399,6 +400,14 @@
       | _ => NONE
     end
 
+val technical_theories =
+  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
+   "New_DSequence", "New_Random_Sequence", "Quickcheck",
+   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
+
+val is_thm_technical =
+  member (op =) technical_theories o Context.theory_name o theory_of_thm
+
 
 (*** Low-level communication with MaSh ***)
 
@@ -700,14 +709,6 @@
           (true, "")
         end)
 
-val evil_theories =
-  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
-   "New_DSequence", "New_Random_Sequence", "Quickcheck",
-   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
-
-fun fact_has_evil_theory (_, th) =
-  member (op =) evil_theories (Context.theory_name (theory_of_thm th))
-
 fun sendback sub =
   Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
 
@@ -722,7 +723,7 @@
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
     val {fact_G} = mash_get ctxt
     val (old_facts, new_facts) =
-      facts |> filter_out fact_has_evil_theory
+      facts |> filter_out (is_thm_technical o snd)
             |> List.partition (is_fact_in_graph fact_G)
             ||> sort (thm_ord o pairself snd)
   in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -775,9 +775,9 @@
             val args = arguments ctxt full_proof extra slice_timeout
                                  (ord, ord_info, sel_weights)
             val command =
-              File.shell_path command0 ^ " " ^ args ^ " " ^
-              File.shell_path prob_file
-              |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
+              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
+              File.shell_path prob_file ^ ")"
+              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
             val _ =
               atp_problem
               |> lines_for_atp_problem format ord ord_info

--- a/src/HOL/Tools/try0.ML	Thu Jul 26 19:57:33 2012 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Jul 26 19:59:06 2012 +0200
@@ -77,12 +77,13 @@
   if mode <> Auto_Try orelse run_if_auto_try then
     let val attrs = attrs_text attrs quad in
       do_generic timeout_opt
-                 (name ^ (if all_goals andalso
-                             nprems_of (#goal (Proof.goal st)) > 1 then
-                            "[1]"
-                          else
-                            "") ^
-                  attrs) I (#goal o Proof.goal)
+                 (name ^ attrs ^
+                  (if all_goals andalso
+                      nprems_of (#goal (Proof.goal st)) > 1 then
+                     " [1]"
+                   else
+                     ""))
+                 I (#goal o Proof.goal)
                  (apply_named_method_on_first_goal (name ^ attrs)
                                                    (Proof.theory_of st)) st
     end