more informative trace
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 55218ed495a5088c6
parent 55217 70035950e19b
child 55219 6fe9fd75f9d7
more informative trace
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 @@ -362,7 +362,7 @@
     1.4  
     1.5          fun trace_isar_proof label proof =
     1.6            if trace then
     1.7 -            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof proof ^ "\n")
     1.8 +            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof true proof ^ "\n")
     1.9            else
    1.10              ()
    1.11  
    1.12 @@ -380,7 +380,7 @@
    1.13            |> `overall_preplay_outcome
    1.14            ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
    1.15        in
    1.16 -        (case string_of_isar_proof isar_proof of
    1.17 +        (case string_of_isar_proof false isar_proof of
    1.18            "" =>
    1.19            if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
    1.20            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 @@ -13,15 +13,16 @@
     2.4  
     2.5    datatype isar_qualifier = Show | Then
     2.6  
     2.7 +  datatype proof_method =
     2.8 +    Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
     2.9 +    Arith_Method | Blast_Method | Meson_Method
    2.10 +
    2.11    datatype isar_proof =
    2.12      Proof of (string * typ) list * (label * term) list * isar_step list
    2.13    and isar_step =
    2.14      Let of term * term |
    2.15      Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
    2.16        (facts * proof_method list list)
    2.17 -  and proof_method =
    2.18 -    Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
    2.19 -    Arith_Method | Blast_Method | Meson_Method
    2.20  
    2.21    val no_label : label
    2.22    val no_facts : facts
    2.23 @@ -43,7 +44,8 @@
    2.24    val canonical_label_ord : (label * label) -> order
    2.25    val relabel_isar_proof_canonically : isar_proof -> isar_proof
    2.26  
    2.27 -  val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
    2.28 +  val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> bool ->
    2.29 +    isar_proof -> string
    2.30  end;
    2.31  
    2.32  structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    2.33 @@ -62,15 +64,16 @@
    2.34  
    2.35  datatype isar_qualifier = Show | Then
    2.36  
    2.37 +datatype proof_method =
    2.38 +  Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
    2.39 +  Arith_Method | Blast_Method | Meson_Method
    2.40 +
    2.41  datatype isar_proof =
    2.42    Proof of (string * typ) list * (label * term) list * isar_step list
    2.43  and isar_step =
    2.44    Let of term * term |
    2.45    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
    2.46      (facts * proof_method list list)
    2.47 -and proof_method =
    2.48 -  Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
    2.49 -  Arith_Method | Blast_Method | Meson_Method
    2.50  
    2.51  val no_label = ("", ~1)
    2.52  val no_facts = ([],[])
    2.53 @@ -79,6 +82,18 @@
    2.54  
    2.55  fun string_of_label (s, num) = s ^ string_of_int num
    2.56  
    2.57 +fun string_of_method meth =
    2.58 +  (case meth of
    2.59 +    Metis_Method => "metis"
    2.60 +  | Simp_Method => "simp"
    2.61 +  | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
    2.62 +  | Auto_Method => "auto"
    2.63 +  | Fastforce_Method => "fastforce"
    2.64 +  | Force_Method => "force"
    2.65 +  | Arith_Method => "arith"
    2.66 +  | Blast_Method => "blast"
    2.67 +  | Meson_Method => "meson")
    2.68 +
    2.69  fun steps_of_proof (Proof (_, _, steps)) = steps
    2.70  
    2.71  fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
    2.72 @@ -148,7 +163,7 @@
    2.73  
    2.74  val indent_size = 2
    2.75  
    2.76 -fun string_of_isar_proof ctxt type_enc lam_trans i n proof =
    2.77 +fun string_of_isar_proof ctxt type_enc lam_trans i n all_methods proof =
    2.78    let
    2.79      (* Make sure only type constraints inserted by the type annotation code are printed. *)
    2.80      val ctxt =
    2.81 @@ -188,18 +203,6 @@
    2.82              |> maybe_quote),
    2.83         ctxt |> Variable.auto_fixes term)
    2.84  
    2.85 -    fun by_method meth = "by " ^
    2.86 -      (case meth of
    2.87 -        Simp_Method => "simp"
    2.88 -      | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
    2.89 -      | Auto_Method => "auto"
    2.90 -      | Fastforce_Method => "fastforce"
    2.91 -      | Force_Method => "force"
    2.92 -      | Arith_Method => "arith"
    2.93 -      | Blast_Method => "blast"
    2.94 -      | Meson_Method => "meson"
    2.95 -      | _ => raise Fail "Sledgehammer_Isar_Print: by_method")
    2.96 -
    2.97      fun with_facts none _ [] [] = none
    2.98        | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
    2.99  
   2.100 @@ -213,7 +216,9 @@
   2.101      fun of_method ls ss Metis_Method =
   2.102          using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
   2.103        | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
   2.104 -      | of_method ls ss meth = using_facts ls ss ^ by_method meth
   2.105 +      | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_method meth
   2.106 +
   2.107 +    val str_of_methodss = map (map string_of_method) #> map commas #> space_implode "; "
   2.108  
   2.109      fun of_free (s, T) =
   2.110        maybe_quote s ^ " :: " ^
   2.111 @@ -256,7 +261,7 @@
   2.112          add_str (of_indent ind ^ "let ")
   2.113          #> add_term t1 #> add_str " = " #> add_term t2
   2.114          #> add_str "\n"
   2.115 -      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), (meth :: _) :: _))) =
   2.116 +      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), (meth :: meths) :: methss))) =
   2.117          add_step_pre ind qs subproofs
   2.118          #> (case xs of
   2.119               [] => add_str (of_have qs (length subproofs) ^ " ")
   2.120 @@ -265,7 +270,9 @@
   2.121          #> add_str (of_label l)
   2.122          #> add_term t
   2.123          #> add_str (" " ^
   2.124 -             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
   2.125 +             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
   2.126 +             (if all_methods then " (* " ^ str_of_methodss (meths :: methss) ^ " *)" else "") ^
   2.127 +             "\n")
   2.128      and add_steps ind = fold (add_step ind)
   2.129      and of_proof ind ctxt (Proof (xs, assms, steps)) =
   2.130        ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst