1.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 21:57:06 2009 +0200
     1.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 21:58:33 2009 +0200
     1.3 @@ -5,6 +5,32 @@
     1.4  structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
     1.5  struct
     1.6  
     1.7 +local
     1.8 +val valid = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
     1.9 +  member (op =) (explode "_.")
    1.10 +val name = Scan.many1 valid >> (rpair Position.none o implode)
    1.11 +
    1.12 +val digit = (fn
    1.13 +  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
    1.14 +  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
    1.15 +  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
    1.16 +fun join d n = 10 * n + d
    1.17 +val number = Scan.repeat1 (Scan.some digit) >> (fn ds => fold join ds 0)
    1.18 +val interval = Scan.option (Scan.$$ "(" |-- number --| Scan.$$ ")" >>
    1.19 +  (single o Facts.Single))
    1.20 +
    1.21 +val fact_ref = name -- interval >> Facts.Named
    1.22 +
    1.23 +in
    1.24 +
    1.25 +fun thm_of_name ctxt s =
    1.26 +  (case try (Scan.read Symbol.stopper fact_ref) (explode s) of
    1.27 +    SOME (SOME r) => ProofContext.get_fact ctxt r
    1.28 +  | _ => [])
    1.29 +
    1.30 +end
    1.31 +
    1.32 +
    1.33  fun sledgehammer_action args {pre=st, ...} =
    1.34    let
    1.35      val prover_name =
    1.36 @@ -16,16 +42,25 @@
    1.37      val prover = the (AtpManager.get_prover prover_name thy)
    1.38      val timeout = AtpManager.get_timeout () 
    1.39  
    1.40 -    val (success, message) =
    1.41 +    (* run sledgehammer *)
    1.42 +    val (success, message, thm_names) =
    1.43        let
    1.44 -        val (success, message, _, _, _) =
    1.45 +        val (success, (message, thm_names), _, _, _) =
    1.46            prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
    1.47 -      in (success, message) end
    1.48 -      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
    1.49 -           | ERROR msg => (false, "error: " ^ msg)
    1.50 +      in (success, message, SOME thm_names) end
    1.51 +      handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
    1.52 +           | ERROR msg => (false, "error: " ^ msg, NONE)
    1.53 +
    1.54 +    (* try metis *)
    1.55 +    val thms = maps (thm_of_name (Proof.context_of st)) (these thm_names)
    1.56 +    fun metis ctxt = MetisTools.metis_tac ctxt thms
    1.57 +    val msg = if not (AList.defined (op =) args "metis") then "" else
    1.58 +      if try (Mirabelle.can_apply metis) st = SOME true
    1.59 +        then "\nMETIS: success"
    1.60 +        else "\nMETIS: failure"
    1.61    in
    1.62      if success
    1.63 -    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
    1.64 +    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
    1.65      else NONE
    1.66    end
    1.67