1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  open Sledgehammer_Provers
     1.5  
     1.6  val trace =
     1.7 -  Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
     1.8 +  Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false)
     1.9  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.10  
    1.11  val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.3 @@ -14,8 +14,11 @@
     2.4    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
     2.5    type prover_result = Sledgehammer_Provers.prover_result
     2.6  
     2.7 +  val trace : bool Config.T
     2.8    val escape_meta : string -> string
     2.9    val escape_metas : string list -> string
    2.10 +  val unescape_meta : string -> string
    2.11 +  val unescape_metas : string -> string list
    2.12    val all_non_tautological_facts_of :
    2.13      theory -> status Termtab.table -> fact list
    2.14    val theory_ord : theory * theory -> order
    2.15 @@ -28,18 +31,20 @@
    2.16    val goal_of_thm : theory -> thm -> thm
    2.17    val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
    2.18    val thy_name_of_fact : string -> string
    2.19 -  val mash_RESET : unit -> unit
    2.20 -  val mash_ADD : (string * string list * string list * string list) list -> unit
    2.21 -  val mash_DEL : string list -> string list -> unit
    2.22 -  val mash_SUGGEST : string list -> string list -> string list
    2.23 -  val mash_reset : unit -> unit
    2.24 -  val mash_can_suggest_facts : unit -> bool
    2.25 +  val mash_RESET : Proof.context -> unit
    2.26 +  val mash_ADD :
    2.27 +    Proof.context -> (string * string list * string list * string list) list
    2.28 +    -> unit
    2.29 +  val mash_DEL : Proof.context -> string list -> string list -> unit
    2.30 +  val mash_SUGGEST : Proof.context -> string list -> string list -> string list
    2.31 +  val mash_reset : Proof.context -> unit
    2.32 +  val mash_can_suggest_facts : Proof.context -> bool
    2.33    val mash_suggest_facts :
    2.34      Proof.context -> params -> string -> int -> term list -> term -> fact list
    2.35      -> fact list * fact list
    2.36 -  val mash_can_learn_thy : theory -> bool
    2.37 -  val mash_learn_thy : Proof.context -> real -> unit
    2.38 -  val mash_learn_proof : theory -> term -> thm list -> unit
    2.39 +  val mash_can_learn_thy : Proof.context -> theory -> bool
    2.40 +  val mash_learn_thy : Proof.context -> theory -> real -> unit
    2.41 +  val mash_learn_proof : Proof.context -> term -> thm list -> unit
    2.42    val relevant_facts :
    2.43      Proof.context -> params -> string -> int -> fact_override -> term list
    2.44      -> term -> fact list -> fact list
    2.45 @@ -55,6 +60,10 @@
    2.46  open Sledgehammer_Filter_Iter
    2.47  open Sledgehammer_Provers
    2.48  
    2.49 +val trace =
    2.50 +  Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
    2.51 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    2.52 +
    2.53  val mash_dir = "mash"
    2.54  val model_file = "model"
    2.55  val state_file = "state"
    2.56 @@ -63,11 +72,10 @@
    2.57    getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file
    2.58    |> Path.explode
    2.59  
    2.60 -val fresh_fact_prefix = Long_Name.separator
    2.61  
    2.62  (*** Isabelle helpers ***)
    2.63  
    2.64 -fun escape_meta_char c =
    2.65 +fun meta_char c =
    2.66    if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
    2.67       c = #")" orelse c = #"," then
    2.68      String.str c
    2.69 @@ -75,8 +83,18 @@
    2.70      (* fixed width, in case more digits follow *)
    2.71      "\\" ^ stringN_of_int 3 (Char.ord c)
    2.72  
    2.73 -val escape_meta = String.translate escape_meta_char
    2.74 +fun unmeta_chars accum [] = String.implode (rev accum)
    2.75 +  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
    2.76 +    (case Int.fromString (String.implode [d1, d2, d3]) of
    2.77 +       SOME n => unmeta_chars (Char.chr n :: accum) cs
    2.78 +     | NONE => "" (* error *))
    2.79 +  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
    2.80 +  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
    2.81 +
    2.82 +val escape_meta = String.translate meta_char
    2.83  val escape_metas = map escape_meta #> space_implode " "
    2.84 +val unescape_meta = unmeta_chars [] o String.explode
    2.85 +val unescape_metas = map unescape_meta o space_explode " "
    2.86  
    2.87  val thy_feature_prefix = "y_"
    2.88  
    2.89 @@ -254,18 +272,6 @@
    2.90            Sledgehammer_Provers.Normal (hd provers)
    2.91    in prover params (K (K (K ""))) problem end
    2.92  
    2.93 -(* ###
    2.94 -fun compute_accessibility thy thy_facts =
    2.95 -  let
    2.96 -    fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th]
    2.97 -    fun add_thy facts =
    2.98 -      let
    2.99 -        val thy = theory_of_thm (hd facts)
   2.100 -        val parents = parent_facts thy_facts thy
   2.101 -      in add_facts facts parents end
   2.102 -  in fold (add_thy o snd) thy_facts end
   2.103 -*)
   2.104 -
   2.105  fun accessibility_of thy thy_facts =
   2.106    case Symtab.lookup thy_facts (Context.theory_name thy) of
   2.107      SOME (fact :: _) => [fact]
   2.108 @@ -276,36 +282,37 @@
   2.109  
   2.110  (*** Low-level communication with MaSh ***)
   2.111  
   2.112 -fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file))
   2.113 +fun mash_RESET ctxt =
   2.114 +  (trace_msg ctxt (K "MaSh RESET"); File.write (mk_path model_file) "")
   2.115  
   2.116 -val mash_ADD =
   2.117 +fun mash_ADD ctxt =
   2.118    let
   2.119      fun add_record (fact, access, feats, deps) =
   2.120        let
   2.121          val s =
   2.122            escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^
   2.123            escape_metas feats ^ "; " ^ escape_metas deps
   2.124 -      in warning ("MaSh ADD " ^ s) end
   2.125 +      in trace_msg ctxt (fn () => "MaSh ADD " ^ s) end
   2.126    in List.app add_record end
   2.127  
   2.128 -fun mash_DEL facts feats =
   2.129 -  warning ("MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats)
   2.130 +fun mash_DEL ctxt facts feats =
   2.131 +  trace_msg ctxt (fn () =>
   2.132 +      "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats)
   2.133  
   2.134 -fun mash_SUGGEST access feats =
   2.135 -  (warning ("MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats);
   2.136 +fun mash_SUGGEST ctxt access feats =
   2.137 +  (trace_msg ctxt (fn () =>
   2.138 +       "MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats);
   2.139     [])
   2.140  
   2.141  
   2.142  (*** High-level communication with MaSh ***)
   2.143  
   2.144  type mash_state =
   2.145 -  {fresh : int,
   2.146 -   dirty_thys : unit Symtab.table,
   2.147 +  {dirty_thys : unit Symtab.table,
   2.148     thy_facts : string list Symtab.table}
   2.149  
   2.150  val empty_state =
   2.151 -  {fresh = 0,
   2.152 -   dirty_thys = Symtab.empty,
   2.153 +  {dirty_thys = Symtab.empty,
   2.154     thy_facts = Symtab.empty}
   2.155  
   2.156  local
   2.157 @@ -318,31 +325,30 @@
   2.158      in
   2.159        (true,
   2.160         case try File.read_lines path of
   2.161 -         SOME (fresh_line :: dirty_line :: facts_lines) =>
   2.162 +         SOME (dirty_line :: facts_lines) =>
   2.163           let
   2.164             fun dirty_thys_of_line line =
   2.165 -             Symtab.make (line |> space_explode " " |> map (rpair ()))
   2.166 +             Symtab.make (line |> unescape_metas |> map (rpair ()))
   2.167             fun add_facts_line line =
   2.168 -             case space_explode " " line of
   2.169 +             case unescape_metas line of
   2.170                 thy :: facts => Symtab.update_new (thy, facts)
   2.171               | _ => I (* shouldn't happen *)
   2.172           in
   2.173 -           {fresh = Int.fromString fresh_line |> the_default 0,
   2.174 -            dirty_thys = dirty_thys_of_line dirty_line,
   2.175 +           {dirty_thys = dirty_thys_of_line dirty_line,
   2.176              thy_facts = fold add_facts_line facts_lines Symtab.empty}
   2.177           end
   2.178         | _ => empty_state)
   2.179      end
   2.180  
   2.181 -fun mash_save ({fresh, dirty_thys, thy_facts} : mash_state) =
   2.182 +fun mash_save ({dirty_thys, thy_facts} : mash_state) =
   2.183    let
   2.184      val path = mk_path state_file
   2.185 -    val dirty_line = (dirty_thys |> Symtab.keys |> escape_metas) ^ "\n"
   2.186 +    val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n"
   2.187      fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n"
   2.188    in
   2.189 -    File.write path (string_of_int fresh ^ "\n" ^ dirty_line);
   2.190 +    File.write path dirty_line;
   2.191      Symtab.fold (fn thy_fact => fn () =>
   2.192 -                    File.append path (fact_line_for thy_fact)) thy_facts
   2.193 +                    File.append path (fact_line_for thy_fact)) thy_facts ()
   2.194    end
   2.195  
   2.196  val global_state =
   2.197 @@ -353,27 +359,27 @@
   2.198  fun mash_map f =
   2.199    Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
   2.200  
   2.201 -fun mash_peek f = Synchronized.change global_state (mash_load ##> tap f)
   2.202 -
   2.203  fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
   2.204  
   2.205 -fun mash_reset () =
   2.206 +fun mash_reset ctxt =
   2.207    Synchronized.change global_state (fn _ =>
   2.208 -      (mash_RESET (); File.rm (mk_path state_file); (true, empty_state)))
   2.209 +      (mash_RESET ctxt; File.write (mk_path state_file) "";
   2.210 +       (true, empty_state)))
   2.211  
   2.212  end
   2.213  
   2.214 -fun mash_can_suggest_facts () = not (Symtab.is_empty (#thy_facts (mash_get ())))
   2.215 +fun mash_can_suggest_facts (_ : Proof.context) =
   2.216 +  not (Symtab.is_empty (#thy_facts (mash_get ())))
   2.217  
   2.218  fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts =
   2.219    let
   2.220      val thy = Proof_Context.theory_of ctxt
   2.221      val access = accessibility_of thy (#thy_facts (mash_get ()))
   2.222      val feats = features_of thy General (concl_t :: hyp_ts)
   2.223 -    val suggs = mash_SUGGEST access feats
   2.224 +    val suggs = mash_SUGGEST ctxt access feats
   2.225    in (facts, []) end
   2.226  
   2.227 -fun mash_can_learn_thy thy =
   2.228 +fun mash_can_learn_thy (_ : Proof.context) thy =
   2.229    not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy))
   2.230  
   2.231  fun is_fact_in_thy_facts thy_facts fact =
   2.232 @@ -401,60 +407,55 @@
   2.233        | NONE => Symtab.update_new (thy, new_facts)
   2.234    in old |> Symtab.fold add_thy new end
   2.235  
   2.236 -fun mash_learn_thy ctxt timeout =
   2.237 +fun mash_learn_thy ctxt thy timeout =
   2.238    let
   2.239 -    val thy = Proof_Context.theory_of ctxt
   2.240      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   2.241      val facts = all_non_tautological_facts_of thy css_table
   2.242      val {thy_facts, ...} = mash_get ()
   2.243      fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th)
   2.244      val (old_facts, new_facts) =
   2.245        facts |> List.partition is_old ||> sort (thm_ord o pairself snd)
   2.246 -    val ths = facts |> map snd
   2.247 -    val all_names = ths |> map Thm.get_name_hint
   2.248 -    fun do_fact ((_, (_, status)), th) (prevs, records) =
   2.249 +  in
   2.250 +    if null new_facts then
   2.251 +      ()
   2.252 +    else
   2.253        let
   2.254 -        val name = Thm.get_name_hint th
   2.255 -        val feats = features_of thy status [prop_of th]
   2.256 -        val deps = isabelle_dependencies_of all_names th
   2.257 -        val record = (name, prevs, feats, deps)
   2.258 -      in ([name], record :: records) end
   2.259 -    val parents = parent_facts thy thy_facts
   2.260 -    val (_, records) = (parents, []) |> fold_rev do_fact new_facts
   2.261 -    val new_thy_facts = new_facts |> thy_facts_from_thms
   2.262 -    fun trans {fresh, dirty_thys, thy_facts} =
   2.263 -      (mash_ADD records;
   2.264 -       {fresh = fresh, dirty_thys = dirty_thys,
   2.265 -        thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts})
   2.266 -  in mash_map trans end
   2.267 +        val ths = facts |> map snd
   2.268 +        val all_names = ths |> map Thm.get_name_hint
   2.269 +        fun do_fact ((_, (_, status)), th) (prevs, records) =
   2.270 +          let
   2.271 +            val name = Thm.get_name_hint th
   2.272 +            val feats = features_of thy status [prop_of th]
   2.273 +            val deps = isabelle_dependencies_of all_names th
   2.274 +            val record = (name, prevs, feats, deps)
   2.275 +          in ([name], record :: records) end
   2.276 +        val parents = parent_facts thy thy_facts
   2.277 +        val (_, records) = (parents, []) |> fold_rev do_fact new_facts
   2.278 +        val new_thy_facts = new_facts |> thy_facts_from_thms
   2.279 +        fun trans {dirty_thys, thy_facts} =
   2.280 +          (mash_ADD ctxt records;
   2.281 +           {dirty_thys = dirty_thys,
   2.282 +            thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts})
   2.283 +      in mash_map trans end
   2.284 +  end
   2.285  
   2.286 -(* ###
   2.287 -fun compute_accessibility thy thy_facts =
   2.288 -  let
   2.289 -    fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th]
   2.290 -    fun add_thy facts =
   2.291 -      let
   2.292 -        val thy = theory_of_thm (hd facts)
   2.293 -        val parents = parent_facts thy_facts thy
   2.294 -      in add_facts facts parents end
   2.295 -  in fold (add_thy o snd) thy_facts end
   2.296 -*)
   2.297 -
   2.298 -fun mash_learn_proof thy t ths =
   2.299 -  mash_map (fn state as {fresh, dirty_thys, thy_facts} =>
   2.300 -    let val deps = ths |> map Thm.get_name_hint in
   2.301 -      if forall (is_fact_in_thy_facts thy_facts) deps then
   2.302 -        let
   2.303 -          val fact = fresh_fact_prefix ^ string_of_int fresh
   2.304 -          val access = accessibility_of thy thy_facts
   2.305 -          val feats = features_of thy General [t]
   2.306 -        in
   2.307 -          mash_ADD [(fact, access, feats, deps)];
   2.308 -          {fresh = fresh + 1, dirty_thys = dirty_thys, thy_facts = thy_facts}
   2.309 -        end
   2.310 -      else
   2.311 -        state
   2.312 -    end)
   2.313 +fun mash_learn_proof ctxt t ths =
   2.314 +  let val thy = Proof_Context.theory_of ctxt in
   2.315 +    mash_map (fn state as {dirty_thys, thy_facts} =>
   2.316 +      let val deps = ths |> map Thm.get_name_hint in
   2.317 +        if forall (is_fact_in_thy_facts thy_facts) deps then
   2.318 +          let
   2.319 +            val fact = ATP_Util.timestamp () (* should be fairly fresh *)
   2.320 +            val access = accessibility_of thy thy_facts
   2.321 +            val feats = features_of thy General [t]
   2.322 +          in
   2.323 +            mash_ADD ctxt [(fact, access, feats, deps)];
   2.324 +            {dirty_thys = dirty_thys, thy_facts = thy_facts}
   2.325 +          end
   2.326 +        else
   2.327 +          state
   2.328 +      end)
   2.329 +  end
   2.330  
   2.331  fun relevant_facts ctxt params prover max_facts
   2.332          ({add, only, ...} : fact_override) hyp_ts concl_t facts =

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     3.3 @@ -36,8 +36,7 @@
     3.4  val running_proversN = "running_provers"
     3.5  val kill_proversN = "kill_provers"
     3.6  val refresh_tptpN = "refresh_tptp"
     3.7 -val mash_resetN = "mash_reset"
     3.8 -val mash_learnN = "mash_learn"
     3.9 +val reset_mashN = "reset_mash"
    3.10  
    3.11  val auto = Unsynchronized.ref false
    3.12  
    3.13 @@ -377,10 +376,8 @@
    3.14        kill_provers ()
    3.15      else if subcommand = refresh_tptpN then
    3.16        refresh_systems_on_tptp ()
    3.17 -    else if subcommand = mash_resetN then
    3.18 -      mash_reset ()
    3.19 -    else if subcommand = mash_learnN then
    3.20 -      () (* TODO: implement *)
    3.21 +    else if subcommand = reset_mashN then
    3.22 +      mash_reset ctxt
    3.23      else
    3.24        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    3.25    end