added a 'trace' option
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 55222a4ef6eb1fc20
parent 55221 ee90eebb8b73
child 55223 3c593bad6b31
added a 'trace' option
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -13,6 +13,8 @@
     1.4    type stature = ATP_Problem_Generate.stature
     1.5    type one_line_params = Sledgehammer_Reconstructor.one_line_params
     1.6  
     1.7 +  val trace : bool Config.T
     1.8 +
     1.9    type isar_params =
    1.10      bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
    1.11  
    1.12 @@ -42,6 +44,8 @@
    1.13  
    1.14  open String_Redirect
    1.15  
    1.16 +val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
    1.17 +
    1.18  val e_skolemize_rules = ["skolemize", "shift_quantors"]
    1.19  val spass_pirate_datatype_rule = "DT"
    1.20  val vampire_skolemisation_rule = "skolemisation"
    1.21 @@ -262,7 +266,7 @@
    1.22          val string_of_isar_proof =
    1.23            string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
    1.24  
    1.25 -        val trace = false
    1.26 +        val trace = Config.get ctxt trace
    1.27  
    1.28          val isar_proof =
    1.29            refute_graph
    1.30 @@ -273,13 +277,17 @@
    1.31            |> postprocess_isar_proof_remove_unreferenced_steps I
    1.32            |> relabel_isar_proof_canonically
    1.33  
    1.34 -        val preplay_data as {overall_preplay_outcome, ...} =
    1.35 +        val preplay_data as {string_of_preplay_outcome, overall_preplay_outcome, ...} =
    1.36            preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.37              preplay_timeout isar_proof
    1.38  
    1.39 +        fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ string_of_preplay_outcome l
    1.40 +        fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
    1.41 +
    1.42          fun trace_isar_proof label proof =
    1.43            if trace then
    1.44 -            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof true proof ^ "\n")
    1.45 +            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
    1.46 +              "\n")
    1.47            else
    1.48              ()
    1.49  
    1.50 @@ -299,7 +307,7 @@
    1.51            ||> kill_useless_labels_in_isar_proof
    1.52            ||> relabel_isar_proof_finally
    1.53        in
    1.54 -        (case string_of_isar_proof false isar_proof of
    1.55 +        (case string_of_isar_proof (K (K "")) isar_proof of
    1.56            "" =>
    1.57            if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
    1.58            else ""
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     2.3 @@ -30,6 +30,8 @@
     2.4    val label_ord : label * label -> order
     2.5    val string_of_label : label -> string
     2.6  
     2.7 +  val string_of_proof_method : proof_method -> string
     2.8 +
     2.9    val steps_of_proof : isar_proof -> isar_step list
    2.10  
    2.11    val label_of_step : isar_step -> label option
    2.12 @@ -48,8 +50,8 @@
    2.13    val relabel_isar_proof_canonically : isar_proof -> isar_proof
    2.14    val relabel_isar_proof_finally : isar_proof -> isar_proof
    2.15  
    2.16 -  val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> bool ->
    2.17 -    isar_proof -> string
    2.18 +  val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
    2.19 +    (label -> proof_method list list -> string) -> isar_proof -> string
    2.20  end;
    2.21  
    2.22  structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    2.23 @@ -86,7 +88,7 @@
    2.24  
    2.25  fun string_of_label (s, num) = s ^ string_of_int num
    2.26  
    2.27 -fun string_of_method meth =
    2.28 +fun string_of_proof_method meth =
    2.29    (case meth of
    2.30      Metis_Method => "metis"
    2.31    | Simp_Method => "simp"
    2.32 @@ -242,7 +244,7 @@
    2.33  
    2.34  val indent_size = 2
    2.35  
    2.36 -fun string_of_isar_proof ctxt type_enc lam_trans i n all_methods proof =
    2.37 +fun string_of_isar_proof ctxt type_enc lam_trans i n comment_of proof =
    2.38    let
    2.39      (* Make sure only type constraints inserted by the type annotation code are printed. *)
    2.40      val ctxt =
    2.41 @@ -295,9 +297,7 @@
    2.42      fun of_method ls ss Metis_Method =
    2.43          using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
    2.44        | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
    2.45 -      | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_method meth
    2.46 -
    2.47 -    val str_of_methodss = map (map string_of_method) #> map commas #> space_implode "; "
    2.48 +      | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_proof_method meth
    2.49  
    2.50      fun of_free (s, T) =
    2.51        maybe_quote s ^ " :: " ^
    2.52 @@ -340,7 +340,7 @@
    2.53          add_str (of_indent ind ^ "let ")
    2.54          #> add_term t1 #> add_str " = " #> add_term t2
    2.55          #> add_str "\n"
    2.56 -      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), (meth :: meths) :: methss))) =
    2.57 +      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), methss as (meth :: _) :: _))) =
    2.58          add_step_pre ind qs subproofs
    2.59          #> (case xs of
    2.60               [] => add_str (of_have qs (length subproofs) ^ " ")
    2.61 @@ -350,8 +350,9 @@
    2.62          #> add_term t
    2.63          #> add_str (" " ^
    2.64               of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
    2.65 -             (if all_methods then " (* " ^ str_of_methodss (meths :: methss) ^ " *)" else "") ^
    2.66 -             "\n")
    2.67 +             (case comment_of l methss of
    2.68 +               "" => ""
    2.69 +             | comment => " (* " ^ comment ^ " *)") ^ "\n")
    2.70      and add_steps ind = fold (add_step ind)
    2.71      and of_proof ind ctxt (Proof (xs, assms, steps)) =
    2.72        ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst