moved code -> easier debugging
authorsmolkas
Tue Jul 09 18:44:59 2013 +0200 (2013-07-09 ago)
changeset 525556811291d1869
parent 52554 19764bef2730
child 52556 c8357085217c
moved code -> easier debugging
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jul 08 14:24:36 2013 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jul 09 18:44:59 2013 +0200
     1.3 @@ -462,7 +462,7 @@
     1.4      fun failed failure =
     1.5        ({outcome = SOME failure, used_facts = [], used_from = [],
     1.6          run_time = Time.zeroTime,
     1.7 -        preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play
     1.8 +        preplay = Lazy.value (Sledgehammer_Reconstructor.Failed_to_Play
     1.9            Sledgehammer_Provers.plain_metis),
    1.10          message = K "", message_tail = ""}, ~1)
    1.11      val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
     2.1 --- a/src/HOL/Sledgehammer.thy	Mon Jul 08 14:24:36 2013 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 09 18:44:59 2013 +0200
     2.3 @@ -14,9 +14,11 @@
     2.4  
     2.5  ML_file "Tools/Sledgehammer/async_manager.ML"
     2.6  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
     2.7 +ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
     2.8  ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
     2.9 +ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
    2.10  ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
    2.11 -ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
    2.12 +ML_file "Tools/Sledgehammer/sledgehammer_print.ML"
    2.13  ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
    2.14  ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
    2.15  ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon Jul 08 14:24:36 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jul 09 18:44:59 2013 +0200
     3.3 @@ -36,6 +36,7 @@
     3.4        val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
     3.5        val ((v', s''), _) = post_traverse_term_type' f env v s'
     3.6      in f (u' $ v') T s'' end
     3.7 +    handle Bind => raise Fail "Sledgehammer_Annotate: post_traverse_term_type'"
     3.8  
     3.9  fun post_traverse_term_type f s t =
    3.10    post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jul 08 14:24:36 2013 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Jul 09 18:44:59 2013 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  signature SLEDGEHAMMER_MINIMIZE =
     4.5  sig
     4.6    type stature = ATP_Problem_Generate.stature
     4.7 -  type play = Sledgehammer_Reconstruct.play
     4.8 +  type play = Sledgehammer_Reconstructor.play
     4.9    type mode = Sledgehammer_Provers.mode
    4.10    type params = Sledgehammer_Provers.params
    4.11    type prover = Sledgehammer_Provers.prover
    4.12 @@ -38,6 +38,7 @@
    4.13  open ATP_Systems
    4.14  open Sledgehammer_Util
    4.15  open Sledgehammer_Fact
    4.16 +open Sledgehammer_Reconstructor
    4.17  open Sledgehammer_Reconstruct
    4.18  open Sledgehammer_Provers
    4.19  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Jul 09 18:44:59 2013 +0200
     5.3 @@ -0,0 +1,246 @@
     5.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Author:     Steffen Juilf Smolka, TU Muenchen
     5.7 +
     5.8 +Basic mapping from proof data structures to proof strings.
     5.9 +*)
    5.10 +
    5.11 +signature SLEDGEHAMMER_PRINT =
    5.12 +sig
    5.13 +  type isar_proof = Sledgehammer_Proof.isar_proof
    5.14 +  type reconstructor = Sledgehammer_Reconstructor.reconstructor
    5.15 +  type one_line_params = Sledgehammer_Reconstructor.one_line_params
    5.16 +
    5.17 +  val string_of_reconstructor : reconstructor -> string
    5.18 +
    5.19 +  val one_line_proof_text : int -> one_line_params -> string
    5.20 +
    5.21 +  val string_of_proof :
    5.22 +    Proof.context -> string -> string -> int -> int -> isar_proof -> string
    5.23 +end;
    5.24 +
    5.25 +structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
    5.26 +struct
    5.27 +
    5.28 +open ATP_Util
    5.29 +open ATP_Proof
    5.30 +open ATP_Problem_Generate
    5.31 +open ATP_Proof_Reconstruct
    5.32 +open Sledgehammer_Util
    5.33 +open Sledgehammer_Reconstructor
    5.34 +open Sledgehammer_Proof
    5.35 +open Sledgehammer_Annotate
    5.36 +
    5.37 +
    5.38 +(** reconstructors **)
    5.39 +
    5.40 +fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
    5.41 +    metis_call type_enc lam_trans
    5.42 +  | string_of_reconstructor SMT = smtN
    5.43 +
    5.44 +
    5.45 +
    5.46 +(** one-liner reconstructor proofs **)
    5.47 +
    5.48 +fun show_time NONE = ""
    5.49 +  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
    5.50 +
    5.51 +(* FIXME: Various bugs, esp. with "unfolding"
    5.52 +fun unusing_chained_facts _ 0 = ""
    5.53 +  | unusing_chained_facts used_chaineds num_chained =
    5.54 +    if length used_chaineds = num_chained then ""
    5.55 +    else if null used_chaineds then "(* using no facts *) "
    5.56 +    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
    5.57 +*)
    5.58 +
    5.59 +fun apply_on_subgoal _ 1 = "by "
    5.60 +  | apply_on_subgoal 1 _ = "apply "
    5.61 +  | apply_on_subgoal i n =
    5.62 +    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    5.63 +
    5.64 +fun using_labels [] = ""
    5.65 +  | using_labels ls =
    5.66 +    "using " ^ space_implode " " (map string_of_label ls) ^ " "
    5.67 +
    5.68 +fun command_call name [] =
    5.69 +    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
    5.70 +  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    5.71 +
    5.72 +fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
    5.73 +  (* unusing_chained_facts used_chaineds num_chained ^ *)
    5.74 +  using_labels ls ^ apply_on_subgoal i n ^
    5.75 +  command_call (string_of_reconstructor reconstr) ss
    5.76 +
    5.77 +fun try_command_line banner time command =
    5.78 +  banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
    5.79 +
    5.80 +fun minimize_line _ [] = ""
    5.81 +  | minimize_line minimize_command ss =
    5.82 +    case minimize_command ss of
    5.83 +      "" => ""
    5.84 +    | command =>
    5.85 +      "\nTo minimize: " ^ Active.sendback_markup command ^ "."
    5.86 +
    5.87 +fun split_used_facts facts =
    5.88 +  facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
    5.89 +        |> pairself (sort_distinct (string_ord o pairself fst))
    5.90 +
    5.91 +fun one_line_proof_text num_chained
    5.92 +        (preplay, banner, used_facts, minimize_command, subgoal,
    5.93 +         subgoal_count) =
    5.94 +  let
    5.95 +    val (chained, extra) = split_used_facts used_facts
    5.96 +    val (failed, reconstr, ext_time) =
    5.97 +      case preplay of
    5.98 +        Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
    5.99 +      | Trust_Playable (reconstr, time) =>
   5.100 +        (false, reconstr,
   5.101 +         case time of
   5.102 +           NONE => NONE
   5.103 +         | SOME time =>
   5.104 +           if time = Time.zeroTime then NONE else SOME (true, time))
   5.105 +      | Failed_to_Play reconstr => (true, reconstr, NONE)
   5.106 +    val try_line =
   5.107 +      ([], map fst extra)
   5.108 +      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
   5.109 +                               num_chained
   5.110 +      |> (if failed then
   5.111 +            enclose "One-line proof reconstruction failed: "
   5.112 +                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
   5.113 +                     \solve this.)"
   5.114 +          else
   5.115 +            try_command_line banner ext_time)
   5.116 +  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
   5.117 +
   5.118 +
   5.119 +
   5.120 +
   5.121 +(** detailed Isar proofs **)
   5.122 +
   5.123 +val indent_size = 2
   5.124 +
   5.125 +fun string_of_proof ctxt type_enc lam_trans i n proof =
   5.126 +  let
   5.127 +    val ctxt =
   5.128 +      (* make sure type constraint are actually printed *)
   5.129 +      ctxt |> Config.put show_markup false
   5.130 +      (* make sure only type constraints inserted by sh_annotate are printed *)
   5.131 +           |> Config.put Printer.show_type_emphasis false
   5.132 +           |> Config.put show_types false
   5.133 +           |> Config.put show_sorts false
   5.134 +           |> Config.put show_consts false
   5.135 +    val register_fixes = map Free #> fold Variable.auto_fixes
   5.136 +    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
   5.137 +    fun of_indent ind = replicate_string (ind * indent_size) " "
   5.138 +    fun of_moreover ind = of_indent ind ^ "moreover\n"
   5.139 +    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
   5.140 +    fun of_obtain qs nr =
   5.141 +      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   5.142 +         "ultimately "
   5.143 +       else if nr=1 orelse member (op =) qs Then then
   5.144 +         "then "
   5.145 +       else
   5.146 +         "") ^ "obtain"
   5.147 +    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
   5.148 +    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
   5.149 +    fun of_prove qs nr =
   5.150 +      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   5.151 +        "ultimately " ^ of_show_have qs
   5.152 +      else if nr=1 orelse member (op =) qs Then then
   5.153 +        of_thus_hence qs
   5.154 +      else
   5.155 +        of_show_have qs
   5.156 +    fun add_term term (s, ctxt) =
   5.157 +      (s ^ (term
   5.158 +            |> singleton (Syntax.uncheck_terms ctxt)
   5.159 +            |> annotate_types ctxt
   5.160 +            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
   5.161 +            |> simplify_spaces
   5.162 +            |> maybe_quote),
   5.163 +       ctxt |> Variable.auto_fixes term)
   5.164 +    val reconstr = Metis (type_enc, lam_trans)
   5.165 +    fun of_metis ind options (ls, ss) =
   5.166 +      "\n" ^ of_indent (ind + 1) ^ options ^
   5.167 +      reconstructor_command reconstr 1 1 [] 0
   5.168 +          (ls |> sort_distinct (prod_ord string_ord int_ord),
   5.169 +           ss |> sort_distinct string_ord)
   5.170 +    fun of_free (s, T) =
   5.171 +      maybe_quote s ^ " :: " ^
   5.172 +      maybe_quote (simplify_spaces (with_vanilla_print_mode
   5.173 +        (Syntax.string_of_typ ctxt) T))
   5.174 +    fun add_frees xs (s, ctxt) =
   5.175 +      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
   5.176 +    fun add_fix _ [] = I
   5.177 +      | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
   5.178 +                        #> add_frees xs
   5.179 +                        #> add_suffix "\n"
   5.180 +    fun add_assm ind (l, t) =
   5.181 +      add_suffix (of_indent ind ^ "assume " ^ of_label l)
   5.182 +      #> add_term t
   5.183 +      #> add_suffix "\n"
   5.184 +    fun add_assms ind assms = fold (add_assm ind) assms
   5.185 +    fun add_step_post ind l t facts options =
   5.186 +      add_suffix (of_label l)
   5.187 +      #> add_term t
   5.188 +      #> add_suffix (of_metis ind options facts ^ "\n")
   5.189 +    fun of_subproof ind ctxt proof =
   5.190 +      let
   5.191 +        val ind = ind + 1
   5.192 +        val s = of_proof ind ctxt proof
   5.193 +        val prefix = "{ "
   5.194 +        val suffix = " }"
   5.195 +      in
   5.196 +        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   5.197 +        String.extract (s, ind * indent_size,
   5.198 +                        SOME (size s - ind * indent_size - 1)) ^
   5.199 +        suffix ^ "\n"
   5.200 +      end
   5.201 +    and of_subproofs _ _ _ [] = ""
   5.202 +      | of_subproofs ind ctxt qs subproofs =
   5.203 +        (if member (op =) qs Then then of_moreover ind else "") ^
   5.204 +        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
   5.205 +    and add_step_pre ind qs subproofs (s, ctxt) =
   5.206 +      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
   5.207 +    and add_step ind (Let (t1, t2)) =
   5.208 +        add_suffix (of_indent ind ^ "let ")
   5.209 +        #> add_term t1
   5.210 +        #> add_suffix " = "
   5.211 +        #> add_term t2
   5.212 +        #> add_suffix "\n"
   5.213 +      | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) =
   5.214 +        (case xs of
   5.215 +          [] => (* have *)
   5.216 +            add_step_pre ind qs subproofs
   5.217 +            #> add_suffix (of_prove qs (length subproofs) ^ " ")
   5.218 +            #> add_step_post ind l t facts ""
   5.219 +        | _ => (* obtain *)
   5.220 +            add_step_pre ind qs subproofs
   5.221 +            #> add_suffix (of_obtain qs (length subproofs) ^ " ")
   5.222 +            #> add_frees xs
   5.223 +            #> add_suffix " where "
   5.224 +            (* The new skolemizer puts the arguments in the same order as the
   5.225 +               ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
   5.226 +               regarding Vampire). *)
   5.227 +            #> add_step_post ind l t facts
   5.228 +                 (if exists (fn (_, T) => length (binder_types T) > 1) xs then
   5.229 +                    "using [[metis_new_skolem]] "
   5.230 +                  else
   5.231 +                    ""))
   5.232 +    and add_steps ind = fold (add_step ind)
   5.233 +    and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
   5.234 +      ("", ctxt)
   5.235 +      |> add_fix ind xs
   5.236 +      |> add_assms ind assms
   5.237 +      |> add_steps ind steps
   5.238 +      |> fst
   5.239 +  in
   5.240 +    (* One-step proofs are pointless; better use the Metis one-liner
   5.241 +       directly. *)
   5.242 +    case proof of
   5.243 +      Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => ""
   5.244 +    | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   5.245 +            of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   5.246 +            of_indent 0 ^ (if n <> 1 then "next" else "qed")
   5.247 +  end
   5.248 +
   5.249 +  end
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 08 14:24:36 2013 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jul 09 18:44:59 2013 +0200
     6.3 @@ -12,9 +12,9 @@
     6.4    type stature = ATP_Problem_Generate.stature
     6.5    type type_enc = ATP_Problem_Generate.type_enc
     6.6    type fact = Sledgehammer_Fact.fact
     6.7 -  type reconstructor = Sledgehammer_Reconstruct.reconstructor
     6.8 -  type play = Sledgehammer_Reconstruct.play
     6.9 -  type minimize_command = Sledgehammer_Reconstruct.minimize_command
    6.10 +  type reconstructor = Sledgehammer_Reconstructor.reconstructor
    6.11 +  type play = Sledgehammer_Reconstructor.play
    6.12 +  type minimize_command = Sledgehammer_Reconstructor.minimize_command
    6.13  
    6.14    datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    6.15  
    6.16 @@ -150,6 +150,8 @@
    6.17  open Metis_Tactic
    6.18  open Sledgehammer_Util
    6.19  open Sledgehammer_Fact
    6.20 +open Sledgehammer_Reconstructor
    6.21 +open Sledgehammer_Print
    6.22  open Sledgehammer_Reconstruct
    6.23  
    6.24  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Jul 08 14:24:36 2013 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jul 09 18:44:59 2013 +0200
     7.3 @@ -9,26 +9,13 @@
     7.4  sig
     7.5    type 'a proof = 'a ATP_Proof.proof
     7.6    type stature = ATP_Problem_Generate.stature
     7.7 -
     7.8 -  datatype reconstructor =
     7.9 -    Metis of string * string |
    7.10 -    SMT
    7.11 +  type one_line_params = Sledgehammer_Print.one_line_params
    7.12  
    7.13 -  datatype play =
    7.14 -    Played of reconstructor * Time.time |
    7.15 -    Trust_Playable of reconstructor * Time.time option |
    7.16 -    Failed_to_Play of reconstructor
    7.17 -
    7.18 -  type minimize_command = string list -> string
    7.19 -  type one_line_params =
    7.20 -    play * string * (string * stature) list * minimize_command * int * int
    7.21    type isar_params =
    7.22      bool * bool * Time.time option * bool * real * string Symtab.table
    7.23      * (string * stature) list vector * (string * term) list * int Symtab.table
    7.24      * string proof * thm
    7.25  
    7.26 -  val smtN : string
    7.27 -  val string_of_reconstructor : reconstructor -> string
    7.28    val lam_trans_of_atp_proof : string proof -> string -> string
    7.29    val is_typed_helper_used_in_atp_proof : string proof -> bool
    7.30    val used_facts_in_atp_proof :
    7.31 @@ -37,7 +24,6 @@
    7.32    val used_facts_in_unsound_atp_proof :
    7.33      Proof.context -> (string * stature) list vector -> 'a proof ->
    7.34      string list option
    7.35 -  val one_line_proof_text : int -> one_line_params -> string
    7.36    val isar_proof_text :
    7.37      Proof.context -> bool option -> isar_params -> one_line_params -> string
    7.38    val proof_text :
    7.39 @@ -54,8 +40,10 @@
    7.40  open ATP_Problem_Generate
    7.41  open ATP_Proof_Reconstruct
    7.42  open Sledgehammer_Util
    7.43 +open Sledgehammer_Reconstructor
    7.44  open Sledgehammer_Proof
    7.45  open Sledgehammer_Annotate
    7.46 +open Sledgehammer_Print
    7.47  open Sledgehammer_Compress
    7.48  
    7.49  structure String_Redirect = ATP_Proof_Redirect(
    7.50 @@ -65,25 +53,6 @@
    7.51  
    7.52  open String_Redirect
    7.53  
    7.54 -
    7.55 -(** reconstructors **)
    7.56 -
    7.57 -datatype reconstructor =
    7.58 -  Metis of string * string |
    7.59 -  SMT
    7.60 -
    7.61 -datatype play =
    7.62 -  Played of reconstructor * Time.time |
    7.63 -  Trust_Playable of reconstructor * Time.time option |
    7.64 -  Failed_to_Play of reconstructor
    7.65 -
    7.66 -val smtN = "smt"
    7.67 -
    7.68 -fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
    7.69 -    metis_call type_enc lam_trans
    7.70 -  | string_of_reconstructor SMT = smtN
    7.71 -
    7.72 -
    7.73  (** fact extraction from ATP proofs **)
    7.74  
    7.75  fun find_first_in_list_vector vec key =
    7.76 @@ -189,83 +158,6 @@
    7.77      end
    7.78  
    7.79  
    7.80 -(** one-liner reconstructor proofs **)
    7.81 -
    7.82 -fun show_time NONE = ""
    7.83 -  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
    7.84 -
    7.85 -(* FIXME: Various bugs, esp. with "unfolding"
    7.86 -fun unusing_chained_facts _ 0 = ""
    7.87 -  | unusing_chained_facts used_chaineds num_chained =
    7.88 -    if length used_chaineds = num_chained then ""
    7.89 -    else if null used_chaineds then "(* using no facts *) "
    7.90 -    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
    7.91 -*)
    7.92 -
    7.93 -fun apply_on_subgoal _ 1 = "by "
    7.94 -  | apply_on_subgoal 1 _ = "apply "
    7.95 -  | apply_on_subgoal i n =
    7.96 -    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    7.97 -
    7.98 -fun using_labels [] = ""
    7.99 -  | using_labels ls =
   7.100 -    "using " ^ space_implode " " (map string_of_label ls) ^ " "
   7.101 -
   7.102 -fun command_call name [] =
   7.103 -    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
   7.104 -  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   7.105 -
   7.106 -fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
   7.107 -  (* unusing_chained_facts used_chaineds num_chained ^ *)
   7.108 -  using_labels ls ^ apply_on_subgoal i n ^
   7.109 -  command_call (string_of_reconstructor reconstr) ss
   7.110 -
   7.111 -fun try_command_line banner time command =
   7.112 -  banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
   7.113 -
   7.114 -fun minimize_line _ [] = ""
   7.115 -  | minimize_line minimize_command ss =
   7.116 -    case minimize_command ss of
   7.117 -      "" => ""
   7.118 -    | command =>
   7.119 -      "\nTo minimize: " ^ Active.sendback_markup command ^ "."
   7.120 -
   7.121 -fun split_used_facts facts =
   7.122 -  facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
   7.123 -        |> pairself (sort_distinct (string_ord o pairself fst))
   7.124 -
   7.125 -type minimize_command = string list -> string
   7.126 -type one_line_params =
   7.127 -  play * string * (string * stature) list * minimize_command * int * int
   7.128 -
   7.129 -fun one_line_proof_text num_chained
   7.130 -        (preplay, banner, used_facts, minimize_command, subgoal,
   7.131 -         subgoal_count) =
   7.132 -  let
   7.133 -    val (chained, extra) = split_used_facts used_facts
   7.134 -    val (failed, reconstr, ext_time) =
   7.135 -      case preplay of
   7.136 -        Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
   7.137 -      | Trust_Playable (reconstr, time) =>
   7.138 -        (false, reconstr,
   7.139 -         case time of
   7.140 -           NONE => NONE
   7.141 -         | SOME time =>
   7.142 -           if time = Time.zeroTime then NONE else SOME (true, time))
   7.143 -      | Failed_to_Play reconstr => (true, reconstr, NONE)
   7.144 -    val try_line =
   7.145 -      ([], map fst extra)
   7.146 -      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
   7.147 -                               num_chained
   7.148 -      |> (if failed then
   7.149 -            enclose "One-line proof reconstruction failed: "
   7.150 -                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
   7.151 -                     \solve this.)"
   7.152 -          else
   7.153 -            try_command_line banner ext_time)
   7.154 -  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
   7.155 -
   7.156 -
   7.157  (** Isar proof construction and manipulation **)
   7.158  
   7.159  val assume_prefix = "a"
   7.160 @@ -429,131 +321,6 @@
   7.161     else
   7.162       map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   7.163  
   7.164 -val indent_size = 2
   7.165 -
   7.166 -fun string_of_proof ctxt type_enc lam_trans i n proof =
   7.167 -  let
   7.168 -    val ctxt =
   7.169 -      (* make sure type constraint are actually printed *)
   7.170 -      ctxt |> Config.put show_markup false
   7.171 -      (* make sure only type constraints inserted by sh_annotate are printed *)
   7.172 -           |> Config.put Printer.show_type_emphasis false
   7.173 -           |> Config.put show_types false
   7.174 -           |> Config.put show_sorts false
   7.175 -           |> Config.put show_consts false
   7.176 -    val register_fixes = map Free #> fold Variable.auto_fixes
   7.177 -    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
   7.178 -    fun of_indent ind = replicate_string (ind * indent_size) " "
   7.179 -    fun of_moreover ind = of_indent ind ^ "moreover\n"
   7.180 -    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
   7.181 -    fun of_obtain qs nr =
   7.182 -      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   7.183 -         "ultimately "
   7.184 -       else if nr=1 orelse member (op =) qs Then then
   7.185 -         "then "
   7.186 -       else
   7.187 -         "") ^ "obtain"
   7.188 -    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
   7.189 -    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
   7.190 -    fun of_prove qs nr =
   7.191 -      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   7.192 -        "ultimately " ^ of_show_have qs
   7.193 -      else if nr=1 orelse member (op =) qs Then then
   7.194 -        of_thus_hence qs
   7.195 -      else
   7.196 -        of_show_have qs
   7.197 -    fun add_term term (s, ctxt) =
   7.198 -      (s ^ (term
   7.199 -            |> singleton (Syntax.uncheck_terms ctxt)
   7.200 -            |> annotate_types ctxt
   7.201 -            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
   7.202 -            |> simplify_spaces
   7.203 -            |> maybe_quote),
   7.204 -       ctxt |> Variable.auto_fixes term)
   7.205 -    val reconstr = Metis (type_enc, lam_trans)
   7.206 -    fun of_metis ind options (ls, ss) =
   7.207 -      "\n" ^ of_indent (ind + 1) ^ options ^
   7.208 -      reconstructor_command reconstr 1 1 [] 0
   7.209 -          (ls |> sort_distinct (prod_ord string_ord int_ord),
   7.210 -           ss |> sort_distinct string_ord)
   7.211 -    fun of_free (s, T) =
   7.212 -      maybe_quote s ^ " :: " ^
   7.213 -      maybe_quote (simplify_spaces (with_vanilla_print_mode
   7.214 -        (Syntax.string_of_typ ctxt) T))
   7.215 -    fun add_frees xs (s, ctxt) =
   7.216 -      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
   7.217 -    fun add_fix _ [] = I
   7.218 -      | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
   7.219 -                        #> add_frees xs
   7.220 -                        #> add_suffix "\n"
   7.221 -    fun add_assm ind (l, t) =
   7.222 -      add_suffix (of_indent ind ^ "assume " ^ of_label l)
   7.223 -      #> add_term t
   7.224 -      #> add_suffix "\n"
   7.225 -    fun add_assms ind assms = fold (add_assm ind) assms
   7.226 -    fun add_step_post ind l t facts options =
   7.227 -      add_suffix (of_label l)
   7.228 -      #> add_term t
   7.229 -      #> add_suffix (of_metis ind options facts ^ "\n")
   7.230 -    fun of_subproof ind ctxt proof =
   7.231 -      let
   7.232 -        val ind = ind + 1
   7.233 -        val s = of_proof ind ctxt proof
   7.234 -        val prefix = "{ "
   7.235 -        val suffix = " }"
   7.236 -      in
   7.237 -        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   7.238 -        String.extract (s, ind * indent_size,
   7.239 -                        SOME (size s - ind * indent_size - 1)) ^
   7.240 -        suffix ^ "\n"
   7.241 -      end
   7.242 -    and of_subproofs _ _ _ [] = ""
   7.243 -      | of_subproofs ind ctxt qs subproofs =
   7.244 -        (if member (op =) qs Then then of_moreover ind else "") ^
   7.245 -        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
   7.246 -    and add_step_pre ind qs subproofs (s, ctxt) =
   7.247 -      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
   7.248 -    and add_step ind (Let (t1, t2)) =
   7.249 -        add_suffix (of_indent ind ^ "let ")
   7.250 -        #> add_term t1
   7.251 -        #> add_suffix " = "
   7.252 -        #> add_term t2
   7.253 -        #> add_suffix "\n"
   7.254 -      | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) =
   7.255 -        (case xs of
   7.256 -          [] => (* have *)
   7.257 -            add_step_pre ind qs subproofs
   7.258 -            #> add_suffix (of_prove qs (length subproofs) ^ " ")
   7.259 -            #> add_step_post ind l t facts ""
   7.260 -        | _ => (* obtain *)
   7.261 -            add_step_pre ind qs subproofs
   7.262 -            #> add_suffix (of_obtain qs (length subproofs) ^ " ")
   7.263 -            #> add_frees xs
   7.264 -            #> add_suffix " where "
   7.265 -            (* The new skolemizer puts the arguments in the same order as the
   7.266 -               ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
   7.267 -               regarding Vampire). *)
   7.268 -            #> add_step_post ind l t facts
   7.269 -                 (if exists (fn (_, T) => length (binder_types T) > 1) xs then
   7.270 -                    "using [[metis_new_skolem]] "
   7.271 -                  else
   7.272 -                    ""))
   7.273 -    and add_steps ind = fold (add_step ind)
   7.274 -    and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
   7.275 -      ("", ctxt)
   7.276 -      |> add_fix ind xs
   7.277 -      |> add_assms ind assms
   7.278 -      |> add_steps ind steps
   7.279 -      |> fst
   7.280 -  in
   7.281 -    (* One-step proofs are pointless; better use the Metis one-liner
   7.282 -       directly. *)
   7.283 -    case proof of
   7.284 -      Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => ""
   7.285 -    | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   7.286 -            of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   7.287 -            of_indent 0 ^ (if n <> 1 then "next" else "qed")
   7.288 -  end
   7.289  
   7.290  val add_labels_of_proof =
   7.291    steps_of_proof #> fold_isar_steps
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Tue Jul 09 18:44:59 2013 +0200
     8.3 @@ -0,0 +1,52 @@
     8.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     8.5 +    Author:     Jasmin Blanchette, TU Muenchen
     8.6 +    Author:     Steffen Juilf Smolka, TU Muenchen
     8.7 +
     8.8 +Reconstructors.
     8.9 +*)
    8.10 +
    8.11 +signature SLEDGEHAMMER_RECONSTRUCTOR =
    8.12 +sig
    8.13 +
    8.14 +  type stature = ATP_Problem_Generate.stature
    8.15 +
    8.16 +  datatype reconstructor =
    8.17 +    Metis of string * string |
    8.18 +    SMT
    8.19 +
    8.20 +  datatype play =
    8.21 +    Played of reconstructor * Time.time |
    8.22 +    Trust_Playable of reconstructor * Time.time option |
    8.23 +    Failed_to_Play of reconstructor
    8.24 +
    8.25 +  type minimize_command = string list -> string
    8.26 +
    8.27 +  type one_line_params =
    8.28 +    play * string * (string * stature) list * minimize_command * int * int
    8.29 +
    8.30 +  val smtN : string
    8.31 +
    8.32 +end
    8.33 +
    8.34 +structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
    8.35 +struct
    8.36 +
    8.37 +open ATP_Problem_Generate
    8.38 +
    8.39 +datatype reconstructor =
    8.40 +  Metis of string * string |
    8.41 +  SMT
    8.42 +
    8.43 +datatype play =
    8.44 +  Played of reconstructor * Time.time |
    8.45 +  Trust_Playable of reconstructor * Time.time option |
    8.46 +  Failed_to_Play of reconstructor
    8.47 +
    8.48 +type minimize_command = string list -> string
    8.49 +
    8.50 +type one_line_params =
    8.51 +  play * string * (string * stature) list * minimize_command * int * int
    8.52 +
    8.53 +val smtN = "smt"
    8.54 +
    8.55 +end
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jul 08 14:24:36 2013 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Jul 09 18:44:59 2013 +0200
     9.3 @@ -10,7 +10,7 @@
     9.4  sig
     9.5    type fact = Sledgehammer_Fact.fact
     9.6    type fact_override = Sledgehammer_Fact.fact_override
     9.7 -  type minimize_command = Sledgehammer_Reconstruct.minimize_command
     9.8 +  type minimize_command = Sledgehammer_Reconstructor.minimize_command
     9.9    type mode = Sledgehammer_Provers.mode
    9.10    type params = Sledgehammer_Provers.params
    9.11