src/HOL/Mirabelle/Actions/mirabelle_refute.ML
changeset 47730 15f4309bb9eb
parent 47729 44d1f4e0a46e
child 47731 39c5a1a80acc
     1.1 --- a/src/HOL/Mirabelle/Actions/mirabelle_refute.ML	Tue Apr 24 13:55:02 2012 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,39 +0,0 @@
     1.4 -(*  Title:      HOL/Mirabelle/Actions/mirabelle_refute.ML
     1.5 -    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     1.6 -*)
     1.7 -
     1.8 -structure Mirabelle_Refute : MIRABELLE_ACTION =
     1.9 -struct
    1.10 -
    1.11 -
    1.12 -(* FIXME:
    1.13 -fun refute_action args timeout {pre=st, ...} = 
    1.14 -  let
    1.15 -    val subgoal = 1
    1.16 -    val thy = Proof.theory_of st
    1.17 -    val thm = #goal (Proof.raw_goal st)
    1.18 -
    1.19 -    val refute = Refute.refute_goal thy args thm
    1.20 -    val _ = TimeLimit.timeLimit timeout refute subgoal
    1.21 -  in
    1.22 -    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
    1.23 -    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
    1.24 -
    1.25 -    val r =
    1.26 -      if Substring.isSubstring "model found" writ_log
    1.27 -      then
    1.28 -        if Substring.isSubstring "spurious" warn_log
    1.29 -        then SOME "potential counterexample"
    1.30 -        else SOME "real counterexample (bug?)"
    1.31 -      else
    1.32 -        if Substring.isSubstring "time limit" writ_log
    1.33 -        then SOME "no counterexample (timeout)"
    1.34 -        else if Substring.isSubstring "Search terminated" writ_log
    1.35 -        then SOME "no counterexample (normal termination)"
    1.36 -        else SOME "no counterexample (unknown)"
    1.37 -  in r end
    1.38 -*)
    1.39 -
    1.40 -fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
    1.41 -
    1.42 -end