1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Fri Aug 21 13:21:19 2009 +0200
     1.3 @@ -0,0 +1,36 @@
     1.4 +(* Title:  mirabelle_refute.ML
     1.5 +   Author: Jasmin Blanchette and Sascha Boehme
     1.6 +*)
     1.7 +
     1.8 +structure Mirabelle_Refute : MIRABELLE_ACTION =
     1.9 +struct
    1.10 +
    1.11 +
    1.12 +fun refute_action args {pre=st, ...} = 
    1.13 +  let
    1.14 +    val subgoal = 0
    1.15 +    val thy     = Proof.theory_of st
    1.16 +    val thm = goal_thm_of st
    1.17 +
    1.18 +    val _ = Refute.refute_subgoal thy args thm subgoal
    1.19 +  in
    1.20 +    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
    1.21 +    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
    1.22 +
    1.23 +    val r =
    1.24 +      if Substring.isSubstring "model found" writ_log
    1.25 +      then
    1.26 +        if Substring.isSubstring "spurious" warn_log
    1.27 +        then SOME "potential counterexample"
    1.28 +        else SOME "real counterexample (bug?)"
    1.29 +      else
    1.30 +        if Substring.isSubstring "time limit" writ_log
    1.31 +        then SOME "no counterexample (time out)"
    1.32 +        else if Substring.isSubstring "Search terminated" writ_log
    1.33 +        then SOME "no counterexample (normal termination)"
    1.34 +        else SOME "no counterexample (unknown)"
    1.35 +  in r end
    1.36 +
    1.37 +fun invoke args = Mirabelle.register ("refute", refute_action args)
    1.38 +
    1.39 +end