diff --git a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML @@ -1,869 +1,857 @@ (* Title: HOL/Tools/ATP/atp_proof_reconstruct.ML Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Basic proof reconstruction from ATP proofs. *) signature ATP_PROOF_RECONSTRUCT = sig type 'a atp_type = 'a ATP_Problem.atp_type type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type stature = ATP_Problem_Generate.stature type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof val metisN : string val full_typesN : string val partial_typesN : string val no_typesN : string val really_full_type_enc : string val full_type_enc : string val partial_type_enc : string val no_type_enc : string val full_type_encs : string list val partial_type_encs : string list val default_metis_lam_trans : string val leo2_extcnf_equal_neg_rule : string val satallax_tab_rule_prefix : string val forall_of : term -> term -> term val exists_of : term -> term -> term val simplify_bool : term -> term val var_name_of_typ : typ -> string val rename_bound_vars : term -> term val type_enc_aliases : (string * string list) list val unalias_type_enc : string -> string list val term_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> bool -> int Symtab.table -> typ option -> (string, string atp_type) atp_term -> term val prop_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> bool -> int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> term + val is_conjecture_used_in_proof : string atp_proof -> bool val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof -> (string * stature) list - val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof -> - string list option val atp_proof_prefers_lifting : string atp_proof -> bool val is_typed_helper_used_in_atp_proof : string atp_proof -> bool val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step -> ('a, 'b) atp_step val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> int Symtab.table -> string atp_proof -> (term, string) atp_step list val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list val infer_formulas_types : Proof.context -> term list -> term list val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> (term, string) atp_step list val termify_atp_abduce_candidate : Proof.context -> string -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> term val top_abduce_candidates : int -> term list -> term list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate val metisN = "metis" val full_typesN = "full_types" val partial_typesN = "partial_types" val no_typesN = "no_types" val really_full_type_enc = "mono_tags" val full_type_enc = "poly_guards_query" val partial_type_enc = "poly_args" val no_type_enc = "erased" val full_type_encs = [full_type_enc, really_full_type_enc] val partial_type_encs = partial_type_enc :: full_type_encs val type_enc_aliases = [(full_typesN, full_type_encs), (partial_typesN, partial_type_encs), (no_typesN, [no_type_enc])] fun unalias_type_enc s = AList.lookup (op =) type_enc_aliases s |> the_default [s] val default_metis_lam_trans = combsN val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" val satallax_tab_rule_prefix = "tab_" fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s | term_name' _ = "" fun lambda' v = Term.lambda_name (term_name' v, v) fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t fun make_tfree ctxt w = let val ww = "'" ^ w in TFree (ww, the_default \<^sort>\type\ (Variable.def_sort ctxt (ww, ~1))) end fun simplify_bool ((all as Const (\<^const_name>\All\, _)) $ Abs (s, T, t)) = let val t' = simplify_bool t in if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t' end | simplify_bool (Const (\<^const_name>\Not\, _) $ t) = s_not (simplify_bool t) | simplify_bool (Const (\<^const_name>\conj\, _) $ t $ u) = s_conj (simplify_bool t, simplify_bool u) | simplify_bool (Const (\<^const_name>\disj\, _) $ t $ u) = s_disj (simplify_bool t, simplify_bool u) | simplify_bool (Const (\<^const_name>\implies\, _) $ t $ u) = s_imp (simplify_bool t, simplify_bool u) | simplify_bool ((t as Const (\<^const_name>\HOL.eq\, _)) $ u $ v) = (case (u, v) of (Const (\<^const_name>\True\, _), _) => v | (u, Const (\<^const_name>\True\, _)) => u | (Const (\<^const_name>\False\, _), v) => s_not v | (u, Const (\<^const_name>\False\, _)) => s_not u | _ => if u aconv v then \<^Const>\True\ else t $ simplify_bool u $ simplify_bool v) | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t) | simplify_bool t = t fun single_letter upper s = let val s' = if String.isPrefix "o" s orelse String.isPrefix "O" s then "z" else s in String.extract (Name.desymbolize (SOME upper) (Long_Name.base_name s'), 0, SOME 1) end fun var_name_of_typ (Type (\<^type_name>\fun\, [_, T])) = if body_type T = HOLogic.boolT then "p" else "f" | var_name_of_typ (Type (\<^type_name>\set\, [T])) = let fun default () = single_letter true (var_name_of_typ T) in (case T of Type (s, [T1, T2]) => if String.isSuffix "prod" s andalso T1 = T2 then "r" else default () | _ => default ()) end | var_name_of_typ (Type (s, Ts)) = if String.isSuffix "list" s then var_name_of_typ (the_single Ts) ^ "s" else single_letter false (Long_Name.base_name s) | var_name_of_typ (TFree (s, _)) = single_letter false (perhaps (try (unprefix "'")) s) | var_name_of_typ (TVar ((s, _), T)) = var_name_of_typ (TFree (s, T)) fun rename_bound_vars (t $ u) = rename_bound_vars t $ rename_bound_vars u | rename_bound_vars (Abs (_, T, t)) = Abs (var_name_of_typ T, T, rename_bound_vars t) | rename_bound_vars t = t exception ATP_CLASS of string list exception ATP_TYPE of string atp_type list exception ATP_TERM of (string, string atp_type) atp_term list exception ATP_FORMULA of (string, string, (string, string atp_type) atp_term, string) atp_formula list exception SAME of unit fun class_of_atp_class cls = (case unprefix_and_unascii class_prefix cls of SOME s => s | NONE => raise ATP_CLASS [cls]) fun atp_type_of_atp_term (ATerm ((s, _), us)) = let val tys = map atp_type_of_atp_term us in if s = tptp_fun_type then (case tys of [ty1, ty2] => AFun (ty1, ty2) | _ => raise ATP_TYPE tys) else AType ((s, []), tys) end (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information from type literals, or by type inference. *) fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) = let val Ts = map (typ_of_atp_type ctxt) tys in (case unprefix_and_unascii native_type_prefix a of SOME b => typ_of_atp_type ctxt (atp_type_of_atp_term (unmangled_type b)) | NONE => (case unprefix_and_unascii type_const_prefix a of SOME b => Type (invert_const b, Ts) | NONE => if not (null tys) then raise ATP_TYPE [ty] (* only "tconst"s have type arguments *) else (case unprefix_and_unascii tfree_prefix a of SOME b => make_tfree ctxt b | NONE => (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". Sometimes variables from the ATP are indistinguishable from Isabelle variables, which forces us to use a type parameter in all cases. *) Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a, (if null clss then \<^sort>\type\ else map class_of_atp_class clss))))) end | typ_of_atp_type ctxt (AFun (ty1, ty2)) = typ_of_atp_type ctxt ty1 --> typ_of_atp_type ctxt ty2 fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term (* Type class literal applied to a type. Returns triple of polarity, class, type. *) fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) = (case (unprefix_and_unascii class_prefix a, map (typ_of_atp_term ctxt) us) of (SOME b, [T]) => (b, T) | _ => raise ATP_TERM [u]) (* Accumulate type constraints in a formula: negative type literals. *) fun add_var (key, z) = Vartab.map_default (key, []) (cons z) fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl) | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl) | add_type_constraint _ _ = I fun repair_var_name s = (case unprefix_and_unascii schematic_var_prefix s of SOME s' => s' | NONE => s) (* The number of type arguments of a constant, zero if it's monomorphic. For (instances of) Skolem pseudoconstants, this information is encoded in the constant name. *) fun robust_const_num_type_args thy s = if String.isPrefix skolem_const_prefix s then s |> Long_Name.explode |> List.last |> Int.fromString |> the else if String.isPrefix lam_lifted_prefix s then if String.isPrefix lam_lifted_poly_prefix s then 2 else 0 else (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT \<^sort>\type\ val spass_skolem_prefix = "sk" (* "skc" or "skf" *) val vampire_skolem_prefix = "sK" fun var_index_of_textual textual = if textual then 0 else 1 fun quantify_over_var textual quant_of var_s var_T t = let val vars = ((var_s, var_index_of_textual textual), var_T) :: filter (fn ((s, _), _) => s = var_s) (Term.add_vars t []) val normTs = vars |> AList.group (op =) |> map (apsnd hd) fun norm_var_types (Var (x, T)) = Var (x, the_default T (AList.lookup (op =) normTs x)) | norm_var_types t = t in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end (* This assumes that distinct names are mapped to distinct names by "Variable.variant_frees". This does not hold in general but should hold for ATP-generated Skolem function names, since these end with a digit and "variant_frees" appends letters. *) fun fresh_up ctxt s = fst (hd (Variable.variant_frees ctxt [] [(s, ())])) (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas are typed. The code is similar to "term_of_atp_fo". *) fun term_of_atp_ho ctxt sym_tab = let val thy = Proof_Context.theory_of ctxt val var_index = var_index_of_textual true fun do_term opt_T u = (case u of AAbs (((var, ty), term), []) => let val typ = typ_of_atp_type ctxt ty val var_name = repair_var_name var val tm = do_term NONE term in quantify_over_var true lambda' var_name typ tm end | ATerm ((s, tys), us) => if s = "" (* special marker generated on parse error *) then error "Isar proof reconstruction failed because the ATP proof contains unparsable \ \material" else if s = tptp_equal then list_comb (Const (\<^const_name>\HOL.eq\, Type_Infer.anyT \<^sort>\type\), map (do_term NONE) us) else if s = tptp_not_equal andalso length us = 2 then \<^const>\HOL.Not\ $ list_comb (Const (\<^const_name>\HOL.eq\, Type_Infer.anyT \<^sort>\type\), map (do_term NONE) us) else if not (null us) then let val args = map (do_term NONE) us val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T) val func = do_term opt_T' (ATerm ((s, tys), [])) in foldl1 (op $) (func :: args) end else if s = tptp_or then HOLogic.disj else if s = tptp_and then HOLogic.conj else if s = tptp_implies then HOLogic.imp else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT else if s = tptp_not_iff orelse s = tptp_not_equal then \<^term>\\x y. x \ y\ else if s = tptp_if then \<^term>\\P Q. Q \ P\ else if s = tptp_not_and then \<^term>\\P Q. \ (P \ Q)\ else if s = tptp_not_or then \<^term>\\P Q. \ (P \ Q)\ else if s = tptp_not then HOLogic.Not else if s = tptp_ho_forall then HOLogic.all_const dummyT else if s = tptp_ho_exists then HOLogic.exists_const dummyT else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT else if s = tptp_hilbert_the then \<^term>\The\ else (case unprefix_and_unascii const_prefix s of SOME s' => let val ((s', _), mangled_us) = s' |> unmangled_const |>> `invert_const val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term NONE) term_us val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us val T = (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then try (Sign.const_instance thy) (s', Ts) else NONE) |> (fn SOME T => T | NONE => map slack_fastype_of term_ts ---> the_default (Type_Infer.anyT \<^sort>\type\) opt_T) val t = Const (unproxify_const s', T) in list_comb (t, term_ts) end | NONE => (* a free or schematic variable *) let val ts = map (do_term NONE) us val T = (case tys of [ty] => typ_of_atp_type ctxt ty | _ => map slack_fastype_of ts ---> (case opt_T of SOME T => T | NONE => Type_Infer.anyT \<^sort>\type\)) val t = (case unprefix_and_unascii fixed_var_prefix s of SOME s => Free (s, T) | NONE => if not (is_tptp_variable s) then Free (fresh_up ctxt s, T) else Var ((repair_var_name s, var_index), T)) in list_comb (t, ts) end)) in do_term end (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}" should allow them to be inferred. *) fun term_of_atp_fo ctxt textual sym_tab = let val thy = Proof_Context.theory_of ctxt (* For Metis, we use 1 rather than 0 because variable references in clauses may otherwise conflict with variable constraints in the goal. At least, type inference often fails otherwise. See also "axiom_inference" in "Metis_Reconstruct". *) val var_index = var_index_of_textual textual fun do_term extra_ts opt_T u = (case u of ATerm ((s, tys), us) => if s = "" (* special marker generated on parse error *) then error "Isar proof reconstruction failed because the ATP proof contains unparsable \ \material" else if String.isPrefix native_type_prefix s then \<^Const>\True\ (* ignore TPTP type information (needed?) *) else if s = tptp_equal then list_comb (Const (\<^const_name>\HOL.eq\, Type_Infer.anyT \<^sort>\type\), map (do_term [] NONE) us) else (case unprefix_and_unascii const_prefix s of SOME s' => let val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const in if s' = type_tag_name then (case mangled_us @ us of [typ_u, term_u] => do_term extra_ts (SOME (typ_of_atp_term ctxt typ_u)) term_u | _ => raise ATP_TERM us) else if s' = predicator_name then do_term [] (SOME \<^typ>\bool\) (hd us) else if s' = app_op_name then let val extra_t = do_term [] NONE (List.last us) in do_term (extra_t :: extra_ts) (case opt_T of SOME T => SOME (slack_fastype_of extra_t --> T) | NONE => NONE) (nth us (length us - 2)) end else if s' = type_guard_name then \<^Const>\True\ (* ignore type predicates *) else let val new_skolem = String.isPrefix new_skolem_const_prefix s'' val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term [] NONE) term_us val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us val T = (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then if new_skolem then SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts)) else if textual then try (Sign.const_instance thy) (s', Ts) else NONE else NONE) |> (fn SOME T => T | NONE => map slack_fastype_of term_ts ---> the_default (Type_Infer.anyT \<^sort>\type\) opt_T) val t = if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T) else Const (unproxify_const s', T) in list_comb (t, term_ts @ extra_ts) end end | NONE => (* a free or schematic variable *) let val term_ts = map (do_term [] NONE) us (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse order, which is incompatible with "metis"'s new skolemizer. *) |> exists (fn pre => String.isPrefix pre s) [spass_skolem_prefix, vampire_skolem_prefix] ? rev val ts = term_ts @ extra_ts val T = (case tys of [ty] => typ_of_atp_type ctxt ty | _ => (case opt_T of SOME T => map slack_fastype_of term_ts ---> T | NONE => map slack_fastype_of ts ---> Type_Infer.anyT \<^sort>\type\)) val t = (case unprefix_and_unascii fixed_var_prefix s of SOME s => Free (s, T) | NONE => if textual andalso not (is_tptp_variable s) then Free (s |> textual ? fresh_up ctxt, T) else Var ((repair_var_name s, var_index), T)) in list_comb (t, ts) end)) in do_term [] end fun term_of_atp ctxt (ATP_Problem.THF _) type_enc = if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt) else error "Unsupported Isar reconstruction" | term_of_atp ctxt _ type_enc = if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt else error "Unsupported Isar reconstruction" fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) = if String.isPrefix class_prefix s then add_type_constraint pos (type_constraint_of_term ctxt u) #> pair \<^Const>\True\ else pair (term_of_atp ctxt format type_enc textual sym_tab (SOME \<^typ>\bool\) u) (* Update schematic type variables with detected sort constraints. It's not totally clear whether this code is necessary. *) fun repair_tvar_sorts (t, tvar_tab) = let fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) | do_type (TFree z) = TFree z fun do_term (Const (a, T)) = Const (a, do_type T) | do_term (Free (a, T)) = Free (a, do_type T) | do_term (Var (xi, T)) = Var (xi, do_type T) | do_term (t as Bound _) = t | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) | do_term (t1 $ t2) = do_term t1 $ do_term t2 in t |> not (Vartab.is_empty tvar_tab) ? do_term end (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the formula. *) fun prop_of_atp ctxt format type_enc textual sym_tab phi = let fun do_formula pos phi = (case phi of AQuant (_, [], phi) => do_formula pos phi | AQuant (q, (s, _) :: xs, phi') => do_formula pos (AQuant (q, xs, phi')) (* FIXME: TFF *) #>> quantify_over_var textual (case q of AForall => forall_of | AExists => exists_of) (repair_var_name s) dummyT | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => do_formula (pos |> c = AImplies ? not) phi1 ##>> do_formula pos phi2 #>> (case c of AAnd => s_conj | AOr => s_disj | AImplies => s_imp | AIff => s_iff | ANot => raise Fail "impossible connective") | AAtom tm => term_of_atom ctxt format type_enc textual sym_tab pos tm | _ => raise ATP_FORMULA [phi]) in repair_tvar_sorts (do_formula true phi Vartab.empty) end val unprefix_fact_number = space_implode "_" o tl o space_explode "_" fun resolve_fact facts s = (case try (unprefix fact_prefix) s of SOME s' => let val s' = s' |> unprefix_fact_number |> unascii_of in AList.lookup (op =) facts s' |> Option.map (pair s') end | NONE => NONE) fun resolve_conjecture s = (case try (unprefix conjecture_prefix) s of SOME s' => Int.fromString s' | NONE => NONE) fun resolve_facts facts = map_filter (resolve_fact facts) val resolve_conjectures = map_filter resolve_conjecture fun is_axiom_used_in_proof pred = exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) +val is_conjecture_used_in_proof = is_axiom_used_in_proof (is_some o resolve_conjecture) + fun add_fact ctxt facts ((num, ss), _, _, rule, deps) = (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse String.isPrefix satallax_tab_rule_prefix rule then insert (op =) (short_thm_name ctxt ext, (Global, General)) else I) #> (if null deps then union (op =) (resolve_facts facts (num :: ss)) else I) fun used_facts_in_atp_proof ctxt facts atp_proof = if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof [] -fun used_facts_in_unsound_atp_proof _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt facts atp_proof = - let - val used_facts = used_facts_in_atp_proof ctxt facts atp_proof - val all_global_facts = forall (fn (_, (sc, _)) => sc = Global) used_facts - val axiom_used = is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof - in - if all_global_facts andalso not axiom_used then - SOME (map fst used_facts) - else - NONE - end - val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix (* overapproximation (good enough) *) fun is_lam_lifted s = String.isPrefix fact_prefix s andalso String.isSubstring ascii_of_lam_fact_prefix s val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) fun atp_proof_prefers_lifting atp_proof = (is_axiom_used_in_proof is_combinator_def atp_proof, is_axiom_used_in_proof is_lam_lifted atp_proof) = (false, true) val is_typed_helper_name = String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix fun is_typed_helper_used_in_atp_proof atp_proof = is_axiom_used_in_proof is_typed_helper_name atp_proof fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] fun replace_dependencies_in_line old_new (name, role, t, rule, deps) = (name, role, t, rule, fold (union (op =) o replace_one_dependency old_new) deps []) fun repair_name "$true" = "c_True" | repair_name "$false" = "c_False" | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) | repair_name s = if is_tptp_equal s orelse (* seen in Vampire proofs *) (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then tptp_equal else s fun set_var_index j = map_aterms (fn Var ((s, 0), T) => Var ((s, j), T) | t => t) fun infer_formulas_types ctxt = map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT)) #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) val combinator_table = [(\<^const_name>\Meson.COMBI\, @{thm Meson.COMBI_def [abs_def]}), (\<^const_name>\Meson.COMBK\, @{thm Meson.COMBK_def [abs_def]}), (\<^const_name>\Meson.COMBB\, @{thm Meson.COMBB_def [abs_def]}), (\<^const_name>\Meson.COMBC\, @{thm Meson.COMBC_def [abs_def]}), (\<^const_name>\Meson.COMBS\, @{thm Meson.COMBS_def [abs_def]})] fun uncombine_term thy = let fun uncomb (t1 $ t2) = betapply (uncomb t1, uncomb t2) | uncomb (Abs (s, T, t)) = Abs (s, T, uncomb t) | uncomb (t as Const (x as (s, _))) = (case AList.lookup (op =) combinator_table s of SOME thm => thm |> Thm.prop_of |> specialize_type thy x |> Logic.dest_equals |> snd | NONE => t) | uncomb t = t in uncomb end fun unlift_aterm lifted (t as Const (s, _)) = if String.isPrefix lam_lifted_prefix s then (* FIXME: do something about the types *) (case AList.lookup (op =) lifted s of SOME t' => unlift_term lifted t' | NONE => t) else t | unlift_aterm _ t = t and unlift_term lifted = map_aterms (unlift_aterm lifted) fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE | termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) = let val thy = Proof_Context.theory_of ctxt val t = u |> prop_of_atp ctxt format type_enc true sym_tab |> unlift_term lifted |> uncombine_term thy |> simplify_bool in SOME (name, role, t, rule, deps) end val waldmeister_conjecture_num = "1.0.0.0" fun repair_waldmeister_endgame proof = let fun repair_tail (name, _, \<^Const>\Trueprop for t\, rule, deps) = (name, Negated_Conjecture, \<^Const>\Trueprop for \s_not t\\, rule, deps) fun repair_body [] = [] | repair_body ((line as ((num, _), _, _, _, _)) :: lines) = if num = waldmeister_conjecture_num then map repair_tail (line :: lines) else line :: repair_body lines in repair_body proof end fun map_proof_terms f (lines : ('a * 'b * 'c * 'd * 'e) list) = map2 (fn c => fn (a, b, _, d, e) => (a, b, c, d, e)) (f (map #3 lines)) lines fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab = nasty_atp_proof pool #> map_term_names_in_atp_proof repair_name #> map_filter (termify_line ctxt format type_enc lifted sym_tab) #> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop) #> local_prover = waldmeisterN ? repair_waldmeister_endgame fun unskolemize_spass_term skos = let val is_skolem_name = member (op =) skos fun find_argless_skolem (Free _ $ Var _) = NONE | find_argless_skolem (Free (x as (s, _))) = if is_skolem_name s then SOME x else NONE | find_argless_skolem (t $ u) = (case find_argless_skolem t of NONE => find_argless_skolem u | sk => sk) | find_argless_skolem (Abs (_, _, t)) = find_argless_skolem t | find_argless_skolem _ = NONE fun find_skolem_arg (Free (s, _) $ Var v) = if is_skolem_name s then SOME v else NONE | find_skolem_arg (t $ u) = (case find_skolem_arg t of NONE => find_skolem_arg u | v => v) | find_skolem_arg (Abs (_, _, t)) = find_skolem_arg t | find_skolem_arg _ = NONE fun kill_skolem_arg (t as Free (s, T) $ Var _) = if is_skolem_name s then Free (s, range_type T) else t | kill_skolem_arg (t $ u) = kill_skolem_arg t $ kill_skolem_arg u | kill_skolem_arg (Abs (s, T, t)) = Abs (s, T, kill_skolem_arg t) | kill_skolem_arg t = t fun find_var (Var v) = SOME v | find_var (t $ u) = (case find_var t of NONE => find_var u | v => v) | find_var (Abs (_, _, t)) = find_var t | find_var _ = NONE val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1) fun unskolem_inner t = (case find_argless_skolem t of SOME (x as (s, T)) => HOLogic.exists_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Free x, t))) | NONE => (case find_skolem_arg t of SOME (v as ((s, _), T)) => let val (haves, have_nots) = HOLogic.disjuncts t |> List.partition (exists_subterm (curry (op =) (Var v))) |> apply2 (fn lits => fold (curry s_disj) lits \<^term>\False\) in s_disj (HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, kill_skolem_arg haves))), unskolem_inner have_nots) end | NONE => (case find_var t of SOME (v as ((s, _), T)) => HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, t))) | NONE => t))) fun unskolem_outer (@{const Trueprop} $ t) = @{const Trueprop} $ unskolem_outer t | unskolem_outer t = unskolem_inner t in unskolem_outer end fun rename_skolem_args t = let fun add_skolem_args (Abs (_, _, t)) = add_skolem_args t | add_skolem_args t = (case strip_comb t of (Free (s, _), args as _ :: _) => if String.isPrefix spass_skolem_prefix s then insert (op =) (s, take_prefix is_Var args) else fold add_skolem_args args | (u, args as _ :: _) => fold add_skolem_args (u :: args) | _ => I) fun subst_of_skolem (sk, args) = map_index (fn (j, Var (z, T)) => (z, Var ((sk ^ "_" ^ string_of_int j, 0), T))) args val subst = maps subst_of_skolem (add_skolem_args t []) in subst_vars ([], subst) t end fun introduce_spass_skolems proof = let fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s | add_skolem _ = I (* union-find would be faster *) fun add_cycle [] = I | add_cycle ss = fold (fn s => Graph.default_node (s, ())) ss #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss]) val (input_steps, other_steps) = List.partition (null o #5) proof (* The names of the formulas are added to the Skolem constants, to ensure that formulas giving rise to several clauses are skolemized together. *) val skoXss = map (fn ((_, ss), _, t, _, _) => Term.fold_aterms add_skolem t ss) input_steps val groups0 = Graph.strong_conn (fold add_cycle skoXss Graph.empty) val groups = filter (exists (String.isPrefix spass_skolem_prefix)) groups0 val skoXss_input_steps = skoXss ~~ input_steps fun step_name_of_group skoXs = (implode skoXs, []) fun in_group group = member (op =) group o hd fun group_of skoX = find_first (fn group => in_group group skoX) groups fun new_steps (skoXss_steps : (string list * (term, 'a) atp_step) list) group = let val name = step_name_of_group group val name0 = name |>> prefix "0" val t = (case map (snd #> #3) skoXss_steps of [t] => t | ts => ts |> map (HOLogic.dest_Trueprop #> rename_skolem_args) |> Library.foldr1 s_conj |> HOLogic.mk_Trueprop) val skos = fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps [] val deps = map (snd #> #1) skoXss_steps in [(name0, Unknown, unskolemize_spass_term skos t, spass_pre_skolemize_rule, deps), (name, Unknown, t, spass_skolemize_rule, [name0])] end val sko_steps = maps (fn group => new_steps (filter (in_group group o fst) skoXss_input_steps) group) groups val old_news = map_filter (fn (skoXs, (name, _, _, _, _)) => Option.map (pair name o single o step_name_of_group) (group_of skoXs)) skoXss_input_steps val repair_deps = fold replace_dependencies_in_line old_news in input_steps @ sko_steps @ map repair_deps other_steps end fun factify_atp_proof facts hyp_ts concl_t atp_proof = let fun factify_step ((num, ss), role, t, rule, deps) = let val (ss', role', t') = (case resolve_conjectures ss of [j] => if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, close_form (nth hyp_ts j)) | _ => (case resolve_facts facts (num :: ss) of [] => (ss, if member (op =) [Definition, Lemma] role then role else Plain, t) | facts => (map fst facts, Axiom, t))) in ((num, ss'), role', t', rule, deps) end val atp_proof = map factify_step atp_proof val names = map #1 atp_proof fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num)) fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps) in map repair_deps atp_proof end fun termify_atp_abduce_candidate ctxt local_prover format type_enc pool lifted sym_tab phi = let val proof = [(("", []), Conjecture, mk_anot phi, "", [])] val new_proof = termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab proof in (case new_proof of [(_, _, phi', _, _)] => phi' | _ => error "Impossible case in termify_atp_abduce_candidate") end fun sort_top n scored_items = if n <= 0 orelse null scored_items then [] else let fun split_min accum [] (_, best_item) = (best_item, List.rev accum) | split_min accum ((score, item) :: scored_items) (best_score, best_item) = if score < best_score then split_min ((best_score, best_item) :: accum) scored_items (score, item) else split_min ((score, item) :: accum) scored_items (best_score, best_item) val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items) in min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items) |> distinct (op aconv) end fun top_abduce_candidates max_candidates candidates = let (* We prefer free variables to other constructs, so that e.g. "x \ y" is prioritized over "x \ 0". *) fun score t = Term.fold_aterms (fn t => fn score => score + (case t of Free _ => 1 | _ => 2)) t 0 (* Equations of the form "x = ..." or "... = x" or similar are too specific to be useful. Quantified formulas are also filtered out. As for "True", it may seem an odd choice for abduction, but it sometimes arises in conjunction with type class constraints, which are removed by the termifier. *) fun maybe_score t = (case t of @{prop True} => NONE | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE | @{const Trueprop} $ (@{const less_eq(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const one_class.one(nat)}) => NONE | @{const Trueprop} $ (@{const Not} $ (@{const less(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE | @{const Trueprop} $ (@{const Not} $ (@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE | @{const Trueprop} $ (@{const Not} $ (@{const less_eq(nat)} $ @{const one_class.one(nat)} $ _)) => NONE | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE | _ => SOME (score t, t)) in sort_top max_candidates (map_filter maybe_score candidates) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer.ML b/src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML @@ -1,598 +1,598 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Sledgehammer's heart. *) signature SLEDGEHAMMER = sig type stature = ATP_Problem_Generate.stature type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type induction_rules = Sledgehammer_Prover.induction_rules type prover_problem = Sledgehammer_Prover.prover_problem type prover_result = Sledgehammer_Prover.prover_result type preplay_result = proof_method * (play_outcome * (string * stature) list) datatype sledgehammer_outcome = SH_Some of prover_result * preplay_result list | SH_Unknown | SH_TimeOut | SH_ResourcesOut | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> Proof.state -> bool * (sledgehammer_outcome * string) end; structure Sledgehammer : SLEDGEHAMMER = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Minimize open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh type preplay_result = proof_method * (play_outcome * (string * stature) list) datatype sledgehammer_outcome = SH_Some of prover_result * preplay_result list | SH_Unknown | SH_TimeOut | SH_ResourcesOut | SH_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" | short_string_of_sledgehammer_outcome SH_TimeOut = "timeout" | short_string_of_sledgehammer_outcome SH_ResourcesOut = "resources_out" | short_string_of_sledgehammer_outcome SH_None = "none" fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) | alternative _ (x as SOME _) NONE = x | alternative _ NONE (y as SOME _) = y | alternative _ NONE NONE = NONE fun varify_nonfixed_terms_global nonfixeds tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Free (x, T) => if member (op =) nonfixeds x then Var ((x, 0), T) else raise Same.SAME | Var (xi, _) => raise TERM (Logic.bad_schematic xi, [tm]) | _ => raise Same.SAME)) fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_TimeOut, _) => true | _ => false) outcomes val resources_out = find_first (fn (SH_ResourcesOut, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in some |> alternative snd unknown |> alternative snd timeout |> alternative snd resources_out |> alternative snd none |> the_default (SH_Unknown, "") end fun play_one_line_proofs minimize timeout used_facts state goal i methss = (if timeout = Time.zeroTime then [] else let val ctxt = Proof.context_of state val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts val fact_names = map fst used_facts val {facts = chained, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i fun try_methss ress [] = ress | try_methss ress (meths :: methss) = let fun mk_step meths = Prove { qualifiers = [], obtains = [], label = ("", 0), goal = goal_t, subproofs = [], facts = ([], fact_names), proof_methods = meths, comment = ""} val ress' = preplay_isar_step ctxt chained timeout [] (mk_step meths) |> map (fn (meth, play_outcome) => (case (minimize, play_outcome) of (true, Played time) => let val (time', used_names') = minimized_isar_step ctxt chained time (mk_step [meth]) ||> (facts_of_isar_step #> snd) val used_facts' = filter (member (op =) used_names' o fst) used_facts in (meth, Played time', used_facts') end | _ => (meth, play_outcome, used_facts))) val any_succeeded = exists (fn (_, Played _, _) => true | _ => false) ress' in try_methss (ress' @ ress) (if any_succeeded then [] else methss) end in try_methss [] methss end) |> map (fn (meth, play_outcome, used_facts) => (meth, (play_outcome, filter_out (fn (_, (sc, _)) => sc = Chained) used_facts))) |> sort (play_outcome_ord o apply2 (fn (_, (play_outcome, _)) => play_outcome)) fun select_one_line_proof used_facts preferred_meth preplay_results = (case preplay_results of (* Select best method if preplay succeeded *) (best_meth, (best_outcome as Played _, best_used_facts)) :: _ => (best_used_facts, (best_meth, best_outcome)) (* Otherwise select preferred method *) | _ => (used_facts, (preferred_meth, (case AList.lookup (op =) preplay_results preferred_meth of SOME (outcome, _) => outcome | NONE => Play_Timed_Out Time.zeroTime)))) |> apfst (filter_out (fn (_, (sc, _)) => sc = Chained)) fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) (slice as ((slice_size, abduce, falsify, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched" ^ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else ""))) val _ = if verbose then writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "") ^ "...") else () fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas |> prefix ("Facts in " ^ name ^ " " ^ (if falsify then "falsification" else "proof") ^ ": ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = let val num_used_facts = length used_facts fun find_indices facts = tag_list 1 facts |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) fun filter_info (fact_filter, facts) = let val indices = find_indices facts (* "Int.max" is there for robustness *) val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" in (commas (indices @ unknowns), fact_filter) end val filter_infos = map filter_info (("actual", used_from) :: factss) |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in "Success: Found " ^ (if falsify then "falsification" else "proof") ^ " with " ^ string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure in get_minimizing_prover ctxt mode learn name params problem slice |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) end fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state goal subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = let val (output, chosen_preplay_outcome) = if outcome = SOME ATP_Proof.TimedOut then (SH_TimeOut, select_one_line_proof used_facts (fst preferred_methss) []) else if outcome = SOME ATP_Proof.OutOfResources then (SH_ResourcesOut, select_one_line_proof used_facts (fst preferred_methss) []) else if is_some outcome then (SH_None, select_one_line_proof used_facts (fst preferred_methss) []) else let val preplay_results = play_one_line_proofs minimize preplay_timeout used_facts state goal subgoal (snd preferred_methss) val chosen_preplay_outcome = select_one_line_proof used_facts (fst preferred_methss) preplay_results in (SH_Some (result, preplay_results), chosen_preplay_outcome) end fun output_message () = message (fn () => chosen_preplay_outcome) in (output, output_message) end fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) = if outcome = SOME ATP_Proof.TimedOut then (SH_TimeOut, K "") else if outcome = SOME ATP_Proof.OutOfResources then (SH_ResourcesOut, K "") else if is_some outcome then (SH_None, K "") else (SH_Some (result, []), fn () => (if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then (case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of [] => "The goal is inconsistent" | facts => "The goal is falsified by these facts: " ^ commas facts) else - "The following facts are inconsistent: " ^ + "Derived \"False\" from these facts alone: " ^ commas (map fst used_facts))) fun check_expected_outcome ctxt prover_name expect outcome = let val outcome_code = short_string_of_sledgehammer_outcome outcome in (* The "expect" argument is deliberately ignored if the prover is missing so that "Metis_Examples" can be processed on any machine. *) if expect = "" orelse not (is_prover_installed ctxt prover_name) then () else (case (expect, outcome) of ("some", SH_Some _) => () | ("some_preplayed", SH_Some (_, preplay_results)) => if exists (fn (_, (Played _, _)) => true | _ => false) preplay_results then () else error ("Unexpected outcome: the external prover found a proof but preplay failed") | ("unknown", SH_Unknown) => () | ("timeout", SH_TimeOut) => () | ("resources_out", SH_ResourcesOut) => () | ("none", SH_None) => () | _ => error ("Unexpected outcome: " ^ quote outcome_code)) end fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode has_already_found_something found_something writeln_result learn (problem as {state, subgoal, ...}) (slice as ((_, _, falsify, _, _), _)) prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout fun flip_problem {comment, state, goal, subgoal, factss = factss, ...} = let val thy = Proof_Context.theory_of ctxt val assms = Assumption.all_assms_of ctxt val assm_ts = map Thm.term_of assms val subgoal_t = Logic.get_goal (Thm.prop_of goal) subgoal val polymorphic_subgoal_t = (Logic.list_implies (assm_ts, subgoal_t)) |> Logic.varify_global val nonfixeds = subtract (op =) (fold Term.add_free_names assm_ts []) (Term.add_free_names subgoal_t []) val monomorphic_subgoal_t = subgoal_t |> varify_nonfixed_terms_global nonfixeds val subgoal_thms = map (Skip_Proof.make_thm thy) [polymorphic_subgoal_t, monomorphic_subgoal_t] val new_facts = map (fn thm => (((sledgehammer_goal_as_fact, (Assum, General)), thm))) subgoal_thms in {comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1, subgoal_count = 1, factss = map (apsnd (append new_facts)) factss, has_already_found_something = has_already_found_something, found_something = found_something "an inconsistency"} end val problem as {goal, ...} = problem |> falsify ? flip_problem fun really_go () = launch_prover params mode learn problem slice prover_name |> (if falsify then analyze_prover_result_for_inconsistency else preplay_prover_result params state goal subgoal) fun go () = if debug then really_go () else (really_go () handle ERROR msg => (SH_Unknown, fn () => msg ^ "\n") | exn => if Exn.is_interrupt exn then Exn.reraise exn else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n")) val (outcome, message) = Timeout.apply hard_timeout go () val () = check_expected_outcome ctxt prover_name expect outcome val message = message () val () = if mode = Auto_Try then () else (case outcome of SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message) | _ => ()) in (outcome, message) end fun string_of_facts filter facts = "Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^ "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts)) fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss) val default_slice_schedule = (* FUDGE (loosely inspired by Seventeen evaluation) *) [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN, cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, zipperpositionN] fun schedule_of_provers provers num_slices = let val (known_provers, unknown_provers) = List.partition (member (op =) default_slice_schedule) provers val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule val num_default_slices = length default_slice_schedule fun round_robin _ [] = [] | round_robin 0 _ = [] | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover]) in if num_slices <= num_default_slices then take num_slices default_slice_schedule else default_slice_schedule @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers) end fun prover_slices_of_schedule ctxt goal subgoal factss ({abduce, falsify, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule = let fun triplicate_slices original = let val shift = map (apfst (fn (slice_size, abduce, falsify, num_facts, fact_filter) => (slice_size, abduce, falsify, num_facts, if fact_filter = mashN then mepoN else if fact_filter = mepoN then meshN else mashN))) val shifted_once = shift original val shifted_twice = shift shifted_once in original @ shifted_once @ shifted_twice end fun adjust_extra (ATP_Slice (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0)) = ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans, the_default uncurried_aliases0 uncurried_aliases, extra_extra0) | adjust_extra (extra as SMT_Slice _) = extra fun adjust_slice max_slice_size ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) val abduce = (case abduce of NONE => abduce0 andalso goal_not_False | SOME max_candidates => max_candidates > 0) val falsify = (case falsify of NONE => falsify0 andalso goal_not_False | SOME falsify => falsify) val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss)) in ((slice_size, abduce, falsify, num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule val prover_slices = map (fn prover => (prover, (is_none fact_filter ? triplicate_slices) (get_slices ctxt prover))) provers val max_threads = Multithreading.max_threads () fun translate_schedule _ 0 _ = [] | translate_schedule _ _ [] = [] | translate_schedule prover_slices slices_left (prover :: schedule) = (case AList.lookup (op =) prover_slices prover of SOME (slice0 :: slices) => let val prover_slices' = AList.update (op =) (prover, slices) prover_slices val slice as ((slice_size, _, _, _, _), _) = adjust_slice ((slices_left + max_threads - 1) div max_threads) slice0 in (prover, slice) :: translate_schedule prover_slices' (slices_left - slice_size) schedule end | _ => translate_schedule prover_slices slices_left schedule) in translate_schedule prover_slices (length schedule) schedule |> distinct (op =) end fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts, max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" else (case subgoal_count state of 0 => (error "No subgoal!"; (false, (SH_None, ""))) | n => let val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () val found_proofs_and_falsifications = Synchronized.var "found_proofs_and_falsifications" 0 fun has_already_found_something () = if mode = Normal then Synchronized.value found_proofs_and_falsifications > 0 else false fun found_something a_proof_or_inconsistency prover_name = if mode = Normal then (Synchronized.change found_proofs_and_falsifications (fn n => n + 1); (the_default writeln writeln_result) (prover_name ^ " found " ^ a_proof_or_inconsistency ^ "...")) else () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate val {facts = chained_thms, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) val ({elapsed, ...}, all_facts) = Timing.timing (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t val _ = spying spy (fn () => (state, i, "All", "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) fun get_factss provers = let val max_max_facts = (case max_facts of SOME n => n | NONE => fold (fn prover => fold (fn ((_, _, _, max_facts, _), _) => Integer.max max_facts) (get_slices ctxt prover)) provers 0) * 51 div 50 (* some slack to account for filtering of induction facts below *) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) all_facts val induction_rules = the_default (if only then Include else Exclude) induction_rules val factss = map (apsnd (maybe_filter_out_induction_rules induction_rules)) factss val () = spying spy (fn () => (state, i, "All", "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); val () = if verbose then print (string_of_factss factss) else () val () = spying spy (fn () => (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)) in factss end fun launch_provers () = let val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss, has_already_found_something = has_already_found_something, found_something = found_something "a proof"} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode has_already_found_something found_something writeln_result learn val schedule = if mode = Auto_Try then provers else schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt goal i factss params schedule val _ = if verbose then writeln ("Running " ^ commas (map fst prover_slices) ^ "...") else () in if mode = Auto_Try then (SH_Unknown, "") |> fold (fn (prover, slice) => fn accum as (SH_Some _, _) => accum | _ => launch problem slice prover) prover_slices else (learn chained_thms; Par_List.map (fn (prover, slice) => if Synchronized.value found_proofs_and_falsifications < max_proofs then launch problem slice prover else (SH_None, "")) prover_slices |> max_outcome) end fun normal_failure () = (the_default writeln writeln_result ("No " ^ (if falsify = SOME true then "falsification" else "proof") ^ " found"); false) in (launch_provers () handle Timeout.TIMEOUT _ => (SH_TimeOut, "")) |> `(fn (outcome, message) => (case outcome of SH_Some _ => (the_default writeln writeln_result "Done"; true) | SH_Unknown => if message = "" then normal_failure () else (the_default writeln writeln_result ("Warning: " ^ message); false) | SH_TimeOut => normal_failure () | SH_ResourcesOut => normal_failure () | SH_None => if message = "" then normal_failure () else (the_default writeln writeln_result ("Warning: " ^ message); false))) end) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,372 +1,371 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_problem_dest_dir : string Config.T val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_problem_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_dest_dir\ (K "") val atp_proof_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_proof_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun choose_type_enc strictness format good_type_enc = type_enc_of_string strictness good_type_enc |> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^Const_>\Trueprop for t1\) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^Const_>\Pure.imp for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^Const_>\implies for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^Const>\False\ orelse do_formula pos t2) | (_, \<^Const_>\Not for t1\) => do_formula (not pos) t1 | (true, \<^Const_>\disj for t1 t2\) => forall (do_formula pos) [t1, t2] | (false, \<^Const_>\conj for t1 t2\) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Important messages are important but not so important that users want to see them each time. *) val important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, has_already_found_something, found_something} : prover_problem) slice = let val (basic_slice as (slice_size, abduce, _, _, _), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = slice val facts = facts_of_basic_slice basic_slice factss val thy = Proof.theory_of state val ctxt = Proof.context_of state val {exec, arguments, proof_delims, known_failures, prem_role, generate_isabelle_info, good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (problem_dest_dir, proof_dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name |> (fn (dir, prefix) => (dir, dir, prefix)) else (Config.get ctxt atp_problem_dest_dir, Config.get ctxt atp_proof_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |> Path.ext "p" val prob_path = if problem_dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode problem_dest_dir) then Path.explode problem_dest_dir + problem_file_name else error ("No such directory: " ^ quote problem_dest_dir) val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun run () = let fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances good_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end val strictness = if strict then Strict else Non_Strict val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slice_size slices timeout val generous_run_timeout = if mode = MaSh then one_day else if abduce then run_timeout + seconds 5.0 else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val readable_names = not (Config.get ctxt atp_full_names) in facts |> not (is_type_enc_sound type_enc) ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_isabelle_info good_format prem_role type_enc atp_mode good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () => (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val args = arguments abduce full_proofs extra run_timeout prob_path val command = space_implode " " (File.bash_path executable :: args) fun run_command () = if exec = isabelle_scala_function then let val {output, timing} = SystemOnTPTP.run_system_encoded args in (output, timing) end else let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = atp_problem |> lines_of_atp_problem good_format (fn () => atp_problem_term_order_info atp_problem) |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val local_name = name |> perhaps (try (unprefix remote_prefix)) val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) = Timeout.apply generous_run_timeout run_command () |>> overlord ? (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> `(atp_proof_of_tstplike_proof false local_name atp_problem) handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg))) val atp_abduce_candidates = if abduce andalso outcome <> NONE andalso not (has_already_found_something ()) then atp_abduce_candidates_of_output local_name atp_problem output else [] val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) val outcome = (case outcome of - NONE => - (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of - SOME facts => - let - val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) - in - if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure - end - | NONE => (found_something name; NONE)) + NONE => (found_something name; NONE) | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates, outcome), (good_format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = Path.split_ext #> apfst (Path.explode o suffix "_proof" o Path.implode) #> swap #> uncurry Path.ext in if proof_dest_dir = "" then Output.system_message "don't export proof" else if File.exists proof_dest_dir_path then File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output else error ("No such directory: " ^ quote proof_dest_dir) end val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (outcome, used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) + val _ = + if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof) + andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then + warning ("Derived \"False\" from these facts alone: " ^ commas (map fst used_facts)) + else + () + val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred = Metis_Method (NONE, NONE) val preferred_methss = (preferred, if try0 then bunches_of_proof_methods ctxt smt_proofs needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN) else [[preferred]]) in (NONE, used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val full_atp_proof = atp_proof_of_tstplike_proof true (perhaps (try (unprefix remote_prefix)) name) atp_problem tstplike_proof val metis_type_enc = if is_typed_helper_used_in_atp_proof full_atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting full_atp_proof then SOME liftingN else NONE val full_atp_proof = full_atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> local_name = spassN ? introduce_spass_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize, full_atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") end) end | SOME failure => let val max_abduce_candidates = the_default default_abduce_max_candidates abduce_max_candidates val abduce_candidates = atp_abduce_candidates |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab) |> top_abduce_candidates max_abduce_candidates in if null abduce_candidates then (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure) else (NONE, [], (Auto_Method (* dummy *), []), fn _ => abduce_text ctxt abduce_candidates) end) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;