skeleton for Simplifier trace by Lars Hupel;
authorwenzelm
Thu Dec 12 21:28:13 2013 +0100 (2013-12-12)
changeset 54730de2d99b459b3
parent 54729 c5cd7a58cf2d
child 54731 384ac33802b0
skeleton for Simplifier trace by Lars Hupel;
src/Pure/Pure.thy
src/Pure/Tools/simplifier_trace.ML
src/Pure/Tools/simplifier_trace.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Pure.thy	Thu Dec 12 21:14:33 2013 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Dec 12 21:28:13 2013 +0100
     1.3 @@ -107,6 +107,7 @@
     1.4  ML_file "Tools/find_theorems.ML"
     1.5  ML_file "Tools/find_consts.ML"
     1.6  ML_file "Tools/proof_general_pure.ML"
     1.7 +ML_file "Tools/simplifier_trace.ML"
     1.8  
     1.9  
    1.10  section {* Further content for the Pure theory *}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Thu Dec 12 21:28:13 2013 +0100
     2.3 @@ -0,0 +1,38 @@
     2.4 +(*  Title:      Pure/Tools/simplifier_trace.ML
     2.5 +    Author:     Lars Hupel, TU Muenchen
     2.6 +
     2.7 +Interactive Simplifier trace.
     2.8 +*)
     2.9 +
    2.10 +signature SIMPLIFIER_TRACE =
    2.11 +sig
    2.12 +  val simp_trace_test: bool Config.T
    2.13 +end
    2.14 +
    2.15 +structure Simplifier_Trace: SIMPLIFIER_TRACE =
    2.16 +struct
    2.17 +
    2.18 +(* Simplifier trace operations *)
    2.19 +
    2.20 +val simp_trace_test =
    2.21 +  Attrib.setup_config_bool @{binding simp_trace_test} (K false)
    2.22 +
    2.23 +val _ = Theory.setup
    2.24 +  (Simplifier.map_theory_simpset (Simplifier.set_trace_ops
    2.25 +   {trace_invoke = fn {depth, term} => fn ctxt =>
    2.26 +      (if Config.get ctxt simp_trace_test then
    2.27 +        tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
    2.28 +          Syntax.string_of_term ctxt term)
    2.29 +       else (); ctxt),
    2.30 +    trace_apply = fn args => fn ctxt => fn cont =>
    2.31 +      (if Config.get ctxt simp_trace_test then
    2.32 +        tracing ("Simplifier " ^ @{make_string} args)
    2.33 +       else (); cont ctxt)}))
    2.34 +
    2.35 +
    2.36 +(* PIDE protocol *)
    2.37 +
    2.38 +val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
    2.39 +
    2.40 +end
    2.41 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Thu Dec 12 21:28:13 2013 +0100
     3.3 @@ -0,0 +1,18 @@
     3.4 +/*  Title:      Pure/Tools/simplifier_trace.scala
     3.5 +    Author:     Lars Hupel, TU Muenchen
     3.6 +
     3.7 +Interactive Simplifier trace.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Simplifier_Trace
    3.14 +{
    3.15 +  /* PIDE protocol */
    3.16 +
    3.17 +  class Handler extends Session.Protocol_Handler
    3.18 +  {
    3.19 +    val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean]
    3.20 +  }
    3.21 +}
     4.1 --- a/src/Pure/build-jars	Thu Dec 12 21:14:33 2013 +0100
     4.2 +++ b/src/Pure/build-jars	Thu Dec 12 21:28:13 2013 +0100
     4.3 @@ -78,6 +78,7 @@
     4.4    Tools/keywords.scala
     4.5    Tools/main.scala
     4.6    Tools/ml_statistics.scala
     4.7 +  Tools/simplifier_trace.scala
     4.8    Tools/sledgehammer_params.scala
     4.9    Tools/task_statistics.scala
    4.10    library.scala