src/HOL/Tools/ATP_Manager/atp_minimal.ML

structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;

(*  Title:      HOL/Tools/ATP_Manager/atp_minimal.ML
    Author:     Philipp Meyer, TU Muenchen

Minimalization of theorem list for metis by using an external automated theorem prover
*)

signature ATP_MINIMAL =
sig
  val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
    (string * thm list) list -> ((string * thm list) list * int) option * string
end

structure ATP_Minimal: ATP_MINIMAL =
struct

(* output control *)

fun debug str = Output.debug (fn () => str)
fun debug_fn f = if ! Output.debugging then f () else ()
fun answer str = Output.writeln str
fun println str = Output.priority str

fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
fun length_string namelist = Int.toString (length namelist)

fun print_names name_thms_pairs =
  let
    val names = map fst name_thms_pairs
    val ordered = order_unique names
  in
    app (fn name => (debug ("  " ^ name))) ordered
  end


(* minimalization algorithm *)

local
  fun isplit (l,r) [] = (l,r)
    | isplit (l,r) (h::[]) = (h::l, r)
    | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
in
  fun split lst = isplit ([],[]) lst
end

local
  fun min p sup [] = raise Empty
    | min p sup [s0] = [s0]
    | min p sup s =
      let
        val (l0, r0) = split s
      in
        if p (sup @ l0)
        then min p sup l0
        else
          if p (sup @ r0)
          then min p sup r0
          else
            let
              val l = min p (sup @ r0) l0
              val r = min p (sup @ l) r0
            in
              l @ r
            end
      end
in
  (* return a minimal subset v of s that satisfies p
   @pre p(s) & ~p([]) & monotone(p)
   @post v subset s & p(v) &
         forall e in v. ~p(v \ e)
   *)
  fun minimal p s =
    let val c = Unsynchronized.ref 0
        fun pc xs = (c := !c + 1; p xs)
    in
    (case min pc [] s of
       [x] => if pc [] then [] else [x]
     | m => m,
     !c)
    end
end


(* failure check and producing answer *)

datatype 'a prove_result = Success of 'a | Failure | Timeout | Error

val string_of_result =
  fn Success _ => "Success"
   | Failure => "Failure"
   | Timeout => "Timeout"
   | Error => "Error"

val failure_strings =
  [("SPASS beiseite: Ran out of time.", Timeout),
   ("Timeout", Timeout),
   ("time limit exceeded", Timeout),
   ("# Cannot determine problem status within resource limit", Timeout),
   ("Error", Error)]

fun produce_answer result =
  let
    val ATP_Wrapper.Prover_Result {success, message, proof=result_string,
      internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result
  in
  if success then
    (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
  else
    let
      val failure = failure_strings |> get_first (fn (s, t) =>
          if String.isSubstring s result_string then SOME (t, result_string) else NONE)
    in
      if is_some failure then
        the failure
      else
        (Failure, result_string)
    end
  end


(* wrapper for calling external prover *)

fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
  let
    val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
    val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    val _ = debug_fn (fn () => print_names name_thm_pairs)
    val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    val problem = ATP_Wrapper.ATP_Problem {
      with_full_types = ! ATP_Manager.full_types,
      subgoal = subgoalno,
      goal = Proof.get_goal state,
      axiom_clauses = SOME axclauses,
      filtered_clauses = filtered }
    val (result, proof) = produce_answer (prover problem time_limit)
    val _ = println (string_of_result result)
    val _ = debug proof
  in
    (result, proof)
  end


(* minimalization of thms *)

fun minimalize prover prover_name time_limit state name_thms_pairs =
  let
    val _ =
      println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
        ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
    val _ = debug_fn (fn () => app (fn (n, tl) =>
        (debug n; app (fn t =>
          debug ("  " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
    val test_thms_fun = sh_test_thms prover time_limit 1 state
    fun test_thms filtered thms =
      case test_thms_fun filtered thms of (Success _, _) => true | _ => false
    val answer' = pair and answer'' = pair NONE
  in
    (* try prove first to check result and get used theorems *)
    (case test_thms_fun NONE name_thms_pairs of
      (Success (used, filtered), _) =>
        let
          val ordered_used = order_unique used
          val to_use =
            if length ordered_used < length name_thms_pairs then
              filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
            else
              name_thms_pairs
          val (min_thms, n) = if null to_use then ([], 0)
            else minimal (test_thms (SOME filtered)) to_use
          val min_names = order_unique (map fst min_thms)
          val _ = println ("Interations: " ^ string_of_int n)
          val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
          val _ = debug_fn (fn () => print_names min_thms)
        in
          answer' (SOME(min_thms,n)) ("Try this command: " ^
            Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
        end
    | (Timeout, _) =>
        answer'' ("Timeout: You may need to increase the time limit of " ^
          Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
    | (Error, msg) =>
        answer'' ("Error in prover: " ^ msg)
    | (Failure, _) =>
        answer'' "Failure: No proof with the theorems supplied")
    handle ResHolClause.TOO_TRIVIAL =>
        answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
    | ERROR msg =>
        answer'' ("Error: " ^ msg)
  end


(* Isar command and parsing input *)

local structure K = OuterKeyword and P = OuterParse and T = OuterLex in

fun get_thms context =
  map (fn (name, interval) =>
    let
      val thmref = Facts.Named ((name, Position.none), interval)
      val ths = ProofContext.get_fact context thmref
      val name' = Facts.string_of_ref thmref
    in
      (name', ths)
    end)

val default_prover = "remote_vampire"
val default_time_limit = 5

fun get_time_limit_arg time_string =
  (case Int.fromString time_string of
    SOME t => t
  | NONE => error ("Invalid time limit: " ^ quote time_string))

val get_options =
  let
    val def = (default_prover, default_time_limit)
  in
    foldl (fn ((name, a), (p, t)) =>
      (case name of
        "time" => (p, (get_time_limit_arg a))
      | "atp" => (a, t)
      | n => error ("Invalid argument: " ^ n))) def
  end

fun sh_min_command args thm_names state =
  let
    val (prover_name, time_limit) = get_options args
    val prover =
      case ATP_Manager.get_prover prover_name (Proof.theory_of state) of
        SOME prover => prover
      | NONE => error ("Unknown prover: " ^ quote prover_name)
    val name_thms_pairs = get_thms (Proof.context_of state) thm_names
    fun print_answer (_, msg) = answer msg
  in
    print_answer (minimalize prover prover_name time_limit state name_thms_pairs)
  end

val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)

val _ =
  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
      Toplevel.no_timing o Toplevel.unknown_proof o
        Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))

end

end