# HG changeset patch # User blanchet # Date 1280248390 -7200 # Node ID 962b0a7f544b152c65e7b275f43f987f8c9e6cf2 # Parent d9c4d87838f31a1338026fc005b95c0d24a98515 more refactoring diff -r d9c4d87838f3 -r 962b0a7f544b src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue Jul 27 17:58:30 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Tue Jul 27 18:33:10 2010 +0200 @@ -20,8 +20,8 @@ ("Tools/ATP_Manager/atp_problem.ML") ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") ("Tools/ATP_Manager/async_manager.ML") - ("Tools/ATP_Manager/atp_manager.ML") ("Tools/ATP_Manager/atp_systems.ML") + ("Tools/Sledgehammer/sledgehammer.ML") ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML") ("Tools/Sledgehammer/sledgehammer_isar.ML") begin @@ -97,9 +97,10 @@ use "Tools/ATP_Manager/atp_problem.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" use "Tools/ATP_Manager/async_manager.ML" -use "Tools/Sledgehammer/sledgehammer.ML" use "Tools/ATP_Manager/atp_systems.ML" setup ATP_Systems.setup +use "Tools/Sledgehammer/sledgehammer.ML" +setup Sledgehammer.setup use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML" use "Tools/Sledgehammer/sledgehammer_isar.ML" setup Metis_Tactics.setup diff -r d9c4d87838f3 -r 962b0a7f544b src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 17:58:30 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 18:33:10 2010 +0200 @@ -7,9 +7,23 @@ signature ATP_SYSTEMS = sig - val dest_dir : string Config.T - val problem_prefix : string Config.T - val measure_runtime : bool Config.T + datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | + OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError + + type prover_config = + {home_var: string, + executable: string, + arguments: bool -> Time.time -> string, + proof_delims: (string * string) list, + known_failures: (failure * string) list, + max_new_relevant_facts_per_iter: int, + prefers_theory_relevant: bool, + explicit_forall: bool} + + val add_prover: string * prover_config -> theory -> theory + val get_prover: theory -> string -> prover_config + val available_atps: theory -> unit val refresh_systems_on_tptp : unit -> unit val default_atps_param_value : unit -> string val setup : theory -> theory @@ -18,28 +32,11 @@ structure ATP_Systems : ATP_SYSTEMS = struct -open Metis_Clauses -open Sledgehammer_Util -open Sledgehammer_Fact_Filter -open ATP_Problem -open Sledgehammer_Proof_Reconstruct -open Sledgehammer - -(** generic ATP **) - -(* external problem files *) +(* prover configuration *) -val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); - (*Empty string means create files in Isabelle's temporary files directory.*) - -val (problem_prefix, problem_prefix_setup) = - Attrib.config_string "atp_problem_prefix" (K "prob"); - -val (measure_runtime, measure_runtime_setup) = - Attrib.config_bool "atp_measure_runtime" (K false); - - -(* prover configuration *) +datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | + OldSpass | MalformedInput | MalformedOutput | UnknownError type prover_config = {home_var: string, @@ -52,728 +49,32 @@ explicit_forall: bool} -(* basic template *) - -val remotify = prefix "remote_" - -fun with_path cleanup after f path = - Exn.capture f path - |> tap (fn _ => cleanup path) - |> Exn.release - |> tap (after path) - -(* Splits by the first possible of a list of delimiters. *) -fun extract_proof delims output = - case pairself (find_first (fn s => String.isSubstring s output)) - (ListPair.unzip delims) of - (SOME begin_delim, SOME end_delim) => - (output |> first_field begin_delim |> the |> snd - |> first_field end_delim |> the |> fst - |> first_field "\n" |> the |> snd - handle Option.Option => "") - | _ => "" - -fun extract_proof_and_outcome complete res_code proof_delims known_failures - output = - case map_filter (fn (failure, pattern) => - if String.isSubstring pattern output then SOME failure - else NONE) known_failures of - [] => (case extract_proof proof_delims output of - "" => ("", SOME UnknownError) - | proof => if res_code = 0 then (proof, NONE) - else ("", SOME UnknownError)) - | (failure :: _) => - ("", SOME (if failure = IncompleteUnprovable andalso complete then - Unprovable - else - failure)) - -fun string_for_failure Unprovable = "The ATP problem is unprovable." - | string_for_failure IncompleteUnprovable = - "The ATP cannot prove the problem." - | string_for_failure CantConnect = "Can't connect to remote ATP." - | string_for_failure TimedOut = "Timed out." - | string_for_failure OutOfResources = "The ATP ran out of resources." - | string_for_failure OldSpass = - (* FIXME: Change the error message below to point to the Isabelle download - page once the package is there. *) - "Warning: Sledgehammer requires a more recent version of SPASS with \ - \support for the TPTP syntax. To install it, download and untar the \ - \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \ - \\"spass-3.7\" directory's full path to \"" ^ - Path.implode (Path.expand (Path.appends - (Path.variable "ISABELLE_HOME_USER" :: - map Path.basic ["etc", "components"]))) ^ - "\" on a line of its own." - | string_for_failure MalformedInput = - "Internal Sledgehammer error: The ATP problem is malformed. Please report \ - \this to the Isabelle developers." - | string_for_failure MalformedOutput = "Error: The ATP output is malformed." - | string_for_failure UnknownError = "Error: An unknown ATP error occurred." - - -(* Clause preparation *) - -datatype fol_formula = - FOLFormula of {formula_name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} - -fun mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) -fun mk_ahorn [] phi = phi - | mk_ahorn (phi :: phis) psi = - AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) - -(* ### FIXME: reintroduce -fun make_clause_table xs = - fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty -(* Remove existing axiom clauses from the conjecture clauses, as this can - dramatically boost an ATP's performance (for some reason). *) -fun subtract_cls ax_clauses = - filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) -*) - -fun combformula_for_prop thy = - let - val do_term = combterm_from_term thy - fun do_quant bs q s T t' = - do_formula ((s, T) :: bs) t' - #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) - and do_conn bs c t1 t2 = - do_formula bs t1 ##>> do_formula bs t2 - #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) - and do_formula bs t = - case t of - @{const Not} $ t1 => - do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) - | Const (@{const_name All}, _) $ Abs (s, T, t') => - do_quant bs AForall s T t' - | Const (@{const_name Ex}, _) $ Abs (s, T, t') => - do_quant bs AExists s T t' - | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 - | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 - | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 - | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - do_conn bs AIff t1 t2 - | _ => (fn ts => do_term bs (Envir.eta_contract t) - |>> APred ||> union (op =) ts) - in do_formula [] end - -(* Converts an elim-rule into an equivalent theorem that does not have the - predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_term" in - "ATP_Systems".) *) -(* FIXME: test! *) -fun transform_elim_term t = - case Logic.strip_imp_concl t of - @{const Trueprop} $ Var (z, @{typ bool}) => - subst_Vars [(z, @{const True})] t - | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t - | _ => t - -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_theorem" in "Clausifier".) *) -fun extensionalize_term t = - let - fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _])) - $ t2 $ Abs (s, var_T, t')) = - let val var_t = Var (("x", j), var_T) in - Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT) - $ betapply (t2, var_t) $ subst_bound (var_t, t') - |> aux (j + 1) - end - | aux _ t = t - in aux (maxidx_of_term t + 1) t end - -(* FIXME: Guarantee freshness *) -fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j -fun conceal_bounds Ts t = - subst_bounds (map (Free o apfst concealed_bound_name) - (length Ts - 1 downto 0 ~~ rev Ts), t) -fun reveal_bounds Ts = - subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) - (0 upto length Ts - 1 ~~ Ts)) +(* named provers *) -fun introduce_combinators_in_term ctxt kind t = - let - val thy = ProofContext.theory_of ctxt - fun aux Ts t = - case t of - @{const Not} $ t1 => @{const Not} $ aux Ts t1 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) - $ t1 $ t2 => - t0 $ aux Ts t1 $ aux Ts t2 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then - t - else - let - val t = t |> conceal_bounds Ts - |> Envir.eta_contract - val ([t], ctxt') = Variable.import_terms true [t] ctxt - in - t |> cterm_of thy - |> Clausifier.introduce_combinators_in_cterm - |> singleton (Variable.export ctxt' ctxt) - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts - end - in t |> not (Meson.is_fol_term thy t) ? aux [] end - handle THM _ => - (* A type variable of sort "{}" will make abstraction fail. *) - case kind of - Axiom => HOLogic.true_const - | Conjecture => HOLogic.false_const - -(* making axiom and conjecture clauses *) -fun make_clause ctxt (formula_name, kind, t) = - let - val thy = ProofContext.theory_of ctxt - (* ### FIXME: perform other transformations previously done by - "Clausifier.to_nnf", e.g. "HOL.If" *) - val t = t |> transform_elim_term - |> Object_Logic.atomize_term thy - |> extensionalize_term - |> introduce_combinators_in_term ctxt kind - val (combformula, ctypes_sorts) = combformula_for_prop thy t [] - in - FOLFormula {formula_name = formula_name, combformula = combformula, - kind = kind, ctypes_sorts = ctypes_sorts} - end - -fun make_axiom_clause ctxt (name, th) = - (name, make_clause ctxt (name, Axiom, prop_of th)) -fun make_conjecture_clauses ctxt ts = - map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t)) - (0 upto length ts - 1) ts - -(** Helper clauses **) - -fun count_combterm (CombConst ((s, _), _, _)) = - Symtab.map_entry s (Integer.add 1) - | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi - | count_combformula (AConn (_, phis)) = fold count_combformula phis - | count_combformula (APred tm) = count_combterm tm -fun count_fol_formula (FOLFormula {combformula, ...}) = - count_combformula combformula - -val optional_helpers = - [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), - (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), - (["c_COMBS"], @{thms COMBS_def})] -val optional_typed_helpers = - [(["c_True", "c_False"], @{thms True_or_False}), - (["c_If"], @{thms if_True if_False True_or_False})] -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} - -val init_counters = - Symtab.make (maps (maps (map (rpair 0) o fst)) - [optional_helpers, optional_typed_helpers]) - -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses = - let - val ct = fold (fold count_fol_formula) [conjectures, axclauses] - init_counters - fun is_needed c = the (Symtab.lookup ct c) > 0 - val cnfs = - (optional_helpers - |> full_types ? append optional_typed_helpers - |> maps (fn (ss, ths) => - if exists is_needed ss then map (`Thm.get_name_hint) ths - else [])) @ - (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) - in map (snd o make_axiom_clause ctxt) cnfs end - -fun s_not (@{const Not} $ t) = t - | s_not t = @{const Not} $ t - -(* prepare for passing to writer, - create additional clauses based on the information from extra_cls *) -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls = - let - val thy = ProofContext.theory_of ctxt - val goal_t = Logic.list_implies (hyp_ts, concl_t) - val is_FO = Meson.is_fol_term thy goal_t - val axtms = map (prop_of o snd) extra_cls - val subs = tfree_classes_of_terms [goal_t] - val supers = tvar_classes_of_terms axtms - val tycons = type_consts_of_terms thy (goal_t :: axtms) - (* TFrees in conjecture clauses; TVars in axiom clauses *) - val conjectures = - map (s_not o HOLogic.dest_Trueprop) hyp_ts @ - [HOLogic.dest_Trueprop concl_t] - |> make_conjecture_clauses ctxt - val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls - val (clnames, axiom_clauses) = - ListPair.unzip (map (make_axiom_clause ctxt) axcls) - (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the - "get_helper_clauses" call? *) - val helper_clauses = - get_helper_clauses ctxt is_FO full_types conjectures extra_clauses - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in - (Vector.fromList clnames, - (conjectures, axiom_clauses, extra_clauses, helper_clauses, - class_rel_clauses, arity_clauses)) - end - -val axiom_prefix = "ax_" -val conjecture_prefix = "conj_" -val arity_clause_prefix = "clsarity_" -val tfrees_name = "tfrees" - -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) - -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) - | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) - | fo_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map fo_term_for_combtyp tys) - -fun fo_literal_for_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_for_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot - -fun fo_term_for_combterm full_types = - let - fun aux top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name, _, ty_args) => - if fst name = "equal" then - (if top_level andalso length args = 2 then name - else ("c_fequal", @{const_name fequal}), []) - else - (name, if full_types then [] else ty_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ - map (aux false) args) - in - if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t - end - in aux true end - -fun formula_for_combformula full_types = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = APred (fo_term_for_combterm full_types tm) - in aux end - -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = - mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) - (type_literals_for_types ctypes_sorts)) - (formula_for_combformula full_types combformula) - -fun problem_line_for_axiom full_types - (formula as FOLFormula {formula_name, kind, ...}) = - Fof (axiom_prefix ^ ascii_of formula_name, kind, - formula_for_axiom full_types formula) - -fun problem_line_for_class_rel_clause - (ClassRelClause {axiom_name, subclass, superclass, ...}) = - let val ty_arg = ATerm (("T", "T"), []) in - Fof (ascii_of axiom_name, Axiom, - AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), - APred (ATerm (superclass, [ty_arg]))])) - end - -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_for_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun problem_line_for_arity_clause - (ArityClause {axiom_name, conclLit, premLits, ...}) = - Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, - mk_ahorn (map (formula_for_fo_literal o apfst not - o fo_literal_for_arity_literal) premLits) - (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit))) - -fun problem_line_for_conjecture full_types - (FOLFormula {formula_name, kind, combformula, ...}) = - Fof (conjecture_prefix ^ formula_name, kind, - formula_for_combformula full_types combformula) +structure Data = Theory_Data +( + type T = (prover_config * stamp) Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data : T = Symtab.merge (eq_snd op =) data + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") +) -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = - map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) - -fun problem_line_for_free_type lit = - Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) -fun problem_lines_for_free_types conjectures = - let - val litss = map free_type_literals_for_conjecture conjectures - val lits = fold (union (op =)) litss [] - in map problem_line_for_free_type lits end - -(** "hBOOL" and "hAPP" **) - -type const_info = {min_arity: int, max_arity: int, sub_level: bool} - -fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_tptp_variable s then - I - else - let val n = length ts in - Symtab.map_default - (s, {min_arity = n, max_arity = 0, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) - end) - #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi - | consider_formula (AConn (_, phis)) = fold consider_formula phis - | consider_formula (APred tm) = consider_term true tm - -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi -fun consider_problem problem = fold (fold consider_problem_line o snd) problem - -fun const_table_for_problem explicit_apply problem = - if explicit_apply then NONE - else SOME (Symtab.empty |> consider_problem problem) - -val tc_fun = make_fixed_type_const @{type_name fun} - -fun min_arity_of thy full_types NONE s = - (if s = "equal" orelse s = type_wrapper_name orelse - String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s then - 16383 (* large number *) - else if full_types then - 0 - else case strip_prefix_and_undo_ascii const_prefix s of - SOME s' => num_type_args thy (invert_const s') - | NONE => 0) - | min_arity_of _ _ (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME ({min_arity, ...} : const_info) => min_arity - | NONE => 0 - -fun full_type_of (ATerm ((s, _), [ty, _])) = - if s = type_wrapper_name then ty else raise Fail "expected type wrapper" - | full_type_of _ = raise Fail "expected type wrapper" - -fun list_hAPP_rev _ t1 [] = t1 - | list_hAPP_rev NONE t1 (t2 :: ts2) = - ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) - | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = - let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, - [full_type_of t2, ty]) in - ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) - end - -fun repair_applications_in_term thy full_types const_tab = - let - fun aux opt_ty (ATerm (name as (s, _), ts)) = - if s = type_wrapper_name then - case ts of - [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) - | _ => raise Fail "malformed type wrapper" - else - let - val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts - in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end - in aux NONE end - -fun boolify t = ATerm (`I "hBOOL", [t]) +fun add_prover (name, config) thy = + Data.map (Symtab.update_new (name, (config, stamp ()))) thy + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") -(* True if the constant ever appears outside of the top-level position in - literals, or if it appears with different arities (e.g., because of different - type instantiations). If false, the constant always receives all of its - arguments and is used as a predicate. *) -fun is_predicate NONE s = - s = "equal" orelse String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s - | is_predicate (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME {min_arity, max_arity, sub_level} => - not sub_level andalso min_arity = max_arity - | NONE => false - -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = - if s = type_wrapper_name then - case ts of - [_, t' as ATerm ((s', _), _)] => - if is_predicate const_tab s' then t' else boolify t - | _ => raise Fail "malformed type wrapper" - else - t |> not (is_predicate const_tab s) ? boolify - -fun close_universally phi = - let - fun term_vars bounds (ATerm (name as (s, _), tms)) = - (is_tptp_variable s andalso not (member (op =) bounds name)) - ? insert (op =) name - #> fold (term_vars bounds) tms - fun formula_vars bounds (AQuant (q, xs, phi)) = - formula_vars (xs @ bounds) phi - | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (APred tm) = term_vars bounds tm - in - case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) - end - -fun repair_formula thy explicit_forall full_types const_tab = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = - APred (tm |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) - in aux #> explicit_forall ? close_universally end - -fun repair_problem_line thy explicit_forall full_types const_tab - (Fof (ident, kind, phi)) = - Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) -fun repair_problem_with_const_table thy = - map o apsnd o map ooo repair_problem_line thy - -fun repair_problem thy explicit_forall full_types explicit_apply problem = - repair_problem_with_const_table thy explicit_forall full_types - (const_table_for_problem explicit_apply problem) problem - -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axiom_clauses, extra_clauses, - helper_clauses, class_rel_clauses, arity_clauses) = - let - val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses - val class_rel_lines = - map problem_line_for_class_rel_clause class_rel_clauses - val arity_lines = map problem_line_for_arity_clause arity_clauses - val helper_lines = map (problem_line_for_axiom full_types) helper_clauses - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures - (* Reordering these might or might not confuse the proof reconstruction - code or the SPASS Flotter hack. *) - val problem = - [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy explicit_forall full_types explicit_apply - val (problem, pool) = nice_tptp_problem readable_names problem - val conjecture_offset = - length axiom_lines + length class_rel_lines + length arity_lines - + length helper_lines - val _ = File.write_list file (strings_for_tptp_problem problem) - in - (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - conjecture_offset) - end - -fun extract_clause_sequence output = - let - val tokens_of = String.tokens (not o Char.isAlphaNum) - fun extract_num ("clause" :: (ss as _ :: _)) = - Int.fromString (List.last ss) - | extract_num _ = NONE - in output |> split_lines |> map_filter (extract_num o tokens_of) end +fun get_prover thy name = + the (Symtab.lookup (Data.get thy) name) |> fst + handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" - -val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" - --| Scan.option ($$ ",") -val parse_clause_formula_relation = - Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" - |-- Scan.repeat parse_clause_formula_pair -val extract_clause_formula_relation = - Substring.full - #> Substring.position set_ClauseFormulaRelationN - #> snd #> Substring.string #> strip_spaces #> explode - #> parse_clause_formula_relation #> fst - -fun repair_conjecture_shape_and_theorem_names output conjecture_shape - thm_names = - if String.isSubstring set_ClauseFormulaRelationN output then - (* This is a hack required for keeping track of axioms after they have been - clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part - of this hack. *) - let - val j0 = hd conjecture_shape - val seq = extract_clause_sequence output - val name_map = extract_clause_formula_relation output - fun renumber_conjecture j = - AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) - |> the_single - |> (fn s => find_index (curry (op =) s) seq + 1) - in - (conjecture_shape |> map renumber_conjecture, - seq |> map (the o AList.lookup (op =) name_map) - |> map (fn s => case try (unprefix axiom_prefix) s of - SOME s' => undo_ascii_of s' - | NONE => "") - |> Vector.fromList) - end - else - (conjecture_shape, thm_names) - - -(* generic TPTP-based provers *) - -fun generic_tptp_prover - (name, {home_var, executable, arguments, proof_delims, known_failures, - max_new_relevant_facts_per_iter, prefers_theory_relevant, - explicit_forall}) - ({debug, overlord, full_types, explicit_apply, relevance_threshold, - relevance_convergence, theory_relevant, defs_relevant, isar_proof, - isar_shrink_factor, ...} : params) - minimize_command timeout - ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} - : problem) = - let - (* get clauses and prepare them for writing *) - val (ctxt, (_, th)) = goal; - val thy = ProofContext.theory_of ctxt - (* ### FIXME: (1) preprocessing for "if" etc. *) - val (params, hyp_ts, concl_t) = strip_subgoal th subgoal - val the_filtered_clauses = - case filtered_clauses of - SOME fcls => fcls - | NONE => relevant_facts full_types relevance_threshold - relevance_convergence defs_relevant - max_new_relevant_facts_per_iter - (the_default prefers_theory_relevant theory_relevant) - relevance_override goal hyp_ts concl_t - val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses - val (internal_thm_names, clauses) = - prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses - the_filtered_clauses - - (* path to unique problem file *) - val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" - else Config.get ctxt dest_dir; - val the_problem_prefix = Config.get ctxt problem_prefix; - fun prob_pathname nr = - let - val probfile = - Path.basic ((if overlord then "prob_" ^ name - else the_problem_prefix ^ serial_string ()) - ^ "_" ^ string_of_int nr) - in - if the_dest_dir = "" then File.tmp_path probfile - else if File.exists (Path.explode the_dest_dir) - then Path.append (Path.explode the_dest_dir) probfile - else error ("No such directory: " ^ the_dest_dir ^ ".") - end; +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - val home = getenv home_var - val command = Path.explode (home ^ "/" ^ executable) - (* write out problem file and call prover *) - fun command_line complete probfile = - let - val core = File.shell_path command ^ " " ^ arguments complete timeout ^ - " " ^ File.shell_path probfile - in - (if Config.get ctxt measure_runtime then - "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" - else - "exec " ^ core) ^ " 2>&1" - end - fun split_time s = - let - val split = String.tokens (fn c => str c = "\n"); - val (output, t) = s |> split |> split_last |> apfst cat_lines; - fun as_num f = f >> (fst o read_int); - val num = as_num (Scan.many1 Symbol.is_ascii_digit); - val digit = Scan.one Symbol.is_ascii_digit; - val num3 = as_num (digit ::: digit ::: (digit >> single)); - val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); - val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; - in (output, as_time t) end; - fun run_on probfile = - if home = "" then - error ("The environment variable " ^ quote home_var ^ " is not set.") - else if File.exists command then - let - fun do_run complete = - let - val command = command_line complete probfile - val ((output, msecs), res_code) = - bash_output command - |>> (if overlord then - prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") - else - I) - |>> (if Config.get ctxt measure_runtime then split_time - else rpair 0) - val (proof, outcome) = - extract_proof_and_outcome complete res_code proof_delims - known_failures output - in (output, msecs, proof, outcome) end - val readable_names = debug andalso overlord - val (pool, conjecture_offset) = - write_tptp_file thy readable_names explicit_forall full_types - explicit_apply probfile clauses - val conjecture_shape = - conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 - val result = - do_run false - |> (fn (_, msecs0, _, SOME _) => - do_run true - |> (fn (output, msecs, proof, outcome) => - (output, msecs0 + msecs, proof, outcome)) - | result => result) - in ((pool, conjecture_shape), result) end - else - error ("Bad executable: " ^ Path.implode command ^ "."); - - (* If the problem file has not been exported, remove it; otherwise, export - the proof file too. *) - fun cleanup probfile = - if the_dest_dir = "" then try File.rm probfile else NONE - fun export probfile (_, (output, _, _, _)) = - if the_dest_dir = "" then - () - else - File.write (Path.explode (Path.implode probfile ^ "_proof")) output - - val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = - with_path cleanup export run_on (prob_pathname subgoal) - val (conjecture_shape, internal_thm_names) = - repair_conjecture_shape_and_theorem_names output conjecture_shape - internal_thm_names - - val (message, used_thm_names) = - case outcome of - NONE => - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (full_types, minimize_command, proof, internal_thm_names, th, - subgoal) - | SOME failure => (string_for_failure failure ^ "\n", []) - in - {outcome = outcome, message = message, pool = pool, - used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, - output = output, proof = proof, internal_thm_names = internal_thm_names, - conjecture_shape = conjecture_shape, - filtered_clauses = the_filtered_clauses} - end - -fun tptp_prover name p = (name, generic_tptp_prover (name, p)); +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 @@ -801,7 +102,7 @@ max_new_relevant_facts_per_iter = 80 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} -val e = tptp_prover "e" e_config +val e = ("e", e_config) (* The "-VarWeight=3" option helps the higher-order problems, probably by @@ -826,7 +127,7 @@ max_new_relevant_facts_per_iter = 26 (* FIXME *), prefers_theory_relevant = true, explicit_forall = true} -val spass = tptp_prover "spass" spass_config +val spass = ("spass", spass_config) (* Vampire *) @@ -848,11 +149,11 @@ max_new_relevant_facts_per_iter = 40 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} -val vampire = tptp_prover "vampire" vampire_config +val vampire = ("vampire", vampire_config) (* Remote prover invocation via SystemOnTPTP *) -val systems = Synchronized.var "atp_systems" ([]: string list); +val systems = Synchronized.var "atp_systems" ([]: string list) fun get_systems () = case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of @@ -893,27 +194,23 @@ prefers_theory_relevant = prefers_theory_relevant, explicit_forall = explicit_forall} -fun remote_tptp_prover prover atp_prefix args config = - tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config) +val remote_name = prefix "remote_" -val remote_e = remote_tptp_prover e "EP---" "" e_config -val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config -val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config +fun remote_prover prover atp_prefix args config = + (remote_name (fst prover), remote_config atp_prefix args config) + +val remote_e = remote_prover e "EP---" "" e_config +val remote_spass = remote_prover spass "SPASS---" "-x" spass_config +val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config fun maybe_remote (name, _) ({home_var, ...} : prover_config) = - name |> getenv home_var = "" ? remotify + name |> getenv home_var = "" ? remote_name fun default_atps_param_value () = space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config, - remotify (fst vampire)] + remote_name (fst vampire)] val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire] -val prover_setup = fold add_prover provers - -val setup = - dest_dir_setup - #> problem_prefix_setup - #> measure_runtime_setup - #> prover_setup +val setup = fold add_prover provers end; diff -r d9c4d87838f3 -r 962b0a7f544b src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 17:58:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 18:33:10 2010 +0200 @@ -8,6 +8,7 @@ signature SLEDGEHAMMER = sig + type failure = ATP_Systems.failure type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = @@ -31,9 +32,6 @@ relevance_override: relevance_override, axiom_clauses: (string * thm) list option, filtered_clauses: (string * thm) list option} - datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | - OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError type prover_result = {outcome: failure option, message: string, @@ -48,24 +46,30 @@ type prover = params -> minimize_command -> Time.time -> problem -> prover_result + val dest_dir : string Config.T + val problem_prefix : string Config.T + val measure_runtime : bool Config.T val kill_atps: unit -> unit val running_atps: unit -> unit val messages: int option -> unit - val add_prover: string * prover -> theory -> theory - val get_prover: theory -> string -> prover - val available_atps: theory -> unit + val get_prover_fun : theory -> string -> prover val start_prover_thread : params -> int -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> string -> unit + val setup : theory -> theory end; structure Sledgehammer : SLEDGEHAMMER = struct open Metis_Clauses +open Sledgehammer_Util open Sledgehammer_Fact_Filter +open ATP_Problem +open ATP_Systems open Sledgehammer_Proof_Reconstruct + (** The Sledgehammer **) val das_Tool = "Sledgehammer" @@ -99,10 +103,6 @@ axiom_clauses: (string * thm) list option, filtered_clauses: (string * thm) list option} -datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | - OldSpass | MalformedInput | MalformedOutput | UnknownError - type prover_result = {outcome: failure option, message: string, @@ -118,38 +118,744 @@ type prover = params -> minimize_command -> Time.time -> problem -> prover_result -(* named provers *) +(* configuration attributes *) + +val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); + (*Empty string means create files in Isabelle's temporary files directory.*) + +val (problem_prefix, problem_prefix_setup) = + Attrib.config_string "atp_problem_prefix" (K "prob"); + +val (measure_runtime, measure_runtime_setup) = + Attrib.config_bool "atp_measure_runtime" (K false); -structure Data = Theory_Data -( - type T = (prover * stamp) Symtab.table; - val empty = Symtab.empty; - val extend = I; - fun merge data : T = Symtab.merge (eq_snd op =) data - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") -); +fun with_path cleanup after f path = + Exn.capture f path + |> tap (fn _ => cleanup path) + |> Exn.release + |> tap (after path) + +(* Splits by the first possible of a list of delimiters. *) +fun extract_proof delims output = + case pairself (find_first (fn s => String.isSubstring s output)) + (ListPair.unzip delims) of + (SOME begin_delim, SOME end_delim) => + (output |> first_field begin_delim |> the |> snd + |> first_field end_delim |> the |> fst + |> first_field "\n" |> the |> snd + handle Option.Option => "") + | _ => "" -fun add_prover (name, prover) thy = - Data.map (Symtab.update_new (name, (prover, stamp ()))) thy - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") +fun extract_proof_and_outcome complete res_code proof_delims known_failures + output = + case map_filter (fn (failure, pattern) => + if String.isSubstring pattern output then SOME failure + else NONE) known_failures of + [] => (case extract_proof proof_delims output of + "" => ("", SOME UnknownError) + | proof => if res_code = 0 then (proof, NONE) + else ("", SOME UnknownError)) + | (failure :: _) => + ("", SOME (if failure = IncompleteUnprovable andalso complete then + Unprovable + else + failure)) -fun get_prover thy name = - the (Symtab.lookup (Data.get thy) name) |> fst - handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") - -fun available_atps thy = - priority ("Available ATPs: " ^ - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") +fun string_for_failure Unprovable = "The ATP problem is unprovable." + | string_for_failure IncompleteUnprovable = + "The ATP cannot prove the problem." + | string_for_failure CantConnect = "Can't connect to remote ATP." + | string_for_failure TimedOut = "Timed out." + | string_for_failure OutOfResources = "The ATP ran out of resources." + | string_for_failure OldSpass = + (* FIXME: Change the error message below to point to the Isabelle download + page once the package is there. *) + "Warning: Sledgehammer requires a more recent version of SPASS with \ + \support for the TPTP syntax. To install it, download and untar the \ + \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \ + \\"spass-3.7\" directory's full path to \"" ^ + Path.implode (Path.expand (Path.appends + (Path.variable "ISABELLE_HOME_USER" :: + map Path.basic ["etc", "components"]))) ^ + "\" on a line of its own." + | string_for_failure MalformedInput = + "Internal Sledgehammer error: The ATP problem is malformed. Please report \ + \this to the Isabelle developers." + | string_for_failure MalformedOutput = "Error: The ATP output is malformed." + | string_for_failure UnknownError = "Error: An unknown ATP error occurred." +(* Clause preparation *) + +datatype fol_formula = + FOLFormula of {formula_name: string, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} + +fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun mk_ahorn [] phi = phi + | mk_ahorn (phi :: phis) psi = + AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) + +(* ### FIXME: reintroduce +fun make_clause_table xs = + fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty +(* Remove existing axiom clauses from the conjecture clauses, as this can + dramatically boost an ATP's performance (for some reason). *) +fun subtract_cls ax_clauses = + filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) +*) + +fun combformula_for_prop thy = + let + val do_term = combterm_from_term thy + fun do_quant bs q s T t' = + do_formula ((s, T) :: bs) t' + #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + and do_conn bs c t1 t2 = + do_formula bs t1 ##>> do_formula bs t2 + #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) + and do_formula bs t = + case t of + @{const Not} $ t1 => + do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) + | Const (@{const_name All}, _) $ Abs (s, T, t') => + do_quant bs AForall s T t' + | Const (@{const_name Ex}, _) $ Abs (s, T, t') => + do_quant bs AExists s T t' + | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 + | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 + | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 + | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => + do_conn bs AIff t1 t2 + | _ => (fn ts => do_term bs (Envir.eta_contract t) + |>> APred ||> union (op =) ts) + in do_formula [] end + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_term" in + "ATP_Systems".) *) +(* FIXME: test! *) +fun transform_elim_term t = + case Logic.strip_imp_concl t of + @{const Trueprop} $ Var (z, @{typ bool}) => + subst_Vars [(z, @{const True})] t + | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t + | _ => t + +(* Removes the lambdas from an equation of the form "t = (%x. u)". + (Cf. "extensionalize_theorem" in "Clausifier".) *) +fun extensionalize_term t = + let + fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _])) + $ t2 $ Abs (s, var_T, t')) = + let val var_t = Var (("x", j), var_T) in + Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT) + $ betapply (t2, var_t) $ subst_bound (var_t, t') + |> aux (j + 1) + end + | aux _ t = t + in aux (maxidx_of_term t + 1) t end + +(* FIXME: Guarantee freshness *) +fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j +fun conceal_bounds Ts t = + subst_bounds (map (Free o apfst concealed_bound_name) + (length Ts - 1 downto 0 ~~ rev Ts), t) +fun reveal_bounds Ts = + subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) + (0 upto length Ts - 1 ~~ Ts)) + +fun introduce_combinators_in_term ctxt kind t = + let + val thy = ProofContext.theory_of ctxt + fun aux Ts t = + case t of + @{const Not} $ t1 => @{const Not} $ aux Ts t1 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) + $ t1 $ t2 => + t0 $ aux Ts t1 $ aux Ts t2 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then + t + else + let + val t = t |> conceal_bounds Ts + |> Envir.eta_contract + val ([t], ctxt') = Variable.import_terms true [t] ctxt + in + t |> cterm_of thy + |> Clausifier.introduce_combinators_in_cterm + |> singleton (Variable.export ctxt' ctxt) + |> prop_of |> Logic.dest_equals |> snd + |> reveal_bounds Ts + end + in t |> not (Meson.is_fol_term thy t) ? aux [] end + handle THM _ => + (* A type variable of sort "{}" will make abstraction fail. *) + case kind of + Axiom => HOLogic.true_const + | Conjecture => HOLogic.false_const + +(* making axiom and conjecture clauses *) +fun make_clause ctxt (formula_name, kind, t) = + let + val thy = ProofContext.theory_of ctxt + (* ### FIXME: perform other transformations previously done by + "Clausifier.to_nnf", e.g. "HOL.If" *) + val t = t |> transform_elim_term + |> Object_Logic.atomize_term thy + |> extensionalize_term + |> introduce_combinators_in_term ctxt kind + val (combformula, ctypes_sorts) = combformula_for_prop thy t [] + in + FOLFormula {formula_name = formula_name, combformula = combformula, + kind = kind, ctypes_sorts = ctypes_sorts} + end + +fun make_axiom_clause ctxt (name, th) = + (name, make_clause ctxt (name, Axiom, prop_of th)) +fun make_conjecture_clauses ctxt ts = + map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t)) + (0 upto length ts - 1) ts + +(** Helper clauses **) + +fun count_combterm (CombConst ((s, _), _, _)) = + Symtab.map_entry s (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi + | count_combformula (AConn (_, phis)) = fold count_combformula phis + | count_combformula (APred tm) = count_combterm tm +fun count_fol_formula (FOLFormula {combformula, ...}) = + count_combformula combformula + +val optional_helpers = + [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), + (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), + (["c_COMBS"], @{thms COMBS_def})] +val optional_typed_helpers = + [(["c_True", "c_False"], @{thms True_or_False}), + (["c_If"], @{thms if_True if_False True_or_False})] +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} + +val init_counters = + Symtab.make (maps (maps (map (rpair 0) o fst)) + [optional_helpers, optional_typed_helpers]) + +fun get_helper_clauses ctxt is_FO full_types conjectures axclauses = + let + val ct = fold (fold count_fol_formula) [conjectures, axclauses] + init_counters + fun is_needed c = the (Symtab.lookup ct c) > 0 + val cnfs = + (optional_helpers + |> full_types ? append optional_typed_helpers + |> maps (fn (ss, ths) => + if exists is_needed ss then map (`Thm.get_name_hint) ths + else [])) @ + (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) + in map (snd o make_axiom_clause ctxt) cnfs end + +fun s_not (@{const Not} $ t) = t + | s_not t = @{const Not} $ t + +(* prepare for passing to writer, + create additional clauses based on the information from extra_cls *) +fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls = + let + val thy = ProofContext.theory_of ctxt + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val is_FO = Meson.is_fol_term thy goal_t + val axtms = map (prop_of o snd) extra_cls + val subs = tfree_classes_of_terms [goal_t] + val supers = tvar_classes_of_terms axtms + val tycons = type_consts_of_terms thy (goal_t :: axtms) + (* TFrees in conjecture clauses; TVars in axiom clauses *) + val conjectures = + map (s_not o HOLogic.dest_Trueprop) hyp_ts @ + [HOLogic.dest_Trueprop concl_t] + |> make_conjecture_clauses ctxt + val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls + val (clnames, axiom_clauses) = + ListPair.unzip (map (make_axiom_clause ctxt) axcls) + (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the + "get_helper_clauses" call? *) + val helper_clauses = + get_helper_clauses ctxt is_FO full_types conjectures extra_clauses + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in + (Vector.fromList clnames, + (conjectures, axiom_clauses, extra_clauses, helper_clauses, + class_rel_clauses, arity_clauses)) + end + +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" +val arity_clause_prefix = "clsarity_" +val tfrees_name = "tfrees" + +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) + +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) + +fun fo_literal_for_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_for_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot + +fun fo_term_for_combterm full_types = + let + fun aux top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name, _, ty_args) => + if fst name = "equal" then + (if top_level andalso length args = 2 then name + else ("c_fequal", @{const_name fequal}), []) + else + (name, if full_types then [] else ty_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (aux false) args) + in + if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t + end + in aux true end + +fun formula_for_combformula full_types = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = APred (fo_term_for_combterm full_types tm) + in aux end + +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = + mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) + (type_literals_for_types ctypes_sorts)) + (formula_for_combformula full_types combformula) + +fun problem_line_for_axiom full_types + (formula as FOLFormula {formula_name, kind, ...}) = + Fof (axiom_prefix ^ ascii_of formula_name, kind, + formula_for_axiom full_types formula) + +fun problem_line_for_class_rel_clause + (ClassRelClause {axiom_name, subclass, superclass, ...}) = + let val ty_arg = ATerm (("T", "T"), []) in + Fof (ascii_of axiom_name, Axiom, + AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), + APred (ATerm (superclass, [ty_arg]))])) + end + +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_for_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun problem_line_for_arity_clause + (ArityClause {axiom_name, conclLit, premLits, ...}) = + Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, + mk_ahorn (map (formula_for_fo_literal o apfst not + o fo_literal_for_arity_literal) premLits) + (formula_for_fo_literal + (fo_literal_for_arity_literal conclLit))) + +fun problem_line_for_conjecture full_types + (FOLFormula {formula_name, kind, combformula, ...}) = + Fof (conjecture_prefix ^ formula_name, kind, + formula_for_combformula full_types combformula) + +fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = + map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) + +fun problem_line_for_free_type lit = + Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) +fun problem_lines_for_free_types conjectures = + let + val litss = map free_type_literals_for_conjecture conjectures + val lits = fold (union (op =)) litss [] + in map problem_line_for_free_type lits end + +(** "hBOOL" and "hAPP" **) + +type const_info = {min_arity: int, max_arity: int, sub_level: bool} + +fun consider_term top_level (ATerm ((s, _), ts)) = + (if is_tptp_variable s then + I + else + let val n = length ts in + Symtab.map_default + (s, {min_arity = n, max_arity = 0, sub_level = false}) + (fn {min_arity, max_arity, sub_level} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + sub_level = sub_level orelse not top_level}) + end) + #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (APred tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi +fun consider_problem problem = fold (fold consider_problem_line o snd) problem + +fun const_table_for_problem explicit_apply problem = + if explicit_apply then NONE + else SOME (Symtab.empty |> consider_problem problem) + +val tc_fun = make_fixed_type_const @{type_name fun} + +fun min_arity_of thy full_types NONE s = + (if s = "equal" orelse s = type_wrapper_name orelse + String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s then + 16383 (* large number *) + else if full_types then + 0 + else case strip_prefix_and_undo_ascii const_prefix s of + SOME s' => num_type_args thy (invert_const s') + | NONE => 0) + | min_arity_of _ _ (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME ({min_arity, ...} : const_info) => min_arity + | NONE => 0 + +fun full_type_of (ATerm ((s, _), [ty, _])) = + if s = type_wrapper_name then ty else raise Fail "expected type wrapper" + | full_type_of _ = raise Fail "expected type wrapper" + +fun list_hAPP_rev _ t1 [] = t1 + | list_hAPP_rev NONE t1 (t2 :: ts2) = + ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) + | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = + let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, + [full_type_of t2, ty]) in + ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) + end + +fun repair_applications_in_term thy full_types const_tab = + let + fun aux opt_ty (ATerm (name as (s, _), ts)) = + if s = type_wrapper_name then + case ts of + [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) + | _ => raise Fail "malformed type wrapper" + else + let + val ts = map (aux NONE) ts + val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts + in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end + in aux NONE end + +fun boolify t = ATerm (`I "hBOOL", [t]) + +(* True if the constant ever appears outside of the top-level position in + literals, or if it appears with different arities (e.g., because of different + type instantiations). If false, the constant always receives all of its + arguments and is used as a predicate. *) +fun is_predicate NONE s = + s = "equal" orelse String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s + | is_predicate (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME {min_arity, max_arity, sub_level} => + not sub_level andalso min_arity = max_arity + | NONE => false + +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = + if s = type_wrapper_name then + case ts of + [_, t' as ATerm ((s', _), _)] => + if is_predicate const_tab s' then t' else boolify t + | _ => raise Fail "malformed type wrapper" + else + t |> not (is_predicate const_tab s) ? boolify + +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (is_tptp_variable s andalso not (member (op =) bounds name)) + ? insert (op =) name + #> fold (term_vars bounds) tms + fun formula_vars bounds (AQuant (q, xs, phi)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (APred tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = + APred (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +fun repair_problem_with_const_table thy = + map o apsnd o map ooo repair_problem_line thy + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types + (const_table_for_problem explicit_apply problem) problem + +fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply + file (conjectures, axiom_clauses, extra_clauses, + helper_clauses, class_rel_clauses, arity_clauses) = + let + val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses + val class_rel_lines = + map problem_line_for_class_rel_clause class_rel_clauses + val arity_lines = map problem_line_for_arity_clause arity_clauses + val helper_lines = map (problem_line_for_axiom full_types) helper_clauses + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures + (* Reordering these might or might not confuse the proof reconstruction + code or the SPASS Flotter hack. *) + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply + val (problem, pool) = nice_tptp_problem readable_names problem + val conjecture_offset = + length axiom_lines + length class_rel_lines + length arity_lines + + length helper_lines + val _ = File.write_list file (strings_for_tptp_problem problem) + in + (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + conjecture_offset) + end + +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = + Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" + |-- Scan.repeat parse_clause_formula_pair +val extract_clause_formula_relation = + Substring.full + #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.string #> strip_spaces #> explode + #> parse_clause_formula_relation #> fst + +fun repair_conjecture_shape_and_theorem_names output conjecture_shape + thm_names = + if String.isSubstring set_ClauseFormulaRelationN output then + (* This is a hack required for keeping track of axioms after they have been + clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part + of this hack. *) + let + val j0 = hd conjecture_shape + val seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + fun renumber_conjecture j = + AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) + |> the_single + |> (fn s => find_index (curry (op =) s) seq + 1) + in + (conjecture_shape |> map renumber_conjecture, + seq |> map (the o AList.lookup (op =) name_map) + |> map (fn s => case try (unprefix axiom_prefix) s of + SOME s' => undo_ascii_of s' + | NONE => "") + |> Vector.fromList) + end + else + (conjecture_shape, thm_names) + + +(* generic TPTP-based provers *) + +fun prover_fun name + {home_var, executable, arguments, proof_delims, known_failures, + max_new_relevant_facts_per_iter, prefers_theory_relevant, + explicit_forall} + ({debug, overlord, full_types, explicit_apply, relevance_threshold, + relevance_convergence, theory_relevant, defs_relevant, isar_proof, + isar_shrink_factor, ...} : params) + minimize_command timeout + ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} + : problem) = + let + (* get clauses and prepare them for writing *) + val (ctxt, (_, th)) = goal; + val thy = ProofContext.theory_of ctxt + (* ### FIXME: (1) preprocessing for "if" etc. *) + val (params, hyp_ts, concl_t) = strip_subgoal th subgoal + val the_filtered_clauses = + case filtered_clauses of + SOME fcls => fcls + | NONE => relevant_facts full_types relevance_threshold + relevance_convergence defs_relevant + max_new_relevant_facts_per_iter + (the_default prefers_theory_relevant theory_relevant) + relevance_override goal hyp_ts concl_t + val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses + val (internal_thm_names, clauses) = + prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses + the_filtered_clauses + + (* path to unique problem file *) + val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" + else Config.get ctxt dest_dir; + val the_problem_prefix = Config.get ctxt problem_prefix; + fun prob_pathname nr = + let + val probfile = + Path.basic ((if overlord then "prob_" ^ name + else the_problem_prefix ^ serial_string ()) + ^ "_" ^ string_of_int nr) + in + if the_dest_dir = "" then File.tmp_path probfile + else if File.exists (Path.explode the_dest_dir) + then Path.append (Path.explode the_dest_dir) probfile + else error ("No such directory: " ^ the_dest_dir ^ ".") + end; + + val home = getenv home_var + val command = Path.explode (home ^ "/" ^ executable) + (* write out problem file and call prover *) + fun command_line complete probfile = + let + val core = File.shell_path command ^ " " ^ arguments complete timeout ^ + " " ^ File.shell_path probfile + in + (if Config.get ctxt measure_runtime then + "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" + else + "exec " ^ core) ^ " 2>&1" + end + fun split_time s = + let + val split = String.tokens (fn c => str c = "\n"); + val (output, t) = s |> split |> split_last |> apfst cat_lines; + fun as_num f = f >> (fst o read_int); + val num = as_num (Scan.many1 Symbol.is_ascii_digit); + val digit = Scan.one Symbol.is_ascii_digit; + val num3 = as_num (digit ::: digit ::: (digit >> single)); + val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); + val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; + in (output, as_time t) end; + fun run_on probfile = + if home = "" then + error ("The environment variable " ^ quote home_var ^ " is not set.") + else if File.exists command then + let + fun do_run complete = + let + val command = command_line complete probfile + val ((output, msecs), res_code) = + bash_output command + |>> (if overlord then + prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") + else + I) + |>> (if Config.get ctxt measure_runtime then split_time + else rpair 0) + val (proof, outcome) = + extract_proof_and_outcome complete res_code proof_delims + known_failures output + in (output, msecs, proof, outcome) end + val readable_names = debug andalso overlord + val (pool, conjecture_offset) = + write_tptp_file thy readable_names explicit_forall full_types + explicit_apply probfile clauses + val conjecture_shape = + conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 + val result = + do_run false + |> (fn (_, msecs0, _, SOME _) => + do_run true + |> (fn (output, msecs, proof, outcome) => + (output, msecs0 + msecs, proof, outcome)) + | result => result) + in ((pool, conjecture_shape), result) end + else + error ("Bad executable: " ^ Path.implode command ^ "."); + + (* If the problem file has not been exported, remove it; otherwise, export + the proof file too. *) + fun cleanup probfile = + if the_dest_dir = "" then try File.rm probfile else NONE + fun export probfile (_, (output, _, _, _)) = + if the_dest_dir = "" then + () + else + File.write (Path.explode (Path.implode probfile ^ "_proof")) output + + val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = + with_path cleanup export run_on (prob_pathname subgoal) + val (conjecture_shape, internal_thm_names) = + repair_conjecture_shape_and_theorem_names output conjecture_shape + internal_thm_names + + val (message, used_thm_names) = + case outcome of + NONE => + proof_text isar_proof + (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (full_types, minimize_command, proof, internal_thm_names, th, + subgoal) + | SOME failure => (string_for_failure failure ^ "\n", []) + in + {outcome = outcome, message = message, pool = pool, + used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, + output = output, proof = proof, internal_thm_names = internal_thm_names, + conjecture_shape = conjecture_shape, + filtered_clauses = the_filtered_clauses} + end + +fun get_prover_fun thy name = prover_fun name (get_prover thy name) + (* start prover thread *) - fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n relevance_override minimize_command proof_state name = let + val thy = Proof.theory_of proof_state val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) - val prover = get_prover (Proof.theory_of proof_state) name + val prover = get_prover_fun thy name val {context = ctxt, facts, goal} = Proof.goal proof_state; val desc = "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ @@ -168,4 +874,9 @@ end) end +val setup = + dest_dir_setup + #> problem_prefix_setup + #> measure_runtime_setup + end; diff -r d9c4d87838f3 -r 962b0a7f544b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 17:58:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 18:33:10 2010 +0200 @@ -81,7 +81,7 @@ let val thy = Proof.theory_of state val prover = case atps of - [atp_name] => get_prover thy atp_name + [atp_name] => get_prover_fun thy atp_name | _ => error "Expected a single ATP." val msecs = Time.toMilliseconds minimize_timeout val _ =