| author | wenzelm |
| Fri, 05 Mar 2010 23:52:09 +0100 | |
| changeset 35593 | 88b49baba092 |
| parent 32858 | 51fda1c8fa2d |
| permissions | -rw-r--r-- |
| 32564 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_refute.ML |
2 |
Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
3 |
*) |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
4 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
5 |
structure Mirabelle_Refute : MIRABELLE_ACTION = |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
6 |
struct |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
7 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
8 |
|
|
32386
18bbd9f4c2cd
disabled refute action (needs changes in the code of refute)
boehmes
parents:
32385
diff
changeset
|
9 |
(* FIXME: |
| 32469 | 10 |
fun refute_action args timeout {pre=st, ...} =
|
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
11 |
let |
|
32858
51fda1c8fa2d
Refute.refute_goal: goal addressing from 1 as usual;
wenzelm
parents:
32564
diff
changeset
|
12 |
val subgoal = 1 |
| 35593 | 13 |
val thy = Proof.theory_of st |
14 |
val thm = #goal (Proof.raw_goal st) |
|
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
15 |
|
|
32858
51fda1c8fa2d
Refute.refute_goal: goal addressing from 1 as usual;
wenzelm
parents:
32564
diff
changeset
|
16 |
val refute = Refute.refute_goal thy args thm |
| 32469 | 17 |
val _ = TimeLimit.timeLimit timeout refute subgoal |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
18 |
in |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
19 |
val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
20 |
val warn_log = Substring.full (the (Symtab.lookup tab "warning")) |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
21 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
22 |
val r = |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
23 |
if Substring.isSubstring "model found" writ_log |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
24 |
then |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
25 |
if Substring.isSubstring "spurious" warn_log |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
26 |
then SOME "potential counterexample" |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
27 |
else SOME "real counterexample (bug?)" |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
28 |
else |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
29 |
if Substring.isSubstring "time limit" writ_log |
| 32518 | 30 |
then SOME "no counterexample (timeout)" |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
31 |
else if Substring.isSubstring "Search terminated" writ_log |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
32 |
then SOME "no counterexample (normal termination)" |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
33 |
else SOME "no counterexample (unknown)" |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
34 |
in r end |
|
32386
18bbd9f4c2cd
disabled refute action (needs changes in the code of refute)
boehmes
parents:
32385
diff
changeset
|
35 |
*) |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
36 |
|
|
32386
18bbd9f4c2cd
disabled refute action (needs changes in the code of refute)
boehmes
parents:
32385
diff
changeset
|
37 |
fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
|
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
38 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
39 |
end |