src/HOL/Mutabelle/MutabelleExtra.thy
author wenzelm
Mon Oct 25 21:23:09 2010 +0200 (2010-10-25)
changeset 40133 b61d52de66f0
parent 40132 7ee65dbffa31
child 40341 03156257040f
permissions -rw-r--r--
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
bulwahn@34965
     1
theory MutabelleExtra
bulwahn@34965
     2
imports Complex_Main SML_Quickcheck
bulwahn@34965
     3
(*
bulwahn@34965
     4
  "~/Downloads/Jinja/J/TypeSafe"
bulwahn@34965
     5
  "~/Downloads/Jinja/J/Annotate"
bulwahn@34965
     6
  (* FIXME "Example" *)
bulwahn@34965
     7
  "~/Downloads/Jinja/J/execute_Bigstep"
bulwahn@34965
     8
  "~/Downloads/Jinja/J/execute_WellType"
bulwahn@34965
     9
  "~/Downloads/Jinja/JVM/JVMDefensive"
bulwahn@34965
    10
  "~/Downloads/Jinja/JVM/JVMListExample"
bulwahn@34965
    11
  "~/Downloads/Jinja/BV/BVExec"
bulwahn@34965
    12
  "~/Downloads/Jinja/BV/LBVJVM"
bulwahn@34965
    13
  "~/Downloads/Jinja/BV/BVNoTypeError"
bulwahn@34965
    14
  "~/Downloads/Jinja/BV/BVExample"
bulwahn@34965
    15
  "~/Downloads/Jinja/Compiler/TypeComp"
bulwahn@34965
    16
*)
bulwahn@34965
    17
(*"~/Downloads/NormByEval/NBE"*)
bulwahn@34965
    18
uses "mutabelle.ML"
bulwahn@34965
    19
     "mutabelle_extra.ML"
bulwahn@34965
    20
begin
bulwahn@34965
    21
wenzelm@40133
    22
(* FIXME !?!?! *)
wenzelm@40133
    23
ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
wenzelm@40133
    24
ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
wenzelm@40133
    25
ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
wenzelm@40133
    26
ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
bulwahn@34965
    27
bulwahn@34965
    28
quickcheck_params [size = 5, iterations = 1000]
bulwahn@34965
    29
(*
bulwahn@34965
    30
nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
bulwahn@34965
    31
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
bulwahn@34965
    32
*)
blanchet@39324
    33
ML {* Auto_Tools.time_limit := 10 *}
bulwahn@34965
    34
bulwahn@34965
    35
bulwahn@34965
    36
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
bulwahn@34965
    37
bulwahn@34965
    38
ML {*
bulwahn@34965
    39
(*
bulwahn@34965
    40
      MutabelleExtra.random_seed := 1.0;
bulwahn@34965
    41
      MutabelleExtra.thms_of true @{theory Complex_Main}
bulwahn@34965
    42
      |> MutabelleExtra.take_random 1000000
bulwahn@34965
    43
      |> (fn thms => List.drop (thms, 1000))
bulwahn@34965
    44
      |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
bulwahn@34965
    45
             @{theory} [MutabelleExtra.quickcheck_mtd "SML",
bulwahn@34965
    46
                        MutabelleExtra.quickcheck_mtd "code"
bulwahn@34965
    47
                        (*MutabelleExtra.refute_mtd,
bulwahn@34965
    48
                        MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
bulwahn@34965
    49
*)
bulwahn@34965
    50
 *}
bulwahn@34965
    51
wenzelm@40133
    52
(* FIXME !?!?! *)
wenzelm@40133
    53
ML {* Output.Private_Hooks.tracing_fn := old_tr *}
wenzelm@40133
    54
ML {* Output.Private_Hooks.writeln_fn := old_wr *}
wenzelm@40133
    55
ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
wenzelm@40133
    56
ML {* Output.Private_Hooks.warning_fn := old_wa *}
bulwahn@34965
    57
blanchet@39324
    58
end