src/HOL/Eisbach/Eisbach_Tools.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 63527 59eff6e56d81
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/Eisbach/Eisbach_Tools.thy
     2     Author:     Daniel Matichuk, NICTA/UNSW
     3 
     4 Usability tools for Eisbach.
     5 *)
     6 
     7 theory Eisbach_Tools
     8 imports Eisbach
     9 begin
    10 
    11 ML \<open>
    12 local
    13 
    14 fun trace_method parser print =
    15   Scan.lift (Args.mode "dummy") -- parser >>
    16     (fn (dummy, x) => fn ctxt => SIMPLE_METHOD (fn st =>
    17       (if dummy orelse not (Method.detect_closure_state st)
    18        then tracing (print ctxt x) else ();
    19        all_tac st)));
    20 
    21 fun setup_trace_method binding parser print =
    22   Method.setup binding
    23     (trace_method parser (fn ctxt => fn x => Binding.name_of binding ^ ": " ^ print ctxt x))
    24     "";
    25 
    26 in
    27 
    28 val _ =
    29   Theory.setup
    30    (setup_trace_method @{binding print_fact}
    31       (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
    32       (fn ctxt => fn (tok, thms) =>
    33         (* FIXME proper formatting!? *)
    34         Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #>
    35     setup_trace_method @{binding print_term}
    36       (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
    37       (fn ctxt => fn (tok, t) =>
    38         (* FIXME proper formatting!? *)
    39         Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #>
    40     setup_trace_method @{binding print_type}
    41       (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ)
    42       (fn ctxt => fn (tok, t) =>
    43         (* FIXME proper formatting!? *)
    44         Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t));
    45 
    46 end
    47 \<close>
    48 
    49 ML \<open>
    50   fun try_map v seq =
    51     (case try Seq.pull seq of
    52       SOME (SOME (x, seq')) => Seq.make (fn () => SOME(x, try_map v seq'))
    53     | SOME NONE => Seq.empty
    54     | NONE => v);
    55 \<close>
    56 
    57 method_setup catch = \<open>
    58   Method.text_closure -- Method.text_closure >>
    59     (fn (text, text') => fn ctxt => fn using => fn st =>
    60       let
    61         val method = Method.evaluate_runtime text ctxt using;
    62         val backup_results = Method.evaluate_runtime text' ctxt using st;
    63       in
    64         (case try method st of
    65           SOME seq => try_map backup_results seq
    66         | NONE => backup_results)
    67       end)
    68 \<close>
    69 
    70 ML \<open>
    71   fun uncurry_rule thm = Conjunction.uncurry_balanced (Thm.nprems_of thm) thm;
    72   fun curry_rule thm =
    73     if Thm.no_prems thm then thm
    74     else
    75       let val conjs = Logic.dest_conjunctions (Thm.major_prem_of thm);
    76       in Conjunction.curry_balanced (length conjs) thm end;
    77 \<close>
    78 
    79 attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\<close>
    80 attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute [] (K curry_rule))\<close>
    81 
    82 end