author | blanchet |
Wed, 03 Nov 2010 22:26:53 +0100 | |
changeset 40341 | 03156257040f |
parent 40133 | b61d52de66f0 |
child 40653 | d921c97bdbd8 |
permissions | -rw-r--r-- |
34965 | 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 |
||
40133
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
22 |
(* FIXME !?!?! *) |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
23 |
ML {* val old_tr = !Output.Private_Hooks.tracing_fn *} |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
24 |
ML {* val old_wr = !Output.Private_Hooks.writeln_fn *} |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
25 |
ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *} |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
26 |
ML {* val old_wa = !Output.Private_Hooks.warning_fn *} |
34965 | 27 |
|
28 |
quickcheck_params [size = 5, iterations = 1000] |
|
29 |
(* |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40133
diff
changeset
|
30 |
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12] |
34965 | 31 |
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat] |
32 |
*) |
|
39324
05452dd66b2b
finished renaming "Auto_Counterexample" to "Auto_Tools"
blanchet
parents:
34965
diff
changeset
|
33 |
ML {* Auto_Tools.time_limit := 10 *} |
34965 | 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 |
||
40133
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
52 |
(* FIXME !?!?! *) |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
53 |
ML {* Output.Private_Hooks.tracing_fn := old_tr *} |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
54 |
ML {* Output.Private_Hooks.writeln_fn := old_wr *} |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
55 |
ML {* Output.Private_Hooks.urgent_message_fn := old_ur *} |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
56 |
ML {* Output.Private_Hooks.warning_fn := old_wa *} |
34965 | 57 |
|
39324
05452dd66b2b
finished renaming "Auto_Counterexample" to "Auto_Tools"
blanchet
parents:
34965
diff
changeset
|
58 |
end |