# HG changeset patch # User blanchet # Date 1272015289 -7200 # Node ID 6767999e8f9ac9562f1fba11b41d78a339adebf6 # Parent c4f5823f282d5f5eff26544db9c6f56897b883bb# Parent b4c2043cc96c68a304c445d76891eea44235838d merged diff -r c4f5823f282d -r 6767999e8f9a src/HOL/Tools/ATP_Manager/SystemOnTPTP --- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Fri Apr 23 10:00:53 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Fri Apr 23 11:34:49 2010 +0200 @@ -123,7 +123,7 @@ $extract =~ s/\)\.cnf/\)\.\ncnf/g; print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n"; - # orientation for res_reconstruct.ML + # orientation for "sledgehammer_proof_reconstruct.ML" print "# SZS output start CNFRefutation.\n"; print "$extract\n"; print "# SZS output end CNFRefutation.\n"; diff -r c4f5823f282d -r 6767999e8f9a src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 10:00:53 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 11:34:49 2010 +0200 @@ -9,6 +9,7 @@ signature ATP_MANAGER = sig type relevance_override = Sledgehammer_Fact_Filter.relevance_override + type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = {debug: bool, verbose: bool, @@ -41,7 +42,8 @@ proof: string, internal_thm_names: string Vector.vector, filtered_clauses: (thm * (string * int)) list} - type prover = params -> Time.time -> problem -> prover_result + type prover = + params -> minimize_command -> Time.time -> problem -> prover_result val atps: string Unsynchronized.ref val timeout: int Unsynchronized.ref @@ -52,7 +54,9 @@ val add_prover: string * prover -> theory -> theory val get_prover: theory -> string -> prover option val available_atps: theory -> unit - val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit + val sledgehammer: + params -> int -> relevance_override -> (string -> minimize_command) + -> Proof.state -> unit end; structure ATP_Manager : ATP_MANAGER = @@ -62,7 +66,7 @@ open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct -(** parameters, problems, results, and provers **) +(** problems, results, provers, etc. **) type params = {debug: bool, @@ -99,7 +103,8 @@ internal_thm_names: string Vector.vector, filtered_clauses: (thm * (string * int)) list}; -type prover = params -> Time.time -> problem -> prover_result; +type prover = + params -> minimize_command -> Time.time -> problem -> prover_result (** preferences **) @@ -107,7 +112,7 @@ val message_store_limit = 20; val message_display_limit = 5; -val atps = Unsynchronized.ref "e spass remote_vampire"; +val atps = Unsynchronized.ref ""; (* set in "ATP_Wrapper" *) val timeout = Unsynchronized.ref 60; val full_types = Unsynchronized.ref false; @@ -323,12 +328,12 @@ val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (eq_snd op =) data - handle Symtab.DUP dup => err_dup_prover dup; + handle Symtab.DUP name => err_dup_prover name; ); fun add_prover (name, prover) thy = Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy - handle Symtab.DUP dup => err_dup_prover dup; + handle Symtab.DUP name => err_dup_prover name; fun get_prover thy name = Option.map #1 (Symtab.lookup (Provers.get thy) name); @@ -341,7 +346,7 @@ (* start prover thread *) fun start_prover (params as {timeout, ...}) birth_time death_time i - relevance_override proof_state name = + relevance_override minimize_command proof_state name = (case get_prover (Proof.theory_of proof_state) name of NONE => warning ("Unknown ATP: " ^ quote name ^ ".") | SOME prover => @@ -359,7 +364,8 @@ {subgoal = i, goal = (ctxt, (facts, goal)), relevance_override = relevance_override, axiom_clauses = NONE, filtered_clauses = NONE} - val message = #message (prover params timeout problem) + val message = + #message (prover params (minimize_command name) timeout problem) handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n [] | ERROR msg => "Error: " ^ msg ^ ".\n"; @@ -371,14 +377,15 @@ (* Sledgehammer the given subgoal *) fun sledgehammer (params as {atps, timeout, ...}) i relevance_override - proof_state = + minimize_command proof_state = let val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *) val _ = priority "Sledgehammering..." val _ = List.app (start_prover params birth_time death_time i - relevance_override proof_state) atps + relevance_override minimize_command + proof_state) atps in () end end; diff -r c4f5823f282d -r 6767999e8f9a src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 10:00:53 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 11:34:49 2010 +0200 @@ -78,13 +78,13 @@ axiom_clauses = SOME axclauses, filtered_clauses = SOME (the_default axclauses filtered_clauses)} in - `outcome_of_result (prover params timeout problem) + `outcome_of_result (prover params (K "") timeout problem) |>> tap (priority o string_of_outcome) end (* minimalization of thms *) -fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus, +fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus, sorts, ...}) prover atp_name i state name_thms_pairs = let @@ -122,8 +122,8 @@ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") in (SOME min_thms, - proof_text isar_proof true modulus sorts atp_name proof - internal_thm_names ctxt goal i |> fst) + proof_text isar_proof debug modulus sorts ctxt + (K "", proof, internal_thm_names, goal, i) |> fst) end | (Timeout, _) => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ diff -r c4f5823f282d -r 6767999e8f9a src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 10:00:53 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 11:34:49 2010 +0200 @@ -43,13 +43,15 @@ (* prover configuration *) +val remotify = prefix "remote_" + type prover_config = - {command: Path.T, + {home: string, + executable: string, arguments: Time.time -> string, known_failures: (string list * string) list, max_new_clauses: int, - prefers_theory_relevant: bool, - supports_isar_proofs: bool}; + prefers_theory_relevant: bool}; (* basic template *) @@ -71,8 +73,10 @@ else "Error: The ATP output is ill-formed." | (message :: _) => message -fun generic_prover overlord get_facts prepare write_file cmd args known_failures - proof_text name ({debug, full_types, explicit_apply, ...} : params) +fun generic_prover overlord get_facts prepare write_file home executable args + known_failures name + ({debug, full_types, explicit_apply, isar_proof, modulus, sorts, ...} + : params) minimize_command ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -105,18 +109,29 @@ in if destdir' = "" then File.tmp_path probfile else if File.exists (Path.explode destdir') - then Path.append (Path.explode destdir') probfile + then Path.append (Path.explode destdir') probfile else error ("No such directory: " ^ destdir' ^ ".") end; + val command = Path.explode (home ^ "/" ^ executable) (* write out problem file and call prover *) - fun cmd_line probfile = - if Config.get ctxt measure_runtime then - "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd, - args, File.shell_path probfile] ^ " ; } 2>&1" - else - space_implode " " ["exec", File.shell_path cmd, args, - File.shell_path probfile, "2>&1"]; + fun command_line probfile = + (if Config.get ctxt measure_runtime then + "TIMEFORMAT='%3U'; { time " ^ + space_implode " " [File.shell_path command, args, + File.shell_path probfile] ^ " ; } 2>&1" + else + space_implode " " ["exec", File.shell_path command, args, + File.shell_path probfile, "2>&1"]) ^ + (if overlord then + " | sed 's/,/, /g' \ + \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \ + \| sed 's/! =/ !=/g' \ + \| sed 's/ / /g' | sed 's/| |/||/g' \ + \| sed 's/ = = =/===/g' \ + \| sed 's/= = /== /g'" + else + "") fun split_time s = let val split = String.tokens (fn c => str c = "\n"); @@ -131,10 +146,10 @@ fun split_time' s = if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = - if File.exists cmd then + if File.exists command then write_file full_types explicit_apply probfile clauses - |> pair (apfst split_time' (bash_output (cmd_line probfile))) - else error ("Bad executable: " ^ Path.implode cmd ^ "."); + |> pair (apfst split_time' (bash_output (command_line probfile))) + else error ("Bad executable: " ^ Path.implode command ^ "."); (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) @@ -144,7 +159,11 @@ () else File.write (Path.explode (Path.implode probfile ^ "_proof")) - ("% " ^ timestamp () ^ "\n" ^ proof) + ((if overlord then + "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^ + "\n" + else + "") ^ proof) val (((proof, atp_run_time_in_msecs), rc), _) = with_path cleanup export run_on (prob_pathname subgoal); @@ -154,9 +173,10 @@ val success = rc = 0 andalso failure = ""; val (message, relevant_thm_names) = if success then - proof_text name proof internal_thm_names ctxt th subgoal + proof_text isar_proof debug modulus sorts ctxt + (minimize_command, proof, internal_thm_names, th, subgoal) else if failure <> "" then - (failure, []) + (failure ^ "\n", []) else ("Unknown ATP error: " ^ proof ^ ".\n", []) in @@ -171,21 +191,19 @@ (* generic TPTP-based provers *) fun generic_tptp_prover - (name, {command, arguments, known_failures, max_new_clauses, - prefers_theory_relevant, supports_isar_proofs}) + (name, {home, executable, arguments, known_failures, max_new_clauses, + prefers_theory_relevant}) (params as {debug, overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, - isar_proof, modulus, sorts, ...}) - timeout = + isar_proof, ...}) + minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order false) - (write_tptp_file (debug andalso overlord andalso not isar_proof)) command - (arguments timeout) known_failures - (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts) - name params + (write_tptp_file (debug andalso overlord andalso not isar_proof)) home + executable (arguments timeout) known_failures name params minimize_command fun tptp_prover name p = (name, generic_tptp_prover (name, p)); @@ -196,10 +214,11 @@ (* Vampire *) -(* NB: Vampire does not work without explicit time limit. *) +(* Vampire requires an explicit time limit. *) val vampire_config : prover_config = - {command = Path.explode "$VAMPIRE_HOME/vampire", + {home = getenv "VAMPIRE_HOME", + executable = "vampire", arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^ string_of_int (generous_to_secs timeout)), known_failures = @@ -208,15 +227,15 @@ (["Refutation not found"], "The ATP failed to determine the problem's status.")], max_new_clauses = 60, - prefers_theory_relevant = false, - supports_isar_proofs = true} + prefers_theory_relevant = false} val vampire = tptp_prover "vampire" vampire_config (* E prover *) val e_config : prover_config = - {command = Path.explode "$E_HOME/eproof", + {home = getenv "E_HOME", + executable = "eproof", arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \ \-tAutoDev --silent --cpu-limit=" ^ string_of_int (generous_to_secs timeout)), @@ -228,44 +247,42 @@ (["# Cannot determine problem status"], "The ATP failed to determine the problem's status.")], max_new_clauses = 100, - prefers_theory_relevant = false, - supports_isar_proofs = true} + prefers_theory_relevant = false} val e = tptp_prover "e" e_config (* SPASS *) fun generic_dfg_prover - (name, ({command, arguments, known_failures, max_new_clauses, - prefers_theory_relevant, ...} : prover_config)) + (name, {home, executable, arguments, known_failures, max_new_clauses, + prefers_theory_relevant}) (params as {overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, ...}) - timeout = + minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses higher_order true) write_dfg_file command - (arguments timeout) known_failures (metis_proof_text false false) - name params + (prepare_clauses higher_order true) write_dfg_file home executable + (arguments timeout) known_failures name params minimize_command fun dfg_prover name p = (name, generic_dfg_prover (name, p)) (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) val spass_config : prover_config = - {command = Path.explode "$SPASS_HOME/SPASS", - arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ - " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^ - string_of_int (generous_to_secs timeout)), - known_failures = - [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."), - (["SPASS beiseite: Ran out of time."], "The ATP timed out."), - (["SPASS beiseite: Maximal number of loops exceeded."], - "The ATP hit its loop limit.")], - max_new_clauses = 40, - prefers_theory_relevant = true, - supports_isar_proofs = false} + {home = getenv "SPASS_HOME", + executable = "SPASS", + arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ + " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^ + string_of_int (generous_to_secs timeout)), + known_failures = + [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."), + (["SPASS beiseite: Ran out of time."], "The ATP timed out."), + (["SPASS beiseite: Maximal number of loops exceeded."], + "The ATP hit its loop limit.")], + max_new_clauses = 40, + prefers_theory_relevant = true} val spass = dfg_prover "spass" spass_config (* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0 @@ -277,7 +294,8 @@ page once the package is there (around the Isabelle2010 release). *) val spass_tptp_config = - {command = #command spass_config, + {home = #home spass_config, + executable = #executable spass_config, arguments = prefix "-TPTP " o #arguments spass_config, known_failures = #known_failures spass_config @ @@ -291,8 +309,7 @@ map Path.basic ["etc", "components"]))) ^ "\" on a line of its own.")], max_new_clauses = #max_new_clauses spass_config, - prefers_theory_relevant = #prefers_theory_relevant spass_config, - supports_isar_proofs = #supports_isar_proofs spass_config} + prefers_theory_relevant = #prefers_theory_relevant spass_config} val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config (* remote prover invocation via SystemOnTPTP *) @@ -328,27 +345,29 @@ fun remote_prover_config prover_prefix args ({known_failures, max_new_clauses, prefers_theory_relevant, ...} : prover_config) : prover_config = - {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", + {home = getenv "ISABELLE_ATP_MANAGER", + executable = "SystemOnTPTP", arguments = (fn timeout => args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^ the_system prover_prefix), known_failures = remote_known_failures @ known_failures, max_new_clauses = max_new_clauses, - prefers_theory_relevant = prefers_theory_relevant, - supports_isar_proofs = false} + prefers_theory_relevant = prefers_theory_relevant} val remote_vampire = - tptp_prover "remote_vampire" + tptp_prover (remotify (fst vampire)) (remote_prover_config "Vampire---9" "" vampire_config) val remote_e = - tptp_prover "remote_e" (remote_prover_config "EP---" "" e_config) + tptp_prover (remotify (fst e)) + (remote_prover_config "EP---" "" e_config) val remote_spass = - tptp_prover "remote_spass" (remote_prover_config "SPASS---" "-x" spass_config) + tptp_prover (remotify (fst spass)) + (remote_prover_config "SPASS---" "-x" spass_config) -val provers = [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, - remote_e] +val provers = + [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e] val prover_setup = fold add_prover provers val setup = @@ -357,4 +376,9 @@ #> measure_runtime_setup #> prover_setup; +fun maybe_remote (name, _) ({home, ...} : prover_config) = + name |> home = "" ? remotify + +val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config, + remotify (fst vampire)] |> space_implode " ") end; diff -r c4f5823f282d -r 6767999e8f9a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 10:00:53 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 11:34:49 2010 +0200 @@ -68,6 +68,10 @@ ("metis_proof", "isar_proof"), ("no_sorts", "sorts")] +val params_for_minimize = + ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus", + "sorts", "minimize_timeout"] + val property_dependent_params = ["atps", "full_types", "timeout"] fun is_known_raw_param s = @@ -98,19 +102,11 @@ val extend = I fun merge p : T = AList.merge (op =) (K true) p) -(* Don't even try to start ATPs that are not installed. - Hack: Should not rely on naming convention. *) -val filter_atps = - space_explode " " - #> filter (fn s => String.isPrefix "remote_" s orelse - getenv (String.map Char.toUpper s ^ "_HOME") <> "") - #> space_implode " " - val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param fun default_raw_params thy = Data.get thy |> fold (AList.default (op =)) - [("atps", [filter_atps (!atps)]), + [("atps", [!atps]), ("full_types", [if !full_types then "true" else "false"]), ("timeout", let val timeout = !timeout in [if timeout <= 0 then "none" @@ -219,18 +215,33 @@ val refresh_tptpN = "refresh_tptp" val helpN = "help" - fun minimizize_raw_param_name "timeout" = "minimize_timeout" | minimizize_raw_param_name name = name +val is_raw_param_relevant_for_minimize = + member (op =) params_for_minimize o fst o unalias_raw_param +fun string_for_raw_param (key, values) = + key ^ (case space_implode " " values of + "" => "" + | value => " = " ^ value) + +fun minimize_command override_params i atp_name facts = + "sledgehammer minimize [atp = " ^ atp_name ^ + (override_params |> filter is_raw_param_relevant_for_minimize + |> implode o map (prefix ", " o string_for_raw_param)) ^ + "] (" ^ space_implode " " facts ^ ")" ^ + (if i = 1 then "" else " " ^ string_of_int i) + fun hammer_away override_params subcommand opt_i relevance_override state = let val thy = Proof.theory_of state val _ = List.app check_raw_param override_params in if subcommand = runN then - sledgehammer (get_params thy override_params) (the_default 1 opt_i) - relevance_override state + let val i = the_default 1 opt_i in + sledgehammer (get_params thy override_params) i relevance_override + (minimize_command override_params i) state + end else if subcommand = minimizeN then minimize (map (apfst minimizize_raw_param_name) override_params) [] (the_default 1 opt_i) (#add relevance_override) state diff -r c4f5823f282d -r 6767999e8f9a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 23 10:00:53 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 23 11:34:49 2010 +0200 @@ -6,6 +6,8 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig + type minimize_command = string list -> string + val chained_hint: string val invert_const: string -> string val invert_type_const: string -> string @@ -15,14 +17,16 @@ val is_proof_well_formed: string -> bool val metis_line: int -> int -> string list -> string val metis_proof_text: - bool -> bool -> string -> string -> string vector -> Proof.context -> thm - -> int -> string * string list + minimize_command * string * string vector * thm * int + -> string * string list val isar_proof_text: - bool -> int -> bool -> string -> string -> string vector -> Proof.context - -> thm -> int -> string * string list + bool -> int -> bool -> Proof.context + -> minimize_command * string * string vector * thm * int + -> string * string list val proof_text: - bool -> bool -> int -> bool -> string -> string -> string vector - -> Proof.context -> thm -> int -> string * string list + bool -> bool -> int -> bool -> Proof.context + -> minimize_command * string * string vector * thm * int + -> string * string list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -31,6 +35,8 @@ open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor +type minimize_command = string list -> string + val trace_proof_path = Path.basic "atp_trace"; fun trace_proof_msg f = @@ -38,9 +44,13 @@ fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" + +fun is_axiom thm_names line_no = line_no <= Vector.length thm_names + (**** PARSING OF TSTP FORMAT ****) -(*Syntax trees, either termlist or formulae*) +(* Syntax trees, either term list or formulae *) datatype stree = Int of int | Br of string * stree list; fun atom x = Br(x,[]); @@ -49,48 +59,88 @@ val listof = List.foldl scons (atom "nil"); (*Strings enclosed in single quotes, e.g. filenames*) -val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode; +val quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode; (*Intended for $true and $false*) fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE); -val truefalse = $$"$" |-- Symbol.scan_id >> (atom o tf); +val truefalse = $$ "$" |-- Symbol.scan_id >> (atom o tf); (*Integer constants, typically proof line numbers*) fun is_digit s = Char.isDigit (String.sub(s,0)); val integer = Scan.many1 is_digit >> (the o Int.fromString o implode); +(* needed for SPASS's nonstandard output format *) +fun smart_Br ("equal", ts) = Br ("c_equal", rev ts) + | smart_Br p = Br p + (*Generalized FO terms, which include filenames, numbers, etc.*) -fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x -and term x = (quoted >> atom || integer>>Int || truefalse || - Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br || - $$"(" |-- term --| $$")" || - $$"[" |-- Scan.optional termlist [] --| $$"]" >> listof) x; +fun term x = (quoted >> atom || integer >> Int || truefalse + || Symbol.scan_id + -- Scan.optional ($$ "(" |-- terms --| $$ ")") [] >> smart_Br + || $$ "(" |-- term --| $$ ")" + || $$ "[" |-- Scan.optional terms [] --| $$ "]" >> listof) x +and terms x = (term ::: Scan.repeat ($$ "," |-- term)) x -fun negate t = Br("c_Not", [t]); -fun equate (t1,t2) = Br("c_equal", [t1,t2]); +fun negate t = Br ("c_Not", [t]) +fun equate t1 t2 = Br ("c_equal", [t1, t2]); (*Apply equal or not-equal to a term*) fun syn_equal (t, NONE) = t - | syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2) - | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2)); + | syn_equal (t1, SOME (NONE, t2)) = equate t1 t2 + | syn_equal (t1, SOME (SOME _, t2)) = negate (equate t1 t2) (*Literals can involve negation, = and !=.*) -fun literal x = ($$"~" |-- literal >> negate || - (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x; +fun literal x = + ($$ "~" |-- literal >> negate + || (term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- term) + >> syn_equal)) x -val literals = literal ::: Scan.repeat ($$"|" |-- literal); +val literals = literal ::: Scan.repeat ($$ "|" |-- literal); (*Clause: a list of literals separated by the disjunction sign*) -val clause = $$"(" |-- literals --| $$")" || Scan.single literal; +val clause = $$ "(" |-- literals --| $$ ")" || Scan.single literal; + +fun ints_of_stree (Int n) = cons n + | ints_of_stree (Br (_, ts)) = fold ints_of_stree ts + +val tstp_annotations = + Scan.optional ($$ "," |-- term --| Scan.option ($$ "," |-- terms) + >> (fn source => ints_of_stree source [])) [] + +fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps) -val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist); +(* ::= cnf(, , ). + The could be an identifier, but we assume integers. *) +val parse_tstp_line = + (Scan.this_string "cnf" -- $$ "(") |-- integer --| $$ "," --| Symbol.scan_id + --| $$ "," -- clause -- tstp_annotations --| $$ ")" --| $$ "." + >> retuple_tstp_line + +(**** PARSING OF SPASS OUTPUT ****) + +val dot_name = integer --| $$ "." --| integer -(* ::= cnf(,,). - The could be an identifier, but we assume integers.*) -val tstp_line = (Scan.this_string "cnf" -- $$"(") |-- - integer --| $$"," -- Symbol.scan_id --| $$"," -- - clause -- Scan.option annotations --| $$ ")"; +val spass_annotations = + Scan.optional ($$ ":" |-- Scan.repeat (dot_name --| Scan.option ($$ ","))) [] + +val starred_literal = literal --| Scan.repeat ($$ "*" || $$ " ") + +val horn_clause = + Scan.repeat starred_literal --| $$ "-" --| $$ ">" + -- Scan.repeat starred_literal + >> (fn ([], []) => [atom (tf "false")] + | (clauses1, clauses2) => map negate clauses1 @ clauses2) +fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps) + +(* Syntax: [0:] || -> **. *) +val parse_spass_proof_line = + integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id + -- spass_annotations --| $$ "]" --| $$ "|" --| $$ "|" -- horn_clause + --| $$ "." + >> retuple_spass_proof_line + +val parse_proof_line = fst o (parse_tstp_line || parse_spass_proof_line) (**** INTERPRETATION OF TSTP SYNTAX TREES ****) @@ -111,7 +161,8 @@ SOME c' => c' | NONE => c; -fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS); +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS); +fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS) fun make_var (b,T) = Var((b,0),T); (*Type variables are given the basic sort, HOL.type. Some will later be constrained @@ -132,7 +183,7 @@ | NONE => case strip_prefix tvar_prefix a of SOME b => make_tvar b - | NONE => make_tvar a (*Variable from the ATP, say X1*) + | NONE => make_tparam a (* Variable from the ATP, say "X1" *) end; (*Invert the table of translations between Isabelle and ATPs*) @@ -178,7 +229,7 @@ | NONE => case strip_prefix schematic_var_prefix a of SOME b => make_var (b,T) - | NONE => make_var (a,T) (*Variable from the ATP, say X1*) + | NONE => make_var (a,T) (* Variable from the ATP, say "X1" *) in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; (*Type class literal applied to a type. Returns triple of polarity, class, type.*) @@ -226,32 +277,21 @@ | tmsubst (t as Bound _) = t | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t) | tmsubst (t $ u) = tmsubst t $ tmsubst u; - in fn t => if Vartab.is_empty vt then t else tmsubst t end; + in not (Vartab.is_empty vt) ? tmsubst end; (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. vt0 holds the initial sort constraints, from the conjecture clauses.*) fun clause_of_strees ctxt vt0 ts = let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt)) - end; + end fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t; -fun ints_of_stree_aux (Int n, ns) = n::ns - | ints_of_stree_aux (Br(_,ts), ns) = List.foldl ints_of_stree_aux ns ts; - -fun ints_of_stree t = ints_of_stree_aux (t, []); - -fun decode_tstp vt0 (name, role, ts, annots) ctxt = - let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source - val cl = clause_of_strees ctxt vt0 ts - in ((name, role, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) end; - -fun dest_tstp ((((name, role), ts), annots), chs) = - case chs of - "."::_ => (name, role, ts, annots) - | _ => error ("TSTP line not terminated by \".\": " ^ implode chs); - +fun decode_proof_step vt0 (name, ts, deps) ctxt = + let val cl = clause_of_strees ctxt vt0 ts in + ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) + end (** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **) @@ -268,9 +308,10 @@ (**** Translation of TSTP files to Isar Proofs ****) -fun decode_tstp_list ctxt tuples = - let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples) - in #1 (fold_map (decode_tstp vt0) tuples ctxt) end; +fun decode_proof_steps ctxt tuples = + let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in + #1 (fold_map (decode_proof_step vt0) tuples ctxt) + end (** Finding a matching assumption. The literals may be permuted, and variable names may disagree. We have to try all combinations of literals (quadratic!) and @@ -342,9 +383,10 @@ fun have_or_show "show" _ = " show \"" | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \"" fun do_line _ (lname, t, []) = - (* No deps: it's a conjecture clause, with no proof. *) + (* No depedencies: it's a conjecture clause, with no proof. *) (case permuted_clause t ctms of SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" + | NONE => " assume? " ^ lname ^ ": \"" ^ string_of_term t ^ "\"\n" | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body", [t])) | do_line have (lname, t, deps) = @@ -368,17 +410,21 @@ (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ only in type information.*) -fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*) - if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*) - then map (replace_deps (lno, [])) lines +fun add_proof_line thm_names (lno, t, []) lines = + (* No dependencies: axiom or conjecture clause *) + if is_axiom thm_names lno then + (* Axioms are not proof lines *) + if eq_types t then + (* Must be clsrel/clsarity: type information, so delete refs to it *) + map (replace_deps (lno, [])) lines + else + (case take_prefix (unequal t) lines of + (_,[]) => lines (*no repetition of proof line*) + | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*) + pre @ map (replace_deps (lno', [lno])) post) else - (case take_prefix (unequal t) lines of - (_,[]) => lines (*no repetition of proof line*) - | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*) - pre @ map (replace_deps (lno', [lno])) post) - | add_prfline ((lno, _, t, []), lines) = (*no deps: conjecture clause*) - (lno, t, []) :: lines - | add_prfline ((lno, _, t, deps), lines) = + (lno, t, []) :: lines + | add_proof_line _ (lno, t, deps) lines = if eq_types t then (lno, t, deps) :: lines (*Type information will be deleted later; skip repetition test.*) else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) @@ -417,12 +463,12 @@ (*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*) fun stringify_deps thm_names deps_map [] = [] | stringify_deps thm_names deps_map ((lno, t, deps) :: lines) = - if lno <= Vector.length thm_names (*axiom*) - then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines + if is_axiom thm_names lno then + (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines else let val lname = Int.toString (length deps_map) - fun fix lno = if lno <= Vector.length thm_names + fun fix lno = if is_axiom thm_names lno then SOME(Vector.sub(thm_names,lno-1)) - else AList.lookup op= deps_map lno; + else AList.lookup (op =) deps_map lno; in (lname, t, map_filter fix (distinct (op=) deps)) :: stringify_deps thm_names ((lno,lname)::deps_map) lines end; @@ -435,14 +481,15 @@ fun isar_proof_end 1 = "qed" | isar_proof_end _ = "next" -fun isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names = +fun isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names = let - val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n") - val tuples = map (dest_tstp o tstp_line o explode) cnfs + val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n") + val tuples = map (parse_proof_line o explode) cnfs val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n") val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt - val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) + val raw_lines = + fold_rev (add_proof_line thm_names) (decode_proof_steps ctxt tuples) [] val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n") val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines @@ -460,12 +507,12 @@ val body = isar_proof_body ctxt sorts (map prop_of ccls) (stringify_deps thm_names [] lines) val n = Logic.count_prems (prop_of goal) - val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n") + val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: finishing\n") in isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^ isar_proof_end n ^ "\n" end - handle STREE _ => error "Could not extract proof (ATP output malformed?)"; + handle STREE _ => raise Fail "Cannot parse ATP output"; (*=== EXTRACTING PROOF-TEXT === *) @@ -479,23 +526,19 @@ "Formulae used in the proof"]; fun get_proof_extract proof = - let - (*splits to_split by the first possible of a list of splitters*) - val (begin_string, end_string) = - (find_first (fn s => String.isSubstring s proof) begin_proof_strs, - find_first (fn s => String.isSubstring s proof) end_proof_strs) - in - if is_none begin_string orelse is_none end_string - then error "Could not extract proof (no substring indicating a proof)" - else proof |> first_field (the begin_string) |> the |> snd - |> first_field (the end_string) |> the |> fst - end; + (* Splits by the first possible of a list of splitters. *) + case pairself (find_first (fn s => String.isSubstring s proof)) + (begin_proof_strs, end_proof_strs) of + (SOME begin_string, SOME end_string) => + proof |> first_field begin_string |> the |> snd + |> first_field end_string |> the |> fst + | _ => raise Fail "Cannot extract proof" (* ==== CHECK IF PROOF WAS SUCCESSFUL === *) fun is_proof_well_formed proof = - exists (fn s => String.isSubstring s proof) begin_proof_strs andalso - exists (fn s => String.isSubstring s proof) end_proof_strs + forall (exists (fn s => String.isSubstring s proof)) + [begin_proof_strs, end_proof_strs] (* === EXTRACTING LEMMAS === *) (* A list consisting of the first number in each line is returned. @@ -505,11 +548,11 @@ extracted. *) fun get_step_nums proof_extract = let - val toks = String.tokens (not o Char.isAlphaNum) + val toks = String.tokens (not o is_ident_char) fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok - | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) = + | inputno ("cnf" :: ntok :: "negated_conjecture" :: _) = Int.fromString ntok - | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *) + | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG format *) | inputno _ = NONE val lines = split_lines proof_extract in map_filter (inputno o toks) lines end @@ -528,55 +571,76 @@ fun metis_line i n xs = "Try this command: " ^ Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" -fun minimize_line _ _ [] = "" - | minimize_line isar_proof atp_name xs = +fun minimize_line _ [] = "" + | minimize_line minimize_command facts = + case minimize_command facts of + "" => "" + | command => "To minimize the number of lemmas, try this command: " ^ - Markup.markup Markup.sendback - ("sledgehammer minimize [atp = " ^ atp_name ^ - (if isar_proof then ", isar_proof" else "") ^ "] (" ^ - space_implode " " xs ^ ")") ^ ".\n" + Markup.markup Markup.sendback command ^ ".\n" -fun metis_proof_text isar_proof minimal atp_name proof thm_names - (_ : Proof.context) goal i = +fun metis_proof_text (minimize_command, proof, thm_names, goal, i) = let val lemmas = proof |> get_proof_extract |> get_step_nums - |> filter (fn i => i <= Vector.length thm_names) + |> filter (is_axiom thm_names) |> map (fn i => Vector.sub (thm_names, i - 1)) |> filter (fn x => x <> "??.unknown") |> sort_distinct string_ord val n = Logic.count_prems (prop_of goal) val xs = kill_chained lemmas in - (metis_line i n xs ^ - (if minimal then "" else minimize_line isar_proof atp_name xs), - kill_chained lemmas) + (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas) end -fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i = +val is_proof_line = String.isPrefix "cnf(" orf String.isSubstring "||" + +fun do_space c = if Char.isSpace c then "" else str c + +fun strip_spaces_in_list [] = "" + | strip_spaces_in_list [c1] = do_space c1 + | strip_spaces_in_list [c1, c2] = do_space c1 ^ do_space c2 + | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = + if Char.isSpace c1 then + strip_spaces_in_list (c2 :: c3 :: cs) + else if Char.isSpace c2 then + if Char.isSpace c3 then + strip_spaces_in_list (c1 :: c3 :: cs) + else + str c1 ^ + (if is_ident_char c1 andalso is_ident_char c3 then " " else "") ^ + strip_spaces_in_list (c3 :: cs) + else + str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) + +val strip_spaces = strip_spaces_in_list o String.explode + +fun isar_proof_text debug modulus sorts ctxt + (minimize_command, proof, thm_names, goal, i) = let - (* We could use "split_lines", but it can return blank lines. *) - val lines = String.tokens (equal #"\n"); - val kill_spaces = - String.translate (fn c => if Char.isSpace c then "" else str c) - val extract = get_proof_extract proof - val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) + val cnfs = proof |> get_proof_extract |> split_lines |> map strip_spaces + |> filter is_proof_line val (one_line_proof, lemma_names) = - metis_proof_text true minimal atp_name proof thm_names ctxt goal i + metis_proof_text (minimize_command, proof, thm_names, goal, i) val tokens = String.tokens (fn c => c = #" ") one_line_proof + fun isar_proof_for () = + case isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names of + "" => "" + | isar_proof => + "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof val isar_proof = - if member (op =) tokens chained_hint then "" - else isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names - in - (one_line_proof ^ - (if isar_proof = "" then "" - else "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof), - lemma_names) - end + if member (op =) tokens chained_hint then + "" + else if debug then + isar_proof_for () + else + try isar_proof_for () + |> the_default "Warning: The Isar proof construction failed.\n" + in (one_line_proof ^ isar_proof, lemma_names) end -fun proof_text isar_proof minimal modulus sorts = - if isar_proof then isar_proof_text minimal modulus sorts - else metis_proof_text isar_proof minimal +fun proof_text isar_proof debug modulus sorts ctxt = + if isar_proof then isar_proof_text debug modulus sorts ctxt + else metis_proof_text end;