moved ML code around
authorblanchet
Fri Jan 31 16:07:20 2014 +0100 (2014-01-31)
changeset 552115d027af93a08
parent 55210 d1e3b708d74b
child 55212 5832470d956e
moved ML code around
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 14:33:02 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 16:07:20 2014 +0100
     1.3 @@ -70,7 +70,6 @@
     1.4      val value = AList.lookup (op =) args key
     1.5    in if is_some value then (label, the value) :: list else list end
     1.6  
     1.7 -
     1.8  datatype sh_data = ShData of {
     1.9    calls: int,
    1.10    success: int,
    1.11 @@ -131,7 +130,6 @@
    1.12    proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
    1.13    nontriv_success, proofs, time, timeout, lemmas, posns)
    1.14  
    1.15 -
    1.16  datatype reconstructor_mode =
    1.17    Unminimized | Minimized | UnminimizedFT | MinimizedFT
    1.18  
    1.19 @@ -349,8 +347,7 @@
    1.20  
    1.21  end
    1.22  
    1.23 -
    1.24 -(* Warning: we implicitly assume single-threaded execution here! *)
    1.25 +(* Warning: we implicitly assume single-threaded execution here *)
    1.26  val data = Unsynchronized.ref ([] : (int * data) list)
    1.27  
    1.28  fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)
    1.29 @@ -496,9 +493,9 @@
    1.30      val time_prover = run_time |> Time.toMilliseconds
    1.31      val msg = message (Lazy.force preplay) ^ message_tail
    1.32    in
    1.33 -    case outcome of
    1.34 +    (case outcome of
    1.35        NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
    1.36 -    | SOME _ => (msg, SH_FAIL (time_isa, time_prover))
    1.37 +    | SOME _ => (msg, SH_FAIL (time_isa, time_prover)))
    1.38    end
    1.39    handle ERROR msg => ("error: " ^ msg, SH_ERROR)
    1.40  
    1.41 @@ -508,7 +505,6 @@
    1.42        ({pre=st, log, pos, ...}: Mirabelle.run_args) =
    1.43    let
    1.44      val thy = Proof.theory_of st
    1.45 -    val ctxt = Proof.context_of st
    1.46      val triv_str = if trivial then "[T] " else ""
    1.47      val _ = change_data id inc_sh_calls
    1.48      val _ = if trivial then () else change_data id inc_sh_nontriv_calls
    1.49 @@ -517,11 +513,12 @@
    1.50      val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
    1.51      val strict = AList.lookup (op =) args strictK |> the_default strict_default
    1.52      val max_facts =
    1.53 -      case AList.lookup (op =) args max_factsK of
    1.54 +      (case AList.lookup (op =) args max_factsK of
    1.55          SOME max => max
    1.56 -      | NONE => case AList.lookup (op =) args max_relevantK of
    1.57 -                  SOME max => max
    1.58 -                | NONE => max_facts_default
    1.59 +      | NONE =>
    1.60 +        (case AList.lookup (op =) args max_relevantK of
    1.61 +          SOME max => max
    1.62 +        | NONE => max_facts_default))
    1.63      val slice = AList.lookup (op =) args sliceK |> the_default slice_default
    1.64      val lam_trans = AList.lookup (op =) args lam_transK
    1.65      val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
    1.66 @@ -546,7 +543,7 @@
    1.67          hard_timeout timeout preplay_timeout sh_minimizeLST
    1.68          max_new_mono_instancesLST max_mono_itersLST dir pos st
    1.69    in
    1.70 -    case result of
    1.71 +    (case result of
    1.72        SH_OK (time_isa, time_prover, names) =>
    1.73          let
    1.74            fun get_thms (name, stature) =
    1.75 @@ -570,16 +567,14 @@
    1.76            val _ = change_data id (inc_sh_time_isa time_isa)
    1.77            val _ = change_data id (inc_sh_time_prover_fail time_prover)
    1.78          in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
    1.79 -    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
    1.80 +    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg))
    1.81    end
    1.82  
    1.83  end
    1.84  
    1.85 -fun run_minimize args reconstructor named_thms id
    1.86 -        ({pre=st, log, ...}: Mirabelle.run_args) =
    1.87 +fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
    1.88    let
    1.89      val thy = Proof.theory_of st
    1.90 -    val ctxt = Proof.context_of st
    1.91      val {goal, ...} = Proof.goal st
    1.92      val n0 = length (these (!named_thms))
    1.93      val prover_name = get_prover_name thy args
    1.94 @@ -613,7 +608,7 @@
    1.95        minimize st goal NONE (these (!named_thms))
    1.96      val msg = message (Lazy.force preplay) ^ message_tail
    1.97    in
    1.98 -    case used_facts of
    1.99 +    (case used_facts of
   1.100        SOME named_thms' =>
   1.101          (change_data id inc_min_succs;
   1.102           change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
   1.103 @@ -623,7 +618,7 @@
   1.104                 named_thms := SOME named_thms';
   1.105                 log (minimize_tag id ^ "succeeded:\n" ^ msg))
   1.106          )
   1.107 -    | NONE => log (minimize_tag id ^ "failed: " ^ msg)
   1.108 +    | NONE => log (minimize_tag id ^ "failed: " ^ msg))
   1.109    end
   1.110  
   1.111  fun override_params prover type_enc timeout =
   1.112 @@ -649,8 +644,7 @@
   1.113            timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
   1.114          fun sledge_tac time_slice prover type_enc =
   1.115            Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
   1.116 -              (override_params prover type_enc (my_timeout time_slice))
   1.117 -              fact_override
   1.118 +            (override_params prover type_enc (my_timeout time_slice)) fact_override
   1.119        in
   1.120          if !reconstructor = "sledgehammer_tac" then
   1.121            sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
   1.122 @@ -674,8 +668,7 @@
   1.123                ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
   1.124            in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
   1.125          else if !reconstructor = "metis" then
   1.126 -          Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt
   1.127 -            thms
   1.128 +          Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
   1.129          else
   1.130            K all_tac
   1.131        end
   1.132 @@ -689,19 +682,16 @@
   1.133            change_data id (inc_reconstructor_lemmas m (length named_thms));
   1.134            change_data id (inc_reconstructor_time m t);
   1.135            change_data id (inc_reconstructor_posns m (pos, trivial));
   1.136 -          if name = "proof" then change_data id (inc_reconstructor_proofs m)
   1.137 -          else ();
   1.138 +          if name = "proof" then change_data id (inc_reconstructor_proofs m) else ();
   1.139            "succeeded (" ^ string_of_int t ^ ")")
   1.140      fun timed_reconstructor named_thms =
   1.141        (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
   1.142 -      handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
   1.143 -               ("timeout", false))
   1.144 +      handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false))
   1.145             | ERROR msg => ("error: " ^ msg, false)
   1.146  
   1.147      val _ = log separator
   1.148      val _ = change_data id (inc_reconstructor_calls m)
   1.149 -    val _ = if trivial then ()
   1.150 -            else change_data id (inc_reconstructor_nontriv_calls m)
   1.151 +    val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m)
   1.152    in
   1.153      named_thms
   1.154      |> timed_reconstructor
     2.1 --- a/src/HOL/Sledgehammer.thy	Fri Jan 31 14:33:02 2014 +0100
     2.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jan 31 16:07:20 2014 +0100
     2.3 @@ -18,9 +18,8 @@
     2.4  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
     2.5  ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
     2.6  ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
     2.7 +ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
     2.8  ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
     2.9 -ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
    2.10 -ML_file "Tools/Sledgehammer/sledgehammer_isar_print.ML"
    2.11  ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
    2.12  ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
    2.13  ML_file "Tools/Sledgehammer/sledgehammer_isar_try0.ML"
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 14:33:02 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:07:20 2014 +0100
     3.3 @@ -32,7 +32,6 @@
     3.4  open Sledgehammer_Reconstructor
     3.5  open Sledgehammer_Isar_Proof
     3.6  open Sledgehammer_Isar_Annotate
     3.7 -open Sledgehammer_Isar_Print
     3.8  open Sledgehammer_Isar_Preplay
     3.9  open Sledgehammer_Isar_Compress
    3.10  open Sledgehammer_Isar_Try0
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML	Fri Jan 31 14:33:02 2014 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,262 +0,0 @@
     4.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
     4.5 -    Author:     Jasmin Blanchette, TU Muenchen
     4.6 -    Author:     Steffen Juilf Smolka, TU Muenchen
     4.7 -
     4.8 -Basic mapping from proof data structures to proof strings.
     4.9 -*)
    4.10 -
    4.11 -signature SLEDGEHAMMER_ISAR_PRINT =
    4.12 -sig
    4.13 -  type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    4.14 -  type reconstructor = Sledgehammer_Reconstructor.reconstructor
    4.15 -  type one_line_params = Sledgehammer_Reconstructor.one_line_params
    4.16 -
    4.17 -  val string_of_reconstructor : reconstructor -> string
    4.18 -  val one_line_proof_text : int -> one_line_params -> string
    4.19 -  val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
    4.20 -end;
    4.21 -
    4.22 -structure Sledgehammer_Isar_Print : SLEDGEHAMMER_ISAR_PRINT =
    4.23 -struct
    4.24 -
    4.25 -open ATP_Util
    4.26 -open ATP_Proof
    4.27 -open ATP_Problem_Generate
    4.28 -open ATP_Proof_Reconstruct
    4.29 -open Sledgehammer_Util
    4.30 -open Sledgehammer_Reconstructor
    4.31 -open Sledgehammer_Isar_Proof
    4.32 -open Sledgehammer_Isar_Annotate
    4.33 -
    4.34 -
    4.35 -(** reconstructors **)
    4.36 -
    4.37 -fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
    4.38 -  | string_of_reconstructor SMT = smtN
    4.39 -
    4.40 -
    4.41 -(** one-liner reconstructor proofs **)
    4.42 -
    4.43 -fun show_time NONE = ""
    4.44 -  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
    4.45 -
    4.46 -(* FIXME: Various bugs, esp. with "unfolding"
    4.47 -fun unusing_chained_facts _ 0 = ""
    4.48 -  | unusing_chained_facts used_chaineds num_chained =
    4.49 -    if length used_chaineds = num_chained then ""
    4.50 -    else if null used_chaineds then "(* using no facts *) "
    4.51 -    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
    4.52 -*)
    4.53 -
    4.54 -fun apply_on_subgoal _ 1 = "by "
    4.55 -  | apply_on_subgoal 1 _ = "apply "
    4.56 -  | apply_on_subgoal i n =
    4.57 -    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    4.58 -
    4.59 -fun using_labels [] = ""
    4.60 -  | using_labels ls = "using " ^ space_implode " " (map string_of_label ls) ^ " "
    4.61 -
    4.62 -fun command_call name [] =
    4.63 -    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
    4.64 -  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    4.65 -
    4.66 -fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
    4.67 -  (* unusing_chained_facts used_chaineds num_chained ^ *)
    4.68 -  using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
    4.69 -
    4.70 -fun try_command_line banner time command =
    4.71 -  banner ^ ": " ^
    4.72 -  Active.sendback_markup [Markup.padding_command] command ^
    4.73 -  show_time time ^ "."
    4.74 -
    4.75 -fun minimize_line _ [] = ""
    4.76 -  | minimize_line minimize_command ss =
    4.77 -    (case minimize_command ss of
    4.78 -      "" => ""
    4.79 -    | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
    4.80 -
    4.81 -fun split_used_facts facts =
    4.82 -  facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
    4.83 -        |> pairself (sort_distinct (string_ord o pairself fst))
    4.84 -
    4.85 -fun one_line_proof_text num_chained
    4.86 -    ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
    4.87 -  let
    4.88 -    val (chained, extra) = split_used_facts used_facts
    4.89 -    val (failed, ext_time) =
    4.90 -      (case play of
    4.91 -        Played time => (false, (SOME (false, time)))
    4.92 -      | Play_Timed_Out time => (false, SOME (true, time))
    4.93 -      | Play_Failed => (true, NONE)
    4.94 -      | Not_Played => (false, NONE))
    4.95 -    val try_line =
    4.96 -      ([], map fst extra)
    4.97 -      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
    4.98 -      |> (if failed then
    4.99 -            enclose "One-line proof reconstruction failed: "
   4.100 -                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
   4.101 -                     \solve this.)"
   4.102 -          else
   4.103 -            try_command_line banner ext_time)
   4.104 -  in
   4.105 -    try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   4.106 -  end
   4.107 -
   4.108 -
   4.109 -(** detailed Isar proofs **)
   4.110 -
   4.111 -val indent_size = 2
   4.112 -
   4.113 -fun string_of_proof ctxt type_enc lam_trans i n proof =
   4.114 -  let
   4.115 -    (* Make sure only type constraints inserted by the type annotation code are printed. *)
   4.116 -    val ctxt =
   4.117 -      ctxt |> Config.put show_markup false
   4.118 -           |> Config.put Printer.show_type_emphasis false
   4.119 -           |> Config.put show_types false
   4.120 -           |> Config.put show_sorts false
   4.121 -           |> Config.put show_consts false
   4.122 -
   4.123 -    val register_fixes = map Free #> fold Variable.auto_fixes
   4.124 -
   4.125 -    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
   4.126 -
   4.127 -    fun of_indent ind = replicate_string (ind * indent_size) " "
   4.128 -    fun of_moreover ind = of_indent ind ^ "moreover\n"
   4.129 -    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
   4.130 -
   4.131 -    fun of_obtain qs nr =
   4.132 -      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   4.133 -         "ultimately "
   4.134 -       else if nr = 1 orelse member (op =) qs Then then
   4.135 -         "then "
   4.136 -       else
   4.137 -         "") ^ "obtain"
   4.138 -
   4.139 -    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
   4.140 -    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
   4.141 -
   4.142 -    fun of_have qs nr =
   4.143 -      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   4.144 -        "ultimately " ^ of_show_have qs
   4.145 -      else if nr = 1 orelse member (op =) qs Then then
   4.146 -        of_thus_hence qs
   4.147 -      else
   4.148 -        of_show_have qs
   4.149 -
   4.150 -    fun add_term term (s, ctxt) =
   4.151 -      (s ^ (term
   4.152 -            |> singleton (Syntax.uncheck_terms ctxt)
   4.153 -            |> annotate_types ctxt
   4.154 -            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
   4.155 -            |> simplify_spaces
   4.156 -            |> maybe_quote),
   4.157 -       ctxt |> Variable.auto_fixes term)
   4.158 -
   4.159 -    fun by_method meth = "by " ^
   4.160 -      (case meth of
   4.161 -        Simp_Method => "simp"
   4.162 -      | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
   4.163 -      | Auto_Method => "auto"
   4.164 -      | Fastforce_Method => "fastforce"
   4.165 -      | Force_Method => "force"
   4.166 -      | Arith_Method => "arith"
   4.167 -      | Blast_Method => "blast"
   4.168 -      | Meson_Method => "meson"
   4.169 -      | _ => raise Fail "Sledgehammer_Isar_Print: by_method")
   4.170 -
   4.171 -    fun with_facts none _ [] [] = none
   4.172 -      | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
   4.173 -
   4.174 -    val using_facts = with_facts "" (enclose "using " " ")
   4.175 -
   4.176 -    (* Local facts are always passed via "using", which affects "meson" and "metis". This is
   4.177 -       arguably stylistically superior, because it emphasises the structure of the proof. It is also
   4.178 -       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
   4.179 -       and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
   4.180 -    fun of_method ls ss Metis_Method =
   4.181 -        using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss)
   4.182 -      | of_method ls ss Meson_Method =
   4.183 -        using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
   4.184 -      | of_method ls ss meth = using_facts ls ss ^ by_method meth
   4.185 -
   4.186 -    fun of_byline ind (ls, ss) meth =
   4.187 -      let
   4.188 -        val ls = ls |> sort_distinct label_ord
   4.189 -        val ss = ss |> sort_distinct string_ord
   4.190 -      in
   4.191 -        "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
   4.192 -      end
   4.193 -
   4.194 -    fun of_free (s, T) =
   4.195 -      maybe_quote s ^ " :: " ^
   4.196 -      maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
   4.197 -
   4.198 -    fun add_frees xs (s, ctxt) =
   4.199 -      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
   4.200 -
   4.201 -    fun add_fix _ [] = I
   4.202 -      | add_fix ind xs =
   4.203 -        add_suffix (of_indent ind ^ "fix ")
   4.204 -        #> add_frees xs
   4.205 -        #> add_suffix "\n"
   4.206 -
   4.207 -    fun add_assm ind (l, t) =
   4.208 -      add_suffix (of_indent ind ^ "assume " ^ of_label l)
   4.209 -      #> add_term t
   4.210 -      #> add_suffix "\n"
   4.211 -
   4.212 -    fun add_assms ind assms = fold (add_assm ind) assms
   4.213 -
   4.214 -    fun add_step_post ind l t facts meth =
   4.215 -      add_suffix (of_label l)
   4.216 -      #> add_term t
   4.217 -      #> add_suffix (of_byline ind facts meth ^ "\n")
   4.218 -
   4.219 -    fun of_subproof ind ctxt proof =
   4.220 -      let
   4.221 -        val ind = ind + 1
   4.222 -        val s = of_proof ind ctxt proof
   4.223 -        val prefix = "{ "
   4.224 -        val suffix = " }"
   4.225 -      in
   4.226 -        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   4.227 -        String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
   4.228 -        suffix ^ "\n"
   4.229 -      end
   4.230 -    and of_subproofs _ _ _ [] = ""
   4.231 -      | of_subproofs ind ctxt qs subproofs =
   4.232 -        (if member (op =) qs Then then of_moreover ind else "") ^
   4.233 -        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
   4.234 -    and add_step_pre ind qs subproofs (s, ctxt) =
   4.235 -      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
   4.236 -    and add_step ind (Let (t1, t2)) =
   4.237 -        add_suffix (of_indent ind ^ "let ")
   4.238 -        #> add_term t1
   4.239 -        #> add_suffix " = "
   4.240 -        #> add_term t2
   4.241 -        #> add_suffix "\n"
   4.242 -      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
   4.243 -        add_step_pre ind qs subproofs
   4.244 -        #> (case xs of
   4.245 -            [] => add_suffix (of_have qs (length subproofs) ^ " ")
   4.246 -          | _ =>
   4.247 -            add_suffix (of_obtain qs (length subproofs) ^ " ")
   4.248 -            #> add_frees xs
   4.249 -            #> add_suffix " where ")
   4.250 -        #> add_step_post ind l t facts meth
   4.251 -    and add_steps ind = fold (add_step ind)
   4.252 -    and of_proof ind ctxt (Proof (xs, assms, steps)) =
   4.253 -      ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
   4.254 -  in
   4.255 -    (* One-step Metis proofs are pointless; better use the one-liner directly. *)
   4.256 -    (case proof of
   4.257 -      Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
   4.258 -    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
   4.259 -    | _ =>
   4.260 -      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   4.261 -      of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   4.262 -      of_indent 0 ^ (if n <> 1 then "next" else "qed"))
   4.263 -  end
   4.264 -
   4.265 -end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 14:33:02 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:07:20 2014 +0100
     5.3 @@ -52,11 +52,21 @@
     5.4    val relabel_proof_canonically : isar_proof -> isar_proof
     5.5  
     5.6    structure Canonical_Lbl_Tab : TABLE
     5.7 +
     5.8 +  val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
     5.9  end;
    5.10  
    5.11  structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    5.12  struct
    5.13  
    5.14 +open ATP_Util
    5.15 +open ATP_Proof
    5.16 +open ATP_Problem_Generate
    5.17 +open ATP_Proof_Reconstruct
    5.18 +open Sledgehammer_Util
    5.19 +open Sledgehammer_Reconstructor
    5.20 +open Sledgehammer_Isar_Annotate
    5.21 +
    5.22  type label = string * int
    5.23  type facts = label list * string list (* local and global facts *)
    5.24  
    5.25 @@ -110,9 +120,7 @@
    5.26  
    5.27  val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
    5.28  
    5.29 -
    5.30 -(** canonical proof labels: 1, 2, 3, ... in post traversal order **)
    5.31 -
    5.32 +(* canonical proof labels: 1, 2, 3, ... in post traversal order *)
    5.33  fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
    5.34  
    5.35  structure Canonical_Lbl_Tab = Table(
    5.36 @@ -154,4 +162,152 @@
    5.37      fst (do_proof proof (0, []))
    5.38    end
    5.39  
    5.40 +val indent_size = 2
    5.41 +
    5.42 +fun string_of_proof ctxt type_enc lam_trans i n proof =
    5.43 +  let
    5.44 +    (* Make sure only type constraints inserted by the type annotation code are printed. *)
    5.45 +    val ctxt =
    5.46 +      ctxt |> Config.put show_markup false
    5.47 +           |> Config.put Printer.show_type_emphasis false
    5.48 +           |> Config.put show_types false
    5.49 +           |> Config.put show_sorts false
    5.50 +           |> Config.put show_consts false
    5.51 +
    5.52 +    val register_fixes = map Free #> fold Variable.auto_fixes
    5.53 +
    5.54 +    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
    5.55 +
    5.56 +    fun of_indent ind = replicate_string (ind * indent_size) " "
    5.57 +    fun of_moreover ind = of_indent ind ^ "moreover\n"
    5.58 +    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
    5.59 +
    5.60 +    fun of_obtain qs nr =
    5.61 +      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
    5.62 +       else if nr = 1 orelse member (op =) qs Then then "then "
    5.63 +       else "") ^ "obtain"
    5.64 +
    5.65 +    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
    5.66 +    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
    5.67 +
    5.68 +    fun of_have qs nr =
    5.69 +      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
    5.70 +      else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
    5.71 +      else of_show_have qs
    5.72 +
    5.73 +    fun add_term term (s, ctxt) =
    5.74 +      (s ^ (term
    5.75 +            |> singleton (Syntax.uncheck_terms ctxt)
    5.76 +            |> annotate_types ctxt
    5.77 +            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
    5.78 +            |> simplify_spaces
    5.79 +            |> maybe_quote),
    5.80 +       ctxt |> Variable.auto_fixes term)
    5.81 +
    5.82 +    fun by_method meth = "by " ^
    5.83 +      (case meth of
    5.84 +        Simp_Method => "simp"
    5.85 +      | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
    5.86 +      | Auto_Method => "auto"
    5.87 +      | Fastforce_Method => "fastforce"
    5.88 +      | Force_Method => "force"
    5.89 +      | Arith_Method => "arith"
    5.90 +      | Blast_Method => "blast"
    5.91 +      | Meson_Method => "meson"
    5.92 +      | _ => raise Fail "Sledgehammer_Isar_Print: by_method")
    5.93 +
    5.94 +    fun with_facts none _ [] [] = none
    5.95 +      | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
    5.96 +
    5.97 +    val using_facts = with_facts "" (enclose "using " " ")
    5.98 +
    5.99 +    (* Local facts are always passed via "using", which affects "meson" and "metis". This is
   5.100 +       arguably stylistically superior, because it emphasises the structure of the proof. It is also
   5.101 +       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
   5.102 +       and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
   5.103 +    fun of_method ls ss Metis_Method =
   5.104 +        using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ss
   5.105 +      | of_method ls ss Meson_Method =
   5.106 +        using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
   5.107 +      | of_method ls ss meth = using_facts ls ss ^ by_method meth
   5.108 +
   5.109 +    fun of_byline ind (ls, ss) meth =
   5.110 +      let
   5.111 +        val ls = ls |> sort_distinct label_ord
   5.112 +        val ss = ss |> sort_distinct string_ord
   5.113 +      in
   5.114 +        "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
   5.115 +      end
   5.116 +
   5.117 +    fun of_free (s, T) =
   5.118 +      maybe_quote s ^ " :: " ^
   5.119 +      maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
   5.120 +
   5.121 +    fun add_frees xs (s, ctxt) =
   5.122 +      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
   5.123 +
   5.124 +    fun add_fix _ [] = I
   5.125 +      | add_fix ind xs =
   5.126 +        add_suffix (of_indent ind ^ "fix ")
   5.127 +        #> add_frees xs
   5.128 +        #> add_suffix "\n"
   5.129 +
   5.130 +    fun add_assm ind (l, t) =
   5.131 +      add_suffix (of_indent ind ^ "assume " ^ of_label l)
   5.132 +      #> add_term t
   5.133 +      #> add_suffix "\n"
   5.134 +
   5.135 +    fun add_assms ind assms = fold (add_assm ind) assms
   5.136 +
   5.137 +    fun add_step_post ind l t facts meth =
   5.138 +      add_suffix (of_label l)
   5.139 +      #> add_term t
   5.140 +      #> add_suffix (of_byline ind facts meth ^ "\n")
   5.141 +
   5.142 +    fun of_subproof ind ctxt proof =
   5.143 +      let
   5.144 +        val ind = ind + 1
   5.145 +        val s = of_proof ind ctxt proof
   5.146 +        val prefix = "{ "
   5.147 +        val suffix = " }"
   5.148 +      in
   5.149 +        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   5.150 +        String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
   5.151 +        suffix ^ "\n"
   5.152 +      end
   5.153 +    and of_subproofs _ _ _ [] = ""
   5.154 +      | of_subproofs ind ctxt qs subproofs =
   5.155 +        (if member (op =) qs Then then of_moreover ind else "") ^
   5.156 +        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
   5.157 +    and add_step_pre ind qs subproofs (s, ctxt) =
   5.158 +      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
   5.159 +    and add_step ind (Let (t1, t2)) =
   5.160 +        add_suffix (of_indent ind ^ "let ")
   5.161 +        #> add_term t1
   5.162 +        #> add_suffix " = "
   5.163 +        #> add_term t2
   5.164 +        #> add_suffix "\n"
   5.165 +      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
   5.166 +        add_step_pre ind qs subproofs
   5.167 +        #> (case xs of
   5.168 +            [] => add_suffix (of_have qs (length subproofs) ^ " ")
   5.169 +          | _ =>
   5.170 +            add_suffix (of_obtain qs (length subproofs) ^ " ")
   5.171 +            #> add_frees xs
   5.172 +            #> add_suffix " where ")
   5.173 +        #> add_step_post ind l t facts meth
   5.174 +    and add_steps ind = fold (add_step ind)
   5.175 +    and of_proof ind ctxt (Proof (xs, assms, steps)) =
   5.176 +      ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
   5.177 +  in
   5.178 +    (* One-step Metis proofs are pointless; better use the one-liner directly. *)
   5.179 +    (case proof of
   5.180 +      Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
   5.181 +    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
   5.182 +    | _ =>
   5.183 +      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   5.184 +      of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   5.185 +      of_indent 0 ^ (if n <> 1 then "next" else "qed"))
   5.186 +  end
   5.187 +
   5.188  end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 14:33:02 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:07:20 2014 +0100
     6.3 @@ -110,7 +110,6 @@
     6.4  open Sledgehammer_Util
     6.5  open Sledgehammer_Fact
     6.6  open Sledgehammer_Reconstructor
     6.7 -open Sledgehammer_Isar_Print
     6.8  open Sledgehammer_Isar
     6.9  
    6.10  (* Empty string means create files in Isabelle's temporary files directory. *)
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 14:33:02 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:07:20 2014 +0100
     7.3 @@ -42,7 +42,6 @@
     7.4  open ATP_Proof_Reconstruct
     7.5  open Sledgehammer_Util
     7.6  open Sledgehammer_Reconstructor
     7.7 -open Sledgehammer_Isar_Print
     7.8  open Sledgehammer_Prover
     7.9  
    7.10  val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Fri Jan 31 14:33:02 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Fri Jan 31 16:07:20 2014 +0100
     8.3 @@ -19,13 +19,16 @@
     8.4      Play_Failed |
     8.5      Not_Played
     8.6  
     8.7 -  val string_of_play_outcome: play_outcome -> string
     8.8 -
     8.9    type minimize_command = string list -> string
    8.10    type one_line_params =
    8.11      (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
    8.12  
    8.13    val smtN : string
    8.14 +  val string_of_reconstructor : reconstructor -> string
    8.15 +  val string_of_play_outcome : play_outcome -> string
    8.16 +  val reconstructor_command : reconstructor -> int -> int -> string list -> int -> string list ->
    8.17 +    string
    8.18 +  val one_line_proof_text : int -> one_line_params -> string
    8.19  
    8.20    val silence_reconstructors : bool -> Proof.context -> Proof.context
    8.21  end;
    8.22 @@ -35,6 +38,7 @@
    8.23  
    8.24  open ATP_Util
    8.25  open ATP_Problem_Generate
    8.26 +open ATP_Proof_Reconstruct
    8.27  
    8.28  datatype reconstructor =
    8.29    Metis of string * string |
    8.30 @@ -46,16 +50,81 @@
    8.31    Play_Failed |
    8.32    Not_Played
    8.33  
    8.34 +type minimize_command = string list -> string
    8.35 +type one_line_params =
    8.36 +  (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
    8.37 +
    8.38 +val smtN = "smt"
    8.39 +
    8.40 +fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
    8.41 +  | string_of_reconstructor SMT = smtN
    8.42 +
    8.43  fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
    8.44    | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
    8.45    | string_of_play_outcome Play_Failed = "failed"
    8.46    | string_of_play_outcome _ = "unknown"
    8.47  
    8.48 -type minimize_command = string list -> string
    8.49 -type one_line_params =
    8.50 -  (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
    8.51 +(* FIXME: Various bugs, esp. with "unfolding"
    8.52 +fun unusing_chained_facts _ 0 = ""
    8.53 +  | unusing_chained_facts used_chaineds num_chained =
    8.54 +    if length used_chaineds = num_chained then ""
    8.55 +    else if null used_chaineds then "(* using no facts *) "
    8.56 +    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
    8.57 +*)
    8.58 +
    8.59 +fun apply_on_subgoal _ 1 = "by "
    8.60 +  | apply_on_subgoal 1 _ = "apply "
    8.61 +  | apply_on_subgoal i n =
    8.62 +    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    8.63 +
    8.64 +fun command_call name [] =
    8.65 +    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
    8.66 +  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    8.67 +
    8.68 +fun reconstructor_command reconstr i n used_chaineds num_chained ss =
    8.69 +  (* unusing_chained_facts used_chaineds num_chained ^ *)
    8.70 +  apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
    8.71 +
    8.72 +fun show_time NONE = ""
    8.73 +  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
    8.74 +
    8.75 +fun try_command_line banner time command =
    8.76 +  banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "."
    8.77  
    8.78 -val smtN = "smt"
    8.79 +fun minimize_line _ [] = ""
    8.80 +  | minimize_line minimize_command ss =
    8.81 +    (case minimize_command ss of
    8.82 +      "" => ""
    8.83 +    | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
    8.84 +
    8.85 +fun split_used_facts facts =
    8.86 +  facts
    8.87 +  |> List.partition (fn (_, (sc, _)) => sc = Chained)
    8.88 +  |> pairself (sort_distinct (string_ord o pairself fst))
    8.89 +
    8.90 +fun one_line_proof_text num_chained
    8.91 +    ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
    8.92 +  let
    8.93 +    val (chained, extra) = split_used_facts used_facts
    8.94 +
    8.95 +    val (failed, ext_time) =
    8.96 +      (case play of
    8.97 +        Played time => (false, (SOME (false, time)))
    8.98 +      | Play_Timed_Out time => (false, SOME (true, time))
    8.99 +      | Play_Failed => (true, NONE)
   8.100 +      | Not_Played => (false, NONE))
   8.101 +
   8.102 +    val try_line =
   8.103 +      map fst extra
   8.104 +      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
   8.105 +      |> (if failed then
   8.106 +            enclose "One-line proof reconstruction failed: "
   8.107 +              ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
   8.108 +          else
   8.109 +            try_command_line banner ext_time)
   8.110 +  in
   8.111 +    try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   8.112 +  end
   8.113  
   8.114  (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
   8.115     bound exceeded" warnings and the like. *)