1.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* ATP Theory Exporter *}
     1.5  
     1.6  theory ATP_Theory_Export
     1.7 -imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
     1.8 +imports Complex_Main
     1.9  uses "atp_theory_export.ML"
    1.10  begin
    1.11  
    1.12 @@ -15,7 +15,7 @@
    1.13  *}
    1.14  
    1.15  ML {*
    1.16 -val do_it = true; (* switch to "true" to generate the files *)
    1.17 +val do_it = false; (* switch to "true" to generate the files *)
    1.18  val thy = @{theory List};
    1.19  val ctxt = @{context}
    1.20  *}

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4      fun do_fact ((_, (_, status)), th) prevs =
     2.5        let
     2.6          val name = Thm.get_name_hint th
     2.7 -        val feats = features_of thy (status, th)
     2.8 +        val feats = features_of thy status [prop_of th]
     2.9          val deps = isabelle_dependencies_of all_names th
    2.10          val kind = Thm.legacy_get_kind th
    2.11          val name = fact_name_of name

     3.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 18 08:44:03 2012 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 18 08:44:03 2012 +0200
     3.3 @@ -94,7 +94,7 @@
     3.4    val is_type_enc_sound : type_enc -> bool
     3.5    val type_enc_from_string : strictness -> string -> type_enc
     3.6    val adjust_type_enc : atp_format -> type_enc -> type_enc
     3.7 -  val has_no_lambdas : term -> bool
     3.8 +  val is_lambda_free : term -> bool
     3.9    val mk_aconns :
    3.10      connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
    3.11    val unmangled_const : string -> string * (string, 'b) ho_term list
    3.12 @@ -699,22 +699,22 @@
    3.13      (if is_type_enc_sound type_enc then Tags else Guards) stuff
    3.14    | adjust_type_enc _ type_enc = type_enc
    3.15  
    3.16 -fun has_no_lambdas t =
    3.17 +fun is_lambda_free t =
    3.18    case t of
    3.19 -    @{const Not} $ t1 => has_no_lambdas t1
    3.20 -  | Const (@{const_name All}, _) $ Abs (_, _, t') => has_no_lambdas t'
    3.21 -  | Const (@{const_name All}, _) $ t1 => has_no_lambdas t1
    3.22 -  | Const (@{const_name Ex}, _) $ Abs (_, _, t') => has_no_lambdas t'
    3.23 -  | Const (@{const_name Ex}, _) $ t1 => has_no_lambdas t1
    3.24 -  | @{const HOL.conj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
    3.25 -  | @{const HOL.disj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
    3.26 -  | @{const HOL.implies} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
    3.27 +    @{const Not} $ t1 => is_lambda_free t1
    3.28 +  | Const (@{const_name All}, _) $ Abs (_, _, t') => is_lambda_free t'
    3.29 +  | Const (@{const_name All}, _) $ t1 => is_lambda_free t1
    3.30 +  | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_lambda_free t'
    3.31 +  | Const (@{const_name Ex}, _) $ t1 => is_lambda_free t1
    3.32 +  | @{const HOL.conj} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
    3.33 +  | @{const HOL.disj} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
    3.34 +  | @{const HOL.implies} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
    3.35    | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    3.36 -    has_no_lambdas t1 andalso has_no_lambdas t2
    3.37 +    is_lambda_free t1 andalso is_lambda_free t2
    3.38    | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
    3.39  
    3.40  fun simple_translate_lambdas do_lambdas ctxt t =
    3.41 -  if has_no_lambdas t then
    3.42 +  if is_lambda_free t then
    3.43      t
    3.44    else
    3.45      let

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    val thms_by_thy : ('a * thm) list -> (string * thm list) list
     4.5    val has_thy : theory -> thm -> bool
     4.6    val parent_facts : (string * thm list) list -> theory -> string list
     4.7 -  val features_of : theory -> status * thm -> string list
     4.8 +  val features_of : theory -> status -> term list -> string list
     4.9    val isabelle_dependencies_of : string list -> thm -> string list
    4.10    val goal_of_thm : theory -> thm -> thm
    4.11    val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
    4.12 @@ -32,10 +32,14 @@
    4.13      Proof.context -> theory -> bool -> string -> unit
    4.14    val generate_atp_dependencies :
    4.15      Proof.context -> params -> theory -> bool -> string -> unit
    4.16 +  val mash_RESET : unit -> unit
    4.17 +  val mash_ADD : string -> string list -> string list -> string list -> unit
    4.18 +  val mash_DEL : string list -> string list -> unit
    4.19 +  val mash_SUGGEST : string list -> string list -> string list
    4.20    val mash_reset : unit -> unit
    4.21    val mash_can_suggest_facts : unit -> bool
    4.22    val mash_suggest_facts :
    4.23 -    theory -> params -> string -> int -> term list -> term -> fact list
    4.24 +    Proof.context -> params -> string -> int -> term list -> term -> fact list
    4.25      -> fact list * fact list
    4.26    val mash_can_learn_thy : theory -> bool
    4.27    val mash_learn_thy : theory -> real -> unit
    4.28 @@ -59,25 +63,11 @@
    4.29  val model_file = "model"
    4.30  val state_file = "state"
    4.31  
    4.32 -fun mash_path file = getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file
    4.33 +fun mk_path file =
    4.34 +  getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file
    4.35 +  |> Path.explode
    4.36  
    4.37 -
    4.38 -(*** Low-level communication with MaSh ***)
    4.39 -
    4.40 -fun mash_RESET () =
    4.41 -  warning "MaSh RESET"
    4.42 -
    4.43 -fun mash_ADD fact access feats deps =
    4.44 -  warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
    4.45 -           space_implode " " feats ^ "; " ^ space_implode " " deps)
    4.46 -
    4.47 -fun mash_DEL fact =
    4.48 -  warning ("MaSh DEL " ^ fact)
    4.49 -
    4.50 -fun mash_SUGGEST access feats =
    4.51 -  warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^
    4.52 -           space_implode " " feats)
    4.53 -
    4.54 +val fresh_fact_prefix = Long_Name.separator
    4.55  
    4.56  (*** Isabelle helpers ***)
    4.57  
    4.58 @@ -145,7 +135,7 @@
    4.59  
    4.60  end
    4.61  
    4.62 -fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
    4.63 +fun interesting_terms_types_and_classes term_max_depth type_max_depth ts =
    4.64    let
    4.65      val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
    4.66      val bad_consts = atp_widely_irrelevant_consts
    4.67 @@ -180,10 +170,10 @@
    4.68           | _ => I)
    4.69          #> fold add_patterns args
    4.70        end
    4.71 -  in [] |> add_patterns t |> sort string_ord end
    4.72 +  in [] |> fold add_patterns ts |> sort string_ord end
    4.73  
    4.74  fun is_likely_tautology th =
    4.75 -  null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
    4.76 +  null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso
    4.77    not (Thm.eq_thm_prop (@{thm ext}, th))
    4.78  
    4.79  fun is_too_meta thy th =
    4.80 @@ -227,22 +217,20 @@
    4.81  val type_max_depth = 1
    4.82  
    4.83  (* TODO: Generate type classes for types? *)
    4.84 -fun features_of thy (status, th) =
    4.85 -  let val t = Thm.prop_of th in
    4.86 -    thy_name_of (thy_name_of_thm th) ::
    4.87 -    interesting_terms_types_and_classes term_max_depth type_max_depth t
    4.88 -    |> not (has_no_lambdas t) ? cons "lambdas"
    4.89 -    |> exists_Const is_exists t ? cons "skolems"
    4.90 -    |> not (is_fo_term thy t) ? cons "ho"
    4.91 -    |> (case status of
    4.92 -          General => I
    4.93 -        | Induction => cons "induction"
    4.94 -        | Intro => cons "intro"
    4.95 -        | Inductive => cons "inductive"
    4.96 -        | Elim => cons "elim"
    4.97 -        | Simp => cons "simp"
    4.98 -        | Def => cons "def")
    4.99 -  end
   4.100 +fun features_of thy status ts =
   4.101 +  thy_name_of (Context.theory_name thy) ::
   4.102 +  interesting_terms_types_and_classes term_max_depth type_max_depth ts
   4.103 +  |> exists (not o is_lambda_free) ts ? cons "lambdas"
   4.104 +  |> exists (exists_Const is_exists) ts ? cons "skolems"
   4.105 +  |> exists (not o is_fo_term thy) ts ? cons "ho"
   4.106 +  |> (case status of
   4.107 +        General => I
   4.108 +      | Induction => cons "induction"
   4.109 +      | Intro => cons "intro"
   4.110 +      | Inductive => cons "inductive"
   4.111 +      | Elim => cons "elim"
   4.112 +      | Simp => cons "simp"
   4.113 +      | Def => cons "def")
   4.114  
   4.115  fun isabelle_dependencies_of all_facts =
   4.116    thms_in_proof (SOME all_facts)
   4.117 @@ -303,7 +291,7 @@
   4.118      fun do_fact ((_, (_, status)), th) =
   4.119        let
   4.120          val name = Thm.get_name_hint th
   4.121 -        val feats = features_of thy (status, th)
   4.122 +        val feats = features_of (theory_of_thm th) status [prop_of th]
   4.123          val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
   4.124        in File.append path s end
   4.125    in List.app do_fact facts end
   4.126 @@ -375,68 +363,106 @@
   4.127    in List.app do_thm ths end
   4.128  
   4.129  
   4.130 +(*** Low-level communication with MaSh ***)
   4.131 +
   4.132 +fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file))
   4.133 +
   4.134 +fun mash_ADD fact access feats deps =
   4.135 +  warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
   4.136 +           space_implode " " feats ^ "; " ^ space_implode " " deps)
   4.137 +
   4.138 +fun mash_DEL facts feats =
   4.139 +  warning ("MaSh DEL " ^ space_implode " " facts ^ "; " ^
   4.140 +           space_implode " " feats)
   4.141 +
   4.142 +fun mash_SUGGEST access feats =
   4.143 +  (warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^
   4.144 +            space_implode " " feats);
   4.145 +   [])
   4.146 +
   4.147 +
   4.148  (*** High-level communication with MaSh ***)
   4.149  
   4.150  type mash_state =
   4.151 -  {completed_thys : unit Symtab.table,
   4.152 +  {fresh : int,
   4.153 +   completed_thys : unit Symtab.table,
   4.154     thy_facts : string list Symtab.table}
   4.155  
   4.156  val mash_zero =
   4.157 -  {completed_thys = Symtab.empty,
   4.158 +  {fresh = 0,
   4.159 +   completed_thys = Symtab.empty,
   4.160     thy_facts = Symtab.empty}
   4.161  
   4.162  local
   4.163  
   4.164  fun mash_load (state as (true, _)) = state
   4.165    | mash_load _ =
   4.166 -    (true,
   4.167 -     case mash_path state_file |> Path.explode |> File.read_lines of
   4.168 -       [] => mash_zero
   4.169 -     | comp_line :: facts_lines =>
   4.170 -       let
   4.171 -         fun comp_thys_of_line comp_line =
   4.172 -           Symtab.make (comp_line |> space_explode " " |> map (rpair ()))
   4.173 -         fun add_facts_line line =
   4.174 -           case space_explode " " line of
   4.175 -             thy :: facts => Symtab.update_new (thy, facts)
   4.176 -           | _ => I (* shouldn't happen *)
   4.177 -       in
   4.178 -         {completed_thys = comp_thys_of_line comp_line,
   4.179 -          thy_facts = fold add_facts_line facts_lines Symtab.empty}
   4.180 -       end)
   4.181 +    let
   4.182 +      val path = mk_path state_file
   4.183 +      val _ = Isabelle_System.mkdir (path |> Path.dir)
   4.184 +    in
   4.185 +      (true,
   4.186 +       case try File.read_lines path of
   4.187 +         SOME (fresh_line :: comp_line :: facts_lines) =>
   4.188 +         let
   4.189 +           fun comp_thys_of_line comp_line =
   4.190 +             Symtab.make (comp_line |> space_explode " " |> map (rpair ()))
   4.191 +           fun add_facts_line line =
   4.192 +             case space_explode " " line of
   4.193 +               thy :: facts => Symtab.update_new (thy, facts)
   4.194 +             | _ => I (* shouldn't happen *)
   4.195 +         in
   4.196 +           {fresh = Int.fromString fresh_line |> the_default 0,
   4.197 +            completed_thys = comp_thys_of_line comp_line,
   4.198 +            thy_facts = fold add_facts_line facts_lines Symtab.empty}
   4.199 +         end
   4.200 +       | _ => mash_zero)
   4.201 +    end
   4.202  
   4.203 -fun mash_save ({completed_thys, thy_facts} : mash_state) =
   4.204 +fun mash_save ({fresh, completed_thys, thy_facts} : mash_state) =
   4.205    let
   4.206 -    val path = mash_path state_file |> Path.explode
   4.207 +    val path = mk_path state_file
   4.208      val comp_line = (completed_thys |> Symtab.keys |> space_implode " ") ^ "\n"
   4.209      fun fact_line_for (thy, facts) = space_implode " " (thy :: facts) ^ "\n"
   4.210    in
   4.211 -    File.write path comp_line;
   4.212 +    File.write path (string_of_int fresh ^ "\n" ^ comp_line);
   4.213      Symtab.fold (fn thy_fact => fn () =>
   4.214                      File.append path (fact_line_for thy_fact)) thy_facts
   4.215    end
   4.216  
   4.217 -val state =
   4.218 -  Synchronized.var "Sledgehammer_Filter_MaSh.state" (false, mash_zero)
   4.219 +val global_state =
   4.220 +  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, mash_zero)
   4.221  
   4.222  in
   4.223  
   4.224  fun mash_change f =
   4.225 -  Synchronized.change state (apsnd (tap mash_save o f) o mash_load)
   4.226 +  Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
   4.227  
   4.228 -fun mash_value () = Synchronized.change_result state (`snd o mash_load)
   4.229 +fun mash_peek f = Synchronized.change global_state (mash_load ##> tap f)
   4.230 +
   4.231 +fun mash_value () = Synchronized.change_result global_state (mash_load #> `snd)
   4.232 +
   4.233 +fun mash_reset () =
   4.234 +  Synchronized.change global_state (fn _ =>
   4.235 +      (mash_RESET (); File.rm (mk_path state_file); (true, mash_zero)))
   4.236  
   4.237  end
   4.238  
   4.239 -fun mash_reset () = mash_change (fn _ => (mash_RESET (); mash_zero))
   4.240 -
   4.241  fun mash_can_suggest_facts () =
   4.242    not (Symtab.is_empty (#thy_facts (mash_value ())))
   4.243  
   4.244 +fun accessibility_of thy thy_facts =
   4.245 +  let
   4.246 +    val _ = 0
   4.247 +  in
   4.248 +    [] (*###*)
   4.249 +  end
   4.250 +
   4.251  fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts =
   4.252    let
   4.253 -    val access = []
   4.254 -    val feats = []
   4.255 +    val thy = Proof_Context.theory_of ctxt
   4.256 +    val access = accessibility_of thy (#thy_facts (mash_value ()))
   4.257 +    val feats = features_of thy General (concl_t :: hyp_ts)
   4.258      val suggs = mash_SUGGEST access feats
   4.259    in (facts, []) end
   4.260  
   4.261 @@ -445,14 +471,20 @@
   4.262                        (Context.theory_name thy))
   4.263  
   4.264  fun mash_learn_thy thy timeout = ()
   4.265 +(* ### *)
   4.266  
   4.267 -fun mash_learn_proof thy t ths = ()
   4.268 -(*###
   4.269 -  let
   4.270 -  in
   4.271 -    mash_ADD
   4.272 -  end
   4.273 -*)
   4.274 +fun mash_learn_proof thy t ths =
   4.275 +  mash_change (fn {fresh, completed_thys, thy_facts} =>
   4.276 +    let
   4.277 +      val fact = fresh_fact_prefix ^ string_of_int fresh
   4.278 +      val access = accessibility_of thy thy_facts
   4.279 +      val feats = features_of thy General [t]
   4.280 +      val deps = ths |> map (fact_name_of o Thm.get_name_hint)
   4.281 +    in
   4.282 +      mash_ADD fact access feats deps;
   4.283 +      {fresh = fresh + 1, completed_thys = completed_thys,
   4.284 +       thy_facts = thy_facts}
   4.285 +    end)
   4.286  
   4.287  fun relevant_facts ctxt params prover max_facts
   4.288          ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   4.289 @@ -472,7 +504,7 @@
   4.290                                   concl_t facts
   4.291        val (mash_facts, mash_rejected) =
   4.292          mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
   4.293 -      val mesh_facts = iter_facts
   4.294 +      val mesh_facts = iter_facts (* ### *)
   4.295      in
   4.296        mesh_facts
   4.297        |> not (null add_ths) ? prepend_facts add_ths

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     5.3 @@ -39,12 +39,6 @@
     5.4  val mash_resetN = "mash_reset"
     5.5  val mash_learnN = "mash_learn"
     5.6  
     5.7 -(* experimental *)
     5.8 -val mash_RESET_N = "mash_RESET"
     5.9 -val mash_ADD_N = "mash_ADD"
    5.10 -val mash_DEL_N = "mash_DEL"
    5.11 -val mash_SUGGEST_N = "mash_SUGGEST"
    5.12 -
    5.13  val auto = Unsynchronized.ref false
    5.14  
    5.15  val _ =
    5.16 @@ -387,14 +381,6 @@
    5.17        mash_reset ()
    5.18      else if subcommand = mash_learnN then
    5.19        () (* TODO: implement *)
    5.20 -    else if subcommand = mash_RESET_N then
    5.21 -      () (* TODO: implement *)
    5.22 -    else if subcommand = mash_ADD_N then
    5.23 -      () (* TODO: implement *)
    5.24 -    else if subcommand = mash_DEL_N then
    5.25 -      () (* TODO: implement *)
    5.26 -    else if subcommand = mash_SUGGEST_N then
    5.27 -      () (* TODO: implement *)
    5.28      else
    5.29        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    5.30    end