File ‹Tools/Mirabelle/mirabelle_arith.ML›

(*  Title:      HOL/Tools/Mirabelle/mirabelle_arith.ML
    Author:     Jasmin Blanchette, TU Munich
    Author:     Sascha Boehme, TU Munich
    Author:     Makarius
    Author:     Martin Desharnais, UniBw Munich

Mirabelle action: "arith".
*)

structure Mirabelle_Arith: MIRABELLE_ACTION =
struct

fun make_action ({timeout, ...} : Mirabelle.action_context) =
  let
    fun run ({pre, ...} : Mirabelle.command) =
      (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
        ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
      | (_, false) => "failed")
  in ("", {run = run, finalize = K ""}) end

val () = Mirabelle.register_action "arith" make_action

end