better tracing + syntactically correct 'metis' calls
authorblanchet
Fri Jan 31 16:41:54 2014 +0100 (2014-01-31)
changeset 5521448a347b40629
parent 55213 dcb36a2540bc
child 55215 b6c926e67350
child 55224 197c36bb30ad
better tracing + syntactically correct 'metis' calls
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 16:26:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:41:54 2014 +0100
     1.3 @@ -342,39 +342,49 @@
     1.4          and isar_proof outer fix assms lems infs =
     1.5            Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
     1.6  
     1.7 -        val (preplay_data as {overall_preplay_outcome, ...}, isar_proof) =
     1.8 +        val string_of_isar_proof =
     1.9 +          string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
    1.10 +
    1.11 +        val trace = false
    1.12 +
    1.13 +        val isar_proof =
    1.14            refute_graph
    1.15 -(*
    1.16 -          |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
    1.17 -*)
    1.18 +          |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
    1.19            |> redirect_graph axioms tainted bot
    1.20 -(*
    1.21 -          |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
    1.22 -*)
    1.23 +          |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
    1.24            |> isar_proof true params assms lems
    1.25            |> postprocess_isar_proof_remove_unreferenced_steps I
    1.26            |> relabel_isar_proof_canonically
    1.27 -          |> `(preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.28 -                 preplay_timeout)
    1.29 +
    1.30 +        val preplay_data as {overall_preplay_outcome, ...} =
    1.31 +          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.32 +            preplay_timeout isar_proof
    1.33 +
    1.34 +        fun trace_isar_proof label proof =
    1.35 +          if trace then
    1.36 +            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof proof ^ "\n")
    1.37 +          else
    1.38 +            ()
    1.39  
    1.40          val (play_outcome, isar_proof) =
    1.41            isar_proof
    1.42 +          |> tap (trace_isar_proof "Original")
    1.43            |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
    1.44                 preplay_data
    1.45 +          |> tap (trace_isar_proof "Compressed")
    1.46            |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
    1.47 +          |> tap (trace_isar_proof "Tried0")
    1.48            |> postprocess_isar_proof_remove_unreferenced_steps
    1.49                 (try0_isar ? minimize_isar_step_dependencies preplay_data)
    1.50 +          |> tap (trace_isar_proof "Minimized")
    1.51            |> `overall_preplay_outcome
    1.52            ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
    1.53 -
    1.54 -        val isar_text =
    1.55 -          string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
    1.56        in
    1.57 -        (case isar_text of
    1.58 +        (case string_of_isar_proof isar_proof of
    1.59            "" =>
    1.60            if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
    1.61            else ""
    1.62 -        | _ =>
    1.63 +        | isar_text =>
    1.64            let
    1.65              val msg =
    1.66                (if verbose then
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:26:43 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:41:54 2014 +0100
     2.3 @@ -204,7 +204,7 @@
     2.4        | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
     2.5  
     2.6      val using_facts = with_facts "" (enclose "using " " ")
     2.7 -    fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("by (" ^ meth) ")") ls ss
     2.8 +    fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("(" ^ meth ^ " ") ")") ls ss
     2.9  
    2.10      (* Local facts are always passed via "using", which affects "meson" and "metis". This is
    2.11         arguably stylistically superior, because it emphasises the structure of the proof. It is also