clarified "simp_trace_new" and corresponding isar-ref section;
authorwenzelm
Mon Jul 21 16:04:45 2014 +0200 (2014-07-21)
changeset 575918c095aef6769
parent 57590 06cb5375e189
child 57592 b73d74d0e428
clarified "simp_trace_new" and corresponding isar-ref section;
NEWS
src/Doc/Isar_Ref/Generic.thy
src/Pure/Tools/simplifier_trace.ML
     1.1 --- a/NEWS	Mon Jul 21 15:16:50 2014 +0200
     1.2 +++ b/NEWS	Mon Jul 21 16:04:45 2014 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  "Detach" a copy where this makes sense.
     1.5  
     1.6  * New Simplifier Trace panel provides an interactive view of the
     1.7 -simplification process, enabled by the "simplifier_trace" attribute
     1.8 +simplification process, enabled by the "simp_trace_new" attribute
     1.9  within the context.
    1.10  
    1.11  
     2.1 --- a/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 15:16:50 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 16:04:45 2014 +0200
     2.3 @@ -395,10 +395,12 @@
     2.4  subsection {* Simplification methods \label{sec:simp-meth} *}
     2.5  
     2.6  text {*
     2.7 -  \begin{matharray}{rcl}
     2.8 +  \begin{tabular}{rcll}
     2.9      @{method_def simp} & : & @{text method} \\
    2.10      @{method_def simp_all} & : & @{text method} \\
    2.11 -  \end{matharray}
    2.12 +    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
    2.13 +  \end{tabular}
    2.14 +  \medskip
    2.15  
    2.16    @{rail \<open>
    2.17      (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
    2.18 @@ -463,6 +465,9 @@
    2.19    The proof method fails if all subgoals remain unchanged after
    2.20    simplification.
    2.21  
    2.22 +  \item @{attribute simp_depth_limit} limits the number of recursive
    2.23 +  invocations of the Simplifier during conditional rewriting.
    2.24 +
    2.25    \end{description}
    2.26  
    2.27    By default the Simplifier methods above take local assumptions fully
    2.28 @@ -586,7 +591,7 @@
    2.29    apply simp
    2.30    oops
    2.31  
    2.32 -text {* See also \secref{sec:simp-config} for options to enable
    2.33 +text {* See also \secref{sec:simp-trace} for options to enable
    2.34    Simplifier trace mode, which often helps to diagnose problems with
    2.35    rewrite systems.
    2.36  *}
    2.37 @@ -859,25 +864,32 @@
    2.38    reorientation and mutual simplification fail to apply.  *}
    2.39  
    2.40  
    2.41 -subsection {* Configuration options \label{sec:simp-config} *}
    2.42 +subsection {* Simplifier tracing and debugging \label{sec:simp-trace} *}
    2.43  
    2.44  text {*
    2.45    \begin{tabular}{rcll}
    2.46 -    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
    2.47      @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
    2.48      @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
    2.49      @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
    2.50 +    @{attribute_def simp_trace_new} & : & @{text attribute} \\
    2.51 +    @{attribute_def simp_break} & : & @{text attribute} \\
    2.52    \end{tabular}
    2.53    \medskip
    2.54  
    2.55 -  These configurations options control further aspects of the Simplifier.
    2.56 -  See also \secref{sec:config}.
    2.57 +  @{rail \<open>
    2.58 +    @@{attribute simp_trace_new} ('interactive')? \<newline>
    2.59 +      ('mode' '=' ('full' | 'normal'))? \<newline>
    2.60 +      ('depth' '=' @{syntax nat})?
    2.61 +    ;
    2.62 +
    2.63 +    @@{attribute simp_break} (@{syntax term}*)
    2.64 +  \<close>}
    2.65 +
    2.66 +  These attributes and configurations options control various aspects of
    2.67 +  Simplifier tracing and debugging.
    2.68  
    2.69    \begin{description}
    2.70  
    2.71 -  \item @{attribute simp_depth_limit} limits the number of recursive
    2.72 -  invocations of the Simplifier during conditional rewriting.
    2.73 -
    2.74    \item @{attribute simp_trace} makes the Simplifier output internal
    2.75    operations.  This includes rewrite steps, but also bookkeeping like
    2.76    modifications of the simpset.
    2.77 @@ -890,57 +902,30 @@
    2.78    information about internal operations.  This includes any attempted
    2.79    invocation of simplification procedures.
    2.80  
    2.81 +  \item @{attribute simp_trace_new} controls Simplifier tracing within
    2.82 +  Isabelle/PIDE applications, notably Isabelle/jEdit \cite{isabelle-jedit}.
    2.83 +  This provides a hierarchical representation of the rewriting steps
    2.84 +  performed by the Simplifier.
    2.85 +
    2.86 +  Users can configure the behaviour by specifying breakpoints, verbosity and
    2.87 +  enabling or disabling the interactive mode. In normal verbosity (the
    2.88 +  default), only rule applications matching a breakpoint will be shown to
    2.89 +  the user. In full verbosity, all rule applications will be logged.
    2.90 +  Interactive mode interrupts the normal flow of the Simplifier and defers
    2.91 +  the decision how to continue to the user via some GUI dialog.
    2.92 +
    2.93 +  \item @{attribute simp_break} declares term or theorem breakpoints for
    2.94 +  @{attribute simp_trace_new} as described above. Term breakpoints are
    2.95 +  patterns which are checked for matches on the redex of a rule application.
    2.96 +  Theorem breakpoints trigger when the corresponding theorem is applied in a
    2.97 +  rewrite step. For example:
    2.98 +
    2.99    \end{description}
   2.100  *}
   2.101  
   2.102 -subsection {* Simplifier trace \label{sec:simplifier-trace} *}
   2.103 -
   2.104 -text {*
   2.105 -  The new visual tracing facility is available in Isabelle/jEdit and
   2.106 -  provides a hierarchical representation of the rewriting steps
   2.107 -  performed by the simplifier.  It is intended to supersede the old
   2.108 -  textual tracing in a future release.
   2.109 -
   2.110 -  Users can configure the behaviour of the new tracing by specifying
   2.111 -  breakpoints, verbosity and enabling or disabling the interactive
   2.112 -  mode.  In normal verbosity (the default), only rule applications
   2.113 -  matching a breakpoint will be shown to the user.  In full verbosity,
   2.114 -  all rule applications will be logged.
   2.115 -
   2.116 -  There are two kinds of breakpoints: term and theorem breakpoints.
   2.117 -  Term breakpoints are patterns which are checked for matches on the
   2.118 -  redex of a rule application.  Theorem breakpoints trigger when the
   2.119 -  corresponding theorem is applied in a rewrite step.
   2.120 -
   2.121 -  In addition to that, the interactive mode interrupts the normal flow
   2.122 -  of the simplifier and defers the decision how to continue to the
   2.123 -  user.
   2.124 -
   2.125 -  \begin{matharray}{rcl}
   2.126 -    @{attribute simplifier_trace} & : & @{text attribute} \\
   2.127 -    @{attribute simp_break} & : & @{text attribute} \\
   2.128 -  \end{matharray}
   2.129 -
   2.130 -  @{rail \<open>
   2.131 -    @@{attribute simplifier_trace} ('interactive')? \<newline>
   2.132 -      ('mode' '=' ('full' | 'normal'))? \<newline>
   2.133 -      ('depth' '=' @{syntax nat})?
   2.134 -    ;
   2.135 -
   2.136 -    @@{attribute simp_break} (@{syntax term}*);
   2.137 -  \<close>}
   2.138 -
   2.139 -  The @{attribute simp_break} option can be used to declare both term
   2.140 -  and theorems, for example:
   2.141 -*}
   2.142 -
   2.143 -declare conjI[simp_break]
   2.144 +declare conjI [simp_break]
   2.145  declare [[simp_break "?x \<and> ?y"]]
   2.146  
   2.147 -text{*
   2.148 -  The other options behave in a similar way as for the old trace (see
   2.149 -  \secref{sec:simp-config}).
   2.150 -*}
   2.151  
   2.152  subsection {* Simplification procedures \label{sec:simproc} *}
   2.153  
     3.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 15:16:50 2014 +0200
     3.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 16:04:45 2014 +0200
     3.3 @@ -419,7 +419,7 @@
     3.4    (Attrib.setup @{binding simp_break}
     3.5      (Scan.repeat Args.term_pattern >> breakpoint)
     3.6      "declaration of a simplifier breakpoint" #>
     3.7 -   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
     3.8 +   Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
     3.9      "simplifier trace configuration")
    3.10  
    3.11  end