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