blanchet@38255: (*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
wenzelm@28477:     Author:     Fabian Immler, TU Muenchen
wenzelm@32996:     Author:     Makarius
blanchet@35967:     Author:     Jasmin Blanchette, TU Muenchen
wenzelm@28477: 
blanchet@38255: Sledgehammer's heart.
wenzelm@28477: *)
wenzelm@28477: 
blanchet@38255: signature SLEDGEHAMMER =
wenzelm@28477: sig
blanchet@38257:   type failure = ATP_Systems.failure
blanchet@39232:   type locality = Sledgehammer_Filter.locality
blanchet@39232:   type relevance_override = Sledgehammer_Filter.relevance_override
blanchet@39232:   type minimize_command = Sledgehammer_Reconstruct.minimize_command
blanchet@35967:   type params =
blanchet@39226:     {blocking: bool,
blanchet@39226:      debug: bool,
blanchet@35967:      verbose: bool,
blanchet@36141:      overlord: bool,
blanchet@35967:      atps: string list,
blanchet@35967:      full_types: bool,
blanchet@36235:      explicit_apply: bool,
blanchet@38984:      relevance_thresholds: real * real,
blanchet@38983:      max_relevant: int option,
blanchet@36220:      theory_relevant: bool option,
blanchet@35967:      isar_proof: bool,
blanchet@36916:      isar_shrink_factor: int,
blanchet@39229:      timeout: Time.time,
blanchet@39229:      expect: string}
blanchet@35867:   type problem =
blanchet@35967:     {subgoal: int,
blanchet@35967:      goal: Proof.context * (thm list * thm),
blanchet@35967:      relevance_override: relevance_override,
blanchet@38991:      axioms: ((string * locality) * thm) list option}
blanchet@35867:   type prover_result =
blanchet@36370:     {outcome: failure option,
blanchet@35967:      message: string,
blanchet@38166:      pool: string Symtab.table,
blanchet@38991:      used_thm_names: (string * locality) list,
blanchet@35967:      atp_run_time_in_msecs: int,
blanchet@36369:      output: string,
blanchet@35967:      proof: string,
blanchet@39053:      axiom_names: (string * locality) list vector,
blanchet@38329:      conjecture_shape: int list list}
blanchet@38346:   type prover = params -> minimize_command -> problem -> prover_result
blanchet@35867: 
blanchet@38257:   val dest_dir : string Config.T
blanchet@38257:   val problem_prefix : string Config.T
blanchet@38257:   val measure_runtime : bool Config.T
blanchet@35967:   val kill_atps: unit -> unit
blanchet@35967:   val running_atps: unit -> unit
wenzelm@29112:   val messages: int option -> unit
blanchet@38257:   val get_prover_fun : theory -> string -> prover
blanchet@38290:   val run_sledgehammer :
blanchet@38290:     params -> int -> relevance_override -> (string -> minimize_command)
blanchet@38290:     -> Proof.state -> unit
blanchet@38257:   val setup : theory -> theory
wenzelm@28477: end;
wenzelm@28477: 
blanchet@38255: structure Sledgehammer : SLEDGEHAMMER =
wenzelm@28477: struct
wenzelm@28477: 
blanchet@38262: open ATP_Problem
blanchet@38262: open ATP_Systems
blanchet@37578: open Metis_Clauses
blanchet@38257: open Sledgehammer_Util
blanchet@39232: open Sledgehammer_Filter
blanchet@38506: open Sledgehammer_Translate
blanchet@39232: open Sledgehammer_Reconstruct
blanchet@37583: 
blanchet@38257: 
blanchet@37583: (** The Sledgehammer **)
blanchet@37583: 
blanchet@38348: (* Identifier to distinguish Sledgehammer from other tools using
blanchet@38348:    "Async_Manager". *)
blanchet@37585: val das_Tool = "Sledgehammer"
blanchet@37585: 
blanchet@37585: fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
blanchet@37585: fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
blanchet@37585: val messages = Async_Manager.thread_messages das_Tool "ATP"
blanchet@35967: 
blanchet@36281: (** problems, results, provers, etc. **)
blanchet@35967: 
blanchet@35967: type params =
blanchet@39226:   {blocking: bool,
blanchet@39226:    debug: bool,
blanchet@35967:    verbose: bool,
blanchet@36141:    overlord: bool,
blanchet@35967:    atps: string list,
blanchet@35967:    full_types: bool,
blanchet@36235:    explicit_apply: bool,
blanchet@38984:    relevance_thresholds: real * real,
blanchet@38983:    max_relevant: int option,
blanchet@36220:    theory_relevant: bool option,
blanchet@35967:    isar_proof: bool,
blanchet@36916:    isar_shrink_factor: int,
blanchet@39229:    timeout: Time.time,
blanchet@39229:    expect: string}
blanchet@35867: 
blanchet@35867: type problem =
blanchet@35967:   {subgoal: int,
blanchet@35967:    goal: Proof.context * (thm list * thm),
blanchet@35967:    relevance_override: relevance_override,
blanchet@38991:    axioms: ((string * locality) * thm) list option}
blanchet@35867: 
blanchet@35867: type prover_result =
blanchet@36370:   {outcome: failure option,
blanchet@35967:    message: string,
blanchet@38166:    pool: string Symtab.table,
blanchet@38991:    used_thm_names: (string * locality) list,
blanchet@35967:    atp_run_time_in_msecs: int,
blanchet@36369:    output: string,
blanchet@35967:    proof: string,
blanchet@39053:    axiom_names: (string * locality) list vector,
blanchet@38329:    conjecture_shape: int list list}
blanchet@35867: 
blanchet@38346: type prover = params -> minimize_command -> problem -> prover_result
blanchet@35867: 
blanchet@38257: (* configuration attributes *)
wenzelm@28484: 
blanchet@38257: val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
blanchet@38257:   (*Empty string means create files in Isabelle's temporary files directory.*)
wenzelm@28484: 
blanchet@38257: val (problem_prefix, problem_prefix_setup) =
blanchet@38257:   Attrib.config_string "atp_problem_prefix" (K "prob");
wenzelm@28477: 
blanchet@38257: val (measure_runtime, measure_runtime_setup) =
blanchet@38257:   Attrib.config_bool "atp_measure_runtime" (K false);
wenzelm@32995: 
blanchet@38257: fun with_path cleanup after f path =
blanchet@38257:   Exn.capture f path
blanchet@38257:   |> tap (fn _ => cleanup path)
blanchet@38257:   |> Exn.release
blanchet@38257:   |> tap (after path)
wenzelm@28484: 
blanchet@38257: (* Splits by the first possible of a list of delimiters. *)
blanchet@38257: fun extract_proof delims output =
blanchet@38257:   case pairself (find_first (fn s => String.isSubstring s output))
blanchet@38257:                 (ListPair.unzip delims) of
blanchet@38257:     (SOME begin_delim, SOME end_delim) =>
blanchet@38257:     (output |> first_field begin_delim |> the |> snd
blanchet@38257:             |> first_field end_delim |> the |> fst
blanchet@38257:             |> first_field "\n" |> the |> snd
blanchet@38257:      handle Option.Option => "")
blanchet@38257:   | _ => ""
blanchet@38257: 
blanchet@38257: fun extract_proof_and_outcome complete res_code proof_delims known_failures
blanchet@38257:                               output =
blanchet@38307:   case known_failure_in_output output known_failures of
blanchet@38307:     NONE => (case extract_proof proof_delims output of
blanchet@38307:              "" => ("", SOME MalformedOutput)
blanchet@38257:            | proof => if res_code = 0 then (proof, NONE)
blanchet@38257:                       else ("", SOME UnknownError))
blanchet@38307:   | SOME failure =>
blanchet@38257:     ("", SOME (if failure = IncompleteUnprovable andalso complete then
blanchet@38257:                  Unprovable
blanchet@38257:                else
blanchet@38257:                  failure))
blanchet@38257: 
blanchet@38257: fun extract_clause_sequence output =
blanchet@38257:   let
blanchet@38257:     val tokens_of = String.tokens (not o Char.isAlphaNum)
blanchet@38257:     fun extract_num ("clause" :: (ss as _ :: _)) =
blanchet@38257:     Int.fromString (List.last ss)
blanchet@38257:       | extract_num _ = NONE
blanchet@38257:   in output |> split_lines |> map_filter (extract_num o tokens_of) end
blanchet@38257: 
blanchet@38257: val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
blanchet@38257: 
blanchet@38257: val parse_clause_formula_pair =
blanchet@38740:   $$ "(" |-- scan_integer --| $$ ","
blanchet@38740:   -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
blanchet@38257:   --| Scan.option ($$ ",")
blanchet@38257: val parse_clause_formula_relation =
blanchet@38257:   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
blanchet@38257:   |-- Scan.repeat parse_clause_formula_pair
blanchet@38257: val extract_clause_formula_relation =
blanchet@38977:   Substring.full #> Substring.position set_ClauseFormulaRelationN
blanchet@38977:   #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
blanchet@38977:   #> explode #> parse_clause_formula_relation #> fst
blanchet@38257: 
blanchet@39232: (* TODO: move to "Sledgehammer_Reconstruct" *)
blanchet@38257: fun repair_conjecture_shape_and_theorem_names output conjecture_shape
blanchet@38937:                                               axiom_names =
blanchet@38257:   if String.isSubstring set_ClauseFormulaRelationN output then
blanchet@38257:     (* This is a hack required for keeping track of axioms after they have been
blanchet@38937:        clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is
blanchet@38937:        also part of this hack. *)
blanchet@38257:     let
blanchet@38286:       val j0 = hd (hd conjecture_shape)
blanchet@38257:       val seq = extract_clause_sequence output
blanchet@38257:       val name_map = extract_clause_formula_relation output
blanchet@38257:       fun renumber_conjecture j =
blanchet@38983:         conjecture_prefix ^ string_of_int (j - j0)
blanchet@38740:         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
blanchet@38286:         |> map (fn s => find_index (curry (op =) s) seq + 1)
blanchet@39053:       fun names_for_number j =
blanchet@39053:         j |> AList.lookup (op =) name_map |> these
blanchet@39053:           |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
blanchet@39053:           |> map (fn name =>
blanchet@39053:                      (name, name |> find_first_in_list_vector axiom_names
blanchet@39053:                                  |> the)
blanchet@39053:                      handle Option.Option =>
blanchet@39053:                             error ("No such fact: " ^ quote name ^ "."))
blanchet@38257:     in
blanchet@38286:       (conjecture_shape |> map (maps renumber_conjecture),
blanchet@39053:        seq |> map names_for_number |> Vector.fromList)
blanchet@38257:     end
blanchet@38257:   else
blanchet@38937:     (conjecture_shape, axiom_names)
blanchet@38257: 
blanchet@38257: 
blanchet@38257: (* generic TPTP-based provers *)
blanchet@38257: 
blanchet@38699: fun prover_fun atp_name
blanchet@38883:         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
blanchet@38983:          known_failures, default_max_relevant, default_theory_relevant,
blanchet@38854:          explicit_forall, use_conjecture_for_hypotheses}
blanchet@38699:         ({debug, verbose, overlord, full_types, explicit_apply,
blanchet@38984:           relevance_thresholds, max_relevant, theory_relevant, isar_proof,
blanchet@38984:           isar_shrink_factor, timeout, ...} : params)
blanchet@38346:         minimize_command
blanchet@39117:         ({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override,
blanchet@39117:           axioms} : problem) =
blanchet@38257:   let
blanchet@39119:     val (_, hyp_ts, concl_t) = strip_subgoal th subgoal
blanchet@38699: 
blanchet@38983:     val print = priority
blanchet@38699:     fun print_v f = () |> verbose ? print o f
blanchet@38699:     fun print_d f = () |> debug ? print o f
blanchet@38699: 
blanchet@38330:     val the_axioms =
blanchet@38330:       case axioms of
blanchet@38329:         SOME axioms => axioms
blanchet@38699:       | NONE =>
blanchet@39117:         (relevant_facts ctxt full_types relevance_thresholds
blanchet@38983:                         (the_default default_max_relevant max_relevant)
blanchet@38812:                         (the_default default_theory_relevant theory_relevant)
blanchet@39117:                         relevance_override chained_ths hyp_ts concl_t
blanchet@38699:          |> tap ((fn n => print_v (fn () =>
blanchet@38984:                           "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
blanchet@38984:                           " for " ^ quote atp_name ^ ".")) o length))
blanchet@38257: 
blanchet@38257:     (* path to unique problem file *)
blanchet@38257:     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
blanchet@38257:                        else Config.get ctxt dest_dir;
blanchet@38257:     val the_problem_prefix = Config.get ctxt problem_prefix;
blanchet@38257:     fun prob_pathname nr =
blanchet@38257:       let
blanchet@38257:         val probfile =
blanchet@38699:           Path.basic ((if overlord then "prob_" ^ atp_name
blanchet@38257:                        else the_problem_prefix ^ serial_string ())
blanchet@38257:                       ^ "_" ^ string_of_int nr)
blanchet@38257:       in
blanchet@38257:         if the_dest_dir = "" then File.tmp_path probfile
blanchet@38257:         else if File.exists (Path.explode the_dest_dir)
blanchet@38257:         then Path.append (Path.explode the_dest_dir) probfile
blanchet@39053:         else error ("No such directory: " ^ quote the_dest_dir ^ ".")
blanchet@38257:       end;
blanchet@38257: 
blanchet@38983:     val measure_run_time = verbose orelse Config.get ctxt measure_runtime
blanchet@38338:     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
blanchet@38257:     (* write out problem file and call prover *)
blanchet@38883:     fun command_line complete timeout probfile =
blanchet@38257:       let
blanchet@38257:         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
blanchet@38257:                    " " ^ File.shell_path probfile
blanchet@38257:       in
blanchet@38983:         (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
blanchet@38983:          else "exec " ^ core) ^ " 2>&1"
blanchet@38257:       end
blanchet@38257:     fun split_time s =
blanchet@38257:       let
blanchet@38257:         val split = String.tokens (fn c => str c = "\n");
blanchet@38257:         val (output, t) = s |> split |> split_last |> apfst cat_lines;
blanchet@38257:         fun as_num f = f >> (fst o read_int);
blanchet@38257:         val num = as_num (Scan.many1 Symbol.is_ascii_digit);
blanchet@38257:         val digit = Scan.one Symbol.is_ascii_digit;
blanchet@38257:         val num3 = as_num (digit ::: digit ::: (digit >> single));
blanchet@38257:         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
blanchet@38257:         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
blanchet@38257:       in (output, as_time t) end;
blanchet@38257:     fun run_on probfile =
blanchet@38338:       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
blanchet@38278:         (home_var, _) :: _ =>
blanchet@38257:         error ("The environment variable " ^ quote home_var ^ " is not set.")
blanchet@38278:       | [] =>
blanchet@38278:         if File.exists command then
blanchet@38278:           let
blanchet@38883:             fun do_run complete timeout =
blanchet@38278:               let
blanchet@38883:                 val command = command_line complete timeout probfile
blanchet@38278:                 val ((output, msecs), res_code) =
blanchet@38278:                   bash_output command
blanchet@38278:                   |>> (if overlord then
blanchet@38278:                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
blanchet@38278:                        else
blanchet@38278:                          I)
blanchet@38983:                   |>> (if measure_run_time then split_time else rpair 0)
blanchet@38278:                 val (proof, outcome) =
blanchet@38278:                   extract_proof_and_outcome complete res_code proof_delims
blanchet@38278:                                             known_failures output
blanchet@38278:               in (output, msecs, proof, outcome) end
blanchet@38278:             val readable_names = debug andalso overlord
blanchet@38506:             val (problem, pool, conjecture_offset, axiom_names) =
blanchet@38506:               prepare_problem ctxt readable_names explicit_forall full_types
blanchet@38506:                               explicit_apply hyp_ts concl_t the_axioms
blanchet@38854:             val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
blanchet@38854:                                               problem
blanchet@38854:             val _ = File.write_list probfile ss
blanchet@38278:             val conjecture_shape =
blanchet@38278:               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
blanchet@38286:               |> map single
blanchet@38699:             val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
blanchet@38883:             val timer = Timer.startRealTimer ()
blanchet@38278:             val result =
blanchet@38883:               do_run false (if has_incomplete_mode then
blanchet@38883:                               Time.fromMilliseconds
blanchet@38883:                                          (2 * Time.toMilliseconds timeout div 3)
blanchet@38883:                             else
blanchet@38883:                               timeout)
blanchet@38883:               |> has_incomplete_mode
blanchet@38883:                  ? (fn (_, msecs0, _, SOME _) =>
blanchet@38883:                        do_run true
blanchet@38883:                               (Time.- (timeout, Timer.checkRealTimer timer))
blanchet@38883:                        |> (fn (output, msecs, proof, outcome) =>
blanchet@38883:                               (output, msecs0 + msecs, proof, outcome))
blanchet@38883:                      | result => result)
blanchet@38506:           in ((pool, conjecture_shape, axiom_names), result) end
blanchet@38278:         else
blanchet@38278:           error ("Bad executable: " ^ Path.implode command ^ ".")
blanchet@38257: 
blanchet@38257:     (* If the problem file has not been exported, remove it; otherwise, export
blanchet@38257:        the proof file too. *)
blanchet@38257:     fun cleanup probfile =
blanchet@38257:       if the_dest_dir = "" then try File.rm probfile else NONE
blanchet@38257:     fun export probfile (_, (output, _, _, _)) =
blanchet@38257:       if the_dest_dir = "" then
blanchet@38257:         ()
blanchet@38257:       else
blanchet@38257:         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
blanchet@38506:     val ((pool, conjecture_shape, axiom_names),
blanchet@38506:          (output, msecs, proof, outcome)) =
blanchet@38257:       with_path cleanup export run_on (prob_pathname subgoal)
blanchet@38506:     val (conjecture_shape, axiom_names) =
blanchet@38257:       repair_conjecture_shape_and_theorem_names output conjecture_shape
blanchet@38506:                                                 axiom_names
blanchet@38257:     val (message, used_thm_names) =
blanchet@38257:       case outcome of
blanchet@38257:         NONE =>
blanchet@38257:         proof_text isar_proof
blanchet@38257:             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
blanchet@38506:             (full_types, minimize_command, proof, axiom_names, th, subgoal)
blanchet@38983:         |>> (fn message =>
blanchet@38983:                 message ^ (if verbose then
blanchet@38983:                              "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
blanchet@38983:                            else
blanchet@38983:                              ""))
blanchet@38820:       | SOME failure => (string_for_failure failure, [])
blanchet@38257:   in
blanchet@38257:     {outcome = outcome, message = message, pool = pool,
blanchet@38257:      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
blanchet@38506:      output = output, proof = proof, axiom_names = axiom_names,
blanchet@38329:      conjecture_shape = conjecture_shape}
blanchet@38257:   end
blanchet@38257: 
blanchet@38257: fun get_prover_fun thy name = prover_fun name (get_prover thy name)
wenzelm@28586: 
blanchet@39226: fun start_prover_thread (params as {blocking, verbose, full_types, timeout,
blanchet@39229:                                     expect, ...})
blanchet@39226:                         i n relevance_override minimize_command proof_state
blanchet@38699:                         atp_name =
blanchet@36379:   let
blanchet@38257:     val thy = Proof.theory_of proof_state
blanchet@37584:     val birth_time = Time.now ()
blanchet@37584:     val death_time = Time.+ (birth_time, timeout)
blanchet@38699:     val prover = get_prover_fun thy atp_name
blanchet@36379:     val {context = ctxt, facts, goal} = Proof.goal proof_state;
blanchet@36379:     val desc =
blanchet@39229:       "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":" ^
blanchet@39229:       (if blocking then
blanchet@39229:          ""
blanchet@39229:        else
blanchet@39229:          "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
blanchet@39226:     fun run () =
blanchet@39226:       let
blanchet@39226:         val problem =
blanchet@39226:           {subgoal = i, goal = (ctxt, (facts, goal)),
blanchet@39226:            relevance_override = relevance_override, axioms = NONE}
blanchet@39229:         val (outcome_code, message) =
blanchet@39229:           prover params (minimize_command atp_name) problem
blanchet@39229:           |> (fn {outcome, message, ...} =>
blanchet@39229:                  (if is_some outcome then "none" else "some", message))
blanchet@39229:           handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
blanchet@39229:                | exn => ("unknown", "Internal error:\n" ^
blanchet@39229:                                     ML_Compiler.exn_message exn ^ "\n")
blanchet@39226:       in
blanchet@39229:         if expect = "" orelse outcome_code = expect then
blanchet@39229:           ()
blanchet@39229:         else if blocking then
blanchet@39229:           error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@39229:         else
blanchet@39229:           warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@39229:         message
blanchet@39226:       end
blanchet@37584:   in
blanchet@39229:     if blocking then priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
blanchet@39229:     else Async_Manager.launch das_Tool verbose birth_time death_time desc run
blanchet@37584:   end
wenzelm@28582: 
blanchet@38290: fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
blanchet@39226:   | run_sledgehammer (params as {blocking, atps, ...}) i relevance_override
blanchet@38290:                      minimize_command state =
blanchet@38290:     case subgoal_count state of
blanchet@38290:       0 => priority "No subgoal!"
blanchet@38290:     | n =>
blanchet@38290:       let
blanchet@38290:         val _ = kill_atps ()
blanchet@38290:         val _ = priority "Sledgehammering..."
blanchet@39226:         val _ =
blanchet@39226:           (if blocking then Par_List.map else map)
blanchet@39226:               (start_prover_thread params i n relevance_override
blanchet@39226:                                    minimize_command state) atps
blanchet@38290:       in () end
blanchet@38290: 
blanchet@38257: val setup =
blanchet@38257:   dest_dir_setup
blanchet@38257:   #> problem_prefix_setup
blanchet@38257:   #> measure_runtime_setup
blanchet@38257: 
wenzelm@28582: end;