moved most of MaSh exporter code to Sledgehammer
authorblanchet
Wed Jul 11 21:43:19 2012 +0200 (2012-07-11)
changeset 482516cdcfbddc077
parent 48250 1065c307fafe
child 48252 e98c3d50ae62
moved most of MaSh exporter code to Sledgehammer
src/HOL/Sledgehammer.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/MaSh_Import.thy
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_export.ML
src/HOL/TPTP/mash_import.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -14,9 +14,9 @@
     1.4       "Tools/Sledgehammer/sledgehammer_fact.ML"
     1.5       "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
     1.6       "Tools/Sledgehammer/sledgehammer_provers.ML"
     1.7 +     "Tools/Sledgehammer/sledgehammer_minimize.ML"
     1.8       "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
     1.9       "Tools/Sledgehammer/sledgehammer_filter.ML"
    1.10 -     "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.11       "Tools/Sledgehammer/sledgehammer_run.ML"
    1.12       "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.13  begin
     2.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     2.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     2.3 @@ -14,17 +14,19 @@
     2.4     lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
     2.5  
     2.6  ML {*
     2.7 +open Sledgehammer_Filter_MaSh
     2.8  open MaSh_Export
     2.9  *}
    2.10  
    2.11  ML {*
    2.12  val do_it = false (* switch to "true" to generate the files *);
    2.13 -val thy = @{theory Nat}
    2.14 +val thy = @{theory Nat};
    2.15 +val params = Sledgehammer_Isar.default_params @{context} []
    2.16  *}
    2.17  
    2.18  ML {*
    2.19  if do_it then
    2.20 -  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
    2.21 +  generate_accessibility thy false "/tmp/mash_accessibility"
    2.22  else
    2.23    ()
    2.24  *}
    2.25 @@ -38,13 +40,6 @@
    2.26  
    2.27  ML {*
    2.28  if do_it then
    2.29 -  generate_accessibility thy false "/tmp/mash_accessibility"
    2.30 -else
    2.31 -  ()
    2.32 -*}
    2.33 -
    2.34 -ML {*
    2.35 -if do_it then
    2.36    generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
    2.37  else
    2.38    ()
    2.39 @@ -52,7 +47,7 @@
    2.40  
    2.41  ML {*
    2.42  if do_it then
    2.43 -  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
    2.44 +  generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies"
    2.45  else
    2.46    ()
    2.47  *}
    2.48 @@ -66,7 +61,7 @@
    2.49  
    2.50  ML {*
    2.51  if do_it then
    2.52 -  generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
    2.53 +  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
    2.54  else
    2.55    ()
    2.56  *}
     3.1 --- a/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 11 21:43:19 2012 +0200
     3.2 +++ b/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 11 21:43:19 2012 +0200
     3.3 @@ -16,13 +16,14 @@
     3.4  *}
     3.5  
     3.6  ML {*
     3.7 -val do_it = true (* switch to "true" to generate the files *);
     3.8 -val thy = @{theory List}
     3.9 +val do_it = false (* switch to "true" to generate the files *);
    3.10 +val thy = @{theory List};
    3.11 +val params = Sledgehammer_Isar.default_params @{context} []
    3.12  *}
    3.13  
    3.14  ML {*
    3.15  if do_it then
    3.16 -  import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
    3.17 +  import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list"
    3.18  else
    3.19    ()
    3.20  *}
     4.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 11 21:43:19 2012 +0200
     4.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 11 21:43:19 2012 +0200
     4.3 @@ -8,11 +8,7 @@
     4.4  signature ATP_THEORY_EXPORT =
     4.5  sig
     4.6    type atp_format = ATP_Problem.atp_format
     4.7 -  type stature = Sledgehammer_Filter.stature
     4.8  
     4.9 -  val theorems_mentioned_in_proof_term :
    4.10 -    string list option -> thm -> string list
    4.11 -  val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list
    4.12    val generate_atp_inference_file_for_theory :
    4.13      Proof.context -> theory -> atp_format -> string -> string -> unit
    4.14  end;
    4.15 @@ -27,45 +23,6 @@
    4.16  
    4.17  val fact_name_of = prefix fact_prefix o ascii_of
    4.18  
    4.19 -(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    4.20 -   fixes that seem to be missing over there; or maybe the two code portions are
    4.21 -   not doing the same? *)
    4.22 -fun fold_body_thms thm_name f =
    4.23 -  let
    4.24 -    fun app n (PBody {thms, ...}) =
    4.25 -      thms |> fold (fn (_, (name, prop, body)) => fn x =>
    4.26 -        let
    4.27 -          val body' = Future.join body
    4.28 -          val n' =
    4.29 -            n + (if name = "" orelse
    4.30 -                    (* uncommon case where the proved theorem occurs twice
    4.31 -                       (e.g., "Transitive_Closure.trancl_into_trancl") *)
    4.32 -                    (n = 1 andalso name = thm_name) then
    4.33 -                   0
    4.34 -                 else
    4.35 -                   1)
    4.36 -          val x' = x |> n' <= 1 ? app n' body'
    4.37 -        in (x' |> n = 1 ? f (name, prop, body')) end)
    4.38 -  in fold (app 0) end
    4.39 -
    4.40 -fun theorems_mentioned_in_proof_term all_names th =
    4.41 -  let
    4.42 -    val is_name_ok =
    4.43 -      case all_names of
    4.44 -        SOME names => member (op =) names
    4.45 -      | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
    4.46 -    fun collect (s, _, _) = is_name_ok s ? insert (op =) s
    4.47 -    val names =
    4.48 -      [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
    4.49 -  in names end
    4.50 -
    4.51 -fun all_facts_of_theory thy =
    4.52 -  let val ctxt = Proof_Context.init_global thy in
    4.53 -    Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
    4.54 -        (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
    4.55 -    |> rev (* try to restore the original order of facts, for MaSh *)
    4.56 -  end
    4.57 -
    4.58  fun inference_term [] = NONE
    4.59    | inference_term ss =
    4.60      ATerm (("inference", []),
    4.61 @@ -153,7 +110,7 @@
    4.62      val mono = not (is_type_enc_polymorphic type_enc)
    4.63      val path = file_name |> Path.explode
    4.64      val _ = File.write path ""
    4.65 -    val facts = all_facts_of_theory thy
    4.66 +    val facts = Sledgehammer_Fact.all_facts_of thy
    4.67      val atp_problem =
    4.68        facts
    4.69        |> map (fn ((_, loc), th) =>
    4.70 @@ -170,7 +127,7 @@
    4.71      val infers =
    4.72        facts |> map (fn (_, th) =>
    4.73                         (fact_name_of (Thm.get_name_hint th),
    4.74 -                        th |> theorems_mentioned_in_proof_term (SOME all_names)
    4.75 +                        th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
    4.76                             |> map fact_name_of))
    4.77      val all_atp_problem_names =
    4.78        atp_problem |> maps (map ident_of_problem_line o snd)
     5.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
     5.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
     5.3 @@ -7,348 +7,23 @@
     5.4  
     5.5  signature MASH_EXPORT =
     5.6  sig
     5.7 -  type stature = ATP_Problem_Generate.stature
     5.8 -  type prover_result = Sledgehammer_Provers.prover_result
     5.9 +  type params = Sledgehammer_Provers.params
    5.10  
    5.11 -  val non_tautological_facts_of :
    5.12 -    theory -> (((unit -> string) * stature) * thm) list
    5.13 -  val theory_ord : theory * theory -> order
    5.14 -  val thm_ord : thm * thm -> order
    5.15 -  val dependencies_of : string list -> thm -> string list
    5.16 -  val goal_of_thm : theory -> thm -> thm
    5.17 -  val meng_paulson_facts :
    5.18 -    Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list
    5.19 -    -> ((string * stature) * thm) list
    5.20 -  val run_sledgehammer :
    5.21 -    Proof.context -> ((string * stature) * thm) list -> thm -> prover_result
    5.22 -  val generate_accessibility : theory -> bool -> string -> unit
    5.23 -  val generate_features : theory -> bool -> string -> unit
    5.24 -  val generate_isa_dependencies : theory -> bool -> string -> unit
    5.25 -  val generate_atp_dependencies :
    5.26 -    Proof.context -> theory -> bool -> string -> unit
    5.27    val generate_commands : theory -> string -> unit
    5.28 -  val generate_meng_paulson_suggestions :
    5.29 -    Proof.context -> theory -> int -> string -> unit
    5.30 +  val generate_iter_suggestions :
    5.31 +    Proof.context -> params -> theory -> int -> string -> unit
    5.32  end;
    5.33  
    5.34  structure MaSh_Export : MASH_EXPORT =
    5.35  struct
    5.36  
    5.37 -open ATP_Util
    5.38 -open ATP_Problem_Generate
    5.39 -open ATP_Theory_Export
    5.40 -
    5.41 -type prover_result = Sledgehammer_Provers.prover_result
    5.42 -
    5.43 -fun stringN_of_int 0 _ = ""
    5.44 -  | stringN_of_int k n =
    5.45 -    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
    5.46 -
    5.47 -fun escape_meta_char c =
    5.48 -  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
    5.49 -     c = #")" orelse c = #"," then
    5.50 -    String.str c
    5.51 -  else
    5.52 -    (* fixed width, in case more digits follow *)
    5.53 -    "\\" ^ stringN_of_int 3 (Char.ord c)
    5.54 -
    5.55 -val escape_meta = String.translate escape_meta_char
    5.56 -
    5.57 -val thy_prefix = "y_"
    5.58 -
    5.59 -val fact_name_of = escape_meta
    5.60 -val thy_name_of = prefix thy_prefix o escape_meta
    5.61 -val const_name_of = prefix const_prefix o escape_meta
    5.62 -val type_name_of = prefix type_const_prefix o escape_meta
    5.63 -val class_name_of = prefix class_prefix o escape_meta
    5.64 -
    5.65 -val thy_name_of_thm = theory_of_thm #> Context.theory_name
    5.66 -
    5.67 -local
    5.68 -
    5.69 -fun has_bool @{typ bool} = true
    5.70 -  | has_bool (Type (_, Ts)) = exists has_bool Ts
    5.71 -  | has_bool _ = false
    5.72 -
    5.73 -fun has_fun (Type (@{type_name fun}, _)) = true
    5.74 -  | has_fun (Type (_, Ts)) = exists has_fun Ts
    5.75 -  | has_fun _ = false
    5.76 -
    5.77 -val is_conn = member (op =)
    5.78 -  [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
    5.79 -   @{const_name HOL.implies}, @{const_name Not},
    5.80 -   @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
    5.81 -   @{const_name HOL.eq}]
    5.82 -
    5.83 -val has_bool_arg_const =
    5.84 -  exists_Const (fn (c, T) =>
    5.85 -                   not (is_conn c) andalso exists has_bool (binder_types T))
    5.86 -
    5.87 -fun higher_inst_const thy (c, T) =
    5.88 -  case binder_types T of
    5.89 -    [] => false
    5.90 -  | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
    5.91 -
    5.92 -val binders = [@{const_name All}, @{const_name Ex}]
    5.93 -
    5.94 -in
    5.95 -
    5.96 -fun is_fo_term thy t =
    5.97 -  let
    5.98 -    val t =
    5.99 -      t |> Envir.beta_eta_contract
   5.100 -        |> transform_elim_prop
   5.101 -        |> Object_Logic.atomize_term thy
   5.102 -  in
   5.103 -    Term.is_first_order binders t andalso
   5.104 -    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
   5.105 -                          | _ => false) t orelse
   5.106 -         has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
   5.107 -  end
   5.108 -
   5.109 -end
   5.110 -
   5.111 -fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
   5.112 -  let
   5.113 -    val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
   5.114 -    val bad_consts = atp_widely_irrelevant_consts
   5.115 -    fun do_add_type (Type (s, Ts)) =
   5.116 -        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
   5.117 -        #> fold do_add_type Ts
   5.118 -      | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
   5.119 -      | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S)
   5.120 -    fun add_type T = type_max_depth >= 0 ? do_add_type T
   5.121 -    fun mk_app s args =
   5.122 -      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
   5.123 -      else s
   5.124 -    fun patternify ~1 _ = ""
   5.125 -      | patternify depth t =
   5.126 -        case strip_comb t of
   5.127 -          (Const (s, _), args) =>
   5.128 -          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
   5.129 -        | _ => ""
   5.130 -    fun add_term_patterns ~1 _ = I
   5.131 -      | add_term_patterns depth t =
   5.132 -        insert (op =) (patternify depth t)
   5.133 -        #> add_term_patterns (depth - 1) t
   5.134 -    val add_term = add_term_patterns term_max_depth
   5.135 -    fun add_patterns t =
   5.136 -      let val (head, args) = strip_comb t in
   5.137 -        (case head of
   5.138 -           Const (s, T) =>
   5.139 -           not (member (op =) bad_consts s) ? (add_term t #> add_type T)
   5.140 -         | Free (_, T) => add_type T
   5.141 -         | Var (_, T) => add_type T
   5.142 -         | Abs (_, T, body) => add_type T #> add_patterns body
   5.143 -         | _ => I)
   5.144 -        #> fold add_patterns args
   5.145 -      end
   5.146 -  in [] |> add_patterns t |> sort string_ord end
   5.147 -
   5.148 -fun is_likely_tautology th =
   5.149 -  null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
   5.150 -  not (Thm.eq_thm_prop (@{thm ext}, th))
   5.151 -
   5.152 -fun is_too_meta thy th =
   5.153 -  fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
   5.154 -
   5.155 -fun non_tautological_facts_of thy =
   5.156 -  all_facts_of_theory thy
   5.157 -  |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
   5.158 -
   5.159 -fun theory_ord p =
   5.160 -  if Theory.eq_thy p then EQUAL
   5.161 -  else if Theory.subthy p then LESS
   5.162 -  else if Theory.subthy (swap p) then GREATER
   5.163 -  else EQUAL
   5.164 -
   5.165 -val thm_ord = theory_ord o pairself theory_of_thm
   5.166 -
   5.167 -fun thms_by_thy ths =
   5.168 -  ths |> map (snd #> `thy_name_of_thm)
   5.169 -      |> AList.group (op =)
   5.170 -      |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
   5.171 -                                   o hd o snd))
   5.172 -      |> map (apsnd (sort thm_ord))
   5.173 -
   5.174 -fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
   5.175 -
   5.176 -fun parent_thms thy_ths thy =
   5.177 -  Theory.parents_of thy
   5.178 -  |> map Context.theory_name
   5.179 -  |> map_filter (AList.lookup (op =) thy_ths)
   5.180 -  |> map List.last
   5.181 -  |> map (fact_name_of o Thm.get_name_hint)
   5.182 -
   5.183 -fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
   5.184 -
   5.185 -val max_depth = 1
   5.186 -
   5.187 -(* TODO: Generate type classes for types? *)
   5.188 -fun features_of thy (status, th) =
   5.189 -  let val t = Thm.prop_of th in
   5.190 -    thy_name_of (thy_name_of_thm th) ::
   5.191 -    interesting_terms_types_and_classes max_depth max_depth t
   5.192 -    |> not (has_no_lambdas t) ? cons "lambdas"
   5.193 -    |> exists_Const is_exists t ? cons "skolems"
   5.194 -    |> not (is_fo_term thy t) ? cons "ho"
   5.195 -    |> (case status of
   5.196 -          General => I
   5.197 -        | Induction => cons "induction"
   5.198 -        | Intro => cons "intro"
   5.199 -        | Inductive => cons "inductive"
   5.200 -        | Elim => cons "elim"
   5.201 -        | Simp => cons "simp"
   5.202 -        | Def => cons "def")
   5.203 -  end
   5.204 -
   5.205 -fun dependencies_of all_facts =
   5.206 -  theorems_mentioned_in_proof_term (SOME all_facts)
   5.207 -  #> map fact_name_of
   5.208 -  #> sort string_ord
   5.209 -
   5.210 -val freezeT = Type.legacy_freeze_type
   5.211 -
   5.212 -fun freeze (t $ u) = freeze t $ freeze u
   5.213 -  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
   5.214 -  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   5.215 -  | freeze (Const (s, T)) = Const (s, freezeT T)
   5.216 -  | freeze (Free (s, T)) = Free (s, freezeT T)
   5.217 -  | freeze t = t
   5.218 -
   5.219 -fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
   5.220 -
   5.221 -fun meng_paulson_facts ctxt max_relevant goal =
   5.222 -  let
   5.223 -    val {provers, relevance_thresholds, ...} =
   5.224 -      Sledgehammer_Isar.default_params ctxt []
   5.225 -    val prover_name = hd provers
   5.226 -    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
   5.227 -    val is_built_in_const =
   5.228 -      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
   5.229 -    val relevance_fudge =
   5.230 -      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
   5.231 -    val relevance_override = {add = [], del = [], only = false}
   5.232 -  in
   5.233 -    Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
   5.234 -        max_relevant is_built_in_const relevance_fudge relevance_override []
   5.235 -        hyp_ts concl_t
   5.236 -  end
   5.237 -
   5.238 -fun run_sledgehammer ctxt facts goal =
   5.239 -  let
   5.240 -    val params as {provers, ...} = Sledgehammer_Isar.default_params ctxt []
   5.241 -    val problem =
   5.242 -      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
   5.243 -       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
   5.244 -    val prover =
   5.245 -      Sledgehammer_Minimize.get_minimizing_prover ctxt
   5.246 -          Sledgehammer_Provers.Normal (hd provers)
   5.247 -  in prover params (K (K (K ""))) problem end
   5.248 -
   5.249 -fun generate_accessibility thy include_thy file_name =
   5.250 -  let
   5.251 -    val path = file_name |> Path.explode
   5.252 -    val _ = File.write path ""
   5.253 -    fun do_thm th prevs =
   5.254 -      let
   5.255 -        val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
   5.256 -        val _ = File.append path s
   5.257 -      in [th] end
   5.258 -    val thy_ths =
   5.259 -      non_tautological_facts_of thy
   5.260 -      |> not include_thy ? filter_out (has_thy thy o snd)
   5.261 -      |> thms_by_thy
   5.262 -    fun do_thy ths =
   5.263 -      let
   5.264 -        val thy = theory_of_thm (hd ths)
   5.265 -        val parents = parent_thms thy_ths thy
   5.266 -        val ths = ths |> map (fact_name_of o Thm.get_name_hint)
   5.267 -      in fold do_thm ths parents; () end
   5.268 -  in List.app (do_thy o snd) thy_ths end
   5.269 -
   5.270 -fun generate_features thy include_thy file_name =
   5.271 -  let
   5.272 -    val path = file_name |> Path.explode
   5.273 -    val _ = File.write path ""
   5.274 -    val facts =
   5.275 -      non_tautological_facts_of thy
   5.276 -      |> not include_thy ? filter_out (has_thy thy o snd)
   5.277 -    fun do_fact ((_, (_, status)), th) =
   5.278 -      let
   5.279 -        val name = Thm.get_name_hint th
   5.280 -        val feats = features_of thy (status, th)
   5.281 -        val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
   5.282 -      in File.append path s end
   5.283 -  in List.app do_fact facts end
   5.284 -
   5.285 -fun generate_isa_dependencies thy include_thy file_name =
   5.286 -  let
   5.287 -    val path = file_name |> Path.explode
   5.288 -    val _ = File.write path ""
   5.289 -    val ths =
   5.290 -      non_tautological_facts_of thy
   5.291 -      |> not include_thy ? filter_out (has_thy thy o snd)
   5.292 -      |> map snd
   5.293 -    val all_names = ths |> map Thm.get_name_hint
   5.294 -    fun do_thm th =
   5.295 -      let
   5.296 -        val name = Thm.get_name_hint th
   5.297 -        val deps = dependencies_of all_names th
   5.298 -        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
   5.299 -      in File.append path s end
   5.300 -  in List.app do_thm ths end
   5.301 -
   5.302 -fun generate_atp_dependencies ctxt thy include_thy file_name =
   5.303 -  let
   5.304 -    val {max_relevant, ...} = Sledgehammer_Isar.default_params ctxt []
   5.305 -    val path = file_name |> Path.explode
   5.306 -    val _ = File.write path ""
   5.307 -    val facts =
   5.308 -      non_tautological_facts_of thy
   5.309 -      |> not include_thy ? filter_out (has_thy thy o snd)
   5.310 -    val ths = facts |> map snd
   5.311 -    val all_names = ths |> map Thm.get_name_hint
   5.312 -    fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
   5.313 -    fun add_isa_dep facts dep accum =
   5.314 -      if exists (is_dep dep) accum then
   5.315 -        accum
   5.316 -      else case find_first (is_dep dep) facts of
   5.317 -        SOME ((name, status), th) => accum @ [((name (), status), th)]
   5.318 -      | NONE => accum (* shouldn't happen *)
   5.319 -    fun fix_name ((_, stature), th) =
   5.320 -      ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
   5.321 -    fun do_thm th =
   5.322 -      let
   5.323 -        val name = Thm.get_name_hint th
   5.324 -        val goal = goal_of_thm thy th
   5.325 -        val deps =
   5.326 -          case dependencies_of all_names th of
   5.327 -            [] => []
   5.328 -          | isa_dep as [_] => isa_dep (* can hardly beat that *)
   5.329 -          | isa_deps =>
   5.330 -            let
   5.331 -              val facts =
   5.332 -                facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
   5.333 -              val facts =
   5.334 -                facts |> meng_paulson_facts ctxt (the max_relevant) goal
   5.335 -                      |> fold (add_isa_dep facts) isa_deps
   5.336 -                      |> map fix_name
   5.337 -            in
   5.338 -              case run_sledgehammer ctxt facts goal of
   5.339 -                {outcome = NONE, used_facts, ...} =>
   5.340 -                used_facts |> map fst |> sort string_ord
   5.341 -              | _ => isa_deps
   5.342 -            end
   5.343 -        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
   5.344 -      in File.append path s end
   5.345 -  in List.app do_thm ths end
   5.346 +open Sledgehammer_Filter_MaSh
   5.347  
   5.348  fun generate_commands thy file_name =
   5.349    let
   5.350      val path = file_name |> Path.explode
   5.351      val _ = File.write path ""
   5.352 -    val facts = non_tautological_facts_of thy
   5.353 +    val facts = all_non_tautological_facts_of thy
   5.354      val (new_facts, old_facts) =
   5.355        facts |> List.partition (has_thy thy o snd)
   5.356              |>> sort (thm_ord o pairself snd)
   5.357 @@ -358,7 +33,7 @@
   5.358        let
   5.359          val name = Thm.get_name_hint th
   5.360          val feats = features_of thy (status, th)
   5.361 -        val deps = dependencies_of all_names th
   5.362 +        val deps = isabelle_dependencies_of all_names th
   5.363          val kind = Thm.legacy_get_kind th
   5.364          val name = fact_name_of name
   5.365          val core =
   5.366 @@ -371,11 +46,11 @@
   5.367      val parents = parent_thms thy_ths thy
   5.368    in fold do_fact new_facts parents; () end
   5.369  
   5.370 -fun generate_meng_paulson_suggestions ctxt thy max_relevant file_name =
   5.371 +fun generate_iter_suggestions ctxt params thy max_relevant file_name =
   5.372    let
   5.373      val path = file_name |> Path.explode
   5.374      val _ = File.write path ""
   5.375 -    val facts = non_tautological_facts_of thy
   5.376 +    val facts = all_non_tautological_facts_of thy
   5.377      val (new_facts, old_facts) =
   5.378        facts |> List.partition (has_thy thy o snd)
   5.379              |>> sort (thm_ord o pairself snd)
   5.380 @@ -388,7 +63,7 @@
   5.381            if kind <> "" then
   5.382              let
   5.383                val suggs =
   5.384 -                old_facts |> meng_paulson_facts ctxt max_relevant goal
   5.385 +                old_facts |> iter_facts ctxt params max_relevant goal
   5.386                            |> map (fact_name_of o fst o fst)
   5.387                            |> sort string_ord
   5.388                val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
     6.1 --- a/src/HOL/TPTP/mash_import.ML	Wed Jul 11 21:43:19 2012 +0200
     6.2 +++ b/src/HOL/TPTP/mash_import.ML	Wed Jul 11 21:43:19 2012 +0200
     6.3 @@ -8,13 +8,16 @@
     6.4  
     6.5  signature MASH_IMPORT =
     6.6  sig
     6.7 +  type params = Sledgehammer_Provers.params
     6.8 +
     6.9    val import_and_evaluate_mash_suggestions :
    6.10 -    Proof.context -> theory -> string -> unit
    6.11 +    Proof.context -> params -> theory -> string -> unit
    6.12  end;
    6.13  
    6.14  structure MaSh_Import : MASH_IMPORT =
    6.15  struct
    6.16  
    6.17 +open Sledgehammer_Filter_MaSh
    6.18  open MaSh_Export
    6.19  
    6.20  val unescape_meta =
    6.21 @@ -30,26 +33,26 @@
    6.22  
    6.23  val of_fact_name = unescape_meta
    6.24  
    6.25 -val depN = "Dependencies"
    6.26 -val mengN = "Meng & Paulson"
    6.27 +val isaN = "Isabelle"
    6.28 +val iterN = "Iterative"
    6.29  val mashN = "MaSh"
    6.30 -val meng_mashN = "M&P+MaSh"
    6.31 +val iter_mashN = "Iter+MaSh"
    6.32  
    6.33  val max_relevant_slack = 2
    6.34  
    6.35 -fun import_and_evaluate_mash_suggestions ctxt thy file_name =
    6.36 +fun import_and_evaluate_mash_suggestions ctxt params thy file_name =
    6.37    let
    6.38      val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} =
    6.39        Sledgehammer_Isar.default_params ctxt []
    6.40      val prover_name = hd provers
    6.41      val path = file_name |> Path.explode
    6.42      val lines = path |> File.read_lines
    6.43 -    val facts = non_tautological_facts_of thy
    6.44 +    val facts = all_non_tautological_facts_of thy
    6.45      val all_names = facts |> map (Thm.get_name_hint o snd)
    6.46 -    val meng_ok = Unsynchronized.ref 0
    6.47 +    val iter_ok = Unsynchronized.ref 0
    6.48      val mash_ok = Unsynchronized.ref 0
    6.49 -    val meng_mash_ok = Unsynchronized.ref 0
    6.50 -    val dep_ok = Unsynchronized.ref 0
    6.51 +    val iter_mash_ok = Unsynchronized.ref 0
    6.52 +    val isa_ok = Unsynchronized.ref 0
    6.53      fun find_sugg facts sugg =
    6.54        find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
    6.55      fun sugg_facts hyp_ts concl_t facts =
    6.56 @@ -57,7 +60,7 @@
    6.57        #> take (max_relevant_slack * the max_relevant)
    6.58        #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
    6.59        #> map (apfst (apfst (fn name => name ())))
    6.60 -    fun meng_mash_facts fs1 fs2 =
    6.61 +    fun iter_mash_facts fs1 fs2 =
    6.62        let
    6.63          val fact_eq = (op =) o pairself fst
    6.64          fun score_in f fs =
    6.65 @@ -92,10 +95,10 @@
    6.66                  |> tag_list 1
    6.67                  |> map index_string
    6.68                  |> space_implode " "))
    6.69 -    fun run_sh ok heading facts goal =
    6.70 +    fun prove ok heading facts goal =
    6.71        let
    6.72          val facts = facts |> take (the max_relevant)
    6.73 -        val res as {outcome, ...} = run_sledgehammer ctxt facts goal
    6.74 +        val res as {outcome, ...} = run_prover ctxt params facts goal
    6.75          val _ = if is_none outcome then ok := !ok + 1 else ()
    6.76        in str_of_res heading facts res end
    6.77      fun solve_goal j name suggs =
    6.78 @@ -105,23 +108,23 @@
    6.79            case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
    6.80              SOME (_, th) => th
    6.81            | NONE => error ("No fact called \"" ^ name ^ "\"")
    6.82 -        val deps = dependencies_of all_names th
    6.83 +        val isa_deps = isabelle_dependencies_of all_names th
    6.84          val goal = goal_of_thm thy th
    6.85          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    6.86          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    6.87 -        val deps_facts = sugg_facts hyp_ts concl_t facts deps
    6.88 -        val meng_facts =
    6.89 -          meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal
    6.90 -                             facts
    6.91 +        val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps
    6.92 +        val iter_facts =
    6.93 +          iter_facts ctxt params (max_relevant_slack * the max_relevant) goal
    6.94 +                     facts
    6.95          val mash_facts = sugg_facts hyp_ts concl_t facts suggs
    6.96 -        val meng_mash_facts = meng_mash_facts meng_facts mash_facts
    6.97 -        val meng_s = run_sh meng_ok mengN meng_facts goal
    6.98 -        val mash_s = run_sh mash_ok mashN mash_facts goal
    6.99 -        val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal
   6.100 -        val dep_s = run_sh dep_ok depN deps_facts goal
   6.101 +        val iter_mash_facts = iter_mash_facts iter_facts mash_facts
   6.102 +        val iter_s = prove iter_ok iterN iter_facts goal
   6.103 +        val mash_s = prove mash_ok mashN mash_facts goal
   6.104 +        val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal
   6.105 +        val isa_s = prove isa_ok isaN isa_facts goal
   6.106        in
   6.107 -        ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s,
   6.108 -         dep_s]
   6.109 +        ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s,
   6.110 +         isa_s]
   6.111          |> cat_lines |> tracing
   6.112        end
   6.113      val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
   6.114 @@ -145,10 +148,10 @@
   6.115      tracing ("Options: " ^ commas options);
   6.116      List.app do_line (tag_list 1 lines);
   6.117      ["Successes (of " ^ string_of_int n ^ " goals)",
   6.118 -     total_of mengN meng_ok n,
   6.119 +     total_of iterN iter_ok n,
   6.120       total_of mashN mash_ok n,
   6.121 -     total_of meng_mashN meng_mash_ok n,
   6.122 -     total_of depN dep_ok n]
   6.123 +     total_of iter_mashN iter_mash_ok n,
   6.124 +     total_of isaN isa_ok n]
   6.125      |> cat_lines |> tracing
   6.126    end
   6.127  
     7.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
     7.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
     7.3 @@ -252,10 +252,6 @@
     7.4    Other characters go to _nnn where nnn is the decimal ASCII code.*)
     7.5  val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
     7.6  
     7.7 -fun stringN_of_int 0 _ = ""
     7.8 -  | stringN_of_int k n =
     7.9 -    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
    7.10 -
    7.11  fun ascii_of_char c =
    7.12    if Char.isAlphaNum c then
    7.13      String.str c
     8.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 11 21:43:19 2012 +0200
     8.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 11 21:43:19 2012 +0200
     8.3 @@ -9,6 +9,7 @@
     8.4    val timestamp : unit -> string
     8.5    val hash_string : string -> int
     8.6    val hash_term : term -> int
     8.7 +  val stringN_of_int : int -> int -> string
     8.8    val strip_spaces : bool -> (char -> bool) -> string -> string
     8.9    val strip_spaces_except_between_idents : string -> string
    8.10    val nat_subscript : int -> string
    8.11 @@ -65,6 +66,10 @@
    8.12  fun hash_string s = Word.toInt (hashw_string (s, 0w0))
    8.13  val hash_term = Word.toInt o hashw_term
    8.14  
    8.15 +fun stringN_of_int 0 _ = ""
    8.16 +  | stringN_of_int k n =
    8.17 +    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
    8.18 +
    8.19  fun strip_spaces skip_comments is_evil =
    8.20    let
    8.21      fun strip_c_style_comment [] accum = accum
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 11 21:43:19 2012 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 11 21:43:19 2012 +0200
     9.3 @@ -21,15 +21,16 @@
     9.4    val fact_from_ref :
     9.5      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     9.6      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     9.7 -  val all_facts :
     9.8 -    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
     9.9 -    -> thm list -> status Termtab.table
    9.10 -    -> (((unit -> string) * stature) * thm) list
    9.11    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    9.12    val maybe_instantiate_inducts :
    9.13      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    9.14      -> (((unit -> string) * 'a) * thm) list
    9.15    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    9.16 +  val all_facts :
    9.17 +    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
    9.18 +    -> thm list -> status Termtab.table
    9.19 +    -> (((unit -> string) * stature) * thm) list
    9.20 +  val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
    9.21    val nearly_all_facts :
    9.22      Proof.context -> bool -> relevance_override -> thm list -> term list -> term
    9.23      -> (((unit -> string) * stature) * thm) list
    9.24 @@ -240,77 +241,6 @@
    9.25            (Term.add_vars t [] |> sort_wrt (fst o fst))
    9.26    |> fst
    9.27  
    9.28 -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
    9.29 -  let
    9.30 -    val thy = Proof_Context.theory_of ctxt
    9.31 -    val global_facts = Global_Theory.facts_of thy
    9.32 -    val local_facts = Proof_Context.facts_of ctxt
    9.33 -    val named_locals = local_facts |> Facts.dest_static []
    9.34 -    val assms = Assumption.all_assms_of ctxt
    9.35 -    fun is_good_unnamed_local th =
    9.36 -      not (Thm.has_name_hint th) andalso
    9.37 -      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
    9.38 -    val unnamed_locals =
    9.39 -      union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
    9.40 -      |> filter is_good_unnamed_local |> map (pair "" o single)
    9.41 -    val full_space =
    9.42 -      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    9.43 -    fun add_facts global foldx facts =
    9.44 -      foldx (fn (name0, ths) =>
    9.45 -        if not exporter andalso name0 <> "" andalso
    9.46 -           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    9.47 -           (Facts.is_concealed facts name0 orelse
    9.48 -            (not (Config.get ctxt ignore_no_atp) andalso
    9.49 -             is_package_def name0) orelse
    9.50 -            exists (fn s => String.isSuffix s name0)
    9.51 -                   (multi_base_blacklist ctxt ho_atp)) then
    9.52 -          I
    9.53 -        else
    9.54 -          let
    9.55 -            val multi = length ths > 1
    9.56 -            val backquote_thm =
    9.57 -              backquote o hackish_string_for_term ctxt o close_form o prop_of
    9.58 -            fun check_thms a =
    9.59 -              case try (Proof_Context.get_thms ctxt) a of
    9.60 -                NONE => false
    9.61 -              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
    9.62 -          in
    9.63 -            pair 1
    9.64 -            #> fold (fn th => fn (j, (multis, unis)) =>
    9.65 -                        (j + 1,
    9.66 -                         if not (member Thm.eq_thm_prop add_ths th) andalso
    9.67 -                            is_theorem_bad_for_atps ho_atp exporter th then
    9.68 -                           (multis, unis)
    9.69 -                         else
    9.70 -                           let
    9.71 -                             val new =
    9.72 -                               (((fn () =>
    9.73 -                                 if name0 = "" then
    9.74 -                                   th |> backquote_thm
    9.75 -                                 else
    9.76 -                                   [Facts.extern ctxt facts name0,
    9.77 -                                    Name_Space.extern ctxt full_space name0,
    9.78 -                                    name0]
    9.79 -                                   |> find_first check_thms
    9.80 -                                   |> (fn SOME name =>
    9.81 -                                          make_name reserved multi j name
    9.82 -                                        | NONE => "")),
    9.83 -                                stature_of_thm global assms chained_ths
    9.84 -                                               css_table name0 th), th)
    9.85 -                           in
    9.86 -                             if multi then (new :: multis, unis)
    9.87 -                             else (multis, new :: unis)
    9.88 -                           end)) ths
    9.89 -            #> snd
    9.90 -          end)
    9.91 -  in
    9.92 -    (* The single-name theorems go after the multiple-name ones, so that single
    9.93 -       names are preferred when both are available. *)
    9.94 -    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
    9.95 -             |> add_facts true Facts.fold_static global_facts global_facts
    9.96 -             |> op @
    9.97 -  end
    9.98 -
    9.99  fun clasimpset_rule_table_of ctxt =
   9.100    let
   9.101      val thy = Proof_Context.theory_of ctxt
   9.102 @@ -416,6 +346,84 @@
   9.103  fun maybe_filter_no_atps ctxt =
   9.104    not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
   9.105  
   9.106 +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
   9.107 +  let
   9.108 +    val thy = Proof_Context.theory_of ctxt
   9.109 +    val global_facts = Global_Theory.facts_of thy
   9.110 +    val local_facts = Proof_Context.facts_of ctxt
   9.111 +    val named_locals = local_facts |> Facts.dest_static []
   9.112 +    val assms = Assumption.all_assms_of ctxt
   9.113 +    fun is_good_unnamed_local th =
   9.114 +      not (Thm.has_name_hint th) andalso
   9.115 +      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   9.116 +    val unnamed_locals =
   9.117 +      union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
   9.118 +      |> filter is_good_unnamed_local |> map (pair "" o single)
   9.119 +    val full_space =
   9.120 +      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   9.121 +    fun add_facts global foldx facts =
   9.122 +      foldx (fn (name0, ths) =>
   9.123 +        if not exporter andalso name0 <> "" andalso
   9.124 +           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   9.125 +           (Facts.is_concealed facts name0 orelse
   9.126 +            (not (Config.get ctxt ignore_no_atp) andalso
   9.127 +             is_package_def name0) orelse
   9.128 +            exists (fn s => String.isSuffix s name0)
   9.129 +                   (multi_base_blacklist ctxt ho_atp)) then
   9.130 +          I
   9.131 +        else
   9.132 +          let
   9.133 +            val multi = length ths > 1
   9.134 +            val backquote_thm =
   9.135 +              backquote o hackish_string_for_term ctxt o close_form o prop_of
   9.136 +            fun check_thms a =
   9.137 +              case try (Proof_Context.get_thms ctxt) a of
   9.138 +                NONE => false
   9.139 +              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   9.140 +          in
   9.141 +            pair 1
   9.142 +            #> fold (fn th => fn (j, (multis, unis)) =>
   9.143 +                        (j + 1,
   9.144 +                         if not (member Thm.eq_thm_prop add_ths th) andalso
   9.145 +                            is_theorem_bad_for_atps ho_atp exporter th then
   9.146 +                           (multis, unis)
   9.147 +                         else
   9.148 +                           let
   9.149 +                             val new =
   9.150 +                               (((fn () =>
   9.151 +                                 if name0 = "" then
   9.152 +                                   th |> backquote_thm
   9.153 +                                 else
   9.154 +                                   [Facts.extern ctxt facts name0,
   9.155 +                                    Name_Space.extern ctxt full_space name0,
   9.156 +                                    name0]
   9.157 +                                   |> find_first check_thms
   9.158 +                                   |> (fn SOME name =>
   9.159 +                                          make_name reserved multi j name
   9.160 +                                        | NONE => "")),
   9.161 +                                stature_of_thm global assms chained_ths
   9.162 +                                               css_table name0 th), th)
   9.163 +                           in
   9.164 +                             if multi then (new :: multis, unis)
   9.165 +                             else (multis, new :: unis)
   9.166 +                           end)) ths
   9.167 +            #> snd
   9.168 +          end)
   9.169 +  in
   9.170 +    (* The single-name theorems go after the multiple-name ones, so that single
   9.171 +       names are preferred when both are available. *)
   9.172 +    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   9.173 +             |> add_facts true Facts.fold_static global_facts global_facts
   9.174 +             |> op @
   9.175 +  end
   9.176 +
   9.177 +fun all_facts_of thy =
   9.178 +  let val ctxt = Proof_Context.init_global thy in
   9.179 +    all_facts ctxt false Symtab.empty true [] []
   9.180 +              (clasimpset_rule_table_of ctxt)
   9.181 +    |> rev (* try to restore the original order of facts, for MaSh *)
   9.182 +  end
   9.183 +
   9.184  fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
   9.185                       chained_ths hyp_ts concl_t =
   9.186    if only andalso null add then
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 11 21:43:19 2012 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 11 21:43:19 2012 +0200
    10.3 @@ -6,6 +6,35 @@
    10.4  
    10.5  signature SLEDGEHAMMER_FILTER_MASH =
    10.6  sig
    10.7 +  type status = ATP_Problem_Generate.status
    10.8 +  type stature = ATP_Problem_Generate.stature
    10.9 +  type params = Sledgehammer_Provers.params
   10.10 +  type prover_result = Sledgehammer_Provers.prover_result
   10.11 +
   10.12 +  val fact_name_of : string -> string
   10.13 +  val all_non_tautological_facts_of :
   10.14 +    theory -> (((unit -> string) * stature) * thm) list
   10.15 +  val theory_ord : theory * theory -> order
   10.16 +  val thm_ord : thm * thm -> order
   10.17 +  val thms_by_thy : ('a * thm) list -> (string * thm list) list
   10.18 +  val has_thy : theory -> thm -> bool
   10.19 +  val parent_thms : (string * thm list) list -> theory -> string list
   10.20 +  val features_of : theory -> status * thm -> string list
   10.21 +  val isabelle_dependencies_of : string list -> thm -> string list
   10.22 +  val goal_of_thm : theory -> thm -> thm
   10.23 +  val iter_facts :
   10.24 +    Proof.context -> params -> int -> thm
   10.25 +    -> (((unit -> string) * stature) * thm) list
   10.26 +    -> ((string * stature) * thm) list
   10.27 +  val run_prover :
   10.28 +    Proof.context -> params -> ((string * stature) * thm) list -> thm
   10.29 +    -> prover_result
   10.30 +  val generate_accessibility : theory -> bool -> string -> unit
   10.31 +  val generate_features : theory -> bool -> string -> unit
   10.32 +  val generate_isa_dependencies : theory -> bool -> string -> unit
   10.33 +  val generate_atp_dependencies :
   10.34 +    Proof.context -> params -> theory -> bool -> string -> unit
   10.35 +
   10.36    val reset : unit -> unit
   10.37    val can_suggest : unit -> bool
   10.38    val can_learn_thy : theory -> bool
   10.39 @@ -16,6 +45,16 @@
   10.40  structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
   10.41  struct
   10.42  
   10.43 +open ATP_Util
   10.44 +open ATP_Problem_Generate
   10.45 +open Sledgehammer_Util
   10.46 +open Sledgehammer_Fact
   10.47 +open Sledgehammer_Filter_Iter
   10.48 +open Sledgehammer_Provers
   10.49 +
   10.50 +
   10.51 +(*** Low-level communication with MaSh ***)
   10.52 +
   10.53  fun mash_reset () =
   10.54    tracing "MaSh RESET"
   10.55  
   10.56 @@ -30,6 +69,311 @@
   10.57    tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
   10.58             space_implode " " feats)
   10.59  
   10.60 +
   10.61 +(*** Isabelle helpers ***)
   10.62 +
   10.63 +val fact_name_of = prefix fact_prefix o ascii_of
   10.64 +
   10.65 +fun escape_meta_char c =
   10.66 +  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
   10.67 +     c = #")" orelse c = #"," then
   10.68 +    String.str c
   10.69 +  else
   10.70 +    (* fixed width, in case more digits follow *)
   10.71 +    "\\" ^ stringN_of_int 3 (Char.ord c)
   10.72 +
   10.73 +val escape_meta = String.translate escape_meta_char
   10.74 +
   10.75 +val thy_prefix = "y_"
   10.76 +
   10.77 +val fact_name_of = escape_meta
   10.78 +val thy_name_of = prefix thy_prefix o escape_meta
   10.79 +val const_name_of = prefix const_prefix o escape_meta
   10.80 +val type_name_of = prefix type_const_prefix o escape_meta
   10.81 +val class_name_of = prefix class_prefix o escape_meta
   10.82 +
   10.83 +val thy_name_of_thm = theory_of_thm #> Context.theory_name
   10.84 +
   10.85 +local
   10.86 +
   10.87 +fun has_bool @{typ bool} = true
   10.88 +  | has_bool (Type (_, Ts)) = exists has_bool Ts
   10.89 +  | has_bool _ = false
   10.90 +
   10.91 +fun has_fun (Type (@{type_name fun}, _)) = true
   10.92 +  | has_fun (Type (_, Ts)) = exists has_fun Ts
   10.93 +  | has_fun _ = false
   10.94 +
   10.95 +val is_conn = member (op =)
   10.96 +  [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
   10.97 +   @{const_name HOL.implies}, @{const_name Not},
   10.98 +   @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
   10.99 +   @{const_name HOL.eq}]
  10.100 +
  10.101 +val has_bool_arg_const =
  10.102 +  exists_Const (fn (c, T) =>
  10.103 +                   not (is_conn c) andalso exists has_bool (binder_types T))
  10.104 +
  10.105 +fun higher_inst_const thy (c, T) =
  10.106 +  case binder_types T of
  10.107 +    [] => false
  10.108 +  | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
  10.109 +
  10.110 +val binders = [@{const_name All}, @{const_name Ex}]
  10.111 +
  10.112 +in
  10.113 +
  10.114 +fun is_fo_term thy t =
  10.115 +  let
  10.116 +    val t =
  10.117 +      t |> Envir.beta_eta_contract
  10.118 +        |> transform_elim_prop
  10.119 +        |> Object_Logic.atomize_term thy
  10.120 +  in
  10.121 +    Term.is_first_order binders t andalso
  10.122 +    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
  10.123 +                          | _ => false) t orelse
  10.124 +         has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
  10.125 +  end
  10.126 +
  10.127 +end
  10.128 +
  10.129 +fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
  10.130 +  let
  10.131 +    val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
  10.132 +    val bad_consts = atp_widely_irrelevant_consts
  10.133 +    fun do_add_type (Type (s, Ts)) =
  10.134 +        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
  10.135 +        #> fold do_add_type Ts
  10.136 +      | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
  10.137 +      | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S)
  10.138 +    fun add_type T = type_max_depth >= 0 ? do_add_type T
  10.139 +    fun mk_app s args =
  10.140 +      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
  10.141 +      else s
  10.142 +    fun patternify ~1 _ = ""
  10.143 +      | patternify depth t =
  10.144 +        case strip_comb t of
  10.145 +          (Const (s, _), args) =>
  10.146 +          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
  10.147 +        | _ => ""
  10.148 +    fun add_term_patterns ~1 _ = I
  10.149 +      | add_term_patterns depth t =
  10.150 +        insert (op =) (patternify depth t)
  10.151 +        #> add_term_patterns (depth - 1) t
  10.152 +    val add_term = add_term_patterns term_max_depth
  10.153 +    fun add_patterns t =
  10.154 +      let val (head, args) = strip_comb t in
  10.155 +        (case head of
  10.156 +           Const (s, T) =>
  10.157 +           not (member (op =) bad_consts s) ? (add_term t #> add_type T)
  10.158 +         | Free (_, T) => add_type T
  10.159 +         | Var (_, T) => add_type T
  10.160 +         | Abs (_, T, body) => add_type T #> add_patterns body
  10.161 +         | _ => I)
  10.162 +        #> fold add_patterns args
  10.163 +      end
  10.164 +  in [] |> add_patterns t |> sort string_ord end
  10.165 +
  10.166 +fun is_likely_tautology th =
  10.167 +  null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
  10.168 +  not (Thm.eq_thm_prop (@{thm ext}, th))
  10.169 +
  10.170 +fun is_too_meta thy th =
  10.171 +  fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
  10.172 +
  10.173 +fun all_non_tautological_facts_of thy =
  10.174 +  all_facts_of thy
  10.175 +  |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
  10.176 +
  10.177 +fun theory_ord p =
  10.178 +  if Theory.eq_thy p then EQUAL
  10.179 +  else if Theory.subthy p then LESS
  10.180 +  else if Theory.subthy (swap p) then GREATER
  10.181 +  else EQUAL
  10.182 +
  10.183 +val thm_ord = theory_ord o pairself theory_of_thm
  10.184 +
  10.185 +fun thms_by_thy ths =
  10.186 +  ths |> map (snd #> `thy_name_of_thm)
  10.187 +      |> AList.group (op =)
  10.188 +      |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
  10.189 +                                   o hd o snd))
  10.190 +      |> map (apsnd (sort thm_ord))
  10.191 +
  10.192 +fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
  10.193 +
  10.194 +fun parent_thms thy_ths thy =
  10.195 +  Theory.parents_of thy
  10.196 +  |> map Context.theory_name
  10.197 +  |> map_filter (AList.lookup (op =) thy_ths)
  10.198 +  |> map List.last
  10.199 +  |> map (fact_name_of o Thm.get_name_hint)
  10.200 +
  10.201 +fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
  10.202 +
  10.203 +val max_depth = 1
  10.204 +
  10.205 +(* TODO: Generate type classes for types? *)
  10.206 +fun features_of thy (status, th) =
  10.207 +  let val t = Thm.prop_of th in
  10.208 +    thy_name_of (thy_name_of_thm th) ::
  10.209 +    interesting_terms_types_and_classes max_depth max_depth t
  10.210 +    |> not (has_no_lambdas t) ? cons "lambdas"
  10.211 +    |> exists_Const is_exists t ? cons "skolems"
  10.212 +    |> not (is_fo_term thy t) ? cons "ho"
  10.213 +    |> (case status of
  10.214 +          General => I
  10.215 +        | Induction => cons "induction"
  10.216 +        | Intro => cons "intro"
  10.217 +        | Inductive => cons "inductive"
  10.218 +        | Elim => cons "elim"
  10.219 +        | Simp => cons "simp"
  10.220 +        | Def => cons "def")
  10.221 +  end
  10.222 +
  10.223 +fun isabelle_dependencies_of all_facts =
  10.224 +  thms_in_proof (SOME all_facts)
  10.225 +  #> map fact_name_of #> sort string_ord
  10.226 +
  10.227 +val freezeT = Type.legacy_freeze_type
  10.228 +
  10.229 +fun freeze (t $ u) = freeze t $ freeze u
  10.230 +  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
  10.231 +  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
  10.232 +  | freeze (Const (s, T)) = Const (s, freezeT T)
  10.233 +  | freeze (Free (s, T)) = Free (s, freezeT T)
  10.234 +  | freeze t = t
  10.235 +
  10.236 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
  10.237 +
  10.238 +fun iter_facts ctxt ({provers, relevance_thresholds, ...} : params) max_relevant
  10.239 +               goal =
  10.240 +  let
  10.241 +    val prover_name = hd provers
  10.242 +    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
  10.243 +    val is_built_in_const =
  10.244 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
  10.245 +    val relevance_fudge =
  10.246 +      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
  10.247 +    val relevance_override = {add = [], del = [], only = false}
  10.248 +  in
  10.249 +    iterative_relevant_facts ctxt relevance_thresholds max_relevant
  10.250 +                             is_built_in_const relevance_fudge
  10.251 +                             relevance_override [] hyp_ts concl_t
  10.252 +  end
  10.253 +
  10.254 +fun run_prover ctxt (params as {provers, ...}) facts goal =
  10.255 +  let
  10.256 +    val problem =
  10.257 +      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
  10.258 +       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
  10.259 +    val prover =
  10.260 +      Sledgehammer_Minimize.get_minimizing_prover ctxt
  10.261 +          Sledgehammer_Provers.Normal (hd provers)
  10.262 +  in prover params (K (K (K ""))) problem end
  10.263 +
  10.264 +fun generate_accessibility thy include_thy file_name =
  10.265 +  let
  10.266 +    val path = file_name |> Path.explode
  10.267 +    val _ = File.write path ""
  10.268 +    fun do_thm th prevs =
  10.269 +      let
  10.270 +        val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
  10.271 +        val _ = File.append path s
  10.272 +      in [th] end
  10.273 +    val thy_ths =
  10.274 +      all_non_tautological_facts_of thy
  10.275 +      |> not include_thy ? filter_out (has_thy thy o snd)
  10.276 +      |> thms_by_thy
  10.277 +    fun do_thy ths =
  10.278 +      let
  10.279 +        val thy = theory_of_thm (hd ths)
  10.280 +        val parents = parent_thms thy_ths thy
  10.281 +        val ths = ths |> map (fact_name_of o Thm.get_name_hint)
  10.282 +      in fold do_thm ths parents; () end
  10.283 +  in List.app (do_thy o snd) thy_ths end
  10.284 +
  10.285 +fun generate_features thy include_thy file_name =
  10.286 +  let
  10.287 +    val path = file_name |> Path.explode
  10.288 +    val _ = File.write path ""
  10.289 +    val facts =
  10.290 +      all_non_tautological_facts_of thy
  10.291 +      |> not include_thy ? filter_out (has_thy thy o snd)
  10.292 +    fun do_fact ((_, (_, status)), th) =
  10.293 +      let
  10.294 +        val name = Thm.get_name_hint th
  10.295 +        val feats = features_of thy (status, th)
  10.296 +        val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
  10.297 +      in File.append path s end
  10.298 +  in List.app do_fact facts end
  10.299 +
  10.300 +fun generate_isa_dependencies thy include_thy file_name =
  10.301 +  let
  10.302 +    val path = file_name |> Path.explode
  10.303 +    val _ = File.write path ""
  10.304 +    val ths =
  10.305 +      all_non_tautological_facts_of thy
  10.306 +      |> not include_thy ? filter_out (has_thy thy o snd)
  10.307 +      |> map snd
  10.308 +    val all_names = ths |> map Thm.get_name_hint
  10.309 +    fun do_thm th =
  10.310 +      let
  10.311 +        val name = Thm.get_name_hint th
  10.312 +        val deps = isabelle_dependencies_of all_names th
  10.313 +        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
  10.314 +      in File.append path s end
  10.315 +  in List.app do_thm ths end
  10.316 +
  10.317 +fun generate_atp_dependencies ctxt (params as {max_relevant, ...}) thy
  10.318 +                              include_thy file_name =
  10.319 +  let
  10.320 +    val path = file_name |> Path.explode
  10.321 +    val _ = File.write path ""
  10.322 +    val facts =
  10.323 +      all_non_tautological_facts_of thy
  10.324 +      |> not include_thy ? filter_out (has_thy thy o snd)
  10.325 +    val ths = facts |> map snd
  10.326 +    val all_names = ths |> map Thm.get_name_hint
  10.327 +    fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
  10.328 +    fun add_isa_dep facts dep accum =
  10.329 +      if exists (is_dep dep) accum then
  10.330 +        accum
  10.331 +      else case find_first (is_dep dep) facts of
  10.332 +        SOME ((name, status), th) => accum @ [((name (), status), th)]
  10.333 +      | NONE => accum (* shouldn't happen *)
  10.334 +    fun fix_name ((_, stature), th) =
  10.335 +      ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
  10.336 +    fun do_thm th =
  10.337 +      let
  10.338 +        val name = Thm.get_name_hint th
  10.339 +        val goal = goal_of_thm thy th
  10.340 +        val deps =
  10.341 +          case isabelle_dependencies_of all_names th of
  10.342 +            [] => []
  10.343 +          | isa_dep as [_] => isa_dep (* can hardly beat that *)
  10.344 +          | isa_deps =>
  10.345 +            let
  10.346 +              val facts =
  10.347 +                facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
  10.348 +              val facts =
  10.349 +                facts |> iter_facts ctxt params (the max_relevant) goal
  10.350 +                      |> fold (add_isa_dep facts) isa_deps
  10.351 +                      |> map fix_name
  10.352 +            in
  10.353 +              case run_prover ctxt params facts goal of
  10.354 +                {outcome = NONE, used_facts, ...} =>
  10.355 +                used_facts |> map fst |> sort string_ord
  10.356 +              | _ => isa_deps
  10.357 +            end
  10.358 +        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
  10.359 +      in File.append path s end
  10.360 +  in List.app do_thm ths end
  10.361 +
  10.362 +
  10.363 +(*** High-level communication with MaSh ***)
  10.364 +
  10.365  fun reset () =
  10.366    ()
  10.367  
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 11 21:43:19 2012 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 11 21:43:19 2012 +0200
    11.3 @@ -14,6 +14,7 @@
    11.4    val subgoal_count : Proof.state -> int
    11.5    val normalize_chained_theorems : thm list -> thm list
    11.6    val reserved_isar_keyword_table : unit -> unit Symtab.table
    11.7 +  val thms_in_proof : string list option -> thm -> string list
    11.8  end;
    11.9  
   11.10  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
   11.11 @@ -60,4 +61,36 @@
   11.12    Keyword.dest () |-> union (op =)
   11.13    |> map (rpair ()) |> Symtab.make
   11.14  
   11.15 +(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
   11.16 +   fixes that seem to be missing over there; or maybe the two code portions are
   11.17 +   not doing the same? *)
   11.18 +fun fold_body_thms thm_name f =
   11.19 +  let
   11.20 +    fun app n (PBody {thms, ...}) =
   11.21 +      thms |> fold (fn (_, (name, prop, body)) => fn x =>
   11.22 +        let
   11.23 +          val body' = Future.join body
   11.24 +          val n' =
   11.25 +            n + (if name = "" orelse
   11.26 +                    (* uncommon case where the proved theorem occurs twice
   11.27 +                       (e.g., "Transitive_Closure.trancl_into_trancl") *)
   11.28 +                    (n = 1 andalso name = thm_name) then
   11.29 +                   0
   11.30 +                 else
   11.31 +                   1)
   11.32 +          val x' = x |> n' <= 1 ? app n' body'
   11.33 +        in (x' |> n = 1 ? f (name, prop, body')) end)
   11.34 +  in fold (app 0) end
   11.35 +
   11.36 +fun thms_in_proof all_names th =
   11.37 +  let
   11.38 +    val is_name_ok =
   11.39 +      case all_names of
   11.40 +        SOME names => member (op =) names
   11.41 +      | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
   11.42 +    fun collect (s, _, _) = is_name_ok s ? insert (op =) s
   11.43 +    val names =
   11.44 +      [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
   11.45 +  in names end
   11.46 +
   11.47  end;