misc tuning and simplification;
authorwenzelm
Mon Jul 21 16:49:06 2014 +0200 (2014-07-21)
changeset 57592b73d74d0e428
parent 57591 8c095aef6769
child 57593 2f7d91242b99
misc tuning and simplification;
src/Pure/Tools/simplifier_trace.ML
     1.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 16:04:45 2014 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 16:49:06 2014 +0200
     1.3 @@ -60,36 +60,43 @@
     1.4       breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
     1.5  )
     1.6  
     1.7 -fun map_breakpoints f_term f_thm =
     1.8 +val get_data = Data.get o Context.Proof
     1.9 +val put_data = Context.proof_map o Data.put
    1.10 +
    1.11 +val get_breakpoints = #breakpoints o get_data
    1.12 +
    1.13 +fun map_breakpoints f =
    1.14    Data.map
    1.15 -    (fn {max_depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
    1.16 +    (fn {max_depth, mode, interactive, parent, memory, breakpoints} =>
    1.17        {max_depth = max_depth,
    1.18         mode = mode,
    1.19         interactive = interactive,
    1.20         memory = memory,
    1.21         parent = parent,
    1.22 -       breakpoints = (f_term term_bs, f_thm thm_bs)})
    1.23 +       breakpoints = f breakpoints})
    1.24  
    1.25  fun add_term_breakpoint term =
    1.26 -  map_breakpoints (Item_Net.update term) I
    1.27 +  map_breakpoints (apfst (Item_Net.update term))
    1.28  
    1.29  fun add_thm_breakpoint thm context =
    1.30    let
    1.31      val rrules = mk_rrules (Context.proof_of context) [thm]
    1.32    in
    1.33 -    map_breakpoints I (fold Item_Net.update rrules) context
    1.34 +    map_breakpoints (apsnd (fold Item_Net.update rrules)) context
    1.35    end
    1.36  
    1.37 -fun is_breakpoint (term, rrule) context =
    1.38 +fun check_breakpoint (term, rrule) ctxt =
    1.39    let
    1.40 -    val {breakpoints, ...} = Data.get context
    1.41 +    val thy = Proof_Context.theory_of ctxt
    1.42 +    val (term_bs, thm_bs) = get_breakpoints ctxt
    1.43  
    1.44 -    fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
    1.45 -    val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
    1.46 +    val term_matches =
    1.47 +      filter (fn pat => Pattern.matches thy (pat, term))
    1.48 +        (Item_Net.retrieve_matching term_bs term)
    1.49  
    1.50 -    val {thm = thm, ...} = rrule
    1.51 -    val thm_matches = exists (eq_rrule o pair rrule)
    1.52 -      (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
    1.53 +    val thm_matches =
    1.54 +      exists (eq_rrule o pair rrule)
    1.55 +        (Item_Net.retrieve_matching thm_bs (Thm.full_prop_of (#thm rrule)))
    1.56    in
    1.57      (term_matches, thm_matches)
    1.58    end
    1.59 @@ -146,7 +153,7 @@
    1.60  
    1.61  fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
    1.62    let
    1.63 -    val {mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
    1.64 +    val {mode, interactive, memory, parent, ...} = get_data ctxt
    1.65  
    1.66      val eligible =
    1.67        (case mode of
    1.68 @@ -195,7 +202,7 @@
    1.69  
    1.70  fun step ({term, thm, unconditional, ctxt, rrule}: data) =
    1.71    let
    1.72 -    val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
    1.73 +    val (matching_terms, thm_triggered) = check_breakpoint (term, rrule) ctxt
    1.74  
    1.75      val {name, ...} = rrule
    1.76      val term_triggered = not (null matching_terms)
    1.77 @@ -232,21 +239,19 @@
    1.78          {props = [], pretty = pretty}
    1.79        end
    1.80  
    1.81 -    val {max_depth, mode, interactive, memory, breakpoints, ...} =
    1.82 -      Data.get (Context.Proof ctxt)
    1.83 +    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
    1.84  
    1.85      fun mk_promise result =
    1.86        let
    1.87          val result_id = #1 result
    1.88  
    1.89 -        fun put mode' interactive' = Data.put
    1.90 +        fun put mode' interactive' = put_data
    1.91            {max_depth = max_depth,
    1.92             mode = mode',
    1.93             interactive = interactive',
    1.94             memory = memory,
    1.95             parent = result_id,
    1.96 -           breakpoints = breakpoints} (Context.Proof ctxt) |>
    1.97 -          Context.the_proof
    1.98 +           breakpoints = breakpoints} ctxt
    1.99  
   1.100          fun to_response "skip" = NONE
   1.101            | to_response "continue" = SOME (put mode true)
   1.102 @@ -273,22 +278,20 @@
   1.103        {props = [],
   1.104         pretty = Syntax.pretty_term ctxt term}
   1.105  
   1.106 -    val {max_depth, mode, interactive, memory, breakpoints, ...} =
   1.107 -      Data.get (Context.Proof ctxt)
   1.108 +    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
   1.109  
   1.110 -    fun put result_id = Data.put
   1.111 +    fun put result_id = put_data
   1.112        {max_depth = max_depth,
   1.113         mode = if depth >= max_depth then Disabled else mode,
   1.114         interactive = interactive,
   1.115         memory = memory,
   1.116         parent = result_id,
   1.117 -       breakpoints = breakpoints} (Context.Proof ctxt)
   1.118 -
   1.119 -    val context' =
   1.120 -      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
   1.121 -        NONE => put 0
   1.122 -      | SOME res => (output_result res; put (#1 res)))
   1.123 -  in Context.the_proof context' end
   1.124 +       breakpoints = breakpoints} ctxt
   1.125 +  in
   1.126 +    (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
   1.127 +      NONE => put 0
   1.128 +    | SOME res => (output_result res; put (#1 res)))
   1.129 +  end
   1.130  
   1.131  fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
   1.132    let
   1.133 @@ -314,7 +317,7 @@
   1.134          {props = [(successN, "false")], pretty = pretty}
   1.135        end
   1.136  
   1.137 -    val {interactive, ...} = Data.get (Context.Proof ctxt)
   1.138 +    val {interactive, ...} = get_data ctxt
   1.139  
   1.140      fun mk_promise result =
   1.141        let